X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=86675e553e48abf02c18c78ecf1043341445b65f;hb=c1dfb763206c3e548b26d1e5f2128c6938a5df14;hp=e130b4fb6aff8fceeaf5436ebcf3cb8410a61066;hpb=8e1a7e55cbc7750446f0a7ab3d071190594243fb;p=helm.git diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl index e130b4fb6..86675e553 100644 --- a/helm/style/mmlextension.xsl +++ b/helm/style/mmlextension.xsl @@ -319,6 +319,23 @@ + + + + + AS + + + + + + + __ + + + + + @@ -366,6 +383,7 @@ + @@ -379,7 +397,7 @@ - + @@ -394,7 +412,7 @@ - + : @@ -403,13 +421,56 @@ + + + + + + + LET + _ + + + + + + + = + + + + + + + + IN + _ + + + + + + + + LET + _ + + = + + _ + IN + _ + + + + - Π + Π @@ -424,7 +485,7 @@ - Π + Π : @@ -440,7 +501,9 @@ - ( + + ( + @@ -448,11 +511,27 @@ - - + + + + + + + + + + + + + + + + + + @@ -460,14 +539,34 @@ + - ( + + ( + - - - ) + + + + + + + + + + + + + + + + + + + ) + @@ -528,7 +627,7 @@ - :> + :> @@ -545,7 +644,7 @@ ( - :> + :> ) @@ -614,7 +713,7 @@ _ - + @@ -625,7 +724,7 @@ |_ - + @@ -655,7 +754,7 @@ - + _ @@ -856,7 +955,7 @@ - we proved + we proved _ @@ -864,6 +963,24 @@ + + + + + + + + + + + + + + + + + + @@ -891,55 +1008,111 @@ ) - + - - + + - Consider - + Consider + _ + - - - - - Rewrite _ - + _ with _ - + _ by _ - - _ - in - _ - - _ - and apply to + + + + + + + + + + + + + + + + + Consider + _ + + + + + + + + + + + + + + + + + + + + + + Then apply it to _ - + - + + + + + + + By induction + + + + + + base case: + + + + + + + + inductive case: + + + + + + + @@ -950,7 +1123,8 @@ - Consider + Consider + _ @@ -1038,6 +1212,50 @@ + + + + + + + + + + + Consider + _ + + + + + + + + + Let + _ + + : + + _ + such that + _ + ( + + ) + _ + + + + + + + + + + + + ERROR @@ -1045,6 +1263,7 @@ + @@ -1109,7 +1328,7 @@ - λ + λ @@ -1124,7 +1343,7 @@ - λ + λ : @@ -1163,9 +1382,7 @@ __ - - = - + = @@ -1429,7 +1646,7 @@ - > + @@ -1441,3 +1658,5 @@ + +