theorem Th12:
for
n being
Nat for
x,
y being
FinSequence holds
(
(n + 1) -BitAdderStr (
x,
y)
= (n -BitAdderStr (x,y)) +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y)))) &
(n + 1) -BitAdderCirc (
x,
y)
= (n -BitAdderCirc (x,y)) +* (BitAdderWithOverflowCirc ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y)))) &
(n + 1) -BitMajorityOutput (
x,
y)
= MajorityOutput (
(x . (n + 1)),
(y . (n + 1)),
(n -BitMajorityOutput (x,y))) )