let m be Nat; :: thesis: for ap, bm, cp, dm being nonpair-yielding FinSequence holds InputVertices (BitGFA2Str ((GFA1AdderOutput ((ap . ((m + 1) + 1)),(bm . ((m + 1) + 1)),(cp . ((m + 1) + 1)))),((m + 1) -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . ((m + 1) + 1)))) misses InnerVertices ((m + 1) -BitFTA1Layer2Str (ap,bm,cp,dm))
let ap, bm, cp, dm be nonpair-yielding FinSequence; :: thesis: InputVertices (BitGFA2Str ((GFA1AdderOutput ((ap . ((m + 1) + 1)),(bm . ((m + 1) + 1)),(cp . ((m + 1) + 1)))),((m + 1) -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . ((m + 1) + 1)))) misses InnerVertices ((m + 1) -BitFTA1Layer2Str (ap,bm,cp,dm))
set X = GFA1AdderOutput ((ap . ((m + 1) + 1)),(bm . ((m + 1) + 1)),(cp . ((m + 1) + 1)));
set Y = (m + 1) -BitFTA1CarryOutput (ap,bm,cp,dm);
set d = dm . ((m + 1) + 1);
set B = BitGFA2Str ((GFA1AdderOutput ((ap . ((m + 1) + 1)),(bm . ((m + 1) + 1)),(cp . ((m + 1) + 1)))),((m + 1) -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . ((m + 1) + 1)));
set L2 = (m + 1) -BitFTA1Layer2Str (ap,bm,cp,dm);
A1: InputVertices (BitGFA2Str ((GFA1AdderOutput ((ap . ((m + 1) + 1)),(bm . ((m + 1) + 1)),(cp . ((m + 1) + 1)))),((m + 1) -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . ((m + 1) + 1)))) = {(GFA1AdderOutput ((ap . ((m + 1) + 1)),(bm . ((m + 1) + 1)),(cp . ((m + 1) + 1)))),((m + 1) -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . ((m + 1) + 1))} by LmT1C2i;
assume InputVertices (BitGFA2Str ((GFA1AdderOutput ((ap . ((m + 1) + 1)),(bm . ((m + 1) + 1)),(cp . ((m + 1) + 1)))),((m + 1) -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . ((m + 1) + 1)))) meets InnerVertices ((m + 1) -BitFTA1Layer2Str (ap,bm,cp,dm)) ; :: thesis: contradiction
then consider w being object such that
A2: w in InputVertices (BitGFA2Str ((GFA1AdderOutput ((ap . ((m + 1) + 1)),(bm . ((m + 1) + 1)),(cp . ((m + 1) + 1)))),((m + 1) -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . ((m + 1) + 1)))) and
A3: w in InnerVertices ((m + 1) -BitFTA1Layer2Str (ap,bm,cp,dm)) by XBOOLE_0:3;

per cases ( w = GFA1AdderOutput ((ap . ((m + 1) + 1)),(bm . ((m + 1) + 1)),(cp . ((m + 1) + 1))) or w = (m + 1) -BitFTA1CarryOutput (ap,bm,cp,dm) or w = dm . ((m + 1) + 1) ) by A2, A1, ENUMSET1:def 1;

suppose w = GFA1AdderOutput ((ap . ((m + 1) + 1)),(bm . ((m + 1) + 1)),(cp . ((m + 1) + 1))) ; :: thesis: contradiction

hence contradiction by A3, LmT1WnI; :: thesis: verum

end;

suppose A5: w = (m + 1) -BitFTA1CarryOutput (ap,bm,cp,dm) ; :: thesis: contradiction

reconsider u1 = ap . (m + 1), v1 = bm . (m + 1), x1 = cp . (m + 1) as non pair set ;
not GFA1CarryOutput (u1,v1,x1) in InnerVertices ((m + 1) -BitFTA1Layer2Str (ap,bm,cp,dm)) by LmT1WnI;
hence contradiction by A5, LmT1COk, A3; :: thesis: verum

end;

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

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

end;

end;