From 74c6905907b0bca229366d52450e2a6982b5b8be Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 22 Dec 2020 18:22:19 +0100 Subject: [PATCH] =?utf8?q?arithmetics=20for=20=CE=BB=CE=B4?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit + predecessor for non-negative integers + web site update --- .../contribs/lambdadelta/ground/arith/nat.txt | 19 +- .../lambdadelta/ground/arith/nat_le_pred.ma | 31 +++ .../lambdadelta/ground/arith/nat_lt.ma | 6 + .../lambdadelta/ground/arith/nat_lt_plus.ma | 46 ++++ .../lambdadelta/ground/arith/nat_lt_pred.ma | 31 +++ .../lambdadelta/ground/arith/nat_plus.ma | 2 +- .../lambdadelta/ground/arith/nat_pred.ma | 34 +++ .../lambdadelta/ground/arith/nat_pred_succ.ma | 25 +++ .../{nat_iter_succ.ma => nat_succ_iter.ma} | 4 +- .../lambdadelta/ground/arith/pnat_dis.ma | 23 ++ .../lambdadelta/ground/web/ground_src.tbl | 196 ++++++++++-------- 11 files changed, 317 insertions(+), 100 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_le_pred.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma rename matita/matita/contribs/lambdadelta/ground/arith/{nat_iter_succ.ma => nat_succ_iter.ma} (95%) create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/pnat_dis.ma diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat.txt b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt index 96c8c9cc3..7fbb2d7b7 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat.txt +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt @@ -56,19 +56,22 @@ "cic:/matita/arithmetics/nat/f_ind.con" "cic:/matita/arithmetics/nat/f2_ind.con" "cic:/matita/arithmetics/nat/f3_ind.con" - -#################################### - -"cic:/matita/arithmetics/nat/lt_plus_Sn_r.con" -"cic:/matita/arithmetics/nat/lt_plus_to_lt_l.con" +# "cic:/matita/arithmetics/nat/monotonic_lt_plus_l.con" "cic:/matita/arithmetics/nat/monotonic_lt_plus_r.con" - -"cic:/matita/arithmetics/nat/le_pred_n.con" +"cic:/matita/arithmetics/nat/lt_plus_Sn_r.con" +"cic:/matita/arithmetics/nat/lt_plus_to_lt_l.con" +# "cic:/matita/arithmetics/nat/pred.con" +# "cic:/matita/arithmetics/nat/pred_Sn.con" -"cic:/matita/arithmetics/nat/S_pred.con" +# +"cic:/matita/arithmetics/nat/le_pred_n.con" "cic:/matita/arithmetics/nat/monotonic_pred.con" +# +"cic:/matita/arithmetics/nat/S_pred.con" + +#################################### "cic:/matita/arithmetics/nat/discr_minus_x_xy.con" "cic:/matita/arithmetics/nat/discr_plus_xy_minus_xz.con" diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_pred.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_pred.ma new file mode 100644 index 000000000..f1824e22e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_pred.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground/arith/nat_pred_succ.ma". +include "ground/arith/nat_le.ma". + +(* NON-NEGATIVE INTEGERS ****************************************************) + +(* Basic constructions with pred ********************************************) + +(*** le_pred_n *) +lemma nle_pred_sn_refl (m): ↓m ≤ m. +#m elim m -m // +qed. + +(*** monotonic_pred *) +lemma nle_pred_bi (m) (n): m ≤ n → ↓m ≤ ↓n. +#m #n #H elim H -n +/2 width=3 by nle_trans/ +qed. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma index fc445dd74..1df0f857d 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma @@ -26,6 +26,12 @@ interpretation (* Basic constructions ******************************************************) +lemma nlt_i (m) (n): ↑m ≤ n → m < n. +// qed. + +lemma nlt_refl_succ (n): n < ↑n. +// qed. + (*** lt_O_S *) lemma nlt_zero_succ (m): 𝟎 < ↑m. /2 width=1 by nle_succ_bi/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma new file mode 100644 index 000000000..e9920e928 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_plus.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground/arith/nat_le_plus.ma". +include "ground/arith/nat_lt.ma". + +(* NON-NEGATIVE INTEGERS ****************************************************) + +(* Basic constructions with plus ********************************************) + +(*** monotonic_lt_plus_l *) +lemma nlt_plus_bi_dx (m) (n1) (n2): n1 < n2 → n1 + m < n2 + m. +#m #n1 #n2 #H +@nlt_i >nplus_succ_sn /2 width=1 by nle_plus_bi_dx/ +qed. + +(*** monotonic_lt_plus_r *) +lemma nlt_plus_bi_sn (m) (n1) (n2): n1 < n2 → m + n1 < m + n2. +#m #n1 #n2 #H +@nlt_i >nplus_succ_dx /2 width=1 by nle_plus_bi_sn/ +qed. + +(*** lt_plus_Sn_r *) (**) +lemma lt_plus_Sn_r: ∀a,x,n. a < a + x + ↑n. +/2 width=1/ qed-. + +(* Basic inversions with plus ***********************************************) + +(*** lt_plus_to_lt_l *) +lemma nlt_inv_plus_bi_dx (m) (n1) (n2): n1 + m < n2 + m → n1 < n2. +/2 width=2 by nle_inv_plus_bi_dx/ qed-. + +(*** lt_plus_to_lt_r *) +lemma nlt_inv_plus_bi_sn (m) (n1) (n2): m + n1 < m + n2 → n1 < n2. +/2 width=2 by nle_inv_plus_bi_sn/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma new file mode 100644 index 000000000..16e5bb239 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_pred.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground/arith/nat_pred_succ.ma". +include "ground/arith/nat_lt.ma". + +(* NON-NEGATIVE INTEGERS ****************************************************) + +(* Basic constructions with pred ********************************************) + +lemma nlt_zero_sn (m): m = ↑↓m → 𝟎 < m. +// qed. + +(* Basic inversions with pred ***********************************************) + +(*** S_pred *) +lemma nlt_inv_zero_sn (m): 𝟎 < m → m = ↑↓m. +#m @(nat_ind … m) -m // +#H elim (nlt_inv_refl … H) +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma index ffb181cc4..e7702b80d 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground/arith/nat_iter_succ.ma". +include "ground/arith/nat_succ_iter.ma". (* NON-NEGATIVE INTEGERS ****************************************************) diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma new file mode 100644 index 000000000..7c5d8a5ac --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground/notation/functions/downarrow_1.ma". +include "ground/arith/pnat_dis.ma". +include "ground/arith/nat.ma". + +(* NON-NEGATIVE INTEGERS ****************************************************) + +(*** pred *) +definition npred (m): nat ≝ match m with +[ nzero ⇒ 𝟎 +| ninj p ⇒ pdis … (𝟎) ninj p +]. + +interpretation + "predecessor (non-negative integers" + 'DownArrow m = (npred m). + +(* Basic rewrites ***********************************************************) + +lemma npred_zero: 𝟎 = ↓𝟎. +// qed. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma new file mode 100644 index 000000000..71e5e921f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground/arith/nat_succ.ma". +include "ground/arith/nat_pred.ma". + +(* NON-NEGATIVE INTEGERS ****************************************************) + +(* Basic rewrites with succ *************************************************) + +(*** pred_Sn *) +lemma npred_succ (n): n = ↓↑n. +* // +qed. diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_iter_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_iter.ma similarity index 95% rename from matita/matita/contribs/lambdadelta/ground/arith/nat_iter_succ.ma rename to matita/matita/contribs/lambdadelta/ground/arith/nat_succ_iter.ma index cdea03939..640e84d6d 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_iter_succ.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_iter.ma @@ -12,12 +12,12 @@ (* *) (**************************************************************************) -include "ground/arith/nat_succ.ma". include "ground/arith/nat_iter.ma". +include "ground/arith/nat_succ.ma". (* NON-NEGATIVE INTEGERS ****************************************************) -(* Rewrites with nsucc ******************************************************) +(* Rewrites with niter ******************************************************) lemma niter_succ (A) (f) (n) (a): f (f^n a) = f^{A}(↑n) a. #A #f * // diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_dis.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_dis.ma new file mode 100644 index 000000000..cc226c94a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_dis.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground/arith/pnat.ma". + +(* POSITIVE INTEGERS ********************************************************) + +definition pdis (A:Type[0]) (a) (f) (p): A ≝ +match p with +[ punit ⇒ a +| psucc q ⇒ f q +]. diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl index 2ca13aee9..686fcb84f 100644 --- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl @@ -1,97 +1,115 @@ name "ground_src" table { - class "gray" - [ { "component" * } { - [ { "plane" * } { - [ "files" * ] - } - ] - } - ] - class "water" - [ { "generic rt-transition counter" * } { - [ { "" * } { - [ "rtc_ist ( 𝐓❪?,?❫ )" "rtc_ist_shift" "rtc_ist_plus" "rtc_ist_max" * ] - [ "rtc_isrc ( 𝐑𝐓❪?,?❫ )" "rtc_isrt_shift" "rtc_isrt_plus" "rtc_isrt_max" "rtc_isrt_max_shift" * ] - [ "rtc ( 〈?,?,?,?〉 ) ( 𝟘𝟘 ) ( 𝟙𝟘 ) ( 𝟘𝟙 )" "rtc_shift ( ↕*? )" "rtc_plus ( ? + ? )" "rtc_max ( ? ∨ ? )" "rtc_max_shift" * ] - } - ] - } - ] - class "green" - [ { "multiple relocation" * } { - [ { "" * } { - [ "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_sdj ( ? ∥ ? )" "rtmap_sand ( ? ⋒ ? ≘ ? )" "rtmap_sor ( ? ⋓ ? ≘ ? )" - "rtmap_at ( @❪?,?❫ ≘ ? )" "rtmap_istot ( 𝐓❪?❫ )" "rtmap_after ( ? ⊚ ? ≘ ? )" "rtmap_coafter ( ? ~⊚ ? ≘ ? )" - "rtmap_basic ( 𝐁❨?,?❩ )" "rtmap_basic_after" - * ] - [ "nstream ( ⫯? ) ( ↑? )" "nstream_eq" "" "" - "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" - "" "" "" "" - "" "" "" "nstream_sor" - "" "nstream_istot ( ?@❨?❩ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )" - "nstream_basic" "" - * ] + class "gray" + [ { "component" * } { + [ { "plane" * } { + [ "files" * ] + } + ] + } + ] + class "water" + [ { "generic rt-transition counter" * } { + [ { "" * } { + [ "rtc_ist ( 𝐓❪?,?❫ )" "rtc_ist_shift" "rtc_ist_plus" "rtc_ist_max" * ] + [ "rtc_isrc ( 𝐑𝐓❪?,?❫ )" "rtc_isrt_shift" "rtc_isrt_plus" "rtc_isrt_max" "rtc_isrt_max_shift" * ] + [ "rtc ( 〈?,?,?,?〉 ) ( 𝟘𝟘 ) ( 𝟙𝟘 ) ( 𝟘𝟙 )" "rtc_shift ( ↕*? )" "rtc_plus ( ? + ? )" "rtc_max ( ? ∨ ? )" "rtc_max_shift" * ] + } + ] + } + ] + class "green" + [ { "multiple relocation" * } { + [ { "" * } { + [ "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_sdj ( ? ∥ ? )" "rtmap_sand ( ? ⋒ ? ≘ ? )" "rtmap_sor ( ? ⋓ ? ≘ ? )" + "rtmap_at ( @❪?,?❫ ≘ ? )" "rtmap_istot ( 𝐓❪?❫ )" "rtmap_after ( ? ⊚ ? ≘ ? )" "rtmap_coafter ( ? ~⊚ ? ≘ ? )" + "rtmap_basic ( 𝐁❨?,?❩ )" "rtmap_basic_after" + * ] + [ "nstream ( ⫯? ) ( ↑? )" "nstream_eq" "" "" + "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" + "" "" "" "" + "" "" "" "nstream_sor" + "" "nstream_istot ( ?@❨?❩ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )" + "nstream_basic" "" + * ] (* - [ "trace ( ∥?∥ )" "trace_at ( @❪?,?❫ ≘ ? )" "trace_after ( ? ⊚ ? ≘ ? )" "trace_isid ( 𝐈❪?❫ )" "trace_isun ( 𝐔❪?❫ )" - "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≘ ? )" "trace_snot ( ∁ ? )" * ] + [ "trace ( ∥?∥ )" "trace_at ( @❪?,?❫ ≘ ? )" "trace_after ( ? ⊚ ? ≘ ? )" "trace_isid ( 𝐈❪?❫ )" "trace_isun ( 𝐔❪?❫ )" + "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≘ ? )" "trace_snot ( ∁ ? )" * ] *) - [ "mr2 ( ◊ ) ( ❨?,?❩;? )" "mr2_append ( ? @@? )" "mr2_at ( @❪?,?❫ ≘ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≘ ? )" * ] - } - ] - } - ] - class "grass" - [ { "natural numbers with infinity" * } { - [ { "" * } { - [ "ynat ( ∞ )" "ynat_pred ( ↓? )" "ynat_succ ( ↑? )" - "ynat_le ( ? ≤ ? )" "ynat_lt ( ? < ? )" - "ynat_plus ( ? + ? )" "ynat_minus_sn ( ? - ? )" * - ] - } - ] - } - ] - class "yellow" - [ { "extensions to the library" * } { - [ { "" * } { - [ "stream ( ? ⨮{?} ? )" "stream_eq ( ? ≗{?} ? )" "stream_hdtl ( ⫰{?}? )" "stream_tls ( ⫰*{?}[?]? )" * ] - [ "list ( Ⓔ{?} ) ( ? ⨮{?} ? )" "list_length ( |?| )" * ] - [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" "arith_2a" "arith_2b" * ] - [ "ltc" "ltc_ctc" * ] - [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" "lstar_2a" * ] - } - ] - } - ] - class "orange" - [ { "generated library" * } { - [ { "generalization with equality" * } { - [ "insert_eq" * ] - } - ] - [ { "permutation of quantifiers" * } { - [ "pull" * ] - } - ] - [ { "logical decomposables" * } { - [ "xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )" * ] - } - ] - } - ] - class "red" - [ { "" * } { - [ { "" * } { - [ * ] - } - ] - } - ] + [ "mr2 ( ◊ ) ( ❨?,?❩;? )" "mr2_append ( ? @@? )" "mr2_at ( @❪?,?❫ ≘ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≘ ? )" * ] + } + ] + } + ] + class "grass" + [ { "natural numbers with infinity" * } { + [ { "" * } { + [ "ynat ( ∞ )" "ynat_pred ( ↓? )" "ynat_succ ( ↑? )" + "ynat_le ( ? ≤ ? )" "ynat_lt ( ? < ? )" + "ynat_plus ( ? + ? )" "ynat_minus_sn ( ? - ? )" * + ] + } + ] + } + ] + class "grass" + [ { "arithmetics" * } { + [ { "non-negative integers" * } { + [ "nat_lt ( ?<? )" "nat_lt_pred" "nat_lt_plus" * ] + [ "nat_le ( ?≤? )" "nat_le_pred" "nat_le_plus" * ] + [ "nat_plus ( ?+? )" * ] + [ "nat_pred ( ↓? )" "nat_pred_succ" * ] + [ "nat_succ ( ↑? )" "nat_succ_iter" * ] + [ "nat ( 𝟎 )" "nat_iter ( ?^{?}? )" * ] + } + ] + [ { "positive integers" * } { + [ "pnat_plus ( ?+? )" * ] + [ "pnat ( 𝟏 ) ( ↑? )" "pnat_dis" "pnat_iter ( ?^{?}? )" * ] + } + ] + } + ] + class "yellow" + [ { "extensions to the library" * } { + [ { "" * } { + [ "stream ( ? ⨮{?} ? )" "stream_eq ( ? ≗{?} ? )" "stream_hdtl ( ⫰{?}? )" "stream_tls ( ⫰*{?}[?]? )" * ] + [ "list ( Ⓔ{?} ) ( ? ⨮{?} ? )" "list_length ( |?| )" * ] + [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" "arith_2a" "arith_2b" * ] + [ "ltc" "ltc_ctc" * ] + [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" "lstar_2a" * ] + } + ] + } + ] + class "orange" + [ { "generated library" * } { + [ { "generalization with equality" * } { + [ "insert_eq" * ] + } + ] + [ { "permutation of quantifiers" * } { + [ "pull" * ] + } + ] + [ { "logical decomposables" * } { + [ "xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )" * ] + } + ] + } + ] + class "red" + [ { "" * } { + [ { "" * } { + [ * ] + } + ] + } + ] } class "top" { * } -- 2.39.2