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(unsat) | = | 0 | status(unsat) | = | [] | list-extension(unsat) | = | Lex | ||
| prec(satck) | = | 0 | status(satck) | = | [2, 1] | list-extension(satck) | = | Lex | ||
| prec(sat) | = | 0 | status(sat) | = | [1] | list-extension(sat) | = | Lex | ||
| prec(verify) | = | 23 | status(verify) | = | [1] | list-extension(verify) | = | Lex | ||
| prec(guess) | = | 1 | status(guess) | = | [1] | list-extension(guess) | = | Lex | ||
| prec(choice) | = | 0 | status(choice) | = | [1] | list-extension(choice) | = | Lex | ||
| prec(negate) | = | 6 | status(negate) | = | [1] | list-extension(negate) | = | Lex | ||
| prec(1) | = | 4 | status(1) | = | [1] | list-extension(1) | = | Lex | ||
| prec(0) | = | 1 | status(0) | = | [1] | list-extension(0) | = | Lex | ||
| prec(O) | = | 0 | status(O) | = | [1] | list-extension(O) | = | Lex | ||
| prec(eq) | = | 0 | status(eq) | = | [1, 2] | list-extension(eq) | = | Lex | ||
| prec(cons) | = | 0 | status(cons) | = | [1, 2] | list-extension(cons) | = | Lex | ||
| prec(member) | = | 5 | status(member) | = | [1, 2] | list-extension(member) | = | Lex | ||
| prec(nil) | = | 0 | status(nil) | = | [] | list-extension(nil) | = | Lex | ||
| prec(false) | = | 0 | status(false) | = | [] | list-extension(false) | = | Lex | ||
| prec(if) | = | 0 | status(if) | = | [3, 1, 2] | list-extension(if) | = | Lex | ||
| prec(true) | = | 0 | status(true) | = | [] | list-extension(true) | = | Lex |
| [unsat] | = | 0 |
| [satck(x1, x2)] | = | max(0, 0 + 1 · x1, 4 + 1 · x2) |
| [sat(x1)] | = | max(0, 7 + 1 · x1) |
| [verify(x1)] | = | 3 + 1 · x1 |
| [guess(x1)] | = | max(1, 2 + 1 · x1) |
| [choice(x1)] | = | max(1, 1 + 1 · x1) |
| [negate(x1)] | = | max(0, 0 + 1 · x1) |
| [1(x1)] | = | max(0, 0 + 1 · x1) |
| [0(x1)] | = | max(0, 0 + 1 · x1) |
| [O(x1)] | = | max(7, 3 + 1 · x1) |
| [eq(x1, x2)] | = | max(3, 0 + 1 · x1, 0 + 1 · x2) |
| [cons(x1, x2)] | = | max(0, 0 + 1 · x1, 0 + 1 · x2) |
| [member(x1, x2)] | = | max(0, 0 + 1 · x1, 3 + 1 · x2) |
| [nil] | = | max(2) |
| [false] | = | max(0) |
| [if(x1, x2, x3)] | = | max(1, 0 + 1 · x1, 2 + 1 · x2, 0 + 1 · x3) |
| [true] | = | max(1) |
| 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) |
There are no rules in the TRS. Hence, it is terminating.