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

At: tc ioa inv vc 1 2 2
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. a: dec()
11. a A.da
12. v = ioa_trans(A;a.lbl;I)

tc_vc(ioa_trans(A;a.lbl;I);A.ds;A.da;de)
By:
Thin -1
THEN
Unfolds [`tc_vc`;`ioa_trans`] 0
THEN
Reduce 0
THEN
Analyze 0
Generated subgoals:

1 tc_pred(I action_pre(a.lbl;A.pre);A.ds;dec_lookup(A.da;a.lbl);de)
2 tc_pred(smts_eff_pred(action_effect(a.lbl;A.eff;A.frame);I);A.ds;dec_lookup(A.da;a.lbl);de)

About:
equal

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