At: tc closed rel 1 3 1
1. 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||
13. closed_term(r1[i])
14. term_types(ds;da2;de;r1[i]) = term_types(ds;da1;de;r1[i])
(de.rel(y))[i] term_types(ds;da1;de;r1[i])
By: SmAuto
Generated subgoals:None
About:
