<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=856fd69718a66103a38e43811ee1b836de23fc0c;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=d352da2a9a6d713dbc99819d8b68a1e15519a968;hpb=f079a5948394ada2f2aba69270869058111bb3fe;p=helm.git diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl index d352da2a9..856fd6971 100644 --- a/helm/style/content_to_html.xsl +++ b/helm/style/content_to_html.xsl @@ -29,39 +29,184 @@ - + + + + - - - - - - + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ??? + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ??? + + + + + + + + + - - - - - - - - + + + + + <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])); + + + + + + + + + + + + + + + @@ -71,7 +216,7 @@ - +

@@ -79,7 +224,6 @@ -

@@ -104,8 +248,513 @@

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

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

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

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

@@ -138,16 +822,11 @@ - - P - - : - - . - + + @@ -155,27 +834,27 @@

-
+

- ® + + + + +

) - ( - - - ® - - ) + + @@ -184,7 +863,7 @@

-
+

@@ -195,13 +874,7 @@ )

- ( - - - - - - ) + @@ -213,7 +886,7 @@ (

:> @@ -223,11 +896,7 @@ ) - ( - - :> - - ) + @@ -255,15 +924,19 @@ > +
+ + CASE

OF - -
+ + +

- +

@@ -273,35 +946,42 @@ | - - Þ - - - + + + + + + + + + + + +
+ + + + + + + + + + + - < - - > - CASE - - OF - - - - | - - - - Þ - - - - + + @@ -309,7 +989,7 @@ { -
+

@@ -319,7 +999,7 @@ -
+

@@ -328,41 +1008,25 @@ -
+

} - FIX - - { - - - : - - := - - - - } - - - ; - - - + + COFIX

{ -
+

@@ -373,7 +1037,7 @@ -
+

@@ -383,57 +1047,927 @@

-
+

} - COFIX - - { - - - : - - := - - - - } - - - ; - - - + - - - - - - - + + let + + := + + + +
+ + + + in + + + + + + + + + + + + + + + + + + + + + + +
+ + + + 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 +
+ + + + ( + + ) + + + +
+ + + + + + + + + + + + + [ + + + + + + + + + + + + + + + + + + + + + ] + + + + _{+
+} + + + + + + + + + + + + + + + + + + + ^{+
+} + ( + + ) + + + + + + + + + + + + + + + + + + + + + + ^{+
+} + ( + + ) + + + + + + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + _{+
+
+
+
+
+} + + + + + + + + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + _{+
+
+
+
+
+ *
+} + + + + + + + + + + | + + + | + + + + + + | + + + | + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + [ + + ] + + + + + + + +

+ - l + + + + +

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

@@ -443,13 +1977,7 @@ - - l - - : - - . - + @@ -458,15 +1986,7 @@ - - - - - - +

@@ -476,7 +1996,27 @@ - + + + + + + + + + + + + + + + + + + + + + @@ -536,15 +2076,15 @@

-DEFINITION ()
-TYPE =
+DEFINITION ()
+TYPE =
-
-BODY =
+
+BODY =
@@ -559,8 +2099,12 @@ BODY =

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

@@ -571,22 +2115,57 @@ TYPE =

-UNFINISHED PROOF ()
+UNFINISHED PROOF ()
THESIS: -
+
CONJECTURES: -
+
- : - + + + + + + + + + _ + + + : + + + + + + + + + + + _ + + + := + + + + + + _ :? _ + + + + |- : + -
+
PROOF: @@ -624,14 +2203,14 @@ PROOF: - ]
+ ]
OF ARITY -
+
BUILT FROM: -
+
@@ -643,10 +2222,10 @@ PROOF: | - + : - + @@ -658,10 +2237,16 @@ PROOF:

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