(* *)
(**************************************************************************)
-include "basic_2/notation/relations/prednormal_5.ma".
include "basic_2/reduction/cnr.ma".
-include "basic_2/reduction/cpx.ma".
-
-(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED REDUCTION ********************)
-
-definition cnx: ∀h. sd h → relation3 genv lenv term ≝
- λh,o,G,L. NF … (cpx h o G L) (eq …).
-
-interpretation
- "normality for context-sensitive extended reduction (term)"
- 'PRedNormal h o L T = (cnx h o L T).
(* Basic inversion lemmas ***************************************************)
-lemma cnx_inv_sort: ∀h,o,G,L,s. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃⋆s⦄ → deg h o s 0.
-#h #o #G #L #s #H elim (deg_total h o s)
-#d @(nat_ind_plus … d) -d // #d #_ #Hkd
-lapply (H (⋆(next h s)) ?) -H /2 width=2 by cpx_st/ -L -d #H
-lapply (destruct_tatom_tatom_aux … H) -H #H (**) (* destruct lemma needed *)
-lapply (destruct_sort_sort_aux … H) -H #H (**) (* destruct lemma needed *)
-lapply (next_lt h s) >H -H #H elim (lt_refl_false … H)
-qed-.
-
-lemma cnx_inv_delta: ∀h,o,I,G,L,K,V,i. ⬇[i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃#i⦄ → ⊥.
-#h #o #I #G #L #K #V #i #HLK #H
-elim (lift_total V 0 (i+1)) #W #HVW
-lapply (H W ?) -H [ /3 width=7 by cpx_delta/ ] -HLK #H destruct
-elim (lift_inv_lref2_be … HVW) -HVW /2 width=1 by ylt_inj/
-qed-.
-
-lemma cnx_inv_abst: ∀h,o,a,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃ⓛ{a}V.T⦄ →
- ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃V⦄ ∧ ⦃G, L.ⓛV⦄ ⊢ ➡[h, o] 𝐍⦃T⦄.
-#h #o #a #G #L #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2 #H destruct //
-]
-qed-.
-
-lemma cnx_inv_abbr: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃-ⓓV.T⦄ →
- ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃V⦄ ∧ ⦃G, L.ⓓV⦄ ⊢ ➡[h, o] 𝐍⦃T⦄.
-#h #o #G #L #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2 #H destruct //
-]
-qed-.
-
lemma cnx_inv_zeta: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃+ⓓV.T⦄ → ⊥.
#h #o #G #L #V #T #H elim (is_lift_dec T 0 1)
[ * #U #HTU
]
qed-.
-lemma cnx_inv_appl: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃ⓐV.T⦄ →
- ∧∧ ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃V⦄ & ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ & 𝐒⦃T⦄.
-#h #o #G #L #V1 #T1 #HVT1 @and3_intro
-[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1 by cpx_pair_sn/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1 by cpx_flat/ -HT2 #H destruct //
-| generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H
- [ elim (lift_total V1 0 1) #V2 #HV12
- lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3 by cpr_cpx, cpr_theta/ -HV12 #H destruct
- | lapply (H (ⓓ{a}ⓝW1.V1.U1) ?) -H /3 width=1 by cpr_cpx, cpr_beta/ #H destruct
- ]
-]
-qed-.
-
-lemma cnx_inv_eps: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃ⓝV.T⦄ → ⊥.
-#h #o #G #L #V #T #H lapply (H T ?) -H
-/2 width=4 by cpx_eps, discr_tpair_xy_y/
-qed-.
-
(* Basic forward lemmas *****************************************************)
lemma cnx_fwd_cnr: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄.
(* Basic properties *********************************************************)
-lemma cnx_sort: ∀h,o,G,L,s. deg h o s 0 → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃⋆s⦄.
-#h #o #G #L #s #Hk #X #H elim (cpx_inv_sort1 … H) -H // * #d #Hkd #_
-lapply (deg_mono … Hkd Hk) -h -L <plus_n_Sm #H destruct
-qed.
-
-lemma cnx_sort_iter: ∀h,o,G,L,s,d. deg h o s d → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃⋆((next h)^d s)⦄.
-#h #o #G #L #s #d #Hkd
-lapply (deg_iter … d Hkd) -Hkd <minus_n_n /2 width=6 by cnx_sort/
-qed.
-
lemma cnx_lref_free: ∀h,o,G,L,i. |L| ≤ i → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃#i⦄.
-#h #o #G #L #i #Hi #X #H elim (cpx_inv_lref1 … H) -H // *
-#I #K #V1 #V2 #HLK lapply (drop_fwd_length_lt2 … HLK) -HLK
-#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/
-qed.
-
-lemma cnx_lref_atom: ∀h,o,G,L,i. ⬇[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃#i⦄.
#h #o #G #L #i #HL @cnx_lref_free >(drop_fwd_length … HL) -HL //
qed.
-lemma cnx_abst: ∀h,o,a,G,L,W,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ →
- ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃ⓛ{a}W.T⦄.
-#h #o #a #G #L #W #T #HW #HT #X #H
-elim (cpx_inv_abst1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
->(HW … HW0) -W0 >(HT … HT0) -T0 //
-qed.
-
-lemma cnx_appl_simple: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃V⦄ → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ → 𝐒⦃T⦄ →
- ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃ⓐV.T⦄.
-#h #o #G #L #V #T #HV #HT #HS #X #H
-elim (cpx_inv_appl1_simple … H) -H // #V0 #T0 #HV0 #HT0 #H destruct
->(HV … HV0) -V0 >(HT … HT0) -T0 //
-qed.
-
axiom cnx_dec: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T1⦄ ∨
∃∃T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 & (T1 = T2 → ⊥).
+++ /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/reduction/cpx_lift.ma".
-include "basic_2/reduction/cnx.ma".
-
-(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED REDUCTION ********************)
-
-(* Relocation properties ****************************************************)
-
-lemma cnx_lift: ∀h,o,G,L0,L,T,T0,c,l,k. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ → ⬇[c, l, k] L0 ≡ L →
- ⬆[l, k] T ≡ T0 → ⦃G, L0⦄ ⊢ ➡[h, o] 𝐍⦃T0⦄.
-#h #o #G #L0 #L #T #T0 #c #l #k #HLT #HL0 #HT0 #X #H
-elim (cpx_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1
-<(HLT … HT1) in HT0; -L #HT0
->(lift_mono … HT10 … HT0) -T1 -X //
-qed.
-
-lemma cnx_inv_lift: ∀h,o,G,L0,L,T,T0,c,l,k. ⦃G, L0⦄ ⊢ ➡[h, o] 𝐍⦃T0⦄ → ⬇[c, l, k] L0 ≡ L →
- ⬆[l, k] T ≡ T0 → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄.
-#h #o #G #L0 #L #T #T0 #c #l #k #HLT0 #HL0 #HT0 #X #H
-elim (lift_total X l k) #X0 #HX0
-lapply (cpx_lift … H … HL0 … HT0 … HX0) -L #HTX0
->(HLT0 … HTX0) in HX0; -L0 -X0 #H
->(lift_inj … H … HT0) -T0 -X -l -k //
-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 G, break term 46 L ⦄ ⊢ ➡ break [ term 46 o , break term 46 h ] 𝐍 break ⦃ term 46 T ⦄ )"
- non associative with precedence 45
- for @{ 'PRedNormal $h $o $G $L $T }.
--- /dev/null
+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
+[ #H elim H -H //
+| #T1 #T #H1 #H2 #IH2 #H12 elim (eq_term_dec T1 T) #H destruct
+ [ -H1 -H2 /3 width=1 by/
+ | -IH2 /3 width=4 by ex3_intro/ (**) (* auto fails without clear *)
+ ]
+]
+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 G, break term 46 L ⦄ ⊢ ➡ break [ term 46 o , break term 46 h ] 𝐍 break ⦃ term 46 T ⦄ )"
+ non associative with precedence 45
+ for @{ 'PRedNormal $h $o $G $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃term 46 G, break term 46 L⦄ ⊢ break term 46 T ⁝ break term 46 A )"
+notation "hvbox( ⦃ term 46 G, break term 46 L⦄ ⊢ break term 46 T ⁝ break term 46 A )"
non associative with precedence 45
for @{ 'AtomicArity $G $L $T $A }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≽ break [ term 46 h, break term 46 o ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≽ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'BTPRed $h $o $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≽ ≽ break [ term 46 h, break term 46 o ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≽ ≽ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'BTPRedAlt $h $o $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≻ break [ term 46 h, break term 46 o ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≻ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'BTPRedProper $h $o $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≥ break [ term 46 h, break term 46 o ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≥ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'BTPRedStar $h $o $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≥ ≥ break [ term 46 h, break term 46 o ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≥ ≥ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'BTPRedStarAlt $h $o $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦥ [ term 46 h, break term 46 o ] break ⦃ term 46 G, break term 46 L, break term 46 T ⦄ )"
+notation "hvbox( ⦥ [ term 46 h, break term 46 o ] ⦃ break term 46 G, break term 46 L, break term 46 T ⦄ )"
non associative with precedence 45
for @{ 'BTSN $h $o $G $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦥ ⦥ [ term 46 h, break term 46 o ] break ⦃ term 46 G, break term 46 L, break term 46 T ⦄ )"
+notation "hvbox( ⦥ ⦥ [ term 46 h, break term 46 o ] ⦃ break term 46 G, break term 46 L, break term 46 T ⦄ )"
non associative with precedence 45
for @{ 'BTSNAlt $h $o $G $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( G ⊢ ~ ⬊ * break [ term 46 h , break term 46 o , break term 46 f ] break term 46 L )"
+notation "hvbox( G ⊢ ~ ⬊ * [ break term 46 h , break term 46 o , break term 46 f ] break term 46 L )"
non associative with precedence 45
for @{ 'CoSN $h $o $f $G $L }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ⬌ * break [ term 46 h , break term 46 o , break term 46 n1 , break term 46 n2 ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ⬌ * [ break term 46 h , break term 46 o , break term 46 n1 , break term 46 n2 ] break term 46 T2 )"
non associative with precedence 45
for @{ 'DPConvStar $h $o $n1 $n2 $G $L $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ➡ * break [ term 46 h , break term 46 o , break term 46 n ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ➡ * [ break term 46 h , break term 46 o , break term 46 n ] break term 46 T2 )"
non associative with precedence 45
for @{ 'DPRedStar $h $o $n $G $L $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( L ⊢ break 𝐅 * ⦃ term 46 T ⦄ ≡ break term 46 f )"
+notation "hvbox( L ⊢ 𝐅 * ⦃ break term 46 T ⦄ ≡ break term 46 f )"
non associative with precedence 45
for @{ 'FreeStar $L $T $f }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L, break term 46 T ⦄ ϵ break [ term 46 R ] break 〚term 46 A 〛 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L, break term 46 T ⦄ ϵ [ break term 46 R ] 〚 break term 46 A 〛 )"
non associative with precedence 45
for @{ 'InEInt $R $G $L $T $A }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ >≡ break [ term 46 h, break term 46 o ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ >≡ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'LazyBTPRedStarProper $h $o $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( L1 ≡ break [ term 46 f ] break term 46 L2 )"
+notation "hvbox( L1 ≡ [ break term 46 f ] break term 46 L2 )"
non associative with precedence 45
for @{ 'LazyEq $f $L1 $L2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( T1 ≡ break [ term 46 h , term 46 o ] break term 46 T2 )"
+notation "hvbox( T1 ≡ [ break term 46 h , term 46 o ] break term 46 T2 )"
non associative with precedence 45
for @{ 'LazyEq $h $o $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( L1 ≡ break [ term 46 h , term 46 o , term 46 T ] break term 46 L2 )"
+notation "hvbox( L1 ≡ [ break term 46 h , break term 46 o , break term 46 T ] break term 46 L2 )"
non associative with precedence 45
for @{ 'LazyEq $h $o $T $L1 $L2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( G ⊢ break term 46 L1 ⫃ break [ term 46 R ] break term 46 L2 )"
+notation "hvbox( G ⊢ break term 46 L1 ⫃ [ break term 46 R ] break term 46 L2 )"
non associative with precedence 45
for @{ 'LRSubEqC $R $G $L1 $L2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 L1, break term 46 f1 ⦄ ⫃ 𝐅* break ⦃ term 46 L2, break term 46 f2 ⦄ )"
+notation "hvbox( ⦃ term 46 L1, break term 46 f1 ⦄ ⫃ 𝐅* ⦃ break term 46 L2, break term 46 f2 ⦄ )"
non associative with precedence 45
for @{ 'LRSubEqF $L1 $f1 $L2 $f2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( G ⊢ break term 46 L1 ⫃ ¡ break [ term 46 h, break term 46 o ] break term 46 L2 )"
+notation "hvbox( G ⊢ break term 46 L1 ⫃ ¡ [ break term 46 h, break term 46 o ] break term 46 L2 )"
non associative with precedence 45
for @{ 'LRSubEqV $h $o $G $L1 $L2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T ¡ break [ term 46 h, break term 46 o ] )"
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T ¡ [ break term 46 h, break term 46 o ] )"
non associative with precedence 45
for @{ 'NativeValid $h $o $G $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T ¡ break [ term 46 h , break term 46 o , break term 46 d ] )"
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T ¡ [ break term 46 h , break term 46 o , break term 46 d ] )"
non associative with precedence 45
for @{ 'NativeValid $h $o $d $G $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ break [ term 46 h ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ [ break term 46 h ] break term 46 T2 )"
non associative with precedence 45
for @{ 'PRed $h $G $L $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ break [ term 46 n, break term 46 h ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ [ break term 46 n, break term 46 h ] break term 46 T2 )"
non associative with precedence 45
for @{ 'PRed $n $h $G $L $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * 𝐍 ⦃ break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'PRedEval $G $L $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break [ term 46 h , break term 46 o ] break 𝐍 ⦃ term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * [ break term 46 h , break term 46 o ] 𝐍 ⦃ break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'PRedEval $h $o $G $L $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ break [ term 46 h , break term 46 T ] break term 46 L2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ [ break term 46 h , break term 46 T ] break term 46 L2 )"
non associative with precedence 45
for @{ 'PRedSn $h $T $G $L1 $L2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ * break [ term 46 h , break term 46 o ] break term 46 L2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ * [ break term 46 h , break term 46 o ] break term 46 L2 )"
non associative with precedence 45
for @{ 'PRedSnStar $h $o $G $L1 $L2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break [ term 46 h , break term 46 o ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * [ break term 46 h , break term 46 o ] break term 46 T2 )"
non associative with precedence 45
for @{ 'PRedStar $h $o $G $L $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬈ break [ term 46 h ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬈ [ break term 46 h ] break term 46 T2 )"
non associative with precedence 45
for @{ 'PRedTy $h $G $L $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬈ break [ term 46 Rt , break term 46 c , break term 46 h ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬈ [ break term 46 Rt , break term 46 c , break term 46 h ] break term 46 T2 )"
non associative with precedence 45
for @{ 'PRedTy $Rt $c $h $G $L $T1 $T2 }.
--- /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 G, break term 46 L ⦄ ⊢ ⬈ [ break term 46 h , break term 46 o ] 𝐍 ⦃ break term 46 T ⦄ )"
+ non associative with precedence 45
+ for @{ 'PRedTyNormal $h $o $G $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ⬈ break [ term 46 h , break term 46 T ] break term 46 L2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ⬈ [ break term 46 h , break term 46 T ] break term 46 L2 )"
non associative with precedence 45
for @{ 'PRedTySn $h $T $G $L1 $L2 }.
--- /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 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬈ * [ break term 46 h ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PRedTyStar $h $G $L $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( L1 ⦻ * break [ term 46 R , break term 46 T ] break term 46 L2 )"
+notation "hvbox( L1 ⦻ * [ break term 46 R , break term 46 T ] break term 46 L2 )"
non associative with precedence 45
for @{ 'RelationStar $R $T $L1 $L2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( L1 ⦻ * break [ term 46 R1 , break term 46 R2 , break term 46 f ] break term 46 L2 )"
+notation "hvbox( L1 ⦻ * [ break term 46 R1 , break term 46 R2 , break term 46 f ] break term 46 L2 )"
non associative with precedence 45
for @{ 'RelationStar $R1 $R2 $f $L1 $L2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬊ * break [ term 46 h, break term 46 o ] break term 46 T )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬊ * [ break term 46 h, break term 46 o ] break term 46 T )"
non associative with precedence 45
for @{ 'SN $h $o $G $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( G ⊢ ⬊ * break [ term 46 h , break term 46 o , break term 46 T , break term 46 f ] break term 46 L )"
+notation "hvbox( G ⊢ ⬊ * [ break term 46 h , break term 46 o , break term 46 T , break term 46 f ] break term 46 L )"
non associative with precedence 45
for @{ 'SN $h $o $T $f $G $L }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬊ ⬊ * break [ term 46 h , break term 46 o ] break term 46 T )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬊ ⬊ * [ break term 46 h , break term 46 o ] break term 46 T )"
non associative with precedence 45
for @{ 'SNAlt $h $o $G $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( G ⊢ ⬊ ⬊ * break [ term 46 h , break term 46 o , break term 46 T , break term 46 f ] break term 46 L )"
+notation "hvbox( G ⊢ ⬊ ⬊ * [ break term 46 h , break term 46 o , break term 46 T , break term 46 f ] break term 46 L )"
non associative with precedence 45
for @{ 'SNAlt $h $o $T $f $G $L }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐ break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐ ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'SupTerm $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐⸮ break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐⸮ ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'SupTermOpt $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ + break ⦃ term 46 G2, term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ + ⦃ break term 46 G2, term 46 L2 , break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'SupTermPlus $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ * break ⦃ term 46 G2, term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ * ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'SupTermStar $G1 $L1 $T1 $G2 $L2 $T2 }.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/predstar_6.ma".
-include "basic_2/reduction/cnx.ma".
-include "basic_2/computation/cprs.ma".
+include "basic_2/notation/relations/predtystar_5.ma".
+include "basic_2/rt_transition/cpx.ma".
-(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
-definition cpxs: ∀h. sd h → relation4 genv lenv term term ≝
- λh,o,G. LTC … (cpx h o G).
+definition cpxs: sh → relation4 genv lenv term term ≝
+ λh,G. LTC … (cpx h G).
-interpretation "extended context-sensitive parallel computation (term)"
- 'PRedStar h o G L T1 T2 = (cpxs h o G L T1 T2).
+interpretation "uncounted context-sensitive parallel rt-computation (term)"
+ 'PRedTyStar h G L T1 T2 = (cpxs h G L T1 T2).
(* Basic eliminators ********************************************************)
-lemma cpxs_ind: ∀h,o,G,L,T1. ∀R:predicate term. R T1 →
- (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T → ⦃G, L⦄ ⊢ T ⬈[h, o] T2 → R T → R T2) →
- ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2 → R T2.
-#h #o #L #G #T1 #R #HT1 #IHT1 #T2 #HT12
+lemma cpxs_ind: ∀h,G,L,T1. ∀R:predicate term. R T1 →
+ (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T → ⦃G, L⦄ ⊢ T ⬈[h] T2 → R T → R T2) →
+ ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → R T2.
+#h #L #G #T1 #R #HT1 #IHT1 #T2 #HT12
@(TC_star_ind … HT1 IHT1 … HT12) //
qed-.
-lemma cpxs_ind_dx: ∀h,o,G,L,T2. ∀R:predicate term. R T2 →
- (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬈[h, o] T → ⦃G, L⦄ ⊢ T ⬈*[h, o] T2 → R T → R T1) →
- ∀T1. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2 → R T1.
-#h #o #G #L #T2 #R #HT2 #IHT2 #T1 #HT12
+lemma cpxs_ind_dx: ∀h,G,L,T2. ∀R:predicate term. R T2 →
+ (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬈[h] T → ⦃G, L⦄ ⊢ T ⬈*[h] T2 → R T → R T1) →
+ ∀T1. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → R T1.
+#h #G #L #T2 #R #HT2 #IHT2 #T1 #HT12
@(TC_star_ind_dx … HT2 IHT2 … HT12) //
qed-.
(* Basic properties *********************************************************)
-lemma cpxs_refl: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ T ⬈*[h, o] T.
+lemma cpxs_refl: ∀h,G,L,T. ⦃G, L⦄ ⊢ T ⬈*[h] T.
/2 width=1 by inj/ qed.
-lemma cpx_cpxs: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h, o] T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2.
+lemma cpx_cpxs: ∀h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h] T2.
/2 width=1 by inj/ qed.
-lemma cpxs_strap1: ∀h,o,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T →
- ∀T2. ⦃G, L⦄ ⊢ T ⬈[h, o] T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2.
-normalize /2 width=3 by step/ qed.
+lemma cpxs_strap1: ∀h,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬈*[h] T →
+ ∀T2. ⦃G, L⦄ ⊢ T ⬈[h] T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h] T2.
+normalize /2 width=3 by step/ qed-.
-lemma cpxs_strap2: ∀h,o,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬈[h, o] T →
- ∀T2. ⦃G, L⦄ ⊢ T ⬈*[h, o] T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2.
-normalize /2 width=3 by TC_strap/ qed.
+lemma cpxs_strap2: ∀h,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬈[h] T →
+ ∀T2. ⦃G, L⦄ ⊢ T ⬈*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h] T2.
+normalize /2 width=3 by TC_strap/ qed-.
-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, o] T2.
-#h #o #G #L #T1 #T2 #H @(cprs_ind … H) -T2 /3 width=3 by cpxs_strap1, cpr_cpx/
-qed.
-
-lemma cpxs_sort: ∀h,o,G,L,s,d1. deg h o s d1 →
- ∀d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ ⋆s ⬈*[h, o] ⋆((next h)^d2 s).
-#h #o #G #L #s #d1 #Hkd1 #d2 @(nat_ind_plus … d2) -d2 /2 width=1 by cpx_cpxs/
-#d2 #IHd2 #Hd21 >iter_SO
-@(cpxs_strap1 … (⋆(iter d2 ℕ (next h) s)))
-[ /3 width=3 by lt_to_le/
-| @(cpx_st … (d1-d2-1)) <plus_minus_k_k
- /2 width=1 by deg_iter, monotonic_le_minus_c/
-]
+(* Basic_2A1: was just: cpxs_sort *)
+lemma cpxs_sort: ∀h,G,L,s,n. ⦃G, L⦄ ⊢ ⋆s ⬈*[h] ⋆((next h)^n s).
+#h #G #L #s #n elim n -n /2 width=1 by cpx_cpxs/
+#n >iter_S /2 width=3 by cpxs_strap1/
qed.
-lemma cpxs_bind_dx: ∀h,o,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h, o] V2 →
- ∀I,T1,T2. ⦃G, L. ⓑ{I}V1⦄ ⊢ T1 ⬈*[h, o] T2 →
- ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ⬈*[h, o] ⓑ{a,I}V2.T2.
-#h #o #G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cpxs_ind_dx … HT12) -T1
+lemma cpxs_bind_dx: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 →
+ ∀I,T1,T2. ⦃G, L. ⓑ{I}V1⦄ ⊢ T1 ⬈*[h] T2 →
+ ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈*[h] ⓑ{p,I}V2.T2.
+#h #G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cpxs_ind_dx … HT12) -T1
/3 width=3 by cpxs_strap2, cpx_cpxs, cpx_pair_sn, cpx_bind/
qed.
-lemma cpxs_flat_dx: ∀h,o,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h, o] V2 →
- ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2 →
- ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬈*[h, o] ⓕ{I}V2.T2.
-#h #o #G #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cpxs_ind … HT12) -T2
+lemma cpxs_flat_dx: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 →
+ ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 →
+ ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬈*[h] ⓕ{I}V2.T2.
+#h #G #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cpxs_ind … HT12) -T2
/3 width=5 by cpxs_strap1, cpx_cpxs, cpx_pair_sn, cpx_flat/
qed.
-lemma cpxs_flat_sn: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h, o] T2 →
- ∀V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h, o] V2 →
- ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬈*[h, o] ⓕ{I}V2.T2.
-#h #o #G #L #T1 #T2 #HT12 #V1 #V2 #H @(cpxs_ind … H) -V2
+lemma cpxs_flat_sn: ∀h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 →
+ ∀V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 →
+ ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬈*[h] ⓕ{I}V2.T2.
+#h #G #L #T1 #T2 #HT12 #V1 #V2 #H @(cpxs_ind … H) -V2
/3 width=5 by cpxs_strap1, cpx_cpxs, cpx_pair_sn, cpx_flat/
qed.
-lemma cpxs_pair_sn: ∀h,o,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h, o] V2 →
- ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ⬈*[h, o] ②{I}V2.T.
-#h #o #I #G #L #V1 #V2 #H @(cpxs_ind … H) -V2
+lemma cpxs_pair_sn: ∀h,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 →
+ ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ⬈*[h] ②{I}V2.T.
+#h #I #G #L #V1 #V2 #H @(cpxs_ind … H) -V2
/3 width=3 by cpxs_strap1, cpx_pair_sn/
qed.
-lemma cpxs_zeta: ∀h,o,G,L,V,T1,T,T2. ⬆[0, 1] T2 ≡ T →
- ⦃G, L.ⓓV⦄ ⊢ T1 ⬈*[h, o] T → ⦃G, L⦄ ⊢ +ⓓV.T1 ⬈*[h, o] T2.
-#h #o #G #L #V #T1 #T #T2 #HT2 #H @(cpxs_ind_dx … H) -T1
+lemma cpxs_zeta: ∀h,G,L,V,T1,T,T2. ⬆*[1] T2 ≡ T →
+ ⦃G, L.ⓓV⦄ ⊢ T1 ⬈*[h] T → ⦃G, L⦄ ⊢ +ⓓV.T1 ⬈*[h] T2.
+#h #G #L #V #T1 #T #T2 #HT2 #H @(cpxs_ind_dx … H) -T1
/3 width=3 by cpxs_strap2, cpx_cpxs, cpx_bind, cpx_zeta/
qed.
-lemma cpxs_eps: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2 →
- ∀V. ⦃G, L⦄ ⊢ ⓝV.T1 ⬈*[h, o] T2.
-#h #o #G #L #T1 #T2 #H @(cpxs_ind … H) -T2
+lemma cpxs_eps: ∀h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 →
+ ∀V. ⦃G, L⦄ ⊢ ⓝV.T1 ⬈*[h] T2.
+#h #G #L #T1 #T2 #H @(cpxs_ind … H) -T2
/3 width=3 by cpxs_strap1, cpx_cpxs, cpx_eps/
qed.
-lemma cpxs_ct: ∀h,o,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h, o] V2 →
- ∀T. ⦃G, L⦄ ⊢ ⓝV1.T ⬈*[h, o] V2.
-#h #o #G #L #V1 #V2 #H @(cpxs_ind … H) -V2
-/3 width=3 by cpxs_strap1, cpx_cpxs, cpx_ct/
+(* Basic_2A1: was: cpxs_ct *)
+lemma cpxs_ee: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 →
+ ∀T. ⦃G, L⦄ ⊢ ⓝV1.T ⬈*[h] V2.
+#h #G #L #V1 #V2 #H @(cpxs_ind … H) -V2
+/3 width=3 by cpxs_strap1, cpx_cpxs, cpx_ee/
qed.
-lemma cpxs_beta_dx: ∀h,o,a,G,L,V1,V2,W1,W2,T1,T2.
- ⦃G, L⦄ ⊢ V1 ⬈[h, o] V2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈*[h, o] T2 → ⦃G, L⦄ ⊢ W1 ⬈[h, o] W2 →
- ⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ⬈*[h, o] ⓓ{a}ⓝW2.V2.T2.
-#h #o #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 * -T2
+lemma cpxs_beta_dx: ∀h,p,G,L,V1,V2,W1,W2,T1,T2.
+ ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈*[h] T2 → ⦃G, L⦄ ⊢ W1 ⬈[h] W2 →
+ ⦃G, L⦄ ⊢ ⓐV1.ⓛ{p}W1.T1 ⬈*[h] ⓓ{p}ⓝW2.V2.T2.
+#h #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 * -T2
/4 width=7 by cpx_cpxs, cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_beta/
qed.
-lemma cpxs_theta_dx: ∀h,o,a,G,L,V1,V,V2,W1,W2,T1,T2.
- ⦃G, L⦄ ⊢ V1 ⬈[h, o] V → ⬆[0, 1] V ≡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈*[h, o] T2 →
- ⦃G, L⦄ ⊢ W1 ⬈[h, o] W2 → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ⬈*[h, o] ⓓ{a}W2.ⓐV2.T2.
-#h #o #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2
+lemma cpxs_theta_dx: ∀h,p,G,L,V1,V,V2,W1,W2,T1,T2.
+ ⦃G, L⦄ ⊢ V1 ⬈[h] V → ⬆*[1] V ≡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈*[h] T2 →
+ ⦃G, L⦄ ⊢ W1 ⬈[h] W2 → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ⬈*[h] ⓓ{p}W2.ⓐV2.T2.
+#h #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2
/4 width=9 by cpx_cpxs, cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_theta/
qed.
(* Basic inversion lemmas ***************************************************)
-lemma cpxs_inv_sort1: ∀h,o,G,L,U2,s. ⦃G, L⦄ ⊢ ⋆s ⬈*[h, o] U2 →
- ∃∃n,d. deg h o s (n+d) & U2 = ⋆((next h)^n s).
-#h #o #G #L #U2 #s #H @(cpxs_ind … H) -U2
-[ elim (deg_total h o s) #d #Hkd
- @(ex2_2_intro … 0 … Hkd) -Hkd //
-| #U #U2 #_ #HU2 * #n #d #Hknd #H destruct
- elim (cpx_inv_sort1 … HU2) -HU2
- [ #H destruct /2 width=4 by ex2_2_intro/
- | * #d0 #Hkd0 #H destruct -d
- @(ex2_2_intro … (n+1) d0) /2 width=1 by deg_inv_prec/ >iter_SO //
- ]
-]
+(* Basic_2A1: wa just: cpxs_inv_sort1 *)
+lemma cpxs_inv_sort1: ∀h,G,L,X2,s. ⦃G, L⦄ ⊢ ⋆s ⬈*[h] X2 →
+ ∃n. X2 = ⋆((next h)^n s).
+#h #G #L #X2 #s #H @(cpxs_ind … H) -X2 /2 width=2 by ex_intro/
+#X #X2 #_ #HX2 * #n #H destruct
+elim (cpx_inv_sort1 … HX2) -HX2 #H destruct /2 width=2 by ex_intro/
+@(ex_intro … (⫯n)) >iter_S //
qed-.
-lemma cpxs_inv_cast1: ∀h,o,G,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓝW1.T1 ⬈*[h, o] U2 →
- ∨∨ ∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ⬈*[h, o] W2 & ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2 & U2 = ⓝW2.T2
- | ⦃G, L⦄ ⊢ T1 ⬈*[h, o] U2
- | ⦃G, L⦄ ⊢ W1 ⬈*[h, o] U2.
-#h #o #G #L #W1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by or3_intro0, ex3_2_intro/
+lemma cpxs_inv_cast1: ∀h,G,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓝW1.T1 ⬈*[h] U2 →
+ ∨∨ ∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ⬈*[h] W2 & ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 & U2 = ⓝW2.T2
+ | ⦃G, L⦄ ⊢ T1 ⬈*[h] U2
+ | ⦃G, L⦄ ⊢ W1 ⬈*[h] U2.
+#h #G #L #W1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by or3_intro0, ex3_2_intro/
#U2 #U #_ #HU2 * /3 width=3 by cpxs_strap1, or3_intro1, or3_intro2/ *
#W #T #HW1 #HT1 #H destruct
elim (cpx_inv_cast1 … HU2) -HU2 /3 width=3 by cpxs_strap1, or3_intro1, or3_intro2/ *
lapply (cpxs_strap1 … HW1 … HW2) -W
lapply (cpxs_strap1 … HT1 … HT2) -T /3 width=5 by or3_intro0, ex3_2_intro/
qed-.
-
-lemma cpxs_inv_cnx1: ∀h,o,G,L,T,U. ⦃G, L⦄ ⊢ T ⬈*[h, o] U → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃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, o] T2 → (T1 = T2 → ⊥) →
- ∃∃T. ⦃G, L⦄ ⊢ T1 ⬈[h, o] T & T1 = T → ⊥ & ⦃G, L⦄ ⊢ T ⬈*[h, o] T2.
-#h #o #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1
-[ #H elim H -H //
-| #T1 #T #H1 #H2 #IH2 #H12 elim (eq_term_dec T1 T) #H destruct
- [ -H1 -H2 /3 width=1 by/
- | -IH2 /3 width=4 by ex3_intro/ (**) (* auto fails without clear *)
- ]
-]
-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/syntax/tdeq_tdeq.ma".
+include "basic_2/rt_computation/cpxs.ma".
+include "basic_2/rt_transition/cpx_lfdeq.ma".
+include "basic_2/static/lfdeq_fqup.ma".
+include "basic_2/rt_transition/lfpx_fqup.ma".
+
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+
+axiom tdeq_dec: ∀h,o,T1,T2. Decidable (tdeq h o T1 T2).
+
+axiom tdeq_canc_sn: ∀h,o. left_cancellable … (tdeq h o).
+
+lemma tdeq_cpx_trans: ∀h,o,U1,T1. U1 ≡[h, o] T1 → ∀G,L,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 →
+ ∃∃U2. ⦃G, L⦄ ⊢ U1 ⬈[h] U2 & U2 ≡[h, o] T2.
+#h #o #U1 #T1 #HUT1 #G #L #T2 #HT12
+elim (cpx_tdeq_conf_lexs … o … HT12 … U1 … L … L) /3 width=3 by tdeq_sym, ex2_intro/
+qed-.
+
+lemma tdeq_cpxs_trans: ∀h,o,U1,T1. U1 ≡[h, o] T1 → ∀G,L,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 →
+ ∃∃U2. ⦃G, L⦄ ⊢ U1 ⬈*[h] U2 & U2 ≡[h, o] T2.
+#h #o #U1 #T1 #HUT1 #G #L #T2 #HT12 @(cpxs_ind … HT12) -T2 /2 width=3 by ex2_intro/
+#T #T2 #_ #HT2 * #U #HU1 #HUT elim (tdeq_cpx_trans … HUT … HT2) -T -T1
+/3 width=3 by ex2_intro, cpxs_strap1/
+qed-.
+
+(* Note: this requires tdeq to be symmetric *)
+lemma cpxs_tdneq_inv_step_sn: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) →
+ ∃∃T,T0. ⦃G, L⦄ ⊢ T1 ⬈[h] T & T1 ≡[h, o] T → ⊥ & ⦃G, L⦄ ⊢ T ⬈*[h] T0 & T0 ≡[h, o] T2.
+#h #o #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1
+[ #H elim H -H //
+| #T1 #T #H1 #H2 #IH #Hn12 elim (tdeq_dec h o T1 T) #H destruct
+ [ -H1 -H2 elim IH -IH /3 width=3 by tdeq_trans/ -Hn12
+ #X #X2 #HTX #HnTX #HX2 #HXT2 elim (tdeq_cpx_trans … H … HTX) -HTX
+ #X1 #HTX1 #HX1 elim (tdeq_cpxs_trans … HX1 … HX2) -HX2
+ /5 width=8 by tdeq_canc_sn, tdeq_trans, ex4_2_intro/ (* Note: 2 tdeq_trans *)
+ | -IH -Hn12 /3 width=6 by ex4_2_intro/
+ ]
+]
+qed-.
+
+(* Basic_2A1: removed theorems 1: cpxs_neq_inv_step_sn *)
--- /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/notation/relations/predtynormal_5.ma".
+include "basic_2/syntax/tdeq.ma".
+include "basic_2/rt_transition/cpx.ma".
+
+(* NORMAL TERMS FOR UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ******)
+
+definition cnx: ∀h. sd h → relation3 genv lenv term ≝
+ λh,o,G,L. NF … (cpx h G L) (tdeq h o …).
+
+interpretation
+ "normality for uncounted context-sensitive parallel rt-transition (term)"
+ 'PRedTyNormal h o G L T = (cnx h o G L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cnx_inv_sort: ∀h,o,G,L,s. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃⋆s⦄ → deg h o s 0.
+#h #o #G #L #s #H
+lapply (H (⋆(next h s)) ?) -H /2 width=2 by cpx_ess/ -G -L #H
+elim (tdeq_inv_sort1 … H) -H #s0 #d #H1 #H2 #H destruct
+lapply (deg_next … H1) #H0
+lapply (deg_mono … H0 … H2) -H0 -H2 #H
+<(pred_inv_refl … H) -H //
+qed-.
+
+lemma cnx_inv_abst: ∀h,o,p,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃ⓛ{p}V.T⦄ →
+ ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃V⦄ ∧ ⦃G, L.ⓛV⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄.
+#h #o #p #G #L #V1 #T1 #HVT1 @conj
+[ #V2 #HV2 lapply (HVT1 (ⓛ{p}V2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2
+| #T2 #HT2 lapply (HVT1 (ⓛ{p}V1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2
+]
+#H elim (tdeq_inv_pair … H) -H //
+qed-.
+
+(* Basic_2A1: was: cnx_inv_abbr *)
+lemma cnx_inv_abbr_neg: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃-ⓓV.T⦄ →
+ ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃V⦄ ∧ ⦃G, L.ⓓV⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄.
+#h #o #G #L #V1 #T1 #HVT1 @conj
+[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2
+| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2
+]
+#H elim (tdeq_inv_pair … H) -H //
+qed-.
+
+(* Basic_2A1: was: cnx_inv_eps *)
+lemma cnx_inv_cast: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃ⓝV.T⦄ → ⊥.
+#h #o #G #L #V #T #H lapply (H T ?) -H
+/2 width=6 by cpx_eps, tdeq_inv_pair_xy_y/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma cnx_sort: ∀h,o,G,L,s. deg h o s 0 → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃⋆s⦄.
+#h #o #G #L #s #Hs #X #H elim (cpx_inv_sort1 … H) -H
+/3 width=3 by tdeq_sort, deg_next/
+qed.
+
+lemma cnx_sort_iter: ∀h,o,G,L,s,d. deg h o s d → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃⋆((next h)^d s)⦄.
+#h #o #G #L #s #d #Hs lapply (deg_iter … d Hs) -Hs
+<minus_n_n /2 width=6 by cnx_sort/
+qed.
+
+lemma cnx_abst: ∀h,o,p,G,L,W,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ →
+ ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃ⓛ{p}W.T⦄.
+#h #o #p #G #L #W #T #HW #HT #X #H
+elim (cpx_inv_abst1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
+@tdeq_pair [ @HW | @HT ] // (**) (* auto fails because δ-expansion gets in the way *)
+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_drops.ma".
+include "basic_2/rt_transition/cnx.ma".
+
+(* NORMAL TERMS FOR UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ******)
+
+(* Properties with generic slicing ******************************************)
+
+lemma cnx_lref_atom: ∀h,o,G,L,i. ⬇*[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃#i⦄.
+#h #o #G #L #i #Hi #X #H elim (cpx_inv_lref1_drops … H) -H // *
+#I #K #V1 #V2 #HLK lapply (drops_mono … Hi … HLK) -L #H destruct
+qed.
+
+(* Inversion lemmas with generic slicing ************************************)
+
+(* Basic_2A1: was: cnx_inv_delta *)
+lemma cnx_inv_lref_pair: ∀h,o,I,G,L,K,V,i. ⬇*[i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃#i⦄ → ⊥.
+#h #o #I #G #L #K #V #i #HLK #H
+elim (lifts_total V (𝐔❴⫯i❵)) #W #HVW
+lapply (H W ?) -H /2 width=7 by cpx_delta_drops/ -HLK
+#H lapply (tdeq_inv_lref1 … H) -H #H destruct
+/2 width=5 by lifts_inv_lref2_uni_lt/
+qed-.
+
+(*
+(* Relocation properties ****************************************************)
+
+lemma cnx_lift: ∀h,o,G,L0,L,T,T0,c,l,k. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ → ⬇[c, l, k] L0 ≡ L →
+ ⬆[l, k] T ≡ T0 → ⦃G, L0⦄ ⊢ ➡[h, o] 𝐍⦃T0⦄.
+#h #o #G #L0 #L #T #T0 #c #l #k #HLT #HL0 #HT0 #X #H
+elim (cpx_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1
+<(HLT … HT1) in HT0; -L #HT0
+>(lift_mono … HT10 … HT0) -T1 -X //
+qed.
+
+lemma cnx_inv_lift: ∀h,o,G,L0,L,T,T0,c,l,k. ⦃G, L0⦄ ⊢ ➡[h, o] 𝐍⦃T0⦄ → ⬇[c, l, k] L0 ≡ L →
+ ⬆[l, k] T ≡ T0 → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄.
+#h #o #G #L0 #L #T #T0 #c #l #k #HLT0 #HL0 #HT0 #X #H
+elim (lift_total X l k) #X0 #HX0
+lapply (cpx_lift … H … HL0 … HT0 … HX0) -L #HTX0
+>(HLT0 … HTX0) in HX0; -L0 -X0 #H
+>(lift_inj … H … HT0) -T0 -X -l -k //
+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_simple.ma".
+include "basic_2/rt_transition/cnx.ma".
+
+(* NORMAL TERMS FOR UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ******)
+
+(* Inversion lemmas with simple terms ***************************************)
+
+lemma cnx_inv_appl: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃ⓐV.T⦄ →
+ ∧∧ ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃V⦄ & ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ & 𝐒⦃T⦄.
+#h #o #G #L #V1 #T1 #HVT1 @and3_intro
+[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1 by cpx_pair_sn/ -HV2
+ #H elim (tdeq_inv_pair … H) -H //
+| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1 by cpx_flat/ -HT2
+ #H elim (tdeq_inv_pair … H) -H //
+| generalize in match HVT1; -HVT1 elim T1 -T1 * //
+ #p * #W1 #U1 #_ #_ #H
+ [ elim (lifts_total V1 (𝐔❴1❵)) #V2 #HV12
+ lapply (H (ⓓ{p}W1.ⓐV2.U1) ?) -H /2 width=3 by cpx_theta/ -HV12
+ #H elim (tdeq_inv_pair … H) -H #H destruct
+ | lapply (H (ⓓ{p}ⓝW1.V1.U1) ?) -H /2 width=1 by cpx_beta/
+ #H elim (tdeq_inv_pair … H) -H #H destruct
+ ]
+]
+qed-.
+
+(* Properties with simple terms *********************************************)
+
+lemma cnx_appl_simple: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃V⦄ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → 𝐒⦃T⦄ →
+ ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃ⓐV.T⦄.
+#h #o #G #L #V #T #HV #HT #HS #X #H elim (cpx_inv_appl1_simple … H) -H //
+#V0 #T0 #HV0 #HT0 #H destruct
+@tdeq_pair [ @HV | @HT ] // (**) (* auto fails because δ-expansion gets in the way *)
+qed.
+++ /dev/null
-let cols =
- try int_of_string (Sys.getenv "COLUMNS")
- with Not_found -> failwith "environment variable COLUMNS not visible"
-
-let hl = ref []
-
-let normal = "\x1B[0m"
-
-let color = "\x1B[32m"
-
-let add s =
- if s = "" then false else
- begin hl := s :: !hl; true end
-
-let rec read ich =
- if Scanf.fscanf ich "%s " add then read ich
-
-let length l s = max l (String.length s)
-
-let split s =
-try
- let i = String.rindex s '.' in
- if i = 0 then s, "" else
- String.sub s 0 i, String.sub s i (String.length s - i)
-with Not_found -> s, ""
-
-let compare s1 s2 =
- let n1, e1 = split s1 in
- let n2, e2 = split s2 in
- let e = String.compare e1 e2 in
- if e = 0 then String.compare n1 n2 else e
-
-let write l c s =
- let pre, post = if List.mem s !hl then color, normal else "", "" in
- let spc = String.make (l - String.length s) ' ' in
- let bol, ret =
- if c = 0 || c = cols then "", l else
- if c + l < cols then " ", c + succ l else "\n", l
- in
- Printf.printf "%s%s%s%s%s" bol pre s post spc;
- ret
-
-let process fname =
- let ich = open_in fname in
- read ich; close_in ich
-
-let help = ""
-
-let main =
- Arg.parse [] process help;
- let files = Sys.readdir "." in
- let l = Array.fold_left length 0 files in
- if cols < l then failwith "window too small";
- Array.fast_sort compare files;
- let c = Array.fold_left (write l) 0 files in
- if 0 < c && c < cols then print_newline ();
-
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 cpx_lfdeq.ma
lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma lfpx_aaa.ma
+cnx.ma cnx_simple.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
#s2 #x #Hx <(deg_mono h o … Hx … Hs1) -s1 -d /2 width=3 by ex2_intro/
qed-.
-lemma tdeq_inv_pair: ∀h,o,I,V1,V2,T1,T2. ②{I}V1.T1 ≡[h, o] ②{I}V2.T2 →
- V1 ≡[h, o] V2 ∧ T1 ≡[h, o] T2.
-#h #o #I #V1 #V2 #T1 #T2 #H elim (tdeq_inv_pair1 … H) -H
-#V0 #T0 #HV #HT #H destruct /2 width=1 by conj/
-qed-.
+lemma tdeq_inv_pair: ∀h,o,I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ≡[h, o] ②{I2}V2.T2 →
+ ∧∧ I1 = I2 & V1 ≡[h, o] V2 & T1 ≡[h, o] T2.
+#h #o #I1 #I2 #V1 #V2 #T1 #T2 #H elim (tdeq_inv_pair1 … H) -H
+#V0 #T0 #HV #HT #H destruct /2 width=1 by and3_intro/
+qed-.
+
+lemma tdeq_inv_pair_xy_y: ∀h,o,I,T,V. ②{I}V.T ≡[h, o] T → ⊥.
+#h #o #I #T elim T -T
+[ #J #V #H elim (tdeq_inv_pair1 … H) -H #X #Y #_ #_ #H destruct
+| #J #X #Y #_ #IHY #V #H elim (tdeq_inv_pair … H) -H #H #_ #HY destruct /2 width=2 by/
+]
+qed-.
(* Basic forward lemmas *****************************************************)
]
}
]
+*)
class "cyan"
- [ { "computation" * } {
+ [ { "rt-computation" * } {
+(*
[ { "evaluation for context-sensitive rt-reduction" * } {
[ "cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )" * ]
}
[ "scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )" "scpds_lift" + "scpds_aaa" + "scpds_scpds" * ]
}
]
- [ { "context-sensitive rt-computation" * } {
- [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
- [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tsts" + "cpxs_tsts_vector" + "cpxs_lreq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ]
- }
- ]
[ { "context-sensitive computation" * } {
[ "lprs ( ⦃?,?⦄ ⊢ ➡* ? )" "lprs_drop" + "lprs_cprs" + "lprs_lprs" * ]
[ "cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)" "cprs_lift" + "cprs_cprs" * ]
}
]
+*)
+ [ { "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 ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" * ]
+ }
+ ]
+(*
[ { "local env. ref. for generic reducibility" * } {
[ "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drop" + "lsubc_drops" + "lsubc_lsuba" * ]
}
[ "gcp" "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ]
}
]
+*)
}
]
-*)
class "water"
[ { "rt-transition" * } {
[ { "parallel qrst-rtransition" * } {
}
]
[ { "uncounted context-sensitive rt-transition" * } {
+ [ "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" * ]
[ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_aaa" * ]
[ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" + "cpx_lfdeq" * ]
}
]
class "green"
[ { "static typing" * } {
- [ { "restricted ref. for atomic arity assignment" * } {
- [ "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ]
- }
- ]
[ { "atomic arity assignment" * } {
+ [ "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ]
[ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_aaa" * ]
}
]
- [ { "degree-based equivalence for closures on referred entries" * } {
+ [ { "degree-based equivalence on referred entries" * } {
[ "ffdeq ( ⦃?,?,?⦄ ≡[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ]
- }
- ]
- [ { "degree-based equivalence for local environments on referred entries" * } {
[ "lfdeq ( ? ≡[?,?,?] ? )" "lfdeq_length" + "lfdeq_fqup" + "lfdeq_lfdeq" * ]
}
]
[ "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_drops" + "lfxs_fqup" + "lfxs_lfxs" * ]
}
]
- [ { "restricted ref. for context-sensitive free variables" * } {
- [ "lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )" "lsubf_frees" * ]
- }
- ]
[ { "context-sensitive free variables" * } {
+ [ "lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )" "lsubf_frees" * ]
[ "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_weight" + "frees_drops" + "frees_fqup" + "frees_frees" * ]
}
]
class "italic" { 1 }
(*
[ { "normal forms for context-sensitive rt-reduction" * } {
- [ "cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )" "cnx_lift" + "cnx_crx" + "cnx_cix" * ]
+ [ "cnx_crx" + "cnx_cix" * ]
}
]
[ { "irreducible forms for context-sensitive rt-reduction" * } {
qed.
definition NF: ∀A. relation A → relation A → predicate A ≝
- λA,R,S,a1. ∀a2. R a1 a2 → S a2 a1.
+ λA,R,S,a1. ∀a2. R a1 a2 → S a1 a2.
definition NF_dec: ∀A. relation A → relation A → Prop ≝
λA,R,S. ∀a1. NF A R S a1 ∨
- ∃∃a2. R … a1 a2 & (S a2 a1 → ⊥).
+ ∃∃a2. R … a1 a2 & (S a1 a2 → ⊥).
inductive SN (A) (R,S:relation A): predicate A ≝
-| SN_intro: ∀a1. (∀a2. R a1 a2 → (S a2 a1 → ⊥) → SN A R S a2) → SN A R S a1
+| SN_intro: ∀a1. (∀a2. R a1 a2 → (S a1 a2 → ⊥) → SN A R S a2) → SN A R S a1
.
lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a.
qed-.
definition NF_sn: ∀A. relation A → relation A → predicate A ≝
- λA,R,S,a2. ∀a1. R a1 a2 → S a2 a1.
+ λA,R,S,a2. ∀a1. R a1 a2 → S a1 a2.
inductive SN_sn (A) (R,S:relation A): predicate A ≝
-| SN_sn_intro: ∀a2. (∀a1. R a1 a2 → (S a2 a1 → ⊥) → SN_sn A R S a1) → SN_sn A R S a2
+| SN_sn_intro: ∀a2. (∀a1. R a1 a2 → (S a1 a2 → ⊥) → SN_sn A R S a1) → SN_sn A R S a2
.
lemma NF_to_SN_sn: ∀A,R,S,a. NF_sn A R S a → SN_sn A R S a.
--- /dev/null
+let cols =
+ try int_of_string (Sys.getenv "COLUMNS")
+ with Not_found -> failwith "environment variable COLUMNS not visible"
+
+let hl = ref []
+
+let normal = "\x1B[0m"
+
+let color = "\x1B[32m"
+
+let add s =
+ if s = "" then false else
+ begin hl := s :: !hl; true end
+
+let rec read ich =
+ if Scanf.fscanf ich "%s " add then read ich
+
+let length l s = max l (String.length s)
+
+let split s =
+try
+ let i = String.rindex s '.' in
+ if i = 0 then s, "" else
+ String.sub s 0 i, String.sub s i (String.length s - i)
+with Not_found -> s, ""
+
+let compare s1 s2 =
+ let n1, e1 = split s1 in
+ let n2, e2 = split s2 in
+ let e = String.compare e1 e2 in
+ if e = 0 then String.compare n1 n2 else e
+
+let write l c s =
+ let pre, post = if List.mem s !hl then color, normal else "", "" in
+ let spc = String.make (l - String.length s) ' ' in
+ let bol, ret =
+ if c = 0 || c = cols then "", l else
+ if c + l < cols then " ", c + succ l else "\n", l
+ in
+ Printf.printf "%s%s%s%s%s" bol pre s post spc;
+ ret
+
+let process fname =
+ let ich = open_in fname in
+ read ich; close_in ich
+
+let help = ""
+
+let main =
+ Arg.parse [] process help;
+ let files = Sys.readdir "." in
+ let l = Array.fold_left length 0 files in
+ if cols < l then failwith "window too small";
+ Array.fast_sort compare files;
+ let c = Array.fold_left (write l) 0 files in
+ if 0 < c && c < cols then print_newline ();
+
projects / helm.git / commitdiff