At:
rel effect lemma
1
1
2
2
1
1
2
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.
rel_eq(rel_unprime(r);rel_unprime(r0))
13.
2of(unzip(as)) = map(
x.x;1of(unzip(as)))
14.
i:
15.
i < ||as||
16.
s: smt()
17.
f: frame()
18.
f A.frame
19.
kind(act) f.acts
20.
s = mk_smt(f.var, f.var, f.typ)
21.
f.var =
1of(as[i])
22.
2of(as[i]) = f.var
f.var = 1of(as[i])
By:
EqLblFwd
THEN
Analyze
Generated subgoals:
None
About:
