let am, bp, cm, dp, cin be set ; :: thesis: ( am in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & bp in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & cm in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & dp in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & cin in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*am,bp*>,xor2c] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & GFA2AdderOutput (am,bp,cm) in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*am,bp*>,and2a] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*bp,cm*>,and2c] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*cm,am*>,nor2] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & GFA2CarryOutput (am,bp,cm) in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*(GFA2AdderOutput (am,bp,cm)),cin*>,xor2c] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp) in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*(GFA2AdderOutput (am,bp,cm)),cin*>,and2c] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*cin,dp*>,and2a] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp) in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) )
set S1 = BitGFA2Str (am,bp,cm);
set A1 = GFA2AdderOutput (am,bp,cm);
set C1 = GFA2CarryOutput (am,bp,cm);
set S2 = BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp);
set A2 = GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp);
set C2 = GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp);
set ambp0 = [<*am,bp*>,xor2c];
set ambp = [<*am,bp*>,and2a];
set bpcm = [<*bp,cm*>,and2c];
set cmam = [<*cm,am*>,nor2];
set A1cin0 = [<*(GFA2AdderOutput (am,bp,cm)),cin*>,xor2c];
set A1cin = [<*(GFA2AdderOutput (am,bp,cm)),cin*>,and2c];
set cindp = [<*cin,dp*>,and2a];
set dpA1 = [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2];
A1: ( cm in the carrier of (BitGFA2Str (am,bp,cm)) & [<*am,bp*>,xor2c] in the carrier of (BitGFA2Str (am,bp,cm)) ) by GFACIRC1:100;
A2: ( [<*am,bp*>,and2a] in the carrier of (BitGFA2Str (am,bp,cm)) & [<*bp,cm*>,and2c] in the carrier of (BitGFA2Str (am,bp,cm)) ) by GFACIRC1:100;
A3: ( GFA2AdderOutput (am,bp,cm) in the carrier of (BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp)) & cin in the carrier of (BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp)) ) by GFACIRC1:68;
A4: ( [<*cm,am*>,nor2] in the carrier of (BitGFA2Str (am,bp,cm)) & GFA2CarryOutput (am,bp,cm) in the carrier of (BitGFA2Str (am,bp,cm)) ) by GFACIRC1:100;
A5: GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp) in the carrier of (BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp)) by GFACIRC1:68;
A6: ( [<*cin,dp*>,and2a] in the carrier of (BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp)) & [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2] in the carrier of (BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp)) ) by GFACIRC1:68;
A7: ( GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp) in the carrier of (BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp)) & [<*(GFA2AdderOutput (am,bp,cm)),cin*>,and2c] in the carrier of (BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp)) ) by GFACIRC1:68;
A8: ( dp in the carrier of (BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp)) & [<*(GFA2AdderOutput (am,bp,cm)),cin*>,xor2c] in the carrier of (BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp)) ) by GFACIRC1:68;
( am in the carrier of (BitGFA2Str (am,bp,cm)) & bp in the carrier of (BitGFA2Str (am,bp,cm)) ) by GFACIRC1:100;
hence ( am in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & bp in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & cm in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & dp in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & cin in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*am,bp*>,xor2c] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & GFA2AdderOutput (am,bp,cm) in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*am,bp*>,and2a] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*bp,cm*>,and2c] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*cm,am*>,nor2] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & GFA2CarryOutput (am,bp,cm) in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*(GFA2AdderOutput (am,bp,cm)),cin*>,xor2c] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp) in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*(GFA2AdderOutput (am,bp,cm)),cin*>,and2c] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*cin,dp*>,and2a] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2] in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) & GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp) in the carrier of (BitFTA2Str (am,bp,cm,dp,cin)) ) by A1, A2, A4, A3, A8, A7, A6, A5, FACIRC_1:20; :: thesis: verum