University of Leicester

cms

HOME

MAP

CONTACT

On termination of rewriting with real numbers

Addendum

Two automated termination proofs of the Real Number TRS

Middeldorp's Tyrolean Termination Prover (TTT) and Giesl's Automated Program Verification Environment AProVe version 1.1 both need a few seconds to prove that the Real Number TRS is terminating. The TRS describes ternary arithmetic (addition, multiplication and unary minus) with real numbers. Notation used:

  • p(x,y) denotes x+y
  • i(x) denotes -x
  • m(x,y) denotes x.y
  • c(x,y) denotes x:y
  • d(x,y) denotes x;y
Example: 12.345 is denoted by d(c(1,2),d(3,d(4,5))).

TTT's Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    p(0,0)  → 0
2:    p(0,1)  → 1
3:    p(0,2)  → 2
4:    p(1,0)  → 1
5:    p(1,1)  → 2
6:    p(1,2)  → c(1,0)
7:    p(2,0)  → 2
8:    p(2,1)  → c(1,0)
9:    p(2,2)  → c(1,1)
10:    p(x,c(y,z))  → c(y,p(x,z))
11:    p(c(x,y),z)  → c(x,p(y,z))
12:    p(d(x,y),z)  → d(p(x,z),y)
13:    p(x,d(y,z))  → d(p(x,y),z)
14:    p(0,i(1))  → i(1)
15:    p(0,i(2))  → i(2)
16:    p(1,i(1))  → 0
17:    p(1,i(2))  → i(1)
18:    p(2,i(1))  → 1
19:    p(2,i(2))  → 0
20:    p(i(1),0)  → i(1)
21:    p(i(1),1)  → 0
22:    p(i(1),2)  → 1
23:    p(i(2),0)  → i(2)
24:    p(i(2),1)  → i(1)
25:    p(i(2),2)  → 0
26:    p(i(1),i(1))  → i(2)
27:    p(i(1),i(2))  → i(c(1,0))
28:    p(i(2),i(1))  → i(c(1,0))
29:    p(i(2),i(2))  → i(c(1,1))
30:    p(x,i(c(y,z)))  → i(c(p(i(y),x),z))
31:    p(i(c(x,y)),z)  → i(c(p(i(x),z),y))
32:    p(x,i(c(y,z)))  → i(d(p(i(x),y),z))
33:    p(i(c(x,y)),z)  → i(d(p(x,i(z)),y))
34:    m(0,0)  → 0
35:    m(0,1)  → 0
36:    m(0,2)  → 0
37:    m(1,0)  → 0
38:    m(1,1)  → 1
39:    m(1,2)  → 2
40:    m(2,0)  → 0
41:    m(2,1)  → 2
42:    m(2,2)  → c(1,1)
43:    m(c(x,y),z)  → c(m(x,z),m(y,z))
44:    m(x,c(y,z))  → c(m(x,y),m(x,z))
45:    m(d(x,y),z)  → d(m(x,z),m(y,z))
46:    m(x,d(y,z))  → d(m(x,y),m(x,z))
47:    m(i(c(x,y)),z)  → i(c(m(x,z),m(y,z)))
48:    m(x,i(c(y,z)))  → i(c(m(x,y),m(x,z)))
49:    c(x,c(y,z))  → c(p(x,y),z)
50:    c(0,x)  → x
51:    c(d(x,y),z)  → c(x,p(y,z))
52:    c(x,d(y,z))  → d(c(x,y),z)
53:    c(i(x),y)  → i(c(x,i(y)))
54:    c(x,i(c(y,z)))  → i(c(p(i(x),y),z))
55:    d(x,0)  → x
56:    d(d(x,y),z)  → d(x,p(y,z))
57:    d(x,c(y,z))  → d(p(x,y),z)
58:    d(w,d(c(x,y),z))  → d(p(w,x),d(y,z))
59:    d(x,i(y))  → i(c(i(x),y))
60:    d(i(c(x,y)),z)  → i(d(x,p(y,i(z))))
61:    i(0)  → 0
62:    i(i(x))  → x
There are 84 dependency pairs:
63:    C(x,c(y,z))  → C(p(x,y),z)
64:    C(x,c(y,z))  → P(x,y)
65:    C(x,d(y,z))  → C(x,y)
66:    C(x,d(y,z))  → D(c(x,y),z)
67:    C(x,i(c(y,z)))  → C(p(i(x),y),z)
68:    C(x,i(c(y,z)))  → I(x)
69:    C(x,i(c(y,z)))  → I(c(p(i(x),y),z))
70:    C(x,i(c(y,z)))  → P(i(x),y)
71:    C(d(x,y),z)  → C(x,p(y,z))
72:    C(d(x,y),z)  → P(y,z)
73:    C(i(x),y)  → C(x,i(y))
74:    C(i(x),y)  → I(y)
75:    C(i(x),y)  → I(c(x,i(y)))
76:    D(x,c(y,z))  → D(p(x,y),z)
77:    D(x,c(y,z))  → P(x,y)
78:    D(x,i(y))  → C(i(x),y)
79:    D(x,i(y))  → I(x)
80:    D(x,i(y))  → I(c(i(x),y))
81:    D(d(x,y),z)  → D(x,p(y,z))
82:    D(d(x,y),z)  → P(y,z)
83:    D(i(c(x,y)),z)  → D(x,p(y,i(z)))
84:    D(i(c(x,y)),z)  → I(z)
85:    D(i(c(x,y)),z)  → I(d(x,p(y,i(z))))
86:    D(i(c(x,y)),z)  → P(y,i(z))
87:    D(w,d(c(x,y),z))  → D(y,z)
88:    D(w,d(c(x,y),z))  → D(p(w,x),d(y,z))
89:    D(w,d(c(x,y),z))  → P(w,x)
90:    M(x,c(y,z))  → C(m(x,y),m(x,z))
91:    M(x,c(y,z))  → M(x,y)
92:    M(x,c(y,z))  → M(x,z)
93:    M(x,d(y,z))  → D(m(x,y),m(x,z))
94:    M(x,d(y,z))  → M(x,y)
95:    M(x,d(y,z))  → M(x,z)
96:    M(x,i(c(y,z)))  → C(m(x,y),m(x,z))
97:    M(x,i(c(y,z)))  → I(c(m(x,y),m(x,z)))
98:    M(x,i(c(y,z)))  → M(x,y)
99:    M(x,i(c(y,z)))  → M(x,z)
100:    M(2,2)  → C(1,1)
101:    M(c(x,y),z)  → C(m(x,z),m(y,z))
102:    M(c(x,y),z)  → M(x,z)
103:    M(c(x,y),z)  → M(y,z)
104:    M(d(x,y),z)  → D(m(x,z),m(y,z))
105:    M(d(x,y),z)  → M(x,z)
106:    M(d(x,y),z)  → M(y,z)
107:    M(i(c(x,y)),z)  → C(m(x,z),m(y,z))
108:    M(i(c(x,y)),z)  → I(c(m(x,z),m(y,z)))
109:    M(i(c(x,y)),z)  → M(x,z)
110:    M(i(c(x,y)),z)  → M(y,z)
111:    P(x,c(y,z))  → C(y,p(x,z))
112:    P(x,c(y,z))  → P(x,z)
113:    P(x,d(y,z))  → D(p(x,y),z)
114:    P(x,d(y,z))  → P(x,y)
115:    P(x,i(c(y,z)))  → C(p(i(y),x),z)
116:    P(x,i(c(y,z)))  → D(p(i(x),y),z)
117:    P(x,i(c(y,z)))  → I(x)
118:    P(x,i(c(y,z)))  → I(y)
119:    P(x,i(c(y,z)))  → I(c(p(i(y),x),z))
120:    P(x,i(c(y,z)))  → I(d(p(i(x),y),z))
121:    P(x,i(c(y,z)))  → P(i(x),y)
122:    P(x,i(c(y,z)))  → P(i(y),x)
123:    P(1,2)  → C(1,0)
124:    P(1,i(2))  → I(1)
125:    P(2,1)  → C(1,0)
126:    P(2,2)  → C(1,1)
127:    P(c(x,y),z)  → C(x,p(y,z))
128:    P(c(x,y),z)  → P(y,z)
129:    P(d(x,y),z)  → D(p(x,z),y)
130:    P(d(x,y),z)  → P(x,z)
131:    P(i(1),i(1))  → I(2)
132:    P(i(1),i(2))  → C(1,0)
133:    P(i(1),i(2))  → I(c(1,0))
134:    P(i(2),1)  → I(1)
135:    P(i(2),i(1))  → C(1,0)
136:    P(i(2),i(1))  → I(c(1,0))
137:    P(i(2),i(2))  → C(1,1)
138:    P(i(2),i(2))  → I(c(1,1))
139:    P(i(c(x,y)),z)  → C(p(i(x),z),y)
140:    P(i(c(x,y)),z)  → D(p(x,i(z)),y)
141:    P(i(c(x,y)),z)  → I(x)
142:    P(i(c(x,y)),z)  → I(z)
143:    P(i(c(x,y)),z)  → I(c(p(i(x),z),y))
144:    P(i(c(x,y)),z)  → I(d(p(x,i(z)),y))
145:    P(i(c(x,y)),z)  → P(x,i(z))
146:    P(i(c(x,y)),z)  → P(i(x),z)
The approximated dependency graph contains 2 SCCs: {63-67,70-73,76-78,81-83,86-89,111-116,121,122,127-130,139,140,145,146} and {91,92,94,95,98,99,102,103,105,106,109,110}.
  • Consider the SCC {63-67,70-73,76-78,81-83,86-89,111-116,121,122,127-130,139,140,145,146}. The usable rules are {1-33,49-62}. By taking the polynomial interpretation [0] = 0, [1] = [w] = 1, [2] = 2, [i](x) = x, and [C](x,y) = [D](x,y) = [P](x,y) = [c](x,y) = [d](x,y) = [p](x,y) = x + y, the rules in {1-5,7,10-15,20,23,26,30-33,49-67,70-73,76-78,81-83,86,88,89,111-116,121,122,127-130,139,140,145,146} are weakly decreasing and the rules in {6,8,9,16-19,21,22,24,25,27-29,87} are strictly decreasing. There is one new SCC.
    • Consider the SCC {63-67,70-73,76-78,81-83,86,88,89,111-116,121,122,127-130,139,140,145,146}. The usable rules are {1-33,49-62}. By taking the polynomial interpretation [0] = 0, [1] = [w] = 1, [2] = 2, [i](x) = x, [C](x,y) = [D](x,y) = [P](x,y) = [p](x,y) = x + y, and [c](x,y) = [d](x,y) = x + y + 1, the rules in {1-5,7,10-15,20,23,26,30-33,52,53,59,61,62,66,73,78} are weakly decreasing and the rules in {6,8,9,16-19,21,22,24,25,27-29,49-51,54-58,60,63-65,67,70-72,76,77,81-83,86,88,89,111-116,121,122,127-130,139,140,145,146} are strictly decreasing. There is one new SCC.
      • Consider the SCC {66,73,78}. The usable rules are {1-33,49-62}. By taking the polynomial interpretation [0] = 0, [1] = [w] = 1, [2] = 2, [i](x) = x, [p](x,y) = x + y, [c](x,y) = [d](x,y) = x + y + 1, and [C](x,y) = [D](x,y) = y, the rules in {1-5,7,10-15,20,23,26,30-33,52,53,59,61,62,73,78} are weakly decreasing and the rules in {6,8,9,16-19,21,22,24,25,27-29,49-51,54-58,60,66} are strictly decreasing. There is one new SCC.
        • Consider the SCC {73}. By taking the simple projection π with π(C) = 1 together with the subterm relation, rule 73 is strictly decreasing.

  • Consider the SCC {91,92,94,95,98,99,102,103,105,106,109,110}. By taking the simple projection π with π(M) = 1 together with the subterm relation, the rules in {91,92,94,95,98,99} are weakly decreasing and the rules in {102,103,105,106,109,110} are strictly decreasing. There is one new SCC.
    • Consider the SCC {91,92,94,95,98,99}. By taking the simple projection π with π(M) = 2 together with the subterm relation, the rules in {91,92,94,95,98,99} are strictly decreasing.
