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

At: wp2 addprime 1 1 1 2 1
1. A: ioa{i:l}()
2. a: Label
3. P: Fmla
4. x: rel()
5. r: rel()
6. r@0: rel()
7. r@0 P
8. r = (r@0)'
9. as: (LabelTerm) List
10. 1of(unzip(as)) = rel_primed_vars(r)
11. i:. i < ||as|| 2of(as[i]) smts_eff(action_effect(a;A.eff;A.frame);1of(as[i]))
12. x = rel_subst2(as;r)

1of(unzip(as)) = rel_vars(r@0)
By: Subst (rel_vars(r@0) = rel_primed_vars(r)) 0
Generated subgoal:

1 rel_vars(r@0) = rel_primed_vars(r)

About:
productlistless_thanequalimpliesall

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