OAI/Computability/VertexCover/Machines/Composition.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VertexCover.Machine.Compose.K line 52
  2. abbrev OAI.VertexCover.Machine.Compose.Γ line 53
  3. abbrev OAI.VertexCover.Machine.Compose.Λ line 57
  4. abbrev OAI.VertexCover.Machine.Compose.State line 58
  5. instance OAI.VertexCover.Machine.Compose.(instance at line 60) line 60
  6. abbrev OAI.VertexCover.Machine.Compose.Cfg line 62
  7. abbrev OAI.VertexCover.Machine.Compose.Stmt line 63
  8. abbrev OAI.VertexCover.Machine.Compose.first line 65
  9. abbrev OAI.VertexCover.Machine.Compose.second line 66
  10. abbrev OAI.VertexCover.Machine.Compose.temporary line 67
  11. abbrev OAI.VertexCover.Machine.Compose.transfer line 68
  12. def OAI.VertexCover.Machine.Compose.firstStatement line 70
  13. def OAI.VertexCover.Machine.Compose.secondStatement line 79
  14. def OAI.VertexCover.Machine.Compose.program line 92
  15. abbrev OAI.VertexCover.Machine.Compose.machine line 108
  16. def OAI.VertexCover.Machine.Compose.tapes line 120
  17. theorem OAI.VertexCover.Machine.Compose.tapes_first line 126
  18. theorem OAI.VertexCover.Machine.Compose.tapes_second line 128
  19. theorem OAI.VertexCover.Machine.Compose.tapes_temporary line 130
  20. theorem OAI.VertexCover.Machine.Compose.tapes_update_first line 133
  21. theorem OAI.VertexCover.Machine.Compose.tapes_update_second line 145
  22. theorem OAI.VertexCover.Machine.Compose.tapes_update_temporary line 157
  23. def OAI.VertexCover.Machine.Compose.firstCfg line 166
  24. def OAI.VertexCover.Machine.Compose.secondCfg line 172
  25. theorem OAI.VertexCover.Machine.Compose.first_stepAux line 178
  26. theorem OAI.VertexCover.Machine.Compose.second_stepAux line 202
  27. theorem OAI.VertexCover.Machine.Compose.first_step line 226
  28. theorem OAI.VertexCover.Machine.Compose.second_step line 240
  29. def OAI.VertexCover.Machine.Compose.tapeOnly line 254
  30. theorem OAI.VertexCover.Machine.Compose.tapeOnly_self line 257
  31. theorem OAI.VertexCover.Machine.Compose.tapeOnly_nil line 260
  32. theorem OAI.VertexCover.Machine.Compose.tapeOnly_update line 263
  33. def OAI.VertexCover.Machine.Compose.bridgeOne line 267
  34. def OAI.VertexCover.Machine.Compose.bridgeTwo line 272
  35. theorem OAI.VertexCover.Machine.Compose.bridgeOne_cons line 277
  36. theorem OAI.VertexCover.Machine.Compose.bridgeOne_nil line 289
  37. theorem OAI.VertexCover.Machine.Compose.bridgeTwo_cons line 299
  38. theorem OAI.VertexCover.Machine.Compose.init_tapes line 310
  39. theorem OAI.VertexCover.Machine.Compose.halt_tapes line 317
  40. theorem OAI.VertexCover.Machine.Compose.bridgeTwo_nil line 324
  41. def OAI.VertexCover.Machine.Compose.oneStep line 334
  42. def OAI.VertexCover.Machine.Compose.bridgeOne_run line 340
  43. def OAI.VertexCover.Machine.Compose.bridgeTwo_run line 354
  44. theorem OAI.VertexCover.Machine.Compose.cfg_ext line 368
  45. theorem OAI.VertexCover.Machine.Compose.first_initial line 375
  46. theorem OAI.VertexCover.Machine.Compose.first_halted line 392
  47. theorem OAI.VertexCover.Machine.Compose.second_halted line 398
  48. def OAI.VertexCover.Machine.Compose.outputs line 417
  49. theorem OAI.VertexCover.Machine.Compose.finiteAlphabet line 448
  50. def OAI.VertexCover.Machine.compose line 459
  51. theorem OAI.VertexCover.Machine.compose_finite line 479