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