At:
rel effect lemma
1
1
1
1
1
1
1
2
1
1.
A: ioa{i:l}()
2.
rho: Decl
3.
de: sig()
4.
act: (
[[A.da]] rho)
5.
r: rel()
6.
r0: rel()
7.
tc_ioa(A;de)
8.
as: (Label
Term) List
9.
1of(unzip(as)) = rel_vars(r0)
10.
i:
. i < ||as|| 
2of(as[i]) 
smts_eff(action_effect(kind(act);A.eff;A.frame);1of(as[i]))
11.
r = rel_subst(as;r0)
12.
2of(unzip(as)) = map(
x.x;1of(unzip(as)))
13.
x: Label
14.
(x 1of(unzip(as)))
15.
i:
16.
i < ||as||
17.
< x,apply_alist(as;x;x) > = as[i]
18.
x = 1of(as[i])
19.
apply_alist(as;x;x) = 2of(as[i])
20.
2of( < map(p.1of(p);as),map(p.2of(p);as) > )[i]
=
map(x.x;1of( < map(p.1of(p);as),map(p.2of(p);as) > ))[i]
i < ||1of( < map(p.1of(p);as),map(p.2of(p);as) > )||
By:
Reduce 0
THEN
RWW "map_length" 0
Generated subgoals:
None
About:
