OAI/Combinatorics/ThinTrees/Signing/Realization.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Signing realization.

  1. structure OAI.AlgorithmicThinTrees.Signing.Stack.Frame line 15
  2. abbrev OAI.AlgorithmicThinTrees.Signing.Stack.frameDataCode line 20
  3. def OAI.AlgorithmicThinTrees.Signing.Stack.Frame.data line 21
  4. def OAI.AlgorithmicThinTrees.Signing.Stack.frameCode line 22
  5. abbrev OAI.AlgorithmicThinTrees.Signing.Stack.frameView line 23
  6. instance OAI.AlgorithmicThinTrees.Signing.Stack.poly_frameView line 25
  7. abbrev OAI.AlgorithmicThinTrees.Signing.Stack.frameDim line 29
  8. abbrev OAI.AlgorithmicThinTrees.Signing.Stack.frameRows line 30
  9. instance OAI.AlgorithmicThinTrees.Signing.Stack.poly_frameDim line 31
  10. instance OAI.AlgorithmicThinTrees.Signing.Stack.poly_frameRows line 35
  11. def OAI.AlgorithmicThinTrees.Signing.Stack.complexField line 39
  12. instance OAI.AlgorithmicThinTrees.Signing.Stack.poly_complexField line 41
  13. def OAI.AlgorithmicThinTrees.Signing.Stack.outerFields line 43
  14. instance OAI.AlgorithmicThinTrees.Signing.Stack.poly_outerFields line 50
  15. lemma OAI.AlgorithmicThinTrees.Signing.Stack.outerFields_data line 52
  16. def OAI.AlgorithmicThinTrees.Signing.Stack.signerInput line 59
  17. instance OAI.AlgorithmicThinTrees.Signing.Stack.poly_signerInput line 71
  18. def OAI.AlgorithmicThinTrees.Signing.Stack.signs line 75
  19. lemma OAI.AlgorithmicThinTrees.Signing.Stack.runsPoly_signs line 79
  20. structure OAI.AlgorithmicThinTrees.Signing.Stack.FormFrame line 85
  21. abbrev OAI.AlgorithmicThinTrees.Signing.Stack.formDataCode line 90
  22. def OAI.AlgorithmicThinTrees.Signing.Stack.FormFrame.data line 91
  23. def OAI.AlgorithmicThinTrees.Signing.Stack.formCode line 92
  24. abbrev OAI.AlgorithmicThinTrees.Signing.Stack.formView line 93
  25. instance OAI.AlgorithmicThinTrees.Signing.Stack.poly_formView line 95
  26. abbrev OAI.AlgorithmicThinTrees.Signing.Stack.formMatrix line 99
  27. abbrev OAI.AlgorithmicThinTrees.Signing.Stack.formRows line 100
  28. lemma OAI.AlgorithmicThinTrees.Signing.Stack.factorColumns_data line 102
  29. def OAI.AlgorithmicThinTrees.Signing.Stack.factorRows line 111
  30. lemma OAI.AlgorithmicThinTrees.Signing.Stack.runsPoly_factorRows line 116
  31. def OAI.AlgorithmicThinTrees.Signing.Stack.FormFrame.whiten line 129
  32. def OAI.AlgorithmicThinTrees.Signing.Stack.whiten line 133
  33. lemma OAI.AlgorithmicThinTrees.Signing.Stack.runsPoly_whiten line 147
  34. structure OAI.AlgorithmicThinTrees.Signing.Stack.FramePair line 164
  35. def OAI.AlgorithmicThinTrees.Signing.Stack.FramePair.left line 171
  36. def OAI.AlgorithmicThinTrees.Signing.Stack.FramePair.right line 172
  37. def OAI.AlgorithmicThinTrees.Signing.Stack.FramePair.stack line 173
  38. def OAI.AlgorithmicThinTrees.Signing.Stack.pairCode line 175
  39. abbrev OAI.AlgorithmicThinTrees.Signing.Stack.pairView line 176
  40. instance OAI.AlgorithmicThinTrees.Signing.Stack.poly_pairView line 180
  41. abbrev OAI.AlgorithmicThinTrees.Signing.Stack.pairLeft line 184
  42. abbrev OAI.AlgorithmicThinTrees.Signing.Stack.pairRight line 185
  43. lemma OAI.AlgorithmicThinTrees.Signing.Stack.stack_data line 187
  44. def OAI.AlgorithmicThinTrees.Signing.Stack.stack line 195
  45. instance OAI.AlgorithmicThinTrees.Signing.Stack.poly_stack line 209
  46. structure OAI.AlgorithmicThinTrees.Signing.Stack.FormPair line 215
  47. def OAI.AlgorithmicThinTrees.Signing.Stack.FormPair.left line 222
  48. def OAI.AlgorithmicThinTrees.Signing.Stack.FormPair.right line 223
  49. def OAI.AlgorithmicThinTrees.Signing.Stack.FormPair.whiten line 224
  50. def OAI.AlgorithmicThinTrees.Signing.Stack.formsCode line 226
  51. abbrev OAI.AlgorithmicThinTrees.Signing.Stack.formsView line 227
  52. instance OAI.AlgorithmicThinTrees.Signing.Stack.poly_formsView line 231
  53. abbrev OAI.AlgorithmicThinTrees.Signing.Stack.formsLeft line 235
  54. abbrev OAI.AlgorithmicThinTrees.Signing.Stack.formsRight line 236
  55. def OAI.AlgorithmicThinTrees.Signing.Stack.whitenPair line 238
  56. def OAI.AlgorithmicThinTrees.Signing.Stack.simultaneousSigns line 242
  57. lemma OAI.AlgorithmicThinTrees.Signing.Stack.runsPoly_simultaneousSigns line 248