OAI/Combinatorics/HoneycombCorridor/CollisionHistories.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialVacuumBridge.Corridor.neighbor_ne_self line 10
  2. theorem OAI.PolynomialVacuumBridge.Corridor.outgoingSlot_ne line 13
  3. theorem OAI.PolynomialVacuumBridge.Corridor.terminal_previous_mem line 17
  4. theorem OAI.PolynomialVacuumBridge.Corridor.terminal_previous_suffix line 27
  5. theorem OAI.PolynomialVacuumBridge.Corridor.return_slot_ne_outgoing line 31
  6. theorem OAI.PolynomialVacuumBridge.Corridor.return_slot_ne_incoming line 55
  7. theorem OAI.PolynomialVacuumBridge.Corridor.collision_root_slots line 67
  8. def OAI.PolynomialVacuumBridge.Corridor.reverseAt line 88
  9. theorem OAI.PolynomialVacuumBridge.Corridor.reverseAt_involutive line 93
  10. theorem OAI.PolynomialVacuumBridge.Corridor.reverseAt_length line 102
  11. theorem OAI.PolynomialVacuumBridge.Corridor.stopped_iff_trace line 109
  12. theorem OAI.PolynomialVacuumBridge.Corridor.reverse_return_trace line 141
  13. theorem OAI.PolynomialVacuumBridge.Corridor.reverse_advance_vertex line 170
  14. theorem OAI.PolynomialVacuumBridge.Corridor.reverseAt_collision line 174
  15. def OAI.PolynomialVacuumBridge.Corridor.collisionReverse line 198
  16. theorem OAI.PolynomialVacuumBridge.Corridor.collisionReverse_properties line 201
  17. theorem OAI.PolynomialVacuumBridge.Corridor.collisionReverse_leaf line 213