OAI/NumberTheory/SingleFold/MacroMachine.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingleFold.Counter.step line 7
  2. inductive OAI.SingleFold.Macro.Instr line 15
  3. def OAI.SingleFold.Macro.radix line 23
  4. structure OAI.SingleFold.Macro.Cfg line 24
  5. def OAI.SingleFold.Macro.next line 28
  6. def OAI.SingleFold.Macro.step line 36
  7. inductive OAI.SingleFold.Macro.State line 39
  8. abbrev OAI.SingleFold.Macro.Reg line 50
  9. def OAI.SingleFold.Macro.scratch line 51
  10. def OAI.SingleFold.Macro.zeroReg line 52
  11. def OAI.SingleFold.Macro.succ5 line 54
  12. def OAI.SingleFold.Macro.go line 55
  13. def OAI.SingleFold.Macro.finish line 57
  14. def OAI.SingleFold.Macro.compileInstr line 63
  15. def OAI.SingleFold.Macro.compile line 89
  16. def OAI.SingleFold.Macro.cfg line 106
  17. def OAI.SingleFold.Macro.encode line 108
  18. lemma OAI.SingleFold.Macro.inc_reg line 113
  19. lemma OAI.SingleFold.Macro.inc_scratch line 122
  20. lemma OAI.SingleFold.Macro.test_reg line 133
  21. lemma OAI.SingleFold.Macro.test_scratch line 142
  22. lemma OAI.SingleFold.Macro.goto line 154
  23. lemma OAI.SingleFold.Macro.prepend line 166
  24. lemma OAI.SingleFold.Macro.inc_at line 170
  25. lemma OAI.SingleFold.Macro.test_at_zero line 175
  26. lemma OAI.SingleFold.Macro.test_at_succ line 180
  27. lemma OAI.SingleFold.Macro.grow_loop line 186
  28. lemma OAI.SingleFold.Macro.multiply_loop line 202
  29. lemma OAI.SingleFold.Macro.copy_loop line 217
  30. lemma OAI.SingleFold.Macro.add_loop line 235
  31. lemma OAI.SingleFold.Macro.radix_pos line 259
  32. lemma OAI.SingleFold.Macro.radix_le line 260
  33. def OAI.SingleFold.Macro.mod5 line 261
  34. lemma OAI.SingleFold.Macro.mod5_val line 262
  35. lemma OAI.SingleFold.Macro.mod5_self line 263
  36. lemma OAI.SingleFold.Macro.quotient_loop line 268
  37. lemma OAI.SingleFold.Macro.simulate line 295
  38. lemma OAI.SingleFold.Macro.respects line 336
  39. lemma OAI.SingleFold.Macro.eval_dom line 344
  40. lemma OAI.SingleFold.Counter.step_eq_none line 353
  41. lemma OAI.SingleFold.Counter.reaches_iterate line 357
  42. lemma OAI.SingleFold.Counter.reaches_run line 371
  43. lemma OAI.SingleFold.Counter.halts_iff_exists line 381
  44. lemma OAI.SingleFold.Counter.eval_dom_iff_halts line 386