Nuprl - Pf trace consistent action effect

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

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))

By: Unfold `trace_consistent_pred` 0 THEN Unfold `col_all` 0 THEN Try (Fold `pred` 0)

Generated subgoal:

1 1. A: ioa{i:l}()
2. I: Fmla
3. rho: Decl
4. te: LabelLabel
5. a: dec()
6. ioa_mentions_trace(A)
7. r:rel(). r I trace_consistent_rel(rho;A.da;te;r)
8. a A.da
9. r: rel()
10. r smts_eff_pred(action_effect(a.lbl;A.eff;A.frame);I)
trace_consistent_rel(rho;A.da;te;r)

About:

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