TRIV is a built-in module in which only one sort Elt is declared.

The sort NzNat is declared in the module NAT-VALUE imported into NAT and stands for non-zero natural numbers.

The result is a reduct of the term, but it might not be in normal form. For example, the result of evaluating inf(1) is cons(1, inf(1+1)) that is not in normal form w.r.t. TEST1.

Kazuhiro Ogata
Mon Nov 29 13:47:22 JST 1999