8.56/2.77	YES
8.56/2.77	
8.56/2.77	Proof:
8.56/2.77	This system is confluent.
8.56/2.77	By \cite{ALS94}, Theorem 4.1.
8.56/2.78	This system is of type 3 or smaller.
8.56/2.78	This system is strongly deterministic.
8.56/2.78	This system is quasi-decreasing.
8.56/2.78	By \cite{O02}, p. 214, Proposition 7.2.50.
8.56/2.78	This system is of type 3 or smaller.
8.56/2.78	This system is deterministic.
8.56/2.78	System R transformed to U(R).
8.56/2.78	This system is terminating.
8.56/2.78	Call external tool:
8.56/2.78	./ttt2.sh
8.56/2.78	Input:
8.56/2.78	  lt(x, 0) -> false
8.56/2.78	  lt(0, s(x)) -> true
8.56/2.78	  lt(s(x), s(y)) -> lt(x, y)
8.56/2.78	  m(0, s(y)) -> 0
8.56/2.78	  m(x, 0) -> x
8.56/2.78	  m(s(x), s(y)) -> m(x, y)
8.56/2.78	  div(0, s(x)) -> pair(0, 0)
8.56/2.78	  ?1(true, x, y) -> pair(0, s(x))
8.56/2.78	  div(s(x), s(y)) -> ?1(lt(x, y), x, y)
8.56/2.78	  ?3(pair(q, r), x, y) -> pair(s(q), r)
8.56/2.78	  ?2(false, x, y) -> ?3(div(m(x, y), s(y)), x, y)
8.56/2.78	  div(s(x), s(y)) -> ?2(lt(x, y), x, y)
8.56/2.78	
8.56/2.79	 DP Processor:
8.56/2.79	  DPs:
8.56/2.79	   lt#(s(x),s(y)) -> lt#(x,y)
8.56/2.79	   m#(s(x),s(y)) -> m#(x,y)
8.56/2.79	   div#(s(x),s(y)) -> lt#(x,y)
8.56/2.79	   div#(s(x),s(y)) -> ?1#(lt(x,y),x,y)
8.56/2.79	   ?2#(false(),x,y) -> m#(x,y)
8.56/2.79	   ?2#(false(),x,y) -> div#(m(x,y),s(y))
8.56/2.79	   ?2#(false(),x,y) -> ?3#(div(m(x,y),s(y)),x,y)
8.56/2.79	   div#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
8.56/2.79	  TRS:
8.56/2.79	   lt(x,0()) -> false()
8.56/2.79	   lt(0(),s(x)) -> true()
8.56/2.79	   lt(s(x),s(y)) -> lt(x,y)
8.56/2.79	   m(0(),s(y)) -> 0()
8.56/2.79	   m(x,0()) -> x
8.56/2.79	   m(s(x),s(y)) -> m(x,y)
8.56/2.79	   div(0(),s(x)) -> pair(0(),0())
8.56/2.79	   ?1(true(),x,y) -> pair(0(),s(x))
8.56/2.79	   div(s(x),s(y)) -> ?1(lt(x,y),x,y)
8.56/2.79	   ?3(pair(q,r),x,y) -> pair(s(q),r)
8.56/2.79	   ?2(false(),x,y) -> ?3(div(m(x,y),s(y)),x,y)
8.56/2.79	   div(s(x),s(y)) -> ?2(lt(x,y),x,y)
8.56/2.79	  TDG Processor:
8.56/2.79	   DPs:
8.56/2.79	    lt#(s(x),s(y)) -> lt#(x,y)
8.56/2.79	    m#(s(x),s(y)) -> m#(x,y)
8.56/2.79	    div#(s(x),s(y)) -> lt#(x,y)
8.56/2.79	    div#(s(x),s(y)) -> ?1#(lt(x,y),x,y)
8.56/2.79	    ?2#(false(),x,y) -> m#(x,y)
8.56/2.79	    ?2#(false(),x,y) -> div#(m(x,y),s(y))
8.56/2.79	    ?2#(false(),x,y) -> ?3#(div(m(x,y),s(y)),x,y)
8.56/2.79	    div#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
8.56/2.79	   TRS:
8.56/2.80	    lt(x,0()) -> false()
8.56/2.80	    lt(0(),s(x)) -> true()
8.56/2.80	    lt(s(x),s(y)) -> lt(x,y)
8.56/2.80	    m(0(),s(y)) -> 0()
8.56/2.80	    m(x,0()) -> x
8.56/2.80	    m(s(x),s(y)) -> m(x,y)
8.56/2.80	    div(0(),s(x)) -> pair(0(),0())
8.56/2.80	    ?1(true(),x,y) -> pair(0(),s(x))
8.56/2.80	    div(s(x),s(y)) -> ?1(lt(x,y),x,y)
8.56/2.80	    ?3(pair(q,r),x,y) -> pair(s(q),r)
8.56/2.80	    ?2(false(),x,y) -> ?3(div(m(x,y),s(y)),x,y)
8.56/2.80	    div(s(x),s(y)) -> ?2(lt(x,y),x,y)
8.56/2.80	   graph:
8.56/2.80	    ?2#(false(),x,y) -> div#(m(x,y),s(y)) ->
8.56/2.80	    div#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
8.56/2.80	    ?2#(false(),x,y) -> div#(m(x,y),s(y)) ->
8.56/2.80	    div#(s(x),s(y)) -> ?1#(lt(x,y),x,y)
8.56/2.80	    ?2#(false(),x,y) -> div#(m(x,y),s(y)) -> div#(s(x),s(y)) -> lt#(x,y)
8.56/2.80	    ?2#(false(),x,y) -> m#(x,y) -> m#(s(x),s(y)) -> m#(x,y)
8.56/2.80	    div#(s(x),s(y)) -> ?2#(lt(x,y),x,y) ->
8.56/2.80	    ?2#(false(),x,y) -> ?3#(div(m(x,y),s(y)),x,y)
8.56/2.80	    div#(s(x),s(y)) -> ?2#(lt(x,y),x,y) ->
8.56/2.80	    ?2#(false(),x,y) -> div#(m(x,y),s(y))
8.56/2.80	    div#(s(x),s(y)) -> ?2#(lt(x,y),x,y) -> ?2#(false(),x,y) -> m#(x,y)
8.56/2.80	    div#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y)
8.56/2.80	    m#(s(x),s(y)) -> m#(x,y) -> m#(s(x),s(y)) -> m#(x,y)
8.56/2.80	    lt#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y)
8.56/2.80	   SCC Processor:
8.56/2.80	    #sccs: 3
8.56/2.80	    #rules: 4
8.56/2.80	    #arcs: 10/64
8.56/2.80	    DPs:
8.56/2.80	     ?2#(false(),x,y) -> div#(m(x,y),s(y))
8.56/2.80	     div#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
8.56/2.80	    TRS:
8.56/2.80	     lt(x,0()) -> false()
8.56/2.80	     lt(0(),s(x)) -> true()
8.56/2.80	     lt(s(x),s(y)) -> lt(x,y)
8.56/2.80	     m(0(),s(y)) -> 0()
8.56/2.80	     m(x,0()) -> x
8.56/2.80	     m(s(x),s(y)) -> m(x,y)
8.56/2.80	     div(0(),s(x)) -> pair(0(),0())
8.56/2.80	     ?1(true(),x,y) -> pair(0(),s(x))
8.56/2.80	     div(s(x),s(y)) -> ?1(lt(x,y),x,y)
8.56/2.80	     ?3(pair(q,r),x,y) -> pair(s(q),r)
8.56/2.80	     ?2(false(),x,y) -> ?3(div(m(x,y),s(y)),x,y)
8.56/2.80	     div(s(x),s(y)) -> ?2(lt(x,y),x,y)
8.56/2.80	    Subterm Criterion Processor:
8.56/2.80	     simple projection:
8.56/2.80	      pi(m) = 0
8.56/2.80	      pi(div#) = 0
8.56/2.80	      pi(?2#) = 1
8.56/2.80	     problem:
8.56/2.80	      DPs:
8.56/2.81	       ?2#(false(),x,y) -> div#(m(x,y),s(y))
8.56/2.81	      TRS:
8.56/2.81	       lt(x,0()) -> false()
8.56/2.81	       lt(0(),s(x)) -> true()
8.56/2.81	       lt(s(x),s(y)) -> lt(x,y)
8.56/2.81	       m(0(),s(y)) -> 0()
8.56/2.81	       m(x,0()) -> x
8.56/2.81	       m(s(x),s(y)) -> m(x,y)
8.56/2.81	       div(0(),s(x)) -> pair(0(),0())
8.56/2.81	       ?1(true(),x,y) -> pair(0(),s(x))
8.56/2.81	       div(s(x),s(y)) -> ?1(lt(x,y),x,y)
8.56/2.81	       ?3(pair(q,r),x,y) -> pair(s(q),r)
8.56/2.81	       ?2(false(),x,y) -> ?3(div(m(x,y),s(y)),x,y)
8.56/2.81	       div(s(x),s(y)) -> ?2(lt(x,y),x,y)
8.56/2.81	     SCC Processor:
8.56/2.81	      #sccs: 0
8.56/2.81	      #rules: 0
8.56/2.81	      #arcs: 2/1
8.56/2.81	      
8.56/2.81	    
8.56/2.81	    DPs:
8.56/2.81	     m#(s(x),s(y)) -> m#(x,y)
8.56/2.82	    TRS:
8.56/2.82	     lt(x,0()) -> false()
8.56/2.82	     lt(0(),s(x)) -> true()
8.56/2.82	     lt(s(x),s(y)) -> lt(x,y)
8.56/2.82	     m(0(),s(y)) -> 0()
8.56/2.82	     m(x,0()) -> x
8.56/2.82	     m(s(x),s(y)) -> m(x,y)
8.56/2.82	     div(0(),s(x)) -> pair(0(),0())
8.56/2.82	     ?1(true(),x,y) -> pair(0(),s(x))
8.56/2.82	     div(s(x),s(y)) -> ?1(lt(x,y),x,y)
8.56/2.82	     ?3(pair(q,r),x,y) -> pair(s(q),r)
8.56/2.82	     ?2(false(),x,y) -> ?3(div(m(x,y),s(y)),x,y)
8.56/2.82	     div(s(x),s(y)) -> ?2(lt(x,y),x,y)
8.56/2.82	    Subterm Criterion Processor:
8.56/2.82	     simple projection:
8.56/2.82	      pi(m#) = 0
8.56/2.82	     problem:
8.56/2.82	      DPs:
8.56/2.82	       
8.56/2.82	      TRS:
8.56/2.82	       lt(x,0()) -> false()
8.56/2.82	       lt(0(),s(x)) -> true()
8.56/2.82	       lt(s(x),s(y)) -> lt(x,y)
8.56/2.82	       m(0(),s(y)) -> 0()
8.56/2.82	       m(x,0()) -> x
8.56/2.82	       m(s(x),s(y)) -> m(x,y)
8.56/2.82	       div(0(),s(x)) -> pair(0(),0())
8.56/2.82	       ?1(true(),x,y) -> pair(0(),s(x))
8.56/2.82	       div(s(x),s(y)) -> ?1(lt(x,y),x,y)
8.56/2.82	       ?3(pair(q,r),x,y) -> pair(s(q),r)
8.56/2.82	       ?2(false(),x,y) -> ?3(div(m(x,y),s(y)),x,y)
8.56/2.82	       div(s(x),s(y)) -> ?2(lt(x,y),x,y)
8.56/2.82	     Qed
8.56/2.82	    
8.56/2.82	    DPs:
8.56/2.82	     lt#(s(x),s(y)) -> lt#(x,y)
8.56/2.82	    TRS:
8.56/2.82	     lt(x,0()) -> false()
8.56/2.82	     lt(0(),s(x)) -> true()
8.56/2.82	     lt(s(x),s(y)) -> lt(x,y)
8.56/2.82	     m(0(),s(y)) -> 0()
8.56/2.82	     m(x,0()) -> x
8.56/2.82	     m(s(x),s(y)) -> m(x,y)
8.56/2.82	     div(0(),s(x)) -> pair(0(),0())
8.56/2.83	     ?1(true(),x,y) -> pair(0(),s(x))
8.56/2.83	     div(s(x),s(y)) -> ?1(lt(x,y),x,y)
8.56/2.83	     ?3(pair(q,r),x,y) -> pair(s(q),r)
8.56/2.83	     ?2(false(),x,y) -> ?3(div(m(x,y),s(y)),x,y)
8.56/2.83	     div(s(x),s(y)) -> ?2(lt(x,y),x,y)
8.56/2.83	    Subterm Criterion Processor:
8.56/2.83	     simple projection:
8.56/2.83	      pi(lt#) = 0
8.56/2.83	     problem:
8.56/2.83	      DPs:
8.56/2.83	       
8.56/2.83	      TRS:
8.56/2.83	       lt(x,0()) -> false()
8.56/2.83	       lt(0(),s(x)) -> true()
8.56/2.83	       lt(s(x),s(y)) -> lt(x,y)
8.56/2.83	       m(0(),s(y)) -> 0()
8.56/2.83	       m(x,0()) -> x
8.56/2.83	       m(s(x),s(y)) -> m(x,y)
8.56/2.83	       div(0(),s(x)) -> pair(0(),0())
8.56/2.83	       ?1(true(),x,y) -> pair(0(),s(x))
8.56/2.83	       div(s(x),s(y)) -> ?1(lt(x,y),x,y)
8.56/2.83	       ?3(pair(q,r),x,y) -> pair(s(q),r)
8.56/2.83	       ?2(false(),x,y) -> ?3(div(m(x,y),s(y)),x,y)
8.56/2.83	       div(s(x),s(y)) -> ?2(lt(x,y),x,y)
8.56/2.83	     Qed
8.56/2.83	All 2 critical pairs are joinable.
8.56/2.83	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: {($1,y'), ($2,z')})
8.56/2.83	CP: pair(0, s(y')) = pair(s(z), x') <= lt(y', z') = false, div(m(y', z'), s(z')) = pair(z, x'), lt(y', z') = true
8.56/2.83	This critical pair is unfeasible.
8.56/2.83	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: {($1,z), ($2,x')})
8.56/2.83	CP: pair(s(y'), z') = pair(0, s(z)) <= lt(z, x') = true, lt(z, x') = false, div(m(z, x'), s(x')) = pair(y', z')
8.56/2.83	This critical pair is unfeasible.
8.56/2.83	
9.57/3.08	EOF