let x, y, z be set ; :: thesis: for p being set holds GFA3AdderOutput (x,y,z) <> [p,nor2]
let p be set ; :: thesis: GFA3AdderOutput (x,y,z) <> [p,nor2]
set A1 = GFA3AdderOutput (x,y,z);
(GFA3AdderOutput (x,y,z)) `2 = xor2 ;
then [p,nor2] `2 <> (GFA3AdderOutput (x,y,z)) `2 by TWOSCOMP:9, TWOSCOMP:11;
hence GFA3AdderOutput (x,y,z) <> [p,nor2] ; :: thesis: verum