YES(O(1),O(n^1)) 560.35/148.44 YES(O(1),O(n^1)) 560.35/148.44 560.35/148.44 We are left with following problem, upon which TcT provides the 560.35/148.44 certificate YES(O(1),O(n^1)). 560.35/148.44 560.35/148.44 Strict Trs: 560.35/148.44 { number42() -> 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Nil())))))))))))))))))))))))))))))))))))))))))) 560.35/148.44 , nolexicord(Nil(), b1, a2, b2, a3, b3) -> 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Nil())))))))))))))))))))))))))))))))))))))))))) 560.35/148.44 , nolexicord(Cons(x, xs), b1, a2, b2, a3, b3) -> 560.35/148.44 nolexicord[Ite][False][Ite](eqNatList(Cons(x, xs), b1), 560.35/148.44 Cons(x, xs), 560.35/148.44 b1, 560.35/148.44 a2, 560.35/148.44 b2, 560.35/148.44 a3, 560.35/148.44 b3) 560.35/148.44 , eqNatList(Nil(), Nil()) -> True() 560.35/148.44 , eqNatList(Nil(), Cons(y, ys)) -> False() 560.35/148.44 , eqNatList(Cons(x, xs), Nil()) -> False() 560.35/148.44 , eqNatList(Cons(x, xs), Cons(y, ys)) -> 560.35/148.44 eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) 560.35/148.44 , goal(a1, b1, a2, b2, a3, b3) -> 560.35/148.44 nolexicord(a1, b1, a2, b2, a3, b3) } 560.35/148.44 Weak Trs: 560.35/148.44 { nolexicord[Ite][False][Ite](True(), 560.35/148.44 Cons(x', xs'), 560.35/148.44 Cons(x', xs'), 560.35/148.44 Cons(x', xs'), 560.35/148.44 Cons(x', xs'), 560.35/148.44 Cons(x, xs), 560.35/148.44 Cons(x', xs')) 560.35/148.44 -> nolexicord(xs', xs', xs', xs', xs', xs) 560.35/148.44 , nolexicord[Ite][False][Ite](False(), 560.35/148.44 Cons(x', xs'), 560.35/148.44 Cons(x', xs'), 560.35/148.44 Cons(x', xs'), 560.35/148.44 Cons(x', xs'), 560.35/148.44 Cons(x', xs'), 560.35/148.44 Cons(x, xs)) 560.35/148.44 -> nolexicord(xs', xs', xs', xs', xs', xs) 560.35/148.44 , !EQ(S(x), S(y)) -> !EQ(x, y) 560.35/148.44 , !EQ(S(x), 0()) -> False() 560.35/148.44 , !EQ(0(), S(y)) -> False() 560.35/148.44 , !EQ(0(), 0()) -> True() } 560.35/148.44 Obligation: 560.35/148.44 innermost runtime complexity 560.35/148.44 Answer: 560.35/148.44 YES(O(1),O(n^1)) 560.35/148.44 560.35/148.44 We add the following weak dependency pairs: 560.35/148.44 560.35/148.44 Strict DPs: 560.35/148.44 { number42^#() -> c_1() 560.35/148.44 , nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_2() 560.35/148.44 , nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) -> 560.35/148.44 c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1), 560.35/148.44 Cons(x, xs), 560.35/148.44 b1, 560.35/148.44 a2, 560.35/148.44 b2, 560.35/148.44 a3, 560.35/148.44 b3)) 560.35/148.44 , eqNatList^#(Nil(), Nil()) -> c_4() 560.35/148.44 , eqNatList^#(Nil(), Cons(y, ys)) -> c_5() 560.35/148.44 , eqNatList^#(Cons(x, xs), Nil()) -> c_6() 560.35/148.44 , eqNatList^#(Cons(x, xs), Cons(y, ys)) -> c_7(!EQ^#(x, y)) 560.35/148.44 , goal^#(a1, b1, a2, b2, a3, b3) -> 560.35/148.44 c_8(nolexicord^#(a1, b1, a2, b2, a3, b3)) } 560.35/148.44 Weak DPs: 560.35/148.44 { nolexicord[Ite][False][Ite]^#(True(), 560.35/148.44 Cons(x', xs'), 560.35/148.44 Cons(x', xs'), 560.35/148.44 Cons(x', xs'), 560.35/148.44 Cons(x', xs'), 560.35/148.44 Cons(x, xs), 560.35/148.44 Cons(x', xs')) 560.35/148.44 -> c_9(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.44 , nolexicord[Ite][False][Ite]^#(False(), 560.35/148.44 Cons(x', xs'), 560.35/148.44 Cons(x', xs'), 560.35/148.44 Cons(x', xs'), 560.35/148.44 Cons(x', xs'), 560.35/148.44 Cons(x', xs'), 560.35/148.44 Cons(x, xs)) 560.35/148.44 -> c_10(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.44 , !EQ^#(S(x), S(y)) -> c_11(!EQ^#(x, y)) 560.35/148.44 , !EQ^#(S(x), 0()) -> c_12() 560.35/148.44 , !EQ^#(0(), S(y)) -> c_13() 560.35/148.44 , !EQ^#(0(), 0()) -> c_14() } 560.35/148.44 560.35/148.44 and mark the set of starting terms. 560.35/148.44 560.35/148.44 We are left with following problem, upon which TcT provides the 560.35/148.44 certificate YES(O(1),O(n^1)). 560.35/148.44 560.35/148.44 Strict DPs: 560.35/148.44 { number42^#() -> c_1() 560.35/148.44 , nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_2() 560.35/148.44 , nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) -> 560.35/148.44 c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1), 560.35/148.44 Cons(x, xs), 560.35/148.44 b1, 560.35/148.44 a2, 560.35/148.44 b2, 560.35/148.44 a3, 560.35/148.44 b3)) 560.35/148.44 , eqNatList^#(Nil(), Nil()) -> c_4() 560.35/148.44 , eqNatList^#(Nil(), Cons(y, ys)) -> c_5() 560.35/148.44 , eqNatList^#(Cons(x, xs), Nil()) -> c_6() 560.35/148.44 , eqNatList^#(Cons(x, xs), Cons(y, ys)) -> c_7(!EQ^#(x, y)) 560.35/148.44 , goal^#(a1, b1, a2, b2, a3, b3) -> 560.35/148.44 c_8(nolexicord^#(a1, b1, a2, b2, a3, b3)) } 560.35/148.44 Strict Trs: 560.35/148.44 { number42() -> 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.44 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Nil())))))))))))))))))))))))))))))))))))))))))) 560.35/148.45 , nolexicord(Nil(), b1, a2, b2, a3, b3) -> 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Cons(Nil(), 560.35/148.45 Nil())))))))))))))))))))))))))))))))))))))))))) 560.35/148.45 , nolexicord(Cons(x, xs), b1, a2, b2, a3, b3) -> 560.35/148.45 nolexicord[Ite][False][Ite](eqNatList(Cons(x, xs), b1), 560.35/148.45 Cons(x, xs), 560.35/148.45 b1, 560.35/148.45 a2, 560.35/148.45 b2, 560.35/148.45 a3, 560.35/148.45 b3) 560.35/148.45 , eqNatList(Nil(), Nil()) -> True() 560.35/148.45 , eqNatList(Nil(), Cons(y, ys)) -> False() 560.35/148.45 , eqNatList(Cons(x, xs), Nil()) -> False() 560.35/148.45 , eqNatList(Cons(x, xs), Cons(y, ys)) -> 560.35/148.45 eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) 560.35/148.45 , goal(a1, b1, a2, b2, a3, b3) -> 560.35/148.45 nolexicord(a1, b1, a2, b2, a3, b3) } 560.35/148.45 Weak DPs: 560.35/148.45 { nolexicord[Ite][False][Ite]^#(True(), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x, xs), 560.35/148.45 Cons(x', xs')) 560.35/148.45 -> c_9(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.45 , nolexicord[Ite][False][Ite]^#(False(), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x, xs)) 560.35/148.45 -> c_10(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.45 , !EQ^#(S(x), S(y)) -> c_11(!EQ^#(x, y)) 560.35/148.45 , !EQ^#(S(x), 0()) -> c_12() 560.35/148.45 , !EQ^#(0(), S(y)) -> c_13() 560.35/148.45 , !EQ^#(0(), 0()) -> c_14() } 560.35/148.45 Weak Trs: 560.35/148.45 { nolexicord[Ite][False][Ite](True(), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x, xs), 560.35/148.45 Cons(x', xs')) 560.35/148.45 -> nolexicord(xs', xs', xs', xs', xs', xs) 560.35/148.45 , nolexicord[Ite][False][Ite](False(), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x, xs)) 560.35/148.45 -> nolexicord(xs', xs', xs', xs', xs', xs) 560.35/148.45 , !EQ(S(x), S(y)) -> !EQ(x, y) 560.35/148.45 , !EQ(S(x), 0()) -> False() 560.35/148.45 , !EQ(0(), S(y)) -> False() 560.35/148.45 , !EQ(0(), 0()) -> True() } 560.35/148.45 Obligation: 560.35/148.45 innermost runtime complexity 560.35/148.45 Answer: 560.35/148.45 YES(O(1),O(n^1)) 560.35/148.45 560.35/148.45 We replace rewrite rules by usable rules: 560.35/148.45 560.35/148.45 Strict Usable Rules: 560.35/148.45 { eqNatList(Nil(), Nil()) -> True() 560.35/148.45 , eqNatList(Nil(), Cons(y, ys)) -> False() 560.35/148.45 , eqNatList(Cons(x, xs), Nil()) -> False() 560.35/148.45 , eqNatList(Cons(x, xs), Cons(y, ys)) -> 560.35/148.45 eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) } 560.35/148.45 Weak Usable Rules: 560.35/148.45 { !EQ(S(x), S(y)) -> !EQ(x, y) 560.35/148.45 , !EQ(S(x), 0()) -> False() 560.35/148.45 , !EQ(0(), S(y)) -> False() 560.35/148.45 , !EQ(0(), 0()) -> True() } 560.35/148.45 560.35/148.45 We are left with following problem, upon which TcT provides the 560.35/148.45 certificate YES(O(1),O(n^1)). 560.35/148.45 560.35/148.45 Strict DPs: 560.35/148.45 { number42^#() -> c_1() 560.35/148.45 , nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_2() 560.35/148.45 , nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) -> 560.35/148.45 c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1), 560.35/148.45 Cons(x, xs), 560.35/148.45 b1, 560.35/148.45 a2, 560.35/148.45 b2, 560.35/148.45 a3, 560.35/148.45 b3)) 560.35/148.45 , eqNatList^#(Nil(), Nil()) -> c_4() 560.35/148.45 , eqNatList^#(Nil(), Cons(y, ys)) -> c_5() 560.35/148.45 , eqNatList^#(Cons(x, xs), Nil()) -> c_6() 560.35/148.45 , eqNatList^#(Cons(x, xs), Cons(y, ys)) -> c_7(!EQ^#(x, y)) 560.35/148.45 , goal^#(a1, b1, a2, b2, a3, b3) -> 560.35/148.45 c_8(nolexicord^#(a1, b1, a2, b2, a3, b3)) } 560.35/148.45 Strict Trs: 560.35/148.45 { eqNatList(Nil(), Nil()) -> True() 560.35/148.45 , eqNatList(Nil(), Cons(y, ys)) -> False() 560.35/148.45 , eqNatList(Cons(x, xs), Nil()) -> False() 560.35/148.45 , eqNatList(Cons(x, xs), Cons(y, ys)) -> 560.35/148.45 eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) } 560.35/148.45 Weak DPs: 560.35/148.45 { nolexicord[Ite][False][Ite]^#(True(), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x, xs), 560.35/148.45 Cons(x', xs')) 560.35/148.45 -> c_9(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.45 , nolexicord[Ite][False][Ite]^#(False(), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x, xs)) 560.35/148.45 -> c_10(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.45 , !EQ^#(S(x), S(y)) -> c_11(!EQ^#(x, y)) 560.35/148.45 , !EQ^#(S(x), 0()) -> c_12() 560.35/148.45 , !EQ^#(0(), S(y)) -> c_13() 560.35/148.45 , !EQ^#(0(), 0()) -> c_14() } 560.35/148.45 Weak Trs: 560.35/148.45 { !EQ(S(x), S(y)) -> !EQ(x, y) 560.35/148.45 , !EQ(S(x), 0()) -> False() 560.35/148.45 , !EQ(0(), S(y)) -> False() 560.35/148.45 , !EQ(0(), 0()) -> True() } 560.35/148.45 Obligation: 560.35/148.45 innermost runtime complexity 560.35/148.45 Answer: 560.35/148.45 YES(O(1),O(n^1)) 560.35/148.45 560.35/148.45 The weightgap principle applies (using the following constant 560.35/148.45 growth matrix-interpretation) 560.35/148.45 560.35/148.45 The following argument positions are usable: 560.35/148.45 Uargs(eqNatList[Match][Cons][Match][Cons][Ite]) = {1}, 560.35/148.45 Uargs(c_3) = {1}, Uargs(nolexicord[Ite][False][Ite]^#) = {1}, 560.35/148.45 Uargs(c_7) = {1}, Uargs(c_8) = {1}, Uargs(c_9) = {1}, 560.35/148.45 Uargs(c_10) = {1}, Uargs(c_11) = {1} 560.35/148.45 560.35/148.45 TcT has computed the following constructor-restricted matrix 560.35/148.45 interpretation. 560.35/148.45 560.35/148.45 [True] = [0] 560.35/148.45 [0] 560.35/148.45 560.35/148.45 [Nil] = [0] 560.35/148.45 [2] 560.35/148.45 560.35/148.45 [eqNatList[Match][Cons][Match][Cons][Ite]](x1, x2, x3, x4, x5) = [1 560.35/148.45 0] x1 + [1] 560.35/148.45 [0 560.35/148.45 0] [0] 560.35/148.45 560.35/148.45 [!EQ](x1, x2) = [0] 560.35/148.45 [0] 560.35/148.45 560.35/148.45 [S](x1) = [1 560.35/148.45 0] x1 + [0] 560.35/148.45 [0 560.35/148.45 0] [0] 560.35/148.45 560.35/148.45 [Cons](x1, x2) = [0] 560.35/148.45 [2] 560.35/148.45 560.35/148.45 [0] = [0] 560.35/148.45 [0] 560.35/148.45 560.35/148.45 [eqNatList](x1, x2) = [0 560.35/148.45 2] x1 + [0] 560.35/148.45 [0 560.35/148.45 0] [0] 560.35/148.45 560.35/148.45 [False] = [0] 560.35/148.45 [0] 560.35/148.45 560.35/148.45 [number42^#] = [2] 560.35/148.45 [1] 560.35/148.45 560.35/148.45 [c_1] = [1] 560.35/148.45 [1] 560.35/148.45 560.35/148.45 [nolexicord^#](x1, x2, x3, x4, x5, x6) = [0] 560.35/148.45 [0] 560.35/148.45 560.35/148.45 [c_2] = [1] 560.35/148.45 [1] 560.35/148.45 560.35/148.45 [c_3](x1) = [1 560.35/148.45 0] x1 + [2] 560.35/148.45 [0 560.35/148.45 1] [2] 560.35/148.45 560.35/148.45 [nolexicord[Ite][False][Ite]^#](x1, x2, x3, x4, x5, x6, x7) = [1 560.35/148.45 0] x1 + [0] 560.35/148.45 [0 560.35/148.45 0] [0] 560.35/148.45 560.35/148.45 [eqNatList^#](x1, x2) = [0] 560.35/148.45 [0] 560.35/148.45 560.35/148.45 [c_4] = [1] 560.35/148.45 [1] 560.35/148.45 560.35/148.45 [c_5] = [1] 560.35/148.45 [1] 560.35/148.45 560.35/148.45 [c_6] = [2] 560.35/148.45 [1] 560.35/148.45 560.35/148.45 [c_7](x1) = [1 560.35/148.45 0] x1 + [1] 560.35/148.45 [0 560.35/148.45 1] [2] 560.35/148.45 560.35/148.45 [!EQ^#](x1, x2) = [1] 560.35/148.45 [0] 560.35/148.45 560.35/148.45 [goal^#](x1, x2, x3, x4, x5, x6) = [1 560.35/148.45 1] x1 + [2 1] x2 + [1 2] x3 + [1 560.35/148.45 1] x4 + [2 560.35/148.45 1] x5 + [2 560.35/148.45 1] x6 + [1] 560.35/148.45 [1 560.35/148.45 1] [1 1] [1 1] [1 560.35/148.45 1] [1 560.35/148.45 1] [1 560.35/148.45 1] [1] 560.35/148.45 560.35/148.45 [c_8](x1) = [1 560.35/148.45 0] x1 + [2] 560.35/148.45 [0 560.35/148.45 1] [2] 560.35/148.45 560.35/148.45 [c_9](x1) = [1 560.35/148.45 0] x1 + [0] 560.35/148.45 [0 560.35/148.45 1] [0] 560.35/148.45 560.35/148.45 [c_10](x1) = [1 560.35/148.45 0] x1 + [0] 560.35/148.45 [0 560.35/148.45 1] [0] 560.35/148.45 560.35/148.45 [c_11](x1) = [1 560.35/148.45 0] x1 + [0] 560.35/148.45 [0 560.35/148.45 1] [0] 560.35/148.45 560.35/148.45 [c_12] = [1] 560.35/148.45 [0] 560.35/148.45 560.35/148.45 [c_13] = [1] 560.35/148.45 [0] 560.35/148.45 560.35/148.45 [c_14] = [1] 560.35/148.45 [0] 560.35/148.45 560.35/148.45 The order satisfies the following ordering constraints: 560.35/148.45 560.35/148.45 [!EQ(S(x), S(y))] = [0] 560.35/148.45 [0] 560.35/148.45 >= [0] 560.35/148.45 [0] 560.35/148.45 = [!EQ(x, y)] 560.35/148.45 560.35/148.45 [!EQ(S(x), 0())] = [0] 560.35/148.45 [0] 560.35/148.45 >= [0] 560.35/148.45 [0] 560.35/148.45 = [False()] 560.35/148.45 560.35/148.45 [!EQ(0(), S(y))] = [0] 560.35/148.45 [0] 560.35/148.45 >= [0] 560.35/148.45 [0] 560.35/148.45 = [False()] 560.35/148.45 560.35/148.45 [!EQ(0(), 0())] = [0] 560.35/148.45 [0] 560.35/148.45 >= [0] 560.35/148.45 [0] 560.35/148.45 = [True()] 560.35/148.45 560.35/148.45 [eqNatList(Nil(), Nil())] = [4] 560.35/148.45 [0] 560.35/148.45 > [0] 560.35/148.45 [0] 560.35/148.45 = [True()] 560.35/148.45 560.35/148.45 [eqNatList(Nil(), Cons(y, ys))] = [4] 560.35/148.45 [0] 560.35/148.45 > [0] 560.35/148.45 [0] 560.35/148.45 = [False()] 560.35/148.45 560.35/148.45 [eqNatList(Cons(x, xs), Nil())] = [4] 560.35/148.45 [0] 560.35/148.45 > [0] 560.35/148.45 [0] 560.35/148.45 = [False()] 560.35/148.45 560.35/148.45 [eqNatList(Cons(x, xs), Cons(y, ys))] = [4] 560.35/148.45 [0] 560.35/148.45 > [1] 560.35/148.45 [0] 560.35/148.45 = [eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs)] 560.35/148.45 560.35/148.45 [number42^#()] = [2] 560.35/148.45 [1] 560.35/148.45 > [1] 560.35/148.45 [1] 560.35/148.45 = [c_1()] 560.35/148.45 560.35/148.45 [nolexicord^#(Nil(), b1, a2, b2, a3, b3)] = [0] 560.35/148.45 [0] 560.35/148.45 ? [1] 560.35/148.45 [1] 560.35/148.45 = [c_2()] 560.35/148.45 560.35/148.45 [nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3)] = [0] 560.35/148.45 [0] 560.35/148.45 ? [6] 560.35/148.45 [2] 560.35/148.45 = [c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1), 560.35/148.45 Cons(x, xs), 560.35/148.45 b1, 560.35/148.45 a2, 560.35/148.45 b2, 560.35/148.45 a3, 560.35/148.45 b3))] 560.35/148.45 560.35/148.45 [nolexicord[Ite][False][Ite]^#(True(), = [0] 560.35/148.45 Cons(x', xs'), [0] 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x, xs), 560.35/148.45 Cons(x', xs'))] 560.35/148.45 >= [0] 560.35/148.45 [0] 560.35/148.45 = [c_9(nolexicord^#(xs', xs', xs', xs', xs', xs))] 560.35/148.45 560.35/148.45 [nolexicord[Ite][False][Ite]^#(False(), = [0] 560.35/148.45 Cons(x', xs'), [0] 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x', xs'), 560.35/148.45 Cons(x, xs))] 560.35/148.46 >= [0] 560.35/148.46 [0] 560.35/148.46 = [c_10(nolexicord^#(xs', xs', xs', xs', xs', xs))] 560.35/148.46 560.35/148.46 [eqNatList^#(Nil(), Nil())] = [0] 560.35/148.46 [0] 560.35/148.46 ? [1] 560.35/148.46 [1] 560.35/148.46 = [c_4()] 560.35/148.46 560.35/148.46 [eqNatList^#(Nil(), Cons(y, ys))] = [0] 560.35/148.46 [0] 560.35/148.46 ? [1] 560.35/148.46 [1] 560.35/148.46 = [c_5()] 560.35/148.46 560.35/148.46 [eqNatList^#(Cons(x, xs), Nil())] = [0] 560.35/148.46 [0] 560.35/148.46 ? [2] 560.35/148.46 [1] 560.35/148.46 = [c_6()] 560.35/148.46 560.35/148.46 [eqNatList^#(Cons(x, xs), Cons(y, ys))] = [0] 560.35/148.46 [0] 560.35/148.46 ? [2] 560.35/148.46 [2] 560.35/148.46 = [c_7(!EQ^#(x, y))] 560.35/148.46 560.35/148.46 [!EQ^#(S(x), S(y))] = [1] 560.35/148.46 [0] 560.35/148.46 >= [1] 560.35/148.46 [0] 560.35/148.46 = [c_11(!EQ^#(x, y))] 560.35/148.46 560.35/148.46 [!EQ^#(S(x), 0())] = [1] 560.35/148.46 [0] 560.35/148.46 >= [1] 560.35/148.46 [0] 560.35/148.46 = [c_12()] 560.35/148.46 560.35/148.46 [!EQ^#(0(), S(y))] = [1] 560.35/148.46 [0] 560.35/148.46 >= [1] 560.35/148.46 [0] 560.35/148.46 = [c_13()] 560.35/148.46 560.35/148.46 [!EQ^#(0(), 0())] = [1] 560.35/148.46 [0] 560.35/148.46 >= [1] 560.35/148.46 [0] 560.35/148.46 = [c_14()] 560.35/148.46 560.35/148.46 [goal^#(a1, b1, a2, b2, a3, b3)] = [2 1] b1 + [1 2] a2 + [1 1] b2 + [2 1] a3 + [2 1] b3 + [1 560.35/148.46 1] a1 + [1] 560.35/148.46 [1 1] [1 1] [1 1] [1 1] [1 1] [1 560.35/148.46 1] [1] 560.35/148.46 ? [2] 560.35/148.46 [2] 560.35/148.46 = [c_8(nolexicord^#(a1, b1, a2, b2, a3, b3))] 560.35/148.46 560.35/148.46 560.35/148.46 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 560.35/148.46 560.35/148.46 We are left with following problem, upon which TcT provides the 560.35/148.46 certificate YES(O(1),O(n^1)). 560.35/148.46 560.35/148.46 Strict DPs: 560.35/148.46 { nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_2() 560.35/148.46 , nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) -> 560.35/148.46 c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1), 560.35/148.46 Cons(x, xs), 560.35/148.46 b1, 560.35/148.46 a2, 560.35/148.46 b2, 560.35/148.46 a3, 560.35/148.46 b3)) 560.35/148.46 , eqNatList^#(Nil(), Nil()) -> c_4() 560.35/148.46 , eqNatList^#(Nil(), Cons(y, ys)) -> c_5() 560.35/148.46 , eqNatList^#(Cons(x, xs), Nil()) -> c_6() 560.35/148.46 , eqNatList^#(Cons(x, xs), Cons(y, ys)) -> c_7(!EQ^#(x, y)) 560.35/148.46 , goal^#(a1, b1, a2, b2, a3, b3) -> 560.35/148.46 c_8(nolexicord^#(a1, b1, a2, b2, a3, b3)) } 560.35/148.46 Weak DPs: 560.35/148.46 { number42^#() -> c_1() 560.35/148.46 , nolexicord[Ite][False][Ite]^#(True(), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x, xs), 560.35/148.46 Cons(x', xs')) 560.35/148.46 -> c_9(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.46 , nolexicord[Ite][False][Ite]^#(False(), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x, xs)) 560.35/148.46 -> c_10(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.46 , !EQ^#(S(x), S(y)) -> c_11(!EQ^#(x, y)) 560.35/148.46 , !EQ^#(S(x), 0()) -> c_12() 560.35/148.46 , !EQ^#(0(), S(y)) -> c_13() 560.35/148.46 , !EQ^#(0(), 0()) -> c_14() } 560.35/148.46 Weak Trs: 560.35/148.46 { !EQ(S(x), S(y)) -> !EQ(x, y) 560.35/148.46 , !EQ(S(x), 0()) -> False() 560.35/148.46 , !EQ(0(), S(y)) -> False() 560.35/148.46 , !EQ(0(), 0()) -> True() 560.35/148.46 , eqNatList(Nil(), Nil()) -> True() 560.35/148.46 , eqNatList(Nil(), Cons(y, ys)) -> False() 560.35/148.46 , eqNatList(Cons(x, xs), Nil()) -> False() 560.35/148.46 , eqNatList(Cons(x, xs), Cons(y, ys)) -> 560.35/148.46 eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) } 560.35/148.46 Obligation: 560.35/148.46 innermost runtime complexity 560.35/148.46 Answer: 560.35/148.46 YES(O(1),O(n^1)) 560.35/148.46 560.35/148.46 We estimate the number of application of {3,4,5,6} by applications 560.35/148.46 of Pre({3,4,5,6}) = {}. Here rules are labeled as follows: 560.35/148.46 560.35/148.46 DPs: 560.35/148.46 { 1: nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_2() 560.35/148.46 , 2: nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) -> 560.35/148.46 c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1), 560.35/148.46 Cons(x, xs), 560.35/148.46 b1, 560.35/148.46 a2, 560.35/148.46 b2, 560.35/148.46 a3, 560.35/148.46 b3)) 560.35/148.46 , 3: eqNatList^#(Nil(), Nil()) -> c_4() 560.35/148.46 , 4: eqNatList^#(Nil(), Cons(y, ys)) -> c_5() 560.35/148.46 , 5: eqNatList^#(Cons(x, xs), Nil()) -> c_6() 560.35/148.46 , 6: eqNatList^#(Cons(x, xs), Cons(y, ys)) -> c_7(!EQ^#(x, y)) 560.35/148.46 , 7: goal^#(a1, b1, a2, b2, a3, b3) -> 560.35/148.46 c_8(nolexicord^#(a1, b1, a2, b2, a3, b3)) 560.35/148.46 , 8: number42^#() -> c_1() 560.35/148.46 , 9: nolexicord[Ite][False][Ite]^#(True(), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x, xs), 560.35/148.46 Cons(x', xs')) 560.35/148.46 -> c_9(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.46 , 10: nolexicord[Ite][False][Ite]^#(False(), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x, xs)) 560.35/148.46 -> c_10(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.46 , 11: !EQ^#(S(x), S(y)) -> c_11(!EQ^#(x, y)) 560.35/148.46 , 12: !EQ^#(S(x), 0()) -> c_12() 560.35/148.46 , 13: !EQ^#(0(), S(y)) -> c_13() 560.35/148.46 , 14: !EQ^#(0(), 0()) -> c_14() } 560.35/148.46 560.35/148.46 We are left with following problem, upon which TcT provides the 560.35/148.46 certificate YES(O(1),O(n^1)). 560.35/148.46 560.35/148.46 Strict DPs: 560.35/148.46 { nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_2() 560.35/148.46 , nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) -> 560.35/148.46 c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1), 560.35/148.46 Cons(x, xs), 560.35/148.46 b1, 560.35/148.46 a2, 560.35/148.46 b2, 560.35/148.46 a3, 560.35/148.46 b3)) 560.35/148.46 , goal^#(a1, b1, a2, b2, a3, b3) -> 560.35/148.46 c_8(nolexicord^#(a1, b1, a2, b2, a3, b3)) } 560.35/148.46 Weak DPs: 560.35/148.46 { number42^#() -> c_1() 560.35/148.46 , nolexicord[Ite][False][Ite]^#(True(), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x, xs), 560.35/148.46 Cons(x', xs')) 560.35/148.46 -> c_9(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.46 , nolexicord[Ite][False][Ite]^#(False(), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x, xs)) 560.35/148.46 -> c_10(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.46 , eqNatList^#(Nil(), Nil()) -> c_4() 560.35/148.46 , eqNatList^#(Nil(), Cons(y, ys)) -> c_5() 560.35/148.46 , eqNatList^#(Cons(x, xs), Nil()) -> c_6() 560.35/148.46 , eqNatList^#(Cons(x, xs), Cons(y, ys)) -> c_7(!EQ^#(x, y)) 560.35/148.46 , !EQ^#(S(x), S(y)) -> c_11(!EQ^#(x, y)) 560.35/148.46 , !EQ^#(S(x), 0()) -> c_12() 560.35/148.46 , !EQ^#(0(), S(y)) -> c_13() 560.35/148.46 , !EQ^#(0(), 0()) -> c_14() } 560.35/148.46 Weak Trs: 560.35/148.46 { !EQ(S(x), S(y)) -> !EQ(x, y) 560.35/148.46 , !EQ(S(x), 0()) -> False() 560.35/148.46 , !EQ(0(), S(y)) -> False() 560.35/148.46 , !EQ(0(), 0()) -> True() 560.35/148.46 , eqNatList(Nil(), Nil()) -> True() 560.35/148.46 , eqNatList(Nil(), Cons(y, ys)) -> False() 560.35/148.46 , eqNatList(Cons(x, xs), Nil()) -> False() 560.35/148.46 , eqNatList(Cons(x, xs), Cons(y, ys)) -> 560.35/148.46 eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) } 560.35/148.46 Obligation: 560.35/148.46 innermost runtime complexity 560.35/148.46 Answer: 560.35/148.46 YES(O(1),O(n^1)) 560.35/148.46 560.35/148.46 The following weak DPs constitute a sub-graph of the DG that is 560.35/148.46 closed under successors. The DPs are removed. 560.35/148.46 560.35/148.46 { number42^#() -> c_1() 560.35/148.46 , eqNatList^#(Nil(), Nil()) -> c_4() 560.35/148.46 , eqNatList^#(Nil(), Cons(y, ys)) -> c_5() 560.35/148.46 , eqNatList^#(Cons(x, xs), Nil()) -> c_6() 560.35/148.46 , eqNatList^#(Cons(x, xs), Cons(y, ys)) -> c_7(!EQ^#(x, y)) 560.35/148.46 , !EQ^#(S(x), S(y)) -> c_11(!EQ^#(x, y)) 560.35/148.46 , !EQ^#(S(x), 0()) -> c_12() 560.35/148.46 , !EQ^#(0(), S(y)) -> c_13() 560.35/148.46 , !EQ^#(0(), 0()) -> c_14() } 560.35/148.46 560.35/148.46 We are left with following problem, upon which TcT provides the 560.35/148.46 certificate YES(O(1),O(n^1)). 560.35/148.46 560.35/148.46 Strict DPs: 560.35/148.46 { nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_2() 560.35/148.46 , nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) -> 560.35/148.46 c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1), 560.35/148.46 Cons(x, xs), 560.35/148.46 b1, 560.35/148.46 a2, 560.35/148.46 b2, 560.35/148.46 a3, 560.35/148.46 b3)) 560.35/148.46 , goal^#(a1, b1, a2, b2, a3, b3) -> 560.35/148.46 c_8(nolexicord^#(a1, b1, a2, b2, a3, b3)) } 560.35/148.46 Weak DPs: 560.35/148.46 { nolexicord[Ite][False][Ite]^#(True(), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x, xs), 560.35/148.46 Cons(x', xs')) 560.35/148.46 -> c_9(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.46 , nolexicord[Ite][False][Ite]^#(False(), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x, xs)) 560.35/148.46 -> c_10(nolexicord^#(xs', xs', xs', xs', xs', xs)) } 560.35/148.46 Weak Trs: 560.35/148.46 { !EQ(S(x), S(y)) -> !EQ(x, y) 560.35/148.46 , !EQ(S(x), 0()) -> False() 560.35/148.46 , !EQ(0(), S(y)) -> False() 560.35/148.46 , !EQ(0(), 0()) -> True() 560.35/148.46 , eqNatList(Nil(), Nil()) -> True() 560.35/148.46 , eqNatList(Nil(), Cons(y, ys)) -> False() 560.35/148.46 , eqNatList(Cons(x, xs), Nil()) -> False() 560.35/148.46 , eqNatList(Cons(x, xs), Cons(y, ys)) -> 560.35/148.46 eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) } 560.35/148.46 Obligation: 560.35/148.46 innermost runtime complexity 560.35/148.46 Answer: 560.35/148.46 YES(O(1),O(n^1)) 560.35/148.46 560.35/148.46 Consider the dependency graph 560.35/148.46 560.35/148.46 1: nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_2() 560.35/148.46 560.35/148.46 2: nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) -> 560.35/148.46 c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1), 560.35/148.46 Cons(x, xs), 560.35/148.46 b1, 560.35/148.46 a2, 560.35/148.46 b2, 560.35/148.46 a3, 560.35/148.46 b3)) 560.35/148.46 -->_1 nolexicord[Ite][False][Ite]^#(False(), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x, xs)) 560.35/148.46 -> c_10(nolexicord^#(xs', xs', xs', xs', xs', xs)) :5 560.35/148.46 -->_1 nolexicord[Ite][False][Ite]^#(True(), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x, xs), 560.35/148.46 Cons(x', xs')) 560.35/148.46 -> c_9(nolexicord^#(xs', xs', xs', xs', xs', xs)) :4 560.35/148.46 560.35/148.46 3: goal^#(a1, b1, a2, b2, a3, b3) -> 560.35/148.46 c_8(nolexicord^#(a1, b1, a2, b2, a3, b3)) 560.35/148.46 -->_1 nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) -> 560.35/148.46 c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1), 560.35/148.46 Cons(x, xs), 560.35/148.46 b1, 560.35/148.46 a2, 560.35/148.46 b2, 560.35/148.46 a3, 560.35/148.46 b3)) :2 560.35/148.46 -->_1 nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_2() :1 560.35/148.46 560.35/148.46 4: nolexicord[Ite][False][Ite]^#(True(), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x, xs), 560.35/148.46 Cons(x', xs')) 560.35/148.46 -> c_9(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.46 -->_1 nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) -> 560.35/148.46 c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1), 560.35/148.46 Cons(x, xs), 560.35/148.46 b1, 560.35/148.46 a2, 560.35/148.46 b2, 560.35/148.46 a3, 560.35/148.46 b3)) :2 560.35/148.46 -->_1 nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_2() :1 560.35/148.46 560.35/148.46 5: nolexicord[Ite][False][Ite]^#(False(), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x, xs)) 560.35/148.46 -> c_10(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.46 -->_1 nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) -> 560.35/148.46 c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1), 560.35/148.46 Cons(x, xs), 560.35/148.46 b1, 560.35/148.46 a2, 560.35/148.46 b2, 560.35/148.46 a3, 560.35/148.46 b3)) :2 560.35/148.46 -->_1 nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_2() :1 560.35/148.46 560.35/148.46 560.35/148.46 Following roots of the dependency graph are removed, as the 560.35/148.46 considered set of starting terms is closed under reduction with 560.35/148.46 respect to these rules (modulo compound contexts). 560.35/148.46 560.35/148.46 { goal^#(a1, b1, a2, b2, a3, b3) -> 560.35/148.46 c_8(nolexicord^#(a1, b1, a2, b2, a3, b3)) } 560.35/148.46 560.35/148.46 560.35/148.46 We are left with following problem, upon which TcT provides the 560.35/148.46 certificate YES(O(1),O(n^1)). 560.35/148.46 560.35/148.46 Strict DPs: 560.35/148.46 { nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_2() 560.35/148.46 , nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) -> 560.35/148.46 c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1), 560.35/148.46 Cons(x, xs), 560.35/148.46 b1, 560.35/148.46 a2, 560.35/148.46 b2, 560.35/148.46 a3, 560.35/148.46 b3)) } 560.35/148.46 Weak DPs: 560.35/148.46 { nolexicord[Ite][False][Ite]^#(True(), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x, xs), 560.35/148.46 Cons(x', xs')) 560.35/148.46 -> c_9(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.46 , nolexicord[Ite][False][Ite]^#(False(), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x, xs)) 560.35/148.46 -> c_10(nolexicord^#(xs', xs', xs', xs', xs', xs)) } 560.35/148.46 Weak Trs: 560.35/148.46 { !EQ(S(x), S(y)) -> !EQ(x, y) 560.35/148.46 , !EQ(S(x), 0()) -> False() 560.35/148.46 , !EQ(0(), S(y)) -> False() 560.35/148.46 , !EQ(0(), 0()) -> True() 560.35/148.46 , eqNatList(Nil(), Nil()) -> True() 560.35/148.46 , eqNatList(Nil(), Cons(y, ys)) -> False() 560.35/148.46 , eqNatList(Cons(x, xs), Nil()) -> False() 560.35/148.46 , eqNatList(Cons(x, xs), Cons(y, ys)) -> 560.35/148.46 eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) } 560.35/148.46 Obligation: 560.35/148.46 innermost runtime complexity 560.35/148.46 Answer: 560.35/148.46 YES(O(1),O(n^1)) 560.35/148.46 560.35/148.46 We use the processor 'matrix interpretation of dimension 1' to 560.35/148.46 orient following rules strictly. 560.35/148.46 560.35/148.46 DPs: 560.35/148.46 { 1: nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_2() } 560.35/148.46 560.35/148.46 Sub-proof: 560.35/148.46 ---------- 560.35/148.46 The following argument positions are usable: 560.35/148.46 Uargs(c_3) = {1}, Uargs(c_9) = {1}, Uargs(c_10) = {1} 560.35/148.46 560.35/148.46 TcT has computed the following constructor-restricted matrix 560.35/148.46 interpretation. Note that the diagonal of the component-wise maxima 560.35/148.46 of interpretation-entries (of constructors) contains no more than 0 560.35/148.46 non-zero entries. 560.35/148.46 560.35/148.46 [True] = [0] 560.35/148.46 560.35/148.46 [Nil] = [0] 560.35/148.46 560.35/148.46 [eqNatList[Match][Cons][Match][Cons][Ite]](x1, x2, x3, x4, x5) = [6] 560.35/148.46 560.35/148.46 [!EQ](x1, x2) = [0] 560.35/148.46 560.35/148.46 [S](x1) = [0] 560.35/148.46 560.35/148.46 [Cons](x1, x2) = [0] 560.35/148.46 560.35/148.46 [0] = [0] 560.35/148.46 560.35/148.46 [eqNatList](x1, x2) = [0] 560.35/148.46 560.35/148.46 [False] = [0] 560.35/148.46 560.35/148.46 [nolexicord^#](x1, x2, x3, x4, x5, x6) = [1] 560.35/148.46 560.35/148.46 [c_2] = [0] 560.35/148.46 560.35/148.46 [c_3](x1) = [1] x1 + [0] 560.35/148.46 560.35/148.46 [nolexicord[Ite][False][Ite]^#](x1, x2, x3, x4, x5, x6, x7) = [1] 560.35/148.46 560.35/148.46 [c_9](x1) = [1] x1 + [0] 560.35/148.46 560.35/148.46 [c_10](x1) = [1] x1 + [0] 560.35/148.46 560.35/148.46 The order satisfies the following ordering constraints: 560.35/148.46 560.35/148.46 [!EQ(S(x), S(y))] = [0] 560.35/148.46 >= [0] 560.35/148.46 = [!EQ(x, y)] 560.35/148.46 560.35/148.46 [!EQ(S(x), 0())] = [0] 560.35/148.46 >= [0] 560.35/148.46 = [False()] 560.35/148.46 560.35/148.46 [!EQ(0(), S(y))] = [0] 560.35/148.46 >= [0] 560.35/148.46 = [False()] 560.35/148.46 560.35/148.46 [!EQ(0(), 0())] = [0] 560.35/148.46 >= [0] 560.35/148.46 = [True()] 560.35/148.46 560.35/148.46 [eqNatList(Nil(), Nil())] = [0] 560.35/148.46 >= [0] 560.35/148.46 = [True()] 560.35/148.46 560.35/148.46 [eqNatList(Nil(), Cons(y, ys))] = [0] 560.35/148.46 >= [0] 560.35/148.46 = [False()] 560.35/148.46 560.35/148.46 [eqNatList(Cons(x, xs), Nil())] = [0] 560.35/148.46 >= [0] 560.35/148.46 = [False()] 560.35/148.46 560.35/148.46 [eqNatList(Cons(x, xs), Cons(y, ys))] = [0] 560.35/148.46 ? [6] 560.35/148.46 = [eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs)] 560.35/148.46 560.35/148.46 [nolexicord^#(Nil(), b1, a2, b2, a3, b3)] = [1] 560.35/148.46 > [0] 560.35/148.46 = [c_2()] 560.35/148.46 560.35/148.46 [nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3)] = [1] 560.35/148.46 >= [1] 560.35/148.46 = [c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1), 560.35/148.46 Cons(x, xs), 560.35/148.46 b1, 560.35/148.46 a2, 560.35/148.46 b2, 560.35/148.46 a3, 560.35/148.46 b3))] 560.35/148.46 560.35/148.46 [nolexicord[Ite][False][Ite]^#(True(), = [1] 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x, xs), 560.35/148.46 Cons(x', xs'))] 560.35/148.46 >= [1] 560.35/148.46 = [c_9(nolexicord^#(xs', xs', xs', xs', xs', xs))] 560.35/148.46 560.35/148.46 [nolexicord[Ite][False][Ite]^#(False(), = [1] 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.46 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x, xs))] 560.35/148.47 >= [1] 560.35/148.47 = [c_10(nolexicord^#(xs', xs', xs', xs', xs', xs))] 560.35/148.47 560.35/148.47 560.35/148.47 The strictly oriented rules are moved into the weak component. 560.35/148.47 560.35/148.47 We are left with following problem, upon which TcT provides the 560.35/148.47 certificate YES(O(1),O(n^1)). 560.35/148.47 560.35/148.47 Strict DPs: 560.35/148.47 { nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) -> 560.35/148.47 c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1), 560.35/148.47 Cons(x, xs), 560.35/148.47 b1, 560.35/148.47 a2, 560.35/148.47 b2, 560.35/148.47 a3, 560.35/148.47 b3)) } 560.35/148.47 Weak DPs: 560.35/148.47 { nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_2() 560.35/148.47 , nolexicord[Ite][False][Ite]^#(True(), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x, xs), 560.35/148.47 Cons(x', xs')) 560.35/148.47 -> c_9(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.47 , nolexicord[Ite][False][Ite]^#(False(), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x, xs)) 560.35/148.47 -> c_10(nolexicord^#(xs', xs', xs', xs', xs', xs)) } 560.35/148.47 Weak Trs: 560.35/148.47 { !EQ(S(x), S(y)) -> !EQ(x, y) 560.35/148.47 , !EQ(S(x), 0()) -> False() 560.35/148.47 , !EQ(0(), S(y)) -> False() 560.35/148.47 , !EQ(0(), 0()) -> True() 560.35/148.47 , eqNatList(Nil(), Nil()) -> True() 560.35/148.47 , eqNatList(Nil(), Cons(y, ys)) -> False() 560.35/148.47 , eqNatList(Cons(x, xs), Nil()) -> False() 560.35/148.47 , eqNatList(Cons(x, xs), Cons(y, ys)) -> 560.35/148.47 eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) } 560.35/148.47 Obligation: 560.35/148.47 innermost runtime complexity 560.35/148.47 Answer: 560.35/148.47 YES(O(1),O(n^1)) 560.35/148.47 560.35/148.47 The following weak DPs constitute a sub-graph of the DG that is 560.35/148.47 closed under successors. The DPs are removed. 560.35/148.47 560.35/148.47 { nolexicord^#(Nil(), b1, a2, b2, a3, b3) -> c_2() } 560.35/148.47 560.35/148.47 We are left with following problem, upon which TcT provides the 560.35/148.47 certificate YES(O(1),O(n^1)). 560.35/148.47 560.35/148.47 Strict DPs: 560.35/148.47 { nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) -> 560.35/148.47 c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1), 560.35/148.47 Cons(x, xs), 560.35/148.47 b1, 560.35/148.47 a2, 560.35/148.47 b2, 560.35/148.47 a3, 560.35/148.47 b3)) } 560.35/148.47 Weak DPs: 560.35/148.47 { nolexicord[Ite][False][Ite]^#(True(), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x, xs), 560.35/148.47 Cons(x', xs')) 560.35/148.47 -> c_9(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.47 , nolexicord[Ite][False][Ite]^#(False(), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x, xs)) 560.35/148.47 -> c_10(nolexicord^#(xs', xs', xs', xs', xs', xs)) } 560.35/148.47 Weak Trs: 560.35/148.47 { !EQ(S(x), S(y)) -> !EQ(x, y) 560.35/148.47 , !EQ(S(x), 0()) -> False() 560.35/148.47 , !EQ(0(), S(y)) -> False() 560.35/148.47 , !EQ(0(), 0()) -> True() 560.35/148.47 , eqNatList(Nil(), Nil()) -> True() 560.35/148.47 , eqNatList(Nil(), Cons(y, ys)) -> False() 560.35/148.47 , eqNatList(Cons(x, xs), Nil()) -> False() 560.35/148.47 , eqNatList(Cons(x, xs), Cons(y, ys)) -> 560.35/148.47 eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) } 560.35/148.47 Obligation: 560.35/148.47 innermost runtime complexity 560.35/148.47 Answer: 560.35/148.47 YES(O(1),O(n^1)) 560.35/148.47 560.35/148.47 We use the processor 'matrix interpretation of dimension 1' to 560.35/148.47 orient following rules strictly. 560.35/148.47 560.35/148.47 DPs: 560.35/148.47 { 2: nolexicord[Ite][False][Ite]^#(True(), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x, xs), 560.35/148.47 Cons(x', xs')) 560.35/148.47 -> c_9(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.47 , 3: nolexicord[Ite][False][Ite]^#(False(), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x, xs)) 560.35/148.47 -> c_10(nolexicord^#(xs', xs', xs', xs', xs', xs)) } 560.35/148.47 560.35/148.47 Sub-proof: 560.35/148.47 ---------- 560.35/148.47 The following argument positions are usable: 560.35/148.47 Uargs(c_3) = {1}, Uargs(c_9) = {1}, Uargs(c_10) = {1} 560.35/148.47 560.35/148.47 TcT has computed the following constructor-based matrix 560.35/148.47 interpretation satisfying not(EDA). 560.35/148.47 560.35/148.47 [True] = [0] 560.35/148.47 560.35/148.47 [Nil] = [0] 560.35/148.47 560.35/148.47 [eqNatList[Match][Cons][Match][Cons][Ite]](x1, x2, x3, x4, x5) = [1] x2 + [1] x3 + [1] x4 + [1] x5 + [1] 560.35/148.47 560.35/148.47 [!EQ](x1, x2) = [0] 560.35/148.47 560.35/148.47 [S](x1) = [1] x1 + [0] 560.35/148.47 560.35/148.47 [Cons](x1, x2) = [1] x2 + [1] 560.35/148.47 560.35/148.47 [0] = [0] 560.35/148.47 560.35/148.47 [eqNatList](x1, x2) = [0] 560.35/148.47 560.35/148.47 [False] = [0] 560.35/148.47 560.35/148.47 [nolexicord^#](x1, x2, x3, x4, x5, x6) = [1] x2 + [1] 560.35/148.47 560.35/148.47 [c_2] = [0] 560.35/148.47 560.35/148.47 [c_3](x1) = [1] x1 + [0] 560.35/148.47 560.35/148.47 [nolexicord[Ite][False][Ite]^#](x1, x2, x3, x4, x5, x6, x7) = [1] x3 + [1] 560.35/148.47 560.35/148.47 [c_9](x1) = [1] x1 + [0] 560.35/148.47 560.35/148.47 [c_10](x1) = [1] x1 + [0] 560.35/148.47 560.35/148.47 The order satisfies the following ordering constraints: 560.35/148.47 560.35/148.47 [!EQ(S(x), S(y))] = [0] 560.35/148.47 >= [0] 560.35/148.47 = [!EQ(x, y)] 560.35/148.47 560.35/148.47 [!EQ(S(x), 0())] = [0] 560.35/148.47 >= [0] 560.35/148.47 = [False()] 560.35/148.47 560.35/148.47 [!EQ(0(), S(y))] = [0] 560.35/148.47 >= [0] 560.35/148.47 = [False()] 560.35/148.47 560.35/148.47 [!EQ(0(), 0())] = [0] 560.35/148.47 >= [0] 560.35/148.47 = [True()] 560.35/148.47 560.35/148.47 [eqNatList(Nil(), Nil())] = [0] 560.35/148.47 >= [0] 560.35/148.47 = [True()] 560.35/148.47 560.35/148.47 [eqNatList(Nil(), Cons(y, ys))] = [0] 560.35/148.47 >= [0] 560.35/148.47 = [False()] 560.35/148.47 560.35/148.47 [eqNatList(Cons(x, xs), Nil())] = [0] 560.35/148.47 >= [0] 560.35/148.47 = [False()] 560.35/148.47 560.35/148.47 [eqNatList(Cons(x, xs), Cons(y, ys))] = [0] 560.35/148.47 ? [1] x + [1] xs + [1] y + [1] ys + [1] 560.35/148.47 = [eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs)] 560.35/148.47 560.35/148.47 [nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3)] = [1] b1 + [1] 560.35/148.47 >= [1] b1 + [1] 560.35/148.47 = [c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1), 560.35/148.47 Cons(x, xs), 560.35/148.47 b1, 560.35/148.47 a2, 560.35/148.47 b2, 560.35/148.47 a3, 560.35/148.47 b3))] 560.35/148.47 560.35/148.47 [nolexicord[Ite][False][Ite]^#(True(), = [1] xs' + [2] 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x, xs), 560.35/148.47 Cons(x', xs'))] 560.35/148.47 > [1] xs' + [1] 560.35/148.47 = [c_9(nolexicord^#(xs', xs', xs', xs', xs', xs))] 560.35/148.47 560.35/148.47 [nolexicord[Ite][False][Ite]^#(False(), = [1] xs' + [2] 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x, xs))] 560.35/148.47 > [1] xs' + [1] 560.35/148.47 = [c_10(nolexicord^#(xs', xs', xs', xs', xs', xs))] 560.35/148.47 560.35/148.47 560.35/148.47 We return to the main proof. Consider the set of all dependency 560.35/148.47 pairs 560.35/148.47 560.35/148.47 : 560.35/148.47 { 1: nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) -> 560.35/148.47 c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1), 560.35/148.47 Cons(x, xs), 560.35/148.47 b1, 560.35/148.47 a2, 560.35/148.47 b2, 560.35/148.47 a3, 560.35/148.47 b3)) 560.35/148.47 , 2: nolexicord[Ite][False][Ite]^#(True(), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x, xs), 560.35/148.47 Cons(x', xs')) 560.35/148.47 -> c_9(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.47 , 3: nolexicord[Ite][False][Ite]^#(False(), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x, xs)) 560.35/148.47 -> c_10(nolexicord^#(xs', xs', xs', xs', xs', xs)) } 560.35/148.47 560.35/148.47 Processor 'matrix interpretation of dimension 1' induces the 560.35/148.47 complexity certificate YES(?,O(n^1)) on application of dependency 560.35/148.47 pairs {2,3}. These cover all (indirect) predecessors of dependency 560.35/148.47 pairs {1,2,3}, their number of application is equally bounded. The 560.35/148.47 dependency pairs are shifted into the weak component. 560.35/148.47 560.35/148.47 We are left with following problem, upon which TcT provides the 560.35/148.47 certificate YES(O(1),O(1)). 560.35/148.47 560.35/148.47 Weak DPs: 560.35/148.47 { nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) -> 560.35/148.47 c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1), 560.35/148.47 Cons(x, xs), 560.35/148.47 b1, 560.35/148.47 a2, 560.35/148.47 b2, 560.35/148.47 a3, 560.35/148.47 b3)) 560.35/148.47 , nolexicord[Ite][False][Ite]^#(True(), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x, xs), 560.35/148.47 Cons(x', xs')) 560.35/148.47 -> c_9(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.47 , nolexicord[Ite][False][Ite]^#(False(), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x, xs)) 560.35/148.47 -> c_10(nolexicord^#(xs', xs', xs', xs', xs', xs)) } 560.35/148.47 Weak Trs: 560.35/148.47 { !EQ(S(x), S(y)) -> !EQ(x, y) 560.35/148.47 , !EQ(S(x), 0()) -> False() 560.35/148.47 , !EQ(0(), S(y)) -> False() 560.35/148.47 , !EQ(0(), 0()) -> True() 560.35/148.47 , eqNatList(Nil(), Nil()) -> True() 560.35/148.47 , eqNatList(Nil(), Cons(y, ys)) -> False() 560.35/148.47 , eqNatList(Cons(x, xs), Nil()) -> False() 560.35/148.47 , eqNatList(Cons(x, xs), Cons(y, ys)) -> 560.35/148.47 eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) } 560.35/148.47 Obligation: 560.35/148.47 innermost runtime complexity 560.35/148.47 Answer: 560.35/148.47 YES(O(1),O(1)) 560.35/148.47 560.35/148.47 The following weak DPs constitute a sub-graph of the DG that is 560.35/148.47 closed under successors. The DPs are removed. 560.35/148.47 560.35/148.47 { nolexicord^#(Cons(x, xs), b1, a2, b2, a3, b3) -> 560.35/148.47 c_3(nolexicord[Ite][False][Ite]^#(eqNatList(Cons(x, xs), b1), 560.35/148.47 Cons(x, xs), 560.35/148.47 b1, 560.35/148.47 a2, 560.35/148.47 b2, 560.35/148.47 a3, 560.35/148.47 b3)) 560.35/148.47 , nolexicord[Ite][False][Ite]^#(True(), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x, xs), 560.35/148.47 Cons(x', xs')) 560.35/148.47 -> c_9(nolexicord^#(xs', xs', xs', xs', xs', xs)) 560.35/148.47 , nolexicord[Ite][False][Ite]^#(False(), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x', xs'), 560.35/148.47 Cons(x, xs)) 560.35/148.47 -> c_10(nolexicord^#(xs', xs', xs', xs', xs', xs)) } 560.35/148.47 560.35/148.47 We are left with following problem, upon which TcT provides the 560.35/148.47 certificate YES(O(1),O(1)). 560.35/148.47 560.35/148.47 Weak Trs: 560.35/148.47 { !EQ(S(x), S(y)) -> !EQ(x, y) 560.35/148.47 , !EQ(S(x), 0()) -> False() 560.35/148.47 , !EQ(0(), S(y)) -> False() 560.35/148.47 , !EQ(0(), 0()) -> True() 560.35/148.47 , eqNatList(Nil(), Nil()) -> True() 560.35/148.47 , eqNatList(Nil(), Cons(y, ys)) -> False() 560.35/148.47 , eqNatList(Cons(x, xs), Nil()) -> False() 560.35/148.47 , eqNatList(Cons(x, xs), Cons(y, ys)) -> 560.35/148.47 eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) } 560.35/148.47 Obligation: 560.35/148.47 innermost runtime complexity 560.35/148.47 Answer: 560.35/148.47 YES(O(1),O(1)) 560.35/148.47 560.35/148.47 No rule is usable, rules are removed from the input problem. 560.35/148.47 560.35/148.47 We are left with following problem, upon which TcT provides the 560.35/148.47 certificate YES(O(1),O(1)). 560.35/148.47 560.35/148.47 Rules: Empty 560.35/148.47 Obligation: 560.35/148.47 innermost runtime complexity 560.35/148.47 Answer: 560.35/148.47 YES(O(1),O(1)) 560.35/148.47 560.35/148.47 Empty rules are trivially bounded 560.35/148.47 560.35/148.47 Hurray, we answered YES(O(1),O(n^1)) 560.67/148.68 EOF