Nuprl - Pf rel_subst2

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

1. r: rel()
2. as: (LabelTerm) List
3. ds: Collection(dec())
4. da: Collection(SimpleType)
5. de: sig()
6. tc(r;ds;da;de)
7. x:Label. (x rel_primed_vars(r)) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))

tc(rel_subst2(as;r);ds;da;de)

By: All (Unfolds [`tc`;`rel_subst2`]) THEN Analyze 1 THEN Analyze 1 THEN All Reduce THEN ExRepD

Generated subgoals:

1 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)))
||map(t.term_subst2(as;t);r1)|| = 2 & x term_types(ds;da;de;map(t.term_subst2(as;t);r1)[0]) & x term_types(ds;da;de;map(t.term_subst2(as;t);r1)[1])

2 1. y: Label
2. r1: Term List
3. as: (LabelTerm) List
4. ds: Collection(dec())
5. da: Collection(SimpleType)
6. de: sig()
7. ||de.rel(y)|| = ||r1||
8. i:. i < ||r1|| (de.rel(y))[i] term_types(ds;da;de;r1[i])
9. x:Label. (x rel_primed_vars( < inr(y),r1 > )) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))
||de.rel(y)|| = ||map(t.term_subst2(as;t);r1)|| & (i:. i < ||map(t.term_subst2(as;t);r1)|| (de.rel(y))[i] term_types(ds;da;de;map(t.term_subst2(as;t);r1)[i]))

About:

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