1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "lambda/terms/parallel_reduction.ma".
17 include "lambda/notation/relations/parredstar_2.ma".
19 (* PARALLEL COMPUTATION (MULTISTEP) *****************************************)
21 definition preds: relation term ≝ star … pred.
23 interpretation "parallel computation"
24 'ParRedStar M N = (preds M N).
26 lemma preds_refl: reflexive … preds.
30 lemma preds_step_sn: ∀M1,M. M1 ⤇ M → ∀M2. M ⤇* M2 → M1 ⤇* M2.
34 lemma preds_step_dx: ∀M1,M. M1 ⤇* M → ∀M2. M ⤇ M2 → M1 ⤇* M2.
38 lemma preds_step_rc: ∀M1,M2. M1 ⤇ M2 → M1 ⤇* M2.
42 lemma preds_compatible_abst: compatible_abst preds.
46 lemma preds_compatible_sn: compatible_sn preds.
50 lemma preds_compatible_dx: compatible_dx preds.
54 lemma preds_compatible_appl: compatible_appl preds.
58 lemma preds_lift: liftable preds.
62 lemma preds_inv_lift: deliftable_sn preds.
63 /3 width=3 by star_deliftable_sn, pred_inv_lift/
66 lemma preds_dsubst_dx: dsubstable_dx preds.
70 lemma preds_dsubst: dsubstable preds.
74 theorem preds_trans: transitive … preds.
75 /2 width=3 by trans_star/
78 lemma preds_strip: ∀M0,M1. M0 ⤇* M1 → ∀M2. M0 ⤇ M2 →
79 ∃∃M. M1 ⤇ M & M2 ⤇* M.
80 /3 width=3 by star_strip, pred_conf/
83 theorem preds_conf: confluent … preds.
84 /3 width=3 by star_confluent, pred_conf/