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

At: effect subst mentions trace

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)
By: Auto
Generated subgoal:

11. 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)

About:
productlistassertless_thanimpliesall

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