let ap, bm, cp, dm, cin be set ; :: thesis: ( ap in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & bm in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & cp in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & dm in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & cin in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*ap,bm*>,xor2c] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA1AdderOutput (ap,bm,cp) in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*ap,bm*>,and2c] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*bm,cp*>,and2a] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*cp,ap*>,and2] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA1CarryOutput (ap,bm,cp) in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*cin,dm*>,and2c] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) )
set S1 = BitGFA1Str (ap,bm,cp);
set A1 = GFA1AdderOutput (ap,bm,cp);
set C1 = GFA1CarryOutput (ap,bm,cp);
set S2 = BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm);
set A2 = GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm);
set C2 = GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm);
set apbm0 = [<*ap,bm*>,xor2c];
set apbm = [<*ap,bm*>,and2c];
set bmcp = [<*bm,cp*>,and2a];
set cpap = [<*cp,ap*>,and2];
set A1cin0 = [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c];
set A1cin = [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a];
set cindm = [<*cin,dm*>,and2c];
set dmA1 = [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2];
A1: ( cp in the carrier of (BitGFA1Str (ap,bm,cp)) & [<*ap,bm*>,xor2c] in the carrier of (BitGFA1Str (ap,bm,cp)) ) by GFACIRC1:68;
A2: ( [<*ap,bm*>,and2c] in the carrier of (BitGFA1Str (ap,bm,cp)) & [<*bm,cp*>,and2a] in the carrier of (BitGFA1Str (ap,bm,cp)) ) by GFACIRC1:68;
A3: ( GFA1AdderOutput (ap,bm,cp) in the carrier of (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) & cin in the carrier of (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) ) by GFACIRC1:100;
A4: ( [<*cp,ap*>,and2] in the carrier of (BitGFA1Str (ap,bm,cp)) & GFA1CarryOutput (ap,bm,cp) in the carrier of (BitGFA1Str (ap,bm,cp)) ) by GFACIRC1:68;
A5: GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) in the carrier of (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) by GFACIRC1:100;
A6: ( [<*cin,dm*>,and2c] in the carrier of (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) & [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] in the carrier of (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) ) by GFACIRC1:100;
A7: ( GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) in the carrier of (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) & [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a] in the carrier of (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) ) by GFACIRC1:100;
A8: ( dm in the carrier of (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) & [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c] in the carrier of (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) ) by GFACIRC1:100;
( ap in the carrier of (BitGFA1Str (ap,bm,cp)) & bm in the carrier of (BitGFA1Str (ap,bm,cp)) ) by GFACIRC1:68;
hence ( ap in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & bm in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & cp in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & dm in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & cin in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*ap,bm*>,xor2c] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA1AdderOutput (ap,bm,cp) in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*ap,bm*>,and2c] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*bm,cp*>,and2a] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*cp,ap*>,and2] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA1CarryOutput (ap,bm,cp) in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*cin,dm*>,and2c] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) in the carrier of (BitFTA1Str (ap,bm,cp,dm,cin)) ) by A1, A2, A4, A3, A8, A7, A6, A5, FACIRC_1:20; :: thesis: verum