X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=86675e553e48abf02c18c78ecf1043341445b65f;hb=083c36a4acd76127530b9af3d4c6c311f447d79b;hp=d467b77af79d18b15e7129e780ba83a35019c703;hpb=fe7df3d309dc0876576773d7c32f91fbc7617d81;p=helm.git diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl index d467b77af..86675e553 100644 --- a/helm/style/mmlextension.xsl +++ b/helm/style/mmlextension.xsl @@ -1,5 +1,29 @@ + + + + + + + + + + + + + + + + + + + + + + + + @@ -295,6 +319,23 @@ + + + + + AS + + + + + + + __ + + + + + @@ -342,6 +383,7 @@ + @@ -349,13 +391,86 @@ + + + + + + + + + + + + + + . + + + + + + + + + + : + + . + + + + + + + + + + + LET + _ + + + + + + + = + + + + + + + + IN + _ + + + + + + + + LET + _ + + = + + _ + IN + _ + + + + - Π + Π @@ -370,7 +485,7 @@ - Π + Π : @@ -386,7 +501,9 @@ - ( + + ( + @@ -394,11 +511,27 @@ - - + + + + + + + + + + + + + + + + + + @@ -406,14 +539,34 @@ + - ( + + ( + - - - ) + + + + + + + + + + + + + + + + + + + ) + @@ -474,7 +627,7 @@ - :> + :> @@ -491,7 +644,7 @@ ( - :> + :> ) @@ -560,7 +713,7 @@ _ - + @@ -571,7 +724,7 @@ |_ - + @@ -601,7 +754,7 @@ - + _ @@ -802,7 +955,7 @@ - we proved + we proved _ @@ -810,6 +963,24 @@ + + + + + + + + + + + + + + + + + + @@ -837,55 +1008,111 @@ ) - + - - + + - Consider - + Consider + _ + - - - - - Rewrite _ - + _ with _ - + _ by _ - - _ - in - _ - - _ - and apply + + + + + + + + + + + + + + + + + Consider + _ + + + + + + + + + + + + + + + + + + + + + + Then apply it to _ - + - + + + + + + + By induction + + + + + + base case: + + + + + + + + inductive case: + + + + + + + @@ -896,7 +1123,8 @@ - Consider + Consider + _ @@ -984,6 +1212,50 @@ + + + + + + + + + + + Consider + _ + + + + + + + + + Let + _ + + : + + _ + such that + _ + ( + + ) + _ + + + + + + + + + + + + ERROR @@ -991,6 +1263,7 @@ + @@ -1055,7 +1328,7 @@ - λ + λ @@ -1070,7 +1343,7 @@ - λ + λ : @@ -1109,9 +1382,7 @@ __ - - = - + = @@ -1375,7 +1646,7 @@ - > + @@ -1387,3 +1658,5 @@ + +