X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fstyle%2Fmmlextension.xsl;h=86675e553e48abf02c18c78ecf1043341445b65f;hb=083c36a4acd76127530b9af3d4c6c311f447d79b;hp=90f8cca103d34b091ebb4af014c0c21b1f953857;hpb=c539f832ce69f7488e79e80d78c2c5003674dc50;p=helm.git diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl index 90f8cca10..86675e553 100644 --- a/helm/style/mmlextension.xsl +++ b/helm/style/mmlextension.xsl @@ -963,6 +963,24 @@ + + + + + + + + + + + + + + + + + + @@ -990,55 +1008,111 @@ ) - + - - + + - Consider - + Consider + _ + - - - - - Rewrite _ - + _ with _ - + _ by _ - - _ - in - _ - - _ - and apply to + + + + + + + + + + + + + + + + + Consider + _ + + + + + + + + + + + + + + + + + + + + + + Then apply it to _ - + - + + + + + + + By induction + + + + + + base case: + + + + + + + + inductive case: + + + + + + + @@ -1049,7 +1123,8 @@ - Consider + Consider + _ @@ -1147,7 +1222,8 @@ - Consider + Consider + _ @@ -1187,6 +1263,7 @@ +