let am, bm, cm, dm, cin be set ; :: thesis: ( am in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & bm in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & cm in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & dm in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & cin in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*am,bm*>,xor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3AdderOutput (am,bm,cm) in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*am,bm*>,nor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*bm,cm*>,nor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*cm,am*>,nor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3CarryOutput (am,bm,cm) in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*cin,dm*>,nor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) )
set S1 = BitGFA3Str (am,bm,cm);
set A1 = GFA3AdderOutput (am,bm,cm);
set C1 = GFA3CarryOutput (am,bm,cm);
set S2 = BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm);
set A2 = GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm);
set C2 = GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm);
set ambm0 = [<*am,bm*>,xor2];
set ambm = [<*am,bm*>,nor2];
set bmcm = [<*bm,cm*>,nor2];
set cmam = [<*cm,am*>,nor2];
set A1cin0 = [<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2];
set A1cin = [<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2];
set cindm = [<*cin,dm*>,nor2];
set dmA1 = [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2];
A1: ( cm in the carrier of (BitGFA3Str (am,bm,cm)) & [<*am,bm*>,xor2] in the carrier of (BitGFA3Str (am,bm,cm)) ) by GFACIRC1:132;
A2: ( [<*am,bm*>,nor2] in the carrier of (BitGFA3Str (am,bm,cm)) & [<*bm,cm*>,nor2] in the carrier of (BitGFA3Str (am,bm,cm)) ) by GFACIRC1:132;
A3: ( GFA3AdderOutput (am,bm,cm) in the carrier of (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)) & cin in the carrier of (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)) ) by GFACIRC1:132;
A4: ( [<*cm,am*>,nor2] in the carrier of (BitGFA3Str (am,bm,cm)) & GFA3CarryOutput (am,bm,cm) in the carrier of (BitGFA3Str (am,bm,cm)) ) by GFACIRC1:132;
A5: GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) in the carrier of (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)) by GFACIRC1:132;
A6: ( [<*cin,dm*>,nor2] in the carrier of (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)) & [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] in the carrier of (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)) ) by GFACIRC1:132;
A7: ( GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) in the carrier of (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)) & [<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2] in the carrier of (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)) ) by GFACIRC1:132;
A8: ( dm in the carrier of (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)) & [<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2] in the carrier of (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)) ) by GFACIRC1:132;
( am in the carrier of (BitGFA3Str (am,bm,cm)) & bm in the carrier of (BitGFA3Str (am,bm,cm)) ) by GFACIRC1:132;
hence ( am in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & bm in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & cm in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & dm in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & cin in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*am,bm*>,xor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3AdderOutput (am,bm,cm) in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*am,bm*>,nor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*bm,cm*>,nor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*cm,am*>,nor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3CarryOutput (am,bm,cm) in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*cin,dm*>,nor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) in the carrier of (BitFTA3Str (am,bm,cm,dm,cin)) ) by A1, A2, A4, A3, A8, A7, A6, A5, FACIRC_1:20; :: thesis: verum