From: Ferruccio Guidi Date: Wed, 21 Mar 2018 19:20:36 +0000 (+0100) Subject: update in basic_2 X-Git-Tag: make_still_working~348 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1fd62f1ce4f8209dec780d80aa53b140a8882ad7;p=helm.git update in basic_2 + first results on fsb --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbs/fpbs_fpb.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbs/fpbs_fpb.etc deleted file mode 100644 index 40a2eb057..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbs/fpbs_fpb.etc +++ /dev/null @@ -1,16 +0,0 @@ -(* Properties on extended context-sensitive parallel computation for terms **) - -lemma fpbs_cpx_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, o] U2 → (T2 = U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ≥[h, o] ⦃G2, L2, U2⦄. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 #HnTU2 elim (fpbs_inv_alt … H) -H -#L00 #L0 #T0 #HT10 #H10 #HL00 #HL02 lapply (lleq_cpx_trans … HTU2 … HL02) -HTU2 -#HTU2 lapply (cpx_lleq_conf_sn … HTU2 … HL02) -HL02 -#HL02 lapply (lpxs_cpx_trans … HTU2 … HL00) -HTU2 -#HTU2 elim (fqus_cpxs_trans_neq … H10 … HTU2 HnTU2) -H10 -HTU2 -HnTU2 -#U0 #HTU0 #HnTU0 #HU02 elim (eq_term_dec T1 T0) #HnT10 destruct -[ -HT10 elim (cpxs_neq_inv_step_sn … HTU0 HnTU0) -HTU0 -HnTU0 -| -HnTU0 elim (cpxs_neq_inv_step_sn … HT10 HnT10) -HT10 -HnT10 -] -/4 width=10 by fpbs_intro_alt, cpxs_trans, ex3_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsn_5.ma deleted file mode 100644 index fa72d2355..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsn_5.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦥ [ term 46 h, 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 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsnalt_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsnalt_5.ma deleted file mode 100644 index e9984754d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsnalt_5.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦥ ⦥ [ term 46 h, 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 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystrong_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystrong_5.ma new file mode 100644 index 000000000..adc313743 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystrong_5.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ≥ [ term 46 h, break term 46 o ] 𝐒 ⦃ break term 46 G, break term 46 L, break term 46 T ⦄ )" + non associative with precedence 45 + for @{ 'PRedSubTyStrong $h $o $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma index c27ffaba5..925beb513 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma @@ -12,11 +12,10 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/btsn_5.ma". -include "basic_2/reduction/fpb.ma". -include "basic_2/computation/csx.ma". +include "basic_2/notation/relations/predsubtystrong_5.ma". +include "basic_2/rt_transition/fpb.ma". -(* "QRST" STRONGLY NORMALIZING CLOSURES *************************************) +(* STRONGLY NORMALIZING CLOSURES FOR PARALLEL RST-TRANSITION ****************) inductive fsb (h) (o): relation3 genv lenv term ≝ | fsb_intro: ∀G1,L1,T1. ( @@ -25,23 +24,23 @@ inductive fsb (h) (o): relation3 genv lenv term ≝ . interpretation - "'qrst' strong normalization (closure)" - 'BTSN h o G L T = (fsb h o G L T). + "strong normalization for parallel rst-transition (closure)" + 'PRedSubTyStrong h o G L T = (fsb h o G L T). (* Basic eliminators ********************************************************) +(* Note: eliminator with shorter ground hypothesis *) +(* Note: to be named fsb_ind when fsb becomes a definition like csx, lfsx ***) lemma fsb_ind_alt: ∀h,o. ∀R: relation3 …. ( - ∀G1,L1,T1. ⦥[h,o] ⦃G1, L1, T1⦄ → ( + ∀G1,L1,T1. ≥[h,o] 𝐒⦃G1, L1, T1⦄ → ( ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2 ) → R G1 L1 T1 ) → - ∀G,L,T. ⦥[h, o] ⦃G, L, T⦄ → R G L T. + ∀G,L,T. ≥[h, o] 𝐒⦃G, L, T⦄ → R G L T. #h #o #R #IH #G #L #T #H elim H -G -L -T /4 width=1 by fsb_intro/ qed-. -(* Basic inversion lemmas ***************************************************) - -lemma fsb_inv_csx: ∀h,o,G,L,T. ⦥[h, o] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ ⬊*[h, o] T. -#h #o #G #L #T #H elim H -G -L -T /5 width=1 by csx_intro, fpb_cpx/ -qed-. +(* Basic_2A1: removed theorems 5: + fsba_intro fsba_ind_alt fsba_fpbs_trans fsb_fsba fsba_inv_fsb +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_alt.ma deleted file mode 100644 index eadfece46..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_alt.ma +++ /dev/null @@ -1,82 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/btsnalt_5.ma". -include "basic_2/computation/fpbg_fpbs.ma". -include "basic_2/computation/fsb.ma". - -(* "QRST" STRONGLY NORMALIZING CLOSURES *************************************) - -(* Note: alternative definition of fsb *) -inductive fsba (h) (o): relation3 genv lenv term ≝ -| fsba_intro: ∀G1,L1,T1. ( - ∀G2,L2,T2. ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄ → fsba h o G2 L2 T2 - ) → fsba h o G1 L1 T1. - -interpretation - "'big tree' strong normalization (closure) alternative" - 'BTSNAlt h o G L T = (fsba h o G L T). - -(* Basic eliminators ********************************************************) - -lemma fsba_ind_alt: ∀h,o. ∀R: relation3 …. ( - ∀G1,L1,T1. ⦥⦥[h,o] ⦃G1, L1, T1⦄ → ( - ∀G2,L2,T2. ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2 - ) → R G1 L1 T1 - ) → - ∀G,L,T. ⦥⦥[h, o] ⦃G, L, T⦄ → R G L T. -#h #o #R #IH #G #L #T #H elim H -G -L -T -/4 width=1 by fsba_intro/ -qed-. - -(* Basic properties *********************************************************) - -lemma fsba_fpbs_trans: ∀h,o,G1,L1,T1. ⦥⦥[h, o] ⦃G1, L1, T1⦄ → - ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → ⦥⦥[h, o] ⦃G2, L2, T2⦄. -#h #o #G1 #L1 #T1 #H @(fsba_ind_alt … H) -G1 -L1 -T1 -/4 width=5 by fsba_intro, fpbs_fpbg_trans/ -qed-. - -(* Main properties **********************************************************) - -theorem fsb_fsba: ∀h,o,G,L,T. ⦥[h, o] ⦃G, L, T⦄ → ⦥⦥[h, o] ⦃G, L, T⦄. -#h #o #G #L #T #H @(fsb_ind_alt … H) -G -L -T -#G1 #L1 #T1 #_ #IH @fsba_intro -#G2 #L2 #T2 * /3 width=5 by fsba_fpbs_trans/ -qed. - -(* Main inversion lemmas ****************************************************) - -theorem fsba_inv_fsb: ∀h,o,G,L,T. ⦥⦥[h, o] ⦃G, L, T⦄ → ⦥[h, o] ⦃G, L, T⦄. -#h #o #G #L #T #H @(fsba_ind_alt … H) -G -L -T -/4 width=1 by fsb_intro, fpb_fpbg/ -qed-. - -(* Advanced properties ******************************************************) - -lemma fsb_fpbs_trans: ∀h,o,G1,L1,T1. ⦥[h, o] ⦃G1, L1, T1⦄ → - ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → ⦥[h, o] ⦃G2, L2, T2⦄. -/4 width=5 by fsba_inv_fsb, fsb_fsba, fsba_fpbs_trans/ qed-. - -(* Advanced eliminators *****************************************************) - -lemma fsb_ind_fpbg: ∀h,o. ∀R:relation3 genv lenv term. - (∀G1,L1,T1. ⦥[h, o] ⦃G1, L1, T1⦄ → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ >≛[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - R G1 L1 T1 - ) → - ∀G1,L1,T1. ⦥[h, o] ⦃G1, L1, T1⦄ → R G1 L1 T1. -#h #o #R #IH #G1 #L1 #T1 #H @(fsba_ind_alt h o … G1 L1 T1) -/3 width=1 by fsba_inv_fsb, fsb_fsba/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_ffdeq.ma new file mode 100644 index 000000000..fa0242a51 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_ffdeq.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fpb_ffdeq.ma". +include "basic_2/rt_computation/fsb.ma". + +(* STRONGLY NORMALIZING CLOSURES FOR PARALLEL RST-TRANSITION ****************) + +(* Properties with degree-based equivalence for closures ********************) + +lemma fsb_ffdeq_trans: ∀h,o,G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ≥[h, o] 𝐒⦃G2, L2, T2⦄. +#h #o #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1 +#G1 #L1 #T1 #_ #IH #G2 #L2 #T2 #H12 +@fsb_intro #G #L #T #H2 +elim (ffdeq_fpb_trans … H12 … H2) -G2 -L2 -T2 +/2 width=5 by/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma new file mode 100644 index 000000000..4dbe33e07 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma @@ -0,0 +1,66 @@ +(**************************************************************************) +(* ___ *) +(* ||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_computation/fpbg_fpbs.ma". +include "basic_2/rt_computation/fsb_ffdeq.ma". + +(* STRONGLY NORMALIZING CLOSURES FOR PARALLEL RST-TRANSITION ****************) + +(* Properties with parallel rst-computation for closures ********************) + +lemma fsb_fpbs_trans: ∀h,o,G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → ≥[h, o] 𝐒⦃G2, L2, T2⦄. +#h #o #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1 +#G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12 +elim (fpbs_inv_fpbg … H12) -H12 +[ -IH /2 width=5 by fsb_ffdeq_trans/ +| -H1 * /2 width=5 by/ +] +qed-. + +(* Properties with proper parallel rst-computation for closures *************) + +lemma fsb_intro_fpbg: ∀h,o,G1,L1,T1. ( + ∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → ≥[h, o] 𝐒⦃G2, L2, T2⦄ + ) → ≥[h, o] 𝐒⦃G1, L1, T1⦄. +/4 width=1 by fsb_intro, fpb_fpbg/ qed. + +(* Eliminators with proper parallel rst-computation for closures ************) + +lemma fsb_ind_fpbg_fpbs: ∀h,o. ∀R:relation3 genv lenv term. + (∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + R G1 L1 T1 + ) → + ∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2. +#h #o #R #IH1 #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1 +#G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12 +@IH1 -IH1 +[ -IH /2 width=5 by fsb_fpbs_trans/ +| -H1 #G0 #L0 #T0 #H10 + elim (fpbs_fpbg_trans … H12 … H10) -G2 -L2 -T2 + /2 width=5 by/ +] +qed-. + +lemma fsb_ind_fpbg: ∀h,o. ∀R:relation3 genv lenv term. + (∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + R G1 L1 T1 + ) → + ∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ → R G1 L1 T1. +#h #o #R #IH #G1 #L1 #T1 #H @(fsb_ind_fpbg_fpbs … H) -H +/3 width=1 by/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index 10c38172d..c92ce8415 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -8,3 +8,4 @@ lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lpx.ma lfsx_lpxs.ma lfsx_lfpxs.ma lfsx_c lsubsx.ma lsubsx_lfsx.ma lsubsx_lsubsx.ma fpbs.ma fpbs_fqup.ma fpbs_fqus.ma fpbs_aaa.ma fpbs_fpb.ma fpbs_cpxs.ma fpbs_lfpxs.ma fpbs_csx.ma fpbs_fpbs.ma fpbg.ma fpbg_fqup.ma fpbg_cpxs.ma fpbg_lfpxs.ma fpbg_fpbs.ma fpbg_fpbg.ma +fsb.ma fsb_ffdeq.ma fsb_fpbg.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 7ec7cd11c..c56156618 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -74,22 +74,6 @@ table { class "sky" [ { "rt-computation" * } { (* - [ { "evaluation for context-sensitive rt-reduction" * } { - [ [ "" ] "cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )" * ] - } - ] - [ { "evaluation for context-sensitive reduction" * } { - [ [ "" ] "cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )" "cpre_cpre" * ] - } - ] - [ { "strongly normalizing qrst-computation" * } { - [ [ "" ] "fsb ( ⦥[?,?] ⦃?,?,?⦄ )" "fsb_alt ( ⦥⦥[?,?] ⦃?,?,?⦄ )" "fsb_aaa" + "fsb_csx" * ] - } - ] - [ { "parallel qrst-computation" * } { - - } - ] [ { "decomposed rt-computation" * } { [ [ "" ] "scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )" "scpds_lift" + "scpds_aaa" + "scpds_scpds" * ] } @@ -101,6 +85,7 @@ table { ] *) [ { "uncounted context-sensitive parallel rst-computation" * } { + [ [ "strongly normalizing for closures" ] "fsb" + "( ≥[?,?] 𝐒⦃?,?,?⦄ )" "fsb_ffdeq" + "fsb_aaa" + "fsb_csx" + "fsb_fpbg" * ] [ [ "proper for closures" ] "fpbg" + "( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_fqup" + "fpbg_cpxs" + "fpbg_lfpxs" + "fpbg_fpbs" + "fpbg_fpbg" * ] [ [ "for closures" ] "fpbs" + "( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_fqup" + "fpbs_fqus" + "fpbs_aaa" + "fpbs_fpb" + "fpbs_cpxs" + "fpbs_lfpxs" + "fpbs_csx" + "fpbs_fpbs" * ] } @@ -304,6 +289,14 @@ class "capitalize italic" { 0 1 } class "italic" { 2 } (* + [ { "evaluation for context-sensitive rt-reduction" * } { + [ [ "" ] "cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )" * ] + } + ] + [ { "evaluation for context-sensitive reduction" * } { + [ [ "" ] "cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )" "cpre_cpre" * ] + } + ] [ { "normal forms for context-sensitive rt-reduction" * } { [ [ "" ] "cnx_crx" + "cnx_cix" * ] } @@ -348,14 +341,6 @@ class "italic" { 2 } [ [ "" ] "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ] } ] - [ { "pointwise union for local environments" * } { - [ [ "" ] "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" * ] - } - ] [ { "global env. slicing" * } { [ [ "" ] "gget ( ⬇[?] ? ≡ ? )" "gget_gget" * ] } @@ -368,10 +353,4 @@ class "italic" { 2 } [ [ "" ] "lsuby ( ? ⊆[?,?] ? )" "lsuby_lsuby" * ] } ] - [ { "pointwise extension of a relation" * } { - [ [ "" ] "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" * ] *)