OAI/Computability/PerfectCompleteness/Machines/WholeArrayInteriorOwnInputLaw.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.WholeArrayInteriorOwnInputLaw.F2 line 14
  2. theorem OAI.PerfectCompleteness.WholeArrayInteriorOwnInputLaw.pushforward_eq_of_readout_weights line 18
  3. abbrev OAI.PerfectCompleteness.WholeArrayInteriorOwnInputLaw.fullPath line 38
  4. abbrev OAI.PerfectCompleteness.WholeArrayInteriorOwnInputLaw.RawExterior line 41
  5. def OAI.PerfectCompleteness.WholeArrayInteriorOwnInputLaw.exterior line 46
  6. def OAI.PerfectCompleteness.WholeArrayInteriorOwnInputLaw.readExterior line 58
  7. theorem OAI.PerfectCompleteness.WholeArrayInteriorOwnInputLaw.exterior_split line 66
  8. def OAI.PerfectCompleteness.WholeArrayInteriorOwnInputLaw.exteriorLaw line 85
  9. def OAI.PerfectCompleteness.WholeArrayInteriorOwnInputLaw.exposedRead line 92
  10. theorem OAI.PerfectCompleteness.WholeArrayInteriorOwnInputLaw.exposedRead_law line 101
  11. def OAI.PerfectCompleteness.WholeArrayInteriorOwnInputLaw.readInput line 124
  12. def OAI.PerfectCompleteness.WholeArrayInteriorOwnInputLaw.ownInput line 136
  13. theorem OAI.PerfectCompleteness.WholeArrayInteriorOwnInputLaw.readInput_split line 146
  14. def OAI.PerfectCompleteness.WholeArrayInteriorOwnInputLaw.hiddenOutput line 157
  15. theorem OAI.PerfectCompleteness.WholeArrayInteriorOwnInputLaw.conditional_referenceLaw line 167