<xsl:value-of select="$CICURI"/>

X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fcontent_to_html.xsl;h=5a48cc1ea49933cc3b3d492a119822d5c07f8353;hb=3f40909b16020098d481eb0c8814c56e26865bf1;hp=32d7a542c2b6b08f1cfbf512fcfe0c5888f5546f;hpb=38d52eb66058f38d4e7afcde55da86f894924378;p=helm.git diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl index 32d7a542c..5a48cc1ea 100644 --- a/helm/style/content_to_html.xsl +++ b/helm/style/content_to_html.xsl @@ -29,18 +29,11 @@ - + - - - - - - -

getxml?uri=

- -

apply?keys=&param.naturalLanguage=&param.annotations=&param.keys=&param.getterURL=&param.processorURL=&xmluri=

+ + @@ -48,11 +41,6 @@ - - - - - @@ -70,22 +58,32 @@ media-type="text/html" doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN" /> - + - - - - - - - - - - + + + + + <xsl:value-of select="$CICURI"/> + + + + + + + + + + + + + + + + + @@ -135,12 +133,7 @@ - - - - - - +

@@ -178,7 +171,7 @@ (

- + ®

@@ -226,7 +219,7 @@

- Þ + Þ

@@ -281,6 +274,11 @@ proves

+ + + + Contradiction. + From @@ -299,6 +297,139 @@ hence

+ + + + [ + + + + ¬ + + + + ] + + + + _{+
+} + + + + + + ^{+
+} + ( + + ) + + + + + + + + + ^{+
+} + ( + + ) + + + + + + + + ® + + _{+
+ b
+
+} + + + + + + + + + ® + + _{+
+ b*
+
+} + + + + + + + + + Þ + + _{+
+ b
+
+} + + + + + + + + + Þ + + _{+
+ b*
+
+} + + + + + + + | + + | + + + + + + + + + + @ + + + + + + + + [ + + ] + +

@@ -390,7 +521,7 @@ - + ®

@@ -473,6 +604,9 @@

> +
+ + CASE

@@ -481,7 +615,7 @@

- +

@@ -492,10 +626,29 @@

- Þ - - - + Þ + + + + + +
+ + + + + + + + + + +

@@ -580,6 +733,23 @@ + + let + + := + + + +
+ + + + in + + + + + @@ -648,16 +818,47 @@ + + + + + + + + + + + + +

Rewrite - - with - - by - + + + +
+ + + + + with + + + +
+ + + + + by + + + @@ -671,6 +872,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. + @@ -717,6 +1068,62 @@ + + + + + + + + + + Consider + + + +
+ + + + We proceed by cases to prove + +
+ + + + Left: suppose + ( + + ) + +
+ + + + + + +
+ + + + Right: suppose + ( + + ) + +
+ + + + + + + @@ -796,6 +1203,141 @@ + + + + + + [ + + + + ¬ + + + + ] + + + + _{+
+} + + + + + + ^{+
+} + ( + + ) + + + + + + + + + ^{+
+} + ( + + ) + + + + + + + + ® + + _{+
+ b
+
+} + + + + + + + + + ® + + _{+
+ b*
+
+} + + + + + + + + + Þ + + _{+
+ b
+
+} + + + + + + + + + Þ + + _{+
+ b*
+
+} + + + + + + + | + + | + + + + + + + + + + @ + + + + + + + + [ + + ] + + @@ -837,12 +1379,7 @@ - - - - - - +