At:
tc ioa inv vc122112
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 action_pre(a.lbl;A.pre)
tc(r;A.ds;dec_lookup(A.da;a.lbl);de)
By:
Unfold `action_pre` -1
THEN
RWW "member_col_map" -1
THEN
RWW "member_col_filter" -1
THEN
ExRepD
THEN
SubstFor r 0
Generated subgoal: