Protocol

Difficulty: moderate — 2 definitions, 0 abbreviations, 0 lemmas, 1 theorems, 0 examples.

definition theorem
legend
def Sender.step (poly : List Bool) (n : ℕ) :
  InformationSystem Bool (Bool × Frame poly n poly.length) (Frame poly n poly.length)
Show details 
| Sender.step poly n = { step := fun x ack_e => (!ack_e.1, ack_e.2), conserves := ⋯ }

Complexity: 177 (size of the value term)

Outer dependencies: Frame, InformationSystem, instNonemptyFrame, instNormBool_computerNetworks, instNormFrame, instNormProd_computerNetworks

Inner dependencies: Bit, instNormBit, instNormForallFin_computerNetworks

Mathlib dependencies: Finset, Finset.card, Finset.sum, Finset.sum_congr, Finset.sum_const, Finset.univ, Fintype.card_fin, Real, mul_one, nsmul_eq_mul, zero_add

Lean core dependencies: Bool, Bool.not, Eq, Eq.trans, Fin, List, List.length, Nat, Nat.cast, Prod, True, congr, congrArg, congrFun', eq_self, of_eq_true

Used by: (none)

def Receiver.step (poly : List Bool) (n : ℕ) :
  InformationSystem Unit (Frame poly n poly.length) (Frame poly n poly.length × Bool)
Show details 
| Receiver.step poly n = { step := fun x e => ((), e, decide (Frame.valid poly e)), conserves := ⋯ }

Complexity: 391 (size of the value term)

Outer dependencies: Frame, InformationSystem, instNonemptyFrame, instNormBool_computerNetworks, instNormFrame, instNormProd_computerNetworks, instNormUnit_computerNetworks

Inner dependencies: Bit, Frame.crc, Frame.valid, instNormBit, instNormForallFin_computerNetworks

Mathlib dependencies: Finset, Finset.card, Finset.sum, Finset.sum_congr, Finset.sum_const, Finset.univ, Fintype.card_fin, Real, add_zero, mul_one, nsmul_eq_mul, zero_add

Lean core dependencies: Bool, Decidable.decide, Eq, Eq.trans, Fin, List, List.length, List.ofFn, Nat, Nat.cast, Option.getD, Prod, True, Unit, Unit.unit, congr, congrArg, congrFun', eq_self, of_eq_true

Used by: Receiver.step_correct

theorem Receiver.step_correct {poly : List Bool} {n : ℕ} (e : Frame poly n poly.length) :
  ((Receiver.step poly n).step () e).2.2 = true ↔ Frame.valid poly e
Show details 
fun {poly} {n} e => decide_eq_true_iff

Complexity: 249 (size of the value term)

Dependencies: Frame, Frame.valid, Receiver.step, instNonemptyFrame, instNormBool_computerNetworks, instNormFrame, instNormProd_computerNetworks, instNormUnit_computerNetworks

Proof dependencies: Bit, Frame.crc

Lean core dependencies: Bool, Eq, Fin, Iff, List, List.length, List.ofFn, Nat, Option.getD, Prod, Unit, Unit.unit, decide_eq_true_iff

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitiontheoremdeclared elsewheredependencyproof dependency
legend