let ap, bm, cp, dm be non pair set ; for cin being set st cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] & not cin in InnerVertices (BitGFA1Str (ap,bm,cp)) holds
InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) = {ap,bm,cp,dm,cin}
let cin be set ; ( cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] & not cin in InnerVertices (BitGFA1Str (ap,bm,cp)) implies InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) = {ap,bm,cp,dm,cin} )
set S = BitFTA1Str (ap,bm,cp,dm,cin);
set S1 = BitGFA1Str (ap,bm,cp);
set A1 = GFA1AdderOutput (ap,bm,cp);
set C1 = GFA1CarryOutput (ap,bm,cp);
set S2 = BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm);
set apbm0 = [<*ap,bm*>,xor2c];
set apbm = [<*ap,bm*>,and2c];
set bmcp = [<*bm,cp*>,and2a];
set cpap = [<*cp,ap*>,and2];
set dmA1 = [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2];
assume that
A1:
cin <> [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2]
and
A2:
not cin in InnerVertices (BitGFA1Str (ap,bm,cp))
; InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) = {ap,bm,cp,dm,cin}
A3:
not dm in {(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,xor2c],[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))}
by ENUMSET1:def 4;
GFA1AdderOutput (ap,bm,cp) in {(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,xor2c],[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))}
by ENUMSET1:def 4;
then A4:
{(GFA1AdderOutput (ap,bm,cp))} \ {(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,xor2c],[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))} = {}
by ZFMISC_1:60;
A5: InnerVertices (BitGFA1Str (ap,bm,cp)) =
(({[<*ap,bm*>,xor2c]} \/ {(GFA1AdderOutput (ap,bm,cp))}) \/ {[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2]}) \/ {(GFA1CarryOutput (ap,bm,cp))}
by GFACIRC1:63
.=
({[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp))} \/ {[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2]}) \/ {(GFA1CarryOutput (ap,bm,cp))}
by ENUMSET1:1
.=
{[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp))} \/ ({[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2]} \/ {(GFA1CarryOutput (ap,bm,cp))})
by XBOOLE_1:4
.=
{(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,xor2c]} \/ {[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))}
by ENUMSET1:6
.=
{(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,xor2c],[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))}
by ENUMSET1:12
;
then A6: {(GFA1AdderOutput (ap,bm,cp)),cin,dm} \ (InnerVertices (BitGFA1Str (ap,bm,cp))) =
({(GFA1AdderOutput (ap,bm,cp))} \/ {cin,dm}) \ {(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,xor2c],[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))}
by ENUMSET1:2
.=
({(GFA1AdderOutput (ap,bm,cp))} \ {(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,xor2c],[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))}) \/ ({cin,dm} \ {(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,xor2c],[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))})
by XBOOLE_1:42
.=
({cin} \/ {dm}) \ {(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,xor2c],[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))}
by A4, ENUMSET1:1
.=
({cin} \ {(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,xor2c],[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))}) \/ ({dm} \ {(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,xor2c],[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))})
by XBOOLE_1:42
.=
{cin} \/ ({dm} \ {(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,xor2c],[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))})
by A2, A5, ZFMISC_1:59
.=
{cin} \/ {dm}
by A3, ZFMISC_1:59
.=
{cin,dm}
by ENUMSET1:1
;
( InnerVertices (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) misses InputVertices (BitGFA1Str (ap,bm,cp)) & BitGFA1Str (ap,bm,cp) tolerates BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm) )
by Lm12, CIRCCOMB:47;
hence InputVertices (BitFTA1Str (ap,bm,cp,dm,cin)) =
(InputVertices (BitGFA1Str (ap,bm,cp))) \/ ((InputVertices (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm))) \ (InnerVertices (BitGFA1Str (ap,bm,cp))))
by FACIRC_1:4
.=
{ap,bm,cp} \/ ((InputVertices (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm))) \ (InnerVertices (BitGFA1Str (ap,bm,cp))))
by GFACIRC1:66
.=
{ap,bm,cp} \/ ({(GFA1AdderOutput (ap,bm,cp)),cin,dm} \ (InnerVertices (BitGFA1Str (ap,bm,cp))))
by A1, Lm11, GFACIRC1:97
.=
{ap,bm,cp,dm,cin}
by A6, ENUMSET1:9
;
verum