let ap, bm, cp, dm, cin be set ; InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) = (({[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp))} \/ {[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))}) \/ {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c],(GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))}) \/ {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a],[<*cin,dm*>,and2c],[<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2],(GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))}
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))*>,nor2];
BitGFA1Str (ap,bm,cp) tolerates BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)
by CIRCCOMB:47;
hence InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) =
(InnerVertices (BitGFA1Str (ap,bm,cp))) \/ (InnerVertices (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)))
by CIRCCOMB:11
.=
((({[<*ap,bm*>,xor2c]} \/ {(GFA1AdderOutput (ap,bm,cp))}) \/ {[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2]}) \/ {(GFA1CarryOutput (ap,bm,cp))}) \/ (InnerVertices (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)))
by GFACIRC1:63
.=
(({[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp))} \/ {[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2]}) \/ {(GFA1CarryOutput (ap,bm,cp))}) \/ (InnerVertices (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)))
by ENUMSET1:1
.=
({[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp))} \/ ({[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2]} \/ {(GFA1CarryOutput (ap,bm,cp))})) \/ (InnerVertices (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)))
by XBOOLE_1:4
.=
({[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp))} \/ {[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))}) \/ (InnerVertices (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)))
by ENUMSET1:6
.=
({[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp))} \/ {[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))}) \/ ((({[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c]} \/ {(GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))}) \/ {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a],[<*cin,dm*>,and2c],[<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2]}) \/ {(GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))})
by GFACIRC1:95
.=
({[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp))} \/ {[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))}) \/ (({[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c],(GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))} \/ {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a],[<*cin,dm*>,and2c],[<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2]}) \/ {(GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))})
by ENUMSET1:1
.=
({[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp))} \/ {[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))}) \/ ({[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c],(GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))} \/ ({[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a],[<*cin,dm*>,and2c],[<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2]} \/ {(GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))}))
by XBOOLE_1:4
.=
({[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp))} \/ {[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))}) \/ ({[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c],(GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))} \/ {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a],[<*cin,dm*>,and2c],[<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2],(GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))})
by ENUMSET1:6
.=
(({[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp))} \/ {[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))}) \/ {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c],(GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))}) \/ {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a],[<*cin,dm*>,and2c],[<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2],(GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))}
by XBOOLE_1:4
;
verum