let am, bp, cm, dp be non pair set ; for cin being set st cin <> [<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ] & not cin in InnerVertices (BitGFA2Str am,bp,cm) holds
InputVertices (BitFTA2Str am,bp,cm,dp,cin) = {am,bp,cm,dp,cin}
let cin be set ; ( cin <> [<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ] & not cin in InnerVertices (BitGFA2Str am,bp,cm) implies InputVertices (BitFTA2Str am,bp,cm,dp,cin) = {am,bp,cm,dp,cin} )
set S = BitFTA2Str am,bp,cm,dp,cin;
set S1 = BitGFA2Str am,bp,cm;
set A1 = GFA2AdderOutput am,bp,cm;
set C1 = GFA2CarryOutput am,bp,cm;
set S2 = BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp;
set A2 = GFA1AdderOutput (GFA2AdderOutput am,bp,cm),cin,dp;
set C2 = GFA1CarryOutput (GFA2AdderOutput am,bp,cm),cin,dp;
set ambp0 = [<*am,bp*>,xor2c ];
set ambp = [<*am,bp*>,and2a ];
set bpcm = [<*bp,cm*>,and2c ];
set cmam = [<*cm,am*>,and2b ];
set A1cin0 = [<*(GFA2AdderOutput am,bp,cm),cin*>,xor2c ];
set A1cin = [<*(GFA2AdderOutput am,bp,cm),cin*>,and2c ];
set cindp = [<*cin,dp*>,and2a ];
set dpA1 = [<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ];
assume that
A1:
cin <> [<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ]
and
A2:
not cin in InnerVertices (BitGFA2Str am,bp,cm)
; InputVertices (BitFTA2Str am,bp,cm,dp,cin) = {am,bp,cm,dp,cin}
A3:
not dp in {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)}
by ENUMSET1:def 4;
GFA2AdderOutput am,bp,cm in {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)}
by ENUMSET1:def 4;
then A4:
{(GFA2AdderOutput am,bp,cm)} \ {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)} = {}
by ZFMISC_1:68;
A5: InnerVertices (BitGFA2Str am,bp,cm) =
(({[<*am,bp*>,xor2c ]} \/ {(GFA2AdderOutput am,bp,cm)}) \/ {[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ]}) \/ {(GFA2CarryOutput am,bp,cm)}
by GFACIRC1:113
.=
({[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm)} \/ {[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ]}) \/ {(GFA2CarryOutput am,bp,cm)}
by ENUMSET1:41
.=
{[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm)} \/ ({[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ]} \/ {(GFA2CarryOutput am,bp,cm)})
by XBOOLE_1:4
.=
{(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ]} \/ {[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)}
by ENUMSET1:46
.=
{(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)}
by ENUMSET1:52
;
then A6: {(GFA2AdderOutput am,bp,cm),cin,dp} \ (InnerVertices (BitGFA2Str am,bp,cm)) =
({(GFA2AdderOutput am,bp,cm)} \/ {cin,dp}) \ {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)}
by ENUMSET1:42
.=
({(GFA2AdderOutput am,bp,cm)} \ {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)}) \/ ({cin,dp} \ {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)})
by XBOOLE_1:42
.=
({cin} \/ {dp}) \ {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)}
by A4, ENUMSET1:41
.=
({cin} \ {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)}) \/ ({dp} \ {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)})
by XBOOLE_1:42
.=
{cin} \/ ({dp} \ {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)})
by A2, A5, ZFMISC_1:67
.=
{cin} \/ {dp}
by A3, ZFMISC_1:67
.=
{cin,dp}
by ENUMSET1:41
;
( InnerVertices (BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp) misses InputVertices (BitGFA2Str am,bp,cm) & BitGFA2Str am,bp,cm tolerates BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp )
by Lm22, CIRCCOMB:55;
hence InputVertices (BitFTA2Str am,bp,cm,dp,cin) =
(InputVertices (BitGFA2Str am,bp,cm)) \/ ((InputVertices (BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp)) \ (InnerVertices (BitGFA2Str am,bp,cm)))
by FACIRC_1:4
.=
{am,bp,cm} \/ ((InputVertices (BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp)) \ (InnerVertices (BitGFA2Str am,bp,cm)))
by GFACIRC1:116
.=
{am,bp,cm} \/ ({(GFA2AdderOutput am,bp,cm),cin,dp} \ (InnerVertices (BitGFA2Str am,bp,cm)))
by A1, Lm21, GFACIRC1:78
.=
{am,bp,cm,dp,cin}
by A6, ENUMSET1:49
;
verum