let ap, bp, cp, dp, cin be set ; ( ap in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & bp in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & cp in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & dp in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & cin in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & [<*ap,bp*>,xor2 ] in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & GFA0AdderOutput ap,bp,cp in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & [<*ap,bp*>,and2 ] in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & [<*bp,cp*>,and2 ] in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & [<*cp,ap*>,and2 ] in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & GFA0CarryOutput ap,bp,cp in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & [<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ] in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & GFA0AdderOutput (GFA0AdderOutput ap,bp,cp),cin,dp in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & [<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ] in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & [<*cin,dp*>,and2 ] in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & [<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ] in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & GFA0CarryOutput (GFA0AdderOutput ap,bp,cp),cin,dp in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) )
set S = BitFTA0Str ap,bp,cp,dp,cin;
set S1 = BitGFA0Str ap,bp,cp;
set A1 = GFA0AdderOutput ap,bp,cp;
set C1 = GFA0CarryOutput ap,bp,cp;
set S2 = BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp;
set A2 = GFA0AdderOutput (GFA0AdderOutput ap,bp,cp),cin,dp;
set C2 = GFA0CarryOutput (GFA0AdderOutput ap,bp,cp),cin,dp;
set apbp0 = [<*ap,bp*>,xor2 ];
set apbp = [<*ap,bp*>,and2 ];
set bpcp = [<*bp,cp*>,and2 ];
set cpap = [<*cp,ap*>,and2 ];
set A1cin0 = [<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ];
set A1cin = [<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ];
set cindp = [<*cin,dp*>,and2 ];
set dpA1 = [<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ];
A1:
( cp in the carrier of (BitGFA0Str ap,bp,cp) & [<*ap,bp*>,xor2 ] in the carrier of (BitGFA0Str ap,bp,cp) )
by GFACIRC1:44;
A2:
( [<*ap,bp*>,and2 ] in the carrier of (BitGFA0Str ap,bp,cp) & [<*bp,cp*>,and2 ] in the carrier of (BitGFA0Str ap,bp,cp) )
by GFACIRC1:44;
A3:
( GFA0AdderOutput ap,bp,cp in the carrier of (BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp) & cin in the carrier of (BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp) )
by GFACIRC1:44;
A4:
( [<*cp,ap*>,and2 ] in the carrier of (BitGFA0Str ap,bp,cp) & GFA0CarryOutput ap,bp,cp in the carrier of (BitGFA0Str ap,bp,cp) )
by GFACIRC1:44;
A5:
GFA0CarryOutput (GFA0AdderOutput ap,bp,cp),cin,dp in the carrier of (BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp)
by GFACIRC1:44;
A6:
( [<*cin,dp*>,and2 ] in the carrier of (BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp) & [<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ] in the carrier of (BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp) )
by GFACIRC1:44;
A7:
( GFA0AdderOutput (GFA0AdderOutput ap,bp,cp),cin,dp in the carrier of (BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp) & [<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ] in the carrier of (BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp) )
by GFACIRC1:44;
A8:
( dp in the carrier of (BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp) & [<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ] in the carrier of (BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp) )
by GFACIRC1:44;
( ap in the carrier of (BitGFA0Str ap,bp,cp) & bp in the carrier of (BitGFA0Str ap,bp,cp) )
by GFACIRC1:44;
hence
( ap in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & bp in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & cp in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & dp in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & cin in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & [<*ap,bp*>,xor2 ] in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & GFA0AdderOutput ap,bp,cp in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & [<*ap,bp*>,and2 ] in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & [<*bp,cp*>,and2 ] in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & [<*cp,ap*>,and2 ] in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & GFA0CarryOutput ap,bp,cp in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & [<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ] in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & GFA0AdderOutput (GFA0AdderOutput ap,bp,cp),cin,dp in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & [<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ] in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & [<*cin,dp*>,and2 ] in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & [<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ] in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) & GFA0CarryOutput (GFA0AdderOutput ap,bp,cp),cin,dp in the carrier of (BitFTA0Str ap,bp,cp,dp,cin) )
by A1, A2, A4, A3, A8, A7, A6, A5, FACIRC_1:20; verum