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_computation.ma".
17 include "lambda/notation/relations/seqredstar_2.ma".
19 (* SEQUENTIAL COMPUTATION (MULTISTEP) ***************************************)
21 definition sreds: relation term ≝ star … sred.
23 interpretation "sequential computation"
24 'SeqRedStar M N = (sreds M N).
26 lemma sreds_refl: reflexive … sreds.
30 lemma sreds_step_sn: ∀M1,M. M1 ↦ M → ∀M2. M ↦* M2 → M1 ↦* M2.
34 lemma sreds_step_dx: ∀M1,M. M1 ↦* M → ∀M2. M ↦ M2 → M1 ↦* M2.
38 lemma sreds_step_rc: ∀M1,M2. M1 ↦ M2 → M1 ↦* M2.
42 lemma lsred_compatible_abst: compatible_abst sreds.
46 lemma sreds_compatible_sn: compatible_sn sreds.
50 lemma sreds_compatible_dx: compatible_dx sreds.
54 lemma sreds_compatible_appl: compatible_appl sreds.
58 lemma sreds_lift: liftable sreds.
62 lemma sreds_inv_lift: deliftable_sn sreds.
63 /3 width=3 by star_deliftable_sn, sred_inv_lift/
66 lemma sreds_dsubst: dsubstable_dx sreds.
70 theorem sreds_trans: transitive … sreds.
71 /2 width=3 by trans_star/
74 (* Note: the substitution should be unparentesized *)
75 lemma sreds_compatible_beta: ∀B1,B2. B1 ↦* B2 → ∀A1,A2. A1 ↦* A2 →
76 @B1.𝛌.A1 ↦* ([↙B2] A2).
77 #B1 #B2 #HB12 #A1 #A2 #HA12
78 @(sreds_trans … (@B2.𝛌.A1)) /2 width=1/ -B1
79 @(sreds_step_dx … (@B2.𝛌.A2)) // /3 width=1/
82 theorem sreds_preds: ∀M1,M2. M1 ↦* M2 → M1 ⤇* M2.
83 #M1 #M2 #H @(star_ind_l … M1 H) -M1 //
85 @(preds_step_sn … IHM2) -M2 /2 width=2/
88 lemma pred_sreds: ∀M1,M2. M1 ⤇ M2 → M1 ↦* M2.
89 #M1 #M2 #H elim H -M1 -M2 // /2 width=1/
92 theorem preds_sreds: ∀M1,M2. M1 ⤇* M2 → M1 ↦* M2.
93 #M1 #M2 #H elim H -M2 //
95 lapply (pred_sreds … HM2) -HM2 #HM2
96 @(sreds_trans … HM1 … HM2)
99 theorem sreds_conf: ∀M0,M1. M0 ↦* M1 → ∀M2. M0 ↦* M2 →
100 ∃∃M. M1 ↦* M & M2 ↦* M.
101 #M0 #M1 #HM01 #M2 #HM02
102 lapply (sreds_preds … HM01) #HM01
103 lapply (sreds_preds … HM02) #HM02
104 elim (preds_conf … HM01 … HM02) -M0 #M #HM1 #HM2
105 lapply (preds_sreds … HM1) -HM1
106 lapply (preds_sreds … HM2) -HM2 /2 width=3/