Nuprl - Pf tc wp2 1

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

At: tc wp2 1

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

tc_pred((rQ.col_subst2(x.smts_eff(action_effect(a;A.eff;A.frame);x);r));A.ds;dec_lookup(A.da;a);de)

By: ((Unfold `tc_pred` 0) THEN UnivCD) THENA (Auto THEN (Fold `pred` 0))

Generated subgoal:

1 8. r: rel()
9. r (rQ.col_subst2(x.smts_eff(action_effect(a;A.eff;A.frame);x);r))
tc(r;A.ds;dec_lookup(A.da;a);de)

About:

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