25.38/7.84 YES 25.38/7.84 25.38/7.84 Problem: 25.38/7.84 lte(0(), n) -> true() 25.38/7.84 lte(s(m), 0()) -> false() 25.38/7.84 lte(s(m), s(n)) -> lte(m, n) 25.38/7.84 insert(nil(), m) -> cons(m, nil()) 25.38/7.84 insert(cons(n, l), m) -> cons(m, cons(n, l)) <= lte(m, n) = true() 25.38/7.84 insert(cons(n, l), m) -> cons(n, insert(l, m)) <= lte(m, n) = false() 25.38/7.84 ordered(nil()) -> true() 25.38/7.84 ordered(cons(m, nil())) -> true() 25.38/7.84 ordered(cons(m, cons(n, l))) -> ordered(cons(n, l)) <= lte(m, n) = true() 25.38/7.84 ordered(cons(m, cons(n, l))) -> false() <= lte(m, n) = false() 25.38/7.84 25.38/7.84 Proof: 25.38/7.84 This system is confluent. 25.38/7.84 By \cite{SMI95}, Corollary 4.7 or 5.3. 25.38/7.84 This system is oriented. 25.38/7.84 This system is of type 3 or smaller. 25.38/7.84 This system is right-stable. 25.38/7.84 This system is properly oriented. 25.38/7.84 This is an overlay system. 25.38/7.84 This system is left-linear. 25.38/7.84 All 4 critical pairs are trivial or infeasible. 25.38/7.84 CP: cons(x', cons(y', z')) = cons(y', insert(z', x')) <= lte(x', y') = false(), lte(x', y') = true(): 25.38/7.84 This critical pair is infeasible. 25.38/7.84 This critical pair is conditional. 25.38/7.84 This critical pair has some non-trivial conditions. 25.38/7.84 This system is of type 3 or smaller. 25.38/7.84 This system is deterministic. 25.38/7.84 This system is quasi-decreasing. 25.38/7.84 By \cite{A14}, Theorem 11.5.9. 25.38/7.84 This system is of type 3 or smaller. 25.38/7.84 This system is deterministic. 25.38/7.84 System R transformed to V(R) + Emb. 25.38/7.84 This system is terminating. 25.38/7.84 Call external tool: 25.38/7.84 ./ttt2.sh 25.38/7.84 Input: 25.38/7.84 lte(0(), n) -> true() 25.38/7.84 lte(s(m), 0()) -> false() 25.38/7.84 lte(s(m), s(n)) -> lte(m, n) 25.38/7.84 insert(nil(), m) -> cons(m, nil()) 25.38/7.84 insert(cons(n, l), m) -> cons(m, cons(n, l)) 25.38/7.84 insert(cons(n, l), m) -> lte(m, n) 25.38/7.84 insert(cons(n, l), m) -> cons(n, insert(l, m)) 25.38/7.84 ordered(nil()) -> true() 25.38/7.84 ordered(cons(m, nil())) -> true() 25.38/7.84 ordered(cons(m, cons(n, l))) -> ordered(cons(n, l)) 25.38/7.84 ordered(cons(m, cons(n, l))) -> lte(m, n) 25.38/7.84 ordered(cons(m, cons(n, l))) -> false() 25.38/7.84 s(x) -> x 25.38/7.84 insert(x, y) -> x 25.38/7.84 insert(x, y) -> y 25.38/7.84 lte(x, y) -> x 25.38/7.84 lte(x, y) -> y 25.38/7.84 ordered(x) -> x 25.38/7.84 cons(x, y) -> x 25.38/7.84 cons(x, y) -> y 25.38/7.84 25.38/7.84 Matrix Interpretation Processor: dim=1 25.38/7.84 25.38/7.84 interpretation: 25.38/7.84 [ordered](x0) = 4x0 + 2, 25.38/7.84 25.38/7.84 [cons](x0, x1) = 2x0 + x1 + 2, 25.38/7.84 25.38/7.84 [insert](x0, x1) = 2x0 + 2x1 + 6, 25.38/7.84 25.38/7.84 [nil] = 3, 25.38/7.84 25.38/7.84 [false] = 0, 25.38/7.84 25.38/7.84 [s](x0) = 2x0 + 1, 25.38/7.84 25.38/7.84 [true] = 0, 25.38/7.84 25.38/7.84 [lte](x0, x1) = 2x0 + 4x1 + 1, 25.38/7.84 25.38/7.84 [0] = 7 25.38/7.84 orientation: 25.38/7.84 lte(0(),n) = 4n + 15 >= 0 = true() 25.38/7.84 25.38/7.84 lte(s(m),0()) = 4m + 31 >= 0 = false() 25.38/7.84 25.38/7.84 lte(s(m),s(n)) = 4m + 8n + 7 >= 2m + 4n + 1 = lte(m,n) 25.38/7.84 25.38/7.84 insert(nil(),m) = 2m + 12 >= 2m + 5 = cons(m,nil()) 25.38/7.84 25.38/7.84 insert(cons(n,l),m) = 2l + 2m + 4n + 10 >= l + 2m + 2n + 4 = cons(m,cons(n,l)) 25.38/7.84 25.38/7.84 insert(cons(n,l),m) = 2l + 2m + 4n + 10 >= 2m + 4n + 1 = lte(m,n) 25.38/7.84 25.38/7.84 insert(cons(n,l),m) = 2l + 2m + 4n + 10 >= 2l + 2m + 2n + 8 = cons(n,insert(l,m)) 25.38/7.84 25.38/7.84 ordered(nil()) = 14 >= 0 = true() 25.38/7.84 25.38/7.84 ordered(cons(m,nil())) = 8m + 22 >= 0 = true() 25.38/7.84 25.38/7.84 ordered(cons(m,cons(n,l))) = 4l + 8m + 8n + 18 >= 4l + 8n + 10 = ordered(cons(n,l)) 25.38/7.84 25.38/7.84 ordered(cons(m,cons(n,l))) = 4l + 8m + 8n + 18 >= 2m + 4n + 1 = lte(m,n) 25.38/7.84 25.38/7.84 ordered(cons(m,cons(n,l))) = 4l + 8m + 8n + 18 >= 0 = false() 25.38/7.84 25.38/7.84 s(x) = 2x + 1 >= x = x 25.38/7.84 25.38/7.85 insert(x,y) = 2x + 2y + 6 >= x = x 25.38/7.85 25.38/7.85 insert(x,y) = 2x + 2y + 6 >= y = y 25.38/7.85 25.38/7.85 lte(x,y) = 2x + 4y + 1 >= x = x 25.38/7.85 25.38/7.85 lte(x,y) = 2x + 4y + 1 >= y = y 25.38/7.85 25.38/7.85 ordered(x) = 4x + 2 >= x = x 25.38/7.85 25.38/7.85 cons(x,y) = 2x + y + 2 >= x = x 25.38/7.85 25.38/7.85 cons(x,y) = 2x + y + 2 >= y = y 25.38/7.85 problem: 25.38/7.85 25.38/7.85 Qed 25.38/7.85 This critical pair is unfeasible. 25.38/7.85 CP: cons(x', insert(y', z')) = cons(z', cons(x', y')) <= lte(z', x') = true(), lte(z', x') = false(): 25.38/7.85 This critical pair is infeasible. 25.38/7.85 This critical pair is conditional. 25.38/7.85 This critical pair has some non-trivial conditions. 25.38/7.85 This system is of type 3 or smaller. 25.38/7.85 This system is deterministic. 25.38/7.85 This system is quasi-decreasing. 25.38/7.85 By \cite{A14}, Theorem 11.5.9. 25.38/7.85 This system is of type 3 or smaller. 25.38/7.85 This system is deterministic. 25.38/7.85 System R transformed to V(R) + Emb. 25.38/7.85 This system is terminating. 25.38/7.85 Call external tool: 25.38/7.85 ./ttt2.sh 25.38/7.85 Input: 25.38/7.85 lte(0(), n) -> true() 25.38/7.85 lte(s(m), 0()) -> false() 25.38/7.85 lte(s(m), s(n)) -> lte(m, n) 25.38/7.85 insert(nil(), m) -> cons(m, nil()) 25.38/7.85 insert(cons(n, l), m) -> cons(m, cons(n, l)) 25.38/7.85 insert(cons(n, l), m) -> lte(m, n) 25.38/7.85 insert(cons(n, l), m) -> cons(n, insert(l, m)) 25.38/7.85 ordered(nil()) -> true() 25.38/7.85 ordered(cons(m, nil())) -> true() 25.38/7.85 ordered(cons(m, cons(n, l))) -> ordered(cons(n, l)) 25.38/7.85 ordered(cons(m, cons(n, l))) -> lte(m, n) 25.38/7.85 ordered(cons(m, cons(n, l))) -> false() 25.38/7.85 s(x) -> x 25.38/7.85 insert(x, y) -> x 25.38/7.85 insert(x, y) -> y 25.38/7.85 lte(x, y) -> x 25.38/7.85 lte(x, y) -> y 25.38/7.85 ordered(x) -> x 25.38/7.85 cons(x, y) -> x 25.38/7.85 cons(x, y) -> y 25.38/7.85 25.38/7.85 Matrix Interpretation Processor: dim=1 25.38/7.85 25.38/7.85 interpretation: 25.38/7.85 [ordered](x0) = 4x0 + 2, 25.38/7.85 25.38/7.85 [cons](x0, x1) = 2x0 + x1 + 2, 25.38/7.85 25.38/7.85 [insert](x0, x1) = 2x0 + 2x1 + 6, 25.38/7.85 25.38/7.85 [nil] = 3, 25.38/7.85 25.38/7.85 [false] = 0, 25.38/7.85 25.38/7.85 [s](x0) = 2x0 + 1, 25.38/7.85 25.38/7.85 [true] = 0, 25.38/7.85 25.38/7.85 [lte](x0, x1) = 2x0 + 4x1 + 1, 25.38/7.85 25.38/7.85 [0] = 7 25.38/7.85 orientation: 25.38/7.85 lte(0(),n) = 4n + 15 >= 0 = true() 25.38/7.85 25.38/7.85 lte(s(m),0()) = 4m + 31 >= 0 = false() 25.38/7.85 25.38/7.85 lte(s(m),s(n)) = 4m + 8n + 7 >= 2m + 4n + 1 = lte(m,n) 25.38/7.85 25.38/7.85 insert(nil(),m) = 2m + 12 >= 2m + 5 = cons(m,nil()) 25.38/7.85 25.38/7.85 insert(cons(n,l),m) = 2l + 2m + 4n + 10 >= l + 2m + 2n + 4 = cons(m,cons(n,l)) 25.38/7.85 25.38/7.85 insert(cons(n,l),m) = 2l + 2m + 4n + 10 >= 2m + 4n + 1 = lte(m,n) 25.38/7.85 25.38/7.85 insert(cons(n,l),m) = 2l + 2m + 4n + 10 >= 2l + 2m + 2n + 8 = cons(n,insert(l,m)) 25.38/7.85 25.38/7.85 ordered(nil()) = 14 >= 0 = true() 25.38/7.85 25.38/7.85 ordered(cons(m,nil())) = 8m + 22 >= 0 = true() 25.38/7.85 25.38/7.85 ordered(cons(m,cons(n,l))) = 4l + 8m + 8n + 18 >= 4l + 8n + 10 = ordered(cons(n,l)) 25.38/7.85 25.38/7.85 ordered(cons(m,cons(n,l))) = 4l + 8m + 8n + 18 >= 2m + 4n + 1 = lte(m,n) 25.38/7.85 25.38/7.85 ordered(cons(m,cons(n,l))) = 4l + 8m + 8n + 18 >= 0 = false() 25.38/7.85 25.38/7.85 s(x) = 2x + 1 >= x = x 25.38/7.85 25.38/7.85 insert(x,y) = 2x + 2y + 6 >= x = x 25.38/7.85 25.38/7.85 insert(x,y) = 2x + 2y + 6 >= y = y 25.38/7.85 25.38/7.85 lte(x,y) = 2x + 4y + 1 >= x = x 25.38/7.85 25.38/7.85 lte(x,y) = 2x + 4y + 1 >= y = y 25.38/7.85 25.38/7.85 ordered(x) = 4x + 2 >= x = x 25.38/7.85 25.38/7.85 cons(x,y) = 2x + y + 2 >= x = x 25.38/7.85 25.38/7.85 cons(x,y) = 2x + y + 2 >= y = y 25.38/7.85 problem: 25.38/7.85 25.38/7.85 Qed 25.38/7.85 This critical pair is unfeasible. 25.38/7.85 CP: ordered(cons(x', y')) = false() <= lte(z', x') = false(), lte(z', x') = true(): 25.38/7.85 This critical pair is infeasible. 25.38/7.85 This critical pair is conditional. 25.38/7.85 This critical pair has some non-trivial conditions. 25.38/7.85 This system is of type 3 or smaller. 25.38/7.85 This system is deterministic. 25.38/7.85 This system is quasi-decreasing. 25.38/7.85 By \cite{A14}, Theorem 11.5.9. 25.38/7.85 This system is of type 3 or smaller. 25.38/7.85 This system is deterministic. 25.38/7.85 System R transformed to V(R) + Emb. 25.38/7.85 This system is terminating. 25.38/7.85 Call external tool: 25.38/7.85 ./ttt2.sh 25.38/7.85 Input: 25.38/7.85 lte(0(), n) -> true() 25.38/7.85 lte(s(m), 0()) -> false() 25.38/7.85 lte(s(m), s(n)) -> lte(m, n) 25.38/7.85 insert(nil(), m) -> cons(m, nil()) 25.38/7.85 insert(cons(n, l), m) -> cons(m, cons(n, l)) 25.38/7.85 insert(cons(n, l), m) -> lte(m, n) 25.38/7.85 insert(cons(n, l), m) -> cons(n, insert(l, m)) 25.38/7.85 ordered(nil()) -> true() 25.38/7.85 ordered(cons(m, nil())) -> true() 25.38/7.85 ordered(cons(m, cons(n, l))) -> ordered(cons(n, l)) 25.38/7.85 ordered(cons(m, cons(n, l))) -> lte(m, n) 25.38/7.85 ordered(cons(m, cons(n, l))) -> false() 25.38/7.85 s(x) -> x 25.38/7.85 insert(x, y) -> x 25.38/7.85 insert(x, y) -> y 25.38/7.85 lte(x, y) -> x 25.38/7.85 lte(x, y) -> y 25.38/7.85 ordered(x) -> x 25.38/7.85 cons(x, y) -> x 25.38/7.85 cons(x, y) -> y 25.38/7.85 25.38/7.85 Matrix Interpretation Processor: dim=1 25.38/7.88 25.38/7.88 interpretation: 25.38/7.88 [ordered](x0) = 4x0 + 2, 25.38/7.88 25.38/7.88 [cons](x0, x1) = 2x0 + x1 + 2, 25.38/7.88 25.38/7.88 [insert](x0, x1) = 2x0 + 2x1 + 6, 25.38/7.88 25.38/7.88 [nil] = 3, 25.38/7.88 25.38/7.88 [false] = 0, 25.38/7.88 25.38/7.88 [s](x0) = 2x0 + 1, 25.38/7.88 25.38/7.88 [true] = 0, 25.38/7.88 25.38/7.88 [lte](x0, x1) = 2x0 + 4x1 + 1, 25.38/7.88 25.38/7.88 [0] = 7 25.38/7.88 orientation: 25.38/7.88 lte(0(),n) = 4n + 15 >= 0 = true() 25.38/7.88 25.38/7.88 lte(s(m),0()) = 4m + 31 >= 0 = false() 25.38/7.88 25.38/7.88 lte(s(m),s(n)) = 4m + 8n + 7 >= 2m + 4n + 1 = lte(m,n) 25.38/7.88 25.38/7.88 insert(nil(),m) = 2m + 12 >= 2m + 5 = cons(m,nil()) 25.38/7.88 25.38/7.88 insert(cons(n,l),m) = 2l + 2m + 4n + 10 >= l + 2m + 2n + 4 = cons(m,cons(n,l)) 25.38/7.88 25.38/7.88 insert(cons(n,l),m) = 2l + 2m + 4n + 10 >= 2m + 4n + 1 = lte(m,n) 25.38/7.88 25.38/7.88 insert(cons(n,l),m) = 2l + 2m + 4n + 10 >= 2l + 2m + 2n + 8 = cons(n,insert(l,m)) 25.38/7.88 25.38/7.88 ordered(nil()) = 14 >= 0 = true() 25.38/7.88 25.38/7.88 ordered(cons(m,nil())) = 8m + 22 >= 0 = true() 25.38/7.88 25.38/7.88 ordered(cons(m,cons(n,l))) = 4l + 8m + 8n + 18 >= 4l + 8n + 10 = ordered(cons(n,l)) 25.38/7.88 25.38/7.88 ordered(cons(m,cons(n,l))) = 4l + 8m + 8n + 18 >= 2m + 4n + 1 = lte(m,n) 25.38/7.88 25.38/7.88 ordered(cons(m,cons(n,l))) = 4l + 8m + 8n + 18 >= 0 = false() 25.38/7.88 25.38/7.88 s(x) = 2x + 1 >= x = x 25.38/7.88 25.38/7.88 insert(x,y) = 2x + 2y + 6 >= x = x 25.38/7.88 25.38/7.88 insert(x,y) = 2x + 2y + 6 >= y = y 25.38/7.88 25.38/7.88 lte(x,y) = 2x + 4y + 1 >= x = x 25.38/7.88 25.38/7.88 lte(x,y) = 2x + 4y + 1 >= y = y 25.38/7.88 25.38/7.88 ordered(x) = 4x + 2 >= x = x 25.38/7.88 25.38/7.88 cons(x,y) = 2x + y + 2 >= x = x 25.38/7.88 25.38/7.88 cons(x,y) = 2x + y + 2 >= y = y 25.38/7.88 problem: 25.38/7.88 25.38/7.88 Qed 25.38/7.88 This critical pair is unfeasible. 25.38/7.88 CP: false() = ordered(cons(x', y')) <= lte(z', x') = true(), lte(z', x') = false(): 25.38/7.88 This critical pair is infeasible. 25.38/7.88 This critical pair is conditional. 25.38/7.88 This critical pair has some non-trivial conditions. 25.38/7.88 This system is of type 3 or smaller. 25.38/7.88 This system is deterministic. 25.38/7.88 This system is quasi-decreasing. 25.38/7.88 By \cite{A14}, Theorem 11.5.9. 25.38/7.88 This system is of type 3 or smaller. 25.38/7.88 This system is deterministic. 25.38/7.88 System R transformed to V(R) + Emb. 25.38/7.88 This system is terminating. 25.38/7.88 Call external tool: 25.38/7.88 ./ttt2.sh 25.38/7.88 Input: 25.38/7.88 lte(0(), n) -> true() 25.38/7.88 lte(s(m), 0()) -> false() 25.38/7.88 lte(s(m), s(n)) -> lte(m, n) 25.38/7.88 insert(nil(), m) -> cons(m, nil()) 25.38/7.88 insert(cons(n, l), m) -> cons(m, cons(n, l)) 25.38/7.88 insert(cons(n, l), m) -> lte(m, n) 25.38/7.88 insert(cons(n, l), m) -> cons(n, insert(l, m)) 25.38/7.88 ordered(nil()) -> true() 25.38/7.88 ordered(cons(m, nil())) -> true() 25.38/7.88 ordered(cons(m, cons(n, l))) -> ordered(cons(n, l)) 25.38/7.88 ordered(cons(m, cons(n, l))) -> lte(m, n) 25.38/7.88 ordered(cons(m, cons(n, l))) -> false() 25.38/7.88 s(x) -> x 25.38/7.88 insert(x, y) -> x 25.38/7.88 insert(x, y) -> y 25.38/7.88 lte(x, y) -> x 25.38/7.88 lte(x, y) -> y 25.38/7.88 ordered(x) -> x 25.38/7.88 cons(x, y) -> x 25.38/7.88 cons(x, y) -> y 25.38/7.88 25.38/7.88 Matrix Interpretation Processor: dim=1 25.38/7.88 25.38/7.88 interpretation: 25.38/7.88 [ordered](x0) = 4x0 + 2, 25.38/7.88 25.38/7.88 [cons](x0, x1) = 2x0 + x1 + 2, 25.38/7.88 25.38/7.88 [insert](x0, x1) = 2x0 + 2x1 + 6, 25.38/7.88 25.38/7.88 [nil] = 3, 25.38/7.88 25.38/7.88 [false] = 0, 25.38/7.88 25.38/7.88 [s](x0) = 2x0 + 1, 25.38/7.88 25.38/7.88 [true] = 0, 25.38/7.88 25.38/7.88 [lte](x0, x1) = 2x0 + 4x1 + 1, 25.38/7.88 25.38/7.88 [0] = 7 25.38/7.88 orientation: 25.38/7.88 lte(0(),n) = 4n + 15 >= 0 = true() 25.38/7.88 25.38/7.88 lte(s(m),0()) = 4m + 31 >= 0 = false() 25.38/7.88 25.38/7.88 lte(s(m),s(n)) = 4m + 8n + 7 >= 2m + 4n + 1 = lte(m,n) 25.38/7.88 25.38/7.88 insert(nil(),m) = 2m + 12 >= 2m + 5 = cons(m,nil()) 25.38/7.88 25.38/7.88 insert(cons(n,l),m) = 2l + 2m + 4n + 10 >= l + 2m + 2n + 4 = cons(m,cons(n,l)) 25.38/7.88 25.38/7.88 insert(cons(n,l),m) = 2l + 2m + 4n + 10 >= 2m + 4n + 1 = lte(m,n) 25.38/7.88 25.38/7.88 insert(cons(n,l),m) = 2l + 2m + 4n + 10 >= 2l + 2m + 2n + 8 = cons(n,insert(l,m)) 25.38/7.88 25.38/7.88 ordered(nil()) = 14 >= 0 = true() 25.38/7.90 25.38/7.90 ordered(cons(m,nil())) = 8m + 22 >= 0 = true() 25.38/7.90 25.38/7.90 ordered(cons(m,cons(n,l))) = 4l + 8m + 8n + 18 >= 4l + 8n + 10 = ordered(cons(n,l)) 25.38/7.90 25.38/7.90 ordered(cons(m,cons(n,l))) = 4l + 8m + 8n + 18 >= 2m + 4n + 1 = lte(m,n) 25.38/7.90 25.38/7.90 ordered(cons(m,cons(n,l))) = 4l + 8m + 8n + 18 >= 0 = false() 25.38/7.90 25.38/7.90 s(x) = 2x + 1 >= x = x 25.38/7.90 25.38/7.90 insert(x,y) = 2x + 2y + 6 >= x = x 25.38/7.90 25.38/7.90 insert(x,y) = 2x + 2y + 6 >= y = y 25.38/7.90 25.38/7.90 lte(x,y) = 2x + 4y + 1 >= x = x 25.38/7.90 25.38/7.90 lte(x,y) = 2x + 4y + 1 >= y = y 25.38/7.90 25.38/7.90 ordered(x) = 4x + 2 >= x = x 25.38/7.90 25.38/7.90 cons(x,y) = 2x + y + 2 >= x = x 25.38/7.90 25.38/7.90 cons(x,y) = 2x + y + 2 >= y = y 25.38/7.90 problem: 25.38/7.90 25.38/7.90 Qed 25.38/7.90 This critical pair is unfeasible. 25.38/7.90 25.68/8.28 EOF