let x, y, z be set ; for p being set holds GFA1AdderOutput (x,y,z) <> [p,and2c]
let p be set ; GFA1AdderOutput (x,y,z) <> [p,and2c]
set A1 = GFA1AdderOutput (x,y,z);
(GFA1AdderOutput (x,y,z)) `2 = xor2c
;
then
[p,and2c] `2 <> (GFA1AdderOutput (x,y,z)) `2
by GFACIRC1:3, GFACIRC1:4;
hence
GFA1AdderOutput (x,y,z) <> [p,and2c]
; verum