OAI/Computability/WLIdentification/SeedBits.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.WLIdentification.BinaryAddress.ofNat_apply line 7
2. def OAI.WLIdentification.FinitePresentation.Test.ofNatBit line 20
3. def OAI.WLIdentification.FinitePresentation.ProductRealizer.singletonBits line 32
4. def OAI.WLIdentification.FinitePresentation.ProductRealizer.aboveBits line 40
5. theorem OAI.WLIdentification.FinitePresentation.InitialRealizer.span_poly line 62
6. abbrev OAI.WLIdentification.FinitePresentation.InitialRealizer.positionP line 63
7. abbrev OAI.WLIdentification.FinitePresentation.InitialRealizer.digitP line 64
8. def OAI.WLIdentification.FinitePresentation.InitialRealizer.spanBit line 65
9. def OAI.WLIdentification.FinitePresentation.InitialRealizer.zeroBit line 68
10. abbrev OAI.WLIdentification.FinitePresentation.InitialRealizer.thresholdDigitP line 70
11. abbrev OAI.WLIdentification.FinitePresentation.InitialRealizer.thresholdP line 72
12. abbrev OAI.WLIdentification.FinitePresentation.InitialRealizer.seedP line 73
13. def OAI.WLIdentification.FinitePresentation.InitialRealizer.positionBits line 74
14. def OAI.WLIdentification.FinitePresentation.InitialRealizer.thresholdMap line 76
15. def OAI.WLIdentification.FinitePresentation.InitialRealizer.seedMap line 84