0.00/0.79 YES 0.00/0.79 0.00/0.79 Problem: 0.00/0.79 a() -> c() 0.00/0.79 b() -> c() 0.00/0.79 f(x) -> x <= a() = x 0.00/0.79 0.00/0.79 Proof: 0.00/0.79 This system is confluent. 0.00/0.79 By \cite{ALS94}, Theorem 4.1. 0.00/0.79 This system is of type 3 or smaller. 0.00/0.79 This system is strongly deterministic. 0.00/0.79 All 0 critical pairs are joinable. 0.00/0.79 This system is quasi-decreasing. 0.00/0.79 By \cite{O02}, p. 214, Proposition 7.2.50. 0.00/0.79 This system is of type 3 or smaller. 0.00/0.79 This system is deterministic. 0.00/0.79 System R transformed to optimized U(R). 0.00/0.79 This system is terminating. 0.00/0.79 Call external tool: 0.00/0.79 ./ttt2.sh 0.00/0.79 Input: 0.00/0.79 a() -> c() 0.00/0.79 b() -> c() 0.00/0.79 ?1(x, x) -> x 0.00/0.79 f(x) -> ?1(a(), x) 0.00/0.79 0.00/0.79 Polynomial Interpretation Processor: 0.00/0.79 dimension: 1 0.00/0.79 interpretation: 0.00/0.79 [f](x0) = 7x0 + 7x0x0 + 4, 0.00/0.79 0.00/0.79 [?1](x0, x1) = 4x1 + 2x0x0 + 7x1x1 + 1, 0.00/0.79 0.00/0.79 [b] = 2, 0.00/0.79 0.00/0.79 [c] = 0, 0.00/0.79 0.00/0.79 [a] = 1 0.00/0.79 orientation: 0.00/0.79 a() = 1 >= 0 = c() 0.00/0.79 0.00/0.79 b() = 2 >= 0 = c() 0.00/0.79 0.00/0.79 ?1(x,x) = 4x + 9x*x + 1 >= x = x 0.00/0.79 0.00/0.79 f(x) = 7x + 7x*x + 4 >= 4x + 7x*x + 3 = ?1(a(),x) 0.00/0.79 problem: 0.00/0.79 0.00/0.79 Qed 0.00/0.79 0.00/0.81 EOF