\l parse io:{[s]_ssr/[_ssr[_ssr["",s;"<->";"~"];"->";">"];"^v";"&|"]} oi:{[s]_ssr/[_ssr[_ssr["",s;">";"->"];"~";"<->"];"&|";"^v"]} parse:.parse.p io@ unparse:oi .parse.u@ / 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;~(v:`$y)_in!x;();y~a:x v;@[x;v;:;z];a~z;x;()]} / normalize ["vars";rules;expr] n:{{:[@z;z;_f[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]} / truth table t:.+(`p`q`r;2_vs!8) f:("|&>=~";(|;&;~>;=;~:)) v:{:[~@x;{x[0]. 1_ x}@_f'x;x _in*f;f[1]f[0]?x;t@`$x]} / commutative -> sort c:"" s:{:[@x;x;x[0],(::;{x@y" ;"y|-x") ("x<->y" ;"(x->y)^y->x")) x:"xyz" c:"v^" z:unparse s n[x;y]parse@ z"r<->(-((-q)v-p))->r"