OAI/Computability/MinUncut/Estimates/CodeContinuations.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.Costed.Arena.simulate_cons line 9
  2. lemma OAI.MinUncut.Costed.Arena.simulate_fixDone line 45
  3. lemma OAI.MinUncut.Costed.Arena.simulate_fixMore line 66
  4. lemma OAI.MinUncut.Costed.Arena.Simulates.mono line 90
  5. lemma OAI.MinUncut.Costed.Arena.CodeRun.simulates line 95
  6. def OAI.MinUncut.Costed.Arena.listCells line 109
  7. lemma OAI.MinUncut.Costed.Arena.listCells_spec line 115
  8. lemma OAI.MinUncut.Costed.Arena.listCells_length line 122
  9. def OAI.MinUncut.Costed.Arena.initialState line 127
  10. lemma OAI.MinUncut.Costed.Arena.initialState_spec line 132
  11. lemma OAI.MinUncut.Costed.Arena.State.tick_halted line 137
  12. lemma OAI.MinUncut.Costed.Arena.Trace.pad_halted line 141
  13. lemma OAI.MinUncut.Costed.Arena.CodeRun.interpreted line 151
  14. structure OAI.MinUncut.Costed.Arena.OutputState line 168
  15. def OAI.MinUncut.Costed.Arena.OutputState.encode line 173
  16. def OAI.MinUncut.Costed.Arena.OutputState.tick line 176
  17. def OAI.MinUncut.Costed.Arena.outRead line 179
  18. def OAI.MinUncut.Costed.Arena.outputStep line 183
  19. def OAI.MinUncut.Costed.Arena.outputStepProgram line 187
  20. lemma OAI.MinUncut.Costed.Arena.out_encode_reg0 line 194
  21. lemma OAI.MinUncut.Costed.Arena.out_encode_reg1 line 195
  22. lemma OAI.MinUncut.Costed.Arena.out_encode_reg2 line 196
  23. lemma OAI.MinUncut.Costed.Arena.outRead_encode line 198
  24. lemma OAI.MinUncut.Costed.Arena.outputStep_encode line 213
  25. lemma OAI.MinUncut.Costed.Arena.output_raw_iter line 222
  26. lemma OAI.MinUncut.Costed.Arena.ListRep.output_iter line 228
  27. lemma OAI.MinUncut.Costed.Arena.output_null_iter line 239
  28. lemma OAI.MinUncut.Costed.Arena.ListRep.output_padded line 245