X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=67859db656d243d62babbc0a06ecc6dea80cf792;hb=0125d0d8d9844a1f0df8df3b21c1ef50e238b7fb;hp=698e8fce5f9a427cd5d22033960e8370e32447e6;hpb=aa12f8cd84908fb3757a582cadd36ef49e269a2b;p=helm.git diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl index 698e8fce5..67859db65 100644 --- a/helm/style/mmlextension.xsl +++ b/helm/style/mmlextension.xsl @@ -1,5 +1,29 @@ + + + + + + + + + + + + + + + + + + + + + + + + @@ -13,6 +37,7 @@ xmlns:helm="http://www.cs.unibo.it/helm"> + @@ -33,7 +58,9 @@ + @@ -295,6 +322,23 @@ + + + + + AS + + + + + + + __ + + + + + @@ -342,6 +386,7 @@ + @@ -355,7 +400,7 @@ - + @@ -370,7 +415,7 @@ - + : @@ -379,13 +424,56 @@ + + + + + + + LET + _ + + + + + + + = + + + + + + + + IN + _ + + + + + + + + LET + _ + + = + + _ + IN + _ + + + + - Π + Π @@ -400,7 +488,7 @@ - Π + Π : @@ -416,7 +504,9 @@ - ( + + ( + @@ -424,11 +514,27 @@ - - + + + + + + + + + + + + + + + + + + @@ -436,14 +542,34 @@ + - ( + + ( + - - - ) + + + + + + + + + + + + + + + + + + + ) + @@ -504,7 +630,7 @@ - :> + :> @@ -521,7 +647,7 @@ ( - :> + :> ) @@ -590,7 +716,7 @@ _ - + @@ -601,7 +727,7 @@ |_ - + @@ -631,7 +757,7 @@ - + _ @@ -832,7 +958,7 @@ - we proved + we proved _ @@ -840,6 +966,24 @@ + + + + + + + + + + + + + + + + + + @@ -867,55 +1011,113 @@ ) - + - - + + - Consider - + Consider + _ + - - - - - Rewrite _ - + _ with _ - + _ by _ - - _ - in - _ - - _ - and apply to + + + + + + + + + + + + + + + + + + + + Then apply it to _ - + - + + + + + + + By induction + + + + + + base case: + + + + + + + + inductive case: + + + + + + + @@ -926,7 +1128,8 @@ - Consider + Consider + _ @@ -1014,6 +1217,50 @@ + + + + + + + + + + + Consider + _ + + + + + + + + + Let + _ + + : + + _ + such that + _ + ( + + ) + _ + + + + + + + + + + + + ERROR @@ -1021,6 +1268,7 @@ + @@ -1085,7 +1333,7 @@ - λ + λ @@ -1100,7 +1348,7 @@ - λ + λ : @@ -1139,9 +1387,7 @@ __ - - = - + = @@ -1405,7 +1651,7 @@ - > + @@ -1417,3 +1663,5 @@ + +