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)*>,and2b ],(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)*>,and2b ];
BitGFA1Str ap,bm,cp tolerates BitGFA2Str (GFA1AdderOutput ap,bm,cp),cin,dm
by CIRCCOMB:55;
hence InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) =
(InnerVertices (BitGFA1Str ap,bm,cp)) \/ (InnerVertices (BitGFA2Str (GFA1AdderOutput ap,bm,cp),cin,dm))
by CIRCCOMB:15
.=
((({[<*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:76
.=
(({[<*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:41
.=
({[<*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:46
.=
({[<*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)*>,and2b ]}) \/ {(GFA2CarryOutput (GFA1AdderOutput ap,bm,cp),cin,dm)})
by GFACIRC1:113
.=
({[<*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)*>,and2b ]}) \/ {(GFA2CarryOutput (GFA1AdderOutput ap,bm,cp),cin,dm)})
by ENUMSET1:41
.=
({[<*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)*>,and2b ]} \/ {(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)*>,and2b ],(GFA2CarryOutput (GFA1AdderOutput ap,bm,cp),cin,dm)})
by ENUMSET1:46
.=
(({[<*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)*>,and2b ],(GFA2CarryOutput (GFA1AdderOutput ap,bm,cp),cin,dm)}
by XBOOLE_1:4
;
verum