Internal variables of incidence trails

In an edge instance, an internal visit uses both incidences of its variable. It cannot therefore revisit a trail's starting variable. These structural facts transfer internal consistency through a preparatory root-path flip, using the existing exact defect equation.

theorem Cslib.Logic.PL.CSP.Walk.InternallyConsistent.append_of_outputs {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {f : F.OccurrenceLabeling Bool} {ss ts : List (F.Occurrence × F.Occurrence)} (hs : ∀ s ∈ ss, ¬Inconsistent f s.2.var) (ht : InternallyConsistent f ts) : InternallyConsistent f (ss ++ ts)

Consistency at every output of the left segment permits any internally consistent continuation. The last output is included because the continuation may be nonempty.

theorem Cslib.Logic.PL.CSP.Walk.internallyConsistent_iff_splits {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (f : F.OccurrenceLabeling Bool) (ss : List (F.Occurrence × F.Occurrence)) : InternallyConsistent f ss ↔ ∀ (pre : List (F.Occurrence × F.Occurrence)) (o p a b : F.Occurrence) (post : List (F.Occurrence × F.Occurrence)), ss = pre ++ (o, p) :: (a, b) :: post → ¬Inconsistent f p.var

Internal consistency is exactly consistency at every transition between consecutive steps.

theorem Cslib.Logic.PL.CSP.Walk.IsWalk.internal_var_ne_start {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (hF : F.EdgeInstance) {w : F.Walk} (hw : w.IsWalk) {pre post : List (F.Occurrence × F.Occurrence)} {o p a b : F.Occurrence} (he : w.steps = pre ++ (o, p) :: (a, b) :: post) : p.var ≠ w.start

An internal variable cannot equal the starting variable of an incidence trail in an edge instance: the transition would need a third distinct incidence at that variable.

theorem Cslib.Logic.PL.CSP.Walk.IsWalk.internallyConsistent_flip {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (hF : F.EdgeInstance) {w prep : F.Walk} (hw : w.IsWalk) (hp : prep.IsWalk) (f : F.OccurrenceLabeling Bool) (he : prep.finish = w.start) (hr : Inconsistent f prep.start) (hi : InternallyConsistent f w.steps) : InternallyConsistent (prep.flip f) w.steps

Preparing a walk's base by a trail from an inconsistent root preserves all of the walk's original internal consistency. Validity of labelings is a separate obligation.