Nuprl - Pf trace consistent wp2 1

(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)

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

By: Assert (r:rel(). r Q trace_consistent_pred(rho;A.da;R;wp2_rel(A;k;r)))

Generated subgoals:

1 r:rel(). r Q trace_consistent_pred(rho;A.da;R;wp2_rel(A;k;r))

2 8. r:rel(). r Q trace_consistent_pred(rho;A.da;R;wp2_rel(A;k;r))
trace_consistent_pred(rho;A.da;R;wp2(A;k;Q))

About:

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

1	`r:rel(). r Q trace_consistent_pred(rho;A.da;R;wp2_rel(A;k;r))`
2	8. `r:rel(). r Q trace_consistent_pred(rho;A.da;R;wp2_rel(A;k;r))` `trace_consistent_pred(rho;A.da;R;wp2(A;k;Q))`