theorem Th7: :: FACIRC_2:7

for a, b being FinSequence holds
( 0 -BitAdderStr (a,b) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & 0 -BitAdderCirc (a,b) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & 0 -BitMajorityOutput (a,b) = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] )