OAI/Combinatorics/ContingencyTables/Machines/ListWordProgram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Binary execution of the finite-list proposal

The list is scanned only up to its own length. A binary index beyond the end produces none; its numerical magnitude never determines a loop bound.

  1. def OAI.ContingencyTables.ProfilePrograms.getOptionFast line 19
  2. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_getOptionFast line 29
  3. def OAI.ContingencyTables.ProfilePrograms.listWordChoice line 37
  4. def OAI.ContingencyTables.ProfilePrograms.listWordChoiceRealizer line 40
  5. theorem OAI.ContingencyTables.ProfilePrograms.polynomial_listWordChoice line 43
  6. lemma OAI.ContingencyTables.ProfilePrograms.bitValue_eq_word line 49
  7. theorem OAI.ContingencyTables.ProfilePrograms.listWordChoice_ofFn line 70
  8. theorem OAI.ContingencyTables.ProfilePrograms.listWordChoice_mass line 77

    Source documentation

    The literal binary program has the previously proved dyadic proposal law, including all unused indices that return none.

    theorem listWordChoice_mass [Fintype A] [DecidableEq A]
    (xs : List A) (hxs : xs.Nodup) (k : ℕ) (hk : xs.length≤2^k) (a : A) :
    (FirstSuccess.mapLaw
      (FirstSuccess.uniformLaw (α := Fin k → Bool))
…

    Mentions: OAI.ContingencyTables.FirstSuccess.mapLaw, OAI.ContingencyTables.FirstSuccess.uniformLaw