PrintForm Definitions mb automata 3 Sections GenAutomata Doc

At: no mention implies consistent term


rho:Decl, t:Term, da:Collection(dec()), R:(LabelLabel). mentions_trace(t) trace_consistent(rho;da;R;t)

By:
Auto
THEN
Unfold `trace_consistent` 0
THEN
Analyze -3
THEN
Easy


Generated subgoals:

None


About:
boolassertfunctionimpliesall

PrintForm Definitions mb automata 3 Sections GenAutomata Doc