At:
rel effect lemma
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)))
||2of(unzip(as))|| = ||map(x.x;1of(unzip(as)))||
By:
Unfold `unzip` 0
THEN
Reduce 0
THEN
RWW "map_length_nat" 0
Generated subgoals:
None
About:
