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*>,and2b ] 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 S = 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*>,and2b ];
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:118;
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:118;
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:81;
A4: ( [<*cm,am*>,and2b ] in the carrier of (BitGFA2Str am,bp,cm) & GFA2CarryOutput am,bp,cm in the carrier of (BitGFA2Str am,bp,cm) ) by GFACIRC1:118;
A5: GFA1CarryOutput (GFA2AdderOutput am,bp,cm),cin,dp in the carrier of (BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp) by GFACIRC1:81;
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:81;
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:81;
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:81;
( am in the carrier of (BitGFA2Str am,bp,cm) & bp in the carrier of (BitGFA2Str am,bp,cm) ) by GFACIRC1:118;
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*>,and2b ] 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