pr0/dec nf0_dec
pr0/subst1 pr0_subst1_back
pr0/subst1 pr0_subst1_fwd
-pr1/pr1 pr1_strip
-pr1/pr1 pr1_confluence
-pr1/props pr1_pr0
-pr1/props pr1_t
-pr1/props pr1_head_1
-pr1/props pr1_head_2
-pr1/props pr1_comp
+
pr1/props pr1_eta
+
pr2/fwd pr2_gen_void
pr3/fwd pr3_gen_void
-pr3/pr1 pr3_pr1
pr3/props pr3_eta
sn3/props sns3_lifts
sty1/cnt sty1_cnt
(**************************************************************************)
include "basic_2/reducibility/cnf.ma".
+include "basic_2/computation/tprs.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
@(cprs_strap1 … IHT2) -IHT2 /2 width=1/
qed.
+(* Basic_1: was: pr3_pr1 *)
+lemma tprs_cprs: ∀T1,T2. T1 ➡* T2 → ∀L. L ⊢ T1 ➡* T2.
+#T1 #T2 #H @(tprs_ind … H) -T2 /2 width=1/ /3 width=3/
+qed.
+
(* Basic inversion lemmas ***************************************************)
(* Basic_1: was: pr3_gen_sort *)
lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/
qed-.
+lemma tprs_inv_cnf1: ∀T,U. T ➡* U → ⋆ ⊢ 𝐍⦃T⦄ → T = U.
+/3 width=3 by tprs_cprs, cprs_inv_cnf1/ qed-.
+
(* Basic_1: removed theorems 10:
clear_pr3_trans pr3_cflat pr3_gen_bind
pr3_head_1 pr3_head_2 pr3_head_21 pr3_head_12
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/reducibility/ltpr.ma".
+include "basic_2/computation/tprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************)
+
+definition ltprs: relation lenv ≝ TC … ltpr.
+
+interpretation
+ "context-free parallel computation (environment)"
+ 'PRedStar L1 L2 = (ltprs L1 L2).
+
+(* Basic eliminators ********************************************************)
+
+lemma ltprs_ind: ∀L1. ∀R:predicate lenv. R L1 →
+ (∀L,L2. L1 ➡* L → L ➡ L2 → R L → R L2) →
+ ∀L2. L1 ➡* L2 → R L2.
+#L1 #R #HL1 #IHL1 #L2 #HL12
+@(TC_star_ind … HL1 IHL1 … HL12) //
+qed-.
+
+lemma ltprs_ind_dx: ∀L2. ∀R:predicate lenv. R L2 →
+ (∀L1,L. L1 ➡ L → L ➡* L2 → R L → R L1) →
+ ∀L1. L1 ➡* L2 → R L1.
+#L2 #R #HL2 #IHL2 #L1 #HL12
+@(TC_star_ind_dx … HL2 IHL2 … HL12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma ltprs_refl: reflexive … ltprs.
+/2 width=1/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ltprs_inv_atom1: ∀L2. ⋆ ➡* L2 → L2 = ⋆.
+#L2 #H @(ltprs_ind … H) -L2 //
+#L #L2 #_ #HL2 #IHL1 destruct
+>(ltpr_inv_atom1 … HL2) -L2 //
+qed-.
+
+lemma ltprs_inv_pair1: ∀I,K1,L2,V1. K1. ⓑ{I} V1 ➡* L2 →
+ ∃∃K2,V2. K1 ➡* K2 & V1 ➡* V2 & L2 = K2. ⓑ{I} V2.
+#I #K1 #L2 #V1 #H @(ltprs_ind … H) -L2 /2 width=5/
+#L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct
+elim (ltpr_inv_pair1 … HL2) -HL2 #K2 #V2 #HK2 #HV2 #H destruct /3 width=5/
+qed-.
+
+lemma ltprs_inv_atom2: ∀L1. L1 ➡* ⋆ → L1 = ⋆.
+#L1 #H @(ltprs_ind_dx … H) -L1 //
+#L1 #L #HL1 #_ #IHL2 destruct
+>(ltpr_inv_atom2 … HL1) -L1 //
+qed-.
+
+lemma ltprs_inv_pair2: ∀I,L1,K2,V2. L1 ➡* K2. ⓑ{I} V2 →
+ ∃∃K1,V1. K1 ➡* K2 & V1 ➡* V2 & L1 = K1. ⓑ{I} V1.
+#I #L1 #K2 #V2 #H @(ltprs_ind_dx … H) -L1 /2 width=5/
+#L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct
+elim (ltpr_inv_pair2 … HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct /3 width=5/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma ltprs_fwd_length: ∀L1,L2. L1 ➡* L2 → |L1| = |L2|.
+#L1 #L2 #H @(ltprs_ind … H) -L2 //
+#L #L2 #_ #HL2 #IHL1
+>IHL1 -L1 >(ltpr_fwd_length … HL2) -HL2 //
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/ltprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************)
+
+(* alternative definition of ltprs *)
+definition ltprsa: relation lenv ≝ lpx tprs.
+
+interpretation
+ "context-free parallel computation (environment) alternative"
+ 'PRedStarAlt L1 L2 = (ltprsa L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma ltprs_ltprsa: ∀L1,L2. L1 ➡* L2 → L1 ➡➡* L2.
+/2 width=1/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ltprsa_ltprs: ∀L1,L2. L1 ➡➡* L2 → L1 ➡* L2.
+/2 width=1/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/reducibility/ltpr_ldrop.ma".
+include "basic_2/computation/ltprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************)
+
+lemma ltprs_ldrop_conf: dropable_sn ltprs.
+/2 width=3/ qed.
+
+lemma ldrop_ltprs_trans: dedropable_sn ltprs.
+/2 width=3/ qed.
+
+lemma ltprs_ldrop_trans_O1: dropable_dx ltprs.
+/2 width=3/ qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/reducibility/ltpr_ltpr.ma".
+include "basic_2/computation/ltprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************)
+
+(* Advanced properties ******************************************************)
+
+lemma ltprs_strip: ∀L1. ∀L:term. L ➡* L1 → ∀L2. L ➡ L2 →
+ ∃∃L0. L1 ➡ L0 & L2 ➡* L0.
+/3 width=3/ qed.
+
+(* Main properties **********************************************************)
+
+theorem ltprs_conf: Confluent … ltprs.
+/3 width=3/ qed.
+
+theorem ltprs_trans: Transitive … ltprs.
+/2 width=3/ qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/reducibility/tpr.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************)
+
+(* Basic_1: includes: pr1_pr0 *)
+definition tprs: relation term ≝ TC … tpr.
+
+interpretation "context-free parallel computation (term)"
+ 'PRedStar T1 T2 = (tprs T1 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma tprs_ind: ∀T1. ∀R:predicate term. R T1 →
+ (∀T,T2. T1 ➡* T → T ➡ T2 → R T → R T2) →
+ ∀T2. T1 ➡* T2 → R T2.
+#T1 #R #HT1 #IHT1 #T2 #HT12
+@(TC_star_ind … HT1 IHT1 … HT12) //
+qed-.
+
+lemma tprs_ind_dx: ∀T2. ∀R:predicate term. R T2 →
+ (∀T1,T. T1 ➡ T → T ➡* T2 → R T → R T1) →
+ ∀T1. T1 ➡* T2 → R T1.
+#T2 #R #HT2 #IHT2 #T1 #HT12
+@(TC_star_ind_dx … HT2 IHT2 … HT12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma tprs_refl: reflexive … tprs.
+/2 width=1/ qed.
+
+lemma tprs_strap1: ∀T1,T,T2. T1 ➡* T → T ➡ T2 → T1 ➡* T2.
+/2 width=3/ qed.
+
+lemma tprs_strap2: ∀T1,T,T2. T1 ➡ T → T ➡* T2 → T1 ➡* T2.
+/2 width=3/ qed.
+
+(* Basic_1: was only: pr1_head_1 *)
+lemma tprs_pair_sn: ∀I,T1,T2. T1 ➡ T2 → ∀V1,V2. V1 ➡* V2 →
+ ②{I} V1. T1 ➡* ②{I} V2. T2.
+* [ #a ] #I #T1 #T2 #HT12 #V1 #V2 #H @(tprs_ind … H) -V2
+[1,3: /3 width=1/
+|2,4: #V #V2 #_ #HV2 #IHV1
+ @(tprs_strap1 … IHV1) -IHV1 /2 width=1/
+]
+qed.
+
+(* Basic_1: was only: pr1_head_2 *)
+lemma tprs_pair_dx: ∀I,V1,V2. V1 ➡ V2 → ∀T1,T2. T1 ➡* T2 →
+ ②{I} V1. T1 ➡* ②{I} V2. T2.
+* [ #a ] #I #V1 #V2 #HV12 #T1 #T2 #H @(tprs_ind … H) -T2
+[1,3: /3 width=1/
+|2,4: #T #T2 #_ #HT2 #IHT1
+ @(tprs_strap1 … IHT1) -IHT1 /2 width=1/
+]
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma tprs_inv_atom1: ∀U2,k. ⋆k ➡* U2 → U2 = ⋆k.
+#U2 #k #H @(tprs_ind … H) -U2 //
+#U #U2 #_ #HU2 #IHU1 destruct
+>(tpr_inv_atom1 … HU2) -HU2 //
+qed-.
+
+lemma tprs_inv_cast1: ∀W1,T1,U2. ⓝW1.T1 ➡* U2 → T1 ➡* U2 ∨
+ ∃∃W2,T2. W1 ➡* W2 & T1 ➡* T2 & U2 = ⓝW2.T2.
+#W1 #T1 #U2 #H @(tprs_ind … H) -U2 /3 width=5/
+#U #U2 #_ #HU2 * /3 width=3/ *
+#W #T #HW1 #HT1 #H destruct
+elim (tpr_inv_cast1 … HU2) -HU2 /3 width=3/ *
+#W2 #T2 #HW2 #HT2 #H destruct /4 width=5/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/reducibility/tpr_lift.ma".
+include "basic_2/computation/tprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma tprs_inv_abst1: ∀a,V1,T1,U2. ⓛ{a}V1. T1 ➡* U2 →
+ ∃∃V2,T2. V1 ➡* V2 & T1 ➡* T2 & U2 = ⓛ{a}V2. T2.
+#a #V1 #T1 #U2 #H @(tprs_ind … H) -U2 /2 width=5/
+#U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
+elim (tpr_inv_abst1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/
+qed-.
+
+lemma tprs_inv_abst: ∀a,V1,V2,T1,T2. ⓛ{a}V1. T1 ➡* ⓛ{a}V2. T2 →
+ V1 ➡* V2 ∧ T1 ➡* T2.
+#a #V1 #V2 #T1 #T2 #H
+elim (tprs_inv_abst1 … H) -H #V #T #HV1 #HT1 #H destruct /2 width=1/
+qed-.
+
+(* Relocation properties ****************************************************)
+
+(* Note: this was missing in basic_1 *)
+lemma tprs_lift: t_liftable tprs.
+/3 width=7/ qed.
+
+(* Note: this was missing in basic_1 *)
+lemma tprs_inv_lift1: t_deliftable_sn tprs.
+/3 width=3 by tpr_inv_lift1, t_deliftable_sn_TC/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/reducibility/tpr_tpr.ma".
+include "basic_2/computation/tprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_1: was: pr1_strip *)
+lemma tprs_strip: ∀T1,T. T ➡* T1 → ∀T2. T ➡ T2 →
+ ∃∃T0. T1 ➡ T0 & T2 ➡* T0.
+/3 width=3/ qed.
+
+(* Main propertis ***********************************************************)
+
+(* Basic_1: was: pr1_confluence *)
+theorem tprs_conf: Confluent … tprs.
+/3 width=3/ qed.
+
+(* Basic_1: was: pr1_t *)
+theorem tprs_trans: Transitive … tprs.
+/2 width=3/ qed.
+
+(* Basic_1: was: pr1_comp *)
+lemma tprs_pair: ∀I,V1,V2. V1 ➡* V2 → ∀T1,T2. T1 ➡* T2 →
+ ②{I} V1. T1 ➡* ②{I} V2. T2.
+#I #V1 #V2 #H @(tprs_ind … H) -V2 /2 width=1/
+#V #V2 #_ #HV2 #IHV1 #T1 #T2 #HT12
+@(tprs_trans … (②{I}V.T2)) /2 width=1/
+qed.
inductive lpx (R:relation term): relation lenv ≝
| lpx_stom: lpx R (⋆) (⋆)
-| lpx_pair: ∀K1,K2,I,V1,V2.
+| lpx_pair: ∀I,K1,K2,V1,V2.
lpx R K1 K2 → R V1 V2 → lpx R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2)
.
-(* Basic properties *********************************************************)
-
-lemma lpx_refl: ∀R. reflexive ? R → reflexive … (lpx R).
-#R #HR #L elim L -L // /2 width=1/
-qed.
-
(* Basic inversion lemmas ***************************************************)
fact lpx_inv_atom1_aux: ∀R,L1,L2. lpx R L1 L2 → L1 = ⋆ → L2 = ⋆.
#R #L1 #L2 * -L1 -L2
[ //
-| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct
+| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
]
qed-.
lemma lpx_inv_atom1: ∀R,L2. lpx R (⋆) L2 → L2 = ⋆.
/2 width=4 by lpx_inv_atom1_aux/ qed-.
-fact lpx_inv_pair1_aux: ∀R,L1,L2. lpx R L1 L2 → ∀K1,I,V1. L1 = K1. ⓑ{I} V1 →
+fact lpx_inv_pair1_aux: ∀R,L1,L2. lpx R L1 L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
∃∃K2,V2. lpx R K1 K2 & R V1 V2 & L2 = K2. ⓑ{I} V2.
#R #L1 #L2 * -L1 -L2
-[ #K1 #I #V1 #H destruct
-| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct /2 width=5/
+[ #J #K1 #V1 #H destruct
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5/
]
qed-.
-lemma lpx_inv_pair1: ∀R,K1,I,V1,L2. lpx R (K1. ⓑ{I} V1) L2 →
+lemma lpx_inv_pair1: ∀R,I,K1,V1,L2. lpx R (K1. ⓑ{I} V1) L2 →
∃∃K2,V2. lpx R K1 K2 & R V1 V2 & L2 = K2. ⓑ{I} V2.
/2 width=3 by lpx_inv_pair1_aux/ qed-.
fact lpx_inv_atom2_aux: ∀R,L1,L2. lpx R L1 L2 → L2 = ⋆ → L1 = ⋆.
#R #L1 #L2 * -L1 -L2
[ //
-| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct
+| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
]
qed-.
lemma lpx_inv_atom2: ∀R,L1. lpx R L1 (⋆) → L1 = ⋆.
/2 width=4 by lpx_inv_atom2_aux/ qed-.
-fact lpx_inv_pair2_aux: ∀R,L1,L2. lpx R L1 L2 → ∀K2,I,V2. L2 = K2. ⓑ{I} V2 →
+fact lpx_inv_pair2_aux: ∀R,L1,L2. lpx R L1 L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
∃∃K1,V1. lpx R K1 K2 & R V1 V2 & L1 = K1. ⓑ{I} V1.
#R #L1 #L2 * -L1 -L2
-[ #K2 #I #V2 #H destruct
-| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #K #J #W #H destruct /2 width=5/
+[ #J #K2 #V2 #H destruct
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5/
]
qed-.
-lemma lpx_inv_pair2: ∀R,L1,K2,I,V2. lpx R L1 (K2. ⓑ{I} V2) →
+lemma lpx_inv_pair2: ∀R,I,L1,K2,V2. lpx R L1 (K2. ⓑ{I} V2) →
∃∃K1,V1. lpx R K1 K2 & R V1 V2 & L1 = K1. ⓑ{I} V1.
/2 width=3 by lpx_inv_pair2_aux/ qed-.
lemma lpx_fwd_length: ∀R,L1,L2. lpx R L1 L2 → |L1| = |L2|.
#R #L1 #L2 #H elim H -L1 -L2 normalize //
qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lpx_refl: ∀R. reflexive ? R → reflexive … (lpx R).
+#R #HR #L elim L -L // /2 width=1/
+qed.
+
+lemma lpx_trans: ∀R. Transitive ? R → Transitive … (lpx R).
+#R #HR #L1 #L #H elim H -L //
+#I #K1 #K #V1 #V #_ #HV1 #IHK1 #X #H
+elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK2 #HV2 #H destruct /3 width=3/
+qed.
+
+lemma lpx_conf: ∀R. Confluent ? R → Confluent … (lpx R).
+#R #HR #L0 #L1 #H elim H -L1
+[ #X #H >(lpx_inv_atom1 … H) -X /2 width=3/
+| #I #K0 #K1 #V0 #V1 #_ #HV01 #IHK01 #X #H
+ elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK02 #HV02 #H destruct
+ elim (IHK01 … HK02) -K0 #K #HK1 #HK2
+ elim (HR … HV01 … HV02) -HR -V0 /3 width=5/
+]
+qed.
+
+lemma lpx_TC_inj: ∀R,L1,L2. lpx R L1 L2 → lpx (TC … R) L1 L2.
+#R #L1 #L2 #H elim H -L1 -L2 // /3 width=1/
+qed.
+
+lemma lpx_TC_step: ∀R,L1,L. lpx (TC … R) L1 L →
+ ∀L2. lpx R L L2 → lpx (TC … R) L1 L2.
+#R #L1 #L #H elim H -L /2 width=1/
+#I #K1 #K #V1 #V #_ #HV1 #IHK1 #X #H
+elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK2 #HV2 #H destruct /3 width=3/
+qed.
+
+lemma TC_lpx_pair_dx: ∀R. reflexive ? R →
+ ∀I,K,V1,V2. TC … R V1 V2 →
+ TC … (lpx R) (K.ⓑ{I}V1) (K.ⓑ{I}V2).
+#R #HR #I #K #V1 #V2 #H elim H -V2
+/4 width=5 by lpx_refl, lpx_pair, inj, step/ (**) (* too slow without trace *)
+qed.
+
+lemma TC_lpx_pair_sn: ∀R. reflexive ? R →
+ ∀I,V,K1,K2. TC … (lpx R) K1 K2 →
+ TC … (lpx R) (K1.ⓑ{I}V) (K2.ⓑ{I}V).
+#R #HR #I #V #K1 #K2 #H elim H -K2
+/4 width=5 by lpx_refl, lpx_pair, inj, step/ (**) (* too slow without trace *)
+qed.
+
+lemma lpx_TC: ∀R,L1,L2. TC … (lpx R) L1 L2 → lpx (TC … R) L1 L2.
+#R #L1 #L2 #H elim H -L2 /2 width=1/ /2 width=3/
+qed.
+
+lemma lpx_inv_TC: ∀R. reflexive ? R →
+ ∀L1,L2. lpx (TC … R) L1 L2 → TC … (lpx R) L1 L2.
+#R #HR #L1 #L2 #H elim H -L1 -L2 /2 width=1/ /3 width=3/
+qed.
non associative with precedence 45
for @{ 'PRedStar $L $T1 $T2 }.
+notation "hvbox( T1 ➡➡* break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PRedStarAlt $T1 $T2 }.
+
notation "hvbox( L1 ⊢ ➡* break term 46 L2 )"
non associative with precedence 45
for @{ 'CPRedStar $L1 $L2 }.
theorem ltpr_conf: ∀L0:lenv. ∀L1. L0 ➡ L1 → ∀L2. L0 ➡ L2 →
∃∃L. L1 ➡ L & L2 ➡ L.
#L0 #L1 #H elim H -L0 -L1 /2 width=3/
-#K0 #K1 #I #V0 #V1 #_ #HV01 #IHK01 #L2 #H
+#I #K0 #K1 #V0 #V1 #_ #HV01 #IHK01 #L2 #H
elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK02 #HV02 #H destruct
elim (IHK01 … HK02) -K0 #K #HK1 #HK2
elim (tpr_conf … HV01 HV02) -V0 /3 width=5/
]
qed.
+lemma dropable_sn_TC: ∀R. dropable_sn R → dropable_sn (TC … R).
+#R #HR #L1 #K1 #d #e #HLK1 #L2 #H elim H -L2
+[ #L2 #HL12
+ elim (HR … HLK1 … HL12) -HR -L1 /3 width=3/
+| #L #L2 #_ #HL2 * #K #HK1 #HLK
+ elim (HR … HLK … HL2) -HR -L /3 width=3/
+]
+qed.
+
+lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (TC … R).
+#R #HR #L1 #K1 #d #e #HLK1 #K2 #H elim H -K2
+[ #K2 #HK12
+ elim (HR … HLK1 … HK12) -HR -K1 /3 width=3/
+| #K #K2 #_ #HK2 * #L #HL1 #HLK
+ elim (HR … HLK … HK2) -HR -K /3 width=3/
+]
+qed.
+
+lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (TC … R).
+#R #HR #L1 #L2 #H elim H -L2
+[ #L2 #HL12 #K2 #e #HLK2
+ elim (HR … HL12 … HLK2) -HR -L2 /3 width=3/
+| #L #L2 #_ #HL2 #IHL1 #K2 #e #HLK2
+ elim (HR … HL2 … HLK2) -HR -L2 #K #HLK #HK2
+ elim (IHL1 … HLK) -L /3 width=5/
+]
+qed.
+
(* Basic forvard lemmas *****************************************************)
(* Basic_1: was: drop_S *)
definition Decidable: Prop → Prop ≝ λR. R ∨ (R → ⊥).
+definition Confluent: ∀A. ∀R: relation A. Prop ≝ λA,R.
+ ∀a0,a1. R a0 a1 → ∀a2. R a0 a2 →
+ ∃∃a. R a1 a & R a2 a.
+
+definition Transitive: ∀A. ∀R: relation A. Prop ≝ λA,R.
+ ∀a1,a0. R a1 a0 → ∀a2. R a0 a2 → R a1 a2.
+
definition confluent2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
∀a0,a1. R1 a0 a1 → ∀a2. R2 a0 a2 →
∃∃a. R2 a1 a & R1 a2 a.
projects / helm.git / commitdiff