Nuprl - Pf rel mng 2 wf 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. e: {[[de]] rho}
9. s: {[[ds]] rho}
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]] 1of(e) s s' a tr);[[relname_other(y)]] rho 2of(e) ;l) Prop

By: Unfold `relname_mng` 0 THEN Reduce 0

Generated subgoal:

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

About:

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