`permits_append`

proved

show as: view math explainer →

module: IndisputableMonolith.Recognition.Consent
domain: Recognition
line: 63 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Recognition.Consent on GitHub at line 63.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  60def permits {A} (L : ConsentLedger A) (t : Nat) (a : A) : Bool :=
  61  L.windows.any (fun w => ConsentWindow.permitsAt w t a)
  62
  63@[simp] lemma permits_append {A} (L1 L2 : List (ConsentWindow A)) (t : Nat) (a : A) :
  64  (ConsentLedger.permits { windows := L1 ++ L2 } t a)
  65  = (ConsentLedger.permits { windows := L1 } t a
  66     || ConsentLedger.permits { windows := L2 } t a) := by
  67  unfold ConsentLedger.permits
  68  simp [List.any_append]
  69
  70end ConsentLedger
  71
  72end Recognition
  73end IndisputableMonolith
  74

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.