- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
- 12
- 13
- 14
- 15
- 16
- 17
- 18
- 19
- 20
- 21
- 22
- 23
- 24
- 25
- 26
- 27
- 28
(** Set of all possible interleaving of two traces is a trace
ensemble. As we later prove in [interleaving_to_permutation], this
definition is dual to [Permutation]. *)
Inductive Interleaving : list TE -> list TE -> TraceEnsemble :=
| ilv_cons_l : forall te t1 t2 t,
Interleaving t1 t2 t ->
Interleaving (te :: t1) t2 (te :: t)
| ilv_cons_r : forall te t1 t2 t,
Interleaving t1 t2 t ->
Interleaving t1 (te :: t2) (te :: t)
| ilv_nil : Interleaving [] [] [].
Попытка оптимизации:
(* Left-biased version of [Interleaving] that doesn't make
distinction between schedulings of commuting elements: *)
Inductive UniqueInterleaving : list TE -> list TE -> TraceEnsemble :=
| uilv_cons_l : forall l t1 t2 t,
UniqueInterleaving t1 t2 t ->
UniqueInterleaving (l :: t1) t2 (l :: t)
| uilv_cons_r1 : forall l r t1 t2 t,
~trace_elems_commute l r ->
UniqueInterleaving (l :: t1) t2 (l :: t) ->
UniqueInterleaving (l :: t1) (r :: t2) (r :: l :: t)
| uilv_cons_r2 : forall r1 r2 t1 t2 t,
UniqueInterleaving t1 (r1 :: t2) (r1 :: t) ->
UniqueInterleaving t1 (r2 :: r1 :: t2) (r2 :: r1 :: t)
| uilv_nil : forall t, UniqueInterleaving [] t t.