Ignore:
Timestamp:
Jun 12, 2012, 10:52:37 AM (8 years ago)
Author:
campbell
Message:

PCs for RTLabs structured traces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r1976 r2044  
    250250(* Version in Prop for showing existence. *)
    251251coinductive trace_label_diverges_exists (S:abstract_status) : S → Prop ≝
    252   | tld_step:
     252  | tld_step':
    253253      ∀status_initial: S.
    254254      ∀status_labelled: S.
     
    256256          trace_label_diverges_exists S status_labelled →
    257257            trace_label_diverges_exists S status_initial
    258   | tld_base:
     258  | tld_base':
    259259      ∀status_initial: S.
    260260      ∀status_pre_fun_call: S.
Note: See TracChangeset for help on using the changeset viewer.