A:ioa{i:l}(), as:(Label
Term) List, k:Label.
ioa_mentions_trace(A) 
(i:
. i < ||as|| 2of(as[i]) 
smts_eff(action_effect(k;A.eff;A.frame);1of(as[i])))
subst_mentions_trace(as)
e:eff(). e A.eff & 
mentions_trace(e.smt.term))
(p:pre(). p A.pre & rel_mentions_trace(p.rel))
(r:rel(). r A.init & rel_mentions_trace(r))
is mentioned by
|
Thm* A:ioa{i:l}(), as:(LabelTerm) List, k:Label.
ioa_mentions_trace(A)
(i:. i < ||as|| 2of(as[i]) smts_eff(action_effect(k;A.eff;A.frame);1of(as[i])))
subst_mentions_trace(as) | [effect_subst_mentions_trace] |
Try larger context: GenAutomata