Nuprl - Pf rel subst mng 2 iff 3 2 1 1

(65steps) (too big for print form) Definitions Lemmas mb automata 4 Sections GenAutomata Doc

1. r: rel()
2. as: (LabelTerm) List
3. ds: Collection(dec())
4. daa: Collection(dec())
5. da: Collection(SimpleType)
6. de: sig()
7. rho: Decl
8. e: {[[de]] rho}
9. s: {[[ds]] rho}
10. s': {[[ds]] rho}
11. k: Label
12. a: [[da]] rho
13. tr: trace_env([[daa]] rho)
14. trace_consistent_rel(rho;daa;tr.proj;r)
15. tc(r;ds;da;de)
16. x: Label
17. (x rel_primed_vars(r))
18. t: SimpleType
19. mk_dec(x, t) ds
20. t term_types(ds;da;de;apply_alist(as;x;x))
21. g: Label
22. term_mentions_guard(g;apply_alist(as;x;x))
23. (apply_alist(as;x;x) 2of(unzip(as)))

subst_mentions_trace(as)

By: Unfolds [`l_member`;`unzip`] -1 THEN Reduce -1 THEN RWO "map_length" -1

Generated subgoals:

1 23. i:. i < ||map(p.2of(p);as)|| & apply_alist(as;x;x) = map(p.2of(p);as)[i]
24. i:
(i < ||map(p.2of(p);as)||) = (i < ||as||) Type{[1 | i 0]}

2 23. i:. i < ||as|| & apply_alist(as;x;x) = map(p.2of(p);as)[i]
subst_mentions_trace(as)

About:

(65steps) (too big for print form) Definitions Lemmas mb automata 4 Sections GenAutomata Doc

1	23. `i:. i < \|\|map(p.2of(p);as)\|\| & apply_alist(as;x;x) = map(p.2of(p);as)[i]` 24. `i:` `(i < \|\|map(p.2of(p);as)\|\|) = (i < \|\|as\|\|) Type{[1 \| i 0]}`
2	23. `i:. i < \|\|as\|\| & apply_alist(as;x;x) = map(p.2of(p);as)[i]` `subst_mentions_trace(as)`