OAI/Combinatorics/ContingencyTables/Machines/OnlineRetryPrefix.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite execution prefixes of the unbounded exact-rejection loop

  1. def OAI.ContingencyTables.OnlineRetryPrefix.At line 17

    Source documentation

    A failed finite prefix ends at the live retry label, while a successful prefix ends in the machine's halted configuration.

    def At (M : Λ → Instr R Λ) (out : α → Option Λ×Env R)
    (l : Option Λ) (E : Env R) (p : Experiment α) : Prop :=
…
  2. lemma OAI.ContingencyTables.OnlineRetryPrefix.done line 21
  3. lemma OAI.ContingencyTables.OnlineRetryPrefix.halt line 24
  4. lemma OAI.ContingencyTables.OnlineRetryPrefix.go line 31
  5. lemma OAI.ContingencyTables.OnlineRetryPrefix.nilBranch line 38
  6. lemma OAI.ContingencyTables.OnlineRetryPrefix.consBranch line 47
  7. lemma OAI.ContingencyTables.OnlineRetryPrefix.call line 56
  8. lemma OAI.ContingencyTables.OnlineRetryPrefix.deterministicCall line 74