Changeset 896 for src

Timestamp:

Jun 8, 2011, 10:38:31 AM (10 years ago)

Author:

sacerdot

Message:

Proof finished (but ugly) :-)

File:

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

src/ASM/AssemblyProof.ma

@@ -750 +750 @@
    change in ⊢ (let fetched ≝ % in ?) with (fetch0 ??)
    whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?)
-   <H2 whd BUGHERE
- ]
+   <H2 whd >eq_instruction_refl >H4 @eq_bv_refl]
  #H >H * #H1 try (change in ⊢ (% → ?) with (? ∧ ?) * #H2)
  try (change in ⊢ (% → ?) with (? ∧ ?) * #H3) whd in ⊢ (% → ?) #H4
@@ -760 +759 @@
   37,38,39,40,41,44,45, 46,49,50,53,54,57,58,62,64,65,68,69,79,82,85,86,87,88,
   89,90,91,92,93,94: <H2]
- whd >eq_instruction_refl >H4 try @eq_bv_refl
+ whd >eq_instruction_refl >H4 @eq_bv_refl
 qed.