[Why3-club] Consistency of map theory

Santiago Zanella szanella at gmail.com
Thu Nov 22 14:34:31 CET 2012

I believe the culprit is a typo in the permut_eq lemma:

  lemma permut_eq :
    forall a1 a2 : map int 'a. forall l u : int.
    permut_sub a1 a2 l u ->
    forall i:int. (i < l \/ u <= i) -> a2[i] = a1[i]
The last line should read

    forall i:int. (i < u \/ l <= i) -> a2[i] = a1[i]
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20121122/35ca3c7a/attachment.html>

More information about the Why3-club mailing list