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

At: tproj w f 1 1 1 2
1. da: Collection(dec())
2. rho: Decl
3. tr: trace_env([[da]] rho)
4. y1: Label
5. L: ([[da]] rho) List
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
By: SplitOnConclITE
Generated subgoals:

None

About:
listconsifthenelseassertsetlambdaapplymember

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