2.18/1.11 YES 2.18/1.11 2.18/1.11 Problem: 2.18/1.11 f(x) -> c() <= a() = b() 2.18/1.11 g(x, x) -> g(f(a()), f(b())) 2.18/1.11 2.18/1.11 Proof: 2.18/1.11 This system is confluent. 2.18/1.11 By \cite{ALS94}, Theorem 4.1. 2.18/1.11 This system is of type 3 or smaller. 2.18/1.11 This system is strongly deterministic. 2.18/1.11 All 0 critical pairs are joinable. 2.18/1.11 This system is quasi-decreasing. 2.18/1.11 By \cite{O02}, p. 214, Proposition 7.2.50. 2.18/1.11 This system is of type 3 or smaller. 2.18/1.11 This system is deterministic. 2.18/1.11 System R transformed to optimized U(R). 2.18/1.11 This system is terminating. 2.18/1.11 Call external tool: 2.18/1.11 ./ttt2.sh 2.18/1.11 Input: 2.18/1.11 ?1(b(), x) -> c() 2.18/1.11 f(x) -> ?1(a(), x) 2.18/1.11 g(x, x) -> g(f(a()), f(b())) 2.18/1.11 2.18/1.11 Matrix Interpretation Processor: dim=2 2.18/1.11 2.18/1.11 interpretation: 2.18/1.11 [1 0] [1 0] 2.18/1.11 [g](x0, x1) = [3 1]x0 + [1 0]x1, 2.18/1.11 2.18/1.11 [0] 2.18/1.11 [a] = [0], 2.18/1.11 2.18/1.11 [1 0] 2.18/1.11 [f](x0) = [0 2]x0, 2.18/1.11 2.18/1.11 [0] 2.18/1.11 [c] = [0], 2.18/1.11 2.18/1.11 [1 2] [1 0] 2.18/1.11 [?1](x0, x1) = [0 0]x0 + [0 0]x1, 2.18/1.11 2.18/1.11 [0] 2.18/1.11 [b] = [2] 2.18/1.11 orientation: 2.18/1.11 [1 0] [4] [0] 2.18/1.11 ?1(b(),x) = [0 0]x + [0] >= [0] = c() 2.18/1.11 2.18/1.11 [1 0] [1 0] 2.18/1.11 f(x) = [0 2]x >= [0 0]x = ?1(a(),x) 2.18/1.11 2.18/1.11 [2 0] [0] 2.18/1.11 g(x,x) = [4 1]x >= [0] = g(f(a()),f(b())) 2.18/1.11 problem: 2.18/1.11 f(x) -> ?1(a(),x) 2.18/1.11 g(x,x) -> g(f(a()),f(b())) 2.18/1.11 DP Processor: 2.18/1.11 DPs: 2.18/1.11 g#(x,x) -> f#(b()) 2.18/1.11 g#(x,x) -> f#(a()) 2.18/1.11 g#(x,x) -> g#(f(a()),f(b())) 2.18/1.12 TRS: 2.18/1.12 f(x) -> ?1(a(),x) 2.18/1.12 g(x,x) -> g(f(a()),f(b())) 2.18/1.12 TDG Processor: 2.18/1.12 DPs: 2.18/1.12 g#(x,x) -> f#(b()) 2.18/1.12 g#(x,x) -> f#(a()) 2.18/1.12 g#(x,x) -> g#(f(a()),f(b())) 2.18/1.12 TRS: 2.18/1.12 f(x) -> ?1(a(),x) 2.18/1.12 g(x,x) -> g(f(a()),f(b())) 2.18/1.12 graph: 2.18/1.12 g#(x,x) -> g#(f(a()),f(b())) -> g#(x,x) -> g#(f(a()),f(b())) 2.18/1.12 g#(x,x) -> g#(f(a()),f(b())) -> g#(x,x) -> f#(a()) 2.18/1.12 g#(x,x) -> g#(f(a()),f(b())) -> g#(x,x) -> f#(b()) 2.18/1.12 SCC Processor: 2.18/1.12 #sccs: 1 2.18/1.12 #rules: 1 2.18/1.12 #arcs: 3/9 2.18/1.12 DPs: 2.18/1.12 g#(x,x) -> g#(f(a()),f(b())) 2.18/1.12 TRS: 2.18/1.12 f(x) -> ?1(a(),x) 2.18/1.12 g(x,x) -> g(f(a()),f(b())) 2.18/1.12 CDG Processor: 2.18/1.12 DPs: 2.18/1.12 g#(x,x) -> g#(f(a()),f(b())) 2.18/1.12 TRS: 2.18/1.12 f(x) -> ?1(a(),x) 2.18/1.12 g(x,x) -> g(f(a()),f(b())) 2.18/1.12 graph: 2.18/1.12 2.18/1.12 Qed 2.18/1.12 3.04/1.20 EOF