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())
  Redundant Rules Transformation:
   a() -> a'()
   h(x,a'(),y) -> h(x,y,y)
   h(x,y,a'()) -> h(x,y,y)
   g() -> f()
   Church Rosser Transformation Processor (no redundant rules):
    strict:
     g() -> f()
     h(x,y,a'()) -> h(x,y,y)
     h(x,a'(),y) -> h(x,y,y)
     a() -> a'()
    weak:
     
    critical peaks: 2
     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'())
    Closedness Processor (*feeble*):
     
     Qed