PAT

PAT里面有一个trace的隐藏功能。如下面的例子：

P()=a->b->c->P()[]a->b->P(){b};
Q()=a->Q();

两个判断

#assert P() refines Q();
#assert Q() refines P();

判断结果：