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

At: trace consistent wp2

A:ioa{i:l}(), Q:Fmla, rho:Decl, R:(LabelLabel), k:Label. ioa_mentions_trace(A) trace_consistent_pred(rho;A.da;R;Q) trace_consistent_pred(rho;A.da;R;wp2(A;k;Q))
By: Auto
Generated subgoal:

11. 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))

About:
boolfunctionimpliesall

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