<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=5ffa0742ab22e605089eb9ccddfc98b84e10c463;hb=9615625bcabfb81bda129ee14c3bf396ba761416;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..5ffa0742a 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,171 @@ - - - + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ??? + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ??? + + + + + + + + + - - - - - - - - - - + + + + + <xsl:value-of select="$CICURI"/> + + + + + + if(document.getElementById) + for(var i=0;i<document.to_be_deleted.length;i++) + Hide(document.getElementById(document.to_be_deleted[i])); + + + + + + + + + + + + + + + @@ -119,10 +256,7 @@ - - - - +

@@ -138,10 +272,15 @@

- " + + + + +

@@ -149,7 +288,11 @@

- Õ + + + + +

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

- - ® - + + + + +

)

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

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

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

@@ -258,34 +408,337 @@ - +

proves

+ + letin1 (inline error) + + + + + Contradiction. + From

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

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

@@ -308,18 +761,23 @@

- " + + + + +

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

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

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

@@ -372,9 +834,11 @@

- - ® - + + + + +

@@ -455,15 +919,19 @@

> +
+ + CASE

OF - + +

- +

@@ -473,11 +941,34 @@ | - - Þ - - - + + + + + + + + + + + +
+ + + + + + + + + + + @@ -562,24 +1053,199 @@ - - - - - - - + + let + + := + +
-

- we proved + in + + + + + + + + + + + + + + + + + + + + + + +
+ + + + we proved + + + + +

+ + + + + + + + + + + + + + + + + + + + + + + We have the following equality chain: + + +
+ + + + + + + + + = + + + = + + + + + + +
+ + + + + + + + + + + + We have the following chain of disequalities: + + +
+ + + + + + + + + + + + + + + + + + + + +
+ + + + + + + + +

@@ -610,9 +1276,9 @@

- ( + ( - ) + )

@@ -630,16 +1296,49 @@

+ + + + + + + + + + + + + + +

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

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

- ( + ( - ) + )

@@ -685,9 +1494,9 @@

- ( + ( - ) + )

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

- * + Left:

@@ -731,7 +1596,7 @@

- * + Right:

@@ -757,16 +1622,16 @@ Let

- : + : such that

- ( + ( - ) + )

@@ -778,6 +1643,299 @@

+ + + + + + [ + + + + + + + + + + + + + + + + + + + + + ] + + + + _{+
+} + + + + + + + + + + + + + + + + + + + ^{+
+} + ( + + ) + + + + + + + + + + + + + + + + + + + + + + ^{+
+} + ( + + ) + + + + + + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + + | + + + | + + + + + + | + + + | + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + [ + + ] + + @@ -794,12 +1952,16 @@ - l + + + + +

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

@@ -819,10 +1981,7 @@ - - - - +

@@ -832,7 +1991,27 @@ - + + + + + + + + + + + + + + + + + + + + + @@ -1003,10 +2182,10 @@ PROOF: |

- + : - + @@ -1022,6 +2201,12 @@ VARIABLE
TYPE =

+ +
+BODY = + + +