X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fstyle%2Fcontent_to_html.xsl;h=856fd69718a66103a38e43811ee1b836de23fc0c;hb=bf6bbd9f2e47ce7a465c0bb3105f9a7c7d73a9ea;hp=8da220b070e3d0e810c1cb1b8225adcfb40eaab3;hpb=3fd609889e80b83cf1f3419dcfa3fc34b41a86ad;p=helm.git
diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index 8da220b07..856fd6971 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -29,15 +29,12 @@
-
+
-
-
-
-getciconly?uri=
-
-/apply?key=C1&key=HC2¶m.getterURL=¶m.processorURL=&xmluri=
+
+
+
@@ -45,30 +42,171 @@
-
-
-
+
+
+
+
+
+
+
+
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ ???
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ ???
+
+
+
+
+
+
+
+
+
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+ if(document.getElementById)
+ for(var i=0;i<document.to_be_deleted.length;i++)
+ Hide(document.getElementById(document.to_be_deleted[i]));
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -118,10 +256,7 @@
-
-
-
-
+
@@ -137,10 +272,15 @@
+
- "
+
+
+
+
+
:
@@ -148,7 +288,11 @@
- Õ
+
+
+
+
+
:
@@ -159,9 +303,11 @@
(
-
- ®
-
+
+
+
+
+
)
@@ -200,16 +346,21 @@
CASE
OF
-
+
+
|
-
- Þ
+
+
+
+
+
+
+ select="./*[1]"/>
@@ -256,35 +407,343 @@
-
-
+
+
proves
+
+ which is equivalent to
+
+
+
+
+
+ letin1 (inline error)
+
+
+
+
+ Contradiction.
From
we get
- (
+ (
- )
+ )
and
- (
+ (
- )
+ )
- ;
+ ;
hence
+
+
+
+ [
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ ]
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ *
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ *
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ *
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ *
+
+
+
+
+
+
+
+
+
+
+ |
+
+
+ |
+
+
+
+
+
+ |
+
+
+ |
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ [
+
+ ]
+
+
- l
+
+
+
+
+
:
@@ -307,18 +766,23 @@
+
- "
+
+
+
+
+
:
+ select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
@@ -338,12 +802,16 @@
- Õ
+
+
+
+
+
:
+ select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
@@ -371,9 +839,11 @@
-
- ®
-
+
+
+
+
+
@@ -454,15 +924,19 @@
>
+
+
+
CASE
OF
-
+
+
-
+
@@ -472,11 +946,34 @@
|
-
- Þ
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -561,24 +1058,199 @@
-
-
-
-
-
-
-
+
+ let
+
+ :=
+
+
-
- we proved
+ in
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ we proved
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ We have the following equality chain:
+
+
+
+
+
+
+
+
+
+
+
+ =
+
+
+ =
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ We have the following chain of disequalities:
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -609,9 +1281,9 @@
- (
+ (
- )
+ )
@@ -629,16 +1301,49 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Rewrite
-
- with
-
- by
-
+
+
+
+
+
+
+
+
+ with
+
+
+
+
+
+
+
+
+ by
+
+
+
@@ -652,6 +1357,116 @@
Then apply it to
+
+
+ We prove
+
+
+
+
+
+
+
+ by induction on
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Case
+
+
+
+
+
+
+
+
+ By induction hypothesis, we have:
+
+
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ (
+
+
+
+
+ :
+
+
+ )
+
+
+
+
+
+
+
+
+
+
+
+
+ Contradiction.
+
@@ -674,9 +1489,9 @@
- (
+ (
- )
+ )
@@ -684,9 +1499,9 @@
- (
+ (
- )
+ )
@@ -698,6 +1513,62 @@
+
+
+
+
+
+
+
+
+
+ Consider
+
+
+
+
+
+
+
+ We proceed by cases to prove
+
+
+
+
+
+ Left: suppose
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+
+
+
+ Right: suppose
+ (
+
+ )
+
+
+
+
+
+
+
+
+
@@ -722,7 +1593,7 @@
- *
+ Left:
@@ -730,7 +1601,7 @@
- *
+ Right:
@@ -756,16 +1627,16 @@
Let
- :
+ :
such that
- (
+ (
- )
+ )
@@ -777,6 +1648,299 @@
+
+
+
+
+
+ [
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ ]
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ *
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ *
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ *
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ *
+
+
+
+
+
+
+
+
+
+
+ |
+
+
+ |
+
+
+
+
+
+ |
+
+
+ |
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ [
+
+ ]
+
+
@@ -793,12 +1957,16 @@
- l
+
+
+
+
+
:
+ select="$current_indent + 4 + 2*string-length(m:bvar/m:ci)"/>
@@ -818,10 +1986,7 @@
-
-
-
-
+
@@ -831,7 +1996,27 @@
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -940,8 +2125,43 @@ CONJECTURES:
- :
-
+
+
+
+
+
+
+
+
+ _
+
+
+ :
+
+
+
+
+
+
+
+
+
+
+ _
+
+
+ :=
+
+
+
+
+
+ _ :? _
+
+
+
+ |- :
+
@@ -1002,10 +2222,10 @@ PROOF:
|
-
+
:
-
+
@@ -1021,6 +2241,12 @@ VARIABLE
TYPE =
+
+
+BODY =
+
+
+