We consider the system 427.

  Alphabet:

    all : [T -> F] --> F 
    and : [F * F] --> F 
    ex : [T -> F] --> F 
    not : [F] --> F 
    or : [F * F] --> F 

  Rules:

    and(X, all(/\x.Y(x))) => all(/\y.and(X, Y(y))) 
    and(all(/\x.X(x)), Y) => all(/\y.and(X(y), Y)) 
    or(X, all(/\x.Y(x))) => all(/\y.or(X, Y(y))) 
    or(all(/\x.X(x)), Y) => all(/\y.or(X(y), Y)) 
    and(X, ex(/\x.Y(x))) => ex(/\y.and(X, Y(y))) 
    and(ex(/\x.X(x)), Y) => ex(/\y.and(X(y), Y)) 
    or(X, ex(/\x.Y(x))) => ex(/\y.or(X, Y(y))) 
    or(ex(/\x.X(x)), Y) => ex(/\y.or(X(y), Y)) 
    not(all(/\x.X(x))) => ex(/\y.not(X(y))) 
    not(ex(/\x.X(x))) => all(/\y.not(X(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]):

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

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

The following interpretation satisfies the requirements:

  all = \G0.1 + G0(0) 
  and = \y0y1.y1 + 2y0 
  ex = \G0.1 + G0(0) 
  not = \y0.2y0 
  or = \y0y1.y1 + 2y0 

Using this interpretation, the requirements translate to:

  [[and(_x0, all(/\x._x1(x)))]] = 1 + 2x0 + F1(0) >= 1 + 2x0 + F1(0) = [[all(/\x.and(_x0, _x1(x)))]] 
  [[and(all(/\x._x0(x)), _x1)]] = 2 + x1 + 2F0(0) > 1 + x1 + 2F0(0) = [[all(/\x.and(_x0(x), _x1))]] 
  [[or(_x0, all(/\x._x1(x)))]] = 1 + 2x0 + F1(0) >= 1 + 2x0 + F1(0) = [[all(/\x.or(_x0, _x1(x)))]] 
  [[or(all(/\x._x0(x)), _x1)]] = 2 + x1 + 2F0(0) > 1 + x1 + 2F0(0) = [[all(/\x.or(_x0(x), _x1))]] 
  [[and(_x0, ex(/\x._x1(x)))]] = 1 + 2x0 + F1(0) >= 1 + 2x0 + F1(0) = [[ex(/\x.and(_x0, _x1(x)))]] 
  [[and(ex(/\x._x0(x)), _x1)]] = 2 + x1 + 2F0(0) > 1 + x1 + 2F0(0) = [[ex(/\x.and(_x0(x), _x1))]] 
  [[or(_x0, ex(/\x._x1(x)))]] = 1 + 2x0 + F1(0) >= 1 + 2x0 + F1(0) = [[ex(/\x.or(_x0, _x1(x)))]] 
  [[or(ex(/\x._x0(x)), _x1)]] = 2 + x1 + 2F0(0) > 1 + x1 + 2F0(0) = [[ex(/\x.or(_x0(x), _x1))]] 
  [[not(all(/\x._x0(x)))]] = 2 + 2F0(0) > 1 + 2F0(0) = [[ex(/\x.not(_x0(x)))]] 
  [[not(ex(/\x._x0(x)))]] = 2 + 2F0(0) > 1 + 2F0(0) = [[all(/\x.not(_x0(x)))]] 

We can thus remove the following rules:

  and(all(/\x.X(x)), Y) => all(/\y.and(X(y), Y)) 
  or(all(/\x.X(x)), Y) => all(/\y.or(X(y), Y)) 
  and(ex(/\x.X(x)), Y) => ex(/\y.and(X(y), Y)) 
  or(ex(/\x.X(x)), Y) => ex(/\y.or(X(y), Y)) 
  not(all(/\x.X(x))) => ex(/\y.not(X(y))) 
  not(ex(/\x.X(x))) => all(/\y.not(X(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]):

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

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

The following interpretation satisfies the requirements:

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

Using this interpretation, the requirements translate to:

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

We can thus remove the following rules:

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

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.