OAI/Computability/PerfectCompleteness/Decoding/LowerCutScalar.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.PerfectCompleteness.LowerCutScalar.Valuesline 17 - def
OAI.PerfectCompleteness.LowerCutScalar.reconstructline 21 - theorem
OAI.PerfectCompleteness.LowerCutScalar.reconstruct_reflline 36 - theorem
OAI.PerfectCompleteness.LowerCutScalar.reconstruct_stepline 42 - theorem
OAI.PerfectCompleteness.LowerCutScalar.reconstruct_splitTapeline 57 - theorem
OAI.PerfectCompleteness.LowerCutScalar.reconstruct_joinline 91