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 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:36;
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:36;
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:36;
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:36;
A5:
GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp) in the carrier of (BitGFA0Str ((GFA0AdderOutput (ap,bp,cp)),cin,dp))
by GFACIRC1:36;
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:36;
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:36;
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:36;
( ap in the carrier of (BitGFA0Str (ap,bp,cp)) & bp in the carrier of (BitGFA0Str (ap,bp,cp)) )
by GFACIRC1:36;
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