tt-conspect icon indicating copy to clipboard operation
tt-conspect copied to clipboard

Published 20 hours ago • verified publisher icon artemohanjanyan

Fix unification

Open artemohanjanyan opened this issue 7 years ago • 0 comments

Substitution definition is wrong, it can't be applied to any function which is not id. E.g. S(x) = {y_1, if x=x_1; x otherwise}, then S(x_1)=y_1, S(x_1->x_1)=y_1->y_1, S(x_1->x_1->x_1)=y_1->y_1->y_1, and so on.

artemohanjanyan avatar Jun 03 '17 11:06 artemohanjanyan