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

Proof:
 Church Rosser Transformation Processor (no redundant rules):
  strict:
   
  weak:
   
  critical peaks: 2
   a() <-1|[]- f(y,y) -2|[]-> f(g(y),g(y))
   f(g(x),g(x)) <-2|[]- f(x,x) -1|[]-> a()
  Redundant Rules Transformation:
   g(x) -> x
   f(x,x) -> a()
   f(x,y) -> f(g(x),g(x))
   f(x,y) -> f(g(x),x)
   f(x,y) -> f(x,g(x))
   f(x,y) -> a()
   f(x,y) -> f(g(g(x)),g(g(x)))
   Church Rosser Transformation Processor (no redundant rules):
    strict:
     
    weak:
     
    critical peaks: 20
     f(g(g(x)),g(g(x))) <-0|[]- f(x,y) -1|[]-> a()
     f(g(g(x)),g(g(x))) <-0|[]- f(x,y) -2|[]-> f(x,g(x))
     f(g(g(x)),g(g(x))) <-0|[]- f(x,y) -3|[]-> f(g(x),x)
     f(g(g(x)),g(g(x))) <-0|[]- f(x,y) -4|[]-> f(g(x),g(x))
     a() <-1|[]- f(x,y) -0|[]-> f(g(g(x)),g(g(x)))
     a() <-1|[]- f(x,y) -2|[]-> f(x,g(x))
     a() <-1|[]- f(x,y) -3|[]-> f(g(x),x)
     a() <-1|[]- f(x,y) -4|[]-> f(g(x),g(x))
     f(x,g(x)) <-2|[]- f(x,y) -0|[]-> f(g(g(x)),g(g(x)))
     f(x,g(x)) <-2|[]- f(x,y) -1|[]-> a()
     f(x,g(x)) <-2|[]- f(x,y) -3|[]-> f(g(x),x)
     f(x,g(x)) <-2|[]- f(x,y) -4|[]-> f(g(x),g(x))
     f(g(x),x) <-3|[]- f(x,y) -0|[]-> f(g(g(x)),g(g(x)))
     f(g(x),x) <-3|[]- f(x,y) -1|[]-> a()
     f(g(x),x) <-3|[]- f(x,y) -2|[]-> f(x,g(x))
     f(g(x),x) <-3|[]- f(x,y) -4|[]-> f(g(x),g(x))
     f(g(x),g(x)) <-4|[]- f(x,y) -0|[]-> f(g(g(x)),g(g(x)))
     f(g(x),g(x)) <-4|[]- f(x,y) -1|[]-> a()
     f(g(x),g(x)) <-4|[]- f(x,y) -2|[]-> f(x,g(x))
     f(g(x),g(x)) <-4|[]- f(x,y) -3|[]-> f(g(x),x)
    Redundant Rules Transformation:
     f(x,y) -> f(g(g(x)),g(g(x)))
     f(x,y) -> f(g(g(g(g(x)))),g(g(g(g(x)))))
     f(x,y) -> a()
     f(x,y) -> f(g(g(x)),g(g(g(x))))
     f(x,y) -> f(g(g(g(x))),g(g(x)))
     f(x,y) -> f(g(g(g(x))),g(g(g(x))))
     f(x,y) -> f(g(g(x)),g(x))
     f(x,y) -> f(g(x),g(g(x)))
     f(x,y) -> f(x,g(x))
     f(x,y) -> f(g(x),x)
     f(x,y) -> f(g(x),g(x))
     f(x,y) -> f(x,x)
     g(x) -> x
     Church Rosser Transformation Processor (no redundant rules):
      strict:
       g(x) -> x
       f(x,y) -> f(x,x)
       f(x,y) -> f(g(x),g(x))
       f(x,y) -> f(g(x),x)
       f(x,y) -> f(x,g(x))
       f(x,y) -> f(g(x),g(g(x)))
       f(x,y) -> f(g(g(x)),g(x))
       f(x,y) -> f(g(g(g(x))),g(g(g(x))))
       f(x,y) -> f(g(g(g(x))),g(g(x)))
       f(x,y) -> f(g(g(x)),g(g(g(x))))
       f(x,y) -> a()
       f(x,y) -> f(g(g(g(g(x)))),g(g(g(g(x)))))
       f(x,y) -> f(g(g(x)),g(g(x)))
      weak:
       
      critical peaks: 132
       f(x,x) <-1|[]- f(x,y) -2|[]-> f(g(x),g(x))
       f(x,x) <-1|[]- f(x,y) -3|[]-> f(g(x),x)
       f(x,x) <-1|[]- f(x,y) -4|[]-> f(x,g(x))
       f(x,x) <-1|[]- f(x,y) -5|[]-> f(g(x),g(g(x)))
       f(x,x) <-1|[]- f(x,y) -6|[]-> f(g(g(x)),g(x))
       f(x,x) <-1|[]- f(x,y) -7|[]-> f(g(g(g(x))),g(g(g(x))))
       f(x,x) <-1|[]- f(x,y) -8|[]-> f(g(g(g(x))),g(g(x)))
       f(x,x) <-1|[]- f(x,y) -9|[]-> f(g(g(x)),g(g(g(x))))
       f(x,x) <-1|[]- f(x,y) -10|[]-> a()
       f(x,x) <-1|[]- f(x,y) -11|[]-> f(g(g(g(g(x)))),g(g(g(g(x)))))
       f(x,x) <-1|[]- f(x,y) -12|[]-> f(g(g(x)),g(g(x)))
       f(g(x),g(x)) <-2|[]- f(x,y) -1|[]-> f(x,x)
       f(g(x),g(x)) <-2|[]- f(x,y) -3|[]-> f(g(x),x)
       f(g(x),g(x)) <-2|[]- f(x,y) -4|[]-> f(x,g(x))
       f(g(x),g(x)) <-2|[]- f(x,y) -5|[]-> f(g(x),g(g(x)))
       f(g(x),g(x)) <-2|[]- f(x,y) -6|[]-> f(g(g(x)),g(x))
       f(g(x),g(x)) <-2|[]- f(x,y) -7|[]-> f(g(g(g(x))),g(g(g(x))))
       f(g(x),g(x)) <-2|[]- f(x,y) -8|[]-> f(g(g(g(x))),g(g(x)))
       f(g(x),g(x)) <-2|[]- f(x,y) -9|[]-> f(g(g(x)),g(g(g(x))))
       f(g(x),g(x)) <-2|[]- f(x,y) -10|[]-> a()
       f(g(x),g(x)) <-2|[]- f(x,y) -11|[]-> f(g(g(g(g(x)))),g(g(g(g(x)))))
       f(g(x),g(x)) <-2|[]- f(x,y) -12|[]-> f(g(g(x)),g(g(x)))
       f(g(x),x) <-3|[]- f(x,y) -1|[]-> f(x,x)
       f(g(x),x) <-3|[]- f(x,y) -2|[]-> f(g(x),g(x))
       f(g(x),x) <-3|[]- f(x,y) -4|[]-> f(x,g(x))
       f(g(x),x) <-3|[]- f(x,y) -5|[]-> f(g(x),g(g(x)))
       f(g(x),x) <-3|[]- f(x,y) -6|[]-> f(g(g(x)),g(x))
       f(g(x),x) <-3|[]- f(x,y) -7|[]-> f(g(g(g(x))),g(g(g(x))))
       f(g(x),x) <-3|[]- f(x,y) -8|[]-> f(g(g(g(x))),g(g(x)))
       f(g(x),x) <-3|[]- f(x,y) -9|[]-> f(g(g(x)),g(g(g(x))))
       f(g(x),x) <-3|[]- f(x,y) -10|[]-> a()
       f(g(x),x) <-3|[]- f(x,y) -11|[]-> f(g(g(g(g(x)))),g(g(g(g(x)))))
       f(g(x),x) <-3|[]- f(x,y) -12|[]-> f(g(g(x)),g(g(x)))
       f(x,g(x)) <-4|[]- f(x,y) -1|[]-> f(x,x)
       f(x,g(x)) <-4|[]- f(x,y) -2|[]-> f(g(x),g(x))
       f(x,g(x)) <-4|[]- f(x,y) -3|[]-> f(g(x),x)
       f(x,g(x)) <-4|[]- f(x,y) -5|[]-> f(g(x),g(g(x)))
       f(x,g(x)) <-4|[]- f(x,y) -6|[]-> f(g(g(x)),g(x))
       f(x,g(x)) <-4|[]- f(x,y) -7|[]-> f(g(g(g(x))),g(g(g(x))))
       f(x,g(x)) <-4|[]- f(x,y) -8|[]-> f(g(g(g(x))),g(g(x)))
       f(x,g(x)) <-4|[]- f(x,y) -9|[]-> f(g(g(x)),g(g(g(x))))
       f(x,g(x)) <-4|[]- f(x,y) -10|[]-> a()
       f(x,g(x)) <-4|[]- f(x,y) -11|[]-> f(g(g(g(g(x)))),g(g(g(g(x)))))
       f(x,g(x)) <-4|[]- f(x,y) -12|[]-> f(g(g(x)),g(g(x)))
       f(g(x),g(g(x))) <-5|[]- f(x,y) -1|[]-> f(x,x)
       f(g(x),g(g(x))) <-5|[]- f(x,y) -2|[]-> f(g(x),g(x))
       f(g(x),g(g(x))) <-5|[]- f(x,y) -3|[]-> f(g(x),x)
       f(g(x),g(g(x))) <-5|[]- f(x,y) -4|[]-> f(x,g(x))
       f(g(x),g(g(x))) <-5|[]- f(x,y) -6|[]-> f(g(g(x)),g(x))
       f(g(x),g(g(x))) <-5|[]- f(x,y) -7|[]-> f(g(g(g(x))),g(g(g(x))))
       f(g(x),g(g(x))) <-5|[]- f(x,y) -8|[]-> f(g(g(g(x))),g(g(x)))
       f(g(x),g(g(x))) <-5|[]- f(x,y) -9|[]-> f(g(g(x)),g(g(g(x))))
       f(g(x),g(g(x))) <-5|[]- f(x,y) -10|[]-> a()
       f(g(x),g(g(x))) <-5|[]- f(x,y) -11|[]-> f(g(g(g(g(x)))),g(g(g(g(x)))))
       f(g(x),g(g(x))) <-5|[]- f(x,y) -12|[]-> f(g(g(x)),g(g(x)))
       f(g(g(x)),g(x)) <-6|[]- f(x,y) -1|[]-> f(x,x)
       f(g(g(x)),g(x)) <-6|[]- f(x,y) -2|[]-> f(g(x),g(x))
       f(g(g(x)),g(x)) <-6|[]- f(x,y) -3|[]-> f(g(x),x)
       f(g(g(x)),g(x)) <-6|[]- f(x,y) -4|[]-> f(x,g(x))
       f(g(g(x)),g(x)) <-6|[]- f(x,y) -5|[]-> f(g(x),g(g(x)))
       f(g(g(x)),g(x)) <-6|[]- f(x,y) -7|[]-> f(g(g(g(x))),g(g(g(x))))
       f(g(g(x)),g(x)) <-6|[]- f(x,y) -8|[]-> f(g(g(g(x))),g(g(x)))
       f(g(g(x)),g(x)) <-6|[]- f(x,y) -9|[]-> f(g(g(x)),g(g(g(x))))
       f(g(g(x)),g(x)) <-6|[]- f(x,y) -10|[]-> a()
       f(g(g(x)),g(x)) <-6|[]- f(x,y) -11|[]-> f(g(g(g(g(x)))),g(g(g(g(x)))))
       f(g(g(x)),g(x)) <-6|[]- f(x,y) -12|[]-> f(g(g(x)),g(g(x)))
       f(g(g(g(x))),g(g(g(x)))) <-7|[]- f(x,y) -1|[]-> f(x,x)
       f(g(g(g(x))),g(g(g(x)))) <-7|[]- f(x,y) -2|[]-> f(g(x),g(x))
       f(g(g(g(x))),g(g(g(x)))) <-7|[]- f(x,y) -3|[]-> f(g(x),x)
       f(g(g(g(x))),g(g(g(x)))) <-7|[]- f(x,y) -4|[]-> f(x,g(x))
       f(g(g(g(x))),g(g(g(x)))) <-7|[]- f(x,y) -5|[]-> f(g(x),g(g(x)))
       f(g(g(g(x))),g(g(g(x)))) <-7|[]- f(x,y) -6|[]-> f(g(g(x)),g(x))
       f(g(g(g(x))),g(g(g(x)))) <-7|[]- f(x,y) -8|[]-> f(g(g(g(x))),g(g(x)))
       f(g(g(g(x))),g(g(g(x)))) <-7|[]- f(x,y) -9|[]-> f(g(g(x)),g(g(g(x))))
       f(g(g(g(x))),g(g(g(x)))) <-7|[]- f(x,y) -10|[]-> a()
       f(g(g(g(x))),g(g(g(x)))) <-7|[]- f(x,y) -11|[]-> f(g(g(g(g(x)))),g(g(g(g(x)))))
       f(g(g(g(x))),g(g(g(x)))) <-7|[]- f(x,y) -12|[]-> f(g(g(x)),g(g(x)))
       f(g(g(g(x))),g(g(x))) <-8|[]- f(x,y) -1|[]-> f(x,x)
       f(g(g(g(x))),g(g(x))) <-8|[]- f(x,y) -2|[]-> f(g(x),g(x))
       f(g(g(g(x))),g(g(x))) <-8|[]- f(x,y) -3|[]-> f(g(x),x)
       f(g(g(g(x))),g(g(x))) <-8|[]- f(x,y) -4|[]-> f(x,g(x))
       f(g(g(g(x))),g(g(x))) <-8|[]- f(x,y) -5|[]-> f(g(x),g(g(x)))
       f(g(g(g(x))),g(g(x))) <-8|[]- f(x,y) -6|[]-> f(g(g(x)),g(x))
       f(g(g(g(x))),g(g(x))) <-8|[]- f(x,y) -7|[]-> f(g(g(g(x))),g(g(g(x))))
       f(g(g(g(x))),g(g(x))) <-8|[]- f(x,y) -9|[]-> f(g(g(x)),g(g(g(x))))
       f(g(g(g(x))),g(g(x))) <-8|[]- f(x,y) -10|[]-> a()
       f(g(g(g(x))),g(g(x))) <-8|[]- f(x,y) -11|[]-> f(g(g(g(g(x)))),g(g(g(g(x)))))
       f(g(g(g(x))),g(g(x))) <-8|[]- f(x,y) -12|[]-> f(g(g(x)),g(g(x)))
       f(g(g(x)),g(g(g(x)))) <-9|[]- f(x,y) -1|[]-> f(x,x)
       f(g(g(x)),g(g(g(x)))) <-9|[]- f(x,y) -2|[]-> f(g(x),g(x))
       f(g(g(x)),g(g(g(x)))) <-9|[]- f(x,y) -3|[]-> f(g(x),x)
       f(g(g(x)),g(g(g(x)))) <-9|[]- f(x,y) -4|[]-> f(x,g(x))
       f(g(g(x)),g(g(g(x)))) <-9|[]- f(x,y) -5|[]-> f(g(x),g(g(x)))
       f(g(g(x)),g(g(g(x)))) <-9|[]- f(x,y) -6|[]-> f(g(g(x)),g(x))
       f(g(g(x)),g(g(g(x)))) <-9|[]- f(x,y) -7|[]-> f(g(g(g(x))),g(g(g(x))))
       f(g(g(x)),g(g(g(x)))) <-9|[]- f(x,y) -8|[]-> f(g(g(g(x))),g(g(x)))
       f(g(g(x)),g(g(g(x)))) <-9|[]- f(x,y) -10|[]-> a()
       f(g(g(x)),g(g(g(x)))) <-9|[]- f(x,y) -11|[]-> f(g(g(g(g(x)))),g(g(g(g(x)))))
       f(g(g(x)),g(g(g(x)))) <-9|[]- f(x,y) -12|[]-> f(g(g(x)),g(g(x)))
       a() <-10|[]- f(x,y) -1|[]-> f(x,x)
       a() <-10|[]- f(x,y) -2|[]-> f(g(x),g(x))
       a() <-10|[]- f(x,y) -3|[]-> f(g(x),x)
       a() <-10|[]- f(x,y) -4|[]-> f(x,g(x))
       a() <-10|[]- f(x,y) -5|[]-> f(g(x),g(g(x)))
       a() <-10|[]- f(x,y) -6|[]-> f(g(g(x)),g(x))
       a() <-10|[]- f(x,y) -7|[]-> f(g(g(g(x))),g(g(g(x))))
       a() <-10|[]- f(x,y) -8|[]-> f(g(g(g(x))),g(g(x)))
       a() <-10|[]- f(x,y) -9|[]-> f(g(g(x)),g(g(g(x))))
       a() <-10|[]- f(x,y) -11|[]-> f(g(g(g(g(x)))),g(g(g(g(x)))))
       a() <-10|[]- f(x,y) -12|[]-> f(g(g(x)),g(g(x)))
       f(g(g(g(g(x)))),g(g(g(g(x))))) <-11|[]- f(x,y) -1|[]-> f(x,x)
       f(g(g(g(g(x)))),g(g(g(g(x))))) <-11|[]- f(x,y) -2|[]-> f(g(x),g(x))
       f(g(g(g(g(x)))),g(g(g(g(x))))) <-11|[]- f(x,y) -3|[]-> f(g(x),x)
       f(g(g(g(g(x)))),g(g(g(g(x))))) <-11|[]- f(x,y) -4|[]-> f(x,g(x))
       f(g(g(g(g(x)))),g(g(g(g(x))))) <-11|[]- f(x,y) -5|[]-> f(g(x),g(g(x)))
       f(g(g(g(g(x)))),g(g(g(g(x))))) <-11|[]- f(x,y) -6|[]-> f(g(g(x)),g(x))
       f(g(g(g(g(x)))),g(g(g(g(x))))) <-11|[]- f(x,y) -7|[]-> f(g(g(g(x))),g(g(g(x))))
       f(g(g(g(g(x)))),g(g(g(g(x))))) <-11|[]- f(x,y) -8|[]-> f(g(g(g(x))),g(g(x)))
       f(g(g(g(g(x)))),g(g(g(g(x))))) <-11|[]- f(x,y) -9|[]-> f(g(g(x)),g(g(g(x))))
       f(g(g(g(g(x)))),g(g(g(g(x))))) <-11|[]- f(x,y) -10|[]-> a()
       f(g(g(g(g(x)))),g(g(g(g(x))))) <-11|[]- f(x,y) -12|[]-> f(g(g(x)),g(g(x)))
       f(g(g(x)),g(g(x))) <-12|[]- f(x,y) -1|[]-> f(x,x)
       f(g(g(x)),g(g(x))) <-12|[]- f(x,y) -2|[]-> f(g(x),g(x))
       f(g(g(x)),g(g(x))) <-12|[]- f(x,y) -3|[]-> f(g(x),x)
       f(g(g(x)),g(g(x))) <-12|[]- f(x,y) -4|[]-> f(x,g(x))
       f(g(g(x)),g(g(x))) <-12|[]- f(x,y) -5|[]-> f(g(x),g(g(x)))
       f(g(g(x)),g(g(x))) <-12|[]- f(x,y) -6|[]-> f(g(g(x)),g(x))
       f(g(g(x)),g(g(x))) <-12|[]- f(x,y) -7|[]-> f(g(g(g(x))),g(g(g(x))))
       f(g(g(x)),g(g(x))) <-12|[]- f(x,y) -8|[]-> f(g(g(g(x))),g(g(x)))
       f(g(g(x)),g(g(x))) <-12|[]- f(x,y) -9|[]-> f(g(g(x)),g(g(g(x))))
       f(g(g(x)),g(g(x))) <-12|[]- f(x,y) -10|[]-> a()
       f(g(g(x)),g(g(x))) <-12|[]- f(x,y) -11|[]-> f(g(g(g(g(x)))),g(g(g(g(x)))))
      Closedness Processor (*parallel*):
       
       Qed