At:
tc ioa inv vc
1
1
1.
A: ioa{i:l}()
2.
I: Fmla
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 = vc_imp(mk_imp(A.init, I))
tc_vc(v;A.ds;A.da;de)
By:
HypSubst -1 0
THEN
Unfold `tc_vc` 0
THEN
Reduce 0
THEN
All (Unfold `tc_ioa`)
Generated subgoals:
None
About:
