theorem :: FSCIRC_2:4

for a, b, 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) )