let am, bp, cm, dp, cin be set ; InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) = (({[<*am,bp*>,xor2c],(GFA2AdderOutput (am,bp,cm))} \/ {[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2],(GFA2CarryOutput (am,bp,cm))}) \/ {[<*(GFA2AdderOutput (am,bp,cm)),cin*>,xor2c],(GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp))}) \/ {[<*(GFA2AdderOutput (am,bp,cm)),cin*>,and2c],[<*cin,dp*>,and2a],[<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2],(GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp))}
set S = BitFTA2Str (am,bp,cm,dp,cin);
set S1 = BitGFA2Str (am,bp,cm);
set A1 = GFA2AdderOutput (am,bp,cm);
set C1 = GFA2CarryOutput (am,bp,cm);
set S2 = BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp);
set A2 = GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp);
set C2 = GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp);
set ambp0 = [<*am,bp*>,xor2c];
set ambp = [<*am,bp*>,and2a];
set bpcm = [<*bp,cm*>,and2c];
set cmam = [<*cm,am*>,nor2];
set A1cin0 = [<*(GFA2AdderOutput (am,bp,cm)),cin*>,xor2c];
set A1cin = [<*(GFA2AdderOutput (am,bp,cm)),cin*>,and2c];
set cindp = [<*cin,dp*>,and2a];
set dpA1 = [<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2];
BitGFA2Str (am,bp,cm) tolerates BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp)
by CIRCCOMB:47;
hence InnerVertices (BitFTA2Str (am,bp,cm,dp,cin)) =
(InnerVertices (BitGFA2Str (am,bp,cm))) \/ (InnerVertices (BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp)))
by CIRCCOMB:11
.=
((({[<*am,bp*>,xor2c]} \/ {(GFA2AdderOutput (am,bp,cm))}) \/ {[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2]}) \/ {(GFA2CarryOutput (am,bp,cm))}) \/ (InnerVertices (BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp)))
by GFACIRC1:95
.=
(({[<*am,bp*>,xor2c],(GFA2AdderOutput (am,bp,cm))} \/ {[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2]}) \/ {(GFA2CarryOutput (am,bp,cm))}) \/ (InnerVertices (BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp)))
by ENUMSET1:1
.=
({[<*am,bp*>,xor2c],(GFA2AdderOutput (am,bp,cm))} \/ ({[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2]} \/ {(GFA2CarryOutput (am,bp,cm))})) \/ (InnerVertices (BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp)))
by XBOOLE_1:4
.=
({[<*am,bp*>,xor2c],(GFA2AdderOutput (am,bp,cm))} \/ {[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2],(GFA2CarryOutput (am,bp,cm))}) \/ (InnerVertices (BitGFA1Str ((GFA2AdderOutput (am,bp,cm)),cin,dp)))
by ENUMSET1:6
.=
({[<*am,bp*>,xor2c],(GFA2AdderOutput (am,bp,cm))} \/ {[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2],(GFA2CarryOutput (am,bp,cm))}) \/ ((({[<*(GFA2AdderOutput (am,bp,cm)),cin*>,xor2c]} \/ {(GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp))}) \/ {[<*(GFA2AdderOutput (am,bp,cm)),cin*>,and2c],[<*cin,dp*>,and2a],[<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2]}) \/ {(GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp))})
by GFACIRC1:63
.=
({[<*am,bp*>,xor2c],(GFA2AdderOutput (am,bp,cm))} \/ {[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2],(GFA2CarryOutput (am,bp,cm))}) \/ (({[<*(GFA2AdderOutput (am,bp,cm)),cin*>,xor2c],(GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp))} \/ {[<*(GFA2AdderOutput (am,bp,cm)),cin*>,and2c],[<*cin,dp*>,and2a],[<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2]}) \/ {(GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp))})
by ENUMSET1:1
.=
({[<*am,bp*>,xor2c],(GFA2AdderOutput (am,bp,cm))} \/ {[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2],(GFA2CarryOutput (am,bp,cm))}) \/ ({[<*(GFA2AdderOutput (am,bp,cm)),cin*>,xor2c],(GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp))} \/ ({[<*(GFA2AdderOutput (am,bp,cm)),cin*>,and2c],[<*cin,dp*>,and2a],[<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2]} \/ {(GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp))}))
by XBOOLE_1:4
.=
({[<*am,bp*>,xor2c],(GFA2AdderOutput (am,bp,cm))} \/ {[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2],(GFA2CarryOutput (am,bp,cm))}) \/ ({[<*(GFA2AdderOutput (am,bp,cm)),cin*>,xor2c],(GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp))} \/ {[<*(GFA2AdderOutput (am,bp,cm)),cin*>,and2c],[<*cin,dp*>,and2a],[<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2],(GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp))})
by ENUMSET1:6
.=
(({[<*am,bp*>,xor2c],(GFA2AdderOutput (am,bp,cm))} \/ {[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2],(GFA2CarryOutput (am,bp,cm))}) \/ {[<*(GFA2AdderOutput (am,bp,cm)),cin*>,xor2c],(GFA1AdderOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp))}) \/ {[<*(GFA2AdderOutput (am,bp,cm)),cin*>,and2c],[<*cin,dp*>,and2a],[<*dp,(GFA2AdderOutput (am,bp,cm))*>,and2],(GFA1CarryOutput ((GFA2AdderOutput (am,bp,cm)),cin,dp))}
by XBOOLE_1:4
;
verum