<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=1a66b86dd489cf8280e0d4a870afcf4abdec3717;hb=7ff85e55518d06d96b9abbea4aa68d83e6be35b0;hp=dd1c0779482e712b80130c6f8807266e823ab1ea;hpb=aa87f28d3a96456e7cec9493c6533e5c146812e8;p=helm.git diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl index dd1c07794..1a66b86dd 100644 --- a/helm/style/content_to_html.xsl +++ b/helm/style/content_to_html.xsl @@ -1,43 +1,224 @@ + + + + + + + + + + + + + + + + + + + + + + + + - + + + + - - - - - - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ??? + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ??? + + + + + + + + + - - - - - - - - + + + + + <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])); + + + + + + + + + + + + + + + @@ -46,8 +227,14 @@ + - +

@@ -55,7 +242,6 @@ -

@@ -80,8 +266,563 @@

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

+ + + + + + + + + + : + + . + + + + + + + + + + : + + . + + + + + ( + + + + + + + + ) + + + + ( + + + + + + + + ) + + + + ( + + + + + + + + ) + + + + ( + + + + + + ) + + + + ( + + : + + ) + + + Prop + + + Set + + + Type + + + + < + + > + CASE + + OF + + + + + | + + + + + + + + + + + + + + + { + + + / + + + + + + + + } + + + + + FIX + + { + + + : + + := + + + + } + + + ; + + + + + + + COFIX + + { + + + : + + := + + + + } + + + ; + + + + + + + if + + then + + else + + + + + + proves + + + which is equivalent to + + + + + + letin1 (inline error) + + + + + Contradiction. + + + + From + + we get + ( + + ) + + and + ( + + ) + + ; + hence + + + + + + [ + + + + + + + + + + + + + + + + + + + + + ] + + + + _{+
+} + + + + + + + + + + + + + + + + + + + ^{+
+} + ( + + ) + + + + + + + + + + + + + + + + + + + + + + ^{+
+} + ( + + ) + + + + + + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + + | + + + | + + + + + + | + + + | + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + [ + + ] + + + + + + + + + + + + + : + + . + + + + + + + @@ -93,18 +834,57 @@ +

- + + + + + + - P + + + + + + + : + + + +
+ + + + . + + + + + + + + + + + + + + + + + +

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

