Nuprl - Pf vc trace correctness

(51steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc

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) guarded_trace(A.da;te;I) tc_pred(I;A.ds; < > ;de) covers_pred(A;I) closed_pred(I) single_valued_decls(A.ds) let M = [[A]] rho de e in (s:M.state, tr:([[A.da]] rho) List. (M -tr- > s) [[VCs(A;I)]] rho A.ds A.da de e s mk_trace_env(tr, te)) (M |= always s,tr.[[I]] rho A.ds < > de e s mk_trace_env(tr, te))

By: Unfold `let` 0 THEN Reduce 0 THEN Try ((Unfold `decl` 0) THEN (Complete Auto)) THEN Try ((Unfold `ioa_mng` 0) THEN (Reduce 0) THEN Trivial) THEN Try TrivialIoaHyp THEN Try Easy

Generated subgoals:

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. guarded_trace(A.da;te;I)
11. tc_pred(I;A.ds; < > ;de)
12. covers_pred(A;I)
13. closed_pred(I)
14. single_valued_decls(A.ds)
15. s:[[A]] rho de e.state, tr:([[A.da]] rho) List. ([[A]] rho de e -tr- > s) [[VCs(A;I)]] rho A.ds A.da de e s mk_trace_env(tr, te)
([[A]] rho de e |= always s,tr.[[I]] rho A.ds < > de e s mk_trace_env(tr, te))

2 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. guarded_trace(A.da;te;I)
11. tc_pred(I;A.ds; < > ;de)
12. covers_pred(A;I)
13. closed_pred(I)
14. single_valued_decls(A.ds)
15. s: [[A]] rho de e.state
16. tr: ([[A.da]] rho) List
17. ([[A]] rho de e -tr- > s)
(vVCs(A;I).trace_consistent_vc(rho;A.da;mk_trace_env(tr, te).proj;v))

About:

(51steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc