let n be Nat; :: thesis: for ap, bm, cp, dm being FinSequence holds [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] in InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm))
let ap, bm, cp, dm be FinSequence; :: thesis: [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] in InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm))
set c0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)];
defpred S₁[ Nat] means [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] in InnerVertices ($1 -BitFTA1Layer2Str (ap,bm,cp,dm));
0 -BitFTA1Layer2Str (ap,bm,cp,dm) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) by LmT10L2;
then InnerVertices (0 -BitFTA1Layer2Str (ap,bm,cp,dm)) = {[<*>,((0 -tuples_on BOOLEAN) --> FALSE)]} by CIRCCOMB:42;
then A1: S₁[ 0 ] by TARSKI:def 1;
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 S₁[i] ; :: thesis: S₁[i + 1]
then [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] in (InnerVertices (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))))) by XBOOLE_0:def 3;
hence S₁[i + 1] by LmT1L2inner; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A2);
hence [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] in InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm)) ; :: thesis: verum