OAI/GroupTheory/PeriodicGroups/Machines/RegisterOperators.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceBurnside.Structured.Binary.pushList line 11
  2. lemma OAI.SourceBurnside.Structured.Binary.pushList_run line 14
  3. def OAI.SourceBurnside.Structured.Binary.dropN line 23
  4. lemma OAI.SourceBurnside.Structured.Binary.dropN_run line 26
  5. abbrev OAI.SourceBurnside.Structured.Device.Constant.L line 43
  6. def OAI.SourceBurnside.Structured.Device.Constant.program line 45
  7. lemma OAI.SourceBurnside.Structured.Device.Constant.program_run line 49
  8. lemma OAI.SourceBurnside.Structured.Device.Constant.value_false line 79
  9. lemma OAI.SourceBurnside.Structured.Device.Constant.value_bits line 81
  10. def OAI.SourceBurnside.Structured.Device.constant line 91
  11. abbrev OAI.SourceBurnside.Structured.Device.AddOperator.L line 114
  12. def OAI.SourceBurnside.Structured.Device.AddOperator.load line 116
  13. def OAI.SourceBurnside.Structured.Device.AddOperator.program line 118
  14. def OAI.SourceBurnside.Structured.Device.AddOperator.loaded line 120
  15. def OAI.SourceBurnside.Structured.Device.AddOperator.first line 123
  16. def OAI.SourceBurnside.Structured.Device.AddOperator.second line 124
  17. lemma OAI.SourceBurnside.Structured.Device.AddOperator.load_run line 126
  18. lemma OAI.SourceBurnside.Structured.Device.AddOperator.program_run line 150
  19. def OAI.SourceBurnside.Structured.Device.add line 182
  20. abbrev OAI.SourceBurnside.Structured.Device.SubOperator.L line 211
  21. def OAI.SourceBurnside.Structured.Device.SubOperator.load line 213
  22. def OAI.SourceBurnside.Structured.Device.SubOperator.program line 215
  23. def OAI.SourceBurnside.Structured.Device.SubOperator.loaded line 217
  24. def OAI.SourceBurnside.Structured.Device.SubOperator.first line 220
  25. def OAI.SourceBurnside.Structured.Device.SubOperator.second line 221
  26. lemma OAI.SourceBurnside.Structured.Device.SubOperator.load_run line 223
  27. lemma OAI.SourceBurnside.Structured.Device.SubOperator.program_run line 247
  28. def OAI.SourceBurnside.Structured.Device.subtract line 279
  29. abbrev OAI.SourceBurnside.Structured.Device.CompareOperator.L line 303
  30. def OAI.SourceBurnside.Structured.Device.CompareOperator.finish line 305
  31. def OAI.SourceBurnside.Structured.Device.CompareOperator.program line 307
  32. def OAI.SourceBurnside.Structured.Device.CompareOperator.padded line 309
  33. lemma OAI.SourceBurnside.Structured.Device.CompareOperator.padded_length line 310
  34. lemma OAI.SourceBurnside.Structured.Device.CompareOperator.padded_value line 311
  35. lemma OAI.SourceBurnside.Structured.Device.CompareOperator.finish_run line 314
  36. lemma OAI.SourceBurnside.Structured.Device.CompareOperator.program_run line 346
  37. def OAI.SourceBurnside.Structured.Device.lessEqualReversed line 372
  38. abbrev OAI.SourceBurnside.Structured.Device.MultiplyOperator.L line 396
  39. def OAI.SourceBurnside.Structured.Device.MultiplyOperator.load line 398
  40. def OAI.SourceBurnside.Structured.Device.MultiplyOperator.program line 401
  41. def OAI.SourceBurnside.Structured.Device.MultiplyOperator.loaded line 402
  42. lemma OAI.SourceBurnside.Structured.Device.MultiplyOperator.load_run line 405
  43. lemma OAI.SourceBurnside.Structured.Device.MultiplyOperator.program_run line 439
  44. def OAI.SourceBurnside.Structured.Device.multiply line 476
  45. abbrev OAI.SourceBurnside.Structured.Device.DivideOperator.L line 507
  46. def OAI.SourceBurnside.Structured.Device.DivideOperator.load line 509
  47. def OAI.SourceBurnside.Structured.Device.DivideOperator.chosen line 514
  48. def OAI.SourceBurnside.Structured.Device.DivideOperator.other line 515
  49. def OAI.SourceBurnside.Structured.Device.DivideOperator.program line 516
  50. def OAI.SourceBurnside.Structured.Device.DivideOperator.loaded line 518
  51. lemma OAI.SourceBurnside.Structured.Device.DivideOperator.load_run line 521
  52. lemma OAI.SourceBurnside.Structured.Device.DivideOperator.finish_run line 571
  53. lemma OAI.SourceBurnside.Structured.Device.DivideOperator.program_correct line 593
  54. def OAI.SourceBurnside.Structured.Device.divide line 631