theorem Th12: :: GFACIRC2:12

for f, g being nonpair-yielding FinSequence
for n being Nat holds
( InputVertices ((n + 1) -BitGFA0Str (f,g)) = (InputVertices (n -BitGFA0Str (f,g))) \/ ((InputVertices (BitGFA0Str ((f . (n + 1)),(g . (n + 1)),(n -BitGFA0CarryOutput (f,g))))) \ {(n -BitGFA0CarryOutput (f,g))}) & InnerVertices (n -BitGFA0Str (f,g)) is Relation & InputVertices (n -BitGFA0Str (f,g)) is without_pairs )