set f0 = xor2c ;
set f1 = and2a ;
set f2 = and2c ;
set f3 = and2b ;
set f4 = nor3 ;
let x, y, z be set ; :: thesis: ( x in the carrier of (BitGFA2Str x,y,z) & y in the carrier of (BitGFA2Str x,y,z) & z in the carrier of (BitGFA2Str x,y,z) & [<*x,y*>,xor2c ] in the carrier of (BitGFA2Str x,y,z) & [<*[<*x,y*>,xor2c ],z*>,xor2c ] in the carrier of (BitGFA2Str x,y,z) & [<*x,y*>,and2a ] in the carrier of (BitGFA2Str x,y,z) & [<*y,z*>,and2c ] in the carrier of (BitGFA2Str x,y,z) & [<*z,x*>,and2b ] in the carrier of (BitGFA2Str x,y,z) & [<*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ] in the carrier of (BitGFA2Str x,y,z) )
set xy = [<*x,y*>,and2a ];
set yz = [<*y,z*>,and2c ];
set zx = [<*z,x*>,and2b ];
set xyz = [<*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ];
set S1 = GFA2AdderStr x,y,z;
set S2 = GFA2CarryStr x,y,z;
A1: ( x in the carrier of (GFA2AdderStr x,y,z) & y in the carrier of (GFA2AdderStr x,y,z) & z in the carrier of (GFA2AdderStr x,y,z) & [<*x,y*>,xor2c ] in the carrier of (GFA2AdderStr x,y,z) & [<*[<*x,y*>,xor2c ],z*>,xor2c ] in the carrier of (GFA2AdderStr x,y,z) ) by FACIRC_1:60, FACIRC_1:61;
( [<*x,y*>,and2a ] in the carrier of (GFA2CarryStr x,y,z) & [<*y,z*>,and2c ] in the carrier of (GFA2CarryStr x,y,z) & [<*z,x*>,and2b ] in the carrier of (GFA2CarryStr x,y,z) & [<*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ] in the carrier of (GFA2CarryStr x,y,z) ) by Th92;
hence ( x in the carrier of (BitGFA2Str x,y,z) & y in the carrier of (BitGFA2Str x,y,z) & z in the carrier of (BitGFA2Str x,y,z) & [<*x,y*>,xor2c ] in the carrier of (BitGFA2Str x,y,z) & [<*[<*x,y*>,xor2c ],z*>,xor2c ] in the carrier of (BitGFA2Str x,y,z) & [<*x,y*>,and2a ] in the carrier of (BitGFA2Str x,y,z) & [<*y,z*>,and2c ] in the carrier of (BitGFA2Str x,y,z) & [<*z,x*>,and2b ] in the carrier of (BitGFA2Str x,y,z) & [<*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ] in the carrier of (BitGFA2Str x,y,z) ) by A1, FACIRC_1:20; :: thesis: verum