Nuprl - Pf wp2 addprime 1 2 2 1

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

1. A: ioa{i:l}()
2. a: Label
3. P: Fmla
4. x: rel()
5. r: rel()
6. r P
7. as: (LabelTerm) List
8. 1of(unzip(as)) = rel_vars(r)
9. i:. i < ||as|| 2of(as[i]) smts_eff(action_effect(a;A.eff;A.frame);1of(as[i]))
10. x = rel_subst(as;r)

rel_subst(as;r) = rel_subst2(as;(r)')

By: Symmetry THEN BackThru Thm* r:rel(), as:(LabelTerm) List. 1of(unzip(as)) = rel_vars(r) rel_subst2(as;(r)') = rel_subst(as;r)

Generated subgoals:

None

About:

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