Tyrolean Termination Tool   ---  October 13, 2004

AProVE's Termination Proof Script

Term rewriting system R:

[x, y, z, w]
p(0, 0) -> 0
p(0, 1) -> 1
p(0, 2) -> 2
p(1, 0) -> 1
p(1, 1) -> 2
p(1, 2) -> c(1, 0)
p(2, 0) -> 2
p(2, 1) -> c(1, 0)
p(2, 2) -> c(1, 1)
p(x, c(y, z)) -> c(y, p(x, z))
p(c(x, y), z) -> c(x, p(y, z))
p(d(x, y), z) -> d(p(x, z), y)
p(x, d(y, z)) -> d(p(x, y), z)
m(0, 0) -> 0
m(0, 1) -> 0
m(0, 2) -> 0
m(1, 0) -> 0
m(1, 1) -> 1
m(1, 2) -> 2
m(2, 0) -> 0
m(2, 1) -> 2
m(2, 2) -> c(1, 1)
m(c(x, y), z) -> c(m(x, z), m(y, z))
m(x, c(y, z)) -> c(m(x, y), m(x, z))
c(x, c(y, z)) -> c(p(x, y), z)
c(0, x) -> x
c(d(x, y), z) -> c(x, p(y, z))
c(x, d(y, z)) -> d(c(x, y), z)
d(x, 0) -> x
d(d(x, y), z) -> d(x, p(y, z))
d(x, c(y, z)) -> d(p(x, y), z)
d(w, d(c(x, y), z)) -> d(p(w, x), d(y, z))
Dependency Pairs for R
C(d(x, y), z) -> C(x, p(y, z))
C(d(x, y), z) -> P(y, z)
C(x, c(y, z)) -> C(p(x, y), z)
C(x, c(y, z)) -> P(x, y)
C(x, d(y, z)) -> D(c(x, y), z)
C(x, d(y, z)) -> C(x, y)
D(d(x, y), z) -> D(x, p(y, z))
D(d(x, y), z) -> P(y, z)
D(w, d(c(x, y), z)) -> D(p(w, x), d(y, z))
D(w, d(c(x, y), z)) -> P(w, x)
D(w, d(c(x, y), z)) -> D(y, z)
D(x, c(y, z)) -> D(p(x, y), z)
D(x, c(y, z)) -> P(x, y)
P(d(x, y), z) -> D(p(x, z), y)
P(d(x, y), z) -> P(x, z)
P(2, 1) -> C(1, 0)
P(x, c(y, z)) -> C(y, p(x, z))
P(x, c(y, z)) -> P(x, z)
P(1, 2) -> C(1, 0)
P(c(x, y), z) -> C(x, p(y, z))
P(c(x, y), z) -> P(y, z)
P(x, d(y, z)) -> D(p(x, y), z)
P(x, d(y, z)) -> P(x, y)
P(2, 2) -> C(1, 1)
M(2, 2) -> C(1, 1)
M(c(x, y), z) -> C(m(x, z), m(y, z))
M(c(x, y), z) -> M(x, z)
M(c(x, y), z) -> M(y, z)
M(x, c(y, z)) -> C(m(x, y), m(x, z))
M(x, c(y, z)) -> M(x, y)
M(x, c(y, z)) -> M(x, z)
Termination of R to be shown using SCCs of the Estimated Dependency Pair Graph. The Dependency Pair Graph for R contains 2 SCCs:
1
C(x, d(y, z)) -> C(x, y)
P(x, d(y, z)) -> P(x, y)
D(x, c(y, z)) -> P(x, y)
D(x, c(y, z)) -> D(p(x, y), z)
D(w, d(c(x, y), z)) -> D(y, z)
P(x, d(y, z)) -> D(p(x, y), z)
P(c(x, y), z) -> P(y, z)
D(w, d(c(x, y), z)) -> P(w, x)
D(w, d(c(x, y), z)) -> D(p(w, x), d(y, z))
C(x, d(y, z)) -> D(c(x, y), z)
P(c(x, y), z) -> C(x, p(y, z))
P(x, c(y, z)) -> P(x, z)
C(x, c(y, z)) -> P(x, y)
C(x, c(y, z)) -> C(p(x, y), z)
P(x, c(y, z)) -> C(y, p(x, z))
P(d(x, y), z) -> P(x, z)
D(d(x, y), z) -> P(y, z)
D(d(x, y), z) -> D(x, p(y, z))
P(d(x, y), z) -> D(p(x, z), y)
C(d(x, y), z) -> P(y, z)
C(d(x, y), z) -> C(x, p(y, z))
Oriented Rule(s):

