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

At: rel mng 2 wf 1 1 1
1. x: SimpleType
2. r1: Term List
3. ds: Collection(dec())
4. da: Collection(dec())
5. de: sig()
6. rho: Decl
7. st1: Collection(SimpleType)
8. e: {[[de]] rho}
9. s: {[[ds]] rho}
10. s': {[[ds]] rho}
11. a: [[st1]] rho
12. tr: trace_env([[da]] rho)
13. trace_consistent_rel(rho;da;tr.proj; < inl(x),r1 > )
14. l: Term List
15. r1 = l
16. ||l|| = 2
17. x term_types(ds;st1;de;l[0])
18. x term_types(ds;st1;de;l[1])

list_accum(x,t.x([[t]] 1of(e) s s' a tr);[[relname_eq(x)]] rho 2of(e) ;l) Prop
By:
Using [`ls',[x; x];`da',da;`de',de] (BackThru Thm* 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))
THEN
Try ((Analyze 7) THEN (All Reduce) THEN Trivial)
THEN
Try ((Unfold `relname_mng` 0) THEN (Reduce 0))
THEN
Try ((Reduce 0) THEN ExRepD THEN (CaseNat 0 `i') THEN (Reduce 0) THEN (CaseNat 1 `i') THEN (Reduce 0))
Generated subgoals:

1 1of(e) {1of([[de]] rho)}
219. i: ||l||
20. i = 0
21. i = 1
trace_consistent(rho;da;tr.proj;l[0])
319. i: ||l||
20. i = 0
21. i = 1
trace_consistent(rho;da;tr.proj;l[1])

About:
pairlistconsnilintnatural_numberinlapplyequalmemberprop

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