@@ -114,281 +894,1223 @@ - - P - - : - - . - + + + + + + + + + ( + + + +
+ + + + + + + + + + + + + ) + + + + + + + + + + + ( + + + +
+ + + + + + + + + + + + + ) + + + + + + + + + + + ( + + + +
+ + + + + + + + + + + + + ) + + + + + + + + + + + ( + + + + +
+ + + + + + + + ) + + + + + + + + + + + + ( + + +
+ + + :> + + + + ) + + + + + + + + + + + + + + + Prop + + + Set + + + Type + + + + + < + + + + > +
+ + + CASE + + + + OF + + +
+ + + + + + + + + | + + + + + + + + + + + + + +
+ + + + + + + + + + + + + + + + + + + + + + + FIX + + { + +
+ + + + + : + + + +
+ + + + := + + + + +
+ + + + } + + + + + + + + + + + COFIX + + { +
+ + + + + + : + + + +
+ + + + := + + + + + +
+ + + + } + + + + + + + + let + + := + + + +
+ + + + in + + + + + + + if + + + +
+ + + + then + + + +
+ + + + else + + + + + + + + + + + + + + + + + + + + +
+ + + + we proved + + + +
+ + + + and by delta equivalence + + + + + + + +
+ + + + we proved + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + We have the following equality chain: + + +
+ + + + + + + + + = + + + = + + + + + + +
+ + + + + + + + + + + + We have the following chain of disequalities: + + +
+ + + + + + + + + + + + + + + + + + + + +
+ + + + + + + + + + + + + + +
+ + + + + + + + + + + + + +
+ + + + + + + + + + + ( + + ) + + + + + + + + + + + + + + Consider + + + + + + + + + + + + + + + + + + +
+ + + + Rewrite + + + +
+ + + + + with + + + +
+ + + + + by + + + + + + + + + +
+ + + + Then apply it to + + + + + We prove + + + +
+ + + + by induction on + + + + + + + + + + + +
+ + + + Case + + + + +
+ + + + By induction hypothesis, we have: + +
+ + + + ( + + ) + + + + + +
+ + + + + + + + + + + + + + + + ( + + + + + : + + + ) + + + + + + + + +
+ + + + Contradiction. + + + + + + + + + + + Consider + + + +
+ + + + In particular, we have +
+ + + + ( + + ) + + + +
+ + + + ( + + ) + + + +
+ + + + + + + + + + + + + + + + + Consider + + + +
+ + + + We proceed by cases to prove + +
+ + + + Left: suppose + ( + + ) + +
+ + + + + + +
+ + + + Right: suppose + ( + + ) + +
+ + + + + + + + + + + + + + + + + Consider + + + +
+ + + + We prove + + by cases: +
+ + + + Left: + + + +
+ + + + Right: + + + + + + + + + + + + + + Consider + + + + + +
+ + + + Let + + : + + such that +
+ + + + ( + + ) + + + +
+ + + + + + + + + + + + + [ + + + + + + + + + + + + + + + + + + + ] - + + + _{+
+} - + + + + + + + + + + + + + + + + + + ^{+
+} ( - - - -
- - - - - ® - - - + ) + + + + + + + + + + + + - ( - - - ® - - ) + + + + + + ^{+
+} + ( + + ) - + + + + - - ( - - - - -
- - - - - - - - ) + + + + + + + + _{+
+
+
+
+
+} + - ( - - - - - - ) + + + + + + _{+
+
+
+
+
+} + - + + + - - - - ( - - -
- - - :> - - - - ) - - - ( - - :> - - ) - - - - - - - - + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + _{+
+
+
+
+
+ *
+} + + - - Prop - - - Set - - - Type + + + + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + _{+
+
+
+
+
+} + + + - + + + - - < - - - - > - CASE - - - - OF - -
- - - - - - - - - | - - - - Þ - - - - + + + + + + + + _{+
+
+
+
+
+ *
+} + - < - - > - CASE - - OF - - - - | - - - - Þ - - - - + + + + + + _{+
+
+
+
+
+ *
+} + - + + + - - FIX - - { - -
- - - - - : - - - -
- - - - := - - - - -
- - - - } + + | - FIX - - { - - - : - - := - - - - } - - - ; - - - + | - - + - - COFIX - - { -
- - - - - - : - - - -
- - - - := - - - + + | + + + | + + + - -
- - - - } + + + + + + + + + + + + + + - COFIX - - { - - - : - - := - - - - } - - - ; - - - + + + + + + - - + + + + [ + + ] + + + @@ -400,16 +2122,21 @@ + - l + + + + +

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

@@ -419,13 +2146,7 @@ - - l - - : - - . - + @@ -434,15 +2155,7 @@ - - - - - - +

@@ -452,7 +2165,27 @@ - + + + + + + + + + + + + + + + + + + + + + @@ -512,15 +2245,15 @@

-DEFINITION ()
-TYPE =
+DEFINITION ()
+TYPE =
-
-BODY =
+
+BODY =
@@ -535,8 +2268,12 @@ BODY =

-AXIOM ()
-TYPE = +AXIOM ()
+TYPE =
+ + + +

@@ -547,22 +2284,57 @@ TYPE =

-UNFINISHED PROOF ()
+UNFINISHED PROOF ()
THESIS: -
+
CONJECTURES: -
+
- : - + + + + + + + + + _ + + + : + + + + + + + + + + + _ + + + := + + + + + + _ :? _ + + + + |- : + -
+
PROOF: @@ -600,14 +2372,14 @@ PROOF: - ]
+ ]
OF ARITY -
+
BUILT FROM: -
+
@@ -619,10 +2391,10 @@ PROOF: | - + : - + @@ -634,10 +2406,16 @@ PROOF:

-VARIABLE
+VARIABLE
TYPE = + +
+BODY = + + +