theorem Th3: :: FTACELL2:3

for n being Nat
for ap, bp, cp, dp being FinSequence holds
( (n + 1) -BitFTA0Str (ap,bp,cp,dp) = (n -BitFTA0Str (ap,bp,cp,dp)) +* (BitFTA0Str ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),(n -BitFTA0CarryOutput (ap,bp,cp,dp)))) & (n + 1) -BitFTA0Circ (ap,bp,cp,dp) = (n -BitFTA0Circ (ap,bp,cp,dp)) +* (BitFTA0Circ ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),(n -BitFTA0CarryOutput (ap,bp,cp,dp)))) & (n + 1) -BitFTA0CarryOutput (ap,bp,cp,dp) = BitFTA0CarryOutput ((ap . (n + 1)),(bp . (n + 1)),(cp . (n + 1)),(dp . (n + 1)),(n -BitFTA0CarryOutput (ap,bp,cp,dp))) )