OAI/Combinatorics/ContingencyTables/Rooted/RootedOracleWordProgram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A single fixed word drives an executed oracle transition

  1. abbrev OAI.ContingencyTables.RootedOracleStepProgram.WordInput line 12
  2. def OAI.ContingencyTables.RootedOracleStepProgram.proposalWidth line 14
  3. def OAI.ContingencyTables.RootedOracleStepProgram.proposalWidthRealizer line 15
  4. lemma OAI.ContingencyTables.RootedOracleStepProgram.polynomial_proposalWidth line 23
  5. def OAI.ContingencyTables.RootedOracleStepProgram.wordStep line 34
  6. def OAI.ContingencyTables.RootedOracleStepProgram.wordStepRealizer line 36
  7. theorem OAI.ContingencyTables.RootedOracleStepProgram.polynomial_wordStep line 42
  8. theorem OAI.ContingencyTables.RootedOracleStepProgram.wordStep_data line 56

    Source documentation

    Exact code agreement for the prescribed finite word, including unused direction codes and unsuccessful acceptance tests.

    theorem wordStep_data (A : Instance (Fin m) (Fin n)) (C a K : ℕ) (hC : 0 < C)
    (z : View A → ℕ) (v : Grid (I := Fin (RootedCatalogGrid.freeCount A)) K)
…

    Mentions: OAI.ContingencyTables.RootedCatalogGrid.freeCount