[\lambda\delta home]
cic:/matita/lambdadelta/ground/ (background for ฮปฮด version 2)
[Spacer]

homenewsspecificationspecification log
documentationimplementation
forewordmilestonesversion 2(background - syntax - core - applications)
version 2helenaOpen Symbolic Notation (OSN)
citationsvisibilityversion 1(background - core)(static HELM directory)version 1library(static LDDL directory)
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents and its timeline.
categoryunits




sizescharacters (files)190840 (374)nodes (objects)415047 (1294)intrinsic loss factor2.2
propositionstheorems60lemmas1041total1101
conceptsdeclared75defined100total175
Logical Structure of the Specification [butterfly]
This table reports the specification's components and their planes.
componentplanefiles













generic rt-transition countersrtc_ist ( ๐“โช?,?โซ )rtc_ist_shiftrtc_ist_plusrtc_ist_max












rtc_ism ( ๐Œโช?,?โซ )rtc_ism_shiftrtc_ism_plusrtc_ism_maxrtc_ism_max_shift











rtc ( โŒฉ?,?,?,?โŒช ) ( ๐Ÿ˜๐Ÿ˜ ) ( ๐Ÿ™๐Ÿ˜ ) ( ๐Ÿ˜๐Ÿ™ )rtc_shift ( โ†•*? )rtc_plus ( ? + ? )rtc_max ( ? โˆจ ? )rtc_max_shift









relocation mapsfinite relocation with pairsfr2_nat ( @โช?,?โซ โ‰˜ ? )fr2_nat_nat














fr2_minus ( ? โ–ญ ? โ‰˜ ? )















fr2_append ( ?@@? )















fr2_plus ( ?+? )















fr2_map ( โ—Š ) ( โจ?,?โฉ;? )














generic relocationgr_sor ( ? โ‹“ ? โ‰˜ ? )gr_sor_eqgr_sor_tlsgr_sor_isigr_sor_fclagr_sor_isfgr_sor_coafter_ist_isfgr_sor_slegr_sor_sorgr_sor_sor_sle






gr_sand ( ? โ‹’ ? โ‰˜ ? )gr_sand_eq














gr_sdj ( ? โˆฅ ? )gr_sdj_eqgr_sdj_isi













gr_sle ( ? โŠ† ? )gr_sle_eqgr_sle_pushsgr_sle_tlsgr_sle_isigr_sle_isdgr_sle_sle









gr_coafter ( ? ~โŠš ? โ‰˜ ? )gr_coafter_eqgr_coafter_uni_pushsgr_coafter_pat_tlsgr_coafter_nat_tlsgr_coafter_nat_tls_pushsgr_coafter_isigr_coafter_isugr_coafter_ist_isigr_coafter_ist_isfgr_coafter_coaftergr_coafter_coafter_ist




gr_after ( ? โŠš ? โ‰˜ ? )gr_after_eqgr_after_unigr_after_basicgr_after_patgr_after_pat_tlsgr_after_pat_uni_tlsgr_after_nat_uni_tlsgr_after_isigr_after_isugr_after_istgr_after_ist_isigr_after_aftergr_after_after_ist


gr_isd ( ๐›€โช?โซ )gr_isd_eqgr_isd_tlgr_isd_nextsgr_isd_tls











gr_ist ( ๐“โช?โซ )gr_ist_tlsgr_ist_isigr_ist_ist












gr_isf ( ๐…โช?โซ )gr_isf_eqgr_isf_tlgr_isf_pushsfr_isf_tlsgr_ifs_unigr_isf_isu









gr_fcla ( ๐‚โช?โซ โ‰˜ ? )gr_fcla_eqfcla_unigr_fcla_fcla












gr_isu ( ๐”โช?โซ )gr_isu_tlgr_isu_uni













gr_isi ( ๐ˆโช?โซ )gr_isi_eqgr_isi_tlgr_isi_pushsgr_isi_tlsgr_isi_idgr_isi_unigr_isi_pat








gr_nat ( @โ†‘โช?,?โซ โ‰˜ ? )gr_nat_unigr_nat_basicgr_nat_nat












