PrintForm Definitions mb events Sections GenAutomata Doc

At: trace projection cons

a,tr,P:Top. [a / tr] | P ~ if P(kind(a)) [a / tr | P] else tr | P fi
By:
Unfold `trace_projection` 0
THEN
Reduce 0
THEN
Reduce 0
THEN
Fold `trace_projection` 0
Generated subgoals:

None

About:
consifthenelseapplysqequaltopall

PrintForm Definitions mb events Sections GenAutomata Doc