hc> (pi K. (append nil K K))
ll> (pi K. ((false oplus 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) oplus L) oplus K) o-o ((item X) oplus M)) <== ((L oplus K) o-o M)))
Invariant proved.

hc> (pi X. (split X nil nil nil))
ll> (pi X. (((item X) oplus false) o-o ((item X) oplus (false oplus false))))
Invariant proved.

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

hc> (pi X, A, B, R, S. (((split X (cons A R) (cons A S) B) <== (gr X A)) <== (split X R S B)))
ll> (pi X, A, B, R, S. (((((item X) oplus ((item A) oplus R)) o-o ((item X) oplus (((item A) oplus S) oplus B))) <== one) <== (((item X) oplus R) o-o ((item X) oplus (S oplus 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 X) oplus ((item A) oplus R)) o-o ((item X) oplus (S oplus ((item A) oplus B)))) <== one) <== (((item X) oplus R) o-o ((item X) oplus (S oplus B)))))
Invariant proved.

hc> (sort nil nil)
ll> (false o-o false)
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) oplus R) o-o S) <== (((item F) oplus R) o-o ((item F) oplus (Sm oplus Bg)))) <== (Sm o-o SS)) <== (Bg o-o BS)) <== ((SS oplus ((item F) oplus BS)) o-o S)))
Invariant proved.