At:
rel effect lemma
1
1
1
1
1
2
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)))
unprime(apply_alist(as;x;x)) = x
By:
Subst (apply_alist(as;x;x) = x) 0
Generated subgoals:
1 | apply_alist(as;x;x) = x |
2 | unprime(x) = x |
About: