Changeset 2264 for src/ASM/Policy.ma
- Timestamp:
- Jul 26, 2012, 12:38:42 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Policy.ma
r2230 r2264 30 30 ] (refl … z) 31 31 ] (refl … n). 32 [5: cases labels #label_map #spec #id #id_ok cases (spec … id_ok) //32 [5: #l #_ % 33 33 | normalize nodelta cases (jump_expansion_start program (create_label_map program)) 34 34 #x cases x -x … … 262 262 | Some p ⇒ measure_int l policy acc ≤ measure_int l p acc 263 263 ]. 264 [2: cases (create_label_map ?) #label_map #H #id #id_ok cases (H … id_ok) //]264 [2: #l #_ %] 265 265 #program #policy #l elim l -l; 266 266 [ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q -pi1; cases q [ // | #x #_ @le_n ] … … 332 332 [ None ⇒ True 333 333 | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → sigma_jump_equal program policy p ]. 334 [2: cases (create_label_map ?) #label_map #H #id #id_ok cases (H … id_ok) //]334 [2: #l #_ %] 335 335 #program #policy inversion (jump_expansion_step ???) 336 336 #p cases p -p #ch #pol normalize nodelta cases pol
Note: See TracChangeset
for help on using the changeset viewer.