OAI/Computability/DegreeRigidity/OrdinalCodes/IndexedOrder.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.IndexedOrder.Reads line 8
2. def OAI.TuringRigidity.IndexedOrder.values line 11
3. theorem OAI.TuringRigidity.IndexedOrder.reads_values line 13
4. theorem OAI.TuringRigidity.IndexedOrder.exists_reads line 23
5. def OAI.TuringRigidity.IndexedOrder.Certificate line 36
6. theorem OAI.TuringRigidity.IndexedOrder.certificate_iff_run line 40
7. def OAI.TuringRigidity.IndexedOrder.OrderWitness line 58
8. theorem OAI.TuringRigidity.IndexedOrder.order_iff_witness line 62