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