PrintForm Definitions mb automata 4 Sections GenAutomata Doc

At: tc vcs wf


vs:VCs{i}, ds,da:Collection{i}(dec()), de:sig(). tc_vcs{i}(vs;ds;da;de) Prop{i'}

By:
Unfold `tc_vcs` 0
THEN
Try (Fold `vcs` 0)


Generated subgoals:

None

About:
memberpropall

PrintForm Definitions mb automata 4 Sections GenAutomata Doc