At:
tc ioa inv vc
2
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}()
( < *vc_imp(mk_imp(A.init, I))* > {i} +* ioa_trans_all{i}(A;I)) 
Collection{i'}(vc{i:l}())
By:
Fold `vcs` 0
Generated subgoals:
None
About:
