:: deftheorem defines GFA0AdderStr GFACIRC1:def 10 :
for x, y, z being set holds GFA0AdderStr (x,y,z) = 2GatesCircStr (x,y,z,xor2);