18.85/7.83 MAYBE 18.85/7.83 18.85/7.83 Problem: 18.85/7.83 f(x) -> b() <= f(x) = z, x = z 18.85/7.83 a() -> f(a()) 18.85/7.83 18.85/7.83 Proof: 18.85/7.83 ConCon could not decide confluence of the system. 18.85/7.83 \cite{GNG13}, Theorem 9 does not apply. 18.85/7.83 System R transformed to optimized U(R). 18.85/7.83 The external tool could not decide confluence of the system. 18.85/7.83 Call external tool: 18.85/7.83 ./csi.sh 18.85/7.83 Input: 18.85/7.83 ?1(z, x, z) -> b() 18.85/7.83 ?2(z, x) -> ?1(x, x, z) 18.85/7.83 f(x) -> ?2(f(x), x) 18.85/7.83 a() -> f(a()) 18.85/7.83 18.85/7.83 18.85/7.83 EOF