YES(O(1),O(n^2)) 33.14/9.88 YES(O(1),O(n^2)) 33.14/9.88 33.14/9.88 We are left with following problem, upon which TcT provides the 33.14/9.88 certificate YES(O(1),O(n^2)). 33.14/9.88 33.14/9.88 Strict Trs: 33.14/9.88 { if(true(), t, e) -> t 33.14/9.88 , if(false(), t, e) -> e 33.14/9.88 , member(x, nil()) -> false() 33.14/9.88 , member(x, cons(y, ys)) -> if(eq(x, y), true(), member(x, ys)) 33.14/9.88 , eq(nil(), nil()) -> true() 33.14/9.88 , eq(O(x), 0(y)) -> eq(x, y) 33.14/9.88 , eq(0(x), 1(y)) -> false() 33.14/9.88 , eq(1(x), 0(y)) -> false() 33.14/9.88 , eq(1(x), 1(y)) -> eq(x, y) 33.14/9.88 , negate(0(x)) -> 1(x) 33.14/9.88 , negate(1(x)) -> 0(x) 33.14/9.88 , choice(cons(x, xs)) -> x 33.14/9.88 , choice(cons(x, xs)) -> choice(xs) 33.14/9.88 , guess(nil()) -> nil() 33.14/9.88 , guess(cons(clause, cnf)) -> cons(choice(clause), guess(cnf)) 33.14/9.88 , verify(nil()) -> true() 33.14/9.88 , verify(cons(l, ls)) -> 33.14/9.88 if(member(negate(l), ls), false(), verify(ls)) 33.14/9.88 , sat(cnf) -> satck(cnf, guess(cnf)) 33.14/9.88 , satck(cnf, assign) -> if(verify(assign), assign, unsat()) } 33.14/9.88 Obligation: 33.14/9.88 innermost runtime complexity 33.14/9.88 Answer: 33.14/9.88 YES(O(1),O(n^2)) 33.14/9.88 33.14/9.88 The weightgap principle applies (using the following nonconstant 33.14/9.88 growth matrix-interpretation) 33.14/9.88 33.14/9.88 The following argument positions are usable: 33.14/9.88 Uargs(if) = {1, 3}, Uargs(member) = {1}, Uargs(cons) = {1, 2}, 33.14/9.88 Uargs(satck) = {2} 33.14/9.88 33.14/9.88 TcT has computed the following matrix interpretation satisfying 33.14/9.88 not(EDA) and not(IDA(1)). 33.14/9.88 33.14/9.88 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1] 33.14/9.88 33.14/9.88 [true] = [0] 33.14/9.88 33.14/9.88 [false] = [0] 33.14/9.88 33.14/9.88 [member](x1, x2) = [1] x1 + [7] 33.14/9.88 33.14/9.88 [nil] = [0] 33.14/9.88 33.14/9.88 [cons](x1, x2) = [1] x1 + [1] x2 + [1] 33.14/9.88 33.14/9.88 [eq](x1, x2) = [7] 33.14/9.88 33.14/9.88 [O](x1) = [1] x1 + [7] 33.14/9.88 33.14/9.88 [0](x1) = [7] 33.14/9.88 33.14/9.88 [1](x1) = [7] 33.14/9.88 33.14/9.88 [negate](x1) = [0] 33.14/9.88 33.14/9.88 [choice](x1) = [1] x1 + [7] 33.14/9.88 33.14/9.88 [guess](x1) = [1] x1 + [7] 33.14/9.88 33.14/9.88 [verify](x1) = [0] 33.14/9.88 33.14/9.88 [sat](x1) = [1] x1 + [7] 33.14/9.88 33.14/9.88 [satck](x1, x2) = [1] x2 + [7] 33.14/9.88 33.14/9.88 [unsat] = [7] 33.14/9.88 33.14/9.88 The order satisfies the following ordering constraints: 33.14/9.88 33.14/9.88 [if(true(), t, e)] = [1] t + [1] e + [1] 33.14/9.88 > [1] t + [0] 33.14/9.88 = [t] 33.14/9.88 33.14/9.88 [if(false(), t, e)] = [1] t + [1] e + [1] 33.14/9.88 > [1] e + [0] 33.14/9.88 = [e] 33.14/9.88 33.14/9.88 [member(x, nil())] = [1] x + [7] 33.14/9.88 > [0] 33.14/9.88 = [false()] 33.14/9.88 33.14/9.88 [member(x, cons(y, ys))] = [1] x + [7] 33.14/9.88 ? [1] x + [15] 33.14/9.88 = [if(eq(x, y), true(), member(x, ys))] 33.14/9.88 33.14/9.88 [eq(nil(), nil())] = [7] 33.14/9.88 > [0] 33.14/9.88 = [true()] 33.14/9.88 33.14/9.88 [eq(O(x), 0(y))] = [7] 33.14/9.88 >= [7] 33.14/9.88 = [eq(x, y)] 33.14/9.88 33.14/9.88 [eq(0(x), 1(y))] = [7] 33.14/9.88 > [0] 33.14/9.88 = [false()] 33.14/9.88 33.14/9.88 [eq(1(x), 0(y))] = [7] 33.14/9.88 > [0] 33.14/9.88 = [false()] 33.14/9.88 33.14/9.88 [eq(1(x), 1(y))] = [7] 33.14/9.88 >= [7] 33.14/9.88 = [eq(x, y)] 33.14/9.88 33.14/9.88 [negate(0(x))] = [0] 33.14/9.88 ? [7] 33.14/9.88 = [1(x)] 33.14/9.88 33.14/9.88 [negate(1(x))] = [0] 33.14/9.88 ? [7] 33.14/9.88 = [0(x)] 33.14/9.88 33.14/9.88 [choice(cons(x, xs))] = [1] x + [1] xs + [8] 33.14/9.88 > [1] x + [0] 33.14/9.88 = [x] 33.14/9.88 33.14/9.88 [choice(cons(x, xs))] = [1] x + [1] xs + [8] 33.14/9.88 > [1] xs + [7] 33.14/9.88 = [choice(xs)] 33.14/9.88 33.14/9.88 [guess(nil())] = [7] 33.14/9.88 > [0] 33.14/9.88 = [nil()] 33.14/9.88 33.14/9.88 [guess(cons(clause, cnf))] = [1] clause + [1] cnf + [8] 33.14/9.88 ? [1] clause + [1] cnf + [15] 33.14/9.88 = [cons(choice(clause), guess(cnf))] 33.14/9.88 33.14/9.88 [verify(nil())] = [0] 33.14/9.88 >= [0] 33.14/9.88 = [true()] 33.14/9.88 33.14/9.88 [verify(cons(l, ls))] = [0] 33.14/9.88 ? [8] 33.14/9.88 = [if(member(negate(l), ls), false(), verify(ls))] 33.14/9.88 33.14/9.88 [sat(cnf)] = [1] cnf + [7] 33.14/9.88 ? [1] cnf + [14] 33.14/9.88 = [satck(cnf, guess(cnf))] 33.14/9.88 33.14/9.88 [satck(cnf, assign)] = [1] assign + [7] 33.14/9.88 ? [1] assign + [8] 33.14/9.88 = [if(verify(assign), assign, unsat())] 33.14/9.88 33.14/9.88 33.14/9.88 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 33.14/9.88 33.14/9.88 We are left with following problem, upon which TcT provides the 33.14/9.88 certificate YES(O(1),O(n^2)). 33.14/9.88 33.14/9.88 Strict Trs: 33.14/9.88 { member(x, cons(y, ys)) -> if(eq(x, y), true(), member(x, ys)) 33.14/9.88 , eq(O(x), 0(y)) -> eq(x, y) 33.14/9.88 , eq(1(x), 1(y)) -> eq(x, y) 33.14/9.88 , negate(0(x)) -> 1(x) 33.14/9.88 , negate(1(x)) -> 0(x) 33.14/9.88 , guess(cons(clause, cnf)) -> cons(choice(clause), guess(cnf)) 33.14/9.88 , verify(nil()) -> true() 33.14/9.88 , verify(cons(l, ls)) -> 33.14/9.88 if(member(negate(l), ls), false(), verify(ls)) 33.14/9.88 , sat(cnf) -> satck(cnf, guess(cnf)) 33.14/9.88 , satck(cnf, assign) -> if(verify(assign), assign, unsat()) } 33.14/9.88 Weak Trs: 33.14/9.88 { if(true(), t, e) -> t 33.14/9.88 , if(false(), t, e) -> e 33.14/9.88 , member(x, nil()) -> false() 33.14/9.88 , eq(nil(), nil()) -> true() 33.14/9.88 , eq(0(x), 1(y)) -> false() 33.14/9.88 , eq(1(x), 0(y)) -> false() 33.14/9.88 , choice(cons(x, xs)) -> x 33.14/9.88 , choice(cons(x, xs)) -> choice(xs) 33.14/9.88 , guess(nil()) -> nil() } 33.14/9.88 Obligation: 33.14/9.88 innermost runtime complexity 33.14/9.88 Answer: 33.14/9.88 YES(O(1),O(n^2)) 33.14/9.88 33.14/9.88 The weightgap principle applies (using the following nonconstant 33.14/9.88 growth matrix-interpretation) 33.14/9.88 33.14/9.88 The following argument positions are usable: 33.14/9.88 Uargs(if) = {1, 3}, Uargs(member) = {1}, Uargs(cons) = {1, 2}, 33.14/9.88 Uargs(satck) = {2} 33.14/9.88 33.14/9.88 TcT has computed the following matrix interpretation satisfying 33.14/9.88 not(EDA) and not(IDA(1)). 33.14/9.88 33.14/9.88 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 33.14/9.88 33.14/9.88 [true] = [2] 33.14/9.88 33.14/9.88 [false] = [0] 33.14/9.88 33.14/9.88 [member](x1, x2) = [1] x1 + [0] 33.14/9.88 33.14/9.88 [nil] = [7] 33.14/9.88 33.14/9.88 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 33.14/9.88 33.14/9.88 [eq](x1, x2) = [6] 33.14/9.88 33.14/9.88 [O](x1) = [1] x1 + [7] 33.14/9.88 33.14/9.88 [0](x1) = [0] 33.14/9.88 33.14/9.88 [1](x1) = [0] 33.14/9.88 33.14/9.88 [negate](x1) = [1] 33.14/9.88 33.14/9.88 [choice](x1) = [1] x1 + [0] 33.14/9.88 33.14/9.88 [guess](x1) = [1] x1 + [0] 33.14/9.88 33.14/9.88 [verify](x1) = [0] 33.14/9.88 33.14/9.88 [sat](x1) = [1] x1 + [7] 33.14/9.88 33.14/9.88 [satck](x1, x2) = [1] x2 + [3] 33.14/9.88 33.14/9.88 [unsat] = [0] 33.14/9.88 33.14/9.88 The order satisfies the following ordering constraints: 33.14/9.88 33.14/9.88 [if(true(), t, e)] = [1] t + [1] e + [2] 33.14/9.88 > [1] t + [0] 33.14/9.88 = [t] 33.14/9.88 33.14/9.88 [if(false(), t, e)] = [1] t + [1] e + [0] 33.14/9.88 >= [1] e + [0] 33.14/9.88 = [e] 33.14/9.88 33.14/9.88 [member(x, nil())] = [1] x + [0] 33.14/9.88 >= [0] 33.14/9.88 = [false()] 33.14/9.88 33.14/9.88 [member(x, cons(y, ys))] = [1] x + [0] 33.14/9.88 ? [1] x + [8] 33.14/9.88 = [if(eq(x, y), true(), member(x, ys))] 33.14/9.88 33.14/9.88 [eq(nil(), nil())] = [6] 33.14/9.88 > [2] 33.14/9.88 = [true()] 33.14/9.88 33.14/9.88 [eq(O(x), 0(y))] = [6] 33.14/9.88 >= [6] 33.14/9.88 = [eq(x, y)] 33.14/9.88 33.14/9.88 [eq(0(x), 1(y))] = [6] 33.14/9.88 > [0] 33.14/9.88 = [false()] 33.14/9.88 33.14/9.88 [eq(1(x), 0(y))] = [6] 33.14/9.88 > [0] 33.14/9.88 = [false()] 33.14/9.88 33.14/9.88 [eq(1(x), 1(y))] = [6] 33.14/9.88 >= [6] 33.14/9.88 = [eq(x, y)] 33.14/9.88 33.14/9.88 [negate(0(x))] = [1] 33.14/9.88 > [0] 33.14/9.88 = [1(x)] 33.14/9.88 33.14/9.88 [negate(1(x))] = [1] 33.14/9.88 > [0] 33.14/9.88 = [0(x)] 33.14/9.88 33.14/9.88 [choice(cons(x, xs))] = [1] x + [1] xs + [0] 33.14/9.88 >= [1] x + [0] 33.14/9.88 = [x] 33.14/9.88 33.14/9.88 [choice(cons(x, xs))] = [1] x + [1] xs + [0] 33.14/9.89 >= [1] xs + [0] 33.14/9.89 = [choice(xs)] 33.14/9.89 33.14/9.89 [guess(nil())] = [7] 33.14/9.89 >= [7] 33.14/9.89 = [nil()] 33.14/9.89 33.14/9.89 [guess(cons(clause, cnf))] = [1] clause + [1] cnf + [0] 33.14/9.89 >= [1] clause + [1] cnf + [0] 33.14/9.89 = [cons(choice(clause), guess(cnf))] 33.14/9.89 33.14/9.89 [verify(nil())] = [0] 33.14/9.89 ? [2] 33.14/9.89 = [true()] 33.14/9.89 33.14/9.89 [verify(cons(l, ls))] = [0] 33.14/9.89 ? [1] 33.14/9.89 = [if(member(negate(l), ls), false(), verify(ls))] 33.14/9.89 33.14/9.89 [sat(cnf)] = [1] cnf + [7] 33.14/9.89 > [1] cnf + [3] 33.14/9.89 = [satck(cnf, guess(cnf))] 33.14/9.89 33.14/9.89 [satck(cnf, assign)] = [1] assign + [3] 33.14/9.89 > [1] assign + [0] 33.14/9.89 = [if(verify(assign), assign, unsat())] 33.14/9.89 33.14/9.89 33.14/9.89 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 33.14/9.89 33.14/9.89 We are left with following problem, upon which TcT provides the 33.14/9.89 certificate YES(O(1),O(n^2)). 33.14/9.89 33.14/9.89 Strict Trs: 33.14/9.89 { member(x, cons(y, ys)) -> if(eq(x, y), true(), member(x, ys)) 33.14/9.89 , eq(O(x), 0(y)) -> eq(x, y) 33.14/9.89 , eq(1(x), 1(y)) -> eq(x, y) 33.14/9.89 , guess(cons(clause, cnf)) -> cons(choice(clause), guess(cnf)) 33.14/9.89 , verify(nil()) -> true() 33.14/9.89 , verify(cons(l, ls)) -> 33.14/9.89 if(member(negate(l), ls), false(), verify(ls)) } 33.14/9.89 Weak Trs: 33.14/9.89 { if(true(), t, e) -> t 33.14/9.89 , if(false(), t, e) -> e 33.14/9.89 , member(x, nil()) -> false() 33.14/9.89 , eq(nil(), nil()) -> true() 33.14/9.89 , eq(0(x), 1(y)) -> false() 33.14/9.89 , eq(1(x), 0(y)) -> false() 33.14/9.89 , negate(0(x)) -> 1(x) 33.14/9.89 , negate(1(x)) -> 0(x) 33.14/9.89 , choice(cons(x, xs)) -> x 33.14/9.89 , choice(cons(x, xs)) -> choice(xs) 33.14/9.89 , guess(nil()) -> nil() 33.14/9.89 , sat(cnf) -> satck(cnf, guess(cnf)) 33.14/9.89 , satck(cnf, assign) -> if(verify(assign), assign, unsat()) } 33.14/9.89 Obligation: 33.14/9.89 innermost runtime complexity 33.14/9.89 Answer: 33.14/9.89 YES(O(1),O(n^2)) 33.14/9.89 33.14/9.89 The weightgap principle applies (using the following nonconstant 33.14/9.89 growth matrix-interpretation) 33.14/9.89 33.14/9.89 The following argument positions are usable: 33.14/9.89 Uargs(if) = {1, 3}, Uargs(member) = {1}, Uargs(cons) = {1, 2}, 33.14/9.89 Uargs(satck) = {2} 33.14/9.89 33.14/9.89 TcT has computed the following matrix interpretation satisfying 33.14/9.89 not(EDA) and not(IDA(1)). 33.14/9.89 33.14/9.89 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 33.14/9.89 33.14/9.89 [true] = [0] 33.14/9.89 33.14/9.89 [false] = [0] 33.14/9.89 33.14/9.89 [member](x1, x2) = [1] x1 + [0] 33.14/9.89 33.14/9.89 [nil] = [7] 33.14/9.89 33.14/9.89 [cons](x1, x2) = [1] x1 + [1] x2 + [0] 33.14/9.89 33.14/9.89 [eq](x1, x2) = [0] 33.14/9.89 33.14/9.89 [O](x1) = [1] x1 + [7] 33.14/9.89 33.14/9.89 [0](x1) = [4] 33.14/9.89 33.14/9.89 [1](x1) = [4] 33.14/9.89 33.14/9.89 [negate](x1) = [4] 33.14/9.89 33.14/9.89 [choice](x1) = [1] x1 + [0] 33.14/9.89 33.14/9.89 [guess](x1) = [1] x1 + [0] 33.14/9.89 33.14/9.89 [verify](x1) = [4] 33.14/9.89 33.14/9.89 [sat](x1) = [1] x1 + [7] 33.14/9.89 33.14/9.89 [satck](x1, x2) = [1] x2 + [7] 33.14/9.89 33.14/9.89 [unsat] = [0] 33.14/9.89 33.14/9.89 The order satisfies the following ordering constraints: 33.14/9.89 33.14/9.89 [if(true(), t, e)] = [1] t + [1] e + [0] 33.14/9.89 >= [1] t + [0] 33.14/9.89 = [t] 33.14/9.89 33.14/9.89 [if(false(), t, e)] = [1] t + [1] e + [0] 33.14/9.89 >= [1] e + [0] 33.14/9.89 = [e] 33.14/9.89 33.14/9.89 [member(x, nil())] = [1] x + [0] 33.14/9.89 >= [0] 33.14/9.89 = [false()] 33.14/9.89 33.14/9.89 [member(x, cons(y, ys))] = [1] x + [0] 33.14/9.89 >= [1] x + [0] 33.14/9.89 = [if(eq(x, y), true(), member(x, ys))] 33.14/9.89 33.14/9.89 [eq(nil(), nil())] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [true()] 33.14/9.89 33.14/9.89 [eq(O(x), 0(y))] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [eq(x, y)] 33.14/9.89 33.14/9.89 [eq(0(x), 1(y))] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [false()] 33.14/9.89 33.14/9.89 [eq(1(x), 0(y))] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [false()] 33.14/9.89 33.14/9.89 [eq(1(x), 1(y))] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [eq(x, y)] 33.14/9.89 33.14/9.89 [negate(0(x))] = [4] 33.14/9.89 >= [4] 33.14/9.89 = [1(x)] 33.14/9.89 33.14/9.89 [negate(1(x))] = [4] 33.14/9.89 >= [4] 33.14/9.89 = [0(x)] 33.14/9.89 33.14/9.89 [choice(cons(x, xs))] = [1] x + [1] xs + [0] 33.14/9.89 >= [1] x + [0] 33.14/9.89 = [x] 33.14/9.89 33.14/9.89 [choice(cons(x, xs))] = [1] x + [1] xs + [0] 33.14/9.89 >= [1] xs + [0] 33.14/9.89 = [choice(xs)] 33.14/9.89 33.14/9.89 [guess(nil())] = [7] 33.14/9.89 >= [7] 33.14/9.89 = [nil()] 33.14/9.89 33.14/9.89 [guess(cons(clause, cnf))] = [1] clause + [1] cnf + [0] 33.14/9.89 >= [1] clause + [1] cnf + [0] 33.14/9.89 = [cons(choice(clause), guess(cnf))] 33.14/9.89 33.14/9.89 [verify(nil())] = [4] 33.14/9.89 > [0] 33.14/9.89 = [true()] 33.14/9.89 33.14/9.89 [verify(cons(l, ls))] = [4] 33.14/9.89 ? [8] 33.14/9.89 = [if(member(negate(l), ls), false(), verify(ls))] 33.14/9.89 33.14/9.89 [sat(cnf)] = [1] cnf + [7] 33.14/9.89 >= [1] cnf + [7] 33.14/9.89 = [satck(cnf, guess(cnf))] 33.14/9.89 33.14/9.89 [satck(cnf, assign)] = [1] assign + [7] 33.14/9.89 > [1] assign + [4] 33.14/9.89 = [if(verify(assign), assign, unsat())] 33.14/9.89 33.14/9.89 33.14/9.89 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 33.14/9.89 33.14/9.89 We are left with following problem, upon which TcT provides the 33.14/9.89 certificate YES(O(1),O(n^2)). 33.14/9.89 33.14/9.89 Strict Trs: 33.14/9.89 { member(x, cons(y, ys)) -> if(eq(x, y), true(), member(x, ys)) 33.14/9.89 , eq(O(x), 0(y)) -> eq(x, y) 33.14/9.89 , eq(1(x), 1(y)) -> eq(x, y) 33.14/9.89 , guess(cons(clause, cnf)) -> cons(choice(clause), guess(cnf)) 33.14/9.89 , verify(cons(l, ls)) -> 33.14/9.89 if(member(negate(l), ls), false(), verify(ls)) } 33.14/9.89 Weak Trs: 33.14/9.89 { if(true(), t, e) -> t 33.14/9.89 , if(false(), t, e) -> e 33.14/9.89 , member(x, nil()) -> false() 33.14/9.89 , eq(nil(), nil()) -> true() 33.14/9.89 , eq(0(x), 1(y)) -> false() 33.14/9.89 , eq(1(x), 0(y)) -> false() 33.14/9.89 , negate(0(x)) -> 1(x) 33.14/9.89 , negate(1(x)) -> 0(x) 33.14/9.89 , choice(cons(x, xs)) -> x 33.14/9.89 , choice(cons(x, xs)) -> choice(xs) 33.14/9.89 , guess(nil()) -> nil() 33.14/9.89 , verify(nil()) -> true() 33.14/9.89 , sat(cnf) -> satck(cnf, guess(cnf)) 33.14/9.89 , satck(cnf, assign) -> if(verify(assign), assign, unsat()) } 33.14/9.89 Obligation: 33.14/9.89 innermost runtime complexity 33.14/9.89 Answer: 33.14/9.89 YES(O(1),O(n^2)) 33.14/9.89 33.14/9.89 We use the processor 'matrix interpretation of dimension 1' to 33.14/9.89 orient following rules strictly. 33.14/9.89 33.14/9.89 Trs: 33.14/9.89 { guess(cons(clause, cnf)) -> cons(choice(clause), guess(cnf)) } 33.14/9.89 33.14/9.89 The induced complexity on above rules (modulo remaining rules) is 33.14/9.89 YES(?,O(n^1)) . These rules are moved into the corresponding weak 33.14/9.89 component(s). 33.14/9.89 33.14/9.89 Sub-proof: 33.14/9.89 ---------- 33.14/9.89 The following argument positions are usable: 33.14/9.89 Uargs(if) = {1, 3}, Uargs(member) = {1}, Uargs(cons) = {1, 2}, 33.14/9.89 Uargs(satck) = {2} 33.14/9.89 33.14/9.89 TcT has computed the following constructor-based matrix 33.14/9.89 interpretation satisfying not(EDA). 33.14/9.89 33.14/9.89 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 33.14/9.89 33.14/9.89 [true] = [0] 33.14/9.89 33.14/9.89 [false] = [0] 33.14/9.89 33.14/9.89 [member](x1, x2) = [1] x1 + [0] 33.14/9.89 33.14/9.89 [nil] = [0] 33.14/9.89 33.14/9.89 [cons](x1, x2) = [1] x1 + [1] x2 + [2] 33.14/9.89 33.14/9.89 [eq](x1, x2) = [0] 33.14/9.89 33.14/9.89 [O](x1) = [1] x1 + [7] 33.14/9.89 33.14/9.89 [0](x1) = [0] 33.14/9.89 33.14/9.89 [1](x1) = [0] 33.14/9.89 33.14/9.89 [negate](x1) = [0] 33.14/9.89 33.14/9.89 [choice](x1) = [2] x1 + [0] 33.14/9.89 33.14/9.89 [guess](x1) = [4] x1 + [7] 33.14/9.89 33.14/9.89 [verify](x1) = [0] 33.14/9.89 33.14/9.89 [sat](x1) = [7] x1 + [7] 33.14/9.89 33.14/9.89 [satck](x1, x2) = [3] x1 + [1] x2 + [0] 33.14/9.89 33.14/9.89 [unsat] = [0] 33.14/9.89 33.14/9.89 The order satisfies the following ordering constraints: 33.14/9.89 33.14/9.89 [if(true(), t, e)] = [1] t + [1] e + [0] 33.14/9.89 >= [1] t + [0] 33.14/9.89 = [t] 33.14/9.89 33.14/9.89 [if(false(), t, e)] = [1] t + [1] e + [0] 33.14/9.89 >= [1] e + [0] 33.14/9.89 = [e] 33.14/9.89 33.14/9.89 [member(x, nil())] = [1] x + [0] 33.14/9.89 >= [0] 33.14/9.89 = [false()] 33.14/9.89 33.14/9.89 [member(x, cons(y, ys))] = [1] x + [0] 33.14/9.89 >= [1] x + [0] 33.14/9.89 = [if(eq(x, y), true(), member(x, ys))] 33.14/9.89 33.14/9.89 [eq(nil(), nil())] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [true()] 33.14/9.89 33.14/9.89 [eq(O(x), 0(y))] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [eq(x, y)] 33.14/9.89 33.14/9.89 [eq(0(x), 1(y))] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [false()] 33.14/9.89 33.14/9.89 [eq(1(x), 0(y))] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [false()] 33.14/9.89 33.14/9.89 [eq(1(x), 1(y))] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [eq(x, y)] 33.14/9.89 33.14/9.89 [negate(0(x))] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [1(x)] 33.14/9.89 33.14/9.89 [negate(1(x))] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [0(x)] 33.14/9.89 33.14/9.89 [choice(cons(x, xs))] = [2] x + [2] xs + [4] 33.14/9.89 > [1] x + [0] 33.14/9.89 = [x] 33.14/9.89 33.14/9.89 [choice(cons(x, xs))] = [2] x + [2] xs + [4] 33.14/9.89 > [2] xs + [0] 33.14/9.89 = [choice(xs)] 33.14/9.89 33.14/9.89 [guess(nil())] = [7] 33.14/9.89 > [0] 33.14/9.89 = [nil()] 33.14/9.89 33.14/9.89 [guess(cons(clause, cnf))] = [4] clause + [4] cnf + [15] 33.14/9.89 > [2] clause + [4] cnf + [9] 33.14/9.89 = [cons(choice(clause), guess(cnf))] 33.14/9.89 33.14/9.89 [verify(nil())] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [true()] 33.14/9.89 33.14/9.89 [verify(cons(l, ls))] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [if(member(negate(l), ls), false(), verify(ls))] 33.14/9.89 33.14/9.89 [sat(cnf)] = [7] cnf + [7] 33.14/9.89 >= [7] cnf + [7] 33.14/9.89 = [satck(cnf, guess(cnf))] 33.14/9.89 33.14/9.89 [satck(cnf, assign)] = [3] cnf + [1] assign + [0] 33.14/9.89 >= [1] assign + [0] 33.14/9.89 = [if(verify(assign), assign, unsat())] 33.14/9.89 33.14/9.89 33.14/9.89 We return to the main proof. 33.14/9.89 33.14/9.89 We are left with following problem, upon which TcT provides the 33.14/9.89 certificate YES(O(1),O(n^2)). 33.14/9.89 33.14/9.89 Strict Trs: 33.14/9.89 { member(x, cons(y, ys)) -> if(eq(x, y), true(), member(x, ys)) 33.14/9.89 , eq(O(x), 0(y)) -> eq(x, y) 33.14/9.89 , eq(1(x), 1(y)) -> eq(x, y) 33.14/9.89 , verify(cons(l, ls)) -> 33.14/9.89 if(member(negate(l), ls), false(), verify(ls)) } 33.14/9.89 Weak Trs: 33.14/9.89 { if(true(), t, e) -> t 33.14/9.89 , if(false(), t, e) -> e 33.14/9.89 , member(x, nil()) -> false() 33.14/9.89 , eq(nil(), nil()) -> true() 33.14/9.89 , eq(0(x), 1(y)) -> false() 33.14/9.89 , eq(1(x), 0(y)) -> false() 33.14/9.89 , negate(0(x)) -> 1(x) 33.14/9.89 , negate(1(x)) -> 0(x) 33.14/9.89 , choice(cons(x, xs)) -> x 33.14/9.89 , choice(cons(x, xs)) -> choice(xs) 33.14/9.89 , guess(nil()) -> nil() 33.14/9.89 , guess(cons(clause, cnf)) -> cons(choice(clause), guess(cnf)) 33.14/9.89 , verify(nil()) -> true() 33.14/9.89 , sat(cnf) -> satck(cnf, guess(cnf)) 33.14/9.89 , satck(cnf, assign) -> if(verify(assign), assign, unsat()) } 33.14/9.89 Obligation: 33.14/9.89 innermost runtime complexity 33.14/9.89 Answer: 33.14/9.89 YES(O(1),O(n^2)) 33.14/9.89 33.14/9.89 We use the processor 'matrix interpretation of dimension 1' to 33.14/9.89 orient following rules strictly. 33.14/9.89 33.14/9.89 Trs: 33.14/9.89 { verify(cons(l, ls)) -> 33.14/9.89 if(member(negate(l), ls), false(), verify(ls)) } 33.14/9.89 33.14/9.89 The induced complexity on above rules (modulo remaining rules) is 33.14/9.89 YES(?,O(n^1)) . These rules are moved into the corresponding weak 33.14/9.89 component(s). 33.14/9.89 33.14/9.89 Sub-proof: 33.14/9.89 ---------- 33.14/9.89 The following argument positions are usable: 33.14/9.89 Uargs(if) = {1, 3}, Uargs(member) = {1}, Uargs(cons) = {1, 2}, 33.14/9.89 Uargs(satck) = {2} 33.14/9.89 33.14/9.89 TcT has computed the following constructor-based matrix 33.14/9.89 interpretation satisfying not(EDA). 33.14/9.89 33.14/9.89 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 33.14/9.89 33.14/9.89 [true] = [0] 33.14/9.89 33.14/9.89 [false] = [0] 33.14/9.89 33.14/9.89 [member](x1, x2) = [1] x1 + [0] 33.14/9.89 33.14/9.89 [nil] = [0] 33.14/9.89 33.14/9.89 [cons](x1, x2) = [1] x1 + [1] x2 + [2] 33.14/9.89 33.14/9.89 [eq](x1, x2) = [0] 33.14/9.89 33.14/9.89 [O](x1) = [1] x1 + [7] 33.14/9.89 33.14/9.89 [0](x1) = [0] 33.14/9.89 33.14/9.89 [1](x1) = [0] 33.14/9.89 33.14/9.89 [negate](x1) = [0] 33.14/9.89 33.14/9.89 [choice](x1) = [2] x1 + [0] 33.14/9.89 33.14/9.89 [guess](x1) = [2] x1 + [0] 33.14/9.89 33.14/9.89 [verify](x1) = [1] x1 + [0] 33.14/9.89 33.14/9.89 [sat](x1) = [7] x1 + [7] 33.14/9.89 33.14/9.89 [satck](x1, x2) = [3] x1 + [2] x2 + [5] 33.14/9.89 33.14/9.89 [unsat] = [0] 33.14/9.89 33.14/9.89 The order satisfies the following ordering constraints: 33.14/9.89 33.14/9.89 [if(true(), t, e)] = [1] t + [1] e + [0] 33.14/9.89 >= [1] t + [0] 33.14/9.89 = [t] 33.14/9.89 33.14/9.89 [if(false(), t, e)] = [1] t + [1] e + [0] 33.14/9.89 >= [1] e + [0] 33.14/9.89 = [e] 33.14/9.89 33.14/9.89 [member(x, nil())] = [1] x + [0] 33.14/9.89 >= [0] 33.14/9.89 = [false()] 33.14/9.89 33.14/9.89 [member(x, cons(y, ys))] = [1] x + [0] 33.14/9.89 >= [1] x + [0] 33.14/9.89 = [if(eq(x, y), true(), member(x, ys))] 33.14/9.89 33.14/9.89 [eq(nil(), nil())] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [true()] 33.14/9.89 33.14/9.89 [eq(O(x), 0(y))] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [eq(x, y)] 33.14/9.89 33.14/9.89 [eq(0(x), 1(y))] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [false()] 33.14/9.89 33.14/9.89 [eq(1(x), 0(y))] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [false()] 33.14/9.89 33.14/9.89 [eq(1(x), 1(y))] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [eq(x, y)] 33.14/9.89 33.14/9.89 [negate(0(x))] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [1(x)] 33.14/9.89 33.14/9.89 [negate(1(x))] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [0(x)] 33.14/9.89 33.14/9.89 [choice(cons(x, xs))] = [2] x + [2] xs + [4] 33.14/9.89 > [1] x + [0] 33.14/9.89 = [x] 33.14/9.89 33.14/9.89 [choice(cons(x, xs))] = [2] x + [2] xs + [4] 33.14/9.89 > [2] xs + [0] 33.14/9.89 = [choice(xs)] 33.14/9.89 33.14/9.89 [guess(nil())] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [nil()] 33.14/9.89 33.14/9.89 [guess(cons(clause, cnf))] = [2] clause + [2] cnf + [4] 33.14/9.89 > [2] clause + [2] cnf + [2] 33.14/9.89 = [cons(choice(clause), guess(cnf))] 33.14/9.89 33.14/9.89 [verify(nil())] = [0] 33.14/9.89 >= [0] 33.14/9.89 = [true()] 33.14/9.89 33.14/9.89 [verify(cons(l, ls))] = [1] l + [1] ls + [2] 33.14/9.89 > [1] ls + [0] 33.14/9.89 = [if(member(negate(l), ls), false(), verify(ls))] 33.14/9.89 33.14/9.89 [sat(cnf)] = [7] cnf + [7] 33.14/9.89 > [7] cnf + [5] 33.14/9.89 = [satck(cnf, guess(cnf))] 33.14/9.89 33.14/9.89 [satck(cnf, assign)] = [3] cnf + [2] assign + [5] 33.14/9.89 > [2] assign + [0] 33.14/9.89 = [if(verify(assign), assign, unsat())] 33.14/9.89 33.14/9.89 33.14/9.89 We return to the main proof. 33.14/9.89 33.14/9.89 We are left with following problem, upon which TcT provides the 33.14/9.89 certificate YES(O(1),O(n^2)). 33.14/9.89 33.14/9.89 Strict Trs: 33.14/9.89 { member(x, cons(y, ys)) -> if(eq(x, y), true(), member(x, ys)) 33.14/9.89 , eq(O(x), 0(y)) -> eq(x, y) 33.14/9.89 , eq(1(x), 1(y)) -> eq(x, y) } 33.14/9.89 Weak Trs: 33.14/9.89 { if(true(), t, e) -> t 33.14/9.89 , if(false(), t, e) -> e 33.14/9.89 , member(x, nil()) -> false() 33.14/9.89 , eq(nil(), nil()) -> true() 33.14/9.89 , eq(0(x), 1(y)) -> false() 33.14/9.89 , eq(1(x), 0(y)) -> false() 33.14/9.89 , negate(0(x)) -> 1(x) 33.14/9.89 , negate(1(x)) -> 0(x) 33.14/9.89 , choice(cons(x, xs)) -> x 33.14/9.89 , choice(cons(x, xs)) -> choice(xs) 33.14/9.89 , guess(nil()) -> nil() 33.14/9.89 , guess(cons(clause, cnf)) -> cons(choice(clause), guess(cnf)) 33.14/9.89 , verify(nil()) -> true() 33.14/9.89 , verify(cons(l, ls)) -> 33.14/9.89 if(member(negate(l), ls), false(), verify(ls)) 33.14/9.89 , sat(cnf) -> satck(cnf, guess(cnf)) 33.14/9.89 , satck(cnf, assign) -> if(verify(assign), assign, unsat()) } 33.14/9.89 Obligation: 33.14/9.89 innermost runtime complexity 33.14/9.89 Answer: 33.14/9.89 YES(O(1),O(n^2)) 33.14/9.89 33.14/9.89 We use the processor 'matrix interpretation of dimension 2' to 33.14/9.89 orient following rules strictly. 33.14/9.89 33.14/9.89 Trs: 33.14/9.89 { eq(O(x), 0(y)) -> eq(x, y) 33.14/9.89 , eq(1(x), 1(y)) -> eq(x, y) } 33.14/9.89 33.14/9.89 The induced complexity on above rules (modulo remaining rules) is 33.14/9.89 YES(?,O(n^2)) . These rules are moved into the corresponding weak 33.14/9.89 component(s). 33.14/9.89 33.14/9.89 Sub-proof: 33.14/9.89 ---------- 33.14/9.89 The following argument positions are usable: 33.14/9.89 Uargs(if) = {1, 3}, Uargs(member) = {1}, Uargs(cons) = {1, 2}, 33.14/9.89 Uargs(satck) = {2} 33.14/9.89 33.14/9.89 TcT has computed the following constructor-based matrix 33.14/9.89 interpretation satisfying not(EDA). 33.14/9.89 33.14/9.89 [if](x1, x2, x3) = [1 0] x1 + [2 0] x2 + [1 0] x3 + [0] 33.14/9.89 [0 0] [0 1] [0 2] [0] 33.14/9.89 33.14/9.89 [true] = [0] 33.14/9.89 [0] 33.14/9.89 33.14/9.89 [false] = [0] 33.14/9.89 [0] 33.14/9.89 33.14/9.89 [member](x1, x2) = [1 0] x1 + [0 1] x2 + [0] 33.14/9.89 [0 0] [0 0] [0] 33.14/9.89 33.14/9.89 [nil] = [0] 33.14/9.89 [0] 33.14/9.89 33.14/9.89 [cons](x1, x2) = [1 2] x1 + [1 2] x2 + [0] 33.14/9.89 [0 1] [0 1] [0] 33.14/9.89 33.14/9.89 [eq](x1, x2) = [0 0] x1 + [0 1] x2 + [0] 33.14/9.89 [1 1] [4 0] [0] 33.14/9.89 33.14/9.89 [O](x1) = [1 3] x1 + [0] 33.14/9.89 [0 1] [0] 33.14/9.89 33.14/9.89 [0](x1) = [1 1] x1 + [0] 33.14/9.89 [0 1] [4] 33.14/9.89 33.14/9.89 [1](x1) = [1 1] x1 + [0] 33.14/9.89 [0 1] [4] 33.14/9.89 33.14/9.89 [negate](x1) = [2 2] x1 + [0] 33.14/9.89 [2 0] [4] 33.14/9.89 33.14/9.89 [choice](x1) = [1 0] x1 + [0] 33.14/9.89 [0 1] [0] 33.14/9.89 33.14/9.89 [guess](x1) = [1 0] x1 + [0] 33.14/9.89 [0 1] [0] 33.14/9.89 33.14/9.89 [verify](x1) = [4 0] x1 + [0] 33.14/9.89 [0 0] [0] 33.14/9.89 33.14/9.89 [sat](x1) = [7 7] x1 + [7] 33.14/9.89 [7 7] [7] 33.14/9.89 33.14/9.89 [satck](x1, x2) = [1 7] x1 + [6 0] x2 + [7] 33.14/9.89 [7 3] [0 1] [7] 33.14/9.89 33.14/9.89 [unsat] = [0] 33.14/9.89 [0] 33.14/9.89 33.14/9.89 The order satisfies the following ordering constraints: 33.14/9.89 33.14/9.89 [if(true(), t, e)] = [2 0] t + [1 0] e + [0] 33.14/9.89 [0 1] [0 2] [0] 33.14/9.89 >= [1 0] t + [0] 33.14/9.89 [0 1] [0] 33.14/9.89 = [t] 33.14/9.89 33.14/9.89 [if(false(), t, e)] = [2 0] t + [1 0] e + [0] 33.14/9.89 [0 1] [0 2] [0] 33.14/9.89 >= [1 0] e + [0] 33.14/9.89 [0 1] [0] 33.14/9.89 = [e] 33.14/9.89 33.14/9.89 [member(x, nil())] = [1 0] x + [0] 33.14/9.89 [0 0] [0] 33.14/9.89 >= [0] 33.14/9.89 [0] 33.14/9.89 = [false()] 33.14/9.89 33.14/9.89 [member(x, cons(y, ys))] = [1 0] x + [0 1] y + [0 1] ys + [0] 33.14/9.89 [0 0] [0 0] [0 0] [0] 33.14/9.89 >= [1 0] x + [0 1] y + [0 1] ys + [0] 33.14/9.89 [0 0] [0 0] [0 0] [0] 33.14/9.89 = [if(eq(x, y), true(), member(x, ys))] 33.14/9.89 33.14/9.89 [eq(nil(), nil())] = [0] 33.14/9.89 [0] 33.14/9.89 >= [0] 33.14/9.89 [0] 33.14/9.89 = [true()] 33.14/9.89 33.14/9.89 [eq(O(x), 0(y))] = [0 0] x + [0 1] y + [4] 33.14/9.89 [1 4] [4 4] [0] 33.14/9.89 > [0 0] x + [0 1] y + [0] 33.14/9.89 [1 1] [4 0] [0] 33.14/9.89 = [eq(x, y)] 33.14/9.89 33.14/9.89 [eq(0(x), 1(y))] = [0 0] x + [0 1] y + [4] 33.14/9.89 [1 2] [4 4] [4] 33.14/9.89 > [0] 33.14/9.89 [0] 33.14/9.89 = [false()] 33.14/9.89 33.14/9.89 [eq(1(x), 0(y))] = [0 0] x + [0 1] y + [4] 33.14/9.89 [1 2] [4 4] [4] 33.14/9.89 > [0] 33.14/9.89 [0] 33.14/9.89 = [false()] 33.14/9.89 33.14/9.89 [eq(1(x), 1(y))] = [0 0] x + [0 1] y + [4] 33.14/9.89 [1 2] [4 4] [4] 33.14/9.89 > [0 0] x + [0 1] y + [0] 33.14/9.89 [1 1] [4 0] [0] 33.14/9.89 = [eq(x, y)] 33.14/9.89 33.14/9.89 [negate(0(x))] = [2 4] x + [8] 33.14/9.89 [2 2] [4] 33.14/9.89 > [1 1] x + [0] 33.14/9.89 [0 1] [4] 33.14/9.89 = [1(x)] 33.14/9.89 33.14/9.89 [negate(1(x))] = [2 4] x + [8] 33.14/9.89 [2 2] [4] 33.14/9.89 > [1 1] x + [0] 33.14/9.89 [0 1] [4] 33.14/9.89 = [0(x)] 33.14/9.89 33.14/9.89 [choice(cons(x, xs))] = [1 2] x + [1 2] xs + [0] 33.14/9.89 [0 1] [0 1] [0] 33.14/9.89 >= [1 0] x + [0] 33.14/9.89 [0 1] [0] 33.14/9.89 = [x] 33.14/9.89 33.14/9.89 [choice(cons(x, xs))] = [1 2] x + [1 2] xs + [0] 33.14/9.89 [0 1] [0 1] [0] 33.14/9.89 >= [1 0] xs + [0] 33.14/9.89 [0 1] [0] 33.14/9.89 = [choice(xs)] 33.14/9.89 33.14/9.89 [guess(nil())] = [0] 33.14/9.89 [0] 33.14/9.89 >= [0] 33.14/9.89 [0] 33.14/9.89 = [nil()] 33.14/9.89 33.14/9.89 [guess(cons(clause, cnf))] = [1 2] clause + [1 2] cnf + [0] 33.14/9.89 [0 1] [0 1] [0] 33.14/9.89 >= [1 2] clause + [1 2] cnf + [0] 33.14/9.89 [0 1] [0 1] [0] 33.14/9.89 = [cons(choice(clause), guess(cnf))] 33.14/9.89 33.14/9.89 [verify(nil())] = [0] 33.14/9.89 [0] 33.14/9.89 >= [0] 33.14/9.89 [0] 33.14/9.89 = [true()] 33.14/9.89 33.14/9.89 [verify(cons(l, ls))] = [4 8] l + [4 8] ls + [0] 33.14/9.89 [0 0] [0 0] [0] 33.14/9.89 >= [2 2] l + [4 1] ls + [0] 33.14/9.89 [0 0] [0 0] [0] 33.14/9.89 = [if(member(negate(l), ls), false(), verify(ls))] 33.14/9.89 33.14/9.89 [sat(cnf)] = [7 7] cnf + [7] 33.14/9.89 [7 7] [7] 33.14/9.89 >= [7 7] cnf + [7] 33.14/9.89 [7 4] [7] 33.14/9.89 = [satck(cnf, guess(cnf))] 33.14/9.89 33.14/9.89 [satck(cnf, assign)] = [1 7] cnf + [6 0] assign + [7] 33.14/9.89 [7 3] [0 1] [7] 33.14/9.89 > [6 0] assign + [0] 33.14/9.89 [0 1] [0] 33.14/9.89 = [if(verify(assign), assign, unsat())] 33.14/9.89 33.14/9.89 33.14/9.89 We return to the main proof. 33.14/9.89 33.14/9.89 We are left with following problem, upon which TcT provides the 33.14/9.89 certificate YES(O(1),O(n^2)). 33.14/9.89 33.14/9.89 Strict Trs: 33.14/9.89 { member(x, cons(y, ys)) -> if(eq(x, y), true(), member(x, ys)) } 33.14/9.89 Weak Trs: 33.14/9.89 { if(true(), t, e) -> t 33.14/9.89 , if(false(), t, e) -> e 33.14/9.89 , member(x, nil()) -> false() 33.14/9.89 , eq(nil(), nil()) -> true() 33.14/9.89 , eq(O(x), 0(y)) -> eq(x, y) 33.14/9.89 , eq(0(x), 1(y)) -> false() 33.14/9.89 , eq(1(x), 0(y)) -> false() 33.14/9.89 , eq(1(x), 1(y)) -> eq(x, y) 33.14/9.89 , negate(0(x)) -> 1(x) 33.14/9.89 , negate(1(x)) -> 0(x) 33.14/9.89 , choice(cons(x, xs)) -> x 33.14/9.89 , choice(cons(x, xs)) -> choice(xs) 33.14/9.89 , guess(nil()) -> nil() 33.14/9.89 , guess(cons(clause, cnf)) -> cons(choice(clause), guess(cnf)) 33.14/9.89 , verify(nil()) -> true() 33.14/9.89 , verify(cons(l, ls)) -> 33.14/9.89 if(member(negate(l), ls), false(), verify(ls)) 33.14/9.89 , sat(cnf) -> satck(cnf, guess(cnf)) 33.14/9.89 , satck(cnf, assign) -> if(verify(assign), assign, unsat()) } 33.14/9.89 Obligation: 33.14/9.89 innermost runtime complexity 33.14/9.89 Answer: 33.14/9.89 YES(O(1),O(n^2)) 33.14/9.89 33.14/9.89 We use the processor 'matrix interpretation of dimension 2' to 33.14/9.89 orient following rules strictly. 33.14/9.89 33.14/9.89 Trs: 33.14/9.89 { member(x, cons(y, ys)) -> if(eq(x, y), true(), member(x, ys)) } 33.14/9.89 33.14/9.89 The induced complexity on above rules (modulo remaining rules) is 33.14/9.89 YES(?,O(n^2)) . These rules are moved into the corresponding weak 33.14/9.89 component(s). 33.14/9.89 33.14/9.89 Sub-proof: 33.14/9.89 ---------- 33.14/9.89 The following argument positions are usable: 33.14/9.89 Uargs(if) = {1, 3}, Uargs(member) = {1}, Uargs(cons) = {1, 2}, 33.14/9.89 Uargs(satck) = {2} 33.14/9.89 33.14/9.89 TcT has computed the following constructor-based matrix 33.14/9.89 interpretation satisfying not(EDA). 33.14/9.89 33.14/9.89 [if](x1, x2, x3) = [2 0] x1 + [1 0] x2 + [1 0] x3 + [0] 33.14/9.89 [0 0] [0 1] [0 4] [0] 33.14/9.89 33.14/9.89 [true] = [0] 33.14/9.89 [0] 33.14/9.89 33.14/9.89 [false] = [0] 33.14/9.89 [0] 33.14/9.89 33.14/9.89 [member](x1, x2) = [1 0] x1 + [0 4] x2 + [0] 33.14/9.89 [0 0] [0 0] [0] 33.14/9.89 33.14/9.89 [nil] = [0] 33.14/9.89 [0] 33.14/9.89 33.14/9.89 [cons](x1, x2) = [1 0] x1 + [1 4] x2 + [0] 33.14/9.89 [0 1] [0 1] [1] 33.14/9.89 33.14/9.89 [eq](x1, x2) = [0 0] x1 + [0] 33.14/9.89 [4 0] [0] 33.14/9.89 33.14/9.89 [O](x1) = [1 2] x1 + [0] 33.14/9.89 [0 1] [0] 33.14/9.89 33.14/9.89 [0](x1) = [1 0] x1 + [2] 33.14/9.89 [0 0] [0] 33.14/9.89 33.14/9.89 [1](x1) = [1 0] x1 + [2] 33.14/9.89 [0 0] [0] 33.14/9.89 33.14/9.89 [negate](x1) = [1 0] x1 + [0] 33.14/9.89 [0 0] [4] 33.14/9.89 33.14/9.89 [choice](x1) = [1 0] x1 + [0] 33.14/9.89 [0 1] [0] 33.14/9.89 33.14/9.89 [guess](x1) = [1 0] x1 + [0] 33.14/9.89 [0 1] [0] 33.14/9.89 33.14/9.89 [verify](x1) = [3 0] x1 + [0] 33.14/9.89 [0 0] [0] 33.14/9.89 33.14/9.89 [sat](x1) = [7 7] x1 + [7] 33.14/9.89 [7 7] [7] 33.14/9.89 33.14/9.89 [satck](x1, x2) = [0 3] x1 + [7 4] x2 + [7] 33.14/9.89 [7 3] [0 1] [7] 33.14/9.89 33.14/9.89 [unsat] = [0] 33.14/9.89 [0] 33.14/9.89 33.14/9.89 The order satisfies the following ordering constraints: 33.14/9.89 33.14/9.89 [if(true(), t, e)] = [1 0] t + [1 0] e + [0] 33.14/9.89 [0 1] [0 4] [0] 33.14/9.89 >= [1 0] t + [0] 33.14/9.89 [0 1] [0] 33.14/9.89 = [t] 33.14/9.89 33.14/9.89 [if(false(), t, e)] = [1 0] t + [1 0] e + [0] 33.14/9.89 [0 1] [0 4] [0] 33.14/9.89 >= [1 0] e + [0] 33.14/9.89 [0 1] [0] 33.14/9.89 = [e] 33.14/9.89 33.14/9.89 [member(x, nil())] = [1 0] x + [0] 33.14/9.89 [0 0] [0] 33.14/9.89 >= [0] 33.14/9.89 [0] 33.14/9.89 = [false()] 33.14/9.89 33.14/9.89 [member(x, cons(y, ys))] = [1 0] x + [0 4] y + [0 4] ys + [4] 33.14/9.89 [0 0] [0 0] [0 0] [0] 33.14/9.89 > [1 0] x + [0 4] ys + [0] 33.14/9.89 [0 0] [0 0] [0] 33.14/9.89 = [if(eq(x, y), true(), member(x, ys))] 33.14/9.89 33.14/9.89 [eq(nil(), nil())] = [0] 33.14/9.89 [0] 33.14/9.89 >= [0] 33.14/9.89 [0] 33.14/9.89 = [true()] 33.14/9.89 33.14/9.89 [eq(O(x), 0(y))] = [0 0] x + [0] 33.14/9.89 [4 8] [0] 33.14/9.89 >= [0 0] x + [0] 33.14/9.89 [4 0] [0] 33.14/9.89 = [eq(x, y)] 33.14/9.89 33.14/9.89 [eq(0(x), 1(y))] = [0 0] x + [0] 33.14/9.89 [4 0] [8] 33.14/9.89 >= [0] 33.14/9.89 [0] 33.14/9.89 = [false()] 33.14/9.89 33.14/9.89 [eq(1(x), 0(y))] = [0 0] x + [0] 33.14/9.89 [4 0] [8] 33.14/9.89 >= [0] 33.14/9.89 [0] 33.14/9.89 = [false()] 33.14/9.89 33.14/9.89 [eq(1(x), 1(y))] = [0 0] x + [0] 33.14/9.89 [4 0] [8] 33.14/9.89 >= [0 0] x + [0] 33.14/9.89 [4 0] [0] 33.14/9.89 = [eq(x, y)] 33.14/9.89 33.14/9.89 [negate(0(x))] = [1 0] x + [2] 33.14/9.89 [0 0] [4] 33.14/9.89 >= [1 0] x + [2] 33.14/9.89 [0 0] [0] 33.14/9.89 = [1(x)] 33.14/9.89 33.14/9.89 [negate(1(x))] = [1 0] x + [2] 33.14/9.89 [0 0] [4] 33.14/9.89 >= [1 0] x + [2] 33.14/9.89 [0 0] [0] 33.14/9.89 = [0(x)] 33.14/9.89 33.14/9.89 [choice(cons(x, xs))] = [1 0] x + [1 4] xs + [0] 33.14/9.89 [0 1] [0 1] [1] 33.14/9.89 >= [1 0] x + [0] 33.14/9.89 [0 1] [0] 33.14/9.89 = [x] 33.14/9.89 33.14/9.89 [choice(cons(x, xs))] = [1 0] x + [1 4] xs + [0] 33.14/9.89 [0 1] [0 1] [1] 33.14/9.89 >= [1 0] xs + [0] 33.14/9.89 [0 1] [0] 33.14/9.89 = [choice(xs)] 33.14/9.89 33.14/9.89 [guess(nil())] = [0] 33.14/9.89 [0] 33.14/9.89 >= [0] 33.14/9.89 [0] 33.14/9.89 = [nil()] 33.14/9.89 33.14/9.89 [guess(cons(clause, cnf))] = [1 0] clause + [1 4] cnf + [0] 33.14/9.89 [0 1] [0 1] [1] 33.14/9.90 >= [1 0] clause + [1 4] cnf + [0] 33.14/9.90 [0 1] [0 1] [1] 33.14/9.90 = [cons(choice(clause), guess(cnf))] 33.14/9.90 33.14/9.90 [verify(nil())] = [0] 33.14/9.90 [0] 33.14/9.90 >= [0] 33.14/9.90 [0] 33.14/9.90 = [true()] 33.14/9.90 33.14/9.90 [verify(cons(l, ls))] = [3 0] l + [3 12] ls + [0] 33.14/9.90 [0 0] [0 0] [0] 33.14/9.90 >= [2 0] l + [3 8] ls + [0] 33.14/9.90 [0 0] [0 0] [0] 33.14/9.90 = [if(member(negate(l), ls), false(), verify(ls))] 33.14/9.90 33.14/9.90 [sat(cnf)] = [7 7] cnf + [7] 33.14/9.90 [7 7] [7] 33.14/9.90 >= [7 7] cnf + [7] 33.14/9.90 [7 4] [7] 33.14/9.90 = [satck(cnf, guess(cnf))] 33.14/9.90 33.14/9.90 [satck(cnf, assign)] = [0 3] cnf + [7 4] assign + [7] 33.14/9.90 [7 3] [0 1] [7] 33.14/9.90 > [7 0] assign + [0] 33.14/9.90 [0 1] [0] 33.14/9.90 = [if(verify(assign), assign, unsat())] 33.14/9.90 33.14/9.90 33.14/9.90 We return to the main proof. 33.14/9.90 33.14/9.90 We are left with following problem, upon which TcT provides the 33.14/9.90 certificate YES(O(1),O(1)). 33.14/9.90 33.14/9.90 Weak Trs: 33.14/9.90 { if(true(), t, e) -> t 33.14/9.90 , if(false(), t, e) -> e 33.14/9.90 , member(x, nil()) -> false() 33.14/9.90 , member(x, cons(y, ys)) -> if(eq(x, y), true(), member(x, ys)) 33.14/9.90 , eq(nil(), nil()) -> true() 33.14/9.90 , eq(O(x), 0(y)) -> eq(x, y) 33.14/9.90 , eq(0(x), 1(y)) -> false() 33.14/9.90 , eq(1(x), 0(y)) -> false() 33.14/9.90 , eq(1(x), 1(y)) -> eq(x, y) 33.14/9.90 , negate(0(x)) -> 1(x) 33.14/9.90 , negate(1(x)) -> 0(x) 33.14/9.90 , choice(cons(x, xs)) -> x 33.14/9.90 , choice(cons(x, xs)) -> choice(xs) 33.14/9.90 , guess(nil()) -> nil() 33.14/9.90 , guess(cons(clause, cnf)) -> cons(choice(clause), guess(cnf)) 33.14/9.90 , verify(nil()) -> true() 33.14/9.90 , verify(cons(l, ls)) -> 33.14/9.90 if(member(negate(l), ls), false(), verify(ls)) 33.14/9.90 , sat(cnf) -> satck(cnf, guess(cnf)) 33.14/9.90 , satck(cnf, assign) -> if(verify(assign), assign, unsat()) } 33.14/9.90 Obligation: 33.14/9.90 innermost runtime complexity 33.14/9.90 Answer: 33.14/9.90 YES(O(1),O(1)) 33.14/9.90 33.14/9.90 Empty rules are trivially bounded 33.14/9.90 33.14/9.90 Hurray, we answered YES(O(1),O(n^2)) 33.41/9.91 EOF