X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fcontent_to_html.xsl;h=6e7ff7ca510fec16a2887df9dddeadf81d974841;hb=50e2ee8fb7fd4a2a14bf60779e1c709b220c6072;hp=30d7009cf684e069a799f7d8caef7fec73513046;hpb=315b5ad70270b2b5b151a512501b30b50b6c4916;p=helm.git
diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index 30d7009cf..6e7ff7ca5 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -29,16 +29,12 @@
-
+
-
-
-
-
-getciconly?uri=
-
-apply?keys=¶m.naturalLanguage=¶m.keys=¶m.getterURL=¶m.processorURL=&xmluri=
+
+
+
@@ -46,34 +42,171 @@
-
-
-
-
-
-
-
+
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ ???
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ ???
+
+
+
+
+
+
+
+
+
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+ if(document.getElementById)
+ for(var i=0;i<document.to_be_deleted.length;i++)
+ Hide(document.getElementById(document.to_be_deleted[i]));
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -123,12 +256,7 @@
-
-
-
-
-
-
+
@@ -144,10 +272,15 @@
+
- "
+
+
+
+
+
:
@@ -155,7 +288,11 @@
- Õ
+
+
+
+
+
:
@@ -166,9 +303,11 @@
(
-
- ®
-
+
+
+
+
+
)
@@ -207,16 +346,21 @@
CASE
OF
-
+
+
|
-
- Þ
+
+
+
+
+
+
+ select="./*[1]"/>
@@ -269,29 +413,329 @@
proves
+
+
+
+ Contradiction.
+
From
we get
- (
+ (
- )
+ )
and
- (
+ (
- )
+ )
- ;
+ ;
hence
+
+
+
+ [
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ ]
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ *
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ *
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ *
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ *
+
+
+
+
+
+
+
+
+
+
+ |
+
+
+ |
+
+
+
+
+
+ |
+
+
+ |
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ [
+
+ ]
+
+
- l
+
+
+
+
+
:
@@ -314,13 +758,18 @@
+
- "
+
+
+
+
+
:
@@ -345,7 +794,11 @@
- Õ
+
+
+
+
+
:
@@ -378,9 +831,11 @@
-
- ®
-
+
+
+
+
+
@@ -461,15 +916,19 @@
>
+
+
+
CASE
OF
-
+
+
-
+
@@ -479,11 +938,34 @@
|
-
- Þ
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -568,20 +1050,78 @@
-
-
-
-
-
-
-
+
+ let
+
+ :=
+
+
-
- we proved
+ in
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ we proved
+
+
+
+
+
@@ -616,9 +1156,9 @@
- (
+ (
- )
+ )
@@ -636,16 +1176,49 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Rewrite
-
- with
-
- by
-
+
+
+
+
+
+
+
+
+ with
+
+
+
+
+
+
+
+
+ by
+
+
+
@@ -659,6 +1232,116 @@
Then apply it to
+
+
+ We prove
+
+
+
+
+
+
+
+ by induction on
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Case
+
+
+
+
+
+
+
+
+ By induction hypothesis, we have:
+
+
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ (
+
+
+
+
+ :
+
+
+ )
+
+
+
+
+
+
+
+
+
+
+
+
+ Contradiction.
+
@@ -681,9 +1364,9 @@
- (
+ (
- )
+ )
@@ -691,9 +1374,9 @@
- (
+ (
- )
+ )
@@ -705,6 +1388,62 @@
+
+
+
+
+
+
+
+
+
+ Consider
+
+
+
+
+
+
+
+ We proceed by cases to prove
+
+
+
+
+
+ Left: suppose
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+
+
+
+ Right: suppose
+ (
+
+ )
+
+
+
+
+
+
+
+
+
@@ -729,7 +1468,7 @@
- *
+ Left:
@@ -737,7 +1476,7 @@
- *
+ Right:
@@ -763,16 +1502,16 @@
Let
- :
+ :
such that
- (
+ (
- )
+ )
@@ -784,6 +1523,299 @@
+
+
+
+
+
+ [
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ ]
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ *
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ *
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ *
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ *
+
+
+
+
+
+
+
+
+
+
+ |
+
+
+ |
+
+
+
+
+
+ |
+
+
+ |
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ [
+
+ ]
+
+
@@ -800,7 +1832,11 @@
- l
+
+
+
+
+
:
@@ -825,12 +1861,7 @@
-
-
-
-
-
-
+
@@ -840,7 +1871,27 @@
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+