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

At: tc ioa inv vc 1 2 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

tc_pred(smts_eff_pred(action_effect(a.lbl;A.eff;A.frame);I);A.ds;dec_lookup(A.da;a.lbl);de)
By: ((Unfold `tc_pred` 0) THEN UnivCD) THENA (Auto THEN (Fold `pred` 0))
Generated subgoal:

112. r: rel()
13. r smts_eff_pred(action_effect(a.lbl;A.eff;A.frame);I)
tc(r;A.ds;dec_lookup(A.da;a.lbl);de)

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