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

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 1
   g(b()) <-2|0[]- g(a()) -0|[]-> f(g(a()))
  Redundant Rules Transformation:
   g(b()) -> c(a())
   a() -> b()
   f(x) -> h(x)
   h(x) -> c(b())
   Qed (ToyamaOyamaguchi95Cor22)