Changeset 2168


Ignore:
Timestamp:
Jul 8, 2012, 4:34:21 PM (5 years ago)
Author:
sacerdot
Message:

No more daemons left! All axioms are real axioms.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Test.ma

    r2167 r2168  
    369369      (low_internal_ram pseudo_assembly_program cm s)).
    370370 /2 by insert_low_internal_ram_of_pseudo_low_internal_ram/
     371qed.
     372
     373(* Real axiom ATM *)
     374axiom insert_high_internal_ram_of_pseudo_high_internal_ram:
     375 ∀M,sigma,cm,s,addr,v,v'.
     376 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' →
     377  insert Byte 7 addr v'
     378  (high_internal_ram_of_pseudo_high_internal_ram M
     379   (high_internal_ram pseudo_assembly_program cm s))
     380  =high_internal_ram_of_pseudo_high_internal_ram M
     381   (insert Byte 7 addr v (high_internal_ram pseudo_assembly_program cm s)).
     382
     383lemma insert_high_internal_ram_status_of_pseudo_status:
     384 ∀M,cm,sigma,policy,s,addr,v,v'.
     385 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' →
     386  insert Byte 7 addr v'
     387   (high_internal_ram (BitVectorTrie Byte 16)
     388    (code_memory_of_pseudo_assembly_program cm sigma policy)
     389    (status_of_pseudo_status M cm s sigma policy))
     390  = high_internal_ram_of_pseudo_high_internal_ram M
     391     (insert Byte 7 addr v
     392      (high_internal_ram pseudo_assembly_program cm s)).
     393 /2 by insert_high_internal_ram_of_pseudo_high_internal_ram/
    371394qed.
    372395
     
    676699      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
    677700      >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta
    678       [ cases daemon (*CSC*)
    679       | >(insert_low_internal_ram_status_of_pseudo_status … v) // <EQ2
    680         @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % ]
     701      [ >(insert_high_internal_ram_status_of_pseudo_status … v)
     702      | >(insert_low_internal_ram_status_of_pseudo_status … v) ]
     703      // <EQ2 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
    681704  |5: #EQ1 #EQ2 <EQ2 >get_register_status_of_pseudo_status
    682705      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.