X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fstyle%2Fcontent_to_html.xsl;h=028f65504cfa970ec95bd0e6dfa5f299ad62c784;hb=0125d0d8d9844a1f0df8df3b21c1ef50e238b7fb;hp=62a4936f0c071e83f6b74fa5da0061a2769a39c3;hpb=f5a06d5c51c59dcfe432a3b4236f0a4189f031f6;p=helm.git
diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index 62a4936f0..028f65504 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -32,28 +32,30 @@
-
-
-
-getciconly?uri=
-
-/apply?key=C1&key=HC2¶m.getterURL=¶m.processorURL=&xmluri=
-
-
-
-
+
+
+
+
+
+
+
+
-
+
@@ -118,10 +120,7 @@
-
-
-
-
+
@@ -256,11 +255,35 @@
+
- we proved
+ proves
+
+
+
+ Contradiction.
+
+
+
+ From
+
+ we get
+ (
+
+ )
+
+ and
+ (
+
+ )
+
+ ;
+ hence
+
+
@@ -299,7 +322,7 @@
:
+ select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
@@ -324,7 +347,7 @@
:
+ select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
@@ -590,9 +613,9 @@
- (
+ (
- )
+ )
@@ -610,16 +633,47 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
Rewrite
-
- with
-
- by
-
+
+
+
+
+
+
+
+
+ with
+
+
+
+
+
+
+
+
+ by
+
+
+
@@ -633,6 +687,156 @@
Then apply it to
+
+
+ We prove
+
+
+
+
+
+
+
+ by induction on
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Case
+
+
+
+
+
+
+
+
+ By induction hypothesis, we have:
+
+
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ (
+
+
+
+
+ :
+
+
+ )
+
+
+
+
+
+ By induction on
+ :
+
+
+
+
+ 0
+ Þ
+
+
+
+
+
+
+
+ S(
+
+ )
+ Þ
+ Assume by induction
+
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Contradiction.
+
@@ -655,9 +859,9 @@
- (
+ (
- )
+ )
@@ -665,9 +869,9 @@
- (
+ (
- )
+ )
@@ -679,6 +883,62 @@
+
+
+
+
+
+
+
+
+
+ Consider
+
+
+
+
+
+
+
+ We proceed by cases to prove
+
+
+
+
+
+ Left: suppose
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+
+
+
+ Right: suppose
+ (
+
+ )
+
+
+
+
+
+
+
+
+
@@ -703,7 +963,7 @@
- *
+ *
@@ -711,7 +971,7 @@
- *
+ *
@@ -737,16 +997,16 @@
Let
- :
+ :
such that
- (
+ (
- )
+ )
@@ -779,7 +1039,7 @@
:
+ select="$current_indent + 4 + 2*string-length(m:bvar/m:ci)"/>
@@ -799,10 +1059,7 @@
-
-
-
-
+
@@ -983,10 +1240,10 @@ PROOF:
|
-
+
:
-
+