Problem:
 a() -> a'()
 h(x,a'(),y) -> h(x,y,y)
 h(x,y,a'()) -> h(x,y,y)
 g() -> f()
 h(f(),a(),a()) -> h(g(),a(),a())
 h(g(),a(),a()) -> h(f(),a(),a())

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 7
   h(f(),a'(),a()) <-0|1[]- h(f(),a(),a()) -4|[]-> h(g(),a(),a())
   h(f(),a(),a'()) <-0|2[]- h(f(),a(),a()) -4|[]-> h(g(),a(),a())
   h(g(),a'(),a()) <-0|1[]- h(g(),a(),a()) -5|[]-> h(f(),a(),a())
   h(g(),a(),a'()) <-0|2[]- h(g(),a(),a()) -5|[]-> h(f(),a(),a())
   h(x,a'(),a'()) <-1|[]- h(x,a'(),a'()) -2|[]-> h(x,a'(),a'())
   h(x,a'(),a'()) <-2|[]- h(x,a'(),a'()) -1|[]-> h(x,a'(),a'())
   h(f(),a(),a()) <-3|0[]- h(g(),a(),a()) -5|[]-> h(f(),a(),a())
  Shift Processor lab=left (dd) (force):
   strict:
    h(f(),a(),a()) -> h(f(),a'(),a())
    h(f(),a(),a()) -> h(g(),a(),a())
    h(f(),a'(),a()) -> h(f(),a(),a())
    h(g(),a(),a()) -> h(f(),a(),a())
    h(f(),a(),a()) -> h(f(),a(),a'())
    h(f(),a(),a()) -> h(g(),a(),a())
    h(f(),a(),a'()) -> h(f(),a(),a())
    h(g(),a(),a()) -> h(f(),a(),a())
    h(g(),a(),a()) -> h(g(),a'(),a())
    h(g(),a(),a()) -> h(f(),a(),a())
    h(g(),a'(),a()) -> h(g(),a(),a())
    h(f(),a(),a()) -> h(g(),a(),a())
    h(g(),a'(),a()) -> h(f(),a'(),a())
    h(f(),a(),a()) -> h(f(),a'(),a())
    h(g(),a(),a()) -> h(g(),a(),a'())
    h(g(),a(),a()) -> h(f(),a(),a())
    h(g(),a(),a'()) -> h(g(),a(),a())
    h(f(),a(),a()) -> h(g(),a(),a())
    h(g(),a(),a'()) -> h(f(),a(),a'())
    h(f(),a(),a()) -> h(f(),a(),a'())
    h(x,a'(),a'()) -> h(x,a'(),a'())
    h(x,a'(),a'()) -> h(x,a'(),a'())
    h(x,a'(),a'()) -> h(x,a'(),a'())
    h(x,a'(),a'()) -> h(x,a'(),a'())
    h(g(),a(),a()) -> h(f(),a(),a())
    h(g(),a(),a()) -> h(f(),a(),a())
   weak:
    a() -> a'()
    h(x,a'(),y) -> h(x,y,y)
    h(x,y,a'()) -> h(x,y,y)
    g() -> f()
    h(f(),a(),a()) -> h(g(),a(),a())
    h(g(),a(),a()) -> h(f(),a(),a())
   Shift Processor (ldh) lab=left (force):
    strict:
     
    weak:
     
    Rule Labeling Processor:
     strict:
      
     weak:
      
     rule labeling (right):
      a() -> a'(): 3
      h(x,a'(),y) -> h(x,y,y): 0
      h(x,y,a'()) -> h(x,y,y): 0
      g() -> f(): 0
      h(f(),a(),a()) -> h(g(),a(),a()): 1
      h(g(),a(),a()) -> h(f(),a(),a()): 2
     Rule Labeling Processor:
      strict:
       
      weak:
       
      rule labeling (left):
       a() -> a'(): 1
       h(x,a'(),y) -> h(x,y,y): 4
       h(x,y,a'()) -> h(x,y,y): 4
       g() -> f(): 0
       h(f(),a(),a()) -> h(g(),a(),a()): 4
       h(g(),a(),a()) -> h(f(),a(),a()): 1
      Decreasing Processor:
       The following diagrams are decreasing:
       peak:
        h(f(),a'(),a()) <-0|1[=>1,==1,=?3]- h(f(),a(),a()) -4|[?=4,==1,>=1]-> h(g(),a(),a())
       joins (1):
        h(f(),a'(),a()) -1|[?=4,==1,>>0]-> h(f(),a(),a())
        h(g(),a(),a()) -5|[=>1,==1,>?2]-> h(f(),a(),a())
       peak:
        h(f(),a(),a'()) <-0|2[=>1,==1,=?3]- h(f(),a(),a()) -4|[?=4,==1,>=1]-> h(g(),a(),a())
       joins (1):
        h(f(),a(),a'()) -2|[?=4,==1,>>0]-> h(f(),a(),a())
        h(g(),a(),a()) -5|[=>1,==1,>?2]-> h(f(),a(),a())
       peak:
        h(g(),a'(),a()) <-0|1[==1,==1,=?3]- h(g(),a(),a()) -5|[==1,==1,>=2]-> h(f(),a(),a())
       joins (1):
        h(g(),a'(),a()) -3|0[>>0,==1,>>0]-> h(f(),a'(),a())
        h(f(),a(),a()) -0|1[==1,==1,=?3]-> h(f(),a'(),a())
       peak:
        h(g(),a(),a'()) <-0|2[==1,==1,=?3]- h(g(),a(),a()) -5|[==1,==1,>=2]-> h(f(),a(),a())
       joins (1):
        h(g(),a(),a'()) -3|0[>>0,==1,>>0]-> h(f(),a(),a'())
        h(f(),a(),a()) -0|2[==1,==1,=?3]-> h(f(),a(),a'())
       peak:
        h(x,a'(),a'()) <-1|[==4,==1,==0]- h(x,a'(),a'()) -2|[==4,==1,==0]-> h(x,a'(),a'())
       joins (1):
        
        
       peak:
        h(x,a'(),a'()) <-2|[==4,==1,==0]- h(x,a'(),a'()) -1|[==4,==1,==0]-> h(x,a'(),a'())
       joins (1):
        
        
       peak:
        h(f(),a(),a()) <-3|0[=>0,==1,=>0]- h(g(),a(),a()) -5|[?=1,==1,?=2]-> h(f(),a(),a())
       joins (1):
        
        
       Qed