5.58/2.41 MAYBE 5.58/2.41 5.58/2.41 Proof: 5.58/2.41 ConCon could not decide confluence of the system. 5.58/2.41 \cite{ALS94}, Theorem 4.1 does not apply. 5.58/2.41 This system is of type 3 or smaller. 5.58/2.41 This system is strongly deterministic. 5.58/2.41 This system is quasi-decreasing. 5.58/2.42 By \cite{O02}, p. 214, Proposition 7.2.50. 5.58/2.42 This system is of type 3 or smaller. 5.58/2.42 This system is deterministic. 5.58/2.42 System R transformed to U(R). 5.58/2.42 This system is terminating. 5.58/2.42 Call external tool: 5.58/2.42 ./ttt2.sh 5.58/2.42 Input: 5.58/2.42 (VAR x) 5.58/2.42 (RULES 5.58/2.42 s(p(x)) -> x 5.58/2.42 p(s(x)) -> x 5.58/2.42 pos(0) -> false 5.58/2.42 pos(s(0)) -> true 5.58/2.42 ?1(true, x) -> true 5.58/2.42 pos(s(x)) -> ?1(pos(x), x) 5.58/2.42 ?2(false, x) -> false 5.58/2.42 pos(p(x)) -> ?2(pos(x), x) 5.58/2.42 ) 5.58/2.42 5.58/2.42 Matrix Interpretation Processor: dim=1 5.58/2.42 5.58/2.42 interpretation: 5.58/2.42 [?2](x0, x1) = x0 + 4x1, 5.58/2.42 5.58/2.42 [?1](x0, x1) = x0 + 4x1 + 2, 5.58/2.42 5.58/2.42 [true] = 0, 5.58/2.42 5.58/2.42 [false] = 0, 5.58/2.42 5.58/2.42 [pos](x0) = 2x0 + 3, 5.58/2.42 5.58/2.42 [0] = 0, 5.58/2.42 5.58/2.42 [s](x0) = 3x0 + 4, 5.58/2.42 5.58/2.42 [p](x0) = 5x0 5.58/2.42 orientation: 5.58/2.42 s(p(x)) = 15x + 4 >= x = x 5.58/2.42 5.58/2.42 p(s(x)) = 15x + 20 >= x = x 5.58/2.42 5.58/2.42 pos(0()) = 3 >= 0 = false() 5.58/2.42 5.58/2.42 pos(s(0())) = 11 >= 0 = true() 5.58/2.42 5.58/2.42 ?1(true(),x) = 4x + 2 >= 0 = true() 5.58/2.42 5.58/2.42 pos(s(x)) = 6x + 11 >= 6x + 5 = ?1(pos(x),x) 5.58/2.42 5.58/2.42 ?2(false(),x) = 4x >= 0 = false() 5.58/2.42 5.58/2.42 pos(p(x)) = 10x + 3 >= 6x + 3 = ?2(pos(x),x) 5.58/2.42 problem: 5.58/2.42 ?2(false(),x) -> false() 5.58/2.42 pos(p(x)) -> ?2(pos(x),x) 5.58/2.42 Matrix Interpretation Processor: dim=3 5.58/2.42 5.58/2.42 interpretation: 5.58/2.42 [1 1 0] [1 1 1] 5.58/2.42 [?2](x0, x1) = [0 1 0]x0 + [0 0 0]x1 5.58/2.42 [0 0 0] [0 0 0] , 5.58/2.42 5.58/2.42 [1] 5.58/2.42 [false] = [1] 5.58/2.42 [0], 5.58/2.42 5.58/2.42 [1 1 1] 5.58/2.42 [pos](x0) = [0 0 0]x0 5.58/2.42 [0 0 0] , 5.58/2.42 5.58/2.42 [1 1 1] 5.58/2.42 [p](x0) = [0 1 1]x0 5.58/2.42 [1 0 0] 5.58/2.42 orientation: 5.58/2.42 [1 1 1] [2] [1] 5.58/2.42 ?2(false(),x) = [0 0 0]x + [1] >= [1] = false() 5.58/2.42 [0 0 0] [0] [0] 5.58/2.42 5.58/2.42 [2 2 2] [2 2 2] 5.58/2.42 pos(p(x)) = [0 0 0]x >= [0 0 0]x = ?2(pos(x),x) 5.58/2.42 [0 0 0] [0 0 0] 5.58/2.42 problem: 5.58/2.42 pos(p(x)) -> ?2(pos(x),x) 5.58/2.42 Matrix Interpretation Processor: dim=3 5.58/2.42 5.58/2.42 interpretation: 5.58/2.42 [1 1 0] [1 1 0] [0] 5.58/2.42 [?2](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [1] 5.58/2.42 [0 0 0] [0 0 0] [0], 5.58/2.42 5.58/2.42 [1 1 0] [1] 5.58/2.42 [pos](x0) = [0 0 0]x0 + [1] 5.58/2.42 [0 0 0] [0], 5.58/2.42 5.58/2.42 [1 1 0] [1] 5.58/2.42 [p](x0) = [1 1 0]x0 + [1] 5.58/2.42 [0 0 0] [0] 5.58/2.42 orientation: 5.58/2.42 [2 2 0] [3] [2 2 0] [2] 5.58/2.42 pos(p(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = ?2(pos(x),x) 5.58/2.42 [0 0 0] [0] [0 0 0] [0] 5.58/2.42 problem: 5.58/2.42 5.58/2.42 Qed 5.58/2.42 Overlap: (rule1: s(p(y)) -> y, rule2: p(s(z)) -> z, pos: 1, mgu: {(y,s(z))}) 5.58/2.42 CP: s(z) = s(z) 5.58/2.42 This critical pair is context-joinable. 5.58/2.42 Overlap: (rule1: p(s(y)) -> y, rule2: s(p(z)) -> z, pos: 1, mgu: {(y,p(z))}) 5.58/2.42 CP: p(z) = p(z) 5.58/2.42 This critical pair is context-joinable. 5.58/2.42 Overlap: (rule1: pos(s(0)) -> true, rule2: pos(s(y)) -> true <= pos(y) = true, pos: ε, mgu: {(y,0)}) 5.58/2.42 CP: true = true <= pos(0) = true 5.58/2.42 This critical pair is context-joinable. 5.58/2.42 This critical pair is conditional. 5.58/2.42 This critical pair has some non-trivial conditions. 5.58/2.42 ConCon could not decide whether all 6 critical pairs are joinable or not. 5.89/2.42 Overlap: (rule1: pos(s(y)) -> true <= pos(y) = true, rule2: s(p(z)) -> z, pos: 1, mgu: {(y,p(z))}) 5.89/2.42 CP: pos(z) = true <= pos(p(z)) = true 5.89/2.42 ConCon could not decide infeasibility of this critical pair. 5.89/2.42 5.89/2.45 EOF