Nuprl - Pf tc wp 1 1

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

At: tc wp 1 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)
8. 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)

By: (((Unfold `smts_eff_pred` -1) THEN (Using [`T',rel()] (FwdThru Thm* c:Collection(T), f:(TCollection(T')), y:T'. y (xc.f(x)) (x:T. x c & y f(x)) [-1]))) THEN ExRepD THEN (Unfold `smts_eff_rel` -1) THEN (RWW "member_col_subst" -1) THEN ExRepD THEN (HypSubst -1 0)) THENA (Auto THEN (Try (Fold `pred` 0)))

Generated subgoal:

1 9. r (rQ.smts_eff_rel(action_effect(a;A.eff;A.frame);r))
10. r1: rel()
11. r1 Q
12. as: (LabelTerm) List
13. 1of(unzip(as)) = rel_vars(r1)
14. i:. i < ||as|| 2of(as[i]) (x.smts_eff(action_effect(a;A.eff;A.frame);x))(1of(as[i]))
15. r = rel_subst(as;r1)
tc(rel_subst(as;r1);A.ds;dec_lookup(A.da;a);de)

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