let n be Nat; :: thesis: for ap, bp, cp, dp being FinSequence holds InnerVertices ((n + 1) -BitFTA0Layer2Str (ap,bp,cp,dp)) = (InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp))) \/ (InnerVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)))),(n -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (n + 1)))))
let ap, bp, cp, dp be FinSequence; :: thesis: InnerVertices ((n + 1) -BitFTA0Layer2Str (ap,bp,cp,dp)) = (InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp))) \/ (InnerVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)))),(n -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (n + 1)))))
set B = BitGFA0Str ((GFA0AdderOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)))),(n -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (n + 1)));
reconsider S1 = n -BitFTA0Layer2Str (ap,bp,cp,dp) as non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;
thus InnerVertices ((n + 1) -BitFTA0Layer2Str (ap,bp,cp,dp)) = InnerVertices (S1 +* (BitGFA0Str ((GFA0AdderOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)))),(n -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (n + 1))))) by LmT05B
.= (InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp))) \/ (InnerVertices (BitGFA0Str ((GFA0AdderOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)))),(n -BitFTA0CarryOutput (ap,bp,cp,dp)),(dp . (n + 1))))) by FACIRC_1:27 ; :: thesis: verum