The rewrite relation of the following TRS is considered.
| if(true,t,e) | → | t | (1) |
| if(false,t,e) | → | e | (2) |
| member(x,nil) | → | false | (3) |
| member(x,cons(y,ys)) | → | if(eq(x,y),true,member(x,ys)) | (4) |
| eq(nil,nil) | → | true | (5) |
| eq(O(x),0(y)) | → | eq(x,y) | (6) |
| eq(0(x),1(y)) | → | false | (7) |
| eq(1(x),0(y)) | → | false | (8) |
| eq(1(x),1(y)) | → | eq(x,y) | (9) |
| negate(0(x)) | → | 1(x) | (10) |
| negate(1(x)) | → | 0(x) | (11) |
| choice(cons(x,xs)) | → | x | (12) |
| choice(cons(x,xs)) | → | choice(xs) | (13) |
| guess(nil) | → | nil | (14) |
| guess(cons(clause,cnf)) | → | cons(choice(clause),guess(cnf)) | (15) |
| verify(nil) | → | true | (16) |
| verify(cons(l,ls)) | → | if(member(negate(l),ls),false,verify(ls)) | (17) |
| sat(cnf) | → | satck(cnf,guess(cnf)) | (18) |
| satck(cnf,assign) | → | if(verify(assign),assign,unsat) | (19) |
| prec(if) | = | 0 | stat(if) | = | mul | |
| prec(true) | = | 3 | stat(true) | = | mul | |
| prec(false) | = | 3 | stat(false) | = | mul | |
| prec(member) | = | 2 | stat(member) | = | lex | |
| prec(nil) | = | 3 | stat(nil) | = | mul | |
| prec(cons) | = | 3 | stat(cons) | = | lex | |
| prec(eq) | = | 1 | stat(eq) | = | lex | |
| prec(0) | = | 3 | stat(0) | = | lex | |
| prec(negate) | = | 3 | stat(negate) | = | lex | |
| prec(sat) | = | 5 | stat(sat) | = | lex | |
| prec(satck) | = | 4 | stat(satck) | = | lex | |
| prec(unsat) | = | 4 | stat(unsat) | = | mul |
| π(if) | = | [1,2,3] |
| π(true) | = | [] |
| π(false) | = | [] |
| π(member) | = | [1,2] |
| π(nil) | = | [] |
| π(cons) | = | [1,2] |
| π(eq) | = | [2,1] |
| π(O) | = | 1 |
| π(0) | = | [1] |
| π(1) | = | 1 |
| π(negate) | = | [1] |
| π(choice) | = | 1 |
| π(guess) | = | 1 |
| π(verify) | = | 1 |
| π(sat) | = | [1] |
| π(satck) | = | [2,1] |
| π(unsat) | = | [] |
| if(true,t,e) | → | t | (1) |
| if(false,t,e) | → | e | (2) |
| member(x,nil) | → | false | (3) |
| member(x,cons(y,ys)) | → | if(eq(x,y),true,member(x,ys)) | (4) |
| eq(nil,nil) | → | true | (5) |
| eq(O(x),0(y)) | → | eq(x,y) | (6) |
| eq(0(x),1(y)) | → | false | (7) |
| eq(1(x),0(y)) | → | false | (8) |
| negate(0(x)) | → | 1(x) | (10) |
| choice(cons(x,xs)) | → | x | (12) |
| choice(cons(x,xs)) | → | choice(xs) | (13) |
| verify(cons(l,ls)) | → | if(member(negate(l),ls),false,verify(ls)) | (17) |
| sat(cnf) | → | satck(cnf,guess(cnf)) | (18) |
| satck(cnf,assign) | → | if(verify(assign),assign,unsat) | (19) |
| prec(nil) | = | 4 | weight(nil) | = | 1 | ||||
| prec(true) | = | 7 | weight(true) | = | 2 | ||||
| prec(1) | = | 1 | weight(1) | = | 1 | ||||
| prec(negate) | = | 3 | weight(negate) | = | 1 | ||||
| prec(0) | = | 2 | weight(0) | = | 2 | ||||
| prec(guess) | = | 6 | weight(guess) | = | 1 | ||||
| prec(choice) | = | 9 | weight(choice) | = | 0 | ||||
| prec(verify) | = | 8 | weight(verify) | = | 1 | ||||
| prec(cons) | = | 5 | weight(cons) | = | 0 | ||||
| prec(eq) | = | 0 | weight(eq) | = | 0 |
| eq(1(x),1(y)) | → | eq(x,y) | (9) |
| negate(1(x)) | → | 0(x) | (11) |
| guess(nil) | → | nil | (14) |
| guess(cons(clause,cnf)) | → | cons(choice(clause),guess(cnf)) | (15) |
| verify(nil) | → | true | (16) |
There are no rules in the TRS. Hence, it is terminating.