search

gleiss / rapid

Software Verification tool, which uses superposition-based theorem proving to establish the functional correctness of array- and hyper-properties.
3 stars 6 forks source link

intermediate value lemma: forall quantification in premise #22

Closed mina1604 closed 5 years ago

mina1604 commented 5 years ago

Moved quantification over iterations into premise for intermediate value lemma, stating forall it. v(s(it)) = v(it)+1 as part of the premise.

gleiss commented 5 years ago

Hey, I manually added your change to one of my commit, since I refactored most of the Trace Lemma code.