X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=6dce30b65a73b02bf009013469380fd523eb18a0;hb=d4dd07ecc4191d9dac83b5d4d23dfc61c4492d77;hp=a4dfc5f01e7210c6ecc3aca3246cbe4b322c23fb;hpb=ce56bfc29034be5add28ef28007f2598d9030ad2;p=helm.git diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl index a4dfc5f01..6dce30b65 100644 --- a/helm/style/mmlextension.xsl +++ b/helm/style/mmlextension.xsl @@ -44,6 +44,8 @@ which generates the toplevel element (see for instance xlink) --> + + @@ -371,21 +373,27 @@ which generates the toplevel element (see for instance xlink) --> - - : + + + : + + + - - : - + + + : + + @@ -403,10 +411,12 @@ which generates the toplevel element (see for instance xlink) --> - + + + @@ -414,7 +424,7 @@ which generates the toplevel element (see for instance xlink) --> - + @@ -430,7 +440,7 @@ which generates the toplevel element (see for instance xlink) --> - + : @@ -439,6 +449,7 @@ which generates the toplevel element (see for instance xlink) --> + @@ -484,6 +495,7 @@ which generates the toplevel element (see for instance xlink) --> + @@ -516,6 +528,7 @@ which generates the toplevel element (see for instance xlink) --> + @@ -592,6 +605,7 @@ which generates the toplevel element (see for instance xlink) --> + @@ -634,6 +648,7 @@ which generates the toplevel element (see for instance xlink) --> + @@ -672,15 +687,19 @@ which generates the toplevel element (see for instance xlink) --> + Prop + Set + Type + @@ -719,8 +738,8 @@ which generates the toplevel element (see for instance xlink) --> - - + + @@ -733,10 +752,10 @@ which generates the toplevel element (see for instance xlink) --> _ - + - + @@ -747,7 +766,7 @@ which generates the toplevel element (see for instance xlink) --> |_ - + @@ -769,21 +788,22 @@ which generates the toplevel element (see for instance xlink) --> _ OF - + | - + - + _ END + @@ -873,6 +893,7 @@ which generates the toplevel element (see for instance xlink) --> + @@ -965,26 +986,75 @@ which generates the toplevel element (see for instance xlink) --> + - - - - - - - - - - - - we proved - _ - - - - - + + + + + + + + + + We can prove + _ + + + _ + (explain) + + + + + + + + + + + + + + + + + + + + + we proved + _ + + + + _ + + + (hide details) + + + + + + + + + + + + + + + + + + + @@ -1003,6 +1073,140 @@ which generates the toplevel element (see for instance xlink) --> + + + + + + We prove + _ + + + + + + + + by induction on + _ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Case + _ + + + + + + + + _ + + + + + + By induction hypothesis, we have: + + + + + + + _ + + ( + + ) + _ + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + _ + + : + + + ) + + + + + + + + + + + + + + + + + + Contradiction. + + + + + + @@ -1024,12 +1228,14 @@ which generates the toplevel element (see for instance xlink) --> + ( ) + @@ -1090,6 +1296,7 @@ which generates the toplevel element (see for instance xlink) --> --> + @@ -1102,7 +1309,7 @@ which generates the toplevel element (see for instance xlink) --> - Then apply it to + Then apply it to _ @@ -1110,34 +1317,65 @@ which generates the toplevel element (see for instance xlink) --> - - + + - By induction + + + + + + + Consider + _ + + + + - base case: - + In particular, we have - inductive case: + ( + ) + _ + + + + + + + + ( + + ) + _ + + + + + + + + - - + + @@ -1158,41 +1396,56 @@ which generates the toplevel element (see for instance xlink) --> - In particular, we have + We proceed by cases to prove + _ + - ( - - ) + Left: suppose _ - - + ( + + ) + _ + + - ( - - ) _ - - + + - + Right: suppose + _ + ( + + ) + _ + + + + + + + + + @@ -1214,18 +1467,18 @@ which generates the toplevel element (see for instance xlink) --> - We prove + We prove _ _ - by cases: + by cases: - * + Left @@ -1233,13 +1486,14 @@ which generates the toplevel element (see for instance xlink) --> - * + Right + @@ -1267,7 +1521,7 @@ which generates the toplevel element (see for instance xlink) --> : _ - such that + such that _ ( @@ -1286,8 +1540,134 @@ which generates the toplevel element (see for instance xlink) --> + + + + + + + + [ + + + + + + + ] + + + + + + + + + + + + ( + + ) + + + + + + + + + + + + + + ( + + ) + + + + + + + + + + + β + + + + + + + + + + + + β + * + + + + + + + + + + + + β + + + + + + + + + + + + β + * + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - ERROR + ERROR @@ -1318,7 +1698,7 @@ which generates the toplevel element (see for instance xlink) --> - we get + we get _ @@ -1336,7 +1716,7 @@ which generates the toplevel element (see for instance xlink) --> - we get + we get _ @@ -1352,7 +1732,12 @@ which generates the toplevel element (see for instance xlink) --> - + + + + + + @@ -1399,7 +1784,7 @@ which generates the toplevel element (see for instance xlink) --> - + @@ -1417,7 +1802,12 @@ which generates the toplevel element (see for instance xlink) --> __ - = + + + + + + = @@ -1446,43 +1836,43 @@ which generates the toplevel element (see for instance xlink) --> - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -1492,7 +1882,7 @@ which generates the toplevel element (see for instance xlink) --> - + @@ -1510,9 +1900,12 @@ which generates the toplevel element (see for instance xlink) --> __ - - - + + + + + + @@ -1536,9 +1929,12 @@ which generates the toplevel element (see for instance xlink) --> - - - + + + + + + @@ -1552,7 +1948,12 @@ which generates the toplevel element (see for instance xlink) --> - { + + + + + + { @@ -1569,7 +1970,12 @@ which generates the toplevel element (see for instance xlink) --> - } + + + + + + } @@ -1580,7 +1986,12 @@ which generates the toplevel element (see for instance xlink) --> - { + + + + + + { , @@ -1604,7 +2015,12 @@ which generates the toplevel element (see for instance xlink) --> - } + + + + + + } @@ -1631,11 +2047,6 @@ which generates the toplevel element (see for instance xlink) --> - - - - - @@ -1718,6 +2129,3 @@ which generates the toplevel element (see for instance xlink) --> - - -