OAI/MathematicalPhysics/AlternatingFlow/Encoding.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AlternatingNS.Encoding.code line 10
  2. def OAI.AlternatingNS.Encoding.tailMax line 14
  3. lemma OAI.AlternatingNS.Encoding.tailMax_nonneg line 18
  4. lemma OAI.AlternatingNS.Encoding.tailMax_lt_one line 23
  5. lemma OAI.AlternatingNS.Encoding.tailMax_identity line 29
  6. lemma OAI.AlternatingNS.Encoding.code_nonneg line 37
  7. lemma OAI.AlternatingNS.Encoding.code_le_tailMax line 42
  8. lemma OAI.AlternatingNS.Encoding.digit_interval line 54
  9. lemma OAI.AlternatingNS.Encoding.code_append line 63
  10. lemma OAI.AlternatingNS.Encoding.code_denominator line 73
  11. lemma OAI.AlternatingNS.Encoding.configuration_block line 88
  12. lemma OAI.AlternatingNS.Encoding.integral_rescale line 94
  13. lemma OAI.AlternatingNS.Encoding.sum_integral line 104
  14. def OAI.AlternatingNS.Encoding.donor line 114
  15. lemma OAI.AlternatingNS.Encoding.old_record_integral line 117
  16. lemma OAI.AlternatingNS.Encoding.donor_integer_add line 133
  17. def OAI.AlternatingNS.Encoding.DecoderLaw line 152
  18. lemma OAI.AlternatingNS.Encoding.decoder_int_add line 155
  19. lemma OAI.AlternatingNS.Encoding.read_current line 160
  20. lemma OAI.AlternatingNS.Encoding.remove_prefix line 169
  21. lemma OAI.AlternatingNS.Encoding.read_after_prefix line 185
  22. lemma OAI.AlternatingNS.Encoding.read_configuration line 193
  23. lemma OAI.AlternatingNS.Encoding.donor_in_plateau line 223
  24. lemma OAI.AlternatingNS.Encoding.pop_code line 247
  25. lemma OAI.AlternatingNS.Encoding.tape_step_right line 254
  26. lemma OAI.AlternatingNS.Encoding.tape_step_stay line 260
  27. lemma OAI.AlternatingNS.Encoding.tape_step_left line 266