make: `tl.lp' is up to date.

hc> (pi N. (leq z N))
ll> (pi N. ((bottom par false) -o N))
Invariant proved.

hc> (pi M, N. ((leq (s N) (s M)) <== (leq N M)))
ll> (pi M, N. ((((stroke par N) par false) -o (stroke par M)) <== ((N par false) -o M)))
Invariant proved.

hc> (pi M. (gr (s M) z))
ll> (pi M. (((bottom par stroke) par false) -o (stroke par M)))
Invariant proved.

hc> (pi M, N. ((gr (s N) (s M)) <== (gr N M)))
ll> (pi M, N. (((((stroke par M) par stroke) par false) -o (stroke par N)) <== (((M par stroke) par false) -o N)))
Invariant proved.

hc> (pi X. (insert X root (bt X root root)))
ll> (pi X. (((item X) par bottom) o-o (((item X) par bottom) par bottom)))
Invariant proved.

hc> (pi NewL, D, R, L, X, N. (((insert X (bt D L R) (bt D NewL R)) <== (leq X D)) <== (insert X L NewL)))
ll> (pi NewL, D, R, L, X, N. (((((item X) par (((item D) par L) par R)) o-o (((item D) par NewL) par R)) <== ((X par false) -o D)) <== (((item X) par L) o-o NewL)))
Invariant proved.

hc> (pi NewR, D, R, L, X, N. (((insert X (bt D L R) (bt D L NewR)) <== (gr X D)) <== (insert X R NewR)))
ll> (pi NewR, D, R, L, X, N. (((((item X) par (((item D) par L) par R)) o-o (((item D) par L) par NewR)) <== (((D par stroke) par false) -o X)) <== (((item X) par R) o-o NewR)))
Invariant proved.

hc> (pi R, L, X. (lookup X (bt X L R)))
ll> (pi R, L, X. (((item X) par false) -o (((item X) par L) par R)))
Invariant proved.

hc> (pi D, R, L, X. (((lookup X (bt D L R)) <== (leq X D)) <== (lookup X L)))
ll> (pi D, R, L, X. (((((item X) par false) -o (((item D) par L) par R)) <== ((X par false) -o D)) <== (((item X) par false) -o L)))
Invariant proved.

hc> (pi D, R, L, X. (((lookup X (bt D L R)) <== (gr X D)) <== (lookup X R)))
ll> (pi D, R, L, X. (((((item X) par false) -o (((item D) par L) par R)) <== (((D par stroke) par false) -o X)) <== (((item X) par false) -o R)))
Invariant proved.

hc> (build nil root)
ll> (bottom o-o bottom)
Invariant proved.

hc> (pi T1, T2, L, X. (((build (cons X L) T1) <== (build L T2)) <== (insert X T2 T1)))
ll> (pi T1, T2, L, X. (((((item X) par L) o-o T1) <== (L o-o T2)) <== (((item X) par T2) o-o T1)))
Invariant proved.

hc> (traverse root nil)
ll> (bottom o-o bottom)
Invariant proved.

hc> (pi Left, Right, S, D, R, L. ((((traverse (bt D L R) S) <== (traverse L Left)) <== (traverse R Right)) <== (append Left (cons D Right) S)))
ll> (pi Left, Right, S, D, R, L. (((((((item D) par L) par R) o-o S) <== (L o-o Left)) <== (R o-o Right)) <== ((Left par ((item D) par Right)) o-o S)))
Invariant proved.

hc> (pi S, L. (((tsort L S) <== (build L top)) <== (traverse top S)))
ll> (pi S, L. (((L o-o S) <== (L o-o top)) <== (top o-o S)))
Invariant proved.

hc> (rotate root root)
ll> (bottom o-o bottom)
Invariant proved.

hc> (pi T, N. (rotate (bt N root T) (bt N root T)))
ll> (pi T, N. ((((item N) par bottom) par T) o-o (((item N) par bottom) par T)))
Invariant proved.

hc> (pi Res, T, R, L, M, N. ((rotate (bt N (bt M L R) T) Res) <== (rotate (bt M L (bt N R T)) Res)))
ll> (pi Res, T, R, L, M, N. (((((item N) par (((item M) par L) par R)) par T) o-o Res) <== ((((item M) par L) par (((item N) par R) par T)) o-o Res)))
Invariant proved.

hc> (rtraverse root nil)
ll> (bottom o-o bottom)
Invariant proved.

hc> (pi S, R, N. ((rtraverse (bt N root R) (cons N S)) <== (rtraverse R S)))
ll> (pi S, R, N. (((((item N) par bottom) par R) o-o ((item N) par S)) <== (R o-o S)))
Invariant proved.

hc> (pi U, T, S, R, L, M, N. (((rtraverse (bt N (bt M L R) T) S) <== (rotate (bt N (bt M L R) T) U)) <== (rtraverse U S)))
ll> (pi U, T, S, R, L, M, N. ((((((item N) par (((item M) par L) par R)) par T) o-o S) <== ((((item N) par (((item M) par L) par R)) par T) o-o U)) <== (U o-o S)))
Invariant proved.

hc> (pi T, S, L. (((rsort L S) <== (build L T)) <== (rtraverse T S)))
ll> (pi T, S, L. (((L o-o S) <== (L o-o T)) <== (T o-o S)))
Invariant proved.