[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Very slow proof of interpolation lemma

Hi all,

Attached is a PVS theory designed to make working with linearly interpolated lookup tables easier. Don’t be fooled by the name — although it’s called LookupTable2D and has a structure with a similar name, it’s really just about 2-d interpolation (the lookup tables are in the original version, but are not of interest for my question). Here is the theory along with its proof file:

Attachment: LookupTable2D.pvs
Description: Binary data

Attachment: LookupTable2D.prf
Description: Binary data

When I run this, it takes an extremely long time to run. Are there tricks (such as hiding more sequents) that I should be using to improve this?

Any suggestions are appreciated. The lemma of primary importance is interpolate_2D_interpolates.

Best Regards,
Ben Hocking