matita/matita/lib/lambda/terms/parallel_computation.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "lambda/terms/parallel_reduction.ma".
  16
  17 include "lambda/notation/relations/parredstar_2.ma".
  18
  19 (* PARALLEL COMPUTATION (MULTISTEP) *****************************************)
  20
  21 definition preds: relation term ≝ star … pred.
  22
  23 interpretation "parallel computation"
  24    'ParRedStar M N = (preds M N).
  25
  26 lemma preds_refl: reflexive … preds.
  27 //
  28 qed.
  29
  30 lemma preds_step_sn: ∀M1,M. M1 ⤇ M → ∀M2. M ⤇* M2 → M1 ⤇* M2.
  31 /2 width=3/
  32 qed-.
  33
  34 lemma preds_step_dx: ∀M1,M. M1 ⤇* M → ∀M2. M ⤇ M2 → M1 ⤇* M2.
  35 /2 width=3/
  36 qed-.
  37
  38 lemma preds_step_rc: ∀M1,M2. M1 ⤇ M2 → M1 ⤇* M2.
  39 /2 width=1/
  40 qed.
  41
  42 lemma preds_compatible_abst: compatible_abst preds.
  43 /3 width=1/
  44 qed.
  45
  46 lemma preds_compatible_sn: compatible_sn preds.
  47 /3 width=1/
  48 qed.
  49
  50 lemma preds_compatible_dx: compatible_dx preds.
  51 /3 width=1/
  52 qed.
  53
  54 lemma preds_compatible_appl: compatible_appl preds.
  55 /3 width=1/
  56 qed.
  57
  58 lemma preds_lift: liftable preds.
  59 /2 width=1/
  60 qed.
  61
  62 lemma preds_inv_lift: deliftable_sn preds.
  63 /3 width=3 by star_deliftable_sn, pred_inv_lift/
  64 qed-.
  65
  66 lemma preds_dsubst_dx: dsubstable_dx preds.
  67 /2 width=1/
  68 qed.
  69
  70 lemma preds_dsubst: dsubstable preds.
  71 /2 width=1/
  72 qed.
  73
  74 theorem preds_trans: transitive … preds.
  75 /2 width=3 by trans_star/
  76 qed-.
  77
  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/
  81 qed-.
  82
  83 theorem preds_conf: confluent … preds.
  84 /3 width=3 by star_confluent, pred_conf/
  85 qed-.