Nuprl - Pf trace consistent wp 1 2

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

1. A: ioa{i:l}()
2. Q: Fmla
3. rho: Decl
4. R: LabelLabel
5. k: Label
6. ioa_mentions_trace(A)
7. trace_consistent_pred(rho;A.da;R;Q)
8. r:rel(). r Q trace_consistent_pred(rho;A.da;R;wp_rel(A;k;r))

trace_consistent_pred(rho;A.da;R;wp(A;k;Q))

By: Unfold `trace_consistent_pred` 0 THEN Unfold `col_all` 0

Generated subgoals:

1 9. r: rel()
10. r wp(A;k;Q)
trace_consistent_rel(rho;A.da;R;r)

2 9. r: rel()
wp(A;k;Q) Collection(rel())

About:

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

1	9. `r:` `rel()` 10. `r wp(A;k;Q)` `trace_consistent_rel(rho;A.da;R;r)`
2	9. `r:` `rel()` `wp(A;k;Q) Collection(rel())`