p(d(x, y), z) -> d(p(x, z), y)
p(1, 0) -> 1
p(0, 0) -> 0
p(2, 1) -> c(1, 0)
p(1, 1) -> 2
p(2, 0) -> 2
p(x, c(y, z)) -> c(y, p(x, z))
p(0, 1) -> 1
p(1, 2) -> c(1, 0)
p(c(x, y), z) -> c(x, p(y, z))
p(0, 2) -> 2
p(x, d(y, z)) -> d(p(x, y), z)
p(2, 2) -> c(1, 1)
d(d(x, y), z) -> d(x, p(y, z))
d(w, d(c(x, y), z)) -> d(p(w, x), d(y, z))
d(x, c(y, z)) -> d(p(x, y), z)
d(x, 0) -> x
c(d(x, y), z) -> c(x, p(y, z))
c(x, c(y, z)) -> c(p(x, y), z)
c(0, x) -> x
c(x, d(y, z)) -> d(c(x, y), z)

Ordering: Polynomial ordering
Polynomial interpretation:
  POL(p(x1, x2)) =  x1 + x2  
  POL(c(x1, x2)) =  x1 + x2  
  POL(P(x1, x2)) =  x1 + x2  
  POL(d(x1, x2)) =  x1 + x2  
  POL(2) =  1  
  POL(D(x1, x2)) =  x1 + x2  
  POL(0) =  0  
  POL(C(x1, x2)) =  x1 + x2  
  POL(1) =  1  

