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

At: trace consistent init

A:ioa{i:l}(), rho:Decl, te:(LabelLabel). ioa_mentions_trace(A) trace_consistent_pred(rho;A.da;te;A.init)
By:
Unfold `trace_consistent_pred` 0
THEN
Unfold `col_all` 0
Generated subgoal:

11. A: ioa{i:l}()
2. rho: Decl
3. te: LabelLabel
4. ioa_mentions_trace(A)
5. r: rel()
6. r A.init
trace_consistent_rel(rho;A.da;te;r)

About:
boolfunctionimpliesall

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