theorem :: GFACIRC2:23

for n being Nat
for x, y being FinSequence holds InnerVertices ((n + 1) -BitGFA1Str (x,y)) = (InnerVertices (n -BitGFA1Str (x,y))) \/ (InnerVertices (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y)))))