Problem:
 f(f(x)) -> x
 f(x) -> f(f(x))

Proof:
 Church Rosser Transformation Processor (no redundant rules):
  strict:
   
  weak:
   
  critical peaks: 4
   f(f(f(x))) <-0|[]- f(f(x)) -1|[]-> x
   f(f(f(x))) <-0|0[]- f(f(x)) -1|[]-> x
   x9 <-1|[]- f(f(x9)) -0|[]-> f(f(f(x9)))
   f(x10) <-1|0[]- f(f(f(x10))) -1|[]-> f(x10)
  Redundant Rules Transformation:
   f(x) -> f(f(x))
   f(x) -> f(f(f(x)))
   f(x) -> x
   f(f(x)) -> x
   Church Rosser Transformation Processor:
    strict:
     
    weak:
     
    critical peaks: 16
     f(f(x)) <-0|[]- f(x) -1|[]-> f(f(f(x)))
     f(f(x)) <-0|[]- f(x) -2|[]-> x
     f(f(f(x))) <-0|[]- f(f(x)) -3|[]-> x
     f(f(f(x))) <-0|0[]- f(f(x)) -3|[]-> x
     f(f(f(x))) <-1|[]- f(x) -0|[]-> f(f(x))
     f(f(f(x))) <-1|[]- f(x) -2|[]-> x
     f(f(f(f(x)))) <-1|[]- f(f(x)) -3|[]-> x
     f(f(f(f(x)))) <-1|0[]- f(f(x)) -3|[]-> x
     x <-2|[]- f(x) -0|[]-> f(f(x))
     x <-2|[]- f(x) -1|[]-> f(f(f(x)))
     f(x) <-2|[]- f(f(x)) -3|[]-> x
     f(x) <-2|0[]- f(f(x)) -3|[]-> x
     x43 <-3|[]- f(f(x43)) -0|[]-> f(f(f(x43)))
     x44 <-3|[]- f(f(x44)) -1|[]-> f(f(f(f(x44))))
     x45 <-3|[]- f(f(x45)) -2|[]-> f(x45)
     f(x46) <-3|0[]- f(f(f(x46))) -3|[]-> f(x46)
    Shift Processor lab=left (dd) (force):
     strict:
      f(x) -> f(f(x))
      f(x) -> f(f(f(x)))
      f(f(f(x))) -> f(f(x))
      f(f(x)) -> f(f(f(x)))
      f(f(x)) -> f(f(f(f(x))))
      f(f(f(x))) -> f(f(f(f(x))))
      f(f(x)) -> f(x)
      f(f(f(x))) -> f(x)
      f(x) -> f(f(x))
      f(x) -> x
      f(f(x)) -> x
      f(f(x)) -> f(f(f(x)))
      f(f(x)) -> x
      f(f(f(x))) -> f(f(x))
      f(f(x)) -> x
      f(f(f(x))) -> f(x)
      f(x) -> x
      f(f(x)) -> f(f(f(x)))
      f(f(x)) -> x
      f(f(f(x))) -> f(f(x))
      f(f(x)) -> x
      f(f(f(x))) -> f(x)
      f(x) -> x
      f(x) -> f(f(f(x)))
      f(x) -> f(f(x))
      f(f(x)) -> f(f(f(x)))
      f(f(f(x))) -> f(f(f(f(x))))
      f(f(x)) -> f(f(f(f(x))))
      f(f(f(x))) -> f(f(x))
      f(f(f(x))) -> f(x)
      f(f(x)) -> f(x)
      f(x) -> f(f(f(x)))
      f(x) -> x
      f(f(f(x))) -> f(f(x))
      f(f(x)) -> x
      f(f(f(x))) -> f(x)
      f(x) -> x
      f(f(x)) -> f(f(f(f(x))))
      f(f(x)) -> x
      f(f(f(f(x)))) -> f(f(x))
      f(f(x)) -> x
      f(f(x)) -> f(f(f(f(x))))
      f(f(x)) -> x
      f(f(f(f(x)))) -> f(f(x))
      f(f(x)) -> x
      f(x) -> x
      f(x) -> f(f(x))
      f(f(x)) -> x
      f(x) -> x
      f(x) -> f(f(f(x)))
      f(f(f(x))) -> f(f(x))
      f(f(x)) -> x
      f(f(f(x))) -> f(x)
      f(x) -> x
      f(f(x)) -> f(x)
      f(f(x)) -> x
      f(x) -> x
      f(f(x)) -> f(x)
      f(f(x)) -> x
      f(x) -> x
      f(f(x43)) -> x43
      f(f(x43)) -> f(f(f(x43)))
      f(f(f(x43))) -> f(f(x43))
      f(f(x43)) -> x43
      f(f(f(x43))) -> f(x43)
      f(x43) -> x43
      f(f(x44)) -> x44
      f(f(x44)) -> f(f(f(f(x44))))
      f(f(f(f(x44)))) -> f(f(x44))
      f(f(x44)) -> x44
      f(f(x45)) -> x45
      f(f(x45)) -> f(x45)
      f(x45) -> x45
      f(f(f(x46))) -> f(x46)
      f(f(f(x46))) -> f(x46)
     weak:
      f(x) -> f(f(x))
      f(x) -> f(f(f(x)))
      f(x) -> x
      f(f(x)) -> x
     Shift Processor (ldh) lab=left (force):
      strict:
       
      weak:
       
      Rule Labeling Processor:
       strict:
        
       weak:
        
       rule labeling (right):
        f(x) -> f(f(x)): 1
        f(x) -> f(f(f(x))): 1
        f(x) -> x: 0
        f(f(x)) -> x: 0
       Rule Labeling Processor:
        strict:
         
        weak:
         
        rule labeling (left):
         f(x) -> f(f(x)): 0
         f(x) -> f(f(f(x))): 0
         f(x) -> x: 0
         f(f(x)) -> x: 0
        Decreasing Processor:
         The following diagrams are decreasing:
         peak:
          f(f(x)) <-0|[==0,==1,==1]- f(x) -1|[==0,==1,==1]-> f(f(f(x)))
         joins (1):
          
          f(f(f(x))) -2|[==0,==1,>>0]-> f(f(x))
         peak:
          f(f(x)) <-0|[==0,==1,=?1]- f(x) -2|[==0,==1,>=0]-> x
         joins (1):
          f(f(x)) -3|[==0,==1,>=0]-> x
          
         peak:
          f(f(f(x))) <-0|[==0,==1,=?1]- f(f(x)) -3|[==0,==1,>=0]-> x
         joins (1):
          f(f(f(x))) -2|[==0,==1,>=0]-> f(f(x)) -3|[==0,==1,>=0]-> x
          
         peak:
          f(f(f(x))) <-0|0[==0,==1,=?1]- f(f(x)) -3|[==0,==1,>=0]-> x
         joins (1):
          f(f(f(x))) -2|[==0,==1,>=0]-> f(f(x)) -3|[==0,==1,>=0]-> x
          
         peak:
          f(f(f(x))) <-1|[==0,==1,==1]- f(x) -0|[==0,==1,==1]-> f(f(x))
         joins (1):
          
          f(f(x)) -0|[==0,==1,==1]-> f(f(f(x)))
         peak:
          f(f(f(x))) <-1|[==0,==1,=?1]- f(x) -2|[==0,==1,>=0]-> x
         joins (1):
          f(f(f(x))) -2|[==0,==1,>=0]-> f(f(x)) -3|[==0,==1,>=0]-> x
          
         peak:
          f(f(f(f(x)))) <-1|[==0,==1,=?1]- f(f(x)) -3|[==0,==1,>=0]-> x
         joins (1):
          f(f(f(f(x)))) -3|[==0,==1,>=0]-> f(f(x)) -3|[==0,==1,>=0]-> x
          
         peak:
          f(f(f(f(x)))) <-1|0[==0,==1,=?1]- f(f(x)) -3|[==0,==1,>=0]-> x
         joins (1):
          f(f(f(f(x)))) -3|[==0,==1,>=0]-> f(f(x)) -3|[==0,==1,>=0]-> x
          
         peak:
          x <-2|[==0,==1,=>0]- f(x) -0|[==0,==1,?=1]-> f(f(x))
         joins (1):
          
          f(f(x)) -3|[==0,==1,=>0]-> x
         peak:
          x <-2|[==0,==1,=>0]- f(x) -1|[==0,==1,?=1]-> f(f(f(x)))
         joins (1):
          
          f(f(f(x))) -2|[==0,==1,=>0]-> f(f(x)) -3|[==0,==1,=>0]-> x
         peak:
          f(x) <-2|[==0,==1,==0]- f(f(x)) -3|[==0,==1,==0]-> x
         joins (1):
          f(x) -2|[==0,==1,==0]-> x
          
         peak:
          f(x) <-2|0[==0,==1,==0]- f(f(x)) -3|[==0,==1,==0]-> x
         joins (1):
          f(x) -2|[==0,==1,==0]-> x
          
         peak:
          x43 <-3|[==0,==1,=>0]- f(f(x43)) -0|[==0,==1,?=1]-> f(f(f(x43)))
         joins (1):
          
          f(f(f(x43))) -2|[==0,==1,=>0]-> f(f(x43)) -3|[==0,==1,=>0]-> x43
         peak:
          x44 <-3|[==0,==1,=>0]- f(f(x44)) -1|[==0,==1,?=1]-> f(f(f(f(x44))))
         joins (1):
          
          f(f(f(f(x44)))) -3|[==0,==1,=>0]-> f(f(x44)) -3|[==0,==1,=>0]-> x44
         peak:
          x45 <-3|[==0,==1,==0]- f(f(x45)) -2|[==0,==1,==0]-> f(x45)
         joins (1):
          
          f(x45) -2|[==0,==1,==0]-> x45
         peak:
          f(x46) <-3|0[==0,==1,==0]- f(f(f(x46))) -3|[==0,==1,==0]-> f(x46)
         joins (1):
          
          
         Qed