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

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

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

then <*[<*a,b*>,and2c],[<*b,c*>,and2a],[<*c,a*>,and2]*> = <*[<*X,Y*>,and2a],[<*Y,d*>,and2c],[<*d,X*>,nor2]*> by XTUPLE_0:1;
then [<*b,c*>,and2a] = [<*Y,d*>,and2c] by FINSEQ_1:78;
then <*b,c*> = <*Y,d*> by XTUPLE_0:1;
hence contradiction by A1, FINSEQ_1:77; :: thesis: verum

end;

end;