let n be Nat; :: thesis: for ap, bm, cp, dm being FinSequence holds InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm)) is Relation
let ap, bm, cp, dm be FinSequence; :: thesis: InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm)) is Relation
deffunc H₁( Nat) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign = $1 -BitFTA1Layer2Str (ap,bm,cp,dm);
defpred S₁[ Nat] means InnerVertices H₁($1) is Relation;
H₁( 0 ) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) by LmT10L2;
then A1: S₁[ 0 ] by FACIRC_1:38;

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

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume B1: S₁[i] ; :: thesis: S₁[i + 1]
B2: H₁(i + 1) = H₁(i) +* (BitGFA2Str ((GFA1AdderOutput ((ap . (i + 1)),(bm . (i + 1)),(cp . (i + 1)))),(i -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (i + 1)))) by LmT15B;
InnerVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (i + 1)),(bm . (i + 1)),(cp . (i + 1)))),(i -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (i + 1)))) is Relation by GFACIRC1:96;
hence S₁[i + 1] by B1, B2, FACIRC_1:3; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A2);
hence InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm)) is Relation ; :: thesis: verum