Changeset 1072 for src/common


Ignore:
Timestamp:
Jul 15, 2011, 4:56:04 PM (8 years ago)
Author:
campbell
Message:

Use not equals form of showing entry/exit labels.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r1070 r1072  
    113113
    114114lemma lookup_add_oblivious : ∀tag,A,m,i,j,a.
    115   (∃v. lookup tag A m i = Some ? v) →
    116   ∃v. lookup tag A (add tag A m j a) i = Some ? v.
    117 #tag #A #m #i #j #a * #v #H
     115  (lookup tag A m i ≠ None ?) →
     116  lookup tag A (add tag A m j a) i ≠ None ?.
     117#tag #A #m #i #j #a #H
    118118lapply (lookup_add_miss … m i j a)
    119119@eq_identifier_elim
    120 [ #E #_ %{a} >E @lookup_add_hit
    121 | #_ #H' %{v} <H @H' %
     120[ #E #_ >E >lookup_add_hit % #N destruct
     121| #_ #H' >H' //
    122122] qed.
    123123
Note: See TracChangeset for help on using the changeset viewer.