Changeset 1386 for src/LIN


Ignore:
Timestamp:
Oct 17, 2011, 1:58:47 AM (8 years ago)
Author:
sacerdot
Message:

Structure of semantic parameters simplified.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1385 r1386  
    3636 λ_.λ_.λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
    3737
    38 definition ltl_lin_more_sem_params1 : ∀succT,succ,pointer_of_label.more_sem_params1 … ltl_lin_params1 ≝
    39  λsuccT,succ,pointer_of_label.
    40  mk_more_sem_params1 ? ltl_lin_params1 (ltl_lin_more_sem_params succT succ pointer_of_label)
    41   ltl_lin_init_locals (ltl_lin_save_frame …).
    42 
    4338(*CSC: XXXXX, for is_final only *)
    4439axiom ltl_lin_fetch_result:
     
    5954 ∀globals. more_sem_params2 … (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) ≝
    6055 λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals.
    61   mk_more_sem_params2 … (ltl_lin_more_sem_params1 … succ pointer_of_label)
    62    (fetch globals) (load_ra …) (ltl_lin_fetch_result …) (ltl_lin_pop_frame …)
     56  mk_more_sem_params2 … (ltl_lin_more_sem_params … succ pointer_of_label)
     57   (fetch globals) (load_ra …) (ltl_lin_fetch_result …)
     58   ltl_lin_init_locals (ltl_lin_save_frame …) (ltl_lin_pop_frame …)
    6359   (ltl_lin_fetch_external_args …) (ltl_lin_set_result …) (ltl_lin_exec_extended …).
    6460
Note: See TracChangeset for help on using the changeset viewer.