let x, y, z be set ; :: thesis: for p being set holds GFA2AdderOutput (x,y,z) <> [p,and2a]
let p be set ; :: thesis: GFA2AdderOutput (x,y,z) <> [p,and2a]
set A1 = GFA2AdderOutput (x,y,z);
(GFA2AdderOutput (x,y,z)) `2 = xor2c ;
then [p,and2a] `2 <> (GFA2AdderOutput (x,y,z)) `2 by GFACIRC1:4, TWOSCOMP:9;
hence GFA2AdderOutput (x,y,z) <> [p,and2a] ; :: thesis: verum