X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fstyle%2Fmmlextension.xsl;h=6e66736a32aeb8e1fc866033a8091fc511f028f7;hb=fb158d51c621e55962a6139d03cd1678cfb2e8f1;hp=698e8fce5f9a427cd5d22033960e8370e32447e6;hpb=aa12f8cd84908fb3757a582cadd36ef49e269a2b;p=helm.git diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl index 698e8fce5..6e66736a3 100644 --- a/helm/style/mmlextension.xsl +++ b/helm/style/mmlextension.xsl @@ -1,5 +1,29 @@ + + + + + + + + + + + + + + + + + + + + + + + + @@ -33,7 +57,9 @@ + @@ -295,6 +321,23 @@ + + + + + AS + + + + + + + __ + + + + + @@ -342,6 +385,7 @@ + @@ -355,7 +399,7 @@ - + @@ -370,7 +414,7 @@ - + : @@ -379,13 +423,56 @@ + + + + + + + LET + _ + + + + + + + = + + + + + + + + IN + _ + + + + + + + + LET + _ + + = + + _ + IN + _ + + + + - Π + Π @@ -400,7 +487,7 @@ - Π + Π : @@ -416,7 +503,9 @@ - ( + + ( + @@ -424,11 +513,27 @@ - - + + + + + + + + + + + + + + + + + + @@ -436,14 +541,34 @@ + - ( + + ( + - - - ) + + + + + + + + + + + + + + + + + + + ) + @@ -504,7 +629,7 @@ - :> + :> @@ -521,7 +646,7 @@ ( - :> + :> ) @@ -590,7 +715,7 @@ _ - + @@ -601,7 +726,7 @@ |_ - + @@ -631,7 +756,7 @@ - + _ @@ -832,7 +957,7 @@ - we proved + we proved _ @@ -840,6 +965,24 @@ + + + + + + + + + + + + + + + + + + @@ -867,55 +1010,113 @@ ) - + - - + + - Consider - + Consider + _ + - - - - - Rewrite _ - + _ with _ - + _ by _ - - _ - in - _ - - _ - and apply to + + + + + + + + + + + + + + + + + + + + Then apply it to _ - + - + + + + + + + By induction + + + + + + base case: + + + + + + + + inductive case: + + + + + + + @@ -926,7 +1127,8 @@ - Consider + Consider + _ @@ -1014,6 +1216,50 @@ + + + + + + + + + + + Consider + _ + + + + + + + + + Let + _ + + : + + _ + such that + _ + ( + + ) + _ + + + + + + + + + + + + ERROR @@ -1021,6 +1267,7 @@ + @@ -1085,7 +1332,7 @@ - λ + λ @@ -1100,7 +1347,7 @@ - λ + λ : @@ -1139,9 +1386,7 @@ __ - - = - + = @@ -1405,7 +1650,7 @@ - > + @@ -1417,3 +1662,5 @@ + +