theorem Th7:
for
n being
Nat for
x,
y being
FinSequence holds
(
(n + 1) -BitGFA0Str (
x,
y)
= (n -BitGFA0Str (x,y)) +* (BitGFA0Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y)))) &
(n + 1) -BitGFA0Circ (
x,
y)
= (n -BitGFA0Circ (x,y)) +* (BitGFA0Circ ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y)))) &
(n + 1) -BitGFA0CarryOutput (
x,
y)
= GFA0CarryOutput (
(x . (n + 1)),
(y . (n + 1)),
(n -BitGFA0CarryOutput (x,y))) )