where we removed the following rules (MRR):

p(2, 1) -> c(1, 0)
p(1, 1) -> 2
p(1, 2) -> c(1, 0)
Need to check 1 sub cycle of this SCC.
1.1
P(x, d(y, z)) -> P(x, y)
D(x, c(y, z)) -> P(x, y)
D(x, c(y, z)) -> D(p(x, y), z)
D(w, d(c(x, y), z)) -> D(y, z)
P(x, d(y, z)) -> D(p(x, y), z)
P(c(x, y), z) -> P(y, z)
D(w, d(c(x, y), z)) -> P(w, x)
D(w, d(c(x, y), z)) -> D(p(w, x), d(y, z))
C(x, d(y, z)) -> D(c(x, y), z)
P(c(x, y), z) -> C(x, p(y, z))
P(x, c(y, z)) -> P(x, z)
C(x, c(y, z)) -> P(x, y)
C(x, c(y, z)) -> C(p(x, y), z)
P(x, c(y, z)) -> C(y, p(x, z))
P(d(x, y), z) -> P(x, z)
D(d(x, y), z) -> P(y, z)
D(d(x, y), z) -> D(x, p(y, z))
P(d(x, y), z) -> D(p(x, z), y)
C(d(x, y), z) -> P(y, z)
C(d(x, y), z) -> C(x, p(y, z))
C(x, d(y, z)) -> C(x, y)
Oriented Rule(s):

