Nuprl - Pf term_subst_mentions

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

as:(LabelTerm) List, g:Label, t:Term. subst_mentions_trace(as) term_mentions_guard(g;term_subst(as;t)) term_mentions_guard(g;t)

By: RepeatFor 3 (Analyze 0) THEN TermInd -1 THEN Reduce 0 THEN Try ((All (RW assert_pushdownC)) THEN (ParallelOp -1) THEN (Complete EasyHyp)) THEN Try ((Analyze -2) THEN (RWO "assert_subst_mentions_trace" 0))

Generated subgoals:

1 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))
i:||as||. mentions_trace(2of(as[i]))

2 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. x: Label
7. term_mentions_guard(g;apply_alist(as;x;x'))
i:||as||. mentions_trace(2of(as[i]))

About:

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

1	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))` `i:\|\|as\|\|. mentions_trace(2of(as[i]))`
2	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. `x:` `Label` 7. `term_mentions_guard(g;apply_alist(as;x;x'))` `i:\|\|as\|\|. mentions_trace(2of(as[i]))`