16.46/5.13	YES
16.46/5.13	
16.46/5.13	Proof:
16.46/5.14	This system is confluent.
16.46/5.14	By \cite{ALS94}, Theorem 4.1.
16.46/5.14	This system is of type 3 or smaller.
16.84/5.20	This system is strongly deterministic.
16.84/5.20	This system is quasi-decreasing.
16.84/5.20	By \cite{A14}, Theorem 11.5.9.
16.84/5.20	This system is of type 3 or smaller.
16.84/5.20	This system is deterministic.
16.84/5.20	System R transformed to V(R) + Emb.
16.84/5.20	This system is terminating.
16.84/5.20	Call external tool:
16.84/5.20	./ttt2.sh
16.84/5.20	Input:
16.84/5.20	(VAR x y l)
16.84/5.20	(RULES
16.84/5.20	  le(0, s(x)) -> true
16.84/5.20	  le(x, 0) -> false
16.84/5.20	  le(s(x), s(y)) -> le(x, y)
16.84/5.20	  min(cons(x, nil)) -> x
16.84/5.20	  min(cons(x, l)) -> x
16.84/5.20	  min(cons(x, l)) -> le(x, min(l))
16.84/5.20	  min(cons(x, l)) -> min(l)
16.84/5.20	  s(x) -> x
16.84/5.20	  min(x) -> x
16.84/5.20	  le(x, y) -> x
16.84/5.20	  le(x, y) -> y
16.84/5.20	  cons(x, y) -> x
16.84/5.20	  cons(x, y) -> y
16.84/5.20	)
16.84/5.20	
16.84/5.20	 Matrix Interpretation Processor: dim=1
16.84/5.20	  
16.84/5.20	  interpretation:
16.84/5.20	   [min](x0) = 4x0 + 3,
16.84/5.20	   
16.84/5.20	   [cons](x0, x1) = 5x0 + 4x1 + 5,
16.84/5.20	   
16.84/5.20	   [nil] = 0,
16.84/5.20	   
16.84/5.20	   [false] = 0,
16.84/5.20	   
16.84/5.21	   [true] = 0,
16.84/5.21	   
16.84/5.21	   [le](x0, x1) = x0 + 4x1 + 4,
16.84/5.21	   
16.84/5.21	   [s](x0) = x0 + 1,
16.84/5.21	   
16.84/5.21	   [0] = 5
16.84/5.21	  orientation:
16.84/5.21	   le(0(),s(x)) = 4x + 13 >= 0 = true()
16.84/5.21	   
16.84/5.21	   le(x,0()) = x + 24 >= 0 = false()
16.84/5.21	   
16.84/5.21	   le(s(x),s(y)) = x + 4y + 9 >= x + 4y + 4 = le(x,y)
16.84/5.21	   
16.84/5.21	   min(cons(x,nil())) = 20x + 23 >= x = x
16.84/5.21	   
16.84/5.21	   min(cons(x,l)) = 16l + 20x + 23 >= x = x
16.84/5.21	   
16.84/5.21	   min(cons(x,l)) = 16l + 20x + 23 >= 16l + x + 16 = le(x,min(l))
16.84/5.21	   
16.84/5.21	   min(cons(x,l)) = 16l + 20x + 23 >= 4l + 3 = min(l)
16.84/5.21	   
16.84/5.21	   s(x) = x + 1 >= x = x
16.84/5.21	   
16.84/5.21	   min(x) = 4x + 3 >= x = x
16.84/5.21	   
16.84/5.21	   le(x,y) = x + 4y + 4 >= x = x
16.84/5.21	   
16.84/5.21	   le(x,y) = x + 4y + 4 >= y = y
16.84/5.21	   
16.84/5.21	   cons(x,y) = 5x + 4y + 5 >= x = x
16.84/5.21	   
16.84/5.21	   cons(x,y) = 5x + 4y + 5 >= y = y
16.84/5.21	  problem:
16.84/5.21	   
16.84/5.21	  Qed
16.84/5.21	All 12 critical pairs are joinable.
16.84/5.21	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')})
16.84/5.21	CP: min(x') = min(x') <= le(y', min(x')) = false, min(x') = y'
16.84/5.21	This critical pair is context-joinable.
16.84/5.21	Overlap: (rule1: min(cons(z, y)) -> min(y) <= min(y) = z, rule2: min(cons(x', nil)) -> x', pos: ε, mgu: {(z,x'), (y,nil)})
16.84/5.21	CP: x' = min(nil) <= min(nil) = x'
16.84/5.21	This critical pair is context-joinable.
16.84/5.21	Overlap: (rule1: min(cons(y, nil)) -> y, rule2: min(cons(x', z)) -> min(z) <= min(z) = x', pos: ε, mgu: {(y,x'), (z,nil)})
16.84/5.21	CP: min(nil) = x' <= min(nil) = x'
16.84/5.21	This critical pair is context-joinable.
16.84/5.21	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')})
16.84/5.21	CP: min(x') = y' <= le(y', min(x')) = true, min(x') = y'
16.84/5.21	This critical pair is context-joinable.
16.84/5.21	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)})
16.84/5.21	CP: min(nil) = x' <= le(x', min(nil)) = false
16.84/5.21	This critical pair is infeasible.
16.84/5.21	This critical pair is conditional.
16.84/5.21	This critical pair has some non-trivial conditions.
16.84/5.21	'tcap_{R_u}(le(x', min(nil)))' and 'false' are not unifiable.
16.84/5.21	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')})
16.84/5.21	CP: min(x') = y' <= le(y', min(x')) = true, le(y', min(x')) = false
16.84/5.21	This critical pair is unfeasible.
16.84/5.21	Overlap: (rule1: min(cons(z, y)) -> z <= le(z, min(y)) = true, rule2: min(cons(x', nil)) -> x', pos: ε, mgu: {(z,x'), (y,nil)})
16.84/5.21	CP: x' = x' <= le(x', min(nil)) = true
16.84/5.21	This critical pair is infeasible.
16.84/5.21	This critical pair is conditional.
16.84/5.21	This critical pair has some non-trivial conditions.
16.84/5.21	'\Sigma(le(x', min(nil))) \cap (->^*_R)[\Sigma(REN(true))]' is empty by ETAC.
16.84/5.21	Overlap: (rule1: min(cons(y, nil)) -> y, rule2: min(cons(x', z)) -> x' <= le(x', min(z)) = true, pos: ε, mgu: {(y,x'), (z,nil)})
16.84/5.21	CP: x' = x' <= le(x', min(nil)) = true
16.84/5.21	This critical pair is infeasible.
16.84/5.21	This critical pair is conditional.
16.84/5.21	This critical pair has some non-trivial conditions.
16.84/5.21	'tcap_{R_u}(le(x', min(nil)))' and 'true' are not unifiable.
16.84/5.21	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')})
16.84/5.21	CP: y' = min(x') <= le(y', min(x')) = false, le(y', min(x')) = true
16.84/5.21	This critical pair is unfeasible.
16.84/5.21	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')})
16.84/5.21	CP: y' = min(x') <= min(x') = y', le(y', min(x')) = true
16.84/5.21	This critical pair is context-joinable.
16.84/5.21	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')})
16.84/5.21	CP: min(x') = min(x') <= min(x') = y', le(y', min(x')) = false
16.84/5.21	This critical pair is context-joinable.
16.84/5.21	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)})
16.84/5.21	CP: x' = min(nil) <= le(x', min(nil)) = false
16.84/5.21	This critical pair is infeasible.
16.84/5.21	This critical pair is conditional.
16.84/5.21	This critical pair has some non-trivial conditions.
16.84/5.21	'tcap_{R_u}(le(x', min(nil)))' and 'false' are not unifiable.
16.84/5.21	
17.28/5.36	EOF