theorem Th2: :: FSCIRC_2:2

for a, b being FinSequence holds
( 0 -BitSubtracterStr (a,b) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & 0 -BitSubtracterCirc (a,b) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & 0 -BitBorrowOutput (a,b) = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] )