Nuprl - Pf rel mng wf 1 1 2 1

(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. e: {[[de]] rho}
9. s: {[[ds]] rho}
10. a: [[st1]] rho
11. tr: trace_env([[da]] rho)
12. trace_consistent_rel(rho;da;tr.proj; < inr(y),r1 > )
13. l: Term List
14. r1 = l
15. ||de.rel(y)|| = ||l||
16. i:. i < ||l|| (de.rel(y))[i] term_types(ds;st1;de;l[i])

list_accum(x,t.x([[t]] 1of(e) s a tr);2of(e).y;l) Prop

By: let i 8 , j 9 in (Analyze i) THEN (All Reduce) THEN (Unfold `sig_mng` j) THEN (Unfold `record` j) THEN (Unfold `decl_type` j) THEN (Reduce j) THEN (Unfold `st_list_mng` j)

Generated subgoal:

1 8. e1: {1of([[de]] rho)}
9. e2: l:Labelreduce(s,m. [[s]] rhom;Prop;de.rel(l))
10. s: {[[ds]] rho}
11. a: [[st1]] rho
12. tr: trace_env([[da]] rho)
13. trace_consistent_rel(rho;da;tr.proj; < inr(y),r1 > )
14. l: Term List
15. r1 = l
16. ||de.rel(y)|| = ||l||
17. i:. i < ||l|| (de.rel(y))[i] term_types(ds;st1;de;l[i])
list_accum(x,t.x([[t]] e1 s a tr);e2.y;l) Prop

About:

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