lemma tps_weak: ∀L,T1,T2,d1,e1. L ⊢ T1 [d1, e1] ≫ T2 →
∀d2,e2. d2 ≤ d1 → d1 + e1 ≤ d2 + e2 →
L ⊢ T1 [d2, e2] ≫ T2.
-#L #T1 #T #d1 #e1 #H elim H -L T1 T d1 e1
+#L #T1 #T2 #d1 #e1 #H elim H -H L T1 T2 d1 e1
[ //
| #L #K #V #W #i #d1 #e1 #Hid1 #Hide1 #HLK #HVW #d2 #e2 #Hd12 #Hde12
lapply (transitive_le … Hd12 … Hid1) -Hd12 Hid1 #Hid2
lemma tps_weak_top: ∀L,T1,T2,d,e.
L ⊢ T1 [d, e] ≫ T2 → L ⊢ T1 [d, |L| - d] ≫ T2.
-#L #T1 #T #d #e #H elim H -L T1 T d e
+#L #T1 #T2 #d #e #H elim H -H L T1 T2 d e
[ //
| #L #K #V #W #i #d #e #Hdi #_ #HLK #HVW
lapply (drop_fwd_drop2_length … HLK) #Hi
lemma tps_weak_all: ∀L,T1,T2,d,e.
L ⊢ T1 [d, e] ≫ T2 → L ⊢ T1 [0, |L|] ≫ T2.
-#L #T1 #T #d #e #HT12
+#L #T1 #T2 #d #e #HT12
lapply (tps_weak … HT12 0 (d + e) ? ?) -HT12 // #HT12
lapply (tps_weak_top … HT12) //
qed.
lemma tps_split_up: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → ∀i. d ≤ i → i ≤ d + e →
∃∃T. L ⊢ T1 [d, i - d] ≫ T & L ⊢ T [i, d + e - i] ≫ T2.
-#L #T1 #T2 #d #e #H elim H -L T1 T2 d e
+#L #T1 #T2 #d #e #H elim H -H L T1 T2 d e
[ /2/
| #L #K #V #W #i #d #e #Hdi #Hide #HLK #HVW #j #Hdj #Hjde
elim (lt_or_ge i j)
(* PARTIAL SUBSTITUTION ON TERMS ********************************************)
+(* Advanced inversion lemmas ************************************************)
+
+fact tps_inv_refl_SO2_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → e = 1 →
+ ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
+#L #T1 #T2 #d #e #H elim H -H L T1 T2 d e
+[ //
+| #L #K0 #V0 #W #i #d #e #Hdi #Hide #HLK0 #_ #H destruct -e;
+ >(le_to_le_to_eq … Hdi ?) /2/ -d #K #V #HLK
+ lapply (drop_mono … HLK0 … HLK) #H destruct
+| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H1 #K #V #HLK
+ >(IHV12 H1 … HLK) -IHV12 >(IHT12 H1 K V) -IHT12 /2/
+| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H1 #K #V #HLK
+ >(IHV12 H1 … HLK) -IHV12 >(IHT12 H1 … HLK) -IHT12 //
+]
+qed.
+
+lemma tps_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫ T2 →
+ ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
+/2 width=8/ qed.
+
(* Relocation properties ****************************************************)
(* Basic-1: was: subst1_lift_lt *)
lapply (tps_inv_lift1_eq … HU1 … HTU1) -HU1 #HU1 destruct -U1;
elim (tps_inv_lift1_ge … HU2 … HLK … HTU1 ?) -HU2 HLK HTU1 // <minus_plus_m_m /2/
qed.
-
-(* Advanced inversion lemmas ************************************************)
-
-fact tps_inv_refl_SO2_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → e = 1 →
- ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
-#L #T1 #T2 #d #e #H elim H -H L T1 T2 d e
-[ //
-| #L #K0 #V0 #W #i #d #e #Hdi #Hide #HLK0 #_ #H destruct -e;
- >(le_to_le_to_eq … Hdi ?) /2/ -d #K #V #HLK
- lapply (drop_mono … HLK0 … HLK) #H destruct
-| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H1 #K #V #HLK
- >(IHV12 H1 … HLK) -IHV12 >(IHT12 H1 K V) -IHT12 /2/
-| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H1 #K #V #HLK
- >(IHV12 H1 … HLK) -IHV12 >(IHT12 H1 … HLK) -IHT12 //
-]
-qed.
-
-lemma tps_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫ T2 →
- ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
-/2 width=8/ qed.
(* Basic properties *********************************************************)
+lemma tpss_ind: ∀d,e,L,T1. ∀R: term → Prop. R T1 →
+ (∀T,T2. L ⊢ T1 [d, e] ≫* T → L ⊢ T[d, e] ≫ T2 → R T → R T2) →
+ ∀T2. L ⊢ T1 [d, e] ≫* T2 → R T2.
+#d #e #L #T1 #R #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) //
+qed.
+
+lemma tpss_leq_repl_dx: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫* T2 →
+ ∀L2. L1 [d, e] ≈ L2 → L2 ⊢ T1 [d, e] ≫* T2.
+/3/ qed.
+
+lemma tpss_refl: ∀d,e,L,T. L ⊢ T [d, e] ≫* T.
+/2/ qed.
+
+lemma tpss_bind: ∀L,V1,V2,d,e. L ⊢ V1 [d, e] ≫* V2 →
+ ∀I,T1,T2. L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ≫* T2 →
+ L ⊢ 𝕓{I} V1. T1 [d, e] ≫* 𝕓{I} V2. T2.
+#L #V1 #V2 #d #e #HV12 elim HV12 -HV12 V2
+[ #V2 #HV12 #I #T1 #T2 #HT12 elim HT12 -HT12 T2
+ [ /3 width=5/
+ | #T #T2 #_ #HT2 #IHT @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
+ ]
+| #V #V2 #_ #HV12 #IHV #I #T1 #T2 #HT12
+ lapply (tpss_leq_repl_dx … HT12 (L. 𝕓{I} V) ?) -HT12 /2/ #HT12
+ lapply (IHV … HT12) -IHV HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
+]
+qed.
+
+lemma tpss_flat: ∀L,I,V1,V2,T1,T2,d,e.
+ L ⊢ V1 [d, e] ≫ * V2 → L ⊢ T1 [d, e] ≫* T2 →
+ L ⊢ 𝕗{I} V1. T1 [d, e] ≫* 𝕗{I} V2. T2.
+#L #I #V1 #V2 #T1 #T2 #d #e #HV12 elim HV12 -HV12 V2
+[ #V2 #HV12 #HT12 elim HT12 -HT12 T2
+ [ /3/
+ | #T #T2 #_ #HT2 #IHT @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
+ ]
+| #V #V2 #_ #HV12 #IHV #HT12
+ lapply (IHV … HT12) -IHV HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
+]
+qed.
+
+lemma tpss_weak: ∀L,T1,T2,d1,e1. L ⊢ T1 [d1, e1] ≫* T2 →
+ ∀d2,e2. d2 ≤ d1 → d1 + e1 ≤ d2 + e2 →
+ L ⊢ T1 [d2, e2] ≫* T2.
+#L #T1 #T2 #d1 #e1 #H #d1 #d2 #Hd21 #Hde12 @(tpss_ind … H) -H T2
+[ //
+| #T #T2 #_ #HT12 #IHT
+ lapply (tps_weak … HT12 … Hd21 Hde12) -HT12 Hd21 Hde12 /2/
+]
+qed.
+
+lemma tpss_weak_top: ∀L,T1,T2,d,e.
+ L ⊢ T1 [d, e] ≫* T2 → L ⊢ T1 [d, |L| - d] ≫* T2.
+#L #T1 #T2 #d #e #H @(tpss_ind … H) -H T2
+[ //
+| #T #T2 #_ #HT12 #IHT
+ lapply (tps_weak_top … HT12) -HT12 /2/
+]
+qed.
+
+lemma tpss_weak_all: ∀L,T1,T2,d,e.
+ L ⊢ T1 [d, e] ≫* T2 → L ⊢ T1 [0, |L|] ≫* T2.
+#L #T1 #T2 #d #e #HT12
+lapply (tpss_weak … HT12 0 (d + e) ? ?) -HT12 // #HT12
+lapply (tpss_weak_top … HT12) //
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+(* Note: this can be derived from tpss_inv_atom1 *)
+lemma tpss_inv_sort1: ∀L,T2,k,d,e. L ⊢ ⋆k [d, e] ≫* T2 → T2 = ⋆k.
+#L #T2 #k #d #e #H @(tpss_ind … H) -H T2
+[ //
+| #T #T2 #_ #HT2 #IHT destruct -T
+ >(tps_inv_sort1 … HT2) -HT2 //
+]
+qed.
+
+lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫* U2 →
+ ∃∃V2,T2. L ⊢ V1 [d, e] ≫* V2 &
+ L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ≫* T2 &
+ U2 = 𝕓{I} V2. T2.
+#d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -H U2
+[ /2 width=5/
+| #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct -U;
+ elim (tps_inv_bind1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H
+ lapply (tpss_leq_repl_dx … HT1 (L. 𝕓{I} V2) ?) -HT1 /3 width=5/
+]
+qed.
+
+lemma tpss_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕗{I} V1. T1 [d, e] ≫* U2 →
+ ∃∃V2,T2. L ⊢ V1 [d, e] ≫* V2 & L ⊢ T1 [d, e] ≫* T2 &
+ U2 = 𝕗{I} V2. T2.
+#d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -H U2
+[ /2 width=5/
+| #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct -U;
+ elim (tps_inv_flat1 … HU2) -HU2 /3 width=5/
+]
+qed.
+
+lemma tpss_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ≫* T2 → T1 = T2.
+#L #T1 #T2 #d #H @(tpss_ind … H) -H T2
+[ //
+| #T #T2 #_ #HT2 #IHT <(tps_inv_refl_O2 … HT2) -HT2 //
+]
+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/substitution/tps_lift.ma".
+include "Basic-2/unfold/tpss.ma".
+
+(* PARTIAL UNFOLD ON TERMS **************************************************)
+
+(* Advanced properties ******************************************************)
+
+lemma tpss_subst: ∀L,K,V,U1,i,d,e.
+ d ≤ i → i < d + e →
+ ↓[0, i] L ≡ K. 𝕓{Abbr} V → K ⊢ V [0, d + e - i - 1] ≫* U1 →
+ ∀U2. ↑[0, i + 1] U1 ≡ U2 → L ⊢ #i [d, e] ≫* U2.
+#L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(tpss_ind … H) -H U1
+[ /3/
+| #U #U1 #_ #HU1 #IHU #U2 #HU12
+ elim (lift_total U 0 (i+1)) #U0 #HU0
+ lapply (IHU … HU0) -IHU #H
+ lapply (drop_fwd_drop2 … HLK) -HLK #HLK
+ lapply (tps_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 HLK HU0 HU12 // normalize #HU02
+ lapply (tps_weak … HU02 d e ? ?) -HU02 [ >arith_i2 // | /2/ | /2/ ]
+]
+qed.
+
+(* Advanced inverion lemmas *************************************************)
+
+lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ 𝕒{I} [d, e] ≫* T2 →
+ T2 = 𝕒{I} ∨
+ ∃∃K,V1,V2,i. d ≤ i & i < d + e &
+ ↓[O, i] L ≡ K. 𝕓{Abbr} V1 &
+ K ⊢ V1 [0, d + e - i - 1] ≫* V2 &
+ ↑[O, i + 1] V2 ≡ T2 &
+ I = LRef i.
+#L #T2 #I #d #e #H @(tpss_ind … H) -H T2
+[ /2/
+| #T #T2 #_ #HT2 *
+ [ #H destruct -T;
+ elim (tps_inv_atom1 … HT2) -HT2 [ /2/ | * /3 width=10/ ]
+ | * #K #V1 #V #i #Hdi #Hide #HLK #HV1 #HVT #HI
+ lapply (drop_fwd_drop2 … HLK) #H
+ elim (tps_inv_lift1_up … HT2 … H … HVT ? ? ?) normalize -HT2 H HVT [2,3,4: /2/ ] #V2 <minus_plus #HV2 #HVT2
+ @or_intror @(ex6_4_intro … Hdi Hide HLK … HVT2 HI) /2/ (**) (* /4 width=10/ is too slow *)
+ ]
+]
+qed.
+
+lemma tpss_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ≫* T2 →
+ T2 = #i ∨
+ ∃∃K,V1,V2. d ≤ i & i < d + e &
+ ↓[O, i] L ≡ K. 𝕓{Abbr} V1 &
+ K ⊢ V1 [0, d + e - i - 1] ≫* V2 &
+ ↑[O, i + 1] V2 ≡ T2.
+#L #T2 #i #d #e #H
+elim (tpss_inv_atom1 … H) -H /2/
+* #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct -i /3 width=6/
+qed.
+
+lemma tpss_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫* T2 →
+ ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
+#L #T1 #T2 #d #H #K #V #HLK @(tpss_ind … H) -H T2 //
+#T #T2 #_ #HT2 #IHT <(tps_inv_refl_SO2 … HT2 … HLK) //
+qed.
+
+(* Relocation properties ****************************************************)
+
+lemma tpss_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 →
+ ∀L,U1,d,e. dt + et ≤ d → ↓[d, e] L ≡ K →
+ ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 →
+ L ⊢ U1 [dt, et] ≫* U2.
+#K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdetd #HLK #HTU1 @(tpss_ind … H) -H T2
+[ #U2 #H >(lift_mono … HTU1 … H) -H //
+| -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
+ elim (lift_total T d e) #U #HTU
+ lapply (IHT … HTU) -IHT #HU1
+ lapply (tps_lift_le … HT2 … HLK HTU HTU2 ?) -HT2 HLK HTU HTU2 /2/
+]
+qed.
+
+lemma tpss_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 →
+ ∀L,U1,d,e. d ≤ dt → ↓[d, e] L ≡ K →
+ ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 →
+ L ⊢ U1 [dt + e, et] ≫* U2.
+#K #T1 #T2 #dt #et #H #L #U1 #d #e #Hddt #HLK #HTU1 @(tpss_ind … H) -H T2
+[ #U2 #H >(lift_mono … HTU1 … H) -H //
+| -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
+ elim (lift_total T d e) #U #HTU
+ lapply (IHT … HTU) -IHT #HU1
+ lapply (tps_lift_ge … HT2 … HLK HTU HTU2 ?) -HT2 HLK HTU HTU2 /2/
+]
+qed.
+
+lemma tpss_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
+ ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 →
+ dt + et ≤ d →
+ ∃∃T2. K ⊢ T1 [dt, et] ≫* T2 & ↑[d, e] T2 ≡ U2.
+#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdetd @(tpss_ind … H) -H U2
+[ /2/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+ elim (tps_inv_lift1_le … HU2 … HLK … HTU ?) -HU2 HLK HTU /3/
+]
+qed.
+
+lemma tpss_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
+ ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 →
+ d + e ≤ dt →
+ ∃∃T2. K ⊢ T1 [dt - e, et] ≫* T2 & ↑[d, e] T2 ≡ U2.
+#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdedt @(tpss_ind … H) -H U2
+[ /2/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+ elim (tps_inv_lift1_ge … HU2 … HLK … HTU ?) -HU2 HLK HTU /3/
+]
+qed.
+
+lemma tpss_inv_lift1_eq: ∀L,U1,U2,d,e.
+ L ⊢ U1 [d, e] ≫* U2 → ∀T1. ↑[d, e] T1 ≡ U1 → U1 = U2.
+#L #U1 #U2 #d #e #H #T1 #HTU1 @(tpss_ind … H) -H U2 //
+#U #U2 #_ #HU2 #IHU destruct -U1
+<(tps_inv_lift1_eq … HU2 … HTU1) -HU2 HTU1 //
+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/substitution/tps_tps.ma".
+include "Basic-2/unfold/tpss_lift.ma".
+
+(* PARTIAL UNFOLD ON TERMS **************************************************)
+
+(* Advanced properties ******************************************************)
+
+lemma tpss_trans_down_strap1: ∀L,T1,T0,d1,e1. L ⊢ T1 [d1, e1] ≫* T0 →
+ ∀T2,d2,e2. L ⊢ T0 [d2, e2] ≫ T2 → d2 + e2 ≤ d1 →
+ ∃∃T. L ⊢ T1 [d2, e2] ≫ T & L ⊢ T [d1, e1] ≫* T2.
+/3/ qed.
+
+lemma tpss_split_up: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫* T2 →
+ ∀i. d ≤ i → i ≤ d + e →
+ ∃∃T. L ⊢ T1 [d, i - d] ≫* T & L ⊢ T [i, d + e - i] ≫* T2.
+#L #T1 #T2 #d #e #H #i #Hdi #Hide @(tpss_ind … H) -H T2
+[ /2/
+| #T #T2 #_ #HT12 * #T3 #HT13 #HT3
+ elim (tps_split_up … HT12 … Hdi Hide) -HT12 Hide #T0 #HT0 #HT02
+ elim (tpss_trans_down_strap1 … HT3 … HT0 ?) -T [2: <plus_minus_m_m_comm // ]
+ /3 width=7 by ex2_1_intro, step/ (**) (* just /3 width=7/ is too slow *)
+]
+qed.
+
+lemma tpss_inv_lift1_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
+ ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 →
+ d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
+ ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ≫* T2 & ↑[d, e] T2 ≡ U2.
+#L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
+elim (tpss_split_up … HU12 (d + e) ? ?) -HU12 // -Hdedet #U #HU1 #HU2
+lapply (tpss_weak … HU1 d e ? ?) -HU1 // <plus_minus_m_m_comm // -Hddt Hdtde #HU1
+lapply (tpss_inv_lift1_eq … HU1 … HTU1) -HU1 #HU1 destruct -U1;
+elim (tpss_inv_lift1_ge … HU2 … HLK … HTU1 ?) -HU2 HLK HTU1 // <minus_plus_m_m /2/
+qed.
+
+(* Main properties **********************************************************)
+
+theorem tpss_conf_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 [d1, e1] ≫* T1 →
+ ∀T2,d2,e2. L ⊢ T0 [d2, e2] ≫* T2 →
+ ∃∃T. L ⊢ T1 [d2, e2] ≫* T & L ⊢ T2 [d1, e1] ≫* T.
+/3/ qed.
+
+theorem tpss_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 [d1, e1] ≫* T1 →
+ ∀L2,T2,d2,e2. L2 ⊢ T0 [d2, e2] ≫* T2 →
+ (d1 + e1 ≤ d2 ∨ d2 + e2 ≤ d1) →
+ ∃∃T. L2 ⊢ T1 [d2, e2] ≫* T & L1 ⊢ T2 [d1, e1] ≫* T.
+/3/ qed.
+
+theorem tpss_trans_eq: ∀L,T1,T,T2,d,e.
+ L ⊢ T1 [d, e] ≫* T → L ⊢ T [d, e] ≫* T2 →
+ L ⊢ T1 [d, e] ≫* T2.
+/2/ qed.
+
+theorem tpss_trans_down: ∀L,T1,T0,d1,e1. L ⊢ T1 [d1, e1] ≫* T0 →
+ ∀T2,d2,e2. L ⊢ T0 [d2, e2] ≫* T2 → d2 + e2 ≤ d1 →
+ ∃∃T. L ⊢ T1 [d2, e2] ≫* T & L ⊢ T [d1, e1] ≫* T2.
+/3/ qed.
(* PROPERTIES of RELATIONS **************************************************)
-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.
-
-lemma TC_strip: ∀A,R. confluent A R →
- ∀a0,a1. TC … R a0 a1 → ∀a2. R a0 a2 →
- ∃∃a. R a1 a & TC … R a2 a.
-#A #R #HR #a0 #a1 #H elim H -H a1
+definition confluent: ∀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.
+
+definition transitive: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
+ ∀a1,a0. R1 a1 a0 → ∀a2. R2 a0 a2 →
+ ∃∃a. R2 a1 a & R1 a a2.
+
+lemma TC_strip1: ∀A,R1,R2. confluent A R1 R2 →
+ ∀a0,a1. TC … R1 a0 a1 → ∀a2. R2 a0 a2 →
+ ∃∃a. R2 a1 a & TC … R1 a2 a.
+#A #R1 #R2 #HR12 #a0 #a1 #H elim H -H a1
[ #a1 #Ha01 #a2 #Ha02
- elim (HR … Ha01 … Ha02) -HR a0 /3/
+ elim (HR12 … Ha01 … Ha02) -HR12 a0 /3/
| #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
elim (IHa0 … Ha02) -IHa0 Ha02 a0 #a0 #Ha0 #Ha20
- elim (HR … Ha1 … Ha0) -HR a /4/
+ elim (HR12 … Ha1 … Ha0) -HR12 a /4/
+]
+qed.
+
+lemma TC_strip2: ∀A,R1,R2. confluent A R1 R2 →
+ ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a0 a1 →
+ ∃∃a. R1 a2 a & TC … R2 a1 a.
+#A #R1 #R2 #HR12 #a0 #a2 #H elim H -H a2
+[ #a2 #Ha02 #a1 #Ha01
+ elim (HR12 … Ha01 … Ha02) -HR12 a0 /3/
+| #a #a2 #_ #Ha2 #IHa0 #a1 #Ha01
+ elim (IHa0 … Ha01) -IHa0 Ha01 a0 #a0 #Ha0 #Ha21
+ elim (HR12 … Ha0 … Ha2) -HR12 a /4/
]
qed.
-lemma TC_confluent: ∀A,R. confluent A R → confluent A (TC … R).
-#A #R #HR #a0 #a1 #H elim H -H a1
+lemma TC_confluent: ∀A,R1,R2.
+ confluent A R1 R2 → confluent A (TC … R1) (TC … R2).
+#A #R1 #R2 #HR12 #a0 #a1 #H elim H -H a1
[ #a1 #Ha01 #a2 #Ha02
- elim (TC_strip … HR … Ha02 … Ha01) -HR a0 /3/
+ elim (TC_strip2 … HR12 … Ha02 … Ha01) -HR12 a0 /3/
| #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
elim (IHa0 … Ha02) -IHa0 Ha02 a0 #a0 #Ha0 #Ha20
- elim (TC_strip … HR … Ha0 … Ha1) -HR a /4/
+ elim (TC_strip2 … HR12 … Ha0 … Ha1) -HR12 a /4/
+]
+qed.
+
+lemma TC_strap1: ∀A,R1,R2. transitive A R1 R2 →
+ ∀a1,a0. TC … R1 a1 a0 → ∀a2. R2 a0 a2 →
+ ∃∃a. R2 a1 a & TC … R1 a a2.
+#A #R1 #R2 #HR12 #a1 #a0 #H elim H -H a0
+[ #a0 #Ha10 #a2 #Ha02
+ elim (HR12 … Ha10 … Ha02) -HR12 a0 /3/
+| #a #a0 #_ #Ha0 #IHa #a2 #Ha02
+ elim (HR12 … Ha0 … Ha02) -HR12 a0 #a0 #Ha0 #Ha02
+ elim (IHa … Ha0) -a /4/
+]
+qed.
+
+lemma TC_strap2: ∀A,R1,R2. transitive A R1 R2 →
+ ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a1 a0 →
+ ∃∃a. R1 a a2 & TC … R2 a1 a.
+#A #R1 #R2 #HR12 #a0 #a2 #H elim H -H a2
+[ #a2 #Ha02 #a1 #Ha10
+ elim (HR12 … Ha10 … Ha02) -HR12 a0 /3/
+| #a #a2 #_ #Ha02 #IHa #a1 #Ha10
+ elim (IHa … Ha10) -a0 #a0 #Ha0 #Ha10
+ elim (HR12 … Ha0 … Ha02) -HR12 a /4/
+]
+qed.
+
+lemma TC_transitive: ∀A,R1,R2.
+ transitive A R1 R2 → transitive A (TC … R1) (TC … R2).
+#A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0
+[ #a0 #Ha10 #a2 #Ha02
+ elim (TC_strap2 … HR12 … Ha02 … Ha10) -HR12 a0 /3/
+| #a #a0 #_ #Ha0 #IHa #a2 #Ha02
+ elim (TC_strap2 … HR12 … Ha02 … Ha0) -HR12 a0 #a0 #Ha02 #Ha0
+ elim (IHa … Ha0) -a /4/
]
qed.
lemma TC_reflexive: ∀A,R. reflexive A R → reflexive A (TC … R).
/2/ qed.
+lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:A→Prop.
+ P a1 → (∀a,a2. TC … R a1 a → R a a2 → P a → P a2) →
+ ∀a2. TC … R a1 a2 → P a2.
+#A #R #H #a1 #P #Ha1 #IHa1 #a2 #Ha12 elim Ha12 -Ha12 a2 /3/
+qed.
<key name="ex">4 4</key>
<key name="ex">5 3</key>
<key name="ex">5 4</key>
+ <key name="ex">6 4</key>
<key name="ex">6 6</key>
<key name="ex">7 6</key>
<key name="or">3</key>
interpretation "multiple existental quantifier (5, 4)" 'Ex P0 P1 P2 P3 P4 = (ex5_4 ? ? ? ? P0 P1 P2 P3 P4).
+(* multiple existental quantifier (6, 4) *)
+
+inductive ex6_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→Prop) : Prop ≝
+ | ex6_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → ex6_4 ? ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (6, 4)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_4 ? ? ? ? P0 P1 P2 P3 P4 P5).
+
(* multiple existental quantifier (6, 6) *)
inductive ex6_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝
non associative with precedence 20
for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) }.
+(* multiple existental quantifier (6, 4) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P5) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) }.
+
(* multiple existental quantifier (6, 6) *)
notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)"
--- /dev/null
+#!/bin/sh
+for V in `cat Make`; do
+ echo ${V}; sed "s/$1/$2/g" ${V} > ${V}.new
+ if diff ${V} ${V}.new > /dev/null;
+ then rm -f ${V}.new; else mv -f ${V}.new ${V}; fi
+done
+
+unset V
projects / helm.git / commitdiff