OAI/Analysis/MatrixSigning/Complexity/PolynomialLists.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Realization.prefix_code_length line 13
2. lemma OAI.CurrentKS.Realization.prefix_length line 16
3. instance OAI.CurrentKS.Realization.poly_consList line 19
4. instance OAI.CurrentKS.Realization.poly_appendList line 22
5. instance OAI.CurrentKS.Realization.poly_reverseBody line 26
6. instance OAI.CurrentKS.Realization.size_reverseBody line 28
7. instance OAI.CurrentKS.Realization.poly_reverseList line 37
8. instance OAI.CurrentKS.Realization.poly_mapCtxBody line 40
9. instance OAI.CurrentKS.Realization.size_mapCtxBody line 44
10. instance OAI.CurrentKS.Realization.poly_mapCtx line 75
11. instance OAI.CurrentKS.Realization.poly_natSucc line 80
12. instance OAI.CurrentKS.Realization.poly_natPred line 81
13. instance OAI.CurrentKS.Realization.poly_natAdd line 82
14. instance OAI.CurrentKS.Realization.poly_natIsZero line 89
15. instance OAI.CurrentKS.Realization.poly_rangeStep line 96
16. lemma OAI.CurrentKS.Realization.range_iterate_size line 97
17. instance OAI.CurrentKS.Realization.size_rangeStep line 112
18. instance OAI.CurrentKS.Realization.poly_range line 120
19. instance OAI.CurrentKS.Realization.poly_lengthBody line 122
20. instance OAI.CurrentKS.Realization.size_lengthBody line 123
21. instance OAI.CurrentKS.Realization.poly_lengthList line 133
22. instance OAI.CurrentKS.Realization.poly_tabulate line 134