let n be Nat; :: thesis: for ap, bp, cp, dp being nonpair-yielding FinSequence
for w being set holds
( not w in InputVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp)) or 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) )
let ap, bp, cp, dp be nonpair-yielding FinSequence; :: thesis: for w being set holds
( not w in InputVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp)) or 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) )
set c0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)];
defpred S₁[ Nat] means for w being set holds
( not w in InputVertices ($1 -BitFTA0Layer2Str (ap,bp,cp,dp)) or 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) );
A1: S₁[ 0 ]

proof

let w be set ; :: thesis: ( not w in InputVertices (0 -BitFTA0Layer2Str (ap,bp,cp,dp)) or 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) )
assume B1: w in InputVertices (0 -BitFTA0Layer2Str (ap,bp,cp,dp)) ; :: thesis: ( 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) )
0 -BitFTA0Layer2Str (ap,bp,cp,dp) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) by LmT00L2;
then InputVertices (0 -BitFTA0Layer2Str (ap,bp,cp,dp)) = rng <*> by CIRCCOMB:42
.= {} ;
hence ( 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 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 = GFA0AdderOutput ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)));
set Y = i -BitFTA0CarryOutput (ap,bp,cp,dp);
set d = dp . (i + 1);
set B = BitGFA0Str ((GFA0AdderOutput ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)))),(i -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (i + 1)));
set S1 = i -BitFTA0Layer2Str (ap,bp,cp,dp);
B2: (i + 1) -BitFTA0Layer2Str (ap,bp,cp,dp) = (i -BitFTA0Layer2Str (ap,bp,cp,dp)) +* (BitGFA0Str ((GFA0AdderOutput ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)))),(i -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (i + 1)))) by LmT05B;
B3: InputVertices ((i -BitFTA0Layer2Str (ap,bp,cp,dp)) +* (BitGFA0Str ((GFA0AdderOutput ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)))),(i -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (i + 1))))) = ((InputVertices (i -BitFTA0Layer2Str (ap,bp,cp,dp))) \ (InnerVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)))),(i -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (i + 1)))))) \/ ((InputVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)))),(i -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (i + 1))))) \ (InnerVertices (i -BitFTA0Layer2Str (ap,bp,cp,dp)))) by CIRCCOMB:47, CIRCCMB2:5;
B4: InputVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)))),(i -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (i + 1)))) = {(GFA0AdderOutput ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)))),(i -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (i + 1))} by LmT0C2i;
let w be set ; :: thesis: ( not w in InputVertices ((i + 1) -BitFTA0Layer2Str (ap,bp,cp,dp)) or 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) )
assume B5: w in InputVertices ((i + 1) -BitFTA0Layer2Str (ap,bp,cp,dp)) ; :: thesis: ( 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) )

per cases ( w in (InputVertices (i -BitFTA0Layer2Str (ap,bp,cp,dp))) \ (InnerVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)))),(i -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (i + 1))))) or w in (InputVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)))),(i -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (i + 1))))) \ (InnerVertices (i -BitFTA0Layer2Str (ap,bp,cp,dp))) ) by B5, B2, B3, XBOOLE_0:def 3;

suppose w in (InputVertices (i -BitFTA0Layer2Str (ap,bp,cp,dp))) \ (InnerVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)))),(i -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (i + 1))))) ; :: thesis: ( 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) )

then w in InputVertices (i -BitFTA0Layer2Str (ap,bp,cp,dp)) by XBOOLE_0:def 5;
hence ( 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 B1; :: thesis: verum

end;

suppose B6: w in (InputVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)))),(i -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (i + 1))))) \ (InnerVertices (i -BitFTA0Layer2Str (ap,bp,cp,dp))) ; :: thesis: ( 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) )

then C1: w in {(GFA0AdderOutput ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)))),(i -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (i + 1))} by B4, XBOOLE_0:def 5;

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

suppose C2: w = GFA0AdderOutput ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1))) ; :: thesis: ( 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) )

thus ( 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 C2; :: thesis: verum

end;

suppose C3: w = i -BitFTA0CarryOutput (ap,bp,cp,dp) ; :: thesis: ( 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) )

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 = GFA0AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA0CarryOutput (u,v,x) )

E1: not w in InnerVertices (i -BitFTA0Layer2Str (ap,bp,cp,dp)) by B6, XBOOLE_0:def 5;
w = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] by C3, D1, LmT00CO;
hence ( 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 LmT0Cin0In, 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 = GFA0AdderOutput (u,v,x) or ex u, v, x being non pair set st w = GFA0CarryOutput (u,v,x) )

then consider m being Nat such that
E1: i = m + 1 ;
reconsider u1 = ap . (m + 1), v1 = bp . (m + 1), x1 = cp . (m + 1) as non pair set ;
w = GFA0CarryOutput (u1,v1,x1) by C3, E1, LmT0COk;
hence ( 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) ) ; :: thesis: verum

end;

end;

end;

suppose w = dp . (i + 1) ; :: thesis: ( 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) )

hence ( 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) ) ; :: 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 -BitFTA0Layer2Str (ap,bp,cp,dp)) or 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) ) ; :: thesis: verum