OAI/Computability/Superstring/FactoryPoly.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Superstring.BlockFactory.PackInput line 8
  2. instance OAI.Superstring.BlockFactory.codedPackInput line 9
  3. theorem OAI.Superstring.BlockFactory.poly_pack line 11
  4. abbrev OAI.Superstring.BlockFactory.IndividualInput line 17
  5. instance OAI.Superstring.BlockFactory.codedIndividualInput line 18
  6. theorem OAI.Superstring.BlockFactory.poly_individual line 19
  7. abbrev OAI.Superstring.BlockFactory.CollectiveInput line 25
  8. instance OAI.Superstring.BlockFactory.codedCollectiveInput line 26
  9. theorem OAI.Superstring.BlockFactory.poly_collective line 27
  10. def OAI.Superstring.LayerArray.shortWords line 41
  11. def OAI.Superstring.LayerArray.hasShort line 43
  12. def OAI.Superstring.LayerArray.shortLoop line 44
  13. theorem OAI.Superstring.LayerArray.hasShort_eq line 48
  14. theorem OAI.Superstring.LayerArray.shortLoop_spec line 67
  15. theorem OAI.Superstring.LayerArray.poly_shortWords line 96
  16. theorem OAI.Superstring.LayerArray.poly_hasShort line 101
  17. theorem OAI.Superstring.LayerArray.poly_shortLoop line 104
  18. theorem OAI.Superstring.BlockClose.step_nil line 114
  19. theorem OAI.Superstring.BlockClose.iterate_step line 118
  20. theorem OAI.Superstring.BlockClose.rooted_length line 146
  21. abbrev OAI.Superstring.BlockClose.Input line 158
  22. def OAI.Superstring.BlockClose.iterStep line 159
  23. def OAI.Superstring.BlockClose.capacity line 160
  24. def OAI.Superstring.BlockClose.close line 162
  25. theorem OAI.Superstring.BlockClose.iterate_iterStep line 166
  26. theorem OAI.Superstring.BlockClose.state_size line 173
  27. theorem OAI.Superstring.BlockClose.close_spec line 193
  28. theorem OAI.Superstring.BlockClose.poly_iterStep line 220
  29. theorem OAI.Superstring.BlockClose.poly_capacity line 223
  30. theorem OAI.Superstring.BlockClose.poly_close line 228
  31. def OAI.Superstring.WalkCode.collect line 239
  32. theorem OAI.Superstring.WalkCode.fold_join_spec line 241
  33. theorem OAI.Superstring.WalkCode.collect_spec line 262
  34. theorem OAI.Superstring.WalkCode.poly_collect line 270