5.59/2.35 MAYBE 5.59/2.35 5.59/2.35 Proof: 5.59/2.35 ConCon could not decide confluence of the system. 5.59/2.35 \cite{ALS94}, Theorem 4.1 does not apply. 5.59/2.35 This system is of type 3 or smaller. 5.59/2.35 This system is strongly deterministic. 5.59/2.35 This system is quasi-decreasing. 5.59/2.35 By \cite{O02}, p. 214, Proposition 7.2.50. 5.59/2.35 This system is of type 3 or smaller. 5.59/2.35 This system is deterministic. 5.59/2.35 System R transformed to U(R). 5.59/2.35 This system is terminating. 5.59/2.35 Call external tool: 5.59/2.35 ./ttt2.sh 5.59/2.35 Input: 5.59/2.35 (VAR x y) 5.59/2.35 (RULES 5.59/2.35 ?1(d, x, y) -> g(x) 5.59/2.35 f(x, y) -> ?1(a, x, y) 5.59/2.35 ?2(d, x, y) -> h(x) 5.59/2.35 f(x, y) -> ?2(b, x, y) 5.59/2.35 g(s(x)) -> x 5.59/2.35 h(s(x)) -> x 5.59/2.35 a -> d 5.59/2.35 b -> d 5.59/2.35 ) 5.59/2.35 5.59/2.35 Matrix Interpretation Processor: dim=3 5.59/2.35 5.59/2.35 interpretation: 5.59/2.35 [1 0 1] 5.59/2.35 [s](x0) = [0 0 0]x0 5.59/2.35 [1 1 1] , 5.59/2.35 5.59/2.35 [0] 5.59/2.35 [b] = [0] 5.59/2.35 [0], 5.59/2.35 5.59/2.35 [1 0 0] 5.59/2.35 [h](x0) = [0 0 1]x0 5.59/2.35 [0 0 1] , 5.59/2.35 5.59/2.35 [1 0 0] [1 0 0] [1 0 0] [1] 5.59/2.35 [?2](x0, x1, x2) = [0 0 0]x0 + [0 0 1]x1 + [0 0 0]x2 + [0] 5.59/2.35 [0 0 0] [0 0 1] [0 0 0] [0], 5.59/2.35 5.59/2.35 [0] 5.59/2.35 [a] = [1] 5.59/2.35 [0], 5.59/2.35 5.59/2.35 [1 0 0] [1 0 0] [1] 5.59/2.35 [f](x0, x1) = [0 0 1]x0 + [0 0 0]x1 + [0] 5.59/2.35 [0 0 1] [0 0 0] [0], 5.59/2.35 5.59/2.35 [1 0 0] 5.59/2.35 [g](x0) = [0 0 1]x0 5.59/2.35 [0 0 1] , 5.59/2.35 5.59/2.35 [1 0 0] [1 0 0] [1 0 0] [1] 5.59/2.35 [?1](x0, x1, x2) = [0 0 0]x0 + [0 0 1]x1 + [0 0 0]x2 + [0] 5.59/2.35 [0 0 0] [0 0 1] [0 0 0] [0], 5.59/2.35 5.59/2.35 [0] 5.59/2.35 [d] = [0] 5.59/2.35 [0] 5.59/2.35 orientation: 5.59/2.35 [1 0 0] [1 0 0] [1] [1 0 0] 5.59/2.35 ?1(d(),x,y) = [0 0 1]x + [0 0 0]y + [0] >= [0 0 1]x = g(x) 5.59/2.35 [0 0 1] [0 0 0] [0] [0 0 1] 5.59/2.35 5.59/2.35 [1 0 0] [1 0 0] [1] [1 0 0] [1 0 0] [1] 5.59/2.35 f(x,y) = [0 0 1]x + [0 0 0]y + [0] >= [0 0 1]x + [0 0 0]y + [0] = ?1(a(),x,y) 5.59/2.35 [0 0 1] [0 0 0] [0] [0 0 1] [0 0 0] [0] 5.59/2.35 5.59/2.36 [1 0 0] [1 0 0] [1] [1 0 0] 5.59/2.36 ?2(d(),x,y) = [0 0 1]x + [0 0 0]y + [0] >= [0 0 1]x = h(x) 5.59/2.36 [0 0 1] [0 0 0] [0] [0 0 1] 5.59/2.36 5.59/2.36 [1 0 0] [1 0 0] [1] [1 0 0] [1 0 0] [1] 5.59/2.36 f(x,y) = [0 0 1]x + [0 0 0]y + [0] >= [0 0 1]x + [0 0 0]y + [0] = ?2(b(),x,y) 5.59/2.36 [0 0 1] [0 0 0] [0] [0 0 1] [0 0 0] [0] 5.59/2.36 5.59/2.36 [1 0 1] 5.59/2.36 g(s(x)) = [1 1 1]x >= x = x 5.59/2.36 [1 1 1] 5.59/2.36 5.59/2.36 [1 0 1] 5.59/2.36 h(s(x)) = [1 1 1]x >= x = x 5.59/2.36 [1 1 1] 5.59/2.36 5.59/2.36 [0] [0] 5.59/2.36 a() = [1] >= [0] = d() 5.59/2.36 [0] [0] 5.59/2.36 5.59/2.36 [0] [0] 5.59/2.36 b() = [0] >= [0] = d() 5.59/2.36 [0] [0] 5.59/2.36 problem: 5.59/2.36 f(x,y) -> ?1(a(),x,y) 5.59/2.36 f(x,y) -> ?2(b(),x,y) 5.59/2.36 g(s(x)) -> x 5.59/2.36 h(s(x)) -> x 5.59/2.36 a() -> d() 5.59/2.36 b() -> d() 5.59/2.36 Matrix Interpretation Processor: dim=3 5.59/2.36 5.59/2.36 interpretation: 5.59/2.36 [1 0 0] 5.59/2.36 [s](x0) = [0 0 0]x0 5.59/2.36 [0 1 1] , 5.59/2.36 5.59/2.36 [0] 5.59/2.36 [b] = [0] 5.59/2.36 [0], 5.59/2.36 5.59/2.36 [1 0 0] 5.59/2.36 [h](x0) = [0 0 1]x0 5.59/2.36 [0 0 1] , 5.59/2.36 5.59/2.36 [1 0 0] [1 0 0] [1 0 0] 5.59/2.36 [?2](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2 5.59/2.36 [0 0 0] [0 0 0] [0 0 0] , 5.59/2.36 5.59/2.36 [0] 5.59/2.36 [a] = [0] 5.59/2.36 [1], 5.59/2.36 5.59/2.36 [1 0 0] [1 0 0] [1] 5.59/2.36 [f](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0] 5.59/2.36 [0 0 0] [0 0 0] [1], 5.59/2.36 5.59/2.36 [1 0 0] 5.59/2.36 [g](x0) = [0 0 1]x0 5.59/2.36 [0 0 1] , 5.59/2.36 5.59/2.36 [1 0 0] [1 0 0] [1 0 0] 5.59/2.36 [?1](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2 5.59/2.36 [0 0 0] [0 0 0] [0 0 0] , 5.59/2.36 5.59/2.36 [0] 5.59/2.36 [d] = [0] 5.59/2.36 [0] 5.59/2.36 orientation: 5.59/2.36 [1 0 0] [1 0 0] [1] [1 0 0] [1 0 0] 5.59/2.36 f(x,y) = [0 0 0]x + [0 0 0]y + [0] >= [0 0 0]x + [0 0 0]y = ?1(a(),x,y) 5.59/2.36 [0 0 0] [0 0 0] [1] [0 0 0] [0 0 0] 5.59/2.36 5.59/2.36 [1 0 0] [1 0 0] [1] [1 0 0] [1 0 0] 5.59/2.36 f(x,y) = [0 0 0]x + [0 0 0]y + [0] >= [0 0 0]x + [0 0 0]y = ?2(b(),x,y) 5.59/2.36 [0 0 0] [0 0 0] [1] [0 0 0] [0 0 0] 5.59/2.36 5.59/2.36 [1 0 0] 5.59/2.36 g(s(x)) = [0 1 1]x >= x = x 5.59/2.36 [0 1 1] 5.59/2.36 5.59/2.36 [1 0 0] 5.59/2.36 h(s(x)) = [0 1 1]x >= x = x 5.59/2.36 [0 1 1] 5.59/2.36 5.59/2.36 [0] [0] 5.59/2.36 a() = [0] >= [0] = d() 5.59/2.36 [1] [0] 5.59/2.36 5.59/2.36 [0] [0] 5.59/2.36 b() = [0] >= [0] = d() 5.59/2.36 [0] [0] 5.59/2.36 problem: 5.59/2.36 g(s(x)) -> x 5.59/2.36 h(s(x)) -> x 5.59/2.36 a() -> d() 5.59/2.36 b() -> d() 5.59/2.36 Matrix Interpretation Processor: dim=3 5.59/2.36 5.59/2.36 interpretation: 5.59/2.36 [1 0 1] [0] 5.59/2.36 [s](x0) = [1 0 1]x0 + [1] 5.59/2.36 [0 1 1] [0], 5.59/2.36 5.59/2.36 [1] 5.59/2.36 [b] = [0] 5.59/2.36 [1], 5.59/2.36 5.59/2.36 [1 1 0] 5.59/2.36 [h](x0) = [0 0 1]x0 5.59/2.36 [0 1 0] , 5.59/2.36 5.59/2.36 [1] 5.59/2.36 [a] = [0] 5.59/2.36 [1], 5.59/2.36 5.59/2.36 [1 0 0] [0] 5.59/2.36 [g](x0) = [0 0 1]x0 + [1] 5.59/2.36 [1 1 0] [1], 5.59/2.36 5.59/2.36 [0] 5.59/2.36 [d] = [0] 5.59/2.36 [0] 5.59/2.36 orientation: 5.59/2.36 [1 0 1] [0] 5.59/2.36 g(s(x)) = [0 1 1]x + [1] >= x = x 5.59/2.36 [2 0 2] [2] 5.59/2.36 5.59/2.36 [2 0 2] [1] 5.59/2.36 h(s(x)) = [0 1 1]x + [0] >= x = x 5.59/2.36 [1 0 1] [1] 5.59/2.36 5.59/2.36 [1] [0] 5.59/2.36 a() = [0] >= [0] = d() 5.59/2.36 [1] [0] 5.59/2.36 5.59/2.36 [1] [0] 5.59/2.36 b() = [0] >= [0] = d() 5.59/2.36 [1] [0] 5.59/2.37 problem: 5.59/2.37 g(s(x)) -> x 5.59/2.37 Matrix Interpretation Processor: dim=3 5.59/2.37 5.59/2.37 interpretation: 5.59/2.37 [1 0 0] 5.59/2.37 [s](x0) = [0 0 1]x0 5.59/2.37 [0 1 0] , 5.59/2.37 5.59/2.37 [1 0 0] [1] 5.59/2.37 [g](x0) = [0 0 1]x0 + [0] 5.59/2.37 [0 1 0] [0] 5.59/2.37 orientation: 5.59/2.37 [1] 5.59/2.37 g(s(x)) = x + [0] >= x = x 5.59/2.37 [0] 5.59/2.37 problem: 5.59/2.37 5.59/2.37 Qed 5.59/2.37 This critical pair is conditional. 5.59/2.37 This critical pair has some non-trivial conditions. 5.59/2.37 ConCon could not decide whether all 2 critical pairs are joinable or not. 5.59/2.37 Overlap: (rule1: f(z, x') -> h(z) <= b = d, rule2: f(y', z') -> g(y') <= a = d, pos: ε, mgu: {(z,y'), (x',z')}) 5.59/2.37 CP: g(y') = h(y') <= b = d, a = d 5.59/2.37 ConCon could not decide infeasibility of this critical pair. 5.59/2.37 5.75/2.39 EOF