Nuprl - Pf rel_subst2

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

1. x: SimpleType
2. r1: Term List
3. as: (LabelTerm) List
4. ds: Collection(dec())
5. da: Collection(SimpleType)
6. de: sig()
7. ||r1|| = 2
8. x term_types(ds;da;de;r1[0])
9. x term_types(ds;da;de;r1[1])
10. x@0:Label. (x@0 rel_primed_vars( < inl(x),r1 > )) (t:SimpleType. mk_dec(x@0, t) ds t term_types(ds;da;de;apply_alist(as;x@0;x@0)))
11. ||r1|| = 2

x term_types(ds;da;de;term_subst2(as;r1[0])) & x term_types(ds;da;de;term_subst2(as;r1[1]))

By: Analyze 0 THEN BackThru Thm* 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)) THEN InstHyp [x1] -6 THEN Try BackThruSomeHyp THEN Try ((Folds [`relname_eq`;`mk_rel`] 0) THEN (RWW "member_rel_primed_vars" 0) THEN (Reduce 0)) THEN Try ((InstConcl [0]) THEN (Complete Auto)) THEN Try (InstConcl [1])

Generated subgoals:

None

About:

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