4.39/1.58	YES
4.39/1.58	
4.39/1.58	Problem:
4.39/1.58	a() -> c()
4.39/1.58	a() -> d()
4.39/1.58	b() -> c()
4.39/1.58	b() -> d()
4.39/1.58	c() -> e()
4.39/1.58	d() -> e()
4.39/1.58	k() -> e()
4.39/1.58	l() -> e()
4.39/1.58	s(c()) -> t(k())
4.39/1.58	s(c()) -> t(l())
4.39/1.58	s(e()) -> t(e())
4.39/1.58	g(x, x) -> h(x, x)
4.39/1.58	f(x) -> pair(x, y) <= s(x) = t(y)
4.39/1.58	
4.39/1.58	Proof:
4.39/1.58	This system is confluent.
4.39/1.58	By \cite{ALS94}, Theorem 4.1.
4.39/1.58	This system is of type 3 or smaller.
4.39/1.58	This system is strongly deterministic.
4.39/1.58	All 8 critical pairs are joinable.
4.39/1.58	CP: c() = d():
4.39/1.58	This critical pair is context-joinable.
4.39/1.58	CP: t(l()) = t(k()):
4.39/1.58	This critical pair is context-joinable.
4.39/1.58	CP: d() = c():
4.39/1.58	This critical pair is context-joinable.
4.39/1.58	CP: t(k()) = t(l()):
4.39/1.58	This critical pair is context-joinable.
4.39/1.58	CP: s(e()) = t(k()):
4.39/1.58	This critical pair is context-joinable.
4.39/1.58	CP: d() = c():
4.39/1.58	This critical pair is context-joinable.
4.39/1.58	CP: c() = d():
4.39/1.58	This critical pair is context-joinable.
4.39/1.58	CP: s(e()) = t(l()):
4.39/1.58	This critical pair is context-joinable.
4.39/1.58	This system is quasi-decreasing.
4.39/1.58	By \cite{A14}, Theorem 11.5.9.
4.39/1.58	This system is of type 3 or smaller.
4.39/1.58	This system is deterministic.
4.39/1.58	System R transformed to V(R) + Emb.
4.39/1.58	This system is terminating.
4.39/1.58	Call external tool:
4.39/1.58	./ttt2.sh
4.39/1.58	Input:
4.39/1.58	  a() -> c()
4.39/1.58	  a() -> d()
4.39/1.58	  b() -> c()
4.39/1.58	  b() -> d()
4.39/1.58	  c() -> e()
4.39/1.58	  d() -> e()
4.39/1.58	  k() -> e()
4.39/1.58	  l() -> e()
4.39/1.58	  s(c()) -> t(k())
4.39/1.58	  s(c()) -> t(l())
4.39/1.58	  s(e()) -> t(e())
4.39/1.58	  g(x, x) -> h(x, x)
4.39/1.58	  f(x) -> pair(x, s(x))
4.39/1.58	  f(x) -> s(x)
4.39/1.58	  h(x, y) -> x
4.39/1.58	  h(x, y) -> y
4.39/1.58	  pair(x, y) -> x
4.39/1.58	  pair(x, y) -> y
4.39/1.58	  s(x) -> x
4.39/1.58	  g(x, y) -> x
4.39/1.58	  g(x, y) -> y
4.39/1.58	  t(x) -> x
4.39/1.58	  f(x) -> x
4.39/1.58	
4.39/1.58	 Polynomial Interpretation Processor:
4.39/1.58	  dimension: 1
4.39/1.58	  interpretation:
4.39/1.58	   [pair](x0, x1) = 2x0 + x1 + x0x0 + 1,
4.39/1.58	   
4.39/1.58	   [f](x0) = 6x0 + 3x0x0 + 5,
4.39/1.58	   
4.39/1.59	   [h](x0, x1) = x0 + 2x1 + x0x0 + 2x1x1 + 1,
4.39/1.59	   
4.39/1.59	   [g](x0, x1) = 4x0 + 4x1 + 2x0x0 + 2x1x1 + 4,
4.39/1.59	   
4.39/1.59	   [t](x0) = x0 + 7,
4.39/1.59	   
4.39/1.59	   [s](x0) = 4x0 + 2x0x0 + 1,
4.39/1.59	   
4.39/1.59	   [l] = 4,
4.39/1.59	   
4.39/1.59	   [k] = 3,
4.39/1.59	   
4.39/1.59	   [e] = 2,
4.39/1.59	   
4.39/1.59	   [b] = 5,
4.39/1.59	   
4.39/1.59	   [d] = 4,
4.39/1.59	   
4.39/1.59	   [c] = 3,
4.39/1.59	   
4.39/1.59	   [a] = 5
4.39/1.59	  orientation:
4.39/1.59	   a() = 5 >= 3 = c()
4.39/1.59	   
4.39/1.59	   a() = 5 >= 4 = d()
4.39/1.59	   
4.39/1.59	   b() = 5 >= 3 = c()
4.39/1.59	   
4.39/1.59	   b() = 5 >= 4 = d()
4.39/1.59	   
4.39/1.59	   c() = 3 >= 2 = e()
4.39/1.59	   
4.39/1.59	   d() = 4 >= 2 = e()
4.39/1.59	   
4.39/1.59	   k() = 3 >= 2 = e()
4.39/1.59	   
4.39/1.59	   l() = 4 >= 2 = e()
4.39/1.59	   
4.39/1.59	   s(c()) = 31 >= 10 = t(k())
4.39/1.59	   
4.39/1.59	   s(c()) = 31 >= 11 = t(l())
4.39/1.59	   
4.39/1.59	   s(e()) = 17 >= 9 = t(e())
4.39/1.59	   
4.39/1.59	   g(x,x) = 8x + 4x*x + 4 >= 3x + 3x*x + 1 = h(x,x)
4.39/1.59	   
4.39/1.59	   f(x) = 6x + 3x*x + 5 >= 6x + 3x*x + 2 = pair(x,s(x))
4.39/1.59	   
4.39/1.59	   f(x) = 6x + 3x*x + 5 >= 4x + 2x*x + 1 = s(x)
4.39/1.59	   
4.39/1.59	   h(x,y) = x + x*x + 2y + 2y*y + 1 >= x = x
4.39/1.59	   
4.39/1.59	   h(x,y) = x + x*x + 2y + 2y*y + 1 >= y = y
4.39/1.59	   
4.39/1.59	   pair(x,y) = 2x + x*x + y + 1 >= x = x
4.39/1.59	   
4.39/1.59	   pair(x,y) = 2x + x*x + y + 1 >= y = y
4.39/1.59	   
4.39/1.59	   s(x) = 4x + 2x*x + 1 >= x = x
4.39/1.59	   
4.39/1.59	   g(x,y) = 4x + 2x*x + 4y + 2y*y + 4 >= x = x
4.39/1.59	   
4.39/1.59	   g(x,y) = 4x + 2x*x + 4y + 2y*y + 4 >= y = y
4.39/1.59	   
4.39/1.59	   t(x) = x + 7 >= x = x
4.39/1.59	   
4.39/1.59	   f(x) = 6x + 3x*x + 5 >= x = x
4.39/1.59	  problem:
4.39/1.59	   
4.39/1.59	  Qed
4.39/1.59	
5.21/1.73	EOF