Documentation

DescriptiveComplexity.Problems.Wide.NexOuter

The clocked program's outer layer #

The EXPSPACE program's outer loop (DescriptiveComplexity.Draw.OuterPh) is an iteration: startup, then a sweep, a convergence test and a copy-back, round after round until the fixed point stops moving. A program on a clock cannot iterate – a partial fixed point may run through doubly exponentially many stages – and it cannot use the input channel's mark ladder either, since reaching it costs more than the clock allows. What it does instead is four things once:

  1. lay its own register file out, low on the tape, one cell per block and tuple (DescriptiveComplexity.blkFile: one per element is what a clock cannot pay for);
  2. guess the certificate onto the same stretch, one write per address;
  3. run the evaluation over the region, exactly the EXPSPACE program's;
  4. accept.

This file is that outer layer, with the evaluation abstract – its phase type PE, its site family and its boundary rules are parameters, as in DescriptiveComplexity.Draw.Data.outerRule – and with the two sweeps' writes abstract too, because what a cell of the file holds is a fact about the layout the caller chose and not about the shape of the loop. The runs the two sweeps discharge against are DescriptiveComplexity.Draw.Prog.reachesIn_buildFile and DescriptiveComplexity.Draw.Prog.reachesIn_guessTracks.

Why the guess is a shape and not a guard #

Every other site here separates in-shape: from the guard and the phase, the rule that fired is recoverable, which is what the backward reading of a run needs. The guessing site does not, and must not – its shapes are the certificate's values at one cell, all of them firing under the same guard. That is the whole nondeterminism of the program, and nexSep states the separation for every other site, which is what DescriptiveComplexity.TMData.UniqueFrom asks for.

Why the two sweeps stop on the control and not on the tape #

Both sweeps run right along a stretch whose ends are addresses, and a rule sees only the control and the cell under the head. The cell cannot say where the stretch ends – the tape is blank there, and blank is what the cells ahead hold too – so the stop test is a predicate on the control: the pointer has passed the file's top. It is the caller's, along with the write and the pointer's advance, bundled as SweepSpec.

Why the block is in the phase and the tuple in the control #

A register is named by a block and a tuple, and only the tuple is made of elements: the control holds elements, so the tuple lives there, and the block – finite, and one of finitely many – lives in the phase, which is where finite data belongs. That is why NexPh.buildP and NexPh.guessP carry a B.

A destination phase is a constant, not a function of the control, so a sweep whose pointer rolls over into the next block cannot decide that in the stepping rule: the roll-over is its own rule, guarded by the pointer holding the last tuple of its block (SweepSpec.Roll). The last register of the file is written by a third – Roll ∧ Done – which moves right like the others and lands in NexPh.buildDoneP, one cell past the file, where a fourth turns the machine round. The last register has to be written, and the writes happen on the right-moving steps, which is why the turn-around is a phase of its own and not the exit guard of the sweep. The three guards at NexPh.buildP are pairwise disjoint by construction, which is what nexSep reads off.

The exit into the next sweep resets the pointer (SweepSpec.st0): the sweep that just finished left it at the file's last register, and the next one starts at the first.

The phases #

source
inductive DescriptiveComplexity.Draw.NexPh (B PE : Type) :
Type

The phases of the clocked program: the two opening sweeps with a walk home after each, the evaluation, and the accepting phase.

  • start {B PE : Type} : NexPh B PE

    The initial phase: mark the home cell and set off.

  • approachP {B PE : Type} : NexPh B PE

    Walking up to the file's base, writing nothing. Where it stops is the program's choice: a machine has no landmark but the cell it started on , and the file has to be laid above the data.

  • buildP {B PE : Type} : B → NexPh B PE

    Laying the register file out, in the block the phase names.

  • buildDoneP {B PE : Type} : NexPh B PE

    The file is laid: standing one cell past its last register.

  • homeBuildP {B PE : Type} : NexPh B PE

    Walking home after the file is laid out.

  • guessP {B PE : Type} : B → NexPh B PE

    Guessing the certificate onto the region, in the block the phase names.

  • guessDoneP {B PE : Type} : NexPh B PE

    The certificate is guessed: standing one cell past the last register.

  • homeGuessP {B PE : Type} : NexPh B PE

    Walking home after the guess.

  • acceptP {B PE : Type} : NexPh B PE

    The accepting phase: no rule leaves it.

  • evalP {B PE : Type} : PE → NexPh B PE

    A phase of the evaluation.

Instances For
    Dependency graph
    source
    instance DescriptiveComplexity.Draw.instFiniteNexPh {B PE : Type} [Finite B] [Finite PE] :
    Finite (NexPh B PE)
    Dependency graph

    The sites #

    source
    inductive DescriptiveComplexity.Draw.NexSite (SE : Type) :
    Type

    The call sites of the clocked program, plus the evaluation's.

    • start {SE : Type} : NexSite SE

      The initial step.

    • approach {SE : Type} : NexSite SE

      The walk up to the file's base: like the guess, it does not separate in-shape, its stop being a choice.

    • build {SE : Type} : NexSite SE

      The file-laying sweep.

    • homeBuild {SE : Type} : NexSite SE

      The walk home after it.

    • guess {SE : Type} : NexSite SE

      The guessing sweep: the one site that does not separate in-shape.

    • homeGuess {SE : Type} : NexSite SE

      The walk home after it.

    • accept {SE : Type} : NexSite SE

      The accepting phase's site: no rules.

    • eval {SE : Type} : SE → NexSite SE

      An evaluation site.

    Instances For
      Dependency graph
      source
      instance DescriptiveComplexity.Draw.instFiniteNexSite {SE : Type} [Finite SE] :
      Finite (NexSite SE)
      Dependency graph
      source
      def DescriptiveComplexity.Draw.NexSh (SE B G : Type) (ShE : SE → Type) :
      NexSite SE → Type

      The rule shape of each site of the clocked program: the sweep's step and its exit, the walks' kit rules and their exits, and the guess's values G.

      Equations
      Instances For
        Dependency graph
        source
        instance DescriptiveComplexity.Draw.instFiniteNexSh {SE B G : Type} {ShE : SE → Type} [Finite B] [Finite G] [∀ (e : SE), Finite (ShE e)] (i : NexSite SE) :
        Finite (NexSh SE B G ShE i)
        Dependency graph

        What a sweep writes #

        source
        structure DescriptiveComplexity.Draw.SweepSpec (A Q W B : Type) :
        Type

        One right-running sweep, from the rules' side: what it writes at the cell under the head, where it leaves the pointer, and when it is over.

        The three are the caller's because they are facts about the layout, not about the shape of the loop: the file-laying sweep writes the background of the file it is building, the guessing sweep writes one value of the certificate, and both stop when the pointer has passed the stretch's top.

        • wr : B → (Q → A) → (W → A) → W → A

          The tracks the cell under the head is left holding, in this block.

        • st : B → (Q → A) → (W → A) → Q → A

          The pointer the rule leaves in the control, within a block.

        • st0 : (Q → A) → (W → A) → Q → A

          The pointer at the file's first register: what the exit into the next sweep leaves, since the sweep just finished left it at the last.

        • stRoll : B → (Q → A) → (W → A) → Q → A

          The pointer it leaves when the tuple rolls over into the next block.

        • nx : B → B

          The next block.

        • Roll : B → (Q → A) → Prop

          The pointer holds the last tuple of the block: the step rolls over. A destination phase is a constant, so the roll-over is its own rule and this is what tells the two apart.

        • Done : B → (Q → A) → Prop

          The pointer holds the last tuple of the last block: the sweep is over.

        Instances For
          Dependency graph
          source
          structure DescriptiveComplexity.Draw.GuessSpec (A Q W B G : Type) :
          Type

          One right-running sweep that guesses: the same three, with the write and the pointer's advance depending on the value G guessed at the cell. All of them fire under one guard, which is what makes the phase a guess.

          • wr : B → G → (Q → A) → (W → A) → W → A

            The tracks the cell under the head is left holding, at this value.

          • st : B → G → (Q → A) → (W → A) → Q → A

            The pointer the rule leaves in the control, at this value.

          • stRoll : B → G → (Q → A) → (W → A) → Q → A

            The pointer it leaves when the tuple rolls over into the next block.

          • nx : B → B

            The next block.

          • Roll : B → (Q → A) → Prop

            The pointer holds the last tuple of the block.

          • Done : B → (Q → A) → Prop

            The pointer holds the last tuple of the last block.

          Instances For
            Dependency graph
            source
            def DescriptiveComplexity.Draw.NexPh.PostGuess {B PE : Type} :
            NexPh B PE → Prop

            The phases from the guess's walk home onward. The program's only nondeterminism is at NexPh.guessP, and no rule returns there: from the walk home after the guess the machine is deterministic, which is the shape DescriptiveComplexity.TMData.UniqueFrom wants.

            Equations
            Instances For
              Dependency graph
              source
              noncomputable def DescriptiveComplexity.Draw.Data.nexRule {L : FirstOrder.Language} (dt : Data L) {A Q B G PE SE : Type} [DecidableEq dt.SlotIx] (one : A) {ShE : SE → Type} (β : SweepSpec A Q dt.SlotIx B) (γ : GuessSpec A Q dt.SlotIx B G) (ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (NexPh B PE)) (evalEntry : PE) (bot : B) (i : NexSite SE) :
              NexSh SE B G ShE i → Rule A Q dt.SlotIx (NexPh B PE)

              The rules of the clocked program's outer layer: the initial step, the two sweeps at their specifications with their exits, the two walks home at their kits, and the evaluation's rules as the parameter ruleE.

              Equations
              Instances For
                Dependency graph
                source
                def DescriptiveComplexity.Draw.Data.nexOwner {B PE SE : Type} (ownE : PE → SE) :
                NexPh B PE → NexSite SE

                The owner of each phase: the site whose copy of a phase it is; the evaluation's phases are owned through the parameter.

                Equations
                Instances For
                  Dependency graph
                  source
                  theorem DescriptiveComplexity.Draw.Data.nexOwner_nexRule {L : FirstOrder.Language} {dt : Data L} {A Q B G PE SE : Type} [DecidableEq dt.SlotIx] {one : A} {ShE : SE → Type} {β : SweepSpec A Q dt.SlotIx B} {γ : GuessSpec A Q dt.SlotIx B G} {ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (NexPh B PE)} {evalEntry : PE} {bot : B} {ownE : PE → SE} (hownE : ∀ (e : SE) (ρ : ShE e), nexOwner ownE (ruleE e ρ).srcPh = NexSite.eval e) (i : NexSite SE) (ρ : NexSh SE B G ShE i) :
                  nexOwner ownE (dt.nexRule one β γ ruleE evalEntry bot i ρ).srcPh = i

                  Every rule fires from a phase its site owns, given that the evaluation's do. This is the howner field of the program's DescriptiveComplexity.Draw.Assembly.

                  Dependency graph
                  source
                  theorem DescriptiveComplexity.Draw.Data.nexSep {L : FirstOrder.Language} {dt : Data L} {A Q B G PE SE : Type} [DecidableEq dt.SlotIx] {one : A} {ShE : SE → Type} {β : SweepSpec A Q dt.SlotIx B} {γ : GuessSpec A Q dt.SlotIx B G} {ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (NexPh B PE)} {evalEntry : PE} {bot : B} (hsepE : ∀ (e : SE) (ρ ρ' : ShE e) (f : Q → A) (g : dt.SlotIx → A), (ruleE e ρ).guard f g → (ruleE e ρ').guard f g → (ruleE e ρ).srcPh = (ruleE e ρ').srcPh → ρ = ρ') (i : NexSite SE) :
                  i ≠ NexSite.guess → i ≠ NexSite.approach → ∀ (ρ ρ' : NexSh SE B G ShE i) (f : Q → A) (g : dt.SlotIx → A), (dt.nexRule one β γ ruleE evalEntry bot i ρ).guard f g → (dt.nexRule one β γ ruleE evalEntry bot i ρ').guard f g → (dt.nexRule one β γ ruleE evalEntry bot i ρ).srcPh = (dt.nexRule one β γ ruleE evalEntry bot i ρ').srcPh → ρ = ρ'

                  Every site but the guess separates in-shape. The two sweeps' steps are told from their exits by the stop test, the walks home by their kits, and the accepting site has no rules at all; the guessing site is left out because its shapes are the certificate's values, all firing under one guard, which is the program's only nondeterminism.

                  Dependency graph
                  source
                  theorem DescriptiveComplexity.Draw.Data.postGuess_nexRule {L : FirstOrder.Language} {dt : Data L} {A Q B G PE SE : Type} [DecidableEq dt.SlotIx] {one : A} {ShE : SE → Type} {β : SweepSpec A Q dt.SlotIx B} {γ : GuessSpec A Q dt.SlotIx B G} {ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (NexPh B PE)} {evalEntry : PE} {bot : B} (hclosedE : ∀ (e : SE) (ρ : ShE e), (ruleE e ρ).dstPh.PostGuess) (i : NexSite SE) (ρ : NexSh SE B G ShE i) :
                  (dt.nexRule one β γ ruleE evalEntry bot i ρ).srcPh.PostGuess → (dt.nexRule one β γ ruleE evalEntry bot i ρ).dstPh.PostGuess

                  No rule leaves the post-guess phases, given that the evaluation's do not. With nexSep_postGuess this is what says the clocked program guesses once and is deterministic ever after.

                  Dependency graph
                  source
                  theorem DescriptiveComplexity.Draw.Data.nexSep_postGuess {L : FirstOrder.Language} {dt : Data L} {A Q B G PE SE : Type} [DecidableEq dt.SlotIx] {one : A} {ShE : SE → Type} {β : SweepSpec A Q dt.SlotIx B} {γ : GuessSpec A Q dt.SlotIx B G} {ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (NexPh B PE)} {evalEntry : PE} {bot : B} (hsepE : ∀ (e : SE) (ρ ρ' : ShE e) (f : Q → A) (g : dt.SlotIx → A), (ruleE e ρ).guard f g → (ruleE e ρ').guard f g → (ruleE e ρ).srcPh = (ruleE e ρ').srcPh → ρ = ρ') (i : NexSite SE) (ρ ρ' : NexSh SE B G ShE i) (f : Q → A) (g : dt.SlotIx → A) :
                  (dt.nexRule one β γ ruleE evalEntry bot i ρ).srcPh.PostGuess → (dt.nexRule one β γ ruleE evalEntry bot i ρ).guard f g → (dt.nexRule one β γ ruleE evalEntry bot i ρ').guard f g → (dt.nexRule one β γ ruleE evalEntry bot i ρ).srcPh = (dt.nexRule one β γ ruleE evalEntry bot i ρ').srcPh → ρ = ρ'

                  The clocked program separates in-shape at every phase it can be in after the guess. The guessing site is excluded by its phase, not by hand: its rules fire from NexPh.guessP alone, which postGuess_nexRule shows unreachable from there on.

                  Dependency graph

                  The rules, discharged #

                  Each phase of the outer layer, in the form its run asks for: a rightward or a leftward rule with its six attributes. The two walks home are HomeKit's, so their own rules are hrules specialized and need nothing here.

                  source
                  theorem DescriptiveComplexity.Draw.Data.hasRight_start {L : FirstOrder.Language} {dt : Data L} {A R' Q B PE SE G : Type} [Fintype Q] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {ShE : SE → Type} {PR : Prog A R' (NexPh B PE) Q dt.SlotIx dt.KIx dt.dd} {β : SweepSpec A Q dt.SlotIx B} {γ : GuessSpec A Q dt.SlotIx B G} {ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (NexPh B PE)} {evalEntry : PE} {bot : B} {rEmb : (i : NexSite SE) → NexSh SE B G ShE i → R'} (hrules : ∀ (i : NexSite SE) (ρ : NexSh SE B G ShE i), PR.rules (rEmb i ρ) = dt.nexRule PR.one β γ ruleE evalEntry bot i ρ) (f : Q → A) (g : dt.SlotIx → A) :
                  PR.HasRight NexPh.start f g NexPh.approachP f (Function.update (Function.update g Slot.wk PR.one) Slot.bot PR.one)

                  The opening step: mark the home cell – the working marker and the bottom mark alike – and set off for the file's base.

                  Dependency graph
                  source
                  theorem DescriptiveComplexity.Draw.Data.hasRight_approach {L : FirstOrder.Language} {dt : Data L} {A R' Q B PE SE G : Type} [Fintype Q] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {ShE : SE → Type} {PR : Prog A R' (NexPh B PE) Q dt.SlotIx dt.KIx dt.dd} {β : SweepSpec A Q dt.SlotIx B} {γ : GuessSpec A Q dt.SlotIx B G} {ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (NexPh B PE)} {evalEntry : PE} {bot : B} {rEmb : (i : NexSite SE) → NexSh SE B G ShE i → R'} (hrules : ∀ (i : NexSite SE) (ρ : NexSh SE B G ShE i), PR.rules (rEmb i ρ) = dt.nexRule PR.one β γ ruleE evalEntry bot i ρ) (f : Q → A) (g : dt.SlotIx → A) :
                  PR.HasRight NexPh.approachP f g NexPh.approachP f g

                  A step of the approach walk: move on, writing nothing.

                  Dependency graph
                  source
                  theorem DescriptiveComplexity.Draw.Data.hasRight_approachExit {L : FirstOrder.Language} {dt : Data L} {A R' Q B PE SE G : Type} [Fintype Q] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {ShE : SE → Type} {PR : Prog A R' (NexPh B PE) Q dt.SlotIx dt.KIx dt.dd} {β : SweepSpec A Q dt.SlotIx B} {γ : GuessSpec A Q dt.SlotIx B G} {ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (NexPh B PE)} {evalEntry : PE} {bot : B} {rEmb : (i : NexSite SE) → NexSh SE B G ShE i → R'} (hrules : ∀ (i : NexSite SE) (ρ : NexSh SE B G ShE i), PR.rules (rEmb i ρ) = dt.nexRule PR.one β γ ruleE evalEntry bot i ρ) (f : Q → A) (g : dt.SlotIx → A) :
                  PR.HasRight NexPh.approachP f g (NexPh.buildP bot) f g

                  The approach's exit: stop walking and start laying the file here.

                  Dependency graph
                  source
                  theorem DescriptiveComplexity.Draw.Data.hasRight_build {L : FirstOrder.Language} {dt : Data L} {A R' Q B PE SE G : Type} [Fintype Q] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {ShE : SE → Type} {PR : Prog A R' (NexPh B PE) Q dt.SlotIx dt.KIx dt.dd} {β : SweepSpec A Q dt.SlotIx B} {γ : GuessSpec A Q dt.SlotIx B G} {ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (NexPh B PE)} {evalEntry : PE} {bot : B} {rEmb : (i : NexSite SE) → NexSh SE B G ShE i → R'} (hrules : ∀ (i : NexSite SE) (ρ : NexSh SE B G ShE i), PR.rules (rEmb i ρ) = dt.nexRule PR.one β γ ruleE evalEntry bot i ρ) (b : B) (f : Q → A) (g : dt.SlotIx → A) (hg : ¬β.Roll b f) :
                  PR.HasRight (NexPh.buildP b) f g (NexPh.buildP b) (β.st b f g) (β.wr b f g)

                  The file-laying sweep's step: write the cell, advance the pointer, move on.

                  Dependency graph
                  source
                  theorem DescriptiveComplexity.Draw.Data.hasRight_buildRoll {L : FirstOrder.Language} {dt : Data L} {A R' Q B PE SE G : Type} [Fintype Q] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {ShE : SE → Type} {PR : Prog A R' (NexPh B PE) Q dt.SlotIx dt.KIx dt.dd} {β : SweepSpec A Q dt.SlotIx B} {γ : GuessSpec A Q dt.SlotIx B G} {ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (NexPh B PE)} {evalEntry : PE} {bot : B} {rEmb : (i : NexSite SE) → NexSh SE B G ShE i → R'} (hrules : ∀ (i : NexSite SE) (ρ : NexSh SE B G ShE i), PR.rules (rEmb i ρ) = dt.nexRule PR.one β γ ruleE evalEntry bot i ρ) (b : B) (f : Q → A) (g : dt.SlotIx → A) (hroll : β.Roll b f) (hg : ¬β.Done b f) :
                  PR.HasRight (NexPh.buildP b) f g (NexPh.buildP (β.nx b)) (β.stRoll b f g) (β.wr b f g)

                  The file-laying sweep's roll-over: the last tuple of a block is written and the pointer opens the next one.

                  Dependency graph
                  source
                  theorem DescriptiveComplexity.Draw.Data.hasRight_buildLast {L : FirstOrder.Language} {dt : Data L} {A R' Q B PE SE G : Type} [Fintype Q] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {ShE : SE → Type} {PR : Prog A R' (NexPh B PE) Q dt.SlotIx dt.KIx dt.dd} {β : SweepSpec A Q dt.SlotIx B} {γ : GuessSpec A Q dt.SlotIx B G} {ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (NexPh B PE)} {evalEntry : PE} {bot : B} {rEmb : (i : NexSite SE) → NexSh SE B G ShE i → R'} (hrules : ∀ (i : NexSite SE) (ρ : NexSh SE B G ShE i), PR.rules (rEmb i ρ) = dt.nexRule PR.one β γ ruleE evalEntry bot i ρ) (b : B) (f : Q → A) (g : dt.SlotIx → A) (hroll : β.Roll b f) (hg : β.Done b f) :
                  PR.HasRight (NexPh.buildP b) f g NexPh.buildDoneP (β.stRoll b f g) (β.wr b f g)

                  The file-laying sweep's exit: the pointer is past the file's top, so turn round.

                  Dependency graph
                  source
                  theorem DescriptiveComplexity.Draw.Data.hasLeft_buildExit {L : FirstOrder.Language} {dt : Data L} {A R' Q B PE SE G : Type} [Fintype Q] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {ShE : SE → Type} {PR : Prog A R' (NexPh B PE) Q dt.SlotIx dt.KIx dt.dd} {β : SweepSpec A Q dt.SlotIx B} {γ : GuessSpec A Q dt.SlotIx B G} {ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (NexPh B PE)} {evalEntry : PE} {bot : B} {rEmb : (i : NexSite SE) → NexSh SE B G ShE i → R'} (hrules : ∀ (i : NexSite SE) (ρ : NexSh SE B G ShE i), PR.rules (rEmb i ρ) = dt.nexRule PR.one β γ ruleE evalEntry bot i ρ) (f : Q → A) (g : dt.SlotIx → A) :
                  PR.HasLeft NexPh.buildDoneP f g NexPh.homeBuildP f g

                  The file-laying sweep's turn-around: one cell past the last register, the file laid, the machine turns back.

                  Dependency graph
                  source
                  theorem DescriptiveComplexity.Draw.Data.hasRight_homeBuildExit {L : FirstOrder.Language} {dt : Data L} {A R' Q B PE SE G : Type} [Fintype Q] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {ShE : SE → Type} {PR : Prog A R' (NexPh B PE) Q dt.SlotIx dt.KIx dt.dd} {β : SweepSpec A Q dt.SlotIx B} {γ : GuessSpec A Q dt.SlotIx B G} {ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (NexPh B PE)} {evalEntry : PE} {bot : B} {rEmb : (i : NexSite SE) → NexSh SE B G ShE i → R'} (hrules : ∀ (i : NexSite SE) (ρ : NexSh SE B G ShE i), PR.rules (rEmb i ρ) = dt.nexRule PR.one β γ ruleE evalEntry bot i ρ) (f : Q → A) (g : dt.SlotIx → A) (hg : dt.exitG PR.one g) :
                  PR.HasRight NexPh.homeBuildP f g (NexPh.guessP bot) (β.st0 f g) g

                  The exit of the walk home after the file: at the marker, start guessing.

                  Dependency graph
                  source
                  theorem DescriptiveComplexity.Draw.Data.hasRight_guess {L : FirstOrder.Language} {dt : Data L} {A R' Q B PE SE G : Type} [Fintype Q] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {ShE : SE → Type} {PR : Prog A R' (NexPh B PE) Q dt.SlotIx dt.KIx dt.dd} {β : SweepSpec A Q dt.SlotIx B} {γ : GuessSpec A Q dt.SlotIx B G} {ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (NexPh B PE)} {evalEntry : PE} {bot : B} {rEmb : (i : NexSite SE) → NexSh SE B G ShE i → R'} (hrules : ∀ (i : NexSite SE) (ρ : NexSh SE B G ShE i), PR.rules (rEmb i ρ) = dt.nexRule PR.one β γ ruleE evalEntry bot i ρ) (b : B) (x : G) (f : Q → A) (g : dt.SlotIx → A) (hg : ¬γ.Roll b f) :
                  PR.HasRight (NexPh.guessP b) f g (NexPh.guessP b) (γ.st b x f g) (γ.wr b x f g)

                  The guessing sweep's step, at one value: every value fires under the same guard, which is the program's whole nondeterminism.

                  Dependency graph
                  source
                  theorem DescriptiveComplexity.Draw.Data.hasRight_guessRoll {L : FirstOrder.Language} {dt : Data L} {A R' Q B PE SE G : Type} [Fintype Q] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {ShE : SE → Type} {PR : Prog A R' (NexPh B PE) Q dt.SlotIx dt.KIx dt.dd} {β : SweepSpec A Q dt.SlotIx B} {γ : GuessSpec A Q dt.SlotIx B G} {ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (NexPh B PE)} {evalEntry : PE} {bot : B} {rEmb : (i : NexSite SE) → NexSh SE B G ShE i → R'} (hrules : ∀ (i : NexSite SE) (ρ : NexSh SE B G ShE i), PR.rules (rEmb i ρ) = dt.nexRule PR.one β γ ruleE evalEntry bot i ρ) (b : B) (x : G) (f : Q → A) (g : dt.SlotIx → A) (hroll : γ.Roll b f) (hg : ¬γ.Done b f) :
                  PR.HasRight (NexPh.guessP b) f g (NexPh.guessP (γ.nx b)) (γ.stRoll b x f g) (γ.wr b x f g)

                  The guessing sweep's roll-over, at one value.

                  Dependency graph
                  source
                  theorem DescriptiveComplexity.Draw.Data.hasRight_guessLast {L : FirstOrder.Language} {dt : Data L} {A R' Q B PE SE G : Type} [Fintype Q] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {ShE : SE → Type} {PR : Prog A R' (NexPh B PE) Q dt.SlotIx dt.KIx dt.dd} {β : SweepSpec A Q dt.SlotIx B} {γ : GuessSpec A Q dt.SlotIx B G} {ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (NexPh B PE)} {evalEntry : PE} {bot : B} {rEmb : (i : NexSite SE) → NexSh SE B G ShE i → R'} (hrules : ∀ (i : NexSite SE) (ρ : NexSh SE B G ShE i), PR.rules (rEmb i ρ) = dt.nexRule PR.one β γ ruleE evalEntry bot i ρ) (b : B) (x : G) (f : Q → A) (g : dt.SlotIx → A) (hroll : γ.Roll b f) (hg : γ.Done b f) :
                  PR.HasRight (NexPh.guessP b) f g NexPh.guessDoneP (γ.stRoll b x f g) (γ.wr b x f g)

                  The guessing sweep's exit.

                  Dependency graph
                  source
                  theorem DescriptiveComplexity.Draw.Data.hasLeft_guessExit {L : FirstOrder.Language} {dt : Data L} {A R' Q B PE SE G : Type} [Fintype Q] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {ShE : SE → Type} {PR : Prog A R' (NexPh B PE) Q dt.SlotIx dt.KIx dt.dd} {β : SweepSpec A Q dt.SlotIx B} {γ : GuessSpec A Q dt.SlotIx B G} {ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (NexPh B PE)} {evalEntry : PE} {bot : B} {rEmb : (i : NexSite SE) → NexSh SE B G ShE i → R'} (hrules : ∀ (i : NexSite SE) (ρ : NexSh SE B G ShE i), PR.rules (rEmb i ρ) = dt.nexRule PR.one β γ ruleE evalEntry bot i ρ) (f : Q → A) (g : dt.SlotIx → A) :
                  PR.HasLeft NexPh.guessDoneP f g NexPh.homeGuessP f g

                  The guessing sweep's turn-around.

                  Dependency graph
                  source
                  theorem DescriptiveComplexity.Draw.Data.hasLeft_guessStop {L : FirstOrder.Language} {dt : Data L} {A R' Q B PE SE G : Type} [Fintype Q] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {ShE : SE → Type} {PR : Prog A R' (NexPh B PE) Q dt.SlotIx dt.KIx dt.dd} {β : SweepSpec A Q dt.SlotIx B} {γ : GuessSpec A Q dt.SlotIx B G} {ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (NexPh B PE)} {evalEntry : PE} {bot : B} {rEmb : (i : NexSite SE) → NexSh SE B G ShE i → R'} (hrules : ∀ (i : NexSite SE) (ρ : NexSh SE B G ShE i), PR.rules (rEmb i ρ) = dt.nexRule PR.one β γ ruleE evalEntry bot i ρ) (b : B) (f : Q → A) (g : dt.SlotIx → A) :
                  PR.HasLeft (NexPh.guessP b) f g NexPh.homeGuessP f g

                  The guessing sweep stops here: the rule that ends a region-wide guess, available at every address, so where the walk stops is one more nondeterministic choice and nothing has to recognize the region's end.

                  Dependency graph
                  source
                  theorem DescriptiveComplexity.Draw.Data.hasRight_homeGuessExit {L : FirstOrder.Language} {dt : Data L} {A R' Q B PE SE G : Type} [Fintype Q] [Fintype dt.SlotIx] [DecidableEq dt.SlotIx] {ShE : SE → Type} {PR : Prog A R' (NexPh B PE) Q dt.SlotIx dt.KIx dt.dd} {β : SweepSpec A Q dt.SlotIx B} {γ : GuessSpec A Q dt.SlotIx B G} {ruleE : (e : SE) → ShE e → Rule A Q dt.SlotIx (NexPh B PE)} {evalEntry : PE} {bot : B} {rEmb : (i : NexSite SE) → NexSh SE B G ShE i → R'} (hrules : ∀ (i : NexSite SE) (ρ : NexSh SE B G ShE i), PR.rules (rEmb i ρ) = dt.nexRule PR.one β γ ruleE evalEntry bot i ρ) (f : Q → A) (g : dt.SlotIx → A) (hg : dt.exitG PR.one g) :
                  PR.HasRight NexPh.homeGuessP f g (NexPh.evalP evalEntry) f g

                  The exit of the walk home after the guess: at the marker, enter the evaluation.

                  Dependency graph