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

hc> (pi K. (append nil K K))
ll> (pi K. ((bottom par K) o-o K))
Invariant proved.

hc> (pi X, L, K, M. ((append (cons X L) K (cons X M)) <== (append L K M)))
ll> (pi X, L, K, M. (((((item X) par L) par K) o-o ((item X) par M)) <== ((L par K) o-o M)))
Invariant proved.

hc> (pi X. (split X nil nil nil))
ll> (pi X. (bottom o-o (bottom par bottom)))
Invariant proved.

hc> (pi X, A, B, R, S. (((split X (cons A R) (cons A S) B) <== (leq A X)) <== (split X R S B)))
ll> (pi X, A, B, R, S. (((((item A) par R) o-o (((item A) par S) par B)) <== one) <== (R o-o (S par B))))
Invariant proved.

hc> (pi X, A, B, R, S. (((split X (cons A R) S (cons A B)) <== (gr A X)) <== (split X R S B)))
ll> (pi X, A, B, R, S. (((((item A) par R) o-o (S par ((item A) par B))) <== one) <== (R o-o (S par B))))
Invariant proved.

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

hc> (pi F, R, S, Sm, Bg, SS, BS. (((((sort (cons F R) S) <== (split F R Sm Bg)) <== (sort Sm SS)) <== (sort Bg BS)) <== (append SS (cons F BS) S)))
ll> (pi F, R, S, Sm, Bg, SS, BS. (((((((item F) par R) o-o S) <== (R o-o (Sm par Bg))) <== (Sm o-o SS)) <== (Bg o-o BS)) <== ((SS par ((item F) par BS)) o-o S)))
Invariant proved.

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

hc> (pi L, H, T, V, U, W. ((((perm L (cons H T)) <== (append V (cons H U) L)) <== (append V U W)) <== (perm W T)))
ll> (pi L, H, T, V, U, W. ((((L o-o ((item H) par T)) <== ((V par ((item H) par U)) o-o L)) <== ((V par U) o-o W)) <== (W o-o T)))
Invariant proved.

hc> (pi L, K. ((reverse L K) <== (rev L K nil)))
ll> (pi L, K. ((L o-o K) <== ((L par bottom) o-o K)))
Invariant proved.

hc> (pi L. ((rev nil L L) <== top))
ll> (pi L. (((bottom par L) o-o L) <== top))
Invariant proved.

hc> (pi L, K, M, X. ((rev (cons X L) K M) <== (rev L K (cons X M))))
ll> (pi L, K, M, X. (((((item X) par L) par M) o-o K) <== ((L par ((item X) par M)) o-o K)))
Invariant proved.

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

hc> (pi X, L, K, M. (((nreverse (cons X L) K) <== (nreverse L M)) <== (append M (cons X nil) K)))
ll> (pi X, L, K, M. (((((item X) par L) o-o K) <== (L o-o M)) <== ((M par ((item X) par bottom)) o-o K)))
Invariant proved.

hc> (pi X, L. ((memb X (cons X L)) <== top))
ll> (pi X, L. ((((item X) par false) -o ((item X) par L)) <== top))
Invariant proved.

hc> (pi X, L, Y. ((memb X (cons Y L)) <== (memb X L)))
ll> (pi X, L, Y. ((((item X) par false) -o ((item Y) par L)) <== (((item X) par false) -o L)))
Invariant proved.

hc> (pi A, Rest. ((memb_and_rest A (cons A Rest) Rest) <== top))
ll> (pi A, Rest. (((((item A) par false) -o ((item A) par Rest)) && ((Rest par false) -o ((item A) par Rest))) <== top))
Invariant proved.

hc> (pi A, B, Tail, Rest. ((memb_and_rest A (cons B Tail) (cons B Rest)) <== (memb_and_rest A Tail Rest)))
ll> (pi A, B, Tail, Rest. (((((item A) par false) -o ((item B) par Tail)) && ((((item B) par Rest) par false) -o ((item B) par Tail))) <== ((((item A) par false) -o Tail) && ((Rest par false) -o Tail))))
Invariant proved.