theorem :: GFACIRC2:6

for n being Nat
for x, y being FinSeqLen of n
for a, b being set holds
( (n + 1) -BitGFA0Str ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitGFA0Str (x,y)) +* (BitGFA0Str (a,b,(n -BitGFA0CarryOutput (x,y)))) & (n + 1) -BitGFA0Circ ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitGFA0Circ (x,y)) +* (BitGFA0Circ (a,b,(n -BitGFA0CarryOutput (x,y)))) & (n + 1) -BitGFA0CarryOutput ((x ^ <*a*>),(y ^ <*b*>)) = GFA0CarryOutput (a,b,(n -BitGFA0CarryOutput (x,y))) )