let a, b, c be non pair set ; :: thesis: for X, Y, d being set st Y is pair holds
not GFA0AdderOutput (a,b,c) in InnerVertices (BitGFA0Str (X,Y,d))
let X, Y, d be set ; :: thesis: ( Y is pair implies not GFA0AdderOutput (a,b,c) in InnerVertices (BitGFA0Str (X,Y,d)) )
assume A1: Y is pair ; :: thesis: not GFA0AdderOutput (a,b,c) in InnerVertices (BitGFA0Str (X,Y,d))
set w = GFA0AdderOutput (a,b,c);
set bA = GFA0AdderOutput (X,Y,d);
set bC = GFA0CarryOutput (X,Y,d);
assume GFA0AdderOutput (a,b,c) in InnerVertices (BitGFA0Str (X,Y,d)) ; :: thesis: contradiction
then GFA0AdderOutput (a,b,c) in (({[<*X,Y*>,xor2]} \/ {(GFA0AdderOutput (X,Y,d))}) \/ {[<*X,Y*>,and2],[<*Y,d*>,and2],[<*d,X*>,and2]}) \/ {(GFA0CarryOutput (X,Y,d))} by GFACIRC1:31;
then ( GFA0AdderOutput (a,b,c) in ({[<*X,Y*>,xor2]} \/ {(GFA0AdderOutput (X,Y,d))}) \/ {[<*X,Y*>,and2],[<*Y,d*>,and2],[<*d,X*>,and2]} or GFA0AdderOutput (a,b,c) in {(GFA0CarryOutput (X,Y,d))} ) by XBOOLE_0:def 3;
then ( GFA0AdderOutput (a,b,c) in {[<*X,Y*>,xor2]} \/ {(GFA0AdderOutput (X,Y,d))} or GFA0AdderOutput (a,b,c) in {[<*X,Y*>,and2],[<*Y,d*>,and2],[<*d,X*>,and2]} or GFA0AdderOutput (a,b,c) in {(GFA0CarryOutput (X,Y,d))} ) by XBOOLE_0:def 3;
then A2: ( GFA0AdderOutput (a,b,c) in {[<*X,Y*>,xor2]} or GFA0AdderOutput (a,b,c) in {(GFA0AdderOutput (X,Y,d))} or GFA0AdderOutput (a,b,c) in {[<*X,Y*>,and2],[<*Y,d*>,and2],[<*d,X*>,and2]} or GFA0AdderOutput (a,b,c) in {(GFA0CarryOutput (X,Y,d))} ) by XBOOLE_0:def 3;

per cases ( GFA0AdderOutput (a,b,c) = [<*X,Y*>,xor2] or GFA0AdderOutput (a,b,c) = GFA0AdderOutput (X,Y,d) or GFA0AdderOutput (a,b,c) = [<*X,Y*>,and2] or GFA0AdderOutput (a,b,c) = [<*Y,d*>,and2] or GFA0AdderOutput (a,b,c) = [<*d,X*>,and2] or GFA0AdderOutput (a,b,c) = GFA0CarryOutput (X,Y,d) ) by A2, TARSKI:def 1, ENUMSET1:def 1;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

suppose GFA0AdderOutput (a,b,c) = GFA0CarryOutput (X,Y,d) ; :: thesis: contradiction

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

end;

end;