:: deftheorem defines GFA0CarryCirc GFACIRC1:def 8 :
for x, y, z being set holds GFA0CarryCirc (x,y,z) = (GFA0CarryICirc (x,y,z)) +* (1GateCircuit ([<*x,y*>,and2],[<*y,z*>,and2],[<*z,x*>,and2],or3));