OAI/Computability/SpaceSimulation/Stack/Duo.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Fifths.SM.clone line 11

    Source documentation

    Copy stack k onto empty y using empty tmp t.

    def clone (k y t : K) : SM X J K Unit :=
…

    Mentions: OAI.Fifths.SM

  2. theorem OAI.Fifths.SM.exec_clone line 15
  3. def OAI.Fifths.SM.gather line 42

    Source documentation

    Two stack words become one prefix pair (on y); work slot t initially empty and returned empty.

    def gather (k y t : K) : SM X J K Unit :=
…

    Mentions: OAI.Fifths.SM

  4. theorem OAI.Fifths.SM.exec_gather line 46
  5. def OAI.Fifths.SM.parsePush line 80
  6. def OAI.Fifths.SM.parseNext line 84
  7. def OAI.Fifths.SM.crack line 89

    Source documentation

    Consume frame prefix of k, pushing first component reversed onto t.

    def crack (k t : K) : SM X J K Unit :=
…

    Mentions: OAI.Fifths.SM

  8. theorem OAI.Fifths.SM.exec_crack line 92
  9. def OAI.Fifths.SM.sendFirst line 142

    Source documentation

    Move first component of frame k to empty y normal order, leaving second on k.

    def sendFirst (k y t : K) : SM X J K Unit :=
…

    Mentions: OAI.Fifths.SM

  10. theorem OAI.Fifths.SM.exec_sendFirst line 145
  11. def OAI.Fifths.SM.projF line 168

    Source documentation

    In-place first or second projection.

    def projF (k t : K) : SM X J K Unit :=
…

    Mentions: OAI.Fifths.SM

  12. def OAI.Fifths.SM.projS line 170
  13. theorem OAI.Fifths.SM.exec_projF line 173
  14. theorem OAI.Fifths.SM.exec_projS line 199