At:
tc ioa lemma
2
1
2
1
1
1
1
1
1
1
1
2
1
1.
as: (Label
Term) List
2.
u: Label
Term
3.
v: (Label
Term) 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_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)
2of(u) = e.smt.term
By:
SubstFor e.smt 0
Generated subgoals:
None
About: