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

At: term subst tc 1
1. t: Term
2. u: TermType{i'}
3. w: t:{v:Term| u(v) }s:SimpleType, as:(LabelTerm) List, ds:Collection{i}(dec()) , da:Collection{i}(SimpleType), de:sig(). s term_types(ds;da;de;t) (x:Label. (x term_vars(t)) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))) s term_types(ds;da;de;term_subst(as;t))
4. x: Label

s:SimpleType, as:(LabelTerm) List, ds:Collection{i}(dec()), da:Collection{i}(SimpleType) , de:sig(). s dec_lookup(ds;x) (x@0:Label. (x@0 [x]) (t:SimpleType. mk_dec(x@0, t) ds t term_types(ds;da;de;apply_alist(as;x@0;x@0)))) s term_types(ds;da;de;apply_alist(as;x;x'))
By:
Auto
THEN
Subst (term_types(ds;da;de;apply_alist(as;x;x')) ~ term_types(ds;da;de;apply_alist(as;x;x))) 0
Generated subgoals:

15. s: SimpleType
6. as: (LabelTerm) List
7. ds: Collection{i}(dec())
8. da: Collection{i}(SimpleType)
9. de: sig()
10. s dec_lookup(ds;x)
11. x@0:Label. (x@0 [x]) (t:SimpleType. mk_dec(x@0, t) ds t term_types(ds;da;de;apply_alist(as;x@0;x@0)))
term_types(ds;da;de;apply_alist(as;x;x')) ~ term_types(ds;da;de;apply_alist(as;x;x))
25. s: SimpleType
6. as: (LabelTerm) List
7. ds: Collection{i}(dec())
8. da: Collection{i}(SimpleType)
9. de: sig()
10. s dec_lookup(ds;x)
11. x@0:Label. (x@0 [x]) (t:SimpleType. mk_dec(x@0, t) ds t term_types(ds;da;de;apply_alist(as;x@0;x@0)))
s term_types(ds;da;de;apply_alist(as;x;x))

About:
productlistconsnilsetapply
functionuniversesqequalimpliesall

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