Changeset 1522 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Nov 21, 2011, 3:49:04 PM (8 years ago)
Author:
mulligan
Message:

changes to preamble and lin to asm pass, resolved conflict in interpret

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1514 r1522  
    1 
    21include "ASM/ASMCosts.ma".
    32include "ASM/WellLabeled.ma".
     
    209208    cases(lt_to_not_zero … proof)
    210209  | #m' #proof
    211     normalize in ⊢ (???%)
     210    normalize in ⊢ (???%);
    212211    cases n
    213212    [ normalize //
     
    256255  ]
    257256qed.
     257
     258include alias "arithmetics/nat.ma".
    258259
    259260lemma plus_minus_rearrangement_1:
     
    277278              >(associative_plus (m' - n) 1 (o - m' - 1))
    278279              <commutative_plus in match (1 + (o - m' - 1));
    279               <(minus_m_n_minus_minus_plus_1 o m') in match (o - m' - 1 + 1)
     280              <(minus_m_n_minus_minus_plus_1 o m') in match (o - m' - 1 + 1);
    280281              [1: >ind_hyp
    281282                [1: %
     
    338339    clock … (write_at_stack_pointer … s sp) = clock … s.
    339340  #s #sp
    340   change in match (write_at_stack_pointer (BitVectorTrie Byte 16) s sp) with (
     341  change in match (write_at_stack_pointer (BitVectorTrie Byte 16) s sp); with (
    341342      let 〈nu, nl〉 ≝ split bool 4 4 (get_8051_sfr … s SFR_SP) in
    342343        ?);
Note: See TracChangeset for help on using the changeset viewer.