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

At: covers pred lemma2 1 2 1 1 1 1 1 1
1. r: rel()
2. I: Collection(rel())
3. A: ioa{i:l}()
4. a: Label
5. r I
6. x:Label. (x rel_vars(r)) covers_var(A;x)
7. x: Label

(x rel_primed_vars(r)) (x rel_primed_vars(r))
By: ((Decide x rel_primed_vars(r)) THEN (RWW "assert_lbls_member" -1)) THENL [Sel 1 (Analyze 0);Sel 2 (Analyze 0)]
Generated subgoals:

None

About:
assertimpliesorall

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