L1 ⪤*[R,T] L2.
#R #L1 #L2 #T #f #Hf #H elim H -L2
[ elim (frees_total L1 T) | #L elim (frees_total L T) ]
-/5 width=7 by sex_sdj, rexs_step_dx, sdj_isid_sn, inj, ex2_intro/
+/5 width=7 by sex_sdj, rexs_step_dx, pr_sdj_isi_sn, inj, ex2_intro/
qed.
(* Advanced eliminators *****************************************************)
| #L0 #L2 #_ #HL02 * #L * #f0 #Hf0 #HL1 #HL0
lapply (req_rex_trans … HL0 … HL02) -L0 // * #f1 #Hf1 #HL2
elim (sex_sdj_split_sn … ceq_ext … HL2 f0 ?) -HL2
- [ #L0 #HL0 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ]
- lapply (sex_sdj … HL0 f1 ?) /2 width=1 by sdj_isid_sn/ #H
+ [ #L0 #HL0 #HL02 |*: /2 width=1 by ext2_refl, pr_sdj_isi_dx/ ]
+ lapply (sex_sdj … HL0 f1 ?) /2 width=1 by pr_sdj_isi_sn/ #H
elim (frees_sex_conf_fsge … Hf1 … H) // -H2R -H #f2 #Hf2 #Hf21
lapply (sle_sex_trans … HL02 … Hf21) -f1 // #HL02
lapply (sex_co ?? cfull (CTC … (cext2 R)) … HL1) -HL1 /2 width=1 by ext2_inv_tc/ #HL1
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⇡[ term 46 h ] )"
+ non associative with precedence 46
+ for @{ 'UpArrow_1_0 $h }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⇡*[ term 46 h, term 46 n ] )"
+ non associative with precedence 46
+ for @{ 'UpArrowStar_2_0 $h $n }.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⫯[ term 46 h ] break term 46 s )"
- non associative with precedence 46
- for @{ 'UpSpoon $h $s }.
(* Basic_2A1: includes: drop_atom drop_pair drop_drop drop_skip
drop_refl_atom_O2 drop_drop_lt drop_skip_lt
*)
-inductive drops (b:bool): rtmap → relation lenv ≝
+inductive drops (b:bool): pr_map → relation lenv ≝
| drops_atom: ∀f. (b = Ⓣ → 𝐈❪f❫) → drops b (f) (⋆) (⋆)
| drops_drop: ∀f,I,L1,L2. drops b f L1 L2 → drops b (↑f) (L1.ⓘ[I]) L2
| drops_skip: ∀f,I1,I2,L1,L2.
'RDropStar b f L1 L2 = (drops b f L1 L2).
interpretation "uniform slicing (local environment)"
- 'RDrop i L1 L2 = (drops true (uni i) L1 L2).
+ 'RDrop i L1 L2 = (drops true (pr_uni i) L1 L2).
definition d_liftable1: predicate (relation2 lenv term) ≝
λR. ∀K,T. R K T → ∀b,f,L. ⇩*[b,f] L ≘ K →
#f @drops_atom #H destruct
qed.
-lemma drops_eq_repl_back: ∀b,L1,L2. eq_repl_back … (λf. ⇩*[b,f] L1 ≘ L2).
+lemma drops_eq_repl_back: ∀b,L1,L2. pr_eq_repl_back … (λf. ⇩*[b,f] L1 ≘ L2).
#b #L1 #L2 #f1 #H elim H -f1 -L1 -L2
-[ /4 width=3 by drops_atom, isid_eq_repl_back/
+[ /4 width=3 by drops_atom, pr_isi_eq_repl_back/
| #f1 #I #L1 #L2 #_ #IH #f2 #H elim (eq_inv_nx … H) -H
/3 width=3 by drops_drop/
| #f1 #I1 #I2 #L1 #L2 #_ #HI #IH #f2 #H elim (eq_inv_px … H) -H
]
qed-.
-lemma drops_eq_repl_fwd: ∀b,L1,L2. eq_repl_fwd … (λf. ⇩*[b,f] L1 ≘ L2).
-#b #L1 #L2 @eq_repl_sym /2 width=3 by drops_eq_repl_back/ (**) (* full auto fails *)
+lemma drops_eq_repl_fwd: ∀b,L1,L2. pr_eq_repl_fwd … (λf. ⇩*[b,f] L1 ≘ L2).
+#b #L1 #L2 @pr_eq_repl_sym /2 width=3 by drops_eq_repl_back/ (**) (* full auto fails *)
qed-.
(* Basic_2A1: includes: drop_FT *)
⇩*[b,g] K ≘ Y.
#b #f #X #Y * -f -X -Y
[ #f #Hf #g #J #K #H destruct
-| #f #I #L1 #L2 #HL #g #J #K #H1 #H2 <(injective_next … H2) -g destruct //
-| #f #I1 #I2 #L1 #L2 #_ #_ #g #J #K #_ #H2 elim (discr_push_next … H2)
+| #f #I #L1 #L2 #HL #g #J #K #H1 #H2 <(eq_inv_pr_next_bi … H2) -g destruct //
+| #f #I1 #I2 #L1 #L2 #_ #_ #g #J #K #_ #H2 elim (eq_inv_pr_push_next … H2)
]
qed-.
∃∃I2,K2. ⇩*[b,g] K1 ≘ K2 & ⇧*[g] I2 ≘ I1 & Y = K2.ⓘ[I2].
#b #f #X #Y * -f -X -Y
[ #f #Hf #g #J1 #K1 #H destruct
-| #f #I #L1 #L2 #_ #g #J1 #K1 #_ #H2 elim (discr_next_push … H2)
-| #f #I1 #I2 #L1 #L2 #HL #HI #g #J1 #K1 #H1 #H2 <(injective_push … H2) -g destruct
+| #f #I #L1 #L2 #_ #g #J1 #K1 #_ #H2 elim (eq_inv_pr_next_push … H2)
+| #f #I1 #I2 #L1 #L2 #HL #HI #g #J1 #K1 #H1 #H2 <(eq_inv_pr_push_bi … H2) -g destruct
/2 width=5 by ex3_2_intro/
]
qed-.
∃∃I1,K1. ⇩*[b,g] K1 ≘ K2 & ⇧*[g] I2 ≘ I1 & X = K1.ⓘ[I1].
#b #f #X #Y * -f -X -Y
[ #f #Hf #g #J2 #K2 #H destruct
-| #f #I #L1 #L2 #_ #g #J2 #K2 #_ #H2 elim (discr_next_push … H2)
-| #f #I1 #I2 #L1 #L2 #HL #HV #g #J2 #K2 #H1 #H2 <(injective_push … H2) -g destruct
+| #f #I #L1 #L2 #_ #g #J2 #K2 #_ #H2 elim (eq_inv_pr_next_push … H2)
+| #f #I1 #I2 #L1 #L2 #HL #HV #g #J2 #K2 #H1 #H2 <(eq_inv_pr_push_bi … H2) -g destruct
/2 width=5 by ex3_2_intro/
]
qed-.
#b #f2 #X #Y #H elim H -f2 -X -Y
[ #f2 #Hf2 #J #K #H destruct
| #f2 #I #L1 #L2 #_ #IHL #J #K #H elim (IHL … H) -IHL
- /3 width=7 by after_next, ex3_2_intro, drops_drop/
+ /3 width=7 by pr_after_next, ex3_2_intro, drops_drop/
| #f2 #I1 #I2 #L1 #L2 #HL #_ #_ #J #K #H destruct
- lapply (after_isid_dx 𝐢 … f2) /3 width=9 by after_push, ex3_2_intro, drops_drop/
+ lapply (pr_after_isi_dx 𝐢 … f2) /3 width=9 by pr_after_push, ex3_2_intro, drops_drop/
]
qed-.
(* Basic_2A1: includes: drop_refl *)
lemma drops_refl: ∀b,L,f. 𝐈❪f❫ → ⇩*[b,f] L ≘ L.
#b #L elim L -L /2 width=1 by drops_atom/
-#L #I #IHL #f #Hf elim (isid_inv_gen … Hf) -Hf
+#L #I #IHL #f #Hf elim (pr_isi_inv_gen … Hf) -Hf
/3 width=1 by drops_skip, liftsb_refl/
qed.
(* Basic_2A1: includes: drop_inv_O2 *)
lemma drops_fwd_isid: ∀b,f,L1,L2. ⇩*[b,f] L1 ≘ L2 → 𝐈❪f❫ → L1 = L2.
#b #f #L1 #L2 #H elim H -f -L1 -L2 //
-[ #f #I #L1 #L2 #_ #_ #H elim (isid_inv_next … H) //
-| /5 width=5 by isid_inv_push, liftsb_fwd_isid, eq_f2, sym_eq/
+[ #f #I #L1 #L2 #_ #_ #H elim (pr_isi_inv_next … H) //
+| /5 width=5 by pr_isi_inv_push, liftsb_fwd_isid, eq_f2, sym_eq/
]
qed-.
lemma drops_after_fwd_drop2: ∀b,f2,I,X,K. ⇩*[b,f2] X ≘ K.ⓘ[I] →
∀f1,f. 𝐈❪f1❫ → f2 ⊚ ↑f1 ≘ f → ⇩*[b,f] X ≘ K.
#b #f2 #I #X #K #H #f1 #f #Hf1 #Hf elim (drops_fwd_drop2 … H) -H
-#g1 #g #Hg1 #Hg #HK lapply (after_mono_eq … Hg … Hf ??) -Hg -Hf
-/3 width=5 by drops_eq_repl_back, isid_inv_eq_repl, eq_next/
+#g1 #g #Hg1 #Hg #HK lapply (pr_after_mono_eq … Hg … Hf ??) -Hg -Hf
+/3 width=5 by drops_eq_repl_back, pr_isi_inv_eq_repl, pr_eq_next/
qed-.
(* Forward lemmas with test for finite colength *****************************)
lemma drops_fwd_isfin: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐅❪f❫.
#f #L1 #L2 #H elim H -f -L1 -L2
-/3 width=1 by isfin_next, isfin_push, isfin_isid/
+/3 width=1 by pr_isf_next, pr_isf_push, pr_isf_isi/
qed-.
(* Properties with test for uniformity **************************************)
∃∃g,I,K. ⇩*[Ⓣ,g] K ≘ L2 & 𝐔❪g❫ & L1 = K.ⓘ[I] & f = ↑g.
#f #L1 #L2 * -f -L1 -L2
[ /4 width=1 by or_introl, conj/
-| /4 width=7 by isuni_inv_next, ex4_3_intro, or_intror/
-| /7 width=6 by drops_fwd_isid, liftsb_fwd_isid, isuni_inv_push, isid_push, or_introl, conj, eq_f2, sym_eq/
+| /4 width=7 by pr_isu_inv_next, ex4_3_intro, or_intror/
+| /7 width=6 by drops_fwd_isid, liftsb_fwd_isid, pr_isu_inv_push, pr_isi_push, or_introl, conj, eq_f2, sym_eq/
]
qed-.
lemma drops_inv_bind1_isuni: ∀b,f,I,K,L2. 𝐔❪f❫ → ⇩*[b,f] K.ⓘ[I] ≘ L2 →
(𝐈❪f❫ ∧ L2 = K.ⓘ[I]) ∨
∃∃g. 𝐔❪g❫ & ⇩*[b,g] K ≘ L2 & f = ↑g.
-#b #f #I #K #L2 #Hf #H elim (isuni_split … Hf) -Hf * #g #Hg #H0 destruct
+#b #f #I #K #L2 #Hf #H elim (pr_isu_split … Hf) -Hf * #g #Hg #H0 destruct
[ lapply (drops_inv_skip1 … H) -H * #Z #Y #HY #HZ #H destruct
<(drops_fwd_isid … HY Hg) -Y >(liftsb_fwd_isid … HZ Hg) -Z
- /4 width=3 by isid_push, or_introl, conj/
+ /4 width=3 by pr_isi_push, or_introl, conj/
| lapply (drops_inv_drop1 … H) -H /3 width=4 by ex3_intro, or_intror/
]
qed-.
lemma drops_inv_bind2_isuni_next: ∀b,f,I,K,L1. 𝐔❪f❫ → ⇩*[b,↑f] L1 ≘ K.ⓘ[I] →
∃∃I1,K1. ⇩*[b,f] K1 ≘ K.ⓘ[I] & L1 = K1.ⓘ[I1].
-#b #f #I #K #L1 #Hf #H elim (drops_inv_bind2_isuni … H) -H /2 width=3 by isuni_next/ -Hf *
-[ #H elim (isid_inv_next … H) -H //
+#b #f #I #K #L1 #Hf #H elim (drops_inv_bind2_isuni … H) -H /2 width=3 by pr_isu_next/ -Hf *
+[ #H elim (pr_isi_inv_next … H) -H //
| /2 width=4 by ex2_2_intro/
]
qed-.
#f #L1 #L2 #H elim H -f -L1 -L2
[ #f #_ #_ #J #K #H destruct
| #f #I #L1 #L2 #_ #IH #Hf #J #K #H destruct
- /4 width=3 by drops_drop, isuni_inv_next/
+ /4 width=3 by drops_drop, pr_isu_inv_next/
| #f #I1 #I2 #L1 #L2 #HL12 #HI21 #_ #Hf #J #K #H destruct
- lapply (isuni_inv_push … Hf ??) -Hf [1,2: // ] #Hf
+ lapply (pr_isu_inv_push … Hf ??) -Hf [1,2: // ] #Hf
<(drops_fwd_isid … HL12) -K // <(liftsb_fwd_isid … HI21) -I1
- /3 width=3 by drops_refl, isid_push/
+ /3 width=3 by drops_refl, pr_isi_push/
]
qed-.
(* Basic_1: was: drop_S *)
(* Basic_2A1: was: drop_fwd_drop2 *)
lemma drops_isuni_fwd_drop2: ∀b,f,I,X,K. 𝐔❪f❫ → ⇩*[b,f] X ≘ K.ⓘ[I] → ⇩*[b,↑f] X ≘ K.
-/3 width=7 by drops_after_fwd_drop2, after_isid_isuni/ qed-.
+/3 width=7 by drops_after_fwd_drop2, pr_after_isu_isi_next/ qed-.
(* Inversion lemmas with uniform relocations ********************************)
lemma drops_inv_atom2: ∀b,L,f. ⇩*[b,f] L ≘ ⋆ →
∃∃n,f1. ⇩*[b,𝐔❨n❩] L ≘ ⋆ & 𝐔❨n❩ ⊚ f1 ≘ f.
#b #L elim L -L
-[ /3 width=4 by drops_atom, after_isid_sn, ex2_2_intro/
-| #L #I #IH #f #H elim (pn_split f) * #g #H0 destruct
+[ /3 width=4 by drops_atom, pr_after_isi_sn, ex2_2_intro/
+| #L #I #IH #f #H elim (pr_map_split_tl f) * #g #H0 destruct
[ elim (drops_inv_skip1 … H) -H #J #K #_ #_ #H destruct
| lapply (drops_inv_drop1 … H) -H #HL
- elim (IH … HL) -IH -HL /3 width=8 by drops_drop, after_next, ex2_2_intro/
+ elim (IH … HL) -IH -HL /3 width=8 by drops_drop, pr_after_next, ex2_2_intro/
]
]
qed-.
lemma drops_inv_succ: ∀L1,L2,i. ⇩[↑i] L1 ≘ L2 →
∃∃I,K. ⇩[i] K ≘ L2 & L1 = K.ⓘ[I].
#L1 #L2 #i #H elim (drops_inv_isuni … H) -H // *
-[ #H elim (isid_inv_next … H) -H //
+[ #H elim (pr_isi_inv_next … H) -H //
| /2 width=4 by ex2_2_intro/
]
qed-.
#b #f #L1 #L2 #H elim H -f -L1 -L2
[ #f #H0f #f1 #f2 #Hf #Hf1 @(ex2_intro … (⋆)) @drops_atom
#H lapply (H0f H) -b
- #H elim (after_inv_isid3 … Hf H) -f //
-| #f #I #L1 #L2 #HL12 #IHL12 #f1 #f2 #Hf #Hf1 elim (after_inv_xxn … Hf) -Hf [1,3: * |*: // ]
+ #H elim (pr_after_inv_isi … Hf H) -f //
+| #f #I #L1 #L2 #HL12 #IHL12 #f1 #f2 #Hf #Hf1 elim (pr_after_inv_next … Hf) -Hf [1,3: * |*: // ]
[ #g1 #g2 #Hf #H1 #H2 destruct
- lapply (isuni_inv_push … Hf1 ??) -Hf1 [1,2: // ] #Hg1
+ lapply (pr_isu_inv_push … Hf1 ??) -Hf1 [1,2: // ] #Hg1
elim (IHL12 … Hf) -f
- /4 width=5 by drops_drop, drops_skip, liftsb_refl, isuni_isid, ex2_intro/
+ /4 width=5 by drops_drop, drops_skip, liftsb_refl, pr_isu_isi, ex2_intro/
| #g1 #Hf #H destruct elim (IHL12 … Hf) -f
- /3 width=5 by ex2_intro, drops_drop, isuni_inv_next/
+ /3 width=5 by ex2_intro, drops_drop, pr_isu_inv_next/
]
-| #f #I1 #I2 #L1 #L2 #_ #HI21 #IHL12 #f1 #f2 #Hf #Hf1 elim (after_inv_xxp … Hf) -Hf [2,3: // ]
+| #f #I1 #I2 #L1 #L2 #_ #HI21 #IHL12 #f1 #f2 #Hf #Hf1 elim (pr_after_inv_push … Hf) -Hf [2,3: // ]
#g1 #g2 #Hf #H1 #H2 destruct elim (liftsb_split_trans … HI21 … Hf) -HI21
- elim (IHL12 … Hf) -f /3 width=5 by ex2_intro, drops_skip, isuni_fwd_push/
+ elim (IHL12 … Hf) -f /3 width=5 by ex2_intro, drops_skip, pr_isu_fwd_push/
]
qed-.
∃∃L2. ⇩*[Ⓕ,f2] L ≘ L2 & ⇩*[Ⓕ,f] L1 ≘ L2.
#b #f1 #L1 #L #H elim H -f1 -L1 -L
[ #f1 #Hf1 #f2 #f #Hf #Hf2 @(ex2_intro … (⋆)) @drops_atom #H destruct
-| #f1 #I #L1 #L #HL1 #IH #f2 #f #Hf #Hf2 elim (after_inv_nxx … Hf) -Hf [2,3: // ]
+| #f1 #I #L1 #L #HL1 #IH #f2 #f #Hf #Hf2 elim (pr_after_inv_next_sn … Hf) -Hf [2,3: // ]
#g #Hg #H destruct elim (IH … Hg) -IH -Hg /3 width=5 by drops_drop, ex2_intro/
| #f1 #I1 #I #L1 #L #HL1 #HI1 #IH #f2 #f #Hf #Hf2
- elim (after_inv_pxx … Hf) -Hf [1,3: * |*: // ]
+ elim (pr_after_inv_push_sn … Hf) -Hf [1,3: * |*: // ]
#g2 #g #Hg #H2 #H0 destruct
- [ lapply (isuni_inv_push … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -IH
- lapply (after_isid_inv_dx … Hg … Hg2) -Hg #Hg
- /5 width=7 by drops_eq_repl_back, drops_F, drops_refl, drops_skip, liftsb_eq_repl_back, isid_push, ex2_intro/
- | lapply (isuni_inv_next … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -HL1 -HI1
+ [ lapply (pr_isu_inv_push … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -IH
+ lapply (pr_after_isi_inv_dx … Hg … Hg2) -Hg #Hg
+ /5 width=7 by drops_eq_repl_back, drops_F, drops_refl, drops_skip, liftsb_eq_repl_back, pr_isi_push, ex2_intro/
+ | lapply (pr_isu_inv_next … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -HL1 -HI1
elim (IH … Hg) -f1 /3 width=3 by drops_drop, ex2_intro/
]
]
lemma drops_tls_at: ∀f,i1,i2. @❪i1,f❫ ≘ i2 →
∀b,L1,L2. ⇩*[b,⫰*[i2]f] L1 ≘ L2 →
⇩*[b,⫯⫰*[↑i2]f] L1 ≘ L2.
-/3 width=3 by drops_eq_repl_fwd, at_inv_tls/ qed-.
+/3 width=3 by drops_eq_repl_fwd, pr_pat_inv_succ_dx_tls/ qed-.
lemma drops_split_trans_bind2: ∀b,f,I,L,K0. ⇩*[b,f] L ≘ K0.ⓘ[I] → ∀i. @❪O,f❫ ≘ i →
∃∃J,K. ⇩[i]L ≘ K.ⓘ[J] & ⇩*[b,⫰*[↑i]f] K ≘ K0 & ⇧*[⫰*[↑i]f] I ≘ J.
#b #f #I #L #K0 #H #i #Hf
-elim (drops_split_trans … H) -H [ |5: @(after_uni_dx … Hf) |2,3: skip ] /2 width=1 by after_isid_dx/ #Y #HLY #H
+elim (drops_split_trans … H) -H [ |5: @(pr_after_nat_uni … Hf) |2,3: skip ] /2 width=1 by pr_after_isi_dx/ #Y #HLY #H
lapply (drops_tls_at … Hf … H) -H #H
elim (drops_inv_skip2 … H) -H #J #K #HK0 #HIJ #H destruct
/3 width=5 by drops_inv_gen, ex3_2_intro/
#b1 #f1 #L1 #L #H elim H -f1 -L1 -L
[ #f1 #_ #b2 #f #L2 #HL2 #f2 #Hf12 elim (drops_inv_atom1 … HL2) -b1 -HL2
#H #Hf destruct @drops_atom
- #H elim (after_inv_isid3 … Hf12) -Hf12 /2 width=1 by/
-| #f1 #I1 #K1 #K #_ #IH #b2 #f #L2 #HL2 #f2 #Hf elim (after_inv_nxx … Hf) -Hf [2,3: // ]
+ #H elim (pr_after_inv_isi … Hf12) -Hf12 /2 width=1 by/
+| #f1 #I1 #K1 #K #_ #IH #b2 #f #L2 #HL2 #f2 #Hf elim (pr_after_inv_next_sn … Hf) -Hf [2,3: // ]
#g #Hg #H destruct /3 width=3 by drops_inv_drop1/
-| #f1 #I1 #I #K1 #K #_ #HI1 #IH #b2 #f #L2 #HL2 #f2 #Hf elim (after_inv_pxx … Hf) -Hf [1,3: * |*:// ]
+| #f1 #I1 #I #K1 #K #_ #HI1 #IH #b2 #f #L2 #HL2 #f2 #Hf elim (pr_after_inv_push_sn … Hf) -Hf [1,3: * |*:// ]
#g2 #g #Hf #H1 #H2 destruct
[ elim (drops_inv_skip1 … HL2) -HL2 /3 width=6 by drops_skip, liftsb_div3/
| /4 width=3 by drops_inv_drop1, drops_drop/
#b1 #f1 #L1 #L #H elim H -f1 -L1 -L
[ #f1 #Hf1 #b2 #f2 #L2 #HL2 #f #Hf elim (drops_inv_atom1 … HL2) -HL2
#H #Hf2 destruct @drops_atom #H elim (andb_inv_true_dx … H) -H
- #H1 #H2 lapply (after_isid_inv_sn … Hf ?) -Hf
- /3 width=3 by isid_eq_repl_back/
-| #f1 #I1 #K1 #K #_ #IH #b2 #f2 #L2 #HL2 #f #Hf elim (after_inv_nxx … Hf) -Hf
+ #H1 #H2 lapply (pr_after_isi_inv_sn … Hf ?) -Hf
+ /3 width=3 by pr_isi_eq_repl_back/
+| #f1 #I1 #K1 #K #_ #IH #b2 #f2 #L2 #HL2 #f #Hf elim (pr_after_inv_next_sn … Hf) -Hf
/3 width=3 by drops_drop/
-| #f1 #I1 #I #K1 #K #_ #HI1 #IH #b2 #f2 #L2 #HL2 #f #Hf elim (after_inv_pxx … Hf) -Hf [1,3: * |*: // ]
+| #f1 #I1 #I #K1 #K #_ #HI1 #IH #b2 #f2 #L2 #HL2 #f #Hf elim (pr_after_inv_push_sn … Hf) -Hf [1,3: * |*: // ]
#g2 #g #Hg #H1 #H2 destruct
[ elim (drops_inv_skip1 … HL2) -HL2 /3 width=6 by drops_skip, liftsb_trans/
| /4 width=3 by drops_inv_drop1, drops_drop/
𝐔❪f1❫ → 𝐔❪f2❫ → f1 ≡ f2.
#f1 #L #K #H elim H -f1 -L -K
[ #f1 #Hf1 #f2 #Hf2 elim (drops_inv_atom1 … Hf2) -Hf2
- /3 width=1 by isid_inv_eq_repl/
-| #f1 #I #L #K #Hf1 #IH #f2 elim (pn_split f2) *
+ /3 width=1 by pr_isi_inv_eq_repl/
+| #f1 #I #L #K #Hf1 #IH #f2 elim (pr_map_split_tl f2) *
#g2 #H2 #Hf2 #HU1 #HU2 destruct
[ elim (drops_inv_skip1 … Hf2) -IH -HU1 -Hf2 #Y2 #X2 #HY2 #_ #H destruct
- lapply (drops_fwd_isid … HY2 ?) -HY2 /2 width=3 by isuni_inv_push/ -HU2
+ lapply (drops_fwd_isid … HY2 ?) -HY2 /2 width=3 by pr_isu_inv_push/ -HU2
#H destruct elim (drops_inv_x_bind_xy … Hf1)
- | /4 width=5 by drops_inv_drop1, isuni_inv_next, eq_next/
+ | /4 width=5 by drops_inv_drop1, pr_isu_inv_next, pr_eq_next/
]
-| #f1 #I1 #I2 #L #K #Hf1 #_ #IH #f2 elim (pn_split f2) *
+| #f1 #I1 #I2 #L #K #Hf1 #_ #IH #f2 elim (pr_map_split_tl f2) *
#g2 #H2 #Hf2 #HU1 #HU2 destruct
[ elim (drops_inv_skip1 … Hf2) -Hf2 #Y2 #X2 #HY2 #_ #H destruct -Hf1
- /4 width=5 by isuni_fwd_push, eq_push/
+ /4 width=5 by pr_isu_fwd_push, pr_eq_push/
| lapply (drops_inv_drop1 … Hf2) -Hf2 -IH -HU2 #Hg2
- lapply (drops_fwd_isid … Hf1 ?) -Hf1 /2 width=3 by isuni_inv_push/ -HU1
+ lapply (drops_fwd_isid … Hf1 ?) -Hf1 /2 width=3 by pr_isu_inv_push/ -HU1
#H destruct elim (drops_inv_x_bind_xy … Hg2)
]
]
(* Basic_2A1: includes: drop_mono *)
lemma drops_mono: ∀b1,f,L,L1. ⇩*[b1,f] L ≘ L1 →
∀b2,L2. ⇩*[b2,f] L ≘ L2 → L1 = L2.
-#b1 #f #L #L1 lapply (after_isid_dx 𝐢 … f)
+#b1 #f #L #L1 lapply (pr_after_isi_dx 𝐢 … f)
/3 width=8 by drops_conf, drops_fwd_isid/
qed-.
#f1 #f2 #I1 #I2 #L #K #Hf1 #Hf2 #HU1 #HU2
lapply (drops_isuni_fwd_drop2 … Hf1) // #H1
lapply (drops_isuni_fwd_drop2 … Hf2) // #H2
-lapply (drops_conf_div_isuni … H1 … H2 ??) /2 width=3 by isuni_next/ -H1 -H2 -HU1 -HU2 #H
+lapply (drops_conf_div_isuni … H1 … H2 ??) /2 width=3 by pr_isu_next/ -H1 -H2 -HU1 -HU2 #H
lapply (eq_inv_nn … H ????) -H [5: |*: // ] #H12
lapply (drops_eq_repl_back … Hf1 … H12) -Hf1 #H0
lapply (drops_mono … H0 … Hf2) -L #H
(* Basic_2A1: includes: drop_fwd_length_le4 *)
lemma drops_fwd_length_le4: ∀b,f,L1,L2. ⇩*[b,f] L1 ≘ L2 → |L2| ≤ |L1|.
-#b #f #L1 #L2 #H elim H -f -L1 -L2 /2 width=1 by le_S, le_S_S/
+#b #f #L1 #L2 #H elim H -f -L1 -L2 /2 width=1 by nle_succ_dx, nle_succ_bi/
qed-.
(* Basic_2A1: includes: drop_fwd_length_eq1 *)
lemma drops_fwd_fcla: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 →
∃∃n. 𝐂❪f❫ ≘ n & |L1| = |L2| + n.
#f #L1 #L2 #H elim H -f -L1 -L2
-[ /4 width=3 by fcla_isid, ex2_intro/
-| #f #I #L1 #L2 #_ * >length_bind /3 width=3 by fcla_next, ex2_intro, eq_f/
-| #f #I1 #I2 #L1 #L2 #_ #_ * >length_bind >length_bind /3 width=3 by fcla_push, ex2_intro/
+[ /4 width=3 by pr_fcla_isi, ex2_intro/
+| #f #I #L1 #L2 #_ * >length_bind /3 width=3 by pr_fcla_next, ex2_intro, eq_f/
+| #f #I1 #I2 #L1 #L2 #_ #_ * >length_bind >length_bind /3 width=3 by pr_fcla_push, ex2_intro/
]
qed-.
lemma drops_fcla_fwd: ∀f,L1,L2,n. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐂❪f❫ ≘ n →
|L1| = |L2| + n.
#f #l1 #l2 #n #Hf #Hn elim (drops_fwd_fcla … Hf) -Hf
-#k #Hm #H <(fcla_mono … Hm … Hn) -f //
+#k #Hm #H <(pr_fcla_mono … Hm … Hn) -f //
qed-.
lemma drops_fwd_fcla_le2: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 →
lemma drops_fcla_fwd_le2: ∀f,L1,L2,n. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐂❪f❫ ≘ n →
n ≤ |L1|.
#f #L1 #L2 #n #H #Hn elim (drops_fwd_fcla_le2 … H) -H
-#k #Hm #H <(fcla_mono … Hm … Hn) -f //
+#k #Hm #H <(pr_fcla_mono … Hm … Hn) -f //
qed-.
lemma drops_fwd_fcla_lt2: ∀f,L1,I2,K2. ⇩*[Ⓣ,f] L1 ≘ K2.ⓘ[I2] →
∃∃n. 𝐂❪f❫ ≘ n & n < |L1|.
#f #L1 #I2 #K2 #H elim (drops_fwd_fcla … H) -H
-#n #Hf #H >H -L1 /3 width=3 by le_S_S, ex2_intro/
+#n #Hf #H >H -L1 /3 width=3 by nle_succ_bi, ex2_intro/
qed-.
(* Basic_2A1: includes: drop_fwd_length_lt2 *)
⇩*[Ⓣ,f] L1 ≘ K2.ⓘ[I2] → 𝐂❪f❫ ≘ n →
n < |L1|.
#f #L1 #I2 #K2 #n #H #Hn elim (drops_fwd_fcla_lt2 … H) -H
-#k #Hm #H <(fcla_mono … Hm … Hn) -f //
+#k #Hm #H <(pr_fcla_mono … Hm … Hn) -f //
qed-.
(* Basic_2A1: includes: drop_fwd_length_lt4 *)
lemma drops_fcla_fwd_lt4: ∀f,L1,L2,n. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐂❪f❫ ≘ n → 0 < n →
|L2| < |L1|.
#f #L1 #L2 #n #H #Hf #Hn lapply (drops_fcla_fwd … H Hf) -f
-/2 width=1 by lt_minus_to_plus_r/ qed-.
+/2 width=1 by nlt_inv_minus_dx/ qed-.
(* Basic_2A1: includes: drop_inv_length_eq *)
lemma drops_inv_length_eq: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 → |L1| = |L2| → 𝐈❪f❫.
#f #L1 #L2 #H #HL12 elim (drops_fwd_fcla … H) -H
-#n #Hn <HL12 -L2 #H lapply (discr_plus_x_xy … H) -H
-/2 width=3 by fcla_inv_xp/
+#n #Hn <HL12 -L2 #H lapply (nplus_refl_sn … H) -H
+/2 width=3 by pr_fcla_inv_zero/
qed-.
(* Basic_2A1: includes: drop_fwd_length_eq2 *)
#f #L1 #L2 #K1 #K2 #HLK1 #HLK2 #HL12
elim (drops_fwd_fcla … HLK1) -HLK1 #n1 #Hn1 #H1 >H1 -L1
elim (drops_fwd_fcla … HLK2) -HLK2 #n2 #Hn2 #H2 >H2 -L2
-<(fcla_mono … Hn2 … Hn1) -f //
+<(pr_fcla_mono … Hn2 … Hn1) -f //
qed-.
theorem drops_conf_div: ∀f1,f2,L1,L2. ⇩*[Ⓣ,f1] L1 ≘ L2 → ⇩*[Ⓣ,f2] L1 ≘ L2 →
#f1 #f2 #L1 #L2 #H1 #H2
elim (drops_fwd_fcla … H1) -H1 #n1 #Hf1 #H1
elim (drops_fwd_fcla … H2) -H2 #n2 #Hf2 >H1 -L1 #H
-lapply (injective_plus_r … H) -L2 #H destruct /2 width=3 by ex2_intro/
+lapply (eq_inv_nplus_bi_sn … H) -L2 #H destruct /2 width=3 by ex2_intro/
qed-.
theorem drops_conf_div_fcla: ∀f1,f2,L1,L2,n1,n2.
#f1 #f2 #L1 #L2 #n1 #n2 #Hf1 #Hf2 #Hn1 #Hn2
lapply (drops_fcla_fwd … Hf1 Hn1) -f1 #H1
lapply (drops_fcla_fwd … Hf2 Hn2) -f2 >H1 -L1
-/2 width=1 by injective_plus_r/
+/2 width=1 by eq_inv_nplus_bi_sn/
qed-.
d_liftable2_sn … lifts R → dedropable_sn R.
#R #H1R #H2R #b #f #L1 #K1 #HLK1 #K2 * #f1 #Hf1 #HK12
elim (sex_liftable_co_dedropable_sn … HLK1 … HK12) -K1
-/3 width=6 by cext2_d_liftable2_sn, cfull_lift_sn, ext2_refl, coafter_isid_dx, ex3_intro, ex2_intro/
+/3 width=6 by cext2_d_liftable2_sn, cfull_lift_sn, ext2_refl, pr_coafter_isi_dx, ex3_intro, ex2_intro/
qed-.
(* Inversion lemmas with generic extension **********************************)
lemma lex_dropable_sn (R): dropable_sn R.
#R #b #f #L1 #K1 #HLK1 #H1f #L2 * #f2 #Hf2 #HL12
elim (sex_co_dropable_sn … HLK1 … HL12) -L1
-/3 width=3 by coafter_isid_dx, ex2_intro/
+/3 width=3 by pr_coafter_isi_dx, ex2_intro/
qed-.
(* Basic_2A1: was: lpx_sn_dropable *)
lemma lex_dropable_dx (R): dropable_dx R.
#R #L1 #L2 * #f2 #Hf2 #HL12 #b #f #K2 #HLK2 #Hf
elim (sex_co_dropable_dx … HL12 … HLK2) -L2
-/3 width=5 by coafter_isid_dx, ex2_intro/
+/3 width=5 by pr_coafter_isi_dx, ex2_intro/
qed-.
(* Basic_2A1: includes: lpx_sn_drop_conf *)
[ #Z2 #K2 #HLK2 #HK12 #H
elim (ext2_inv_pair_sn … H) -H #V2 #HV12 #H destruct
/3 width=5 by ex3_2_intro, ex2_intro/
-| /3 width=3 by coafter_isid_dx, isid_push/
+| /3 width=3 by pr_coafter_isi_dx, pr_isi_push/
]
qed-.
[ #Z1 #K1 #HLK1 #HK12 #H
elim (ext2_inv_pair_dx … H) -H #V1 #HV12 #H destruct
/3 width=5 by ex3_2_intro, ex2_intro/
-| /3 width=3 by coafter_isid_dx, isid_push/
+| /3 width=3 by pr_coafter_isi_dx, pr_isi_push/
]
qed-.
[ #f #Hf #_ #f2 #X #H #f1 #Hf2 >(sex_inv_atom1 … H) -X
/4 width=3 by sex_atom, drops_atom, ex2_intro/
| #f #I1 #L1 #K1 #_ #IH #Hf #f2 #X #H #f1 #Hf2
- elim (coafter_inv_nxx … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H2 destruct
+ elim (pr_coafter_inv_next_sn … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H2 destruct
elim (sex_inv_push1 … H) -H #I2 #L2 #HL12 #HI12 #H destruct
elim (IH … HL12 … Hg2) -g2
- /3 width=3 by isuni_inv_next, drops_drop, ex2_intro/
+ /3 width=3 by pr_isu_inv_next, drops_drop, ex2_intro/
| #f #I1 #J1 #L1 #K1 #HLK #HJI1 #IH #Hf #f2 #X #H #f1 #Hf2
- lapply (isuni_inv_push … Hf ??) -Hf [3: |*: // ] #Hf
+ lapply (pr_isu_inv_push … Hf ??) -Hf [3: |*: // ] #Hf
lapply (drops_fwd_isid … HLK … Hf) -HLK #H0 destruct
lapply (liftsb_fwd_isid … HJI1 … Hf) -HJI1 #H0 destruct
- elim (coafter_inv_pxx … Hf2) -Hf2 [1,3:* |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct
+ elim (pr_coafter_inv_push_sn … Hf2) -Hf2 [1,3:* |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct
[ elim (sex_inv_push1 … H) | elim (sex_inv_next1 … H) ] -H #I2 #L2 #HL12 #HI12 #H destruct
- elim (IH … HL12 … Hg2) -g2 -IH /2 width=1 by isuni_isid/ #K2 #HK12 #HLK2
+ elim (IH … HL12 … Hg2) -g2 -IH /2 width=1 by pr_isu_isi/ #K2 #HK12 #HLK2
lapply (drops_fwd_isid … HLK2 … Hf) -HLK2 #H0 destruct
- /4 width=3 by drops_refl, sex_next, sex_push, isid_push, ex2_intro/
+ /4 width=3 by drops_refl, sex_next, sex_push, pr_isi_push, ex2_intro/
]
qed-.
f ~⊚ f1 ≘ f2 → L1 ⪤[RN,RP,f2] L2.
#RN #RP #HRN #HRP #f2 #L1 #L2 #H elim H -f2 -L1 -L2 //
#g2 #I1 #I2 #L1 #L2 #HL12 #HI12 #IH #f1 #Y1 #Y2 #HK12 #b #f #HY1 #HY2 #H
-[ elim (coafter_inv_xxn … H) [ |*: // ] -H #g #g1 #Hg2 #H1 #H2 destruct
+[ elim (pr_coafter_inv_next … H) [ |*: // ] -H #g #g1 #Hg2 #H1 #H2 destruct
elim (drops_inv_skip1 … HY1) -HY1 #J1 #K1 #HLK1 #HJI1 #H destruct
elim (drops_inv_skip1 … HY2) -HY2 #J2 #K2 #HLK2 #HJI2 #H destruct
elim (sex_inv_next … HK12) -HK12 #HK12 #HJ12
elim (HRN … HJ12 … HLK1 … HJI1) -HJ12 -HJI1 #Z #Hz
>(liftsb_mono … Hz … HJI2) -Z /3 width=9 by sex_next/
-| elim (coafter_inv_xxp … H) [1,2: |*: // ] -H *
+| elim (pr_coafter_inv_push … H) [1,2: |*: // ] -H *
[ #g #g1 #Hg2 #H1 #H2 destruct
elim (drops_inv_skip1 … HY1) -HY1 #J1 #K1 #HLK1 #HJI1 #H destruct
elim (drops_inv_skip1 … HY2) -HY2 #J2 #K2 #HLK2 #HJI2 #H destruct
[ #f #Hf #X #f1 #H #f2 #Hf2 >(sex_inv_atom1 … H) -X
/4 width=4 by drops_atom, sex_atom, ex3_intro/
| #f #I1 #L1 #K1 #_ #IHLK1 #K2 #f1 #HK12 #f2 #Hf2
- elim (coafter_inv_nxx … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H destruct
+ elim (pr_coafter_inv_next_sn … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H destruct
elim (IHLK1 … HK12 … Hg2) -K1
/3 width=6 by drops_drop, sex_next, sex_push, ex3_intro/
| #f #I1 #J1 #L1 #K1 #HLK1 #HJI1 #IHLK1 #X #f1 #H #f2 #Hf2
- elim (coafter_inv_pxx … Hf2) -Hf2 [1,3: * |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct
+ elim (pr_coafter_inv_push_sn … Hf2) -Hf2 [1,3: * |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct
[ elim (sex_inv_push1 … H) | elim (sex_inv_next1 … H) ] -H #J2 #K2 #HK12 #HJ12 #H destruct
[ elim (H2RP … HJ12 … HLK1 … HJI1) | elim (H2RN … HJ12 … HLK1 … HJI1) ] -J1
elim (IHLK1 … HK12 … Hg2) -K1
[ #f #Hf #_ #f2 #X #H #f1 #Hf2 lapply (sex_inv_atom2 … H) -H
#H destruct /4 width=3 by sex_atom, drops_atom, ex2_intro/
| #f #I2 #L2 #K2 #_ #IH #Hf #f2 #X #HX #f1 #Hf2
- elim (coafter_inv_nxx … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H destruct
+ elim (pr_coafter_inv_next_sn … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H destruct
elim (sex_inv_push2 … HX) -HX #I1 #L1 #HL12 #HI12 #H destruct
elim (IH … HL12 … Hg2) -L2 -I2 -g2
- /3 width=3 by drops_drop, isuni_inv_next, ex2_intro/
+ /3 width=3 by drops_drop, pr_isu_inv_next, ex2_intro/
| #f #I2 #J2 #L2 #K2 #_ #HJI2 #IH #Hf #f2 #X #HX #f1 #Hf2
- elim (coafter_inv_pxx … Hf2) -Hf2 [1,3: * |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct
+ elim (pr_coafter_inv_push_sn … Hf2) -Hf2 [1,3: * |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct
[ elim (sex_inv_push2 … HX) | elim (sex_inv_next2 … HX) ] -HX #I1 #L1 #HL12 #HI12 #H destruct
- elim (IH … HL12 … Hg2) -L2 -g2 /2 width=3 by isuni_fwd_push/ #K1 #HLK1 #HK12
- lapply (isuni_inv_push … Hf ??) -Hf [3,6: |*: // ] #Hf
+ elim (IH … HL12 … Hg2) -L2 -g2 /2 width=3 by pr_isu_fwd_push/ #K1 #HLK1 #HK12
+ lapply (pr_isu_inv_push … Hf ??) -Hf [3,6: |*: // ] #Hf
lapply (liftsb_fwd_isid … HJI2 … Hf) #H destruct -HJI2
lapply (drops_fwd_isid … HLK1 … Hf) #H destruct -HLK1
- /4 width=5 by sex_next, sex_push, drops_refl, isid_push, ex2_intro/
+ /4 width=5 by sex_next, sex_push, drops_refl, pr_isi_push, ex2_intro/
]
qed-.
[ #f1 #_ #L2 #H #f2 #_
lapply (sex_inv_atom1 … H) -H #H destruct
/2 width=3 by sex_atom, ex2_intro/
-| #K1 #I1 #IH #f1 elim (pn_split f1) * #g1 #H destruct
+| #K1 #I1 #IH #f1 elim (pr_map_split_tl f1) * #g1 #H destruct
#HR #L2 #H #f2 #Hf
[ elim (sex_inv_push1 … H) -H #I2 #K2 #HK12 #HI12 #H destruct
- elim (sdj_inv_px … Hf ??) -Hf [1,3: * |*: // ] #g2 #Hg #H destruct
+ elim (pr_sdj_inv_push_sn … Hf ??) -Hf [1,3: * |*: // ] #g2 #Hg #H destruct
elim (IH … HK12 … Hg) -IH -HK12 -Hg
[1,3: /3 width=5 by sex_next, sex_push, ex2_intro/
|2,4: /3 width=3 by drops_drop/
]
| elim (sex_inv_next1 … H) -H #I2 #K2 #HK12 #HI12 #H destruct
- elim (sdj_inv_nx … Hf ??) -Hf [|*: // ] #g2 #Hg #H destruct
+ elim (pr_sdj_inv_next_sn … Hf ??) -Hf [|*: // ] #g2 #Hg #H destruct
elim (IH … HK12 … Hg) -IH -HK12 -Hg
[ /5 width=11 by sex_next, sex_push, drops_refl, ex2_intro/
| /3 width=3 by drops_drop/
(* Basic_2A1: includes: drop_fwd_lw *)
lemma drops_fwd_lw: ∀b,f,L1,L2. ⇩*[b,f] L1 ≘ L2 → ♯❨L2❩ ≤ ♯❨L1❩.
#b #f #L1 #L2 #H elim H -f -L1 -L2 //
-[ /2 width=3 by transitive_le/
+[ /2 width=3 by nle_trans/
| #f #I1 #I2 #L1 #L2 #_ #HI21 #IHL12 normalize
- >(liftsb_fwd_bw … HI21) -HI21 /2 width=1 by monotonic_le_plus_l/
+ >(liftsb_fwd_bw … HI21) -HI21 /2 width=1 by nle_plus_bi_dx/
]
qed-.
(𝐈❪f❫ → ⊥) → ♯❨L2❩ < ♯❨L1❩.
#f #L1 #L2 #H elim H -f -L1 -L2
[ #f #Hf #Hnf elim Hnf -Hnf /2 width=1 by/
-| /3 width=3 by drops_fwd_lw, le_to_lt_to_lt/
+| /3 width=3 by drops_fwd_lw, nle_nlt_trans/
| #f #I1 #I2 #L1 #L2 #_ #HI21 #IHL12 #H normalize in ⊢ (?%%);
- >(liftsb_fwd_bw … HI21) -I2 /5 width=3 by isid_push, monotonic_lt_plus_l/
+ >(liftsb_fwd_bw … HI21) -I2 /5 width=3 by pr_isi_push, nlt_plus_bi_dx/
]
qed-.
(* Basic_2A1: includes: drop_fwd_rfw *)
lemma drops_bind2_fwd_rfw: ∀b,f,I,L,K,V. ⇩*[b,f] L ≘ K.ⓑ[I]V → ∀T. ♯❨K,V❩ < ♯❨L,T❩.
#b #f #I #L #K #V #HLK lapply (drops_fwd_lw … HLK) -HLK
-normalize in ⊢ (%→?→?%%); /3 width=3 by le_to_lt_to_lt, monotonic_lt_plus_r/
+normalize in ⊢ (%→?→?%%); /3 width=3 by nle_nlt_trans, nlt_plus_bi_sn/
qed-.
(* Advanced inversion lemma *************************************************)
lemma drops_inv_x_bind_xy: ∀b,f,I,L. ⇩*[b,f] L ≘ L.ⓘ[I] → ⊥.
#b #f #I #L #H lapply (drops_fwd_lw … H) -b -f
-/2 width=4 by lt_le_false/ (**) (* full auto is a bit slow: 19s *)
+/2 width=4 by nlt_ge_false/ (**) (* full auto is a bit slow: 19s *)
qed-.
lemma lex_bind (R): ∀I1,I2,K1,K2. K1 ⪤[R] K2 → cext2 R K1 I1 I2 →
K1.ⓘ[I1] ⪤[R] K2.ⓘ[I2].
#R #I1 #I2 #K1 #K2 * #f #Hf #HK12 #HI12
-/3 width=3 by sex_push, isid_push, ex2_intro/
+/3 width=3 by sex_push, pr_isi_push, ex2_intro/
qed.
(* Basic_2A1: was: lpx_sn_refl *)
lemma lex_inv_bind_sn (R): ∀I1,L2,K1. K1.ⓘ[I1] ⪤[R] L2 →
∃∃I2,K2. K1 ⪤[R] K2 & cext2 R K1 I1 I2 & L2 = K2.ⓘ[I2].
#R #I1 #L2 #K1 * #f #Hf #H
-lapply (sex_eq_repl_fwd … H (⫯f) ?) -H /2 width=1 by eq_push_inv_isid/ #H
+lapply (sex_eq_repl_fwd … H (⫯f) ?) -H /2 width=1 by pr_isi_inv_eq_push/ #H
elim (sex_inv_push1 … H) -H #I2 #K2 #HK12 #HI12 #H destruct
/3 width=5 by ex2_intro, ex3_2_intro/
qed-.
lemma lex_inv_bind_dx (R): ∀I2,L1,K2. L1 ⪤[R] K2.ⓘ[I2] →
∃∃I1,K1. K1 ⪤[R] K2 & cext2 R K1 I1 I2 & L1 = K1.ⓘ[I1].
#R #I2 #L1 #K2 * #f #Hf #H
-lapply (sex_eq_repl_fwd … H (⫯f) ?) -H /2 width=1 by eq_push_inv_isid/ #H
+lapply (sex_eq_repl_fwd … H (⫯f) ?) -H /2 width=1 by pr_isi_inv_eq_push/ #H
elim (sex_inv_push2 … H) -H #I1 #K1 #HK12 #HI12 #H destruct
/3 width=5 by ex3_2_intro, ex2_intro/
qed-.
∀L1,L2. L1 ⪤[R] L2 → Q L1 L2.
#R #Q #IH1 #IH2 #IH3 #L1 #L2 * #f @pull_2 #H
elim H -f -L1 -L2 // #f #I1 #I2 #K1 #K2 @pull_4 #H
-[ elim (isid_inv_next … H)
-| lapply (isid_inv_push … H ??)
+[ elim (pr_isi_inv_next … H)
+| lapply (pr_isi_inv_push … H ??)
] -H [5:|*: // ] #Hf @pull_2 #H
elim H -H /3 width=3 by ex2_intro/
qed-.
TC … (lex R) ⊆ lex (CTC … R).
#R #HR #L1 #L2 #HL12
lapply (monotonic_TC … (sex cfull (cext2 R) 𝐢) … HL12) -HL12
-[ #L1 #L2 * /3 width=3 by sex_eq_repl_fwd, eq_id_inv_isid/
+[ #L1 #L2 * /3 width=3 by sex_eq_repl_fwd, pr_isi_inv_eq_id/
| /5 width=9 by s_rs_transitive_lex_inv_isid, sex_tc_dx, sex_co, ext2_tc, ex2_intro/
]
qed-.
lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat
lifts_nil lifts_cons
*)
-inductive lifts: rtmap → relation term ≝
+inductive lifts: pr_map → relation term ≝
| lifts_sort: ∀f,s. lifts f (⋆s) (⋆s)
| lifts_lref: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → lifts f (#i1) (#i2)
| lifts_gref: ∀f,l. lifts f (§l) (§l)
'RLiftStar f T1 T2 = (lifts f T1 T2).
interpretation "uniform relocation (term)"
- 'RLift i T1 T2 = (lifts (uni i) T1 T2).
+ 'RLift i T1 T2 = (lifts (pr_uni i) T1 T2).
definition liftable2_sn: predicate (relation term) ≝
λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⇧*[f] T1 ≘ U1 →
∀X. ⇧*[⫯f]#0 ≘ X → #0 = X.
#f #X #H
elim (lifts_inv_lref1 … H) -H #i #Hi #H destruct
-lapply (at_inv_ppx … Hi ???) -Hi //
+lapply (pr_pat_inv_unit_push … Hi ???) -Hi //
qed-.
lemma lifts_inv_push_succ_sn (f) (i1):
∃∃i2. ⇧*[f]#i1 ≘ #i2 & #(↑i2) = X.
#f #i1 #X #H
elim (lifts_inv_lref1 … H) -H #j #Hij #H destruct
-elim (at_inv_npx … Hij) -Hij [|*: // ] #i2 #Hi12 #H destruct
+elim (pr_pat_inv_succ_push … Hij) -Hij [|*: // ] #i2 #Hi12 #H destruct
/3 width=3 by lifts_lref, ex2_intro/
qed-.
(* Inversion lemmas with uniform relocations ********************************)
lemma lifts_inv_lref1_uni: ∀l,Y,i. ⇧[l] #i ≘ Y → Y = #(l+i).
-#l #Y #i1 #H elim (lifts_inv_lref1 … H) -H /4 width=4 by at_mono, eq_f/
+#l #Y #i1 #H elim (lifts_inv_lref1 … H) -H /4 width=4 by fr2_nat_mono, eq_f/
qed-.
lemma lifts_inv_lref2_uni: ∀l,X,i2. ⇧[l] X ≘ #i2 →
∃∃i1. X = #i1 & i2 = l + i1.
#l #X #i2 #H elim (lifts_inv_lref2 … H) -H
-/3 width=3 by at_inv_uni, ex2_intro/
+/3 width=3 by pr_pat_inv_uni, ex2_intro/
qed-.
lemma lifts_inv_lref2_uni_ge: ∀l,X,i. ⇧[l] X ≘ #(l + i) → X = #i.
#l #X #i2 #H elim (lifts_inv_lref2_uni … H) -H
-#i1 #H1 #H2 destruct /4 width=2 by injective_plus_r, eq_f, sym_eq/
+#i1 #H1 #H2 destruct /4 width=2 by eq_inv_nplus_bi_sn, eq_f, sym_eq/
qed-.
lemma lifts_inv_lref2_uni_lt: ∀l,X,i. ⇧[l] X ≘ #i → i < l → ⊥.
#l #X #i2 #H elim (lifts_inv_lref2_uni … H) -H
-#i1 #_ #H1 #H2 destruct /2 width=4 by lt_le_false/
+#i1 #_ #H1 #H2 destruct /2 width=4 by nlt_ge_false/
qed-.
(* Basic forward lemmas *****************************************************)
(* Basic_2A1: includes: lift_inv_O2 *)
lemma lifts_fwd_isid: ∀f,T1,T2. ⇧*[f] T1 ≘ T2 → 𝐈❪f❫ → T1 = T2.
#f #T1 #T2 #H elim H -f -T1 -T2
-/4 width=3 by isid_inv_at_mono, isid_push, eq_f2, eq_f/
+/4 width=3 by pr_isi_pat_des, pr_isi_push, eq_f2, eq_f/
qed-.
(* Basic_2A1: includes: lift_fwd_pair1 *)
elim (H1R … U1 … HTU2) -H1R /3 width=3 by ex2_intro/
qed-.
-lemma lifts_eq_repl_back: ∀T1,T2. eq_repl_back … (λf. ⇧*[f] T1 ≘ T2).
+lemma lifts_eq_repl_back: ∀T1,T2. pr_eq_repl_back … (λf. ⇧*[f] T1 ≘ T2).
#T1 #T2 #f1 #H elim H -T1 -T2 -f1
-/4 width=5 by lifts_flat, lifts_bind, lifts_lref, at_eq_repl_back, eq_push/
+/4 width=5 by lifts_flat, lifts_bind, lifts_lref, pr_pat_eq_repl_back, pr_eq_push/
qed-.
-lemma lifts_eq_repl_fwd: ∀T1,T2. eq_repl_fwd … (λf. ⇧*[f] T1 ≘ T2).
-#T1 #T2 @eq_repl_sym /2 width=3 by lifts_eq_repl_back/ (**) (* full auto fails *)
+lemma lifts_eq_repl_fwd: ∀T1,T2. pr_eq_repl_fwd … (λf. ⇧*[f] T1 ≘ T2).
+#T1 #T2 @pr_eq_repl_sym /2 width=3 by lifts_eq_repl_back/ (**) (* full auto fails *)
qed-.
(* Basic_1: includes: lift_r *)
(* Basic_2A1: includes: lift_refl *)
lemma lifts_refl: ∀T,f. 𝐈❪f❫ → ⇧*[f] T ≘ T.
#T elim T -T *
-/4 width=3 by lifts_flat, lifts_bind, lifts_lref, isid_inv_at, isid_push/
+/4 width=3 by lifts_flat, lifts_bind, lifts_lref, pr_isi_inv_pat, pr_isi_push/
qed.
(* Basic_2A1: includes: lift_total *)
lemma lifts_push_lref (f) (i1) (i2): ⇧*[f]#i1 ≘ #i2 → ⇧*[⫯f]#(↑i1) ≘ #(↑i2).
#f1 #i1 #i2 #H
elim (lifts_inv_lref1 … H) -H #j #Hij #H destruct
-/3 width=7 by lifts_lref, at_push/
+/3 width=7 by lifts_lref, pr_pat_push/
qed.
lemma lifts_lref_uni: ∀l,i. ⇧[l] #i ≘ #(l+i).
∃∃T. ⇧*[f1] T1 ≘ T & ⇧*[f2] T ≘ T2.
#f #T1 #T2 #H elim H -f -T1 -T2
[ /3 width=3 by lifts_sort, ex2_intro/
-| #f #i1 #i2 #Hi #f1 #f2 #Ht elim (after_at_fwd … Hi … Ht) -Hi -Ht
+| #f #i1 #i2 #Hi #f1 #f2 #Ht elim (pr_after_pat_des … Hi … Ht) -Hi -Ht
/3 width=3 by lifts_lref, ex2_intro/
| /3 width=3 by lifts_gref, ex2_intro/
| #f #p #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f1 #f2 #Ht
∃∃T. ⇧*[f2] T2 ≘ T & ⇧*[f] T1 ≘ T.
#f1 #T1 #T2 #H elim H -f1 -T1 -T2
[ /3 width=3 by lifts_sort, ex2_intro/
-| #f1 #i1 #i2 #Hi #f2 #f #Ht elim (after_at1_fwd … Hi … Ht) -Hi -Ht
+| #f1 #i1 #i2 #Hi #f2 #f #Ht elim (pr_after_des_ist_pat … Hi … Ht) -Hi -Ht
/3 width=3 by lifts_lref, ex2_intro/
| /3 width=3 by lifts_gref, ex2_intro/
| #f1 #p #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f2 #f #Ht
lemma is_lifts_dec: ∀T2,f. Decidable (∃T1. ⇧*[f] T1 ≘ T2).
#T1 elim T1 -T1
[ * [1,3: /3 width=2 by lifts_sort, lifts_gref, ex_intro, or_introl/ ]
- #i2 #f elim (is_at_dec f i2) //
+ #i2 #f elim (is_pr_pat_dec f i2) //
[ * /4 width=3 by lifts_lref, ex_intro, or_introl/
| #H @or_intror *
#X #HX elim (lifts_inv_lref2 … HX) -HX
(* Properties with basic relocation *****************************************)
lemma lifts_lref_lt (m,n,i): i < m → ⇧[m,n] #i ≘ #i.
-/3 width=1 by lifts_lref, at_basic_lt/ qed.
+/3 width=1 by lifts_lref, pr_pat_basic_lt/ qed.
lemma lifts_lref_ge (m,n,i): m ≤ i → ⇧[m,n] #i ≘ #(n+i).
-/3 width=1 by lifts_lref, at_basic_ge/ qed.
+/3 width=1 by lifts_lref, pr_pat_basic_ge/ qed.
lemma lifts_lref_ge_minus (m,n,i): n+m ≤ i → ⇧[m,n] #(i-n) ≘ #i.
#m #n #i #Hi
->(plus_minus_m_m i n) in ⊢ (???%);
-/3 width=2 by lifts_lref_ge, le_plus_to_minus_l, le_plus_b/
+>(nplus_minus_sn_refl_sn i n) in ⊢ (???%);
+/3 width=2 by lifts_lref_ge, nle_minus_dx_dx, nle_inv_plus_sn_dx/
qed.
(* GENERIC RELOCATION FOR BINDERS *******************************************)
-definition liftsb: rtmap → relation bind ≝
+definition liftsb: pr_map → relation bind ≝
λf. ext2 (lifts f).
interpretation "generic relocation (binder for local environments)"
'RLiftStar f I1 I2 = (liftsb f I1 I2).
interpretation "uniform relocation (binder for local environments)"
- 'RLift i I1 I2 = (liftsb (uni i) I1 I2).
+ 'RLift i I1 I2 = (liftsb (pr_uni i) I1 I2).
(* Basic_inversion lemmas **************************************************)
(* Basic properties *********************************************************)
-lemma liftsb_eq_repl_back: ∀I1,I2. eq_repl_back … (λf. ⇧*[f] I1 ≘ I2).
+lemma liftsb_eq_repl_back: ∀I1,I2. pr_eq_repl_back … (λf. ⇧*[f] I1 ≘ I2).
#I1 #I2 #f1 * -I1 -I2 /3 width=3 by lifts_eq_repl_back, ext2_pair/
qed-.
(* Basic_1: includes: lift_gen_lift *)
(* Basic_2A1: includes: lift_div_le lift_div_be *)
theorem lifts_div4: ∀f2,Tf,T. ⇧*[f2] Tf ≘ T → ∀g2,Tg. ⇧*[g2] Tg ≘ T →
- ∀f1,g1. H_at_div f2 g2 f1 g1 →
+ ∀f1,g1. H_pr_pat_div f2 g2 f1 g1 →
∃∃T0. ⇧*[f1] T0 ≘ Tf & ⇧*[g1] T0 ≘ Tg.
#f2 #Tf #T #H elim H -f2 -Tf -T
[ #f2 #s #g2 #Tg #H #f1 #g1 #_
| #f2 #p #I #Vf #V #Tf #T #_ #_ #IHV #IHT #g2 #X #H #f1 #g1 #H0
elim (lifts_inv_bind2 … H) -H #Vg #Tg #HVg #HTg #H destruct
elim (IHV … HVg … H0) -IHV -HVg
- elim (IHT … HTg) -IHT -HTg [ |*: /2 width=8 by at_div_pp/ ]
+ elim (IHT … HTg) -IHT -HTg [ |*: /2 width=8 by pr_pat_div_push_bi/ ]
/3 width=5 by lifts_bind, ex2_intro/
| #f2 #I #Vf #V #Tf #T #_ #_ #IHV #IHT #g2 #X #H #f1 #g1 #H0
elim (lifts_inv_flat2 … H) -H #Vg #Tg #HVg #HTg #H destruct
lemma lifts_div4_one: ∀f,Tf,T. ⇧*[⫯f] Tf ≘ T →
∀T1. ⇧[1] T1 ≘ T →
∃∃T0. ⇧[1] T0 ≘ Tf & ⇧*[f] T0 ≘ T1.
-/4 width=6 by lifts_div4, at_div_id_dx, at_div_pn/ qed-.
+/4 width=6 by lifts_div4, pr_pat_div_id_dx, pr_pat_div_push_next/ qed-.
theorem lifts_div3: ∀f2,T,T2. ⇧*[f2] T2 ≘ T → ∀f,T1. ⇧*[f] T1 ≘ T →
∀f1. f2 ⊚ f1 ≘ f → ⇧*[f1] T1 ≘ T2.
#f2 #T #T2 #H elim H -f2 -T -T2
[ #f2 #s #f #T1 #H >(lifts_inv_sort2 … H) -T1 //
| #f2 #i2 #i #Hi2 #f #T1 #H #f1 #Ht21 elim (lifts_inv_lref2 … H) -H
- #i1 #Hi1 #H destruct /3 width=6 by lifts_lref, after_fwd_at1/
+ #i1 #Hi1 #H destruct /3 width=6 by lifts_lref, pr_after_des_pat_dx/
| #f2 #l #f #T1 #H >(lifts_inv_gref2 … H) -T1 //
| #f2 #p #I #W2 #W #U2 #U #_ #_ #IHW #IHU #f #T1 #H
elim (lifts_inv_bind2 … H) -H #W1 #U1 #HW1 #HU1 #H destruct
#f1 #T1 #T #H elim H -f1 -T1 -T
[ #f1 #s #f2 #T2 #H >(lifts_inv_sort1 … H) -T2 //
| #f1 #i1 #i #Hi1 #f2 #T2 #H #f #Ht21 elim (lifts_inv_lref1 … H) -H
- #i2 #Hi2 #H destruct /3 width=6 by lifts_lref, after_fwd_at/
+ #i2 #Hi2 #H destruct /3 width=6 by lifts_lref, pr_after_des_pat/
| #f1 #l #f2 #T2 #H >(lifts_inv_gref1 … H) -T2 //
| #f1 #p #I #W1 #W #U1 #U #_ #_ #IHW #IHU #f2 #T2 #H
elim (lifts_inv_bind1 … H) -H #W2 #U2 #HW2 #HU2 #H destruct
lemma lifts_trans4_one (f) (T1) (T2):
∀T. ⇧[1]T1 ≘ T → ⇧*[⫯f]T ≘ T2 →
∃∃T0. ⇧*[f]T1 ≘ T0 & ⇧[1]T0 ≘ T2.
-/4 width=6 by lifts_trans, lifts_split_trans, after_uni_one_dx/ qed-.
+/4 width=6 by lifts_trans, lifts_split_trans, pr_after_push_unit/ qed-.
(* Basic_2A1: includes: lift_conf_O1 lift_conf_be *)
theorem lifts_conf: ∀f1,T,T1. ⇧*[f1] T ≘ T1 → ∀f,T2. ⇧*[f] T ≘ T2 →
#f1 #T #T1 #H elim H -f1 -T -T1
[ #f1 #s #f #T2 #H >(lifts_inv_sort1 … H) -T2 //
| #f1 #i #i1 #Hi1 #f #T2 #H #f2 #Ht21 elim (lifts_inv_lref1 … H) -H
- #i2 #Hi2 #H destruct /3 width=6 by lifts_lref, after_fwd_at2/
+ #i2 #Hi2 #H destruct /3 width=6 by lifts_lref, pr_after_des_pat_sn/
| #f1 #l #f #T2 #H >(lifts_inv_gref1 … H) -T2 //
| #f1 #p #I #W #W1 #U #U1 #_ #_ #IHW #IHU #f #T2 #H
elim (lifts_inv_bind1 … H) -H #W2 #U2 #HW2 #HU2 #H destruct
(* Basic_2A1: includes: lift_inj *)
lemma lifts_inj: ∀f. is_inj2 … (lifts f).
-#f #T1 #U #H1 #T2 #H2 lapply (after_isid_dx 𝐢 … f)
+#f #T1 #U #H1 #T2 #H2 lapply (pr_after_isi_dx 𝐢 … f)
/3 width=6 by lifts_div3, lifts_fwd_isid/
qed-.
(* Basic_2A1: includes: lift_mono *)
lemma lifts_mono: ∀f,T. is_mono … (lifts f T).
-#f #T #U1 #H1 #U2 #H2 lapply (after_isid_sn 𝐢 … f)
+#f #T #U1 #H1 #U2 #H2 lapply (pr_after_isi_sn 𝐢 … f)
/3 width=6 by lifts_conf, lifts_fwd_isid/
qed-.
(* Advanced proprerties *****************************************************)
lemma liftsb_inj: ∀f. is_inj2 … (liftsb f).
-#f #T1 #U #H1 #T2 #H2 lapply (after_isid_dx 𝐢 … f)
+#f #T1 #U #H1 #T2 #H2 lapply (pr_after_isi_dx 𝐢 … f)
/3 width=6 by liftsb_div3, liftsb_fwd_isid/
qed-.
lemma liftsb_mono: ∀f,T. is_mono … (liftsb f T).
-#f #T #U1 #H1 #U2 #H2 lapply (after_isid_sn 𝐢 … f)
+#f #T #U1 #H1 #U2 #H2 lapply (pr_after_isi_sn 𝐢 … f)
/3 width=6 by liftsb_conf, liftsb_fwd_isid/
qed-.
| #j #f #X1 #H1 #X2 #H2
elim (lifts_inv_lref2 … H1) -H1 #i1 #Hj1 #H destruct
elim (lifts_inv_lref2 … H2) -H2 #i2 #Hj2 #H destruct
- <(at_inj … Hj2 … Hj1) -j -f -i1
+ <(pr_pat_inj … Hj2 … Hj1) -j -f -i1
/1 width=1 by teqo_lref/
| #l #f #X1 #H1 #X2 #H2
>(lifts_inv_gref2 … H1) -H1 >(lifts_inv_gref2 … H2) -H2
| #j #f #X1 #H1 #X2 #H2
elim (lifts_inv_lref2 … H1) -H1 #i1 #Hj1 #H destruct
elim (lifts_inv_lref2 … H2) -H2 #i2 #Hj2 #H destruct
- <(at_inj … Hj2 … Hj1) -j -f -i1
+ <(pr_pat_inj … Hj2 … Hj1) -j -f -i1
/1 width=1 by teqw_lref/
| #l #f #X1 #H1 #X2 #H2
>(lifts_inv_gref2 … H1) -H1 >(lifts_inv_gref2 … H2) -H2
lemma teqw_inv_abbr_pos_x_lifts_y_y (T) (f):
∀V,U. +ⓓV.U ≃ T → ⇧*[f]T ≘ U → ⊥.
-@(f_ind … tw) #n #IH #T #Hn #f #V #U #H1 #H2 destruct
+@(wf1_ind_nlt … tw) #n #IH #T #Hn #f #V #U #H1 #H2 destruct
elim (teqw_inv_abbr_pos_sn … H1) -H1 #X1 #X2 #HX2 #H destruct -V
elim (lifts_inv_bind1 … H2) -H2 #Y1 #Y2 #_ #HXY2 #H destruct
/2 width=7 by/
'RLiftStar f T1s T2s = (liftsv f T1s T2s).
interpretation "uniform relocation (term vector)"
- 'RLift i T1s T2s = (liftsv (uni i) T1s T2s).
+ 'RLift i T1s T2s = (liftsv (pr_uni i) T1s T2s).
(* Basic inversion lemmas ***************************************************)
(* SYNTACTIC EQUIVALENCE FOR SELECTED LOCAL ENVIRONMENTS ********************)
(* Basic_2A1: includes: lreq_atom lreq_zero lreq_pair lreq_succ *)
-definition seq: relation3 rtmap lenv lenv ≝
+definition seq: relation3 pr_map lenv lenv ≝
sex ceq_ext cfull.
interpretation
(* Basic properties *********************************************************)
lemma seq_eq_repl_back:
- ∀L1,L2. eq_repl_back … (λf. L1 ≡[f] L2).
+ ∀L1,L2. pr_eq_repl_back … (λf. L1 ≡[f] L2).
/2 width=3 by sex_eq_repl_back/ qed-.
lemma seq_eq_repl_fwd:
- ∀L1,L2. eq_repl_fwd … (λf. L1 ≡[f] L2).
+ ∀L1,L2. pr_eq_repl_fwd … (λf. L1 ≡[f] L2).
/2 width=3 by sex_eq_repl_fwd/ qed-.
lemma sle_seq_trans:
(* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
-inductive sex (RN,RP:relation3 lenv bind bind): rtmap → relation lenv ≝
+inductive sex (RN,RP:relation3 lenv bind bind): pr_map → relation lenv ≝
| sex_atom: ∀f. sex RN RP f (⋆) (⋆)
| sex_next: ∀f,I1,I2,L1,L2.
sex RN RP f L1 L2 → RN L1 I1 I2 →
relation3 lenv bind bind → relation3 lenv bind bind →
relation3 lenv bind bind →
relation3 lenv bind bind → relation3 lenv bind bind →
- relation3 rtmap lenv bind ≝
+ relation3 pr_map lenv bind ≝
λR1,R2,R3,RN,RP,f,L1,I1.
∀I. R1 L1 I1 I → ∀L2. L1 ⪤[RN,RP,f] L2 →
∀I2. R2 L2 I I2 → R3 L1 I1 I2.
definition R_pw_confluent1_sex:
relation3 lenv bind bind → relation3 lenv bind bind →
relation3 lenv bind bind → relation3 lenv bind bind →
- relation3 rtmap lenv bind ≝
+ relation3 pr_map lenv bind ≝
λR1,R2,RN,RP,f,L1,I1.
∀I2. R1 L1 I1 I2 → ∀L2. L1 ⪤[RN,RP,f] L2 → R2 L2 I1 I2.
relation3 lenv bind bind → relation3 lenv bind bind →
relation3 lenv bind bind → relation3 lenv bind bind →
relation3 lenv bind bind → relation3 lenv bind bind →
- relation3 rtmap lenv bind ≝
+ relation3 pr_map lenv bind ≝
λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0.
∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 →
∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 →
relation3 lenv bind bind → relation3 lenv bind bind →
relation3 lenv bind bind → relation3 lenv bind bind →
relation3 lenv bind bind → relation3 lenv bind bind →
- relation3 rtmap lenv bind ≝
+ relation3 pr_map lenv bind ≝
λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0.
∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 →
∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 →
∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & Y = K2.ⓘ[J2].
#RN #RP #f #X #Y * -f -X -Y
[ #f #g #J1 #K1 #H destruct
-| #f #I1 #I2 #L1 #L2 #HL #HI #g #J1 #K1 #H1 #H2 <(injective_next … H2) -g destruct
+| #f #I1 #I2 #L1 #L2 #HL #HI #g #J1 #K1 #H1 #H2 <(eq_inv_pr_next_bi … H2) -g destruct
/2 width=5 by ex3_2_intro/
-| #f #I1 #I2 #L1 #L2 #_ #_ #g #J1 #K1 #_ #H elim (discr_push_next … H)
+| #f #I1 #I2 #L1 #L2 #_ #_ #g #J1 #K1 #_ #H elim (eq_inv_pr_push_next … H)
]
qed-.
∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & Y = K2.ⓘ[J2].
#RN #RP #f #X #Y * -f -X -Y
[ #f #g #J1 #K1 #H destruct
-| #f #I1 #I2 #L1 #L2 #_ #_ #g #J1 #K1 #_ #H elim (discr_next_push … H)
-| #f #I1 #I2 #L1 #L2 #HL #HI #g #J1 #K1 #H1 #H2 <(injective_push … H2) -g destruct
+| #f #I1 #I2 #L1 #L2 #_ #_ #g #J1 #K1 #_ #H elim (eq_inv_pr_next_push … H)
+| #f #I1 #I2 #L1 #L2 #HL #HI #g #J1 #K1 #H1 #H2 <(eq_inv_pr_push_bi … H2) -g destruct
/2 width=5 by ex3_2_intro/
]
qed-.
∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & X = K1.ⓘ[J1].
#RN #RP #f #X #Y * -f -X -Y
[ #f #g #J2 #K2 #H destruct
-| #f #I1 #I2 #L1 #L2 #HL #HI #g #J2 #K2 #H1 #H2 <(injective_next … H2) -g destruct
+| #f #I1 #I2 #L1 #L2 #HL #HI #g #J2 #K2 #H1 #H2 <(eq_inv_pr_next_bi … H2) -g destruct
/2 width=5 by ex3_2_intro/
-| #f #I1 #I2 #L1 #L2 #_ #_ #g #J2 #K2 #_ #H elim (discr_push_next … H)
+| #f #I1 #I2 #L1 #L2 #_ #_ #g #J2 #K2 #_ #H elim (eq_inv_pr_push_next … H)
]
qed-.
∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & X = K1.ⓘ[J1].
#RN #RP #f #X #Y * -f -X -Y
[ #f #J2 #K2 #g #H destruct
-| #f #I1 #I2 #L1 #L2 #_ #_ #g #J2 #K2 #_ #H elim (discr_next_push … H)
-| #f #I1 #I2 #L1 #L2 #HL #HI #g #J2 #K2 #H1 #H2 <(injective_push … H2) -g destruct
+| #f #I1 #I2 #L1 #L2 #_ #_ #g #J2 #K2 #_ #H elim (eq_inv_pr_next_push … H)
+| #f #I1 #I2 #L1 #L2 #HL #HI #g #J2 #K2 #H1 #H2 <(eq_inv_pr_push_bi … H2) -g destruct
/2 width=5 by ex3_2_intro/
]
qed-.
∀f,I1,I2,L1,L2. L1 ⪤[RN,RP,⫰f] L2 →
RN L1 I1 I2 → RP L1 I1 I2 →
L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2].
-#RN #RP #f #I1 #I2 #L2 #L2 elim (pn_split f) *
+#RN #RP #f #I1 #I2 #L2 #L2 elim (pr_map_split_tl f) *
/2 width=1 by sex_next, sex_push/
qed-.
∀f,I1,I2,L1,L2.
L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2] → L1 ⪤[RN,RP,⫰f] L2.
#RN #RP #f #I1 #I2 #L1 #L2 #Hf
-elim (pn_split f) * #g #H destruct
+elim (pr_map_split_tl f) * #g #H destruct
[ elim (sex_inv_push … Hf) | elim (sex_inv_next … Hf) ] -Hf //
qed-.
(* Basic properties *********************************************************)
lemma sex_eq_repl_back (RN) (RP):
- ∀L1,L2. eq_repl_back … (λf. L1 ⪤[RN,RP,f] L2).
+ ∀L1,L2. pr_eq_repl_back … (λf. L1 ⪤[RN,RP,f] L2).
#RN #RP #L1 #L2 #f1 #H elim H -f1 -L1 -L2 //
#f1 #I1 #I2 #L1 #L2 #_ #HI #IH #f2 #H
[ elim (eq_inv_nx … H) -H /3 width=3 by sex_next/
qed-.
lemma sex_eq_repl_fwd (RN) (RP):
- ∀L1,L2. eq_repl_fwd … (λf. L1 ⪤[RN,RP,f] L2).
-#RN #RP #L1 #L2 @eq_repl_sym /2 width=3 by sex_eq_repl_back/ (**) (* full auto fails *)
+ ∀L1,L2. pr_eq_repl_fwd … (λf. L1 ⪤[RN,RP,f] L2).
+#RN #RP #L1 #L2 @pr_eq_repl_sym /2 width=3 by sex_eq_repl_back/ (**) (* full auto fails *)
qed-.
lemma sex_refl (RN) (RP):
c_reflexive … RN → c_reflexive … RP →
∀f.reflexive … (sex RN RP f).
#RN #RP #HRN #HRP #f #L generalize in match f; -f elim L -L //
-#L #I #IH #f elim (pn_split f) *
+#L #I #IH #f elim (pr_map_split_tl f) *
#g #H destruct /2 width=1 by sex_next, sex_push/
qed.
L1 ⪤[RN2,RP2,f] L2.
#RN1 #RP1 #RN2 #RP2 #HR #f #L1 #L2 #H elim H -f -L1 -L2 //
#f #I1 #I2 #K1 #K2 #_ #HI12 #IH #H
-[ elim (isid_inv_next … H) -H //
-| /4 width=3 by sex_push, isid_inv_push/
+[ elim (pr_isi_inv_next … H) -H //
+| /4 width=3 by sex_push, pr_isi_inv_push/
]
qed-.
∀f2. f1 ∥ f2 → L1 ⪤[RP,RN,f2] L2.
#RN #RP #HR #f1 #L1 #L2 #H elim H -f1 -L1 -L2 //
#f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H12
-[ elim (sdj_inv_nx … H12) -H12 [2,3: // ]
+[ elim (pr_sdj_inv_next_sn … H12) -H12 [2,3: // ]
#g2 #H #H2 destruct /3 width=1 by sex_push/
-| elim (sdj_inv_px … H12) -H12 [2,4: // ] *
+| elim (pr_sdj_inv_push_sn … H12) -H12 [2,4: // ] *
#g2 #H #H2 destruct /3 width=1 by sex_next, sex_push/
]
qed-.
∀f1. f1 ⊆ f2 → L1 ⪤[RN,RP,f1] L2.
#RN #RP #HR #f2 #L1 #L2 #H elim H -f2 -L1 -L2 //
#f2 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f1 #H12
-[ elim (pn_split f1) * ]
-[ /4 width=5 by sex_push, sle_inv_pn/
-| /4 width=5 by sex_next, sle_inv_nn/
-| elim (sle_inv_xp … H12) -H12 [2,3: // ]
+[ elim (pr_map_split_tl f1) * ]
+[ /4 width=5 by sex_push, pr_sle_inv_push_next/
+| /4 width=5 by sex_next, pr_sle_inv_next_bi/
+| elim (pr_sle_inv_push_dx … H12) -H12 [2,3: // ]
#g1 #H #H1 destruct /3 width=5 by sex_push/
]
qed-.
∀f2. f1 ⊆ f2 → L1 ⪤[RN,RP,f2] L2.
#RN #RP #HR #f1 #L1 #L2 #H elim H -f1 -L1 -L2 //
#f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H12
-[2: elim (pn_split f2) * ]
-[ /4 width=5 by sex_push, sle_inv_pp/
-| /4 width=5 by sex_next, sle_inv_pn/
-| elim (sle_inv_nx … H12) -H12 [2,3: // ]
+[2: elim (pr_map_split_tl f2) * ]
+[ /4 width=5 by sex_push, pr_sle_inv_push_bi/
+| /4 width=5 by sex_next, pr_sle_inv_push_next/
+| elim (pr_sle_inv_next_sn … H12) -H12 [2,3: // ]
#g2 #H #H2 destruct /3 width=5 by sex_next/
]
qed-.
#R1 #R2 #RP #HR1 #HR2 #f #L1 #L2 #H elim H -f -L1 -L2
[ /2 width=3 by sex_atom, ex2_intro/ ]
#f #I1 #I2 #L1 #L2 #_ #HI12 #IH #y #H
-[ elim (sle_inv_nx … H ??) -H [ |*: // ] #g #Hfg #H destruct
+[ elim (pr_sle_inv_next_sn … H ??) -H [ |*: // ] #g #Hfg #H destruct
elim (IH … Hfg) -IH -Hfg /3 width=5 by sex_next, ex2_intro/
-| elim (sle_inv_px … H ??) -H [1,3: * |*: // ] #g #Hfg #H destruct
+| elim (pr_sle_inv_push_sn … H ??) -H [1,3: * |*: // ] #g #Hfg #H destruct
elim (IH … Hfg) -IH -Hfg /3 width=5 by sex_next, sex_push, ex2_intro/
]
qed-.
#R1 #R2 #RP #HR1 #HR2 #f #L1 #L2 #H elim H -f -L1 -L2
[ /2 width=3 by sex_atom, ex2_intro/ ]
#f #I1 #I2 #L1 #L2 #_ #HI12 #IH #y #H
-[ elim (sdj_inv_nx … H ??) -H [ |*: // ] #g #Hfg #H destruct
+[ elim (pr_sdj_inv_next_sn … H ??) -H [ |*: // ] #g #Hfg #H destruct
elim (IH … Hfg) -IH -Hfg /3 width=5 by sex_next, sex_push, ex2_intro/
-| elim (sdj_inv_px … H ??) -H [1,3: * |*: // ] #g #Hfg #H destruct
+| elim (pr_sdj_inv_push_sn … H ??) -H [1,3: * |*: // ] #g #Hfg #H destruct
elim (IH … Hfg) -IH -Hfg /3 width=5 by sex_next, sex_push, ex2_intro/
]
qed-.
lapply (sex_inv_atom2 … H) -H #H destruct
| #L2 #I2 #f elim (IH L2 (⫰f)) -IH #HL12
[2: /4 width=3 by sex_fwd_bind, or_intror/ ]
- elim (pn_split f) * #g #H destruct
+ elim (pr_map_split_tl f) * #g #H destruct
[ elim (HRP L1 I1 I2) | elim (HRN L1 I1 I2) ] -HRP -HRN #HV12
[1,3: /3 width=1 by sex_push, sex_next, or_introl/ ]
@or_intror #H
[ #Y2 #H >(length_inv_zero_sn … H) -Y2 //
| #L1 #I1 #IH #Y2 #H #f
elim (length_inv_succ_sn … H) -H #I2 #L2 #HL12 #H destruct
- elim (pn_split f) * #g #H destruct /3 width=1 by sex_next, sex_push/
+ elim (pr_map_split_tl f) * #g #H destruct /3 width=1 by sex_next, sex_push/
]
qed.
[ #Y2 #H >(length_inv_zero_sn … H) -Y2 //
| #L1 #I1 #IH #Y2 #H #f #Hf
elim (length_inv_succ_sn … H) -H #I2 #L2 #HL12 #H destruct
- elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct /3 width=1 by sex_push/
+ elim (pr_isi_inv_gen … Hf) -Hf #g #Hg #H destruct /3 width=1 by sex_push/
]
qed.
lapply (sex_inv_atom1 … H1) -H1 #H destruct
lapply (sex_inv_atom1 … H2) -H2 #H destruct
/2 width=1 by sex_atom/
-| #K1 #I1 #IH #f elim (pn_split f) * #g #H destruct
+| #K1 #I1 #IH #f elim (pr_map_split_tl f) * #g #H destruct
#HN #HP #L0 #H1 #L2 #H2
[ elim (sex_inv_push1 … H1) -H1 #I0 #K0 #HK10 #HI10 #H destruct
elim (sex_inv_push1 … H2) -H2 #I2 #K2 #HK02 #HI02 #H destruct
#R1 #R2 #R3 #L1 #L #f #H elim H -L1 -L -f
[ #f #Hf #L2 #H >(sex_inv_atom1 … H) -L2 // ]
#f #I1 #I #K1 #K #HK1 #_ #IH #Hf #L2 #H
-[ elim (isid_inv_next … Hf) | lapply (isid_inv_push … Hf ??) ] -Hf [5: |*: // ] #Hf
+[ elim (pr_isi_inv_next … Hf) | lapply (pr_isi_inv_push … Hf ??) ] -Hf [5: |*: // ] #Hf
elim (sex_inv_push1 … H) -H #I2 #K2 #HK2 #_ #H destruct
/3 width=1 by sex_push/
qed-.
#RN1 #RP1 #RN2 #RP2 #L elim L -L
[ #f #_ #_ #L1 #H1 #L2 #H2 >(sex_inv_atom1 … H1) >(sex_inv_atom1 … H2) -H2 -H1
/2 width=3 by sex_atom, ex2_intro/
-| #L #I0 #IH #f elim (pn_split f) * #g #H destruct
+| #L #I0 #IH #f elim (pr_map_split_tl f) * #g #H destruct
#HN #HP #Y1 #H1 #Y2 #H2
[ elim (sex_inv_push1 … H1) -H1 #I1 #L1 #HL1 #HI01 #H destruct
elim (sex_inv_push1 … H2) -H2 #I2 #L2 #HL2 #HI02 #H destruct
lapply (sex_inv_atom1 … HY) -HY #H destruct
lapply (sex_inv_atom1 … HY1) -HY1 #H destruct
lapply (sex_inv_atom1 … HY2) -HY2 #H destruct //
-| #L1 #I1 #IH #f elim (pn_split f) * #g #H destruct
+| #L1 #I1 #IH #f elim (pr_map_split_tl f) * #g #H destruct
#HN #HP #Y #HY #Y1 #HY1 #Y2 #HY2
[ elim (sex_inv_push1 … HY) -HY #I2 #L2 #HL12 #HI12 #H destruct
elim (sex_inv_push1 … HY1) -HY1 #J1 #K1 #HLK1 #HIJ1 #H destruct
∀f. f1 ⋒ f2 ≘ f → L1 ⪤[RN,RP,f] L2.
#RN #RP #L1 #L2 #f1 #H elim H -f1 -L1 -L2 //
#f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H #f #Hf
-elim (pn_split f2) * #g2 #H2 destruct
+elim (pr_map_split_tl f2) * #g2 #H2 destruct
try elim (sex_inv_push … H) try elim (sex_inv_next … H) -H
-[ elim (sand_inv_npx … Hf) | elim (sand_inv_nnx … Hf)
-| elim (sand_inv_ppx … Hf) | elim (sand_inv_pnx … Hf)
+[ elim (pr_sand_inv_next_push … Hf) | elim (pr_sand_inv_next_bi … Hf)
+| elim (pr_sand_inv_push_bi … Hf) | elim (pr_sand_inv_push_next … Hf)
] -Hf /3 width=5 by sex_next, sex_push/
qed-.
∀f. f1 ⋓ f2 ≘ f → L1 ⪤[RN,RP,f] L2.
#RN #RP #L1 #L2 #f1 #H elim H -f1 -L1 -L2 //
#f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H #f #Hf
-elim (pn_split f2) * #g2 #H2 destruct
+elim (pr_map_split_tl f2) * #g2 #H2 destruct
try elim (sex_inv_push … H) try elim (sex_inv_next … H) -H
-[ elim (sor_inv_npx … Hf) | elim (sor_inv_nnx … Hf)
-| elim (sor_inv_ppx … Hf) | elim (sor_inv_pnx … Hf)
+[ elim (pr_sor_inv_next_push … Hf) | elim (pr_sor_inv_next_bi … Hf)
+| elim (pr_sor_inv_push_bi … Hf) | elim (pr_sor_inv_push_next … Hf)
] -Hf /3 width=5 by sex_next, sex_push/
qed-.
#RN #RP #HRP #f #L1 #L #H elim H -f -L1 -L
[ #f #_ #Y #H -HRP >(sex_inv_atom1 … H) -Y // ]
#f #I1 #I #L1 #L #HL1 #HI1 #IH #Hf #Y #H
-[ elim (isid_inv_next … Hf) -Hf //
-| lapply (isid_inv_push … Hf ??) -Hf [3: |*: // ] #Hf
+[ elim (pr_isi_inv_next … Hf) -Hf //
+| lapply (pr_isi_inv_push … Hf ??) -Hf [3: |*: // ] #Hf
elim (sex_inv_push1 … H) -H #I2 #L2 #HL2 #HI2 #H destruct
@sex_push [ /2 width=1 by/ ] -L2 -IH
@(TC_strap … HI1) -HI1
lemma fqup_fwd_fw: ∀b,G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂+[b] ❪G2,L2,T2❫ →
♯❨G2,L2,T2❩ < ♯❨G1,L1,T1❩.
#b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
-/3 width=3 by fqu_fwd_fw, transitive_lt/
+/3 width=3 by fqu_fwd_fw, nlt_trans/
qed-.
(* Advanced eliminators *****************************************************)
∀G1,L1,T1. (∀G2,L2,T2. ❪G1,L1,T1❫ ⬂+[b] ❪G2,L2,T2❫ → Q G2 L2 T2) →
Q G1 L1 T1
) → ∀G1,L1,T1. Q G1 L1 T1.
-#b #Q #HQ @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct
+#b #Q #HQ @(wf3_ind_nlt … fw) #x #IHx #G1 #L1 #T1 #H destruct
/4 width=2 by fqup_fwd_fw/
qed-.
∀G1,L1,T1. (∀G2,L2,T2. ❪G1,L1,T1❫ ⬂+[b] ❪G2,L2,T2❫ → Q G2 L2 T2) →
∀G2,L2,T2. G1 = G2 → L1 = L2 → T1 = T2 → Q G2 L2 T2
) → ∀G1,L1,T1. Q G1 L1 T1.
-#b #Q #HQ @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct
+#b #Q #HQ @(wf3_ind_nlt … fw) #x #IHx #G1 #L1 #T1 #H destruct
/4 width=7 by fqup_fwd_fw/
qed-.
lemma fqus_fwd_fw: ∀b,G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂*[b] ❪G2,L2,T2❫ →
♯❨G2,L2,T2❩ ≤ ♯❨G1,L1,T1❩.
#b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -L2 -T2
-/3 width=3 by fquq_fwd_fw, transitive_le/
+/3 width=3 by fquq_fwd_fw, nle_trans/
qed-.
(* Advanced inversion lemmas ************************************************)
lemma fqus_inv_refl_atom3: ∀b,I,G,L,X. ❪G,L,⓪[I]❫ ⬂*[b] ❪G,L,X❫ → ⓪[I] = X.
#b #I #G #L #X #H elim (fqus_inv_fqu_sn … H) -H * //
#G0 #L0 #T0 #H1 #H2 lapply (fqu_fwd_fw … H1) lapply (fqus_fwd_fw … H2) -H2 -H1
-#H2 #H1 lapply (le_to_lt_to_lt … H2 H1) -G0 -L0 -T0
-#H elim (lt_le_false … H) -H /2 width=1 by monotonic_le_plus_r/
+#H2 #H1 lapply (nle_nlt_trans … H2 H1) -G0 -L0 -T0
+#H elim (nlt_ge_false … H) -H /2 width=1 by nle_plus_bi_sn/
qed-.
∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T2❫ →
G1 = G2 → |L1| = |L2| → T1 ≛[S] T2 → ⊥.
#S #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
-[1: #I #G #L #V #_ #H elim (succ_inv_refl_sn … H)
-|6: #I #G #L #T #U #_ #_ #H elim (succ_inv_refl_sn … H)
+[1: #I #G #L #V #_ #H elim (nsucc_inv_refl … H)
+|6: #I #G #L #T #U #_ #_ #H elim (nsucc_inv_refl … H)
]
/2 width=6 by teqg_inv_pair_xy_y, teqg_inv_pair_xy_x/
qed-.
♯❨G2,L2,T2❩ < ♯❨G1,L1,T1❩.
#b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 //
#I #I1 #I2 #G #L #HI12 normalize in ⊢ (?%%); -I1
-<(lifts_fwd_tw … HI12) /3 width=1 by monotonic_lt_plus_r, monotonic_lt_plus_l/
+<(lifts_fwd_tw … HI12) /3 width=1 by nlt_plus_bi_sn, nlt_plus_bi_dx/
qed-.
(* Advanced eliminators *****************************************************)
∀G1,L1,T1. (∀G2,L2,T2. ❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T2❫ → Q G2 L2 T2) →
Q G1 L1 T1
) → ∀G1,L1,T1. Q G1 L1 T1.
-#b #Q #HQ @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct /4 width=2 by fqu_fwd_fw/
+#b #Q #HQ @(wf3_ind_nlt … fw) #x #IHx #G1 #L1 #T1 #H destruct /4 width=2 by fqu_fwd_fw/
qed-.
lemma fquq_fwd_length_lref1: ∀b,G1,G2,L1,L2,T2,i. ❪G1,L1,#i❫ ⬂⸮[b] ❪G2,L2,T2❫ →
|L2| ≤ |L1|.
#b #G1 #G2 #L1 #L2 #T2 #i #H elim H -H [2: * ]
-/3 width=6 by fqu_fwd_length_lref1, lt_to_le/
+/3 width=6 by fqu_fwd_length_lref1, nlt_des_le/
qed-.
lemma fquq_fwd_fw: ∀b,G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ⬂⸮[b] ❪G2,L2,T2❫ →
♯❨G2,L2,T2❩ ≤ ♯❨G1,L1,T1❩.
#b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H [2: * ]
-/3 width=2 by fqu_fwd_fw, lt_to_le/
+/3 width=2 by fqu_fwd_fw, nlt_des_le/
qed-.
#I #G #K #V #B #i elim i -i
[ #L #H lapply (drops_fwd_isid … H ?) -H //
#H destruct /2 width=1 by aaa_zero/
-| #i #IH #L <uni_succ #H #HB lapply (drops_inv_bind2_isuni_next … H) -H // *
+| #i #IH #L <pr_uni_succ #H #HB lapply (drops_inv_bind2_isuni_next … H) -H // *
#Z #Y #HY #H destruct /3 width=1 by aaa_lref/
]
qed.
elim (aaa_inv_lref_drops … H) -H #J #K1 #V1 #HLK1 #HA
elim (lifts_inv_lref1 … HX) -HX #i2 #Hf #H destruct
lapply (drops_trans … HL21 … HLK1 ??) -HL21 [1,2: // ] #H
- elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK2 #HY
+ elim (drops_split_trans … H) -H [ |*: /2 width=6 by pr_after_nat_uni/ ] #Y #HLK2 #HY
lapply (drops_tls_at … Hf … HY) -HY #HY -Hf
elim (drops_inv_skip2 … HY) -HY #Z #K2 #HK21 #HZ #H destruct
elim (liftsb_inv_pair_sn … HZ) -HZ #V2 #HV12 #H destruct
elim (aaa_inv_lref_drops … H) -H #J #K2 #V2 #HLK2 #HA
elim (lifts_inv_lref2 … HX) -HX #i1 #Hf #H destruct
lapply (drops_split_div … HL21 (𝐔❨i1❩) ???) -HL21 [4: * |*: // ] #Y #HLK1 #HY
- lapply (drops_conf … HLK2 … HY ??) -HY [1,2: /2 width=6 by after_uni_dx/ ] #HY
+ lapply (drops_conf … HLK2 … HY ??) -HY [1,2: /2 width=6 by pr_after_nat_uni/ ] #HY
lapply (drops_tls_at … Hf … HY) -HY #HY -Hf
elim (drops_inv_skip1 … HY) -HY #Z #K1 #HK21 #HZ #H destruct
elim (liftsb_inv_pair_dx … HZ) -HZ #V1 #HV12 #H destruct
lemma fqu_fneqg (S) (b) (G1) (G2) (L1) (L2) (T1) (T2):
❪G1,L1,T1❫ ⬂[b] ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → ⊥.
#S #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-[ /3 width=8 by feqg_fwd_length, succ_inv_refl_sn/
+[ /3 width=8 by feqg_fwd_length, nsucc_inv_refl/
| /3 width=9 by teqg_inv_pair_xy_x, feqg_fwd_teqg/
| /3 width=9 by teqg_inv_pair_xy_y, feqg_fwd_teqg/
| /3 width=9 by teqg_inv_pair_xy_y, feqg_fwd_teqg/
| /3 width=9 by teqg_inv_pair_xy_y, feqg_fwd_teqg/
-| /3 width=8 by feqg_fwd_length, succ_inv_refl_sn/
+| /3 width=8 by feqg_fwd_length, nsucc_inv_refl/
]
qed-.
(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
-inductive frees: relation3 lenv term rtmap ≝
+inductive frees: relation3 lenv term pr_map ≝
| frees_sort: ∀f,L,s. 𝐈❪f❫ → frees L (⋆s) f
| frees_atom: ∀f,i. 𝐈❪f❫ → frees (⋆) (#i) (⫯*[i]↑f)
| frees_pair: ∀f,I,L,V. frees L V f →
(* Basic properties ********************************************************)
-lemma frees_eq_repl_back: ∀L,T. eq_repl_back … (λf. L ⊢ 𝐅+❪T❫ ≘ f).
+lemma frees_eq_repl_back: ∀L,T. pr_eq_repl_back … (λf. L ⊢ 𝐅+❪T❫ ≘ f).
#L #T #f1 #H elim H -f1 -L -T
-[ /3 width=3 by frees_sort, isid_eq_repl_back/
+[ /3 width=3 by frees_sort, pr_isi_eq_repl_back/
| #f1 #i #Hf1 #g2 #H
- elim (eq_inv_pushs_sn … H) -H #g #Hg #H destruct
+ elim (pr_eq_inv_pushs_sn … H) -H #g #Hg #H destruct
elim (eq_inv_nx … Hg) -Hg
- /3 width=3 by frees_atom, isid_eq_repl_back/
+ /3 width=3 by frees_atom, pr_isi_eq_repl_back/
| #f1 #I #L #V #_ #IH #g2 #H
elim (eq_inv_nx … H) -H
/3 width=3 by frees_pair/
| #f1 #I #L #Hf1 #g2 #H
elim (eq_inv_nx … H) -H
- /3 width=3 by frees_unit, isid_eq_repl_back/
+ /3 width=3 by frees_unit, pr_isi_eq_repl_back/
| #f1 #I #L #i #_ #IH #g2 #H
elim (eq_inv_px … H) -H /3 width=3 by frees_lref/
-| /3 width=3 by frees_gref, isid_eq_repl_back/
-| /3 width=7 by frees_bind, sor_eq_repl_back3/
-| /3 width=7 by frees_flat, sor_eq_repl_back3/
+| /3 width=3 by frees_gref, pr_isi_eq_repl_back/
+| /3 width=7 by frees_bind, pr_sor_eq_repl_back/
+| /3 width=7 by frees_flat, pr_sor_eq_repl_back/
]
qed-.
-lemma frees_eq_repl_fwd: ∀L,T. eq_repl_fwd … (λf. L ⊢ 𝐅+❪T❫ ≘ f).
-#L #T @eq_repl_sym /2 width=3 by frees_eq_repl_back/
+lemma frees_eq_repl_fwd: ∀L,T. pr_eq_repl_fwd … (λf. L ⊢ 𝐅+❪T❫ ≘ f).
+#L #T @pr_eq_repl_sym /2 width=3 by frees_eq_repl_back/
qed-.
lemma frees_lref_push: ∀f,i. ⋆ ⊢ 𝐅+❪#i❫ ≘ f → ⋆ ⊢ 𝐅+❪#↑i❫ ≘ ⫯f.
lemma frees_fwd_isfin: ∀f,L,T. L ⊢ 𝐅+❪T❫ ≘ f → 𝐅❪f❫.
#f #L #T #H elim H -f -L -T
-/4 width=5 by sor_isfin, isfin_isid, isfin_tl, isfin_pushs, isfin_push, isfin_next/
+/4 width=5 by pr_sor_inv_isf_bi, pr_isf_isi, pr_isf_tl, pr_isf_pushs, pr_isf_push, pr_isf_next/
qed-.
(* Basic_2A1: removed theorems 30:
∀f2. f ~⊚ f1 ≘ f2 → L ⊢ 𝐅+❪U❫ ≘ f2.
#b #f1 #K #T #H lapply (frees_fwd_isfin … H) elim H -f1 -K -T
[ #f1 #K #s #Hf1 #_ #f #L #HLK #U #H2 #f2 #H3
- lapply (coafter_isid_inv_dx … H3 … Hf1) -f1 #Hf2
+ lapply (pr_coafter_isi_inv_dx … H3 … Hf1) -f1 #Hf2
>(lifts_inv_sort1 … H2) -U /2 width=1 by frees_sort/
| #f1 #i #Hf1 #_ #f #L #H1 #U #H2 #f2 #H3
elim (lifts_inv_lref1 … H2) -H2 #j #Hij #H destruct
elim (coafter_fwd_xnx_pushs … Hij H3) -H3 #g2 #Hg2 #H2 destruct
- lapply (coafter_isid_inv_dx … Hg2 … Hf1) -f1 #Hf2
+ lapply (pr_coafter_isi_inv_dx … Hg2 … Hf1) -f1 #Hf2
elim (drops_inv_atom2 … H1) -H1 #n #g #H1 #Hf
- elim (after_at_fwd … Hij … Hf) -f #x #_ #Hj -g -i
- lapply (at_inv_uni … Hj) -Hj #H destruct
+ elim (pr_after_pat_des … Hij … Hf) -f #x #_ #Hj -g -i
+ lapply (pr_pat_inv_uni … Hj) -Hj #H destruct
/3 width=8 by frees_atom_drops, drops_trans/
| #f1 #I #K #V #_ #IH #Hf1 #f #L #H1 #U #H2 #f2 #H3
- lapply (isfin_inv_next … Hf1 ??) -Hf1 [3: |*: // ] #Hf1
+ lapply (pr_isf_inv_next … Hf1 ??) -Hf1 [3: |*: // ] #Hf1
lapply (lifts_inv_lref1 … H2) -H2 * #j #Hf #H destruct
elim (drops_split_trans_bind2 … H1) -H1 [ |*: // ] #Z #Y #HLY #HYK #H
elim (liftsb_inv_pair_sn … H) -H #W #HVW #H destruct
| #f1 #I #K #Hf1 #_ #f #L #H1 #U #H2 #f2 #H3
lapply (lifts_inv_lref1 … H2) -H2 * #j #Hf #H destruct
elim (coafter_fwd_xnx_pushs … Hf H3) -H3 #g2 #H3 #H2 destruct
- lapply (coafter_isid_inv_dx … H3 … Hf1) -f1 #Hg2
+ lapply (pr_coafter_isi_inv_dx … H3 … Hf1) -f1 #Hg2
elim (drops_split_trans_bind2 … H1 … Hf) -H1 -Hf #Z #Y #HLY #_ #H
lapply (liftsb_inv_unit_sn … H) -H #H destruct
/2 width=3 by frees_unit_drops/
| #f1 #I #K #i #_ #IH #Hf1 #f #L #H1 #U #H2 #f2 #H3
- lapply (isfin_inv_push … Hf1 ??) -Hf1 [3: |*: // ] #Hf1
+ lapply (pr_isf_inv_push … Hf1 ??) -Hf1 [3: |*: // ] #Hf1
lapply (lifts_inv_lref1 … H2) -H2 * #x #Hf #H destruct
- elim (at_inv_nxx … Hf) -Hf [ |*: // ] #j #Hf #H destruct
+ elim (pr_pat_inv_succ_sn … Hf) -Hf [ |*: // ] #j #Hf #H destruct
elim (drops_split_trans_bind2 … H1) -H1 [ |*: // ] #Z #Y #HLY #HYK #_
elim (coafter_fwd_xpx_pushs … 0 … H3) [ |*: // ] #g2 #H3 #H2 destruct
lapply (drops_isuni_fwd_drop2 … HLY) -HLY // #HLY
lapply (IH … HYK … H3) -IH -H3 -HYK [4: |*: /2 width=2 by lifts_lref/ ]
- >plus_S1 /2 width=3 by frees_lref_pushs/ (**) (* full auto fails *)
+ >nplus_succ_sn /2 width=3 by frees_lref_pushs/ (**) (* full auto fails *)
| #f1 #K #l #Hf1 #_ #f #L #HLK #U #H2 #f2 #H3
- lapply (coafter_isid_inv_dx … H3 … Hf1) -f1 #Hf2
+ lapply (pr_coafter_isi_inv_dx … H3 … Hf1) -f1 #Hf2
>(lifts_inv_gref1 … H2) -U /2 width=1 by frees_gref/
| #f1V #f1T #f1 #p #I #K #V #T #_ #_ #H1f1 #IHV #IHT #H2f1 #f #L #H1 #Y #H2 #f2 #H3
- elim (sor_inv_isfin3 … H1f1) // #Hf1V #H
- lapply (isfin_inv_tl … H) -H
+ elim (pr_sor_inv_isf … H1f1) // #Hf1V #H
+ lapply (pr_isf_inv_tl … H) -H
elim (lifts_inv_bind1 … H2) -H2 #W #U #HVW #HTU #H destruct
- elim (coafter_sor … H3 … H1f1) /2 width=5 by coafter_isfin2_fwd/ -H3 -H1f1 #f2V #f2T #Hf2V #H
- elim (coafter_inv_tl1 … H) -H
+ elim (pr_sor_coafter_dx_tans … H3 … H1f1) /2 width=5 by pr_coafter_des_ist_isf/ -H3 -H1f1 #f2V #f2T #Hf2V #H
+ elim (pr_coafter_inv_tl_dx … H) -H
/5 width=5 by frees_bind, drops_skip, ext2_pair/
| #f1V #f1T #f1 #I #K #V #T #_ #_ #H1f1 #IHV #IHT #H2f1 #f #L #H1 #Y #H2 #f2 #H3
- elim (sor_inv_isfin3 … H1f1) //
+ elim (pr_sor_inv_isf … H1f1) //
elim (lifts_inv_flat1 … H2) -H2 #W #U #HVW #HTU #H destruct
- elim (coafter_sor … H3 … H1f1)
- /3 width=5 by coafter_isfin2_fwd, frees_flat/
+ elim (pr_sor_coafter_dx_tans … H3 … H1f1)
+ /3 width=5 by pr_coafter_des_ist_isf, frees_flat/
]
qed-.
∀b,f2,L,U. L ⊢ 𝐅+❪U❫ ≘ f2 →
∀f,K. ⇩*[b,f] L ≘ K → ∀T. ⇧*[f] T ≘ U →
∀f1. K ⊢ 𝐅+❪T❫ ≘ f1 → f ~⊚ f1 ≘ f2.
-/4 width=11 by frees_lifts, frees_mono, coafter_eq_repl_back0/ qed-.
+/4 width=11 by frees_lifts, frees_mono, pr_coafter_eq_repl_back/ qed-.
(* Inversion lemmas with generic slicing for local environments *************)
∀K. ⇩*[b,𝐔❨1❩] L ≘ K → ∀T. ⇧[1] T ≘ U →
K ⊢ 𝐅+❪T❫ ≘ ⫰f.
#b #f #L #U #H #K #HLK #T #HTU elim(frees_inv_lifts_ex … H … HLK … HTU) -b -L -U
-#f1 #Hf #Hf1 elim (coafter_inv_nxx … Hf) -Hf
-/3 width=5 by frees_eq_repl_back, coafter_isid_inv_sn/
+#f1 #Hf #Hf1 elim (pr_coafter_inv_next_sn … Hf) -Hf
+/3 width=5 by frees_eq_repl_back, pr_coafter_isi_inv_sn/
qed-.
lemma frees_inv_lifts:
∀f,K. ⇩*[b,f] L ≘ K → ∀T. ⇧*[f] T ≘ U →
∀f1. f ~⊚ f1 ≘ f2 → K ⊢ 𝐅+❪T❫ ≘ f1.
#b #f2 #L #U #H #f #K #HLK #T #HTU #f1 #Hf2 elim (frees_inv_lifts_ex … H … HLK … HTU) -b -L -U
-/3 width=7 by frees_eq_repl_back, coafter_inj/
+/3 width=7 by frees_eq_repl_back, pr_coafter_inj/
qed-.
(* Note: this is used by rex_conf and might be modified *)
∃∃g2. L2 ⊢ 𝐅+❪V2❫ ≘ g2 & g2 ⊆ g1.
#f1 #L1 #T1 #H elim H -f1 -L1 -T1
[ #f1 #L1 #s #Hf1 #I2 #L2 #V2 #j #_ #g1 #H1 -I2 -L1 -s
- lapply (isid_tls j … Hf1) -Hf1 <H1 -f1 #Hf1
- elim (isid_inv_next … Hf1) -Hf1 //
+ lapply (pr_isi_tls j … Hf1) -Hf1 <H1 -f1 #Hf1
+ elim (pr_isi_inv_next … Hf1) -Hf1 //
| #f1 #i #_ #I2 #L2 #V2 #j #H
elim (drops_inv_atom1 … H) -H #H destruct
| #f1 #I1 #L1 #V1 #Hf1 #IH #I2 #L2 #V2 *
[ -IH #HL12 lapply (drops_fwd_isid … HL12 ?) -HL12 //
- #H destruct #g1 #Hgf1 >(injective_next … Hgf1) -g1
+ #H destruct #g1 #Hgf1 >(eq_inv_pr_next_bi … Hgf1) -g1
/2 width=3 by ex2_intro/
| -Hf1 #j #HL12 lapply (drops_inv_drop1 … HL12) -HL12
- #HL12 #g1 <tls_xn <tl_next_rew #Hgf1 elim (IH … HL12 … Hgf1) -IH -HL12 -Hgf1
+ #HL12 #g1 <pr_tls_swap <pr_tl_next #Hgf1 elim (IH … HL12 … Hgf1) -IH -HL12 -Hgf1
/2 width=3 by ex2_intro/
]
| #f1 #I1 #L1 #Hf1 #I2 #L2 #V2 *
[ #HL12 lapply (drops_fwd_isid … HL12 ?) -HL12 // #H destruct
- | #j #_ #g1 #Hgf1 elim (isid_inv_next … Hgf1) -Hgf1 <tls_xn /2 width=1 by isid_tls/
+ | #j #_ #g1 #Hgf1 elim (pr_isi_inv_next … Hgf1) -Hgf1 <pr_tls_swap /2 width=1 by pr_isi_tls/
]
| #f1 #I1 #L1 #i #_ #IH #I2 #L2 #V2 *
- [ -IH #_ #g1 #Hgf1 elim (discr_next_push … Hgf1)
+ [ -IH #_ #g1 #Hgf1 elim (eq_inv_pr_next_push … Hgf1)
| #j #HL12 lapply (drops_inv_drop1 … HL12) -HL12
- #HL12 #g1 <tls_xn #Hgf1 elim (IH … HL12 … Hgf1) -IH -HL12 -Hgf1
+ #HL12 #g1 <pr_tls_swap #Hgf1 elim (IH … HL12 … Hgf1) -IH -HL12 -Hgf1
/2 width=3 by ex2_intro/
]
| #f1 #L1 #l #Hf1 #I2 #L2 #V2 #j #_ #g1 #H1 -I2 -L1 -l
- lapply (isid_tls j … Hf1) -Hf1 <H1 -f1 #Hf1
- elim (isid_inv_next … Hf1) -Hf1 //
+ lapply (pr_isi_tls j … Hf1) -Hf1 <H1 -f1 #Hf1
+ elim (pr_isi_inv_next … Hf1) -Hf1 //
| #fV1 #fT1 #f1 #p #I1 #L1 #V1 #T1 #_ #_ #Hf1 #IHV1 #IHT1 #I2 #L2 #V2 #j #HL12 #g1 #Hgf1
- lapply (sor_tls … Hf1 j) -Hf1 <Hgf1 -Hgf1 #Hf1
- elim (sor_xxn_tl … Hf1) [1,2: * |*: // ] -Hf1
+ lapply (pr_sor_tls … Hf1 j) -Hf1 <Hgf1 -Hgf1 #Hf1
+ elim (pr_sor_next_tl … Hf1) [1,2: * |*: // ] -Hf1
#gV1 #gT1 #Hg1
[ -IHT1 #H1 #_ elim (IHV1 … HL12 … H1) -IHV1 -HL12 -H1
- /3 width=6 by sor_inv_sle_sn_trans, ex2_intro/
- | -IHV1 #_ >tls_xn #H2 elim (IHT1 … H2) -IHT1 -H2
- /3 width=6 by drops_drop, sor_inv_sle_dx_trans, ex2_intro/
+ /3 width=6 by pr_sor_inv_sle_sn_trans, ex2_intro/
+ | -IHV1 #_ >pr_tls_swap #H2 elim (IHT1 … H2) -IHT1 -H2
+ /3 width=6 by drops_drop, pr_sor_inv_sle_dx_trans, ex2_intro/
]
| #fV1 #fT1 #f1 #I1 #L1 #V1 #T1 #_ #_ #Hf1 #IHV1 #IHT1 #I2 #L2 #V2 #j #HL12 #g1 #Hgf1
- lapply (sor_tls … Hf1 j) -Hf1 <Hgf1 -Hgf1 #Hf1
- elim (sor_xxn_tl … Hf1) [1,2: * |*: // ] -Hf1
+ lapply (pr_sor_tls … Hf1 j) -Hf1 <Hgf1 -Hgf1 #Hf1
+ elim (pr_sor_next_tl … Hf1) [1,2: * |*: // ] -Hf1
#gV1 #gT1 #Hg1
[ -IHT1 #H1 #_ elim (IHV1 … HL12 … H1) -IHV1 -HL12 -H1
- /3 width=6 by sor_inv_sle_sn_trans, ex2_intro/
+ /3 width=6 by pr_sor_inv_sle_sn_trans, ex2_intro/
| -IHV1 #_ #H2 elim (IHT1 … HL12 … H2) -IHT1 -HL12 -H2
- /3 width=6 by sor_inv_sle_dx_trans, ex2_intro/
+ /3 width=6 by pr_sor_inv_sle_dx_trans, ex2_intro/
]
]
qed-.
| #p #I #V #T #HG #HL #HT destruct
elim (IH G L V) // #f1 #HV
elim (IH G (L.ⓑ[I]V) T) -IH // #f2 #HT
- elim (sor_isfin_ex f1 (⫰f2))
- /3 width=6 by frees_fwd_isfin, frees_bind, isfin_tl, ex_intro/
+ elim (pr_sor_isf_bi f1 (⫰f2))
+ /3 width=6 by frees_fwd_isfin, frees_bind, pr_isf_tl, ex_intro/
| #I #V #T #HG #HL #HT destruct
elim (IH G L V) // #f1 #HV
elim (IH G L T) -IH // #f2 #HT
- elim (sor_isfin_ex f1 f2)
+ elim (pr_sor_isf_bi f1 f2)
/3 width=6 by frees_fwd_isfin, frees_flat, ex_intro/
]
qed-.
#f1 #L #V #Hf1 #f2 #T #Hf2 #f #Hf #p #I
elim (frees_total (L.ⓑ[I]V) T) #f0 #Hf0
lapply (lsubr_lsubf … Hf2 … Hf0) -Hf2 /2 width=5 by lsubr_unit/ #H02
-elim (pn_split f2) * #g2 #H destruct
+elim (pr_map_split_tl f2) * #g2 #H destruct
[ elim (lsubf_inv_push2 … H02) -H02 #g0 #Z #Y #H02 #H0 #H destruct
lapply (lsubf_inv_refl … H02) -H02 #H02
- lapply (sor_eq_repl_fwd2 … Hf … H02) -g2 #Hf
+ lapply (pr_sor_eq_repl_fwd_dx … Hf … H02) -g2 #Hf
/2 width=5 by frees_bind/
| elim (lsubf_inv_unit2 … H02) -H02 * [ #g0 #Y #_ #_ #H destruct ]
#z1 #g0 #z #Z #Y #X #H02 #Hz1 #Hz #H0 #H destruct
lapply (lsubf_inv_refl … H02) -H02 #H02
lapply (frees_mono … Hz1 … Hf1) -Hz1 #H1
- lapply (sor_eq_repl_back1 … Hz … H02) -g0 #Hz
- lapply (sor_eq_repl_back2 … Hz … H1) -z1 #Hz
- lapply (sor_comm … Hz) -Hz #Hz
- lapply (sor_mono … f Hz ?) // -Hz #H
- lapply (sor_inv_sle_sn … Hf) -Hf #Hf
- lapply (frees_eq_repl_back … Hf0 (↑f) ?) /2 width=5 by eq_next/ -z #Hf0
+ lapply (pr_sor_eq_repl_back_sn … Hz … H02) -g0 #Hz
+ lapply (pr_sor_eq_repl_back_dx … Hz … H1) -z1 #Hz
+ lapply (pr_sor_comm … Hz) -Hz #Hz
+ lapply (pr_sor_mono … f Hz ?) // -Hz #H
+ lapply (pr_sor_inv_sle_sn … Hf) -Hf #Hf
+ lapply (frees_eq_repl_back … Hf0 (↑f) ?) /2 width=5 by pr_eq_next/ -z #Hf0
@(frees_bind … Hf1 Hf0) -Hf1 -Hf0 (**) (* constructor needed *)
- /2 width=1 by sor_sle_dx/
+ /2 width=1 by pr_sor_sle_dx/
]
qed-.
elim (frees_inv_bind … H) -H #f1 #f2 #Hf1 #Hf2 #Hf
elim (frees_total (L.ⓧ) T) #f0 #Hf0
lapply (lsubr_lsubf … Hf0 … Hf2) -Hf2 /2 width=5 by lsubr_unit/ #H20
-elim (pn_split f0) * #g0 #H destruct
+elim (pr_map_split_tl f0) * #g0 #H destruct
[ elim (lsubf_inv_push2 … H20) -H20 #g2 #I #Y #H20 #H2 #H destruct
lapply (lsubf_inv_refl … H20) -H20 #H20
- lapply (sor_eq_repl_back2 … Hf … H20) -g2 #Hf
+ lapply (pr_sor_eq_repl_back_dx … Hf … H20) -g2 #Hf
/2 width=5 by ex3_2_intro/
| elim (lsubf_inv_unit2 … H20) -H20 * [ #g2 #Y #_ #_ #H destruct ]
#z1 #z0 #g2 #Z #Y #X #H20 #Hz1 #Hg2 #H2 #H destruct
lapply (lsubf_inv_refl … H20) -H20 #H0
lapply (frees_mono … Hz1 … Hf1) -Hz1 #H1
- lapply (sor_eq_repl_back1 … Hg2 … H0) -z0 #Hg2
- lapply (sor_eq_repl_back2 … Hg2 … H1) -z1 #Hg2
+ lapply (pr_sor_eq_repl_back_sn … Hg2 … H0) -z0 #Hg2
+ lapply (pr_sor_eq_repl_back_dx … Hg2 … H1) -z1 #Hg2
@(ex3_2_intro … Hf1 Hf0) -Hf1 -Hf0 (**) (* constructor needed *)
- /2 width=3 by sor_comm_23_idem/
+ /2 width=3 by pr_sor_comm_23_idem/
]
qed-.
theorem frees_mono: ∀f1,L,T. L ⊢ 𝐅+❪T❫ ≘ f1 → ∀f2. L ⊢ 𝐅+❪T❫ ≘ f2 → f1 ≡ f2.
#f1 #L #T #H elim H -f1 -L -T
-[ /3 width=3 by frees_inv_sort, isid_inv_eq_repl/
+[ /3 width=3 by frees_inv_sort, pr_isi_inv_eq_repl/
| #f1 #i #Hf1 #g2 #H
elim (frees_inv_atom … H) -H #f2 #Hf2 #H destruct
- /4 width=5 by isid_inv_eq_repl, pushs_eq_repl, eq_next/
+ /4 width=5 by pr_isi_inv_eq_repl, pr_pushs_eq_repl, pr_eq_next/
| #f1 #I #L #V #_ #IH #g2 #H elim (frees_inv_pair … H) -H
- #f2 #Hf2 #H destruct /3 width=5 by eq_next/
+ #f2 #Hf2 #H destruct /3 width=5 by pr_eq_next/
| #f1 #I #L #Hf1 #g2 #H elim (frees_inv_unit … H) -H
- #f2 #Hf2 #H destruct /3 width=5 by isid_inv_eq_repl, eq_next/
+ #f2 #Hf2 #H destruct /3 width=5 by pr_isi_inv_eq_repl, pr_eq_next/
| #f1 #I #L #i #_ #IH #g2 #H elim (frees_inv_lref … H) -H
- #f2 #Hf2 #H destruct /3 width=5 by eq_push/
-| /3 width=3 by frees_inv_gref, isid_inv_eq_repl/
+ #f2 #Hf2 #H destruct /3 width=5 by pr_eq_push/
+| /3 width=3 by frees_inv_gref, pr_isi_inv_eq_repl/
| #f1V #f1T #f1 #p #I #L #V #T #_ #_ #Hf1 #IHV #IHT #f2 #H elim (frees_inv_bind … H) -H
- #f2V #f2T #HV #HT #Hf2 @(sor_mono … Hf1) -Hf1
- /5 width=3 by sor_eq_repl_fwd2, sor_eq_repl_fwd1, tl_eq_repl/ (**) (* full auto too slow *)
+ #f2V #f2T #HV #HT #Hf2 @(pr_sor_mono … Hf1) -Hf1
+ /5 width=3 by pr_sor_eq_repl_fwd_dx, pr_sor_eq_repl_fwd_sn, pr_tl_eq_repl/ (**) (* full auto too slow *)
| #f1V #f1T #f1 #I #L #V #T #_ #_ #Hf1 #IHV #IHT #f2 #H elim (frees_inv_flat … H) -H
- #f2V #f2T #HV #HT #Hf2 @(sor_mono … Hf1) -Hf1
- /4 width=3 by sor_eq_repl_fwd2, sor_eq_repl_fwd1/ (**) (* full auto too slow *)
+ #f2V #f2T #HV #HT #Hf2 @(pr_sor_mono … Hf1) -Hf1
+ /4 width=3 by pr_sor_eq_repl_fwd_dx, pr_sor_eq_repl_fwd_sn/ (**) (* full auto too slow *)
]
qed-.
(* Basic properties *********************************************************)
lemma fsle_sort: ∀L,s1,s2. ❪L,⋆s1❫ ⊆ ❪L,⋆s2❫.
-/3 width=8 by frees_sort, sle_refl, ex4_4_intro/ qed.
+/3 width=8 by frees_sort, pr_sle_refl, ex4_4_intro/ qed.
lemma fsle_gref: ∀L,l1,l2. ❪L,§l1❫ ⊆ ❪L,§l2❫.
-/3 width=8 by frees_gref, sle_refl, ex4_4_intro/ qed.
+/3 width=8 by frees_gref, pr_sle_refl, ex4_4_intro/ qed.
* #n1 #n2 #f1 #f2 #Hf1 #Hf2 #HK12 #Hf12
#W1 #HVW1 #I1 #I2
elim (lveq_inj_length … HK12) // -HK #H1 #H2 destruct
-/5 width=12 by frees_lifts_SO, frees_pair, drops_refl, drops_drop, lveq_bind, sle_weak, ex4_4_intro/
+/5 width=12 by frees_lifts_SO, frees_pair, drops_refl, drops_drop, lveq_bind, pr_sle_weak, ex4_4_intro/
qed.
lemma fsle_lifts_SO: ∀K1,K2. |K1| = |K2| → ∀T1,T2. ❪K1,T1❫ ⊆ ❪K2,T2❫ →
* #n1 #n2 #f1 #f2 #Hf1 #Hf2 #HK12 #Hf12
#U1 #U2 #HTU1 #HTU2 #I1 #I2
elim (lveq_inj_length … HK12) // -HK #H1 #H2 destruct
-/5 width=12 by frees_lifts_SO, drops_refl, drops_drop, lveq_bind, sle_push, ex4_4_intro/
+/5 width=12 by frees_lifts_SO, drops_refl, drops_drop, lveq_bind, pr_sle_push, ex4_4_intro/
qed.
(* Advanced inversion lemmas ************************************************)
* #n #m #f2 #g2 #Hf2 #Hg2 #HL #Hfg2 #p
elim (lveq_inv_pair_pair … HL) -HL #HL #H1 #H2 destruct
elim (frees_total L2 V2) #g1 #Hg1
-elim (sor_isfin_ex g1 (⫰g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+elim (pr_sor_isf_bi g1 (⫰g2)) /3 width=3 by frees_fwd_isfin, pr_isf_tl/ #g #Hg #_
lapply (frees_inv_lifts_SO (Ⓣ) … Hf2 … HTU1)
[1,2: /3 width=4 by drops_refl, drops_drop/ ] -U1 #Hf2
-lapply (sor_inv_sle_dx … Hg) #H0g
-/5 width=10 by frees_bind, sle_tl, sle_trans, ex4_4_intro/
+lapply (pr_sor_inv_sle_dx … Hg) #H0g
+/5 width=10 by frees_bind, pr_sle_tl, pr_sle_trans, ex4_4_intro/
qed-.
lemma fsle_refl: bi_reflexive … fsle.
#L #T
elim (frees_total L T) #f #Hf
-/2 width=8 by sle_refl, ex4_4_intro/
+/2 width=8 by pr_sle_refl, ex4_4_intro/
qed.
lemma fsle_shift: ∀L1,L2. |L1| = |L2| →
elim (lveq_inj_length … H2L) // -H1L #H1 #H2 destruct
lapply (lveq_inv_bind_O … H2L) -H2L #HL
elim (frees_total L2 V) #g1 #Hg1
-elim (sor_isfin_ex g1 (⫰g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
-lapply (sor_inv_sle_dx … Hg) #H0g
-/4 width=10 by frees_bind, lveq_void_sn, sle_tl, sle_trans, ex4_4_intro/
+elim (pr_sor_isf_bi g1 (⫰g2)) /3 width=3 by frees_fwd_isfin, pr_isf_tl/ #g #Hg #_
+lapply (pr_sor_inv_sle_dx … Hg) #H0g
+/4 width=10 by frees_bind, lveq_void_sn, pr_sle_tl, pr_sle_trans, ex4_4_intro/
qed.
lemma fsle_bind_dx_sn: ∀L1,L2,V1,V2. ❪L1,V1❫ ⊆ ❪L2,V2❫ →
∀p,I,T2. ❪L1,V1❫ ⊆ ❪L2,ⓑ[p,I]V2.T2❫.
#L1 #L2 #V1 #V2 * #n1 #m1 #f1 #g1 #Hf1 #Hg1 #HL12 #Hfg1 #p #I #T2
elim (frees_total (L2.ⓧ) T2) #g2 #Hg2
-elim (sor_isfin_ex g1 (⫰g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+elim (pr_sor_isf_bi g1 (⫰g2)) /3 width=3 by frees_fwd_isfin, pr_isf_tl/ #g #Hg #_
@(ex4_4_intro … g Hf1 … HL12) (**) (* full auto too slow *)
-/4 width=5 by frees_bind_void, sor_inv_sle_sn, sor_tls, sle_trans/
+/4 width=5 by frees_bind_void, pr_sor_inv_sle_sn, pr_sor_tls, pr_sle_trans/
qed.
lemma fsle_bind_dx_dx: ∀L1,L2,T1,T2. ❪L1,T1❫ ⊆ ❪L2.ⓧ,T2❫ → |L1| ≤ |L2| →
∀p,I,V2. ❪L1,T1❫ ⊆ ❪L2,ⓑ[p,I]V2.T2❫.
#L1 #L2 #T1 #T2 * #n1 #x1 #f2 #g2 #Hf2 #Hg2 #H #Hfg2 #HL12 #p #I #V2
elim (lveq_inv_void_dx_length … H HL12) -H -HL12 #m1 #HL12 #H1 #H2 destruct
-<tls_xn in Hfg2; #Hfg2
+<pr_tls_swap in Hfg2; #Hfg2
elim (frees_total L2 V2) #g1 #Hg1
-elim (sor_isfin_ex g1 (⫰g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+elim (pr_sor_isf_bi g1 (⫰g2)) /3 width=3 by frees_fwd_isfin, pr_isf_tl/ #g #Hg #_
@(ex4_4_intro … g Hf2 … HL12) (**) (* full auto too slow *)
-/4 width=5 by frees_bind_void, sor_inv_sle_dx, sor_tls, sle_trans/
+/4 width=5 by frees_bind_void, pr_sor_inv_sle_dx, pr_sor_tls, pr_sle_trans/
qed.
lemma fsle_flat_dx_sn: ∀L1,L2,V1,V2. ❪L1,V1❫ ⊆ ❪L2,V2❫ →
∀I,T2. ❪L1,V1❫ ⊆ ❪L2,ⓕ[I]V2.T2❫.
#L1 #L2 #V1 #V2 * #n1 #m1 #f1 #g1 #Hf1 #Hg1 #HL12 #Hfg1 #I #T2
elim (frees_total L2 T2) #g2 #Hg2
-elim (sor_isfin_ex g1 g2) /2 width=3 by frees_fwd_isfin/ #g #Hg #_
+elim (pr_sor_isf_bi g1 g2) /2 width=3 by frees_fwd_isfin/ #g #Hg #_
@(ex4_4_intro … g Hf1 … HL12) (**) (* full auto too slow *)
-/4 width=5 by frees_flat, sor_inv_sle_sn, sor_tls, sle_trans/
+/4 width=5 by frees_flat, pr_sor_inv_sle_sn, pr_sor_tls, pr_sle_trans/
qed.
lemma fsle_flat_dx_dx: ∀L1,L2,T1,T2. ❪L1,T1❫ ⊆ ❪L2,T2❫ →
∀I,V2. ❪L1,T1❫ ⊆ ❪L2,ⓕ[I]V2.T2❫.
#L1 #L2 #T1 #T2 * #n1 #m1 #f2 #g2 #Hf2 #Hg2 #HL12 #Hfg2 #I #V2
elim (frees_total L2 V2) #g1 #Hg1
-elim (sor_isfin_ex g1 g2) /2 width=3 by frees_fwd_isfin/ #g #Hg #_
+elim (pr_sor_isf_bi g1 g2) /2 width=3 by frees_fwd_isfin/ #g #Hg #_
@(ex4_4_intro … g Hf2 … HL12) (**) (* full auto too slow *)
-/4 width=5 by frees_flat, sor_inv_sle_dx, sor_tls, sle_trans/
+/4 width=5 by frees_flat, pr_sor_inv_sle_dx, pr_sor_tls, pr_sle_trans/
qed.
(* Advanced forward lemmas ***************************************************)
elim (lveq_inv_pair_pair … HL12) -HL12 #HL12 #H1 #H2 destruct
elim (frees_total (L1.ⓧ) T1) #g1 #Hg1
lapply (lsubr_lsubf … Hg1 … Hf1) -Hf1 /2 width=1 by lsubr_unit/ #Hfg1
-/5 width=10 by lsubf_fwd_sle, lveq_bind, sle_trans, ex4_4_intro/ (**) (* full auto too slow *)
+/5 width=10 by lsubf_fwd_sle, lveq_bind, pr_sle_trans, ex4_4_intro/ (**) (* full auto too slow *)
qed-.
∃∃n1,n2,f1. L1 ⊢ 𝐅+❪T1❫ ≘ f1 & L1 ≋ⓧ*[n1,n2] L2 & ⫰*[n1]f1 ⊆ ⫰*[n2]f2.
#L1 #L2 #T1 #T2 * #n1 #n2 #f1 #g2 #Hf1 #Hg2 #HL #Hn #f2 #Hf2
lapply (frees_mono … Hg2 … Hf2) -Hg2 -Hf2 #Hgf2
-lapply (tls_eq_repl n2 … Hgf2) -Hgf2 #Hgf2
-lapply (sle_eq_repl_back2 … Hn … Hgf2) -g2
+lapply (pr_tls_eq_repl n2 … Hgf2) -Hgf2 #Hgf2
+lapply (pr_sle_eq_repl_back_dx … Hn … Hgf2) -g2
/2 width=6 by ex3_3_intro/
qed-.
f1 ⊆ f2.
#L1 #L2 #H1L #T1 #T2 #H2L #f1 #Hf1 #f2 #Hf2
elim (fsle_frees_trans_eq … H2L … Hf2) // -L2 -T2
-/3 width=6 by frees_mono, sle_eq_repl_back1/
+/3 width=6 by frees_mono, pr_sle_eq_repl_back_sn/
qed-.
lemma fsle_frees_conf:
∃∃n1,n2,f2. L2 ⊢ 𝐅+❪T2❫ ≘ f2 & L1 ≋ⓧ*[n1,n2] L2 & ⫰*[n1]f1 ⊆ ⫰*[n2]f2.
#L1 #L2 #T1 #T2 * #n1 #n2 #g1 #g2 #Hg1 #Hg2 #HL #Hn #f1 #Hf1
lapply (frees_mono … Hg1 … Hf1) -Hg1 -Hf1 #Hgf1
-lapply (tls_eq_repl n1 … Hgf1) -Hgf1 #Hgf1
-lapply (sle_eq_repl_back1 … Hn … Hgf1) -g1
+lapply (pr_tls_eq_repl n1 … Hgf1) -Hgf1 #Hgf1
+lapply (pr_sle_eq_repl_back_sn … Hn … Hgf1) -g1
/2 width=6 by ex3_3_intro/
qed-.
* #n0 #n2 #f0 #f2 #Hf0 #Hf2 #Hn #Hf
lapply (frees_mono … Hf0 … Hg0) -Hf0 -Hg0 #Hfg0
elim (lveq_inj_length … Hn) // -Hn #H1 #H2 destruct
-lapply (sle_eq_repl_back1 … Hf … Hfg0) -f0
-/4 width=10 by sle_tls, sle_trans, ex4_4_intro/
+lapply (pr_sle_eq_repl_back_sn … Hf … Hfg0) -f0
+/4 width=10 by pr_sle_tls, pr_sle_trans, ex4_4_intro/
qed-.
theorem fsle_trans_dx:
* #n0 #n2 #f0 #f2 #Hf0 #Hf2 #Hn #Hf
lapply (frees_mono … Hg0 … Hf0) -Hg0 -Hf0 #Hgf0
elim (lveq_inj_length … Hm) // -Hm #H1 #H2 destruct
-lapply (sle_eq_repl_back2 … Hg … Hgf0) -g0
-/4 width=10 by sle_tls, sle_trans, ex4_4_intro/
+lapply (pr_sle_eq_repl_back_dx … Hg … Hgf0) -g0
+/4 width=10 by pr_sle_tls, pr_sle_trans, ex4_4_intro/
qed-.
theorem fsle_trans_rc:
lapply (frees_mono … Hg0 … Hf0) -Hg0 -Hf0 #Hgf0
elim (lveq_inj_length … Hm) // -Hm #H1 #H2 destruct
elim (lveq_inj_length … Hn) // -Hn #H1 #H2 destruct
-lapply (sle_eq_repl_back2 … Hg … Hgf0) -g0
-/3 width=10 by lveq_length_eq, sle_trans, ex4_4_intro/
+lapply (pr_sle_eq_repl_back_dx … Hg … Hgf0) -g0
+/3 width=10 by lveq_length_eq, pr_sle_trans, ex4_4_intro/
qed-.
theorem fsle_bind_sn_ge:
#L1 #L2 #HL #V1 #T1 #T * #n1 #x #f1 #g #Hf1 #Hg #H1n1 #H2n1 #H #p #I
elim (fsle_frees_trans … H … Hg) -H #n2 #n #f2 #Hf2 #H1n2 #H2n2
elim (lveq_inj_void_sn_ge … H1n1 … H1n2) -H1n2 // #H1 #H2 #H3 destruct
-elim (sor_isfin_ex f1 (⫰f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
-<tls_xn in H2n2; #H2n2
-/4 width=12 by frees_bind_void, sor_inv_sle, sor_tls, ex4_4_intro/
+elim (pr_sor_isf_bi f1 (⫰f2)) /3 width=3 by frees_fwd_isfin, pr_isf_tl/ #f #Hf #_
+<pr_tls_swap in H2n2; #H2n2
+/4 width=12 by frees_bind_void, pr_sor_inv_sle_bi, pr_sor_tls, ex4_4_intro/
qed.
theorem fsle_flat_sn:
#L1 #L2 #V1 #T1 #T * #n1 #x #f1 #g #Hf1 #Hg #H1n1 #H2n1 #H #I
elim (fsle_frees_trans … H … Hg) -H #n2 #n #f2 #Hf2 #H1n2 #H2n2
elim (lveq_inj … H1n1 … H1n2) -H1n2 #H1 #H2 destruct
-elim (sor_isfin_ex f1 f2) /2 width=3 by frees_fwd_isfin/ #f #Hf #_
-/4 width=12 by frees_flat, sor_inv_sle, sor_tls, ex4_4_intro/
+elim (pr_sor_isf_bi f1 f2) /2 width=3 by frees_fwd_isfin/ #f #Hf #_
+/4 width=12 by frees_flat, pr_sor_inv_sle_bi, pr_sor_tls, ex4_4_intro/
qed.
theorem fsle_bind_eq:
* #n2 #m2 #f2 #g2 #Hf2 #Hg2 #H2L #Hfg2 #p #I1
elim (lveq_inj_length … H1L) // #H1 #H2 destruct
elim (lveq_inj_length … H2L) // -HL -H2L #H1 #H2 destruct
-elim (sor_isfin_ex f1 (⫰f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
-elim (sor_isfin_ex g1 (⫰g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
-/4 width=15 by frees_bind_void, frees_bind, monotonic_sle_sor, sle_tl, ex4_4_intro/
+elim (pr_sor_isf_bi f1 (⫰f2)) /3 width=3 by frees_fwd_isfin, pr_isf_tl/ #f #Hf #_
+elim (pr_sor_isf_bi g1 (⫰g2)) /3 width=3 by frees_fwd_isfin, pr_isf_tl/ #g #Hg #_
+/4 width=15 by frees_bind_void, frees_bind, pr_sor_monotonic_sle, pr_sle_tl, ex4_4_intro/
qed.
theorem fsle_bind:
* #n2 #m2 #f2 #g2 #Hf2 #Hg2 #H2L #Hfg2 #p
elim (lveq_inv_pair_pair … H2L) -H2L #H2L #H1 #H2 destruct
elim (lveq_inj … H2L … H1L) -H1L #H1 #H2 destruct
-elim (sor_isfin_ex f1 (⫰f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
-elim (sor_isfin_ex g1 (⫰g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
-/4 width=15 by frees_bind, monotonic_sle_sor, sle_tl, ex4_4_intro/
+elim (pr_sor_isf_bi f1 (⫰f2)) /3 width=3 by frees_fwd_isfin, pr_isf_tl/ #f #Hf #_
+elim (pr_sor_isf_bi g1 (⫰g2)) /3 width=3 by frees_fwd_isfin, pr_isf_tl/ #g #Hg #_
+/4 width=15 by frees_bind, pr_sor_monotonic_sle, pr_sle_tl, ex4_4_intro/
qed.
theorem fsle_flat:
(* Properties with length for local environments ****************************)
lemma fsle_sort_bi: ∀L1,L2,s1,s2. |L1| = |L2| → ❪L1,⋆s1❫ ⊆ ❪L2,⋆s2❫.
-/3 width=8 by lveq_length_eq, frees_sort, sle_refl, ex4_4_intro/ qed.
+/3 width=8 by lveq_length_eq, frees_sort, pr_sle_refl, ex4_4_intro/ qed.
lemma fsle_gref_bi: ∀L1,L2,l1,l2. |L1| = |L2| → ❪L1,§l1❫ ⊆ ❪L2,§l2❫.
-/3 width=8 by lveq_length_eq, frees_gref, sle_refl, ex4_4_intro/ qed.
+/3 width=8 by lveq_length_eq, frees_gref, pr_sle_refl, ex4_4_intro/ qed.
lemma fsle_pair_bi: ∀K1,K2. |K1| = |K2| → ∀V1,V2. ❪K1,V1❫ ⊆ ❪K2,V2❫ →
∀I1,I2. ❪K1.ⓑ[I1]V1,#O❫ ⊆ ❪K2.ⓑ[I2]V2,#O❫.
* #n1 #n2 #f1 #f2 #Hf1 #Hf2 #HK12 #Hf12
#I1 #I2
elim (lveq_inj_length … HK12) // -HK #H1 #H2 destruct
-/3 width=12 by frees_pair, lveq_bind, sle_next, ex4_4_intro/
+/3 width=12 by frees_pair, lveq_bind, pr_sle_next, ex4_4_intro/
qed.
lemma fsle_unit_bi: ∀K1,K2. |K1| = |K2| →
∀I1,I2. ❪K1.ⓤ[I1],#O❫ ⊆ ❪K2.ⓤ[I2],#O❫.
-/3 width=8 by frees_unit, lveq_length_eq, sle_refl, ex4_4_intro/
+/3 width=8 by frees_unit, lveq_length_eq, pr_sle_refl, ex4_4_intro/
qed.
elim (lifts_inv_lref1 … H0) -H0 #j #Hf #H destruct
lapply (acr_gcr … H1RP H2RP A) #HA
lapply (drops_trans … HL01 … HLK1 ??) -HL01 [3: |*: // ] #H
- elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK0 #HY
+ elim (drops_split_trans … H) -H [ |*: /2 width=6 by pr_after_nat_uni/ ] #Y #HLK0 #HY
lapply (drops_tls_at … Hf … HY) -Hf -HY #HY
elim (drops_inv_skip2 … HY) -HY #Z #K0 #HK01 #HZ #H destruct
elim (liftsb_inv_pair_sn … HZ) -HZ #V0 #HV10 #H destruct
elim (lifts_inv_applv1 … H) -H #V0s #X0 #HV0s #H0 #H destruct
elim (lifts_inv_lref1 … H0) -H0 #j #Hf #H destruct
lapply (drops_trans … HL0 … HLK ??) [3: |*: // ] -HLK #H
- elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK0 #HY
+ elim (drops_split_trans … H) -H [ |*: /2 width=6 by pr_after_nat_uni/ ] #Y #HLK0 #HY
lapply (drops_tls_at … Hf … HY) -HY #HY
elim (drops_inv_skip2 … HY) -HY #Z #K0 #HK0 #HZ #H destruct
elim (liftsb_inv_pair_sn … HZ) -HZ #W1 #HVW1 #H destruct
elim (lifts_total W1 (𝐔❨↑j❩)) #W2 #HW12
lapply (lifts_trans … HVW1 … HW12 ??) -HVW1 [3: |*: // ] #H
- lapply (lifts_conf … HV12 … H f ?) -V1 [ /2 width=3 by after_uni_succ_sn/ ] #HVW2
+ lapply (lifts_conf … HV12 … H f ?) -V1 [ /2 width=3 by pr_pat_after_uni_tls/ ] #HVW2
@(s5 … IHA … (V0⨮V0s) … HW12) /3 width=4 by drops_inv_gen, lifts_applv/
| #G #L #V1s #V2s #HV12s #p #V #T #HA #HV #f #L0 #V10 #X #HL0 #H #HB
elim (lifts_inv_applv1 … H) -H #V10s #X0 #HV10s #H0 #H destruct
@(HA … (⫯f)) /3 width=2 by drops_skip, ext2_pair/
[ @lifts_applv //
lapply (liftsv_trans … HV10s … HV120s ??) -V10s [3: |*: // ] #H
- elim (liftsv_split_trans … H (𝐔❨1❩) (⫯f)) /2 width=1 by after_uni_one_sn/ #V10s #HV10s #HV120s
+ elim (liftsv_split_trans … H (𝐔❨1❩) (⫯f)) /2 width=1 by pr_after_unit_sn/ #V10s #HV10s #HV120s
>(liftsv_mono … HV12s … HV10s) -V1s //
| @(acr_lifts … H1RP … HB … HV120) /3 width=2 by drops_refl, drops_drop/
]
(* RESTRICTED REFINEMENT FOR CONTEXT-SENSITIVE FREE VARIABLES ***************)
-inductive lsubf: relation4 lenv rtmap lenv rtmap ≝
+inductive lsubf: relation4 lenv pr_map lenv pr_map ≝
| lsubf_atom: ∀f1,f2. f1 ≡ f2 → lsubf (⋆) f1 (⋆) f2
| lsubf_push: ∀f1,f2,I1,I2,L1,L2. lsubf L1 (f1) L2 (f2) →
lsubf (L1.ⓘ[I1]) (⫯f1) (L2.ⓘ[I2]) (⫯f2)
#f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
[ #f1 #f2 #_ #g1 #J1 #K1 #_ #H destruct
| #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g1 #J1 #K1 #H1 #H2 destruct
- <(injective_push … H1) -g1 /2 width=6 by ex3_3_intro/
-| #f1 #f2 #I #L1 #L2 #_ #g1 #J1 #K1 #H elim (discr_next_push … H)
-| #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g1 #J1 #K1 #H elim (discr_next_push … H)
-| #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g1 #J1 #K1 #H elim (discr_next_push … H)
+ <(eq_inv_pr_push_bi … H1) -g1 /2 width=6 by ex3_3_intro/
+| #f1 #f2 #I #L1 #L2 #_ #g1 #J1 #K1 #H elim (eq_inv_pr_next_push … H)
+| #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g1 #J1 #K1 #H elim (eq_inv_pr_next_push … H)
+| #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g1 #J1 #K1 #H elim (eq_inv_pr_next_push … H)
]
qed-.
K1 ⊢ 𝐅+❪X❫ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2 & L2 = K2.ⓤ[J].
#f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
[ #f1 #f2 #_ #g1 #J #K1 #X #_ #H destruct
-| #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g1 #J #K1 #X #H elim (discr_push_next … H)
+| #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g1 #J #K1 #X #H elim (eq_inv_pr_push_next … H)
| #f1 #f2 #I #L1 #L2 #H12 #g1 #J #K1 #X #H1 #H2 destruct
- <(injective_next … H1) -g1 /3 width=5 by or3_intro0, ex3_2_intro/
+ <(eq_inv_pr_next_bi … H1) -g1 /3 width=5 by or3_intro0, ex3_2_intro/
| #f #f0 #f1 #f2 #L1 #L2 #W #V #Hf #Hf1 #H12 #g1 #J #K1 #X #H1 #H2 destruct
- <(injective_next … H1) -g1 /3 width=12 by or3_intro1, ex7_6_intro/
+ <(eq_inv_pr_next_bi … H1) -g1 /3 width=12 by or3_intro1, ex7_6_intro/
| #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #Hf #Hf1 #H12 #g1 #J #K1 #X #H1 #H2 destruct
- <(injective_next … H1) -g1 /3 width=10 by or3_intro2, ex5_5_intro/
+ <(eq_inv_pr_next_bi … H1) -g1 /3 width=10 by or3_intro2, ex5_5_intro/
]
qed-.
∃∃g2,K2. ❪K1,g1❫ ⫃𝐅+ ❪K2,g2❫ & f2 = ↑g2 & L2 = K2.ⓤ[I].
#f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
[ #f1 #f2 #_ #g1 #J #K1 #_ #H destruct
-| #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g1 #J #K1 #H elim (discr_push_next … H)
+| #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g1 #J #K1 #H elim (eq_inv_pr_push_next … H)
| #f1 #f2 #I #L1 #L2 #H12 #g1 #J #K1 #H1 #H2 destruct
- <(injective_next … H1) -g1 /2 width=5 by ex3_2_intro/
+ <(eq_inv_pr_next_bi … H1) -g1 /2 width=5 by ex3_2_intro/
| #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g1 #J #K1 #_ #H destruct
| #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g1 #J #K1 #_ #H destruct
]
#f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
[ #f1 #f2 #_ #g2 #J2 #K2 #_ #H destruct
| #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g2 #J2 #K2 #H1 #H2 destruct
- <(injective_push … H1) -g2 /2 width=6 by ex3_3_intro/
-| #f1 #f2 #I #L1 #L2 #_ #g2 #J2 #K2 #H elim (discr_next_push … H)
-| #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g2 #J2 #K2 #H elim (discr_next_push … H)
-| #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g2 #J2 #K2 #H elim (discr_next_push … H)
+ <(eq_inv_pr_push_bi … H1) -g2 /2 width=6 by ex3_3_intro/
+| #f1 #f2 #I #L1 #L2 #_ #g2 #J2 #K2 #H elim (eq_inv_pr_next_push … H)
+| #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g2 #J2 #K2 #H elim (eq_inv_pr_next_push … H)
+| #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g2 #J2 #K2 #H elim (eq_inv_pr_next_push … H)
]
qed-.
I = Abst & L1 = K1.ⓓⓝW.V.
#f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
[ #f1 #f2 #_ #g2 #J #K2 #X #_ #H destruct
-| #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g2 #J #K2 #X #H elim (discr_push_next … H)
+| #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g2 #J #K2 #X #H elim (eq_inv_pr_push_next … H)
| #f1 #f2 #I #L1 #L2 #H12 #g2 #J #K2 #X #H1 #H2 destruct
- <(injective_next … H1) -g2 /3 width=5 by ex3_2_intro, or_introl/
+ <(eq_inv_pr_next_bi … H1) -g2 /3 width=5 by ex3_2_intro, or_introl/
| #f #f0 #f1 #f2 #L1 #L2 #W #V #Hf #Hf1 #H12 #g2 #J #K2 #X #H1 #H2 destruct
- <(injective_next … H1) -g2 /3 width=10 by ex6_5_intro, or_intror/
+ <(eq_inv_pr_next_bi … H1) -g2 /3 width=10 by ex6_5_intro, or_intror/
| #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #g2 #J #K2 #X #_ #H destruct
]
qed-.
K1 ⊢ 𝐅+❪V❫ ≘ g & g0 ⋓ g ≘ g1 & f1 = ↑g1 & L1 = K1.ⓑ[J]V.
#f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
[ #f1 #f2 #_ #g2 #J #K2 #_ #H destruct
-| #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g2 #J #K2 #H elim (discr_push_next … H)
+| #f1 #f2 #I1 #I2 #L1 #L2 #H12 #g2 #J #K2 #H elim (eq_inv_pr_push_next … H)
| #f1 #f2 #I #L1 #L2 #H12 #g2 #J #K2 #H1 #H2 destruct
- <(injective_next … H1) -g2 /3 width=5 by ex3_2_intro, or_introl/
+ <(eq_inv_pr_next_bi … H1) -g2 /3 width=5 by ex3_2_intro, or_introl/
| #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #g2 #J #K2 #_ #H destruct
| #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #Hf #Hf1 #H12 #g2 #J #K2 #H1 #H2 destruct
- <(injective_next … H1) -g2 /3 width=11 by ex5_6_intro, or_intror/
+ <(eq_inv_pr_next_bi … H1) -g2 /3 width=11 by ex5_6_intro, or_intror/
]
qed-.
lemma lsubf_inv_refl: ∀L,f1,f2. ❪L,f1❫ ⫃𝐅+ ❪L,f2❫ → f1 ≡ f2.
#L elim L -L /2 width=1 by lsubf_inv_atom/
#L #I #IH #f1 #f2 #H12
-elim (pn_split f1) * #g1 #H destruct
+elim (pr_map_split_tl f1) * #g1 #H destruct
[ elim (lsubf_inv_push_sn … H12) | elim (lsubf_inv_bind_sn … H12) ] -H12
-#g2 #H12 #H destruct /3 width=5 by eq_next, eq_push/
+#g2 #H12 #H destruct /3 width=5 by pr_eq_next, pr_eq_push/
qed-.
(* Basic forward lemmas *****************************************************)
lemma lsubf_fwd_bind_tl:
∀f1,f2,I,L1,L2. ❪L1.ⓘ[I],f1❫ ⫃𝐅+ ❪L2.ⓘ[I],f2❫ → ❪L1,⫰f1❫ ⫃𝐅+ ❪L2,⫰f2❫.
#f1 #f2 #I #L1 #L2 #H
-elim (pn_split f1) * #g1 #H0 destruct
+elim (pr_map_split_tl f1) * #g1 #H0 destruct
[ elim (lsubf_inv_push_sn … H) | elim (lsubf_inv_bind_sn … H) ] -H
#g2 #H12 #H destruct //
qed-.
lemma lsubf_fwd_isid_dx: ∀f1,f2,L1,L2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫ → 𝐈❪f2❫ → 𝐈❪f1❫.
#f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2
-[ /2 width=3 by isid_eq_repl_fwd/
-| /4 width=3 by isid_inv_push, isid_push/
-| #f1 #f2 #I #L1 #L2 #_ #_ #H elim (isid_inv_next … H) -H //
-| #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H elim (isid_inv_next … H) -H //
-| #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #_ #H elim (isid_inv_next … H) -H //
+[ /2 width=3 by pr_isi_eq_repl_fwd/
+| /4 width=3 by pr_isi_inv_push, pr_isi_push/
+| #f1 #f2 #I #L1 #L2 #_ #_ #H elim (pr_isi_inv_next … H) -H //
+| #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H elim (pr_isi_inv_next … H) -H //
+| #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #_ #H elim (pr_isi_inv_next … H) -H //
]
qed-.
lemma lsubf_fwd_isid_sn: ∀f1,f2,L1,L2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫ → 𝐈❪f1❫ → 𝐈❪f2❫.
#f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2
-[ /2 width=3 by isid_eq_repl_back/
-| /4 width=3 by isid_inv_push, isid_push/
-| #f1 #f2 #I #L1 #L2 #_ #_ #H elim (isid_inv_next … H) -H //
-| #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H elim (isid_inv_next … H) -H //
-| #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #_ #H elim (isid_inv_next … H) -H //
+[ /2 width=3 by pr_isi_eq_repl_back/
+| /4 width=3 by pr_isi_inv_push, pr_isi_push/
+| #f1 #f2 #I #L1 #L2 #_ #_ #H elim (pr_isi_inv_next … H) -H //
+| #f #f0 #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H elim (pr_isi_inv_next … H) -H //
+| #f #f0 #f1 #f2 #I1 #I2 #L1 #L2 #V #_ #_ #_ #_ #H elim (pr_isi_inv_next … H) -H //
]
qed-.
lemma lsubf_fwd_sle: ∀f1,f2,L1,L2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫ → f2 ⊆ f1.
#f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2
-/3 width=5 by sor_inv_sle_sn_trans, sle_next, sle_push, sle_refl_eq, eq_sym/
+/3 width=5 by pr_sor_inv_sle_sn_trans, pr_sle_next, pr_sle_push, pr_sle_refl_eq, pr_eq_sym/
qed-.
(* Basic properties *********************************************************)
-lemma lsubf_eq_repl_back1: ∀f2,L1,L2. eq_repl_back … (λf1. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫).
+lemma lsubf_eq_repl_back1: ∀f2,L1,L2. pr_eq_repl_back … (λf1. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫).
#f2 #L1 #L2 #f #H elim H -f -f2 -L1 -L2
[ #f1 #f2 #Hf12 #g1 #Hfg1
- /3 width=3 by lsubf_atom, eq_canc_sn/
+ /3 width=3 by lsubf_atom, pr_eq_canc_sn/
| #f1 #f2 #I1 #I2 #K1 #K2 #_ #IH #g #H
elim (eq_inv_px … H) -H [|*: // ] #g1 #Hfg1 #H destruct
/3 width=1 by lsubf_push/
/3 width=1 by lsubf_bind/
| #f #f0 #f1 #f2 #K1 #L2 #W #V #Hf #Hf1 #_ #IH #g #H
elim (eq_inv_nx … H) -H [|*: // ] #g1 #Hfg1 #H destruct
- /3 width=5 by lsubf_beta, sor_eq_repl_back3/
+ /3 width=5 by lsubf_beta, pr_sor_eq_repl_back/
| #f #f0 #f1 #f2 #I1 #I2 #K1 #K2 #V #Hf #Hf1 #_ #IH #g #H
elim (eq_inv_nx … H) -H [|*: // ] #g1 #Hfg1 #H destruct
- /3 width=5 by lsubf_unit, sor_eq_repl_back3/
+ /3 width=5 by lsubf_unit, pr_sor_eq_repl_back/
]
qed-.
-lemma lsubf_eq_repl_fwd1: ∀f2,L1,L2. eq_repl_fwd … (λf1. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫).
-#f2 #L1 #L2 @eq_repl_sym /2 width=3 by lsubf_eq_repl_back1/
+lemma lsubf_eq_repl_fwd1: ∀f2,L1,L2. pr_eq_repl_fwd … (λf1. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫).
+#f2 #L1 #L2 @pr_eq_repl_sym /2 width=3 by lsubf_eq_repl_back1/
qed-.
-lemma lsubf_eq_repl_back2: ∀f1,L1,L2. eq_repl_back … (λf2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫).
+lemma lsubf_eq_repl_back2: ∀f1,L1,L2. pr_eq_repl_back … (λf2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫).
#f1 #L1 #L2 #f #H elim H -f1 -f -L1 -L2
[ #f1 #f2 #Hf12 #g2 #Hfg2
- /3 width=3 by lsubf_atom, eq_trans/
+ /3 width=3 by lsubf_atom, pr_eq_trans/
| #f1 #f2 #I1 #I2 #K1 #K2 #_ #IH #g #H
elim (eq_inv_px … H) -H [|*: // ] #g2 #Hfg2 #H destruct
/3 width=1 by lsubf_push/
]
qed-.
-lemma lsubf_eq_repl_fwd2: ∀f1,L1,L2. eq_repl_fwd … (λf2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫).
-#f1 #L1 #L2 @eq_repl_sym /2 width=3 by lsubf_eq_repl_back2/
+lemma lsubf_eq_repl_fwd2: ∀f1,L1,L2. pr_eq_repl_fwd … (λf2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫).
+#f1 #L1 #L2 @pr_eq_repl_sym /2 width=3 by lsubf_eq_repl_back2/
qed-.
lemma lsubf_refl: bi_reflexive … lsubf.
-#L elim L -L /2 width=1 by lsubf_atom, eq_refl/
-#L #I #IH #f elim (pn_split f) * #g #H destruct
+#L elim L -L /2 width=1 by lsubf_atom, pr_eq_refl/
+#L #I #IH #f elim (pr_map_split_tl f) * #g #H destruct
/2 width=1 by lsubf_push, lsubf_bind/
qed.
∀g1,f2,I,L1,L2. ❪L1,g1❫ ⫃𝐅+ ❪L2,⫰f2❫ →
∃∃f1. ❪L1.ⓘ[I],f1❫ ⫃𝐅+ ❪L2.ⓘ[I],f2❫ & g1 = ⫰f1.
#g1 #f2 #I #L1 #L2 #H
-elim (pn_split f2) * #g2 #H2 destruct
+elim (pr_map_split_tl f2) * #g2 #H2 destruct
@ex2_intro [1,2,4,5: /2 width=2 by lsubf_push, lsubf_bind/ ] // (**) (* constructor needed *)
qed-.
∀f2,L2,W. ❪L1,f0❫ ⫃𝐅+ ❪L2,⫰f2❫ →
∃∃f1. ❪L1.ⓓⓝW.V,f1❫ ⫃𝐅+ ❪L2.ⓛW,f2❫ & ⫰f1 ⊆ g1.
#f #f0 #g1 #L1 #V #Hf #Hg1 #f2
-elim (pn_split f2) * #x2 #H2 #L2 #W #HL12 destruct
-[ /3 width=4 by lsubf_push, sor_inv_sle_sn, ex2_intro/
+elim (pr_map_split_tl f2) * #x2 #H2 #L2 #W #HL12 destruct
+[ /3 width=4 by lsubf_push, pr_sor_inv_sle_sn, ex2_intro/
| @(ex2_intro … (↑g1)) /2 width=5 by lsubf_beta/ (**) (* full auto fails *)
]
qed-.
∀f2l,f2r. f2l⋓f2r ≘ f2 →
∃∃f1l,f1r. ❪L1,f1l❫ ⫃𝐅+ ❪L2,f2l❫ & ❪L1,f1r❫ ⫃𝐅+ ❪L2,f2r❫ & f1l⋓f1r ≘ f1.
#f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2
-[ /3 width=7 by sor_eq_repl_fwd3, ex3_2_intro/
+[ /3 width=7 by pr_sor_eq_repl_fwd, ex3_2_intro/
| #g1 #g2 #I1 #I2 #L1 #L2 #_ #IH #f2l #f2r #H
- elim (sor_inv_xxp … H) -H [|*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
- elim (IH … Hg2) -g2 /3 width=11 by lsubf_push, sor_pp, ex3_2_intro/
+ elim (pr_sor_inv_push … H) -H [|*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
+ elim (IH … Hg2) -g2 /3 width=11 by lsubf_push, pr_sor_push_bi, ex3_2_intro/
| #g1 #g2 #I #L1 #L2 #_ #IH #f2l #f2r #H
- elim (sor_inv_xxn … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
- elim (IH … Hg2) -g2 /3 width=11 by lsubf_push, lsubf_bind, sor_np, sor_pn, sor_nn, ex3_2_intro/
+ elim (pr_sor_inv_next … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
+ elim (IH … Hg2) -g2 /3 width=11 by lsubf_push, lsubf_bind, pr_sor_next_push, pr_sor_push_next, pr_sor_next_bi, ex3_2_intro/
| #g #g0 #g1 #g2 #L1 #L2 #W #V #Hg #Hg1 #_ #IH #f2l #f2r #H
- elim (sor_inv_xxn … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
+ elim (pr_sor_inv_next … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
elim (IH … Hg2) -g2 #g1l #g1r #Hl #Hr #Hg0
- [ lapply (sor_comm_23 … Hg0 Hg1 ?) -g0 [3: |*: // ] #Hg1
- /3 width=11 by lsubf_push, lsubf_beta, sor_np, ex3_2_intro/
- | lapply (sor_assoc_dx … Hg1 … Hg0 ??) -g0 [3: |*: // ] #Hg1
- /3 width=11 by lsubf_push, lsubf_beta, sor_pn, ex3_2_intro/
- | lapply (sor_distr_dx … Hg0 … Hg1) -g0 [5: |*: // ] #Hg1
- /3 width=11 by lsubf_beta, sor_nn, ex3_2_intro/
+ [ lapply (pr_sor_comm_23 … Hg0 Hg1 ?) -g0 [3: |*: // ] #Hg1
+ /3 width=11 by lsubf_push, lsubf_beta, pr_sor_next_push, ex3_2_intro/
+ | lapply (pr_sor_assoc_dx … Hg1 … Hg0 ??) -g0 [3: |*: // ] #Hg1
+ /3 width=11 by lsubf_push, lsubf_beta, pr_sor_push_next, ex3_2_intro/
+ | lapply (pr_sor_distr_dx … Hg0 … Hg1) -g0 [5: |*: // ] #Hg1
+ /3 width=11 by lsubf_beta, pr_sor_next_bi, ex3_2_intro/
]
| #g #g0 #g1 #g2 #I1 #I2 #L1 #L2 #V #Hg #Hg1 #_ #IH #f2l #f2r #H
- elim (sor_inv_xxn … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
+ elim (pr_sor_inv_next … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
elim (IH … Hg2) -g2 #g1l #g1r #Hl #Hr #Hg0
- [ lapply (sor_comm_23 … Hg0 Hg1 ?) -g0 [3: |*: // ] #Hg1
- /3 width=11 by lsubf_push, lsubf_unit, sor_np, ex3_2_intro/
- | lapply (sor_assoc_dx … Hg1 … Hg0 ??) -g0 [3: |*: // ] #Hg1
- /3 width=11 by lsubf_push, lsubf_unit, sor_pn, ex3_2_intro/
- | lapply (sor_distr_dx … Hg0 … Hg1) -g0 [5: |*: // ] #Hg1
- /3 width=11 by lsubf_unit, sor_nn, ex3_2_intro/
+ [ lapply (pr_sor_comm_23 … Hg0 Hg1 ?) -g0 [3: |*: // ] #Hg1
+ /3 width=11 by lsubf_push, lsubf_unit, pr_sor_next_push, ex3_2_intro/
+ | lapply (pr_sor_assoc_dx … Hg1 … Hg0 ??) -g0 [3: |*: // ] #Hg1
+ /3 width=11 by lsubf_push, lsubf_unit, pr_sor_push_next, ex3_2_intro/
+ | lapply (pr_sor_distr_dx … Hg0 … Hg1) -g0 [5: |*: // ] #Hg1
+ /3 width=11 by lsubf_unit, pr_sor_next_bi, ex3_2_intro/
]
]
qed-.
[ /3 width=5 by lsubf_fwd_isid_dx, frees_sort/
| #f2 #i #Hf2 #g1 #Y1 #H
elim (lsubf_inv_atom2 … H) -H #Hg1 #H destruct
- elim (eq_inv_pushs_dx … Hg1) -Hg1 #g #Hg #H destruct
+ elim (pr_eq_inv_pushs_dx … Hg1) -Hg1 #g #Hg #H destruct
elim (eq_inv_xn … Hg) -Hg
- /3 width=3 by frees_atom, isid_eq_repl_fwd/
+ /3 width=3 by frees_atom, pr_isi_eq_repl_fwd/
| #f2 #I #K2 #W #_ #IH #g1 #Y1 #H elim (lsubf_inv_pair2 … H) -H *
[ #f1 #K1 #H12 #H1 #H2 destruct /3 width=1 by frees_pair/
| #f #f0 #f1 #K1 #V #H12 #Hf #Hf1 #H1 #H2 #H3 destruct
[ #f1 #L1 #H12 #H1 #H2 destruct
/3 width=5 by lsubf_fwd_isid_dx, frees_unit/
| #f #f0 #f1 #J #L1 #V #H12 #Hf #Hf1 #H1 #H2 destruct
- /5 width=9 by lsubf_fwd_isid_dx, frees_eq_repl_back, frees_pair, sor_isid_inv_sn/
+ /5 width=9 by lsubf_fwd_isid_dx, frees_eq_repl_back, frees_pair, pr_sor_inv_isi_sn/
]
| #f2 #I #L2 #i #_ #IH #g1 #L1 #H elim (lsubf_inv_push2 … H) -H
/3 width=1 by frees_lref/
[ #L #g1 #f1 #H1 #g2 #f2 #H2 #g #Hg #f #Hf
elim (lsubf_inv_atom1 … H1) -H1 #H1 #H destruct
lapply (lsubf_inv_atom … H2) -H2 #H2
- /5 width=4 by lsubf_atom, sor_mono, sor_eq_repl_back2, sor_eq_repl_back1/
+ /5 width=4 by lsubf_atom, pr_sor_mono, pr_sor_eq_repl_back_dx, pr_sor_eq_repl_back_sn/
| #K #J #IH #L #g1 #f1 #H1 #g2 #f2 #H2 #g #Hg #f #Hf
- elim (pn_split g1) * #y1 #H destruct
- elim (pn_split g2) * #y2 #H destruct
- [ elim (sor_inv_ppx … Hg) -Hg [|*: // ] #y #Hy #H destruct
+ elim (pr_map_split_tl g1) * #y1 #H destruct
+ elim (pr_map_split_tl g2) * #y2 #H destruct
+ [ elim (pr_sor_inv_push_bi … Hg) -Hg [|*: // ] #y #Hy #H destruct
elim (lsubf_inv_push1 … H1) -H1 #x1 #Z1 #Y1 #H1 #H #H0 destruct
elim (lsubf_inv_push_sn … H2) -H2 #x2 #H2 #H destruct
- elim (sor_inv_ppx … Hf) -Hf [|*: // ] #x #Hx #H destruct
+ elim (pr_sor_inv_push_bi … Hf) -Hf [|*: // ] #x #Hx #H destruct
/3 width=8 by lsubf_push/
- | elim (sor_inv_pnx … Hg) -Hg [|*: // ] #y #Hy #H destruct
+ | elim (pr_sor_inv_push_next … Hg) -Hg [|*: // ] #y #Hy #H destruct
elim (lsubf_inv_push1 … H1) -H1 #x1 #Z1 #Y1 #H1 #H #H0 destruct
generalize in match H2; -H2 cases J -J #J [| #V ] #H2
[ elim (lsubf_inv_unit1 … H2) -H2 #x2 #Y2 #H2 #H #H0 destruct
| #y3 #y4 #x2 #Z2 #Y2 #H2 #Hy3 #Hy2 #H #H0 destruct
]
]
- elim (sor_inv_pnx … Hf) -Hf [1,6,11,16:|*: // ] #x #Hx #H destruct
- /3 width=12 by lsubf_unit, lsubf_beta, lsubf_bind, sor_assoc_sn/
- | elim (sor_inv_npx … Hg) -Hg [|*: // ] #y #Hy #H destruct
+ elim (pr_sor_inv_push_next … Hf) -Hf [1,6,11,16:|*: // ] #x #Hx #H destruct
+ /3 width=12 by lsubf_unit, lsubf_beta, lsubf_bind, pr_sor_assoc_sn/
+ | elim (pr_sor_inv_next_push … Hg) -Hg [|*: // ] #y #Hy #H destruct
elim (lsubf_inv_push1 … H2) -H2 #x2 #Z2 #Y2 #H2 #H #H0 destruct
generalize in match H1; -H1 cases J -J #J [| #V ] #H1
[ elim (lsubf_inv_unit1 … H1) -H1 #x1 #Y1 #H1 #H #H0 destruct
| #y3 #y4 #x1 #Z1 #Y1 #H1 #Hy3 #Hy1 #H #H0 destruct
]
]
- elim (sor_inv_npx … Hf) -Hf [1,6,11,16:|*: // ] #x #Hx #H destruct
- /3 width=12 by lsubf_unit, lsubf_beta, lsubf_bind, sor_comm_23/
- | elim (sor_inv_nnx … Hg) -Hg [|*: // ] #y #Hy #H destruct
+ elim (pr_sor_inv_next_push … Hf) -Hf [1,6,11,16:|*: // ] #x #Hx #H destruct
+ /3 width=12 by lsubf_unit, lsubf_beta, lsubf_bind, pr_sor_comm_23/
+ | elim (pr_sor_inv_next_bi … Hg) -Hg [|*: // ] #y #Hy #H destruct
generalize in match H2; generalize in match H1; -H1 -H2 cases J -J #J [| #V ] #H1 #H2
[ elim (lsubf_inv_unit1 … H1) -H1 #x1 #Y1 #H1 #H #H0 destruct
elim (lsubf_inv_bind_sn … H2) -H2 #x2 #H2 #H destruct
| #y3 #y4 #x1 #Y1 #W #U #H1 #Hy3 #Hy1 #H #H0 #H3 #H4 destruct
elim (lsubf_inv_beta_sn … H2) -H2 #z3 #z4 #x2 #H2 #Hz3 #Hy2 #H destruct
lapply (frees_mono … Hz3 … Hy3) -Hz3 #H3
- lapply (sor_eq_repl_back2 … Hy2 … H3) -z3 #Hy2
+ lapply (pr_sor_eq_repl_back_dx … Hy2 … H3) -z3 #Hy2
| #y3 #y4 #x1 #Z1 #Y1 #H1 #Hy3 #Hy1 #H #H0 destruct
elim (lsubf_inv_unit_sn … H2) -H2 #z3 #z4 #x2 #H2 #Hz3 #Hy2 #H destruct
lapply (frees_mono … Hz3 … Hy3) -Hz3 #H3
- lapply (sor_eq_repl_back2 … Hy2 … H3) -z3 #Hy2
+ lapply (pr_sor_eq_repl_back_dx … Hy2 … H3) -z3 #Hy2
]
]
- elim (sor_inv_nnx … Hf) -Hf [1,6,11,16:|*: // ] #x #Hx #H destruct
- /3 width=12 by lsubf_unit, lsubf_beta, lsubf_bind, sor_coll_dx/
+ elim (pr_sor_inv_next_bi … Hf) -Hf [1,6,11,16:|*: // ] #x #Hx #H destruct
+ /3 width=12 by lsubf_unit, lsubf_beta, lsubf_bind, pr_sor_coll_dx/
]
]
qed-.
lemma lsubf_fwd_lsubr_isdiv:
∀f1,f2,L1,L2. ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫ → 𝛀❪f1❫ → 𝛀❪f2❫ → L1 ⫃ L2.
#f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2
-/4 width=3 by lsubr_bind, isdiv_inv_next/
+/4 width=3 by lsubr_bind, pr_isd_inv_next/
[ #f1 #f2 #I1 #I2 #L1 #L2 #_ #_ #H
- elim (isdiv_inv_push … H) //
-| /5 width=5 by lsubf_fwd_sle, lsubr_beta, sle_inv_isdiv_sn, isdiv_inv_next/
-| /5 width=5 by lsubf_fwd_sle, lsubr_unit, sle_inv_isdiv_sn, isdiv_inv_next/
+ elim (pr_isd_inv_push … H) //
+| /5 width=5 by lsubf_fwd_sle, lsubr_beta, pr_sle_inv_isd_sn, pr_isd_inv_next/
+| /5 width=5 by lsubf_fwd_sle, lsubr_unit, pr_sle_inv_isd_sn, pr_isd_inv_next/
]
qed-.
lemma lsubr_lsubf_isid:
∀L1,L2. L1 ⫃ L2 → ∀f1,f2. 𝐈❪f1❫ → 𝐈❪f2❫ → ❪L1,f1❫ ⫃𝐅+ ❪L2,f2❫.
#L1 #L2 #H elim H -L1 -L2
-[ /3 width=1 by lsubf_atom, isid_inv_eq_repl/
+[ /3 width=1 by lsubf_atom, pr_isi_inv_eq_repl/
| #I #L1 #L2 | #L1 #L2 #V #W | #I1 #I2 #L1 #L2 #V
]
#_ #IH #f1 #f2 #Hf1 #Hf2
-elim (isid_inv_gen … Hf1) -Hf1 #g1 #Hg1 #H destruct
-elim (isid_inv_gen … Hf2) -Hf2 #g2 #Hg2 #H destruct
+elim (pr_isi_inv_gen … Hf1) -Hf1 #g1 #Hg1 #H destruct
+elim (pr_isi_inv_gen … Hf2) -Hf2 #g2 #Hg2 #H destruct
/3 width=1 by lsubf_push/
qed.
| #f2 #i #Hf2 #Y1 #HY1
>(lsubr_inv_atom2 … HY1) -Y1 #g1 #Hg1
elim (frees_inv_atom … Hg1) -Hg1 #f1 #Hf1 #H destruct
- /5 width=5 by lsubf_atom, isid_inv_eq_repl, pushs_eq_repl, eq_next/
+ /5 width=5 by lsubf_atom, pr_isi_inv_eq_repl, pr_pushs_eq_repl, pr_eq_next/
| #f2 #Z #L2 #W #_ #IH #Y1 #HY1 #g1 #Hg1 elim (lsubr_inv_pair2 … HY1) -HY1 *
[ #L1 #HL12 #H destruct
elim (frees_inv_pair … Hg1) -Hg1 #f1 #Hf1 #H destruct
/3 width=1 by lsubf_bind, lsubr_lsubf_isid/
| #I #L1 #V #HL12 #H destruct
elim (frees_inv_pair … Hg1) -Hg1 #f1 #Hf1 #H destruct
- /3 width=5 by lsubf_unit, sor_isid_sn, lsubr_lsubf_isid/
+ /3 width=5 by lsubf_unit, pr_sor_isi_sn, lsubr_lsubf_isid/
]
| #f2 #I2 #L2 #i #_ #IH #Y1 #HY1 #g1 #Hg1
elim (lsubr_fwd_bind2 … HY1) -HY1 #I1 #L1 #HL12 #H destruct
(* Basic_2A1: was: lleq *)
definition req: relation3 term lenv lenv ≝
- reqg (eq …).
+ reqg (pr_eq …).
interpretation
"syntactic equivalence on referred entries (local environment)"
>(teqg_inv_gref1 … H1) -X /2 width=1 by frees_gref/
| #f1V #f1T #f1 #p #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #X #H1
elim (teqg_inv_pair1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H1 #L2 #HL12 destruct
- /6 width=5 by frees_bind, sex_inv_tl, ext2_pair, sle_sex_trans, sor_inv_sle_dx, sor_inv_sle_sn/
+ /6 width=5 by frees_bind, sex_inv_tl, ext2_pair, sle_sex_trans, pr_sor_inv_sle_dx, pr_sor_inv_sle_sn/
| #f1V #f1T #f1 #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #X #H1
elim (teqg_inv_pair1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H1 #L2 #HL12 destruct
- /5 width=5 by frees_flat, sle_sex_trans, sor_inv_sle_dx, sor_inv_sle_sn/
+ /5 width=5 by frees_flat, sle_sex_trans, pr_sor_inv_sle_dx, pr_sor_inv_sle_sn/
]
qed-.
rex_fsle_compatible (ceqg S).
#S #HS #L1 #L2 #T #HL12
elim (frees_total L1 T) #f #Hf
-/4 width=8 by frees_reqg_conf, rex_fwd_length, lveq_length_eq, sle_refl, ex4_4_intro/
+/4 width=8 by frees_reqg_conf, rex_fwd_length, lveq_length_eq, pr_sle_refl, ex4_4_intro/
qed.
(* Advanced properties ******************************************************)
#R * [ | #Y1 #I1 ] #Y2 #s * #f #H1 #H2
[ lapply (sex_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/
| lapply (frees_inv_sort … H1) -H1 #Hf
- elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct
+ elim (pr_isi_inv_gen … Hf) -Hf #g #Hg #H destruct
elim (sex_inv_push1 … H2) -H2 #I2 #L2 #H12 #_ #H destruct
/5 width=7 by frees_sort, ex3_4_intro, ex2_intro, or_intror/
]
#R * [ | #Y1 #I1 ] #Y2 #l * #f #H1 #H2
[ lapply (sex_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/
| lapply (frees_inv_gref … H1) -H1 #Hf
- elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct
+ elim (pr_isi_inv_gen … Hf) -Hf #g #Hg #H destruct
elim (sex_inv_push1 … H2) -H2 #I2 #L2 #H12 #_ #H destruct
/5 width=7 by frees_gref, ex3_4_intro, ex2_intro, or_intror/
]
∀p,I,L1,L2,V1,V2,T. L1 ⪤[R,ⓑ[p,I]V1.T] L2 → R L1 V1 V2 →
∧∧ L1 ⪤[R,V1] L2 & L1.ⓑ[I]V1 ⪤[R,T] L2.ⓑ[I]V2.
#R #p #I #L1 #L2 #V1 #V2 #T * #f #Hf #HL #HV elim (frees_inv_bind … Hf) -Hf
-/6 width=6 by sle_sex_trans, sex_inv_tl, ext2_pair, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/
+/6 width=6 by sle_sex_trans, sex_inv_tl, ext2_pair, pr_sor_inv_sle_dx, pr_sor_inv_sle_sn, ex2_intro, conj/
qed-.
(* Basic_2A1: uses: llpx_sn_inv_flat *)
∀I,L1,L2,V,T. L1 ⪤[R,ⓕ[I]V.T] L2 →
∧∧ L1 ⪤[R,V] L2 & L1 ⪤[R,T] L2.
#R #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_flat … Hf) -Hf
-/5 width=6 by sle_sex_trans, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/
+/5 width=6 by sle_sex_trans, pr_sor_inv_sle_dx, pr_sor_inv_sle_sn, ex2_intro, conj/
qed-.
(* Advanced inversion lemmas ************************************************)
∀I,L1,L2,V,T. L1 ⪤[R,②[I]V.T] L2 → L1 ⪤[R,V] L2.
#R * [ #p ] #I #L1 #L2 #V #T * #f #Hf #HL
[ elim (frees_inv_bind … Hf) | elim (frees_inv_flat … Hf) ] -Hf
-/4 width=6 by sle_sex_trans, sor_inv_sle_sn, ex2_intro/
+/4 width=6 by sle_sex_trans, pr_sor_inv_sle_sn, ex2_intro/
qed-.
(* Basic_2A1: uses: llpx_sn_fwd_bind_dx llpx_sn_fwd_bind_O_dx *)
lemma rex_fwd_dx (R):
∀I2,L1,K2,T. L1 ⪤[R,T] K2.ⓘ[I2] →
∃∃I1,K1. L1 = K1.ⓘ[I1].
-#R #I2 #L1 #K2 #T * #f elim (pn_split f) * #g #Hg #_ #Hf destruct
+#R #I2 #L1 #K2 #T * #f elim (pr_map_split_tl f) * #g #Hg #_ #Hf destruct
[ elim (sex_inv_push2 … Hf) | elim (sex_inv_next2 … Hf) ] -Hf #I1 #K1 #_ #_ #H destruct
/2 width=3 by ex1_2_intro/
qed-.
∀I1,I2,L1,L2,s. L1 ⪤[R,⋆s] L2 → L1.ⓘ[I1] ⪤[R,⋆s] L2.ⓘ[I2].
#R #I1 #I2 #L1 #L2 #s * #f #Hf #H12
lapply (frees_inv_sort … Hf) -Hf
-/4 width=3 by frees_sort, sex_push, isid_push, ex2_intro/
+/4 width=3 by frees_sort, sex_push, pr_isi_push, ex2_intro/
qed.
lemma rex_pair (R):
∀I1,I2,L1,L2,l. L1 ⪤[R,§l] L2 → L1.ⓘ[I1] ⪤[R,§l] L2.ⓘ[I2].
#R #I1 #I2 #L1 #L2 #l * #f #Hf #H12
lapply (frees_inv_gref … Hf) -Hf
-/4 width=3 by frees_gref, sex_push, isid_push, ex2_intro/
+/4 width=3 by frees_gref, sex_push, pr_isi_push, ex2_intro/
qed.
lemma rex_bind_repl_dx (R):
∀L,V1,V2. R L V1 V2 → ∀I,T. L.ⓑ[I]V1 ⪤[R,T] L.ⓑ[I]V2.
#R #HR #L #V1 #V2 #HV12 #I #T
elim (frees_total (L.ⓑ[I]V1) T) #f #Hf
-elim (pn_split f) * #g #H destruct
+elim (pr_map_split_tl f) * #g #H destruct
/5 width=3 by sex_refl, sex_next, sex_push, ext2_refl, ext2_pair, ex2_intro/
qed.
lemma rex_inv_bind_void (R):
∀p,I,L1,L2,V,T. L1 ⪤[R,ⓑ[p,I]V.T] L2 → L1 ⪤[R,V] L2 ∧ L1.ⓧ ⪤[R,T] L2.ⓧ.
#R #p #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_bind_void … Hf) -Hf
-/6 width=6 by sle_sex_trans, sex_inv_tl, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/
+/6 width=6 by sle_sex_trans, sex_inv_tl, pr_sor_inv_sle_dx, pr_sor_inv_sle_sn, ex2_intro, conj/
qed-.
(* Advanced forward lemmas **************************************************)
elim (frees_inv_flat … Hg) #y1 #y2 #H #_ #Hy
]
lapply(frees_mono … H … Hf) -H #H1
-lapply (sor_eq_repl_back1 … Hy … H1) -y1 #Hy
-lapply (sor_inv_sle_sn … Hy) -y2 #Hfg
+lapply (pr_sor_eq_repl_back_sn … Hy … H1) -y1 #Hy
+lapply (pr_sor_inv_sle_sn … Hy) -y2 #Hfg
elim (sex_sle_split_sn (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2
lapply (sle_sex_trans … HL1 … Hfg) // #H
elim (frees_sex_conf_fsge … Hf … H) -Hf -H
elim (frees_total L1 (ⓕ[I]V.T)) #g #Hg
elim (frees_inv_flat … Hg) #y1 #y2 #_ #H #Hy
lapply(frees_mono … H … Hf) -H #H2
-lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy
-lapply (sor_inv_sle_dx … Hy) -y1 #Hfg
+lapply (pr_sor_eq_repl_back_dx … Hy … H2) -y2 #Hy
+lapply (pr_sor_inv_sle_dx … Hy) -y1 #Hfg
elim (sex_sle_split_sn (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2
lapply (sle_sex_trans … HL1 … Hfg) // #H
elim (frees_sex_conf_fsge … Hf … H) -Hf -H
elim (frees_total L1 (ⓑ[p,I]V1.T)) #g #Hg
elim (frees_inv_bind … Hg) #y1 #y2 #_ #H #Hy
lapply(frees_mono … H … Hf) -H #H2
-lapply (tl_eq_repl … H2) -H2 #H2
-lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy
-lapply (sor_inv_sle_dx … Hy) -y1 #Hfg
-lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg
+lapply (pr_tl_eq_repl … H2) -H2 #H2
+lapply (pr_sor_eq_repl_back_dx … Hy … H2) -y2 #Hy
+lapply (pr_sor_inv_sle_dx … Hy) -y1 #Hfg
+lapply (pr_sle_inv_tl_sn … Hfg) -Hfg #Hfg
elim (sex_sle_split_sn (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2
lapply (sle_sex_trans … H … Hfg) // #H0
elim (sex_inv_next1 … H) -H #Z #L #HL1 #H
elim (frees_total L1 (ⓑ[p,I]V.T)) #g #Hg
elim (frees_inv_bind_void … Hg) #y1 #y2 #_ #H #Hy
lapply(frees_mono … H … Hf) -H #H2
-lapply (tl_eq_repl … H2) -H2 #H2
-lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy
-lapply (sor_inv_sle_dx … Hy) -y1 #Hfg
-lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg
+lapply (pr_tl_eq_repl … H2) -H2 #H2
+lapply (pr_sor_eq_repl_back_dx … Hy … H2) -y2 #Hy
+lapply (pr_sor_inv_sle_dx … Hy) -y1 #Hfg
+lapply (pr_sle_inv_tl_sn … Hfg) -Hfg #Hfg
elim (sex_sle_split_sn (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2
lapply (sle_sex_trans … H … Hfg) // #H0
elim (sex_inv_next1 … H) -H #Z #L #HL1 #H
∀L1,L2. L1 ⪤[R] L2 → ∀T. L1 ⪤[R,T] L2.
#R #L1 #L2 * #f #Hf #HL12 #T
elim (frees_total L1 T) #g #Hg
-/4 width=5 by sex_sdj, sdj_isid_sn, ex2_intro/
+/4 width=5 by sex_sdj, pr_sdj_isi_sn, ex2_intro/
qed.
(* Inversion lemmas with generic extension of a context sensitive relation **)
#R #H1R #H2R #L1 #L2 #T * #f1 #Hf1 #HL
elim (sex_sdj_split_dx … ceq_ext … HL 𝐢) -HL
[ #L0 #HL10 #HL02
- lapply (sex_sdj … HL02 f1 ?) /2 width=1 by sdj_isid_sn/ #H
+ lapply (sex_sdj … HL02 f1 ?) /2 width=1 by pr_sdj_isi_sn/ #H
/3 width=5 by (* 2x *) ex2_intro/
-|*: /2 width=1 by ext2_refl, sdj_isid_dx/
+|*: /2 width=1 by ext2_refl, pr_sdj_isi_dx/
#g #I #K #n #HLK #Hg @H2R /width=7 by/ (**) (* no auto with H2R *)
]
qed-.
∃∃L. L1 ⪤[R] L & L ≡[T] L2.
#R #H1R #H2R #L1 #L2 #T * #f1 #Hf1 #HL
elim (sex_sdj_split_sn … ceq_ext … HL 𝐢 ?) -HL
-[ #L0 #HL10 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ] -H1R
-lapply (sex_sdj … HL10 f1 ?) /2 width=1 by sdj_isid_sn/ #H
+[ #L0 #HL10 #HL02 |*: /2 width=1 by ext2_refl, pr_sdj_isi_dx/ ] -H1R
+lapply (sex_sdj … HL10 f1 ?) /2 width=1 by pr_sdj_isi_sn/ #H
elim (frees_sex_conf_fsge … Hf1 … H) // -H2R -H #f0 #Hf0 #Hf01
/4 width=7 by sle_sex_trans, (* 2x *) ex2_intro/
qed-.
∀L1,L2,V1,V2,T. L1 ⪤[R,V1] L2 → L1.ⓑ[I]V1 ⪤[R,T] L2.ⓑ[I]V2 →
L1 ⪤[R,ⓑ[p,I]V1.T] L2.
#R #p #I #L1 #L2 #V1 #V2 #T * #f1 #HV #Hf1 * #f2 #HT #Hf2
-lapply (sex_fwd_bind … Hf2) -Hf2 #Hf2 elim (sor_isfin_ex f1 (⫰f2))
-/3 width=7 by frees_fwd_isfin, frees_bind, sex_join, isfin_tl, ex2_intro/
+lapply (sex_fwd_bind … Hf2) -Hf2 #Hf2 elim (pr_sor_isf_bi f1 (⫰f2))
+/3 width=7 by frees_fwd_isfin, frees_bind, sex_join, pr_isf_tl, ex2_intro/
qed.
(* Basic_2A1: llpx_sn_flat *)
theorem rex_flat (R) (I):
∀L1,L2,V,T. L1 ⪤[R,V] L2 → L1 ⪤[R,T] L2 → L1 ⪤[R,ⓕ[I]V.T] L2.
-#R #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2 elim (sor_isfin_ex f1 f2)
+#R #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2 elim (pr_sor_isf_bi f1 f2)
/3 width=7 by frees_fwd_isfin, frees_flat, sex_join, ex2_intro/
qed.
theorem rex_bind_void (R) (p) (I):
∀L1,L2,V,T. L1 ⪤[R,V] L2 → L1.ⓧ ⪤[R,T] L2.ⓧ → L1 ⪤[R,ⓑ[p,I]V.T] L2.
#R #p #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2
-lapply (sex_fwd_bind … Hf2) -Hf2 #Hf2 elim (sor_isfin_ex f1 (⫰f2))
-/3 width=7 by frees_fwd_isfin, frees_bind_void, sex_join, isfin_tl, ex2_intro/
+lapply (sex_fwd_bind … Hf2) -Hf2 #Hf2 elim (pr_sor_isf_bi f1 (⫰f2))
+/3 width=7 by frees_fwd_isfin, frees_bind_void, sex_join, pr_isf_tl, ex2_intro/
qed.
(* Negated inversion lemmas *************************************************)
(* *)
(**************************************************************************)
-include "ground/lib/arith.ma".
+include "ground/arith/nat_le.ma".
include "static_2/notation/functions/one_0.ma".
include "static_2/notation/functions/two_0.ma".
include "static_2/notation/functions/omega_0.ma".
definition ac_eq (k): ac ≝ mk_ac (eq … k).
interpretation "one (applicability domain)"
- 'Two = (ac_eq (S O)).
+ 'Two = (ac_eq (nsucc nzero)).
interpretation "zero (applicability domain)"
- 'One = (ac_eq O).
+ 'One = (ac_eq nzero).
lemma ac_eq_props (k): ac_props (ac_eq k) ≝ mk_ac_props ….
-#m elim (le_dec m k) #Hm
+#m elim (nle_dec m k) #Hm
[ /3 width=3 by or_introl, ex2_intro/
| @or_intror * #n #Hn #Hmn destruct /2 width=1 by/
]
definition ac_le (k): ac ≝ mk_ac (λn. n ≤ k).
lemma ac_le_props (k): ac_props (ac_le k) ≝ mk_ac_props ….
-#m elim (le_dec m k) #Hm
+#m elim (nle_dec m k) #Hm
[ /3 width=3 by or_introl, ex2_intro/
| @or_intror * #n #Hn #Hmn
- /3 width=3 by transitive_le/
+ /3 width=3 by nle_trans/
]
qed.
lemma acle_le_monotonic_le (k1) (k2):
k1 ≤ k2 → (ac_le k1) ⊆ (ac_le k2).
#k1 #k2 #Hk #m #Hm
-/3 width=3 by acle_refl, transitive_le/
+/3 width=3 by acle_refl, nle_trans/
qed.
lemma acle_eq_le (k): (ac_eq k) ⊆ (ac_le k).
#k #m #Hm destruct
-/2 width=1 by acle_refl, le_n/
+/2 width=1 by nle_refl, acle_refl/
qed.
lemma acle_le_eq (k): (ac_le k) ⊆ (ac_eq k).
#a1 #a #Ha1 #a2 #Ha2 #m1 #Hm1
elim (Ha1 … Hm1) -Ha1 -Hm1 #m #Ha #Hm1
elim (Ha2 … Ha) -Ha2 -Ha #m2 #Ha2 #Hm2
-/3 width=5 by transitive_le, ex2_intro/
+/3 width=5 by nle_trans, ex2_intro/
qed-.
| LBind K I ⇒ (append L K).ⓘ[I]
].
-interpretation "append (local environment)" 'plus L1 L2 = (append L1 L2).
+interpretation "append (local environment)" 'nplus L1 L2 = (append L1 L2).
interpretation "local environment tail binding construction (generic)"
'SnItem I L = (append (LBind LAtom I) L).
#K1 elim K1 -K1
[ * /2 width=1 by conj/
#K2 #I2 #L1 #L2 >append_atom >append_bind #H destruct
- >length_bind >append_length >plus_n_Sm
- #H elim (plus_xSy_x_false … H)
+ >length_bind >append_length >nplus_succ_dx
+ #H elim (succ_nplus_refl_sn … H)
| #K1 #I1 #IH *
[ #L1 #L2 >append_bind >append_atom #H destruct
- >length_bind >append_length >plus_n_Sm #H
- lapply (discr_plus_x_xy … H) -H #H destruct
+ >length_bind >append_length >nplus_succ_dx #H
+ lapply (nplus_refl_sn … H) -H #H destruct
| #K2 #I2 #L1 #L2 >append_bind >append_bind #H1 #H2
elim (destruct_lbind_lbind_aux … H1) -H1 #H1 #H3 destruct (**) (* destruct lemma needed *)
elim (IH … H1) -IH -H1 /2 width=1 by conj/
(* Basic_2A1: was: lenv_ind_alt *)
lemma lenv_ind_tail: ∀Q:predicate lenv.
Q (⋆) → (∀I,L. Q L → Q (ⓘ[I].L)) → ∀L. Q L.
-#Q #IH1 #IH2 #L @(f_ind … length … L) -L #x #IHx * //
+#Q #IH1 #IH2 #L @(wf1_ind_nlt … length … L) -L #x #IHx * //
#L #I -IH1 #H destruct
elim (lenv_case_tail … L) [2: * #K #J ]
#H destruct /3 width=1 by/
(* Basic_1: was: flt_shift *)
lemma rfw_shift: ∀p,I,K,V,T. ♯❨K.ⓑ[I]V,T❩ < ♯❨K,ⓑ[p,I]V.T❩.
-normalize /2 width=1 by monotonic_le_plus_r/
+normalize /2 width=1 by nle_plus_bi_sn/
qed.
lemma rfw_clear: ∀p,I1,I2,K,V,T. ♯❨K.ⓤ[I1],T❩ < ♯❨K,ⓑ[p,I2]V.T❩.
-normalize /4 width=1 by monotonic_le_plus_r, le_S_S/
+normalize /4 width=1 by nle_plus_bi_sn, nle_succ_bi/
qed.
lemma rfw_tpair_sn: ∀I,L,V,T. ♯❨L,V❩ < ♯❨L,②[I]V.T❩.
qed.
lemma rfw_lpair_sn: ∀I,L,V,T. ♯❨L,V❩ < ♯❨L.ⓑ[I]V,T❩.
-normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/
+normalize /3 width=1 by nlt_plus_bi_dx, nle_plus_bi_sn/
qed.
lemma rfw_lpair_dx: ∀I,L,V,T. ♯❨L,T❩ < ♯❨L.ⓑ[I]V,T❩.
-normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/
+normalize /3 width=1 by nlt_plus_bi_dx, nle_plus_bi_sn/
qed.
(* Basic_1: removed theorems 7:
(* Basic_1: was: flt_shift *)
lemma fw_shift: ∀p,I,G,K,V,T. ♯❨G,K.ⓑ[I]V,T❩ < ♯❨G,K,ⓑ[p,I]V.T❩.
-normalize /2 width=1 by monotonic_le_plus_r/
+normalize /2 width=1 by nle_plus_bi_sn/
qed.
lemma fw_clear: ∀p,I1,I2,G,K,V,T. ♯❨G,K.ⓤ[I1],T❩ < ♯❨G,K,ⓑ[p,I2]V.T❩.
-normalize /4 width=1 by monotonic_le_plus_r, le_S_S/
+normalize /4 width=1 by nle_plus_bi_sn, nle_succ_bi/
qed.
lemma fw_tpair_sn: ∀I,G,L,V,T. ♯❨G,L,V❩ < ♯❨G,L,②[I]V.T❩.
qed.
lemma fw_lpair_sn: ∀I,G,L,V,T. ♯❨G,L,V❩ < ♯❨G,L.ⓑ[I]V,T❩.
-normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/
+normalize /3 width=1 by nlt_plus_bi_dx, nle_plus_bi_sn/
qed.
(* Basic_1: removed theorems 7:
]
].
-interpretation "fold (restricted closure)" 'plus L T = (fold L T).
+interpretation "fold (restricted closure)" 'nplus L T = (fold L T).
(* Basic properties *********************************************************)
(* Basic properties *********************************************************)
lemma gw_pair: ∀I,G,T. ♯❨G❩ < ♯❨G.ⓑ[I]T❩.
-normalize /2 width=1 by monotonic_le_plus_r/ qed.
+normalize /2 width=1 by nle_plus_bi_sn/ qed.
(**************************************************************************)
include "ground/lib/bool.ma".
-include "ground/lib/arith.ma".
+include "ground/arith/nat.ma".
(* ITEMS ********************************************************************)
∃∃I,K. |K| = n & L = K. ⓘ[I].
#n *
[ >length_atom #H destruct
-| #L #I >length_bind /3 width=4 by ex2_2_intro, injective_S/
+| #L #I >length_bind /3 width=4 by ex2_2_intro, eq_inv_nsucc_bi/
]
qed-.
(* Basic_2A1: uses: lw_pair *)
lemma lw_bind: ∀I,L. ♯❨L❩ < ♯❨L.ⓘ[I]❩.
-normalize /2 width=1 by monotonic_le_plus_r/ qed.
+normalize /2 width=1 by nle_plus_bi_sn/ qed.
(* Basic_1: removed theorems 4: clt_cong clt_head clt_thead clt_wf_ind *)
(* Basic_1: removed local theorems 1: clt_wf__q_ind *)
lemma lveq_fwd_length_le_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → n1 ≤ |L1|.
#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
-/2 width=1 by le_S_S/
+/2 width=1 by nle_succ_bi/
qed-.
lemma lveq_fwd_length_le_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → n2 ≤ |L2|.
#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
-/2 width=1 by le_S_S/
+/2 width=1 by nle_succ_bi/
qed-.
lemma lveq_fwd_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
∧∧ |L1|-|L2| = n1 & |L2|-|L1| = n2.
#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 /2 width=1 by conj/
-#K1 #K2 #n #_ * #H1 #H2 >length_bind /3 width=1 by minus_Sn_m, conj/
+#K1 #K2 #n #_ * #H1 #H2 >length_bind /3 width=1 by nminus_succ_sn, conj/
qed-.
lemma lveq_length_fwd_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → |L1| ≤ |L2| → 0 = n1.
#L1 #L2 #n1 #n2 #H #HL
elim (lveq_fwd_length … H) -H
->(eq_minus_O … HL) //
+>(nle_inv_eq_zero_minus … HL) //
qed-.
lemma lveq_length_fwd_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → |L2| ≤ |L1| → 0 = n2.
#L1 #L2 #n1 #n2 #H #HL
elim (lveq_fwd_length … H) -H
->(eq_minus_O … HL) //
+>(nle_inv_eq_zero_minus … HL) //
qed-.
lemma lveq_inj_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
lemma lveq_fwd_length_plus: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
|L1| + n2 = |L2| + n1.
#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
-/2 width=2 by injective_plus_r/
+/2 width=2 by eq_inv_nplus_bi_sn/
qed-.
lemma lveq_fwd_length_eq: ∀L1,L2. L1 ≋ⓧ*[0,0] L2 → |L1| = |L2|.
-/3 width=2 by lveq_fwd_length_plus, injective_plus_l/ qed-.
+/3 width=2 by lveq_fwd_length_plus, eq_inv_nplus_bi_dx/ qed-.
lemma lveq_fwd_length_minus: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
|L1| - n1 = |L2| - n2.
-/3 width=3 by lveq_fwd_length_plus, lveq_fwd_length_le_dx, lveq_fwd_length_le_sn, plus_to_minus_2/ qed-.
+/3 width=3 by lveq_fwd_length_plus, lveq_fwd_length_le_dx, lveq_fwd_length_le_sn, nminus_plus_swap/ qed-.
lemma lveq_fwd_abst_bind_length_le: ∀I1,I2,L1,L2,V1,n1,n2.
L1.ⓑ[I1]V1 ≋ⓧ*[n1,n2] L2.ⓘ[I2] → |L1| ≤ |L2|.
lemma lveq_inv_void_dx_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2.ⓧ → |L1| ≤ |L2| →
∃∃m2. L1 ≋ ⓧ*[n1,m2] L2 & 0 = n1 & ↑m2 = n2.
#L1 #L2 #n1 #n2 #H #HL12
-lapply (lveq_fwd_length_plus … H) normalize >plus_n_Sm #H0
-lapply (plus2_le_sn_sn … H0 HL12) -H0 -HL12 #H0
-elim (le_inv_S1 … H0) -H0 #m2 #_ #H0 destruct
+lapply (lveq_fwd_length_plus … H) normalize >nplus_succ_dx #H0
+lapply (nplus_2_des_le_sn_sn … H0 HL12) -H0 -HL12 #H0
+elim (nle_inv_succ_sn … H0) -H0 #m2 #_ #H0 destruct
elim (lveq_inv_void_succ_dx … H) -H /2 width=3 by ex3_intro/
qed-.
#L1 #L2 #HL #n1 #n2 #Hn #m1 #m2 #Hm
elim (lveq_fwd_length … Hn) -Hn #H1 #H2 destruct
elim (lveq_fwd_length … Hm) -Hm #H1 #H2 destruct
->length_bind >eq_minus_S_pred >(eq_minus_O … HL)
-/3 width=4 by plus_minus, and3_intro/
+>length_bind >nminus_succ_dx >(nle_inv_eq_zero_minus … HL)
+/3 width=4 by nminus_plus_comm_23, and3_intro/
qed-.
theorem lveq_inj_void_dx_le: ∀K1,K2. |K1| ≤ |K2| →
(* *)
(**************************************************************************)
-include "static_2/syntax/sh.ma".
+include "ground/arith/nat_plus.ma".
+include "ground/arith/nat_minus.ma".
+include "ground/arith/nat_lt_pred.ma".
+include "static_2/syntax/sh_nexts.ma".
(* SORT DEGREE **************************************************************)
deg_total: ∀s. ∃d. deg o s d;
deg_mono : ∀s,d1,d2. deg o s d1 → deg o s d2 → d1 = d2;
(* compatibility condition *)
- deg_next : â\88\80s,d. deg o s d â\86\92 deg o (⫯[h]s) (↓d)
+ deg_next : â\88\80s,d. deg o s d â\86\92 deg o (â\87¡[h]s) (↓d)
}.
(* Notable specifications ***************************************************)
-definition deg_O: relation nat ≝ λs,d. d = 0.
+definition deg_O: relation nat ≝ λs,d. d = 𝟎.
definition sd_O: sd ≝ mk_sd deg_O.
lemma sd_O_props (h): sd_props h sd_O ≝ mk_sd_props ….
-/2 width=2 by le_n_O_to_eq, le_n, ex_intro/ qed.
+/2 width=2 by nle_inv_zero_dx, nle_refl, ex_intro/ qed.
(* Basic inversion lemmas ***************************************************)
lemma deg_inv_pred (h) (o): sd_props h o →
- â\88\80s,d. deg o (⫯[h]s) (↑d) → deg o s (↑↑d).
+ â\88\80s,d. deg o (â\87¡[h]s) (↑d) → deg o s (↑↑d).
#h #o #Ho #s #d #H1
elim (deg_total … Ho s) #d0 #H0
lapply (deg_next … Ho … H0) #H2
-lapply (deg_mono … Ho … H1 H2) -H1 -H2 #H >H >S_pred
-/2 width=2 by ltn_to_ltO/
+lapply (deg_mono … Ho … H1 H2) -H1 -H2 #H >H <nlt_des_gen
+/2 width=2 by nlt_des_lt_zero_sn/
qed-.
lemma deg_inv_prec (h) (o): sd_props h o →
- ∀s,n,d. deg o ((next h)^n s) (↑d) → deg o s (↑(d+n)).
-#h #o #H0 #s #n elim n -n normalize /3 width=3 by deg_inv_pred/
+ ∀s,n,d. deg o (⇡*[h,n]s) (↑d) → deg o s (↑(d+n)).
+#h #o #H0 #s #n @(nat_ind_succ … n) -n [ // ]
+#n #IH #d <sh_nexts_succ
+#H <nplus_succ_shift
+@IH -IH @(deg_inv_pred … H0) // (**) (* auto fails *)
qed-.
(* Basic properties *********************************************************)
lemma deg_iter (h) (o): sd_props h o →
- ∀s,d,n. deg o s d → deg o ((next h)^n s) (d-n).
-#h #o #Ho #s #d #n elim n -n normalize /3 width=1 by deg_next/
+ ∀s,d,n. deg o s d → deg o (⇡*[h,n]s) (d-n).
+#h #o #Ho #s #d #n @(nat_ind_succ … n) -n [ // ]
+#n #IH #H <nminus_succ_dx <sh_nexts_succ
+/3 width=1 by deg_next/
qed.
lemma deg_next_SO (h) (o): sd_props h o →
- ∀s,d. deg o s (↑d) → deg o (next h s) d.
+ ∀s,d. deg o s (↑d) → deg o (⇡[h]s) d.
/2 width=1 by deg_next/ qed-.
(* Basic_2A1: includes: deg_SO_pos *)
inductive deg_SO (h) (s) (s0): predicate nat ≝
-| deg_SO_succ : ∀n. (next h)^n s0 = s → deg_SO h s s0 (↑n)
-| deg_SO_zero: (∀n. (next h)^n s0 = s → ⊥) → deg_SO h s s0 0
+| deg_SO_succ : ∀n. ⇡*[h,n]s0 = s → deg_SO h s s0 (↑n)
+| deg_SO_zero: (∀n. ⇡*[h,n]s0 = s → ⊥) → deg_SO h s s0 𝟎
.
fact deg_SO_inv_succ_aux (h) (s) (s0):
- ∀n0. deg_SO h s s0 n0 → ∀n. n0 = ↑n → (next h)^n s0 = s.
+ ∀n0. deg_SO h s s0 n0 → ∀n. n0 = ↑n → ⇡*[h,n]s0 = s.
#h #s #s0 #n0 * -n0
[ #n #Hn #x #H destruct //
-| #_ #x #H destruct
+| #_ #x #H elim (eq_inv_zero_nsucc … H)
]
qed-.
(* Basic_2A1: was: deg_SO_inv_pos *)
lemma deg_SO_inv_succ (h) (s) (s0):
- ∀n. deg_SO h s s0 (↑n) → (next h)^n s0 = s.
+ ∀n. deg_SO h s s0 (↑n) → ⇡*[h,n]s0 = s.
/2 width=3 by deg_SO_inv_succ_aux/ qed-.
-lemma deg_SO_refl (h) (s): deg_SO h s s 1.
-#h #s @(deg_SO_succ … 0 ?) //
+lemma deg_SO_refl (h) (s): deg_SO h s s 𝟏.
+#h #s @(deg_SO_succ … 𝟎 ?) //
qed.
definition sd_SO (h) (s): sd ≝ mk_sd (deg_SO h s).
#h #s #Hhd #Hha
@mk_sd_props
[ #s0
- elim (nexts_dec … Hhd s0 s) -Hhd
+ elim (sh_nexts_dec … Hhd s0 s) -Hhd
[ * /3 width=2 by deg_SO_succ, ex_intro/
| /5 width=2 by deg_SO_zero, ex_intro/
]
| #s0 #d1 #d2 * [ #n1 ] #H1 * [1,3: #n2 ] #H2
[ < H2 in H1; -H2 #H
- lapply (nexts_inj … Hha … H) -H #H destruct //
+ lapply (sh_nexts_inj … Hha … H) -H #H destruct //
| elim H1 /2 width=2 by ex_intro/
| elim H2 /2 width=2 by ex_intro/
| //
]
| #s0 #d *
- [ #n #H destruct cases n -n normalize
- [ @deg_SO_zero #n >iter_n_Sm #H
- lapply (nexts_inj … Hha … (↑n) 0 H) -H #H destruct
- | #n @deg_SO_succ >iter_n_Sm //
+ [ #n #H destruct
+ <npred_succ @(nat_ind_succ … n) -n
+ [ @deg_SO_zero #n >(sh_nexts_succ_next h n s0) #H
+ lapply (sh_nexts_inj … Hha ???) -H #H destruct
+ | #n @deg_SO_succ >sh_nexts_swap //
]
- | #H0 @deg_SO_zero #n >iter_n_Sm #H destruct
+ | #H0 @deg_SO_zero #n >sh_nexts_swap #H destruct
/2 width=2 by/
]
]
[ O ⇒ sd_O
| S d ⇒ match d with
[ O ⇒ sd_SO h s
- | _ ⇒ sd_d h (next h s) d
+ | _ ⇒ sd_d h (pr_next h s) d
]
].
∀s1,s2. s1 < s2 → deg_SO h s1 s2 0.
#h #Hh #s1 #s2 #Hs12 @deg_SO_zero * normalize
[ #H destruct
- elim (lt_refl_false … Hs12)
+ elim (nlt_inv_refl … Hs12)
| #n #H
- lapply (next_lt … Hh ((next h)^n s2)) >H -H #H
- lapply (transitive_lt … H Hs12) -s1 #H1
- /3 width=5 by lt_le_false, nexts_le/ (* full auto too slow *)
+ lapply (next_lt … Hh ((pr_next h)^n s2)) >H -H #H
+ lapply (nlt_trans … H Hs12) -s1 #H1
+ /3 width=5 by nlt_ge_false, nexts_le/ (* full auto too slow *)
]
qed.
(* *)
(**************************************************************************)
-include "ground/lib/arith.ma".
-include "static_2/notation/functions/upspoon_2.ma".
+include "ground/arith/nat.ma".
+include "static_2/notation/functions/uparrow_1_0.ma".
(* SORT HIERARCHY ***********************************************************)
(* sort hierarchy specification *)
record sh: Type[0] ≝ {
- next: nat → nat (* next sort in the hierarchy *)
+ sh_next: nat → nat (* next sort in the hierarchy *)
}.
interpretation "next sort (sort hierarchy)"
- 'UpSpoon h s = (next h s).
+ 'UpArrow_1_0 h = (sh_next h).
definition sh_is_next (h): relation nat ≝
- λs1,s2. ⫯[h]s1 = s2.
+ λs1,s2. â\87¡[h]s1 = s2.
(* *)
(**************************************************************************)
+include "ground/arith/nat_lt_minus.ma".
include "static_2/syntax/sh_props.ma".
(* SORT HIERARCHY ***********************************************************)
(* strict monotonicity condition *)
record sh_lt (h): Prop ≝
{
- next_lt: ∀s. s < ⫯[h]s
+ sh_next_lt: ∀s. s < ⇡[h]s
}.
(* Basic properties *********************************************************)
-lemma nexts_le (h): sh_lt h → ∀s,n. s ≤ (next h)^n s.
-#h #Hh #s #n elim n -n [ // ] normalize #n #IH
-lapply (next_lt … Hh ((next h)^n s)) #H
-lapply (le_to_lt_to_lt … IH H) -IH -H /2 width=2 by lt_to_le/
+lemma sh_nexts_le (h): sh_lt h → ∀s,n. s ≤ ⇡*[h,n]s.
+#h #Hh #s #n @(nat_ind_succ … n) -n [ // ] #n #IH <sh_nexts_succ
+lapply (sh_next_lt … Hh ((sh_next h)^n s)) #H
+lapply (nle_nlt_trans … IH H) -IH -H /2 width=2 by nlt_des_le/
qed.
-lemma nexts_lt (h): sh_lt h → ∀s,n. s < (next h)^(↑n) s.
-#h #Hh #s #n normalize
-lapply (nexts_le … Hh s n) #H
-@(le_to_lt_to_lt … H) /2 width=1 by next_lt/
+lemma sh_nexts_lt (h): sh_lt h → ∀s,n. s < ⇡*[h,↑n]s.
+#h #Hh #s #n <sh_nexts_succ
+lapply (sh_nexts_le … Hh s n) #H
+@(nle_nlt_trans … H) /2 width=1 by sh_next_lt/
qed.
lemma sh_lt_nexts_inv_lt (h): sh_lt h →
- ∀s,n1,n2. (next h)^n1 s < (next h)^n2 s → n1 < n2.
+ ∀s,n1,n2. ⇡*[h,n1]s < ⇡*[h,n2]s → n1 < n2.
#h #Hh
@pull_2 #n1
-elim n1 -n1
-[ #s *
- [ #H elim (lt_refl_false … H)
- | #n2 //
+@(nat_ind_succ … n1) -n1
+[ #s #n2 @(nat_ind_succ … n2) -n2
+ [ #H elim (nlt_inv_refl … H)
+ | #n2 #_ //
]
-| #n1 #IH #s *
- [ >iter_O #H
- elim (lt_refl_false s)
- /3 width=3 by nexts_lt, transitive_lt/
- | #n2 >iter_S >iter_S <(iter_n_Sm … (next h)) <(iter_n_Sm … (next h)) #H
- /3 width=2 by lt_S_S/
+| #n1 #IH #s #n2 @(nat_ind_succ … n2) -n2
+ [ <sh_nexts_zero #H
+ elim (nlt_inv_refl s)
+ /3 width=3 by sh_nexts_lt, nlt_trans/
+ | #n2 #_ <sh_nexts_succ <sh_nexts_succ >sh_nexts_swap >sh_nexts_swap #H
+ /3 width=2 by nlt_succ_bi/
]
]
qed-.
#h #Hh
@mk_sh_acyclic
@pull_2 #n1
-elim n1 -n1
-[ #s * [ // ] #n2 >iter_O #H
- elim (lt_refl_false s) >H in ⊢ (??%); -H
- /2 width=1 by nexts_lt/
-| #n1 #IH #s *
- [ >iter_O #H -IH
- elim (lt_refl_false s) <H in ⊢ (??%); -H
- /2 width=1 by nexts_lt/
- | #n2 >iter_S >iter_S <(iter_n_Sm … (next h)) <(iter_n_Sm … (next h)) #H
- /3 width=2 by eq_f/
+@(nat_ind_succ … n1) -n1
+[ #s #n2 @(nat_ind_succ … n2) -n2 [ // ] #n2 #_ <sh_nexts_zero #H
+ elim (nlt_inv_refl s) >H in ⊢ (??%); -H
+ /2 width=1 by sh_nexts_lt/
+| #n1 #IH #s #n2 @(nat_ind_succ … n2) -n2
+ [ <sh_nexts_zero #H -IH
+ elim (nlt_inv_refl s) <H in ⊢ (??%); -H
+ /2 width=1 by sh_nexts_lt/
+ | #n2 #_ <sh_nexts_succ <sh_nexts_succ >sh_nexts_swap >sh_nexts_swap #H
+ lapply (IH … H) -IH -H //
]
]
qed.
lemma sh_lt_dec (h): sh_lt h → sh_decidable h.
#h #Hh
@mk_sh_decidable #s1 #s2
-elim (lt_or_ge s2 s1) #Hs
+elim (nat_split_lt_ge s2 s1) #Hs
[ @or_intror * #n #H destruct
- @(lt_le_false … Hs) /2 width=1 by nexts_le/ (**) (* full auto too slow *)
-| @(nat_elim_le_sn … Hs) -s1 -s2 #s1 #s2 #IH #Hs12
- elim (lt_or_eq_or_gt s2 (⫯[h]s1)) #Hs21 destruct
- [ elim (le_to_or_lt_eq … Hs12) -Hs12 #Hs12 destruct
+ @(nlt_ge_false … Hs) /2 width=1 by sh_nexts_le/ (**) (* full auto too slow *)
+| @(nle_ind_sn … Hs) -s1 -s2 #s1 #s2 #IH #Hs12
+ elim (nat_split_lt_eq_gt s2 (⇡[h]s1)) #Hs21 destruct
+ [ elim (nle_split_lt_eq … Hs12) -Hs12 #Hs12 destruct
[ -IH @or_intror * #n #H destruct
generalize in match Hs21; -Hs21
- <(iter_O … (next h) s1) in ⊢ (??%→?); <(iter_S … (next h)) #H
+ >sh_nexts_unit #H
lapply (sh_lt_nexts_inv_lt … Hh … H) -H #H
- <(le_n_O_to_eq n) in Hs12;
- /2 width=2 by lt_refl_false, le_S_S_to_le/
+ <(nle_inv_zero_dx n) in Hs12;
+ /2 width=2 by nlt_inv_refl, nle_inv_succ_bi/
| /3 width=2 by ex_intro, or_introl/
]
- | -IH @or_introl @(ex_intro … 1) // (**) (* auto fails *)
- | lapply (transitive_lt s1 ??? Hs21) [ /2 width=1 by next_lt/ ] -Hs12 #Hs12
- elim (IH (s2-⫯[h]s1)) -IH
- [3: /3 width=1 by next_lt, monotonic_lt_minus_r/ ]
- >minus_minus_m_m [2,4: /2 width=1 by lt_to_le/ ] -Hs21
+ | -IH @or_introl @(ex_intro … 𝟏) // (**) (* auto fails *)
+ | lapply (nlt_trans s1 ??? Hs21) [ /2 width=1 by sh_next_lt/ ] -Hs12 #Hs12
+ elim (IH (s2-â\87¡[h]s1)) -IH
+ [3: /3 width=1 by sh_next_lt, nlt_minus_bi_sn/ ]
+ <nminus_minus_dx_refl_sn [2,4: /2 width=1 by nlt_des_le/ ] -Hs21
[ * #n #H destruct
- @or_introl @(ex_intro … (↑n)) >iter_S >iter_n_Sm //
+ @or_introl @(ex_intro … (↑n)) <sh_nexts_succ >sh_nexts_swap //
| #H1 @or_intror * #n #H2 @H1 -H1 destruct
generalize in match Hs12; -Hs12
- <(iter_O … (next h) s1) in ⊢ (?%?→?); #H
+ >(sh_nexts_zero h s1) in ⊢ (?%?→?); #H
lapply (sh_lt_nexts_inv_lt … Hh … H) -H #H
- <(S_pred … H) -H
- @(ex_intro … (↓n)) >(iter_n_Sm … (next h)) >iter_S //
+ >(nlt_des_gen … H) -H
+ @(ex_intro … (↓n)) <sh_nexts_succ >sh_nexts_swap //
]
]
]
--- /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 "ground/arith/nat_succ_iter.ma".
+include "static_2/notation/functions/uparrowstar_2_0.ma".
+include "static_2/syntax/sh.ma".
+
+(* SORT HIERARCHY ***********************************************************)
+
+definition sh_nexts (h) (n): nat → nat ≝ ⇡[h]^n.
+
+interpretation
+ "iterated next sort (sort hierarchy)"
+ 'UpArrowStar_2_0 h n = (sh_nexts h n).
+
+(* Basic constructions *)
+
+lemma sh_nexts_zero (h): ∀s. s = ⇡*[h,𝟎]s.
+// qed.
+
+lemma sh_nexts_unit (h): ⇡[h] ≐ ⇡*[h,𝟏].
+// qed.
+
+lemma sh_nexts_succ (h) (n): ⇡[h] ∘ (⇡*[h,n]) ≐ ⇡*[h,↑n].
+/2 width=1 by niter_succ/ qed.
+
+(* Advanced constructions ****************************)
+
+lemma sh_nexts_swap (h) (n): ⇡[h] ∘ (⇡*[h,n]) ≐ ⇡*[h,n] ∘ ⇡[h].
+/2 width=1 by niter_appl/ qed.
+
+(* Helper constructions *****************************************************)
+
+lemma sh_nexts_succ_next (h) (n): ⇡*[h,n] ∘ (⇡[h]) ≐ ⇡*[h,↑n].
+// qed.
(* *)
(**************************************************************************)
-include "static_2/syntax/sh.ma".
+include "static_2/syntax/sh_nexts.ma".
(* SORT HIERARCHY ***********************************************************)
(* acyclicity condition *)
record sh_acyclic (h): Prop ≝
{
- nexts_inj: ∀s,n1,n2. (next h)^n1 s = (next h)^n2 s → n1 = n2
+(**) (* use extensional equivalence *)
+ sh_nexts_inj: ∀s,n1,n2. ⇡*[h,n1]s = ⇡*[h,n2]s → n1 = n2
}.
(* decidability condition *)
record sh_decidable (h): Prop ≝
{
- nexts_dec: ∀s1,s2. Decidable (∃n. (next h)^n s1 = s2)
+ sh_nexts_dec: ∀s1,s2. Decidable (∃n. ⇡*[h,n]s1 = s2)
}.
(* SYNTACTIC EQUIVALENCE ON TERMS *******************************************)
definition teq: relation term ≝
- teqg (eq …).
+ teqg (pr_eq …).
interpretation
"context-free syntactic equivalence (term)"
(* SYNTACTIC EQUIVALENCE ****************************************************)
definition ceq: relation3 lenv term term ≝
- ceqg (eq …).
+ ceqg (pr_eq …).
definition ceq_ext: lenv → relation bind ≝
- ceqg_ext (eq …).
+ ceqg_ext (pr_eq …).
interpretation
"context-dependent syntactic equivalence (term)"
(* *)
(**************************************************************************)
+include "ground/xoa/or_3.ma".
include "ground/xoa/ex_3_2.ma".
include "static_2/notation/relations/stareq_3.ma".
include "static_2/syntax/term.ma".
qed-.
lemma teqw_inv_cast_xy_y: ∀T,V. ⓝV.T ≃ T → ⊥.
-@(f_ind … tw) #n #IH #T #Hn #V #H destruct
+@(wf1_ind_nlt … tw) #n #IH #T #Hn #V #H destruct
elim (teqw_inv_cast_sn … H) -H #X1 #X2 #_ #HX2 #H destruct -V
/2 width=4 by/
qed-.
rec definition applv Vs T on Vs ≝
match Vs with
[ nil ⇒ T
- | cons hd tl ⇒ ⓐhd. (applv tl T)
+ | cons hd pr_tl ⇒ ⓐhd. (applv pr_tl T)
].
interpretation "application to vector (term)"
qed.
lemma tw_le_pair_dx (I): ∀V,T. ♯❨T❩ < ♯❨②[I]V.T❩.
-#I #V #T /2 width=1 by le_S_S/
+#I #V #T /2 width=1 by nle_succ_bi/
qed.
(* Basic_1: removed theorems 11:
projects / helm.git / commitdiff