We consider the system 469.

  Alphabet:

    all : [term -> form] --> form 
    and : [form * form] --> form 
    or : [form * form] --> form 

  Rules:

    all(/\x.X) => X 
    all(/\x.and(X(x), Y(x))) => and(all(X), all(Y)) 
    all(/\x.or(X(x), Y)) => or(all(X), Y) 
    all(/\x.or(X, Y(x))) => or(X, all(Y)) 

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

  all(/\x.X) >? X 
  all(/\x.and(X(x), Y(x))) >? and(all(X), all(Y)) 
  all(/\x.or(X(x), Y)) >? or(all(X), Y) 
  all(/\x.or(X, Y(x))) >? or(X, all(Y)) 

We orient these requirements with a polynomial interpretation in the natural numbers.

The following interpretation satisfies the requirements:

  all = \G0.3G0(0) 
  and = \y0y1.3 + y0 + y1 
  or = \y0y1.3 + y0 + y1 

Using this interpretation, the requirements translate to:

  [[all(/\x._x0)]] = 3x0 >= x0 = [[_x0]] 
  [[all(/\x.and(_x0(x), _x1(x)))]] = 9 + 3F0(0) + 3F1(0) > 3 + 3F0(0) + 3F1(0) = [[and(all(_x0), all(_x1))]] 
  [[all(/\x.or(_x0(x), _x1))]] = 9 + 3x1 + 3F0(0) > 3 + x1 + 3F0(0) = [[or(all(_x0), _x1)]] 
  [[all(/\x.or(_x0, _x1(x)))]] = 9 + 3x0 + 3F1(0) > 3 + x0 + 3F1(0) = [[or(_x0, all(_x1))]] 

We can thus remove the following rules:

  all(/\x.and(X(x), Y(x))) => and(all(X), all(Y)) 
  all(/\x.or(X(x), Y)) => or(all(X), Y) 
  all(/\x.or(X, Y(x))) => or(X, all(Y)) 

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

  all(/\x.X) >? X 

We orient these requirements with a polynomial interpretation in the natural numbers.

The following interpretation satisfies the requirements:

  all = \G0.1 + G0(0) 

Using this interpretation, the requirements translate to:

  [[all(/\x._x0)]] = 1 + x0 > x0 = [[_x0]] 

We can thus remove the following rules:

  all(/\x.X) => X 

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.


+++ Citations +++

[Kop12]  C. Kop.  Higher Order Termination.  PhD Thesis, 2012.