We consider the system 459.

  Alphabet:

    and : [form * form] --> form 
    exists : [term -> form] --> form 
    forall : [term -> form] --> form 
    neg : [form] --> form 
    or : [form * form] --> form 

  Rules:

    neg(neg(X)) => X 
    neg(and(X, Y)) => or(neg(X), neg(Y)) 
    neg(or(X, Y)) => and(neg(X), neg(Y)) 
    neg(forall(/\x.X(x))) => exists(/\y.neg(X(y))) 
    neg(exists(/\x.X(x))) => forall(/\y.neg(X(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, formative):

  Dependency Pairs P_0:

    0] neg#(and(X, Y)) =#> neg#(X)   
    1] neg#(and(X, Y)) =#> neg#(Y)   
    2] neg#(or(X, Y)) =#> neg#(X)   
    3] neg#(or(X, Y)) =#> neg#(Y)   
    4] neg#(forall(/\x.X(x))) =#> neg#(X(y))   
    5] neg#(forall(/\x.X(x))) =#> X(y)   
    6] neg#(exists(/\x.X(x))) =#> neg#(X(y))   
    7] neg#(exists(/\x.X(x))) =#> X(y)   

  Rules R_0:

    neg(neg(X)) => X 
    neg(and(X, Y)) => or(neg(X), neg(Y)) 
    neg(or(X, Y)) => and(neg(X), neg(Y)) 
    neg(forall(/\x.X(x))) => exists(/\y.neg(X(y))) 
    neg(exists(/\x.X(x))) => forall(/\y.neg(X(y))) 

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

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

We will use the reduction pair processor [Kop12, Thm. 7.16].  As the system is abstraction-simple and the formative flag is set, it suffices to find a tagged reduction pair [Kop12, Def. 6.70].  Thus, we must orient:

  neg#(and(X, Y)) >? neg#(X) 
  neg#(and(X, Y)) >? neg#(Y) 
  neg#(or(X, Y)) >? neg#(X) 
  neg#(or(X, Y)) >? neg#(Y) 
  neg#(forall(/\x.X(x))) >? neg#(X(~c0)) 
  neg#(forall(/\x.X(x))) >? X(~c1) 
  neg#(exists(/\x.X(x))) >? neg#(X(~c2)) 
  neg#(exists(/\x.X(x))) >? X(~c3) 
  neg(neg(X)) >= X 
  neg(and(X, Y)) >= or(neg(X), neg(Y)) 
  neg(or(X, Y)) >= and(neg(X), neg(Y)) 
  neg(forall(/\x.X(x))) >= exists(/\y.neg-(X(y))) 
  neg(exists(/\x.X(x))) >= forall(/\y.neg-(X(y))) 
  neg-(X) >= neg(X) 
  neg-(X) >= neg#(X) 

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

The following interpretation satisfies the requirements:

  and = \y0y1.1 + y0 + 2y1 
  exists = \G0.2G0(0) 
  forall = \G0.2G0(0) 
  neg = \y0.y0 
  neg- = \y0.y0 
  neg# = \y0.y0 
  or = \y0y1.1 + y0 + 2y1 
  ~c0 = 0 
  ~c1 = 0 
  ~c2 = 0 
  ~c3 = 0 

