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?


Attachment: patch-2.8.1.pbc.100131.gz
Description: GNU Zip compressed data

Proofpower mailing list

Reply via email to