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

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

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

then <*[<*a,b*>,and2],[<*b,c*>,and2],[<*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 GFA0CarryOutput (a,b,c) = GFA0AdderOutput (X,Y,d) ; :: thesis: contradiction

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

end;

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

then <*[<*a,b*>,and2],[<*b,c*>,and2],[<*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 GFA0CarryOutput (a,b,c) = [<*Y,d*>,and2] ; :: thesis: contradiction

then <*[<*a,b*>,and2],[<*b,c*>,and2],[<*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 GFA0CarryOutput (a,b,c) = [<*d,X*>,and2] ; :: thesis: contradiction

then <*[<*a,b*>,and2],[<*b,c*>,and2],[<*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 GFA0CarryOutput (a,b,c) = GFA0CarryOutput (X,Y,d) ; :: thesis: contradiction

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

end;

end;