OAI/Computability/DegreeRigidity/SetModels/ElementaryLanguage.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.TuringRigidity.ElementaryModel.SentenceForm line 11
  2. def OAI.TuringRigidity.ElementaryModel.SentenceForm.Sat line 21
  3. def OAI.TuringRigidity.ElementaryModel.SentenceForm.bound line 28
  4. theorem OAI.TuringRigidity.ElementaryModel.SentenceForm.finite_support line 34
  5. def OAI.TuringRigidity.ElementaryModel.SentenceForm.disj line 59
  6. def OAI.TuringRigidity.ElementaryModel.SentenceForm.imp line 60
  7. def OAI.TuringRigidity.ElementaryModel.SentenceForm.iff line 61
  8. def OAI.TuringRigidity.ElementaryModel.SentenceForm.all line 62
  9. theorem OAI.TuringRigidity.ElementaryModel.SentenceForm.sat_disj line 64
  10. theorem OAI.TuringRigidity.ElementaryModel.SentenceForm.sat_imp line 66
  11. theorem OAI.TuringRigidity.ElementaryModel.SentenceForm.sat_iff line 68
  12. theorem OAI.TuringRigidity.ElementaryModel.SentenceForm.sat_all line 70
  13. def OAI.TuringRigidity.ElementaryModel.SentenceForm.rename line 73
  14. theorem OAI.TuringRigidity.ElementaryModel.SentenceForm.sat_rename line 80
  15. def OAI.TuringRigidity.ElementaryModel.Elementary line 96