let am, bm, cm, dm, cin be set ; InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) = (({[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm))} \/ {[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))}) \/ {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2],(GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))}) \/ {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2],[<*cin,dm*>,nor2],[<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2],(GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))}
set S = BitFTA3Str (am,bm,cm,dm,cin);
set S1 = BitGFA3Str (am,bm,cm);
set A1 = GFA3AdderOutput (am,bm,cm);
set C1 = GFA3CarryOutput (am,bm,cm);
set S2 = BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm);
set A2 = GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm);
set C2 = GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm);
set ambm0 = [<*am,bm*>,xor2];
set ambm = [<*am,bm*>,nor2];
set bmcm = [<*bm,cm*>,nor2];
set cmam = [<*cm,am*>,nor2];
set A1cin0 = [<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2];
set A1cin = [<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2];
set cindm = [<*cin,dm*>,nor2];
set dmA1 = [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2];
BitGFA3Str (am,bm,cm) tolerates BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)
by CIRCCOMB:47;
hence InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) =
(InnerVertices (BitGFA3Str (am,bm,cm))) \/ (InnerVertices (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)))
by CIRCCOMB:11
.=
((({[<*am,bm*>,xor2]} \/ {(GFA3AdderOutput (am,bm,cm))}) \/ {[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2]}) \/ {(GFA3CarryOutput (am,bm,cm))}) \/ (InnerVertices (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)))
by GFACIRC1:127
.=
(({[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm))} \/ {[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2]}) \/ {(GFA3CarryOutput (am,bm,cm))}) \/ (InnerVertices (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)))
by ENUMSET1:1
.=
({[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm))} \/ ({[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2]} \/ {(GFA3CarryOutput (am,bm,cm))})) \/ (InnerVertices (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)))
by XBOOLE_1:4
.=
({[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm))} \/ {[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))}) \/ (InnerVertices (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)))
by ENUMSET1:6
.=
({[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm))} \/ {[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))}) \/ ((({[<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2]} \/ {(GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))}) \/ {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2],[<*cin,dm*>,nor2],[<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2]}) \/ {(GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))})
by GFACIRC1:127
.=
({[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm))} \/ {[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))}) \/ (({[<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2],(GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))} \/ {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2],[<*cin,dm*>,nor2],[<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2]}) \/ {(GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))})
by ENUMSET1:1
.=
({[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm))} \/ {[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))}) \/ ({[<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2],(GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))} \/ ({[<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2],[<*cin,dm*>,nor2],[<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2]} \/ {(GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))}))
by XBOOLE_1:4
.=
({[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm))} \/ {[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))}) \/ ({[<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2],(GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))} \/ {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2],[<*cin,dm*>,nor2],[<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2],(GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))})
by ENUMSET1:6
.=
(({[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm))} \/ {[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))}) \/ {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2],(GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))}) \/ {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2],[<*cin,dm*>,nor2],[<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2],(GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))}
by XBOOLE_1:4
;
verum