Ignore:
Timestamp:
Jul 30, 2012, 6:33:11 PM (7 years ago)
Author:
mulligan
Message:

Half of JC case complete

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplitSplit.ma

    r2273 r2278  
    11include "ASM/AssemblyProofSplit.ma".
    22include "common/LabelledObjects.ma".
    3 
    4 lemma short_jump_cond_ok:
    5   ∀v1, v2: Word.
    6   ∀is_possible, offset.
    7     〈is_possible, offset〉 = short_jump_cond v1 v2 →
    8       is_possible → v2 = add 16 v1 (sign_extension offset).
    9   #v1 #v2 #is_possible #offset
    10   whd in match short_jump_cond; normalize nodelta
    11   @pair_elim #result #flags #sub16_refl
    12   @pair_elim #upper #lower #vsplit_refl
    13   inversion (get_index' bool ???) #get_index_refl normalize nodelta
    14   #relevant destruct(relevant) #relevant
    15   [1:
    16     @(sub_16_to_add_16_8_1 … flags)
    17   |2:
    18     @(sub_16_to_add_16_8_0 … flags)
    19   ]
    20   try assumption >sub16_refl
    21   <(eq_bv_eq … relevant)
    22   >(vsplit_ok … (sym_eq … vsplit_refl)) %
    23 qed.
    243
    254lemma absolute_jump_cond_ok:
Note: See TracChangeset for help on using the changeset viewer.