let x, y, z be set ; :: thesis:
set f1 = and2a ;
set f2 = and2c ;
set f3 = nor2 ;
set f4 = nor3 ;
set f0 = xor2c ;
set xy = [<*x,y*>,and2a];
set yz = [<*y,z*>,and2c];
set zx = [<*z,x*>,nor2];
set xyz = [<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]*>,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)) ) by FACIRC_1:60;
A2: ( z in the carrier of (GFA2AdderStr (x,y,z)) & [<*x,y*>,xor2c] in the carrier of (GFA2AdderStr (x,y,z)) ) by FACIRC_1:60, FACIRC_1:61;
A3: [<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]*>,nor3] in the carrier of (GFA2CarryStr (x,y,z)) by Th79;
A4: ( [<*y,z*>,and2c] in the carrier of (GFA2CarryStr (x,y,z)) & [<*z,x*>,nor2] in the carrier of (GFA2CarryStr (x,y,z)) ) by Th79;
( [<*[<*x,y*>,xor2c],z*>,xor2c] in the carrier of (GFA2AdderStr (x,y,z)) & [<*x,y*>,and2a] in the carrier of (GFA2CarryStr (x,y,z)) ) by Th79, FACIRC_1:61;
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*>,nor2] in the carrier of (BitGFA2Str (x,y,z)) & [<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]*>,nor3] in the carrier of (BitGFA2Str (x,y,z)) ) by A1, A2, A4, A3, FACIRC_1:20; :: thesis: