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