OAI/Computability/MaxCut/Estimates/CorrectSum.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.OptimalMaxCut.CounterMachine.Expr.correct_sum line 11
  2. theorem OAI.OptimalMaxCut.CounterMachine.Expr.correct line 116
  3. def OAI.OptimalMaxCut.CounterMachine.Data.restrict line 132
  4. def OAI.OptimalMaxCut.CounterMachine.Command.Bounded line 137
  5. def OAI.OptimalMaxCut.CounterMachine.Command.regCount line 145
  6. theorem OAI.OptimalMaxCut.CounterMachine.Command.bounded_of_count line 153
  7. def OAI.OptimalMaxCut.CounterMachine.Command.restrict line 156
  8. theorem OAI.OptimalMaxCut.CounterMachine.Command.restrict_inc line 168
  9. theorem OAI.OptimalMaxCut.CounterMachine.Command.restrict_dec line 180
  10. theorem OAI.OptimalMaxCut.CounterMachine.Command.Evaluates.restrict line 192
  11. def OAI.OptimalMaxCut.CounterMachine.Command.finite line 213
  12. theorem OAI.OptimalMaxCut.CounterMachine.Command.finite_evaluates line 216
  13. def OAI.OptimalMaxCut.CounterMachine.table line 227

    Source documentation

    A bit table specified by two bounded-arithmetic expressions. These are syntax, not assumed computable functions or unit-time arithmetic oracles.

    def table (len bit : Expr) (input : List Bool) : List Bool :=
…

    Mentions: OAI.OptimalMaxCut.CounterMachine.Expr

  14. def OAI.OptimalMaxCut.CounterMachine.emit line 231
  15. theorem OAI.OptimalMaxCut.CounterMachine.emit_evaluates line 233
  16. def OAI.OptimalMaxCut.CounterMachine.print line 245
  17. theorem OAI.OptimalMaxCut.CounterMachine.print_evaluates line 249
  18. def OAI.OptimalMaxCut.CounterMachine.eraseInput line 321

    Source documentation

    Required cleanup before Mathlib's exact halt-list convention.

    def eraseInput : Command ℕ := .seq (inputLength 1 0) (.loop 0 .discard)

    Mentions: OAI.OptimalMaxCut.CounterMachine.Command

  19. theorem OAI.OptimalMaxCut.CounterMachine.eraseInput_evaluates line 323