Here is a small patch that adds the power operator to the theory z_numbers and adds the obvious theorem about the finiteness and size of a powerset (of a finite set) to the theory z_numbers1. (There could be scope for improving the proof.)
Before I do more on this I wondered - has anyone already done this? - is this heading in the right direction? Thanks, Phil
patch-2.8.1.pbc.100131.gz
Description: GNU Zip compressed data
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