gr_pat ( @โช?,?โซ โ‰˜ ? )gr_pat_ltgr_pat_eqgr_pat_tlsgr_pat_idgr_pat_unigr_pat_basicgr_pat_patgr_pat_pat_id







gr_basic ( ๐›โจ?,?โฉ )















gr_uni ( ๐ฎโจ?โฉ )gr_uni_eq














gr_id ( ๐ข ) gr_id_eq














gr_tls ( โซฑ*[?]? )gr_tls_eqgr_tls_pushsgr_tls_pushs_eqgr_tls_nexts_eq











gr_nexts ( โ†‘*[?]? )gr_nexts_eq














gr_pushs ( โซฏ*[?]? )gr_pushs_eq














gr_tl ( โซฑ? )gr_tl_eqgr_tl_eq_eq













gr_eq ( ? โ‰ก ? )















gr_map ( โซฏ? ) ( โ†‘? )













arithmeticsextensionsarith_2a ( ๐Ÿ )arith_2b













well-founded inductionwf1_ind_ylt















wf1_ind_nltwf2_ind_nltwf3_ind_nlt.ma












non-negative integers with infinityynat_lt ( ?<? )ynat_lt_succynat_lt_predynat_lt_pred_succynat_lt_plusynat_lt_plus_predynat_lt_lminusynat_lt_lminus_plusynat_lt_leynat_lt_le_succynat_lt_le_predynat_lt_le_pred_succynat_lt_le_plusynat_lt_le_lminusynat_lt_le_lminus_plus


ynat_le ( ?โ‰ค? )ynat_le_succynat_le_predynat_le_pred_succynat_le_plusynat_le_lminusynat_le_lminus_succynat_le_lminus_plus








ynat_lminus ( ?-? )ynat_lminus_succynat_lminus_plus













ynat_plus ( ?+? )















ynat_pred ( โ†“? )ynat_pred_succ














ynat_succ ( โ†‘? )















ynat ( ๐ŸŽ ) ( โˆž )ynat_nat













non-negative integersnat_lt ( ?<? )nat_lt_trinat_lt_prednat_lt_plusnat_lt_minusnat_lt_minus_plus










nat_le ( ?โ‰ค? )nat_le_prednat_le_plusnat_le_minusnat_le_minus_plusnat_le_max










nat_max ( ?โˆจ? )















nat_minus ( ?-? )nat_minus_plus














nat_plus ( ?+? )nat_plus_prednat_plus_rplus













nat_rplus ( ?+? )nat_rplus_succ














nat_pred ( โ†“? )nat_pred_succ














nat_succ ( โ†‘? )nat_succ_iternat_succ_tri













nat ( ๐ŸŽ )nat_iter ( ?^{?}? )











nat_tri

positive integersnat_lt ( ?<? )pnat_lt_pred














pnat_le ( ?โ‰ค? )pnat_le_predpnat_le_plus













pnat_plus ( ?+? )















nat_pred ( โ†“? )















pnat ( ๐Ÿ ) ( โ†‘? )pnat_dispnat_iter ( ?^{?}? )pnat_tri










extensions to the librarystreamsstream_tls ( โซฐ*{?}[?]? )stream_tls_eq














stream_hdtl ( โซฐ{?}? )















stream_eq ( ? โ‰—{?} ? )stream_eq_eq














stream ( ? โจฎ{?} ? )














list ( โ’บ{?} ) ( ? โจฎ{?} ? )list_eqlist_length ( |?| )













bool ( โ’ป ) ( โ“‰ )bool_orbool_and













ltcltc_ctc














logic ( โŠฅ ) ( โŠค )relations ( ? โŠ† ? )functionsexteq ( ? โ‰{?,?} ? )starlstar_2a








generated librarygeneralization with equalityinsert_eq














permutation of quantifierspull














logical decomposablesxoa ( โˆƒโˆƒ ) ( โˆจโˆจ ) ( โˆงโˆง )




























[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: Sat, 29 May 2021 16:45:32 +0200