18.13/5.51 YES 18.13/5.51 18.13/5.51 Problem: 18.13/5.51 lt(x, 0()) -> false() 18.13/5.51 lt(0(), s(x)) -> true() 18.13/5.51 lt(s(x), s(y)) -> lt(x, y) 18.13/5.51 m(0(), s(y)) -> 0() 18.13/5.51 m(x, 0()) -> x 18.13/5.51 m(s(x), s(y)) -> m(x, y) 18.13/5.51 div(0(), s(x)) -> pair(0(), 0()) 18.13/5.51 div(s(x), s(y)) -> pair(0(), s(x)) <= lt(x, y) = true() 18.13/5.51 div(s(x), s(y)) -> pair(s(q), r) <= lt(x, y) = false(), div(m(x, y), s(y)) = pair(q, r) 18.13/5.51 18.13/5.51 Proof: 18.13/5.51 This system is confluent. 18.13/5.51 By \cite{ALS94}, Theorem 4.1. 18.13/5.51 This system is of type 3 or smaller. 18.13/5.51 This system is strongly deterministic. 18.13/5.51 All 2 critical pairs are joinable. 18.13/5.51 CP: pair(0(), s(x)) = pair(s(y), $1) <= lt(x, $2) = false(), div(m(x, $2), s($2)) = pair(y, $1), lt(x, $2) = true(): 18.13/5.51 This critical pair is unfeasible. 18.13/5.51 CP: pair(s(x), y) = pair(0(), s($1)) <= lt($1, $2) = true(), lt($1, $2) = false(), div(m($1, $2), s($2)) = pair(x, y): 18.13/5.51 This critical pair is unfeasible. 18.13/5.51 This system is quasi-decreasing. 18.13/5.51 By \cite{O02}, p. 214, Proposition 7.2.50. 18.13/5.51 This system is of type 3 or smaller. 18.13/5.51 This system is deterministic. 18.13/5.51 System R transformed to U(R). 18.13/5.51 This system is terminating. 18.13/5.51 Call external tool: 18.13/5.51 ./ttt2.sh 18.13/5.51 Input: 18.13/5.51 lt(x, 0()) -> false() 18.13/5.51 lt(0(), s(x)) -> true() 18.13/5.51 lt(s(x), s(y)) -> lt(x, y) 18.13/5.51 m(0(), s(y)) -> 0() 18.13/5.51 m(x, 0()) -> x 18.13/5.51 m(s(x), s(y)) -> m(x, y) 18.13/5.51 div(0(), s(x)) -> pair(0(), 0()) 18.13/5.51 ?1(true(), x, y) -> pair(0(), s(x)) 18.13/5.51 div(s(x), s(y)) -> ?1(lt(x, y), x, y) 18.13/5.51 ?3(pair(q, r), x, y) -> pair(s(q), r) 18.13/5.51 ?2(false(), x, y) -> ?3(div(m(x, y), s(y)), x, y) 18.13/5.51 div(s(x), s(y)) -> ?2(lt(x, y), x, y) 18.13/5.51 18.13/5.51 DP Processor: 18.13/5.51 DPs: 18.13/5.51 lt#(s(x),s(y)) -> lt#(x,y) 18.13/5.51 m#(s(x),s(y)) -> m#(x,y) 18.13/5.51 div#(s(x),s(y)) -> lt#(x,y) 18.13/5.51 div#(s(x),s(y)) -> ?1#(lt(x,y),x,y) 18.13/5.51 ?2#(false(),x,y) -> m#(x,y) 18.13/5.51 ?2#(false(),x,y) -> div#(m(x,y),s(y)) 18.13/5.51 ?2#(false(),x,y) -> ?3#(div(m(x,y),s(y)),x,y) 18.13/5.51 div#(s(x),s(y)) -> ?2#(lt(x,y),x,y) 18.13/5.51 TRS: 18.13/5.51 lt(x,0()) -> false() 18.13/5.51 lt(0(),s(x)) -> true() 18.13/5.51 lt(s(x),s(y)) -> lt(x,y) 18.13/5.51 m(0(),s(y)) -> 0() 18.13/5.51 m(x,0()) -> x 18.13/5.51 m(s(x),s(y)) -> m(x,y) 18.13/5.51 div(0(),s(x)) -> pair(0(),0()) 18.13/5.51 ?1(true(),x,y) -> pair(0(),s(x)) 18.13/5.51 div(s(x),s(y)) -> ?1(lt(x,y),x,y) 18.13/5.51 ?3(pair(q,r),x,y) -> pair(s(q),r) 18.13/5.51 ?2(false(),x,y) -> ?3(div(m(x,y),s(y)),x,y) 18.13/5.52 div(s(x),s(y)) -> ?2(lt(x,y),x,y) 18.13/5.52 TDG Processor: 18.13/5.52 DPs: 18.13/5.52 lt#(s(x),s(y)) -> lt#(x,y) 18.50/5.54 m#(s(x),s(y)) -> m#(x,y) 18.50/5.54 div#(s(x),s(y)) -> lt#(x,y) 18.50/5.54 div#(s(x),s(y)) -> ?1#(lt(x,y),x,y) 18.50/5.54 ?2#(false(),x,y) -> m#(x,y) 18.50/5.54 ?2#(false(),x,y) -> div#(m(x,y),s(y)) 18.50/5.54 ?2#(false(),x,y) -> ?3#(div(m(x,y),s(y)),x,y) 18.50/5.54 div#(s(x),s(y)) -> ?2#(lt(x,y),x,y) 18.50/5.54 TRS: 18.50/5.54 lt(x,0()) -> false() 18.50/5.54 lt(0(),s(x)) -> true() 18.50/5.54 lt(s(x),s(y)) -> lt(x,y) 18.50/5.54 m(0(),s(y)) -> 0() 18.50/5.54 m(x,0()) -> x 18.50/5.54 m(s(x),s(y)) -> m(x,y) 18.50/5.54 div(0(),s(x)) -> pair(0(),0()) 18.50/5.54 ?1(true(),x,y) -> pair(0(),s(x)) 18.50/5.54 div(s(x),s(y)) -> ?1(lt(x,y),x,y) 18.50/5.54 ?3(pair(q,r),x,y) -> pair(s(q),r) 18.50/5.54 ?2(false(),x,y) -> ?3(div(m(x,y),s(y)),x,y) 18.50/5.54 div(s(x),s(y)) -> ?2(lt(x,y),x,y) 18.50/5.54 graph: 18.50/5.54 ?2#(false(),x,y) -> div#(m(x,y),s(y)) -> 18.50/5.54 div#(s(x),s(y)) -> ?2#(lt(x,y),x,y) 18.50/5.54 ?2#(false(),x,y) -> div#(m(x,y),s(y)) -> 18.50/5.54 div#(s(x),s(y)) -> ?1#(lt(x,y),x,y) 18.50/5.54 ?2#(false(),x,y) -> div#(m(x,y),s(y)) -> div#(s(x),s(y)) -> lt#(x,y) 18.50/5.54 ?2#(false(),x,y) -> m#(x,y) -> m#(s(x),s(y)) -> m#(x,y) 18.50/5.54 div#(s(x),s(y)) -> ?2#(lt(x,y),x,y) -> 18.50/5.54 ?2#(false(),x,y) -> ?3#(div(m(x,y),s(y)),x,y) 18.50/5.54 div#(s(x),s(y)) -> ?2#(lt(x,y),x,y) -> 18.50/5.54 ?2#(false(),x,y) -> div#(m(x,y),s(y)) 18.50/5.54 div#(s(x),s(y)) -> ?2#(lt(x,y),x,y) -> ?2#(false(),x,y) -> m#(x,y) 18.50/5.54 div#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y) 18.50/5.54 m#(s(x),s(y)) -> m#(x,y) -> m#(s(x),s(y)) -> m#(x,y) 18.50/5.54 lt#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y) 18.50/5.54 SCC Processor: 18.50/5.54 #sccs: 3 18.50/5.54 #rules: 4 18.50/5.54 #arcs: 10/64 18.50/5.54 DPs: 18.50/5.54 ?2#(false(),x,y) -> div#(m(x,y),s(y)) 18.50/5.54 div#(s(x),s(y)) -> ?2#(lt(x,y),x,y) 18.50/5.54 TRS: 18.50/5.54 lt(x,0()) -> false() 18.50/5.54 lt(0(),s(x)) -> true() 18.50/5.54 lt(s(x),s(y)) -> lt(x,y) 18.50/5.54 m(0(),s(y)) -> 0() 18.50/5.54 m(x,0()) -> x 18.50/5.54 m(s(x),s(y)) -> m(x,y) 18.50/5.54 div(0(),s(x)) -> pair(0(),0()) 18.50/5.54 ?1(true(),x,y) -> pair(0(),s(x)) 18.50/5.54 div(s(x),s(y)) -> ?1(lt(x,y),x,y) 18.50/5.54 ?3(pair(q,r),x,y) -> pair(s(q),r) 18.50/5.54 ?2(false(),x,y) -> ?3(div(m(x,y),s(y)),x,y) 18.50/5.54 div(s(x),s(y)) -> ?2(lt(x,y),x,y) 18.50/5.54 Usable Rule Processor: 18.50/5.54 DPs: 18.50/5.54 ?2#(false(),x,y) -> div#(m(x,y),s(y)) 18.50/5.54 div#(s(x),s(y)) -> ?2#(lt(x,y),x,y) 18.50/5.54 TRS: 18.50/5.54 m(0(),s(y)) -> 0() 18.50/5.54 m(x,0()) -> x 18.50/5.54 m(s(x),s(y)) -> m(x,y) 18.50/5.54 lt(x,0()) -> false() 18.50/5.54 lt(0(),s(x)) -> true() 18.50/5.54 lt(s(x),s(y)) -> lt(x,y) 18.50/5.54 Arctic Interpretation Processor: 18.50/5.54 dimension: 1 18.50/5.54 usable rules: 18.50/5.54 m(0(),s(y)) -> 0() 18.50/5.54 m(x,0()) -> x 18.50/5.54 m(s(x),s(y)) -> m(x,y) 18.50/5.54 lt(x,0()) -> false() 18.50/5.54 lt(0(),s(x)) -> true() 18.50/5.54 lt(s(x),s(y)) -> lt(x,y) 18.50/5.54 interpretation: 18.50/5.54 [?2#](x0, x1, x2) = x0 + 3x1 + 0, 18.50/5.54 18.50/5.54 [div#](x0, x1) = x0 + 0, 18.50/5.54 18.50/5.54 [m](x0, x1) = x0 + 0, 18.50/5.54 18.50/5.54 [true] = 4, 18.50/5.54 18.50/5.54 [s](x0) = 4x0 + 2, 18.50/5.54 18.50/5.54 [false] = 1, 18.50/5.54 18.50/5.54 [lt](x0, x1) = 1x0 + 2, 18.50/5.54 18.50/5.54 [0] = 3 18.50/5.54 orientation: 18.50/5.54 ?2#(false(),x,y) = 3x + 1 >= x + 0 = div#(m(x,y),s(y)) 18.50/5.54 18.50/5.54 div#(s(x),s(y)) = 4x + 2 >= 3x + 2 = ?2#(lt(x,y),x,y) 18.50/5.54 18.50/5.54 m(0(),s(y)) = 3 >= 3 = 0() 18.50/5.54 18.50/5.54 m(x,0()) = x + 0 >= x = x 18.50/5.54 18.50/5.54 m(s(x),s(y)) = 4x + 2 >= x + 0 = m(x,y) 18.50/5.54 18.50/5.54 lt(x,0()) = 1x + 2 >= 1 = false() 18.50/5.54 18.50/5.54 lt(0(),s(x)) = 4 >= 4 = true() 18.50/5.54 18.50/5.54 lt(s(x),s(y)) = 5x + 3 >= 1x + 2 = lt(x,y) 18.50/5.64 problem: 18.50/5.64 DPs: 18.50/5.64 div#(s(x),s(y)) -> ?2#(lt(x,y),x,y) 18.50/5.64 TRS: 18.50/5.64 m(0(),s(y)) -> 0() 18.50/5.64 m(x,0()) -> x 18.50/5.64 m(s(x),s(y)) -> m(x,y) 18.50/5.64 lt(x,0()) -> false() 18.50/5.64 lt(0(),s(x)) -> true() 18.50/5.64 lt(s(x),s(y)) -> lt(x,y) 18.50/5.64 Restore Modifier: 18.50/5.64 DPs: 18.50/5.64 div#(s(x),s(y)) -> ?2#(lt(x,y),x,y) 18.50/5.64 TRS: 18.50/5.64 lt(x,0()) -> false() 18.50/5.64 lt(0(),s(x)) -> true() 18.50/5.64 lt(s(x),s(y)) -> lt(x,y) 18.50/5.64 m(0(),s(y)) -> 0() 18.50/5.64 m(x,0()) -> x 18.50/5.64 m(s(x),s(y)) -> m(x,y) 18.50/5.64 div(0(),s(x)) -> pair(0(),0()) 18.50/5.64 ?1(true(),x,y) -> pair(0(),s(x)) 18.50/5.64 div(s(x),s(y)) -> ?1(lt(x,y),x,y) 18.50/5.64 ?3(pair(q,r),x,y) -> pair(s(q),r) 18.50/5.64 ?2(false(),x,y) -> ?3(div(m(x,y),s(y)),x,y) 18.50/5.64 div(s(x),s(y)) -> ?2(lt(x,y),x,y) 18.50/5.64 SCC Processor: 18.50/5.64 #sccs: 0 18.50/5.64 #rules: 0 18.50/5.64 #arcs: 2/1 18.50/5.64 18.50/5.64 18.50/5.64 DPs: 18.50/5.64 m#(s(x),s(y)) -> m#(x,y) 18.50/5.64 TRS: 18.50/5.64 lt(x,0()) -> false() 18.50/5.64 lt(0(),s(x)) -> true() 18.50/5.64 lt(s(x),s(y)) -> lt(x,y) 18.50/5.64 m(0(),s(y)) -> 0() 18.50/5.64 m(x,0()) -> x 18.50/5.64 m(s(x),s(y)) -> m(x,y) 18.50/5.64 div(0(),s(x)) -> pair(0(),0()) 18.50/5.64 ?1(true(),x,y) -> pair(0(),s(x)) 18.50/5.64 div(s(x),s(y)) -> ?1(lt(x,y),x,y) 18.50/5.64 ?3(pair(q,r),x,y) -> pair(s(q),r) 18.50/5.64 ?2(false(),x,y) -> ?3(div(m(x,y),s(y)),x,y) 18.50/5.64 div(s(x),s(y)) -> ?2(lt(x,y),x,y) 18.50/5.64 Subterm Criterion Processor: 18.50/5.64 simple projection: 19.44/5.70 pi(m#) = 0 19.44/5.70 problem: 19.44/5.70 DPs: 19.44/5.70 19.44/5.70 TRS: 19.44/5.70 lt(x,0()) -> false() 19.44/5.70 lt(0(),s(x)) -> true() 19.44/5.70 lt(s(x),s(y)) -> lt(x,y) 19.44/5.70 m(0(),s(y)) -> 0() 19.44/5.70 m(x,0()) -> x 19.44/5.70 m(s(x),s(y)) -> m(x,y) 19.44/5.70 div(0(),s(x)) -> pair(0(),0()) 19.44/5.70 ?1(true(),x,y) -> pair(0(),s(x)) 19.44/5.70 div(s(x),s(y)) -> ?1(lt(x,y),x,y) 19.44/5.70 ?3(pair(q,r),x,y) -> pair(s(q),r) 19.44/5.70 ?2(false(),x,y) -> ?3(div(m(x,y),s(y)),x,y) 19.44/5.70 div(s(x),s(y)) -> ?2(lt(x,y),x,y) 19.44/5.70 Qed 19.44/5.70 19.44/5.70 DPs: 19.44/5.70 lt#(s(x),s(y)) -> lt#(x,y) 19.44/5.70 TRS: 19.44/5.70 lt(x,0()) -> false() 19.44/5.70 lt(0(),s(x)) -> true() 19.44/5.70 lt(s(x),s(y)) -> lt(x,y) 19.44/5.70 m(0(),s(y)) -> 0() 19.44/5.70 m(x,0()) -> x 19.44/5.70 m(s(x),s(y)) -> m(x,y) 19.44/5.70 div(0(),s(x)) -> pair(0(),0()) 19.44/5.70 ?1(true(),x,y) -> pair(0(),s(x)) 19.44/5.70 div(s(x),s(y)) -> ?1(lt(x,y),x,y) 19.44/5.70 ?3(pair(q,r),x,y) -> pair(s(q),r) 19.44/5.70 ?2(false(),x,y) -> ?3(div(m(x,y),s(y)),x,y) 19.44/5.70 div(s(x),s(y)) -> ?2(lt(x,y),x,y) 19.44/5.70 Subterm Criterion Processor: 19.44/5.70 simple projection: 19.44/5.70 pi(lt#) = 0 19.44/5.70 problem: 19.44/5.70 DPs: 19.44/5.70 19.44/5.70 TRS: 19.44/5.70 lt(x,0()) -> false() 19.44/5.70 lt(0(),s(x)) -> true() 19.44/5.70 lt(s(x),s(y)) -> lt(x,y) 19.44/5.70 m(0(),s(y)) -> 0() 19.44/5.70 m(x,0()) -> x 19.44/5.70 m(s(x),s(y)) -> m(x,y) 19.44/5.70 div(0(),s(x)) -> pair(0(),0()) 19.44/5.70 ?1(true(),x,y) -> pair(0(),s(x)) 19.44/5.70 div(s(x),s(y)) -> ?1(lt(x,y),x,y) 19.44/5.70 ?3(pair(q,r),x,y) -> pair(s(q),r) 19.44/5.70 ?2(false(),x,y) -> ?3(div(m(x,y),s(y)),x,y) 19.44/5.70 div(s(x),s(y)) -> ?2(lt(x,y),x,y) 19.44/5.70 Qed 19.44/5.70 21.63/6.20 EOF