(By 'denormalized Z term', I mean a term that is not Z but is alpha-convertible to a Z term, so could be fixed to be a Z term. I can't remember if we decided on better word than 'denormalized' - I will happily use some other word if one exists.)

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.

Is the intention that Z proof operations always produce (valid) Z terms?


P.S. I have noticed that inst [] [] is not an identity operation, which may be related to item 1 above.

Attachment: denormalized_z_egs.sml.gz
Description: GNU Zip compressed data

Proofpower mailing list

Reply via email to