Problem:
 F(c(x)) -> G(x)
 G(x) -> F(x)
 c(x) -> x

Proof:
 Church Rosser Transformation Processor (kb):
  F(c(x)) -> G(x)
  G(x) -> F(x)
  c(x) -> x
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [G](x0) = x0 + 5,
    
    [F](x0) = x0,
    
    [c](x0) = 4x0 + 5
   orientation:
    F(c(x)) = 4x + 5 >= x + 5 = G(x)
    
    G(x) = x + 5 >= x = F(x)
    
    c(x) = 4x + 5 >= x = x
   problem:
    F(c(x)) -> G(x)
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [G](x0) = x0,
     
     [F](x0) = x0 + 3,
     
     [c](x0) = x0
    orientation:
     F(c(x)) = x + 3 >= x = G(x)
    problem:
     
    Qed