X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fcontent_to_html.xsl;h=028f65504cfa970ec95bd0e6dfa5f299ad62c784;hb=d4b90e232867dd3cda85b7707ac456b547539a06;hp=9de7d48962cfe82ab3522e65dfd56f9db15cd66b;hpb=21cff2a40a629fd6543403f61ef8da0591711cf9;p=helm.git
diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index 9de7d4896..028f65504 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -55,7 +55,7 @@
media-type="text/html"
doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN" />
-
+
@@ -261,6 +261,11 @@
proves
+
+
+
+ Contradiction.
+
From
@@ -628,16 +633,47 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
Rewrite
-
- with
-
- by
-
+
+
+
+
+
+
+
+
+ with
+
+
+
+
+
+
+
+
+ by
+
+
+
@@ -651,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.
+
@@ -697,6 +883,62 @@
+
+
+
+
+
+
+
+
+
+ Consider
+
+
+
+
+
+
+
+ We proceed by cases to prove
+
+
+
+
+
+ Left: suppose
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+
+
+
+ Right: suppose
+ (
+
+ )
+
+
+
+
+
+
+
+
+