At:
rel effect lemma
1
1
1
1
1
1
1
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])
2of(unzip(as))[i] = map(x.x;1of(unzip(as)))[i]
By:
Analyze
Generated subgoal:
| 1 | i < ||2of(unzip(as))|| |
About:
