At:
tc ioa inv vc
1
2
1
1.
A: ioa{i:l}()
2.
I: Fmla{i}
3.
de: sig()
4.
tc_ioa(A;de)
5.
tc_pred(I;A.ds; < > ;de)
6.
covers_pred(A;I)
7.
closed_pred(I)
8.
single_valued_decls(A.ds)
9.
v: vc{i:l}()
10.
v 
< ioa_trans(A;a.lbl;I) | a A.da >
A ioa{i':l}
By:
BackThru
Thm* 
A:ioa{i:l}(). A ioa{i':l}
Generated subgoals:
None
About:
