OAI/Combinatorics/HoneycombCorridor/Excursions.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumBridge.Corridor.reverseGerm line 10
  2. def OAI.PolynomialVacuumBridge.Corridor.reverseTurns line 12
  3. theorem OAI.PolynomialVacuumBridge.Corridor.reverseGerm_reverseGerm line 14
  4. theorem OAI.PolynomialVacuumBridge.Corridor.reverseTurns_reverseTurns line 19
  5. theorem OAI.PolynomialVacuumBridge.Corridor.reverseTurns_nil line 23
  6. theorem OAI.PolynomialVacuumBridge.Corridor.reverseTurns_cons line 25
  7. theorem OAI.PolynomialVacuumBridge.Corridor.terminalGerm_append line 29
  8. theorem OAI.PolynomialVacuumBridge.Corridor.traced_append line 35
  9. theorem OAI.PolynomialVacuumBridge.Corridor.advance_reverse line 41
  10. theorem OAI.PolynomialVacuumBridge.Corridor.terminalGerm_reverse line 46
  11. theorem OAI.PolynomialVacuumBridge.Corridor.traced_reverse line 54
  12. theorem OAI.PolynomialVacuumBridge.Corridor.stepWeight_not line 63
  13. theorem OAI.PolynomialVacuumBridge.Corridor.wordWeight_reverse line 72
  14. theorem OAI.PolynomialVacuumBridge.Corridor.stopped_of_trace line 81
  15. def OAI.PolynomialVacuumBridge.Corridor.IsExcursion line 94
  16. def OAI.PolynomialVacuumBridge.Corridor.excursions line 98
  17. theorem OAI.PolynomialVacuumBridge.Corridor.mem_excursions line 103
  18. def OAI.PolynomialVacuumBridge.Corridor.reverseExcursion line 115
  19. theorem OAI.PolynomialVacuumBridge.Corridor.reverseExcursion_reverseExcursion line 118
  20. theorem OAI.PolynomialVacuumBridge.Corridor.IsExcursion.nonempty line 123
  21. theorem OAI.PolynomialVacuumBridge.Corridor.reverse_first_mem line 128
  22. theorem OAI.PolynomialVacuumBridge.Corridor.IsExcursion.reverse line 140
  23. theorem OAI.PolynomialVacuumBridge.Corridor.reverseExcursion_mem line 153
  24. def OAI.PolynomialVacuumBridge.Corridor.visitSum line 158
  25. theorem OAI.PolynomialVacuumBridge.Corridor.visitSum_conj line 162
  26. theorem OAI.PolynomialVacuumBridge.Corridor.visitSum_im line 178
  27. def OAI.PolynomialVacuumBridge.Corridor.markedLeaves line 181
  28. def OAI.PolynomialVacuumBridge.Corridor.firstArrival line 185
  29. theorem OAI.PolynomialVacuumBridge.Corridor.sum_leaves_of_mem line 190
  30. theorem OAI.PolynomialVacuumBridge.Corridor.leaves_of_not_mem line 199
  31. theorem OAI.PolynomialVacuumBridge.Corridor.markedLeaves_eq_firstArrival line 202
  32. def OAI.PolynomialVacuumBridge.Corridor.exitSum line 249
  33. def OAI.PolynomialVacuumBridge.Corridor.collisionSum line 253
  34. theorem OAI.PolynomialVacuumBridge.Corridor.exit_add_collision line 257
  35. def OAI.PolynomialVacuumBridge.Corridor.boundaryGerms line 267
  36. theorem OAI.PolynomialVacuumBridge.Corridor.mem_boundaryGerms line 271
  37. def OAI.PolynomialVacuumBridge.Corridor.firstArrivals line 276
  38. theorem OAI.PolynomialVacuumBridge.Corridor.mem_firstArrivals line 283
  39. def OAI.PolynomialVacuumBridge.Corridor.rayExits line 296
  40. theorem OAI.PolynomialVacuumBridge.Corridor.mem_rayExits line 303
  41. def OAI.PolynomialVacuumBridge.Corridor.reversePrefix line 316
  42. def OAI.PolynomialVacuumBridge.Corridor.reverseRay line 319
  43. theorem OAI.PolynomialVacuumBridge.Corridor.reversePrefix_initial line 322
  44. theorem OAI.PolynomialVacuumBridge.Corridor.reversePrefix_mem line 328
  45. theorem OAI.PolynomialVacuumBridge.Corridor.reverseRay_mem line 346
  46. theorem OAI.PolynomialVacuumBridge.Corridor.reversePrefix_reverseRay line 369
  47. theorem OAI.PolynomialVacuumBridge.Corridor.reverseRay_reversePrefix line 375
  48. theorem OAI.PolynomialVacuumBridge.Corridor.prefix_ray_reversal line 381
  49. theorem OAI.PolynomialVacuumBridge.Corridor.IsExcursion.distinct_ports line 399