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