Nuprl - Pf trace consistent action effect 1

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

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)

By: Unfold `smts_eff_pred` -1 THEN RW ColMemberC -1 THEN ExRepD THEN AllHyps (h.(InstWithVar -3 h) THENA (Complete Auto))

Generated subgoal:

1 10. r@0: rel()
11. r@0 I
12. r smts_eff_rel(action_effect(a.lbl;A.eff;A.frame);r@0)
13. trace_consistent_rel(rho;A.da;te;r@0)
trace_consistent_rel(rho;A.da;te;r)

About:

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