let n be Nat; :: thesis: for ap, bm, cp, dm being FinSequence holds InnerVertices ((n + 1) -BitFTA1Layer2Str (ap,bm,cp,dm)) = (InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm))) \/ (InnerVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)))),(n -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (n + 1)))))
let ap, bm, cp, dm be FinSequence; :: thesis: InnerVertices ((n + 1) -BitFTA1Layer2Str (ap,bm,cp,dm)) = (InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm))) \/ (InnerVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)))),(n -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (n + 1)))))
set B = BitGFA2Str ((GFA1AdderOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)))),(n -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (n + 1)));
reconsider S1 = n -BitFTA1Layer2Str (ap,bm,cp,dm) as non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;
thus InnerVertices ((n + 1) -BitFTA1Layer2Str (ap,bm,cp,dm)) = InnerVertices (S1 +* (BitGFA2Str ((GFA1AdderOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)))),(n -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (n + 1))))) by LmT15B
.= (InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm))) \/ (InnerVertices (BitGFA2Str ((GFA1AdderOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)))),(n -BitFTA1CarryOutput (ap,bm,cp,dm)),(dm . (n + 1))))) by FACIRC_1:27 ; :: thesis: verum