let a, b be set ; :: thesis: for c being set st c = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] holds
( 1 -BitSubtracterStr <*a*>,<*b*> = (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) +* (BitSubtracterWithBorrowStr a,b,c) & 1 -BitSubtracterCirc <*a*>,<*b*> = (1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) +* (BitSubtracterWithBorrowCirc a,b,c) & 1 -BitBorrowOutput <*a*>,<*b*> = BorrowOutput a,b,c )
( <*a*> . 1 = a & <*b*> . 1 = b ) by FINSEQ_1:57;
hence for c being set st c = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] holds
( 1 -BitSubtracterStr <*a*>,<*b*> = (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) +* (BitSubtracterWithBorrowStr a,b,c) & 1 -BitSubtracterCirc <*a*>,<*b*> = (1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) +* (BitSubtracterWithBorrowCirc a,b,c) & 1 -BitBorrowOutput <*a*>,<*b*> = BorrowOutput a,b,c ) by Th3; :: thesis: verum