OAI/Combinatorics/VariableWL/Program.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VariableWL.Computation.Symbol line 9
  2. def OAI.VariableWL.Computation.bitSymbol line 11
  3. def OAI.VariableWL.Computation.typedWordCells line 13
  4. structure OAI.VariableWL.Computation.Program line 16
  5. structure OAI.VariableWL.Computation.State line 20
  6. theorem OAI.VariableWL.Computation.configuration_ext line 25
  7. def OAI.VariableWL.Computation.Program.initial line 34
  8. def OAI.VariableWL.Computation.Program.step line 39
  9. def OAI.VariableWL.Computation.Program.run line 45
  10. def OAI.VariableWL.Computation.Program.OutputsWithin line 49
  11. def OAI.VariableWL.Computation.Program.controlCode line 56
  12. def OAI.VariableWL.Computation.Program.symbolCode line 60
  13. theorem OAI.VariableWL.Computation.Program.controlCode_injective line 66
  14. theorem OAI.VariableWL.Computation.Program.symbolCode_injective line 81
  15. def OAI.VariableWL.Computation.Program.controlDecode line 119
  16. def OAI.VariableWL.Computation.Program.symbolDecode line 120
  17. theorem OAI.VariableWL.Computation.Program.control_roundtrip line 122
  18. theorem OAI.VariableWL.Computation.Program.symbol_roundtrip line 124
  19. def OAI.VariableWL.Computation.Program.compile line 127
  20. def OAI.VariableWL.Computation.Program.encodeState line 135
  21. theorem OAI.VariableWL.Computation.Program.encodeWord line 140
  22. theorem OAI.VariableWL.Computation.Program.encode_initial line 149
  23. theorem OAI.VariableWL.Computation.Program.encode_step line 159
  24. theorem OAI.VariableWL.Computation.Program.encode_run line 175
  25. theorem OAI.VariableWL.Computation.Program.compile_outputs line 183
  26. theorem OAI.VariableWL.Computation.typedWordCells_nil line 203
  27. theorem OAI.VariableWL.Computation.typedWordCells_cons line 207
  28. def OAI.VariableWL.Computation.stackCells line 227
  29. def OAI.VariableWL.Computation.stackHead line 228
  30. theorem OAI.VariableWL.Computation.stackCells_nil line 230
  31. theorem OAI.VariableWL.Computation.stackCells_cons line 233
  32. theorem OAI.VariableWL.Computation.stackCells_head line 246
  33. theorem OAI.VariableWL.Computation.stackCells_below line 256
  34. theorem OAI.VariableWL.Computation.stackCells_nonnegative line 263
  35. inductive OAI.VariableWL.Computation.Stack.Action line 272
  36. def OAI.VariableWL.Computation.Stack.Action.apply line 276
  37. def OAI.VariableWL.Computation.Stack.Action.firstMove line 281
  38. def OAI.VariableWL.Computation.Stack.Action.firstWrite line 286
  39. def OAI.VariableWL.Computation.Stack.Action.secondWrite line 289
  40. theorem OAI.VariableWL.Computation.Stack.firstUpdate line 294
  41. theorem OAI.VariableWL.Computation.Stack.secondUpdate line 300
  42. structure OAI.VariableWL.Computation.Stack.Machine line 343
  43. structure OAI.VariableWL.Computation.Stack.State line 348
  44. def OAI.VariableWL.Computation.Stack.Machine.step line 354
  45. def OAI.VariableWL.Computation.Stack.Machine.initial line 358
  46. def OAI.VariableWL.Computation.Stack.Machine.run line 362
  47. def OAI.VariableWL.Computation.Stack.Machine.OutputsWithin line 366
  48. theorem OAI.VariableWL.Computation.Stack.Action.length_apply_le line 369
  49. theorem OAI.VariableWL.Computation.Stack.Machine.length_run line 373