∀L1,L2,d,i. |L1| = |L2| → yinj i < d → R d (#i) L1 L2
) → (
∀I,L1,L2,K1,K2,V,d,i. d ≤ yinj i →
- â\87©[i] L1 â\89¡ K1.â\93\91{I}V â\86\92 â\87©[i] L2 ≡ K2.ⓑ{I}V →
+ â¬\87[i] L1 â\89¡ K1.â\93\91{I}V â\86\92 â¬\87[i] L2 ≡ K2.ⓑ{I}V →
K1 ≡[V, yinj O] K2 → R (yinj O) V K1 K2 → R d (#i) L1 L2
) → (
∀L1,L2,d,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → R d (#i) L1 L2
lemma lleq_fwd_lref: ∀L1,L2,d,i. L1 ≡[#i, d] L2 →
∨∨ |L1| ≤ i ∧ |L2| ≤ i
| yinj i < d
- | â\88\83â\88\83I,K1,K2,V. â\87©[i] L1 ≡ K1.ⓑ{I}V &
- â\87©[i] L2 ≡ K2.ⓑ{I}V &
+ | â\88\83â\88\83I,K1,K2,V. â¬\87[i] L1 ≡ K1.ⓑ{I}V &
+ â¬\87[i] L2 ≡ K2.ⓑ{I}V &
K1 ≡[V, yinj 0] K2 & d ≤ yinj i.
#L1 #L2 #d #i #H elim (llpx_sn_fwd_lref … H) /2 width=1/
* /3 width=7 by or3_intro2, ex4_4_intro/
qed-.
-lemma lleq_fwd_ldrop_sn: ∀L1,L2,T,d. L1 ≡[d, T] L2 → ∀K1,i. ⇩[i] L1 ≡ K1 →
- â\88\83K2. â\87©[i] L2 ≡ K2.
-/2 width=7 by llpx_sn_fwd_ldrop_sn/ qed-.
+lemma lleq_fwd_drop_sn: ∀L1,L2,T,d. L1 ≡[d, T] L2 → ∀K1,i. ⬇[i] L1 ≡ K1 →
+ â\88\83K2. â¬\87[i] L2 ≡ K2.
+/2 width=7 by llpx_sn_fwd_drop_sn/ qed-.
-lemma lleq_fwd_ldrop_dx: ∀L1,L2,T,d. L1 ≡[d, T] L2 → ∀K2,i. ⇩[i] L2 ≡ K2 →
- â\88\83K1. â\87©[i] L1 ≡ K1.
-/2 width=7 by llpx_sn_fwd_ldrop_dx/ qed-.
+lemma lleq_fwd_drop_dx: ∀L1,L2,T,d. L1 ≡[d, T] L2 → ∀K2,i. ⬇[i] L2 ≡ K2 →
+ â\88\83K1. â¬\87[i] L1 ≡ K1.
+/2 width=7 by llpx_sn_fwd_drop_dx/ qed-.
lemma lleq_fwd_bind_sn: ∀a,I,L1,L2,V,T,d.
L1 ≡[ⓑ{a,I}V.T, d] L2 → L1 ≡[V, d] L2.
/2 width=1 by llpx_sn_skip/ qed.
lemma lleq_lref: ∀I,L1,L2,K1,K2,V,d,i. d ≤ yinj i →
- â\87©[i] L1 â\89¡ K1.â\93\91{I}V â\86\92 â\87©[i] L2 ≡ K2.ⓑ{I}V →
+ â¬\87[i] L1 â\89¡ K1.â\93\91{I}V â\86\92 â¬\87[i] L2 ≡ K2.ⓑ{I}V →
K1 ≡[V, 0] K2 → L1 ≡[#i, d] L2.
/2 width=9 by llpx_sn_lref/ qed.
qed-.
lemma lleq_ge_up: ∀L1,L2,U,dt. L1 ≡[U, dt] L2 →
- â\88\80T,d,e. â\87§[d, e] T ≡ U →
+ â\88\80T,d,e. â¬\86[d, e] T ≡ U →
dt ≤ d + e → L1 ≡[U, d] L2.
/2 width=6 by llpx_sn_ge_up/ qed-.
L1 ≡[ⓑ{a,I}V.T, 0] L2.
/2 width=1 by llpx_sn_bind_O/ qed-.
-(* Advancded properties on lazy pointwise exyensions ************************)
+(* Advanceded properties on lazy pointwise extensions ************************)
lemma llpx_sn_lrefl: ∀R. (∀L. reflexive … (R L)) →
∀L1,L2,T,d. L1 ≡[T, d] L2 → llpx_sn R d T L1 L2.