@[instance_reducible]

def DY.Example.MerkleTree.SubF : Type → Type

Equations

• DY.Example.MerkleTree.SubF = DY.BytesFunctor.combine DY.Example.MerkleTree.SubF.internal

def DY.Example.MerkleTree.SubF.length.internal (id✝ : Fin 5) : Bytes.PartialLength (SubF.internal id✝)

Equations

• DY.Example.MerkleTree.SubF.length.internal 0 = DY.Literal.SubF.length
• DY.Example.MerkleTree.SubF.length.internal 1 = DY.Concat.SubF.length
• DY.Example.MerkleTree.SubF.length.internal 2 = DY.Hash.SubF.length
• DY.Example.MerkleTree.SubF.length.internal 3 = DY.Signature.SubF.length
• DY.Example.MerkleTree.SubF.length.internal 4 = DY.Random.SubF.length
• DY.Example.MerkleTree.SubF.length.internal ⟨n.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

instance DY.Example.MerkleTree.instHasSubF : BytesFunctor.Has SubF

Equations

• DY.Example.MerkleTree.instHasSubF = { toSubFunctorTC := DY.ALaCarte.instSubFunctorTC DY.Example.MerkleTree.SubF }

@[instance_reducible]

instance DY.Example.MerkleTree.instBytesLength_examples : BytesLength

Equations

• DY.Example.MerkleTree.instBytesLength_examples = { funs := DY.Example.MerkleTree.SubF.length }

@[instance_reducible]

instance DY.Example.MerkleTree.instBytesFunctor_examples : BytesFunctor

Equations

• DY.Example.MerkleTree.instBytesFunctor_examples = { BytesF := DY.Example.MerkleTree.SubF, inst := DY.Example.MerkleTree.wfInst✝ }

def DY.Example.MerkleTree.SubF.internal : Fin 5 → Type → Type

Equations

• DY.Example.MerkleTree.SubF.internal 0 = DY.Literal.SubF
• DY.Example.MerkleTree.SubF.internal 1 = DY.Concat.SubF
• DY.Example.MerkleTree.SubF.internal 2 = DY.Hash.SubF
• DY.Example.MerkleTree.SubF.internal 3 = DY.Signature.SubF
• DY.Example.MerkleTree.SubF.internal 4 = DY.Random.SubF
• DY.Example.MerkleTree.SubF.internal ⟨n.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

instance DY.Example.MerkleTree.instHasSubFAttackerKnowledge : AttackerKnowledge.Has attackerKnowledge

instance DY.Example.MerkleTree.instHasSubFLength : BytesLength.Has SubF.length

@[instance_reducible]

instance DY.Example.MerkleTree.instAttackerKnowledge_examples : AttackerKnowledge

Equations

• DY.Example.MerkleTree.instAttackerKnowledge_examples = { attackerKnowledge := DY.Example.MerkleTree.attackerKnowledge }

def DY.Example.MerkleTree.attackerKnowledge.internal (id✝ : Fin 5) : SubAttackerKnowledge (SubF.internal id✝)

Equations

• DY.Example.MerkleTree.attackerKnowledge.internal 0 = DY.Literal.attackerKnowledge
• DY.Example.MerkleTree.attackerKnowledge.internal 1 = DY.Concat.attackerKnowledge
• DY.Example.MerkleTree.attackerKnowledge.internal 2 = DY.Hash.attackerKnowledge
• DY.Example.MerkleTree.attackerKnowledge.internal 3 = DY.Signature.attackerKnowledge
• DY.Example.MerkleTree.attackerKnowledge.internal 4 = DY.Random.attackerKnowledge
• DY.Example.MerkleTree.attackerKnowledge.internal ⟨n.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.Example.MerkleTree.SubF.length : Bytes.PartialLength SubF

Equations

• DY.Example.MerkleTree.SubF.length = DY.Bytes.PartialLength.combine DY.Example.MerkleTree.SubF.length.internal

@[instance_reducible]

def DY.Example.MerkleTree.attackerKnowledge : SubAttackerKnowledge SubF

Equations

