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