Nuprl - Pf rel mng 2 wf 1 1 2 1 1 2

(16steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc

1. y: Label
2. r1: Term List
3. ds: Collection(dec())
4. da: Collection(dec())
5. de: sig()
6. rho: Decl
7. st1: Collection(SimpleType)
8. e1: {1of([[de]] rho)}
9. e2: l:Labelreduce(s,m. [[s]] rhom;Prop;de.rel(l))
10. s: {[[ds]] rho}
11. s': {[[ds]] rho}
12. a: [[st1]] rho
13. tr: trace_env([[da]] rho)
14. trace_consistent_rel(rho;da;tr.proj; < inr(y),r1 > )
15. l: Term List
16. r1 = l
17. ||de.rel(y)|| = ||l||
18. i:. i < ||l|| (de.rel(y))[i] term_types(ds;st1;de;l[i])
19. f: reduce(s,m. [[s]] rhom;Prop;de.rel(y))
20. e2.y = f

list_accum(x,t.x([[t]] e1 s s' a tr);f;l) Prop

By: BackThru Thm* ds,da:Collection(dec()), de:sig(), rho:Decl, st1:Collection(SimpleType), e1:{1of([[de]] rho)}, s,s':{[[ds]] rho}, a:[[st1]] rho, tr:trace_env([[da]] rho), l:Term List. (i:||l||. trace_consistent(rho;da;tr.proj;l[i])) (ls:SimpleType List, f:reduce(s,m. [[s]] rhom;Prop;ls). ||ls|| = ||l|| & (i:. i < ||l|| ls[i] term_types(ds;st1;de;l[i])) list_accum(x,t.x([[t]] e1 s s' a tr);f;l) Prop) THEN EasyHyp

Generated subgoal:

1 21. i: ||l||
trace_consistent(rho;da;tr.proj;l[i])

About:

(16steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc