- Timestamp:
- Jul 23, 2012, 11:31:57 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/PolicyStep.ma
r2237 r2238 374 374 |4: lapply (pi2 ?? acc) >p lapply (refl ? (inc_pc_sigma)) cases inc_pc_sigma in ⊢ (???% → %); 375 375 #inc_pc #inc_sigma #Hips 376 lapply (refl ? (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)) 377 cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in ⊢ (???% → %); 376 inversion (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) 378 377 #old_pc #old_length #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim 379 378 #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta … … 397 396 <Heq2b >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl 398 397 | (* jump_increase *) 399 @(jump_expansion_step3 …) 400 cases daemon (*XXX*) 398 @(jump_expansion_step3 … (pi1 ?? old_sigma) … prf … p1 ??? old_length Holdeq 399 … Heq1 prefix_ok1 prefix_ok Heq2b) 400 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 401 cases (pi2 … old_sigma) * * * #H #_ #_ #_ #_ @H 401 402 | (* sigma_compact_unsafe *) cases daemon (* 402 403 #i >append_length <commutative_plus #Hi normalize in Hi;
Note: See TracChangeset
for help on using the changeset viewer.