At:
tc ioa lemma
1
1
1.
as: (Label
Term) List
A:ioa{i:l}(), de:sig(), x:Label, t:SimpleType, k:Label. single_valued_decls(A.ds) 
tc_ioa(A;de) 
(
i:
. i < 0 
2of(nil[i])
smts_eff(action_effect(k;A.eff;A.frame);1of(nil[i]))) 
mk_dec(x, t)
A.ds 
t
dec_lookup(A.ds;x)
By:
RWW "member_dec_lookup" 0
Generated subgoals:
None
About: