OAI/Computability/BinPacking/Arithmetic/BinaryOrderMachine.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.BinaryOrderMachine.updateOrder line 12
  2. def OAI.BinPackingGap.BinaryOrderMachine.scanOrder line 15
  3. def OAI.BinPackingGap.BinaryOrderMachine.orderNat line 24
  4. theorem OAI.BinPackingGap.BinaryOrderMachine.orderNat_self line 27
  5. theorem OAI.BinPackingGap.BinaryOrderMachine.orderNat_bit line 30
  6. theorem OAI.BinPackingGap.BinaryOrderMachine.scanOrder_value line 43
  7. theorem OAI.BinPackingGap.BinaryOrderMachine.scanOrder_bits line 63
  8. theorem OAI.BinPackingGap.BinaryOrderMachine.orderNat_eq_lt line 67
  9. theorem OAI.BinPackingGap.BinaryOrderMachine.orderNat_eq_gt line 71
  10. theorem OAI.BinPackingGap.BinaryOrderMachine.orderNat_eq_eq line 76
  11. abbrev OAI.BinPackingGap.BinaryOrderMachine.Alphabet line 84
  12. abbrev OAI.BinPackingGap.BinaryOrderMachine.State line 85
  13. def OAI.BinPackingGap.BinaryOrderMachine.clean line 87
  14. def OAI.BinPackingGap.BinaryOrderMachine.exitAt line 89
  15. def OAI.BinPackingGap.BinaryOrderMachine.finish line 94
  16. def OAI.BinPackingGap.BinaryOrderMachine.loop line 97
  17. theorem OAI.BinPackingGap.BinaryOrderMachine.stepAux_exitAt line 111
  18. theorem OAI.BinPackingGap.BinaryOrderMachine.stepAux_finish line 116
  19. theorem OAI.BinPackingGap.BinaryOrderMachine.update_left line 121
  20. theorem OAI.BinPackingGap.BinaryOrderMachine.update_right line 132
  21. theorem OAI.BinPackingGap.BinaryOrderMachine.step_empty line 138
  22. theorem OAI.BinPackingGap.BinaryOrderMachine.step_nil_cons line 153
  23. theorem OAI.BinPackingGap.BinaryOrderMachine.step_cons_nil line 168
  24. theorem OAI.BinPackingGap.BinaryOrderMachine.step_cons_cons line 183
  25. theorem OAI.BinPackingGap.BinaryOrderMachine.trace_left_empty line 198
  26. theorem OAI.BinPackingGap.BinaryOrderMachine.compareTrace_prior line 223
  27. theorem OAI.BinPackingGap.BinaryOrderMachine.compareTrace line 258
  28. theorem OAI.BinPackingGap.BinaryOrderMachine.compareTrace_fromTapes line 271
  29. theorem OAI.BinPackingGap.BinaryOrderMachine.drained_other line 283
  30. def OAI.BinPackingGap.BinaryOrderMachine.compareInTime line 287
  31. def OAI.BinPackingGap.BinaryOrderMachine.compareNatInTime line 301
  32. inductive OAI.BinPackingGap.BinaryOrderMachine.PreserveLabel line 320
  33. abbrev OAI.BinPackingGap.BinaryOrderMachine.PreserveLabel.enumList line 324
  34. theorem OAI.BinPackingGap.BinaryOrderMachine.PreserveLabel.enumList_getElem?_ctorIdx_eq line 327
  35. theorem OAI.BinPackingGap.BinaryOrderMachine.PreserveLabel.enumList_nodup line 331
  36. instance OAI.BinPackingGap.BinaryOrderMachine.(instance at line 333) line 333
  37. def OAI.BinPackingGap.BinaryOrderMachine.preservingInstruction line 337
  38. def OAI.BinPackingGap.BinaryOrderMachine.preservingSteps line 349
  39. theorem OAI.BinPackingGap.BinaryOrderMachine.preservingSteps_le line 352
  40. theorem OAI.BinPackingGap.BinaryOrderMachine.joinTrace line 357
  41. theorem OAI.BinPackingGap.BinaryOrderMachine.preservingTrace line 361
  42. def OAI.BinPackingGap.BinaryOrderMachine.preservingInTime line 420
  43. def OAI.BinPackingGap.BinaryOrderMachine.preservingNatInTime line 437
  44. def OAI.BinPackingGap.BinaryOrderMachine.machine line 454
  45. theorem OAI.BinPackingGap.BinaryOrderMachine.machine_finiteAlphabet line 467
  46. def OAI.BinPackingGap.BinaryOrderMachine.preservingMachine line 472
  47. theorem OAI.BinPackingGap.BinaryOrderMachine.preservingMachine_finiteAlphabet line 486