Nuprl - Pf term_subst_mentions_guard 2 1 2 2

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

At: term subst mentions guard 2 1 2 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. i:
8. i < ||as||
9. apply_alist(as;x;x') = 2of(unzip(as))[i]

term_mentions_guard(g;2of(as[i])) mentions_trace(2of(as[i]))

By: GenConcl (2of(as[i]) = t2) THEN Thin -1 THEN TermInd -1 THEN Reduce 0

Generated subgoal:

1 10. t2: Term
11. u1: TermType{i'}
12. w1: t2:{v:Term| u1(v) }term_mentions_guard(g;t2) mentions_trace(t2)
13. y1: {v:Term| u1(v) }
14. y2: {v:Term| u1(v) }
15. term_mentions_guard(g;y1) term_mentions_guard(g;y2)
mentions_trace(y1) mentions_trace(y2)

About:

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