OAI/Combinatorics/KMedianRecovery/Recovery/FrameStacks.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.frameStacks line 9
  2. lemma OAI.MetricKMedianRecovery.BitMachine.frameStacks_inl line 11
  3. lemma OAI.MetricKMedianRecovery.BitMachine.frameStacks_inr line 14
  4. lemma OAI.MetricKMedianRecovery.BitMachine.frameStacks_update line 17
  5. lemma OAI.MetricKMedianRecovery.BitMachine.stepAux_frame line 23
  6. lemma OAI.MetricKMedianRecovery.BitMachine.extractPrefix_length line 50
  7. abbrev OAI.MetricKMedianRecovery.BitMachine.MapLeft.Stack line 60
  8. abbrev OAI.MetricKMedianRecovery.BitMachine.MapLeft.Label line 61
  9. abbrev OAI.MetricKMedianRecovery.BitMachine.MapLeft.State line 62
  10. def OAI.MetricKMedianRecovery.BitMachine.MapLeft.mapStacks line 64
  11. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.stacks_left line 65
  12. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.stacks_zero line 67
  13. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.stacks_one line 69
  14. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.updLeft line 71
  15. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.upd0 line 74
  16. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.upd1 line 80
  17. abbrev OAI.MetricKMedianRecovery.BitMachine.MapLeft.program line 87
  18. def OAI.MetricKMedianRecovery.BitMachine.MapLeft.pure line 128
  19. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.pure_at line 129
  20. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.pure_update line 130
  21. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.pure_nil line 132
  22. def OAI.MetricKMedianRecovery.BitMachine.MapLeft.cfg line 134
  23. def OAI.MetricKMedianRecovery.BitMachine.MapLeft.done line 136
  24. def OAI.MetricKMedianRecovery.BitMachine.MapLeft.runCfg line 139
  25. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.run_step line 142
  26. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.parse_nil line 156
  27. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.parse_false line 160
  28. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.parse_one line 164
  29. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.parse_true line 168
  30. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.restore_nil line 172
  31. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.restore_cons line 176
  32. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.reverse_nil line 180
  33. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.reverse_cons line 184
  34. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.encode_nil line 188
  35. lemma OAI.MetricKMedianRecovery.BitMachine.MapLeft.encode_cons line 191