Nuprl - Pf trace consistent wp 1 2 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)
8. r:rel(). r Q trace_consistent_pred(rho;A.da;R;wp_rel(A;k;r))
9. r: rel()
10. r wp(A;k;Q)

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

By: Unfold `wp` -1 THEN Unfold `smts_eff_pred` -1 THEN RW ColMemberC -1 THEN ExRepD THEN Fold `wp_rel` -1

Generated subgoal:

1 10. r@0: rel()
11. r@0 Q
12. r wp_rel(A;k;r@0)
trace_consistent_rel(rho;A.da;R;r)

About:

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