OAI/Computability/Superstring/DistributeCode.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Superstring.DistributeCode.Result line 8
2. def OAI.Superstring.DistributeCode.one line 10
3. def OAI.Superstring.DistributeCode.budget line 16
4. def OAI.Superstring.DistributeCode.combine line 18
5. def OAI.Superstring.DistributeCode.many line 20
6. theorem OAI.Superstring.DistributeCode.one_spec line 25
7. theorem OAI.Superstring.DistributeCode.combine_budget line 74
8. theorem OAI.Superstring.DistributeCode.gather_budget line 81
9. theorem OAI.Superstring.DistributeCode.flatMap_sublist line 97
10. theorem OAI.Superstring.DistributeCode.many_spec line 105
11. instance OAI.Superstring.DistributeCode.codedResult line 155
12. abbrev OAI.Superstring.DistributeCode.OneInput line 156
13. instance OAI.Superstring.DistributeCode.codedOneInput line 157
14. theorem OAI.Superstring.DistributeCode.poly_one line 159
15. theorem OAI.Superstring.DistributeCode.poly_budget line 163
16. theorem OAI.Superstring.DistributeCode.poly_many line 168
17. def OAI.Superstring.LayerArray.belowLoop line 191
18. def OAI.Superstring.LayerArray.below line 193
19. theorem OAI.Superstring.LayerArray.belowLoop_spec line 196
20. theorem OAI.Superstring.LayerArray.below_spec line 221
21. theorem OAI.Superstring.LayerArray.poly_belowLoop line 248
22. theorem OAI.Superstring.LayerArray.poly_below line 252
23. def OAI.Superstring.DistributeCode.record line 266
24. theorem OAI.Superstring.DistributeCode.record_spec line 274
25. abbrev OAI.Superstring.DistributeCode.RecordInput line 360
26. instance OAI.Superstring.DistributeCode.codedRecordInput line 361
27. theorem OAI.Superstring.DistributeCode.poly_record line 363
28. def OAI.Superstring.LayerArray.attachBand line 391
29. theorem OAI.Superstring.LayerArray.band_general line 394
30. theorem OAI.Superstring.LayerArray.attachBand_spec line 437
31. theorem OAI.Superstring.LayerArray.poly_attachBand line 462