5.90/2.20	MAYBE
5.90/2.20	
5.90/2.20	Proof:
5.90/2.20	ConCon could not decide confluence of the system.
5.97/2.24	\cite{ALS94}, Theorem 4.1 does not apply.
5.97/2.24	This system is of type 3 or smaller.
5.97/2.24	This system is strongly deterministic.
5.97/2.24	This system is quasi-decreasing.
5.97/2.24	By \cite{O02}, p. 214, Proposition 7.2.50.
5.97/2.24	This system is of type 3 or smaller.
5.97/2.24	This system is deterministic.
5.97/2.24	System R transformed to optimized U(R).
5.97/2.24	This system is terminating.
5.97/2.24	Call external tool:
5.97/2.24	./ttt2.sh
5.97/2.24	Input:
5.97/2.24	  gcd(x, y) -> ?1(leq(y, x), x, y)
5.97/2.24	  ?1(false, x, y) -> gcd(y, x)
5.97/2.24	  add(s(x), y) -> s(add(x, y))
5.97/2.24	  gcd(y, add(x, y)) -> gcd(x, y)
5.97/2.24	  gcd(0, x) -> x
5.97/2.24	  gcd(x, 0) -> x
5.97/2.24	  add(0, y) -> y
5.97/2.24	  gcd(add(x, y), y) -> gcd(x, y)
5.97/2.24	
5.97/2.24	 DP Processor:
5.97/2.24	  DPs:
5.97/2.24	   gcd#(x,y) -> ?1#(leq(y,x),x,y)
5.97/2.24	   ?1#(false(),x,y) -> gcd#(y,x)
5.97/2.24	   add#(s(x),y) -> add#(x,y)
5.97/2.24	   gcd#(y,add(x,y)) -> gcd#(x,y)
5.97/2.24	   gcd#(add(x,y),y) -> gcd#(x,y)
5.97/2.24	  TRS:
5.97/2.24	   gcd(x,y) -> ?1(leq(y,x),x,y)
5.97/2.24	   ?1(false(),x,y) -> gcd(y,x)
5.97/2.24	   add(s(x),y) -> s(add(x,y))
5.97/2.24	   gcd(y,add(x,y)) -> gcd(x,y)
5.97/2.24	   gcd(0(),x) -> x
5.97/2.24	   gcd(x,0()) -> x
5.97/2.24	   add(0(),y) -> y
5.97/2.24	   gcd(add(x,y),y) -> gcd(x,y)
5.97/2.24	  TDG Processor:
5.97/2.24	   DPs:
5.97/2.24	    gcd#(x,y) -> ?1#(leq(y,x),x,y)
5.97/2.24	    ?1#(false(),x,y) -> gcd#(y,x)
5.97/2.24	    add#(s(x),y) -> add#(x,y)
5.97/2.24	    gcd#(y,add(x,y)) -> gcd#(x,y)
5.97/2.24	    gcd#(add(x,y),y) -> gcd#(x,y)
5.97/2.24	   TRS:
5.97/2.24	    gcd(x,y) -> ?1(leq(y,x),x,y)
5.97/2.24	    ?1(false(),x,y) -> gcd(y,x)
5.97/2.24	    add(s(x),y) -> s(add(x,y))
5.97/2.24	    gcd(y,add(x,y)) -> gcd(x,y)
5.97/2.24	    gcd(0(),x) -> x
5.97/2.24	    gcd(x,0()) -> x
5.97/2.24	    add(0(),y) -> y
5.97/2.24	    gcd(add(x,y),y) -> gcd(x,y)
5.97/2.24	   graph:
5.97/2.24	    add#(s(x),y) -> add#(x,y) -> add#(s(x),y) -> add#(x,y)
5.97/2.24	    ?1#(false(),x,y) -> gcd#(y,x) -> gcd#(add(x,y),y) -> gcd#(x,y)
5.97/2.24	    ?1#(false(),x,y) -> gcd#(y,x) -> gcd#(y,add(x,y)) -> gcd#(x,y)
5.97/2.24	    ?1#(false(),x,y) -> gcd#(y,x) -> gcd#(x,y) -> ?1#(leq(y,x),x,y)
5.97/2.24	    gcd#(add(x,y),y) -> gcd#(x,y) -> gcd#(add(x,y),y) -> gcd#(x,y)
5.97/2.24	    gcd#(add(x,y),y) -> gcd#(x,y) -> gcd#(y,add(x,y)) -> gcd#(x,y)
5.97/2.24	    gcd#(add(x,y),y) -> gcd#(x,y) -> gcd#(x,y) -> ?1#(leq(y,x),x,y)
5.97/2.24	    gcd#(y,add(x,y)) -> gcd#(x,y) -> gcd#(add(x,y),y) -> gcd#(x,y)
5.97/2.24	    gcd#(y,add(x,y)) -> gcd#(x,y) -> gcd#(y,add(x,y)) -> gcd#(x,y)
5.97/2.24	    gcd#(y,add(x,y)) -> gcd#(x,y) -> gcd#(x,y) -> ?1#(leq(y,x),x,y)
5.97/2.24	    gcd#(x,y) -> ?1#(leq(y,x),x,y) -> ?1#(false(),x,y) -> gcd#(y,x)
5.97/2.24	   SCC Processor:
5.97/2.24	    #sccs: 2
5.97/2.24	    #rules: 5
5.97/2.24	    #arcs: 11/25
5.97/2.24	    DPs:
5.97/2.24	     ?1#(false(),x,y) -> gcd#(y,x)
5.97/2.24	     gcd#(x,y) -> ?1#(leq(y,x),x,y)
5.97/2.24	     gcd#(y,add(x,y)) -> gcd#(x,y)
5.97/2.24	     gcd#(add(x,y),y) -> gcd#(x,y)
5.97/2.24	    TRS:
5.97/2.24	     gcd(x,y) -> ?1(leq(y,x),x,y)
5.97/2.24	     ?1(false(),x,y) -> gcd(y,x)
5.97/2.24	     add(s(x),y) -> s(add(x,y))
5.97/2.24	     gcd(y,add(x,y)) -> gcd(x,y)
5.97/2.24	     gcd(0(),x) -> x
5.97/2.24	     gcd(x,0()) -> x
5.97/2.24	     add(0(),y) -> y
5.97/2.24	     gcd(add(x,y),y) -> gcd(x,y)
5.97/2.24	    EDG Processor:
5.97/2.24	     DPs:
5.97/2.24	      ?1#(false(),x,y) -> gcd#(y,x)
5.97/2.24	      gcd#(x,y) -> ?1#(leq(y,x),x,y)
5.97/2.24	      gcd#(y,add(x,y)) -> gcd#(x,y)
5.97/2.24	      gcd#(add(x,y),y) -> gcd#(x,y)
5.97/2.24	     TRS:
5.97/2.24	      gcd(x,y) -> ?1(leq(y,x),x,y)
5.97/2.24	      ?1(false(),x,y) -> gcd(y,x)
5.97/2.24	      add(s(x),y) -> s(add(x,y))
5.97/2.24	      gcd(y,add(x,y)) -> gcd(x,y)
5.97/2.24	      gcd(0(),x) -> x
5.97/2.24	      gcd(x,0()) -> x
5.97/2.24	      add(0(),y) -> y
5.97/2.24	      gcd(add(x,y),y) -> gcd(x,y)
5.97/2.24	     graph:
5.97/2.24	      ?1#(false(),x,y) -> gcd#(y,x) -> gcd#(x,y) -> ?1#(leq(y,x),x,y)
5.97/2.24	      ?1#(false(),x,y) -> gcd#(y,x) -> gcd#(y,add(x,y)) -> gcd#(x,y)
5.97/2.24	      ?1#(false(),x,y) -> gcd#(y,x) -> gcd#(add(x,y),y) -> gcd#(x,y)
5.97/2.24	      gcd#(add(x,y),y) -> gcd#(x,y) -> gcd#(x,y) -> ?1#(leq(y,x),x,y)
5.97/2.24	      gcd#(add(x,y),y) -> gcd#(x,y) -> gcd#(y,add(x,y)) -> gcd#(x,y)
5.97/2.24	      gcd#(add(x,y),y) -> gcd#(x,y) -> gcd#(add(x,y),y) -> gcd#(x,y)
5.97/2.24	      gcd#(y,add(x,y)) -> gcd#(x,y) -> gcd#(x,y) -> ?1#(leq(y,x),x,y)
5.97/2.24	      gcd#(y,add(x,y)) -> gcd#(x,y) -> gcd#(y,add(x,y)) -> gcd#(x,y)
5.97/2.24	      gcd#(y,add(x,y)) -> gcd#(x,y) -> gcd#(add(x,y),y) -> gcd#(x,y)
5.97/2.24	     SCC Processor:
5.97/2.24	      #sccs: 1
5.97/2.24	      #rules: 2
5.97/2.24	      #arcs: 9/16
5.97/2.24	      DPs:
5.97/2.24	       gcd#(add(x,y),y) -> gcd#(x,y)
5.97/2.24	       gcd#(y,add(x,y)) -> gcd#(x,y)
5.97/2.24	      TRS:
5.97/2.24	       gcd(x,y) -> ?1(leq(y,x),x,y)
5.97/2.24	       ?1(false(),x,y) -> gcd(y,x)
5.97/2.24	       add(s(x),y) -> s(add(x,y))
5.97/2.24	       gcd(y,add(x,y)) -> gcd(x,y)
5.97/2.24	       gcd(0(),x) -> x
5.97/2.24	       gcd(x,0()) -> x
5.97/2.24	       add(0(),y) -> y
5.97/2.24	       gcd(add(x,y),y) -> gcd(x,y)
5.97/2.24	      Size-Change Termination Processor:
5.97/2.24	       DPs:
5.97/2.24	        
5.97/2.24	       TRS:
5.97/2.24	        gcd(x,y) -> ?1(leq(y,x),x,y)
5.97/2.24	        ?1(false(),x,y) -> gcd(y,x)
5.97/2.24	        add(s(x),y) -> s(add(x,y))
5.97/2.24	        gcd(y,add(x,y)) -> gcd(x,y)
5.97/2.24	        gcd(0(),x) -> x
5.97/2.24	        gcd(x,0()) -> x
5.97/2.24	        add(0(),y) -> y
5.97/2.24	        gcd(add(x,y),y) -> gcd(x,y)
5.97/2.24	       The DP: gcd#(add(x,y),y) -> gcd#(x,y) has the edges:
5.97/2.24	         0 >   1
5.97/2.24	         0 >   0
5.97/2.24	         1 >=  1
5.97/2.24	       The DP: gcd#(y,add(x,y)) -> gcd#(x,y) has the edges:
5.97/2.24	         0 >=  1
5.97/2.24	         1 >   1
5.97/2.24	         1 >   0
5.97/2.24	       Qed
5.97/2.24	    
5.97/2.24	    DPs:
5.97/2.24	     add#(s(x),y) -> add#(x,y)
5.97/2.24	    TRS:
5.97/2.24	     gcd(x,y) -> ?1(leq(y,x),x,y)
5.97/2.24	     ?1(false(),x,y) -> gcd(y,x)
5.97/2.24	     add(s(x),y) -> s(add(x,y))
5.97/2.24	     gcd(y,add(x,y)) -> gcd(x,y)
5.97/2.24	     gcd(0(),x) -> x
5.97/2.24	     gcd(x,0()) -> x
5.97/2.24	     add(0(),y) -> y
5.97/2.24	     gcd(add(x,y),y) -> gcd(x,y)
5.97/2.24	    Subterm Criterion Processor:
5.97/2.24	     simple projection:
5.97/2.24	      pi(add#) = 0
5.97/2.24	     problem:
5.97/2.24	      DPs:
5.97/2.24	       
5.97/2.25	      TRS:
5.97/2.25	       gcd(x,y) -> ?1(leq(y,x),x,y)
5.97/2.25	       ?1(false(),x,y) -> gcd(y,x)
5.97/2.25	       add(s(x),y) -> s(add(x,y))
5.97/2.25	       gcd(y,add(x,y)) -> gcd(x,y)
5.97/2.25	       gcd(0(),x) -> x
5.97/2.25	       gcd(x,0()) -> x
5.97/2.25	       add(0(),y) -> y
5.97/2.25	       gcd(add(x,y),y) -> gcd(x,y)
5.97/2.25	     Qed
5.97/2.25	Overlap: (rule1: gcd(z, x') -> gcd(x', z) <= leq(x', z) = false, rule2: gcd(z', add(y', z')) -> gcd(y', z'), pos: ε, mgu: {(z',z), (x',add(y', z))})
5.97/2.25	CP: gcd(y', z) = gcd(add(y', z), z) <= leq(add(y', z), z) = false
5.97/2.25	This critical pair is context-joinable.
5.97/2.25	This critical pair is not unfeasible.
5.97/2.25	ConCon could not decide whether all 18 critical pairs are joinable or not.
5.97/2.25	Overlap: (rule1: gcd(add(z, x'), x') -> gcd(z, x'), rule2: add(0, x) -> x, pos: 1, mgu: {(z,0), (x,x')})
5.97/2.25	CP: gcd(x', x') = gcd(0, x')
5.97/2.25	This critical pair is not unfeasible.
5.97/2.25	
7.43/2.64	EOF