Nuprl - Pf rel_mng_2

(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)

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)

By: Analyze 0 THEN ListInd -1 THEN Reduce 0 THEN Analyze 0

Generated subgoals:

1 11. l: Term List
12. i:0. trace_consistent(rho;da;tr.proj;nil[i])
ls:SimpleType List, f:reduce(s,m. [[s]] rhom;Prop;ls). ||ls|| = 0 & (i:. i < 0 ls[i] term_types(ds;st1;de;nil[i])) f Prop

2 11. l: Term List
12. u: Term
13. v: Term List
14. (i:||v||. trace_consistent(rho;da;tr.proj;v[i])) (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)
15. i:(||v||+1). trace_consistent(rho;da;tr.proj;[u / v][i])
ls:SimpleType List, f:reduce(s,m. [[s]] rhom;Prop;ls). ||ls|| = ||v||+1 & (i:. i < ||v||+1 ls[i] term_types(ds;st1;de;[u / v][i])) list_accum(x,t.x([[t]] e1 s s' a tr);f([[u]] e1 s s' a tr);v) Prop

3 11. l: Term List
12. u: Term
13. v: Term List
14. (i:||v||. trace_consistent(rho;da;tr.proj;v[i])) (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)
15. i: (||v||+1)
i < ||[u / v]||

About:

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

1	11. `l:` `Term List` 12. `i:0. trace_consistent(rho;da;tr.proj;nil[i])` `ls:SimpleType List, f:reduce(s,m. [[s]] rhom;Prop;ls). \|\|ls\|\| = 0 & (i:. i < 0 ls[i] term_types(ds;st1;de;nil[i])) f Prop`
2	11. `l:` `Term List` 12. `u:` `Term` 13. `v:` `Term List` 14. `(i:\|\|v\|\|. trace_consistent(rho;da;tr.proj;v[i])) (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)` 15. `i:(\|\|v\|\|+1). trace_consistent(rho;da;tr.proj;[u / v][i])` `ls:SimpleType List, f:reduce(s,m. [[s]] rhom;Prop;ls). \|\|ls\|\| = \|\|v\|\|+1 & (i:. i < \|\|v\|\|+1 ls[i] term_types(ds;st1;de;[u / v][i])) list_accum(x,t.x([[t]] e1 s s' a tr);f([[u]] e1 s s' a tr);v) Prop`
3	11. `l:` `Term List` 12. `u:` `Term` 13. `v:` `Term List` 14. `(i:\|\|v\|\|. trace_consistent(rho;da;tr.proj;v[i])) (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)` 15. `i:` `(\|\|v\|\|+1)` `i < \|\|[u / v]\|\|`