OAI/MathematicalPhysics/NavierStokes/VelocityDetection/History.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.VelocityDetection.History.Configuration line 17

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

  2. def OAI.VelocityDetection.History.radix line 39

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

  3. def OAI.VelocityDetection.History.tag line 41

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

  4. theorem OAI.VelocityDetection.History.tag_lt line 45
  5. theorem OAI.VelocityDetection.History.radix_pos line 51
  6. def OAI.VelocityDetection.History.applyRule line 54

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

  7. theorem OAI.VelocityDetection.History.recover_tag line 59
  8. theorem OAI.VelocityDetection.History.recover_history line 66
  9. theorem OAI.VelocityDetection.History.tag_decode_state line 73
  10. theorem OAI.VelocityDetection.History.tag_decode_read line 78
  11. theorem OAI.VelocityDetection.History.applyRule_injective line 82
  12. def OAI.VelocityDetection.History.next line 110
  13. theorem OAI.VelocityDetection.History.next_tape line 113
  14. def OAI.VelocityDetection.History.orbit line 117
  15. theorem OAI.VelocityDetection.History.orbit_zero line 121
  16. theorem OAI.VelocityDetection.History.orbit_succ line 123
  17. theorem OAI.VelocityDetection.History.orbit_tape line 126
  18. def OAI.VelocityDetection.History.Halts line 132
  19. theorem OAI.VelocityDetection.History.halts_iff line 135
  20. def OAI.VelocityDetection.History.Fits line 140
  21. theorem OAI.VelocityDetection.History.applyRule_fits line 145
  22. theorem OAI.VelocityDetection.History.next_fits line 151
  23. theorem OAI.VelocityDetection.History.orbit_fits line 164
  24. def OAI.VelocityDetection.History.packedState line 173

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

  25. theorem OAI.VelocityDetection.History.packedState_lt line 175
  26. theorem OAI.VelocityDetection.History.packedState_mod line 178
  27. theorem OAI.VelocityDetection.History.packedState_div line 181
  28. def OAI.VelocityDetection.History.address line 185

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

  29. theorem OAI.VelocityDetection.History.address_le line 188
  30. theorem OAI.VelocityDetection.History.address_injective line 192
  31. theorem OAI.VelocityDetection.History.address_count_geometric line 207
  32. abbrev OAI.VelocityDetection.History.Box line 213

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

  33. def OAI.VelocityDetection.History.config line 215

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

  34. theorem OAI.VelocityDetection.History.config_fits line 218
  35. theorem OAI.VelocityDetection.History.config_injective line 221
  36. def OAI.VelocityDetection.History.Active line 228

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

  37. instance OAI.VelocityDetection.History.(instance at line 230) line 230
  38. def OAI.VelocityDetection.History.rule line 234

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

  39. theorem OAI.VelocityDetection.History.lookup_rule line 237
  40. def OAI.VelocityDetection.History.target line 241

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

  41. def OAI.VelocityDetection.History.sourceAddress line 244

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

  42. def OAI.VelocityDetection.History.targetAddress line 246

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

  43. theorem OAI.VelocityDetection.History.sourceAddress_injective line 248
  44. theorem OAI.VelocityDetection.History.target_fits line 254
  45. theorem OAI.VelocityDetection.History.targetAddress_injective line 258
  46. theorem OAI.VelocityDetection.History.sourceAddress_count line 266
  47. theorem OAI.VelocityDetection.History.targetAddress_count line 269