18.69/5.88 YES 18.69/5.88 18.69/5.88 Proof: 18.69/5.88 This system is confluent. 18.69/5.88 By \cite{ALS94}, Theorem 4.1. 18.69/5.88 This system is of type 3 or smaller. 18.69/5.88 This system is strongly deterministic. 18.69/5.88 This system is quasi-decreasing. 18.69/5.88 By \cite{O02}, p. 214, Proposition 7.2.50. 18.69/5.88 This system is of type 3 or smaller. 18.69/5.88 This system is deterministic. 18.69/5.88 System R transformed to U(R). 18.69/5.88 This system is terminating. 18.69/5.88 Call external tool: 18.69/5.88 ./ttt2.sh 18.69/5.88 Input: 18.69/5.88 (VAR x y l) 18.69/5.88 (RULES 18.69/5.88 le(0, s(x)) -> true 18.69/5.88 le(x, 0) -> false 18.69/5.88 le(s(x), s(y)) -> le(x, y) 18.69/5.88 min(cons(x, nil)) -> x 18.69/5.88 ?1(true, x, l) -> x 18.69/5.88 min(cons(x, l)) -> ?1(le(x, min(l)), x, l) 18.69/5.88 ?2(false, x, l) -> min(l) 18.69/5.88 min(cons(x, l)) -> ?2(le(x, min(l)), x, l) 18.69/5.88 ?3(x, x, l) -> min(l) 18.69/5.88 min(cons(x, l)) -> ?3(min(l), x, l) 18.69/5.88 ) 18.69/5.88 18.69/5.88 Matrix Interpretation Processor: dim=1 18.69/5.88 18.69/5.88 interpretation: 18.69/5.88 [?3](x0, x1, x2) = x0 + 7x1 + 2x2 + 4, 18.69/5.88 18.69/5.88 [?2](x0, x1, x2) = x0 + x1 + 2x2 + 4, 18.69/5.88 18.69/5.88 [?1](x0, x1, x2) = x0 + 6x1 + 2x2, 18.69/5.88 18.69/5.88 [min](x0) = 2x0, 18.69/5.88 18.69/5.88 [cons](x0, x1) = 6x0 + 5x1 + 2, 18.69/5.88 18.69/5.88 [nil] = 2, 18.69/5.88 18.69/5.88 [false] = 3, 18.69/5.88 18.69/5.88 [true] = 4, 18.69/5.88 18.69/5.88 [le](x0, x1) = 6x0 + 4x1, 18.69/5.88 18.69/5.88 [s](x0) = 4x0 + 2, 18.69/5.88 18.69/5.88 [0] = 1 18.69/5.88 orientation: 18.69/5.88 le(0(),s(x)) = 16x + 14 >= 4 = true() 18.69/5.88 18.69/5.88 le(x,0()) = 6x + 4 >= 3 = false() 18.69/5.88 18.69/5.88 le(s(x),s(y)) = 24x + 16y + 20 >= 6x + 4y = le(x,y) 18.69/5.88 18.69/5.88 min(cons(x,nil())) = 12x + 24 >= x = x 18.69/5.88 18.69/5.88 ?1(true(),x,l) = 2l + 6x + 4 >= x = x 18.69/5.88 18.69/5.88 min(cons(x,l)) = 10l + 12x + 4 >= 10l + 12x = ?1(le(x,min(l)),x,l) 18.69/5.88 18.69/5.88 ?2(false(),x,l) = 2l + x + 7 >= 2l = min(l) 18.69/5.88 18.69/5.88 min(cons(x,l)) = 10l + 12x + 4 >= 10l + 7x + 4 = ?2(le(x,min(l)),x,l) 18.69/5.88 18.69/5.88 ?3(x,x,l) = 2l + 8x + 4 >= 2l = min(l) 18.69/5.88 18.69/5.88 min(cons(x,l)) = 10l + 12x + 4 >= 4l + 7x + 4 = ?3(min(l),x,l) 18.69/5.88 problem: 18.69/5.88 min(cons(x,l)) -> ?2(le(x,min(l)),x,l) 18.69/5.88 min(cons(x,l)) -> ?3(min(l),x,l) 18.69/5.88 Matrix Interpretation Processor: dim=1 18.69/5.88 18.69/5.88 interpretation: 18.69/5.88 [?3](x0, x1, x2) = x0 + 6x1 + 6x2, 18.69/5.88 18.69/5.88 [?2](x0, x1, x2) = x0 + x1 + 3x2 + 3, 18.69/5.88 18.69/5.88 [min](x0) = 3x0, 18.69/5.88 18.69/5.88 [cons](x0, x1) = 2x0 + 7x1 + 3, 18.69/5.88 18.69/5.88 [le](x0, x1) = 5x0 + 6x1 + 6 18.69/5.88 orientation: 18.69/5.88 min(cons(x,l)) = 21l + 6x + 9 >= 21l + 6x + 9 = ?2(le(x,min(l)),x,l) 18.69/5.88 18.69/5.88 min(cons(x,l)) = 21l + 6x + 9 >= 9l + 6x = ?3(min(l),x,l) 18.69/5.88 problem: 18.69/5.88 min(cons(x,l)) -> ?2(le(x,min(l)),x,l) 18.69/5.88 Matrix Interpretation Processor: dim=3 18.69/5.88 18.69/5.88 interpretation: 18.69/5.88 [1 0 0] [1 0 0] [1 0 0] 18.69/5.88 [?2](x0, x1, x2) = [1 0 0]x0 + [0 1 0]x1 + [0 0 0]x2 18.69/5.88 [0 0 0] [0 0 0] [0 0 0] , 18.69/5.88 18.69/5.88 [1 1 1] [1] 18.69/5.88 [min](x0) = [1 1 1]x0 + [0] 18.69/5.88 [0 0 1] [0], 18.69/5.88 18.69/5.89 [1 0 0] [1 0 0] [1] 18.69/5.89 [cons](x0, x1) = [1 0 0]x0 + [0 1 1]x1 + [0] 18.69/5.89 [0 1 0] [1 0 0] [1], 18.69/5.89 18.69/5.89 [1 0 0] [1 0 0] 18.69/5.89 [le](x0, x1) = [0 0 0]x0 + [0 1 1]x1 18.69/5.89 [0 0 0] [0 0 0] 18.69/5.89 orientation: 18.69/5.89 [2 1 1] [2 1 0] [3] [2 1 1] [2 0 0] [1] 18.69/5.89 min(cons(x,l)) = [2 1 1]l + [2 1 0]x + [2] >= [1 1 1]l + [1 1 0]x + [1] = ?2(le(x,min(l)),x,l) 18.69/5.89 [1 0 0] [0 1 0] [1] [0 0 0] [0 0 0] [0] 18.69/5.89 problem: 18.69/5.89 18.69/5.89 Qed 18.69/5.89 All 12 critical pairs are joinable. 18.69/5.89 Overlap: (rule1: min(cons(z, y)) -> min(y) <= le(z, min(y)) = false, rule2: min(cons(y', x')) -> min(x') <= min(x') = y', pos: ε, mgu: {(z,y'), (y,x')}) 18.69/5.89 CP: min(x') = min(x') <= le(y', min(x')) = false, min(x') = y' 18.69/5.89 This critical pair is context-joinable. 18.69/5.89 Overlap: (rule1: min(cons(z, y)) -> min(y) <= min(y) = z, rule2: min(cons(x', nil)) -> x', pos: ε, mgu: {(z,x'), (y,nil)}) 18.69/5.89 CP: x' = min(nil) <= min(nil) = x' 18.69/5.89 This critical pair is context-joinable. 18.69/5.89 Overlap: (rule1: min(cons(y, nil)) -> y, rule2: min(cons(x', z)) -> min(z) <= min(z) = x', pos: ε, mgu: {(y,x'), (z,nil)}) 18.69/5.89 CP: min(nil) = x' <= min(nil) = x' 18.69/5.89 This critical pair is context-joinable. 18.69/5.89 Overlap: (rule1: min(cons(z, y)) -> z <= le(z, min(y)) = true, rule2: min(cons(y', x')) -> min(x') <= min(x') = y', pos: ε, mgu: {(z,y'), (y,x')}) 18.69/5.89 CP: min(x') = y' <= le(y', min(x')) = true, min(x') = y' 18.69/5.89 This critical pair is context-joinable. 18.69/5.89 Overlap: (rule1: min(cons(y, nil)) -> y, rule2: min(cons(x', z)) -> min(z) <= le(x', min(z)) = false, pos: ε, mgu: {(y,x'), (z,nil)}) 18.69/5.89 CP: min(nil) = x' <= le(x', min(nil)) = false 18.69/5.89 This critical pair is infeasible. 18.69/5.89 This critical pair is conditional. 18.69/5.89 This critical pair has some non-trivial conditions. 18.69/5.89 'tcap_{R_u}(le(x', min(nil)))' and 'false' are not unifiable. 18.69/5.89 Overlap: (rule1: min(cons(z, y)) -> z <= le(z, min(y)) = true, rule2: min(cons(y', x')) -> min(x') <= le(y', min(x')) = false, pos: ε, mgu: {(z,y'), (y,x')}) 18.69/5.89 CP: min(x') = y' <= le(y', min(x')) = true, le(y', min(x')) = false 18.69/5.89 This critical pair is unfeasible. 18.69/5.89 Overlap: (rule1: min(cons(z, y)) -> z <= le(z, min(y)) = true, rule2: min(cons(x', nil)) -> x', pos: ε, mgu: {(z,x'), (y,nil)}) 18.69/5.89 CP: x' = x' <= le(x', min(nil)) = true 18.69/5.89 This critical pair is infeasible. 18.69/5.89 This critical pair is conditional. 18.69/5.89 This critical pair has some non-trivial conditions. 18.69/5.89 'tcap_{R_u}(le(x', min(nil)))' and 'true' are not unifiable. 18.69/5.89 Overlap: (rule1: min(cons(y, nil)) -> y, rule2: min(cons(x', z)) -> x' <= le(x', min(z)) = true, pos: ε, mgu: {(y,x'), (z,nil)}) 18.69/5.89 CP: x' = x' <= le(x', min(nil)) = true 18.69/5.89 This critical pair is context-joinable. 18.69/5.89 Overlap: (rule1: min(cons(z, y)) -> min(y) <= le(z, min(y)) = false, rule2: min(cons(y', x')) -> y' <= le(y', min(x')) = true, pos: ε, mgu: {(z,y'), (y,x')}) 18.69/5.89 CP: y' = min(x') <= le(y', min(x')) = false, le(y', min(x')) = true 18.69/5.89 This critical pair is unfeasible. 18.69/5.89 Overlap: (rule1: min(cons(z, y)) -> min(y) <= min(y) = z, rule2: min(cons(y', x')) -> y' <= le(y', min(x')) = true, pos: ε, mgu: {(z,y'), (y,x')}) 18.69/5.89 CP: y' = min(x') <= min(x') = y', le(y', min(x')) = true 18.69/5.89 This critical pair is context-joinable. 18.69/5.89 Overlap: (rule1: min(cons(z, y)) -> min(y) <= min(y) = z, rule2: min(cons(y', x')) -> min(x') <= le(y', min(x')) = false, pos: ε, mgu: {(z,y'), (y,x')}) 18.69/5.89 CP: min(x') = min(x') <= min(x') = y', le(y', min(x')) = false 18.69/5.89 This critical pair is context-joinable. 18.69/5.89 Overlap: (rule1: min(cons(z, y)) -> min(y) <= le(z, min(y)) = false, rule2: min(cons(x', nil)) -> x', pos: ε, mgu: {(z,x'), (y,nil)}) 18.69/5.89 CP: x' = min(nil) <= le(x', min(nil)) = false 18.69/5.89 This critical pair is infeasible. 18.69/5.89 This critical pair is conditional. 18.69/5.89 This critical pair has some non-trivial conditions. 18.69/5.89 'tcap_{R_u}(le(x', min(nil)))' and 'false' are not unifiable. 18.69/5.89 19.01/5.94 EOF