OAI/NumberTheory/SingleFold/CounterBounds.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleFold.Packed.bits_pack line 6
  2. lemma OAI.SingleFold.Packed.exists_scale line 17
  3. def OAI.SingleFold.Counter.stateAt line 41
  4. def OAI.SingleFold.Counter.zeroAt line 42
  5. def OAI.SingleFold.Counter.decAt line 46
  6. def OAI.SingleFold.Counter.arcAt line 50
  7. lemma OAI.SingleFold.Counter.stateAt_le line 57
  8. lemma OAI.SingleFold.Counter.zeroAt_le line 59
  9. lemma OAI.SingleFold.Counter.decAt_le line 63
  10. lemma OAI.SingleFold.Counter.arcAt_inactive line 67
  11. lemma OAI.SingleFold.Counter.arcAt_halt line 70
  12. lemma OAI.SingleFold.Counter.testAt_partition line 76
  13. def OAI.SingleFold.Counter.incomingAt line 81
  14. def OAI.SingleFold.Counter.incAt line 83
  15. def OAI.SingleFold.Counter.subAt line 85
  16. lemma OAI.SingleFold.Counter.incomingAt_active line 88
  17. lemma OAI.SingleFold.Counter.incAt_active line 96
  18. lemma OAI.SingleFold.Counter.subAt_active line 104
  19. lemma OAI.SingleFold.Counter.incAt_le line 112
  20. lemma OAI.SingleFold.Counter.subAt_le line 115
  21. lemma OAI.SingleFold.Counter.incomingAt_next line 118
  22. lemma OAI.SingleFold.Counter.counterAt_next line 126
  23. lemma OAI.SingleFold.Counter.incAt_halt line 141
  24. lemma OAI.SingleFold.Counter.subAt_halt line 143
  25. lemma OAI.SingleFold.Packed.pack_ite_const line 148
  26. def OAI.SingleFold.Counter.valueAt line 155
  27. def OAI.SingleFold.Counter.trace line 158
  28. lemma OAI.SingleFold.Counter.trace_arc line 175
  29. lemma OAI.SingleFold.Counter.trace_incoming line 178
  30. lemma OAI.SingleFold.Counter.trace_inc line 181
  31. lemma OAI.SingleFold.Counter.trace_sub line 187
  32. lemma OAI.SingleFold.Counter.trace_transition line 193
  33. lemma OAI.SingleFold.Counter.trace_update line 210
  34. lemma OAI.SingleFold.Counter.valueAt_bound line 221
  35. lemma OAI.SingleFold.Packed.bits_of_le_one line 233
  36. lemma OAI.SingleFold.Counter.trace_clock line 243
  37. lemma OAI.SingleFold.Counter.trace_system line 254
  38. theorem OAI.SingleFold.Counter.system_complete line 348