OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Stacks.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.VelocityDetection.Stacks.Move line 10

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:55 (same declaration text).

  2. def OAI.VelocityDetection.Stacks.update line 16

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:61 (same declaration text).

  3. theorem OAI.VelocityDetection.Stacks.replace_digit line 22
  4. def OAI.VelocityDetection.Stacks.writtenDigit line 27
  5. def OAI.VelocityDetection.Stacks.undo line 33
  6. theorem OAI.VelocityDetection.Stacks.left_as_digits line 39
  7. theorem OAI.VelocityDetection.Stacks.left_div line 43
  8. theorem OAI.VelocityDetection.Stacks.left_div_sq line 49
  9. theorem OAI.VelocityDetection.Stacks.left_mod line 58
  10. theorem OAI.VelocityDetection.Stacks.writtenDigit_update line 62
  11. theorem OAI.VelocityDetection.Stacks.undo_update line 71
  12. theorem OAI.VelocityDetection.Stacks.written_eq_of_update_eq line 84
  13. theorem OAI.VelocityDetection.Stacks.stacks_eq_of_update_eq line 91
  14. structure OAI.VelocityDetection.Stacks.Rule line 98

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:67 (same declaration text).

  15. structure OAI.VelocityDetection.Stacks.Configuration line 103

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:72 (same declaration text).

  16. def OAI.VelocityDetection.Stacks.applyRule line 109

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:78 (same declaration text).

  17. def OAI.VelocityDetection.Stacks.IncomingDirection line 113
  18. def OAI.VelocityDetection.Stacks.IncomingRule line 117
  19. theorem OAI.VelocityDetection.Stacks.applyRule_injective line 121
  20. theorem OAI.VelocityDetection.Stacks.packed_lt line 147
  21. theorem OAI.VelocityDetection.Stacks.two_digits_lt line 154
  22. theorem OAI.VelocityDetection.Stacks.update_lt line 158
  23. def OAI.VelocityDetection.Stacks.address line 186

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:82 (same declaration text).

  24. theorem OAI.VelocityDetection.Stacks.address_packed line 188
  25. theorem OAI.VelocityDetection.Stacks.address_sub_one line 193
  26. theorem OAI.VelocityDetection.Stacks.address_pos line 197
  27. theorem OAI.VelocityDetection.Stacks.address_le line 201
  28. theorem OAI.VelocityDetection.Stacks.address_decode_x line 209
  29. theorem OAI.VelocityDetection.Stacks.address_decode_y line 213
  30. theorem OAI.VelocityDetection.Stacks.address_decode_state line 218
  31. theorem OAI.VelocityDetection.Stacks.address_injective line 227
  32. def OAI.VelocityDetection.Stacks.capacity line 238

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:84 (same declaration text).

  33. theorem OAI.VelocityDetection.Stacks.capacity_succ line 240
  34. theorem OAI.VelocityDetection.Stacks.capacity_dvd line 245
  35. theorem OAI.VelocityDetection.Stacks.update_capacity line 249
  36. theorem OAI.VelocityDetection.Stacks.address_count_geometric line 256