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 the dependency pair framework as described in [Kop12, Ch. 6/7], with dynamic dependency pairs.

We thus obtain the following dependency pair problem (P_0, R_0, minimal, all):

  Dependency Pairs P_0:

    0] all#(/\x.and(X(x), Y(x))) =#> all#(X)   
    1] all#(/\x.and(X(x), Y(x))) =#> all#(Y)   
    2] all#(/\x.or(X(x), Y)) =#> all#(X)   
    3] all#(/\x.or(X, Y(x))) =#> all#(Y)   

  Rules R_0:

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

Thus, the original system is terminating if (P_0, R_0, minimal, all) is finite.

We consider the dependency pair problem (P_0, R_0, minimal, all).

We will use the reduction pair processor with usable rules [Kop12, Thm. 7.44].  (P_0, R_0) has no usable rules.

It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

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

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

The following interpretation satisfies the requirements:

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

Using this interpretation, the requirements translate to:

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

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_0, R_0) by ({}, R_0).  By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed.

As all dependency pair problems were succesfully simplified with sound (and complete) processors until nothing remained, we conclude termination.


+++ Citations +++

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