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

At: rel mng 2 iff 1 1 2 1
1. y: Label
2. ds: Collection(dec())
3. daa: Collection(dec())
4. da: Collection(SimpleType)
5. de: sig()
6. rho: Decl
7. e1: {1of([[de]] rho)}
8. e2: l:Labelreduce(s,m. [[s]] rhom;Prop;de.rel(l))
9. s1: {[[ds]] rho}
10. s2: {[[ds]] rho}
11. a: [[da]] rho
12. tr: trace_env([[daa]] rho)
13. l1: Term List
14. u: Term
15. v: Term List
16. l2:Term List. ||v|| = ||l2|| (ls:SimpleType List. ||ls|| = ||v|| (f:reduce(s,m. [[s]] rhom;Prop;ls). (i:||v||. trace_consistent(rho;daa;tr.proj;v[i])) (i:||l2||. trace_consistent(rho;daa;tr.proj;l2[i])) ||ls|| = ||v|| & (i:. i < ||v|| ls[i] term_types(ds;da;de;v[i])) ||ls|| = ||l2|| & (i:. i < ||l2|| ls[i] term_types(ds;da;de;l2[i])) (i:. i < ||v|| [[v[i]]] e1 s1 a tr = [[l2[i]]] e1 s1 s2 a tr [[ls[i]]] rho) (list_accum(x,t.x([[t]] e1 s1 a tr);f;v) list_accum(x,t.x([[t]] e1 s1 s2 a tr);f;l2))))
17. l2: Term List
18. u1: Term
19. v1: Term List
20. ||[u / v]|| = ||v1|| (ls:SimpleType List. ||ls|| = ||[u / v]|| (f:reduce(s,m. [[s]] rhom;Prop;ls). (i:||[u / v]||. trace_consistent(rho;daa;tr.proj;[u / v][i])) (i:||v1||. trace_consistent(rho;daa;tr.proj;v1[i])) ||ls|| = ||[u / v]|| & (i:. i < ||[u / v]|| ls[i] term_types(ds;da;de;[u / v][i])) ||ls|| = ||v1|| & (i:. i < ||v1|| ls[i] term_types(ds;da;de;v1[i])) (i:. i < ||[u / v]|| [[[u / v][i]]] e1 s1 a tr = [[v1[i]]] e1 s1 s2 a tr [[ls[i]]] rho) (list_accum(x,t.x([[t]] e1 s1 a tr);f;[u / v]) list_accum(x,t.x([[t]] e1 s1 s2 a tr);f;v1))))
21. ||v||+1 = ||v1||+1
22. ls: SimpleType List
23. u2: SimpleType
24. v2: SimpleType List
25. ||v2|| = ||v||+1 (f:reduce(s,m. [[s]] rhom;Prop;v2). (i:(||v||+1). trace_consistent(rho;daa;tr.proj;[u / v][i])) (i:(||v1||+1). trace_consistent(rho;daa;tr.proj;[u1 / v1][i])) ||v2|| = ||v||+1 & (i:. i < ||v||+1 v2[i] term_types(ds;da;de;[u / v][i])) ||v2|| = ||v1||+1 & (i:. i < ||v1||+1 v2[i] term_types(ds;da;de;[u1 / v1][i])) (i:. i < ||v||+1 [[[u / v][i]]] e1 s1 a tr = [[[u1 / v1][i]]] e1 s1 s2 a tr [[v2[i]]] rho) (list_accum(x,t.x([[t]] e1 s1 a tr);f([[u]] e1 s1 a tr);v) list_accum(x,t.x([[t]] e1 s1 s2 a tr);f([[u1]] e1 s1 s2 a tr);v1)))
26. ||v2||+1 = ||v||+1
27. f: [[u2]] rhoreduce(s,m. [[s]] rhom;Prop;v2)
28. i:(||v||+1). trace_consistent(rho;daa;tr.proj;[u / v][i])
29. i:(||v1||+1). trace_consistent(rho;daa;tr.proj;[u1 / v1][i])
30. ||v2||+1 = ||v||+1 & (i:. i < ||v||+1 [u2 / v2][i] term_types(ds;da;de;[u / v][i]))
31. ||v2||+1 = ||v1||+1 & (i:. i < ||v1||+1 [u2 / v2][i] term_types(ds;da;de;[u1 / v1][i]))