p(d(x, y), z) -> d(p(x, z), y)
p(1, 0) -> 1
p(0, 0) -> 0
p(2, 0) -> 2
p(x, c(y, z)) -> c(y, p(x, z))
p(0, 1) -> 1
p(c(x, y), z) -> c(x, p(y, z))
p(0, 2) -> 2
p(x, d(y, z)) -> d(p(x, y), z)
p(2, 2) -> c(1, 1)
d(d(x, y), z) -> d(x, p(y, z))
d(w, d(c(x, y), z)) -> d(p(w, x), d(y, z))
d(x, c(y, z)) -> d(p(x, y), z)
d(x, 0) -> x
c(d(x, y), z) -> c(x, p(y, z))
c(x, c(y, z)) -> c(p(x, y), z)
c(0, x) -> x
c(x, d(y, z)) -> d(c(x, y), z)

Ordering: Polynomial ordering
Polynomial interpretation:
  POL(p(x1, x2)) =  x1 + x2  
  POL(c(x1, x2)) =  x1 + x2  
  POL(P(x1, x2)) =  x1 + x2  
  POL(d(x1, x2)) =  x1 + x2  
  POL(2) =  1  
  POL(D(x1, x2)) =  x1 + x2  
  POL(0) =  0  
  POL(C(x1, x2)) =  x1 + x2  
  POL(1) =  0  

