let a, b be set ; :: thesis: for c being set st c = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] holds
( 1 -BitAdderStr (<*a*>,<*b*>) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) +* (BitAdderWithOverflowStr (a,b,c)) & 1 -BitAdderCirc (<*a*>,<*b*>) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) +* (BitAdderWithOverflowCirc (a,b,c)) & 1 -BitMajorityOutput (<*a*>,<*b*>) = MajorityOutput (a,b,c) )
A1: <*a*> . 1 = a by FINSEQ_1:40;
<*b*> . 1 = b by FINSEQ_1:40;
hence for c being set st c = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] holds
( 1 -BitAdderStr (<*a*>,<*b*>) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) +* (BitAdderWithOverflowStr (a,b,c)) & 1 -BitAdderCirc (<*a*>,<*b*>) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) +* (BitAdderWithOverflowCirc (a,b,c)) & 1 -BitMajorityOutput (<*a*>,<*b*>) = MajorityOutput (a,b,c) ) by A1, Th9; :: thesis: verum