Changeset 2113


Ignore:
Timestamp:
Jun 27, 2012, 12:49:22 AM (5 years ago)
Author:
sacerdot
Message:

Proof by cases repaired; dead code removed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2112 r2113  
    935935 #H >H * #H1 try (whd in ⊢ (% → ?); * #H2)
    936936 try (whd in ⊢ (% → ?); * #H3) whd in ⊢ (% → ?); #H4
    937  XXX
    938  [ whd in match fetch; normalize nodelta <H1 ] cases daemon
    939 (*
    940  whd in ⊢ (let ? ≝ ??% in ?); <H1 whd in ⊢ (let fetched ≝ % in ?)
    941  [17,18,19,20,21,22,23,24,25,26,31,34,35,36,37,38: <H3]
    942  [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,
    943   30,31,32,33,34,35,36,37,38,39,40,43,45,48,49,52,53,54,55,56,57,60,61,62,65,66,
    944   69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2]
    945  whd >eq_instruction_refl >H4 @eq_bv_refl
    946 *) (* XXX: not working! *)
     937 whd in match fetch; normalize nodelta <H1 whd in ⊢ (match % with [ _ ⇒ ? ]);
     938 [17,18,19,20,21,22,23,24,25,26,32,34,35,36,37,39: <H3]
     939 try <H2 whd >eq_instruction_refl >H4 @eq_bv_refl
    947940qed.
    948941
Note: See TracChangeset for help on using the changeset viewer.