where we removed the following rules (MRR):

p(2, 2) -> c(1, 1)
Need to check 1 sub cycle of this SCC.
1.1.1
C(x, d(y, z)) -> C(x, y)
C(x, d(y, z)) -> D(c(x, y), z)
D(x, c(y, z)) -> P(x, y)
D(x, c(y, z)) -> D(p(x, y), z)
D(w, d(c(x, y), z)) -> D(y, z)
D(w, d(c(x, y), z)) -> P(w, x)
D(w, d(c(x, y), z)) -> D(p(w, x), d(y, z))
P(x, d(y, z)) -> D(p(x, y), z)
P(c(x, y), z) -> P(y, z)
C(x, c(y, z)) -> P(x, y)
C(x, c(y, z)) -> C(p(x, y), z)
P(c(x, y), z) -> C(x, p(y, z))
P(x, c(y, z)) -> P(x, z)
C(d(x, y), z) -> P(y, z)
C(d(x, y), z) -> C(x, p(y, z))
P(x, c(y, z)) -> C(y, p(x, z))
P(d(x, y), z) -> P(x, z)
D(d(x, y), z) -> P(y, z)
D(d(x, y), z) -> D(x, p(y, z))
P(d(x, y), z) -> D(p(x, z), y)
P(x, d(y, z)) -> P(x, y)
Oriented Rule(s):

c(d(x, y), z) -> c(x, p(y, z))
c(x, c(y, z)) -> c(p(x, y), z)
c(0, x) -> x
c(x, d(y, z)) -> d(c(x, y), z)
p(d(x, y), z) -> d(p(x, z), y)
p(1, 0) -> 1
p(0, 0) -> 0
p(2, 0) -> 2
p(x, c(y, z)) -> c(y, p(x, z))
p(0, 1) -> 1
p(c(x, y), z) -> c(x, p(y, z))
p(0, 2) -> 2
p(x, d(y, z)) -> d(p(x, y), z)
d(d(x, y), z) -> d(x, p(y, z))
d(w, d(c(x, y), z)) -> d(p(w, x), d(y, z))
d(x, c(y, z)) -> d(p(x, y), z)
d(x, 0) -> x

Ordering: Polynomial ordering
Polynomial interpretation:
  POL(p(x1, x2)) =  x1 + x2  
  POL(c(x1, x2)) =  1 + x1 + x2  
  POL(P(x1, x2)) =  x1 + x2  
  POL(d(x1, x2)) =  x1 + x2  
  POL(2) =  0  
  POL(D(x1, x2)) =  x1 + x2  
  POL(0) =  0  
  POL(C(x1, x2)) =  1 + x1 + x2  
  POL(1) =  0  

where we removed the following rules (MRR):

