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 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 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 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 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