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*>,and2b ],(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*>,and2b ];
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:55;
hence InnerVertices (BitFTA2Str am,bp,cm,dp,cin) =
(InnerVertices (BitGFA2Str am,bp,cm)) \/ (InnerVertices (BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp))
by CIRCCOMB:15
.=
((({[<*am,bp*>,xor2c ]} \/ {(GFA2AdderOutput am,bp,cm)}) \/ {[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ]}) \/ {(GFA2CarryOutput am,bp,cm)}) \/ (InnerVertices (BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp))
by GFACIRC1:113
.=
(({[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm)} \/ {[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ]}) \/ {(GFA2CarryOutput am,bp,cm)}) \/ (InnerVertices (BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp))
by ENUMSET1:41
.=
({[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm)} \/ ({[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ]} \/ {(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*>,and2b ],(GFA2CarryOutput am,bp,cm)}) \/ (InnerVertices (BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp))
by ENUMSET1:46
.=
({[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm)} \/ {[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(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:76
.=
({[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm)} \/ {[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(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:41
.=
({[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm)} \/ {[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(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*>,and2b ],(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:46
.=
(({[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm)} \/ {[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(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