Changeset 2207 for src/ASM/Test.ma


Ignore:
Timestamp:
Jul 18, 2012, 12:29:14 PM (8 years ago)
Author:
mulligan
Message:

Improvements and corrections to the main lemma proof in AssemblyProofSplit?.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Test.ma

    r2204 r2207  
    13551355qed.
    13561356
    1357 lemma get_cy_flag_status_of_pseudo_status:
    1358   ∀M: internal_pseudo_address_map.
    1359   ∀sigma: Word → Word.
    1360   ∀policy: Word → bool.
    1361   ∀code_memory: pseudo_assembly_program.
    1362   ∀s: PreStatus ? code_memory.
    1363   ∀s'.
    1364     status_of_pseudo_status M code_memory s sigma policy = s' →
    1365       get_cy_flag ?? s' = get_cy_flag ? code_memory s.
    1366   #M #sigma #policy #code_memory #s #s' #s_refl <s_refl
    1367   whd in match get_cy_flag; normalize nodelta
    1368   whd in match status_of_pseudo_status; normalize nodelta
    1369   whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    1370   cases (\snd M) try %
    1371   * normalize nodelta #address
    1372   @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
    1373   whd in match sfr_8051_index; normalize nodelta
    1374   >get_index_v_set_index_miss [2,4: /2/] %
    1375 qed.
    1376 
    13771357lemma get_ov_flag_status_of_pseudo_status:
    13781358  ∀M: internal_pseudo_address_map.
Note: See TracChangeset for help on using the changeset viewer.