I have found denormalized terms popping up rather more than I would hope and causing me problems. I have found them occurring in two ways:

1. ML quotations nested in Z terms; 2. when avoiding variable capture, primarily z_%forall%_elim etc. The attached script gives an account of these issues.

## Advertising

Is the intention that Z proof operations always produce (valid) Z terms? PhilP.S. I have noticed that inst [] [] is not an identity operation, which may be related to item 1 above.

**
denormalized_z_egs.sml.gz**

*Description:* GNU Zip compressed data

_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com