3 | s0,x:[[A]] rho de e.state, act:[[A]] rho de e.action, x':[[A]] rho de e.state, l:[[A]] rho de e.action List. [[A]] rho de e.init(s0)  trace_reachable([[A]] rho de e;s0;l;x)  [[I]] rho A.ds < > de e x mk_trace_env(l, te)  [[A]] rho de e.trans(x,act,x')  [[I]] rho A.ds < > de e x' mk_trace_env(l @ [act], te) |