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. (((stroke par bottom) par false) -o (bottom par stroke)))
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. (((((stroke par NewL) par false) -o ((stroke par L) par stroke)) <== ((X par false) -o D)) <== ((NewL par false) -o (L par stroke))))
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. (((((stroke par L) par false) -o ((stroke par L) par stroke)) <== (((D par stroke) par false) -o X)) <== ((NewR par false) -o (R par stroke))))
Invariant proved.

hc> (pi R, L, X. (lookup X (bt X L R)))
ll> (pi R, L, X. ((stroke par false) -o (stroke par L)))
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. ((((stroke par false) -o (stroke par L)) <== ((X par false) -o D)) <== ((stroke 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. ((((stroke par false) -o (stroke par L)) <== (((D par stroke) par false) -o X)) <== ((stroke par false) -o R)))
Invariant proved.

hc> (build nil root)
ll> ((bottom par false) -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. ((((T1 par false) -o (stroke par L)) <== ((T2 par false) -o L)) <== ((T1 par false) -o (T2 par stroke))))
Invariant proved.

hc> (traverse root nil)
ll> ((bottom par false) -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. ((((((stroke par L) par false) -o S) <== ((L par false) -o Left)) <== ((R par false) -o Right)) <== ((Left par (stroke par Right)) o-o S)))
Invariant proved.

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

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

hc> (pi T, N. (rotate (bt N root T) (bt N root T)))
ll> (pi T, N. (((stroke par bottom) par false) -o (stroke par bottom)))
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. (((Res par false) -o (stroke par (stroke par L))) <== ((Res par false) -o (stroke par L))))
Invariant proved.

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

hc> (rtraverse root nil)
ll> ((bottom par false) -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. ((((stroke par bottom) par false) -o (stroke par S)) <== ((R par false) -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. (((((stroke par (stroke par L)) par false) -o S) <== ((U par false) -o (stroke par (stroke par L)))) <== ((U par false) -o S)))
Invariant FAILS.