14.96/4.86	YES
14.96/4.86	
14.96/4.86	Proof:
14.96/4.86	This system is confluent.
14.96/4.86	By \cite{ALS94}, Theorem 4.1.
14.96/4.86	This system is of type 3 or smaller.
14.96/4.86	This system is strongly deterministic.
14.96/4.86	This system is quasi-decreasing.
14.96/4.86	By \cite{O02}, p. 214, Proposition 7.2.50.
14.96/4.86	This system is of type 3 or smaller.
14.96/4.86	This system is deterministic.
14.96/4.86	System R transformed to optimized U(R).
14.96/4.86	This system is terminating.
14.96/4.86	Call external tool:
14.96/4.86	./ttt2.sh
14.96/4.86	Input:
14.96/4.86	(VAR x l y)
14.96/4.86	(RULES
14.96/4.86	  le(0, s(x)) -> true
14.96/4.86	  min(cons(x, l)) -> ?1(le(x, min(l)), x, l)
14.96/4.86	  ?1(false, x, l) -> min(l)
14.96/4.86	  le(s(x), s(y)) -> le(x, y)
14.96/4.86	  le(x, 0) -> false
14.96/4.86	  min(cons(x, l)) -> ?2(min(l), x, l)
14.96/4.86	  ?2(x, x, l) -> min(l)
14.96/4.86	  min(cons(x, l)) -> ?1(le(x, min(l)), x, l)
14.96/4.86	  ?1(true, x, l) -> x
14.96/4.86	  min(cons(x, nil)) -> x
14.96/4.86	)
14.96/4.86	
14.96/4.86	 Matrix Interpretation Processor: dim=1
14.96/4.86	  
14.96/4.86	  interpretation:
14.96/4.86	   [nil] = 0,
14.96/4.86	   
14.96/4.86	   [?2](x0, x1, x2) = x0 + 2x1 + 4x2 + 3,
14.96/4.86	   
14.96/4.86	   [false] = 0,
14.96/4.86	   
14.96/4.86	   [?1](x0, x1, x2) = 3x0 + 4x1 + 4x2 + 1,
14.96/4.86	   
14.96/4.86	   [min](x0) = 4x0 + 1,
14.96/4.86	   
14.96/4.86	   [cons](x0, x1) = 4x0 + 7x1 + 4,
14.96/4.86	   
14.96/4.86	   [true] = 2,
14.96/4.86	   
14.96/4.86	   [le](x0, x1) = x0 + 2x1 + 1,
14.96/4.86	   
14.96/4.86	   [s](x0) = 2x0,
14.96/4.86	   
14.96/4.86	   [0] = 2
14.96/4.86	  orientation:
14.96/4.86	   le(0(),s(x)) = 4x + 3 >= 2 = true()
14.96/4.86	   
14.96/4.86	   min(cons(x,l)) = 28l + 16x + 17 >= 28l + 7x + 10 = ?1(le(x,min(l)),x,l)
14.96/4.86	   
14.96/4.86	   ?1(false(),x,l) = 4l + 4x + 1 >= 4l + 1 = min(l)
14.96/4.86	   
14.96/4.86	   le(s(x),s(y)) = 2x + 4y + 1 >= x + 2y + 1 = le(x,y)
14.96/4.86	   
14.96/4.86	   le(x,0()) = x + 5 >= 0 = false()
14.96/4.86	   
14.96/4.86	   min(cons(x,l)) = 28l + 16x + 17 >= 8l + 2x + 4 = ?2(min(l),x,l)
15.35/4.89	   
15.35/4.89	   ?2(x,x,l) = 4l + 3x + 3 >= 4l + 1 = min(l)
15.35/4.89	   
15.35/4.89	   ?1(true(),x,l) = 4l + 4x + 7 >= x = x
15.35/4.89	   
15.35/4.89	   min(cons(x,nil())) = 16x + 17 >= x = x
15.35/4.89	  problem:
15.35/4.89	   ?1(false(),x,l) -> min(l)
15.35/4.89	   le(s(x),s(y)) -> le(x,y)
15.35/4.89	  Matrix Interpretation Processor: dim=3
15.35/4.89	   
15.35/4.89	   interpretation:
15.35/4.89	              [0]
15.35/4.89	    [false] = [0]
15.35/4.89	              [0],
15.35/4.89	    
15.35/4.89	                       [1 0 0]     [1 0 0]     [1 0 0]  
15.35/4.89	    [?1](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2
15.35/4.89	                       [0 0 0]     [0 0 0]     [0 0 0]  ,
15.35/4.89	    
15.35/4.89	                [1 0 0]  
15.35/4.89	    [min](x0) = [0 0 0]x0
15.35/4.89	                [0 0 0]  ,
15.35/4.89	    
15.35/4.89	                   [1 1 1]     [1 0 0]  
15.35/4.89	    [le](x0, x1) = [0 0 0]x0 + [0 0 0]x1
15.35/4.89	                   [0 0 0]     [0 0 0]  ,
15.35/4.89	    
15.35/4.89	              [1 0 0]     [0]
15.35/4.89	    [s](x0) = [0 0 0]x0 + [1]
15.43/4.94	              [0 1 1]     [0]
15.43/4.94	   orientation:
15.43/4.94	                      [1 0 0]    [1 0 0]     [1 0 0]          
15.43/4.94	    ?1(false(),x,l) = [0 0 0]l + [0 0 0]x >= [0 0 0]l = min(l)
15.43/4.94	                      [0 0 0]    [0 0 0]     [0 0 0]          
15.43/4.94	    
15.43/4.94	                    [1 1 1]    [1 0 0]    [1]    [1 1 1]    [1 0 0]           
15.43/4.94	    le(s(x),s(y)) = [0 0 0]x + [0 0 0]y + [0] >= [0 0 0]x + [0 0 0]y = le(x,y)
15.43/4.94	                    [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]           
15.43/4.94	   problem:
15.43/4.94	    ?1(false(),x,l) -> min(l)
15.43/4.94	   Matrix Interpretation Processor: dim=3
15.43/4.94	    
15.43/4.94	    interpretation:
15.43/4.94	               [0]
15.43/4.94	     [false] = [1]
15.43/4.94	               [0],
15.43/4.94	     
15.43/4.94	                        [1 0 0]     [1 0 0]     [1 0 0]     [1]
15.43/4.94	     [?1](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2 + [0]
15.43/4.94	                        [0 1 0]     [0 0 0]     [0 0 0]     [0],
15.43/4.94	     
15.43/4.94	                 [1 0 0]     [0]
15.43/4.94	     [min](x0) = [0 0 0]x0 + [0]
15.43/4.94	                 [0 0 0]     [1]
15.43/4.94	    orientation:
15.43/4.94	                       [1 0 0]    [1 0 0]    [1]    [1 0 0]    [0]         
15.43/4.94	     ?1(false(),x,l) = [0 0 0]l + [0 0 0]x + [0] >= [0 0 0]l + [0] = min(l)
15.43/4.94	                       [0 0 0]    [0 0 0]    [1]    [0 0 0]    [1]         
15.43/4.94	    problem:
15.43/4.94	     
15.43/4.94	    Qed
15.43/4.94	All 12 critical pairs are joinable.
15.43/4.94	Overlap: (rule1: min(cons(z, y)) -> min(y) <= le(z, min(y)) = false, rule2: min(cons(y', x')) -> min(x') <= min(x') = y', pos: ε, mgu: {(z,y'), (y,x')})
15.43/4.94	CP: min(x') = min(x') <= le(y', min(x')) = false, min(x') = y'
15.43/4.94	This critical pair is context-joinable.
15.43/4.94	Overlap: (rule1: min(cons(z, y)) -> min(y) <= min(y) = z, rule2: min(cons(x', nil)) -> x', pos: ε, mgu: {(z,x'), (y,nil)})
15.43/4.94	CP: x' = min(nil) <= min(nil) = x'
15.43/4.94	This critical pair is context-joinable.
15.43/4.94	Overlap: (rule1: min(cons(y, nil)) -> y, rule2: min(cons(x', z)) -> min(z) <= min(z) = x', pos: ε, mgu: {(y,x'), (z,nil)})
15.43/4.94	CP: min(nil) = x' <= min(nil) = x'
15.43/4.94	This critical pair is context-joinable.
15.43/4.94	Overlap: (rule1: min(cons(z, y)) -> z <= le(z, min(y)) = true, rule2: min(cons(y', x')) -> min(x') <= min(x') = y', pos: ε, mgu: {(z,y'), (y,x')})
15.43/4.94	CP: min(x') = y' <= le(y', min(x')) = true, min(x') = y'
15.43/4.94	This critical pair is context-joinable.
15.43/4.94	Overlap: (rule1: min(cons(y, nil)) -> y, rule2: min(cons(x', z)) -> min(z) <= le(x', min(z)) = false, pos: ε, mgu: {(y,x'), (z,nil)})
15.43/4.94	CP: min(nil) = x' <= le(x', min(nil)) = false
15.43/4.94	This critical pair is infeasible.
15.43/4.94	This critical pair is conditional.
15.43/4.94	This critical pair has some non-trivial conditions.
15.43/4.94	'tcap_{R_u}(le(x', min(nil)))' and 'false' are not unifiable.
15.43/4.94	Overlap: (rule1: min(cons(z, y)) -> z <= le(z, min(y)) = true, rule2: min(cons(y', x')) -> min(x') <= le(y', min(x')) = false, pos: ε, mgu: {(z,y'), (y,x')})
15.43/4.94	CP: min(x') = y' <= le(y', min(x')) = true, le(y', min(x')) = false
15.43/4.94	This critical pair is unfeasible.
15.43/4.94	Overlap: (rule1: min(cons(z, y)) -> z <= le(z, min(y)) = true, rule2: min(cons(x', nil)) -> x', pos: ε, mgu: {(z,x'), (y,nil)})
15.43/4.94	CP: x' = x' <= le(x', min(nil)) = true
15.43/4.94	This critical pair is context-joinable.
15.43/4.94	Overlap: (rule1: min(cons(y, nil)) -> y, rule2: min(cons(x', z)) -> x' <= le(x', min(z)) = true, pos: ε, mgu: {(y,x'), (z,nil)})
15.43/4.94	CP: x' = x' <= le(x', min(nil)) = true
15.43/4.94	This critical pair is context-joinable.
15.43/4.94	Overlap: (rule1: min(cons(z, y)) -> min(y) <= le(z, min(y)) = false, rule2: min(cons(y', x')) -> y' <= le(y', min(x')) = true, pos: ε, mgu: {(z,y'), (y,x')})
15.43/4.94	CP: y' = min(x') <= le(y', min(x')) = false, le(y', min(x')) = true
15.43/4.94	This critical pair is unfeasible.
15.43/4.94	Overlap: (rule1: min(cons(z, y)) -> min(y) <= min(y) = z, rule2: min(cons(y', x')) -> y' <= le(y', min(x')) = true, pos: ε, mgu: {(z,y'), (y,x')})
15.43/4.94	CP: y' = min(x') <= min(x') = y', le(y', min(x')) = true
15.43/4.94	This critical pair is context-joinable.
15.43/4.94	Overlap: (rule1: min(cons(z, y)) -> min(y) <= min(y) = z, rule2: min(cons(y', x')) -> min(x') <= le(y', min(x')) = false, pos: ε, mgu: {(z,y'), (y,x')})
15.43/4.94	CP: min(x') = min(x') <= min(x') = y', le(y', min(x')) = false
15.43/4.94	This critical pair is context-joinable.
15.43/4.94	Overlap: (rule1: min(cons(z, y)) -> min(y) <= le(z, min(y)) = false, rule2: min(cons(x', nil)) -> x', pos: ε, mgu: {(z,x'), (y,nil)})
15.43/4.94	CP: x' = min(nil) <= le(x', min(nil)) = false
15.43/4.94	This critical pair is infeasible.
15.43/4.94	This critical pair is conditional.
15.43/4.94	This critical pair has some non-trivial conditions.
15.43/4.94	'\Sigma(le(x', min(nil))) \cap (->^*_R)[\Sigma(REN(false))]' is empty by ETAC.
15.43/4.94	
15.43/4.95	EOF