structure DY.Label [ExecTraceTypes] : Type

• isCorrupt : ExecTrace → Prop
• isCorruptLater (tr1 tr2 : ExecTrace) : tr1 ≤ tr2 → self.isCorrupt tr1 → self.isCorrupt tr2

theorem DY.Label.isCorruptLater_grind [ExecTraceTypes] (l : Label) (tr1 tr2 : ExecTrace) : tr1 ≤ tr2 → l.isCorrupt tr1 → l.isCorrupt tr2

theorem DY.Label.ext [ExecTraceTypes] (l1 l2 : Label) : (∀ (tr : ExecTrace), l1.isCorrupt tr = l2.isCorrupt tr) → l1 = l2

theorem DY.Label.ext_iff [ExecTraceTypes] {l1 l2 : Label} : l1 = l2 ↔ ∀ (tr : ExecTrace), l1.isCorrupt tr = l2.isCorrupt tr

def DY.Label.canFlow [ExecTraceTypes] (l1 l2 : Label) (tr : ExecTrace) : Prop

Equations

• l1.canFlow l2 tr = ∀ (trLater : DY.ExecTrace), tr ≤ trLater → l2.isCorrupt trLater → l1.isCorrupt trLater

theorem DY.Label.canFlowLater [ExecTraceTypes] (l1 l2 : Label) (tr1 tr2 : ExecTrace) : tr1 ≤ tr2 → l1.canFlow l2 tr1 → l1.canFlow l2 tr2

theorem DY.canFlowRefl [ExecTraceTypes] (l : Label) (tr : ExecTrace) : l.canFlow l tr

theorem DY.canFlowTrans [ExecTraceTypes] (l1 l2 l3 : Label) (tr : ExecTrace) : l1.canFlow l2 tr → l2.canFlow l3 tr → l1.canFlow l3 tr

@[reducible, inline]

abbrev DY.Label.equivalent [ExecTraceTypes] (l1 l2 : Label) (tr : ExecTrace) : Prop

Equations

• l1.equivalent l2 tr = (l1.canFlow l2 tr ∧ l2.canFlow l1 tr)