Changeset 2183 for src/ASM/Test.ma


Ignore:
Timestamp:
Jul 13, 2012, 5:03:15 PM (8 years ago)
Author:
mulligan
Message:

More progress on main lemma proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Test.ma

    r2181 r2183  
    1111  ∀policy.
    1212  ∀s, s'.
    13   ∀new_ppc.
     13  ∀new_ppc, new_ppc'.
     14    sigma new_ppc = new_ppc' →
    1415    status_of_pseudo_status M cm s sigma policy = s' →
    1516    set_program_counter (BitVectorTrie Byte 16)
    1617      (code_memory_of_pseudo_assembly_program cm sigma policy)
    17       s'
    18       (sigma new_ppc) =
     18      s' new_ppc' =
    1919    status_of_pseudo_status M cm (set_program_counter … cm s new_ppc) sigma policy.
    20   #M #cm #sigma #policy #s #s' #new_ppc #s_refl <s_refl //
     20  #M #cm #sigma #policy #s #s' #new_ppc #new_ppc'
     21  #new_ppc_refl #s_refl <new_ppc_refl <s_refl //
    2122qed.
    2223
Note: See TracChangeset for help on using the changeset viewer.