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

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

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

hc> (pi N. (pluss (s z) N (s N)))
ll> (pi N. ((((stroke par bottom) par false) -o (stroke par N)) && (((N par stroke) par false) -o (stroke par N))))
Invariant proved.

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

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

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

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

hc> (pi N. (max (s N) z (s N)))
ll> (pi N. ((((stroke par N) par false) -o (stroke par N)) && ((bottom par false) -o (stroke par N))))
Invariant proved.

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

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

hc> (pi N. (min (s N) z z))
ll> (pi N. (((bottom par false) -o (stroke par N)) && ((bottom par false) -o bottom)))
Invariant proved.

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