(20steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc

At: tc ioa inv vc 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))* > +* ioa_trans_all{i}(A;I)

tc_vc(v;A.ds;A.da;de)
By:
Unfolds [`vcs_singleton`;`vcs_add`] -1
THEN
RW ColMemberC -1
THEN
Analyze -1
Generated subgoals:

110. v = vc_imp(mk_imp(A.init, I))
tc_vc(v;A.ds;A.da;de)
210. v ioa_trans_all{i}(A;I)
tc_vc(v;A.ds;A.da;de)

(20steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc