OAI/Computability/WLIdentification/PolynomialWords.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLIdentification.WordExpressions.Poly line 12

    Source documentation

    Uniform polynomial boundedness of a fixed word expression. This is a proven realizer property, not an oracle or a unit-cost word instruction.

    def Poly {n : ℕ} (f : (Fin n → Word) → Word) : Prop :=
…

    Mentions: OAI.WLIdentification.Word

  2. theorem OAI.WLIdentification.WordExpressions.Poly.congr line 21
  3. theorem OAI.WLIdentification.WordExpressions.Poly.var line 25
  4. theorem OAI.WLIdentification.WordExpressions.Poly.nil line 28
  5. theorem OAI.WLIdentification.WordExpressions.Poly.snoc line 31
  6. theorem OAI.WLIdentification.WordExpressions.Poly.drop line 42
  7. theorem OAI.WLIdentification.WordExpressions.Poly.const line 46
  8. theorem OAI.WLIdentification.WordExpressions.Poly.cases line 51
  9. theorem OAI.WLIdentification.WordExpressions.Poly.rename line 75
  10. theorem OAI.WLIdentification.WordExpressions.Poly.bind line 81
  11. theorem OAI.WLIdentification.WordExpressions.Poly.subst line 98
  12. theorem OAI.WLIdentification.WordExpressions.Poly.stages_congr line 120
  13. theorem OAI.WLIdentification.WordExpressions.Poly.loop line 128

    Source documentation

    Polynomial bounded loop rule. The index and accumulator bounds are mathematical invariants of the actual semantics; no execution primitive is added.

    theorem loop {c a : (Fin n → Word) → Word} {f : (Fin (n+2) → Word) → Word}
    (hc : Poly c) (ha : Poly a) (hf : Poly f) (H : ℕ → ℕ) (hH : Polynomial H)
    (hstage : ∀ S N, (∀ j, (S j).length ≤ N) → ∀ i ≤ (c S).length,
      (Expr.stages f S (a S) i).length ≤ H N) :
    Poly (fun S => Expr.stages f S (a S) (c S).length) := by
…

    Mentions: OAI.WLIdentification.Word, OAI.WLIdentification.WordExpressions.Poly, OAI.WLIdentification.WordExpressions.Poly.length, OAI.WLIdentification.WordExpressions.Expr.stages

  14. abbrev OAI.WLIdentification.WordExpressions.unary line 166
  15. abbrev OAI.WLIdentification.WordExpressions.boolWord line 167
  16. def OAI.WLIdentification.WordExpressions.old line 169
  17. def OAI.WLIdentification.WordExpressions.index line 170
  18. def OAI.WLIdentification.WordExpressions.accum line 171
  19. theorem OAI.WLIdentification.WordExpressions.extend_old line 173
  20. theorem OAI.WLIdentification.WordExpressions.extend_index line 175
  21. theorem OAI.WLIdentification.WordExpressions.extend_accum line 177
  22. theorem OAI.WLIdentification.WordExpressions.snoc_prefix line 180
  23. theorem OAI.WLIdentification.WordExpressions.extend_prefix line 183
  24. theorem OAI.WLIdentification.WordExpressions.extend_base line 186
  25. theorem OAI.WLIdentification.WordExpressions.Poly.branches line 193
  26. theorem OAI.WLIdentification.WordExpressions.Poly.emptyTest line 200
  27. theorem OAI.WLIdentification.WordExpressions.Poly.length line 212
  28. theorem OAI.WLIdentification.WordExpressions.Poly.unaryLength line 225
  29. theorem OAI.WLIdentification.WordExpressions.Poly.stages_drop line 230
  30. theorem OAI.WLIdentification.WordExpressions.Poly.cut line 241
  31. theorem OAI.WLIdentification.WordExpressions.Poly.cutOf line 250
  32. theorem OAI.WLIdentification.WordExpressions.Poly.sub line 255
  33. theorem OAI.WLIdentification.WordExpressions.Poly.le line 261
  34. theorem OAI.WLIdentification.WordExpressions.Poly.stages_add line 267
  35. theorem OAI.WLIdentification.WordExpressions.Poly.add line 275
  36. theorem OAI.WLIdentification.WordExpressions.Poly.addOf line 284