for n being Nat
for x, y being FinSequence
for p being set holds
( n -BitBorrowOutput (x,y) <> [p,and2] & n -BitBorrowOutput (x,y) <> [p,and2a] & n -BitBorrowOutput (x,y) <> [p,'xor'] )