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

At: rel mng 2 lemma


ds,da:Collection(dec()), de:sig(), rho:Decl, st1:Collection(SimpleType), e1:{1of([[de]] rho)} , s,s':{[[ds]] rho}, a:[[st1]] rho, tr:trace_env([[da]] rho), l:Term List. (i:||l||. trace_consistent(rho;da;tr.proj;l[i])) (ls:SimpleType List, f:reduce(s,m. [[s]] rhom;Prop;ls). ||ls|| = ||l|| & (i:. i < ||l|| ls[i] term_types(ds;st1;de;l[i])) list_accum(x,t.x([[t]] e1 s s' a tr);f;l) Prop)

By: RepeatFor 10 (Analyze 0)

Generated subgoal:

11. ds: Collection(dec())
2. da: Collection(dec())
3. de: sig()
4. rho: Decl
5. st1: Collection(SimpleType)
6. e1: {1of([[de]] rho)}
7. s: {[[ds]] rho}
8. s': {[[ds]] rho}
9. a: [[st1]] rho
10. tr: trace_env([[da]] rho)
l:Term List. (i:||l||. trace_consistent(rho;da;tr.proj;l[i])) (ls:SimpleType List, f:reduce(s,m. [[s]] rhom;Prop;ls). ||ls|| = ||l|| & (i:. i < ||l|| ls[i] term_types(ds;st1;de;l[i])) list_accum(x,t.x([[t]] e1 s s' a tr);f;l) Prop)


About:
listnatural_numberless_thanlambdaapply
functionequalmemberpropimplies
all

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