theorem Th21: :: GFACIRC2:21

for n being Nat
for x, y being FinSequence holds
( (n + 1) -BitGFA1Str (x,y) = (n -BitGFA1Str (x,y)) +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y)))) & (n + 1) -BitGFA1Circ (x,y) = (n -BitGFA1Circ (x,y)) +* (BitGFA1Circ ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y)))) & (n + 1) -BitGFA1CarryOutput (x,y) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y))) )