Nuprl - Pf effect_subst_mentions

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

1. A: ioa{i:l}()
2. as: (LabelTerm) List
3. k: Label
4. ioa_mentions_trace(A)
5. i:. i < ||as|| 2of(as[i]) smts_eff(action_effect(k;A.eff;A.frame);1of(as[i]))

subst_mentions_trace(as)

By: ParallelOp -2 THEN RWO "assert_subst_mentions_trace" -1 THEN ExRepD THEN InstWithVar -2 -3

Generated subgoal:

1 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. 2of(as[i]) smts_eff(action_effect(k;A.eff;A.frame);1of(as[i]))
ioa_mentions_trace(A)

About:

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