OAI/Analysis/MatrixSigning/Realization/RawRationalArrayMachine.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.RawRationalArrayMachine.extend line 13
  2. def OAI.CurrentKS.RawRationalArrayMachine.state line 16
  3. def OAI.CurrentKS.RawRationalArrayMachine.ports line 19
  4. def OAI.CurrentKS.RawRationalArrayMachine.normalizer line 20
  5. def OAI.CurrentKS.RawRationalArrayMachine.framePorts line 21
  6. def OAI.CurrentKS.RawRationalArrayMachine.framing line 22
  7. def OAI.CurrentKS.RawRationalArrayMachine.appendFrame line 23
  8. def OAI.CurrentKS.RawRationalArrayMachine.popCount line 24
  9. def OAI.CurrentKS.RawRationalArrayMachine.body line 25
  10. def OAI.CurrentKS.RawRationalArrayMachine.scan line 26
  11. def OAI.CurrentKS.RawRationalArrayMachine.finish line 27
  12. def OAI.CurrentKS.RawRationalArrayMachine.program line 28
  13. def OAI.CurrentKS.RawRationalArrayMachine.rawTape line 30
  14. def OAI.CurrentKS.RawRationalArrayMachine.canonicalTape line 31
  15. def OAI.CurrentKS.RawRationalArrayMachine.unary line 33
  16. lemma OAI.CurrentKS.RawRationalArrayMachine.extend_port line 35
  17. lemma OAI.CurrentKS.RawRationalArrayMachine.extend_other line 38
  18. lemma OAI.CurrentKS.RawRationalArrayMachine.normalizer_spec line 45
  19. lemma OAI.CurrentKS.RawRationalArrayMachine.framing_spec line 52
  20. lemma OAI.CurrentKS.RawRationalArrayMachine.appendFrame_spec line 60
  21. lemma OAI.CurrentKS.RawRationalArrayMachine.popCount_spec line 69
  22. def OAI.CurrentKS.RawRationalArrayMachine.bodyTicks line 78
  23. lemma OAI.CurrentKS.RawRationalArrayMachine.body_spec line 82
  24. lemma OAI.CurrentKS.RawRationalArrayMachine.bodyTicks_le line 95
  25. lemma OAI.CurrentKS.RawRationalArrayMachine.scan_trace line 103
  26. lemma OAI.CurrentKS.RawRationalArrayMachine.finish_spec line 128
  27. theorem OAI.CurrentKS.RawRationalArrayMachine.program_spec line 136
  28. lemma OAI.CurrentKS.RawRationalArrayMachine.member_length_le line 147
  29. lemma OAI.CurrentKS.RawRationalArrayMachine.count_le_raw line 158
  30. lemma OAI.CurrentKS.RawRationalArrayMachine.canonical_length_le line 166
  31. theorem OAI.CurrentKS.RawRationalArrayMachine.polynomial_spec line 176