Changeset 2487 for src/Clight/switchRemoval.ma

Timestamp:

Nov 23, 2012, 3:47:22 PM (8 years ago)

Author:

campbell

Message:

Set up "after_n_steps" to enforce an invariant on states.

File:

• src/Clight/switchRemoval.ma (modified) (1 diff)

src/Clight/switchRemoval.ma

@@ -2757 +2757 @@
   switch_state_sim ge s1 s1' →
   exec_step ge s1 = Value … 〈tr,s2〉 →  
-  ∃n. after_n_steps (S n) … clight_exec ge' s1'
+  ∃n. after_n_steps (S n) … clight_exec ge' s1' (λ_. true)
   (λtr',s2'. tr = tr' ∧ switch_state_sim ge' s2 s2').
 #ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state