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

At: rel mng lemma 1 2 1 2 1 1 2
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. a: [[st1]] rho
9. tr: trace_env([[da]] rho)
10. l: Term List
11. u: Term
12. v: Term List
13. i:(||v||+1). trace_consistent(rho;da;tr.proj;[u / v][i])
14. ls: SimpleType List
15. f: reduce(s,m. [[s]] rhom;Prop;[hd(ls) / tl(ls)])
16. ||ls|| = ||v||+1
17. i:. i < ||v||+1 ls[i] term_types(ds;st1;de;[u / v][i])
18. 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 a tr);f;v) Prop
19. 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 a tr);f;v) Prop

f([[u]] e1 s a tr) reduce(s,m. [[s]] rhom;Prop;tl(ls))
By:
RecUnfold `reduce` -5
THEN
Reduce -5
Generated subgoal:

115. f: [[hd(ls)]] rhoreduce(s,m. [[s]] rhom;Prop;tl(ls))
16. ||ls|| = ||v||+1
17. i:. i < ||v||+1 ls[i] term_types(ds;st1;de;[u / v][i])
18. 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 a tr);f;v) Prop
19. 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 a tr);f;v) Prop
[[u]] e1 s a tr [[hd(ls)]] rho

About:
listconsnatural_numberaddless_thanlambdaapply
functionequalmemberpropimpliesall

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