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*>,and2b ] in the carrier of (BitGFA3Str x,y,z) & [<*y,z*>,and2b ] in the carrier of (BitGFA3Str x,y,z) & [<*z,x*>,and2b ] in the carrier of (BitGFA3Str x,y,z) & [<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ] in the carrier of (BitGFA3Str x,y,z) )
set f1 = and2b ;
set f2 = and2b ;
set f3 = and2b ;
set f4 = nor3 ;
set f0 = xor2 ;
set xy = [<*x,y*>,and2b ];
set yz = [<*y,z*>,and2b ];
set zx = [<*z,x*>,and2b ];
set xyz = [<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,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*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ] in the carrier of (GFA3CarryStr x,y,z)
by Th129;
A4:
( [<*y,z*>,and2b ] in the carrier of (GFA3CarryStr x,y,z) & [<*z,x*>,and2b ] in the carrier of (GFA3CarryStr x,y,z) )
by Th129;
( [<*[<*x,y*>,xor2 ],z*>,xor2 ] in the carrier of (GFA3AdderStr x,y,z) & [<*x,y*>,and2b ] in the carrier of (GFA3CarryStr x,y,z) )
by Th129, 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*>,and2b ] in the carrier of (BitGFA3Str x,y,z) & [<*y,z*>,and2b ] in the carrier of (BitGFA3Str x,y,z) & [<*z,x*>,and2b ] in the carrier of (BitGFA3Str x,y,z) & [<*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ] in the carrier of (BitGFA3Str x,y,z) )
by A1, A2, A4, A3, FACIRC_1:20; verum