OAI/Computability/VertexCover/Machines/Pair.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VertexCover.Machine.frame line 46
  2. def OAI.VertexCover.Machine.pairBits line 50
  3. theorem OAI.VertexCover.Machine.frame_length line 52
  4. abbrev OAI.VertexCover.Machine.Pair.Λ line 62
  5. abbrev OAI.VertexCover.Machine.Pair.phase line 63
  6. abbrev OAI.VertexCover.Machine.Pair.Cfg line 64
  7. abbrev OAI.VertexCover.Machine.Pair.Stmt line 65
  8. def OAI.VertexCover.Machine.Pair.firstStatement line 66
  9. def OAI.VertexCover.Machine.Pair.secondStatement line 75
  10. def OAI.VertexCover.Machine.Pair.program line 89
  11. abbrev OAI.VertexCover.Machine.Pair.machine line 121
  12. def OAI.VertexCover.Machine.Pair.firstCfg line 133
  13. def OAI.VertexCover.Machine.Pair.secondCfg line 139
  14. theorem OAI.VertexCover.Machine.Pair.first_stepAux line 145
  15. theorem OAI.VertexCover.Machine.Pair.second_stepAux line 169
  16. theorem OAI.VertexCover.Machine.Pair.first_step line 193
  17. theorem OAI.VertexCover.Machine.Pair.second_step line 207
  18. theorem OAI.VertexCover.Machine.Pair.cfg_ext line 221
  19. def OAI.VertexCover.Machine.Pair.oneStep line 228
  20. def OAI.VertexCover.Machine.Pair.cfg0 line 234
  21. def OAI.VertexCover.Machine.Pair.cfg1 line 239
  22. def OAI.VertexCover.Machine.Pair.cfg2 line 245
  23. def OAI.VertexCover.Machine.Pair.cfg3 line 251
  24. theorem OAI.VertexCover.Machine.Pair.cfg0_cons line 256
  25. theorem OAI.VertexCover.Machine.Pair.cfg0_nil line 268
  26. theorem OAI.VertexCover.Machine.Pair.cfg1_cons line 278
  27. theorem OAI.VertexCover.Machine.Pair.cfg1_nil line 291
  28. theorem OAI.VertexCover.Machine.Pair.cfg2_cons line 301
  29. theorem OAI.VertexCover.Machine.Pair.cfg2_nil line 313
  30. theorem OAI.VertexCover.Machine.Pair.cfg3_cons line 325
  31. theorem OAI.VertexCover.Machine.Pair.cfg3_nil line 337
  32. def OAI.VertexCover.Machine.Pair.cfg0_run line 356
  33. def OAI.VertexCover.Machine.Pair.cfg1_run line 369
  34. def OAI.VertexCover.Machine.Pair.cfg2_run line 385
  35. def OAI.VertexCover.Machine.Pair.cfg3_run line 400
  36. theorem OAI.VertexCover.Machine.Pair.initial_eq line 415
  37. theorem OAI.VertexCover.Machine.Pair.first_halted line 429
  38. theorem OAI.VertexCover.Machine.Pair.second_halted line 435
  39. theorem OAI.VertexCover.Machine.Pair.frame_eq line 441
  40. def OAI.VertexCover.Machine.Pair.outputs line 448
  41. theorem OAI.VertexCover.Machine.Pair.finiteAlphabet line 499
  42. def OAI.VertexCover.Machine.pair line 509
  43. theorem OAI.VertexCover.Machine.pair_finite line 534
  44. structure OAI.VertexCover.Machine.Poly line 543
  45. def OAI.VertexCover.Machine.Poly.comp line 547
  46. def OAI.VertexCover.Machine.Poly.pair line 554