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

At: wp2 addprime

A:ioa{i:l}(), a:Label, P:Fmla. wp2(A;a;(P)') = wp(A;a;P)
By:
Auto
THEN
Unfolds [`col_equal`;`wp2`;`wp`] 0
THEN
Unfold `smts_eff_pred` 0
THEN
Unfold `smts_eff_rel` 0
THEN
RW ColMemberC 0
Generated subgoal:

11. 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))

About:
lambdaandallexists

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