OAI/Computability/BinPacking/CookLevin/MachineCircuit.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.MachineCircuit.bool_ext line 15
  2. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.MachineCircuit.StepSafe line 18
  3. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.MachineCircuit.liveCase line 21
  4. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.MachineCircuit.stickyExpr line 26
  5. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.MachineCircuit.absorbing_live line 33
  6. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.MachineCircuit.absorbing_halted line 44
  7. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.MachineCircuit.liveCase_eval line 54
  8. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.MachineCircuit.stickyExpr_eval line 68
  9. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.MachineCircuit.configEncoding_injective line 98
  10. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.MachineCircuit.programCost line 122
  11. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.MachineCircuit.statementCost_le_programCost line 127
  12. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.MachineCircuit.expressionCost line 133
  13. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.MachineCircuit.one_le_expressionCost line 138
  14. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.MachineCircuit.stickyExpr_size_le line 143