theorem :: GFACIRC1:68

for x, y, z being set holds
( x in the carrier of (BitGFA1Str (x,y,z)) & y in the carrier of (BitGFA1Str (x,y,z)) & z in the carrier of (BitGFA1Str (x,y,z)) & [<*x,y*>,xor2c] in the carrier of (BitGFA1Str (x,y,z)) & [<*[<*x,y*>,xor2c],z*>,xor2c] in the carrier of (BitGFA1Str (x,y,z)) & [<*x,y*>,and2c] in the carrier of (BitGFA1Str (x,y,z)) & [<*y,z*>,and2a] in the carrier of (BitGFA1Str (x,y,z)) & [<*z,x*>,and2] in the carrier of (BitGFA1Str (x,y,z)) & [<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3] in the carrier of (BitGFA1Str (x,y,z)) )