let x, y, z be set ; ( x in the carrier of (BitGFA3Str (x,y,z)) & y in the carrier of (BitGFA3Str (x,y,z)) & z in the carrier of (BitGFA3Str (x,y,z)) & [<*x,y*>,xor2] in the carrier of (BitGFA3Str (x,y,z)) & [<*[<*x,y*>,xor2],z*>,xor2] in the carrier of (BitGFA3Str (x,y,z)) & [<*x,y*>,nor2] in the carrier of (BitGFA3Str (x,y,z)) & [<*y,z*>,nor2] in the carrier of (BitGFA3Str (x,y,z)) & [<*z,x*>,nor2] in the carrier of (BitGFA3Str (x,y,z)) & [<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3] in the carrier of (BitGFA3Str (x,y,z)) )
set f1 = nor2 ;
set f2 = nor2 ;
set f3 = nor2 ;
set f4 = nor3 ;
set f0 = xor2 ;
set xy = [<*x,y*>,nor2];
set yz = [<*y,z*>,nor2];
set zx = [<*z,x*>,nor2];
set xyz = [<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3];
set S1 = GFA3AdderStr (x,y,z);
set S2 = GFA3CarryStr (x,y,z);
A1:
( x in the carrier of (GFA3AdderStr (x,y,z)) & y in the carrier of (GFA3AdderStr (x,y,z)) )
by FACIRC_1:60;
A2:
( z in the carrier of (GFA3AdderStr (x,y,z)) & [<*x,y*>,xor2] in the carrier of (GFA3AdderStr (x,y,z)) )
by FACIRC_1:60, FACIRC_1:61;
A3:
[<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3] in the carrier of (GFA3CarryStr (x,y,z))
by Th111;
A4:
( [<*y,z*>,nor2] in the carrier of (GFA3CarryStr (x,y,z)) & [<*z,x*>,nor2] in the carrier of (GFA3CarryStr (x,y,z)) )
by Th111;
( [<*[<*x,y*>,xor2],z*>,xor2] in the carrier of (GFA3AdderStr (x,y,z)) & [<*x,y*>,nor2] in the carrier of (GFA3CarryStr (x,y,z)) )
by Th111, FACIRC_1:61;
hence
( x in the carrier of (BitGFA3Str (x,y,z)) & y in the carrier of (BitGFA3Str (x,y,z)) & z in the carrier of (BitGFA3Str (x,y,z)) & [<*x,y*>,xor2] in the carrier of (BitGFA3Str (x,y,z)) & [<*[<*x,y*>,xor2],z*>,xor2] in the carrier of (BitGFA3Str (x,y,z)) & [<*x,y*>,nor2] in the carrier of (BitGFA3Str (x,y,z)) & [<*y,z*>,nor2] in the carrier of (BitGFA3Str (x,y,z)) & [<*z,x*>,nor2] in the carrier of (BitGFA3Str (x,y,z)) & [<*[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]*>,nor3] in the carrier of (BitGFA3Str (x,y,z)) )
by A1, A2, A4, A3, FACIRC_1:20; verum