Variable-ended subpaths of directed incidence trails

Dropping whole steps starts at the actual endpoint of the removed prefix. Directed paths inherit their ambient DAG certificate on suffixes, so Corollary 36 applies to suffixes without assuming that reversal preserves arbitrary f-walk validity.

theorem Cslib.Logic.PL.CSP.Walk.IsWalk.snoc {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {w : F.Walk} (hw : w.IsWalk) {o p : F.Occurrence} (ho : o.var = w.finish) (hc : o.fst = p.fst) (hne : o ≠ p) (hno : o ∉ w.edges) (hnp : p ∉ w.edges) : (w.snoc o p).IsWalk

Append one linked step at two distinct unused incidences.

theorem Cslib.Logic.PL.CSP.Walk.InternallyConsistent.reverse {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {v : V} {ss : List (F.Occurrence × F.Occurrence)} {f : F.OccurrenceLabeling Bool} (hl : Linked v ss) (hc : InternallyConsistent f ss) : InternallyConsistent f (List.map Prod.swap ss.reverse)

Reversing a linked walk preserves consistency of its internal variables. This says nothing about prefix validity, which need not survive reversal.

def Cslib.Logic.PL.CSP.Walk.drop {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) (n : ℕ) : F.Walk

Remove the first n steps, starting at the endpoint of that prefix.

theorem Cslib.Logic.PL.CSP.Walk.IsWalk.drop {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {w : F.Walk} (hw : w.IsWalk) (n : ℕ) : (w.drop n).IsWalk

A suffix of a linked incidence trail remains a linked incidence trail.

@[simp]

theorem Cslib.Logic.PL.CSP.Walk.take_append_drop {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) (n : ℕ) : (w.take n).append (w.drop n) = w

The prefix and suffix recover the exact candidate steps and starting variable.

@[simp]

theorem Cslib.Logic.PL.CSP.Walk.finish_drop {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) (n : ℕ) : (w.drop n).finish = w.finish

Removing a prefix does not change the final variable.

theorem Cslib.Logic.PL.CSP.Walk.finish_step {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) (hne : w.steps ≠ []) : ∃ s ∈ w.steps, s.2.var = w.finish

A nonempty candidate ends at the output variable of one of its actual steps.

theorem Cslib.Logic.PL.CSP.Walk.finish_take_succ {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w : F.Walk) {k : ℕ} (hk : k < w.steps.length) : (w.take (k + 1)).finish = w.steps[k].2.var

The prefix through a selected step ends at that step's output variable.

theorem Cslib.Logic.PL.CSP.Walk.IsWalk.flip_take_succ {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {w : F.Walk} (hw : w.IsWalk) (f : F.OccurrenceLabeling Bool) {k : ℕ} (hk : k < w.steps.length) : (w.take (k + 1)).flip f = DAG.pairFlip ((w.take k).flip f) w.steps[k].1 w.steps[k].2

Extending a trail prefix by its next actual step performs exactly the corresponding two-port move, with cancellation handled by DAG.pairFlip.

theorem Cslib.Logic.PL.CSP.Walk.IsWalk.join_meeting {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {w z : F.Walk} (hw : w.IsWalk) (hz : z.IsWalk) {a b : F.Occurrence} (ha : a.var = w.finish) (hb : b.var = z.finish) (hc : a.fst = b.fst) (hne : a ≠ b) (hd : w.edges.Disjoint z.edges) (haw : a ∉ w.edges) (hbw : b ∉ w.edges) (haz : a ∉ z.edges) (hbz : b ∉ z.edges) : ((w.snoc a b).append z.reverse).IsWalk

Join two disjoint trails at a fresh constraint step, traversing the second trail in reverse. Prefix validity is a separate theorem about directed DAG paths.

theorem Cslib.Logic.PL.CSP.Walk.finish_join_meeting {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (w z : F.Walk) (a b : F.Occurrence) (hz : Linked z.start z.steps) (hb : b.var = z.finish) : ((w.snoc a b).append z.reverse).finish = z.start

Joining at the second trail's endpoint and reading it backward ends at its start.

theorem Cslib.Logic.PL.CSP.DAG.DirectedPath.mono {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {S T : F.DAG} {w : F.Walk} {time : F.Occurrence → ℕ} (hp : S.DirectedPath w time) (hst : S.Subgraph T) : T.DirectedPath w time

A directed path remains directed in a larger incidence graph.

theorem Cslib.Logic.PL.CSP.DAG.DirectedPath.mem_copies {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {T : F.DAG} {w : F.Walk} {time : F.Occurrence → ℕ} (hp : T.DirectedPath w time) {c : Copy F} : c ∈ (pathDAG w time).copies ↔ ∃ s ∈ w.steps, (inArc time s).copy = c

Copied constraints of a directed path are exactly the copied nodes of its steps.

theorem Cslib.Logic.PL.CSP.DAG.DirectedPath.finish_mem {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {T : F.DAG} {w : F.Walk} {time : F.Occurrence → ℕ} (hp : T.DirectedPath w time) (hs : T.Supported) : w.finish ∈ T.vars

Both endpoints of a directed path belong to its ambient graph's variable support.

theorem Cslib.Logic.PL.CSP.DAG.DirectedPath.drop {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {T : F.DAG} {w : F.Walk} {time : F.Occurrence → ℕ} (hp : T.DirectedPath w time) (hs : T.Supported) (n : ℕ) : T.DirectedPath (w.drop n) time

A suffix is a directed path in the same ambient graph, at the original timestamps.

theorem Cslib.Logic.PL.CSP.DAG.DirectedPath.disjoint_edges {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {T : F.DAG} {w z : F.Walk} {timeW timeZ : F.Occurrence → ℕ} (hw : T.DirectedPath w timeW) (hz : T.DirectedPath z timeZ) (h : IsFDAG sem f T) (hd : Disjoint (pathDAG w timeW).copies (pathDAG z timeZ).copies) : w.edges.Disjoint z.edges

Copied-node disjointness of paths in an f-DAG implies disjointness of their actual incidence lists, by the original-incidence uniqueness condition.

theorem Cslib.Logic.PL.CSP.DAG.meeting_flip_eq {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (w z : F.Walk) (timeW timeZ : F.Occurrence → ℕ) (a b : Arc F) (f : F.OccurrenceLabeling Bool) : (((pathDAG w timeW).union (pathDAG z timeZ)).union (terminalPair a b)).flip f = ((w.snoc a.occurrence b.occurrence).append z.reverse).flip f

The graph flip at two meeting paths equals the flip of their joined positional walk. This identity alone does not assert validity of any prefix.

theorem Cslib.Logic.PL.CSP.DAG.DirectedPath.valid_take_meeting {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {T : F.DAG} {w z : F.Walk} {timeW timeZ : F.Occurrence → ℕ} {a b : Arc F} (hw : T.DirectedPath w timeW) (hz : T.DirectedPath z timeZ) (h : IsFDAG sem f T) (hM : EdgeInstance.EvenConstraints sem F) (ha : a ∈ T.arcs) (hb : b ∈ T.arcs) (hai : a.incoming = true) (hcopy : a.copy = b.copy) (hne : a ≠ b) (hd : Disjoint (pathDAG w timeW).copies (pathDAG z timeZ).copies) (hwfresh : a.copy ∉ (pathDAG w timeW).copies) (hzfresh : a.copy ∉ (pathDAG z timeZ).copies) (n : ℕ) : ValidLabeling sem ((((w.snoc a.occurrence b.occurrence).append z.reverse).take n).flip f)

Every variable-ended prefix of the walk formed by two meeting directed paths has a valid flip. Prefixes after the meeting use suffixes of the second directed path in Corollary 36; this does not assume reversal closure of f-walks.