OAI/Combinatorics/ParityLifts/Simulation.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ParityWL.Complexity.BEval.loop_completes line 7
  2. def OAI.ParityWL.Complexity.smallControl line 36
  3. def OAI.ParityWL.Complexity.simStepExpr line 39
  4. def OAI.ParityWL.Complexity.simStartExpr line 44
  5. def OAI.ParityWL.Complexity.simAnswerExpr line 46
  6. lemma OAI.ParityWL.Complexity.simStartExpr_eval line 48
  7. lemma OAI.ParityWL.Complexity.simStepExpr_fixed line 53
  8. lemma OAI.ParityWL.Complexity.simStepExpr_eval line 56
  9. lemma OAI.ParityWL.Complexity.simStepExpr_iterate line 74
  10. lemma OAI.ParityWL.Complexity.smallControl_size line 81
  11. lemma OAI.ParityWL.Complexity.simLoop_run line 86
  12. def OAI.ParityWL.Complexity.smallInitialExpr line 127
  13. def OAI.ParityWL.Complexity.smallBitProgram line 131
  14. def OAI.ParityWL.Complexity.smallInitialProgram line 135
  15. lemma OAI.ParityWL.Complexity.PolyProgram.congr_degree line 149
  16. lemma OAI.ParityWL.Complexity.PolyProgram.reverse_degree line 156
  17. lemma OAI.ParityWL.Complexity.PolyProgram.map_degree line 162
  18. def OAI.ParityWL.Complexity.smallInitialDegree line 171
  19. lemma OAI.ParityWL.Complexity.smallInitialProgram_degree line 173
  20. lemma OAI.ParityWL.Complexity.treeEncode_bits_size line 183
  21. def OAI.ParityWL.Complexity.simulationCode line 188
  22. def OAI.ParityWL.Complexity.simulationDegree line 193
  23. def OAI.ParityWL.Complexity.simulationCoefficient line 195
  24. lemma OAI.ParityWL.Complexity.simulation_run line 202
  25. def OAI.ParityWL.Complexity.Machine.preprocess line 276
  26. def OAI.ParityWL.Complexity.preprocessingDegree line 278
  27. lemma OAI.ParityWL.Complexity.Machine.preprocess_run line 280