let ap, bp, cp, dp, cin be set ; ( [<*ap,bp*>,xor2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & GFA0AdderOutput (ap,bp,cp) in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*ap,bp*>,and2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*bp,cp*>,and2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*cp,ap*>,and2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & GFA0CarryOutput (ap,bp,cp) in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp) in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*cin,dp*>,and2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp) in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) )
set S = BitFTA0Str (ap,bp,cp,dp,cin);
set A1 = GFA0AdderOutput (ap,bp,cp);
set C1 = GFA0CarryOutput (ap,bp,cp);
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];
set p1 = {[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp)),[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2],(GFA0CarryOutput (ap,bp,cp))};
set p2 = {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp)),[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2],[<*cin,dp*>,and2],[<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))};
A1:
( [<*ap,bp*>,xor2] in {[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp)),[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2],(GFA0CarryOutput (ap,bp,cp))} & GFA0AdderOutput (ap,bp,cp) in {[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp)),[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2],(GFA0CarryOutput (ap,bp,cp))} )
by ENUMSET1:def 4;
A2:
( [<*ap,bp*>,and2] in {[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp)),[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2],(GFA0CarryOutput (ap,bp,cp))} & [<*bp,cp*>,and2] in {[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp)),[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2],(GFA0CarryOutput (ap,bp,cp))} )
by ENUMSET1:def 4;
A3:
( [<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2] in {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp)),[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2],[<*cin,dp*>,and2],[<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))} & GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp) in {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp)),[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2],[<*cin,dp*>,and2],[<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))} )
by ENUMSET1:def 4;
A4:
( [<*cp,ap*>,and2] in {[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp)),[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2],(GFA0CarryOutput (ap,bp,cp))} & GFA0CarryOutput (ap,bp,cp) in {[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp)),[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2],(GFA0CarryOutput (ap,bp,cp))} )
by ENUMSET1:def 4;
A5:
( [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] in {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp)),[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2],[<*cin,dp*>,and2],[<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))} & GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp) in {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp)),[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2],[<*cin,dp*>,and2],[<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))} )
by ENUMSET1:def 4;
A6:
( [<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2] in {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp)),[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2],[<*cin,dp*>,and2],[<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))} & [<*cin,dp*>,and2] in {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp)),[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2],[<*cin,dp*>,and2],[<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))} )
by ENUMSET1:def 4;
InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) =
(({[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp))} \/ {[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2],(GFA0CarryOutput (ap,bp,cp))}) \/ {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))}) \/ {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2],[<*cin,dp*>,and2],[<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))}
by Th1
.=
({[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp)),[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2],(GFA0CarryOutput (ap,bp,cp))} \/ {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))}) \/ {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2],[<*cin,dp*>,and2],[<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))}
by ENUMSET1:12
.=
{[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp)),[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2],(GFA0CarryOutput (ap,bp,cp))} \/ ({[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))} \/ {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2],[<*cin,dp*>,and2],[<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))})
by XBOOLE_1:4
.=
{[<*ap,bp*>,xor2],(GFA0AdderOutput (ap,bp,cp)),[<*ap,bp*>,and2],[<*bp,cp*>,and2],[<*cp,ap*>,and2],(GFA0CarryOutput (ap,bp,cp))} \/ {[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2],(GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp)),[<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2],[<*cin,dp*>,and2],[<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2],(GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp))}
by ENUMSET1:12
;
hence
( [<*ap,bp*>,xor2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & GFA0AdderOutput (ap,bp,cp) in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*ap,bp*>,and2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*bp,cp*>,and2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*cp,ap*>,and2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & GFA0CarryOutput (ap,bp,cp) in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*(GFA0AdderOutput (ap,bp,cp)),cin*>,xor2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & GFA0AdderOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp) in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*(GFA0AdderOutput (ap,bp,cp)),cin*>,and2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*cin,dp*>,and2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & [<*dp,(GFA0AdderOutput (ap,bp,cp))*>,and2] in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) & GFA0CarryOutput ((GFA0AdderOutput (ap,bp,cp)),cin,dp) in InnerVertices (BitFTA0Str (ap,bp,cp,dp,cin)) )
by A1, A2, A4, A3, A6, A5, XBOOLE_0:def 3; verum