theorem Th8: :: FACIRC_2:8

for a, b being FinSequence
for c being set st c = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] holds
( 1 -BitAdderStr (a,b) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) +* (BitAdderWithOverflowStr ((a . 1),(b . 1),c)) & 1 -BitAdderCirc (a,b) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) +* (BitAdderWithOverflowCirc ((a . 1),(b . 1),c)) & 1 -BitMajorityOutput (a,b) = MajorityOutput ((a . 1),(b . 1),c) )