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

Proof:
 Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
  G(x14) -> F(x14)
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [G](x0) = 4x0 + 1,
    
    [F](x0) = 4x0
   orientation:
    G(x14) = 4x14 + 1 >= 4x14 = F(x14)
   problem:
    
   Qed