let ap, bm, cp, dm, cin be set ; ( [<*ap,bm*>,xor2c] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA1AdderOutput (ap,bm,cp) in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*ap,bm*>,and2c] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*bm,cp*>,and2a] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*cp,ap*>,and2] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA1CarryOutput (ap,bm,cp) in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*cin,dm*>,and2c] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) )
set S = BitFTA1Str (ap,bm,cp,dm,cin);
set A1 = GFA1AdderOutput (ap,bm,cp);
set C1 = GFA1CarryOutput (ap,bm,cp);
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))*>,nor2];
set p1 = {[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))};
set p2 = {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c],(GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm)),[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a],[<*cin,dm*>,and2c],[<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2],(GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))};
A1:
( [<*ap,bm*>,xor2c] in {[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))} & GFA1AdderOutput (ap,bm,cp) in {[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))} )
by ENUMSET1:def 4;
A2:
( [<*ap,bm*>,and2c] in {[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))} & [<*bm,cp*>,and2a] in {[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))} )
by ENUMSET1:def 4;
A3:
( [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c] in {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c],(GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm)),[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a],[<*cin,dm*>,and2c],[<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2],(GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))} & GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) in {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c],(GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm)),[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a],[<*cin,dm*>,and2c],[<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2],(GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))} )
by ENUMSET1:def 4;
A4:
( [<*cp,ap*>,and2] in {[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))} & GFA1CarryOutput (ap,bm,cp) in {[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))} )
by ENUMSET1:def 4;
A5:
( [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] in {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c],(GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm)),[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a],[<*cin,dm*>,and2c],[<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2],(GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))} & GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) in {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c],(GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm)),[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a],[<*cin,dm*>,and2c],[<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2],(GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))} )
by ENUMSET1:def 4;
A6:
( [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a] in {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c],(GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm)),[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a],[<*cin,dm*>,and2c],[<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2],(GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))} & [<*cin,dm*>,and2c] in {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c],(GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm)),[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a],[<*cin,dm*>,and2c],[<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2],(GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))} )
by ENUMSET1:def 4;
InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) =
(({[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp))} \/ {[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))}) \/ {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c],(GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))}) \/ {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a],[<*cin,dm*>,and2c],[<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2],(GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))}
by Th11
.=
({[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))} \/ {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c],(GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))}) \/ {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a],[<*cin,dm*>,and2c],[<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2],(GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))}
by ENUMSET1:12
.=
{[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))} \/ ({[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c],(GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))} \/ {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a],[<*cin,dm*>,and2c],[<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2],(GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))})
by XBOOLE_1:4
.=
{[<*ap,bm*>,xor2c],(GFA1AdderOutput (ap,bm,cp)),[<*ap,bm*>,and2c],[<*bm,cp*>,and2a],[<*cp,ap*>,and2],(GFA1CarryOutput (ap,bm,cp))} \/ {[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c],(GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm)),[<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a],[<*cin,dm*>,and2c],[<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2],(GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm))}
by ENUMSET1:12
;
hence
( [<*ap,bm*>,xor2c] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA1AdderOutput (ap,bm,cp) in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*ap,bm*>,and2c] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*bm,cp*>,and2a] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*cp,ap*>,and2] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA1CarryOutput (ap,bm,cp) in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,xor2c] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA2AdderOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*(GFA1AdderOutput (ap,bm,cp)),cin*>,and2a] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*cin,dm*>,and2c] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & [<*dm,(GFA1AdderOutput (ap,bm,cp))*>,nor2] in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) & GFA2CarryOutput ((GFA1AdderOutput (ap,bm,cp)),cin,dm) in InnerVertices (BitFTA1Str (ap,bm,cp,dm,cin)) )
by A1, A2, A4, A3, A6, A5, XBOOLE_0:def 3; verum