Ignore:
Timestamp:
Jun 13, 2011, 10:54:58 AM (8 years ago)
Author:
mulligan
Message:

split definition

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r943 r944  
    15361536    | ADDR11 _ ⇒ true
    15371537    | ADDR16 _ ⇒ true ].
    1538 
    1539 definition next_internal_pseudo_address_map ≝
    1540  λM:internal_pseudo_address_map.
    1541   λs:PseudoStatus.
    1542    match \fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s)) with
     1538   
     1539definition next_internal_pseudo_address_map0 ≝
     1540  λfetched.
     1541  λM: internal_pseudo_address_map.
     1542  λs: PseudoStatus.
     1543   match fetched with
    15431544    [ Comment _ ⇒ Some ? M
    15441545    | Cost _ ⇒ Some … M
     
    15651566            None ?       
    15661567        | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
     1568 
     1569
     1570definition next_internal_pseudo_address_map ≝
     1571 λM:internal_pseudo_address_map.
     1572  λs:PseudoStatus.
     1573    next_internal_pseudo_address_map0 (\fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s))) M s.
    15671574   
    15681575definition status_of_pseudo_status:
     
    20762083  [ cases (code_memory … ps) #preamble #instr_list whd in ⊢ (???% → ?) #EQ >EQ #H #MAP
    20772084    #abs @⊥ normalize in abs; destruct (abs) ]
    2078  * #labels #costs whd in ⊢ (? → ? → ??%? → ?) generalize in match (refl … (code_memory … ps))
     2085 * #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ?)
     2086 generalize in match (refl … (code_memory … ps))
    20792087 cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta;
    20802088 generalize in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) *; normalize nodelta;
Note: See TracChangeset for help on using the changeset viewer.