OAI/Computability/DegreeRigidity/OrdinalCodes/SumComparison.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.RationalCoding.sumLeft line 7
2. def OAI.TuringRigidity.RationalCoding.sumRight line 12
3. theorem OAI.TuringRigidity.RationalCoding.polynomial_primrec line 17
4. theorem OAI.TuringRigidity.RationalCoding.sumLeft_primrec line 33
5. theorem OAI.TuringRigidity.RationalCoding.sumRight_primrec line 36
6. theorem OAI.TuringRigidity.RationalCoding.sum_difference line 39
7. theorem OAI.TuringRigidity.RationalCoding.lt_sum_iff line 51
8. theorem OAI.TuringRigidity.RationalCoding.sum_lt_iff line 69