Changeset 2238 for src/ASM


Ignore:
Timestamp:
Jul 23, 2012, 11:31:57 PM (7 years ago)
Author:
sacerdot
Message:

Taken out lemma integrated.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2237 r2238  
    374374|4: lapply (pi2 ?? acc) >p lapply (refl ? (inc_pc_sigma)) cases inc_pc_sigma in ⊢ (???% → %);
    375375  #inc_pc #inc_sigma #Hips
    376   lapply (refl ? (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉))
    377   cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in ⊢ (???% → %);
     376  inversion (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
    378377  #old_pc #old_length #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim
    379378  #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta
     
    397396    <Heq2b >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
    398397  | (* jump_increase *)
    399     @(jump_expansion_step3 …)
    400     cases daemon (*XXX*)
     398    @(jump_expansion_step3 … (pi1 ?? old_sigma) … prf … p1 ??? old_length Holdeq
     399      … Heq1 prefix_ok1 prefix_ok Heq2b)
     400    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     401    cases (pi2 … old_sigma) * * * #H #_ #_ #_ #_ @H
    401402  | (* sigma_compact_unsafe *) cases daemon (*
    402403    #i >append_length <commutative_plus #Hi normalize in Hi;
Note: See TracChangeset for help on using the changeset viewer.