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
   [0>1, 0>3, 1>5, 2>4, 3>5, 4>5]
 sort attachment (non-strict)
   f : 5 x 5 -> 1
   g : 5 -> 5
   a : 3 x 5 -> 0
   b : 5 x 4 -> 2
 -----
 0:f(x,x) -> f(g(x),g(x))
   a(g(x),x) -> f(x,x)
   Qed (SakaiOyamaguchiOgawa14)
 
 
 1:b(x,g(x)) -> g(x)
   Qed (SakaiOyamaguchiOgawa14)