(51steps)
PrintForm
Definitions
Lemmas
mb
automata
4
Sections
GenAutomata
Doc
At:
vc
trace
correct
action
decl
lemma
1
1
1.
A:
ioa{i:l}()
2.
I:
Fmla
3.
rho:
Decl
4.
de:
sig()
5.
e:
{[[de]] rho}
6.
te:
Label
Label
7.
tc_ioa(A;de)
8.
ioa_mentions_trace(A)
9.
trace_consistent_pred(rho;A.da;te;I)
10.
tc_pred(I;A.ds; < > ;de)
11.
covers_pred(A;I)
12.
guarded_trace(A.da;te;I)
13.
closed_pred(I)
14.
single_valued_decls(A.ds)
15.
s0:
[[A]] rho de e.state
16.
x:
[[A]] rho de e.state
17.
act:
[[A]] rho de e.action
18.
x':
[[A]] rho de e.state
19.
tr:
(
[[A.da]] rho) List
20.
[[A]] rho de e.init(s0)
21.
trace_reachable([[A]] rho de e;s0;mk_trace_env(tr, te).trace;x)
22.
[[I]] rho A.ds < > de e x
mk_trace_env(tr, te)
23.
[[A]] rho de e.trans(x,act,x')
24.
(
t:dec(). t
A.da & t.lbl = kind(act))
[[I]] rho A.ds < > de e x'
tappend(mk_trace_env(tr, te);act)
[[wp(A;kind(act);I)]] rho A.ds dec_lookup(A.da;kind(act)) de e x value(act) tappend(mk_trace_env(tr, te);act)
[[I]] rho A.ds < > de e x'
tappend(mk_trace_env(tr, te);act)
By:
Assert (act
(
[[A.da]] rho))
Generated subgoals:
1
act
(
[[A.da]] rho)
2
25.
act
(
[[A.da]] rho)
[[wp(A;kind(act);I)]] rho A.ds dec_lookup(A.da;kind(act)) de e x value(act) tappend(mk_trace_env(tr, te);act)
[[I]] rho A.ds < > de e x'
tappend(mk_trace_env(tr, te);act)
About:
(51steps)
PrintForm
Definitions
Lemmas
mb
automata
4
Sections
GenAutomata
Doc