X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fstyle%2Fcontent_to_html.xsl;h=028f65504cfa970ec95bd0e6dfa5f299ad62c784;hb=d4b90e232867dd3cda85b7707ac456b547539a06;hp=5b57eb0ff19859363a9c0d74bf25ee064bed9877;hpb=c539f832ce69f7488e79e80d78c2c5003674dc50;p=helm.git diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl index 5b57eb0ff..028f65504 100644 --- a/helm/style/content_to_html.xsl +++ b/helm/style/content_to_html.xsl @@ -32,27 +32,40 @@ - - - + + + + + + + + - + - - + + + + @@ -67,7 +80,7 @@ -   +   @@ -75,7 +88,6 @@ - @@ -100,8 +112,194 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + " + + : + + . + + + + Õ + + : + + . + + + + + ( + + + ® + + + ) + + + + ( + + +   + + + ) + + + + ( + + :> + + ) + + + Prop + + + Set + + + Type + + + + < + + > + CASE + + OF + + + + | + + + + Þ + + + + + + FIX + + { + + + : + + := + + + + } + + + ; + + + + + + + COFIX + + { + + + : + + := + + + + } + + + ; + + + + + + + +  proves  + + + + + + Contradiction. + + + + From  + +  we get + ( + + )  + +  and  + ( + + )  + + ; +  hence  + + + + + + + l + + : + + . + + + + + + + @@ -114,17 +312,43 @@ - + + - P + " + + : + + + +
+ + + + . + + + + + + + + + + + + + + Õ : -
+ select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/> +
@@ -134,16 +358,11 @@ - - P - - : - - . - + + @@ -151,27 +370,25 @@ -
+
- ® + + ® + ) - ( - - - ® - - ) + + @@ -180,7 +397,7 @@ -
+
@@ -191,13 +408,7 @@ ) - ( - - -   - - - ) + @@ -209,7 +420,7 @@ ( -
+
:> @@ -219,11 +430,7 @@ ) - ( - - :> - - ) + @@ -257,7 +464,7 @@ OF -
+
@@ -270,34 +477,18 @@ - Þ + Þ - < - - > - CASE - - OF - - - - | - - - - Þ - - - - + + @@ -305,7 +496,7 @@ { -
+
@@ -315,7 +506,7 @@ -
+
@@ -324,41 +515,25 @@ -
+
} - FIX - - { - - - : - - := - - - - } - - - ; - - - + + COFIX { -
+
@@ -369,7 +544,7 @@ -
+
@@ -379,36 +554,471 @@ -
+
} - COFIX - - { - - - : - - := - - - - } - - - ; - - - + - - + + + + + + + + +
+ + + + + we proved  + + + + + + + + + +
+ + + + + + + + + + + + + +
+ + + + + + + + + + + ( + + ) + + + + + + + + + + + + + + Consider  + + + + + + + + + + + + + + + + +
+ + + + Rewrite  + +   + +
+ + + + + with  + +   + +
+ + + + + by  + + + + + + + + + +
+ + + + Then apply it to  + + + + + We prove  + + + +
+ + + + by induction on  + + + + + + + + + + + +
+ + + + Case  + + + + +
+ + + + By induction hypothesis, we have: + +
+ + + + ( + + )  + + + + + +
+ + + + + + + + + + + + + + + + ( + + +   + + : + + + ) + + + + + + By induction on  + : +
+ + + + 0  + Þ + + + +
+ + + + S( + + )  + Þ + Assume by induction +
+ + + + ( + + ) + + + +
+ + + + + + + + + + + + +
+ + + + Contradiction. + + + + + + + + + + + Consider  + + + +
+ + + + In particular, we have +
+ + + + ( + + )  + + + +
+ + + + ( + + )  + + + +
+ + + + + + + + + + + + + + + + + Consider  + + + +
+ + + + We proceed by cases to prove  + +
+ + + + Left: suppose  + ( + + )  + +
+ + + + + + +
+ + + + Right: suppose  + ( + + )  + +
+ + + + + + + + + + + + + + + + + Consider  + + + +
+ + + + We prove  + +  by cases: +
+ + + + * + + + +
+ + + + * + + + + + + + + + + + + + + Consider  + + + + + +
+ + + + Let  + + : + +  such that +
+ + + + ( + + ) + + + +
+ + + + + + + + @@ -420,16 +1030,17 @@ + - l + l : -
+ select="$current_indent + 4 + 2*string-length(m:bvar/m:ci)"/> +
@@ -439,13 +1050,7 @@ - - l - - : - - . - + @@ -454,15 +1059,7 @@ - - - - - - + @@ -532,15 +1129,15 @@

-DEFINITION ()
-TYPE =
+DEFINITION ()
+TYPE =
-
-BODY =
+
+BODY =
@@ -555,8 +1152,12 @@ BODY =

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

@@ -567,13 +1168,13 @@ TYPE =

-UNFINISHED PROOF ()
+UNFINISHED PROOF ()
THESIS: -
+
CONJECTURES: -
+
@@ -582,7 +1183,7 @@ CONJECTURES: -
+
PROOF: @@ -620,14 +1221,14 @@ PROOF: - ]
+ ]
OF ARITY -
+
BUILT FROM: -
+
@@ -639,10 +1240,10 @@ PROOF: | - + : - + @@ -654,7 +1255,7 @@ PROOF:

-VARIABLE
+VARIABLE
TYPE =