Changeset 1606 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Dec 14, 2011, 1:40:08 PM (8 years ago)
Author:
sacerdot
Message:

Porting to last library of Matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1600 r1606  
    608608  clock ? (execute_1_preinstruction ticks a m f i s) = \fst ticks + clock … s ∨
    609609  clock ? (execute_1_preinstruction ticks a m f i s) = \snd ticks + clock … s.
    610  #ticks #a #m #f #i #s whd in match execute_1_preinstruction; normalize nodelta @sig2
     610 #ticks #a #m #f #i #s whd in match execute_1_preinstruction; normalize nodelta @pi2
    611611qed.
    612612
     
    712712      ]. (*10s*)
    713713    [||||||||*:try assumption]
    714     [1,2,3,4,5,7: @sig2 (*35s*)
     714    [1,2,3,4,5,7: @pi2 (*35s*)
    715715    |8: lapply (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ?
    716716        (λx. λs.
     
    736736
    737737lemma execute_1_ok: ∀s. clock … (execute_1 s) = current_instruction_cost s + clock … s.
    738  #s whd in match execute_1; normalize nodelta @sig2
     738 #s whd in match execute_1; normalize nodelta @pi2
    739739qed-. (*x Andrea: indexing takes ages here *)
    740740
Note: See TracChangeset for help on using the changeset viewer.