Problem:
 a() -> b()
 a() -> c()
 a() -> e()
 b() -> d()
 c() -> a()
 d() -> a()
 d() -> e()
 g(x) -> h(a())
 h(x) -> e()

Proof:
 Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
  c() -> a()
  a() -> b()
  b() -> d()
  d() -> e()
  a() -> e()
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [d] = 0,
    
    [b] = 0,
    
    [e] = 0,
    
    [a] = 4,
    
    [c] = 4
   orientation:
    c() = 4 >= 4 = a()
    
    a() = 4 >= 0 = b()
    
    b() = 0 >= 0 = d()
    
    d() = 0 >= 0 = e()
    
    a() = 4 >= 0 = e()
   problem:
    c() -> a()
    b() -> d()
    d() -> e()
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [d] = 4,
     
     [b] = 4,
     
     [e] = 0,
     
     [a] = 0,
     
     [c] = 0
    orientation:
     c() = 0 >= 0 = a()
     
     b() = 4 >= 4 = d()
     
     d() = 4 >= 0 = e()
    problem:
     c() -> a()
     b() -> d()
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [d] = 0,
      
      [b] = 1,
      
      [a] = 0,
      
      [c] = 0
     orientation:
      c() = 0 >= 0 = a()
      
      b() = 1 >= 0 = d()
     problem:
      c() -> a()
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [a] = 0,
       
       [c] = 1
      orientation:
       c() = 1 >= 0 = a()
      problem:
       
      Qed