-lemma lsubr_cpxs_trans: ∀h,o,G. lsub_trans … (cpxs h o G) lsubr.
-/3 width=5 by lsubr_cpx_trans, LTC_lsub_trans/
-qed-.
lemma cprs_cpxs: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈* T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h] T2.
#h #o #G #L #T1 #T2 #H @(cprs_ind … H) -T2 /3 width=3 by cpxs_strap1,
cpr_cpx/
qed.
-lemma cpxs_inv_cnx1: ∀h,o,G,L,T,U. ⦃G, L⦄ ⊢ T ⬈*[h] U → ⦃G, L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ → T = U.
-#h #o #G #L #T #U #H @(cpxs_ind_dx … H) -T //
-#T0 #T #H1T0 #_ #IHT #H2T0
-lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1 by/
-qed-.
-
lemma cpxs_neq_inv_step_sn: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 = T2 → ⊥) →
∃∃T. ⦃G, L⦄ ⊢ T1 ⬈[h] T & T1 = T → ⊥ & ⦃G, L⦄ ⊢ T ⬈*[h] T2.
#h #o #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1
--- /dev/null
+(* Advanced inversion lemmas ************************************************)
+
+lemma lpxs_inv_pair1: ∀h,o,I,G,K1,L2,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡*[h, o] L2 →
+ ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡*[h, o] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, o] V2 & L2 = K2.ⓑ{I}V2.
+/3 width=3 by TC_lpx_sn_inv_pair1, lpx_cpxs_trans/ qed-.
+
+lemma lpxs_inv_pair2: ∀h,o,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡*[h, o] K2.ⓑ{I}V2 →
+ ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡*[h, o] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, o] V2 & L1 = K1.ⓑ{I}V1.
+/3 width=3 by TC_lpx_sn_inv_pair2, lpx_cpxs_trans/ qed-.
+
+(* Advanced eliminators *****************************************************)
+
+lemma lpxs_ind_alt: ∀h,o,G. ∀R:relation lenv.
+ R (⋆) (⋆) → (
+ ∀I,K1,K2,V1,V2.
+ ⦃G, K1⦄ ⊢ ➡*[h, o] K2 → ⦃G, K1⦄ ⊢ V1 ➡*[h, o] V2 →
+ R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
+ ) →
+ ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → R L1 L2.
+/3 width=4 by TC_lpx_sn_ind, lpx_cpxs_trans/ qed-.
+
+
+(* More advanced properties *************************************************)
+
+lemma lpxs_pair2: ∀h,o,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 →
+ ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡*[h, o] V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, o] L2.ⓑ{I}V2.
+/3 width=3 by lpxs_pair, lpxs_cpxs_trans/ qed.
+
--- /dev/null
+fact tsts_inv_pair2_aux: ∀T1,T2. T1 ≂ T2 → ∀I,W2,U2. T2 = ②{I}W2.U2 →
+ ∃∃W1,U1. T1 = ②{I}W1.U1.
+#T1 #T2 * -T1 -T2
+[ #J #I #W2 #U2 #H destruct
+| #J #V1 #V2 #T1 #T2 #I #W2 #U2 #H destruct /2 width=3 by ex1_2_intro/
+]
+qed-.
+
+lemma tsts_inv_pair2: ∀I,T1,W2,U2. T1 ≂ ②{I}W2.U2 →
+ ∃∃W1,U1. T1 = ②{I}W1.U1.
+/2 width=5 by tsts_inv_pair2_aux/ 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/rt_transition/cnx_cnx.ma".
+include "basic_2/rt_computation/cpxs.ma".
+
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+
+(* Inversion lemmas with normal terms ***************************************)
+
+lemma cpxs_inv_cnx1: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T1⦄ →
+ T1 ≡[h, o] T2.
+#h #o #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1
+/5 width=8 by cnx_tdeq_trans, tdeq_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/rt_transition/cpx_lsubr.ma".
+include "basic_2/rt_computation/cpxs.ma".
+
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+
+(* Properties with restricted refinement for local environments *************)
+
+lemma lsubr_cpxs_trans: ∀h,G. lsub_trans … (cpxs h G) lsubr.
+/3 width=5 by lsubr_cpx_trans, LTC_lsub_trans/
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/syntax/tsts.ma".
+include "basic_2/syntax/tsts_tdeq.ma".
+include "basic_2/rt_computation/cpxs_lsubr.ma".
+include "basic_2/rt_computation/cpxs_cnx.ma".
include "basic_2/rt_computation/lfpxs_cpxs.ma".
(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
(* Forward lemmas with same top term structure ******************************)
-(*
-lemma cpxs_fwd_cnx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → ∀U. ⦃G, L⦄ ⊢ T ⬈*[h, o] U → T ≂ U.
-#h #o #G #L #T #HT #U #H
->(cpxs_inv_cnx1 … H HT) -G -L -T //
-qed-.
-*)
-lemma cpxs_fwd_sort: ∀h,G,L,U,s. ⦃G, L⦄ ⊢ ⋆s ⬈*[h] U →
- ⋆s ≂ U ∨ ⦃G, L⦄ ⊢ ⋆(next h s) ⬈*[h] U.
-#h #G #L #U #s #H elim (cpxs_inv_sort1 … H) -H *
+
+lemma cpxs_fwd_sort: ∀h,o,G,L,U,s. ⦃G, L⦄ ⊢ ⋆s ⬈*[h] U →
+ ⋆s ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⋆(next h s) ⬈*[h] U.
+#h #o #G #L #U #s #H elim (cpxs_inv_sort1 … H) -H *
[ #H destruct /2 width=1 by or_introl/
| #n #H destruct
@or_intror >iter_S <(iter_n_Sm … (next h)) // (**)
qed-.
(* Basic_1: was just: pr3_iso_beta *)
-lemma cpxs_fwd_beta: ∀h,p,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{p}W.T ⬈*[h] U →
- â\93\90V.â\93\9b{p}W.T â\89\82 U ∨ ⦃G, L⦄ ⊢ ⓓ{p}ⓝW.V.T ⬈*[h] U.
-#h #p #G #L #V #W #T #U #H elim (cpxs_inv_appl1 … H) -H *
+lemma cpxs_fwd_beta: ∀h,o,p,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{p}W.T ⬈*[h] U →
+ â\93\90V.â\93\9b{p}W.T ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ ⓓ{p}ⓝW.V.T ⬈*[h] U.
+#h #o #p #G #L #V #W #T #U #H elim (cpxs_inv_appl1 … H) -H *
[ #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/
| #b #W0 #T0 #HT0 #HU
elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct
qed-.
(* Note: probably this is an inversion lemma *)
-lemma cpxs_fwd_delta: ∀h,o,I,G,L,K,V1,i. ⬇[i] L ≡ K.ⓑ{I}V1 →
- ∀V2. ⬆[0, i + 1] V1 ≡ V2 →
- ∀U. ⦃G, L⦄ ⊢ #i ⬈*[h, o] U →
- #i ≂ U ∨ ⦃G, L⦄ ⊢ V2 ⬈*[h, o] U.
+(* Basic_2A1: was: cpxs_fwd_delta *)
+lemma cpxs_fwd_delta_drops: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≡ K.ⓑ{I}V1 →
+ ∀V2. ⬆*[⫯i] V1 ≡ V2 →
+ ∀U. ⦃G, L⦄ ⊢ #i ⬈*[h] U →
+ #i ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ V2 ⬈*[h] U.
#h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #U #H
-elim (cpxs_inv_lref1 … H) -H /2 width=1 by or_introl/
+elim (cpxs_inv_lref1_drops … H) -H /2 width=1 by or_introl/
* #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0
-lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct
-/4 width=10 by cpxs_lift, drop_fwd_drop2, or_intror/
+lapply (drops_mono … HLK0 … HLK) -HLK0 #H destruct
+elim (cpxs_lifts … HVU0 (Ⓣ) … L … HV12) -HVU0 -HV12 /2 width=3 by drops_isuni_fwd_drop2/ #X #H
+<(lifts_mono … HU0 … H) -U0 -X /2 width=1 by or_intror/
qed-.
-lemma cpxs_fwd_theta: ∀h,o,a,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}V.T ⬈*[h, o] U →
- ∀V2. ⬆[0, 1] V1 ≡ V2 → ⓐV1.ⓓ{a}V.T ≂ U ∨
- ⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ⬈*[h, o] U.
-#h #o #a #G #L #V1 #V #T #U #H #V2 #HV12
+lemma cpxs_fwd_theta: ∀h,o,p,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{p}V.T ⬈*[h] U →
+ ∀V2. ⬆*[1] V1 ≡ V2 → ⓐV1.ⓓ{p}V.T ⩳[h, o] U ∨
+ ⦃G, L⦄ ⊢ ⓓ{p}V.ⓐV2.T ⬈*[h] U.
+#h #o #p #G #L #V1 #V #T #U #H #V2 #HV12
elim (cpxs_inv_appl1 … H) -H *
[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/
-| #b #W #T0 #HT0 #HU
+| #q #W #T0 #HT0 #HU
elim (cpxs_inv_abbr1 … HT0) -HT0 *
[ #V3 #T3 #_ #_ #H destruct
| #X #HT2 #H #H0 destruct
- elim (lift_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct
+ elim (lifts_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct
@or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *)
- @(cpxs_trans … (+ⓓV.ⓐV2.ⓛ{b}W2.T2)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T
- @(cpxs_strap2 … (ⓐV1.ⓛ{b}W.T0)) [2: /2 width=1 by cpxs_beta_dx/ ]
- /4 width=7 by cpx_zeta, lift_bind, lift_flat/
+ @(cpxs_trans … (+ⓓV.ⓐV2.ⓛ{q}W2.T2)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T
+ @(cpxs_strap2 … (ⓐV1.ⓛ{q}W.T0)) [2: /2 width=1 by cpxs_beta_dx/ ]
+ /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/
]
-| #b #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU
+| #q #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU
@or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *)
elim (cpxs_inv_abbr1 … HT0) -HT0 *
[ #V5 #T5 #HV5 #HT5 #H destruct
- lapply (cpxs_lift … HV13 (L.ⓓV) … HV12 … HV34) -V1 -V3
- /3 width=2 by cpxs_flat, cpxs_bind, drop_drop/
+ elim (cpxs_lifts … HV13 (Ⓣ) … (L.ⓓV) … HV12) -V1 /3 width=1 by drops_refl, drops_drop/ #X #H
+ <(lifts_mono … HV34 … H) -V3 -X /3 width=1 by cpxs_flat, cpxs_bind/
| #X #HT1 #H #H0 destruct
- elim (lift_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct
- lapply (cpxs_lift … HV13 (L.ⓓV0) … HV12 … HV34) -V3 /2 width=2 by drop_drop/ #HV24
- @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{b}V5.T5)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T
- @(cpxs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V5 -T5
- @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpr_cpx, cpr_theta/
+ elim (lifts_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct
+ elim (cpxs_lifts … HV13 (Ⓣ) … (L.ⓓV0) … HV12) -HV13 /3 width=1 by drops_refl, drops_drop/ #X #H
+ <(lifts_mono … HV34 … H) -V3 -X #HV24
+ @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{q}V5.T5)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T
+ @(cpxs_strap2 … (ⓐV1.ⓓ{q}V0.T0)) [ /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ ] -V -V5 -T5
+ @(cpxs_strap2 … (ⓓ{q}V0.ⓐV2.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpx_theta/
]
]
qed-.
-lemma cpxs_fwd_cast: ∀h,o,G,L,W,T,U. ⦃G, L⦄ ⊢ ⓝW.T ⬈*[h, o] U →
- â\88¨â\88¨ â\93\9dW. T â\89\82 U | â¦\83G, Lâ¦\84 â\8a¢ T â¬\88*[h, o] U | â¦\83G, Lâ¦\84 â\8a¢ W â¬\88*[h, o] U.
+lemma cpxs_fwd_cast: ∀h,o,G,L,W,T,U. ⦃G, L⦄ ⊢ ⓝW.T ⬈*[h] U →
+ â\88¨â\88¨ â\93\9dW. T ⩳[h, o] U | â¦\83G, Lâ¦\84 â\8a¢ T â¬\88*[h] U | â¦\83G, Lâ¦\84 â\8a¢ W â¬\88*[h] U.
#h #o #G #L #W #T #U #H
elim (cpxs_inv_cast1 … H) -H /2 width=1 by or3_intro1, or3_intro2/ *
#W0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or3_intro0/
qed-.
+
+lemma cpxs_fwd_cnx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ →
+ ∀U. ⦃G, L⦄ ⊢ T ⬈*[h] U → T ⩳[h, o] U.
+/3 width=4 by cpxs_inv_cnx1, tdeq_tsts/ qed-.
-cpxs.ma cpxs_tdeq.ma cpxs_drops.ma cpxs_lfpx.ma cpxs_cpxs.ma
+cpxs.ma cpxs_tdeq.ma cpxs_tsts.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma
lfpxs.ma lfpxs_fqup.ma lfpxs_cpxs.ma
csx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma
csx_vector.ma
--- /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/syntax/tdeq_tdeq.ma".
+include "basic_2/rt_transition/lfpx_lfdeq.ma".
+include "basic_2/rt_transition/cnx.ma".
+
+(* NORMAL TERMS FOR UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ******)
+
+(* Advanced properties ******************************************************)
+
+lemma cnx_tdeq_trans: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T1⦄ →
+ ∀T2. T1 ≡[h, o] T2 → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T2⦄.
+#h #o #G #L #T1 #HT1 #T2 #HT12 #T #HT2
+elim (tdeq_cpx_trans … HT12 … HT2) -HT2 #T0 #HT10 #HT0
+lapply (HT1 … HT10) -HT1 -HT10 /2 width=5 by tdeq_repl/ (**) (* full auto fails *)
+qed-.
cpg.ma cpg_simple.ma cpg_drops.ma cpg_lsubr.ma
cpx.ma cpx_simple.ma cpx_drops.ma cpx_fqus.ma cpx_lsubr.ma cpx_lfxs.ma
lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma lfpx_lfdeq.ma lfpx_aaa.ma lfpx_lfpx.ma
-cnx.ma cnx_simple.ma cnx_drops.ma
+cnx.ma cnx_simple.ma cnx_drops.ma cnx_cnx.ma
cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_lfxs.ma cpm_cpx.ma
cpr.ma cpr_drops.ma
lfpr.ma lfpr_length.ma lfpr_drops.ma lfpr_fqup.ma lfpr_frees.ma lfpr_aaa.ma lfpr_lfpx.ma lfpr_lfpr.ma
(**************************************************************************)
include "basic_2/syntax/term_vector.ma".
-include "basic_2/syntax/tsts.ma".
+include "basic_2/syntax/tsts_simple.ma".
(* SAME TOP TERM STRUCTURE **************************************************)
-(* Advanced inversion lemmas ************************************************)
-
+(* Advanced inversion lemmas with simple (neutral) terms ********************)
+(*
(* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *)
-lemma tsts_inv_bind_applv_simple: ∀p,I,Vs,V2,T1,T2. ⒶVs.T1 ≂ ⓑ{p,I}V2.T2 →
+(* Basic_2A1: was: tsts_inv_bind_applv_simple *)
+lemma tsts_inv_applv_bind_simple: ∀h,o,p,I,Vs,V2,T1,T2. ⒶVs.T1 ⩳[h, o] ⓑ{p,I}V2.T2 →
𝐒⦃T1⦄ → ⊥.
-#p #I #Vs #V2 #T1 #T2 #H elim (tsts_inv_pair2 … H) -H
+#h #o #p #I #Vs #V2 #T1 #T2 #H elim (tsts_inv_pair2 … H) -H
#V0 #T0 elim Vs -Vs normalize
[ #H destruct #H /2 width=5 by simple_inv_bind/
| #V #Vs #_ #H destruct
]
qed-.
+*)
[ { "uncounted context-sensitive rt-transition" * } {
(*
[ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
- [ "cpxs_tsts" + "cpxs_tsts_vector" + "cpxs_lreq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ]
+ [ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ]
*)
[ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" * ]
[ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx" + "csx_cpxs" + "csx_csx" * ]
[ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_cpxs" * ]
- [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_drops" + "cpxs_lfpx" + "cpxs_cpxs" * ]
+ [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_tsts" + "cpxs_tsts_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
}
]
}
}
]
[ { "uncounted context-sensitive rt-transition" * } {
- [ "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" * ]
+ [ "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" *+ "cnx_cnx" ]
[ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_lfpx" * ]
[ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" * ]
}
[ "append ( ? @@ ? )" "append_length" * ]
}
]
- [ { "degree-based equivalence for terms" * } {
- [ "deq ( ? ≡[?,?] ? ) " "deq_deq" * ]
+ [ { "same top term structure" * } {
+ [ "tsts ( ? ⩳[?,?] ? )" "tsts_simple" + "tsts_tdeq" + "tsts_tsts" + "tsts_vector" * ]
}
]
- [ { "same top term structure" * } {
- [ "tsts ( ? ≂ ? )" "tsts_tsts" + "tsts_vector" * ]
+ [ { "degree-based equivalence for terms" * } {
+ [ "deq ( ? ≡[?,?] ? ) " "deq_deq" * ]
}
]
[ { "closures" * } {
+../../matitac.opt `cat partial.txt`
cd basic_2/rt_transition/
../../../../matitac.opt `cat partial.txt`
cd ../rt_computation/
projects / helm.git / commitdiff