\e 1
."\\"

/ unify $[fail;fail;list;$[eqheads;unify;fail];eqobj;cont;notvar;fail;free;bind;bound;cont;fail]
u:{$[x~();x;~@y;$[(*y)~*z;u/[x;y;z];()];y~z;x;~y in!x;();y~a:x y;@[x;y;:;z];a~z;x;()]}

/ normalize ["vars";rules;expr]
n:{{$[@z;z;.z.s[x;y]'k[x;y]z]}[x!x;y]/z}
k:{$[#i:&0<#:'s:u[x;;z]'*y;a[x[];s@*i]y[1;*i];z]}
a:{$[~@z;a[x;y]'z;z in x;y z;z]}

/ commutative -> sort
c:""
s:{$[@x;x;(,*x),(::;{x@<x})[(*x)in c]@.z.s'1_x]}

/ words <-> string
p:{$[@x;(-":"=*|x)_x;2=#x;"(",(,/.z.s'x),")";"(",.z.s[x 1],x[0],.z.s[x 2],")"]}
w:$-5!"k)",

/ arithmetic
y:+w''(("x+0";"x")
       ("0+x";"x")
       ("x*1";"x")
       ("1*x";"x")
       ("x-0";"x")
       ("0-x";"-x")
       ("x/1";"x")
       ("x-x";"0")
       ("x/x";"1")
       ("x*y+z";"(x*y)+x*z")
       ("(y+z)*x";"(x*y)+x*z"))

x:+,"xyz"
c:+,"+*"

p s n[x;y]w"b--0"
p s n[x;y]w"a*((b-0)+2)"
p s n[x;y]w"(2+b-0)*a"
p s n[x;y]w"a+((b--5)*2)"
p s n[x;y]w"(2*b-0)+a"
p s n[x;y]w"(2*0-b)+a"

/ logic - (match;transform)
y:+w''(("~~x";"x")
       ("~x|y";"(~x)&~y")
       ("~x&y";"(~x)|~y")
       ("x|y&z";"(x|y)&x|z")
       ("(y&z)|x";"(x|y)&x|z")
       ("x>y";"y|~x")
       ("x=y";"(x>y)&y>x"))

x:+,"xyz"
c:+,"|&"

p s n[x;y]w"r=(~((~q)|~p))>r"

\

\t do[5000;n[x;y]e]

k:{$[#i:&#:'s:u[x;;z]'*y;v[(y[0;*i];c)](z;a[x[];s@*i]c:y[1;*i]);z]}
v:{-1@/:("..";p[*x],"->",p x 1;p[*y],"->",p y 1);y 1}