OAI/Analysis/MatrixSigning/Realization/FaceRunRealization.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.Realization.packFace line 13
  2. def OAI.CurrentKS.Realization.FaceActive.nextBase line 20
  3. def OAI.CurrentKS.Realization.faNextBase line 23
  4. def OAI.CurrentKS.Realization.FaceParams.next line 28
  5. def OAI.CurrentKS.Realization.faceNext line 31
  6. lemma OAI.CurrentKS.Realization.minList_reverse line 42
  7. def OAI.CurrentKS.Realization.minList line 49
  8. def OAI.CurrentKS.Realization.fUniformDrop line 54
  9. def OAI.CurrentKS.Realization.fFuel line 66
  10. def OAI.CurrentKS.Realization.FaceParams.start line 70
  11. def OAI.CurrentKS.Realization.faceStart line 72
  12. lemma OAI.CurrentKS.Realization.run_eq_iterate line 81
  13. lemma OAI.CurrentKS.Realization.next_pack line 93
  14. lemma OAI.CurrentKS.Realization.next_iterate line 96
  15. def OAI.CurrentKS.Realization.faceRun line 105