5.66/2.34 YES 5.66/2.34 5.66/2.34 Proof: 5.66/2.34 This system is confluent. 5.66/2.34 By \cite{ALS94}, Theorem 4.1. 5.66/2.34 This system is of type 3 or smaller. 5.66/2.34 This system is strongly deterministic. 5.66/2.35 This system is quasi-decreasing. 5.66/2.35 By \cite{O02}, p. 214, Proposition 7.2.50. 5.66/2.35 This system is of type 3 or smaller. 5.66/2.35 This system is deterministic. 5.66/2.35 System R transformed to U(R). 5.66/2.35 This system is terminating. 5.66/2.35 Call external tool: 5.66/2.35 ./ttt2.sh 5.66/2.35 Input: 5.66/2.35 (VAR x y) 5.66/2.35 (RULES 5.66/2.35 a -> c 5.66/2.35 a -> d 5.66/2.35 b -> c 5.66/2.35 b -> d 5.66/2.35 c -> e 5.66/2.35 d -> e 5.66/2.35 k -> e 5.66/2.35 l -> e 5.66/2.35 s(c) -> t(k) 5.66/2.35 s(c) -> t(l) 5.66/2.35 s(e) -> t(e) 5.66/2.35 g(x, x) -> h(x, x) 5.66/2.35 ?1(t(y), x) -> pair(x, y) 5.66/2.35 f(x) -> ?1(s(x), x) 5.66/2.35 ) 5.66/2.35 5.66/2.35 Matrix Interpretation Processor: dim=1 5.66/2.35 5.66/2.35 interpretation: 5.66/2.35 [f](x0) = 7x0 + 4, 5.66/2.35 5.66/2.35 [pair](x0, x1) = x0 + x1, 5.66/2.35 5.66/2.35 [?1](x0, x1) = 2x0 + x1, 5.66/2.35 5.66/2.35 [h](x0, x1) = 4x0 + 4x1, 5.66/2.35 5.66/2.35 [g](x0, x1) = 6x0 + 2x1 + 4, 5.66/2.35 5.66/2.35 [t](x0) = 2x0 + 2, 5.66/2.35 5.66/2.35 [s](x0) = 3x0 + 2, 5.66/2.35 5.66/2.35 [l] = 4, 5.66/2.35 5.66/2.35 [k] = 3, 5.66/2.35 5.66/2.35 [e] = 0, 5.66/2.35 5.66/2.35 [b] = 3, 5.66/2.35 5.66/2.35 [d] = 1, 5.66/2.35 5.66/2.35 [c] = 3, 5.66/2.35 5.66/2.35 [a] = 3 5.66/2.35 orientation: 5.66/2.35 a() = 3 >= 3 = c() 5.66/2.35 5.66/2.35 a() = 3 >= 1 = d() 5.66/2.35 5.66/2.35 b() = 3 >= 3 = c() 5.66/2.35 5.66/2.35 b() = 3 >= 1 = d() 5.66/2.35 5.66/2.35 c() = 3 >= 0 = e() 5.66/2.35 5.66/2.35 d() = 1 >= 0 = e() 5.66/2.35 5.66/2.35 k() = 3 >= 0 = e() 5.66/2.35 5.66/2.35 l() = 4 >= 0 = e() 5.66/2.35 5.66/2.35 s(c()) = 11 >= 8 = t(k()) 5.66/2.35 5.66/2.35 s(c()) = 11 >= 10 = t(l()) 5.66/2.35 5.66/2.35 s(e()) = 2 >= 2 = t(e()) 5.66/2.35 5.66/2.35 g(x,x) = 8x + 4 >= 8x = h(x,x) 5.66/2.35 5.66/2.35 ?1(t(y),x) = x + 4y + 4 >= x + y = pair(x,y) 5.66/2.35 5.66/2.35 f(x) = 7x + 4 >= 7x + 4 = ?1(s(x),x) 5.66/2.35 problem: 5.66/2.35 a() -> c() 5.66/2.35 b() -> c() 5.66/2.35 s(e()) -> t(e()) 5.66/2.35 f(x) -> ?1(s(x),x) 5.66/2.35 Matrix Interpretation Processor: dim=1 5.66/2.35 5.66/2.35 interpretation: 5.66/2.35 [f](x0) = 6x0 + 1, 5.66/2.35 5.66/2.35 [?1](x0, x1) = x0 + 5x1, 5.66/2.35 5.66/2.35 [t](x0) = x0, 5.66/2.35 5.66/2.35 [s](x0) = x0, 5.66/2.35 5.66/2.35 [e] = 4, 5.66/2.35 5.66/2.35 [b] = 0, 5.66/2.35 5.66/2.35 [c] = 0, 5.66/2.35 5.66/2.35 [a] = 0 5.66/2.35 orientation: 5.66/2.35 a() = 0 >= 0 = c() 5.66/2.35 5.66/2.36 b() = 0 >= 0 = c() 5.66/2.36 5.66/2.36 s(e()) = 4 >= 4 = t(e()) 5.66/2.36 5.66/2.36 f(x) = 6x + 1 >= 6x = ?1(s(x),x) 5.66/2.36 problem: 5.66/2.36 a() -> c() 5.66/2.36 b() -> c() 5.66/2.36 s(e()) -> t(e()) 5.66/2.36 Matrix Interpretation Processor: dim=3 5.66/2.36 5.66/2.36 interpretation: 5.66/2.36 [1 0 0] 5.66/2.36 [t](x0) = [0 0 0]x0 5.66/2.36 [0 0 0] , 5.66/2.36 5.66/2.36 [1 0 0] [1] 5.66/2.36 [s](x0) = [0 0 0]x0 + [0] 5.66/2.36 [0 0 0] [0], 5.66/2.36 5.66/2.36 [0] 5.66/2.36 [e] = [0] 5.66/2.36 [0], 5.66/2.36 5.66/2.36 [0] 5.66/2.36 [b] = [0] 5.66/2.36 [0], 5.66/2.36 5.66/2.36 [0] 5.66/2.36 [c] = [0] 5.66/2.36 [0], 5.66/2.36 5.66/2.36 [0] 5.66/2.36 [a] = [0] 5.66/2.36 [0] 5.66/2.36 orientation: 5.66/2.36 [0] [0] 5.66/2.36 a() = [0] >= [0] = c() 5.66/2.36 [0] [0] 5.66/2.36 5.66/2.36 [0] [0] 5.66/2.36 b() = [0] >= [0] = c() 5.66/2.36 [0] [0] 5.66/2.36 5.66/2.36 [1] [0] 5.66/2.36 s(e()) = [0] >= [0] = t(e()) 5.66/2.36 [0] [0] 5.66/2.36 problem: 5.66/2.36 a() -> c() 5.66/2.36 b() -> c() 5.66/2.36 Matrix Interpretation Processor: dim=3 5.66/2.36 5.66/2.36 interpretation: 5.66/2.36 [1] 5.66/2.36 [b] = [0] 5.66/2.36 [0], 5.66/2.36 5.66/2.36 [0] 5.66/2.36 [c] = [0] 5.66/2.36 [0], 5.66/2.36 5.66/2.36 [0] 5.66/2.36 [a] = [0] 5.66/2.36 [0] 5.66/2.36 orientation: 5.66/2.36 [0] [0] 5.83/2.37 a() = [0] >= [0] = c() 5.83/2.37 [0] [0] 5.83/2.37 5.83/2.37 [1] [0] 5.83/2.37 b() = [0] >= [0] = c() 5.83/2.37 [0] [0] 5.83/2.37 problem: 5.83/2.37 a() -> c() 5.83/2.37 Matrix Interpretation Processor: dim=3 5.83/2.37 5.83/2.37 interpretation: 5.83/2.37 [0] 5.83/2.37 [c] = [0] 5.83/2.37 [0], 5.83/2.37 5.83/2.37 [1] 5.83/2.37 [a] = [0] 5.83/2.37 [1] 5.83/2.37 orientation: 5.83/2.37 [1] [0] 5.83/2.37 a() = [0] >= [0] = c() 5.83/2.37 [1] [0] 5.83/2.37 problem: 5.83/2.37 5.83/2.37 Qed 5.83/2.37 All 8 critical pairs are joinable. 5.83/2.37 Overlap: (rule1: s(c) -> t(k), rule2: s(c) -> t(l), pos: ε, mgu: {}) 5.83/2.37 CP: t(l) = t(k) 5.83/2.37 This critical pair is context-joinable. 5.83/2.37 Overlap: (rule1: b -> c, rule2: b -> d, pos: ε, mgu: {}) 5.83/2.37 CP: d = c 5.83/2.37 This critical pair is context-joinable. 5.83/2.37 Overlap: (rule1: a -> d, rule2: a -> c, pos: ε, mgu: {}) 5.83/2.37 CP: c = d 5.83/2.37 This critical pair is context-joinable. 5.83/2.37 Overlap: (rule1: b -> d, rule2: b -> c, pos: ε, mgu: {}) 5.83/2.37 CP: c = d 5.83/2.37 This critical pair is context-joinable. 5.83/2.37 Overlap: (rule1: s(c) -> t(k), rule2: c -> e, pos: 1, mgu: {}) 5.83/2.37 CP: s(e) = t(k) 5.83/2.37 This critical pair is context-joinable. 5.83/2.37 Overlap: (rule1: a -> c, rule2: a -> d, pos: ε, mgu: {}) 5.83/2.37 CP: d = c 5.83/2.37 This critical pair is context-joinable. 5.83/2.37 Overlap: (rule1: s(c) -> t(l), rule2: s(c) -> t(k), pos: ε, mgu: {}) 5.83/2.37 CP: t(k) = t(l) 5.83/2.37 This critical pair is context-joinable. 5.83/2.37 Overlap: (rule1: s(c) -> t(l), rule2: c -> e, pos: 1, mgu: {}) 5.83/2.37 CP: s(e) = t(l) 5.83/2.37 This critical pair is context-joinable. 5.83/2.37 5.84/2.38 EOF