c(x, c(y, z)) -> c(p(x, y), z)
c(0, x) -> x
d(w, d(c(x, y), z)) -> d(p(w, x), d(y, z))
d(x, c(y, z)) -> d(p(x, y), z)
Need to check 1 sub cycle of this SCC.
1.1.1.1
P(x, d(y, z)) -> P(x, y)
P(x, d(y, z)) -> D(p(x, y), z)
P(c(x, y), z) -> C(x, p(y, z))
P(x, c(y, z)) -> C(y, p(x, z))
P(d(x, y), z) -> P(x, z)
P(d(x, y), z) -> D(p(x, z), y)
D(d(x, y), z) -> P(y, z)
D(d(x, y), z) -> D(x, p(y, z))
C(x, d(y, z)) -> D(c(x, y), z)
C(d(x, y), z) -> C(x, p(y, z))
C(x, d(y, z)) -> C(x, y)
Oriented Rule(s):

p(d(x, y), z) -> d(p(x, z), y)
p(1, 0) -> 1
p(0, 0) -> 0
p(2, 0) -> 2
p(x, c(y, z)) -> c(y, p(x, z))
p(0, 1) -> 1
p(c(x, y), z) -> c(x, p(y, z))
p(0, 2) -> 2
p(x, d(y, z)) -> d(p(x, y), z)
c(d(x, y), z) -> c(x, p(y, z))
c(x, d(y, z)) -> d(c(x, y), z)
d(d(x, y), z) -> d(x, p(y, z))
d(x, 0) -> x

Ordering: Polynomial ordering
Polynomial interpretation:
  POL(p(x1, x2)) =  x1 + x2  
  POL(c(x1, x2)) =  x1 + x2  
  POL(P(x1, x2)) =  x1 + x2  
  POL(d(x1, x2)) =  x1 + x2  
  POL(2) =  0  
  POL(D(x1, x2)) =  x1 + x2  
  POL(0) =  1  
  POL(C(x1, x2)) =  x1 + x2  
  POL(1) =  0  

where we removed the following rules (MRR):

p(1, 0) -> 1
p(0, 0) -> 0
p(2, 0) -> 2
p(0, 1) -> 1
p(0, 2) -> 2
d(x, 0) -> x
Need to check 1 sub cycle of this SCC.
1.1.1.1.1
P(x, d(y, z)) -> D(p(x, y), z)
P(c(x, y), z) -> C(x, p(y, z))
C(x, d(y, z)) -> C(x, y)
C(x, d(y, z)) -> D(c(x, y), z)
C(d(x, y), z) -> C(x, p(y, z))
P(x, c(y, z)) -> C(y, p(x, z))
P(d(x, y), z) -> P(x, z)
D(d(x, y), z) -> P(y, z)
D(d(x, y), z) -> D(x, p(y, z))
P(d(x, y), z) -> D(p(x, z), y)
P(x, d(y, z)) -> P(x, y)
Oriented Rule(s):

p(d(x, y), z) -> d(p(x, z), y)
p(x, c(y, z)) -> c(y, p(x, z))
p(c(x, y), z) -> c(x, p(y, z))
p(x, d(y, z)) -> d(p(x, y), z)
c(d(x, y), z) -> c(x, p(y, z))
c(x, d(y, z)) -> d(c(x, y), z)
d(d(x, y), z) -> d(x, p(y, z))

Ordering: Polynomial ordering
Polynomial interpretation:
  POL(p(x1, x2)) =  x1 + x2  
  POL(c(x1, x2)) =  x1 + x2  
  POL(P(x1, x2)) =  x1 + x2  
  POL(d(x1, x2)) =  1 + x1 + x2  
  POL(D(x1, x2)) =  x1 + x2  
  POL(C(x1, x2)) =  x1 + x2  

2M(x, c(y, z)) -> M(x, z)
M(x, c(y, z)) -> M(x, y)
M(c(x, y), z) -> M(y, z)
M(c(x, y), z) -> M(x, z)
Oriented Rule(s): none
Ordering: Polynomial ordering
Polynomial interpretation:
  POL(c(x1, x2)) =  1 + x1 + x2  
  POL(M(x1, x2)) =  a1 + x1 + x2  

Termination of R successfully proved!


Duration: 2.3 sec.

Author: F.J. de Vries (fdv1 at mcs.le.ac.uk).
© University of Leicester Wed Oct 13, 2004. . Last modified: 15th October 2004, 13:35:36
CMS Web Maintainer. Any opinions expressed on this page are those of the author.