OAI/Computability/DegreeRigidity/Syntax/BoundedTruthRecursion.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.BoundedTruthRecursion.Local line 10
  2. def OAI.TuringRigidity.BoundedTruthRecursion.Partial line 15
  3. theorem OAI.TuringRigidity.BoundedTruthRecursion.partial_sound line 19
  4. def OAI.TuringRigidity.BoundedTruthRecursion.dropSlots line 32
  5. def OAI.TuringRigidity.BoundedTruthRecursion.partialFormula line 37
  6. theorem OAI.TuringRigidity.BoundedTruthRecursion.partialFormula_spec line 41
  7. def OAI.TuringRigidity.BoundedTruthRecursion.domain line 49
  8. def OAI.TuringRigidity.BoundedTruthRecursion.truth line 52
  9. def OAI.TuringRigidity.BoundedTruthRecursion.candidateSlots line 55
  10. def OAI.TuringRigidity.BoundedTruthRecursion.unionFormula line 60
  11. theorem OAI.TuringRigidity.BoundedTruthRecursion.unionFormula_spec line 63
  12. theorem OAI.TuringRigidity.BoundedTruthRecursion.domain_truth_mem line 73
  13. theorem OAI.TuringRigidity.BoundedTruthRecursion.domain_transitive line 84
  14. theorem OAI.TuringRigidity.BoundedTruthRecursion.truth_subset_domain line 91
  15. theorem OAI.TuringRigidity.BoundedTruthRecursion.truth_agrees line 97
  16. theorem OAI.TuringRigidity.BoundedTruthRecursion.partial_of_agrees line 109
  17. theorem OAI.TuringRigidity.BoundedTruthRecursion.truth_internal line 118