Using this interpretation, the requirements translate to:

  [[neg#(and(_x0, _x1))]] = 1 + x0 + 2x1 > x0 = [[neg#(_x0)]] 
  [[neg#(and(_x0, _x1))]] = 1 + x0 + 2x1 > x1 = [[neg#(_x1)]] 
  [[neg#(or(_x0, _x1))]] = 1 + x0 + 2x1 > x0 = [[neg#(_x0)]] 
  [[neg#(or(_x0, _x1))]] = 1 + x0 + 2x1 > x1 = [[neg#(_x1)]] 
  [[neg#(forall(/\x._x0(x)))]] = 2F0(0) >= F0(0) = [[neg#(_x0(~c0))]] 
  [[neg#(forall(/\x._x0(x)))]] = 2F0(0) >= F0(0) = [[_x0(~c1)]] 
  [[neg#(exists(/\x._x0(x)))]] = 2F0(0) >= F0(0) = [[neg#(_x0(~c2))]] 
  [[neg#(exists(/\x._x0(x)))]] = 2F0(0) >= F0(0) = [[_x0(~c3)]] 
  [[neg(neg(_x0))]] = x0 >= x0 = [[_x0]] 
  [[neg(and(_x0, _x1))]] = 1 + x0 + 2x1 >= 1 + x0 + 2x1 = [[or(neg(_x0), neg(_x1))]] 
  [[neg(or(_x0, _x1))]] = 1 + x0 + 2x1 >= 1 + x0 + 2x1 = [[and(neg(_x0), neg(_x1))]] 
  [[neg(forall(/\x._x0(x)))]] = 2F0(0) >= 2F0(0) = [[exists(/\x.neg-(_x0(x)))]] 
  [[neg(exists(/\x._x0(x)))]] = 2F0(0) >= 2F0(0) = [[forall(/\x.neg-(_x0(x)))]] 
  [[neg-(_x0)]] = x0 >= x0 = [[neg(_x0)]] 
  [[neg-(_x0)]] = x0 >= x0 = [[neg#(_x0)]] 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_0, R_0, minimal, formative) by (P_1, R_0, minimal, formative), where P_1 consists of:

  neg#(forall(/\x.X(x))) =#> neg#(X(y))   
  neg#(forall(/\x.X(x))) =#> X(y)   
  neg#(exists(/\x.X(x))) =#> neg#(X(y))   
  neg#(exists(/\x.X(x))) =#> X(y)   

Thus, the original system is terminating if (P_1, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_1, R_0, minimal, formative).

The formative rules of (P_1, R_0) are R_1 ::=

  neg(neg(X)) => X 
  neg(forall(/\x.X(x))) => exists(/\y.neg(X(y))) 
  neg(exists(/\x.X(x))) => forall(/\y.neg(X(y))) 

By [Kop12, Thm. 7.17], we may replace the dependency pair problem (P_1, R_0, minimal, formative) by (P_1, R_1, minimal, formative).

Thus, the original system is terminating if (P_1, R_1, minimal, formative) is finite.

We consider the dependency pair problem (P_1, R_1, minimal, formative).

We will use the reduction pair processor [Kop12, Thm. 7.16].  As the system is abstraction-simple and the formative flag is set, it suffices to find a tagged reduction pair [Kop12, Def. 6.70].  Thus, we must orient:

  neg#(forall(/\x.X(x))) >? neg#(X(~c0)) 
  neg#(forall(/\x.X(x))) >? X(~c1) 
  neg#(exists(/\x.X(x))) >? neg#(X(~c2)) 
  neg#(exists(/\x.X(x))) >? X(~c3) 
  neg(neg(X)) >= X 
  neg(forall(/\x.X(x))) >= exists(/\y.neg-(X(y))) 
  neg(exists(/\x.X(x))) >= forall(/\y.neg-(X(y))) 
  neg-(X) >= neg(X) 
  neg-(X) >= neg#(X) 

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

The following interpretation satisfies the requirements:

  exists = \G0.1 + 2G0(0) 
  forall = \G0.1 + 2G0(0) 
  neg = \y0.y0 
  neg- = \y0.y0 
  neg# = \y0.y0 
  ~c0 = 0 
  ~c1 = 0 
  ~c2 = 0 
  ~c3 = 0 

Using this interpretation, the requirements translate to:

  [[neg#(forall(/\x._x0(x)))]] = 1 + 2F0(0) > F0(0) = [[neg#(_x0(~c0))]] 
  [[neg#(forall(/\x._x0(x)))]] = 1 + 2F0(0) > F0(0) = [[_x0(~c1)]] 
  [[neg#(exists(/\x._x0(x)))]] = 1 + 2F0(0) > F0(0) = [[neg#(_x0(~c2))]] 
  [[neg#(exists(/\x._x0(x)))]] = 1 + 2F0(0) > F0(0) = [[_x0(~c3)]] 
  [[neg(neg(_x0))]] = x0 >= x0 = [[_x0]] 
  [[neg(forall(/\x._x0(x)))]] = 1 + 2F0(0) >= 1 + 2F0(0) = [[exists(/\x.neg-(_x0(x)))]] 
  [[neg(exists(/\x._x0(x)))]] = 1 + 2F0(0) >= 1 + 2F0(0) = [[forall(/\x.neg-(_x0(x)))]] 
  [[neg-(_x0)]] = x0 >= x0 = [[neg(_x0)]] 
  [[neg-(_x0)]] = x0 >= x0 = [[neg#(_x0)]] 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_1, R_1) by ({}, R_1).  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.