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

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

r':rel(). r' col_subst2(x.smts_eff(action_effect(a;A.eff;A.frame);x);r)
By: Assert (x:Label. rel_mentions(r;x) covers_var(A;x))
Generated subgoals:

1 x:Label. rel_mentions(r;x) covers_var(A;x)
27. x:Label. rel_mentions(r;x) covers_var(A;x)
r':rel(). r' col_subst2(x.smts_eff(action_effect(a;A.eff;A.frame);x);r)

About:
lambdaimpliesandallexists

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