OAI/Analysis/CircleDomains/Selection/InitialBlockPiece.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Replace the first true piece of a grouped chain. This operation is used when consecutive true edges are joined during chain normalization.

  1. def OAI.CircleDomainRigidity.replaceInitialTruePiece line 20
  2. theorem OAI.CircleDomainRigidity.replaceInitialTruePiece_end line 26
  3. theorem OAI.CircleDomainRigidity.replaceInitialTruePiece_valid line 37
  4. theorem OAI.CircleDomainRigidity.replaceInitialTruePiece_cost line 67