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