Changeset 3078 for src/ASM/Policy.ma


Ignore:
Timestamp:
Apr 3, 2013, 3:01:54 PM (6 years ago)
Author:
tranquil
Message:

fixed change of Mov

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2771 r3078  
    640640 [ <plus_n_O #_ @le_n
    641641 | -n #n <plus_n_Sm #Hind #H @(transitive_le ??? (Hind (le_S_to_le … H)))
    642    lapply (proj2 ?? (proj1 ?? (pi2 ?? pol)) (λx.zero 16) (i+n) H)
    643    lapply (refl ? (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)))
    644    cases (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)) in ⊢ (???% → %);
    645    [ normalize nodelta #_ #abs cases abs
    646    | #x cases x -x #pc #jl #EQ normalize nodelta
    647      lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol)))
    648      cases (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol)) in ⊢ (???% → %);
    649      [ normalize nodelta #_ #abs cases abs
    650      | #x cases x -x #Spc #Sjl #SEQ normalize nodelta #Hcomp
     642   lapply (proj2 ?? (proj1 ?? (pi2 ?? pol)) (λx.〈XData, bv_zero 16〉) (i+n) H)
     643   inversion (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol))
     644   [ normalize nodelta #_ *
     645   | * #pc #jl #EQ normalize nodelta
     646     inversion (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol))
     647     [ normalize nodelta #_ *
     648     | * #Spc #Sjl #SEQ normalize nodelta #Hcomp
    651649       >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    652650       >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hcomp @le_plus_n_r
Note: See TracChangeset for help on using the changeset viewer.