Nuprl - Pf tproj_w

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

1. da: Collection(dec())
2. rho: Decl
3. tr: trace_env([[da]] rho)
4. y1: Label
5. L: ([[da]] rho) List
6. tr.trace = L

filter(x.tr.proj(y1,kind(x));L) {a:([[da]] rho)| tr.proj(y1,kind(a)) } List

By: Thin -1 THEN ListInd -1 THEN Reduce 0

Generated subgoals:

1 nil {a:([[da]] rho)| tr.proj(y1,kind(a)) } List

2 6. u: ([[da]] rho)
7. v: ([[da]] rho) List
8. filter(x.tr.proj(y1,kind(x));v) {a:([[da]] rho)| tr.proj(y1,kind(a)) } List
if tr.proj(y1,kind(u)) [u / filter(x.tr.proj(y1,kind(x));v)] else filter(x.tr.proj(y1,kind(x));v) fi {a:([[da]] rho)| tr.proj(y1,kind(a)) } List

About:

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

1	`nil {a:([[da]] rho)\| tr.proj(y1,kind(a)) } List`
2	6. `u:` `([[da]] rho)` 7. `v:` `([[da]] rho) List` 8. `filter(x.tr.proj(y1,kind(x));v) {a:([[da]] rho)\| tr.proj(y1,kind(a)) } List` `if tr.proj(y1,kind(u)) [u / filter(x.tr.proj(y1,kind(x));v)] else filter(x.tr.proj(y1,kind(x));v) fi {a:([[da]] rho)\| tr.proj(y1,kind(a)) } List`