At:
wp2 addprime
1
2
1
1
1.
A: ioa{i:l}()
2.
a: Label
3.
P: Fmla
4.
x: rel()
5.
r: rel()
6.
r 
P
7.
as: (Label
Term) List
8.
1of(unzip(as)) = rel_vars(r)
9.
i:
. i < ||as|| 
2of(as[i]) smts_eff(action_effect(a;A.eff;A.frame);1of(as[i]))
10.
x = rel_subst(as;r)
rel_vars(r) = rel_primed_vars((r)')
By:
RWO "rel_vars_addprime" 0
Generated subgoals:
None
About:
