let m be Nat; :: thesis: for ap, bp, cp, dp being nonpair-yielding FinSequence holds InputVertices (BitGFA0Str ((GFA0AdderOutput ((ap . ((m + 1) + 1)),(bp . ((m + 1) + 1)),(cp . ((m + 1) + 1)))),((m + 1) -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . ((m + 1) + 1)))) misses InnerVertices ((m + 1) -BitFTA0Layer2Str (ap,bp,cp,dp))
let ap, bp, cp, dp be nonpair-yielding FinSequence; :: thesis: InputVertices (BitGFA0Str ((GFA0AdderOutput ((ap . ((m + 1) + 1)),(bp . ((m + 1) + 1)),(cp . ((m + 1) + 1)))),((m + 1) -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . ((m + 1) + 1)))) misses InnerVertices ((m + 1) -BitFTA0Layer2Str (ap,bp,cp,dp))
set X = GFA0AdderOutput ((ap . ((m + 1) + 1)),(bp . ((m + 1) + 1)),(cp . ((m + 1) + 1)));
set Y = (m + 1) -BitFTA0CarryOutput (ap,bp,cp,dp);
set d = dp . ((m + 1) + 1);
set B = BitGFA0Str ((GFA0AdderOutput ((ap . ((m + 1) + 1)),(bp . ((m + 1) + 1)),(cp . ((m + 1) + 1)))),((m + 1) -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . ((m + 1) + 1)));
set L2 = (m + 1) -BitFTA0Layer2Str (ap,bp,cp,dp);
A1: InputVertices (BitGFA0Str ((GFA0AdderOutput ((ap . ((m + 1) + 1)),(bp . ((m + 1) + 1)),(cp . ((m + 1) + 1)))),((m + 1) -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . ((m + 1) + 1)))) = {(GFA0AdderOutput ((ap . ((m + 1) + 1)),(bp . ((m + 1) + 1)),(cp . ((m + 1) + 1)))),((m + 1) -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . ((m + 1) + 1))} by LmT0C2i;
assume InputVertices (BitGFA0Str ((GFA0AdderOutput ((ap . ((m + 1) + 1)),(bp . ((m + 1) + 1)),(cp . ((m + 1) + 1)))),((m + 1) -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . ((m + 1) + 1)))) meets InnerVertices ((m + 1) -BitFTA0Layer2Str (ap,bp,cp,dp)) ; :: thesis: contradiction
then consider w being object such that
A2: w in InputVertices (BitGFA0Str ((GFA0AdderOutput ((ap . ((m + 1) + 1)),(bp . ((m + 1) + 1)),(cp . ((m + 1) + 1)))),((m + 1) -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . ((m + 1) + 1)))) and
A3: w in InnerVertices ((m + 1) -BitFTA0Layer2Str (ap,bp,cp,dp)) by XBOOLE_0:3;

per cases ( w = GFA0AdderOutput ((ap . ((m + 1) + 1)),(bp . ((m + 1) + 1)),(cp . ((m + 1) + 1))) or w = (m + 1) -BitFTA0CarryOutput (ap,bp,cp,dp) or w = dp . ((m + 1) + 1) ) by A2, A1, ENUMSET1:def 1;

suppose A4: w = GFA0AdderOutput ((ap . ((m + 1) + 1)),(bp . ((m + 1) + 1)),(cp . ((m + 1) + 1))) ; :: thesis: contradiction

thus contradiction by A4, A3, LmT0WnI; :: thesis: verum

end;

suppose A5: w = (m + 1) -BitFTA0CarryOutput (ap,bp,cp,dp) ; :: thesis: contradiction

reconsider u1 = ap . (m + 1), v1 = bp . (m + 1), x1 = cp . (m + 1) as non pair set ;
not GFA0CarryOutput (u1,v1,x1) in InnerVertices ((m + 1) -BitFTA0Layer2Str (ap,bp,cp,dp)) by LmT0WnI;
hence contradiction by A5, LmT0COk, A3; :: thesis: verum

end;

suppose A6: w = dp . ((m + 1) + 1) ; :: thesis: contradiction

reconsider d1 = dp . ((m + 1) + 1) as non pair set ;
B1: {d1} misses InnerVertices ((m + 1) -BitFTA0Layer2Str (ap,bp,cp,dp)) by LmT0L2rel, FACIRC_1:5;
d1 in {d1} by TARSKI:def 1;
then d1 in {d1} /\ (InnerVertices ((m + 1) -BitFTA0Layer2Str (ap,bp,cp,dp))) by A6, A3, XBOOLE_0:def 4;
hence contradiction by B1, XBOOLE_0:def 7; :: thesis: verum

end;

end;