(16steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc

At: rel mng wf 1 1 2 1 1
1. y: Label
2. r1: Term List
3. ds: Collection(dec())
4. da: Collection(dec())
5. de: sig()
6. rho: Decl
7. st1: Collection(SimpleType)
8. e1: {1of([[de]] rho)}
9. e2: l:Labelreduce(s,m. [[s]] rhom;Prop;de.rel(l))
10. s: {[[ds]] rho}
11. a: [[st1]] rho
12. tr: trace_env([[da]] rho)
13. trace_consistent_rel(rho;da;tr.proj; < inr(y),r1 > )
14. l: Term List
15. r1 = l
16. ||de.rel(y)|| = ||l||
17. i:. i < ||l|| (de.rel(y))[i] term_types(ds;st1;de;l[i])

list_accum(x,t.x([[t]] e1 s a tr);e2.y;l) Prop
By: GenConcl (e2.y = f)
Generated subgoals:

1 e2.y reduce(s,m. [[s]] rhom;Prop;de.rel(y))
218. f: reduce(s,m. [[s]] rhom;Prop;de.rel(y))
19. e2.y = f
list_accum(x,t.x([[t]] e1 s a tr);f;l) Prop

About:
pairlistless_thaninrlambdaapply
functionequalmemberpropimplies
all

(16steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc