At: effect subst mentions trace 1 1 1 1
1. A: ioa{i:l}()
2. as: (Label
Term) List
3. k: Label
4. 
i:
. i < ||as|| 
2of(as[i]) 
smts_eff(action_effect(k;A.eff;A.frame);1of(as[i]))
5. i: ||as||
6. mentions_trace(2of(as[i]))
7. s: smt()
8. 
e:eff(). e A.eff & e.kind =
k & s = e.smt
9. s.lbl = 1of(as[i])
10. 2of(as[i]) = s.term
e:eff(). e A.eff & mentions_trace(e.smt.term)
By:
ParallelOp -3
THEN
SubstFor e.smt 0
THEN
SubstFor s.term 0
Generated subgoals:None
About:
