A:ioa{i:l}(), I:Fmla, rho:Decl, de:sig(), e:{[[de]] rho}, te:(LabelLabel). tc_ioa(A;de) ioa_mentions_trace(A) trace_consistent_pred(rho;A.da;te;I) tc_pred(I;A.ds; < > ;de) covers_pred(A;I) guarded_trace(A.da;te;I) closed_pred(I) single_valued_decls(A.ds) (s0,x:[[A]] rho de e.state, act:[[A]] rho de e.action, x':[[A]] rho de e.state, tr:([[A.da]] rho) List. [[A]] rho de e.init(s0) trace_reachable([[A]] rho de e;s0;mk_trace_env(tr, te).trace;x) [[I]] rho A.ds < > de e x mk_trace_env(tr, te) [[A]] rho de e.trans(x,act,x') ((t:dec(). t A.da & t.lbl = kind(act)) [[I]] rho A.ds < > de e x' tappend(mk_trace_env(tr, te);act)) [[I]] rho A.ds < > de e x' tappend(mk_trace_env(tr, te);act))

let T1 (Unfold `ioa_mng` 0) THEN (Reduce 0) THEN Trivial , T2 (Try (Unfold `tappend` 0)) THEN (Reduce 0) THEN (Complete Auto) , T Auto THEN (Try (Unfold `decl` 0)) THEN (Try (Fold `pred` 0)) THEN (Try (BackThru Thm* v:Top, rho:Decl. v [[ < > ]] rho)) THEN TrivialIoaHyp THEN (Try T1) THEN (Try T2) in RepeatFor 24 ((Analyze 0) THENA (Complete T))

1

1. A: ioa{i:l}() 2. I: Fmla 3. rho: Decl 4. de: sig() 5. e: {[[de]] rho} 6. te: LabelLabel 7. tc_ioa(A;de) 8. ioa_mentions_trace(A) 9. trace_consistent_pred(rho;A.da;te;I) 10. tc_pred(I;A.ds; < > ;de) 11. covers_pred(A;I) 12. guarded_trace(A.da;te;I) 13. closed_pred(I) 14. single_valued_decls(A.ds) 15. s0: [[A]] rho de e.state 16. x: [[A]] rho de e.state 17. act: [[A]] rho de e.action 18. x': [[A]] rho de e.state 19. tr: ([[A.da]] rho) List 20. [[A]] rho de e.init(s0) 21. trace_reachable([[A]] rho de e;s0;mk_trace_env(tr, te).trace;x) 22. [[I]] rho A.ds < > de e x mk_trace_env(tr, te) 23. [[A]] rho de e.trans(x,act,x') 24. (t:dec(). t A.da & t.lbl = kind(act)) [[I]] rho A.ds < > de e x' tappend(mk_trace_env(tr, te);act) [[I]] rho A.ds < > de e x' tappend(mk_trace_env(tr, te);act)

About: