OAI/MathematicalPhysics/AlternatingFlow/Machines.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AlternatingNS.Machine.Admissible line 10
  2. def OAI.AlternatingNS.Machine.command line 13
  3. lemma OAI.AlternatingNS.Machine.step_eq_command line 18
  4. lemma OAI.AlternatingNS.Machine.command_valid line 29
  5. lemma OAI.AlternatingNS.Machine.initial_admissible line 41
  6. lemma OAI.AlternatingNS.Machine.step_admissible line 52
  7. lemma OAI.AlternatingNS.Machine.run_zero line 63
  8. lemma OAI.AlternatingNS.Machine.run_succ line 65
  9. lemma OAI.AlternatingNS.Machine.run_admissible line 69
  10. def OAI.AlternatingNS.Machine.Window line 75
  11. lemma OAI.AlternatingNS.Machine.initial_window line 79
  12. lemma OAI.AlternatingNS.Machine.step_window line 88
  13. lemma OAI.AlternatingNS.Machine.run_window line 101
  14. def OAI.AlternatingNS.Machine.leftDigits line 107
  15. def OAI.AlternatingNS.Machine.rightDigits line 108
  16. lemma OAI.AlternatingNS.Machine.leftDigits_padded line 110
  17. lemma OAI.AlternatingNS.Machine.rightDigits_padded line 116
  18. def OAI.AlternatingNS.Machine.base line 122
  19. lemma OAI.AlternatingNS.Machine.base_ge_four line 124
  20. lemma OAI.AlternatingNS.Machine.state_digit_bound line 129
  21. lemma OAI.AlternatingNS.Machine.symbol_digit_bound line 135
  22. def OAI.AlternatingNS.Encoding.digits line 147
  23. def OAI.AlternatingNS.Encoding.streamCode line 149
  24. lemma OAI.AlternatingNS.Encoding.digits_length line 151
  25. lemma OAI.AlternatingNS.Encoding.digits_succ line 154
  26. lemma OAI.AlternatingNS.Encoding.streamCode_succ line 158
  27. lemma OAI.AlternatingNS.Encoding.streamCode_congr line 162
  28. lemma OAI.AlternatingNS.Encoding.streamCode_extend_one line 168
  29. lemma OAI.AlternatingNS.Encoding.streamCode_padding line 176
  30. lemma OAI.AlternatingNS.Encoding.streamCode_pop line 182
  31. def OAI.AlternatingNS.Machine.leftCode line 195
  32. def OAI.AlternatingNS.Machine.rightCode line 198
  33. def OAI.AlternatingNS.Machine.recordedDigits line 201
  34. def OAI.AlternatingNS.Machine.recordedBlock line 206
  35. lemma OAI.AlternatingNS.Machine.recordedDigits_bound line 209
  36. lemma OAI.AlternatingNS.Machine.recordedBlock_mem line 221
  37. lemma OAI.AlternatingNS.Machine.recordedBlock_formula line 227
  38. lemma OAI.AlternatingNS.Machine.recordedBlock_integral line 236
  39. lemma OAI.AlternatingNS.Machine.read_run line 246
  40. def OAI.AlternatingNS.Machine.execute line 269
  41. lemma OAI.AlternatingNS.Machine.step_execute line 274
  42. lemma OAI.AlternatingNS.Machine.execute_right line 277
  43. lemma OAI.AlternatingNS.Machine.execute_stay line 292
  44. lemma OAI.AlternatingNS.Machine.execute_left line 305
  45. lemma OAI.AlternatingNS.Machine.code_execute_right line 322
  46. lemma OAI.AlternatingNS.Machine.code_execute_stay line 340
  47. lemma OAI.AlternatingNS.Machine.code_execute_left line 357