Nuprl - Pf term_subst_mentions

(16steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

1. as: (LabelTerm) List
2. g: Label
3. t: Term
4. u: TermType{i'}
5. w: t:{v:Term| u(v) }subst_mentions_trace(as) term_mentions_guard(g;term_subst(as;t)) term_mentions_guard(g;t)
6. x1: Label
7. term_mentions_guard(g;apply_alist(as;x1;x1))
8. i:
9. i < ||2of(unzip(as))||
10. apply_alist(as;x1;x1) = 2of(unzip(as))[i]

mentions_trace(2of(as[i]))

By: Unfold `unzip` -2 THEN Reduce -2 THEN RWO "map_length" -2 THEN MoveToConcl -4 THEN HypSubstSq -1 0 THEN Subst' (2of(unzip(as))[i] = 2of(as[i])) 0

Generated subgoals:

1 7. i:
8. i < ||as||
9. apply_alist(as;x1;x1) = 2of(unzip(as))[i]
10. x,y:Term. x = y (x ~ y)
2of(unzip(as))[i] = 2of(as[i])

2 7. i:
8. i < ||as||
9. apply_alist(as;x1;x1) = 2of(unzip(as))[i]
term_mentions_guard(g;2of(as[i])) mentions_trace(2of(as[i]))

About:

(16steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

1	7. `i:` 8. `i < \|\|as\|\|` 9. `apply_alist(as;x1;x1) = 2of(unzip(as))[i]` 10. `x,y:Term. x = y (x ~ y)` `2of(unzip(as))[i] = 2of(as[i])`
2	7. `i:` 8. `i < \|\|as\|\|` 9. `apply_alist(as;x1;x1) = 2of(unzip(as))[i]` `term_mentions_guard(g;2of(as[i])) mentions_trace(2of(as[i]))`