(40steps)
PrintForm
Definitions
Lemmas
mb
automata
4
Sections
GenAutomata
Doc
At:
rel
effect
lemma
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)))
rel_eq(rel_unprime(rel_subst(as;r0));rel_unprime(r0))
By:
RWW "assert_rel_eq" 0
THEN
BackThru
Thm*
r:rel(), as:(Label
Term) List. (
x:Label. unprime(apply_alist(as;x;x)) = x)
rel_unprime(rel_subst(as;r)) = rel_unprime(r)
Generated subgoal:
1
13.
x:
Label
unprime(apply_alist(as;x;x)) = x
About:
(40steps)
PrintForm
Definitions
Lemmas
mb
automata
4
Sections
GenAutomata
Doc