[ProofPower] Denormalized Z terms

[Phil Clayton]

(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.)

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?

Phil

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: P.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