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 apbp0 = [<*ap,bp*>,xor2];
set apbp = [<*ap,bp*>,and2];
set bpcp = [<*bp,cp*>,and2];
set cpap = [<*cp,ap*>,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:60;
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:31
.=
({[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp))} \/ {[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2]}) \/ {(GFA0CarryOutput (ap,bp,cp))}
by ENUMSET1:1
.=
{[<*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:6
.=
{(GFA0AdderOutput (ap,bp,cp)),[<*ap,bp*>,xor2],[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2],(GFA0CarryOutput (ap,bp,cp))}
by ENUMSET1:12
;
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:2
.=
({(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:1
.=
({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:59
.=
{cin} \/ {dp}
by A3, ZFMISC_1:59
.=
{cin,dp}
by ENUMSET1:1
;
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:47;
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:34
.=
{ap,bp,cp} \/ ({(GFA0AdderOutput (ap,bp,cp)),cin,dp} \ (InnerVertices (BitGFA0Str (ap,bp,cp))))
by A1, A7, GFACIRC1:33
.=
{ap,bp,cp,dp,cin}
by A6, ENUMSET1:9
;
verum