OAI/Computability/DegreeRigidity/Syntax/FiniteSatisfactionCertificate.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.RelativeConstructible.subformulas line 11
  2. theorem OAI.TuringRigidity.RelativeConstructible.self_mem_subformulas line 18
  3. theorem OAI.TuringRigidity.RelativeConstructible.subformulas_closed line 21
  4. def OAI.TuringRigidity.RelativeConstructible.finiteSatisfaction line 47
  5. theorem OAI.TuringRigidity.RelativeConstructible.mem_finiteSatisfaction line 51
  6. theorem OAI.TuringRigidity.RelativeConstructible.finiteSatisfaction_record line 67
  7. theorem OAI.TuringRigidity.RelativeConstructible.finiteSatisfaction_mem line 81
  8. theorem OAI.TuringRigidity.RelativeConstructible.finiteSatisfaction_subset line 91
  9. theorem OAI.TuringRigidity.RelativeConstructible.finiteSatisfaction_covers line 97
  10. def OAI.TuringRigidity.RelativeConstructible.accepts line 104
  11. theorem OAI.TuringRigidity.RelativeConstructible.certificate_correct line 107
  12. theorem OAI.TuringRigidity.RelativeConstructible.certificate_conj line 114
  13. theorem OAI.TuringRigidity.RelativeConstructible.certificate_neg line 128
  14. theorem OAI.TuringRigidity.RelativeConstructible.certificate_ex line 137