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 (star):
  
  strict:
   
  weak:
   
  critical peaks: 8
  b() <-0|[]- a() -1|[]-> c()
  b() <-0|[]- a() -2|[]-> e()
  c() <-1|[]- a() -0|[]-> b()
  c() <-1|[]- a() -2|[]-> e()
  e() <-2|[]- a() -0|[]-> b()
  e() <-2|[]- a() -1|[]-> c()
  a() <-5|[]- d() -6|[]-> e()
  e() <-6|[]- d() -5|[]-> a()
  Shift Processor lab=left (dd):
   
   strict:
    a() -> b()
    a() -> c()
    c() -> a()
    a() -> b()
    b() -> d()
    d() -> a()
    c() -> a()
    b() -> d()
    d() -> e()
    c() -> a()
    a() -> e()
    a() -> b()
    a() -> e()
    b() -> d()
    d() -> e()
    a() -> c()
    a() -> b()
    c() -> a()
    b() -> d()
    d() -> a()
    c() -> a()
    a() -> b()
    c() -> a()
    a() -> e()
    b() -> d()
    d() -> e()
    a() -> c()
    a() -> e()
    c() -> a()
    a() -> e()
    a() -> e()
    a() -> b()
    b() -> d()
    d() -> e()
    a() -> e()
    a() -> c()
    c() -> a()
    a() -> e()
    d() -> a()
    d() -> e()
    a() -> e()
    d() -> e()
    d() -> a()
    a() -> e()
   weak:
    a() -> b()
    a() -> c()
    a() -> e()
    b() -> d()
    c() -> a()
    d() -> a()
    d() -> e()
    g(x) -> h(a())
    h(x) -> e()
   Polynomial Interpretation Processor:
    dimension: 1
    interpretation:
     [h](x0) = x0x0 + 2,
     
     [g](x0) = 2x0x0 + 2,
     
     [d] = 0,
     
     [e] = 0,
     
     [c] = 0,
     
     [b] = 0,
     
     [a] = 0
    orientation:
     a() = 0 >= 0 = b()
     
     a() = 0 >= 0 = c()
     
     c() = 0 >= 0 = a()
     
     a() = 0 >= 0 = b()
     
     b() = 0 >= 0 = d()
     
     d() = 0 >= 0 = a()
     
     c() = 0 >= 0 = a()
     
     b() = 0 >= 0 = d()
     
     d() = 0 >= 0 = e()
     
     c() = 0 >= 0 = a()
     
     a() = 0 >= 0 = e()
     
     a() = 0 >= 0 = b()
     
     a() = 0 >= 0 = e()
     
     b() = 0 >= 0 = d()
     
     d() = 0 >= 0 = e()
     
     a() = 0 >= 0 = c()
     
     a() = 0 >= 0 = b()
     
     c() = 0 >= 0 = a()
     
     b() = 0 >= 0 = d()
     
     d() = 0 >= 0 = a()
     
     c() = 0 >= 0 = a()
     
     a() = 0 >= 0 = b()
     
     c() = 0 >= 0 = a()
     
     a() = 0 >= 0 = e()
     
     b() = 0 >= 0 = d()
     
     d() = 0 >= 0 = e()
     
     a() = 0 >= 0 = c()
     
     a() = 0 >= 0 = e()
     
     c() = 0 >= 0 = a()
     
     a() = 0 >= 0 = e()
     
     a() = 0 >= 0 = e()
     
     a() = 0 >= 0 = b()
     
     b() = 0 >= 0 = d()
     
     d() = 0 >= 0 = e()
     
     a() = 0 >= 0 = e()
     
     a() = 0 >= 0 = c()
     
     c() = 0 >= 0 = a()
     
     a() = 0 >= 0 = e()
     
     d() = 0 >= 0 = a()
     
     d() = 0 >= 0 = e()
     
     a() = 0 >= 0 = e()
     
     d() = 0 >= 0 = e()
     
     d() = 0 >= 0 = a()
     
     a() = 0 >= 0 = e()
     
     g(x) = 2x*x + 2 >= 2 = h(a())
     
     h(x) = x*x + 2 >= 0 = e()
    problem:
     
     strict:
      a() -> b()
      a() -> c()
      c() -> a()
      a() -> b()
      b() -> d()
      d() -> a()
      c() -> a()
      b() -> d()
      d() -> e()
      c() -> a()
      a() -> e()
      a() -> b()
      a() -> e()
      b() -> d()
      d() -> e()
      a() -> c()
      a() -> b()
      c() -> a()
      b() -> d()
      d() -> a()
      c() -> a()
      a() -> b()
      c() -> a()
      a() -> e()
      b() -> d()
      d() -> e()
      a() -> c()
      a() -> e()
      c() -> a()
      a() -> e()
      a() -> e()
      a() -> b()
      b() -> d()
      d() -> e()
      a() -> e()
      a() -> c()
      c() -> a()
      a() -> e()
      d() -> a()
      d() -> e()
      a() -> e()
      d() -> e()
      d() -> a()
      a() -> e()
     weak:
      a() -> b()
      a() -> c()
      a() -> e()
      b() -> d()
      c() -> a()
      d() -> a()
      d() -> e()
      g(x) -> h(a())
    Polynomial Interpretation Processor:
     dimension: 1
     interpretation:
      [h](x0) = x0,
      
      [g](x0) = 2x0x0 + 1,
      
      [d] = 0,
      
      [e] = 0,
      
      [c] = 0,
      
      [b] = 0,
      
      [a] = 0
     orientation:
      a() = 0 >= 0 = b()
      
      a() = 0 >= 0 = c()
      
      c() = 0 >= 0 = a()
      
      a() = 0 >= 0 = b()
      
      b() = 0 >= 0 = d()
      
      d() = 0 >= 0 = a()
      
      c() = 0 >= 0 = a()
      
      b() = 0 >= 0 = d()
      
      d() = 0 >= 0 = e()
      
      c() = 0 >= 0 = a()
      
      a() = 0 >= 0 = e()
      
      a() = 0 >= 0 = b()
      
      a() = 0 >= 0 = e()
      
      b() = 0 >= 0 = d()
      
      d() = 0 >= 0 = e()
      
      a() = 0 >= 0 = c()
      
      a() = 0 >= 0 = b()
      
      c() = 0 >= 0 = a()
      
      b() = 0 >= 0 = d()
      
      d() = 0 >= 0 = a()
      
      c() = 0 >= 0 = a()
      
      a() = 0 >= 0 = b()
      
      c() = 0 >= 0 = a()
      
      a() = 0 >= 0 = e()
      
      b() = 0 >= 0 = d()
      
      d() = 0 >= 0 = e()
      
      a() = 0 >= 0 = c()
      
      a() = 0 >= 0 = e()
      
      c() = 0 >= 0 = a()
      
      a() = 0 >= 0 = e()
      
      a() = 0 >= 0 = e()
      
      a() = 0 >= 0 = b()
      
      b() = 0 >= 0 = d()
      
      d() = 0 >= 0 = e()
      
      a() = 0 >= 0 = e()
      
      a() = 0 >= 0 = c()
      
      c() = 0 >= 0 = a()
      
      a() = 0 >= 0 = e()
      
      d() = 0 >= 0 = a()
      
      d() = 0 >= 0 = e()
      
      a() = 0 >= 0 = e()
      
      d() = 0 >= 0 = e()
      
      d() = 0 >= 0 = a()
      
      a() = 0 >= 0 = e()
      
      g(x) = 2x*x + 1 >= 0 = h(a())
     problem:
      
      strict:
       a() -> b()
       a() -> c()
       c() -> a()
       a() -> b()
       b() -> d()
       d() -> a()
       c() -> a()
       b() -> d()
       d() -> e()
       c() -> a()
       a() -> e()
       a() -> b()
       a() -> e()
       b() -> d()
       d() -> e()
       a() -> c()
       a() -> b()
       c() -> a()
       b() -> d()
       d() -> a()
       c() -> a()
       a() -> b()
       c() -> a()
       a() -> e()
       b() -> d()
       d() -> e()
       a() -> c()
       a() -> e()
       c() -> a()
       a() -> e()
       a() -> e()
       a() -> b()
       b() -> d()
       d() -> e()
       a() -> e()
       a() -> c()
       c() -> a()
       a() -> e()
       d() -> a()
       d() -> e()
       a() -> e()
       d() -> e()
       d() -> a()
       a() -> e()
      weak:
       a() -> b()
       a() -> c()
       a() -> e()
       b() -> d()
       c() -> a()
       d() -> a()
       d() -> e()
     Polynomial Interpretation Processor:
      dimension: 1
      interpretation:
       [d] = 2,
       
       [e] = 0,
       
       [c] = 2,
       
       [b] = 2,
       
       [a] = 2
      orientation:
       a() = 2 >= 2 = b()
       
       a() = 2 >= 2 = c()
       
       c() = 2 >= 2 = a()
       
       a() = 2 >= 2 = b()
       
       b() = 2 >= 2 = d()
       
       d() = 2 >= 2 = a()
       
       c() = 2 >= 2 = a()
       
       b() = 2 >= 2 = d()
       
       d() = 2 >= 0 = e()
       
       c() = 2 >= 2 = a()
       
       a() = 2 >= 0 = e()
       
       a() = 2 >= 2 = b()
       
       a() = 2 >= 0 = e()
       
       b() = 2 >= 2 = d()
       
       d() = 2 >= 0 = e()
       
       a() = 2 >= 2 = c()
       
       a() = 2 >= 2 = b()
       
       c() = 2 >= 2 = a()
       
       b() = 2 >= 2 = d()
       
       d() = 2 >= 2 = a()
       
       c() = 2 >= 2 = a()
       
       a() = 2 >= 2 = b()
       
       c() = 2 >= 2 = a()
       
       a() = 2 >= 0 = e()
       
       b() = 2 >= 2 = d()
       
       d() = 2 >= 0 = e()
       
       a() = 2 >= 2 = c()
       
       a() = 2 >= 0 = e()
       
       c() = 2 >= 2 = a()
       
       a() = 2 >= 0 = e()
       
       a() = 2 >= 0 = e()
       
       a() = 2 >= 2 = b()
       
       b() = 2 >= 2 = d()
       
       d() = 2 >= 0 = e()
       
       a() = 2 >= 0 = e()
       
       a() = 2 >= 2 = c()
       
       c() = 2 >= 2 = a()
       
       a() = 2 >= 0 = e()
       
       d() = 2 >= 2 = a()
       
       d() = 2 >= 0 = e()
       
       a() = 2 >= 0 = e()
       
       d() = 2 >= 0 = e()
       
       d() = 2 >= 2 = a()
       
       a() = 2 >= 0 = e()
      problem:
       
       strict:
        a() -> b()
        a() -> c()
        c() -> a()
        a() -> b()
        b() -> d()
        d() -> a()
        c() -> a()
        b() -> d()
        c() -> a()
        a() -> b()
        b() -> d()
        a() -> c()
        a() -> b()
        c() -> a()
        b() -> d()
        d() -> a()
        c() -> a()
        a() -> b()
        c() -> a()
        b() -> d()
        a() -> c()
        c() -> a()
        a() -> b()
        b() -> d()
        a() -> c()
        c() -> a()
        d() -> a()
        d() -> a()
       weak:
        a() -> b()
        a() -> c()
        b() -> d()
        c() -> a()
        d() -> a()
      Shift Processor (ldh) lab=left (force):
       
       strict:
        
       weak:
        
       Rule Labeling Processor:
        
        strict:
         
        weak:
         
        rule labeling (right):
         a() -> b(): 1
         a() -> c(): 1
         a() -> e(): 1
         b() -> d(): 0
         c() -> a(): 0
         d() -> a(): 2
         d() -> e(): 0
         g(x) -> h(a()): 0
         h(x) -> e(): 0
        Decreasing Processor:
         The following diagrams are decreasing:
         peak:
          b() <-0|[1,1]- a() -1|[1,1]-> c()
         joins:
          
          c() -4|[1,0]-> a() -0|[1,1]-> b()
         peak:
          b() <-0|[1,1]- a() -2|[1,1]-> e()
         joins:
          b() -3|[1,0]-> d() -6|[1,0]-> e()
          
         peak:
          c() <-1|[1,1]- a() -0|[1,1]-> b()
         joins:
          c() -4|[1,0]-> a() -0|[1,1]-> b()
          
         peak:
          c() <-1|[1,1]- a() -2|[1,1]-> e()
         joins:
          c() -4|[1,0]-> a() -2|[1,1]-> e()
          
         peak:
          e() <-2|[1,1]- a() -0|[1,1]-> b()
         joins:
          
          b() -3|[1,0]-> d() -6|[1,0]-> e()
         peak:
          e() <-2|[1,1]- a() -1|[1,1]-> c()
         joins:
          
          c() -4|[1,0]-> a() -2|[1,1]-> e()
         peak:
          a() <-5|[1,2]- d() -6|[1,0]-> e()
         joins:
          a() -2|[1,1]-> e()
          
         peak:
          e() <-6|[1,0]- d() -5|[1,2]-> a()
         joins:
          
          a() -2|[1,1]-> e()
         Qed