(20steps)
PrintForm
Definitions
Lemmas
mb
automata
4
Sections
GenAutomata
Doc
At:
tc
ioa
inv
vc
1
2
2
1
1
1.
A:
ioa{i:l}()
2.
I:
Fmla
3.
de:
sig()
4.
tc_pred(A.init;A.ds; < > ;de)
5.
p:pre(). p
A.pre
tc(p.rel;A.ds;dec_lookup(A.da;p.kind);de)
6.
ef:eff(). ef
A.eff
mk_dec(ef.kind, ef.typ)
A.da & tc_eff(ef;A.ds;de)
7.
f:frame(). f
A.frame
mk_dec(f.var, f.typ)
A.ds
8.
r:rel(). r
I
tc(r;A.ds; < > ;de)
9.
covers_pred(A;I)
10.
r:rel(). r
I
closed_rel(r)
11.
single_valued_decls(A.ds)
12.
v:
vc{i:l}()
13.
a:
dec()
14.
a
A.da
15.
r:
rel()
16.
r
I
action_pre(a.lbl;A.pre)
tc(r;A.ds;dec_lookup(A.da;a.lbl);de)
By:
(((Unfold `pred_and` -1) THEN (RWW "member_col_add" -1)) THEN (Analyze -1)) THENA (Auto THEN (Try (Fold `pred` 0)))
Generated subgoals:
1
16.
r
I
tc(r;A.ds;dec_lookup(A.da;a.lbl);de)
2
16.
r
action_pre(a.lbl;A.pre)
tc(r;A.ds;dec_lookup(A.da;a.lbl);de)
About:
(20steps)
PrintForm
Definitions
Lemmas
mb
automata
4
Sections
GenAutomata
Doc