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

X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fstyle%2Fcontent_to_html.xsl;h=fdf9b7829e3a5970d623ea95ca4f12ed23476849;hb=4668559563eede2f325545a100ff82b774085ed0;hp=cd17b6d4cd45f7c74b243de257ffac390b81cee8;hpb=2e365db5721e934b77f3648ab7df6d31a02142b2;p=helm.git diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl index cd17b6d4c..fdf9b7829 100644 --- a/helm/style/content_to_html.xsl +++ b/helm/style/content_to_html.xsl @@ -29,16 +29,12 @@ - + - - - - -

getciconly?uri=

- -

/apply?keys=&param.keys=&param.getterURL=&param.processorURL=&xmluri=

+ + + @@ -46,30 +42,147 @@ - - - + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ??? + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ??? + + + + + + + + + - - - - - - - - - - + + + + + <xsl:value-of select="$CICURI"/> + + + + + + + + + + + + + + + + + @@ -119,10 +232,7 @@ - - - - +

@@ -141,7 +251,11 @@ - " + + + + +

@@ -149,7 +263,11 @@

- Õ + + + + +

@@ -160,9 +278,11 @@ (

- - ® - + + + + +

)

@@ -201,16 +321,21 @@ CASE

OF - + + | - - Þ + + + + + +

+ select="./*[1]"/>

@@ -263,29 +388,197 @@ proves

+ + + + Contradiction. + From

we get - ( + ( - ) + ) and - ( + ( - ) + ) - ; + ; hence

+ + + + [ + + + + + + + + + + ] + + + + _{+
+} + + + + + + + + ^{+
+} + ( + + ) + + + + + + + + + + + ^{+
+} + ( + + ) + + + + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + | + + | + + + + + + + + + + + + + + + + + + + + [ + + ] + +

- l + + + + +

@@ -314,12 +607,16 @@ - " + + + + +

+ select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>

@@ -339,12 +636,16 @@ - Õ + + + + +

+ select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>

@@ -372,9 +673,11 @@

- - ® - + + + + +

@@ -455,15 +758,19 @@

> +
+ + CASE

OF - + +

- +

@@ -473,11 +780,34 @@ | - - Þ - - - + + + + + + + + + + + +
+ + + + + + + + + + + @@ -562,6 +892,23 @@ + + let + + := + + + +
+ + + + in + + + + + @@ -610,9 +957,9 @@

- ( + ( - ) + )

@@ -630,16 +977,47 @@ + + + + + + + + + + + + +

Rewrite - - with - - by - + + + +
+ + + + + with + + + +
+ + + + + by + + + @@ -653,6 +1031,116 @@ Then apply it to

+ + + We prove + + + +
+ + + + by induction on + + + + + + + + + + + +
+ + + + Case + + + + +
+ + + + By induction hypothesis, we have: + +
+ + + + ( + + ) + + + + + +
+ + + + + + + + + + + + + + + + ( + + + + + : + + + ) + + + + + + + + +
+ + + + Contradiction. + @@ -675,9 +1163,9 @@

- ( + ( - ) + )

@@ -685,9 +1173,9 @@

- ( + ( - ) + )

@@ -699,6 +1187,62 @@ + + + + + + + + + + Consider + + + +
+ + + + We proceed by cases to prove + +
+ + + + Left: suppose + ( + + ) + +
+ + + + + + +
+ + + + Right: suppose + ( + + ) + +
+ + + + + + + @@ -723,7 +1267,7 @@

- * + Left:

@@ -731,7 +1275,7 @@

- * + Right:

@@ -757,16 +1301,16 @@ Let

- : + : such that

- ( + ( - ) + )

@@ -778,6 +1322,167 @@

+ + + + + + [ + + + + + + + + + + ] + + + + _{+
+} + + + + + + + + ^{+
+} + ( + + ) + + + + + + + + + + + ^{+
+} + ( + + ) + + + + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + | + + | + + + + + + + + + + + + + + + + + + + + [ + + ] + +

@@ -794,12 +1499,16 @@ - l + + + + +

+ select="$current_indent + 4 + 2*string-length(m:bvar/m:ci)"/>

@@ -819,10 +1528,7 @@ - - - - +

@@ -1003,10 +1709,10 @@ PROOF: | - + :

- +