let n be Nat; :: thesis: for ap, bm, cp, dm being nonpair-yielding FinSequence
for w being set holds
( not w in InputVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm)) or not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) )
let ap, bm, cp, dm be nonpair-yielding FinSequence; :: thesis: for w being set holds
( not w in InputVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm)) or not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) )
set c0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)];
defpred S₁[ Nat] means for w being set holds
( not w in InputVertices ($1 -BitFTA1Layer2Str (ap,bm,cp,dm)) or not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) );
A1: S₁[ 0 ]

proof

let w be set ; :: thesis: ( not w in InputVertices (0 -BitFTA1Layer2Str (ap,bm,cp,dm)) or not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) )
assume B1: w in InputVertices (0 -BitFTA1Layer2Str (ap,bm,cp,dm)) ; :: thesis: ( not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) )
0 -BitFTA1Layer2Str (ap,bm,cp,dm) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) by LmT10L2;
then InputVertices (0 -BitFTA1Layer2Str (ap,bm,cp,dm)) = rng <*> by CIRCCOMB:42
.= {} ;
hence ( not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) ) by B1; :: thesis: verum

end;

A2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume B1: S₁[i] ; :: thesis: S₁[i + 1]
set X = GFA1AdderOutput ((ap . (i + 1)),(bm . (i + 1)),(cp . (i + 1)));
set Y = i -BitFTA1CarryOutput (ap,bm,cp,dm);
set d = dm . (i + 1);
set B = BitGFA2Str ((GFA1AdderOutput ((ap . (i + 1)),(bm . (i + 1)),(cp . (i + 1)))),(i -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (i + 1)));
set S1 = i -BitFTA1Layer2Str (ap,bm,cp,dm);
B2: (i + 1) -BitFTA1Layer2Str (ap,bm,cp,dm) = (i -BitFTA1Layer2Str (ap,bm,cp,dm)) +* (BitGFA2Str ((GFA1AdderOutput ((ap . (i + 1)),(bm . (i + 1)),(cp . (i + 1)))),(i -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (i + 1)))) by LmT15B;
B3: InputVertices ((i -BitFTA1Layer2Str (ap,bm,cp,dm)) +* (BitGFA2Str ((GFA1AdderOutput ((ap . (i + 1)),(bm . (i + 1)),(cp . (i + 1)))),(i -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (i + 1))))) = ((InputVertices (i -BitFTA1Layer2Str (ap,bm,cp,dm))) \ (InnerVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (i + 1)),(bm . (i + 1)),(cp . (i + 1)))),(i -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (i + 1)))))) \/ ((InputVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (i + 1)),(bm . (i + 1)),(cp . (i + 1)))),(i -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (i + 1))))) \ (InnerVertices (i -BitFTA1Layer2Str (ap,bm,cp,dm)))) by CIRCCOMB:47, CIRCCMB2:5;
B4: InputVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (i + 1)),(bm . (i + 1)),(cp . (i + 1)))),(i -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (i + 1)))) = {(GFA1AdderOutput ((ap . (i + 1)),(bm . (i + 1)),(cp . (i + 1)))),(i -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (i + 1))} by LmT1C2i;
let w be set ; :: thesis: ( not w in InputVertices ((i + 1) -BitFTA1Layer2Str (ap,bm,cp,dm)) or not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) )
assume B5: w in InputVertices ((i + 1) -BitFTA1Layer2Str (ap,bm,cp,dm)) ; :: thesis: ( not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) )

per cases ( w in (InputVertices (i -BitFTA1Layer2Str (ap,bm,cp,dm))) \ (InnerVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (i + 1)),(bm . (i + 1)),(cp . (i + 1)))),(i -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (i + 1))))) or w in (InputVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (i + 1)),(bm . (i + 1)),(cp . (i + 1)))),(i -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (i + 1))))) \ (InnerVertices (i -BitFTA1Layer2Str (ap,bm,cp,dm))) ) by B5, B2, B3, XBOOLE_0:def 3;

suppose w in (InputVertices (i -BitFTA1Layer2Str (ap,bm,cp,dm))) \ (InnerVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (i + 1)),(bm . (i + 1)),(cp . (i + 1)))),(i -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (i + 1))))) ; :: thesis: ( not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) )

then w in InputVertices (i -BitFTA1Layer2Str (ap,bm,cp,dm)) by XBOOLE_0:def 5;
hence ( not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) ) by B1; :: thesis: verum

end;

suppose B6: w in (InputVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (i + 1)),(bm . (i + 1)),(cp . (i + 1)))),(i -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (i + 1))))) \ (InnerVertices (i -BitFTA1Layer2Str (ap,bm,cp,dm))) ; :: thesis: ( not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) )

then C1: w in {(GFA1AdderOutput ((ap . (i + 1)),(bm . (i + 1)),(cp . (i + 1)))),(i -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (i + 1))} by B4, XBOOLE_0:def 5;

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

suppose C2: w = GFA1AdderOutput ((ap . (i + 1)),(bm . (i + 1)),(cp . (i + 1))) ; :: thesis: ( not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) )

thus ( not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) ) by C2; :: thesis: verum

end;

suppose C3: w = i -BitFTA1CarryOutput (ap,bm,cp,dm) ; :: thesis: ( not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) )

per cases ( i = 0 or ex m being Nat st i = m + 1 ) by NAT_1:6;

suppose D1: i = 0 ; :: thesis: ( not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) )

E1: not w in InnerVertices (i -BitFTA1Layer2Str (ap,bm,cp,dm)) by B6, XBOOLE_0:def 5;
w = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] by C3, D1, LmT10CO;
hence ( not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) ) by LmT1Cin0In, E1; :: thesis: verum

end;

suppose ex m being Nat st i = m + 1 ; :: thesis: ( not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) )

then consider m being Nat such that
E1: i = m + 1 ;
reconsider u1 = ap . (m + 1), v1 = bm . (m + 1), x1 = cp . (m + 1) as non pair set ;
w = GFA1CarryOutput (u1,v1,x1) by C3, E1, LmT1COk;
hence ( not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) ) ; :: thesis: verum

end;

end;

end;

suppose w = dm . (i + 1) ; :: thesis: ( not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) )

hence ( not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) ) ; :: thesis: verum

end;

end;

end;

end;

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A2);
hence for w being set holds
( not w in InputVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm)) or not w is pair or ex u, v, x being non pair set st w = GFA1AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA1CarryOutput (u,v,x) ) ; :: thesis: verum