OAI/Analysis/MatrixSigning/Machines/SchurTableMachine.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W07.SchurTableMachine.guard line 13
  2. def OAI.KS.W07.SchurTableMachine.columnIncrementPorts line 18
  3. def OAI.KS.W07.SchurTableMachine.rowIncrementPorts line 19
  4. def OAI.KS.W07.SchurTableMachine.columnBody line 21
  5. def OAI.KS.W07.SchurTableMachine.columnLoop line 24
  6. def OAI.KS.W07.SchurTableMachine.rowBody line 26
  7. def OAI.KS.W07.SchurTableMachine.rowLoop line 31
  8. def OAI.KS.W07.SchurTableMachine.«initialize» line 33
  9. def OAI.KS.W07.SchurTableMachine.finish line 36
  10. def OAI.KS.W07.SchurTableMachine.program line 39
  11. def OAI.KS.W07.SchurTableMachine.inputState line 41
  12. def OAI.KS.W07.SchurTableMachine.outputState line 45
  13. theorem OAI.KS.W07.SchurTableMachine.guard_empty line 52
  14. theorem OAI.KS.W07.SchurTableMachine.guard_cons line 65
  15. theorem OAI.KS.W07.SchurTableMachine.table_length line 78