Nuprl - Pf term_subst2

(6steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc

1. t: Term
2. u: TermType{i'}
3. w: t:{v:Term| u(v) }s:SimpleType, as:(LabelTerm) List, ds:Collection{i}(dec()) , da:Collection{i}(SimpleType), de:sig(). s term_types(ds;da;de;t) (x:Label. (x term_primed_vars(t)) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))) s term_types(ds;da;de;term_subst2(as;t))
4. y1: {v:Term| u(v) }
5. y2: {v:Term| u(v) }

s:SimpleType, as:(LabelTerm) List, ds:Collection{i}(dec()), da:Collection{i}(SimpleType) , de:sig(). s st_app(term_types(ds;da;de;y1);term_types(ds;da;de;y2)) (x:Label. (x term_primed_vars(y1) @ term_primed_vars(y2)) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))) s st_app(term_types(ds;da;de;term_subst2(as;y1));term_types(ds;da;de;term_subst2(as;y2)))

By: Unfold `term_types` 0 THEN Reduce 0 THEN Fold `term_types` 0 THEN RWW "member_st_app" 0

Generated subgoal:

1 6. s: SimpleType
7. as: (LabelTerm) List
8. ds: Collection{i}(dec())
9. da: Collection{i}(SimpleType)
10. de: sig()
11. a:SimpleType. a term_types(ds;da;de;y2) & as term_types(ds;da;de;y1)
12. x:Label. (x term_primed_vars(y1) @ term_primed_vars(y2)) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))
a:SimpleType. a term_types(ds;da;de;term_subst2(as;y2)) & as term_types(ds;da;de;term_subst2(as;y1))

About:

(6steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc