Properties of the monadic CFG interpreter's definitions #
CFG.allCmds_of_mem: a CFG each of whose listed blocks has only commands passing a checkqsatisfiesCFG.allCmds q.
theorem
Imperative.CFG.allCmds_of_mem
{l CmdT : Type}
{P : PureExpr}
[BEq l]
[LawfulBEq l]
{q : CmdT → Bool}
{g : CFG l (DetBlock l CmdT P)}
(h : ∀ (lb : l × DetBlock l CmdT P), lb ∈ g.blocks → lb.snd.cmds.all q = true)
:
allCmds q g
A CFG each of whose listed blocks has only commands passing q satisfies CFG.allCmds q.