(3steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

At: no mention implies consistent rel 1 1
1. rho: Decl
2. r: rel()
3. da: Collection(dec())
4. R: LabelLabel
5. i: ||r.args||
6. g: Label
7. term_mentions_guard(g;r.args[i])

mentions_trace(r.args[i])
By: Easy
Generated subgoals:

None

About:
boolassertnatural_numberfunction

(3steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc