1 | 1. A: ioa{i:l}() 2. de: sig() 3. tc_ioa(A;de) 4. ![]() 5. Q: Fmla 6. rho: Decl 7. e: {[[de]] rho} 8. a: [[A]] rho de e.action 9. tr: trace_env([[A.da]] rho) 10. tc_ioa(A;de) 11. ![]() 12. trace_consistent_pred(rho;A.da;tr.proj;Q) 13. single_valued_decls(A.ds) 14. s: [[A]] rho de e.state 15. x': [[A]] rho de e.state 16. tc_pred(Q;A.ds; < > ;de) 17. closed_pred(Q) 18. covers_pred(A;Q) 19. [[A]] rho de e.trans(s,a,x') 20. pred_mng_2((Q)'; rho; A.ds; < > ; de; e; s; x'; ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
About:
![]() | ![]() | ![]() | ![]() |