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 ambp0 = [<*am,bp*>,xor2c];
set ambp = [<*am,bp*>,and2a];
set bpcm = [<*bp,cm*>,and2c];
set cmam = [<*cm,am*>,nor2];
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*>,nor2],(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*>,nor2],(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*>,nor2],(GFA2CarryOutput (am,bp,cm))} = {}
by ZFMISC_1:60;
A5: InnerVertices (BitGFA2Str (am,bp,cm)) =
(({[<*am,bp*>,xor2c]} \/ {(GFA2AdderOutput (am,bp,cm))}) \/ {[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2]}) \/ {(GFA2CarryOutput (am,bp,cm))}
by GFACIRC1:95
.=
({[<*am,bp*>,xor2c],(GFA2AdderOutput (am,bp,cm))} \/ {[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2]}) \/ {(GFA2CarryOutput (am,bp,cm))}
by ENUMSET1:1
.=
{[<*am,bp*>,xor2c],(GFA2AdderOutput (am,bp,cm))} \/ ({[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2]} \/ {(GFA2CarryOutput (am,bp,cm))})
by XBOOLE_1:4
.=
{(GFA2AdderOutput (am,bp,cm)),[<*am,bp*>,xor2c]} \/ {[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2],(GFA2CarryOutput (am,bp,cm))}
by ENUMSET1:6
.=
{(GFA2AdderOutput (am,bp,cm)),[<*am,bp*>,xor2c],[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2],(GFA2CarryOutput (am,bp,cm))}
by ENUMSET1:12
;
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*>,nor2],(GFA2CarryOutput (am,bp,cm))}
by ENUMSET1:2
.=
({(GFA2AdderOutput (am,bp,cm))} \ {(GFA2AdderOutput (am,bp,cm)),[<*am,bp*>,xor2c],[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2],(GFA2CarryOutput (am,bp,cm))}) \/ ({cin,dp} \ {(GFA2AdderOutput (am,bp,cm)),[<*am,bp*>,xor2c],[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2],(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*>,nor2],(GFA2CarryOutput (am,bp,cm))}
by A4, ENUMSET1:1
.=
({cin} \ {(GFA2AdderOutput (am,bp,cm)),[<*am,bp*>,xor2c],[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2],(GFA2CarryOutput (am,bp,cm))}) \/ ({dp} \ {(GFA2AdderOutput (am,bp,cm)),[<*am,bp*>,xor2c],[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2],(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*>,nor2],(GFA2CarryOutput (am,bp,cm))})
by A2, A5, ZFMISC_1:59
.=
{cin} \/ {dp}
by A3, ZFMISC_1:59
.=
{cin,dp}
by ENUMSET1:1
;
( 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:47;
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:98
.=
{am,bp,cm} \/ ({(GFA2AdderOutput (am,bp,cm)),cin,dp} \ (InnerVertices (BitGFA2Str (am,bp,cm))))
by A1, Lm21, GFACIRC1:65
.=
{am,bp,cm,dp,cin}
by A6, ENUMSET1:9
;
verum