theorem :: GFACIRC2:4

for a, b, c being set st c = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] holds
( 1 -BitGFA0Str (<*a*>,<*b*>) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) +* (BitGFA0Str (a,b,c)) & 1 -BitGFA0Circ (<*a*>,<*b*>) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) +* (BitGFA0Circ (a,b,c)) & 1 -BitGFA0CarryOutput (<*a*>,<*b*>) = GFA0CarryOutput (a,b,c) )