24.47/12.37	MAYBE
24.47/12.37	
24.47/12.37	Proof:
24.47/12.37	ConCon could not decide confluence of the system.
24.47/12.37	\cite{ALS94}, Theorem 4.1 does not apply.
24.47/12.37	This system is of type 3 or smaller.
24.47/12.37	This system is strongly deterministic.
24.47/12.37	This system is quasi-decreasing.
24.47/12.37	By \cite{O02}, p. 214, Proposition 7.2.50.
24.47/12.37	This system is of type 3 or smaller.
24.47/12.37	This system is deterministic.
24.47/12.37	System R transformed to optimized U(R).
24.47/12.37	This system is terminating.
24.47/12.37	Call external tool:
24.47/12.37	./ttt2.sh
24.47/12.37	Input:
24.47/12.37	(VAR x y)
24.47/12.37	(RULES
24.47/12.37	  m(x, 0) -> x
24.47/12.37	  m(s(x), s(y)) -> m(x, y)
24.47/12.37	  lt(x, 0) -> false
24.47/12.37	  gcd(0, s(y)) -> s(y)
24.47/12.37	  gcd(s(x), s(y)) -> ?2(lt(x, y), x, y)
24.47/12.37	  ?2(true, x, y) -> gcd(s(x), m(y, x))
24.47/12.37	  lt(s(x), s(y)) -> lt(x, y)
24.47/12.37	  gcd(s(x), s(y)) -> ?1(lt(y, x), x, y)
24.47/12.37	  ?1(true, x, y) -> gcd(m(x, y), s(y))
24.47/12.37	  lt(0, s(x)) -> true
24.47/12.37	  gcd(x, x) -> x
24.47/12.37	  gcd(s(x), 0) -> s(x)
24.47/12.37	  m(0, s(y)) -> 0
24.47/12.37	)
24.47/12.37	
24.47/12.37	 DP Processor:
24.47/12.37	  DPs:
24.47/12.37	   m#(s(x),s(y)) -> m#(x,y)
24.47/12.37	   gcd#(s(x),s(y)) -> lt#(x,y)
24.47/12.37	   gcd#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
24.47/12.37	   ?2#(true(),x,y) -> m#(y,x)
24.47/12.37	   ?2#(true(),x,y) -> gcd#(s(x),m(y,x))
24.47/12.37	   lt#(s(x),s(y)) -> lt#(x,y)
24.47/12.37	   gcd#(s(x),s(y)) -> lt#(y,x)
24.47/12.37	   gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
24.47/12.37	   ?1#(true(),x,y) -> m#(x,y)
24.47/12.37	   ?1#(true(),x,y) -> gcd#(m(x,y),s(y))
24.47/12.37	  TRS:
24.47/12.37	   m(x,0()) -> x
24.47/12.37	   m(s(x),s(y)) -> m(x,y)
24.47/12.37	   lt(x,0()) -> false()
24.47/12.37	   gcd(0(),s(y)) -> s(y)
24.47/12.37	   gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
24.47/12.37	   ?2(true(),x,y) -> gcd(s(x),m(y,x))
24.47/12.37	   lt(s(x),s(y)) -> lt(x,y)
24.47/12.37	   gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
24.47/12.37	   ?1(true(),x,y) -> gcd(m(x,y),s(y))
24.47/12.37	   lt(0(),s(x)) -> true()
24.47/12.37	   gcd(x,x) -> x
24.47/12.37	   gcd(s(x),0()) -> s(x)
24.47/12.37	   m(0(),s(y)) -> 0()
24.47/12.37	  TDG Processor:
24.47/12.37	   DPs:
24.47/12.37	    m#(s(x),s(y)) -> m#(x,y)
24.47/12.37	    gcd#(s(x),s(y)) -> lt#(x,y)
24.47/12.37	    gcd#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
24.47/12.37	    ?2#(true(),x,y) -> m#(y,x)
24.47/12.37	    ?2#(true(),x,y) -> gcd#(s(x),m(y,x))
24.47/12.37	    lt#(s(x),s(y)) -> lt#(x,y)
24.47/12.37	    gcd#(s(x),s(y)) -> lt#(y,x)
24.47/12.37	    gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
24.47/12.37	    ?1#(true(),x,y) -> m#(x,y)
24.47/12.37	    ?1#(true(),x,y) -> gcd#(m(x,y),s(y))
24.47/12.37	   TRS:
24.47/12.37	    m(x,0()) -> x
24.47/12.37	    m(s(x),s(y)) -> m(x,y)
24.47/12.37	    lt(x,0()) -> false()
24.47/12.37	    gcd(0(),s(y)) -> s(y)
24.47/12.37	    gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
24.47/12.37	    ?2(true(),x,y) -> gcd(s(x),m(y,x))
24.47/12.37	    lt(s(x),s(y)) -> lt(x,y)
24.47/12.37	    gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
24.47/12.37	    ?1(true(),x,y) -> gcd(m(x,y),s(y))
24.47/12.37	    lt(0(),s(x)) -> true()
24.47/12.37	    gcd(x,x) -> x
24.47/12.37	    gcd(s(x),0()) -> s(x)
24.47/12.37	    m(0(),s(y)) -> 0()
24.47/12.37	   graph:
24.47/12.37	    ?1#(true(),x,y) -> gcd#(m(x,y),s(y)) ->
24.47/12.37	    gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
24.47/12.37	    ?1#(true(),x,y) -> gcd#(m(x,y),s(y)) ->
24.47/12.37	    gcd#(s(x),s(y)) -> lt#(y,x)
24.47/12.37	    ?1#(true(),x,y) -> gcd#(m(x,y),s(y)) ->
24.47/12.37	    gcd#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
24.47/12.37	    ?1#(true(),x,y) -> gcd#(m(x,y),s(y)) -> gcd#(s(x),s(y)) -> lt#(x,y)
24.47/12.37	    ?1#(true(),x,y) -> m#(x,y) -> m#(s(x),s(y)) -> m#(x,y)
24.47/12.37	    ?2#(true(),x,y) -> gcd#(s(x),m(y,x)) ->
24.47/12.37	    gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
24.47/12.37	    ?2#(true(),x,y) -> gcd#(s(x),m(y,x)) ->
24.47/12.37	    gcd#(s(x),s(y)) -> lt#(y,x)
24.47/12.37	    ?2#(true(),x,y) -> gcd#(s(x),m(y,x)) ->
24.47/12.37	    gcd#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
24.47/12.37	    ?2#(true(),x,y) -> gcd#(s(x),m(y,x)) -> gcd#(s(x),s(y)) -> lt#(x,y)
24.47/12.37	    ?2#(true(),x,y) -> m#(y,x) -> m#(s(x),s(y)) -> m#(x,y)
24.47/12.37	    gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y) ->
24.47/12.37	    ?1#(true(),x,y) -> gcd#(m(x,y),s(y))
24.47/12.37	    gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y) ->
24.47/12.37	    ?1#(true(),x,y) -> m#(x,y)
24.47/12.37	    gcd#(s(x),s(y)) -> ?2#(lt(x,y),x,y) ->
24.47/12.37	    ?2#(true(),x,y) -> gcd#(s(x),m(y,x))
24.47/12.37	    gcd#(s(x),s(y)) -> ?2#(lt(x,y),x,y) -> ?2#(true(),x,y) -> m#(y,x)
24.47/12.37	    gcd#(s(x),s(y)) -> lt#(y,x) -> lt#(s(x),s(y)) -> lt#(x,y)
24.47/12.37	    gcd#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y)
24.47/12.37	    lt#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y)
24.47/12.37	    m#(s(x),s(y)) -> m#(x,y) -> m#(s(x),s(y)) -> m#(x,y)
24.47/12.37	   SCC Processor:
24.47/12.37	    #sccs: 3
24.47/12.37	    #rules: 6
24.47/12.37	    #arcs: 18/100
24.47/12.37	    DPs:
24.47/12.37	     ?1#(true(),x,y) -> gcd#(m(x,y),s(y))
24.47/12.37	     gcd#(s(x),s(y)) -> ?2#(lt(x,y),x,y)
24.47/12.37	     ?2#(true(),x,y) -> gcd#(s(x),m(y,x))
24.47/12.37	     gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
24.47/12.37	    TRS:
24.47/12.37	     m(x,0()) -> x
24.47/12.37	     m(s(x),s(y)) -> m(x,y)
24.47/12.38	     lt(x,0()) -> false()
24.47/12.38	     gcd(0(),s(y)) -> s(y)
24.47/12.38	     gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
24.47/12.38	     ?2(true(),x,y) -> gcd(s(x),m(y,x))
24.47/12.38	     lt(s(x),s(y)) -> lt(x,y)
24.47/12.38	     gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
24.47/12.38	     ?1(true(),x,y) -> gcd(m(x,y),s(y))
24.47/12.38	     lt(0(),s(x)) -> true()
24.47/12.38	     gcd(x,x) -> x
24.47/12.38	     gcd(s(x),0()) -> s(x)
24.47/12.38	     m(0(),s(y)) -> 0()
24.47/12.38	    Subterm Criterion Processor:
24.47/12.38	     simple projection:
24.47/12.38	      pi(m) = 0
24.47/12.38	      pi(s) = [0,0]
24.47/12.38	      pi(gcd#) = 1
24.47/12.38	      pi(?2#) = 2
24.47/12.38	      pi(?1#) = [2,2]
24.47/12.38	     problem:
24.47/12.38	      DPs:
24.47/12.38	       ?1#(true(),x,y) -> gcd#(m(x,y),s(y))
24.47/12.38	       ?2#(true(),x,y) -> gcd#(s(x),m(y,x))
24.47/12.38	       gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
24.47/12.38	      TRS:
24.47/12.38	       m(x,0()) -> x
24.47/12.38	       m(s(x),s(y)) -> m(x,y)
24.47/12.38	       lt(x,0()) -> false()
24.47/12.38	       gcd(0(),s(y)) -> s(y)
24.47/12.38	       gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
24.47/12.38	       ?2(true(),x,y) -> gcd(s(x),m(y,x))
24.47/12.38	       lt(s(x),s(y)) -> lt(x,y)
24.47/12.38	       gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
24.47/12.38	       ?1(true(),x,y) -> gcd(m(x,y),s(y))
24.47/12.38	       lt(0(),s(x)) -> true()
24.47/12.38	       gcd(x,x) -> x
24.47/12.38	       gcd(s(x),0()) -> s(x)
24.47/12.38	       m(0(),s(y)) -> 0()
24.47/12.38	     SCC Processor:
24.47/12.38	      #sccs: 1
24.47/12.38	      #rules: 2
24.47/12.38	      #arcs: 6/9
24.47/12.38	      DPs:
24.47/12.38	       ?1#(true(),x,y) -> gcd#(m(x,y),s(y))
24.47/12.38	       gcd#(s(x),s(y)) -> ?1#(lt(y,x),x,y)
24.47/12.38	      TRS:
24.47/12.38	       m(x,0()) -> x
24.47/12.38	       m(s(x),s(y)) -> m(x,y)
24.47/12.38	       lt(x,0()) -> false()
24.47/12.38	       gcd(0(),s(y)) -> s(y)
24.47/12.38	       gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
24.47/12.38	       ?2(true(),x,y) -> gcd(s(x),m(y,x))
24.47/12.38	       lt(s(x),s(y)) -> lt(x,y)
24.47/12.38	       gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
24.47/12.38	       ?1(true(),x,y) -> gcd(m(x,y),s(y))
24.47/12.38	       lt(0(),s(x)) -> true()
24.47/12.38	       gcd(x,x) -> x
24.47/12.38	       gcd(s(x),0()) -> s(x)
24.47/12.38	       m(0(),s(y)) -> 0()
24.47/12.38	      Subterm Criterion Processor:
24.47/12.38	       simple projection:
24.47/12.38	        pi(m) = [0,0]
24.47/12.38	        pi(gcd#) = 0
24.47/12.38	        pi(?1#) = [1,1,1]
24.47/12.38	       problem:
24.47/12.38	        DPs:
24.47/12.38	         
24.47/12.38	        TRS:
24.47/12.38	         m(x,0()) -> x
24.47/12.38	         m(s(x),s(y)) -> m(x,y)
24.47/12.38	         lt(x,0()) -> false()
24.47/12.38	         gcd(0(),s(y)) -> s(y)
24.47/12.38	         gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
24.47/12.38	         ?2(true(),x,y) -> gcd(s(x),m(y,x))
24.47/12.38	         lt(s(x),s(y)) -> lt(x,y)
24.47/12.38	         gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
24.47/12.38	         ?1(true(),x,y) -> gcd(m(x,y),s(y))
24.47/12.38	         lt(0(),s(x)) -> true()
24.47/12.38	         gcd(x,x) -> x
24.47/12.38	         gcd(s(x),0()) -> s(x)
24.47/12.38	         m(0(),s(y)) -> 0()
24.47/12.38	       Qed
24.47/12.38	    
24.47/12.38	    DPs:
24.47/12.38	     m#(s(x),s(y)) -> m#(x,y)
24.47/12.38	    TRS:
24.47/12.38	     m(x,0()) -> x
24.47/12.38	     m(s(x),s(y)) -> m(x,y)
24.47/12.38	     lt(x,0()) -> false()
24.47/12.38	     gcd(0(),s(y)) -> s(y)
24.47/12.38	     gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
24.47/12.38	     ?2(true(),x,y) -> gcd(s(x),m(y,x))
24.47/12.38	     lt(s(x),s(y)) -> lt(x,y)
24.47/12.38	     gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
24.47/12.38	     ?1(true(),x,y) -> gcd(m(x,y),s(y))
24.47/12.38	     lt(0(),s(x)) -> true()
24.47/12.38	     gcd(x,x) -> x
24.47/12.38	     gcd(s(x),0()) -> s(x)
24.47/12.38	     m(0(),s(y)) -> 0()
24.47/12.38	    Subterm Criterion Processor:
24.47/12.38	     simple projection:
24.47/12.38	      pi(m#) = 0
24.47/12.38	     problem:
24.47/12.38	      DPs:
24.47/12.38	       
24.47/12.38	      TRS:
24.47/12.38	       m(x,0()) -> x
24.47/12.38	       m(s(x),s(y)) -> m(x,y)
24.47/12.38	       lt(x,0()) -> false()
24.47/12.38	       gcd(0(),s(y)) -> s(y)
24.47/12.38	       gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
24.47/12.38	       ?2(true(),x,y) -> gcd(s(x),m(y,x))
24.47/12.38	       lt(s(x),s(y)) -> lt(x,y)
24.47/12.38	       gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
24.47/12.38	       ?1(true(),x,y) -> gcd(m(x,y),s(y))
24.47/12.38	       lt(0(),s(x)) -> true()
24.47/12.38	       gcd(x,x) -> x
24.47/12.38	       gcd(s(x),0()) -> s(x)
24.47/12.38	       m(0(),s(y)) -> 0()
24.47/12.38	     Qed
24.47/12.38	    
24.47/12.38	    DPs:
24.47/12.38	     lt#(s(x),s(y)) -> lt#(x,y)
24.47/12.38	    TRS:
24.47/12.38	     m(x,0()) -> x
24.47/12.38	     m(s(x),s(y)) -> m(x,y)
24.47/12.38	     lt(x,0()) -> false()
24.47/12.38	     gcd(0(),s(y)) -> s(y)
24.47/12.38	     gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
24.47/12.38	     ?2(true(),x,y) -> gcd(s(x),m(y,x))
24.47/12.38	     lt(s(x),s(y)) -> lt(x,y)
24.47/12.38	     gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
24.47/12.38	     ?1(true(),x,y) -> gcd(m(x,y),s(y))
24.47/12.38	     lt(0(),s(x)) -> true()
24.47/12.38	     gcd(x,x) -> x
24.47/12.38	     gcd(s(x),0()) -> s(x)
24.47/12.38	     m(0(),s(y)) -> 0()
24.47/12.38	    Subterm Criterion Processor:
24.47/12.38	     simple projection:
24.47/12.38	      pi(lt#) = 0
24.47/12.38	     problem:
24.47/12.38	      DPs:
24.47/12.38	       
24.47/12.38	      TRS:
24.47/12.38	       m(x,0()) -> x
24.47/12.38	       m(s(x),s(y)) -> m(x,y)
24.47/12.38	       lt(x,0()) -> false()
24.47/12.38	       gcd(0(),s(y)) -> s(y)
24.47/12.38	       gcd(s(x),s(y)) -> ?2(lt(x,y),x,y)
24.47/12.38	       ?2(true(),x,y) -> gcd(s(x),m(y,x))
24.47/12.38	       lt(s(x),s(y)) -> lt(x,y)
24.47/12.38	       gcd(s(x),s(y)) -> ?1(lt(y,x),x,y)
24.47/12.38	       ?1(true(),x,y) -> gcd(m(x,y),s(y))
24.47/12.38	       lt(0(),s(x)) -> true()
24.47/12.38	       gcd(x,x) -> x
24.47/12.38	       gcd(s(x),0()) -> s(x)
24.47/12.38	       m(0(),s(y)) -> 0()
24.47/12.38	     Qed
24.47/12.38	This critical pair is conditional.
24.47/12.38	This critical pair has some non-trivial conditions.
24.47/12.38	ConCon could not decide whether all 6 critical pairs are joinable or not.
24.47/12.38	Overlap: (rule1: gcd(s(z), s(x')) -> gcd(m(z, x'), s(x')) <= lt(x', z) = true, rule2: gcd(s(y'), s(z')) -> gcd(s(y'), m(z', y')) <= lt(y', z') = true, pos: ε, mgu: {(z,y'), (x',z')})
24.47/12.38	CP: gcd(s(y'), m(z', y')) = gcd(m(y', z'), s(z')) <= lt(z', y') = true, lt(y', z') = true
24.47/12.38	ConCon could not decide infeasibility of this critical pair.
24.47/12.38	
24.47/12.41	EOF