OAI/Analysis/CircleDomains/Selection/PrependOldBlockJump.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Prepend an old jump, creating a new first block with one true piece. The old disk label and its toll are retained exactly.

  1. abbrev OAI.CircleDomainRigidity.prependOldJumpPattern line 15
  2. theorem OAI.CircleDomainRigidity.blockAnchors_prependOld_tail line 20
  3. theorem OAI.CircleDomainRigidity.blockAnchors_change_first_succ line 31
  4. def OAI.CircleDomainRigidity.prependOldBlockJump line 40
  5. theorem OAI.CircleDomainRigidity.prependOldBlockJump_valid line 47
  6. theorem OAI.CircleDomainRigidity.prependOldBlockJump_cost line 92