(14steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc

At: wp2 addprime 1
1. A: ioa{i:l}()
2. a: Label
3. P: Fmla

x:rel(). (r:rel(). r (P)' & x col_subst2(x.smts_eff(action_effect(a;A.eff;A.frame);x);r)) (r:rel(). r P & x col_subst(x.smts_eff(action_effect(a;A.eff;A.frame);x);r))
By:
Unfold `pred_addprime` 0
THEN
RW ColMemberC 0
THEN
RWW "member_col_subst" 0
THEN
RWW "member_col_subst2" 0
THEN
Auto
THEN
Try (Fold `pred` 0)
THEN
Reduce 0
Generated subgoals:

14. x: rel()
5. r:rel(). (r@0:rel(). r@0 P & r = (r@0)') & (as:(LabelTerm) List. 1of(unzip(as)) = rel_primed_vars(r) & (i:. i < ||as|| 2of(as[i]) (x.smts_eff(action_effect(a;A.eff;A.frame);x))(1of(as[i]))) & x = rel_subst2(as;r))
r:rel(). r P & (as:(LabelTerm) List. 1of(unzip(as)) = rel_vars(r) & (i:. i < ||as|| 2of(as[i]) smts_eff(action_effect(a;A.eff;A.frame);1of(as[i]))) & x = rel_subst(as;r))
24. x: rel()
5. r:rel(). r P & (as:(LabelTerm) List. 1of(unzip(as)) = rel_vars(r) & (i:. i < ||as|| 2of(as[i]) (x.smts_eff(action_effect(a;A.eff;A.frame);x))(1of(as[i]))) & x = rel_subst(as;r))
r:rel(). (r@0:rel(). r@0 P & r = (r@0)') & (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]))) & x = rel_subst2(as;r))

About:
productlistless_thanlambdaequalimpliesandallexists

(14steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc