Changeset 2238 for src/ASM

Timestamp:

Jul 23, 2012, 11:31:57 PM (7 years ago)

Author:

sacerdot

Message:

Taken out lemma integrated.

File:

• src/ASM/PolicyStep.ma (modified) (2 diffs)

src/ASM/PolicyStep.ma

@@ -374 +374 @@
 |4: lapply (pi2 ?? acc) >p lapply (refl ? (inc_pc_sigma)) cases inc_pc_sigma in ⊢ (???% → %);
   #inc_pc #inc_sigma #Hips
-  lapply (refl ? (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉))
-  cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in ⊢ (???% → %);
+  inversion (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
   #old_pc #old_length #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim
   #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta
@@ -397 +396 @@
     <Heq2b >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
   | (* jump_increase *)
-    @(jump_expansion_step3 …)
-    cases daemon (*XXX*)
+    @(jump_expansion_step3 … (pi1 ?? old_sigma) … prf … p1 ??? old_length Holdeq
+      … Heq1 prefix_ok1 prefix_ok Heq2b)
+    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
+    cases (pi2 … old_sigma) * * * #H #_ #_ #_ #_ @H
   | (* sigma_compact_unsafe *) cases daemon (*
     #i >append_length <commutative_plus #Hi normalize in Hi;