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

At: covers pred lemma2 1 2 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)

as:(LabelTerm) List. 1of(unzip(as)) = rel_primed_vars(r) & (i:. i < ||as|| 2of(as[i]) smts_eff(action_effect(a;A.eff;A.frame);1of(as[i])))
By: Assert (x:Label. t:Term. (x rel_primed_vars(r)) t smts_eff(action_effect(a;A.eff;A.frame);x))
Generated subgoals:

1 x:Label. t:Term. (x rel_primed_vars(r)) t smts_eff(action_effect(a;A.eff;A.frame);x)
27. x:Label. t:Term. (x rel_primed_vars(r)) t smts_eff(action_effect(a;A.eff;A.frame);x)
as:(LabelTerm) List. 1of(unzip(as)) = rel_primed_vars(r) & (i:. i < ||as|| 2of(as[i]) smts_eff(action_effect(a;A.eff;A.frame);1of(as[i])))

About:
productlistless_thanequalimpliesandallexists

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