X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=4a801a65402c244e03bbe273c6a4d7a7ba1709a3;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=67859db656d243d62babbc0a06ecc6dea80cf792;hpb=98bebe823e0b925f5b4bd3b0c70f1a966ae12758;p=helm.git diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl index 67859db65..4a801a654 100644 --- a/helm/style/mmlextension.xsl +++ b/helm/style/mmlextension.xsl @@ -32,13 +32,22 @@ + + xmlns:helm="http://www.cs.unibo.it/helm" + xmlns:xlink="http://www.w3.org/1999/xlink"> + + + + - + + + @@ -57,11 +66,19 @@ + + - - + + + + + + + + + + @@ -164,10 +181,54 @@ - + __ - : - + + + + + + + + + + _ + + + : + + + + + + + + + + + _ + + + := + + + + + + _ + :? + _ + + + + + ; + + + |- + ? + : + @@ -175,7 +236,7 @@ - CORRESPONDING PROOF: + PROOF: @@ -343,6 +404,61 @@ + + + + + + + none + + + solid + + + + ? + : + _ + + + + + + + + + : + + + := + + + + + + + + + + + + _ + + + + + + + + + + + + + + + @@ -358,21 +474,27 @@ - - : + + + : + + + - - : - + + + : + + @@ -390,18 +512,31 @@ - - + + + + + + + + + + + + + - + + + @@ -415,7 +550,7 @@ - + : @@ -424,15 +559,18 @@ + + LET _ + @@ -467,14 +605,17 @@ + + Π + @@ -497,6 +638,7 @@ + @@ -573,6 +715,7 @@ + @@ -581,7 +724,10 @@ ( - + + + + @@ -590,7 +736,10 @@ ( - + + + + @@ -606,15 +755,22 @@ ( - + + + + _ - + + + + ) + @@ -653,15 +809,19 @@ + Prop + Set + Type + @@ -700,8 +860,8 @@ - - + + @@ -714,10 +874,10 @@ _ - + - + @@ -728,7 +888,7 @@ |_ - + @@ -750,21 +910,22 @@ _ OF - + | - + - + _ END + @@ -854,6 +1015,7 @@ + @@ -946,7 +1108,178 @@ + + + + + + + + + + + We can prove + _ + + + + + _ + (explain) + + + + + + + + + + + + + + + + + + + + + _ + + + (hide details) + + + + + + + we proved + _ + + + + + + + + + + + + that is equivalent to + _ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + We can prove + _ + + + + + _ + (explain) + + + + + + + + + + + + + + + + + + + + + _ + + + (hide details) + + + + + + + we proved + _ + + + + + + + + + + + + that is equivalent to + _ + + + + + + + + + + + + + + + + + + + + + + @@ -958,32 +1291,146 @@ - we proved - _ - - - - - - - - - - - - - - - - - + + + + + + We prove + _ + + + + + + + + by induction on + _ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Case + _ + + + + + + + + _ + + + + + + By induction hypothesis, we have: + + + + + + + _ + + ( + + ) + _ + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + _ + + : + + + ) + + + + + + + + + + + + + + + + + + Contradiction. + + + + + @@ -1005,12 +1452,14 @@ + ( ) + @@ -1071,6 +1520,7 @@ --> + @@ -1083,7 +1533,7 @@ - Then apply it to + Then apply it to _ @@ -1091,34 +1541,65 @@ - - + + - By induction + + + + + + + Consider + _ + + + + - base case: - + In particular, we have - inductive case: + ( + ) + _ + + + + + + + + ( + + ) + _ + + + + + + + + - - + + @@ -1138,40 +1619,57 @@ - In particular, we have + + We proceed by cases to prove + _ + + - ( - - ) + Left: suppose _ - - + ( + + ) + _ + + - ( - - ) _ - - + + - + Right: suppose + _ + ( + + ) + _ + + + + + + + + + @@ -1192,17 +1690,19 @@ - We prove - _ - - _ - by cases: + + We prove + _ + + _ + by cases: + - * + Left @@ -1210,13 +1710,14 @@ - * + Right + @@ -1237,19 +1738,21 @@ - Let - _ - - : - - _ - such that - _ - ( - - ) - _ - + + Let + _ + + : + + _ + such that + _ + ( + + ) + _ + + @@ -1261,8 +1764,220 @@ + + + + + + + We have the following equality chain: + + + + + + + + + + + + _ + = + + + = + _ + + + + + + + + + + + __ + + + + + + + + + + + + + + + We have the following disequality chain: + + + + + + + + + + + + _ + + + + + _ + + + + + + + + + + + __ + + + + + + + + + + + + + + + + [ + + + + + + + ] + + + + + + + + + + + + ( + + ) + + + + + + + + + + + + + + ( + + ) + + + + + + + + + + + β + + + + + + + + + + + + β + * + + + + + + + + + + + + β + + + + + + + + + + + + β + * + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - ERROR + ERROR @@ -1293,7 +2008,7 @@ - we get + we get _ @@ -1311,7 +2026,7 @@ - we get + we get _ @@ -1327,14 +2042,21 @@ - + + + + + + + λ + @@ -1359,227 +2081,6 @@ - - - - - - - - - - - - - - - - - - - - - ( - - - - - - - __ - = - - - - - - - ) - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ( - - - - - - - __ - - - - - - - - - - ) - - - - - - - - - - - - - - - - - - - - - - - - - - - - - { - - - - - - { - | - - - - - - } - - - - - - - - - { - - - , - - - - - - - { - - - , - - - - - - - } - - - - - - - - - - - - - - - - | - - | - - - - - - - @@ -1637,7 +2138,16 @@ - + + + + + + + + + + @@ -1663,5 +2173,3 @@ - -