let am, bm, cm, dm be non pair set ; for cin being set st cin <> [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ] & not cin in InnerVertices (BitGFA3Str am,bm,cm) holds
InputVertices (BitFTA3Str am,bm,cm,dm,cin) = {am,bm,cm,dm,cin}
let cin be set ; ( cin <> [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ] & not cin in InnerVertices (BitGFA3Str am,bm,cm) implies InputVertices (BitFTA3Str am,bm,cm,dm,cin) = {am,bm,cm,dm,cin} )
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 ];
assume that
A1:
cin <> [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ]
and
A2:
not cin in InnerVertices (BitGFA3Str am,bm,cm)
; InputVertices (BitFTA3Str am,bm,cm,dm,cin) = {am,bm,cm,dm,cin}
A3:
not dm in {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)}
by ENUMSET1:def 4;
GFA3AdderOutput am,bm,cm in {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)}
by ENUMSET1:def 4;
then A4:
{(GFA3AdderOutput am,bm,cm)} \ {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)} = {}
by ZFMISC_1:68;
A5: InnerVertices (BitGFA3Str am,bm,cm) =
(({[<*am,bm*>,xor2 ]} \/ {(GFA3AdderOutput am,bm,cm)}) \/ {[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ]}) \/ {(GFA3CarryOutput am,bm,cm)}
by GFACIRC1:150
.=
({[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm)} \/ {[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ]}) \/ {(GFA3CarryOutput am,bm,cm)}
by ENUMSET1:41
.=
{[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm)} \/ ({[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ]} \/ {(GFA3CarryOutput am,bm,cm)})
by XBOOLE_1:4
.=
{(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ]} \/ {[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)}
by ENUMSET1:46
.=
{(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)}
by ENUMSET1:52
;
then A6: {(GFA3AdderOutput am,bm,cm),cin,dm} \ (InnerVertices (BitGFA3Str am,bm,cm)) =
({(GFA3AdderOutput am,bm,cm)} \/ {cin,dm}) \ {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)}
by ENUMSET1:42
.=
({(GFA3AdderOutput am,bm,cm)} \ {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)}) \/ ({cin,dm} \ {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)})
by XBOOLE_1:42
.=
({cin} \/ {dm}) \ {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)}
by A4, ENUMSET1:41
.=
({cin} \ {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)}) \/ ({dm} \ {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)})
by XBOOLE_1:42
.=
{cin} \/ ({dm} \ {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)})
by A2, A5, ZFMISC_1:67
.=
{cin} \/ {dm}
by A3, ZFMISC_1:67
.=
{cin,dm}
by ENUMSET1:41
;
A7:
GFA3AdderOutput am,bm,cm <> [<*cin,dm*>,and2b ]
by Lm31;
( InnerVertices (BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm) misses InputVertices (BitGFA3Str am,bm,cm) & BitGFA3Str am,bm,cm tolerates BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm )
by Lm32, CIRCCOMB:55;
hence InputVertices (BitFTA3Str am,bm,cm,dm,cin) =
(InputVertices (BitGFA3Str am,bm,cm)) \/ ((InputVertices (BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm)) \ (InnerVertices (BitGFA3Str am,bm,cm)))
by FACIRC_1:4
.=
{am,bm,cm} \/ ((InputVertices (BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm)) \ (InnerVertices (BitGFA3Str am,bm,cm)))
by GFACIRC1:153
.=
{am,bm,cm} \/ ({(GFA3AdderOutput am,bm,cm),cin,dm} \ (InnerVertices (BitGFA3Str am,bm,cm)))
by A1, A7, GFACIRC1:152
.=
{am,bm,cm,dm,cin}
by A6, ENUMSET1:49
;
verum