We consider the system prenex.

  Alphabet:

    and : [form * form] --> form 
    exists : [form -> form] --> form 
    forall : [form -> form] --> form 
    not : [form] --> form 
    or : [form * form] --> form 

  Rules:

    and(x, forall(/\y.f y)) => forall(/\z.and(x, f z)) 
    or(x, forall(/\y.f y)) => forall(/\z.or(x, f z)) 
    and(forall(/\x.f x), y) => forall(/\z.and(f z, y)) 
    or(forall(/\x.f x), y) => forall(/\z.or(f z, y)) 
    not(forall(/\x.f x)) => exists(/\y.not(f y)) 
    and(x, exists(/\y.f y)) => exists(/\z.and(x, f z)) 
    or(x, exists(/\y.f y)) => exists(/\z.or(x, f z)) 
    and(exists(/\x.f x), y) => exists(/\z.and(f z, y)) 
    or(exists(/\x.f x), y) => exists(/\z.or(f z, y)) 
    not(exists(/\x.f x)) => forall(/\y.not(f y)) 

Using the transformations described in [Kop11], this system can be brought in a form without leading free variables in the left-hand side, and where the left-hand side of a variable is always a functional term or application headed by a functional term.

We now transform the resulting AFS into an AFSM by replacing all free variables by meta-variables (with arity 0).  This leads to the following AFSM:

  Alphabet:

    and : [form * form] --> form 
    exists : [form -> form] --> form 
    forall : [form -> form] --> form 
    not : [form] --> form 
    or : [form * form] --> form 
    ~AP1 : [form -> form * form] --> form 

  Rules:

    and(X, forall(/\x.~AP1(F, x))) => forall(/\y.and(X, ~AP1(F, y))) 
    or(X, forall(/\x.~AP1(F, x))) => forall(/\y.or(X, ~AP1(F, y))) 
    and(forall(/\x.~AP1(F, x)), X) => forall(/\y.and(~AP1(F, y), X)) 
    or(forall(/\x.~AP1(F, x)), X) => forall(/\y.or(~AP1(F, y), X)) 
    not(forall(/\x.~AP1(F, x))) => exists(/\y.not(~AP1(F, y))) 
    and(X, exists(/\x.~AP1(F, x))) => exists(/\y.and(X, ~AP1(F, y))) 
    or(X, exists(/\x.~AP1(F, x))) => exists(/\y.or(X, ~AP1(F, y))) 
    and(exists(/\x.~AP1(F, x)), X) => exists(/\y.and(~AP1(F, y), X)) 
    or(exists(/\x.~AP1(F, x)), X) => exists(/\y.or(~AP1(F, y), X)) 
    not(exists(/\x.~AP1(F, x))) => forall(/\y.not(~AP1(F, y))) 
    ~AP1(F, X) => F X 

We use the dependency pair framework as described in [Kop12, Ch. 6/7], with dynamic dependency pairs.

After applying [Kop12, Thm. 7.22] to denote collapsing dependency pairs in an extended form, we thus obtain the following dependency pair problem (P_0, R_0, minimal, all):

  Dependency Pairs P_0:

    0] and#(X, forall(/\x.~AP1(F, x))) =#> and#(X, ~AP1(F, y))   
    1] and#(X, forall(/\x.~AP1(F, x))) =#> ~AP1#(F, y)   
    2] or#(X, forall(/\x.~AP1(F, x))) =#> or#(X, ~AP1(F, y))   
    3] or#(X, forall(/\x.~AP1(F, x))) =#> ~AP1#(F, y)   
    4] and#(forall(/\x.~AP1(F, x)), X) =#> and#(~AP1(F, y), X)   
    5] and#(forall(/\x.~AP1(F, x)), X) =#> ~AP1#(F, y)   
    6] or#(forall(/\x.~AP1(F, x)), X) =#> or#(~AP1(F, y), X)   
    7] or#(forall(/\x.~AP1(F, x)), X) =#> ~AP1#(F, y)   
    8] not#(forall(/\x.~AP1(F, x))) =#> not#(~AP1(F, y))   
    9] not#(forall(/\x.~AP1(F, x))) =#> ~AP1#(F, y)   
    10] and#(X, exists(/\x.~AP1(F, x))) =#> and#(X, ~AP1(F, y))   
    11] and#(X, exists(/\x.~AP1(F, x))) =#> ~AP1#(F, y)   
    12] or#(X, exists(/\x.~AP1(F, x))) =#> or#(X, ~AP1(F, y))   
    13] or#(X, exists(/\x.~AP1(F, x))) =#> ~AP1#(F, y)   
    14] and#(exists(/\x.~AP1(F, x)), X) =#> and#(~AP1(F, y), X)   
    15] and#(exists(/\x.~AP1(F, x)), X) =#> ~AP1#(F, y)   
    16] or#(exists(/\x.~AP1(F, x)), X) =#> or#(~AP1(F, y), X)   
    17] or#(exists(/\x.~AP1(F, x)), X) =#> ~AP1#(F, y)   
    18] not#(exists(/\x.~AP1(F, x))) =#> not#(~AP1(F, y))   
    19] not#(exists(/\x.~AP1(F, x))) =#> ~AP1#(F, y)   
    20] ~AP1#(F, X) =#> F(X)   

  Rules R_0:

    and(X, forall(/\x.~AP1(F, x))) => forall(/\y.and(X, ~AP1(F, y))) 
    or(X, forall(/\x.~AP1(F, x))) => forall(/\y.or(X, ~AP1(F, y))) 
    and(forall(/\x.~AP1(F, x)), X) => forall(/\y.and(~AP1(F, y), X)) 
    or(forall(/\x.~AP1(F, x)), X) => forall(/\y.or(~AP1(F, y), X)) 
    not(forall(/\x.~AP1(F, x))) => exists(/\y.not(~AP1(F, y))) 
    and(X, exists(/\x.~AP1(F, x))) => exists(/\y.and(X, ~AP1(F, y))) 
    or(X, exists(/\x.~AP1(F, x))) => exists(/\y.or(X, ~AP1(F, y))) 
    and(exists(/\x.~AP1(F, x)), X) => exists(/\y.and(~AP1(F, y), X)) 
    or(exists(/\x.~AP1(F, x)), X) => exists(/\y.or(~AP1(F, y), X)) 
    not(exists(/\x.~AP1(F, x))) => forall(/\y.not(~AP1(F, y))) 
    ~AP1(F, X) => F X 

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 place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows:

    * 0 : 0, 1, 4, 5, 10, 11, 14, 15 
    * 1 :  
    * 2 : 2, 3, 6, 7, 12, 13, 16, 17 
    * 3 :  
    * 4 : 0, 1, 4, 5, 10, 11, 14, 15 
    * 5 :  
    * 6 : 2, 3, 6, 7, 12, 13, 16, 17 
    * 7 :  
    * 8 : 8, 9, 18, 19 
    * 9 :  
    * 10 : 0, 1, 4, 5, 10, 11, 14, 15 
    * 11 :  
    * 12 : 2, 3, 6, 7, 12, 13, 16, 17 
    * 13 :  
    * 14 : 0, 1, 4, 5, 10, 11, 14, 15 
    * 15 :  
    * 16 : 2, 3, 6, 7, 12, 13, 16, 17 
    * 17 :  
    * 18 : 8, 9, 18, 19 
    * 19 :  
    * 20 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20 

This graph has the following strongly connected components:

  P_1:

    and#(X, forall(/\x.~AP1(F, x))) =#> and#(X, ~AP1(F, y))   
    and#(forall(/\x.~AP1(F, x)), X) =#> and#(~AP1(F, y), X)   
    and#(X, exists(/\x.~AP1(F, x))) =#> and#(X, ~AP1(F, y))   
    and#(exists(/\x.~AP1(F, x)), X) =#> and#(~AP1(F, y), X)   

  P_2:

    or#(X, forall(/\x.~AP1(F, x))) =#> or#(X, ~AP1(F, y))   
    or#(forall(/\x.~AP1(F, x)), X) =#> or#(~AP1(F, y), X)   
    or#(X, exists(/\x.~AP1(F, x))) =#> or#(X, ~AP1(F, y))   
    or#(exists(/\x.~AP1(F, x)), X) =#> or#(~AP1(F, y), X)   

  P_3:

    not#(forall(/\x.~AP1(F, x))) =#> not#(~AP1(F, y))   
    not#(exists(/\x.~AP1(F, x))) =#> not#(~AP1(F, y))   

  P_4:

    ~AP1#(F, X) =#> F(X)   

By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_0, R_0, m, f) by (P_1, R_0, m, f), (P_2, R_0, m, f), (P_3, R_0, m, f) and (P_4, R_0, m, f).

Thus, the original system is terminating if each of (P_1, R_0, minimal, all), (P_2, R_0, minimal, all), (P_3, R_0, minimal, all) and (P_4, R_0, minimal, all) is finite.

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

We will use the reduction pair processor [Kop12, Thm. 7.16].  It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  ~AP1#(F, X) >? F(X) 
  and(X, forall(/\x.~AP1(F, x))) >= forall(/\y.and(X, ~AP1(F, y))) 
  or(X, forall(/\x.~AP1(F, x))) >= forall(/\y.or(X, ~AP1(F, y))) 
  and(forall(/\x.~AP1(F, x)), X) >= forall(/\y.and(~AP1(F, y), X)) 
  or(forall(/\x.~AP1(F, x)), X) >= forall(/\y.or(~AP1(F, y), X)) 
  not(forall(/\x.~AP1(F, x))) >= exists(/\y.not(~AP1(F, y))) 
  and(X, exists(/\x.~AP1(F, x))) >= exists(/\y.and(X, ~AP1(F, y))) 
  or(X, exists(/\x.~AP1(F, x))) >= exists(/\y.or(X, ~AP1(F, y))) 
  and(exists(/\x.~AP1(F, x)), X) >= exists(/\y.and(~AP1(F, y), X)) 
  or(exists(/\x.~AP1(F, x)), X) >= exists(/\y.or(~AP1(F, y), X)) 
  not(exists(/\x.~AP1(F, x))) >= forall(/\y.not(~AP1(F, y))) 
  ~AP1(F, X) >= F X 
  ~AP1(F, X) >= ~AP1#(F, X) 

