let am, bm, cm, dm, cin be set ; InnerVertices (BitFTA3Str am,bm,cm,dm,cin) = (({[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm)} \/ {[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)}) \/ {[<*(GFA3AdderOutput am,bm,cm),cin*>,xor2 ],(GFA3AdderOutput (GFA3AdderOutput am,bm,cm),cin,dm)}) \/ {[<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ],[<*cin,dm*>,and2b ],[<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ],(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*>,and2b ];
set bmcm = [<*bm,cm*>,and2b ];
set cmam = [<*cm,am*>,and2b ];
set A1cin0 = [<*(GFA3AdderOutput am,bm,cm),cin*>,xor2 ];
set A1cin = [<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ];
set cindm = [<*cin,dm*>,and2b ];
set dmA1 = [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ];
BitGFA3Str am,bm,cm tolerates BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm
by CIRCCOMB:55;
hence InnerVertices (BitFTA3Str am,bm,cm,dm,cin) =
(InnerVertices (BitGFA3Str am,bm,cm)) \/ (InnerVertices (BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm))
by CIRCCOMB:15
.=
((({[<*am,bm*>,xor2 ]} \/ {(GFA3AdderOutput am,bm,cm)}) \/ {[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ]}) \/ {(GFA3CarryOutput am,bm,cm)}) \/ (InnerVertices (BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm))
by GFACIRC1:150
.=
(({[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm)} \/ {[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ]}) \/ {(GFA3CarryOutput am,bm,cm)}) \/ (InnerVertices (BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm))
by ENUMSET1:41
.=
({[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm)} \/ ({[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ]} \/ {(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*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)}) \/ (InnerVertices (BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm))
by ENUMSET1:46
.=
({[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm)} \/ {[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)}) \/ ((({[<*(GFA3AdderOutput am,bm,cm),cin*>,xor2 ]} \/ {(GFA3AdderOutput (GFA3AdderOutput am,bm,cm),cin,dm)}) \/ {[<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ],[<*cin,dm*>,and2b ],[<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ]}) \/ {(GFA3CarryOutput (GFA3AdderOutput am,bm,cm),cin,dm)})
by GFACIRC1:150
.=
({[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm)} \/ {[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)}) \/ (({[<*(GFA3AdderOutput am,bm,cm),cin*>,xor2 ],(GFA3AdderOutput (GFA3AdderOutput am,bm,cm),cin,dm)} \/ {[<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ],[<*cin,dm*>,and2b ],[<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ]}) \/ {(GFA3CarryOutput (GFA3AdderOutput am,bm,cm),cin,dm)})
by ENUMSET1:41
.=
({[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm)} \/ {[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)}) \/ ({[<*(GFA3AdderOutput am,bm,cm),cin*>,xor2 ],(GFA3AdderOutput (GFA3AdderOutput am,bm,cm),cin,dm)} \/ ({[<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ],[<*cin,dm*>,and2b ],[<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ]} \/ {(GFA3CarryOutput (GFA3AdderOutput am,bm,cm),cin,dm)}))
by XBOOLE_1:4
.=
({[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm)} \/ {[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)}) \/ ({[<*(GFA3AdderOutput am,bm,cm),cin*>,xor2 ],(GFA3AdderOutput (GFA3AdderOutput am,bm,cm),cin,dm)} \/ {[<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ],[<*cin,dm*>,and2b ],[<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ],(GFA3CarryOutput (GFA3AdderOutput am,bm,cm),cin,dm)})
by ENUMSET1:46
.=
(({[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm)} \/ {[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)}) \/ {[<*(GFA3AdderOutput am,bm,cm),cin*>,xor2 ],(GFA3AdderOutput (GFA3AdderOutput am,bm,cm),cin,dm)}) \/ {[<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ],[<*cin,dm*>,and2b ],[<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ],(GFA3CarryOutput (GFA3AdderOutput am,bm,cm),cin,dm)}
by XBOOLE_1:4
;
verum