(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(cnf, guess(cnf))
satck(cnf, assign) → if(verify(assign), assign, unsat)
Q is empty.
(1) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Combined order from the following AFS and order.
if(
x1,
x2,
x3) =
if(
x1,
x2,
x3)
true =
true
false =
false
member(
x1,
x2) =
member(
x1,
x2)
nil =
nil
cons(
x1,
x2) =
cons(
x1,
x2)
eq(
x1,
x2) =
eq(
x1,
x2)
O(
x1) =
O(
x1)
0(
x1) =
0(
x1)
1(
x1) =
x1
negate(
x1) =
negate(
x1)
choice(
x1) =
x1
guess(
x1) =
x1
verify(
x1) =
verify(
x1)
sat(
x1) =
sat(
x1)
satck(
x1,
x2) =
satck(
x1,
x2)
unsat =
unsat
Recursive path order with status [RPO].
Quasi-Precedence:
sat1 > [verify1, satck2] > member2 > [if3, cons2]
sat1 > [verify1, satck2] > member2 > [true, false, eq2]
sat1 > [verify1, satck2] > negate1 > 01 > [true, false, eq2]
sat1 > [verify1, satck2] > unsat
Status:
if3: multiset
true: multiset
false: multiset
member2: multiset
nil: multiset
cons2: multiset
eq2: multiset
O1: [1]
01: multiset
negate1: multiset
verify1: multiset
sat1: multiset
satck2: multiset
unsat: multiset
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(cnf, guess(cnf))
satck(cnf, assign) → if(verify(assign), assign, unsat)
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
eq(1(x), 1(y)) → eq(x, y)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
Q is empty.
(3) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Knuth-Bendix order [KBO] with precedence:
choice1 > guess1 > cons2 > nil > 11 > eq2
and weight map:
nil=1
1_1=1
guess_1=1
choice_1=0
cons_2=0
eq_2=0
The variable weight is 1With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
eq(1(x), 1(y)) → eq(x, y)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
(4) Obligation:
Q restricted rewrite system:
R is empty.
Q is empty.
(5) RisEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(6) YES