• DY.Example.MerkleTree.attackerKnowledge = DY.SubAttackerKnowledge.combine DY.Example.MerkleTree.attackerKnowledge.internal

@[instance_reducible]

instance DY.Example.MerkleTree.instHasExecBytes : HasExecBytes

Equations

• One or more equations did not get rendered due to their size.

def DY.Example.MerkleTree.baseAttackerKnowledge.internal (id✝ : Fin 5) : SubBaseAttackerKnowledge (ExecEntryT.internal id✝)

Equations

• DY.Example.MerkleTree.baseAttackerKnowledge.internal 0 = DY.Network.baseAttackerKnowledge
• DY.Example.MerkleTree.baseAttackerKnowledge.internal 1 = DY.Random.baseAttackerKnowledge
• DY.Example.MerkleTree.baseAttackerKnowledge.internal 2 = DY.ProtocolEvent.baseAttackerKnowledge DY.Example.MerkleTree.TheEvent
• DY.Example.MerkleTree.baseAttackerKnowledge.internal 3 = DY.PersistentLocalState.CompromisableState.baseAttackerKnowledge DY.Example.MerkleTree.ServerState
• DY.Example.MerkleTree.baseAttackerKnowledge.internal 4 = DY.LongTermKeys.baseAttackerKnowledge "MerkleTree PKI"
• DY.Example.MerkleTree.baseAttackerKnowledge.internal ⟨n.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

instance DY.Example.MerkleTree.instHasExecEntryT : ExecTraceTypes.Has ExecEntryT

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

def DY.Example.MerkleTree.baseAttackerKnowledge : SubBaseAttackerKnowledge ExecEntryT

Equations

• DY.Example.MerkleTree.baseAttackerKnowledge = DY.SubBaseAttackerKnowledge.combine DY.Example.MerkleTree.baseAttackerKnowledge.internal

@[instance_reducible]

instance DY.Example.MerkleTree.instBaseAttackerKnowledge_examples : BaseAttackerKnowledge

Equations

• DY.Example.MerkleTree.instBaseAttackerKnowledge_examples = { attackerKnows := DY.Example.MerkleTree.baseAttackerKnowledge }

instance DY.Example.MerkleTree.instHasExecEntryTBaseAttackerKnowledge : BaseAttackerKnowledge.Has baseAttackerKnowledge

@[instance_reducible]

def DY.Example.MerkleTree.ExecEntryT : Type

Equations

• DY.Example.MerkleTree.ExecEntryT = DY.ExecTraceTypes.combine DY.Example.MerkleTree.ExecEntryT.internal

@[instance_reducible]

instance DY.Example.MerkleTree.instExecTraceTypes_examples : ExecTraceTypes

Equations

• DY.Example.MerkleTree.instExecTraceTypes_examples = { ExecT := DY.Example.MerkleTree.ExecEntryT }

def DY.Example.MerkleTree.ExecEntryT.internal : Fin 5 → Type

Equations

• DY.Example.MerkleTree.ExecEntryT.internal 0 = DY.Network.ExecEntryT
• DY.Example.MerkleTree.ExecEntryT.internal 1 = DY.Random.ExecEntryT
• DY.Example.MerkleTree.ExecEntryT.internal 2 = DY.ProtocolEvent.ExecEntryT DY.Example.MerkleTree.TheEvent
• DY.Example.MerkleTree.ExecEntryT.internal 3 = DY.PersistentLocalState.CompromisableState.ExecEntryT DY.Example.MerkleTree.ServerState
• DY.Example.MerkleTree.ExecEntryT.internal 4 = DY.LongTermKeys.ExecEntryT "MerkleTree PKI"
• DY.Example.MerkleTree.ExecEntryT.internal ⟨n.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

instance DY.Example.MerkleTree.instHasExecTrace : HasExecTrace

Equations

• One or more equations did not get rendered due to their size.

def DY.Example.MerkleTree.ProofEntryT.internal : Fin 5 → Type

Equations

