Add some useful advantage properties

Open cmester0 opened this issue 6 months ago • 3 comments

Jun 06 '25 14:06 cmester0

@MarkusKL @spitters These statements should hopefully enable simpler proof structure and thus better automation. We seem to be missing some weakening statement, as ValidPackage now requires the export interface to match exactly.

Jun 10 '25 18:06 cmester0

Should be revisited after nominal: https://github.com/SSProve/ssprove/pull/82

Jul 14 '25 08:07 spitters

I rebased this on top of the nominal changes.

@MarkusKL most of your comments were addressed. Is there anything more blocking this from being merged?

Nov 06 '25 15:11 4ever2