(40steps)
PrintForm
Definitions
Lemmas
mb
automata
4
Sections
GenAutomata
Doc
At:
rel
effect
lemma
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))
t:dec(). t
A.da & t.lbl = kind(act)
By:
Decide termlist_eq(2of(unzip(as));map(
x.x;1of(unzip(as))))
THEN
RWW "assert_termlist_eq" -1
Generated subgoals:
1
13.
2of(unzip(as)) = map(
x.x;1of(unzip(as)))
t:dec(). t
A.da & t.lbl = kind(act)
2
13.
2of(unzip(as)) = map(
x.x;1of(unzip(as)))
t:dec(). t
A.da & t.lbl = kind(act)
About:
(40steps)
PrintForm
Definitions
Lemmas
mb
automata
4
Sections
GenAutomata
Doc