let ap, bp, cp, dp, cin be set ; InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) = (({[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp))} \/ {[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2],(GFA0CarryOutput (ap,bp,cp))}) \/ {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))}) \/ {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2],[<*cin,dp*>,and2],[<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))}
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];
BitGFA0Str (ap,bp,cp) tolerates BitGFA0Str ((GFA0AdderOutput (ap,bp,cp)),cin,dp)
by CIRCCOMB:47;
hence InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) =
(InnerVertices (BitGFA0Str (ap,bp,cp))) \/ (InnerVertices (BitGFA0Str ((GFA0AdderOutput (ap,bp,cp)),cin,dp)))
by CIRCCOMB:11
.=
((({[<*ap,bp*>,xor2]} \/ {(GFA0AdderOutput (ap,bp,cp))}) \/ {[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2]}) \/ {(GFA0CarryOutput (ap,bp,cp))}) \/ (InnerVertices (BitGFA0Str ((GFA0AdderOutput (ap,bp,cp)),cin,dp)))
by GFACIRC1:31
.=
(({[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp))} \/ {[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2]}) \/ {(GFA0CarryOutput (ap,bp,cp))}) \/ (InnerVertices (BitGFA0Str ((GFA0AdderOutput (ap,bp,cp)),cin,dp)))
by ENUMSET1:1
.=
({[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp))} \/ ({[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2]} \/ {(GFA0CarryOutput (ap,bp,cp))})) \/ (InnerVertices (BitGFA0Str ((GFA0AdderOutput (ap,bp,cp)),cin,dp)))
by XBOOLE_1:4
.=
({[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp))} \/ {[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2],(GFA0CarryOutput (ap,bp,cp))}) \/ (InnerVertices (BitGFA0Str ((GFA0AdderOutput (ap,bp,cp)),cin,dp)))
by ENUMSET1:6
.=
({[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp))} \/ {[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2],(GFA0CarryOutput (ap,bp,cp))}) \/ ((({[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2]} \/ {(GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))}) \/ {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2],[<*cin,dp*>,and2],[<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2]}) \/ {(GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))})
by GFACIRC1:31
.=
({[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp))} \/ {[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2],(GFA0CarryOutput (ap,bp,cp))}) \/ (({[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))} \/ {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2],[<*cin,dp*>,and2],[<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2]}) \/ {(GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))})
by ENUMSET1:1
.=
({[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp))} \/ {[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2],(GFA0CarryOutput (ap,bp,cp))}) \/ ({[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))} \/ ({[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2],[<*cin,dp*>,and2],[<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2]} \/ {(GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))}))
by XBOOLE_1:4
.=
({[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp))} \/ {[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2],(GFA0CarryOutput (ap,bp,cp))}) \/ ({[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))} \/ {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2],[<*cin,dp*>,and2],[<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))})
by ENUMSET1:6
.=
(({[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp))} \/ {[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2],(GFA0CarryOutput (ap,bp,cp))}) \/ {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))}) \/ {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2],[<*cin,dp*>,and2],[<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))}
by XBOOLE_1:4
;
verum