let ap, bm, cp, dm be non pair set ; for cin being set st cin <> [<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ] & 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)*>,and2b ] & 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 A2 = GFA2AdderOutput (GFA1AdderOutput ap,bm,cp),cin,dm;
set C2 = GFA2CarryOutput (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 A1cin0 = [<*(GFA1AdderOutput ap,bm,cp),cin*>,xor2c ];
set A1cin = [<*(GFA1AdderOutput ap,bm,cp),cin*>,and2a ];
set cindm = [<*cin,dm*>,and2c ];
set dmA1 = [<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ];
assume that
A1:
cin <> [<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ]
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:68;
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:76
.=
({[<*ap,bm*>,xor2c ],(GFA1AdderOutput ap,bm,cp)} \/ {[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ]}) \/ {(GFA1CarryOutput ap,bm,cp)}
by ENUMSET1:41
.=
{[<*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:46
.=
{(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,xor2c ],[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)}
by ENUMSET1:52
;
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:42
.=
({(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:41
.=
({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:67
.=
{cin} \/ {dm}
by A3, ZFMISC_1:67
.=
{cin,dm}
by ENUMSET1:41
;
( 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:55;
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:79
.=
{ap,bm,cp} \/ ({(GFA1AdderOutput ap,bm,cp),cin,dm} \ (InnerVertices (BitGFA1Str ap,bm,cp)))
by A1, Lm11, GFACIRC1:115
.=
{ap,bm,cp,dm,cin}
by A6, ENUMSET1:49
;
verum