Changeset 3396 for LTS/Traces.ma


Ignore:
Timestamp:
Nov 15, 2013, 2:51:50 PM (6 years ago)
Author:
piccolo
Message:

correctness proof in developping

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Traces.ma

    r3394 r3396  
    3939coercion a_non_functional_label.
    4040
     41(*
    4142definition ret_act_label_to_cost_label :
    4243(ReturnPostCostLabel + NonFunctionalLabel) → CostLabel ≝
     
    5051
    5152coercion call_act_label_to_cost_label.
     53*)
    5254
    5355definition eq_nf_label : NonFunctionalLabel → NonFunctionalLabel → bool ≝
     
    183185
    184186inductive ActionLabel : Type[0] ≝
    185  | call_act : FunctionName → (CallCostLabel + NonFunctionalLabel) → ActionLabel
    186  | ret_act : option(ReturnPostCostLabel + NonFunctionalLabel) → ActionLabel
     187 | call_act : FunctionName → CallCostLabel → ActionLabel
     188 | ret_act : option(ReturnPostCostLabel) → ActionLabel
    187189 | cost_act : option NonFunctionalLabel → ActionLabel
    188190 | init_act : ActionLabel.
Note: See TracChangeset for help on using the changeset viewer.