(LabelTerm) List

LabelTerm

(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 < ||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))

i:. i < ||[u / v]|| 2of([u / v][i]) smts_eff(action_effect(k;A.eff;A.frame);1of([u / v][i]))

mk_dec(x, t) A.ds

1of(u) = x

(e:eff(). e A.eff & e.kind = k & s = e.smt) (f:frame(). f A.frame & k f.acts & s = mk_smt(f.var, f.var, f.typ))

s.lbl = x

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

1

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))

2

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. f: frame() 20. f A.frame 21. k f.acts 22. s = mk_smt(f.var, f.var, f.typ) 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))

About: