]
qed-.
+lemma cpm_tdeq_inv_bind_dx (a) (h) (o) (n) (p) (I) (G) (L):
+ ∀X. ⦃G, L⦄ ⊢ X ![a,h] →
+ ∀V,T2. ⦃G, L⦄ ⊢ X ➡[n,h] ⓑ{p,I}V.T2 → X ≛[h,o] ⓑ{p,I}V.T2 →
+ ∃∃T1. ⦃G,L⦄ ⊢ V ![a,h] & ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ![a,h] & ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛[h,o] T2 & X = ⓑ{p,I}V.T1.
+#a #h #o #n #p #I #G #L #X #H0 #V #T2 #H1 #H2
+elim (tdeq_inv_pair2 … H2) #V0 #T1 #_ #_ #H destruct
+elim (cpm_tdeq_inv_bind_sn … H0 … H1 H2) -H0 -H1 -H2 #T0 #HV #HT1 #H1T12 #H2T12 #H destruct
+/2 width=5 by ex5_intro/
+qed-.
+
(* Eliminators with restricted rt-transition for terms **********************)
lemma cpm_tdeq_ind (a) (h) (o) (n) (G) (Q:relation3 …):
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/dynamic/cnv_cpm_trans.ma".
+include "basic_2/dynamic/cnv_cpm_tdeq.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+definition IH_cnv_cpm_tdeq_cpm_trans (a) (h) (o): relation3 genv lenv term ≝
+ λG,L,T1. ⦃G, L⦄ ⊢ T1 ![a,h] →
+ ∀n1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → T1 ≛[h,o] T →
+ ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
+ ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡[n1,h] T2 & T0 ≛[h,o] T2.
+
+(* Transitive properties restricted rt-transition for terms *****************)
+
+fact cnv_cpm_tdeq_cpm_trans_sub (a) (h) (o) (G0) (L0) (T0):
+ (∀G,L,T. ⦃G0, L0, T0⦄ >[h,o] ⦃G, L, T⦄ → IH_cnv_cpm_trans_lpr a h G L T) →
+ (∀G,L,T. ⦃G0,L0,T0⦄ ⊐+ ⦃G,L,T⦄ → IH_cnv_cpm_tdeq_cpm_trans a h o G L T) →
+ ∀G,L,T1. G0 = G → L0 = L → T0 = T1 → IH_cnv_cpm_tdeq_cpm_trans a h o G L T1.
+#a #h #o #G0 #L0 #T0 #IH2 #IH1 #G #L * [| * [| * ]]
+[ #I #_ #_ #_ #_ #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct -G0 -L0 -T0
+ elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X *
+ [ #H1 #H2 destruct /2 width=4 by ex3_intro/
+ | #s #H1 #H2 #H3 #Hs destruct
+ elim (cpm_inv_sort1 … HX2) -HX2 #H #Hn2 destruct >iter_n_Sm
+ /5 width=6 by cpm_sort_iter, tdeq_sort, deg_iter, deg_next, ex3_intro/
+ ]
+| #p #I #V1 #T1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct
+ elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T #_ #H0T1 #H1T1 #H2T1 #H destruct
+ elim (cpm_inv_bind1 … HX2) -HX2 *
+ [ #V2 #T2 #HV12 #HT2 #H destruct
+ elim (IH1 … H0T1 … H1T1 H2T1 … HT2) -T -IH1 [| // ] #T0 #HT10 #H1T02 #H2T02
+ lapply (IH2 … H0T1 … HT10 (L.ⓑ{I}V1) ?) -IH2 -H0T1 [3:|*: /2 width=1 by fqup_fpbg/ ] #HT0
+ lapply (cpm_tdeq_free … HT0 … H1T02 H2T02 G (L.ⓑ{I}V2)) -H1T02 #H1T02
+ /3 width=6 by cpm_bind, tdeq_pair, ex3_intro/
+ | #T2 #HT2 #HTX2 #H1 #H2 destruct -IH2
+ elim (tdeq_inv_lifts_dx … H2T1 … HT2) -H2T1 #XT #HXT1 #H2XT2
+ lapply (cpm_inv_lifts_bi … H1T1 (Ⓣ) … HXT1 … HT2) -T [3:|*: /3 width=2 by drops_refl, drops_drop/ ] #H1XT2
+ lapply (cnv_inv_lifts … H0T1 (Ⓣ) … HXT1) -H0T1 [3:|*: /3 width=2 by drops_refl, drops_drop/ ] #H0XT2
+ elim (IH1 … H0XT2 … H1XT2 H2XT2 … HTX2) -T2 -IH1 -H0XT2 [| /2 width=1 by fqup_zeta/ ] #T2 #HXT2 #H1TX2 #H2XT2
+ /3 width=4 by cpm_zeta, ex3_intro/
+ ]
+| #V1 #XT1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct
+ elim (cpm_tdeq_inv_appl_sn … H0 … H1X H2X) -H0 -H1X -H2X #m #q #W1 #U1 #XT #_ #_ #_ #_ #H0T1 #H1T1 #H2T1 #H destruct -m -q -W1 -U1
+ elim (cpm_inv_appl1 … HX2) -HX2 *
+ [ #V2 #T2 #HV12 #HT2 #H destruct -IH2
+ elim (IH1 … H0T1 … H1T1 H2T1 … HT2) -XT -IH1 -H0T1 [| // ] #T0 #HT10 #H1T02 #H2T02
+ /3 width=6 by cpm_appl, tdeq_pair, ex3_intro/
+ | #p #V2 #W1 #W2 #T #T2 #HV12 #HW12 #HT2 #H1 #H2 destruct
+ elim (cpm_tdeq_inv_bind_dx … H0T1 … H1T1 H2T1) -H0T1 -H1T1 -H2T1 #T1 #_ #H0T1 #H1T1 #H2T1 #H destruct
+ elim (IH1 … H0T1 … H1T1 H2T1 … HT2) -T -IH1 [| // ] #T0 #HT10 #H1T02 #H2T02
+ lapply (IH2 … H0T1 … HT10 (L.ⓛW1) ?) -IH2 -H0T1 [3:|*: /2 width=1 by fqup_fpbg/ ] #HT0
+ lapply (cpm_tdeq_free … HT0 … H1T02 H2T02 G (L.ⓓⓝW2.V2)) -H1T02 #H1T02
+ /3 width=6 by cpm_beta, cpm_bind, tdeq_pair, ex3_intro/
+ | #p #V2 #V0 #W1 #W2 #T #T2 #HV12 #HV20 #HW12 #HT2 #H1 #H2 destruct
+ elim (cpm_tdeq_inv_bind_dx … H0T1 … H1T1 H2T1) -H0T1 -H1T1 -H2T1 #T1 #_ #H0T1 #H1T1 #H2T1 #H destruct
+ elim (IH1 … H0T1 … H1T1 H2T1 … HT2) -T -IH1 [| // ] #T0 #HT10 #H1T02 #H2T02
+ lapply (IH2 … H0T1 … HT10 (L.ⓓW1) ?) -IH2 -H0T1 [3:|*: /2 width=1 by fqup_fpbg/ ] #HT0
+ lapply (cpm_tdeq_free … HT0 … H1T02 H2T02 G (L.ⓓW2)) -H1T02
+ /4 width=8 by cpm_theta, cpm_appl, cpm_bind, tdeq_pair, ex3_intro/
+ ]
+| #U1 #T1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct -IH2
+ elim (cpm_tdeq_inv_cast_sn … H0 … H1X H2X) -H0 -H1X -H2X #U0 #U #T #_ #_ #H0U1 #H1U1 #H2U1 #H0T1 #H1T1 #H2T1 #H destruct -U0
+ elim (cpm_inv_cast1 … HX2) -HX2 [ * || * ]
+ [ #U2 #T2 #HU2 #HT2 #H destruct
+ elim (IH1 … H0U1 … H1U1 H2U1 … HU2) -U -H0U1 [| // ] #U0 #HU10 #H1U02 #H2U02
+ elim (IH1 … H0T1 … H1T1 H2T1 … HT2) -T -IH1 -H0T1 [| // ] #T0 #HT10 #H1T02 #H2T02
+ /3 width=6 by cpm_cast, tdeq_pair, ex3_intro/
+ | #HTX2 -U -H0U1
+ elim (IH1 … H0T1 … H1T1 H2T1 … HTX2) -T -IH1 -H0T1 [| // ] #T0 #HT10 #H1T02 #H2T02
+ /3 width=4 by cpm_eps, ex3_intro/
+ | #m2 #HUX2 #H destruct -T -H0T1
+ elim (IH1 … H0U1 … H1U1 H2U1 … HUX2) -U -H0U1 [| // ] #U0 #HU10 #H1U02 #H2U02
+ /3 width=4 by cpm_ee, ex3_intro/
+ ]
+]
+qed-.
+
+fact cnv_cpm_tdeq_cpm_trans_aux (a) (h) (o) (G0) (L0) (T0):
+ (∀G,L,T. ⦃G0, L0, T0⦄ >[h, o] ⦃G, L, T⦄ → IH_cnv_cpm_trans_lpr a h G L T) →
+ IH_cnv_cpm_tdeq_cpm_trans a h o G0 L0 T0.
+#a #h #o #G0 #L0 #T0
+@(fqup_wf_ind (Ⓣ) … G0 L0 T0) -G0 -L0 -T0 #G0 #L0 #T0 #IH #IH0
+/5 width=10 by cnv_cpm_tdeq_cpm_trans_sub, fqup_fpbg_trans/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/dynamic/cnv_cpm_tdeq_trans.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Properties with restricted rt-computation for terms **********************)
+
+fact cpms_tdneq_fwd_step_sn_aux (a) (h) (n) (o) (G) (L) (T1):
+ ∀T2. ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G, L⦄ ⊢ T1 ![a,h] → (T1 ≛[h,o] T2 → ⊥) →
+ (∀G0,L0,T0. ⦃G,L,T1⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+ (∀G0,L0,T0. ⦃G,L,T1⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) →
+ ∃∃n1,n2,T0. ⦃G, L⦄ ⊢ T1 ➡[n1,h] T0 & T1 ≛[h,o] T0 → ⊥ & ⦃G, L⦄ ⊢ T0 ➡*[n2,h] T2 & n1+n2 = n.
+#a #h #n #o #G #L #T1 #T2 #H
+@(cpms_ind_sn … H) -n -T1
+[ #_ #H2T2 elim H2T2 -H2T2 //
+| #n1 #n2 #T1 #T #H1T1 #H1T2 #IH #H0T1 #H2T12 #IH2 #IH1
+ elim (tdeq_dec h o T1 T) #H2T1
+ [ elim (tdeq_dec h o T T2) #H2T2
+ [ -IH -IH2 -IH1 -H0T1 /4 width=7 by tdeq_trans, ex4_3_intro/
+ | lapply (cnv_cpm_trans_lpr_aux … IH2 IH1 … H1T1 L ?) [6:|*: // ] -H1T2 -H2T12 #H0T
+ elim (IH H0T H2T2) [|*: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ] -IH -IH2 -H0T -H2T2
+ #m1 #m2 #T0 #H1T0 #H2T0 #H1T02 #H destruct
+ elim (cnv_cpm_tdeq_cpm_trans_aux … IH1 … H0T1 … H1T1 H2T1 … H1T0) -IH1 -H0T1 -H1T1 -H1T0
+ #T3 #H1T13 #H1T30 #H2T30
+ @(ex4_3_intro … H1T13) /4 width=3 by cpms_step_sn, tdeq_canc_sn/ (**) (* explicit constructor *)
+ ]
+ | -IH -IH2 -IH1 -H2T12 /3 width=7 by tdeq_trans, ex4_3_intro/
+ ]
+]
+qed-.
+
+fact cpms_tdeq_ind_sn (a) (h) (o) (G) (L) (T2) (Q:relation2 …):
+ (⦃G, L⦄ ⊢ T2 ![a,h] → Q 0 T2) →
+ (∀n1,n2,T1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → ⦃G, L⦄ ⊢ T1 ![a,h] → T1 ≛[h,o] T → ⦃G, L⦄ ⊢ T ➡*[n2,h] T2 → ⦃G, L⦄ ⊢ T ![a,h] → T ≛[h,o] T2 → Q n2 T → Q (n1+n2) T1) →
+ ∀n,T1. ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G, L⦄ ⊢ T1 ![a,h] → T1 ≛[h,o] T2 →
+ (∀G0,L0,T0. ⦃G,L,T1⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+ (∀G0,L0,T0. ⦃G,L,T1⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) →
+ Q n T1.
+#a #h #o #G #L #T2 #Q #IB1 #IB2 #n #T1 #H
+@(cpms_ind_sn … H) -n -T1
+[ -IB2 #H0T2 #_ #_ #_ /2 width=1 by/
+| #n1 #n2 #T1 #T #H1T1 #H1T2 #IH #H0T1 #H2T12 #IH2 #IH1 -IB1
+ elim (tdeq_dec h o T1 T) #H2T1
+ [ lapply (cnv_cpm_trans_lpr_aux … IH2 IH1 … H1T1 L ?) [6:|*: // ] #H0T
+ lapply (tdeq_canc_sn … H2T1 … H2T12) -H2T12 #H2T2
+ /6 width=7 by cpm_fpbq, fpbq_fpbg_trans/
+ | -IB2 -IH -IH2 -IH1
+ elim (cnv_fpbg_refl_false … o … H0T1) -a -Q
+ /3 width=8 by cpm_tdneq_cpm_cpms_tdeq_sym_fwd_fpbg/
+ ]
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "static_2/syntax/tdpos.ma".
+include "basic_2/dynamic/cnv_cpm_tdeq.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Forward lemmas with positive rt-transition for terms *********************)
+
+lemma cpm_tdeq_fwd_tdpos_sn (a) (h) (o) (n) (G):
+ ∀L,T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
+ ∀T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 → 𝐏[h,o]⦃T1⦄ →
+ ∧∧ T1 = T2 & 0 = n.
+#a #h #o #n #G #L #T1 #H0 #T2 #H1 #H2
+@(cpm_tdeq_ind … H0 … H1 H2) -L -T1 -T2
+[ /2 width=1 by conj/
+| #L #s #_ #H1 #H
+ elim (tdpos_inv_sort … H) -H #d #H2
+ lapply (deg_mono … H2 H1) -H1 -H2 #H destruct
+| #p #I #L #V #T1 #_ #_ #T2 #_ #_ #IH #H
+ elim (tdpos_inv_pair … H) -H #_ #HT1
+ elim IH // -IH -HT1 #H1 #H2 destruct
+ /2 width=1 by conj/
+| #m #_ #L #V #_ #W #_ #q #T1 #U1 #_ #_ #T2 #_ #_ #IH #H -a -m -q -G -L -W -U1
+ elim (tdpos_inv_pair … H) -H #_ #HT1
+ elim IH // -IH -HT1 #H1 #H2 destruct
+ /2 width=1 by conj/
+| #L #U0 #U1 #T1 #_ #_ #U2 #_ #_ #_ #T2 #_ #_ #_ #IHU #IHT #H
+ elim (tdpos_inv_pair … H) -H #HU1 #HT1
+ elim IHU // -IHU -HU1 #H1 #H2 destruct
+ elim IHT // -IHT -HT1 #H1 #H2 destruct
+ /2 width=1 by conj/
+]
+qed-.
+
+lemma cpm_fwd_tdpos_sn (a) (h) (o) (n) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → 𝐏[h,o]⦃T1⦄ →
+ ∀T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 →
+ ∨∨ ∧∧ T1 = T2 & 0 = n | (T1 ≛[h,o] T2 → ⊥).
+#a #h #o #n #G #L #T1 #H1T1 #H2T1 #T2 #HT12
+elim (tdeq_dec h o T1 T2) #H
+/3 width=9 by cpm_tdeq_fwd_tdpos_sn, or_intror, or_introl/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/dynamic/cnv_cpm_tdpos.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Forward lemmas with positive rt-computation for terms ********************)
+
+lemma cpms_fwd_tdpos_sn (a) (h) (o) (n) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → 𝐏[h,o]⦃T1⦄ →
+ ∀T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 →
+ ∨∨ ∧∧ T1 = T2 & 0 = n
+ | ∃∃n1,n2,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T & (T1 ≛[h,o] T → ⊥) & ⦃G,L⦄ ⊢ T ➡*[n2,h] T2 & n1+n2=n.
+#a #h #o #n #G #L #T1 #H1T1 #H2T1 #T2 #H
+@(cpms_ind_dx … H) -n -T2
+[ /3 width=1 by or_introl, conj/
+| #n1 #n2 #T #T2 #HT1 * *
+ [ #H1 #H2 #HT2 destruct -HT1
+ elim (cpm_fwd_tdpos_sn … H1T1 H2T1 … HT2) -H1T1 -H2T1
+ [ * #H1 #H2 destruct -HT2 /3 width=1 by or_introl, conj/
+ | #HnT2 >commutative_plus in ⊢ (??%); /4 width=7 by ex4_3_intro, or_intror/
+ ]
+ | #m1 #m2 #T0 #H1T10 #H2T10 #HT0 #H #HT2 destruct -H1T1 -H2T1 -HT1
+ >associative_plus in ⊢ (??%); /4 width=7 by cpms_step_dx, ex4_3_intro, or_intror/
+ ]
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( 𝐏 [ term 46 h, term 46 o ] ⦃ term 46 T ⦄ )"
+ non associative with precedence 45
+ for @{ 'Positive $h $o $T }.
--- /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 "static_2/notation/relations/positive_3.ma".
+include "static_2/syntax/item_sd.ma".
+include "static_2/syntax/term.ma".
+
+(* DEGREE POSITIVITY ON TERMS ***********************************************)
+
+inductive tdpos (h) (o): predicate term ≝
+| tdpos_sort: ∀s,d. deg h o s (↑d) → tdpos h o (⋆s)
+| tdpos_lref: ∀i. tdpos h o (#i)
+| tdpos_gref: ∀l. tdpos h o (§l)
+| tdpos_pair: ∀I,V,T. tdpos h o V → tdpos h o T → tdpos h o (②{I}V.T)
+.
+
+interpretation
+ "context-free degree positivity (term)"
+ 'Positive h o T = (tdpos h o T).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact tdpos_inv_sort_aux (h) (o):
+ ∀X. 𝐏[h,o]⦃X⦄ → ∀s. X = ⋆s → ∃d. deg h o s (↑d).
+#h #o #H *
+[ #s #d #Hsd #x #H destruct /2 width=2 by ex_intro/
+| #i #x #H destruct
+| #l #x #H destruct
+| #I #V #T #_ #_ #x #H destruct
+]
+qed-.
+
+lemma tdpos_inv_sort (h) (o): ∀s. 𝐏[h,o]⦃⋆s⦄ → ∃d. deg h o s (↑d).
+/2 width=3 by tdpos_inv_sort_aux/ qed-.
+
+fact tdpos_inv_pair_aux (h) (o): ∀X. 𝐏[h,o]⦃X⦄ → ∀I,V,T. X = ②{I}V.T →
+ ∧∧ 𝐏[h,o]⦃V⦄ & 𝐏[h,o]⦃T⦄.
+#h #o #H *
+[ #s #d #_ #Z #X1 #X2 #H destruct
+| #i #Z #X1 #X2 #H destruct
+| #l #Z #X1 #X2 #H destruct
+| #I #V #T #HV #HT #Z #X1 #X2 #H destruct /2 width=1 by conj/
+]
+qed-.
+
+lemma tdpos_inv_pair (h) (o): ∀I,V,T. 𝐏[h,o]⦃②{I}V.T⦄ →
+ ∧∧ 𝐏[h,o]⦃V⦄ & 𝐏[h,o]⦃T⦄.
+/2 width=4 by tdpos_inv_pair_aux/ qed-.
+
+(* Basic properties *********************************************************)
+
+axiom tdpos_total (h): ∀T. ∃o. 𝐏[h,o]⦃T⦄.
(* Forward lemmas with proper parallel rst-computation for closures *********)
-lemma fqup_cpms_fwd_fpbg (h) (o): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T⦄ →
- ∀n,T2. ⦃G2, L2⦄ ⊢ T ➡*[n,h] T2 → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄.
-/3 width=5 by cpms_fwd_fpbs, fqup_fpbg,fpbg_fpbs_trans/ qed-.
-
lemma fpbg_cpms_trans (h) (o) (n): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T⦄ →
∀T2. ⦃G2, L2⦄ ⊢ T ➡*[n,h] T2 → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄.
/3 width=5 by fpbg_fpbs_trans, cpms_fwd_fpbs/ qed-.
lemma cpms_fpbg_trans (h) (o) (n): ∀G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ➡*[n,h] T →
∀G2,L2,T2. ⦃G1, L1, T⦄ >[h,o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄.
/3 width=5 by fpbs_fpbg_trans, cpms_fwd_fpbs/ qed-.
+
+lemma fqup_cpms_fwd_fpbg (h) (o): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T⦄ →
+ ∀n,T2. ⦃G2, L2⦄ ⊢ T ➡*[n,h] T2 → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄.
+/3 width=5 by cpms_fwd_fpbs, fqup_fpbg,fpbg_fpbs_trans/ qed-.
+
+lemma cpm_tdneq_cpm_cpms_tdeq_sym_fwd_fpbg (h) (o) (G) (L) (T1):
+ ∀n1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → (T1 ≛[h,o] T → ⊥) →
+ ∀n2,T2. ⦃G,L⦄⊢ T ➡*[n2,h] T2 → T1 ≛[h,o] T2 → ⦃G,L,T1⦄ >[h,o] ⦃G,L,T1⦄.
+#h #o #G #L #T1 #n1 #T #H1T1 #H2T1 #n2 #T2 #H1T2 #H2T12
+/4 width=7 by cpms_fwd_fpbs, cpm_fpb, fpbs_tdeq_trans, tdeq_sym, ex2_3_intro/
+qed-.
(* *)
(**************************************************************************)
-include "static_2/static/fdeq_fqup.ma".
include "static_2/static/fdeq_fdeq.ma".
include "basic_2/rt_transition/fpbq_fpb.ma".
+include "basic_2/rt_computation/fpbs_fqup.ma".
include "basic_2/rt_computation/fpbg.ma".
(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
#h #o #G1 #G #L1 #L #T1 #T #H @(fpbs_ind … H) -G -L -T /3 width=5 by fpbq_fpbg_trans/
qed-.
+(* Advanced properties with plus-iterated structural successor for closures *)
+
+lemma fqup_fpbg_trans (h) (o):
+ ∀G1,G,L1,L,T1,T. ⦃G1,L1,T1⦄ ⊐+ ⦃G,L,T⦄ →
+ ∀G2,L2,T2. ⦃G,L,T⦄ >[h,o] ⦃G2,L2,T2⦄ → ⦃G1,L1,T1⦄ >[h,o] ⦃G2,L2,T2⦄.
+/3 width=5 by fpbs_fpbg_trans, fqup_fpbs/ qed-.
+
(* Advanced inversion lemmas of parallel rst-computation on closures ********)
(* Basic_2A1: was: fpbs_fpbg *)
]
qed-.
+lemma cpm_inv_abst_bi: ∀n,h,p1,p2,G,L,V1,V2,T1,T2. ⦃G,L⦄ ⊢ ⓛ{p1}V1.T1 ➡[n,h] ⓛ{p2}V2.T2 →
+ ∧∧ ⦃G,L⦄ ⊢ V1 ➡[h] V2 & ⦃G,L.ⓛV1⦄ ⊢ T1 ➡[n,h] T2 & p1 = p2.
+#n #h #p1 #p2 #G #L #V1 #V2 #T1 #T2 #H
+elim (cpm_inv_abst1 … H) -H #XV #XT #HV #HT #H destruct
+/2 width=1 by and3_intro/
+qed-.
+
(* Basic_1: includes: pr0_gen_appl pr2_gen_appl *)
(* Basic_2A1: includes: cpr_inv_appl1 *)
lemma cpm_inv_appl1: ∀n,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐ V1.U1 ➡[n, h] U2 →
*)
[ { "context-sensitive native validity" * } {
[ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ]
- [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdpos" + "cnv_cpms_tdpos" + "cnv_cpms_conf" + "cnv_preserve_sub" + "cnv_preserve" * ]
+ [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tfeq_trans" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_preserve_sub" + "cnv_preserve" * ]
}
]
}
λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≘ U1 →
∀T2. ⬆*[f] T2 ≘ U2 → R T1 T2.
+definition deliftable2_dx: predicate (relation term) ≝
+ λR. ∀U1,U2. R U1 U2 → ∀f,T2. ⬆*[f] T2 ≘ U2 →
+ ∃∃T1. ⬆*[f] T1 ≘ U1 & R T1 T2.
+
(* Basic inversion lemmas ***************************************************)
fact lifts_inv_sort1_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → ∀s. X = ⋆s → Y = ⋆s.
(* Basic properties *********************************************************)
+lemma deliftable2_sn_dx (R): symmetric … R → deliftable2_sn R → deliftable2_dx R.
+#R #H2R #H1R #U1 #U2 #HU12 #f #T2 #HTU2
+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).
#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/
]
qed-.
+lemma tdeq_inv_lifts_dx (h) (o): deliftable2_dx (tdeq h o).
+/3 width=3 by tdeq_inv_lifts_sn, deliftable2_sn_dx, tdeq_sym/ qed-.
+
lemma tdeq_inv_lifts_bi: ∀h,o. deliftable2_bi (tdeq h o).
/3 width=6 by tdeq_inv_lifts_sn, deliftable2_sn_bi/ qed-.
"context-free degree-based equivalence (term)"
'StarEq h o T1 T2 = (tdeq h o T1 T2).
+(* Basic properties *********************************************************)
+
+lemma tdeq_refl: ∀h,o. reflexive … (tdeq h o).
+#h #o #T elim T -T /2 width=1 by tdeq_pair/
+* /2 width=1 by tdeq_lref, tdeq_gref/
+#s elim (deg_total h o s) /2 width=3 by tdeq_sort/
+qed.
+
+lemma tdeq_sym: ∀h,o. symmetric … (tdeq h o).
+#h #o #T1 #T2 #H elim H -T1 -T2
+/2 width=3 by tdeq_sort, tdeq_lref, tdeq_gref, tdeq_pair/
+qed-.
+
(* Basic inversion lemmas ***************************************************)
fact tdeq_inv_sort1_aux: ∀h,o,X,Y. X ≛[h, o] Y → ∀s1. X = ⋆s1 →
∃∃V2,T2. V1 ≛[h, o] V2 & T1 ≛[h, o] T2 & Y = ②{I}V2.T2.
/2 width=3 by tdeq_inv_pair1_aux/ qed-.
+lemma tdeq_inv_pair2: ∀h,o,I,X1,V2,T2. X1 ≛[h, o] ②{I}V2.T2 →
+ ∃∃V1,T1. V1 ≛[h, o] V2 & T1 ≛[h, o] T2 & X1 = ②{I}V1.T1.
+#h #o #I #X1 #V2 #T2 #H
+elim (tdeq_inv_pair1 h o I V2 T2 X1)
+[ #V1 #T1 #HV #HT #H destruct ]
+/3 width=5 by tdeq_sym, ex3_2_intro/
+qed-.
+
(* Advanced inversion lemmas ************************************************)
lemma tdeq_inv_sort1_deg: ∀h,o,Y,s1. ⋆s1 ≛[h, o] Y → ∀d. deg h o s1 d →
/3 width=4 by tdeq_inv_gref1, tdeq_inv_lref1, ex_intro/
qed-.
-(* Basic properties *********************************************************)
-
-lemma tdeq_refl: ∀h,o. reflexive … (tdeq h o).
-#h #o #T elim T -T /2 width=1 by tdeq_pair/
-* /2 width=1 by tdeq_lref, tdeq_gref/
-#s elim (deg_total h o s) /2 width=3 by tdeq_sort/
-qed.
-
-lemma tdeq_sym: ∀h,o. symmetric … (tdeq h o).
-#h #o #T1 #T2 #H elim H -T1 -T2
-/2 width=3 by tdeq_sort, tdeq_lref, tdeq_gref, tdeq_pair/
-qed-.
+(* Advanced properties ******************************************************)
lemma tdeq_dec: ∀h,o,T1,T2. Decidable (T1 ≛[h, o] T2).
#h #o #T1 elim T1 -T1 [ * #s1 | #I1 #V1 #T1 #IHV #IHT ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ]
[ [ "for terms" ] "theq" + "( ? ⩳[?,?] ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ]
}
]
- [ { "degree positivity" * } {
- [ [ "for terms" ] "tdpos" + "( 𝐏[?,?]⦃?⦄ )" * ]
- }
- ]
[ { "degree-based equivalence" * } {
[ [ "" ] "tdeq_ext" + "( ? ≛[?,?] ? )" + "( ? ⊢ ? ≛[?,?] ? )" * ]
[ [ "" ] "tdeq" + "( ? ≛[?,?] ? )" "tdeq_tdeq" * ]
projects / helm.git / commitdiff