Nuprl - Pf tc wp2 1 1 1 2

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

At: tc wp2 1 1 1 2

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)
8. r: rel()
9. r (rQ.col_subst2(x.smts_eff(action_effect(a;A.eff;A.frame);x);r))
10. r1: rel()
11. r1 Q
12. as: (LabelTerm) List
13. 1of(unzip(as)) = rel_primed_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_subst2(as;r1)
16. x: Label
17. (x rel_primed_vars(r1))
18. t: SimpleType
19. mk_dec(x, t) A.ds

t term_types(A.ds;dec_lookup(A.da;a);de;apply_alist(as;x;x))

By: BackThru Thm* as:(LabelTerm) List, A:ioa{i:l}(), de:sig(), x:Label, t:SimpleType, k:Label. single_valued_decls(A.ds) tc_ioa(A;de) (i:. i < ||as|| 2of(as[i]) smts_eff(action_effect(k;A.eff;A.frame);1of(as[i]))) mk_dec(x, t) A.ds t term_types(A.ds;dec_lookup(A.da;k);de;apply_alist(as;x;x))

Generated subgoal:

1 20. i:
21. i < ||as||
2of(as[i]) smts_eff(action_effect(a;A.eff;A.frame);1of(as[i]))

About:

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