On termination of rewriting with real numbers
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))).
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
[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
orderingPolynomial 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
orderingPolynomial 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
orderingPolynomial 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
orderingPolynomial 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
orderingPolynomial 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 orderingPolynomial interpretation:
POL(c(x1,
x2)) |
= 1 + x1 +
x2
|
POL(M(x1,
x2)) |
= a1 + x1 +
x2
|
Termination of R successfully
proved!
Duration: 2.3 sec.
|
|