Nuprl - Pf term_subst2_mentions

(8steps) 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_subst2(as;t)) term_mentions_guard(g;t)
6. x: Label
7. term_mentions_guard(g;apply_alist(as;x;x'))
8. i:
9. i < ||2of(unzip(as))||
10. apply_alist(as;x;x') = 2of(unzip(as))[i]

i < ||as||

By: Unfold `unzip` -2 THEN Reduce -2 THEN RWO "map_length" -2

Generated subgoals:

None

About:

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