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:57;
<*b*> . 1 = b by FINSEQ_1:57;
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