Nuprl - Pf trace consistent wp2 rel 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)

trace_consistent_pred(rho;A.da;R;wp2_rel(A;k;r))

By: Unfold `trace_consistent_pred` 0 THEN Unfolds [`col_all`;`wp2_rel`] 0 THEN Try (Fold `pred` 0)

Generated subgoal:

1 8. r@0: rel()
9. r@0 col_subst2(x.smts_eff(action_effect(k;A.eff;A.frame);x);r)
trace_consistent_rel(rho;A.da;R;r@0)

About:

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