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