1 | 16. s0: [[A]] rho de e.state 17. x: [[A]] rho de e.state 18. act: [[A]] rho de e.action 19. x': [[A]] rho de e.state 20. l: [[A]] rho de e.action List 21. [[A]] rho de e.init(s0) 22. trace_reachable([[A]] rho de e;s0;l;x) ![]() ![]() |
2 | 16. s0: [[A]] rho de e.state 17. x: [[A]] rho de e.state 18. act: [[A]] rho de e.action 19. x': [[A]] rho de e.state 20. l: [[A]] rho de e.action List 21. [[A]] rho de e.init(s0) 22. trace_reachable([[A]] rho de e;s0;l;x) 23. mk_trace_env(l, te) ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
About:
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |