let ap, bp, cp, dp be non pair set ; for cin being set st cin <> [<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ] & not cin in InnerVertices (BitGFA0Str ap,bp,cp) holds
InputVertices (BitFTA0Str ap,bp,cp,dp,cin) = {ap,bp,cp,dp,cin}
let cin be set ; ( cin <> [<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ] & not cin in InnerVertices (BitGFA0Str ap,bp,cp) implies InputVertices (BitFTA0Str ap,bp,cp,dp,cin) = {ap,bp,cp,dp,cin} )
set S = BitFTA0Str ap,bp,cp,dp,cin;
set S1 = BitGFA0Str ap,bp,cp;
set A1 = GFA0AdderOutput ap,bp,cp;
set C1 = GFA0CarryOutput ap,bp,cp;
set S2 = BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp;
set A2 = GFA0AdderOutput (GFA0AdderOutput ap,bp,cp),cin,dp;
set C2 = GFA0CarryOutput (GFA0AdderOutput ap,bp,cp),cin,dp;
set apbp0 = [<*ap,bp*>,xor2 ];
set apbp = [<*ap,bp*>,and2 ];
set bpcp = [<*bp,cp*>,and2 ];
set cpap = [<*cp,ap*>,and2 ];
set A1cin0 = [<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ];
set A1cin = [<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ];
set cindp = [<*cin,dp*>,and2 ];
set dpA1 = [<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ];
assume that
A1:
cin <> [<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ]
and
A2:
not cin in InnerVertices (BitGFA0Str ap,bp,cp)
; InputVertices (BitFTA0Str ap,bp,cp,dp,cin) = {ap,bp,cp,dp,cin}
A3:
not dp in {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)}
by ENUMSET1:def 4;
GFA0AdderOutput ap,bp,cp in {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)}
by ENUMSET1:def 4;
then A4:
{(GFA0AdderOutput ap,bp,cp)} \ {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)} = {}
by ZFMISC_1:68;
A5: InnerVertices (BitGFA0Str ap,bp,cp) =
(({[<*ap,bp*>,xor2 ]} \/ {(GFA0AdderOutput ap,bp,cp)}) \/ {[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ]}) \/ {(GFA0CarryOutput ap,bp,cp)}
by GFACIRC1:39
.=
({[<*ap,bp*>,xor2 ],(GFA0AdderOutput ap,bp,cp)} \/ {[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ]}) \/ {(GFA0CarryOutput ap,bp,cp)}
by ENUMSET1:41
.=
{[<*ap,bp*>,xor2 ],(GFA0AdderOutput ap,bp,cp)} \/ ({[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ]} \/ {(GFA0CarryOutput ap,bp,cp)})
by XBOOLE_1:4
.=
{(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ]} \/ {[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)}
by ENUMSET1:46
.=
{(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)}
by ENUMSET1:52
;
then A6: {(GFA0AdderOutput ap,bp,cp),cin,dp} \ (InnerVertices (BitGFA0Str ap,bp,cp)) =
({(GFA0AdderOutput ap,bp,cp)} \/ {cin,dp}) \ {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)}
by ENUMSET1:42
.=
({(GFA0AdderOutput ap,bp,cp)} \ {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)}) \/ ({cin,dp} \ {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)})
by XBOOLE_1:42
.=
({cin} \/ {dp}) \ {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)}
by A4, ENUMSET1:41
.=
({cin} \ {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)}) \/ ({dp} \ {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)})
by XBOOLE_1:42
.=
{cin} \/ ({dp} \ {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)})
by A2, A5, ZFMISC_1:67
.=
{cin} \/ {dp}
by A3, ZFMISC_1:67
.=
{cin,dp}
by ENUMSET1:41
;
A7:
GFA0AdderOutput ap,bp,cp <> [<*cin,dp*>,and2 ]
by Lm1;
( InnerVertices (BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp) misses InputVertices (BitGFA0Str ap,bp,cp) & BitGFA0Str ap,bp,cp tolerates BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp )
by Lm2, CIRCCOMB:55;
hence InputVertices (BitFTA0Str ap,bp,cp,dp,cin) =
(InputVertices (BitGFA0Str ap,bp,cp)) \/ ((InputVertices (BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp)) \ (InnerVertices (BitGFA0Str ap,bp,cp)))
by FACIRC_1:4
.=
{ap,bp,cp} \/ ((InputVertices (BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp)) \ (InnerVertices (BitGFA0Str ap,bp,cp)))
by GFACIRC1:42
.=
{ap,bp,cp} \/ ({(GFA0AdderOutput ap,bp,cp),cin,dp} \ (InnerVertices (BitGFA0Str ap,bp,cp)))
by A1, A7, GFACIRC1:41
.=
{ap,bp,cp,dp,cin}
by A6, ENUMSET1:49
;
verum