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

At: trace consistent wp 1 1 1
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()
9. r Q

trace_consistent_pred(rho;A.da;R;wp_rel(A;k;r))
By:
BackThru Thm* A:ioa{i:l}(), rho:Decl, r:rel(), R:(LabelLabel), k:Label. ioa_mentions_trace(A) trace_consistent_rel(rho;A.da;R;r) trace_consistent_pred(rho;A.da;R;wp_rel(A;k;r))
THEN
EasyHypThen Auto
Generated subgoals:

None

About:
boolfunction

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