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

At: tc wp 1
1. A: ioa{i:l}()
2. Q: Fmla
3. de: sig()
4. a: Label
5. tc_ioa(A;de)
6. single_valued_decls(A.ds)
7. tc_pred(Q;A.ds;dec_lookup(A.da;a);de)

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

18. r: rel()
9. r smts_eff_pred(action_effect(a;A.eff;A.frame);Q)
tc(r;A.ds;dec_lookup(A.da;a);de)

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