Problem:
 map (\x. f x) nil -> nil
 map (\x. f x) (cons x xs) -> cons (f x) (map (\x. f x) xs)
 map (\x. f x) (map (\x. g x) xs) -> map (\y. f (g y)) xs

Proof:
 Higher-Order Church Rosser Processor (kb):
  map (\x. f x) nil -> nil
  map (\x. f x) (cons x xs) -> cons (f x) (map (\x. f x) xs)
  map (\x. f x) (map (\x. g x) xs) -> map (\y. f (g y)) xs
  critical peaks: 3, all joinable
   map (\x. f x) nil <-[1]-> map (\y. f (170 y)) nil
   map (\x. f x) (cons (211 212) (map (\x. 211 x) 213)) <-[1]-> map (\y. f (211 y)) (cons 212 213)
   map (\x. f x) (map (\y. 258 (259 y)) 260) <-[1]-> map (\y. f (258 y)) (map (\x. 259 x) 260)
   
   Oracle processor (/home/csag8264/bin/wanda.sh):
    We consider the system csiho.defc5a.
    
      Alphabet:
    
        cons : [a * alist] --> alist 
        map : [a -> a * alist] --> alist 
        nil : [] --> alist 
    
      Rules:
    
        map(/\x.X(x), nil) => nil 
        map(/\x.X(x), cons(Y, Z)) => cons(X(Y), map(/\y.X(y), Z)) 
        map(/\x.X(x), map(/\y.Y(y), Z)) => map(/\z.X(Y(z)), Z) 
    
    We use rule removal, following [Kop12, Theorem 2.23].
    
    This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):
    
      map(/\x.X(x), nil) >? nil 
      map(/\x.X(x), cons(Y, Z)) >? cons(X(Y), map(/\y.X(y), Z)) 
      map(/\x.X(x), map(/\y.Y(y), Z)) >? map(/\z.X(Y(z)), Z) 
    
    We orient these requirements with a polynomial interpretations in the natural numbers.  
    The following interpretation satisfies the requirements:
    
      cons = \y0y1.3 + y0 + y1 
      map = \G0y1.3 + y1 + G0(y1) + 2G0(0) + 3y1G0(y1) 
      nil = 0 
    
    Using this interpretation, the requirements translate to:
    
      [[map(/\x._x0(x), nil)]] = 3 + 3F0(0) > 0 = [[nil]] 
      [[map(/\x._x0(x), cons(_x1, _x2))]] = 6 + x1 + x2 + 2F0(0) + 3x1F0(3 + x1 + x2) + 3x2F0(3 + x1 + x2) + 10F0(3 + x1 + x2) >= 6 + x2 + F0(x1) + F0(x2) + 2F0(0) + 3x2F0(x2) = [[cons(_x0(_x1), map(/\y._x0(y), _x2))]] 
      [[map(/\x._x0(x), map(/\y._x1(y), _x2))]] = 6 + x2 + F1(x2) + 2F0(0) + 2F1(0) + 3x2F0(3 + x2 + F1(x2) + 2F1(0) + 3x2F1(x2)) + 3x2F1(x2) + 3F0(3 + x2 + F1(x2) + 2F1(0) + 3x2F1(x2))F1(x2) + 6F0(3 + x2 + F1(x2) + 2F1(0) + 3x2F1(x2))F1(0) + 9x2F0(3 + x2 + F1(x2) + 2F1(0) + 3x2F1(x2))F1(x2) + 10F0(3 + x2 + F1(x2) + 2F1(0) + 3x2F1(x2)) > 3 + x2 + F0(F1(x2)) + 2F0(F1(0)) + 3x2F0(F1(x2)) = [[map(/\z._x0(_x1(z)), _x2)]] 
    
    We can thus remove the following rules:
    
      map(/\x.X(x), nil) => nil 
      map(/\x.X(x), map(/\y.Y(y), Z)) => map(/\z.X(Y(z)), Z) 
    
    We use rule removal, following [Kop12, Theorem 2.23].
    
    This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):
    
      map(/\x.X(x), cons(Y, Z)) >? cons(X(Y), map(/\y.X(y), Z)) 
    
    We orient these requirements with a polynomial interpretations in the natural numbers.  
    The following interpretation satisfies the requirements:
    
      cons = \y0y1.3 + y0 + y1 
      map = \G0y1.3y1 + G0(0) + G0(y1) + 2y1G0(y1) 
      nil = 0 
    
    Using this interpretation, the requirements translate to:
    
      [[map(/\x._x0(x), cons(_x1, _x2))]] = 9 + 3x1 + 3x2 + F0(0) + 2x1F0(3 + x1 + x2) + 2x2F0(3 + x1 + x2) + 7F0(3 + x1 + x2) > 3 + 3x2 + F0(0) + F0(x1) + F0(x2) + 2x2F0(x2) = [[cons(_x0(_x1), map(/\y._x0(y), _x2))]] 
    
    We can thus remove the following rules:
    
      map(/\x.X(x), cons(Y, Z)) => cons(X(Y), map(/\y.X(y), Z)) 
    
    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