Nuprl - Pf term_subst2

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

t:Term, s:SimpleType, as:(LabelTerm) List, ds:Collection(dec()), da:Collection(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))

By: Analyze 0 THEN TermInd -1 THEN Unfold `term_subst2` 0 THEN Reduce 0 THEN Try (Fold `term_subst2` 0) THEN Try (Complete Auto) THEN Try (Auto THEN BackThruSomeHyp THEN (Try (RWW "member_singleton" 0)) THEN (AllHyps (RWW "member_dec_lookup")))

Generated subgoals:

1 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. x: Label
s:SimpleType, as:(LabelTerm) List, ds:Collection{i}(dec()), da:Collection{i}(SimpleType) , de:sig(). s dec_lookup(ds;x) (x@0:Label. (x@0 [x]) (t:SimpleType. mk_dec(x@0, t) ds t term_types(ds;da;de;apply_alist(as;x@0;x@0)))) s term_types(ds;da;de;apply_alist(as;x;x'))

2 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)))

About:

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