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