27.68/7.95 YES 27.68/7.95 27.68/7.95 Problem: 27.68/7.95 lte(0(), n) -> true() 27.68/7.95 lte(s(m), 0()) -> false() 27.68/7.95 lte(s(m), s(n)) -> lte(m, n) 27.68/7.95 insert(nil(), m) -> cons(m, nil()) 27.68/7.95 insert(cons(n, l), m) -> cons(m, cons(n, l)) <= lte(m, n) = true() 27.68/7.95 insert(cons(n, l), m) -> cons(n, insert(l, m)) <= lte(m, n) = false() 27.68/7.95 ordered(nil()) -> true() 27.68/7.95 ordered(cons(m, nil())) -> true() 27.68/7.95 ordered(cons(m, cons(n, l))) -> ordered(cons(n, l)) <= lte(m, n) = true() 27.68/7.95 ordered(cons(m, cons(n, l))) -> false() <= lte(m, n) = false() 27.68/7.95 27.68/7.95 Proof: 27.68/7.95 This system is confluent. 27.68/7.95 By \cite{ALS94}, Theorem 4.1. 27.68/7.95 This system is of type 3 or smaller. 27.68/7.95 This system is strongly deterministic. 27.68/7.95 All 4 critical pairs are joinable. 27.68/7.95 CP: cons(x', cons(y', z')) = cons(y', insert(z', x')) <= lte(x', y') = false(), lte(x', y') = true(): 27.68/7.95 This critical pair is unfeasible. 27.68/7.95 CP: cons(x', insert(y', z')) = cons(z', cons(x', y')) <= lte(z', x') = true(), lte(z', x') = false(): 27.68/7.95 This critical pair is unfeasible. 27.68/7.95 CP: ordered(cons(x', y')) = false() <= lte(z', x') = false(), lte(z', x') = true(): 27.68/7.95 This critical pair is unfeasible. 27.68/7.95 CP: false() = ordered(cons(x', y')) <= lte(z', x') = true(), lte(z', x') = false(): 27.68/7.95 This critical pair is unfeasible. 27.68/7.95 This system is quasi-decreasing. 27.68/7.95 By \cite{O02}, p. 214, Proposition 7.2.50. 27.68/7.95 This system is of type 3 or smaller. 27.68/7.95 This system is deterministic. 27.68/7.95 System R transformed to U(R). 27.68/7.95 This system is terminating. 27.68/7.95 Call external tool: 27.68/7.95 ./ttt2.sh 27.68/7.95 Input: 27.68/7.95 lte(0(), n) -> true() 27.68/7.95 lte(s(m), 0()) -> false() 27.68/7.95 lte(s(m), s(n)) -> lte(m, n) 27.68/7.95 insert(nil(), m) -> cons(m, nil()) 27.68/7.95 ?1(true(), n, l, m) -> cons(m, cons(n, l)) 27.68/7.95 insert(cons(n, l), m) -> ?1(lte(m, n), n, l, m) 27.68/7.95 ?2(false(), n, l, m) -> cons(n, insert(l, m)) 27.68/7.95 insert(cons(n, l), m) -> ?2(lte(m, n), n, l, m) 27.68/7.95 ordered(nil()) -> true() 27.68/7.95 ordered(cons(m, nil())) -> true() 27.68/7.95 ?4(true(), m, n, l) -> ordered(cons(n, l)) 27.68/7.95 ordered(cons(m, cons(n, l))) -> ?4(lte(m, n), m, n, l) 27.68/7.95 ?3(false(), m, n, l) -> false() 27.68/7.95 ordered(cons(m, cons(n, l))) -> ?3(lte(m, n), m, n, l) 27.68/7.95 27.68/7.95 DP Processor: 27.68/7.95 DPs: 27.68/7.95 lte#(s(m),s(n)) -> lte#(m,n) 27.68/7.95 insert#(cons(n,l),m) -> lte#(m,n) 27.68/7.95 insert#(cons(n,l),m) -> ?1#(lte(m,n),n,l,m) 27.68/7.95 ?2#(false(),n,l,m) -> insert#(l,m) 27.68/7.95 insert#(cons(n,l),m) -> ?2#(lte(m,n),n,l,m) 27.68/7.95 ?4#(true(),m,n,l) -> ordered#(cons(n,l)) 27.68/7.95 ordered#(cons(m,cons(n,l))) -> lte#(m,n) 27.68/7.95 ordered#(cons(m,cons(n,l))) -> ?4#(lte(m,n),m,n,l) 27.68/7.95 ordered#(cons(m,cons(n,l))) -> ?3#(lte(m,n),m,n,l) 27.68/7.95 TRS: 27.68/7.95 lte(0(),n) -> true() 27.68/7.95 lte(s(m),0()) -> false() 27.68/7.95 lte(s(m),s(n)) -> lte(m,n) 27.68/7.95 insert(nil(),m) -> cons(m,nil()) 27.68/7.95 ?1(true(),n,l,m) -> cons(m,cons(n,l)) 27.68/7.95 insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m) 27.68/7.95 ?2(false(),n,l,m) -> cons(n,insert(l,m)) 27.68/7.95 insert(cons(n,l),m) -> ?2(lte(m,n),n,l,m) 27.68/7.95 ordered(nil()) -> true() 27.68/7.95 ordered(cons(m,nil())) -> true() 27.68/7.95 ?4(true(),m,n,l) -> ordered(cons(n,l)) 27.68/7.95 ordered(cons(m,cons(n,l))) -> ?4(lte(m,n),m,n,l) 27.68/7.95 ?3(false(),m,n,l) -> false() 27.68/7.95 ordered(cons(m,cons(n,l))) -> ?3(lte(m,n),m,n,l) 27.68/7.95 TDG Processor: 27.68/7.95 DPs: 27.68/7.95 lte#(s(m),s(n)) -> lte#(m,n) 27.68/7.95 insert#(cons(n,l),m) -> lte#(m,n) 27.68/7.95 insert#(cons(n,l),m) -> ?1#(lte(m,n),n,l,m) 27.68/7.95 ?2#(false(),n,l,m) -> insert#(l,m) 27.68/7.96 insert#(cons(n,l),m) -> ?2#(lte(m,n),n,l,m) 27.68/7.96 ?4#(true(),m,n,l) -> ordered#(cons(n,l)) 27.68/7.96 ordered#(cons(m,cons(n,l))) -> lte#(m,n) 27.68/7.96 ordered#(cons(m,cons(n,l))) -> ?4#(lte(m,n),m,n,l) 27.68/7.96 ordered#(cons(m,cons(n,l))) -> ?3#(lte(m,n),m,n,l) 27.68/7.96 TRS: 27.68/7.96 lte(0(),n) -> true() 27.68/7.96 lte(s(m),0()) -> false() 27.68/7.96 lte(s(m),s(n)) -> lte(m,n) 27.68/7.96 insert(nil(),m) -> cons(m,nil()) 27.68/7.96 ?1(true(),n,l,m) -> cons(m,cons(n,l)) 27.68/7.96 insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m) 27.68/7.96 ?2(false(),n,l,m) -> cons(n,insert(l,m)) 27.68/7.96 insert(cons(n,l),m) -> ?2(lte(m,n),n,l,m) 27.68/7.96 ordered(nil()) -> true() 27.68/7.96 ordered(cons(m,nil())) -> true() 27.68/7.96 ?4(true(),m,n,l) -> ordered(cons(n,l)) 27.68/7.96 ordered(cons(m,cons(n,l))) -> ?4(lte(m,n),m,n,l) 27.68/7.96 ?3(false(),m,n,l) -> false() 27.68/7.96 ordered(cons(m,cons(n,l))) -> ?3(lte(m,n),m,n,l) 27.68/7.96 graph: 27.68/7.96 ?4#(true(),m,n,l) -> ordered#(cons(n,l)) -> 27.68/7.96 ordered#(cons(m,cons(n,l))) -> ?3#(lte(m,n),m,n,l) 27.68/7.96 ?4#(true(),m,n,l) -> ordered#(cons(n,l)) -> 27.68/7.96 ordered#(cons(m,cons(n,l))) -> ?4#(lte(m,n),m,n,l) 27.68/7.96 ?4#(true(),m,n,l) -> ordered#(cons(n,l)) -> 27.68/7.96 ordered#(cons(m,cons(n,l))) -> lte#(m,n) 27.68/7.96 ordered#(cons(m,cons(n,l))) -> ?4#(lte(m,n),m,n,l) -> 27.68/7.96 ?4#(true(),m,n,l) -> ordered#(cons(n,l)) 27.68/7.96 ordered#(cons(m,cons(n,l))) -> lte#(m,n) -> 27.68/7.96 lte#(s(m),s(n)) -> lte#(m,n) 27.68/7.96 ?2#(false(),n,l,m) -> insert#(l,m) -> 27.68/7.96 insert#(cons(n,l),m) -> ?2#(lte(m,n),n,l,m) 27.68/7.96 ?2#(false(),n,l,m) -> insert#(l,m) -> 27.68/7.96 insert#(cons(n,l),m) -> ?1#(lte(m,n),n,l,m) 27.68/7.96 ?2#(false(),n,l,m) -> insert#(l,m) -> 27.68/7.96 insert#(cons(n,l),m) -> lte#(m,n) 27.68/7.96 insert#(cons(n,l),m) -> ?2#(lte(m,n),n,l,m) -> 27.68/7.96 ?2#(false(),n,l,m) -> insert#(l,m) 27.68/7.96 insert#(cons(n,l),m) -> lte#(m,n) -> lte#(s(m),s(n)) -> lte#(m,n) 27.68/7.96 lte#(s(m),s(n)) -> lte#(m,n) -> lte#(s(m),s(n)) -> lte#(m,n) 27.68/7.96 SCC Processor: 27.68/7.96 #sccs: 3 27.68/7.96 #rules: 5 27.68/7.96 #arcs: 11/81 27.68/7.96 DPs: 27.68/7.96 ?2#(false(),n,l,m) -> insert#(l,m) 27.68/7.96 insert#(cons(n,l),m) -> ?2#(lte(m,n),n,l,m) 27.68/7.96 TRS: 27.68/7.96 lte(0(),n) -> true() 27.68/7.96 lte(s(m),0()) -> false() 27.68/7.96 lte(s(m),s(n)) -> lte(m,n) 27.68/7.96 insert(nil(),m) -> cons(m,nil()) 27.68/7.96 ?1(true(),n,l,m) -> cons(m,cons(n,l)) 27.68/7.96 insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m) 27.68/7.96 ?2(false(),n,l,m) -> cons(n,insert(l,m)) 27.68/7.96 insert(cons(n,l),m) -> ?2(lte(m,n),n,l,m) 27.68/7.96 ordered(nil()) -> true() 27.68/7.96 ordered(cons(m,nil())) -> true() 27.68/7.96 ?4(true(),m,n,l) -> ordered(cons(n,l)) 27.68/7.96 ordered(cons(m,cons(n,l))) -> ?4(lte(m,n),m,n,l) 27.68/7.96 ?3(false(),m,n,l) -> false() 27.68/7.96 ordered(cons(m,cons(n,l))) -> ?3(lte(m,n),m,n,l) 27.68/7.96 Subterm Criterion Processor: 27.68/7.96 simple projection: 27.68/7.96 pi(insert#) = 0 27.68/7.96 pi(?2#) = 2 27.68/7.96 problem: 27.68/7.96 DPs: 27.68/7.96 ?2#(false(),n,l,m) -> insert#(l,m) 27.68/7.96 TRS: 27.68/7.96 lte(0(),n) -> true() 27.68/7.96 lte(s(m),0()) -> false() 27.68/7.96 lte(s(m),s(n)) -> lte(m,n) 27.68/7.96 insert(nil(),m) -> cons(m,nil()) 27.68/7.96 ?1(true(),n,l,m) -> cons(m,cons(n,l)) 27.68/7.96 insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m) 27.68/7.96 ?2(false(),n,l,m) -> cons(n,insert(l,m)) 27.68/7.96 insert(cons(n,l),m) -> ?2(lte(m,n),n,l,m) 27.68/7.96 ordered(nil()) -> true() 27.68/7.96 ordered(cons(m,nil())) -> true() 27.68/7.96 ?4(true(),m,n,l) -> ordered(cons(n,l)) 27.68/7.96 ordered(cons(m,cons(n,l))) -> ?4(lte(m,n),m,n,l) 27.68/7.96 ?3(false(),m,n,l) -> false() 27.68/7.96 ordered(cons(m,cons(n,l))) -> ?3(lte(m,n),m,n,l) 27.68/7.96 SCC Processor: 27.68/7.96 #sccs: 0 27.68/7.96 #rules: 0 27.68/7.96 #arcs: 2/1 27.68/7.96 27.68/7.96 27.68/7.96 DPs: 27.68/7.96 ?4#(true(),m,n,l) -> ordered#(cons(n,l)) 27.68/7.96 ordered#(cons(m,cons(n,l))) -> ?4#(lte(m,n),m,n,l) 27.68/7.96 TRS: 27.68/7.96 lte(0(),n) -> true() 27.68/7.96 lte(s(m),0()) -> false() 27.68/7.96 lte(s(m),s(n)) -> lte(m,n) 27.68/7.96 insert(nil(),m) -> cons(m,nil()) 27.68/7.96 ?1(true(),n,l,m) -> cons(m,cons(n,l)) 27.68/7.96 insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m) 27.68/7.96 ?2(false(),n,l,m) -> cons(n,insert(l,m)) 27.68/7.96 insert(cons(n,l),m) -> ?2(lte(m,n),n,l,m) 27.68/7.96 ordered(nil()) -> true() 27.68/7.96 ordered(cons(m,nil())) -> true() 27.68/7.96 ?4(true(),m,n,l) -> ordered(cons(n,l)) 27.68/7.96 ordered(cons(m,cons(n,l))) -> ?4(lte(m,n),m,n,l) 27.68/7.96 ?3(false(),m,n,l) -> false() 27.68/7.96 ordered(cons(m,cons(n,l))) -> ?3(lte(m,n),m,n,l) 27.68/7.96 Usable Rule Processor: 27.68/7.96 DPs: 27.68/7.96 ?4#(true(),m,n,l) -> ordered#(cons(n,l)) 27.68/7.96 ordered#(cons(m,cons(n,l))) -> ?4#(lte(m,n),m,n,l) 27.68/7.96 TRS: 27.68/7.96 lte(0(),n) -> true() 27.68/7.96 lte(s(m),0()) -> false() 27.68/7.96 lte(s(m),s(n)) -> lte(m,n) 27.68/7.96 Arctic Interpretation Processor: 29.30/8.12 dimension: 1 29.30/8.12 usable rules: 29.30/8.12 lte(0(),n) -> true() 29.30/8.12 lte(s(m),0()) -> false() 29.30/8.12 lte(s(m),s(n)) -> lte(m,n) 29.30/8.12 interpretation: 29.30/8.12 [?4#](x0, x1, x2, x3) = x0 + -1x1 + 4x2 + 2x3 + -16, 29.30/8.12 29.30/8.12 [ordered#](x0) = x0 + -16, 29.30/8.12 29.30/8.12 [cons](x0, x1) = 3x0 + 1x1 + -1, 29.30/8.12 29.30/8.12 [false] = 0, 29.30/8.12 29.30/8.12 [s](x0) = 4x0, 29.30/8.12 29.30/8.12 [true] = 0, 29.30/8.12 29.30/8.12 [lte](x0, x1) = x0 + -4x1 + 0, 29.30/8.12 29.30/8.12 [0] = 1 29.30/8.12 orientation: 29.30/8.12 ?4#(true(),m,n,l) = 2l + -1m + 4n + 0 >= 1l + 3n + -1 = ordered#(cons(n,l)) 29.30/8.12 29.30/8.12 ordered#(cons(m,cons(n,l))) = 2l + 3m + 4n + 0 >= 2l + m + 4n + 0 = ?4#(lte(m,n),m,n,l) 29.30/8.12 29.30/8.12 lte(0(),n) = -4n + 1 >= 0 = true() 29.30/8.12 29.30/8.12 lte(s(m),0()) = 4m + 0 >= 0 = false() 29.30/8.12 29.30/8.12 lte(s(m),s(n)) = 4m + n + 0 >= m + -4n + 0 = lte(m,n) 29.30/8.12 problem: 29.30/8.12 DPs: 29.30/8.12 ordered#(cons(m,cons(n,l))) -> ?4#(lte(m,n),m,n,l) 29.30/8.12 TRS: 29.30/8.12 lte(0(),n) -> true() 29.30/8.12 lte(s(m),0()) -> false() 29.30/8.12 lte(s(m),s(n)) -> lte(m,n) 29.30/8.12 Restore Modifier: 29.30/8.12 DPs: 29.30/8.12 ordered#(cons(m,cons(n,l))) -> ?4#(lte(m,n),m,n,l) 29.30/8.12 TRS: 29.30/8.12 lte(0(),n) -> true() 29.30/8.12 lte(s(m),0()) -> false() 29.30/8.12 lte(s(m),s(n)) -> lte(m,n) 29.30/8.12 insert(nil(),m) -> cons(m,nil()) 29.30/8.12 ?1(true(),n,l,m) -> cons(m,cons(n,l)) 29.30/8.12 insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m) 29.30/8.12 ?2(false(),n,l,m) -> cons(n,insert(l,m)) 29.30/8.12 insert(cons(n,l),m) -> ?2(lte(m,n),n,l,m) 29.30/8.12 ordered(nil()) -> true() 29.30/8.12 ordered(cons(m,nil())) -> true() 29.30/8.12 ?4(true(),m,n,l) -> ordered(cons(n,l)) 29.30/8.12 ordered(cons(m,cons(n,l))) -> ?4(lte(m,n),m,n,l) 29.30/8.12 ?3(false(),m,n,l) -> false() 29.30/8.12 ordered(cons(m,cons(n,l))) -> ?3(lte(m,n),m,n,l) 29.30/8.12 SCC Processor: 29.30/8.12 #sccs: 0 29.30/8.12 #rules: 0 29.30/8.12 #arcs: 2/1 29.30/8.12 29.30/8.12 29.30/8.12 DPs: 29.30/8.12 lte#(s(m),s(n)) -> lte#(m,n) 29.30/8.12 TRS: 29.30/8.12 lte(0(),n) -> true() 29.30/8.12 lte(s(m),0()) -> false() 29.30/8.12 lte(s(m),s(n)) -> lte(m,n) 29.30/8.12 insert(nil(),m) -> cons(m,nil()) 29.30/8.12 ?1(true(),n,l,m) -> cons(m,cons(n,l)) 29.30/8.12 insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m) 29.30/8.12 ?2(false(),n,l,m) -> cons(n,insert(l,m)) 29.30/8.12 insert(cons(n,l),m) -> ?2(lte(m,n),n,l,m) 29.30/8.12 ordered(nil()) -> true() 29.30/8.12 ordered(cons(m,nil())) -> true() 29.30/8.12 ?4(true(),m,n,l) -> ordered(cons(n,l)) 29.30/8.12 ordered(cons(m,cons(n,l))) -> ?4(lte(m,n),m,n,l) 29.30/8.12 ?3(false(),m,n,l) -> false() 29.30/8.12 ordered(cons(m,cons(n,l))) -> ?3(lte(m,n),m,n,l) 29.30/8.12 Subterm Criterion Processor: 29.30/8.12 simple projection: 29.30/8.12 pi(lte#) = 0 29.30/8.12 problem: 29.30/8.12 DPs: 29.30/8.12 29.30/8.12 TRS: 29.30/8.12 lte(0(),n) -> true() 29.30/8.12 lte(s(m),0()) -> false() 29.30/8.12 lte(s(m),s(n)) -> lte(m,n) 29.30/8.12 insert(nil(),m) -> cons(m,nil()) 29.30/8.12 ?1(true(),n,l,m) -> cons(m,cons(n,l)) 29.30/8.12 insert(cons(n,l),m) -> ?1(lte(m,n),n,l,m) 29.30/8.12 ?2(false(),n,l,m) -> cons(n,insert(l,m)) 29.30/8.12 insert(cons(n,l),m) -> ?2(lte(m,n),n,l,m) 29.30/8.12 ordered(nil()) -> true() 29.30/8.12 ordered(cons(m,nil())) -> true() 29.30/8.12 ?4(true(),m,n,l) -> ordered(cons(n,l)) 29.30/8.12 ordered(cons(m,cons(n,l))) -> ?4(lte(m,n),m,n,l) 29.30/8.12 ?3(false(),m,n,l) -> false() 29.30/8.12 ordered(cons(m,cons(n,l))) -> ?3(lte(m,n),m,n,l) 29.30/8.12 Qed 29.30/8.12 29.88/8.50 EOF