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 (* PARALLEL COMPUTATION (MULTISTEP) *****************************************)
  18
  19 definition preds: relation term ≝ star … pred.
  20
  21 interpretation "parallel computation"
  22    'ParRedStar M N = (preds M N).
  23
  24 lemma preds_refl: reflexive … preds.
  25 //
  26 qed.
  27
  28 lemma preds_step_sn: ∀M1,M. M1 ⤇ M → ∀M2. M ⤇* M2 → M1 ⤇* M2.
  29 /2 width=3/
  30 qed-.
  31
  32 lemma preds_step_dx: ∀M1,M. M1 ⤇* M → ∀M2. M ⤇ M2 → M1 ⤇* M2.
  33 /2 width=3/
  34 qed-.
  35
  36 lemma preds_step_rc: ∀M1,M2. M1 ⤇ M2 → M1 ⤇* M2.
  37 /2 width=1/
  38 qed.
  39
  40 lemma preds_compatible_abst: compatible_abst preds.
  41 /3 width=1/
  42 qed.
  43
  44 lemma preds_compatible_sn: compatible_sn preds.
  45 /3 width=1/
  46 qed.
  47
  48 lemma preds_compatible_dx: compatible_dx preds.
  49 /3 width=1/
  50 qed.
  51
  52 lemma preds_compatible_appl: compatible_appl preds.
  53 /3 width=1/
  54 qed.
  55
  56 lemma preds_lift: liftable preds.
  57 /2 width=1/
  58 qed.
  59
  60 lemma preds_inv_lift: deliftable_sn preds.
  61 /3 width=3 by star_deliftable_sn, pred_inv_lift/
  62 qed-.
  63
  64 lemma preds_dsubst_dx: dsubstable_dx preds.
  65 /2 width=1/
  66 qed.
  67
  68 lemma preds_dsubst: dsubstable preds.
  69 /2 width=1/
  70 qed.
  71
  72 theorem preds_trans: transitive … preds.
  73 /2 width=3 by trans_star/
  74 qed-.
  75
  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/
  79 qed-.
  80
  81 theorem preds_conf: confluent … preds.
  82 /3 width=3 by star_confluent, pred_conf/
  83 qed-.