Nuprl - Pf tc ioa lemma 2 1 2 1 1 1 1 1 1 1

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

At: tc ioa lemma 2 1 2 1 1 1 1 1 1 1

1. as: (LabelTerm) List
2. u: LabelTerm
3. v: (LabelTerm) List
4. A:ioa{i:l}(), de:sig(), x:Label, t:SimpleType, k:Label. single_valued_decls(A.ds) tc_ioa(A;de) (i:. i < ||v|| 2of(v[i]) smts_eff(action_effect(k;A.eff;A.frame);1of(v[i]))) mk_dec(x, t) A.ds t term_types(A.ds;dec_lookup(A.da;k);de;apply_alist(v;x;x))
5. A: ioa{i:l}()
6. de: sig()
7. x: Label
8. t: SimpleType
9. k: Label
10. single_valued_decls(A.ds)
11. tc_pred(A.init;A.ds; < > ;de)
12. p:pre(). p A.pre tc(p.rel;A.ds;dec_lookup(A.da;p.kind);de)
13. ef:eff(). ef A.eff mk_dec(ef.kind, ef.typ) A.da & tc_eff(ef;A.ds;de)
14. f:frame(). f A.frame mk_dec(f.var, f.typ) A.ds
15. i:. i < ||[u / v]|| 2of([u / v][i]) smts_eff(action_effect(k;A.eff;A.frame);1of([u / v][i]))
16. mk_dec(x, t) A.ds
17. 1of(u) = x
18. s: smt()
19. e: eff()
20. e A.eff
21. e.kind = k
22. s = e.smt
23. s.lbl = x
24. 2of(u) = s.term
25. 1of(u) = x

t term_types(A.ds;dec_lookup(A.da;k);de;2of(u))

By: AllHyps (i.(Unfold `tc_eff` i) THEN (InstHyp [e] i)) THEN Unfold `tc_smt` -1 THEN RepD

Generated subgoal:

1 13. ef:eff(). ef A.eff mk_dec(ef.kind, ef.typ) A.da & tc_smt(ef.smt;A.ds; < ef.typ > ;de)
14. f:frame(). f A.frame mk_dec(f.var, f.typ) A.ds
15. i:. i < ||[u / v]|| 2of([u / v][i]) smts_eff(action_effect(k;A.eff;A.frame);1of([u / v][i]))
16. mk_dec(x, t) A.ds
17. 1of(u) = x
18. s: smt()
19. e: eff()
20. e A.eff
21. e.kind = k
22. s = e.smt
23. s.lbl = x
24. 2of(u) = s.term
25. 1of(u) = x
26. mk_dec(e.kind, e.typ) A.da
27. mk_dec(e.smt.lbl, e.smt.typ) A.ds
28. e.smt.typ term_types(A.ds; < e.typ > ;de;e.smt.term)
t term_types(A.ds;dec_lookup(A.da;k);de;2of(u))

About:

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