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

At: rel mng 2 wf 1 1
1. r: rel()
2. ds: Collection(dec())
3. da: Collection(dec())
4. de: sig()
5. rho: Decl
6. st1: Collection(SimpleType)
7. e: {[[de]] rho}
8. s: {[[ds]] rho}
9. s': {[[ds]] rho}
10. a: [[st1]] rho
11. tr: trace_env([[da]] rho)
12. trace_consistent_rel(rho;da;tr.proj;r)
13. l: Term List
14. r.args = l

Case(r.name) Case eq(Q) = > ||l|| = 2 & Q term_types(ds;st1;de;l[0]) & Q term_types(ds;st1;de;l[1]) Case R = > ||de.rel(R)|| = ||l|| & (i:. i < ||l|| (de.rel(R))[i] term_types(ds;st1;de;l[i])) Default = > False list_accum(x,t.x([[t]] 1of(e) s s' a tr);[[r.name]] rho 2of(e) ;l) Prop
By:
Analyze 1
THEN
Analyze 1
THEN
All Reduce
THEN
Folds [`relname_eq`;`relname_other`] 0
THEN
Analyze 0
THEN
ExRepD
Generated subgoals:

11. x: SimpleType
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; < inl(x),r1 > )
14. l: Term List
15. r1 = l
16. ||l|| = 2
17. x term_types(ds;st1;de;l[0])
18. x term_types(ds;st1;de;l[1])
list_accum(x,t.x([[t]] 1of(e) s s' a tr);[[relname_eq(x)]] rho 2of(e) ;l) Prop
21. 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
31. 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
0||de.rel(y)||
41. 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
0||l||

About:
listintnatural_numberless_thanapplyequalmemberpropimpliesandfalseall

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