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

Proof:
 sorted: (order)
 0:f(x,y) -> f(g(x),g(x))
   g(x) -> h(x)
 1:g(x) -> h(x)
   F(g(x),x) -> F(x,g(x))
   F(h(x),x) -> F(x,h(x))
 -----
 sorts
   [0>2, 1>3, 2>3]
 sort attachment (strict)
   f : 3 x 2 -> 0
   g : 3 -> 3
   h : 3 -> 3
   F : 3 x 3 -> 1
 -----
 0:f(x,y) -> f(g(x),g(x))
   g(x) -> h(x)
   Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
    
    critical peaks: joinable
    Qed
 
 
 1:g(x) -> h(x)
   F(g(x),x) -> F(x,g(x))
   F(h(x),x) -> F(x,h(x))
   Church Rosser Transformation Processor:
    strict:
     
    weak:
     
    critical peaks: 1
     F(h(x),x) <-0|0[]- F(g(x),x) -1|[]-> F(x,g(x))
    Redundant Rules Transformation:
     g(x) -> h(x)
     F(h(x),x) -> F(x,h(x))
     Qed (SakaiOyamaguchiOgawa14)