u = s 
if eq(u,s)
False else mem_f(St;s;LShort(v)) fi
St
x,y:St. eq(x,y) 
x = y mem_f(St;s;LShort(v)) u = s mem_f(St;s;LShort(v) \ u)l:St*, s:St, eq:(StSt), sx:St.
mem_f(St;sx;l \ s) 
if eq(s,sx) False else mem_f(St;sx;l) fi)
0| 1 | u = s if eq(u,s) False else mem_f(St;s;LShort(v)) fi |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |