OAI/Analysis/PeriodicLattice/Arithmetic.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Recursive arithmetic and effective profile syntax.

  1. theorem OAI.PeriodicLattice.RecursiveArithmetic.natPow line 17
  2. theorem OAI.PeriodicLattice.RecursiveArithmetic.factorial line 20
  3. theorem OAI.PeriodicLattice.RecursiveArithmetic.encode_int_ofNat line 25
  4. theorem OAI.PeriodicLattice.RecursiveArithmetic.encode_int_negSucc line 26
  5. theorem OAI.PeriodicLattice.RecursiveArithmetic.intOfNat line 28
  6. theorem OAI.PeriodicLattice.RecursiveArithmetic.intNegSucc line 31
  7. theorem OAI.PeriodicLattice.RecursiveArithmetic.intNatAbs line 34
  8. theorem OAI.PeriodicLattice.RecursiveArithmetic.intNegative line 40
  9. theorem OAI.PeriodicLattice.RecursiveArithmetic.intAbsSign line 45
  10. theorem OAI.PeriodicLattice.RecursiveArithmetic.intNeg line 51
  11. theorem OAI.PeriodicLattice.RecursiveArithmetic.intSubNat line 59
  12. theorem OAI.PeriodicLattice.RecursiveArithmetic.intAdd line 67
  13. theorem OAI.PeriodicLattice.RecursiveArithmetic.intSub line 83
  14. theorem OAI.PeriodicLattice.RecursiveArithmetic.intMul line 86
  15. theorem OAI.PeriodicLattice.RecursiveArithmetic.intLE line 100
  16. theorem OAI.PeriodicLattice.RecursiveArithmetic.int_add line 110
  17. theorem OAI.PeriodicLattice.RecursiveArithmetic.int_sub line 111
  18. theorem OAI.PeriodicLattice.RecursiveArithmetic.int_mul line 112
  19. theorem OAI.PeriodicLattice.RecursiveArithmetic.nat_add line 113
  20. theorem OAI.PeriodicLattice.RecursiveArithmetic.nat_sub line 114
  21. theorem OAI.PeriodicLattice.RecursiveArithmetic.nat_mul line 115
  22. theorem OAI.PeriodicLattice.RecursiveArithmetic.nat_pow line 116
  23. theorem OAI.PeriodicLattice.RecursiveArithmetic.nat_div line 117
  24. theorem OAI.PeriodicLattice.RecursiveArithmetic.nat_mod line 118
  25. theorem OAI.PeriodicLattice.RecursiveArithmetic.nat_max line 119
  26. theorem OAI.PeriodicLattice.RecursiveArithmetic.natSucc line 120
  27. theorem OAI.PeriodicLattice.RecursiveArithmetic.list_cons line 122
  28. theorem OAI.PeriodicLattice.RecursiveArithmetic.list_append line 125
  29. theorem OAI.PeriodicLattice.RecursiveArithmetic.natListSum line 128
  30. theorem OAI.PeriodicLattice.RecursiveArithmetic.natListProd line 132
  31. theorem OAI.PeriodicLattice.RecursiveArithmetic.bool_cond line 139
  32. theorem OAI.PeriodicLattice.RecursiveArithmetic.listMap line 144
  33. theorem OAI.PeriodicLattice.RecursiveArithmetic.listFlatMap line 148
  34. theorem OAI.PeriodicLattice.ProfileJets.factorBound_primrec line 156
  35. theorem OAI.PeriodicLattice.ProfileJets.productBound_primrec line 158
  36. theorem OAI.PeriodicLattice.ProfileJets.termBound_primrec line 160
  37. theorem OAI.PeriodicLattice.ProfileJets.bound_primrec line 162
  38. theorem OAI.PeriodicLattice.ProfileJets.multPrefix_primrec line 165
  39. theorem OAI.PeriodicLattice.ProfileJets.diffFactor_primrec line 171
  40. theorem OAI.PeriodicLattice.ProfileJets.diffProduct_primrec line 174
  41. theorem OAI.PeriodicLattice.ProfileJets.diffTerm_primrec line 181
  42. theorem OAI.PeriodicLattice.ProfileJets.diff_primrec line 183
  43. theorem OAI.PeriodicLattice.ProfileJets.jet_primrec line 185
  44. theorem OAI.PeriodicLattice.ProfileJets.pulseBound_primrec line 188
  45. theorem OAI.PeriodicLattice.ProfileJets.bumpBound_primrec line 190
  46. theorem OAI.PeriodicLattice.RecursiveArithmetic.inputMachine line 195
  47. theorem OAI.PeriodicLattice.RecursiveArithmetic.inputWord line 197
  48. theorem OAI.PeriodicLattice.RecursiveArithmetic.machineStates line 199
  49. theorem OAI.PeriodicLattice.RecursiveArithmetic.machineSymbols line 201
  50. theorem OAI.PeriodicLattice.RecursiveArithmetic.machineStart line 203
  51. theorem OAI.PeriodicLattice.RecursiveArithmetic.listLength line 205
  52. theorem OAI.PeriodicLattice.RecursiveArithmetic.ofDigits line 208
  53. theorem OAI.PeriodicLattice.RecursiveArithmetic.sumRange line 213
  54. theorem OAI.PeriodicLattice.CompilerPlanar.radix_primrec line 221
  55. theorem OAI.PeriodicLattice.CompilerPlanar.loadingCode_primrec line 222
  56. theorem OAI.PeriodicLattice.Scales.capacity_primrec line 234
  57. theorem OAI.PeriodicLattice.Scales.exponent_primrec line 236
  58. theorem OAI.PeriodicLattice.Scales.crudeSlotBound_primrec line 238
  59. theorem OAI.PeriodicLattice.Scales.allSlotsBound_primrec line 241
  60. theorem OAI.PeriodicLattice.Planar.planarBound_primrec line 252