Nuprl - Pf no_mention_implies_consistent

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

rho:Decl, r:rel(), da:Collection(dec()), R:(LabelLabel). rel_mentions_trace(r) trace_consistent_rel(rho;da;R;r)

By: Auto THEN Unfold `trace_consistent_rel` 0 THEN Unfold `trace_consistent` 0 THEN Analyze -4

Generated subgoal:

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)

About:

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