class DY.SubAttackerKnowledgeTheorem [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] {SubF : Type → Type} (att : SubAttackerKnowledge SubF) : Prop

• pf (b : Bytes) (tr : ProofTrace) : Trace.Invariant tr → att.pred (fun (x : Bytes) => x.Publishable tr) b → b.Publishable tr

class DY.AttackerKnowledgeTheorem [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] [AttackerKnowledge] : Prop

• inst : SubAttackerKnowledgeTheorem AttackerKnowledge.attackerKnowledge

instance DY.instSubAttackerKnowledgeTheoremCombine' [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] {SubF : Type → Type} {n : Nat} (atts : Fin n → SubAttackerKnowledge SubF) [pfs : ∀ (id : Fin n), SubAttackerKnowledgeTheorem (atts id)] : SubAttackerKnowledgeTheorem (SubAttackerKnowledge.combine' atts)

instance DY.instSubAttackerKnowledgeTheoremCombineCombine [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] {n : Nat} {SubFs : Fin n → Type → Type} (atts : (id : Fin n) → SubAttackerKnowledge (SubFs id)) [pfs : ∀ (id : Fin n), SubAttackerKnowledgeTheorem (atts id)] : SubAttackerKnowledgeTheorem (SubAttackerKnowledge.combine atts)

theorem DY.Bytes.AttackerKnows_implies_Publishable [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] [BytesInvariantsProofs] [AttackerKnowledge] [BaseAttackerKnowledge] [inst : AttackerKnowledgeTheorem] [BaseAttackerKnowledgeTheorem] (b : Bytes) (tr : ProofTrace) : Trace.Invariant tr → b.AttackerKnows (Trace.erase tr) → b.Publishable tr