let n be Nat; :: thesis: for x, y being FinSequence
for p being set holds
( n -BitMajorityOutput (x,y) <> [p,'&'] & n -BitMajorityOutput (x,y) <> [p,'xor'] )
let x, y be FinSequence; :: thesis: for p being set holds
( n -BitMajorityOutput (x,y) <> [p,'&'] & n -BitMajorityOutput (x,y) <> [p,'xor'] )
let p be set ; :: thesis: ( n -BitMajorityOutput (x,y) <> [p,'&'] & n -BitMajorityOutput (x,y) <> [p,'xor'] )
A1: dom '&' = 2 -tuples_on BOOLEAN by FUNCT_2:def 1;
A2: dom 'xor' = 2 -tuples_on BOOLEAN by FUNCT_2:def 1;
A3: proj1 ([p,'&'] `2) = 2 -tuples_on BOOLEAN by A1;
A4: proj1 ([p,'xor'] `2) = 2 -tuples_on BOOLEAN by A2;
( proj1 ((n -BitMajorityOutput (x,y)) `2) = 0 -tuples_on BOOLEAN or proj1 ((n -BitMajorityOutput (x,y)) `2) = 3 -tuples_on BOOLEAN ) by Th24;
hence ( n -BitMajorityOutput (x,y) <> [p,'&'] & n -BitMajorityOutput (x,y) <> [p,'xor'] ) by A3, A4, FINSEQ_2:110; :: thesis: verum