Nuprl - Pf rel_mng_2_lemma 1 2 1 2 1 1 2 1

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

1. ds: Collection(dec())
2. da: Collection(dec())
3. de: sig()
4. rho: Decl
5. st1: Collection(SimpleType)
6. e1: {1of([[de]] rho)}
7. s: {[[ds]] rho}
8. s': {[[ds]] rho}
9. a: [[st1]] rho
10. tr: trace_env([[da]] rho)
11. l: Term List
12. u: Term
13. v: Term List
14. i:(||v||+1). trace_consistent(rho;da;tr.proj;[u / v][i])
15. ls: SimpleType List
16. f: [[hd(ls)]] rhoreduce(s,m. [[s]] rhom;Prop;tl(ls))
17. ||ls|| = ||v||+1
18. i:. i < ||v||+1 ls[i] term_types(ds;st1;de;[u / v][i])
19. ls:SimpleType List, f:reduce(s,m. [[s]] rhom;Prop;ls). ||ls|| = ||v|| & (i:. i < ||v|| ls[i] term_types(ds;st1;de;v[i])) list_accum(x,t.x([[t]] e1 s s' a tr);f;v) Prop
20. f:reduce(s,m. [[s]] rhom;Prop;tl(ls)). ||tl(ls)|| = ||v|| & (i:. i < ||v|| tl(ls)[i] term_types(ds;st1;de;v[i])) list_accum(x,t.x([[t]] e1 s s' a tr);f;v) Prop

[[u]] e1 s s' a tr [[hd(ls)]] rho

By: BackThru Thm* ds,daa:Collection(dec()), da:Collection(SimpleType), de:sig(), rho:Decl , t:Term, s,s':{[[ds]] rho}, e:{1of([[de]] rho)}, a:SimpleType, v:[[da]] rho , tr:trace_env([[daa]] rho). trace_consistent(rho;daa;tr.proj;t) a term_types(ds;da;de;t) [[t]] e s s' v tr [[a]] rho THEN AllHyps (h.((InstHyp [0] h) THENA (Complete Auto)) THEN (Reduce -1) THEN Trivial) THEN Try ((InstHyp [0] -3) THEN (Unfold `select` -1) THEN (Reduce -1) THEN (Try Trivial))

Generated subgoal:

1 21. hd(ls) term_types(ds;st1;de;u)
ls SimpleType List

About:

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