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

At: tc closed rel 1
1. r: rel()
2. ds: Collection(dec())
3. da1: Collection(SimpleType)
4. da2: Collection(SimpleType)
5. de: sig()
6. closed_rel(r)
7. tc(r;ds;da1;de)
8. i:. closed_rel(r) i < ||r.args|| closed_term(r.args[i])

tc(r;ds;da2;de)
By:
Analyze 1
THEN
Analyze 1
THEN
All (Folds [`mk_rel`;`relname_eq`;`relname_other`])
THEN
All (Unfolds [`tc`])
THEN
All Reduce
THEN
ExRepD
Generated subgoals:

11. x: SimpleType
2. r1: Term List
3. ds: Collection(dec())
4. da1: Collection(SimpleType)
5. da2: Collection(SimpleType)
6. de: sig()
7. closed_rel(mk_rel(relname_eq(x), r1))
8. ||r1|| = 2
9. x term_types(ds;da1;de;r1[0])
10. x term_types(ds;da1;de;r1[1])
11. i:. closed_rel(mk_rel(relname_eq(x), r1)) i < ||r1|| closed_term(r1[i])
x term_types(ds;da2;de;r1[0])
21. x: SimpleType
2. r1: Term List
3. ds: Collection(dec())
4. da1: Collection(SimpleType)
5. da2: Collection(SimpleType)
6. de: sig()
7. closed_rel(mk_rel(relname_eq(x), r1))
8. ||r1|| = 2
9. x term_types(ds;da1;de;r1[0])
10. x term_types(ds;da1;de;r1[1])
11. i:. closed_rel(mk_rel(relname_eq(x), r1)) i < ||r1|| closed_term(r1[i])
x term_types(ds;da2;de;r1[1])
31. y: Label
2. r1: Term List
3. ds: Collection(dec())
4. da1: Collection(SimpleType)
5. da2: Collection(SimpleType)
6. de: sig()
7. closed_rel(mk_rel(relname_other(y), r1))
8. ||de.rel(y)|| = ||r1||
9. i:. i < ||r1|| (de.rel(y))[i] term_types(ds;da1;de;r1[i])
10. i:. closed_rel(mk_rel(relname_other(y), r1)) i < ||r1|| closed_term(r1[i])
11. i:
12. i < ||r1||
(de.rel(y))[i] term_types(ds;da2;de;r1[i])

About:
natural_numberless_thanapplyimpliesall

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