theorem Th14: :: FTACELL2:14

for n being Nat
for ap, bm, cp, dm being FinSequence holds
( (n + 1) -BitFTA1Str (ap,bm,cp,dm) = (n -BitFTA1Str (ap,bm,cp,dm)) +* (BitFTA1Str ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),(n -BitFTA1CarryOutput (ap,bm,cp,dm)))) & (n + 1) -BitFTA1Circ (ap,bm,cp,dm) = (n -BitFTA1Circ (ap,bm,cp,dm)) +* (BitFTA1Circ ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),(n -BitFTA1CarryOutput (ap,bm,cp,dm)))) & (n + 1) -BitFTA1CarryOutput (ap,bm,cp,dm) = BitFTA1CarryOutput ((ap . (n + 1)),(bm . (n + 1)),(cp . (n + 1)),(dm . (n + 1)),(n -BitFTA1CarryOutput (ap,bm,cp,dm))) )