Nuprl - Pf rel effect lemma 1 1 2 1 2

(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. rel_eq(rel_unprime(r);rel_unprime(r0))
13. 2of(unzip(as)) = map(x.x;1of(unzip(as)))
14. i:. i < ||2of(unzip(as))|| & 2of(unzip(as))[i] = map(x.x;1of(unzip(as)))[i]

i:. i < ||as|| & 2of(as[i]) = 1of(as[i])

By: Unfold `unzip` -1 THEN Reduce -1 THEN ExRepD THEN InstConcl [i]

Generated subgoals:

1 14. i:
15. i < ||map(p.2of(p);as)||
16. map(p.2of(p);as)[i] = map(x.x;map(p.1of(p);as))[i]
i < ||as||

2 14. i:
15. i < ||map(p.2of(p);as)||
16. map(p.2of(p);as)[i] = map(x.x;map(p.1of(p);as))[i]
2of(as[i]) = 1of(as[i])

About:

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

1	14. `i:` 15. `i < \|\|map(p.2of(p);as)\|\|` 16. `map(p.2of(p);as)[i] = map(x.x;map(p.1of(p);as))[i]` `i < \|\|as\|\|`
2	14. `i:` 15. `i < \|\|map(p.2of(p);as)\|\|` 16. `map(p.2of(p);as)[i] = map(x.x;map(p.1of(p);as))[i]` `2of(as[i]) = 1of(as[i])`