OAI/NumberTheory/SingleFold/CounterMachine.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.SingleFold.Counter.Instr line 8
  2. structure OAI.SingleFold.Counter.Machine line 14
  3. structure OAI.SingleFold.Counter.Cfg line 20
  4. def OAI.SingleFold.Counter.next line 25
  5. def OAI.SingleFold.Counter.run line 30
  6. lemma OAI.SingleFold.Counter.run_zero line 32
  7. lemma OAI.SingleFold.Counter.run_succ line 34
  8. def OAI.SingleFold.Counter.HaltsAt line 36
  9. def OAI.SingleFold.Counter.Halts line 38
  10. lemma OAI.SingleFold.Counter.haltsAt_unique line 40
  11. lemma OAI.SingleFold.Counter.value_bound line 47
  12. def OAI.SingleFold.Counter.dest line 68
  13. structure OAI.SingleFold.Counter.Witness line 75
  14. def OAI.SingleFold.Counter.baseC line 92
  15. def OAI.SingleFold.Counter.arc line 94
  16. def OAI.SingleFold.Counter.incoming line 101
  17. def OAI.SingleFold.Counter.increments line 104
  18. def OAI.SingleFold.Counter.decrements line 107
  19. def OAI.SingleFold.Counter.Bits line 110
  20. structure OAI.SingleFold.Counter.System line 112
  21. lemma OAI.SingleFold.Counter.System.Cpos line 144
  22. lemma OAI.SingleFold.Counter.System.Bpos line 145
  23. lemma OAI.SingleFold.Counter.System.Bfour line 146
  24. lemma OAI.SingleFold.Counter.System.Bgt line 147
  25. lemma OAI.SingleFold.Counter.System.bpos line 148
  26. lemma OAI.SingleFold.Counter.System.width line 149
  27. lemma OAI.SingleFold.Counter.System.states_bound line 156
  28. lemma OAI.SingleFold.Counter.System.initial_bound line 160
  29. lemma OAI.SingleFold.Counter.System.clock_bound line 166
  30. lemma OAI.SingleFold.Counter.System.last_eq line 167
  31. lemma OAI.SingleFold.Counter.System.mask_eq line 172
  32. lemma OAI.SingleFold.Counter.System.state_info line 176
  33. lemma OAI.SingleFold.Counter.System.counter_info line 182
  34. lemma OAI.SingleFold.Counter.System.rem_eq line 194
  35. lemma OAI.SingleFold.Counter.System.final_eq line 201
  36. lemma OAI.SingleFold.Counter.System.state_partition line 208
  37. lemma OAI.SingleFold.Counter.System.arc_none line 227
  38. lemma OAI.SingleFold.Counter.System.incoming_sum line 230
  39. lemma OAI.SingleFold.Counter.System.outgoing line 241
  40. lemma OAI.SingleFold.Counter.System.outgoing_sum line 252
  41. lemma OAI.SingleFold.Counter.System.transition_sum line 258
  42. lemma OAI.SingleFold.Counter.System.halt_mask line 264
  43. lemma OAI.SingleFold.Counter.System.arc_bits line 277
  44. lemma OAI.SingleFold.Counter.System.arc_info line 287
  45. lemma OAI.SingleFold.Counter.System.arcs_sum_eq line 296
  46. lemma OAI.SingleFold.Counter.System.arc_digit_cap line 305
  47. lemma OAI.SingleFold.Counter.System.arc_digit_sum line 310
  48. def OAI.SingleFold.Counter.System.selected line 320
  49. lemma OAI.SingleFold.Counter.System.selected_digit line 321
  50. lemma OAI.SingleFold.Counter.System.selected_bound line 338
  51. lemma OAI.SingleFold.Counter.System.selected_le_one line 350