OAI/Analysis/MatrixSigning/Matrices/PivotRowLoop.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.KS.W17.PivotRowLoop.Outcome line 9
  2. def OAI.KS.W17.PivotRowLoop.entry line 14
  3. def OAI.KS.W17.PivotRowLoop.outcome line 17
  4. def OAI.KS.W17.PivotRowLoop.state line 21
  5. def OAI.KS.W17.PivotRowLoop.guard line 26
  6. def OAI.KS.W17.PivotRowLoop.program line 30
  7. def OAI.KS.W17.PivotRowLoop.config line 32
  8. def OAI.KS.W17.PivotRowLoop.entryTicks line 34
  9. def OAI.KS.W17.PivotRowLoop.ticks line 37
  10. theorem OAI.KS.W17.PivotRowLoop.step_empty line 41
  11. theorem OAI.KS.W17.PivotRowLoop.step_found line 51
  12. theorem OAI.KS.W17.PivotRowLoop.step_call line 61
  13. theorem OAI.KS.W17.PivotRowLoop.body_spec line 76
  14. theorem OAI.KS.W17.PivotRowLoop.run_scan line 100