OAI/Computability/SpaceSimulation/OneTape/Single.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The computation to be simulated. Coordinates on each source are relative to its head's fixed origin, on two-sided tapes. Tags may be correlated however one likes (same tape read, etc.). Single alphabet, with no loss of different read-only components from a fixed common alphabet.

  1. structure OAI.Fifths.SingleAct line 12

    Also declared: ComparatorChallenges/OneTapeSpace.lean:150 (same declaration text).

  2. structure OAI.Fifths.Single line 17

    Also declared: ComparatorChallenges/OneTapeSpace.lean:155 (same declaration text).

  3. instance OAI.Fifths.Single.(instance at line 33) line 33
  4. instance OAI.Fifths.Single.(instance at line 34) line 34
  5. abbrev OAI.Fifths.Single.Tag line 35

    Also declared: ComparatorChallenges/OneTapeSpace.lean:172 (same declaration text).

  6. structure OAI.Fifths.Single.At line 37

    Also declared: ComparatorChallenges/OneTapeSpace.lean:174 (same declaration text).

  7. def OAI.Fifths.Single.move line 42

    Also declared: ComparatorChallenges/OneTapeSpace.lean:179 (same declaration text).

  8. def OAI.Fifths.Single.initial line 48

    Also declared: ComparatorChallenges/OneTapeSpace.lean:185 (same declaration text).

  9. def OAI.Fifths.Single.next line 51

    Also declared: ComparatorChallenges/OneTapeSpace.lean:188 (same declaration text).

  10. def OAI.Fifths.Single.atTime line 55

    Also declared: ComparatorChallenges/OneTapeSpace.lean:192 (same declaration text).

  11. abbrev OAI.Fifths.Single.Outcome line 58

    Also declared: ComparatorChallenges/OneTapeSpace.lean:195 (same declaration text).

  12. def OAI.Fifths.Single.finish line 60

    Source documentation

    false flag means still running at n.

    Also declared: ComparatorChallenges/OneTapeSpace.lean:196 (same declaration text).

    def finish (q : M.Q) : M.Outcome :=
…

    Mentions: OAI.Fifths.Single.q

  13. def OAI.Fifths.Single.outcome line 62

    Also declared: ComparatorChallenges/OneTapeSpace.lean:198 (same declaration text).

  14. theorem OAI.Fifths.Single.immobile line 65
  15. theorem OAI.Fifths.Single.absorbed line 69
  16. def OAI.Fifths.Single.Inside line 79

    Also declared: ComparatorChallenges/OneTapeSpace.lean:201 (same declaration text).

  17. theorem OAI.Fifths.Single.inches line 80
  18. theorem OAI.Fifths.Single.nearby line 85