OAI/Computability/DegreeRigidity/Effective/FiniteInjurySchedule.lean
14 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.TuringRigidity.FiniteInjurySchedule.exists_missingline 9 - def
OAI.TuringRigidity.FiniteInjurySchedule.visitline 15 - theorem
OAI.TuringRigidity.FiniteInjurySchedule.visit_missingline 17 - theorem
OAI.TuringRigidity.FiniteInjurySchedule.before_visitline 19 - def
OAI.TuringRigidity.FiniteInjurySchedule.resetline 23 - def
OAI.TuringRigidity.FiniteInjurySchedule.seenline 27 - def
OAI.TuringRigidity.FiniteInjurySchedule.scheduledline 31 - theorem
OAI.TuringRigidity.FiniteInjurySchedule.reset_preservesline 34 - theorem
OAI.TuringRigidity.FiniteInjurySchedule.seen_persistsline 44 - theorem
OAI.TuringRigidity.FiniteInjurySchedule.visit_recordedline 49 - theorem
OAI.TuringRigidity.FiniteInjurySchedule.fill_prefixline 54 - theorem
OAI.TuringRigidity.FiniteInjurySchedule.eventually_seenline 83 - theorem
OAI.TuringRigidity.FiniteInjurySchedule.seen_witnessline 92 - theorem
OAI.TuringRigidity.FiniteInjurySchedule.surviving_visitline 118