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