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*>,and2b ] in the carrier of (BitFTA3Str am,bm,cm,dm,cin) & [<*bm,cm*>,and2b ] in the carrier of (BitFTA3Str am,bm,cm,dm,cin) & [<*cm,am*>,and2b ] 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*>,and2b ] in the carrier of (BitFTA3Str am,bm,cm,dm,cin) & [<*cin,dm*>,and2b ] in the carrier of (BitFTA3Str am,bm,cm,dm,cin) & [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ] 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 S = 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*>,and2b ];
set bmcm = [<*bm,cm*>,and2b ];
set cmam = [<*cm,am*>,and2b ];
set A1cin0 = [<*(GFA3AdderOutput am,bm,cm),cin*>,xor2 ];
set A1cin = [<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ];
set cindm = [<*cin,dm*>,and2b ];
set dmA1 = [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ];
A1: ( cm in the carrier of (BitGFA3Str am,bm,cm) & [<*am,bm*>,xor2 ] in the carrier of (BitGFA3Str am,bm,cm) ) by GFACIRC1:155;
A2: ( [<*am,bm*>,and2b ] in the carrier of (BitGFA3Str am,bm,cm) & [<*bm,cm*>,and2b ] in the carrier of (BitGFA3Str am,bm,cm) ) by GFACIRC1:155;
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:155;
A4: ( [<*cm,am*>,and2b ] in the carrier of (BitGFA3Str am,bm,cm) & GFA3CarryOutput am,bm,cm in the carrier of (BitGFA3Str am,bm,cm) ) by GFACIRC1:155;
A5: GFA3CarryOutput (GFA3AdderOutput am,bm,cm),cin,dm in the carrier of (BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm) by GFACIRC1:155;
A6: ( [<*cin,dm*>,and2b ] in the carrier of (BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm) & [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ] in the carrier of (BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm) ) by GFACIRC1:155;
A7: ( GFA3AdderOutput (GFA3AdderOutput am,bm,cm),cin,dm in the carrier of (BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm) & [<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ] in the carrier of (BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm) ) by GFACIRC1:155;
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:155;
( am in the carrier of (BitGFA3Str am,bm,cm) & bm in the carrier of (BitGFA3Str am,bm,cm) ) by GFACIRC1:155;
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*>,and2b ] in the carrier of (BitFTA3Str am,bm,cm,dm,cin) & [<*bm,cm*>,and2b ] in the carrier of (BitFTA3Str am,bm,cm,dm,cin) & [<*cm,am*>,and2b ] 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*>,and2b ] in the carrier of (BitFTA3Str am,bm,cm,dm,cin) & [<*cin,dm*>,and2b ] in the carrier of (BitFTA3Str am,bm,cm,dm,cin) & [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ] 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