OAI/ModelTheory/Choiceless/QueryMachine.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CPTSeparation.TableMachine.headerConsume line 13
  2. def OAI.CPTSeparation.TableMachine.headerBody line 15
  3. def OAI.CPTSeparation.TableMachine.headerLoop line 18
  4. def OAI.CPTSeparation.TableMachine.header line 20
  5. def OAI.CPTSeparation.TableMachine.headerNums line 22
  6. def OAI.CPTSeparation.TableMachine.headerState line 27
  7. lemma OAI.CPTSeparation.TableMachine.headerNums_inc line 30
  8. lemma OAI.CPTSeparation.TableMachine.headerBody_runs line 36
  9. lemma OAI.CPTSeparation.TableMachine.headerLoop_runs line 52
  10. lemma OAI.CPTSeparation.TableMachine.header_runs line 66
  11. lemma OAI.CPTSeparation.StackLang.update_sum_left line 85
  12. lemma OAI.CPTSeparation.StackLang.update_sum_right line 89
  13. def OAI.CPTSeparation.StackLang.leftStore line 93
  14. def OAI.CPTSeparation.StackLang.Action.frameLeft line 96
  15. lemma OAI.CPTSeparation.StackLang.Action.run_frameLeft line 105
  16. def OAI.CPTSeparation.StackLang.Program.frameLeft line 119
  17. def OAI.CPTSeparation.StackLang.Exec.frameLeft line 125
  18. lemma OAI.CPTSeparation.StackLang.Runs.frameLeft line 135
  19. def OAI.CPTSeparation.StackLang.rightStore line 140
  20. def OAI.CPTSeparation.StackLang.Action.frameRight line 143
  21. lemma OAI.CPTSeparation.StackLang.Action.run_frameRight line 152
  22. def OAI.CPTSeparation.StackLang.Program.frameRight line 166
  23. def OAI.CPTSeparation.StackLang.Exec.frameRight line 172
  24. lemma OAI.CPTSeparation.StackLang.Runs.frameRight line 182
  25. abbrev OAI.CPTSeparation.QueryMachine.Letter line 193
  26. abbrev OAI.CPTSeparation.QueryMachine.LeftReg line 195
  27. abbrev OAI.CPTSeparation.QueryMachine.Reg line 197
  28. abbrev OAI.CPTSeparation.QueryMachine.Local line 199
  29. abbrev OAI.CPTSeparation.QueryMachine.Prog line 201
  30. def OAI.CPTSeparation.QueryMachine.initialLocal line 203
  31. def OAI.CPTSeparation.QueryMachine.cs line 205
  32. def OAI.CPTSeparation.QueryMachine.combined line 208
  33. def OAI.CPTSeparation.QueryMachine.build line 211
  34. def OAI.CPTSeparation.QueryMachine.transfers line 214
  35. def OAI.CPTSeparation.QueryMachine.finish line 218
  36. def OAI.CPTSeparation.QueryMachine.program line 223
  37. def OAI.CPTSeparation.QueryMachine.finalStore line 227
  38. lemma OAI.CPTSeparation.QueryMachine.cs_ready line 230
  39. lemma OAI.CPTSeparation.QueryMachine.build_runs line 234
  40. lemma OAI.CPTSeparation.QueryMachine.transfers_runs line 246
  41. lemma OAI.CPTSeparation.QueryMachine.solver_framed line 274
  42. lemma OAI.CPTSeparation.QueryMachine.finish_runs line 282
  43. def OAI.CPTSeparation.QueryMachine.time line 319
  44. lemma OAI.CPTSeparation.QueryMachine.program_runs line 323
  45. lemma OAI.CPTSeparation.QueryMachine.time_polynomial line 343
  46. def OAI.CPTSeparation.QueryMachine.includeLetter line 356
  47. def OAI.CPTSeparation.QueryMachine.projectLetter line 360
  48. lemma OAI.CPTSeparation.QueryMachine.project_include line 364
  49. lemma OAI.CPTSeparation.QueryMachine.code_map line 369
  50. lemma OAI.CPTSeparation.QueryMachine.code_length line 374
  51. lemma OAI.CPTSeparation.QueryMachine.code_decode line 378
  52. lemma OAI.CPTSeparation.QueryMachine.code_injective line 384
  53. def OAI.CPTSeparation.QueryMachine.encoding line 388
  54. def OAI.CPTSeparation.QueryMachine.answer line 391
  55. lemma OAI.CPTSeparation.QueryMachine.answer_correct line 393
  56. def OAI.CPTSeparation.QueryMachine.machine line 396
  57. lemma OAI.CPTSeparation.QueryMachine.initial_configuration line 399
  58. lemma OAI.CPTSeparation.QueryMachine.final_configuration line 418
  59. lemma OAI.CPTSeparation.QueryMachine.polynomial_eval_mono line 428
  60. def OAI.CPTSeparation.QueryMachine.polynomialAlgorithm line 433