55.52/14.85	YES
55.52/14.85	
55.52/14.85	Problem:
55.52/14.85	le(0(), s(x)) -> true()
55.52/14.85	le(x, 0()) -> false()
55.52/14.85	le(s(x), s(y)) -> le(x, y)
55.52/14.90	min(cons(x, nil())) -> x
55.52/14.90	min(cons(x, l)) -> x <= le(x, min(l)) = true()
55.52/14.90	min(cons(x, l)) -> min(l) <= le(x, min(l)) = false()
55.52/14.90	min(cons(x, l)) -> min(l) <= min(l) = x
55.52/14.90	
55.52/14.90	Proof:
55.52/14.90	This system is confluent.
55.52/14.90	By \cite{ALS94}, Theorem 4.1.
55.52/14.90	This system is of type 3 or smaller.
55.52/14.90	This system is strongly deterministic.
55.52/14.90	All 12 critical pairs are joinable.
55.52/14.90	CP: min(x) = min(x) <= min(x) = x', le(x', min(x)) = false():
55.52/14.90	This critical pair is context-joinable.
55.52/14.90	CP: min(x) = x' <= le(x', min(x)) = true(), le(x', min(x)) = false():
55.52/14.90	This critical pair is unfeasible.
55.52/14.90	CP: x = min(x') <= le(x, min(x')) = false(), le(x, min(x')) = true():
55.52/14.90	This critical pair is unfeasible.
55.52/14.90	CP: x = min(x') <= min(x') = x, le(x, min(x')) = true():
55.52/14.90	This critical pair is context-joinable.
55.52/14.90	CP: min(nil()) = x <= le(x, min(nil())) = false():
55.52/14.90	This critical pair is infeasible.
55.52/14.90	This critical pair is conditional.
55.52/14.90	This critical pair has some non-trivial conditions.
55.52/14.90	usable rules
55.52/14.90	'\Sigma(le(x, min(nil()))) \cap (->^*_R)[\Sigma(REN(false()))]' is empty.
55.52/14.90	CP: x = x <= le(x, min(nil())) = true():
55.52/14.90	This critical pair is context-joinable.
55.52/14.90	CP: x = min(nil()) <= min(nil()) = x:
55.52/14.90	This critical pair is context-joinable.
55.52/14.90	CP: min(x) = min(x) <= le(x', min(x)) = false(), min(x) = x':
55.52/14.90	This critical pair is context-joinable.
55.52/14.90	CP: min(x) = x' <= le(x', min(x)) = true(), min(x) = x':
55.52/14.90	This critical pair is context-joinable.
55.52/14.90	CP: min(nil()) = x <= min(nil()) = x:
55.52/14.90	This critical pair is context-joinable.
55.52/14.90	CP: x = min(nil()) <= le(x, min(nil())) = false():
55.52/14.90	This critical pair is infeasible.
55.52/14.90	This critical pair is conditional.
55.52/14.90	This critical pair has some non-trivial conditions.
55.52/14.90	'[\Sigma(REN(conds(le(x, min(nil())))))](->^*_R_\alpha) \cap \Sigma(conds(false()))' is empty.
55.52/14.90	CP: x = x <= le(x, min(nil())) = true():
55.52/14.90	This critical pair is infeasible.
55.52/14.90	This critical pair is conditional.
55.52/14.90	This critical pair has some non-trivial conditions.
55.52/14.90	'[\Sigma(REN(conds(le(x, min(nil())))))](->^*_R_\alpha) \cap \Sigma(conds(true()))' is empty.
55.52/14.90	This system is quasi-decreasing.
55.52/14.90	By \cite{O02}, p. 214, Proposition 7.2.50.
55.52/14.90	This system is of type 3 or smaller.
55.52/14.90	This system is deterministic.
55.52/14.90	System R transformed to U(R).
55.52/14.90	This system is terminating.
55.52/14.90	Call external tool:
55.52/14.90	./ttt2.sh
55.52/14.90	Input:
55.52/14.90	  le(0(), s(x)) -> true()
55.52/14.90	  le(x, 0()) -> false()
55.52/14.90	  le(s(x), s(y)) -> le(x, y)
55.52/14.90	  min(cons(x, nil())) -> x
55.52/14.90	  ?3(true(), x, l) -> x
55.52/14.90	  min(cons(x, l)) -> ?3(le(x, min(l)), x, l)
55.52/14.90	  ?1(false(), x, l) -> min(l)
55.52/14.90	  min(cons(x, l)) -> ?1(le(x, min(l)), x, l)
55.52/14.90	  ?2(x, x, l) -> min(l)
55.52/14.90	  min(cons(x, l)) -> ?2(min(l), x, l)
55.52/14.90	
55.52/14.90	 Matrix Interpretation Processor: dim=1
55.52/14.90	  
55.52/14.90	  interpretation:
55.52/14.90	   [?2](x0, x1, x2) = x0 + 4x1 + 2x2,
55.52/14.90	   
55.52/14.90	   [?1](x0, x1, x2) = x0 + 4x1 + 2x2,
55.52/14.90	   
55.52/14.90	   [?3](x0, x1, x2) = x0 + 3x1 + 2x2,
55.52/14.90	   
55.52/14.90	   [min](x0) = 2x0,
55.52/14.90	   
55.52/14.90	   [cons](x0, x1) = 4x0 + 2x1,
55.52/14.90	   
55.52/14.90	   [nil] = 5,
55.52/14.90	   
55.52/14.90	   [false] = 1,
55.52/14.90	   
55.52/14.90	   [true] = 1,
55.52/14.90	   
55.52/14.90	   [le](x0, x1) = 4x0 + x1,
55.52/14.90	   
55.52/14.90	   [s](x0) = 2x0 + 1,
55.52/14.90	   
55.52/14.90	   [0] = 2
55.52/14.90	  orientation:
55.52/14.90	   le(0(),s(x)) = 2x + 9 >= 1 = true()
55.52/14.90	   
55.52/14.90	   le(x,0()) = 4x + 2 >= 1 = false()
55.52/14.90	   
55.52/14.90	   le(s(x),s(y)) = 8x + 2y + 5 >= 4x + y = le(x,y)
55.52/14.90	   
55.52/14.90	   min(cons(x,nil())) = 8x + 20 >= x = x
55.52/14.90	   
55.52/14.90	   ?3(true(),x,l) = 2l + 3x + 1 >= x = x
55.52/14.90	   
55.52/14.90	   min(cons(x,l)) = 4l + 8x >= 4l + 7x = ?3(le(x,min(l)),x,l)
55.52/14.90	   
55.52/14.90	   ?1(false(),x,l) = 2l + 4x + 1 >= 2l = min(l)
55.52/14.90	   
55.52/14.90	   min(cons(x,l)) = 4l + 8x >= 4l + 8x = ?1(le(x,min(l)),x,l)
55.52/14.90	   
55.52/14.90	   ?2(x,x,l) = 2l + 5x >= 2l = min(l)
55.52/14.90	   
55.52/14.90	   min(cons(x,l)) = 4l + 8x >= 4l + 4x = ?2(min(l),x,l)
55.52/14.90	  problem:
55.52/14.90	   min(cons(x,l)) -> ?3(le(x,min(l)),x,l)
55.52/14.90	   min(cons(x,l)) -> ?1(le(x,min(l)),x,l)
55.52/14.90	   ?2(x,x,l) -> min(l)
55.52/14.90	   min(cons(x,l)) -> ?2(min(l),x,l)
55.52/14.90	  Matrix Interpretation Processor: dim=1
55.52/14.90	   
55.52/14.90	   interpretation:
55.52/14.91	    [?2](x0, x1, x2) = x0 + 2x1 + 5x2,
55.52/14.91	    
55.52/14.91	    [?1](x0, x1, x2) = 4x0 + x1 + 5x2 + 4,
55.52/14.91	    
55.52/14.91	    [?3](x0, x1, x2) = 4x0 + x1 + 4x2 + 4,
55.52/14.91	    
55.52/14.91	    [min](x0) = 3x0,
55.52/14.91	    
55.52/14.91	    [cons](x0, x1) = 6x0 + 6x1 + 4,
55.52/14.91	    
55.52/14.91	    [le](x0, x1) = 4x0 + x1 + 2
55.52/14.91	   orientation:
55.52/14.91	    min(cons(x,l)) = 18l + 18x + 12 >= 16l + 17x + 12 = ?3(le(x,min(l)),x,l)
55.52/14.91	    
55.52/14.91	    min(cons(x,l)) = 18l + 18x + 12 >= 17l + 17x + 12 = ?1(le(x,min(l)),x,l)
55.52/14.91	    
55.52/14.91	    ?2(x,x,l) = 5l + 3x >= 3l = min(l)
55.52/14.91	    
55.52/14.91	    min(cons(x,l)) = 18l + 18x + 12 >= 8l + 2x = ?2(min(l),x,l)
55.52/14.91	   problem:
55.52/14.91	    min(cons(x,l)) -> ?3(le(x,min(l)),x,l)
55.52/14.91	    min(cons(x,l)) -> ?1(le(x,min(l)),x,l)
55.52/14.91	    ?2(x,x,l) -> min(l)
55.52/14.91	   DP Processor:
55.52/14.91	    DPs:
55.52/14.91	     min#(cons(x,l)) -> min#(l)
55.52/14.91	     ?2#(x,x,l) -> min#(l)
55.52/14.91	    TRS:
55.52/14.91	     min(cons(x,l)) -> ?3(le(x,min(l)),x,l)
55.52/14.91	     min(cons(x,l)) -> ?1(le(x,min(l)),x,l)
55.52/14.91	     ?2(x,x,l) -> min(l)
55.52/14.91	    TDG Processor:
55.52/14.91	     DPs:
55.52/14.91	      min#(cons(x,l)) -> min#(l)
55.52/14.91	      ?2#(x,x,l) -> min#(l)
55.52/14.91	     TRS:
55.52/14.91	      min(cons(x,l)) -> ?3(le(x,min(l)),x,l)
55.52/14.91	      min(cons(x,l)) -> ?1(le(x,min(l)),x,l)
55.52/14.92	      ?2(x,x,l) -> min(l)
55.52/14.92	     graph:
55.52/14.92	      ?2#(x,x,l) -> min#(l) -> min#(cons(x,l)) -> min#(l)
55.52/14.92	      min#(cons(x,l)) -> min#(l) -> min#(cons(x,l)) -> min#(l)
55.52/14.92	     SCC Processor:
55.52/14.92	      #sccs: 1
55.52/14.92	      #rules: 1
55.52/14.92	      #arcs: 2/4
55.52/14.92	      DPs:
55.52/14.92	       min#(cons(x,l)) -> min#(l)
55.52/14.92	      TRS:
55.52/14.92	       min(cons(x,l)) -> ?3(le(x,min(l)),x,l)
55.52/14.92	       min(cons(x,l)) -> ?1(le(x,min(l)),x,l)
55.52/14.92	       ?2(x,x,l) -> min(l)
55.52/14.92	      Subterm Criterion Processor:
55.52/14.92	       simple projection:
55.52/14.92	        pi(min#) = 0
55.52/14.92	       problem:
55.52/14.92	        DPs:
55.52/14.92	         
55.52/14.92	        TRS:
55.52/14.92	         min(cons(x,l)) -> ?3(le(x,min(l)),x,l)
55.52/14.92	         min(cons(x,l)) -> ?1(le(x,min(l)),x,l)
55.52/14.92	         ?2(x,x,l) -> min(l)
55.52/14.92	       Qed
55.52/14.92	
58.30/15.61	EOF