Nuprl - Pf trace consistent ioa inv vc 1

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

1. A: ioa{i:l}()
2. I: Fmla
3. rho: Decl
4. te: LabelLabel
5. ioa_mentions_trace(A)
6. trace_consistent_pred(rho;A.da;te;I)
7. v: vc{i:l}()
8. v VCs(A;I)

trace_consistent_vc(rho;A.da;te;v)

By: Unfold `ioa_inv_vc` -1 THEN Unfolds [`vcs_singleton`;`vcs_add`;`ioa_trans_all`] -1 THEN RW ColMemberC -1 THEN Analyze -1 THEN ExRepD THEN SubstFor v 0 THEN Unfolds [`trace_consistent_vc`;`ioa_trans`] 0 THEN Unfolds [`vc_hyp`;`vc_concl`] 0 THEN Reduce 0 THEN Try (BackThru Thm* p,q:Fmla, rho:Decl, da:Collection(dec()), R:(LabelLabel). trace_consistent_pred(rho;da;R;p q) trace_consistent_pred(rho;da;R;p) & trace_consistent_pred(rho;da;R;q)) THEN Try (BackThru Thm* A:ioa{i:l}(), rho:Decl, te:(LabelLabel), k:Label. ioa_mentions_trace(A) trace_consistent_pred(rho;A.da;te;action_pre(k;A.pre))) THEN Try (BackThru Thm* A:ioa{i:l}(), rho:Decl, te:(LabelLabel). ioa_mentions_trace(A) trace_consistent_pred(rho;A.da;te;A.init)) THEN Try (BackThru Thm* A:ioa{i:l}(), I:Fmla, rho:Decl, te:(LabelLabel), a:dec(). ioa_mentions_trace(A) trace_consistent_pred(rho;A.da;te;I) a A.da trace_consistent_pred(rho;A.da;te;smts_eff_pred(action_effect(a.lbl;A.eff;A.frame);I)))

Generated subgoals:

None

About:

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