We apply [Kop12, Thm. 6.75] and use the following argument functions:

  pi( ~AP1#(F, X) ) = #argfun-~AP1##(F X) 

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

The following interpretation satisfies the requirements:

  #argfun-~AP1## = \y0.1 + y0 
  and = \y0y1.y0 + y1 
  exists = \G0.G0(0) 
  forall = \G0.G0(0) 
  not = \y0.y0 
  or = \y0y1.y0 + y1 
  ~AP1 = \G0y1.1 + y1 + G0(0) + G0(y1) 
  ~AP1# = \G0y1.0 

Using this interpretation, the requirements translate to:

  [[#argfun-~AP1##(_F0 _x1)]] = 1 + max(x1, F0(x1)) > F0(x1) = [[_F0(_x1)]] 
  [[and(_x0, forall(/\x.~AP1(_F1, x)))]] = 1 + x0 + 2F1(0) >= 1 + x0 + 2F1(0) = [[forall(/\x.and(_x0, ~AP1(_F1, x)))]] 
  [[or(_x0, forall(/\x.~AP1(_F1, x)))]] = 1 + x0 + 2F1(0) >= 1 + x0 + 2F1(0) = [[forall(/\x.or(_x0, ~AP1(_F1, x)))]] 
  [[and(forall(/\x.~AP1(_F0, x)), _x1)]] = 1 + x1 + 2F0(0) >= 1 + x1 + 2F0(0) = [[forall(/\x.and(~AP1(_F0, x), _x1))]] 
  [[or(forall(/\x.~AP1(_F0, x)), _x1)]] = 1 + x1 + 2F0(0) >= 1 + x1 + 2F0(0) = [[forall(/\x.or(~AP1(_F0, x), _x1))]] 
  [[not(forall(/\x.~AP1(_F0, x)))]] = 1 + 2F0(0) >= 1 + 2F0(0) = [[exists(/\x.not(~AP1(_F0, x)))]] 
  [[and(_x0, exists(/\x.~AP1(_F1, x)))]] = 1 + x0 + 2F1(0) >= 1 + x0 + 2F1(0) = [[exists(/\x.and(_x0, ~AP1(_F1, x)))]] 
  [[or(_x0, exists(/\x.~AP1(_F1, x)))]] = 1 + x0 + 2F1(0) >= 1 + x0 + 2F1(0) = [[exists(/\x.or(_x0, ~AP1(_F1, x)))]] 
  [[and(exists(/\x.~AP1(_F0, x)), _x1)]] = 1 + x1 + 2F0(0) >= 1 + x1 + 2F0(0) = [[exists(/\x.and(~AP1(_F0, x), _x1))]] 
  [[or(exists(/\x.~AP1(_F0, x)), _x1)]] = 1 + x1 + 2F0(0) >= 1 + x1 + 2F0(0) = [[exists(/\x.or(~AP1(_F0, x), _x1))]] 
  [[not(exists(/\x.~AP1(_F0, x)))]] = 1 + 2F0(0) >= 1 + 2F0(0) = [[forall(/\x.not(~AP1(_F0, x)))]] 
  [[~AP1(_F0, _x1)]] = 1 + x1 + F0(0) + F0(x1) >= max(x1, F0(x1)) = [[_F0 _x1]] 
  [[~AP1(_F0, _x1)]] = 1 + x1 + F0(0) + F0(x1) >= 1 + max(x1, F0(x1)) = [[#argfun-~AP1##(_F0 _x1)]] 

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

Thus, the original system is terminating if each of (P_1, R_0, minimal, all), (P_2, R_0, minimal, all) and (P_3, R_0, minimal, all) is finite.

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

We will use the reduction pair processor [Kop12, Thm. 7.16].  It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  not#(forall(/\x.~AP1(F, x))) >? not#(~AP1(F, ~c0)) 
  not#(exists(/\x.~AP1(F, x))) >? not#(~AP1(F, ~c1)) 
  and(X, forall(/\x.~AP1(F, x))) >= forall(/\y.and(X, ~AP1(F, y))) 
  or(X, forall(/\x.~AP1(F, x))) >= forall(/\y.or(X, ~AP1(F, y))) 
  and(forall(/\x.~AP1(F, x)), X) >= forall(/\y.and(~AP1(F, y), X)) 
  or(forall(/\x.~AP1(F, x)), X) >= forall(/\y.or(~AP1(F, y), X)) 
  not(forall(/\x.~AP1(F, x))) >= exists(/\y.not(~AP1(F, y))) 
  and(X, exists(/\x.~AP1(F, x))) >= exists(/\y.and(X, ~AP1(F, y))) 
  or(X, exists(/\x.~AP1(F, x))) >= exists(/\y.or(X, ~AP1(F, y))) 
  and(exists(/\x.~AP1(F, x)), X) >= exists(/\y.and(~AP1(F, y), X)) 
  or(exists(/\x.~AP1(F, x)), X) >= exists(/\y.or(~AP1(F, y), X)) 
  not(exists(/\x.~AP1(F, x))) >= forall(/\y.not(~AP1(F, y))) 
  ~AP1(F, X) >= F X 

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

The following interpretation satisfies the requirements:

  and = \y0y1.0 
  exists = \G0.2G0(0) 
  forall = \G0.G0(0) 
  not = \y0.0 
  not# = \y0.y0 
  or = \y0y1.0 
  ~AP1 = \G0y1.1 + G0(y1) 
  ~c0 = 0 
  ~c1 = 0 

Using this interpretation, the requirements translate to:

  [[not#(forall(/\x.~AP1(_F0, x)))]] = 1 + F0(0) >= 1 + F0(0) = [[not#(~AP1(_F0, ~c0))]] 
  [[not#(exists(/\x.~AP1(_F0, x)))]] = 2 + 2F0(0) > 1 + F0(0) = [[not#(~AP1(_F0, ~c1))]] 
  [[and(_x0, forall(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[forall(/\x.and(_x0, ~AP1(_F1, x)))]] 
  [[or(_x0, forall(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[forall(/\x.or(_x0, ~AP1(_F1, x)))]] 
  [[and(forall(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[forall(/\x.and(~AP1(_F0, x), _x1))]] 
  [[or(forall(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[forall(/\x.or(~AP1(_F0, x), _x1))]] 
  [[not(forall(/\x.~AP1(_F0, x)))]] = 0 >= 0 = [[exists(/\x.not(~AP1(_F0, x)))]] 
  [[and(_x0, exists(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[exists(/\x.and(_x0, ~AP1(_F1, x)))]] 
  [[or(_x0, exists(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[exists(/\x.or(_x0, ~AP1(_F1, x)))]] 
  [[and(exists(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[exists(/\x.and(~AP1(_F0, x), _x1))]] 
  [[or(exists(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[exists(/\x.or(~AP1(_F0, x), _x1))]] 
  [[not(exists(/\x.~AP1(_F0, x)))]] = 0 >= 0 = [[forall(/\x.not(~AP1(_F0, x)))]] 
  [[~AP1(_F0, _x1)]] = 1 + F0(x1) >= F0(x1) = [[_F0 _x1]] 

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

  not#(forall(/\x.~AP1(F, x))) =#> not#(~AP1(F, y))   

Thus, the original system is terminating if each of (P_1, R_0, minimal, all), (P_2, R_0, minimal, all) and (P_5, R_0, minimal, all) is finite.

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

We will use the reduction pair processor [Kop12, Thm. 7.16].  It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  not#(forall(/\x.~AP1(F, x))) >? not#(~AP1(F, ~c0)) 
  and(X, forall(/\x.~AP1(F, x))) >= forall(/\y.and(X, ~AP1(F, y))) 
  or(X, forall(/\x.~AP1(F, x))) >= forall(/\y.or(X, ~AP1(F, y))) 
  and(forall(/\x.~AP1(F, x)), X) >= forall(/\y.and(~AP1(F, y), X)) 
  or(forall(/\x.~AP1(F, x)), X) >= forall(/\y.or(~AP1(F, y), X)) 
  not(forall(/\x.~AP1(F, x))) >= exists(/\y.not(~AP1(F, y))) 
  and(X, exists(/\x.~AP1(F, x))) >= exists(/\y.and(X, ~AP1(F, y))) 
  or(X, exists(/\x.~AP1(F, x))) >= exists(/\y.or(X, ~AP1(F, y))) 
  and(exists(/\x.~AP1(F, x)), X) >= exists(/\y.and(~AP1(F, y), X)) 
  or(exists(/\x.~AP1(F, x)), X) >= exists(/\y.or(~AP1(F, y), X)) 
  not(exists(/\x.~AP1(F, x))) >= forall(/\y.not(~AP1(F, y))) 
  ~AP1(F, X) >= F X 

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

The following interpretation satisfies the requirements:

  and = \y0y1.0 
  exists = \G0.0 
  forall = \G0.2G0(0) 
  not = \y0.0 
  not# = \y0.y0 
  or = \y0y1.0 
  ~AP1 = \G0y1.1 + G0(y1) 
  ~c0 = 0 

Using this interpretation, the requirements translate to:

  [[not#(forall(/\x.~AP1(_F0, x)))]] = 2 + 2F0(0) > 1 + F0(0) = [[not#(~AP1(_F0, ~c0))]] 
  [[and(_x0, forall(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[forall(/\x.and(_x0, ~AP1(_F1, x)))]] 
  [[or(_x0, forall(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[forall(/\x.or(_x0, ~AP1(_F1, x)))]] 
  [[and(forall(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[forall(/\x.and(~AP1(_F0, x), _x1))]] 
  [[or(forall(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[forall(/\x.or(~AP1(_F0, x), _x1))]] 
  [[not(forall(/\x.~AP1(_F0, x)))]] = 0 >= 0 = [[exists(/\x.not(~AP1(_F0, x)))]] 
  [[and(_x0, exists(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[exists(/\x.and(_x0, ~AP1(_F1, x)))]] 
  [[or(_x0, exists(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[exists(/\x.or(_x0, ~AP1(_F1, x)))]] 
  [[and(exists(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[exists(/\x.and(~AP1(_F0, x), _x1))]] 
  [[or(exists(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[exists(/\x.or(~AP1(_F0, x), _x1))]] 
  [[not(exists(/\x.~AP1(_F0, x)))]] = 0 >= 0 = [[forall(/\x.not(~AP1(_F0, x)))]] 
  [[~AP1(_F0, _x1)]] = 1 + F0(x1) >= F0(x1) = [[_F0 _x1]] 

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

Thus, the original system is terminating if each of (P_1, R_0, minimal, all) and (P_2, R_0, minimal, all) is finite.

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

We will use the reduction pair processor [Kop12, Thm. 7.16].  It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  or#(X, forall(/\x.~AP1(F, x))) >? or#(X, ~AP1(F, ~c0)) 
  or#(forall(/\x.~AP1(F, x)), X) >? or#(~AP1(F, ~c1), X) 
  or#(X, exists(/\x.~AP1(F, x))) >? or#(X, ~AP1(F, ~c2)) 
  or#(exists(/\x.~AP1(F, x)), X) >? or#(~AP1(F, ~c3), X) 
  and(X, forall(/\x.~AP1(F, x))) >= forall(/\y.and(X, ~AP1(F, y))) 
  or(X, forall(/\x.~AP1(F, x))) >= forall(/\y.or(X, ~AP1(F, y))) 
  and(forall(/\x.~AP1(F, x)), X) >= forall(/\y.and(~AP1(F, y), X)) 
  or(forall(/\x.~AP1(F, x)), X) >= forall(/\y.or(~AP1(F, y), X)) 
  not(forall(/\x.~AP1(F, x))) >= exists(/\y.not(~AP1(F, y))) 
  and(X, exists(/\x.~AP1(F, x))) >= exists(/\y.and(X, ~AP1(F, y))) 
  or(X, exists(/\x.~AP1(F, x))) >= exists(/\y.or(X, ~AP1(F, y))) 
  and(exists(/\x.~AP1(F, x)), X) >= exists(/\y.and(~AP1(F, y), X)) 
  or(exists(/\x.~AP1(F, x)), X) >= exists(/\y.or(~AP1(F, y), X)) 
  not(exists(/\x.~AP1(F, x))) >= forall(/\y.not(~AP1(F, y))) 
  ~AP1(F, X) >= F X 

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

The following interpretation satisfies the requirements:

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

Using this interpretation, the requirements translate to:

  [[or#(_x0, forall(/\x.~AP1(_F1, x)))]] = 1 + 2x0 + 2F1(0) >= 1 + 2x0 + 2F1(0) = [[or#(_x0, ~AP1(_F1, ~c0))]] 
  [[or#(forall(/\x.~AP1(_F0, x)), _x1)]] = 2 + x1 + 4F0(0) >= 2 + x1 + 4F0(0) = [[or#(~AP1(_F0, ~c1), _x1)]] 
  [[or#(_x0, exists(/\x.~AP1(_F1, x)))]] = 2 + 2x0 + 4F1(0) > 1 + 2x0 + 2F1(0) = [[or#(_x0, ~AP1(_F1, ~c2))]] 
  [[or#(exists(/\x.~AP1(_F0, x)), _x1)]] = 4 + x1 + 8F0(0) > 2 + x1 + 4F0(0) = [[or#(~AP1(_F0, ~c3), _x1)]] 
  [[and(_x0, forall(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[forall(/\x.and(_x0, ~AP1(_F1, x)))]] 
  [[or(_x0, forall(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[forall(/\x.or(_x0, ~AP1(_F1, x)))]] 
  [[and(forall(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[forall(/\x.and(~AP1(_F0, x), _x1))]] 
  [[or(forall(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[forall(/\x.or(~AP1(_F0, x), _x1))]] 
  [[not(forall(/\x.~AP1(_F0, x)))]] = 0 >= 0 = [[exists(/\x.not(~AP1(_F0, x)))]] 
  [[and(_x0, exists(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[exists(/\x.and(_x0, ~AP1(_F1, x)))]] 
  [[or(_x0, exists(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[exists(/\x.or(_x0, ~AP1(_F1, x)))]] 
  [[and(exists(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[exists(/\x.and(~AP1(_F0, x), _x1))]] 
  [[or(exists(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[exists(/\x.or(~AP1(_F0, x), _x1))]] 
  [[not(exists(/\x.~AP1(_F0, x)))]] = 0 >= 0 = [[forall(/\x.not(~AP1(_F0, x)))]] 
  [[~AP1(_F0, _x1)]] = 1 + 2F0(x1) >= F0(x1) = [[_F0 _x1]] 

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

  or#(X, forall(/\x.~AP1(F, x))) =#> or#(X, ~AP1(F, y))   
  or#(forall(/\x.~AP1(F, x)), X) =#> or#(~AP1(F, y), X)   

Thus, the original system is terminating if each of (P_1, R_0, minimal, all) and (P_6, R_0, minimal, all) is finite.

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

We will use the reduction pair processor [Kop12, Thm. 7.16].  It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  or#(X, forall(/\x.~AP1(F, x))) >? or#(X, ~AP1(F, ~c0)) 
  or#(forall(/\x.~AP1(F, x)), X) >? or#(~AP1(F, ~c1), X) 
  and(X, forall(/\x.~AP1(F, x))) >= forall(/\y.and(X, ~AP1(F, y))) 
  or(X, forall(/\x.~AP1(F, x))) >= forall(/\y.or(X, ~AP1(F, y))) 
  and(forall(/\x.~AP1(F, x)), X) >= forall(/\y.and(~AP1(F, y), X)) 
  or(forall(/\x.~AP1(F, x)), X) >= forall(/\y.or(~AP1(F, y), X)) 
  not(forall(/\x.~AP1(F, x))) >= exists(/\y.not(~AP1(F, y))) 
  and(X, exists(/\x.~AP1(F, x))) >= exists(/\y.and(X, ~AP1(F, y))) 
  or(X, exists(/\x.~AP1(F, x))) >= exists(/\y.or(X, ~AP1(F, y))) 
  and(exists(/\x.~AP1(F, x)), X) >= exists(/\y.and(~AP1(F, y), X)) 
  or(exists(/\x.~AP1(F, x)), X) >= exists(/\y.or(~AP1(F, y), X)) 
  not(exists(/\x.~AP1(F, x))) >= forall(/\y.not(~AP1(F, y))) 
  ~AP1(F, X) >= F X 

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

The following interpretation satisfies the requirements:

  and = \y0y1.0 
  exists = \G0.0 
  forall = \G0.2G0(0) 
  not = \y0.0 
  or = \y0y1.0 
  or# = \y0y1.2y1 
  ~AP1 = \G0y1.2 + G0(y1) 
  ~c0 = 0 
  ~c1 = 0 

Using this interpretation, the requirements translate to:

  [[or#(_x0, forall(/\x.~AP1(_F1, x)))]] = 8 + 4F1(0) > 4 + 2F1(0) = [[or#(_x0, ~AP1(_F1, ~c0))]] 
  [[or#(forall(/\x.~AP1(_F0, x)), _x1)]] = 2x1 >= 2x1 = [[or#(~AP1(_F0, ~c1), _x1)]] 
  [[and(_x0, forall(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[forall(/\x.and(_x0, ~AP1(_F1, x)))]] 
  [[or(_x0, forall(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[forall(/\x.or(_x0, ~AP1(_F1, x)))]] 
  [[and(forall(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[forall(/\x.and(~AP1(_F0, x), _x1))]] 
  [[or(forall(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[forall(/\x.or(~AP1(_F0, x), _x1))]] 
  [[not(forall(/\x.~AP1(_F0, x)))]] = 0 >= 0 = [[exists(/\x.not(~AP1(_F0, x)))]] 
  [[and(_x0, exists(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[exists(/\x.and(_x0, ~AP1(_F1, x)))]] 
  [[or(_x0, exists(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[exists(/\x.or(_x0, ~AP1(_F1, x)))]] 
  [[and(exists(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[exists(/\x.and(~AP1(_F0, x), _x1))]] 
  [[or(exists(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[exists(/\x.or(~AP1(_F0, x), _x1))]] 
  [[not(exists(/\x.~AP1(_F0, x)))]] = 0 >= 0 = [[forall(/\x.not(~AP1(_F0, x)))]] 
  [[~AP1(_F0, _x1)]] = 2 + F0(x1) >= F0(x1) = [[_F0 _x1]] 

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

  or#(forall(/\x.~AP1(F, x)), X) =#> or#(~AP1(F, y), X)   

Thus, the original system is terminating if each of (P_1, R_0, minimal, all) and (P_7, R_0, minimal, all) is finite.

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

We will use the reduction pair processor [Kop12, Thm. 7.16].  It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  or#(forall(/\x.~AP1(F, x)), X) >? or#(~AP1(F, ~c0), X) 
  and(X, forall(/\x.~AP1(F, x))) >= forall(/\y.and(X, ~AP1(F, y))) 
  or(X, forall(/\x.~AP1(F, x))) >= forall(/\y.or(X, ~AP1(F, y))) 
  and(forall(/\x.~AP1(F, x)), X) >= forall(/\y.and(~AP1(F, y), X)) 
  or(forall(/\x.~AP1(F, x)), X) >= forall(/\y.or(~AP1(F, y), X)) 
  not(forall(/\x.~AP1(F, x))) >= exists(/\y.not(~AP1(F, y))) 
  and(X, exists(/\x.~AP1(F, x))) >= exists(/\y.and(X, ~AP1(F, y))) 
  or(X, exists(/\x.~AP1(F, x))) >= exists(/\y.or(X, ~AP1(F, y))) 
  and(exists(/\x.~AP1(F, x)), X) >= exists(/\y.and(~AP1(F, y), X)) 
  or(exists(/\x.~AP1(F, x)), X) >= exists(/\y.or(~AP1(F, y), X)) 
  not(exists(/\x.~AP1(F, x))) >= forall(/\y.not(~AP1(F, y))) 
  ~AP1(F, X) >= F X 

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

The following interpretation satisfies the requirements:

  and = \y0y1.0 
  exists = \G0.0 
  forall = \G0.2G0(0) 
  not = \y0.0 
  or = \y0y1.0 
  or# = \y0y1.2y0 
  ~AP1 = \G0y1.1 + 2G0(0) + 2G0(y1) 
  ~c0 = 0 

Using this interpretation, the requirements translate to:

  [[or#(forall(/\x.~AP1(_F0, x)), _x1)]] = 4 + 16F0(0) > 2 + 8F0(0) = [[or#(~AP1(_F0, ~c0), _x1)]] 
  [[and(_x0, forall(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[forall(/\x.and(_x0, ~AP1(_F1, x)))]] 
  [[or(_x0, forall(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[forall(/\x.or(_x0, ~AP1(_F1, x)))]] 
  [[and(forall(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[forall(/\x.and(~AP1(_F0, x), _x1))]] 
  [[or(forall(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[forall(/\x.or(~AP1(_F0, x), _x1))]] 
  [[not(forall(/\x.~AP1(_F0, x)))]] = 0 >= 0 = [[exists(/\x.not(~AP1(_F0, x)))]] 
  [[and(_x0, exists(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[exists(/\x.and(_x0, ~AP1(_F1, x)))]] 
  [[or(_x0, exists(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[exists(/\x.or(_x0, ~AP1(_F1, x)))]] 
  [[and(exists(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[exists(/\x.and(~AP1(_F0, x), _x1))]] 
  [[or(exists(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[exists(/\x.or(~AP1(_F0, x), _x1))]] 
  [[not(exists(/\x.~AP1(_F0, x)))]] = 0 >= 0 = [[forall(/\x.not(~AP1(_F0, x)))]] 
  [[~AP1(_F0, _x1)]] = 1 + 2F0(0) + 2F0(x1) >= F0(x1) = [[_F0 _x1]] 

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

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

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

We will use the reduction pair processor [Kop12, Thm. 7.16].  It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  and#(X, forall(/\x.~AP1(F, x))) >? and#(X, ~AP1(F, ~c0)) 
  and#(forall(/\x.~AP1(F, x)), X) >? and#(~AP1(F, ~c1), X) 
  and#(X, exists(/\x.~AP1(F, x))) >? and#(X, ~AP1(F, ~c2)) 
  and#(exists(/\x.~AP1(F, x)), X) >? and#(~AP1(F, ~c3), X) 
  and(X, forall(/\x.~AP1(F, x))) >= forall(/\y.and(X, ~AP1(F, y))) 
  or(X, forall(/\x.~AP1(F, x))) >= forall(/\y.or(X, ~AP1(F, y))) 
  and(forall(/\x.~AP1(F, x)), X) >= forall(/\y.and(~AP1(F, y), X)) 
  or(forall(/\x.~AP1(F, x)), X) >= forall(/\y.or(~AP1(F, y), X)) 
  not(forall(/\x.~AP1(F, x))) >= exists(/\y.not(~AP1(F, y))) 
  and(X, exists(/\x.~AP1(F, x))) >= exists(/\y.and(X, ~AP1(F, y))) 
  or(X, exists(/\x.~AP1(F, x))) >= exists(/\y.or(X, ~AP1(F, y))) 
  and(exists(/\x.~AP1(F, x)), X) >= exists(/\y.and(~AP1(F, y), X)) 
  or(exists(/\x.~AP1(F, x)), X) >= exists(/\y.or(~AP1(F, y), X)) 
  not(exists(/\x.~AP1(F, x))) >= forall(/\y.not(~AP1(F, y))) 
  ~AP1(F, X) >= F X 

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

The following interpretation satisfies the requirements:

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

Using this interpretation, the requirements translate to:

  [[and#(_x0, forall(/\x.~AP1(_F1, x)))]] = 2 + 2F1(0) > 1 + F1(0) = [[and#(_x0, ~AP1(_F1, ~c0))]] 
  [[and#(forall(/\x.~AP1(_F0, x)), _x1)]] = x1 >= x1 = [[and#(~AP1(_F0, ~c1), _x1)]] 
  [[and#(_x0, exists(/\x.~AP1(_F1, x)))]] = 1 + F1(0) >= 1 + F1(0) = [[and#(_x0, ~AP1(_F1, ~c2))]] 
  [[and#(exists(/\x.~AP1(_F0, x)), _x1)]] = x1 >= x1 = [[and#(~AP1(_F0, ~c3), _x1)]] 
  [[and(_x0, forall(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[forall(/\x.and(_x0, ~AP1(_F1, x)))]] 
  [[or(_x0, forall(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[forall(/\x.or(_x0, ~AP1(_F1, x)))]] 
  [[and(forall(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[forall(/\x.and(~AP1(_F0, x), _x1))]] 
  [[or(forall(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[forall(/\x.or(~AP1(_F0, x), _x1))]] 
  [[not(forall(/\x.~AP1(_F0, x)))]] = 0 >= 0 = [[exists(/\x.not(~AP1(_F0, x)))]] 
  [[and(_x0, exists(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[exists(/\x.and(_x0, ~AP1(_F1, x)))]] 
  [[or(_x0, exists(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[exists(/\x.or(_x0, ~AP1(_F1, x)))]] 
  [[and(exists(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[exists(/\x.and(~AP1(_F0, x), _x1))]] 
  [[or(exists(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[exists(/\x.or(~AP1(_F0, x), _x1))]] 
  [[not(exists(/\x.~AP1(_F0, x)))]] = 0 >= 0 = [[forall(/\x.not(~AP1(_F0, x)))]] 
  [[~AP1(_F0, _x1)]] = 1 + F0(x1) >= F0(x1) = [[_F0 _x1]] 

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

  and#(forall(/\x.~AP1(F, x)), X) =#> and#(~AP1(F, y), X)   
  and#(X, exists(/\x.~AP1(F, x))) =#> and#(X, ~AP1(F, y))   
  and#(exists(/\x.~AP1(F, x)), X) =#> and#(~AP1(F, y), X)   

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

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

We will use the reduction pair processor [Kop12, Thm. 7.16].  It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  and#(forall(/\x.~AP1(F, x)), X) >? and#(~AP1(F, ~c0), X) 
  and#(X, exists(/\x.~AP1(F, x))) >? and#(X, ~AP1(F, ~c1)) 
  and#(exists(/\x.~AP1(F, x)), X) >? and#(~AP1(F, ~c2), X) 
  and(X, forall(/\x.~AP1(F, x))) >= forall(/\y.and(X, ~AP1(F, y))) 
  or(X, forall(/\x.~AP1(F, x))) >= forall(/\y.or(X, ~AP1(F, y))) 
  and(forall(/\x.~AP1(F, x)), X) >= forall(/\y.and(~AP1(F, y), X)) 
  or(forall(/\x.~AP1(F, x)), X) >= forall(/\y.or(~AP1(F, y), X)) 
  not(forall(/\x.~AP1(F, x))) >= exists(/\y.not(~AP1(F, y))) 
  and(X, exists(/\x.~AP1(F, x))) >= exists(/\y.and(X, ~AP1(F, y))) 
  or(X, exists(/\x.~AP1(F, x))) >= exists(/\y.or(X, ~AP1(F, y))) 
  and(exists(/\x.~AP1(F, x)), X) >= exists(/\y.and(~AP1(F, y), X)) 
  or(exists(/\x.~AP1(F, x)), X) >= exists(/\y.or(~AP1(F, y), X)) 
  not(exists(/\x.~AP1(F, x))) >= forall(/\y.not(~AP1(F, y))) 
  ~AP1(F, X) >= F X 

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

The following interpretation satisfies the requirements:

  and = \y0y1.0 
  and# = \y0y1.y0 + y1 
  exists = \G0.2G0(0) 
  forall = \G0.2G0(0) 
  not = \y0.0 
  or = \y0y1.0 
  ~AP1 = \G0y1.1 + 2G0(y1) 
  ~c0 = 0 
  ~c1 = 0 
  ~c2 = 0 

Using this interpretation, the requirements translate to:

  [[and#(forall(/\x.~AP1(_F0, x)), _x1)]] = 2 + x1 + 4F0(0) > 1 + x1 + 2F0(0) = [[and#(~AP1(_F0, ~c0), _x1)]] 
  [[and#(_x0, exists(/\x.~AP1(_F1, x)))]] = 2 + x0 + 4F1(0) > 1 + x0 + 2F1(0) = [[and#(_x0, ~AP1(_F1, ~c1))]] 
  [[and#(exists(/\x.~AP1(_F0, x)), _x1)]] = 2 + x1 + 4F0(0) > 1 + x1 + 2F0(0) = [[and#(~AP1(_F0, ~c2), _x1)]] 
  [[and(_x0, forall(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[forall(/\x.and(_x0, ~AP1(_F1, x)))]] 
  [[or(_x0, forall(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[forall(/\x.or(_x0, ~AP1(_F1, x)))]] 
  [[and(forall(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[forall(/\x.and(~AP1(_F0, x), _x1))]] 
  [[or(forall(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[forall(/\x.or(~AP1(_F0, x), _x1))]] 
  [[not(forall(/\x.~AP1(_F0, x)))]] = 0 >= 0 = [[exists(/\x.not(~AP1(_F0, x)))]] 
  [[and(_x0, exists(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[exists(/\x.and(_x0, ~AP1(_F1, x)))]] 
  [[or(_x0, exists(/\x.~AP1(_F1, x)))]] = 0 >= 0 = [[exists(/\x.or(_x0, ~AP1(_F1, x)))]] 
  [[and(exists(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[exists(/\x.and(~AP1(_F0, x), _x1))]] 
  [[or(exists(/\x.~AP1(_F0, x)), _x1)]] = 0 >= 0 = [[exists(/\x.or(~AP1(_F0, x), _x1))]] 
  [[not(exists(/\x.~AP1(_F0, x)))]] = 0 >= 0 = [[forall(/\x.not(~AP1(_F0, x)))]] 
  [[~AP1(_F0, _x1)]] = 1 + 2F0(x1) >= F0(x1) = [[_F0 _x1]] 

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

[Kop11]  C. Kop.  Simplifying Algebraic Functional Systems.  In Proceedings of CAI 2011, volume 6742 of LNCS.  201--215, Springer, 2011.
[Kop12]  C. Kop.  Higher Order Termination.  PhD Thesis, 2012.