The rewrite relation of the following conditional TRS is considered.
| div(x,y) | → | pair(0,y) | | greater(y,x) ≈ true |
| div(x,y) | → | pair(s(q),r) | | leq(y,x) ≈ true, div(m(x,y),y) ≈ pair(q,r) |
| m(x,0) | → | x | |
| m(0,y) | → | 0 | |
| m(s(x),s(y)) | → | m(x,y) | |
| greater(s(x),s(y)) | → | greater(x,y) | |
| greater(s(x),0) | → | true | |
| leq(s(x),s(y)) | → | leq(x,y) | |
| leq(0,x) | → | true |
| leq($2,$1) | → | true | (1) |
| greater($2,$1) | → | true | (2) |
We collect the conditions in the fresh compound-symbol conds.
Ordered completion is applied to E0, resulting in a ground complete system. The goal equation is ground and its two terms have different normal forms in the resulting system.
Ordered completion results in the TRS R
| eq(x,x) | → | ?1 | (3) |
| leq(0,x) | → | true | (4) |
| greater(s(x),0) | → | true | (5) |
| greater(s(s(x)),s(0)) | → | true | (6) |
| m(x,0) | → | x | (7) |
and the set of equations E
| pair(0,y) | = | pair(s(q),r) | (8) |
| pair(0,x) | = | pair(0,$2) | (9) |
| pair(s(x),$2) | = | pair(s($1),y) | (10) |
| eq(conds(leq(s(x),0),true),conds(true,true)) | = | false | (11) |
| eq(conds(true,greater(0,x)),conds(true,true)) | = | false | (12) |
| pair(s(x),$2) | = | pair(0,y) | (13) |
| eq(conds(leq($2,$1),greater($2,$1)),conds(true,true)) | = | false | (14) |
| div(x,y) | = | pair(0,y) | (15) |
| div(x,y) | = | pair(s(q),r) | (16) |
| m(0,y) | = | 0 | (17) |
| m(s(x),s(y)) | = | m(x,y) | (18) |
| greater(s(x),s(y)) | = | greater(x,y) | (19) |
| leq(s(x),s(y)) | = | leq(x,y) | (20) |
It is proven that E0 is equivalent to (E,R), and (E,R) is ground complete with respect to the following reduction order:
Knuth Bendix order with w0 = 1 and the following precedence and weight functions| prec(conds) | = | 10 | weight(conds) | = | 0 | ||||
| prec(?1) | = | 11 | weight(?1) | = | 2 | ||||
| prec(eq) | = | 12 | weight(eq) | = | 1 | ||||
| prec(pair) | = | 13 | weight(pair) | = | 0 | ||||
| prec(div) | = | 14 | weight(div) | = | 1 | ||||
| prec(true) | = | 15 | weight(true) | = | 3 | ||||
| prec(0) | = | 16 | weight(0) | = | 2 | ||||
| prec(greater) | = | 17 | weight(greater) | = | 0 | ||||
| prec(leq) | = | 18 | weight(leq) | = | 1 | ||||
| prec(m) | = | 19 | weight(m) | = | 0 | ||||
| prec(false) | = | 20 | weight(false) | = | 1 | ||||
| prec(s) | = | 21 | weight(s) | = | 1 |
| greater($2,$1) | → | true | (2) |
| leq($2,$1) | → | true | (1) |
We collect the conditions in the fresh compound-symbol conds.
Ordered completion is applied to E0, resulting in a ground complete system. The goal equation is ground and its two terms have different normal forms in the resulting system.
Ordered completion results in the TRS R
| eq(x,x) | → | ?1 | (3) |
| greater(s(x),0) | → | true | (5) |
| leq(0,x) | → | true | (4) |
| m(x,0) | → | x | (7) |
and the set of equations E
| pair(0,y) | = | pair(s(q),r) | (8) |
| pair(0,x) | = | pair(0,$2) | (9) |
| eq(conds(greater(0,x),true),conds(true,true)) | = | false | (21) |
| eq(conds(true,leq(s(x),0)),conds(true,true)) | = | false | (22) |
| pair(s(x),$2) | = | pair(0,y) | (13) |
| eq(conds(greater($2,$1),leq($2,$1)),conds(true,true)) | = | false | (23) |
| div(x,y) | = | pair(0,y) | (15) |
| div(x,y) | = | pair(s(q),r) | (16) |
| m(0,y) | = | 0 | (17) |
| m(s(x),s(y)) | = | m(x,y) | (18) |
| greater(s(x),s(y)) | = | greater(x,y) | (19) |
| leq(s(x),s(y)) | = | leq(x,y) | (20) |
It is proven that E0 is equivalent to (E,R), and (E,R) is ground complete with respect to the following reduction order:
Knuth Bendix order with w0 = 1 and the following precedence and weight functions| prec(true) | = | 0 | weight(true) | = | 1 | ||||
| prec(leq) | = | 1 | weight(leq) | = | 0 | ||||
| prec(conds) | = | 2 | weight(conds) | = | 1 | ||||
| prec(eq) | = | 3 | weight(eq) | = | 1 | ||||
| prec(0) | = | 4 | weight(0) | = | 2 | ||||
| prec(pair) | = | 5 | weight(pair) | = | 0 | ||||
| prec(?1) | = | 6 | weight(?1) | = | 2 | ||||
| prec(false) | = | 7 | weight(false) | = | 8 | ||||
| prec(m) | = | 8 | weight(m) | = | 0 | ||||
| prec(greater) | = | 9 | weight(greater) | = | 0 | ||||
| prec(s) | = | 10 | weight(s) | = | 1 | ||||
| prec(div) | = | 11 | weight(div) | = | 1 |