OAI/Analysis/PeriodicLattice/EffectiveProfiles.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Effective smooth profiles, stack codes and planar compilation.

  1. theorem OAI.PeriodicLattice.EffectiveProfiles.rho line 18
  2. theorem OAI.PeriodicLattice.EffectiveProfiles.rhoTerm line 23
  3. theorem OAI.PeriodicLattice.EffectiveProfiles.denomInv line 27
  4. theorem OAI.PeriodicLattice.EffectiveProfiles.factor line 33
  5. theorem OAI.PeriodicLattice.EffectiveProfiles.product line 39
  6. theorem OAI.PeriodicLattice.EffectiveProfiles.expression line 44
  7. theorem OAI.PeriodicLattice.EffectiveProfiles.pulse line 51
  8. theorem OAI.PeriodicLattice.EffectiveProfiles.bump line 54
  9. theorem OAI.PeriodicLattice.RecursiveArithmetic.intToNat line 59
  10. theorem OAI.PeriodicLattice.RecursiveArithmetic.int_mod line 62
  11. theorem OAI.PeriodicLattice.RecursiveArithmetic.finVal line 65
  12. theorem OAI.PeriodicLattice.RecursiveArithmetic.machineLookup line 66
  13. theorem OAI.PeriodicLattice.RecursiveArithmetic.optionNone line 70
  14. def OAI.PeriodicLattice.StackCode.Code.equiv line 77
  15. instance OAI.PeriodicLattice.StackCode.(instance at line 82) line 82
  16. theorem OAI.PeriodicLattice.StackCode.codeLeft line 83
  17. theorem OAI.PeriodicLattice.StackCode.codeRight line 84
  18. theorem OAI.PeriodicLattice.StackCode.codeState line 85
  19. theorem OAI.PeriodicLattice.StackCode.codeMk line 86
  20. theorem OAI.PeriodicLattice.StackCode.pack_recursive line 87
  21. theorem OAI.PeriodicLattice.StackCode.unpack_recursive line 89
  22. theorem OAI.PeriodicLattice.StackCode.stepRight_recursive line 95
  23. theorem OAI.PeriodicLattice.StackCode.stepLeft_recursive line 103
  24. theorem OAI.PeriodicLattice.StackCode.stepStay_recursive line 113
  25. theorem OAI.PeriodicLattice.StackCode.step_recursive line 121
  26. theorem OAI.PeriodicLattice.CompilerPlanar.width_recursive line 129
  27. theorem OAI.PeriodicLattice.CompilerPlanar.decode_recursive line 133
  28. theorem OAI.PeriodicLattice.CompilerPlanar.lookupAddress_recursive line 137
  29. theorem OAI.PeriodicLattice.CompilerPlanar.haltTable_recursive line 144
  30. theorem OAI.PeriodicLattice.CompilerPlanar.nextArgs_recursive line 146
  31. theorem OAI.PeriodicLattice.CompilerPlanar.nextTable_recursive line 154
  32. theorem OAI.PeriodicLattice.EffectiveFields.rat_natFloor line 170
  33. def OAI.PeriodicLattice.EffectiveFields.qepsilon line 173
  34. def OAI.PeriodicLattice.EffectiveFields.qbeta line 174
  35. theorem OAI.PeriodicLattice.EffectiveFields.cast_qepsilon line 175
  36. theorem OAI.PeriodicLattice.EffectiveFields.cast_qbeta line 177
  37. theorem OAI.PeriodicLattice.EffectiveFields.qepsilon_recursive line 179
  38. theorem OAI.PeriodicLattice.EffectiveFields.qbeta_recursive line 183
  39. theorem OAI.PeriodicLattice.EffectiveFields.selector_effective line 186
  40. abbrev OAI.PeriodicLattice.EffectiveFields.SlotPoint line 212
  41. theorem OAI.PeriodicLattice.EffectiveFields.slotIndex_recursive line 213
  42. theorem OAI.PeriodicLattice.EffectiveFields.slotNext_recursive line 215
  43. theorem OAI.PeriodicLattice.EffectiveFields.slotPrev_recursive line 217
  44. theorem OAI.PeriodicLattice.EffectiveFields.halt_selector line 221
  45. theorem OAI.PeriodicLattice.EffectiveFields.next_selector line 235
  46. theorem OAI.PeriodicLattice.EffectiveFields.coeff_a line 245
  47. theorem OAI.PeriodicLattice.EffectiveFields.coeff_b line 254
  48. theorem OAI.PeriodicLattice.EffectiveFields.slot_value line 264
  49. theorem OAI.PeriodicLattice.EffectiveFields.pointSlot_recursive line 272
  50. theorem OAI.PeriodicLattice.EffectiveFields.pointPulse_recursive line 275
  51. theorem OAI.PeriodicLattice.EffectiveFields.a_base line 279
  52. theorem OAI.PeriodicLattice.EffectiveFields.b_base line 287