(* Advanced properties ******************************************************)
-lemma tc_lfxs_refl: ∀R. (∀L. reflexive … (R L)) → ∀T. reflexive … (tc_lfxs R T).
+lemma tc_lfxs_refl: ∀R. c_reflexive … R →
+ ∀T. reflexive … (tc_lfxs R T).
/3 width=1 by lfxs_refl, inj/ qed.
(* Basic_2A1: uses: TC_lpx_sn_pair TC_lpx_sn_pair_refl *)
-lemma tc_lfxs_pair_refl: ∀R. (∀L. reflexive … (R L)) →
+lemma tc_lfxs_pair_refl: ∀R. c_reflexive … R →
∀L,V1,V2. LTC … R L V1 V2 → ∀I,T. L.ⓑ{I}V1 ⪤**[R, T] L.ⓑ{I}V2.
#R #HR #L #V1 #V2 #H elim H -V2
/3 width=3 by tc_lfxs_step_dx, lfxs_pair_refl, inj/
(* Advanced eliminators *****************************************************)
-lemma tc_lfxs_ind_sn: ∀R. (∀L. reflexive … (R L)) →
+lemma tc_lfxs_ind_sn: ∀R. c_reflexive … R →
∀L1,T. ∀R0:predicate …. R0 L1 →
(∀L,L2. L1 ⪤**[R, T] L → L ⪤*[R, T] L2 → R0 L → R0 L2) →
∀L2. L1 ⪤**[R, T] L2 → R0 L2.
@(TC_star_ind … HL1 IHL1 … HL12) /2 width=1 by lfxs_refl/
qed-.
-lemma tc_lfxs_ind_dx: ∀R. (∀L. reflexive … (R L)) →
+lemma tc_lfxs_ind_dx: ∀R. c_reflexive … R →
∀L2,T. ∀R0:predicate …. R0 L2 →
(∀L1,L. L1 ⪤*[R, T] L → L ⪤**[R, T] L2 → R0 L → R0 L1) →
∀L1. L1 ⪤**[R, T] L2 → R0 L1.
(* Advanced inversion lemmas ************************************************)
-lemma tc_lfxs_inv_bind_void: ∀R. (∀L. reflexive … (R L)) →
+lemma tc_lfxs_inv_bind_void: ∀R. c_reflexive … R →
∀p,I,L1,L2,V,T. L1 ⪤**[R, ⓑ{p,I}V.T] L2 →
L1 ⪤**[R, V] L2 ∧ L1.ⓧ ⪤**[R, T] L2.ⓧ.
#R #HR #p #I #L1 #L2 #V #T #H @(tc_lfxs_ind_sn … HR … H) -L2
(* Advanced forward lemmas **************************************************)
-lemma tc_lfxs_fwd_bind_dx_void: ∀R. (∀L. reflexive … (R L)) →
+lemma tc_lfxs_fwd_bind_dx_void: ∀R. c_reflexive … R →
∀p,I,L1,L2,V,T. L1 ⪤**[R, ⓑ{p,I}V.T] L2 →
L1.ⓧ ⪤**[R, T] L2.ⓧ.
#R #HR #p #I #L1 #L2 #V #T #H elim (tc_lfxs_inv_bind_void … H) -H //
(* *)
(**************************************************************************)
-include "basic_2/static/lfeq.ma".
+include "basic_2/syntax/ext2_tc.ma".
+include "basic_2/relocation/lexs_tc.ma".
+include "basic_2/relocation/lex.ma".
+include "basic_2/static/lfeq_fqup.ma".
include "basic_2/static/lfxs_lfxs.ma".
include "basic_2/i_static/tc_lfxs_fqup.ma".
-(*
-axiom cext2_inv_LTC: ∀R,L,I1,I2. cext2 (LTC … R) L I1 I2 → LTC … (cext2 R) L I1 I2.
-
-#R #L #I1 #I2 * -I1 -I2
-[ /2 width=1 by ext2_unit, inj/
-| #I #V1 #V2 #HV12
-*)
-
-
-(*
-lemma pippo: ∀RN,RP. (∀L. reflexive … (RP L)) →
- ∀f,L1,L2. L1 ⪤*[LTC … RN, RP, f] L2 →
- TC … (lexs RN RP f) L1 L2.
-#RN #RP #HRP #f #L1 #L2 #H elim H -f -L1 -L2
-[ /2 width=1 by lexs_atom, inj/ ]
-#f #I1 #I2 #L1 #L2 #HL12 #HI12 #IH
-[ @step [3:
-*)
-
-(*
-axiom lexs_frees_confluent_LTC_sn: ∀RN,RP. lexs_frees_confluent RN RP →
- lexs_frees_confluent (LTC … RN) RP.
-
-#RN #RP #HR #f1 #L1 #T #Hf1 #L2 #H
-*)
(* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***)
-lemma pippo: ∀R. (∀L. reflexive … (R L)) →
- (lexs_frees_confluent (cext2 R) cfull) →
- ∀L1,L2,T. L1 ⪤**[R, T] L2 →
- ∃∃L. L1 ⪤*[LTC … R, T] L & L ≡[T] L2.
-#R #H1R #H2R #L1 #L2 #T #H
+lemma tc_lfxs_inv_lex_lfeq: ∀R. c_reflexive … R →
+ (lexs_frees_confluent (cext2 R) cfull) →
+ (∀f. 𝐈⦃f⦄ → s_rs_transitive … (cext2 R) (λ_.lexs cfull (cext2 R) f)) →
+ ∀L1,L2,T. L1 ⪤**[R, T] L2 →
+ ∃∃L. L1 ⪤[LTC … R] L & L ≡[T] L2.
+#R #H1R #H2R #H3R #L1 #L2 #T #H
@(tc_lfxs_ind_sn … H1R … H) -H -L2
-[ /4 width=5 by lfxs_refl, inj, ex2_intro/
-| #L0 #L2 #_ #HL02 * #L * #f1 #Hf1 #HL1 #HL0
- lapply (lexs_co ??? cfull … (cext2_inv_LTC R) … HL1) -HL1 // #HL1
- lapply (lfeq_lfxs_trans … HL0 … HL02) -L0 #HL2
- elim (lexs_frees_confluent_LTC_sn … H2R … Hf1 … HL1) #f2 #Hf2 #Hf21
- lapply (lfxs_inv_frees … HL2 … Hf2) -HL2 #HL2
- elim (lexs_sle_split … ceq_ext … HL2 … Hf21) -HL2
- [ #L0 #HL0 #HL02
- |*: /2 width=1 by ext2_refl/
- ]
- lapply (sle_lexs_trans … HL0 … Hf21) -Hf21 // #H
- elim (H2R … Hf2 … H) -H #f0 #Hf0 #Hf02
- lapply (sle_lexs_trans … HL02 … Hf02) -f2 // #HL02
- @(ex2_intro … L0)
- [ @(ex2_intro … Hf1)
- | @(ex2_intro … HL02) //
+[ /4 width=3 by lfeq_refl, lex_refl, inj, ex2_intro/
+| #L0 #L2 #_ #HL02 * #L * #f0 #Hf0 #HL1 #HL0
+ lapply (lfeq_lfxs_trans … HL0 … HL02) -L0 * #f1 #Hf1 #HL2
+ elim (lexs_sdj_split … ceq_ext … HL2 f0 ?) -HL2
+ [ #L0 #HL0 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ]
+ lapply (lexs_sdj … HL0 f1 ?) /2 width=1 by sdj_isid_sn/ #H
+ elim (H2R … Hf1 … H) -H #f2 #Hf2 #Hf21
+ lapply (sle_lexs_trans … HL02 … Hf21) -f1 // #HL02
+ lapply (lexs_co ?? cfull (LTC … (cext2 R)) … HL1) -HL1 /2 width=1 by ext2_inv_tc/ #HL1
+ lapply (lexs_inv_tc_dx … HL1) -HL1 /2 width=1 by ext2_refl/ #HL1
+ lapply (step ????? HL1 … HL0) -L #HL10
+ lapply (lexs_tc_dx … H3R … HL10) -HL10 // #HL10
+ lapply (lexs_co … cfull (cext2 (LTC … R)) … HL10) -HL10 /2 width=1 by ext2_tc/ #HL10
+ /3 width=5 by ex2_intro/
+]
+qed-.
(* *)
(**************************************************************************)
+include "ground_2/relocation/rtmap_uni.ma".
include "basic_2/notation/relations/relation_3.ma".
+include "basic_2/syntax/cext2.ma".
include "basic_2/relocation/lexs.ma".
(* GENERIC EXTENSION OF A CONTEXT-SENSITIVE REALTION ON TERMS ***************)
(* Basic_2A1: includes: lpx_sn_atom lpx_sn_pair *)
-definition lex: (lenv → relation bind) → relation lenv ≝
- λR,L1,L2. ∃∃f. 𝐈⦃f⦄ & L1 ⪤*[cfull, R, f] L2.
+definition lex: (lenv → relation term) → relation lenv ≝
+ λR,L1,L2. ∃∃f. 𝐈⦃f⦄ & L1 ⪤*[cfull, cext2 R, f] L2.
interpretation "generic extension (local environment)"
'Relation R L1 L2 = (lex R L1 L2).
+
+(* Basic properties *********************************************************)
+
+(* Basic_2A1: was: lpx_sn_refl *)
+lemma lex_refl: ∀R. c_reflexive … R → reflexive … (lex R).
+/4 width=3 by lexs_refl, ext2_refl, ex2_intro/ qed.
(**************************************************************************)
include "ground_2/relocation/rtmap_sle.ma".
+include "ground_2/relocation/rtmap_sdj.ma".
include "basic_2/notation/relations/relationstar_5.ma".
include "basic_2/syntax/lenv.ma".
#RN #RP #L1 #L2 @eq_repl_sym /2 width=3 by lexs_eq_repl_back/ (**) (* full auto fails *)
qed-.
-(* Basic_2A1: uses: lpx_sn_refl *)
-lemma lexs_refl: ∀RN,RP.
- (∀L. reflexive … (RN L)) →
- (∀L. reflexive … (RP L)) →
+lemma lexs_refl: ∀RN,RP. c_reflexive … RN → c_reflexive … RP →
∀f.reflexive … (lexs 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) *
L1.ⓘ{J1} ⪤*[RN, RP, f] L2.ⓘ{J2}.
/3 width=3 by lexs_inv_tl, lexs_fwd_bind/ qed-.
-lemma lexs_co: ∀RN1,RP1,RN2,RP2.
- (∀L1,I1,I2. RN1 L1 I1 I2 → RN2 L1 I1 I2) →
- (∀L1,I1,I2. RP1 L1 I1 I2 → RP2 L1 I1 I2) →
+lemma lexs_co: ∀RN1,RP1,RN2,RP2. RN1 ⊆ RN2 → RP1 ⊆ RP2 →
∀f,L1,L2. L1 ⪤*[RN1, RP1, f] L2 → L1 ⪤*[RN2, RP2, f] L2.
#RN1 #RP1 #RN2 #RP2 #HRN #HRP #f #L1 #L2 #H elim H -f -L1 -L2
/3 width=1 by lexs_atom, lexs_next, lexs_push/
qed-.
-lemma lexs_co_isid: ∀RN1,RP1,RN2,RP2.
- (∀L1,I1,I2. RP1 L1 I1 I2 → RP2 L1 I1 I2) →
+lemma lexs_co_isid: ∀RN1,RP1,RN2,RP2. RP1 ⊆ RP2 →
∀f,L1,L2. L1 ⪤*[RN1, RP1, f] L2 → 𝐈⦃f⦄ →
L1 ⪤*[RN2, RP2, f] L2.
#RN1 #RP1 #RN2 #RP2 #HR #f #L1 #L2 #H elim H -f -L1 -L2 //
]
qed-.
-lemma sle_lexs_trans: ∀RN,RP. (∀L,I1,I2. RN L I1 I2 → RP L I1 I2) →
+lemma lexs_sdj: ∀RN,RP. RP ⊆ RN →
+ ∀f1,L1,L2. L1 ⪤*[RN, RP, f1] L2 →
+ ∀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: // ]
+ #g2 #H #H2 destruct /3 width=1 by lexs_push/
+| elim (sdj_inv_px … H12) -H12 [2,4: // ] *
+ #g2 #H #H2 destruct /3 width=1 by lexs_next, lexs_push/
+]
+qed-.
+
+lemma sle_lexs_trans: ∀RN,RP. RN ⊆ RP →
∀f2,L1,L2. L1 ⪤*[RN, RP, f2] L2 →
∀f1. f1 ⊆ f2 → L1 ⪤*[RN, RP, f1] L2.
#RN #RP #HR #f2 #L1 #L2 #H elim H -f2 -L1 -L2 //
]
qed-.
-lemma sle_lexs_conf: ∀RN,RP. (∀L,I1,I2. RP L I1 I2 → RN L I1 I2) →
+lemma sle_lexs_conf: ∀RN,RP. RP ⊆ RN →
∀f1,L1,L2. L1 ⪤*[RN, RP, f1] L2 →
∀f2. f1 ⊆ f2 → L1 ⪤*[RN, RP, f2] L2.
#RN #RP #HR #f1 #L1 #L2 #H elim H -f1 -L1 -L2 //
]
qed-.
-lemma lexs_sle_split: ∀R1,R2,RP. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
+lemma lexs_sle_split: ∀R1,R2,RP. c_reflexive … R1 → c_reflexive … R2 →
∀f,L1,L2. L1 ⪤*[R1, RP, f] L2 → ∀g. f ⊆ g →
∃∃L. L1 ⪤*[R1, RP, g] L & L ⪤*[R2, cfull, f] L2.
#R1 #R2 #RP #HR1 #HR2 #f #L1 #L2 #H elim H -f -L1 -L2
]
qed-.
+lemma lexs_sdj_split: ∀R1,R2,RP. c_reflexive … R1 → c_reflexive … R2 →
+ ∀f,L1,L2. L1 ⪤*[R1, RP, f] L2 → ∀g. f ∥ g →
+ ∃∃L. L1 ⪤*[RP, R1, g] L & L ⪤*[R2, cfull, f] L2.
+#R1 #R2 #RP #HR1 #HR2 #f #L1 #L2 #H elim H -f -L1 -L2
+[ /2 width=3 by lexs_atom, ex2_intro/ ]
+#f #I1 #I2 #L1 #L2 #_ #HI12 #IH #y #H
+[ elim (sdj_inv_nx … H ??) -H [ |*: // ] #g #Hfg #H destruct
+ elim (IH … Hfg) -IH -Hfg /3 width=5 by lexs_next, lexs_push, ex2_intro/
+| elim (sdj_inv_px … H ??) -H [1,3: * |*: // ] #g #Hfg #H destruct
+ elim (IH … Hfg) -IH -Hfg /3 width=5 by lexs_next, lexs_push, ex2_intro/
+]
+qed-.
+
lemma lexs_dec: ∀RN,RP.
(∀L,I1,I2. Decidable (RN L I1 I2)) →
(∀L,I1,I2. Decidable (RP L I1 I2)) →
(* Properties with transitive closure ***************************************)
-lemma lexs_tc_refl: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) →
+lemma lexs_tc_refl: ∀RN,RP. c_reflexive … RN → c_reflexive … RP →
∀f. reflexive … (TC … (lexs RN RP f)).
/3 width=1 by lexs_refl, TC_reflexive/ qed.
-lemma lexs_tc_next_sn: ∀RN,RP. (∀L. reflexive … (RN L)) →
+lemma lexs_tc_next_sn: ∀RN,RP. c_reflexive … RN →
∀f,I2,L1,L2. TC … (lexs RN RP f) L1 L2 → ∀I1. RN L1 I1 I2 →
TC … (lexs RN RP (⫯f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}).
#RN #RP #HRN #f #I2 #L1 #L2 #H @(TC_ind_dx ??????? H) -L1
/3 width=3 by lexs_next, TC_strap, inj/
qed.
-lemma lexs_tc_next_dx: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) →
+lemma lexs_tc_next_dx: ∀RN,RP. c_reflexive … RN → c_reflexive … RP →
∀f,I1,I2,L1. (LTC … RN) L1 I1 I2 → ∀L2. L1 ⪤*[RN, RP, f] L2 →
TC … (lexs RN RP (⫯f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}).
#RN #RP #HRN #HRP #f #I1 #I2 #L1 #H elim H -I2
/4 width=5 by lexs_refl, lexs_next, step, inj/
qed.
-lemma lexs_tc_push_sn: ∀RN,RP. (∀L. reflexive … (RP L)) →
+lemma lexs_tc_push_sn: ∀RN,RP. c_reflexive … RP →
∀f,I2,L1,L2. TC … (lexs RN RP f) L1 L2 → ∀I1. RP L1 I1 I2 →
TC … (lexs RN RP (↑f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}).
#RN #RP #HRP #f #I2 #L1 #L2 #H @(TC_ind_dx ??????? H) -L1
/3 width=3 by lexs_push, TC_strap, inj/
qed.
-lemma lexs_tc_push_dx: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) →
+lemma lexs_tc_push_dx: ∀RN,RP. c_reflexive … RN → c_reflexive … RP →
∀f,I1,I2,L1. (LTC … RP) L1 I1 I2 → ∀L2. L1 ⪤*[RN, RP, f] L2 →
TC … (lexs RN RP (↑f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}).
#RN #RP #HRN #HRP #f #I1 #I2 #L1 #H elim H -I2
(* Main properties with transitive closure **********************************)
-theorem lexs_tc_next: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) →
+theorem lexs_tc_next: ∀RN,RP. c_reflexive … RN → c_reflexive … RP →
∀f,I1,I2,L1. (LTC … RN) L1 I1 I2 → ∀L2. TC … (lexs RN RP f) L1 L2 →
TC … (lexs RN RP (⫯f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}).
#RN #RP #HRN #HRP #f #I1 #I2 #L1 #H elim H -I2
/4 width=5 by lexs_tc_next_sn, lexs_tc_refl, trans_TC/
qed.
-theorem lexs_tc_push: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) →
+theorem lexs_tc_push: ∀RN,RP. c_reflexive … RN → c_reflexive … RP →
∀f,I1,I2,L1. (LTC … RP) L1 I1 I2 → ∀L2. TC … (lexs RN RP f) L1 L2 →
TC … (lexs RN RP (↑f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}).
#RN #RP #HRN #HRP #f #I1 #I2 #L1 #H elim H -I2
(* Advanced inversion lemmas ************************************************)
-lemma lexs_inv_tc_sn: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) →
+lemma lexs_inv_tc_sn: ∀RN,RP. c_reflexive … RN → c_reflexive … RP →
∀f,L1,L2. L1 ⪤*[LTC … RN, RP, f] L2 → TC … (lexs RN RP f) L1 L2.
#RN #RP #HRN #HRP #f #L1 #L2 #H elim H -f -L1 -L2
/2 width=1 by lexs_tc_next, lexs_tc_push_sn, lexs_atom, inj/
qed-.
(* Basic_2A1: uses: lpx_sn_LTC_TC_lpx_sn *)
-lemma lexs_inv_tc_dx: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) →
+lemma lexs_inv_tc_dx: ∀RN,RP. c_reflexive … RN → c_reflexive … RP →
∀f,L1,L2. L1 ⪤*[RN, LTC … RP, f] L2 → TC … (lexs RN RP f) L1 L2.
#RN #RP #HRN #HRP #f #L1 #L2 #H elim H -f -L1 -L2
/2 width=1 by lexs_tc_push, lexs_tc_next_sn, lexs_atom, inj/
(* Advanced properties ******************************************************)
-(* Basic_2A1: uses: lleq_refl *)
lemma lfdeq_refl: ∀h,o,T. reflexive … (lfdeq h o T).
/2 width=1 by lfxs_refl/ 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/static/lfxs_fqup.ma".
+include "basic_2/static/lfeq.ma".
+
+(* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_2A1: was: lleq_refl *)
+lemma lfeq_refl: ∀T. reflexive … (lfeq T).
+/2 width=1 by lfxs_refl/ qed.
table {
class "gray"
[ { "component" * } {
- [ { "plane" * } {
- [ "files" * ]
+ [ { "section" * } {
+ [ [ "plane" ] "files" * ]
}
]
}
class "wine"
[ { "" * } {
[ { "" * } {
- [ "" * ]
+ [ [ "" ] "" * ]
}
]
}
(*
[ { "higher order dynamic typing" * } {
[ { "higher order native type assignment" * } {
- [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ]
+ [ [ "" ] "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ]
}
]
}
[ { "dynamic typing" * } {
(*
[ { "local env. ref. for native type assignment" * } {
- [ "lsubn ( ? ⊢ ? :⫃ ? )" "lsubn_drop" "lsubn_cpcs" "lsubn_nta" * ]
+ [ [ "" ] "lsubn ( ? ⊢ ? :⫃ ? )" "lsubn_drop" "lsubn_cpcs" "lsubn_nta" * ]
}
]
[ { "native type assignment" * } {
- [ "nta ( ⦃?,?⦄ ⊢ ? : ? )" "nta_alt ( ⦃?,?⦄ ⊢ ? :: ? )" "nta_lift" "nta_ltpss" "nta_thin" "nta_aaa" "nta_sta" "nta_ltpr" "nta_nta" * ]
+ [ [ "" ] "nta ( ⦃?,?⦄ ⊢ ? : ? )" "nta_alt ( ⦃?,?⦄ ⊢ ? :: ? )" "nta_lift" "nta_ltpss" "nta_thin" "nta_aaa" "nta_sta" "nta_ltpr" "nta_nta" * ]
}
]
*)
[ { "local env. ref. for stratified native validity" * } {
- [ "lsubsv ( ? ⊢ ? ⫃¡[?,?] ? )" "lsubsv_lsuba" + "lsubsv_lsubd" + "lsubsv_lstas" + "lsubsv_scpds" + "lsubsv_cpcs" + "lsubsv_snv" * ]
+ [ [ "" ] "lsubsv ( ? ⊢ ? ⫃¡[?,?] ? )" "lsubsv_lsuba" + "lsubsv_lsubd" + "lsubsv_lstas" + "lsubsv_scpds" + "lsubsv_cpcs" + "lsubsv_snv" * ]
}
]
[ { "stratified native validity" * } {
- [ "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ]
- [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_fsb" + "snv_scpes" + "snv_preserve" * ]
+ [ [ "" ] "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ]
+ [ [ "" ] "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_fsb" + "snv_scpes" + "snv_preserve" * ]
}
]
}
class "prune"
[ { "equivalence" * } {
[ { "decomposed rt-equivalence" * } {
- [ "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ]
+ [ [ "" ] "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ]
}
]
[ { "context-sensitive equivalence" * } {
- [ "cpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )" "cpcs_aaa" + "cpcs_cprs" + "cpcs_cpcs" * ]
+ [ [ "" ] "cpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )" "cpcs_aaa" + "cpcs_cprs" + "cpcs_cpcs" * ]
}
]
}
*)
class "blue"
[ { "rt-conversion" * } {
- [ { "context-sensitive r-conversion" * } {
- [ "cpc ( ⦃?,?⦄ ⊢ ? ⬌[?] ? )" "cpc_cpc" * ]
+ [ { "context-sensitive parallel r-conversion" * } {
+ [ [ "for terms" ] "cpc ( ⦃?,?⦄ ⊢ ? ⬌[?] ? )" "cpc_cpc" * ]
}
]
}
[ { "rt-computation" * } {
(*
[ { "evaluation for context-sensitive rt-reduction" * } {
- [ "cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )" * ]
+ [ [ "" ] "cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )" * ]
}
]
[ { "evaluation for context-sensitive reduction" * } {
- [ "cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )" "cpre_cpre" * ]
+ [ [ "" ] "cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )" "cpre_cpre" * ]
}
]
[ { "strongly normalizing qrst-computation" * } {
- [ "fsb ( ⦥[?,?] ⦃?,?,?⦄ )" "fsb_alt ( ⦥⦥[?,?] ⦃?,?,?⦄ )" "fsb_aaa" + "fsb_csx" * ]
+ [ [ "" ] "fsb ( ⦥[?,?] ⦃?,?,?⦄ )" "fsb_alt ( ⦥⦥[?,?] ⦃?,?,?⦄ )" "fsb_aaa" + "fsb_csx" * ]
}
]
[ { "strongly normalizing rt-computation" * } {
- [ "llsx_csx" * ]
- [ "csx_fpbs" * ]
+ [ [ "" ] "llsx_csx" * ]
+ [ [ "" ] "csx_fpbs" * ]
}
]
[ { "parallel qrst-computation" * } {
- [ "fpbg ( ⦃?,?,?⦄ >≛[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbs" + "fpbg_fpbg" * ]
- [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_aaa" + "fpbs_fpb" + "fpbs_fpbs" * ]
+ [ [ "" ] "fpbg ( ⦃?,?,?⦄ >≛[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbs" + "fpbg_fpbg" * ]
+ [ [ "" ] "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_aaa" + "fpbs_fpb" + "fpbs_fpbs" * ]
}
]
[ { "decomposed rt-computation" * } {
- [ "scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )" "scpds_lift" + "scpds_aaa" + "scpds_scpds" * ]
+ [ [ "" ] "scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )" "scpds_lift" + "scpds_aaa" + "scpds_scpds" * ]
}
]
[ { "context-sensitive computation" * } {
- [ "lprs ( ⦃?,?⦄ ⊢ ➡* ? )" "lprs_drop" + "lprs_cprs" + "lprs_lprs" * ]
- [ "cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)" "cprs_lift" + "cprs_cprs" * ]
+ [ [ "" ] "lprs ( ⦃?,?⦄ ⊢ ➡* ? )" "lprs_drop" + "lprs_cprs" + "lprs_lprs" * ]
+ [ [ "" ] "cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)" "cprs_lift" + "cprs_cprs" * ]
}
]
*)
- [ { "uncounted context-sensitive rt-computation" * } {
- [ "lsubsx ( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ]
- [ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ]
- [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
- [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ]
- [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ]
- [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_aaa" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
+ [ { "uncounted context-sensitive parallel rt-computation" * } {
+ [ [ "refinement for lenvs" ] "lsubsx ( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ]
+ [ [ "strongly normalizing on referred entries for lenvs" ] "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ]
+ [ [ "strongly normalizing for term vectors" ] "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
+ [ [ "strongly normalizing for terms" ] "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ]
+ [ [ "on referred entries for lenvs" ] "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ]
+ [ [ "for terms" ] "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_aaa" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
}
]
}
]
class "cyan"
[ { "rt-transition" * } {
- [ { "uncounted rst-transition" * } {
- [ "fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" * ]
- [ "fpb ( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ]
+ [ { "uncounted parallel rst-transition" * } {
+ [ [ "for closures" ] "fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" * ]
+ [ [ "proper for closures" ] "fpb ( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ]
}
]
- [ { "t-bound context-sensitive rt-transition" * } {
- [ "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fquq" + "lfpr_fqup" + "lfpr_frees" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ]
- [ "cpr_ext ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" * ]
- [ "cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" * ]
- [ "cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_lfxs" + "cpm_cpx" * ]
+ [ { "context-sensitive parallel r-transition" * } {
+ [ [ "for lenvs on referred entries" ] "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fquq" + "lfpr_fqup" + "lfpr_frees" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ]
+ [ [ "for binders" ] "cpr_ext ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" * ]
+ [ [ "for terms" ] "cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" * ]
}
]
- [ { "uncounted context-sensitive rt-transition" * } {
- [ "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ]
- [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_cpx" + "lfpx_lfpx" * ]
- [ "cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ]
- [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" * ]
+ [ { "t-bound context-sensitive parallel rt-transition" * } {
+ [ [ "for terms" ] "cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_lfxs" + "cpm_cpx" * ]
}
]
- [ { "counted context-sensitive rt-transition" * } {
- [ "cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )" "cpg_simple" + "cpg_drops" + "cpg_lsubr" * ]
+ [ { "uncounted context-sensitive parallel rt-transition" * } {
+ [ [ "normal form for terms" ] "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ]
+ [ [ "for lenvs on referred entries" ] "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_cpx" + "lfpx_lfpx" * ]
+ [ [ "for binders" ] "cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ]
+ [ [ "for terms" ] "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" * ]
+ }
+ ]
+ [ { "counted context-sensitive parallel rt-transition" * } {
+ [ [ "for terms" ] "cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )" "cpg_simple" + "cpg_drops" + "cpg_lsubr" * ]
}
]
}
class "water"
[ { "iterated static typing" * } {
[ { "iterated extension on referred entries" * } {
- [ "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_drops" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ]
+ [ [ "" ] "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_drops" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ]
}
]
}
class "green"
[ { "static typing" * } {
[ { "generic reducibility" * } {
- [ "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ]
- [ "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ]
- [ "gcp" *]
+ [ [ "" ] "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ]
+ [ [ "" ] "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ]
+ [ [ "" ] "gcp" *]
}
]
[ { "atomic arity assignment" * } {
- [ "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ]
- [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_aaa" * ]
+ [ [ "" ] "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ]
+ [ [ "" ] "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_aaa" * ]
}
]
[ { "degree-based equivalence on referred entries" * } {
- [ "ffdeq ( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ]
- [ "lfdeq ( ? ≛[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ]
+ [ [ "" ] "ffdeq ( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ]
+ [ [ "" ] "lfdeq ( ? ≛[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ]
}
]
[ { "syntactic equivalence on referred entries" * } {
- [ "lfeq ( ? ≡[?] ? )" * ]
+ [ [ "" ] "lfeq ( ? ≡[?] ? )" "lfeq_fqup" * ]
}
+ ]
[ { "generic extension on referred entries" * } {
- [ "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_drops" + "lfxs_fqup" + "lfxs_lfxs" * ]
+ [ [ "" ] "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_drops" + "lfxs_fqup" + "lfxs_lfxs" * ]
}
]
[ { "context-sensitive free variables" * } {
- [ "lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )" "lsubf_lsubr" + "lsubf_frees" + "lsubf_lsubf" * ]
- [ "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_drops" + "frees_fqup" + "frees_frees" * ]
+ [ [ "" ] "lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )" "lsubf_lsubr" + "lsubf_frees" + "lsubf_lsubf" * ]
+ [ [ "" ] "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_drops" + "frees_fqup" + "frees_frees" * ]
}
]
[ { "restricted ref. for local env." * } {
- [ "lsubr ( ? ⫃ ? )" "lsubr_length" + "lsubr_drops" + "lsubr_lsubr" * ]
+ [ [ "" ] "lsubr ( ? ⫃ ? )" "lsubr_length" + "lsubr_drops" + "lsubr_lsubr" * ]
}
]
}
class "grass"
[ { "s-computation" * } {
[ { "iterated structural successor for closures" * } {
- [ "fqus ( ⦃?,?,?⦄ ⊐*[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )" "fqus_weight" + "fqus_drops" + "fqus_fqup" + "fqus_fqus" * ]
- [ "fqup ( ⦃?,?,?⦄ ⊐+[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )" "fqup_weight" + "fqup_drops" + "fqup_fqup" * ]
+ [ [ "" ] "fqus ( ⦃?,?,?⦄ ⊐*[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )" "fqus_weight" + "fqus_drops" + "fqus_fqup" + "fqus_fqus" * ]
+ [ [ "" ] "fqup ( ⦃?,?,?⦄ ⊐+[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )" "fqup_weight" + "fqup_drops" + "fqup_fqup" * ]
}
]
}
class "yellow"
[ { "s-transition" * } {
[ { "structural successor for closures" * } {
- [ "fquq ( ⦃?,?,?⦄ ⊐⸮[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )" "fquq_length" + "fquq_weight" * ]
- [ "fqu ( ⦃?,?,?⦄ ⊐[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )" "fqu_length" + "fqu_weight" * ]
+ [ [ "" ] "fquq ( ⦃?,?,?⦄ ⊐⸮[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )" "fquq_length" + "fquq_weight" * ]
+ [ [ "" ] "fqu ( ⦃?,?,?⦄ ⊐[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )" "fqu_length" + "fqu_weight" * ]
}
]
}
class "orange"
[ { "relocation" * } {
[ { "generic slicing for local environments" * } {
- [ "drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" * ]
- [ "drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" * ]
+ [ [ "" ] "drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" * ]
+ [ [ "" ] "drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" * ]
}
]
[ { "generic relocation" * } {
- [ "lifts_bind ( ⬆*[?] ? ≡ ? )" "lifts_weight_bind" + "lifts_lifts_bind" * ]
- [ "lifts_vector ( ⬆*[?] ? ≡ ? )" "lifts_lifts_vector" * ]
- [ "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_lifts" * ]
+ [ [ "" ] "lifts_bind ( ⬆*[?] ? ≡ ? )" "lifts_weight_bind" + "lifts_lifts_bind" * ]
+ [ [ "" ] "lifts_vector ( ⬆*[?] ? ≡ ? )" "lifts_lifts_vector" * ]
+ [ [ "" ] "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_lifts" * ]
}
]
[ { "ranged equivalence for local environments" * } {
- [ "lreq ( ? ≡[?] ? )" "lreq_length" + "lreq_lreq" * ]
+ [ [ "" ] "lreq ( ? ≡[?] ? )" "lreq_length" + "lreq_lreq" * ]
}
]
[ { "generic entrywise extension" * } {
- [ "lex ( ? ⦻[?] ? )" * ]
- [ "lexs ( ? ⦻*[?,?,?] ? )" "lexs_tc" + "lexs_length" + "lexs_lexs" * ]
+ [ [ "" ] "lex ( ? ⦻[?] ? )" * ]
+ [ [ "" ] "lexs ( ? ⦻*[?,?,?] ? )" "lexs_tc" + "lexs_length" + "lexs_lexs" * ]
}
]
}
class "red"
[ { "syntax" * } {
[ { "append for local environments" * } {
- [ "append ( ? @@ ? )" "append_length" * ]
+ [ [ "" ] "append ( ? @@ ? )" "append_length" * ]
}
]
[ { "head equivalence for terms" * } {
- [ "theq ( ? ⩳[?,?] ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ]
+ [ [ "" ] "theq ( ? ⩳[?,?] ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ]
}
]
[ { "degree-based equivalence" * } {
- [ "tdeq_ext ( ? ≛[?,?] ? ) ( ? ⊢ ? ≛[?,?] ? )" * ]
- [ "tdeq ( ? ≛[?,?] ? )" "tdeq_tdeq" * ]
+ [ [ "" ] "tdeq_ext ( ? ≛[?,?] ? ) ( ? ⊢ ? ≛[?,?] ? )" * ]
+ [ [ "" ] "tdeq ( ? ≛[?,?] ? )" "tdeq_tdeq" * ]
}
]
[ { "closures" * } {
- [ "cl_weight ( ♯{?,?,?} )" * ]
- [ "cl_restricted_weight ( ♯{?,?} )" * ]
+ [ [ "" ] "cl_weight ( ♯{?,?,?} )" * ]
+ [ [ "" ] "cl_restricted_weight ( ♯{?,?} )" * ]
}
]
[ { "global environments" * } {
- [ "genv" * ]
+ [ [ "" ] "genv" * ]
}
]
[ { "local environments" * } {
- [ "ceq_ext" "ceq_ext_ceq_ext" * ]
- [ "cext2" * ]
- [ "lenv_length ( |?| )" * ]
- [ "lenv_weight ( ♯{?} )" * ]
- [ "lenv" * ]
+ [ [ "" ] "ceq_ext" "ceq_ext_ceq_ext" * ]
+ [ [ "" ] "cext2" * ]
+ [ [ "" ] "lenv_length ( |?| )" * ]
+ [ [ "" ] "lenv_weight ( ♯{?} )" * ]
+ [ [ "" ] "lenv" * ]
}
]
[ { "binders for local environments" * } {
- [ "ext2" "ext2_tc" + "ext2_ext2" * ]
- [ "bind" "bind_weight" * ]
+ [ [ "" ] "ext2" "ext2_tc" + "ext2_ext2" * ]
+ [ [ "" ] "bind" "bind_weight" * ]
}
]
[ { "terms" * } {
- [ "term_vector ( Ⓐ?.? )" * ]
- [ "term_simple ( 𝐒⦃?⦄ )" * ]
- [ "term_weight ( ♯{?} )" * ]
- [ "term" * ]
+ [ [ "" ] "term_vector ( Ⓐ?.? )" * ]
+ [ [ "" ] "term_simple ( 𝐒⦃?⦄ )" * ]
+ [ [ "" ] "term_weight ( ♯{?} )" * ]
+ [ [ "" ] "term" * ]
}
]
[ { "items" * } {
- [ "item_sd" * ]
- [ "item_sh" * ]
- [ "item" * ]
+ [ [ "" ] "item_sd" * ]
+ [ [ "" ] "item_sh" * ]
+ [ [ "" ] "item" * ]
}
]
[ { "atomic arities" * } {
- [ "aarity" * ]
+ [ [ "" ] "aarity" * ]
}
]
}
class "top" { * }
-class "capitalize italic" { 0 }
+class "capitalize italic" { 0 1 }
-class "italic" { 1 }
+class "italic" { 2 }
(*
[ { "normal forms for context-sensitive rt-reduction" * } {
- [ "cnx_crx" + "cnx_cix" * ]
+ [ [ "" ] "cnx_crx" + "cnx_cix" * ]
}
]
[ { "irreducible forms for context-sensitive rt-reduction" * } {
- [ "cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )" "cix_lift" * ]
+ [ [ "" ] "cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )" "cix_lift" * ]
}
]
[ { "reducible forms for context-sensitive rt-reduction" * } {
- [ "crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )" "crx_lift" * ]
+ [ [ "" ] "crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )" "crx_lift" * ]
}
]
[ { "normal forms for context-sensitive reduction" * } {
- [ "cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ]
+ [ [ "" ] "cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ]
}
]
[ { "irreducible forms for context-sensitive reduction" * } {
- [ "cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )" "cir_lift" * ]
+ [ [ "" ] "cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )" "cir_lift" * ]
}
]
[ { "reducible forms for context-sensitive reduction" * } {
- [ "crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )" "crr_lift" * ]
+ [ [ "" ] "crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )" "crr_lift" * ]
}
]
[ { "unfold" * } {
- [ "unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )" * ]
+ [ [ "" ] "unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )" * ]
}
]
[ { "iterated static type assignment" * } {
- [ "lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )" "lstas_lift" + "lstas_llpx_sn.ma" + "lstas_aaa" + "lstas_da" + "lstas_lstas" * ]
+ [ [ "" ] "lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )" "lstas_lift" + "lstas_llpx_sn.ma" + "lstas_aaa" + "lstas_da" + "lstas_lstas" * ]
}
]
[ { "local env. ref. for degree assignment" * } {
- [ "lsubd ( ? ⊢ ? ⫃▪[?,?] ? )" "lsubd_da" + "lsubd_lsubd" * ]
+ [ [ "" ] "lsubd ( ? ⊢ ? ⫃▪[?,?] ? )" "lsubd_da" + "lsubd_lsubd" * ]
}
]
[ { "degree assignment" * } {
- [ "da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )" "da_lift" + "da_aaa" + "da_da" * ]
+ [ [ "" ] "da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )" "da_lift" + "da_aaa" + "da_da" * ]
}
]
[ { "context-sensitive multiple rt-substitution" * } {
- [ "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ]
+ [ [ "" ] "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ]
}
]
[ { "pointwise union for local environments" * } {
- [ "llor ( ? ⋓[?,?] ? ≡ ? )" "llor_alt" + "llor_drop" * ]
+ [ [ "" ] "llor ( ? ⋓[?,?] ? ≡ ? )" "llor_alt" + "llor_drop" * ]
}
]
[ { "lazy pointwise extension of a relation" * } {
- [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_lreq" + "llpx_sn_drop" + "llpx_sn_lpx_sn" + "llpx_sn_frees" + "llpx_sn_llor" * ]
+ [ [ "" ] "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_lreq" + "llpx_sn_drop" + "llpx_sn_lpx_sn" + "llpx_sn_frees" + "llpx_sn_llor" * ]
}
]
[ { "global env. slicing" * } {
- [ "gget ( ⬇[?] ? ≡ ? )" "gget_gget" * ]
+ [ [ "" ] "gget ( ⬇[?] ? ≡ ? )" "gget_gget" * ]
}
]
[ { "context-sensitive ordinary rt-substitution" * } {
- [ "cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )" "cpy_lift" + "cpy_nlift" + "cpy_cpy" * ]
+ [ [ "" ] "cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )" "cpy_lift" + "cpy_nlift" + "cpy_cpy" * ]
}
]
[ { "local env. ref. for rt-substitution" * } {
- [ "lsuby ( ? ⊆[?,?] ? )" "lsuby_lsuby" * ]
+ [ [ "" ] "lsuby ( ? ⊆[?,?] ? )" "lsuby_lsuby" * ]
}
]
[ { "pointwise extension of a relation" * } {
- [ "lpx_sn" "lpx_sn_alt" + "lpx_sn_drop" + "lpx_sn_lpx_sn" * ]
+ [ [ "" ] "lpx_sn" "lpx_sn_alt" + "lpx_sn_drop" + "lpx_sn_lpx_sn" * ]
}
]
- [ "cpx_lreq" + "cpr_cir" + "fpb_lift" + "fpbq_lift" ]
- [ "lleq ( ? ≡[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_lreq" + "lleq_drop" + "lleq_fqus" + "lleq_llor" + "lleq_lleq" * ]
+ [ [ "" ] "cpx_lreq" + "cpr_cir" + "fpb_lift" + "fpbq_lift" ]
+ [ [ "" ] "lleq ( ? ≡[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_lreq" + "lleq_drop" + "lleq_fqus" + "lleq_llor" + "lleq_lleq" * ]
*)
--- /dev/null
+../../matitac.opt `cat partial.txt`
+cd basic_2/rt_computation/
+../../../../matitac.opt `cat partial.txt`
+cd ../../
--- /dev/null
+../../matitac.opt `cat static.txt`
(* GENERIC RELATIONS ********************************************************)
-(* PROPERTIES OF RELATIONS **************************************************)
+(* Inclusion ****************************************************************)
-definition relation5 : Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0]
+definition subR2 (S1) (S2): relation (relation2 S1 S2) ≝
+ λR1,R2. (∀a1,a2. R1 a1 a2 → R2 a1 a2).
+
+interpretation "2-relation inclusion"
+ 'subseteq R1 R2 = (subR2 ?? R1 R2).
+
+definition subR3 (S1) (S2) (S3): relation (relation3 S1 S2 S3) ≝
+ λR1,R2. (∀a1,a2,a3. R1 a1 a2 a3 → R2 a1 a2 a3).
+
+interpretation "3-relation inclusion"
+ 'subseteq R1 R2 = (subR3 ??? R1 R2).
+
+(* Properties of relations **************************************************)
+
+definition relation5: Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0]
≝ λA,B,C,D,E.A→B→C→D→E→Prop.
-definition relation6 : Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0]
+definition relation6: Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0]
≝ λA,B,C,D,E,F.A→B→C→D→E→F→Prop.
+(**) (* we dont use "∀a. reflexive … (R a)" since auto seems to dislike repeatd δ-expansion *)
+definition c_reflexive (A) (B): predicate (relation3 A B B) ≝
+ λR. ∀a,b. R a b b.
+
definition Decidable: Prop → Prop ≝ λR. R ∨ (R → ⊥).
definition Transitive: ∀A. ∀R: relation A. Prop ≝ λA,R.
∀a1,a0. R1 a1 a0 → ∀a2. R2 a0 a2 →
∃∃a. R2 a1 a & R1 a a2.
-definition bi_confluent: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R.
- ∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. R a0 b0 a2 b2 →
- ∃∃a,b. R a1 b1 a b & R a2 b2 a b.
+definition bi_confluent: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R.
+ ∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. R a0 b0 a2 b2 →
+ ∃∃a,b. R a1 b1 a b & R a2 b2 a b.
definition lsub_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2.
∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 L1 L2 → R1 L1 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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( f1 ∥ break term 46 f2 )"
+ non associative with precedence 45
+ for @{ 'Parallel $f1 $f2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.tcs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/relations/parallel_2.ma".
+include "ground_2/relocation/rtmap_isid.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+coinductive sdj: relation rtmap ≝
+| sdj_pp: ∀f1,f2,g1,g2. sdj f1 f2 → ↑f1 = g1 → ↑f2 = g2 → sdj g1 g2
+| sdj_np: ∀f1,f2,g1,g2. sdj f1 f2 → ⫯f1 = g1 → ↑f2 = g2 → sdj g1 g2
+| sdj_pn: ∀f1,f2,g1,g2. sdj f1 f2 → ↑f1 = g1 → ⫯f2 = g2 → sdj g1 g2
+.
+
+interpretation "disjointness (rtmap)"
+ 'Parallel f1 f2 = (sdj f1 f2).
+
+(* Basic properties *********************************************************)
+
+axiom sdj_eq_repl_back1: ∀f2. eq_repl_back … (λf1. f1 ∥ f2).
+
+lemma sdj_eq_repl_fwd1: ∀f2. eq_repl_fwd … (λf1. f1 ∥ f2).
+#f2 @eq_repl_sym /2 width=3 by sdj_eq_repl_back1/
+qed-.
+
+axiom sdj_eq_repl_back2: ∀f1. eq_repl_back … (λf2. f1 ∥ f2).
+
+lemma sdj_eq_repl_fwd2: ∀f1. eq_repl_fwd … (λf2. f1 ∥ f2).
+#f1 @eq_repl_sym /2 width=3 by sdj_eq_repl_back2/
+qed-.
+
+corec lemma sdj_sym: symmetric … sdj.
+#f1 #f2 * -f1 -f2
+#f1 #f2 #g1 #g2 #Hf #H1 #H2
+[ @(sdj_pp … H2 H1) | @(sdj_pn … H2 H1) | @(sdj_np … H2 H1) ] -g2 -g1
+/2 width=1 by/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma sdj_inv_pp: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 → f1 ∥ f2.
+#g1 #g2 * -g1 -g2
+#f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
+[ lapply (injective_push … Hx1) -Hx1
+ lapply (injective_push … Hx2) -Hx2 //
+| elim (discr_push_next … Hx1)
+| elim (discr_push_next … Hx2)
+]
+qed-.
+
+lemma sdj_inv_np: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 → f1 ∥ f2.
+#g1 #g2 * -g1 -g2
+#f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
+[ elim (discr_next_push … Hx1)
+| lapply (injective_next … Hx1) -Hx1
+ lapply (injective_push … Hx2) -Hx2 //
+| elim (discr_push_next … Hx2)
+]
+qed-.
+
+lemma sdj_inv_pn: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 → f1 ∥ f2.
+#g1 #g2 * -g1 -g2
+#f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
+[ elim (discr_next_push … Hx2)
+| elim (discr_push_next … Hx1)
+| lapply (injective_push … Hx1) -Hx1
+ lapply (injective_next … Hx2) -Hx2 //
+]
+qed-.
+
+lemma sdj_inv_nn: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → ⊥.
+#g1 #g2 * -g1 -g2
+#f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct
+[ elim (discr_next_push … Hx1)
+| elim (discr_next_push … Hx2)
+| elim (discr_next_push … Hx1)
+]
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma sdj_inv_nx: ∀g1,g2. g1 ∥ g2 → ∀f1. ⫯f1 = g1 →
+ ∃∃f2. f1 ∥ f2 & ↑f2 = g2.
+#g1 #g2 elim (pn_split g2) * #f2 #H2 #H #f1 #H1
+[ lapply (sdj_inv_np … H … H1 H2) -H /2 width=3 by ex2_intro/
+| elim (sdj_inv_nn … H … H1 H2)
+]
+qed-.
+
+lemma sdj_inv_xn: ∀g1,g2. g1 ∥ g2 → ∀f2. ⫯f2 = g2 →
+ ∃∃f1. f1 ∥ f2 & ↑f1 = g1.
+#g1 #g2 elim (pn_split g1) * #f1 #H1 #H #f2 #H2
+[ lapply (sdj_inv_pn … H … H1 H2) -H /2 width=3 by ex2_intro/
+| elim (sdj_inv_nn … H … H1 H2)
+]
+qed-.
+
+lemma sdj_inv_xp: ∀g1,g2. g1 ∥ g2 → ∀f2. ↑f2 = g2 →
+ ∨∨ ∃∃f1. f1 ∥ f2 & ↑f1 = g1
+ | ∃∃f1. f1 ∥ f2 & ⫯f1 = g1.
+#g1 #g2 elim (pn_split g1) * #f1 #H1 #H #f2 #H2
+[ lapply (sdj_inv_pp … H … H1 H2) | lapply (sdj_inv_np … H … H1 H2) ] -H -H2
+/3 width=3 by ex2_intro, or_introl, or_intror/
+qed-.
+
+lemma sdj_inv_px: ∀g1,g2. g1 ∥ g2 → ∀f1. ↑f1 = g1 →
+ ∨∨ ∃∃f2. f1 ∥ f2 & ↑f2 = g2
+ | ∃∃f2. f1 ∥ f2 & ⫯f2 = g2.
+#g1 #g2 elim (pn_split g2) * #f2 #H2 #H #f1 #H1
+[ lapply (sdj_inv_pp … H … H1 H2) | lapply (sdj_inv_pn … H … H1 H2) ] -H -H1
+/3 width=3 by ex2_intro, or_introl, or_intror/
+qed-.
+
+(* Properties with isid *****************************************************)
+
+corec lemma sdj_isid_dx: ∀f2. 𝐈⦃f2⦄ → ∀f1. f1 ∥ f2.
+#f2 * -f2
+#f2 #g2 #Hf2 #H2 #f1 cases (pn_split f1) *
+/3 width=5 by sdj_np, sdj_pp/
+qed.
+
+corec lemma sdj_isid_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ∥ f2.
+#f1 * -f1
+#f1 #g1 #Hf1 #H1 #f2 cases (pn_split f2) *
+/3 width=5 by sdj_pn, sdj_pp/
+qed.
+
+(* Inversion lemmas with isid ***********************************************)
+
+corec lemma sdj_inv_refl: ∀f. f ∥ f → 𝐈⦃f⦄.
+#f cases (pn_split f) * #g #Hg #H
+[ lapply (sdj_inv_pp … H … Hg Hg) -H /3 width=3 by isid_push/
+| elim (sdj_inv_nn … H … Hg Hg)
+]
+qed-.
.
interpretation "inclusion (rtmap)"
- 'subseteq t1 t2 = (sle t1 t2).
+ 'subseteq f1 f2 = (sle f1 f2).
(* Basic properties *********************************************************)
#x1 #H #Hx1 destruct lapply (injective_push … Hx1) -Hx1 //
qed-.
-lemma sle_inv_nn: ∀g1,g2. g1 ⊆ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → f1 ⊆ f2.
+lemma sle_inv_nn: ∀g1,g2. g1 ⊆ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → f1 ⊆ f2.
#g1 #g2 #H #f1 #f2 #H1 #H2 elim (sle_inv_nx … H … H1) -g1
#x2 #H #Hx2 destruct lapply (injective_next … Hx2) -Hx2 //
qed-.
[ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_pushs ( ↑*[?]? )" "rtmap_nexts ( ⫯*[?]? )"
"rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_isdiv ( 𝛀⦃?⦄ )"
"rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )" "rtmap_isfin ( 𝐅⦃?⦄ )" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_uni ( 𝐔❴?❵ )"
- "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_sor ( ? ⋓ ? ≡ ? )"
+ "rtmap_sle ( ? ⊆ ? )" "rtmap_sdj ( ? ∥ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_sor ( ? ⋓ ? ≡ ? )"
"rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" "rtmap_coafter ( ? ~⊚ ? ≡ ? )"
* ]
[ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "" "" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" ""
- "" "" "" "" "" "" "nstream_sor" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )"
+ "" "" "" "" "" "" "" "nstream_sor" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )"
* ]
(*
[ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )"
[ "stream ( ? @ ? )" "stream_eq ( ? ≐ ? )" "stream_hdtl ( ↓? )" "stream_tls ( ↓*[?]? )" * ]
[ "list ( ◊ ) ( ? @ ? ) ( |?| )" "list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )" * ]
[ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ∨ ? ) ( ? ∧ ? )" * ]
- [ "relations" "star" "lstar" * ]
+ [ "relations ( ? ⊆ ? )" "star" "lstar" * ]
}
]
}
+++ /dev/null
-../../matitac.opt `cat partial.txt`
-cd basic_2/rt_computation/
-../../../../matitac.opt `cat partial.txt`
-cd ../../
--- /dev/null
+ground_2
+basic_2/syntax
+basic_2/relocation
+basic_2/s_transition
+basic_2/s_computation
+basic_2/static
+basic_2/i_static
projects / helm.git / commitdiff