OAI/Computability/PerfectCompleteness/Machines/WholeArrayOwnInputLaw.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.WholeArrayOwnInputLaw.condition_pushforward line 16
  2. theorem OAI.PerfectCompleteness.WholeArrayOwnInputLaw.lower_ne_root line 31
  3. def OAI.PerfectCompleteness.WholeArrayOwnInputLaw.rootCut line 38
  4. def OAI.PerfectCompleteness.WholeArrayOwnInputLaw.nodeCut line 46
  5. def OAI.PerfectCompleteness.WholeArrayOwnInputLaw.exposedRead line 51
  6. theorem OAI.PerfectCompleteness.WholeArrayOwnInputLaw.exposedRead_law line 62
  7. def OAI.PerfectCompleteness.WholeArrayOwnInputLaw.ownInput line 72
  8. def OAI.PerfectCompleteness.WholeArrayOwnInputLaw.hiddenOutput line 82
  9. theorem OAI.PerfectCompleteness.WholeArrayOwnInputLaw.conditional_referenceLaw line 91
  10. theorem OAI.PerfectCompleteness.WholeArrayOwnInputLaw.conditional_referenceLaw_node line 163