OAI/GroupTheory/UniversalGroup/HigmanEmbedding.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Higman.WordBinary.Letter line 9
  2. def OAI.Higman.WordBinary.push line 11
  3. def OAI.Higman.WordBinary.code line 12
  4. def OAI.Higman.WordBinary.symbol line 16
  5. def OAI.Higman.WordBinary.spelling line 18
  6. lemma OAI.Higman.WordBinary.push_ge line 22
  7. lemma OAI.Higman.WordBinary.code_pos line 26
  8. lemma OAI.Higman.WordBinary.push_inj line 31
  9. lemma OAI.Higman.WordBinary.code_injective line 43
  10. lemma OAI.Higman.WordBinary.trNat_bit line 67
  11. lemma OAI.Higman.WordBinary.trNat_code line 80
  12. lemma OAI.Higman.WordBinary.push_primrec line 90
  13. lemma OAI.Higman.WordBinary.code_primrec line 99
  14. def OAI.Higman.RangeRecognizer.search line 113
  15. lemma OAI.Higman.RangeRecognizer.search_dom line 116
  16. lemma OAI.Higman.RangeRecognizer.search_partrec line 120
  17. theorem OAI.Higman.RangeRecognizer.exists_code line 124
  18. lemma OAI.Higman.RangeRecognizer.halt_iff_dom line 133
  19. instance OAI.Higman.RecognizingStack.(instance at line 156) line 156
  20. def OAI.Higman.RecognizingStack.support line 158
  21. abbrev OAI.Higman.RecognizingStack.MState line 159
  22. abbrev OAI.Higman.RecognizingStack.MEdge line 160
  23. def OAI.Higman.RecognizingStack.mprog line 164
  24. inductive OAI.Higman.RecognizingStack.State line 167
  25. inductive OAI.Higman.RecognizingStack.Edge line 170
  26. def OAI.Higman.RecognizingStack.initialState line 175
  27. def OAI.Higman.RecognizingStack.finalState line 182
  28. def OAI.Higman.RecognizingStack.prog line 185
  29. def OAI.Higman.RecognizingStack.store line 194
  30. def OAI.Higman.RecognizingStack.encoded line 195
  31. def OAI.Higman.RecognizingStack.seed line 196
  32. lemma OAI.Higman.RecognizingStack.store_push line 198
  33. lemma OAI.Higman.RecognizingStack.initial_forget line 203
  34. def OAI.Higman.RecognizingStack.Correct line 209
  35. lemma OAI.Higman.RecognizingStack.correct_seed line 219
  36. lemma OAI.Higman.RecognizingStack.correct_step line 222
  37. lemma OAI.Higman.RecognizingStack.run_correct line 260
  38. lemma OAI.Higman.RecognizingStack.build_word line 267
  39. lemma OAI.Higman.RecognizingStack.enter_word line 284
  40. lemma OAI.Higman.RecognizingStack.run_machine line 290
  41. lemma OAI.Higman.RecognizingStack.halt_word line 302
  42. theorem OAI.Higman.RecognizingStack.outputs_eq line 320
  43. theorem OAI.Higman.benign_enumerated_words line 337
  44. lemma OAI.Higman.HistoryMachine.value_append line 360
  45. abbrev OAI.Higman.NormalWords.Alphabet line 371
  46. abbrev OAI.Higman.NormalWords.Raw line 372
  47. def OAI.Higman.NormalWords.encodeLetter line 374
  48. def OAI.Higman.NormalWords.generator line 378
  49. def OAI.Higman.NormalWords.weight line 379
  50. def OAI.Higman.NormalWords.encodeWord line 382
  51. lemma OAI.Higman.NormalWords.encoded_value line 384
  52. lemma OAI.Higman.NormalWords.encodeWord_primrec line 394
  53. def OAI.Higman.NormalWords.conjugator line 397
  54. def OAI.Higman.NormalWords.conjugated line 398
  55. def OAI.Higman.NormalWords.enumerate line 401
  56. lemma OAI.Higman.NormalWords.conjugator_primrec line 403
  57. lemma OAI.Higman.NormalWords.invRev_primrec line 406
  58. lemma OAI.Higman.NormalWords.enumerate_computable line 413
  59. lemma OAI.Higman.NormalWords.conjugator_encode line 421
  60. lemma OAI.Higman.NormalWords.mk_conjugated line 424
  61. theorem OAI.Higman.NormalWords.range_values line 429
  62. theorem OAI.Higman.NormalWords.benign_normalClosure line 449
  63. theorem OAI.Higman.NormalWords.embeds_presentation line 455