let k be Nat; :: thesis: for ap, bp, cp, dp being nonpair-yielding FinSequence holds InputVertices (k -BitFTA0Layer2Str (ap,bp,cp,dp)) misses InnerVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))))
let ap, bp, cp, dp be nonpair-yielding FinSequence; :: thesis: InputVertices (k -BitFTA0Layer2Str (ap,bp,cp,dp)) misses InnerVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))))
set X = GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)));
set Y = k -BitFTA0CarryOutput (ap,bp,cp,dp);
set d = dp . (k + 1);
set B = BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)));
set bA = GFA0AdderOutput ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)));
set bC = GFA0CarryOutput ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)));
A1: k -BitFTA0CarryOutput (ap,bp,cp,dp) is pair by LmT0COp;
assume InputVertices (k -BitFTA0Layer2Str (ap,bp,cp,dp)) meets InnerVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))) ; :: thesis: contradiction
then consider w being object such that
A2: w in InputVertices (k -BitFTA0Layer2Str (ap,bp,cp,dp)) and
A3: w in InnerVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1)))) by XBOOLE_0:3;
reconsider w = w as set by TARSKI:1;

per cases ( not w is pair or ex u, v, x being non pair set st w = GFA0AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA0CarryOutput (u,v,x) ) by A2, LmT0InAcc;

suppose A4: not w is pair ; :: thesis: contradiction

w in (({[<*(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp))*>,xor2]} \/ {(GFA0AdderOutput ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))))}) \/ {[<*(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp))*>,and2],[<*(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))*>,and2],[<*(dp . (k + 1)),(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))))*>,and2]}) \/ {(GFA0CarryOutput ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))))} by A3, GFACIRC1:31;
then ( w in ({[<*(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp))*>,xor2]} \/ {(GFA0AdderOutput ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))))}) \/ {[<*(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp))*>,and2],[<*(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))*>,and2],[<*(dp . (k + 1)),(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))))*>,and2]} or w in {(GFA0CarryOutput ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))))} ) by XBOOLE_0:def 3;
then ( w in {[<*(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp))*>,xor2]} \/ {(GFA0AdderOutput ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))))} or w in {[<*(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp))*>,and2],[<*(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))*>,and2],[<*(dp . (k + 1)),(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))))*>,and2]} or w in {(GFA0CarryOutput ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))))} ) by XBOOLE_0:def 3;
then B1: ( w in {[<*(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp))*>,xor2]} or w in {(GFA0AdderOutput ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))))} or w in {[<*(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp))*>,and2],[<*(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))*>,and2],[<*(dp . (k + 1)),(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))))*>,and2]} or w in {(GFA0CarryOutput ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))))} ) by XBOOLE_0:def 3;

per cases ( w = [<*(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp))*>,xor2] or w = GFA0AdderOutput ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))) or w = [<*(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp))*>,and2] or w = [<*(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))*>,and2] or w = [<*(dp . (k + 1)),(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))))*>,and2] or w = GFA0CarryOutput ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))) ) by B1, TARSKI:def 1, ENUMSET1:def 1;

suppose w = [<*(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp))*>,xor2] ; :: thesis: contradiction

hence contradiction by A4; :: thesis: verum

end;

suppose w = GFA0AdderOutput ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))) ; :: thesis: contradiction

hence contradiction by A4; :: thesis: verum

end;

suppose w = [<*(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp))*>,and2] ; :: thesis: contradiction

hence contradiction by A4; :: thesis: verum

end;

suppose w = [<*(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))*>,and2] ; :: thesis: contradiction

hence contradiction by A4; :: thesis: verum

end;

suppose w = [<*(dp . (k + 1)),(GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1))))*>,and2] ; :: thesis: contradiction

hence contradiction by A4; :: thesis: verum

end;

suppose w = GFA0CarryOutput ((GFA0AdderOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))),(k -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (k + 1))) ; :: thesis: contradiction

hence contradiction by A4; :: thesis: verum

end;

end;

end;

suppose ex u, v, x being non pair set st w = GFA0AdderOutput (u,v,x) ; :: thesis: contradiction

then consider u, v, x being non pair set such that
B1: w = GFA0AdderOutput (u,v,x) ;
thus contradiction by A3, B1, A1, LmT0W1; :: thesis: verum

end;

suppose ex u, v, x being non pair set st w = GFA0CarryOutput (u,v,x) ; :: thesis: contradiction

then consider u, v, x being non pair set such that
B1: w = GFA0CarryOutput (u,v,x) ;
thus contradiction by A3, B1, A1, LmT0W2; :: thesis: verum

end;

end;