Problem:
 f(x,x) -> f(g(x),g(x))
 a(g(x),x) -> f(x,x)
 b(x,g(x)) -> g(x)

Proof:
 sorted: (order)
 0:f(x,x) -> f(g(x),g(x))
   a(g(x),x) -> f(x,x)
 1:b(x,g(x)) -> g(x)
 -----
 sorts
   [1>2, 1>4, 2>6, 3>5, 4>6, 5>6]
 sort attachment (non-strict)
   f : 6 x 6 -> 2
   g : 6 -> 6
   a : 4 x 6 -> 1
   b : 6 x 5 -> 3
 -----
 0:f(x,x) -> f(g(x),g(x))
   a(g(x),x) -> f(x,x)
   Open
 
 
 1:b(x,g(x)) -> g(x)
   Church Rosser Transformation Processor (kb):
    b(x,g(x)) -> g(x)
    critical peaks: joinable
    DP Processor:
     DPs:
      
     TRS:
      b(x,g(x)) -> g(x)
     Qed