:: deftheorem defines GFA2AdderStr GFACIRC1:def 34 :
for x, y, z being set holds GFA2AdderStr (x,y,z) = 2GatesCircStr (x,y,z,xor2c);