PrintForm Definitions mb automata 1 Sections GenAutomata Doc

At: ts case wf

A:Type, v,op,f,p,t:(LabelA), x:ts(). ts_case(x)var(a)= > v(a)var'(b)= > p(b)opr(f)= > op(f)fvar(y)= > f(y)trace(P)= > t(P)end_ts_case A
By:
Unfold `ts_case` 0
THEN
Repeat ((Analyze -1) THEN (Reduce 0) THEN (Try (Complete Auto)))
Generated subgoals:

None

About:
functionuniversememberall

PrintForm Definitions mb automata 1 Sections GenAutomata Doc