X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=6e66736a32aeb8e1fc866033a8091fc511f028f7;hb=fb158d51c621e55962a6139d03cd1678cfb2e8f1;hp=d467b77af79d18b15e7129e780ba83a35019c703;hpb=fe7df3d309dc0876576773d7c32f91fbc7617d81;p=helm.git diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl index d467b77af..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 @@ + @@ -349,13 +393,86 @@ + + + + + + + + + + + + + + . + + + + + + + + + + : + + . + + + + + + + + + + + LET + _ + + + + + + + = + + + + + + + + IN + _ + + + + + + + + LET + _ + + = + + _ + IN + _ + + + + - Π + Π @@ -370,7 +487,7 @@ - Π + Π : @@ -386,7 +503,9 @@ - ( + + ( + @@ -394,11 +513,27 @@ - - + + + + + + + + + + + + + + + + + + @@ -406,14 +541,34 @@ + - ( + + ( + - - - ) + + + + + + + + + + + + + + + + + + + ) + @@ -474,7 +629,7 @@ - :> + :> @@ -491,7 +646,7 @@ ( - :> + :> ) @@ -560,7 +715,7 @@ _ - + @@ -571,7 +726,7 @@ |_ - + @@ -601,7 +756,7 @@ - + _ @@ -802,7 +957,7 @@ - we proved + we proved _ @@ -810,6 +965,24 @@ + + + + + + + + + + + + + + + + + + @@ -837,55 +1010,113 @@ ) - + - - + + - Consider - + Consider + _ + - - - - - Rewrite _ - + _ with _ - + _ by _ - - _ - in - _ - - _ - and apply + + + + + + + + + + + + + + + + + + + + Then apply it to _ - + - + + + + + + + By induction + + + + + + base case: + + + + + + + + inductive case: + + + + + + + @@ -896,7 +1127,8 @@ - Consider + Consider + _ @@ -984,6 +1216,50 @@ + + + + + + + + + + + Consider + _ + + + + + + + + + Let + _ + + : + + _ + such that + _ + ( + + ) + _ + + + + + + + + + + + + ERROR @@ -991,6 +1267,7 @@ + @@ -1055,7 +1332,7 @@ - λ + λ @@ -1070,7 +1347,7 @@ - λ + λ : @@ -1109,9 +1386,7 @@ __ - - = - + = @@ -1375,7 +1650,7 @@ - > + @@ -1387,3 +1662,5 @@ + +