OAI/ModelTheory/Choiceless/Counters.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.CPTSeparation.CounterLang.Reg line 11
  2. structure OAI.CPTSeparation.CounterLang.Data line 16
  3. def OAI.CPTSeparation.CounterLang.Data.tapes line 28
  4. lemma OAI.CPTSeparation.CounterLang.Data.tapes_reg line 36
  5. lemma OAI.CPTSeparation.CounterLang.Data.tapes_input line 42
  6. lemma OAI.CPTSeparation.CounterLang.Data.tapes_output line 44
  7. lemma OAI.CPTSeparation.CounterLang.Data.tapes_work line 46
  8. lemma OAI.CPTSeparation.CounterLang.Data.tapes_back line 48
  9. lemma OAI.CPTSeparation.CounterLang.Data.tapes_count line 50
  10. structure OAI.CPTSeparation.CounterLang.State line 54
  11. def OAI.CPTSeparation.CounterLang.unary line 62
  12. lemma OAI.CPTSeparation.CounterLang.unary_update line 64
  13. def OAI.CPTSeparation.CounterLang.State.data line 68
  14. def OAI.CPTSeparation.CounterLang.State.encode line 70
  15. inductive OAI.CPTSeparation.CounterLang.Atom line 72
  16. def OAI.CPTSeparation.CounterLang.Atom.eval line 86
  17. def OAI.CPTSeparation.CounterLang.Atom.cost line 98
  18. inductive OAI.CPTSeparation.CounterLang.Program line 107
  19. inductive OAI.CPTSeparation.CounterLang.Runs line 113
  20. lemma OAI.CPTSeparation.CounterLang.Runs.loop_steps line 123
  21. abbrev OAI.CPTSeparation.CounterLang.LowProgram line 143
  22. def OAI.CPTSeparation.CounterLang.skipBody line 145
  23. def OAI.CPTSeparation.CounterLang.skipLoop line 149
  24. def OAI.CPTSeparation.CounterLang.lookup line 151
  25. def OAI.CPTSeparation.CounterLang.Atom.compile line 160
  26. lemma OAI.CPTSeparation.CounterLang.unary_update_self line 174
  27. lemma OAI.CPTSeparation.CounterLang.unary_length line 179
  28. lemma OAI.CPTSeparation.CounterLang.unary_head line 183
  29. lemma OAI.CPTSeparation.CounterLang.skipLoop_runs line 186
  30. lemma OAI.CPTSeparation.CounterLang.lookup_runs line 204
  31. lemma OAI.CPTSeparation.CounterLang.Atom.zero_runs line 243
  32. lemma OAI.CPTSeparation.CounterLang.Atom.add_runs line 248
  33. lemma OAI.CPTSeparation.CounterLang.Atom.compile_runs line 255
  34. def OAI.CPTSeparation.CounterLang.Program.compile line 291
  35. lemma OAI.CPTSeparation.CounterLang.Runs.compiles line 299
  36. lemma OAI.CPTSeparation.CounterLang.State.ext line 317
  37. lemma OAI.CPTSeparation.CounterLang.Runs.atom_of line 324
  38. lemma OAI.CPTSeparation.CounterLang.bne_nat_zero line 329
  39. def OAI.CPTSeparation.CounterLang.testPos line 332
  40. def OAI.CPTSeparation.CounterLang.flag line 334
  41. def OAI.CPTSeparation.CounterLang.mulBody line 336
  42. def OAI.CPTSeparation.CounterLang.mulLoop line 339
  43. def OAI.CPTSeparation.CounterLang.multiply line 342
  44. def OAI.CPTSeparation.CounterLang.mulState line 346
  45. lemma OAI.CPTSeparation.CounterLang.mulBody_runs line 349
  46. lemma OAI.CPTSeparation.CounterLang.mulLoop_runs line 376
  47. lemma OAI.CPTSeparation.CounterLang.multiply_runs line 384
  48. def OAI.CPTSeparation.CounterLang.repeatAdd line 410
  49. lemma OAI.CPTSeparation.CounterLang.repeatAdd_runs line 414
  50. def OAI.CPTSeparation.CounterLang.indexState line 433
  51. def OAI.CPTSeparation.CounterLang.rangeBody line 436
  52. def OAI.CPTSeparation.CounterLang.forRange line 439
  53. lemma OAI.CPTSeparation.CounterLang.rangeTail_runs line 443
  54. lemma OAI.CPTSeparation.CounterLang.forRange_runs line 467
  55. def OAI.CPTSeparation.CounterLang.bothPositive line 514
  56. def OAI.CPTSeparation.CounterLang.compareBody line 517
  57. def OAI.CPTSeparation.CounterLang.compare line 520
  58. lemma OAI.CPTSeparation.CounterLang.bothPositive_runs line 530
  59. lemma OAI.CPTSeparation.CounterLang.compare_runs line 537