Changeset 896


Ignore:
Timestamp:
Jun 8, 2011, 10:38:31 AM (8 years ago)
Author:
sacerdot
Message:

Proof finished (but ugly) :-)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r894 r896  
    750750   change in ⊢ (let fetched ≝ % in ?) with (fetch0 ??)
    751751   whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?)
    752    <H2 whd BUGHERE
    753  ]
     752   <H2 whd >eq_instruction_refl >H4 @eq_bv_refl]
    754753 #H >H * #H1 try (change in ⊢ (% → ?) with (? ∧ ?) * #H2)
    755754 try (change in ⊢ (% → ?) with (? ∧ ?) * #H3) whd in ⊢ (% → ?) #H4
     
    760759  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,
    761760  89,90,91,92,93,94: <H2]
    762  whd >eq_instruction_refl >H4 try @eq_bv_refl
     761 whd >eq_instruction_refl >H4 @eq_bv_refl
    763762qed.
    764763 
Note: See TracChangeset for help on using the changeset viewer.