1 <?xml version="1.0" encoding="UTF-8"?>
2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
3 <html xmlns="http://www.w3.org/1999/xhtml" dir="ltr" lang="en-us">
5 <meta http-equiv="Content-Language" content="en-us" />
6 <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
7 <meta http-equiv="Content-Style-Type" content="text/css" />
8 <meta name="author" content="Ferruccio Guidi" />
9 <meta name="description" content="background for \lambda\delta version 2" />
10 <title>background for \lambda\delta version 2</title>
11 <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css" />
12 <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css" />
13 <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css" />
14 <link rel="shortcut icon" href="http://lambdadelta.info/images/crux_16.ico" />
18 <a href="http://lambdadelta.info/">
19 <img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
22 <div class="head1">cic:/matita/lambdadelta/ground_2/ (background for λδ version 2)</div>
24 <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
26 <div xmlns:ld="http://lambdadelta.info/" class="head2">Summary of the Specification</div>
27 <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
29 Nodes are counted according to the "intrinsinc complexity measure"
30 [F. Guidi: "Procedural Representation of CIC Proof Terms"
31 Journal of Automated Reasoning 44(1-2), Springer (February 2010),
34 <div xmlns:ld="http://lambdadelta.info/" class="text">
35 <table cellpadding="4" cellspacing="0">
38 <td class="snns component grey">category</td>
39 <td class="snns plane grey">objects</td>
40 <td class="snnn number grey">
43 <td class="snnn plane grey">
46 <td class="snnn number grey">
49 <td class="snnn plane grey">
52 <td class="ssnn number grey">
57 <td class="snns component cyan">sizes</td>
58 <td class="snns plane cyan">files</td>
59 <td class="snnn number cyan">31</td>
60 <td class="snns plane cyan">characters</td>
61 <td class="snnn number cyan">75964</td>
62 <td class="snns plane cyan">nodes</td>
63 <td class="ssnn number cyan">61055</td>
66 <td class="snns component green">propositions</td>
67 <td class="snns plane green">theorems</td>
68 <td class="snnn number green">2</td>
69 <td class="snns plane green">lemmas</td>
70 <td class="snnn number green">182</td>
71 <td class="snns plane green">total</td>
72 <td class="ssnn number green">184</td>
75 <td class="snss component yellow">concepts</td>
76 <td class="snss plane yellow">declared</td>
77 <td class="snsn number yellow">41</td>
78 <td class="snss plane yellow">defined</td>
79 <td class="snsn number yellow">25</td>
80 <td class="snss plane yellow">total</td>
81 <td class="sssn number yellow">66</td>
86 <ul xmlns:ld="http://lambdadelta.info/">
88 <span class="date">2013 November 27.</span>
89 Natural numbers with infinity.
92 <ul xmlns:ld="http://lambdadelta.info/">
94 <span class="date">2011 August 10.</span>
99 <div xmlns:ld="http://lambdadelta.info/" class="head2">Logical Structure of the Specification</div>
100 <div xmlns:ld="http://lambdadelta.info/" class="text">The source files are grouped in planes
101 according to the following table.
102 Notation files covering the whole specification are provided.
103 The notation for the relations or functions introduced in each file
104 is shown in parentheses (? are placeholders).
106 <div xmlns:ld="http://lambdadelta.info/" class="text">
107 <table cellpadding="4" cellspacing="0">
110 <td class="snns plane grey">plane</td>
111 <td class="snns file grey">files</td>
112 <td class="snnn file grey">
115 <td class="snnn file grey">
118 <td class="snnn file grey">
121 <td class="snnn file grey">
124 <td class="snnn file grey">
127 <td class="snnn file grey">
130 <td class="snnn file grey">
133 <td class="ssnn file grey">
138 <td class="snns plane yellow">natural numbers with infinity</td>
139 <td class="snns file yellow">ynat ( ∞ )</td>
140 <td class="snnn file yellow">ynat_pred ( ⫰? )</td>
141 <td class="snnn file yellow">ynat_succ ( ⫯? )</td>
142 <td class="snnn file yellow">ynat_le ( ?≤? )</td>
143 <td class="snnn file yellow">ynat_lt ( ?<? )</td>
144 <td class="snnn file yellow">ynat_minus ( ? - ? )</td>
145 <td class="snnn file yellow">ynat_plus ( ? + ? )</td>
146 <td class="snnn file yellow">ynat_max</td>
147 <td class="ssnn file yellow">ynat_min</td>
150 <td class="snns plane orange">extensions to the library</td>
151 <td class="snns file orange">arith.ma ( ?^? )</td>
152 <td class="snnn file orange">
155 <td class="snnn file orange">
158 <td class="snnn file orange">
161 <td class="snnn file orange">
164 <td class="snnn file orange">
167 <td class="snnn file orange">
170 <td class="snnn file orange">
173 <td class="ssnn file orange">
178 <td class="snss plane red">generated logical decomposables</td>
179 <td class="snss file red">xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )</td>
180 <td class="snsn file red">xoa_props ( ⊥ ) ( ⊤ )</td>
181 <td class="snsn file red">
184 <td class="snsn file red">
187 <td class="snsn file red">
190 <td class="snsn file red">
193 <td class="snsn file red">
196 <td class="snsn file red">
199 <td class="sssn file red">
207 <div xmlns:ld="http://lambdadelta.info/" class="head2">Physical Structure of the Specification</div>
208 <div xmlns:ld="http://lambdadelta.info/" class="text">The source files are grouped in directories,
212 <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
214 <div xmlns:ld="http://lambdadelta.info/" class="spacer">
217 <div xmlns:ld="http://lambdadelta.info/" class="spacer">
218 <a href="http://validator.w3.org/check?uri=referer">
219 <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
221 <a href="http://jigsaw.w3.org/css-validator/check/referer">
222 <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
224 <a href="http://www.w3.org/XML/">
225 <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
227 <a href="http://www.w3.org/Graphics/PNG/">
228 <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
230 <a href="http://www.anybrowser.org/campaign/">
231 <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
234 <div xmlns:ld="http://lambdadelta.info/" class="spacer">
237 <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 18 Jun 2014 17:05:26 +0200</div>