• DY.Example.MerkleTree.ProofEntryT.internal 0 = DY.Network.ProofEntryT
• DY.Example.MerkleTree.ProofEntryT.internal 1 = DY.Random.ProofEntryT
• DY.Example.MerkleTree.ProofEntryT.internal 2 = DY.ProtocolEvent.ProofEntryT DY.Example.MerkleTree.TheEvent
• DY.Example.MerkleTree.ProofEntryT.internal 3 = DY.PersistentLocalState.CompromisableState.ProofEntryT DY.Example.MerkleTree.ServerState
• DY.Example.MerkleTree.ProofEntryT.internal 4 = DY.LongTermKeys.ProofEntryT "MerkleTree PKI"
• DY.Example.MerkleTree.ProofEntryT.internal ⟨n.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

instance DY.Example.MerkleTree.instProofTraceTypes_examples : ProofTraceTypes

Equations

• DY.Example.MerkleTree.instProofTraceTypes_examples = { ProofT := DY.Example.MerkleTree.ProofEntryT, tc := DY.Example.MerkleTree.wfInst✝ }

@[instance_reducible]

def DY.Example.MerkleTree.ProofEntryT : Type

Equations

• DY.Example.MerkleTree.ProofEntryT = DY.ProofTraceTypes.combine DY.Example.MerkleTree.ProofEntryT.internal

@[instance_reducible]

instance DY.Example.MerkleTree.instHasExecEntryTProofEntryT : ProofTraceTypes.Has ProofEntryT

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.Example.MerkleTree.instHasProofTrace : HasProofTrace

Equations

• One or more equations did not get rendered due to their size.

instance DY.Example.MerkleTree.instHasSubFInvariants : BytesInvariants.Has invariants

@[instance_reducible]

def DY.Example.MerkleTree.invariants : Bytes.PartialInvariants SubF

Equations

• DY.Example.MerkleTree.invariants = DY.Bytes.PartialInvariants.combine DY.Example.MerkleTree.invariants.internal

theorem DY.Example.MerkleTree.invariantsProofs.internal (id✝ : Fin 5) : Bytes.PartialInvariantsProofs (invariants.internal id✝)

theorem DY.Example.MerkleTree.invariantsProofs : Bytes.PartialInvariantsProofs invariants

def DY.Example.MerkleTree.invariants.internal (id✝ : Fin 5) : Bytes.PartialInvariants (SubF.internal id✝)

Equations

• DY.Example.MerkleTree.invariants.internal 0 = DY.Literal.invariants
• DY.Example.MerkleTree.invariants.internal 1 = DY.Concat.invariants
• DY.Example.MerkleTree.invariants.internal 2 = DY.Hash.invariants
• DY.Example.MerkleTree.invariants.internal 3 = DY.Signature.invariants
• DY.Example.MerkleTree.invariants.internal 4 = DY.Random.invariants
• DY.Example.MerkleTree.invariants.internal ⟨n.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

instance DY.Example.MerkleTree.instBytesInvariantsProofs_examples : BytesInvariantsProofs

@[instance_reducible]

instance DY.Example.MerkleTree.instBytesInvariants_examples : BytesInvariants

Equations

• DY.Example.MerkleTree.instBytesInvariants_examples = { invs := DY.Example.MerkleTree.invariants }

@[instance_reducible]

instance DY.Example.MerkleTree.instHasBytesInvariants : HasBytesInvariants

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.Example.MerkleTree.instSubTraceInvariantExecEntryTProofEntryT : SubTraceInvariant ProofEntryT

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.Example.MerkleTree.instTraceInvariant_examples : TraceInvariant

Equations

• DY.Example.MerkleTree.instTraceInvariant_examples = { tc_inv := { invariant := DY.Example.MerkleTree.instTraceInvariant_examples._aux_1 } }

instance DY.Example.MerkleTree.instBaseAttackerKnowledgeTheorem_examples : BaseAttackerKnowledgeTheorem

instance DY.Example.MerkleTree.instHasExecEntryTProofEntryT_1 : TraceInvariant.Has ProofEntryT

instance DY.Example.MerkleTree.instAttackerKnowledgeTheorem_examples : AttackerKnowledgeTheorem

@[instance_reducible]

instance DY.Example.MerkleTree.instHasTraceInvariant : HasTraceInvariant

Equations

• One or more equations did not get rendered due to their size.