OAI/Computability/WLIdentification/NumericKernel.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WLIdentification.NumericKernel.lookup line 9
2. def OAI.WLIdentification.NumericKernel.digit line 11
3. def OAI.WLIdentification.NumericKernel.vectorMatch line 13
4. def OAI.WLIdentification.NumericKernel.countMatch line 18
5. def OAI.WLIdentification.NumericKernel.entry line 22
6. def OAI.WLIdentification.NumericKernel.step line 27
7. def OAI.WLIdentification.NumericKernel.table line 31
8. theorem OAI.WLIdentification.WordExpressions.NatPoly.digit line 38
9. theorem OAI.WLIdentification.NumericKernel.vectorMatch_poly line 50

   Source documentation

   All loops below range over explicit unary word lengths.

   theorem vectorMatch_poly : BoolPoly (fun S : Fin 7 → Word =>
       vectorMatch (S 0).length (S 1).length (S 2) (S 3) (S 4).length (S 5).length (S 6).length) := by
   …

   Mentions: OAI.WLIdentification.Word, OAI.WLIdentification.NumericKernel.vectorMatch

10. theorem OAI.WLIdentification.NumericKernel.vectorMatch_poly_of line 65
11. theorem OAI.WLIdentification.NumericKernel.countMatch_poly line 74
12. theorem OAI.WLIdentification.NumericKernel.countMatch_poly_of line 86
13. theorem OAI.WLIdentification.NumericKernel.entry_poly line 95
14. theorem OAI.WLIdentification.NumericKernel.entry_poly_of line 105
15. theorem OAI.WLIdentification.NumericKernel.step_poly line 115
16. theorem OAI.WLIdentification.NumericKernel.step_poly_of line 122
17. theorem OAI.WLIdentification.WordExpressions.Poly.iterate line 137

    Source documentation

    Iteration with a proved output-length invariant. Its loop count is a physical unary word, not an unbounded recursion primitive.

    theorem iterate {c b : (Fin n → Word) → ℕ} {a : (Fin n → Word) → Word}
        {f : (Fin n → Word) → Word → Word} (hc : NatPoly c) (hb : NatPoly b) (ha : Poly a)
        (hf : Poly (fun T => f (T ∘ Fin.castSucc) (T (Fin.last n))))
        (hlen : ∀ S W, (f S W).length ≤ b S) :
        Poly (fun S => (f S)^[c S] (a S)) := by
    …

    Mentions: OAI.WLIdentification.Word, OAI.WLIdentification.WordExpressions.NatPoly, OAI.WLIdentification.WordExpressions.Poly, OAI.WLIdentification.WordExpressions.Poly.length

18. theorem OAI.WLIdentification.NumericKernel.table_poly line 173
19. structure OAI.WLIdentification.NumericKernel.Data line 187
20. def OAI.WLIdentification.NumericKernel.Data.vectors line 193
21. def OAI.WLIdentification.NumericKernel.Encoded line 196
22. def OAI.WLIdentification.NumericKernel.Represents line 201
23. theorem OAI.WLIdentification.NumericKernel.vectorMatch_correct line 204
24. theorem OAI.WLIdentification.NumericKernel.sum_range_fin line 229
25. theorem OAI.WLIdentification.NumericKernel.multiset_countP_sum line 236
26. theorem OAI.WLIdentification.NumericKernel.countMatch_correct line 244
27. theorem OAI.WLIdentification.NumericKernel.entry_correct line 259
28. theorem OAI.WLIdentification.NumericKernel.lookup_step line 275
29. theorem OAI.WLIdentification.NumericKernel.step_correct line 285
30. theorem OAI.WLIdentification.NumericKernel.table_correct line 292