OAI/Analysis/MatrixSigning/Realization/DenseInputMachine.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentKS.DenseInputMachine.frame_eq line 11
  2. lemma OAI.CurrentKS.DenseInputMachine.encodeNat_eq line 16
  3. lemma OAI.CurrentKS.DenseInputMachine.encodeInt_eq line 19
  4. def OAI.CurrentKS.DenseInputMachine.layout line 22
  5. def OAI.CurrentKS.DenseInputMachine.dimPorts line 25
  6. def OAI.CurrentKS.DenseInputMachine.countPorts line 26
  7. def OAI.CurrentKS.DenseInputMachine.readDimension line 27
  8. def OAI.CurrentKS.DenseInputMachine.readCount line 28
  9. def OAI.CurrentKS.DenseInputMachine.readHeader line 29
  10. def OAI.CurrentKS.DenseInputMachine.denseTape line 31
  11. def OAI.CurrentKS.DenseInputMachine.headerTicks line 33
  12. lemma OAI.CurrentKS.DenseInputMachine.readDimension_spec line 37
  13. lemma OAI.CurrentKS.DenseInputMachine.readCount_spec line 47
  14. theorem OAI.CurrentKS.DenseInputMachine.readHeader_spec line 57
  15. lemma OAI.CurrentKS.DenseInputMachine.length_frame line 68
  16. theorem OAI.CurrentKS.DenseInputMachine.headerTicks_le line 72
  17. lemma OAI.CurrentKS.DenseInputMachine.denseTape_length_le line 77
  18. lemma OAI.CurrentKS.DenseInputMachine.matrixTape_nonempty line 81
  19. lemma OAI.CurrentKS.DenseInputMachine.denseTape_eq_nil_iff line 84
  20. lemma OAI.CurrentKS.DenseInputMachine.denseTape_dim_zero line 98
  21. def OAI.CurrentKS.DenseInputMachine.trivialTail line 111
  22. def OAI.CurrentKS.DenseInputMachine.trivialProgram line 113
  23. lemma OAI.CurrentKS.DenseInputMachine.trivialTail_spec line 115
  24. theorem OAI.CurrentKS.DenseInputMachine.trivialProgram_spec line 124
  25. lemma OAI.CurrentKS.DenseInputMachine.trivialOutput_good line 144