Nuprl - Pf rel effect lemma 1

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

1. A: ioa{i:l}()
2. rho: Decl
3. de: sig()
4. act: ([[A.da]] rho)
5. r: rel()
6. r0: rel()
7. tc_ioa(A;de)
8. r smts_eff_rel(action_effect(kind(act);A.eff;A.frame);r0)
9. rel_eq(rel_unprime(r);rel_unprime(r0))

t:dec(). t A.da & t.lbl = kind(act)

By: Unfold `smts_eff_rel` -2 THEN RWW "member_col_subst" -2 THEN Reduce -2 THEN ExRepD

Generated subgoal:

1 8. as: (LabelTerm) List
9. 1of(unzip(as)) = rel_vars(r0)
10. i:. i < ||as|| 2of(as[i]) smts_eff(action_effect(kind(act);A.eff;A.frame);1of(as[i]))
11. r = rel_subst(as;r0)
12. rel_eq(rel_unprime(r);rel_unprime(r0))
t:dec(). t A.da & t.lbl = kind(act)

About:

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