10.19/3.51	YES
10.19/3.51	
10.19/3.51	Proof:
10.19/3.51	This system is confluent.
10.19/3.51	By \cite{ALS94}, Theorem 4.1.
10.19/3.51	This system is of type 3 or smaller.
10.19/3.51	This system is strongly deterministic.
10.19/3.51	This system is quasi-decreasing.
10.19/3.51	By \cite{O02}, p. 214, Proposition 7.2.50.
10.19/3.51	This system is of type 3 or smaller.
10.19/3.51	This system is deterministic.
10.19/3.51	System R transformed to optimized U(R).
10.19/3.51	This system is terminating.
10.19/3.51	Call external tool:
10.19/3.51	./ttt2.sh
10.19/3.51	Input:
10.19/3.51	(VAR x y q r)
10.19/3.51	(RULES
10.19/3.51	  m(x, 0) -> x
10.19/3.51	  m(s(x), s(y)) -> m(x, y)
10.19/3.51	  lt(x, 0) -> false
10.19/3.51	  div(0, s(x)) -> pair(0, 0)
10.19/3.51	  div(s(x), s(y)) -> ?1(lt(x, y), x, y)
10.19/3.51	  ?1(false, x, y) -> ?2(div(m(x, y), s(y)), x, y)
10.19/3.51	  ?2(pair(q, r), x, y) -> pair(s(q), r)
10.19/3.51	  lt(s(x), s(y)) -> lt(x, y)
10.19/3.51	  div(s(x), s(y)) -> ?1(lt(x, y), x, y)
10.19/3.51	  ?1(true, x, y) -> pair(0, s(x))
10.19/3.51	  lt(0, s(x)) -> true
10.19/3.51	  m(0, s(y)) -> 0
10.19/3.51	)
10.19/3.51	
10.19/3.51	 DP Processor:
10.19/3.51	  DPs:
10.19/3.51	   m#(s(x),s(y)) -> m#(x,y)
10.19/3.51	   div#(s(x),s(y)) -> lt#(x,y)
10.19/3.51	   div#(s(x),s(y)) -> ?1#(lt(x,y),x,y)
10.19/3.51	   ?1#(false(),x,y) -> m#(x,y)
10.19/3.51	   ?1#(false(),x,y) -> div#(m(x,y),s(y))
10.19/3.51	   ?1#(false(),x,y) -> ?2#(div(m(x,y),s(y)),x,y)
10.19/3.51	   lt#(s(x),s(y)) -> lt#(x,y)
10.19/3.51	  TRS:
10.19/3.51	   m(x,0()) -> x
10.19/3.51	   m(s(x),s(y)) -> m(x,y)
10.19/3.51	   lt(x,0()) -> false()
10.19/3.51	   div(0(),s(x)) -> pair(0(),0())
10.19/3.51	   div(s(x),s(y)) -> ?1(lt(x,y),x,y)
10.19/3.51	   ?1(false(),x,y) -> ?2(div(m(x,y),s(y)),x,y)
10.19/3.51	   ?2(pair(q,r),x,y) -> pair(s(q),r)
10.19/3.51	   lt(s(x),s(y)) -> lt(x,y)
10.19/3.51	   ?1(true(),x,y) -> pair(0(),s(x))
10.19/3.51	   lt(0(),s(x)) -> true()
10.19/3.51	   m(0(),s(y)) -> 0()
10.19/3.51	  TDG Processor:
10.19/3.51	   DPs:
10.19/3.51	    m#(s(x),s(y)) -> m#(x,y)
10.19/3.51	    div#(s(x),s(y)) -> lt#(x,y)
10.19/3.51	    div#(s(x),s(y)) -> ?1#(lt(x,y),x,y)
10.19/3.51	    ?1#(false(),x,y) -> m#(x,y)
10.19/3.51	    ?1#(false(),x,y) -> div#(m(x,y),s(y))
10.19/3.51	    ?1#(false(),x,y) -> ?2#(div(m(x,y),s(y)),x,y)
10.19/3.51	    lt#(s(x),s(y)) -> lt#(x,y)
10.19/3.51	   TRS:
10.19/3.51	    m(x,0()) -> x
10.19/3.51	    m(s(x),s(y)) -> m(x,y)
10.19/3.51	    lt(x,0()) -> false()
10.19/3.51	    div(0(),s(x)) -> pair(0(),0())
10.19/3.51	    div(s(x),s(y)) -> ?1(lt(x,y),x,y)
10.19/3.51	    ?1(false(),x,y) -> ?2(div(m(x,y),s(y)),x,y)
10.19/3.51	    ?2(pair(q,r),x,y) -> pair(s(q),r)
10.19/3.51	    lt(s(x),s(y)) -> lt(x,y)
10.19/3.51	    ?1(true(),x,y) -> pair(0(),s(x))
10.19/3.51	    lt(0(),s(x)) -> true()
10.19/3.51	    m(0(),s(y)) -> 0()
10.19/3.51	   graph:
10.19/3.51	    ?1#(false(),x,y) -> div#(m(x,y),s(y)) ->
10.19/3.51	    div#(s(x),s(y)) -> ?1#(lt(x,y),x,y)
10.19/3.51	    ?1#(false(),x,y) -> div#(m(x,y),s(y)) -> div#(s(x),s(y)) -> lt#(x,y)
10.19/3.51	    ?1#(false(),x,y) -> m#(x,y) -> m#(s(x),s(y)) -> m#(x,y)
10.19/3.51	    div#(s(x),s(y)) -> ?1#(lt(x,y),x,y) ->
10.19/3.51	    ?1#(false(),x,y) -> ?2#(div(m(x,y),s(y)),x,y)
10.19/3.51	    div#(s(x),s(y)) -> ?1#(lt(x,y),x,y) ->
10.19/3.51	    ?1#(false(),x,y) -> div#(m(x,y),s(y))
10.19/3.51	    div#(s(x),s(y)) -> ?1#(lt(x,y),x,y) -> ?1#(false(),x,y) -> m#(x,y)
10.19/3.51	    div#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y)
10.19/3.51	    lt#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y)
10.19/3.51	    m#(s(x),s(y)) -> m#(x,y) -> m#(s(x),s(y)) -> m#(x,y)
10.19/3.51	   SCC Processor:
10.19/3.51	    #sccs: 3
10.19/3.51	    #rules: 4
10.19/3.51	    #arcs: 9/49
10.19/3.51	    DPs:
10.19/3.51	     ?1#(false(),x,y) -> div#(m(x,y),s(y))
10.19/3.51	     div#(s(x),s(y)) -> ?1#(lt(x,y),x,y)
10.19/3.51	    TRS:
10.19/3.51	     m(x,0()) -> x
10.19/3.51	     m(s(x),s(y)) -> m(x,y)
10.19/3.51	     lt(x,0()) -> false()
10.19/3.51	     div(0(),s(x)) -> pair(0(),0())
10.19/3.51	     div(s(x),s(y)) -> ?1(lt(x,y),x,y)
10.19/3.51	     ?1(false(),x,y) -> ?2(div(m(x,y),s(y)),x,y)
10.19/3.51	     ?2(pair(q,r),x,y) -> pair(s(q),r)
10.19/3.51	     lt(s(x),s(y)) -> lt(x,y)
10.19/3.51	     ?1(true(),x,y) -> pair(0(),s(x))
10.19/3.51	     lt(0(),s(x)) -> true()
10.19/3.51	     m(0(),s(y)) -> 0()
10.19/3.51	    Subterm Criterion Processor:
10.19/3.51	     simple projection:
10.19/3.51	      pi(m) = 0
10.19/3.51	      pi(div#) = 0
10.19/3.51	      pi(?1#) = 1
10.19/3.51	     problem:
10.19/3.51	      DPs:
10.19/3.51	       ?1#(false(),x,y) -> div#(m(x,y),s(y))
10.19/3.51	      TRS:
10.19/3.51	       m(x,0()) -> x
10.19/3.51	       m(s(x),s(y)) -> m(x,y)
10.19/3.51	       lt(x,0()) -> false()
10.19/3.51	       div(0(),s(x)) -> pair(0(),0())
10.19/3.51	       div(s(x),s(y)) -> ?1(lt(x,y),x,y)
10.19/3.51	       ?1(false(),x,y) -> ?2(div(m(x,y),s(y)),x,y)
10.19/3.51	       ?2(pair(q,r),x,y) -> pair(s(q),r)
10.19/3.51	       lt(s(x),s(y)) -> lt(x,y)
10.19/3.51	       ?1(true(),x,y) -> pair(0(),s(x))
10.19/3.51	       lt(0(),s(x)) -> true()
10.19/3.51	       m(0(),s(y)) -> 0()
10.19/3.52	     SCC Processor:
10.19/3.52	      #sccs: 0
10.19/3.52	      #rules: 0
10.19/3.52	      #arcs: 2/1
10.19/3.52	      
10.19/3.52	    
10.19/3.52	    DPs:
10.19/3.52	     m#(s(x),s(y)) -> m#(x,y)
10.19/3.52	    TRS:
10.19/3.52	     m(x,0()) -> x
10.19/3.52	     m(s(x),s(y)) -> m(x,y)
10.19/3.52	     lt(x,0()) -> false()
10.19/3.52	     div(0(),s(x)) -> pair(0(),0())
10.19/3.52	     div(s(x),s(y)) -> ?1(lt(x,y),x,y)
10.19/3.52	     ?1(false(),x,y) -> ?2(div(m(x,y),s(y)),x,y)
10.19/3.52	     ?2(pair(q,r),x,y) -> pair(s(q),r)
10.19/3.52	     lt(s(x),s(y)) -> lt(x,y)
10.19/3.52	     ?1(true(),x,y) -> pair(0(),s(x))
10.19/3.52	     lt(0(),s(x)) -> true()
10.19/3.52	     m(0(),s(y)) -> 0()
10.19/3.52	    Subterm Criterion Processor:
10.19/3.52	     simple projection:
10.19/3.52	      pi(m#) = 0
10.19/3.52	     problem:
10.19/3.52	      DPs:
10.19/3.52	       
10.19/3.52	      TRS:
10.19/3.52	       m(x,0()) -> x
10.19/3.52	       m(s(x),s(y)) -> m(x,y)
10.19/3.52	       lt(x,0()) -> false()
10.19/3.52	       div(0(),s(x)) -> pair(0(),0())
10.19/3.52	       div(s(x),s(y)) -> ?1(lt(x,y),x,y)
10.19/3.52	       ?1(false(),x,y) -> ?2(div(m(x,y),s(y)),x,y)
10.19/3.52	       ?2(pair(q,r),x,y) -> pair(s(q),r)
10.19/3.52	       lt(s(x),s(y)) -> lt(x,y)
10.19/3.52	       ?1(true(),x,y) -> pair(0(),s(x))
10.19/3.52	       lt(0(),s(x)) -> true()
10.19/3.52	       m(0(),s(y)) -> 0()
10.19/3.52	     Qed
10.19/3.52	    
10.19/3.52	    DPs:
10.19/3.52	     lt#(s(x),s(y)) -> lt#(x,y)
10.19/3.52	    TRS:
10.19/3.52	     m(x,0()) -> x
10.19/3.52	     m(s(x),s(y)) -> m(x,y)
10.19/3.52	     lt(x,0()) -> false()
10.19/3.52	     div(0(),s(x)) -> pair(0(),0())
10.19/3.52	     div(s(x),s(y)) -> ?1(lt(x,y),x,y)
10.19/3.52	     ?1(false(),x,y) -> ?2(div(m(x,y),s(y)),x,y)
10.19/3.52	     ?2(pair(q,r),x,y) -> pair(s(q),r)
10.19/3.52	     lt(s(x),s(y)) -> lt(x,y)
10.19/3.52	     ?1(true(),x,y) -> pair(0(),s(x))
10.19/3.52	     lt(0(),s(x)) -> true()
10.19/3.52	     m(0(),s(y)) -> 0()
10.19/3.52	    Subterm Criterion Processor:
10.19/3.52	     simple projection:
10.19/3.52	      pi(lt#) = 0
10.19/3.52	     problem:
10.19/3.52	      DPs:
10.19/3.52	       
10.19/3.52	      TRS:
10.19/3.52	       m(x,0()) -> x
10.19/3.52	       m(s(x),s(y)) -> m(x,y)
10.19/3.52	       lt(x,0()) -> false()
10.19/3.52	       div(0(),s(x)) -> pair(0(),0())
10.19/3.52	       div(s(x),s(y)) -> ?1(lt(x,y),x,y)
10.19/3.52	       ?1(false(),x,y) -> ?2(div(m(x,y),s(y)),x,y)
10.19/3.52	       ?2(pair(q,r),x,y) -> pair(s(q),r)
10.19/3.52	       lt(s(x),s(y)) -> lt(x,y)
10.19/3.52	       ?1(true(),x,y) -> pair(0(),s(x))
10.19/3.52	       lt(0(),s(x)) -> true()
10.19/3.52	       m(0(),s(y)) -> 0()
10.19/3.52	     Qed
10.19/3.52	All 2 critical pairs are joinable.
10.19/3.52	Overlap: (rule1: div(s(y'), s(z')) -> pair(s(z), x') <= lt(y', z') = false, div(m(y', z'), s(z')) = pair(z, x'), rule2: div(s($1), s($2)) -> pair(0, s($1)) <= lt($1, $2) = true, pos: ε, mgu: {(y',$1), (z',$2)})
10.19/3.52	CP: pair(0, s($1)) = pair(s(z), x') <= lt($1, $2) = false, div(m($1, $2), s($2)) = pair(z, x'), lt($1, $2) = true
10.19/3.52	This critical pair is unfeasible.
10.19/3.52	Overlap: (rule1: div(s(z), s(x')) -> pair(0, s(z)) <= lt(z, x') = true, rule2: div(s($1), s($2)) -> pair(s(y'), z') <= lt($1, $2) = false, div(m($1, $2), s($2)) = pair(y', z'), pos: ε, mgu: {(z,$1), (x',$2)})
10.19/3.52	CP: pair(s(y'), z') = pair(0, s($1)) <= lt($1, $2) = true, lt($1, $2) = false, div(m($1, $2), s($2)) = pair(y', z')
10.19/3.52	This critical pair is unfeasible.
10.19/3.52	
10.19/3.56	EOF