OAI/Computability/SpaceSimulation/Evaluation/Local.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Fifths.Modulus.packed line 10
  2. theorem OAI.Fifths.Modulus.packed_lt line 13
  3. theorem OAI.Fifths.Modulus.get_packed line 15
  4. theorem OAI.Fifths.Modulus.aug_bounded line 19
  5. theorem OAI.Fifths.Modulus.aug_val line 23
  6. theorem OAI.Fifths.Modulus.fromAug line 25
  7. abbrev OAI.Fifths.Comp.ReComp line 36

    Source documentation

    Reduce repetition in local uniformity proofs.

    abbrev ReComp {U : Type} (x : I → List X) (S : I → ℕ) (r : U → I) :=
…
  8. theorem OAI.Fifths.Comp.fitPowers line 44
  9. theorem OAI.Fifths.Comp.fitBitsD line 48
  10. theorem OAI.Fifths.Comp.fitPacked line 52
  11. theorem OAI.Fifths.Comp.coord line 57
  12. theorem OAI.Fifths.Comp.wordBit line 65
  13. theorem OAI.Fifths.Comp.vector line 72
  14. theorem OAI.Fifths.Comp.basisAt line 82
  15. theorem OAI.Fifths.Comp.lookupOne line 101
  16. theorem OAI.Fifths.Comp.lookupTwo line 117