OAI/Combinatorics/UniformKServer/LevelHeavyEdits.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Heavy key edits on the actual tape, with a tape-independent auxiliary ramp.

  1. def OAI.UniformKServer.LevelMap.Data.heavyPotential line 19
  2. def OAI.UniformKServer.LevelMap.Data.heavyTrigger line 22
  3. def OAI.UniformKServer.LevelMap.Data.heavyEdit line 26
  4. theorem OAI.UniformKServer.LevelMap.Data.heavyEdit_le line 29
  5. theorem OAI.UniformKServer.LevelMap.Data.heavyFlag_at line 38
  6. theorem OAI.UniformKServer.LevelMap.Data.heavy_stationary line 43
  7. theorem OAI.UniformKServer.LevelMap.Data.heavy_mover line 56