Nuprl - Pf rel effect lemma 1 1 1 1 1 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. 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. 2of(unzip(as)) = map(x.x;1of(unzip(as)))
13. x: Label
14. (x 1of(unzip(as)))

unprime(apply_alist(as;x;x)) = x

By: Using [`d',x] (FwdThru Thm* as:(LabelT) List, d:T, x:Label. (x 1of(unzip(as))) ( < x,apply_alist(as;x;d) > as) [-1]) THEN Unfold `l_member` -1 THEN ExRepD THEN ApFunToHypEquands `z' 1of(z) Label -1 THEN Reduce -1 THEN ApFunToHypEquands `z' 2of(z) Term -2 THEN Reduce -1

Generated subgoal:

1 15. i:
16. i < ||as||
17. < x,apply_alist(as;x;x) > = as[i]
18. x = 1of(as[i])
19. apply_alist(as;x;x) = 2of(as[i])
unprime(apply_alist(as;x;x)) = x

About:

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