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

At: tc ioa inv vc 1 2 2 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. a: dec()
11. a A.da

tc_pred(I action_pre(a.lbl;A.pre);A.ds;dec_lookup(A.da;a.lbl);de)
By: ((All (Unfolds [`tc_ioa`;`tc_pred`;`closed_pred`])) THEN ExRepD) THENA (Auto THEN (Try (Fold `pred` 0)))
Generated subgoal:

14. tc_pred(A.init;A.ds; < > ;de)
5. p:pre(). p A.pre tc(p.rel;A.ds;dec_lookup(A.da;p.kind);de)
6. ef:eff(). ef A.eff mk_dec(ef.kind, ef.typ) A.da & tc_eff(ef;A.ds;de)
7. f:frame(). f A.frame mk_dec(f.var, f.typ) A.ds
8. r:rel(). r I tc(r;A.ds; < > ;de)
9. covers_pred(A;I)
10. r:rel(). r I closed_rel(r)
11. single_valued_decls(A.ds)
12. v: vc{i:l}()
13. a: dec()
14. a A.da
15. r: rel()
16. r I action_pre(a.lbl;A.pre)
tc(r;A.ds;dec_lookup(A.da;a.lbl);de)

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