let ap, bm, cp, dm, cin be set ; ( 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)*>,and2b ] 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 S = 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)*>,and2b ];
A1:
( cp in the carrier of (BitGFA1Str ap,bm,cp) & [<*ap,bm*>,xor2c ] in the carrier of (BitGFA1Str ap,bm,cp) )
by GFACIRC1:81;
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:81;
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:118;
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:81;
A5:
GFA2CarryOutput (GFA1AdderOutput ap,bm,cp),cin,dm in the carrier of (BitGFA2Str (GFA1AdderOutput ap,bm,cp),cin,dm)
by GFACIRC1:118;
A6:
( [<*cin,dm*>,and2c ] in the carrier of (BitGFA2Str (GFA1AdderOutput ap,bm,cp),cin,dm) & [<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ] in the carrier of (BitGFA2Str (GFA1AdderOutput ap,bm,cp),cin,dm) )
by GFACIRC1:118;
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:118;
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:118;
( ap in the carrier of (BitGFA1Str ap,bm,cp) & bm in the carrier of (BitGFA1Str ap,bm,cp) )
by GFACIRC1:81;
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)*>,and2b ] 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; verum