Nuprl - Pf trace consistent wp rel 1 1

(4steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc

1. A: ioa{i:l}()
2. rho: Decl
3. r: rel()
4. R: LabelLabel
5. k: Label
6. ioa_mentions_trace(A)
7. trace_consistent_rel(rho;A.da;R;r)
8. r@0: rel()
9. r@0 smts_eff_rel(action_effect(k;A.eff;A.frame);r)

trace_consistent_rel(rho;A.da;R;r@0)

By: Unfold `smts_eff_rel` -1 THEN RWO "member_col_subst" -1 THEN ExRepD THEN HypSubstSq -1 0 THEN BackThru Thm* r:rel(), as:(LabelTerm) List, daa:Collection(dec()), rho:Decl, te:(LabelLabel). trace_consistent_rel(rho;daa;te;r) subst_mentions_trace(as) trace_consistent_rel(rho;daa;te;rel_subst(as;r))

Generated subgoal:

1 9. as: (LabelTerm) List
10. 1of(unzip(as)) = rel_vars(r)
11. i:. i < ||as|| 2of(as[i]) (x.smts_eff(action_effect(k;A.eff;A.frame);x))(1of(as[i]))
12. r@0 = rel_subst(as;r)
subst_mentions_trace(as)

About:

(4steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc