At:
tc ioa inv vc
1
2
2
1
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
tc(r;A.ds;dec_lookup(A.da;a.lbl);de)
By:
InstHyp [r] -9
THEN
InstHyp [r] -8
THEN
Using [`da1', < > ]
(BackThru
Thm*
r:rel(), ds:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(). closed_rel(r) 
tc(r;ds;da1;de) 
tc(r;ds;da2;de))
Generated subgoals:
None
About: