OAI/MathematicalPhysics/RapidForcing/RawMachine.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RapidForcing.computable_fin_val line 11
  2. lemma OAI.RapidForcing.compPred_nat_lt line 12
  3. lemma OAI.RapidForcing.compPred_nat_le line 13
  4. def OAI.RapidForcing.ScaleData.dataEquiv line 16
  5. instance OAI.RapidForcing.ScaleData.(instance at line 18) line 18
  6. lemma OAI.RapidForcing.ScaleData.primrec_rA line 19
  7. lemma OAI.RapidForcing.ScaleData.primrec_rQ line 20
  8. lemma OAI.RapidForcing.ScaleData.primrec_B line 21
  9. lemma OAI.RapidForcing.ScaleData.primrec_mk line 22
  10. lemma OAI.RapidForcing.ScaleData.computable_A line 25
  11. lemma OAI.RapidForcing.ScaleData.computable_S line 26
  12. lemma OAI.RapidForcing.ScaleData.computable_P line 27
  13. lemma OAI.RapidForcing.ScaleData.computable_L line 28
  14. lemma OAI.RapidForcing.ScaleData.computable_capacity line 29
  15. lemma OAI.RapidForcing.ScaleData.computable_C line 30
  16. lemma OAI.RapidForcing.ScaleData.computable_s line 31
  17. lemma OAI.RapidForcing.ScaleData.computable_D line 32
  18. lemma OAI.RapidForcing.ScaleData.computable_deltaQ line 33
  19. lemma OAI.RapidForcing.ScaleData.computable_bQ line 34
  20. abbrev OAI.RapidForcing.RawMachine line 37
  21. abbrev OAI.RapidForcing.RawInput line 38
  22. def OAI.RapidForcing.RawMachine.instruction line 41
  23. def OAI.RapidForcing.RawMachine.scaleData line 46
  24. def OAI.RapidForcing.RawMachine.terminalDigit line 47
  25. def OAI.RapidForcing.RawMachine.nextDigit line 50
  26. def OAI.RapidForcing.RawMachine.initialDigit line 61
  27. lemma OAI.RapidForcing.RawMachine.computable_scaleData line 65
  28. lemma OAI.RapidForcing.RawMachine.computable_instruction line 67
  29. lemma OAI.RapidForcing.RawMachine.computable_terminalDigit line 72
  30. def OAI.RapidForcing.RawMachine.digitParts line 75
  31. lemma OAI.RapidForcing.RawMachine.computable_digitParts line 80
  32. def OAI.RapidForcing.RawMachine.digitFinish line 87
  33. lemma OAI.RapidForcing.RawMachine.computable_digitFinish line 92
  34. lemma OAI.RapidForcing.RawMachine.computable_nextDigit line 95
  35. def OAI.RapidForcing.RawMachine.tapeDigits line 102
  36. lemma OAI.RapidForcing.RawMachine.tapeDigits_cons line 103
  37. lemma OAI.RapidForcing.RawMachine.computable_initialDigit line 114