lemma ltpss_strap: ∀L1,L,L2,d,e.
L1 [d, e] ≫ L → L [d, e] ≫* L2 → L1 [d, e] ≫* L2.
-/2/ qed.
+/2 width=3/ qed.
lemma ltpss_refl: ∀L,d,e. L [d, e] ≫* L.
-/2/ qed.
+/2 width=1/ qed.
(* Basic inversion lemmas ***************************************************)
lemma ltpss_inv_atom1: ∀d,e,L2. ⋆ [d, e] ≫* L2 → L2 = ⋆.
#d #e #L2 #H @(ltpss_ind … H) -L2 //
-#L #L2 #_ #HL2 #IHL destruct -L
+#L #L2 #_ #HL2 #IHL destruct
>(ltps_inv_atom1 … HL2) -HL2 //
qed-.
-fact ltpss_inv_atom2_aux: ∀d,e,L1,L2.
- L1 [d, e] ≫* L2 → L2 = ⋆ → L1 = ⋆.
+fact ltpss_inv_atom2_aux: ∀d,e,L1,L2. L1 [d, e] ≫* L2 → L2 = ⋆ → L1 = ⋆.
#d #e #L1 #L2 #H @(ltpss_ind … H) -L2 //
-#L2 #L #_ #HL2 #IHL2 #H destruct -L;
-lapply (ltps_inv_atom2 … HL2) -HL2 /2/
+#L2 #L #_ #HL2 #IHL2 #H destruct
+lapply (ltps_inv_atom2 … HL2) -HL2 /2 width=1/
qed.
lemma ltpss_inv_atom2: ∀d,e,L1. L1 [d, e] ≫* ⋆ → L1 = ⋆.
#d #e #L1 #L2 * -d e L1 L2
[ #d #e #_ #_ #K1 #I #V1 #H destruct
| #L1 #I #V #_ #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K2 #J #W2 #H destruct -L2 I V2 /2 width=5/
+| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K2 #J #W2 #H destruct /2 width=5/
| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H)
]
qed.
[ #d #e #_ #I #K2 #V2 #H destruct
| #L #I #V #H elim (lt_refl_false … H)
| #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K2 #W2 #H destruct -L2 I V2
- /2 width=5/
+| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K2 #W2 #H destruct /2 width=5/
]
qed.
∃∃K1,V1. K1 [d - 1, e] ≫ K2 &
K2 ⊢ V1 [d - 1, e] ≫ V2 &
L1 = K1. 𝕓{I} V1.
-/2/ qed.
+/2 width=1/ qed.
*)
lemma ltpss_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 →
∀L2,e2. ↓[0, e2] L0 ≡ L2 →
d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2.
-#L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1 /3 width=6/
+#L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1 // /3 width=6/
qed.
lemma ltpss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
∀L2,e2. ↓[0, e2] L0 ≡ L2 →
d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2.
-#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 /3 width=6/
+#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 // /3 width=6/
qed.
lemma ltpss_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 →
∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
∃∃L. L2 [0, d1 + e1 - e2] ≫* L & ↓[0, e2] L1 ≡ L.
#L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1
-[ /2/
+[ /2 width=3/
| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
elim (IHL … HL02 Hd1e2 He2de1) -L0 #L0 #HL20 #HL0
- elim (ltps_ldrop_conf_be … HL1 … HL0 Hd1e2 He2de1) -L /3/
+ elim (ltps_ldrop_conf_be … HL1 … HL0 Hd1e2 He2de1) -L /3 width=3/
]
qed.
∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
∃∃L. L [0, d1 + e1 - e2] ≫* L2 & ↓[0, e2] L1 ≡ L.
#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0
-[ /2/
+[ /2 width=3/
| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
elim (ltps_ldrop_trans_be … HL0 … HL02 Hd1e2 He2de1) -L0 #L0 #HL02 #HL0
- elim (IHL … HL0 Hd1e2 He2de1) -L /3/
+ elim (IHL … HL0 Hd1e2 He2de1) -L /3 width=3/
]
qed.
∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
∃∃L. L2 [d1 - e2, e1] ≫* L & ↓[0, e2] L1 ≡ L.
#L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1
-[ /2/
+[ /2 width=3/
| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #He2d1
elim (IHL … HL02 He2d1) -L0 #L0 #HL20 #HL0
- elim (ltps_ldrop_conf_le … HL1 … HL0 He2d1) -L /3/
+ elim (ltps_ldrop_conf_le … HL1 … HL0 He2d1) -L /3 width=3/
]
qed.
∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
∃∃L. L [d1 - e2, e1] ≫* L2 & ↓[0, e2] L1 ≡ L.
#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0
-[ /2/
+[ /2 width=3/
| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #He2d1
elim (ltps_ldrop_trans_le … HL0 … HL02 He2d1) -L0 #L0 #HL02 #HL0
- elim (IHL … HL0 He2d1) -L /3/
+ elim (IHL … HL0 He2d1) -L /3 width=3/
]
qed.
theorem ltpss_trans_eq: ∀L1,L,L2,d,e.
L1 [d, e] ≫* L → L [d, e] ≫* L2 → L1 [d, e] ≫* L2.
-/2/ qed.
+/2 width=3/ qed.
lemma ltpss_tpss2: ∀L1,L2,I,V1,V2,e.
L1 [0, e] ≫* L2 → L2 ⊢ V1 [0, e] ≫* V2 →
L1. 𝕓{I} V1 [0, e + 1] ≫* L2. 𝕓{I} V2.
#L1 #L2 #I #V1 #V2 #e #HL12 #H @(tpss_ind … H) -V2
-[ /2/
-| #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2/
+[ /2 width=1/
+| #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2 width=1/
]
qed.
L1 [0, e - 1] ≫* L2 → L2 ⊢ V1 [0, e - 1] ≫* V2 →
0 < e → L1. 𝕓{I} V1 [0, e] ≫* L2. 𝕓{I} V2.
#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
->(plus_minus_m_m e 1) /2/
+>(plus_minus_m_m e 1) // /2 width=1/
qed.
lemma ltpss_tpss1: ∀L1,L2,I,V1,V2,d,e.
L1 [d, e] ≫* L2 → L2 ⊢ V1 [d, e] ≫* V2 →
L1. 𝕓{I} V1 [d + 1, e] ≫* L2. 𝕓{I} V2.
#L1 #L2 #I #V1 #V2 #d #e #HL12 #H @(tpss_ind … H) -V2
-[ /2/
-| #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2/
+[ /2 width=1/
+| #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2 width=1/
]
qed.
L1 [d - 1, e] ≫* L2 → L2 ⊢ V1 [d - 1, e] ≫* V2 →
0 < d → L1. 𝕓{I} V1 [d, e] ≫* L2. 𝕓{I} V2.
#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
->(plus_minus_m_m d 1) /2/
+>(plus_minus_m_m d 1) // /2 width=1/
qed.
d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ≫* U2.
#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 //
#L #L0 #_ #HL0 #IHL #T2 #U2 #d2 #e2 #HTU2 #Hde1d2
-lapply (ltps_tpss_trans_ge … HL0 HTU2) -HL0 HTU2 /2/
+lapply (ltps_tpss_trans_ge … HL0 HTU2) -HL0 -HTU2 /2 width=1/
qed.
lemma ltpss_tps_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ≫* U2.
#L1 #L0 #d1 #e1 #HL10 #T2 #U2 #d2 #e2 #HTU2 #Hde1d2
-@(ltpss_tpss_trans_ge … HL10 … Hde1d2) /2/ (**) (* /3 width=6/ is too slow *)
+@(ltpss_tpss_trans_ge … HL10 … Hde1d2) /2 width=1/ (**) (* /3 width=6/ is too slow *)
qed.
lemma ltpss_tpss_trans_eq: ∀L0,L1,d,e. L0 [d, e] ≫* L1 →
∀T2,U2. L1 ⊢ T2 [d, e] ≫* U2 → L0 ⊢ T2 [d, e] ≫* U2.
#L0 #L1 #d #e #H @(ltpss_ind … H) -L1
-[ /2/
+[ /2 width=1/
| #L #L1 #_ #HL1 #IHL #T2 #U2 #HTU2
- lapply (ltps_tpss_trans_eq … HL1 HTU2) -HL1 HTU2 /2/
+ lapply (ltps_tpss_trans_eq … HL1 HTU2) -HL1 -HTU2 /2 width=1/
]
qed.
lemma ltpss_tps_trans_eq: ∀L0,L1,d,e. L0 [d, e] ≫* L1 →
∀T2,U2. L1 ⊢ T2 [d, e] ≫ U2 → L0 ⊢ T2 [d, e] ≫* U2.
-/3/ qed.
+/3 width=3/ qed.
lemma ltpss_tpss_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 →
L0 ⊢ T2 [d2, e2] ≫* U2 → L0 [d1, e1] ≫* L1 →
#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #H @(ltpss_ind … H) -L1
[ //
| -HTU2 #L #L1 #_ #HL1 #IHL
- lapply (ltps_tpss_conf_ge … HL1 IHL) -HL1 IHL //
+ lapply (ltps_tpss_conf_ge … HL1 IHL) -HL1 -IHL //
]
qed.
L0 ⊢ T2 [d2, e2] ≫ U2 → L0 [d1, e1] ≫* L1 →
L1 ⊢ T2 [d2, e2] ≫* U2.
#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #HL01
-@(ltpss_tpss_conf_ge … Hde1d2 … HL01) /2/ (**) (* /3 width=6/ is too slow *)
+@(ltpss_tpss_conf_ge … Hde1d2 … HL01) /2 width=1/ (**) (* /3 width=6/ is too slow *)
qed.
lemma ltpss_tpss_conf_eq: ∀L0,L1,T2,U2,d,e.
L0 ⊢ T2 [d, e] ≫* U2 → L0 [d, e] ≫* L1 →
∃∃T. L1 ⊢ T2 [d, e] ≫* T & L1 ⊢ U2 [d, e] ≫* T.
#L0 #L1 #T2 #U2 #d #e #HTU2 #H @(ltpss_ind … H) -L1
-[ /2/
+[ /2 width=3/
| -HTU2 #L #L1 #_ #HL1 * #W2 #HTW2 #HUW2
elim (ltps_tpss_conf … HL1 HTW2) -HTW2 #T #HT2 #HW2T
- elim (ltps_tpss_conf … HL1 HUW2) -HL1 HUW2 #U #HU2 #HW2U
- elim (tpss_conf_eq … HW2T … HW2U) -HW2T HW2U #V #HTV #HUV
- lapply (tpss_trans_eq … HT2 … HTV) -T;
- lapply (tpss_trans_eq … HU2 … HUV) -U /2/
+ elim (ltps_tpss_conf … HL1 HUW2) -HL1 -HUW2 #U #HU2 #HW2U
+ elim (tpss_conf_eq … HW2T … HW2U) -HW2T -HW2U #V #HTV #HUV
+ lapply (tpss_trans_eq … HT2 … HTV) -T
+ lapply (tpss_trans_eq … HU2 … HUV) -U /2 width=3/
]
qed.
lemma ltpss_tps_conf_eq: ∀L0,L1,T2,U2,d,e.
L0 ⊢ T2 [d, e] ≫ U2 → L0 [d, e] ≫* L1 →
∃∃T. L1 ⊢ T2 [d, e] ≫* T & L1 ⊢ U2 [d, e] ≫* T.
-/3/ qed.
+/3 width=3/ qed.
lemma ltpss_tpss_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫* T2 →
∀L2,ds,es. L1 [ds, es] ≫* L2 →
∃∃T. L2 ⊢ T1 [d, e] ≫* T & L1 ⊢ T2 [ds, es] ≫* T.
#L1 #T1 #T2 #d #e #HT12 #L2 #ds #es #H @(ltpss_ind … H) -L2
-[ /3/
+[ /3 width=3/
| #L #L2 #HL1 #HL2 * #T #HT1 #HT2
elim (ltps_tpss_conf … HL2 HT1) -HT1 #T0 #HT10 #HT0
- lapply (ltps_tpss_trans_eq … HL2 … HT0) -HL2 HT0 #HT0
- lapply (ltpss_tpss_trans_eq … HL1 … HT0) -HL1 HT0 #HT0
- lapply (tpss_trans_eq … HT2 … HT0) -T /2/
+ lapply (ltps_tpss_trans_eq … HL2 … HT0) -HL2 -HT0 #HT0
+ lapply (ltpss_tpss_trans_eq … HL1 … HT0) -HL1 -HT0 #HT0
+ lapply (tpss_trans_eq … HT2 … HT0) -T /2 width=3/
]
qed.
lemma ltpss_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫ T2 →
∀L2,ds,es. L1 [ds, es] ≫* L2 →
∃∃T. L2 ⊢ T1 [d, e] ≫* T & L1 ⊢ T2 [ds, es] ≫* T.
-/3/ qed.
+/3 width=1/ qed.
(* Advanced properties ******************************************************)
L1 [0, e] ≫* L2 → ∀V1,V2. L2 ⊢ V1 [0, e] ≫ V2 →
L1. 𝕓{I} V1 [0, e + 1] ≫* L2. 𝕓{I} V2.
#L1 #L2 #I #e #H @(ltpss_ind … H) -L2
-[ /3/
+[ /3 width=1/
| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12
elim (ltps_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2
- lapply (IHL … HV1) -IHL HV1 #HL1
+ lapply (IHL … HV1) -IHL -HV1 #HL1
@step /2 width=5/ (**) (* /3 width=5/ is too slow *)
]
qed.
L1 [0, e - 1] ≫* L2 → L2 ⊢ V1 [0, e - 1] ≫ V2 →
0 < e → L1. 𝕓{I} V1 [0, e] ≫* L2. 𝕓{I} V2.
#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
->(plus_minus_m_m e 1) /2/
+>(plus_minus_m_m e 1) // /2 width=1/
qed.
lemma ltpss_tps1: ∀L1,L2,I,d,e. L1 [d, e] ≫* L2 →
∀V1,V2. L2 ⊢ V1 [d, e] ≫ V2 →
L1. 𝕓{I} V1 [d + 1, e] ≫* L2. 𝕓{I} V2.
#L1 #L2 #I #d #e #H @(ltpss_ind … H) -L2
-[ /3/
+[ /3 width=1/
| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12
elim (ltps_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2
- lapply (IHL … HV1) -IHL HV1 #HL1
+ lapply (IHL … HV1) -IHL -HV1 #HL1
@step /2 width=5/ (**) (* /3 width=5/ is too slow *)
]
qed.
L1 [d - 1, e] ≫* L2 → L2 ⊢ V1 [d - 1, e] ≫ V2 →
0 < d → L1. 𝕓{I} V1 [d, e] ≫* L2. 𝕓{I} V2.
#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
->(plus_minus_m_m d 1) /2/
+>(plus_minus_m_m d 1) // /2 width=1/
qed.
(* Advanced forward lemmas **************************************************)
L2 = K2. 𝕓{I} V2.
#e #K1 #I #V1 #L2 #He #H @(ltpss_ind … H) -L2
[ /2 width=5/
-| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct -L;
+| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct
elim (ltps_inv_tps21 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H
lapply (ltps_tps_trans_eq … HV2 … HK2) -HV2 #HV2
lapply (ltpss_tpss_trans_eq … HK1 … HV2) -HV2 #HV2 /3 width=5/
L2 = K2. 𝕓{I} V2.
#d #e #K1 #I #V1 #L2 #Hd #H @(ltpss_ind … H) -L2
[ /2 width=5/
-| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct -L;
+| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct
elim (ltps_inv_tps11 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H
lapply (ltps_tps_trans_eq … HV2 … HK2) -HV2 #HV2
lapply (ltpss_tpss_trans_eq … HK1 … HV2) -HV2 #HV2 /3 width=5/
lemma tpss_strap: ∀L,T1,T,T2,d,e.
L ⊢ T1 [d, e] ≫ T → L ⊢ T [d, e] ≫* T2 → L ⊢ T1 [d, e] ≫* T2.
-/2/ qed.
+/2 width=3/ qed.
lemma tpss_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫* T2 →
∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ≫* T2.
-/3/ qed.
+/3 width=3/ qed.
lemma tpss_refl: ∀d,e,L,T. L ⊢ T [d, e] ≫* T.
-/2/ qed.
+/2 width=1/ 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
+#L #V1 #V2 #d #e #HV12 elim HV12 -V2
+[ #V2 #HV12 #I #T1 #T2 #HT12 elim 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_lsubs_conf … HT12 (L. 𝕓{I} V) ?) -HT12 /2/ #HT12
- lapply (IHV … HT12) -IHV HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
+ lapply (tpss_lsubs_conf … HT12 (L. 𝕓{I} V) ?) -HT12 /2 width=1/ #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/
+#L #I #V1 #V2 #T1 #T2 #d #e #HV12 elim HV12 -V2
+[ #V2 #HV12 #HT12 elim HT12 -T2
+ [ /3 width=1/
| #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 *)
+ 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
+#L #T1 #T2 #d1 #e1 #H #d1 #d2 #Hd21 #Hde12 @(tpss_ind … H) -T2
[ //
| #T #T2 #_ #HT12 #IHT
- lapply (tps_weak … HT12 … Hd21 Hde12) -HT12 Hd21 Hde12 /2/
+ lapply (tps_weak … HT12 … Hd21 Hde12) -HT12 -Hd21 -Hde12 /2 width=3/
]
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
+#L #T1 #T2 #d #e #H @(tpss_ind … H) -T2
[ //
| #T #T2 #_ #HT12 #IHT
- lapply (tps_weak_top … HT12) -HT12 /2/
+ lapply (tps_weak_top … HT12) -HT12 /2 width=3/
]
qed.
(* 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
+#L #T2 #k #d #e #H @(tpss_ind … H) -T2
[ //
-| #T #T2 #_ #HT2 #IHT destruct -T
+| #T #T2 #_ #HT2 #IHT destruct
>(tps_inv_sort1 … HT2) -HT2 //
]
qed-.
∃∃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
+#d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -U2
[ /2 width=5/
-| #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct -U;
+| #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
elim (tps_inv_bind1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H
- lapply (tpss_lsubs_conf … HT1 (L. 𝕓{I} V2) ?) -HT1 /3 width=5/
+ lapply (tpss_lsubs_conf … HT1 (L. 𝕓{I} V2) ?) -HT1 /2 width=1/ /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
+#d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -U2
[ /2 width=5/
-| #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct -U;
+| #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
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
+#L #T1 #T2 #d #H @(tpss_ind … H) -T2
[ //
| #T #T2 #_ #HT2 #IHT <(tps_inv_refl_O2 … HT2) -HT2 //
]
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/
+#L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(tpss_ind … H) -U1
+[ /3 width=4/
| #U #U1 #_ #HU1 #IHU #U2 #HU12
elim (lift_total U 0 (i+1)) #U0 #HU0
lapply (IHU … HU0) -IHU #H
lapply (ldrop_fwd_ldrop2 … 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/ ]
+ lapply (tps_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 -HLK -HU0 -HU12 // normalize #HU02
+ lapply (tps_weak … HU02 d e ? ?) -HU02 [ >arith_i2 // | /2 width=1/ | /2 width=3/ ]
]
qed.
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/
+#L #T2 #I #d #e #H @(tpss_ind … H) -T2
+[ /2 width=1/
| #T #T2 #_ #HT2 *
- [ #H destruct -T;
- elim (tps_inv_atom1 … HT2) -HT2 [ /2/ | * /3 width=10/ ]
+ [ #H destruct
+ elim (tps_inv_atom1 … HT2) -HT2 [ /2 width=1/ | * /3 width=10/ ]
| * #K #V1 #V #i #Hdi #Hide #HLK #HV1 #HVT #HI
lapply (ldrop_fwd_ldrop2 … 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 *)
+ elim (tps_inv_lift1_up … HT2 … H … HVT ? ? ?) normalize -HT2 -H -HVT [2,3,4: /2 width=1/ ] #V2 <minus_plus #HV2 #HVT2
+ @or_intror @(ex6_4_intro … Hdi Hide HLK … HVT2 HI) /2 width=3/ (**) (* /4 width=10/ is too slow *)
]
]
qed-.
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/
+elim (tpss_inv_atom1 … H) -H /2 width=1/
+* #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct /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 //
+#L #T1 #T2 #d #H #K #V #HLK @(tpss_ind … H) -T2 //
#T #T2 #_ #HT2 #IHT <(tps_inv_refl_SO2 … HT2 … HLK) //
qed-.
| -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/
+ lapply (tps_lift_le … HT2 … HLK HTU HTU2 ?) -HT2 -HLK -HTU -HTU2 // /2 width=3/
]
qed.
| -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
elim (lift_total T d e) #U #HTU
lapply (IHT … HTU) -IHT #HU1
- lapply (tps_lift_be … HT2 … HLK HTU HTU2 ? ?) -HT2 HLK HTU HTU2 /2/
+ lapply (tps_lift_be … HT2 … HLK HTU HTU2 ? ?) -HT2 -HLK -HTU -HTU2 // /2 width=3/
]
qed.
| -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/
+ lapply (tps_lift_ge … HT2 … HLK HTU HTU2 ?) -HT2 -HLK -HTU -HTU2 // /2 width=3/
]
qed.
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) -U2
-[ /2/
+[ /2 width=3/
| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
- elim (tps_inv_lift1_le … HU2 … HLK … HTU ?) -HU2 HLK HTU // /3/
+ elim (tps_inv_lift1_le … HU2 … HLK … HTU ?) -HU2 -HLK -HTU // /3 width=3/
]
qed.
dt ≤ d → d + e ≤ dt + et →
∃∃T2. K ⊢ T1 [dt, et - e] ≫* T2 & ↑[d, e] T2 ≡ U2.
#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(tpss_ind … H) -U2
-[ /2/
+[ /2 width=3/
| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
- elim (tps_inv_lift1_be … HU2 … HLK … HTU ? ?) -HU2 HLK HTU // /3/
+ elim (tps_inv_lift1_be … HU2 … HLK … HTU ? ?) -HU2 -HLK -HTU // /3 width=3/
]
qed.
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) -U2
-[ /2/
+[ /2 width=3/
| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
- elim (tps_inv_lift1_ge … HU2 … HLK … HTU ?) -HU2 HLK HTU // /3/
+ elim (tps_inv_lift1_ge … HU2 … HLK … HTU ?) -HU2 -HLK -HTU // /3 width=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) -U2 //
-#U #U2 #_ #HU2 #IHU destruct -U1
-<(tps_inv_lift1_eq … HU2 … HTU1) -HU2 HTU1 //
+#U #U2 #_ #HU2 #IHU destruct
+<(tps_inv_lift1_eq … HU2 … HTU1) -HU2 -HTU1 //
qed.
lemma tpss_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
dt ≤ d → dt + et ≤ d + e →
∃∃T2. K ⊢ T1 [dt, d - dt] ≫* T2 & ↑[d, e] T2 ≡ U2.
#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(tpss_ind … H) -U2
-[ /2/
+[ /2 width=3/
| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
- elim (tps_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -HU2 HLK HTU // /3/
+ elim (tps_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -HU2 -HLK -HTU // /3 width=3/
]
qed.
L0 ⊢ T2 [d2, e2] ≫* U2 → L1 ⊢ T2 [d2, e2] ≫* U2.
#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HL01 #H @(tpss_ind … H) -U2 //
#U #U2 #_ #HU2 #IHU
-lapply (ltps_tps_conf_ge … HU2 … HL01 ?) -HU2 HL01 /2/
+lapply (ltps_tps_conf_ge … HU2 … HL01 ?) -HU2 -HL01 // /2 width=3/
qed.
lemma ltps_tpss_conf: ∀L0,L1,T2,U2,d1,e1,d2,e2.
L0 [d1, e1] ≫ L1 → L0 ⊢ T2 [d2, e2] ≫* U2 →
∃∃T. L1 ⊢ T2 [d2, e2] ≫* T & L1 ⊢ U2 [d1, e1] ≫* T.
#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #HL01 #H @(tpss_ind … H) -U2
-[ /3/
+[ /3 width=3/
| #U #U2 #_ #HU2 * #T #HT2 #HUT
- elim (ltps_tps_conf … HU2 … HL01) -HU2 HL01 #W #HUW #HU2W
+ elim (ltps_tps_conf … HU2 … HL01) -HU2 -HL01 #W #HUW #HU2W
elim (tpss_strip_eq … HUT … HUW) -U
/3 width=5 by ex2_1_intro, step, tpss_strap/ (**) (* just /3 width=5/ is too slow *)
]
L0 ⊢ T2 [d2, e2] ≫* U2 → L1 ⊢ T2 [d2, e2] ≫* U2.
#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HL10 #H @(tpss_ind … H) -U2 //
#U #U2 #_ #HU2 #IHU
-lapply (ltps_tps_trans_ge … HU2 … HL10 ?) -HU2 HL10 /2/
+lapply (ltps_tps_trans_ge … HU2 … HL10 ?) -HU2 -HL10 // /2 width=3/
qed.
lemma ltps_tpss_trans_down: ∀L0,L1,T2,U2,d1,e1,d2,e2. d2 + e2 ≤ d1 →
L1 [d1, e1] ≫ L0 → L0 ⊢ T2 [d2, e2] ≫* U2 →
∃∃T. L1 ⊢ T2 [d2, e2] ≫* T & L0 ⊢ T [d1, e1] ≫* U2.
#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde2d1 #HL10 #H @(tpss_ind … H) -U2
-[ /3/
+[ /3 width=3/
| #U #U2 #_ #HU2 * #T #HT2 #HTU
elim (tpss_strap1_down … HTU … HU2 ?) -U // #U #HTU #HU2
- elim (ltps_tps_trans … HTU … HL10) -HTU HL10 #W #HTW #HWU
- @(ex2_1_intro … W) /2/ (**) (* /3 width=5/ does not work as in ltps_tpss_conf *)
+ elim (ltps_tps_trans … HTU … HL10) -HTU -HL10 #W #HTW #HWU
+ @(ex2_1_intro … W) /2 width=3/ (**) (* /3 width=5/ does not work as in ltps_tpss_conf *)
]
qed.
fact ltps_tps_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e.
L1 ⊢ T2 [d, e] ≫ U2 → ∀L0. L0 [d, e] ≫ L1 →
Y1 = L1 → X2 = T2 → L0 ⊢ T2 [d, e] ≫* U2.
-#Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 X2 #Y1 #X2 #IH
-#L1 #T2 #U2 #d #e * -L1 T2 U2 d e
+#Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH
+#L1 #T2 #U2 #d #e * -L1 -T2 -U2 -d -e
[ //
-| #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #L0 #HL10 #H1 #H2 destruct -Y1 X2;
+| #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #L0 #HL10 #H1 #H2 destruct
lapply (ldrop_fwd_lw … HLK1) normalize #H1
- elim (ltps_ldrop_trans_be … HL10 … HLK1 ? ?) -HL10 HLK1 [2,3: /2/ ] #X #H #HLK0
- elim (ltps_inv_tps22 … H ?) -H [2: /2/ ] #K0 #V0 #HK01 #HV01 #H destruct -X;
+ elim (ltps_ldrop_trans_be … HL10 … HLK1 ? ?) -HL10 -HLK1 /2 width=1/ #X #H #HLK0
+ elim (ltps_inv_tps22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct
lapply (tps_fwd_tw … HV01) #H2
- lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 [ /2/ ] -H2 #H
- lapply (IH … HV01 … HK01 ? ?) -IH HV01 HK01 [1,3: // |2,4: skip | normalize /2/ | /3 width=6/ ]
-| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct -Y1 X2;
- lapply (tps_lsubs_conf … HT12 (L. 𝕓{I} V1) ?) -HT12 /2/ #HT12
+ lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 /2 width=1/ -H2 #H
+ lapply (IH … HV01 … HK01 ? ?) -IH -HV01 -HK01
+ [1,3: // |2,4: skip | normalize /2 width=1/ | /3 width=6/ ]
+| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct
+ lapply (tps_lsubs_conf … HT12 (L. 𝕓{I} V1) ?) -HT12 /2 width=1/ #HT12
lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3,5: normalize // |2,4: skip ] #HV12
- lapply (IH … HT12 (L0. 𝕓{I} V1) ? ? ?) -IH HT12 [1,3,5: /2/ |2,4: skip | normalize // ] -HL0 #HT12
- lapply (tpss_lsubs_conf … HT12 (L0. 𝕓{I} V2) ?) -HT12 /2/
-| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct -Y1 X2;
+ lapply (IH … HT12 (L0. 𝕓{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12
+ lapply (tpss_lsubs_conf … HT12 (L0. 𝕓{I} V2) ?) -HT12 /2 width=1/
+| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct
lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3,5: normalize // |2,4: skip ]
- lapply (IH … HT12 … HL0 ? ?) -IH HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2/
+ lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/
]
qed.
lemma ltps_tpss_trans_eq: ∀L0,L1,T2,U2,d,e. L0 [d, e] ≫ L1 →
L1 ⊢ T2 [d, e] ≫* U2 → L0 ⊢ T2 [d, e] ≫* U2.
#L0 #L1 #T2 #U2 #d #e #HL01 #H @(tpss_ind … H) -U2 //
-#U #U2 #_ #HU2 #IHU @(tpss_trans_eq … IHU) /2/
+#U #U2 #_ #HU2 #IHU @(tpss_trans_eq … IHU) /2 width=3/
qed.
(* Advanced properties ******************************************************)
lemma tpss_tps: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫* T2 → L ⊢ T1 [d, 1] ≫ T2.
-#L #T1 #T2 #d #H @(tpss_ind … H) -H T2 //
+#L #T1 #T2 #d #H @(tpss_ind … H) -T2 //
#T #T2 #_ #HT2 #IHT1
lapply (tps_trans_ge … IHT1 … HT2 ?) //
qed.
lemma tpss_strip_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.
+/3 width=3/ qed.
lemma tpss_strip_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.
+/3 width=3/ qed.
lemma tpss_strap1_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.
+/3 width=3/ qed.
lemma tpss_strap2_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.
+/3 width=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/
+#L #T1 #T2 #d #e #H #i #Hdi #Hide @(tpss_ind … H) -T2
+[ /2 width=3/
| #T #T2 #_ #HT12 * #T3 #HT13 #HT3
- elim (tps_split_up … HT12 … Hdi Hide) -HT12 Hide #T0 #HT0 #HT02
+ elim (tps_split_up … HT12 … Hdi Hide) -HT12 -Hide #T0 #HT0 #HT02
elim (tpss_strap1_down … HT3 … HT0 ?) -T [2: <plus_minus_m_m_comm // ]
/3 width=7 by ex2_1_intro, step/ (**) (* just /3 width=7/ is too slow *)
]
∃∃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/
+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
+elim (tpss_inv_lift1_ge … HU2 … HLK … HTU1 ?) -HU2 -HLK -HTU1 // <minus_plus_m_m /2 width=3/
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.
+/3 width=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.
+/3 width=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.
+/2 width=3/ 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.
+/3 width=3/ qed.
projects / helm.git / commitdiff