Add connected word defintion and format Ochmanski.lean

Author: yisiox

TraceTheory/TraceTheory/Basic.lean

@@ -841,4 +841,23 @@ theorem prod_filter_not_isEmpty (L : List (Trace I)) :
 
 end Trace
 
+namespace List
+
+/-- Predicate for dependence of symbols `a` and `b` in word `x`. -/
+def DepEdge (I : Independence α) (x : List α) (a b : α) :=
+  I.inducedDependence.rel a b ∧ a ∈ x ∧ b ∈ x
+
+/-- Predicate for transitive dependence of symbols `a` and `b` in word `x`. -/
+def DepPath (I : Independence α) (x : List α) (a b : α) :=
+  Relation.TransGen (DepEdge I x) a b
+
+/-- A word `x` is connected if all its symbols are transitively dependent. -/
+def IsConnected (I : Independence α) (x : List α) :=
+  ∀ a ∈ x, ∀ b ∈ x, DepPath I x a b
+
+theorem IsConnected_iff_traceIsConnected (I : Independence α) (w : List α) :
+    IsConnected I w = Trace.IsConnected I ⟦w⟧ := rfl
+
+end List
+
 end TraceTheory

TraceTheory/TraceTheory/Ochmanski.lean

@@ -10,7 +10,8 @@ open Computability Dependence RegularExpression Trace Independence
 
 variable {α : Type} {I : Independence α}
 
-/-- Main component of Theorem 4.1 (ii) => (iii).
+/-
+  Main component of Theorem 4.1 (ii) => (iii).
 
   For a rational expression X, if every iterative factor of L(X) is connected,
   then X' is star-connected (for some rational expression X' with L(X) = L(X')).
@@ -28,7 +29,7 @@ lemma exists_starConnected_of_connectedIterativeFactors_aux
   induction X with
   | zero => use zero, trivial
   | epsilon => use epsilon, trivial
-  | char a => use char a, trivial
+  | char a => use .char a, trivial
   | plus P Q ihP ihQ =>
     have condP : ∀ s, IsIterativeFactor P.matches' s → Trace.IsConnected I ⟦s⟧ := by
       intro s ⟨u, v, h⟩