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:55;
hence InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) =
(InnerVertices (BitGFA0Str ap,bp,cp)) \/ (InnerVertices (BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp))
by CIRCCOMB:15
.=
((({[<*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:39
.=
(({[<*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:41
.=
({[<*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:46
.=
({[<*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:39
.=
({[<*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:41
.=
({[<*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:46
.=
(({[<*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