OAI/GroupTheory/UniversalGroup/StackMachines.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Higman.IntegerStack.code line 10
  2. theorem OAI.Higman.IntegerStack.code_nil line 14
  3. theorem OAI.Higman.IntegerStack.code_cons line 15
  4. lemma OAI.Higman.IntegerStack.push_mod line 23
  5. lemma OAI.Higman.IntegerStack.push_ne_empty line 29
  6. lemma OAI.Higman.IntegerStack.push_injective line 36
  7. theorem OAI.Higman.IntegerStack.decode_push line 46
  8. theorem OAI.Higman.IntegerStack.code_injective line 60
  9. theorem OAI.Higman.IntegerStack.code_pos line 73
  10. inductive OAI.Higman.HistoryMachine.Run line 87
  11. theorem OAI.Higman.HistoryMachine.run_nil line 94
  12. theorem OAI.Higman.HistoryMachine.run_cons line 102
  13. def OAI.Higman.HistoryMachine.Reach line 112
  14. lemma OAI.Higman.HistoryMachine.reach_start line 118
  15. theorem OAI.Higman.HistoryMachine.reach_step_iff line 122
  16. def OAI.Higman.HistoryMachine.value line 138
  17. def OAI.Higman.HistoryMachine.decoration line 142
  18. theorem OAI.Higman.HistoryMachine.decoration_code line 147
  19. lemma OAI.Higman.HistoryMachine.decoration_step line 158
  20. abbrev OAI.Higman.RecordedMachine.Counter line 172
  21. def OAI.Higman.RecordedMachine.scale line 174
  22. lemma OAI.Higman.RecordedMachine.scale_injective line 179
  23. def OAI.Higman.RecordedMachine.augment line 186
  24. def OAI.Higman.RecordedMachine.forget line 187
  25. def OAI.Higman.RecordedMachine.history line 188
  26. lemma OAI.Higman.RecordedMachine.forget_augment line 190
  27. lemma OAI.Higman.RecordedMachine.history_augment line 191
  28. lemma OAI.Higman.RecordedMachine.augment_forget line 192
  29. def OAI.Higman.RecordedMachine.edge line 196
  30. lemma OAI.Higman.RecordedMachine.edge_input line 213
  31. lemma OAI.Higman.RecordedMachine.edge_output line 218
  32. def OAI.Higman.RecordedMachine.edgeList line 225
  33. lemma OAI.Higman.RecordedMachine.mem_edgeList line 228
  34. lemma OAI.Higman.RecordedMachine.of_mem_edgeList line 232
  35. def OAI.Higman.RecordedMachine.Forward line 239
  36. lemma OAI.Higman.RecordedMachine.forward_start line 244
  37. lemma OAI.Higman.RecordedMachine.output_injective line 249
  38. lemma OAI.Higman.RecordedMachine.forward_edge line 255
  39. lemma OAI.Higman.RecordedMachine.reach_implies_forward line 262
  40. lemma OAI.Higman.RecordedMachine.run_implies_reach line 282
  41. lemma OAI.Higman.RecordedMachine.forward_implies_reach line 295
  42. theorem OAI.Higman.RecordedMachine.reach_iff_forward line 304
  43. def OAI.Higman.RecordedMachine.decoration line 317
  44. lemma OAI.Higman.RecordedMachine.decoration_edge line 321
  45. theorem OAI.Higman.RecordedMachine.benign_forward line 335
  46. def OAI.Higman.MarkerEmbedding.coefficientProjection line 356
  47. lemma OAI.Higman.MarkerEmbedding.projection_coefficient line 358
  48. lemma OAI.Higman.MarkerEmbedding.projection_translation line 361
  49. lemma OAI.Higman.MarkerEmbedding.projection_marker line 364
  50. lemma OAI.Higman.MarkerEmbedding.projection_surjective line 368
  51. theorem OAI.Higman.MarkerEmbedding.benign_output line 373
  52. def OAI.Higman.RecordedMachine.acceptedOutputs line 416
  53. theorem OAI.Higman.RecordedMachine.benign_accepted line 422
  54. theorem OAI.Higman.finitelyPresented_pi line 462