Nuprl - Pf effect_subst_mentions_trace 1 1 1 2

(7steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc

At: effect subst mentions trace 1 1 1 2

1. A: ioa{i:l}()
2. as: (LabelTerm) 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. f:frame(). f A.frame & k f.acts & s = mk_smt(f.var, f.var, f.typ)
9. s.lbl = 1of(as[i])
10. 2of(as[i]) = s.term

e:eff(). e A.eff & mentions_trace(e.smt.term)

By: ExRepD THEN Assert (mentions_trace(2of(as[i]))) THEN SubstFor 2of(as[i]) 0 THEN SubstFor s 0

Generated subgoal:

1 8. f: frame()
9. f A.frame
10. k f.acts
11. s = mk_smt(f.var, f.var, f.typ)
12. s.lbl = 1of(as[i])
13. 2of(as[i]) = s.term
mentions_trace(mk_smt(f.var, f.var, f.typ).term)

About:

(7steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc