let a, b, c be non pair set ; :: thesis: for X, Y, d being set st Y is pair holds
not GFA1AdderOutput (a,b,c) in InnerVertices (BitGFA2Str (X,Y,d))
let X, Y, d be set ; :: thesis: ( Y is pair implies not GFA1AdderOutput (a,b,c) in InnerVertices (BitGFA2Str (X,Y,d)) )
assume A1: Y is pair ; :: thesis: not GFA1AdderOutput (a,b,c) in InnerVertices (BitGFA2Str (X,Y,d))
set w = GFA1AdderOutput (a,b,c);
set bA = GFA2AdderOutput (X,Y,d);
set bC = GFA2CarryOutput (X,Y,d);
assume GFA1AdderOutput (a,b,c) in InnerVertices (BitGFA2Str (X,Y,d)) ; :: thesis: contradiction
then GFA1AdderOutput (a,b,c) in (({[<*X,Y*>,xor2c]} \/ {(GFA2AdderOutput (X,Y,d))}) \/ {[<*X,Y*>,and2a],[<*Y,d*>,and2c],[<*d,X*>,nor2]}) \/ {(GFA2CarryOutput (X,Y,d))} by GFACIRC1:95;
then ( GFA1AdderOutput (a,b,c) in ({[<*X,Y*>,xor2c]} \/ {(GFA2AdderOutput (X,Y,d))}) \/ {[<*X,Y*>,and2a],[<*Y,d*>,and2c],[<*d,X*>,nor2]} or GFA1AdderOutput (a,b,c) in {(GFA2CarryOutput (X,Y,d))} ) by XBOOLE_0:def 3;
then ( GFA1AdderOutput (a,b,c) in {[<*X,Y*>,xor2c]} \/ {(GFA2AdderOutput (X,Y,d))} or GFA1AdderOutput (a,b,c) in {[<*X,Y*>,and2a],[<*Y,d*>,and2c],[<*d,X*>,nor2]} or GFA1AdderOutput (a,b,c) in {(GFA2CarryOutput (X,Y,d))} ) by XBOOLE_0:def 3;
then A2: ( GFA1AdderOutput (a,b,c) in {[<*X,Y*>,xor2c]} or GFA1AdderOutput (a,b,c) in {(GFA2AdderOutput (X,Y,d))} or GFA1AdderOutput (a,b,c) in {[<*X,Y*>,and2a],[<*Y,d*>,and2c],[<*d,X*>,nor2]} or GFA1AdderOutput (a,b,c) in {(GFA2CarryOutput (X,Y,d))} ) by XBOOLE_0:def 3;

per cases ( GFA1AdderOutput (a,b,c) = [<*X,Y*>,xor2c] or GFA1AdderOutput (a,b,c) = GFA2AdderOutput (X,Y,d) or GFA1AdderOutput (a,b,c) = [<*X,Y*>,and2a] or GFA1AdderOutput (a,b,c) = [<*Y,d*>,and2c] or GFA1AdderOutput (a,b,c) = [<*d,X*>,nor2] or GFA1AdderOutput (a,b,c) = GFA2CarryOutput (X,Y,d) ) by A2, TARSKI:def 1, ENUMSET1:def 1;

suppose GFA1AdderOutput (a,b,c) = [<*X,Y*>,xor2c] ; :: thesis: contradiction

then <*[<*a,b*>,xor2c],c*> = <*X,Y*> by XTUPLE_0:1;
hence contradiction by A1, FINSEQ_1:77; :: thesis: verum

end;

suppose GFA1AdderOutput (a,b,c) = GFA2AdderOutput (X,Y,d) ; :: thesis: contradiction

then <*[<*a,b*>,xor2c],c*> = <*[<*X,Y*>,xor2c],d*> by XTUPLE_0:1;
then B1: [<*a,b*>,xor2c] = [<*X,Y*>,xor2c] by FINSEQ_1:77;
<*a,b*> = <*X,Y*> by B1, XTUPLE_0:1;
hence contradiction by A1, FINSEQ_1:77; :: thesis: verum

end;

suppose GFA1AdderOutput (a,b,c) = [<*X,Y*>,and2a] ; :: thesis: contradiction

hence contradiction by GFACIRC1:4, TWOSCOMP:9, XTUPLE_0:1; :: thesis: verum

end;

suppose GFA1AdderOutput (a,b,c) = [<*Y,d*>,and2c] ; :: thesis: contradiction

hence contradiction by GFACIRC1:4, GFACIRC1:3, XTUPLE_0:1; :: thesis: verum

end;

suppose GFA1AdderOutput (a,b,c) = [<*d,X*>,nor2] ; :: thesis: contradiction

hence contradiction by GFACIRC1:4, TWOSCOMP:9, XTUPLE_0:1; :: thesis: verum

end;

suppose GFA1AdderOutput (a,b,c) = GFA2CarryOutput (X,Y,d) ; :: thesis: contradiction

then B1: <*[<*a,b*>,xor2c],c*> = <*[<*X,Y*>,and2a],[<*Y,d*>,and2c],[<*d,X*>,nor2]*> by XTUPLE_0:1;
len <*[<*a,b*>,xor2c],c*> = 2 by FINSEQ_1:44;
hence contradiction by B1, FINSEQ_1:45; :: thesis: verum

end;

end;