OAI/Computability/DegreeRigidity/Syntax/AtomicDecisionFormula.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.AtomicForcing.CodeWitness line 10
  2. def OAI.TuringRigidity.AtomicForcing.CodeNeg line 13
  3. def OAI.TuringRigidity.AtomicForcing.CodeRefute line 16
  4. def OAI.TuringRigidity.AtomicForcing.AtomicFormula.witness line 22
  5. theorem OAI.TuringRigidity.AtomicForcing.AtomicFormula.eval_witness line 27
  6. def OAI.TuringRigidity.AtomicForcing.AtomicFormula.negMem line 32
  7. theorem OAI.TuringRigidity.AtomicForcing.AtomicFormula.eval_negMem line 36
  8. def OAI.TuringRigidity.AtomicForcing.AtomicFormula.refute line 42
  9. theorem OAI.TuringRigidity.AtomicForcing.AtomicFormula.eval_refute line 47
  10. def OAI.TuringRigidity.AtomicForcing.AtomicFormula.memTest line 52
  11. def OAI.TuringRigidity.AtomicForcing.AtomicFormula.eqTest line 55
  12. theorem OAI.TuringRigidity.AtomicForcing.child_mem line 62
  13. theorem OAI.TuringRigidity.AtomicForcing.codeWitness_iff line 69
  14. theorem OAI.TuringRigidity.AtomicForcing.negMem_iff_no_witness line 89
  15. theorem OAI.TuringRigidity.AtomicForcing.codeNeg_iff line 100
  16. theorem OAI.TuringRigidity.AtomicForcing.codeRefute_iff line 114