Ignore:
Timestamp:
Jun 26, 2012, 4:05:15 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplitSplit.ma

    r2062 r2110  
    8181qed.
    8282
    83 lemma medium_jump_cond_ok:
     83lemma absolute_jump_cond_ok:
    8484  ∀v1, v2: Word.
    8585  ∀is_possible, offset, v1_upper, v1_lower.
    86     〈is_possible, offset〉 = medium_jump_cond v1 v2 →
     86    〈is_possible, offset〉 = absolute_jump_cond v1 v2 →
    8787      〈v1_upper, v1_lower〉 = vsplit ? 5 11 v1 →
    8888        is_possible → v2 = v1_upper @@ offset.
    8989  #v1 #v2 #is_possible #offset #v1_upper #v1_lower
    90   whd in match medium_jump_cond; normalize nodelta
     90  whd in match absolute_jump_cond; normalize nodelta
    9191  @pair_elim #fst_5_addr #rest_addr #vsplit_v2_refl
    9292  @pair_elim #fst_5_pc #rest_pc #vsplit_v1_refl
     
    202202    inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta
    203203    [2:
    204       inversion (medium_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta
     204      inversion (absolute_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta
    205205      inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta
    206206    ]
     
    240240        [1:
    241241          >EQlookup_labels in mjc_refl; #mjc_refl
    242           @(medium_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))
     242          @(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))
    243243          >(andb_true_l … mj_possible_refl) @I
    244244        ]
Note: See TracChangeset for help on using the changeset viewer.