First entry of an incidence walk into a finite variable set

The first boundary index scans actual step outputs. Linkage proves that all preceding ports are outside and that the first internal port is an output. Variable names are compared as data; no integer interval below their binary values is enumerated.

theorem Cslib.Logic.PL.CSP.Walk.Linked.forall_ports {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {P : V → Prop} {v : V} {ss : List (F.Occurrence × F.Occurrence)} (hl : Linked v ss) (hv : P v) (houtputs : ∀ s ∈ ss, P s.2.var) (o : F.Occurrence) : o ∈ edgesOf ss → P o.var

A linked walk preserves a variable property at all ports when its start and every step output have that property.

theorem Cslib.Logic.PL.CSP.Walk.finish_property {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) {P : V → Prop} (hs : P w.start) (hp : ∀ o ∈ w.edges, P o.var) : P w.finish

The last variable has every property shared by the start and all actual used ports.

theorem Cslib.Logic.PL.CSP.Walk.IsWalk.input_eq_finish_take {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {w : F.Walk} (hw : w.IsWalk) (j : ℕ) (hj : j < w.steps.length) : w.steps[j].1.var = (w.take j).finish

The next actual input names the final variable of its preceding whole-step prefix.

def Cslib.Logic.PL.CSP.Walk.boundaryIndex {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (w : F.Walk) (vs : List V) : ℕ

The first step whose output names a selected variable; length means no such step.

theorem Cslib.Logic.PL.CSP.Walk.boundaryIndex_spec {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {w : F.Walk} (hw : w.IsWalk) (vs : List V) (hstart : w.start ∉ vs) (hex : ∃ o ∈ w.edges, o.var ∈ vs) : ∃ (hk : w.boundaryIndex vs < w.steps.length), w.steps[w.boundaryIndex vs].2.var ∈ vs ∧ ∀ o ∈ (w.take (w.boundaryIndex vs)).edges, o.var ∉ vs

First-entry scan correctness, including avoidance by every earlier actual incidence.