- Makefile: number of objects and intrinsic loss factor added in summary for web page
- basic_2_src.tbl: more descriptions
$$(SUM_$(1)): C0 = $$(shell cat $(1)/$(1)_probe.txt)
$$(SUM_$(1)): S1 = $$(word 1, $$(C0))
$$(SUM_$(1)): S2 = $$(word 2, $$(C0))
+ $$(SUM_$(1)): S3 = $$(word 3, $$(C0))
$$(SUM_$(1)): S4 = $$(word 4, $$(C0))
+ $$(SUM_$(1)): S5 = $$(shell printf "%.1f" `echo "scale=2;$$(S4)/$$(S2)"|bc`)
$$(SUM_$(1)): C1 = $$(word 5, $$(C0))
$$(SUM_$(1)): C2 = $$(word 7, $$(C0))
$$(SUM_$(1)): C3 = $$(shell echo "$$(C1)+$$(C2)"|bc)
$$(SUM_$(1)): P2 = $$(word 9, $$(C0))
$$(SUM_$(1)): P3 = $$(shell echo "$$(P1)+$$(P2)"|bc)
- $$(SUM_$(1)): $$(MAS_$(1)) $(1)/$(1)_probe.txt
+ $$(SUM_$(1)): $$(MAS_$(1)) $(1)/$(1)_probe.txt Makefile
@printf ' SUMMARY $(1)\n'
- @printf 'name "$$(basename $$(@F))"\n\n' > $$@
- @printf 'table {\n' >> $$@
- @printf ' class "gray" [ "category"\n' >> $$@
- @printf ' [ "objects" * ]\n' >> $$@
- @printf ' ]\n' >> $$@
- @printf ' class "water" [ "sizes"\n' >> $$@
- @printf ' [ "files" "$$(S1)" ]\n' >> $$@
- @printf ' [ "characters" "$$(S2)" ]\n' >> $$@
- @printf ' [ "nodes" "$$(S4)" ]\n' >> $$@
- @printf ' ]\n' >> $$@
- @printf ' class "green" [ "propositions"\n' >> $$@
- @printf ' [ "theorems" "$$(P1)" ]\n' >> $$@
- @printf ' [ "lemmas" "$$(P2)" ]\n' >> $$@
- @printf ' [ "total" "$$(P3)" ]\n' >> $$@
- @printf ' ]\n' >> $$@
- @printf ' class "grass" [ "concepts"\n' >> $$@
- @printf ' [ "declared" "$$(C1)" ]\n' >> $$@
- @printf ' [ "defined" "$$(C2)" ]\n' >> $$@
- @printf ' [ "total" "$$(C3)" ]\n' >> $$@
- @printf ' ]\n' >> $$@
- @printf '}\n\n' >> $$@
- @printf 'class "capitalize italic" { 0 }\n\n' >> $$@
- @printf 'class "italic" { 1 } { 3 } { 5 }\n\n' >> $$@
- @printf 'class "right italic" { 2 } { 4 } { 6 }\n' >> $$@
+ @printf 'name "$$(basename $$(@F))"\n\n' > $$@
+ @printf 'table {\n' >> $$@
+ @printf ' class "gray" [ "category"\n' >> $$@
+ @printf ' [ "units" * ]\n' >> $$@
+ @printf ' ]\n' >> $$@
+ @printf ' class "water" [ "sizes"\n' >> $$@
+ @printf ' [ "characters (files)" "$$(S2) ($$(S1))" ]\n' >> $$@
+ @printf ' [ "nodes (objects)" "$$(S4) ($$(S3))" ]\n' >> $$@
+ @printf ' [ "intrinsic loss factor" "$$(S5)" ]\n' >> $$@
+ @printf ' ]\n' >> $$@
+ @printf ' class "green" [ "propositions"\n' >> $$@
+ @printf ' [ "theorems" "$$(P1)" ]\n' >> $$@
+ @printf ' [ "lemmas" "$$(P2)" ]\n' >> $$@
+ @printf ' [ "total" "$$(P3)" ]\n' >> $$@
+ @printf ' ]\n' >> $$@
+ @printf ' class "grass" [ "concepts"\n' >> $$@
+ @printf ' [ "declared" "$$(C1)" ]\n' >> $$@
+ @printf ' [ "defined" "$$(C2)" ]\n' >> $$@
+ @printf ' [ "total" "$$(C3)" ]\n' >> $$@
+ @printf ' ]\n' >> $$@
+ @printf '}\n\n' >> $$@
+ @printf 'class "capitalize italic" { 0 }\n\n' >> $$@
+ @printf 'class "italic" { 1 } { 3 } { 5 }\n\n' >> $$@
+ @printf 'class "right italic" { 2 } { 4 } { 6 }\n' >> $$@
.PHONY: $$(SUM_$(1))
endef
--- /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 L1 ⦄ ⊢ ⬈[ break term 46 h ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'PRedTySn $h $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 L1 ⦄ ⊢ ⬈*[ break term 46 h ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'PRedTySnStar $h $G $L1 $L2 }.
(* 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.
+
+(* Basic inversion lemmas ***************************************************)
+
+(* Basic_2A1: was: lpx_sn_inv_atom1: *)
+lemma lex_inv_atom_sn: ∀R,L2. ⋆ ⪤[R] L2 → L2 = ⋆.
+#R #L2 * #f #Hf #H >(lexs_inv_atom1 … H) -L2 //
+qed-.
+
+(* Basic_2A1: was: lpx_sn_inv_pair1 *)
+lemma lex_inv_pair_sn: ∀R,I,L2,K1,V1. K1.ⓑ{I}V1 ⪤[R] L2 →
+ ∃∃K2,V2. K1 ⪤[R] K2 & R K1 V1 V2 & L2 = K2.ⓑ{I}V2.
+#R #I #L2 #K1 #V1 * #f #Hf #H
+lapply (lexs_eq_repl_fwd … H (↑f) ?) -H /2 width=1 by eq_push_inv_isid/ #H
+elim (lexs_inv_push1 … H) -H #Z2 #K2 #HK12 #HZ2 #H destruct
+elim (ext2_inv_pair_sn … HZ2) -HZ2 #V2 #HV12 #H destruct
+/3 width=5 by ex3_2_intro, ex2_intro/
+qed-.
+
+(* Basic_2A1: was: lpx_sn_inv_atom2 *)
+lemma lex_inv_atom_dx: ∀R,L1. L1 ⪤[R] ⋆ → L1 = ⋆.
+#R #L1 * #f #Hf #H >(lexs_inv_atom2 … H) -L1 //
+qed-.
+
+(* Basic_2A1: was: lpx_sn_inv_pair2 *)
+lemma lex_inv_pair_dx: ∀R,I,L1,K2,V2. L1 ⪤[R] K2.ⓑ{I}V2 →
+ ∃∃K1,V1. K1 ⪤[R] K2 & R K1 V1 V2 & L1 = K1.ⓑ{I}V1.
+#R #I #L1 #K2 #V2 * #f #Hf #H
+lapply (lexs_eq_repl_fwd … H (↑f) ?) -H /2 width=1 by eq_push_inv_isid/ #H
+elim (lexs_inv_push2 … H) -H #Z1 #K1 #HK12 #HZ1 #H destruct
+elim (ext2_inv_pair_dx … HZ1) -HZ1 #V1 #HV12 #H destruct
+/3 width=5 by ex3_2_intro, ex2_intro/
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_2A1: was: lpx_sn_inv_pair *)
+lemma lex_inv_pair: ∀R,I1,I2,L1,L2,V1,V2.
+ L1.ⓑ{I1}V1 ⪤[R] L2.ⓑ{I2}V2 →
+ ∧∧ L1 ⪤[R] L2 & R L1 V1 V2 & I1 = I2.
+#R #I1 #I2 #L1 #L2 #V1 #V2 #H elim (lex_inv_pair_sn … H) -H
+#L0 #V0 #HL10 #HV10 #H destruct /2 width=1 by and3_intro/
+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/i_static/tc_lfxs_lex.ma".
+include "basic_2/rt_transition/lfpx_frees.ma".
+include "basic_2/rt_computation/lpxs.ma".
+include "basic_2/rt_computation/lfpxs.ma".
+
+(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****)
+
+(* Properties with uncounted parallel rt-computation for local environments *)
+
+lemma lfpxs_lpxs_lfeq: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L →
+ ∀L2,T. L ≡[T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
+/2 width=3 by tc_lfxs_lex_lfeq/ qed.
+
+(* Inversion lemmas with uncounted parallel rt-computation for local envs ***)
+
+lemma lpx_cpxs_ext_trans: ∀h,G. s_rs_transitive_isid cfull (cpx_ext h G).
+#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10
+
+
+lemma tc_lfxs_inv_lex_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 →
+ ∃∃L. ⦃G, L1⦄ ⊢ ⬈*[h] L & L ≡[T] L2.
+#h #G @tc_lfxs_inv_lex_lfeq //
+[ @lfpx_frees_conf
+| @lpx_cpxs_ext_trans
\ No newline at end of file
--- /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/predtysnstar_4.ma".
+include "basic_2/relocation/lex.ma".
+include "basic_2/rt_computation/cpxs.ma".
+
+(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *****************)
+
+definition lpxs: ∀h. relation3 genv lenv lenv ≝
+ λh,G. lex (cpxs h G).
+
+interpretation
+ "uncounted parallel rt-computation (local environment)"
+ 'PRedTySnStar h G L1 L2 = (lpxs h G L1 L2).
cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_fqus.ma cpxs_lsubr.ma cpxs_lfdeq.ma cpxs_aaa.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma
+lpxs.ma
lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_aaa.ma lfpxs_cpxs.ma lfpxs_lfpxs.ma
csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_lfdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_lfpxs.ma csx_csx.ma
csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/notation/relations/predtysn_4.ma".
+include "basic_2/relocation/lex.ma".
+include "basic_2/rt_transition/cpx.ma".
+
+(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENVIRONMENTS ******************)
+
+definition lpx: sh → genv → relation lenv ≝
+ λh,G. lex (cpx h G).
+
+interpretation
+ "uncounted parallel rt-transition (local environment)"
+ 'PRedTySn h G L1 L2 = (lpx h G L1 L2).
+
+(* Basic properties *********************************************************)
+
+(*
+lemma lpx_pair: ∀h,g,I,G,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ⬈[h] K2 → ⦃G, K1⦄ ⊢ V1 ⬈[h] V2 →
+ ⦃G, K1.ⓑ{I}V1⦄ ⊢ ⬈[h] K2.ⓑ{I}V2.
+/2 width=1 by lpx_sn_pair/ qed.
+*)
+
+lemma lpx_refl: ∀h,G. reflexive … (lpx h G).
+/2 width=1 by lex_refl/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+(* Basic_2A1: was: lpx_inv_atom1 *)
+lemma lpx_inv_atom_sn: ∀h,G,L2. ⦃G, ⋆⦄ ⊢ ⬈[h] L2 → L2 = ⋆.
+/2 width=2 by lex_inv_atom_sn/ qed-.
+
+(* Basic_2A1: was: lpx_inv_pair1 *)
+lemma lpx_inv_pair_sn: ∀h,I,G,L2,K1,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ⬈[h] L2 →
+ ∃∃K2,V2. ⦃G, K1⦄ ⊢ ⬈[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈[h] V2 &
+ L2 = K2.ⓑ{I}V2.
+/2 width=1 by lex_inv_pair_sn/ qed-.
+
+(* Basic_2A1: was: lpx_inv_atom2 *)
+lemma lpx_inv_atom_dx: ∀h,G,L1. ⦃G, L1⦄ ⊢ ⬈[h] ⋆ → L1 = ⋆.
+/2 width=2 by lex_inv_atom_dx/ qed-.
+
+(* Basic_2A1: was: lpx_inv_pair2 *)
+lemma lpx_inv_pair2_dx: ∀h,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ⬈[h] K2.ⓑ{I}V2 →
+ ∃∃K1,V1. ⦃G, K1⦄ ⊢ ⬈[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈[h] V2 &
+ L1 = K1.ⓑ{I}V1.
+/2 width=1 by lex_inv_pair_dx/ qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lpx_inv_pair: ∀h,I1,I2,G,L1,L2,V1,V2. ⦃G, L1.ⓑ{I1}V1⦄ ⊢ ⬈[h] L2.ⓑ{I2}V2 →
+ ∧∧ ⦃G, L1⦄ ⊢ ⬈[h] L2 & ⦃G, L1⦄ ⊢ V1 ⬈[h] V2 & I1 = I2.
+/2 width=1 by lex_inv_pair/ qed-.
*)
[ { "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 lenvs on referred entries" ] "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 lenvs on referred entries" ] "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ]
+ [ [ "for lenvs on all entries" ] "lpxs ( ⦃?,?⦄ ⊢ ⬈*[?] ? )" * ]
[ [ "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" * ]
}
]
[ { "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 lenvs on all entries" ] "lpx ( ⦃?,?⦄ ⊢ ⬈[?] ? )" * ]
[ [ "for binders" ] "cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ]
[ [ "for terms" ] "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" * ]
}
]
class "water"
[ { "iterated static typing" * } {
- [ { "iterated extension on referred entries" * } {
- [ [ "" ] "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_lex" + "tc_lfxs_drops" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ]
+ [ { "iterated generic extension of a context-sensitive relation" * } {
+ [ [ "for lenvs on referred entries" ] "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_lex" + "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" *]
+ [ [ "restricted refinement for lenvs" ] "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ]
+ [ [ "candidates" ] "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ]
+ [ [ "computation properties" ] "gcp" *]
}
]
[ { "atomic arity assignment" * } {
- [ [ "" ] "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ]
- [ [ "" ] "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_aaa" * ]
+ [ [ "restricted refinement for lenvs" ] "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ]
+ [ [ "for terms" ] "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" * ]
+ [ { "degree-based equivalence" * } {
+ [ [ "for closures on referred entries" ] "ffdeq ( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ]
+ [ [ "for lenvs on referred entries" ] "lfdeq ( ? ≛[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ]
}
]
- [ { "syntactic equivalence on referred entries" * } {
- [ [ "" ] "lfeq ( ? ≡[?] ? )" "lfeq_fqup" + "lfeq_lfeq" * ]
+ [ { "syntactic equivalence" * } {
+ [ [ "for lenvs on referred entries" ] "lfeq ( ? ≡[?] ? )" "lfeq_fqup" + "lfeq_lfeq" * ]
}
]
- [ { "generic extension on referred entries" * } {
- [ [ "" ] "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_drops" + "lfxs_fqup" + "lfxs_lfxs" * ]
+ [ { "generic extension of a context-sensitive relation" * } {
+ [ [ "for lenvs on referred entries" ] "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" * ]
+ [ [ "restricted refinement for lenvs" ] "lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )" "lsubf_lsubr" + "lsubf_frees" + "lsubf_lsubf" * ]
+ [ [ "for terms" ] "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_drops" + "frees_fqup" + "frees_frees" * ]
}
]
- [ { "restricted ref. for local env." * } {
- [ [ "" ] "lsubr ( ? ⫃ ? )" "lsubr_length" + "lsubr_drops" + "lsubr_lsubr" * ]
+ [ { "local environments" * } {
+ [ [ "restricted refinement" ] "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" * ]
+ [ { "iterated structural successor" * } {
+ [ [ "for closures" ] "fqus ( ⦃?,?,?⦄ ⊐*[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )" "fqus_weight" + "fqus_drops" + "fqus_fqup" + "fqus_fqus" * ]
+ [ [ "proper for closures" ] "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" * ]
+ [ { "structural successor" * } {
+ [ [ "for closures" ] "fquq ( ⦃?,?,?⦄ ⊐⸮[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )" "fquq_length" + "fquq_weight" * ]
+ [ [ "proper for closures" ] "fqu ( ⦃?,?,?⦄ ⊐[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )" "fqu_length" + "fqu_weight" * ]
}
]
}
projects / helm.git / commitdiff