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