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 "terms/parallel_reduction.ma".
17 (* PARALLEL COMPUTATION (MULTISTEP) *****************************************)
19 definition preds: relation term ≝ star … pred.
21 interpretation "parallel computation"
22 'ParRedStar M N = (preds M N).
24 lemma preds_refl: reflexive … preds.
28 lemma preds_step_sn: ∀M1,M. M1 ⤇ M → ∀M2. M ⤇* M2 → M1 ⤇* M2.
32 lemma preds_step_dx: ∀M1,M. M1 ⤇* M → ∀M2. M ⤇ M2 → M1 ⤇* M2.
36 lemma preds_step_rc: ∀M1,M2. M1 ⤇ M2 → M1 ⤇* M2.
40 lemma preds_compatible_abst: compatible_abst preds.
44 lemma preds_compatible_sn: compatible_sn preds.
48 lemma preds_compatible_dx: compatible_dx preds.
52 lemma preds_compatible_appl: compatible_appl preds.
56 lemma preds_lift: liftable preds.
60 lemma preds_inv_lift: deliftable_sn preds.
61 /3 width=3 by star_deliftable_sn, pred_inv_lift/
64 lemma preds_dsubst_dx: dsubstable_dx preds.
68 lemma preds_dsubst: dsubstable preds.
72 theorem preds_trans: transitive … preds.
73 /2 width=3 by trans_star/
76 lemma preds_strip: ∀M0,M1. M0 ⤇* M1 → ∀M2. M0 ⤇ M2 →
77 ∃∃M. M1 ⤇ M & M2 ⤇* M.
78 /3 width=3 by star_strip, pred_conf/
81 theorem preds_conf: confluent … preds.
82 /3 width=3 by star_confluent, pred_conf/