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