(i:. i < ||v||+1 [[[u / v][i]]] e1 s1 a tr = [[[u1 / v1][i]]] e1 s1 s2 a tr [[[u2 / v2][i]]] rho) (list_accum(x,t.x([[t]] e1 s1 a tr);f([[u]] e1 s1 a tr);v) list_accum(x,t.x([[t]] e1 s1 s2 a tr);f([[u1]] e1 s1 s2 a tr);v1))
By:
Thin -7
THEN
Thin -11
THEN
Analyze 0
Generated subgoals:

120. ||v||+1 = ||v1||+1
21. ls: SimpleType List
22. u2: SimpleType
23. v2: SimpleType List
24. ||v2||+1 = ||v||+1
25. f: [[u2]] rhoreduce(s,m. [[s]] rhom;Prop;v2)
26. i:(||v||+1). trace_consistent(rho;daa;tr.proj;[u / v][i])
27. i:(||v1||+1). trace_consistent(rho;daa;tr.proj;[u1 / v1][i])
28. ||v2||+1 = ||v||+1 & (i:. i < ||v||+1 [u2 / v2][i] term_types(ds;da;de;[u / v][i]))
29. ||v2||+1 = ||v1||+1 & (i:. i < ||v1||+1 [u2 / v2][i] term_types(ds;da;de;[u1 / v1][i]))
30. i:. i < ||v||+1 [[[u / v][i]]] e1 s1 a tr = [[[u1 / v1][i]]] e1 s1 s2 a tr [[[u2 / v2][i]]] rho
list_accum(x,t.x([[t]] e1 s1 a tr);f([[u]] e1 s1 a tr);v) list_accum(x,t.x([[t]] e1 s1 s2 a tr);f([[u1]] e1 s1 s2 a tr);v1)
220. ||v||+1 = ||v1||+1
21. ls: SimpleType List
22. u2: SimpleType
23. v2: SimpleType List
24. ||v2||+1 = ||v||+1
25. f: [[u2]] rhoreduce(s,m. [[s]] rhom;Prop;v2)
26. i:(||v||+1). trace_consistent(rho;daa;tr.proj;[u / v][i])
27. i:(||v1||+1). trace_consistent(rho;daa;tr.proj;[u1 / v1][i])
28. ||v2||+1 = ||v||+1 & (i:. i < ||v||+1 [u2 / v2][i] term_types(ds;da;de;[u / v][i]))
29. ||v2||+1 = ||v1||+1 & (i:. i < ||v1||+1 [u2 / v2][i] term_types(ds;da;de;[u1 / v1][i]))
30. i:
31. i < ||v||+1
i < ||[u2 / v2]||
320. ||v||+1 = ||v1||+1
21. ls: SimpleType List
22. u2: SimpleType
23. v2: SimpleType List
24. ||v2||+1 = ||v||+1
25. f: [[u2]] rhoreduce(s,m. [[s]] rhom;Prop;v2)
26. i:(||v||+1). trace_consistent(rho;daa;tr.proj;[u / v][i])
27. i:(||v1||+1). trace_consistent(rho;daa;tr.proj;[u1 / v1][i])
28. ||v2||+1 = ||v||+1 & (i:. i < ||v||+1 [u2 / v2][i] term_types(ds;da;de;[u / v][i]))
29. ||v2||+1 = ||v1||+1 & (i:. i < ||v1||+1 [u2 / v2][i] term_types(ds;da;de;[u1 / v1][i]))
30. i:
31. i < ||v||+1
[[[u / v][i]]] e1 s1 a tr [[[u2 / v2][i]]] rho
420. ||v||+1 = ||v1||+1
21. ls: SimpleType List
22. u2: SimpleType
23. v2: SimpleType List
24. ||v2||+1 = ||v||+1
25. f: [[u2]] rhoreduce(s,m. [[s]] rhom;Prop;v2)
26. i:(||v||+1). trace_consistent(rho;daa;tr.proj;[u / v][i])
27. i:(||v1||+1). trace_consistent(rho;daa;tr.proj;[u1 / v1][i])
28. ||v2||+1 = ||v||+1 & (i:. i < ||v||+1 [u2 / v2][i] term_types(ds;da;de;[u / v][i]))
29. ||v2||+1 = ||v1||+1 & (i:. i < ||v1||+1 [u2 / v2][i] term_types(ds;da;de;[u1 / v1][i]))
30. i:
31. i < ||v||+1
[[[u1 / v1][i]]] e1 s1 s2 a tr [[[u2 / v2][i]]] rho

About:
listconsintnatural_numberaddless_thanlambda
applyfunctionequalmemberpropimplies
all

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