0.00/0.05	NO
0.00/0.05	
0.00/0.05	(RULES
0.00/0.05	pi(pi1(z),pi2(z))->z,
0.00/0.05	pi2(pi(z1,z2))->z2,
0.00/0.05	pi1(pi(z1,z2))->z1
0.00/0.05	)
0.00/0.05	
0.00/0.05	Determine termination by WANDA
0.00/0.05	
0.00/0.05	YES
0.00/0.05	We consider the system SMLNJ-LRt4rZ.
0.00/0.05	
0.00/0.05	  Alphabet:
0.00/0.05	
0.00/0.05	    pi : [term * term] --> term 
0.00/0.05	    pi1 : [term] --> term 
0.00/0.05	    pi2 : [term] --> term 
0.00/0.05	
0.00/0.05	  Rules:
0.00/0.05	
0.00/0.05	    pi(pi1(X), pi2(X)) => X 
0.00/0.05	    pi2(pi(X, Y)) => Y 
0.00/0.05	    pi1(pi(X, Y)) => X 
0.00/0.05	
0.00/0.05	We use rule removal, following [Kop12, Theorem 2.23].
0.00/0.05	
0.00/0.05	This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):
0.00/0.05	
0.00/0.05	  pi(pi1(X), pi2(X)) >? X 
0.00/0.05	  pi2(pi(X, Y)) >? Y 
0.00/0.05	  pi1(pi(X, Y)) >? X 
0.00/0.05	
0.00/0.05	We orient these requirements with a polynomial interpretations in the natural numbers.  
0.00/0.05	The following interpretation satisfies the requirements:
0.00/0.05	
0.00/0.05	  pi = \y0y1.3 + 3y0 + 3y1 
0.00/0.05	  pi1 = \y0.3 + 3y0 
0.00/0.05	  pi2 = \y0.3 + 3y0 
0.00/0.05	
0.00/0.05	Using this interpretation, the requirements translate to:
0.00/0.05	
0.00/0.05	  [[pi(pi1(_x0), pi2(_x0))]] = 21 + 18x0 > x0 = [[_x0]] 
0.00/0.05	  [[pi2(pi(_x0, _x1))]] = 12 + 9x0 + 9x1 > x1 = [[_x1]] 
0.00/0.05	  [[pi1(pi(_x0, _x1))]] = 12 + 9x0 + 9x1 > x0 = [[_x0]] 
0.00/0.05	
0.00/0.05	We can thus remove the following rules:
0.00/0.05	
0.00/0.05	  pi(pi1(X), pi2(X)) => X 
0.00/0.05	  pi2(pi(X, Y)) => Y 
0.00/0.05	  pi1(pi(X, Y)) => X 
0.00/0.05	
0.00/0.05	All rules were succesfully removed.  Thus, termination of the original system has been reduced to termination of the beta-rule, which is well-known to hold.
0.00/0.05	
0.00/0.05	
0.00/0.05	+++ Citations +++
0.00/0.05	
0.00/0.05	[Kop12]  C. Kop.  Higher Order Termination.  PhD Thesis, 2012.
0.00/0.05	
0.00/0.05	CP = 
0.00/0.05	[(pi(F38,F39),pi(pi1(pi(F38,F39)),F39))
0.00/0.05	(pi2(F46),pi2(F49))
0.00/0.05	(pi(F62,F63),pi(F62,pi2(pi(F62,F63))))
0.00/0.05	(pi1(F77),pi1(F77))
0.00/0.05	]
0.00/0.05	
0.00/0.05	pi(F38,F39) ->R* pi(F38,F39) |
0.00/0.05	pi(pi1(pi(F38,F39)),F39) ->R* pi(F38,F39)
0.00/0.05	<pi(F38,F39), pi(pi1(pi(F38,F39)),F39)>  joinable
0.00/0.05	
0.00/0.05	pi2(F46) ->R* pi2(F46) |
0.00/0.05	pi2(F49) ->R* pi2(F49)
0.00/0.05	<pi2(F46), pi2(F49)>  not joinable
0.00/0.05	
0.00/0.05	pi(F62,F63) ->R* pi(F62,F63) |
0.00/0.05	pi(F62,pi2(pi(F62,F63))) ->R* pi(F62,F63)
0.00/0.05	<pi(F62,F63), pi(F62,pi2(pi(F62,F63)))>  joinable
0.00/0.05	
0.00/0.05	pi1(F77) ->R* pi1(F77) |
0.00/0.05	pi1(F77) ->R* pi1(F77)
0.00/0.05	<pi1(F77), pi1(F77)>  joinable
0.00/0.05	
0.00/0.05	
0.00/0.05	This higher-order rewriting system is termination,but not all critical pairs are joinable.
0.00/0.05	
0.00/0.05	EOF