OAI/Combinatorics/VariableWL/Encoding.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VariableWL.Computation.Stack.Stores line 7
  2. abbrev OAI.VariableWL.Computation.Stack.Heads line 8
  3. abbrev OAI.VariableWL.Computation.Stack.Actions line 9
  4. def OAI.VariableWL.Computation.Stack.heads line 11
  5. def OAI.VariableWL.Computation.Stack.execute line 12
  6. def OAI.VariableWL.Computation.Stack.nop line 13
  7. theorem OAI.VariableWL.Computation.Stack.execute_nop line 14
  8. inductive OAI.VariableWL.Computation.Stack.Code line 16
  9. def OAI.VariableWL.Computation.Stack.Code.Control line 25
  10. instance OAI.VariableWL.Computation.Stack.Code.controlFintype line 32
  11. def OAI.VariableWL.Computation.Stack.Code.start line 40
  12. def OAI.VariableWL.Computation.Stack.Code.transition line 47
  13. def OAI.VariableWL.Computation.Stack.Code.machine line 65
  14. def OAI.VariableWL.Computation.Stack.Code.step line 70
  15. theorem OAI.VariableWL.Computation.Stack.Code.machine_step line 73
  16. def OAI.VariableWL.Computation.Stack.Code.liftState line 75
  17. theorem OAI.VariableWL.Computation.Stack.Code.lift_steps line 77
  18. inductive OAI.VariableWL.Computation.Stack.Code.Eval line 96
  19. theorem OAI.VariableWL.Computation.Stack.Code.eval_steps line 106
  20. theorem OAI.VariableWL.Computation.Stack.Code.eval_outputs line 150
  21. def OAI.VariableWL.Encoding.value line 175
  22. theorem OAI.VariableWL.Encoding.value_bits line 176
  23. def OAI.VariableWL.Encoding.header line 181
  24. theorem OAI.VariableWL.Encoding.header_code line 186
  25. theorem OAI.VariableWL.Encoding.header_sound line 191
  26. def OAI.VariableWL.Encoding.integer line 204
  27. theorem OAI.VariableWL.Encoding.integer_code line 214
  28. theorem OAI.VariableWL.Encoding.integer_sound line 223
  29. theorem OAI.VariableWL.Encoding.integer_prefix_injective line 238
  30. def OAI.VariableWL.Encoding.matrix line 244
  31. theorem OAI.VariableWL.Encoding.matrix_flat line 248
  32. theorem OAI.VariableWL.Encoding.graphCode_eq line 267
  33. theorem OAI.VariableWL.Encoding.matrix_length line 271
  34. theorem OAI.VariableWL.Encoding.graph_prefix_injective line 273
  35. theorem OAI.VariableWL.Encoding.pair_injective line 299
  36. theorem OAI.VariableWL.Encoding.pair_mem_WL line 308
  37. theorem OAI.VariableWL.Encoding.pair_mem_SubWL line 316
  38. def OAI.VariableWL.Computation.Stack.Code.one line 332
  39. theorem OAI.VariableWL.Computation.Stack.Code.execute_one line 334
  40. def OAI.VariableWL.Computation.Stack.Code.push line 341
  41. def OAI.VariableWL.Computation.Stack.Code.pop line 342
  42. def OAI.VariableWL.Computation.Stack.Code.clear line 343
  43. theorem OAI.VariableWL.Computation.Stack.Code.eval_push line 345
  44. theorem OAI.VariableWL.Computation.Stack.Code.eval_pop line 349
  45. theorem OAI.VariableWL.Computation.Stack.Code.eval_clear_update line 353
  46. theorem OAI.VariableWL.Computation.Stack.Code.eval_clear line 363
  47. def OAI.VariableWL.Computation.Stack.Code.transfer line 367
  48. def OAI.VariableWL.Computation.Stack.Code.pairStore line 371
  49. theorem OAI.VariableWL.Computation.Stack.Code.transfer_action line 374
  50. theorem OAI.VariableWL.Computation.Stack.Code.eval_transfer_pair line 388
  51. theorem OAI.VariableWL.Computation.Stack.Code.eval_transfer line 402