OAI/Combinatorics/VariableWL/MachineCellular.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VariableWL.CircuitCatalog.Data.ext_fields line 6
  2. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.eval_validRequest line 18
  3. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.eval_source line 19
  4. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.eval_destination line 20
  5. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.eval_destinationForm line 21
  6. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.eval_domain line 22
  7. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.eval_map line 23
  8. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.eval_requestGate line 24
  9. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.eval_requestTest line 25
  10. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.eval_requestDomain line 26
  11. theorem OAI.VariableWL.CellularCatalog.Data.catalog_validRequest_eq line 29
  12. theorem OAI.VariableWL.CellularCatalog.Data.catalog_source_eq line 30
  13. theorem OAI.VariableWL.CellularCatalog.Data.catalog_destination_eq line 31
  14. theorem OAI.VariableWL.CellularCatalog.Data.catalog_destinationForm_eq line 32
  15. theorem OAI.VariableWL.CellularCatalog.Data.catalog_domain_eq line 33
  16. theorem OAI.VariableWL.CellularCatalog.Data.catalog_map_eq line 34
  17. theorem OAI.VariableWL.CellularCatalog.Data.catalog_requestGate_eq line 35
  18. theorem OAI.VariableWL.CellularCatalog.Data.catalog_requestTest_eq line 36
  19. theorem OAI.VariableWL.CellularCatalog.Data.catalog_requestDomain_eq line 37
  20. theorem OAI.VariableWL.CellularCatalog.Program.Listing.catalog_validRequest_field line 42
  21. theorem OAI.VariableWL.CellularCatalog.Program.Listing.catalog_validRequest_eval line 43
  22. theorem OAI.VariableWL.CellularCatalog.Program.Listing.catalog_source_field line 46
  23. theorem OAI.VariableWL.CellularCatalog.Program.Listing.catalog_source_eval line 47
  24. theorem OAI.VariableWL.CellularCatalog.Program.Listing.catalog_destination_field line 50
  25. theorem OAI.VariableWL.CellularCatalog.Program.Listing.catalog_destination_eval line 51
  26. theorem OAI.VariableWL.CellularCatalog.Program.Listing.catalog_destinationForm_field line 54
  27. theorem OAI.VariableWL.CellularCatalog.Program.Listing.catalog_destinationForm_eval line 55
  28. theorem OAI.VariableWL.CellularCatalog.Program.Listing.catalog_domain_field line 58
  29. theorem OAI.VariableWL.CellularCatalog.Program.Listing.catalog_domain_eval line 59
  30. theorem OAI.VariableWL.CellularCatalog.Program.Listing.catalog_map_field line 62
  31. theorem OAI.VariableWL.CellularCatalog.Program.Listing.catalog_map_eval line 63
  32. theorem OAI.VariableWL.CellularCatalog.Program.Listing.catalog_requestGate_field line 66
  33. theorem OAI.VariableWL.CellularCatalog.Program.Listing.catalog_requestGate_eval line 67
  34. theorem OAI.VariableWL.CellularCatalog.Program.Listing.catalog_requestTest_field line 70
  35. theorem OAI.VariableWL.CellularCatalog.Program.Listing.catalog_requestTest_eval line 71
  36. theorem OAI.VariableWL.CellularCatalog.Program.Listing.catalog_requestDomain_field line 74
  37. theorem OAI.VariableWL.CellularCatalog.Program.Listing.catalog_requestDomain_eval line 75
  38. theorem OAI.VariableWL.CellularCatalog.Program.Listing.catalog_eval line 78
  39. def OAI.VariableWL.MachineCellular.presentation line 109
  40. def OAI.VariableWL.MachineCellular.alpha line 110
  41. def OAI.VariableWL.MachineCellular.headLetter line 112
  42. def OAI.VariableWL.MachineCellular.tailLetter line 113
  43. def OAI.VariableWL.MachineCellular.emptyLetter line 114
  44. def OAI.VariableWL.MachineCellular.initial line 115
  45. theorem OAI.VariableWL.MachineCellular.input_eq line 118
  46. theorem OAI.VariableWL.MachineCellular.initial_length line 128
  47. def OAI.VariableWL.MachineCellular.letterInput line 134
  48. theorem OAI.VariableWL.MachineCellular.letterInput_eq line 137
  49. theorem OAI.VariableWL.MachineCellular.letterInput_original line 152
  50. def OAI.VariableWL.MachineCellular.inputProgram line 157
  51. theorem OAI.VariableWL.MachineCellular.cons_one_env1 line 164
  52. theorem OAI.VariableWL.MachineCellular.inputProgram_number line 165
  53. def OAI.VariableWL.MachineCellular.fixedPower line 171
  54. theorem OAI.VariableWL.MachineCellular.fixedPower_number line 174
  55. def OAI.VariableWL.MachineCellular.bitProgram line 179
  56. theorem OAI.VariableWL.MachineCellular.bitProgram_number line 182
  57. def OAI.VariableWL.MachineCellular.ruleCode line 186
  58. def OAI.VariableWL.MachineCellular.ruleProgram line 190
  59. def OAI.VariableWL.MachineCellular.acceptCode line 192
  60. def OAI.VariableWL.MachineCellular.acceptProgram line 194
  61. def OAI.VariableWL.MachineCellular.listing line 197
  62. theorem OAI.VariableWL.MachineCellular.presentation_encode line 214
  63. theorem OAI.VariableWL.MachineCellular.presentation_bound line 215
  64. theorem OAI.VariableWL.MachineCellular.presentation_valid line 216
  65. theorem OAI.VariableWL.MachineCellular.ruleCode_encode line 217
  66. theorem OAI.VariableWL.MachineCellular.ruleProgram_number line 224
  67. theorem OAI.VariableWL.MachineCellular.acceptProgram_bit line 232
  68. theorem OAI.VariableWL.MachineCellular.circuit_rule line 245
  69. theorem OAI.VariableWL.MachineCellular.circuit_input line 246
  70. theorem OAI.VariableWL.MachineCellular.circuit_blank line 248
  71. theorem OAI.VariableWL.MachineCellular.circuit_accepting line 249
  72. theorem OAI.VariableWL.MachineCellular.listing_good line 251
  73. theorem OAI.VariableWL.equivalent_iso_iff line 281
  74. theorem OAI.VariableWL.order_eq_of_iso line 288
  75. theorem OAI.VariableWL.subcubic_iso_iff line 290