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

At: trace consistent action effect 1 1 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@0: rel()
11. r@0 I
12. as: (LabelTerm) List
13. 1of(unzip(as)) = rel_vars(r@0)
14. i:. i < ||as|| 2of(as[i]) smts_eff(action_effect(a.lbl;A.eff;A.frame);1of(as[i]))
15. r = rel_subst(as;r@0)
16. trace_consistent_rel(rho;A.da;te;r@0)

trace_consistent_rel(rho;A.da;te;rel_subst(as;r@0))
By: BackThru Thm* r:rel(), as:(LabelTerm) List, daa:Collection(dec()), rho:Decl, te:(LabelLabel). trace_consistent_rel(rho;daa;te;r) subst_mentions_trace(as) trace_consistent_rel(rho;daa;te;rel_subst(as;r))
Generated subgoal:

1 subst_mentions_trace(as)

About:
productlistboolassertless_thanfunctionequalimpliesall

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