theorem Th17: :: GFACIRC2:17

for a, b being FinSequence
for c being set st c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] holds
( 1 -BitGFA1Str (a,b) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Str ((a . 1),(b . 1),c)) & 1 -BitGFA1Circ (a,b) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Circ ((a . 1),(b . 1),c)) & 1 -BitGFA1CarryOutput (a,b) = GFA1CarryOutput ((a . 1),(b . 1),c) )