Problem:
 neg (neg z) -> z
 neg (and z zprime) -> or (neg z) (neg zprime)
 neg (or z zprime) -> and (neg z) (neg zprime)
 neg (forall (\x. y x)) -> exists (\x. neg (y x))
 neg (exists (\x. y x)) -> forall (\x. neg (y x))

Proof:
 Higher-Order Church Rosser Processor (kb):
  neg (neg z) -> z
  neg (and z zprime) -> or (neg z) (neg zprime)
  neg (or z zprime) -> and (neg z) (neg zprime)
  neg (forall (\x. y x)) -> exists (\x. neg (y x))
  neg (exists (\x. y x)) -> forall (\x. neg (y x))
  critical peaks: 5, all joinable
   neg 169 <-[1]-> neg 169
   neg (or (neg 191) (neg 192)) <-[1]-> and 191 192
   neg (and (neg 221) (neg 222)) <-[1]-> or 221 222
   neg (exists (\x. neg (248 x))) <-[1]-> forall (\x. 248 x)
   neg (forall (\x. neg (266 x))) <-[1]-> exists (\x. 266 x)
   
   Oracle processor (/home/csag8264/bin/wanda.sh):
    We consider the system csiho.98c3fc.
    
      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 rule removal, following [Kop12, Theorem 2.23].
    
    This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):
    
      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 orient these requirements with a polynomial interpretations in the natural numbers.  
    The following interpretation satisfies the requirements:
    
      and = \y0y1.1 + y0 + y1 
      exists = \G0.G0(0) 
      forall = \G0.G0(0) 
      neg = \y0.3y0 
      or = \y0y1.2 + y0 + y1 
    
    Using this interpretation, the requirements translate to:
    
      [[neg(neg(_x0))]] = 9x0 >= x0 = [[_x0]] 
      [[neg(and(_x0, _x1))]] = 3 + 3x0 + 3x1 > 2 + 3x0 + 3x1 = [[or(neg(_x0), neg(_x1))]] 
      [[neg(or(_x0, _x1))]] = 6 + 3x0 + 3x1 > 1 + 3x0 + 3x1 = [[and(neg(_x0), neg(_x1))]] 
      [[neg(forall(/\x._x0(x)))]] = 3F0(0) >= 3F0(0) = [[exists(/\y.neg(_x0(y)))]] 
      [[neg(exists(/\x._x0(x)))]] = 3F0(0) >= 3F0(0) = [[forall(/\y.neg(_x0(y)))]] 
    
    We can thus remove the following rules:
    
      neg(and(X, Y)) => or(neg(X), neg(Y)) 
      neg(or(X, Y)) => and(neg(X), neg(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]):
    
      neg(neg(X)) >? X 
      neg(forall(/\x.X(x))) >? exists(/\y.neg(X(y))) 
      neg(exists(/\x.X(x))) >? forall(/\y.neg(X(y))) 
    
    We orient these requirements with a polynomial interpretations in the natural numbers.  
    The following interpretation satisfies the requirements:
    
      and = \y0y1.0 
      exists = \G0.1 + G0(0) 
      forall = \G0.1 + G0(0) 
      neg = \y0.2 + 2y0 
      or = \y0y1.0 
    
    Using this interpretation, the requirements translate to:
    
      [[neg(neg(_x0))]] = 6 + 4x0 > x0 = [[_x0]] 
      [[neg(forall(/\x._x0(x)))]] = 4 + 2F0(0) > 3 + 2F0(0) = [[exists(/\y.neg(_x0(y)))]] 
      [[neg(exists(/\x._x0(x)))]] = 4 + 2F0(0) > 3 + 2F0(0) = [[forall(/\y.neg(_x0(y)))]] 
    
    We can thus remove the following rules:
    
      neg(neg(X)) => X 
      neg(forall(/\x.X(x))) => exists(/\y.neg(X(y))) 
      neg(exists(/\x.X(x))) => forall(/\y.neg(X(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.
    
    Qed