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

At: rel subst tc 1 1 2 1 1
1. x: SimpleType
2. r1: Term List
3. as: (LabelTerm) List
4. ds: Collection(dec())
5. da: Collection(SimpleType)
6. de: sig()
7. ||r1|| = 2
8. x term_types(ds;da;de;r1[0])
9. x term_types(ds;da;de;r1[1])
10. x@0:Label. (x@0 rel_vars( < inl(x),r1 > )) (t:SimpleType. mk_dec(x@0, t) ds t term_types(ds;da;de;apply_alist(as;x@0;x@0)))
11. ||r1|| = 2
12. x1: Label
13. (x1 term_vars(r1[0]))
14. t: SimpleType
15. mk_dec(x1, t) ds

i:. i < ||r1|| & (x1 term_vars(r1[i]))
By: InstConcl [0]
Generated subgoals:

None

About:
pairproductlistintnatural_numberless_thaninlequalimpliesallexists

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