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

Proof:
 sorted: (order)
 0:f(a(x),x) -> f(x,a(x))
   f(b(x),x) -> f(x,b(x))
   a(x) -> b(x)
 1:g(b(x),y) -> g(a(a(x)),y)
   g(c(x),y) -> y
   a(x) -> b(x)
 -----
 sorts
   [0>2, 1>3, 1>7, 2>6, 3>4, 3>6, 4>5]
 sort attachment (non-strict)
   f : 2 x 6 -> 0
   a : 6 -> 6
   b : 6 -> 6
   g : 3 x 7 -> 1
   c : 5 -> 4
 -----
 0:f(a(x),x) -> f(x,a(x))
   f(b(x),x) -> f(x,b(x))
   a(x) -> b(x)
   Church Rosser Transformation Processor (ac):
    f(a(x),x) -> f(x,a(x))
    f(b(x),x) -> f(x,b(x))
    a(x) -> b(x)
    AC critical peaks: joinable
    AC-KBO Processor:
     precedence:
      a > b > f
      weight function:
       w0 = 1
       w(b) = w(a) = 2
       w(f) = 0
      problem:
       
      Qed
 
 
 1:g(b(x),y) -> g(a(a(x)),y)
   g(c(x),y) -> y
   a(x) -> b(x)
   Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
    
    critical peaks: joinable
    Qed