OAI/MathematicalPhysics/RapidForcing/MachineDigits.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RapidForcing.radix_pair_lt line 9
  2. lemma OAI.RapidForcing.replace_digit_lt line 14
  3. lemma OAI.RapidForcing.ScaleData.A_pos line 44
  4. lemma OAI.RapidForcing.ScaleData.one_le_A line 45
  5. lemma OAI.RapidForcing.ScaleData.S_pos line 46
  6. lemma OAI.RapidForcing.ScaleData.P_pos line 47
  7. lemma OAI.RapidForcing.ScaleData.capacity_eq line 49
  8. lemma OAI.RapidForcing.ScaleData.head_lt_P line 54
  9. lemma OAI.RapidForcing.ScaleData.tape_quotient_lt line 61
  10. lemma OAI.RapidForcing.Machine.alphabet_lt_A line 71
  11. lemma OAI.RapidForcing.Machine.states_lt_S line 74
  12. lemma OAI.RapidForcing.Machine.instruction_range line 77
  13. theorem OAI.RapidForcing.Machine.nextDigit_lt line 86