mb automata 4 Sections GenAutomata Doc

Def vc_hyp(v) == Case(v) Case vc_imp(x) = > x.hyp Case vc_qimp(x) = > x.hyp Default = > False

is mentioned by

Def trace_consistent_vc(rho;da;R;v) == trace_consistent_pred(rho;da;R;vc_hyp(v)) & trace_consistent_pred(rho;da;R;vc_concl(v))[trace_consistent_vc]

Try larger context: GenAutomata

mb automata 4 Sections GenAutomata Doc