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