theorem Th6:
for
x,
y being
FinSequence for
f,
g,
h being
ManySortedSet of
NAT st
f . 0 = 1GateCircStr (
<*>,
((0 -tuples_on BOOLEAN) --> FALSE)) &
g . 0 = 1GateCircuit (
<*>,
((0 -tuples_on BOOLEAN) --> FALSE)) &
h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for
n being
Nat for
S being non
empty ManySortedSign for
A being
non-empty MSAlgebra over
S for
z being
set st
S = f . n &
A = g . n &
z = h . n holds
(
f . (n + 1) = S +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),z)) &
g . (n + 1) = A +* (BitAdderWithOverflowCirc ((x . (n + 1)),(y . (n + 1)),z)) &
h . (n + 1) = MajorityOutput (
(x . (n + 1)),
(y . (n + 1)),
z) ) ) holds
for
n being
Nat holds
(
n -BitAdderStr (
x,
y)
= f . n &
n -BitAdderCirc (
x,
y)
= g . n &
n -BitMajorityOutput (
x,
y)
= h . n )