OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/Subprogram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Removing instructions preserves the geometric conditions of a processor. The fresh-state initializer uses this to remove an unreachable incoming row.

  1. def OAI.ShearFlows.Input.withInstructions line 10
  2. theorem OAI.ShearFlows.ValidInput.withInstructions line 13
  3. def OAI.ShearFlows.Input.filterInstructions line 50
  4. theorem OAI.ShearFlows.ValidInput.filterInstructions line 53
  5. theorem OAI.ShearFlows.PositivelySeparated.symm line 57
  6. theorem OAI.ShearFlows.indexed_cons_separation line 62
  7. theorem OAI.ShearFlows.ValidInput.consInstruction line 78
  8. theorem OAI.ShearFlows.ValidInput.prependSublist line 119