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

At: no mention implies consistent rel 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])

rel_mentions_trace(r)
By:
BackThru Thm* r:rel(). rel_mentions_trace(r) (i:. i < ||r.args|| & mentions_trace(r.args[i]))
THEN
InstConcl [i]
Generated subgoal:

1 mentions_trace(r.args[i])

About:
boolassertnatural_numberfunction

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