import AntiDynamics.Lifting

/-!
# Bridge to literal strings: the Syntactic Lemma and the definition of Transparency

The paper defines Transparency on *strings*: for every initial string `α d̲d'` of the sentence
and every sentence completion `β` (any string making `α (d and γ) β` a formula),
`C ⊨ α (d and γ) β ⇔ α γ β`.  `Core.lean` uses one-hole *contexts* instead.  Here we prove
that the two definitions coincide, for formulas over an arbitrary set of leaf tokens `L`
(leaves are single tokens; for the propositional fragment this is exactly the language of (18)).

* `ser` : the bracketed serialization `(not F)`, `(F and G)`, `(F or G)`, `(if F . G)`.
* `ser_append_inj` : unique readability (prefix-freeness) = **Syntactic Lemma (19b)**.
* `syntactic_lemma_a` : **Syntactic Lemma (19a)** in the form in which it is used: if the string
  `α φ β` (with `α` the initial string of an occurrence and `φ` a constituent) is a formula
  then `φ` is a constituent of it at the same position, i.e. the formula is a completion
  context applied to `φ`.
* `StrTransp` : literal reading of (26); `strTransp_iff_transp` : equivalence with `Sys.Transp`.
-/

namespace AntiDyn

variable {L : Type}

inductive Tok (L : Type) where
  | lp | rp | kNot | kAnd | kOr | kIf | kDot
  | lf (l : L)
  deriving DecidableEq

open Tok

/-- Bracketed serialization: `(not F)`, `(F and G)`, `(F or G)`, `(if F . G)`. -/
def ser : Fm L → List (Tok L)
  | .leaf l => [lf l]
  | .neg F => lp :: kNot :: (ser F ++ [rp])
  | .conj F G => lp :: (ser F ++ kAnd :: (ser G ++ [rp]))
  | .disj F G => lp :: (ser F ++ kOr :: (ser G ++ [rp]))
  | .cond F G => lp :: kIf :: (ser F ++ kDot :: (ser G ++ [rp]))

theorem ser_head (F : Fm L) : (∃ l r, ser F = lf l :: r) ∨ ∃ r, ser F = lp :: r := by
  cases F <;> simp [ser]

/-- **Syntactic Lemma (19b)** / unique readability: no formula string is a proper initial
string of another formula string. -/
theorem ser_append_inj : ∀ (F G : Fm L) (s t : List (Tok L)), ser F ++ s = ser G ++ t →
    F = G ∧ s = t := by
  intro F
  induction F with
  | leaf l =>
    intro G s t h
    cases G with
    | leaf l' => simp [ser] at h; exact ⟨by rw [h.1], h.2⟩
    | neg G => simp [ser] at h
    | conj G1 G2 => simp [ser] at h
    | disj G1 G2 => simp [ser] at h
    | cond G1 G2 => simp [ser] at h
  | neg F ih =>
    intro G s t h
    cases G with
    | leaf l' => simp [ser] at h
    | neg G =>
      simp only [ser, List.cons_append, List.cons.injEq, true_and, List.append_assoc] at h
      have := ih G _ _ h
      exact ⟨by rw [this.1], by simpa using this.2⟩
    | conj G1 G2 =>
      simp only [ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases ser_head G1 with ⟨l, r, e⟩ | ⟨r, e⟩ <;> simp [e] at h
    | disj G1 G2 =>
      simp only [ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases ser_head G1 with ⟨l, r, e⟩ | ⟨r, e⟩ <;> simp [e] at h
    | cond G1 G2 => simp [ser] at h
  | conj F1 F2 ih1 ih2 =>
    intro G s t h
    cases G with
    | leaf l' => simp [ser] at h
    | neg G =>
      simp only [ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases ser_head F1 with ⟨l, r, e⟩ | ⟨r, e⟩ <;> simp [e] at h
    | conj G1 G2 =>
      simp only [ser, List.cons_append, List.cons.injEq, true_and, List.append_assoc] at h
      obtain ⟨e1, e2⟩ := ih1 G1 _ _ h
      simp only [List.cons.injEq, true_and] at e2
      obtain ⟨e3, e4⟩ := ih2 G2 _ _ e2
      subst e1; subst e3
      simpa using e4
    | disj G1 G2 =>
      simp only [ser, List.cons_append, List.cons.injEq, true_and, List.append_assoc] at h
      obtain ⟨e1, e2⟩ := ih1 G1 _ _ h
      simp at e2
    | cond G1 G2 =>
      simp only [ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases ser_head F1 with ⟨l, r, e⟩ | ⟨r, e⟩ <;> simp [e] at h
  | disj F1 F2 ih1 ih2 =>
    intro G s t h
    cases G with
    | leaf l' => simp [ser] at h
    | neg G =>
      simp only [ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases ser_head F1 with ⟨l, r, e⟩ | ⟨r, e⟩ <;> simp [e] at h
    | conj G1 G2 =>
      simp only [ser, List.cons_append, List.cons.injEq, true_and, List.append_assoc] at h
      obtain ⟨e1, e2⟩ := ih1 G1 _ _ h
      simp at e2
    | disj G1 G2 =>
      simp only [ser, List.cons_append, List.cons.injEq, true_and, List.append_assoc] at h
      obtain ⟨e1, e2⟩ := ih1 G1 _ _ h
      simp only [List.cons.injEq, true_and] at e2
      obtain ⟨e3, e4⟩ := ih2 G2 _ _ e2
      subst e1; subst e3
      simpa using e4
    | cond G1 G2 =>
      simp only [ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases ser_head F1 with ⟨l, r, e⟩ | ⟨r, e⟩ <;> simp [e] at h
  | cond F1 F2 ih1 ih2 =>
    intro G s t h
    cases G with
    | leaf l' => simp [ser] at h
    | neg G => simp [ser] at h
    | conj G1 G2 =>
      simp only [ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases ser_head G1 with ⟨l, r, e⟩ | ⟨r, e⟩ <;> simp [e] at h
    | disj G1 G2 =>
      simp only [ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases ser_head G1 with ⟨l, r, e⟩ | ⟨r, e⟩ <;> simp [e] at h
    | cond G1 G2 =>
      simp only [ser, List.cons_append, List.cons.injEq, true_and, List.append_assoc] at h
      obtain ⟨e1, e2⟩ := ih1 G1 _ _ h
      simp only [List.cons.injEq, true_and] at e2
      obtain ⟨e3, e4⟩ := ih2 G2 _ _ e2
      subst e1; subst e3
      simpa using e4


/-! ### Initial string and completion of a context -/

/-- The string to the left of the hole of `π` (the initial string `α`, without the occurrence). -/
def pre : Ctx L → List (Tok L)
  | .hole => []
  | .negC c => lp :: kNot :: pre c
  | .conjL c _ => lp :: pre c
  | .conjR l c => lp :: (ser l ++ kAnd :: pre c)
  | .disjL c _ => lp :: pre c
  | .disjR l c => lp :: (ser l ++ kOr :: pre c)
  | .condL c _ => lp :: kIf :: pre c
  | .condR l c => lp :: kIf :: (ser l ++ kDot :: pre c)

/-- The string to the right of the hole of `π` (the completion `β`). -/
def post : Ctx L → List (Tok L)
  | .hole => []
  | .negC c => post c ++ [rp]
  | .conjL c r => post c ++ kAnd :: (ser r ++ [rp])
  | .conjR _ c => post c ++ [rp]
  | .disjL c r => post c ++ kOr :: (ser r ++ [rp])
  | .disjR _ c => post c ++ [rp]
  | .condL c r => post c ++ kDot :: (ser r ++ [rp])
  | .condR _ c => post c ++ [rp]

theorem ser_plug (π : Ctx L) (X : Fm L) : ser (π.plug X) = pre π ++ ser X ++ post π := by
  induction π with
  | hole => simp [Ctx.plug, pre, post]
  | negC c ih => simp [Ctx.plug, ser, pre, post, ih]
  | conjL c r ih => simp [Ctx.plug, ser, pre, post, ih]
  | conjR l c ih => simp [Ctx.plug, ser, pre, post, ih]
  | disjL c r ih => simp [Ctx.plug, ser, pre, post, ih]
  | disjR l c ih => simp [Ctx.plug, ser, pre, post, ih]
  | condL c r ih => simp [Ctx.plug, ser, pre, post, ih]
  | condR l c ih => simp [Ctx.plug, ser, pre, post, ih]

/-- Completions keep the initial string. -/
theorem pre_compl : ∀ (π π' : Ctx L), Compl π π' → pre π' = pre π := by
  intro π
  induction π with
  | hole => intro π' h; simp only [Compl] at h; subst h; rfl
  | negC c ih =>
    intro π' ⟨c', h, hc⟩; subst h; simp [pre, ih c' hc]
  | conjL c r ih =>
    intro π' ⟨c', r', h, hc⟩
    rcases h with rfl | rfl <;> simp [pre, ih c' hc]
  | conjR l c ih =>
    intro π' ⟨c', h, hc⟩; subst h; simp [pre, ih c' hc]
  | disjL c r ih =>
    intro π' ⟨c', r', h, hc⟩
    rcases h with rfl | rfl <;> simp [pre, ih c' hc]
  | disjR l c ih =>
    intro π' ⟨c', h, hc⟩; subst h; simp [pre, ih c' hc]
  | condL c r ih =>
    intro π' ⟨c', r', h, hc⟩; subst h; simp [pre, ih c' hc]
  | condR l c ih =>
    intro π' ⟨c', h, hc⟩; subst h; simp [pre, ih c' hc]

theorem head_pre (c : Ctx L) (φ : Fm L) (β : List (Tok L)) :
    (∃ l r, pre c ++ ser φ ++ β = lf l :: r) ∨ ∃ r, pre c ++ ser φ ++ β = lp :: r := by
  cases c with
  | hole => rcases ser_head φ with ⟨l, r, e⟩ | ⟨r, e⟩ <;> simp [pre, e]
  | _ => right; simp [pre]

/-- **Syntactic Lemma (19a)**, in the form used in the proofs: if `α φ β` is a formula (for `α`
the initial string of an occurrence, `φ` a constituent, `β` arbitrary), then that formula is
`π'[φ]` for a completion `π'` of `π`, with `β` the completion string of `π'`.  I.e. the
occurrence of `φ` is a constituent of the completed formula, at the same bracket depth, whose
enclosing constituents are determined by `α` alone up to the connective and right operand of
constituents opened by a bare `(`. -/
theorem syntactic_lemma_a : ∀ (c : Ctx L) (φ : Fm L) (β : List (Tok L)) (G : Fm L)
    (tl : List (Tok L)), pre c ++ ser φ ++ β = ser G ++ tl →
    ∃ c'', Compl c c'' ∧ G = c''.plug φ ∧ β = post c'' ++ tl := by
  intro c
  induction c with
  | hole =>
    intro φ β G tl h
    simp only [pre, List.nil_append] at h
    have := ser_append_inj φ G β tl h
    obtain ⟨rfl, rfl⟩ := this
    exact ⟨.hole, rfl, rfl, by simp [post]⟩
  | negC c ih =>
    intro φ β G tl h
    cases G with
    | leaf l' => simp [pre, ser] at h
    | neg G =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and, List.append_assoc] at h
      obtain ⟨c'', hc, hG, hβ⟩ := ih φ β G ([rp] ++ tl) (by simpa using h)
      exact ⟨.negC c'', ⟨c'', rfl, hc⟩, by simp [Ctx.plug, hG], by simp [post, hβ]⟩
    | conj G1 G2 =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases ser_head G1 with ⟨l, r, e⟩ | ⟨r, e⟩ <;> simp [e] at h
    | disj G1 G2 =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases ser_head G1 with ⟨l, r, e⟩ | ⟨r, e⟩ <;> simp [e] at h
    | cond G1 G2 => simp [pre, ser] at h
  | conjL c r ih =>
    intro φ β G tl h
    cases G with
    | leaf l' => simp [pre, ser] at h
    | neg G =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases head_pre c φ β with ⟨l, r, e⟩ | ⟨r, e⟩ <;> rw [e] at h <;> simp at h
    | conj G1 G2 =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and, List.append_assoc] at h
      obtain ⟨c'', hc, hG, hβ⟩ := ih φ β G1 (kAnd :: (ser G2 ++ rp :: tl)) (by simpa using h)
      exact ⟨.conjL c'' G2, ⟨c'', G2, Or.inl rfl, hc⟩, by simp [Ctx.plug, hG], by simp [post, hβ]⟩
    | disj G1 G2 =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and, List.append_assoc] at h
      obtain ⟨c'', hc, hG, hβ⟩ := ih φ β G1 (kOr :: (ser G2 ++ rp :: tl)) (by simpa using h)
      exact ⟨.disjL c'' G2, ⟨c'', G2, Or.inr rfl, hc⟩, by simp [Ctx.plug, hG], by simp [post, hβ]⟩
    | cond G1 G2 =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases head_pre c φ β with ⟨l, r, e⟩ | ⟨r, e⟩ <;> rw [e] at h <;> simp at h
  | disjL c r ih =>
    intro φ β G tl h
    cases G with
    | leaf l' => simp [pre, ser] at h
    | neg G =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases head_pre c φ β with ⟨l, r, e⟩ | ⟨r, e⟩ <;> rw [e] at h <;> simp at h
    | conj G1 G2 =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and, List.append_assoc] at h
      obtain ⟨c'', hc, hG, hβ⟩ := ih φ β G1 (kAnd :: (ser G2 ++ rp :: tl)) (by simpa using h)
      exact ⟨.conjL c'' G2, ⟨c'', G2, Or.inl rfl, hc⟩, by simp [Ctx.plug, hG], by simp [post, hβ]⟩
    | disj G1 G2 =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and, List.append_assoc] at h
      obtain ⟨c'', hc, hG, hβ⟩ := ih φ β G1 (kOr :: (ser G2 ++ rp :: tl)) (by simpa using h)
      exact ⟨.disjL c'' G2, ⟨c'', G2, Or.inr rfl, hc⟩, by simp [Ctx.plug, hG], by simp [post, hβ]⟩
    | cond G1 G2 =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases head_pre c φ β with ⟨l, r, e⟩ | ⟨r, e⟩ <;> rw [e] at h <;> simp at h
  | conjR l c ih =>
    intro φ β G tl h
    cases G with
    | leaf l' => simp [pre, ser] at h
    | neg G =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases ser_head l with ⟨x, r, e⟩ | ⟨r, e⟩ <;> rw [e] at h <;> simp at h
    | conj G1 G2 =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and, List.append_assoc] at h
      obtain ⟨e1, e2⟩ := ser_append_inj l G1 _ _ h
      subst e1
      simp only [List.cons.injEq, true_and] at e2
      obtain ⟨c'', hc, hG, hβ⟩ := ih φ β G2 (rp :: tl) (by simpa using e2)
      exact ⟨.conjR l c'', ⟨c'', rfl, hc⟩, by simp [Ctx.plug, hG], by simp [post, hβ]⟩
    | disj G1 G2 =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and, List.append_assoc] at h
      obtain ⟨e1, e2⟩ := ser_append_inj l G1 _ _ h
      simp at e2
    | cond G1 G2 =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases ser_head l with ⟨x, r, e⟩ | ⟨r, e⟩ <;> rw [e] at h <;> simp at h
  | disjR l c ih =>
    intro φ β G tl h
    cases G with
    | leaf l' => simp [pre, ser] at h
    | neg G =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases ser_head l with ⟨x, r, e⟩ | ⟨r, e⟩ <;> rw [e] at h <;> simp at h
    | conj G1 G2 =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and, List.append_assoc] at h
      obtain ⟨e1, e2⟩ := ser_append_inj l G1 _ _ h
      simp at e2
    | disj G1 G2 =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and, List.append_assoc] at h
      obtain ⟨e1, e2⟩ := ser_append_inj l G1 _ _ h
      subst e1
      simp only [List.cons.injEq, true_and] at e2
      obtain ⟨c'', hc, hG, hβ⟩ := ih φ β G2 (rp :: tl) (by simpa using e2)
      exact ⟨.disjR l c'', ⟨c'', rfl, hc⟩, by simp [Ctx.plug, hG], by simp [post, hβ]⟩
    | cond G1 G2 =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases ser_head l with ⟨x, r, e⟩ | ⟨r, e⟩ <;> rw [e] at h <;> simp at h
  | condL c r ih =>
    intro φ β G tl h
    cases G with
    | leaf l' => simp [pre, ser] at h
    | neg G => simp [pre, ser] at h
    | conj G1 G2 =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases ser_head G1 with ⟨l, r, e⟩ | ⟨r, e⟩ <;> simp [e] at h
    | disj G1 G2 =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases ser_head G1 with ⟨l, r, e⟩ | ⟨r, e⟩ <;> simp [e] at h
    | cond G1 G2 =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and, List.append_assoc] at h
      obtain ⟨c'', hc, hG, hβ⟩ := ih φ β G1 (kDot :: (ser G2 ++ rp :: tl)) (by simpa using h)
      exact ⟨.condL c'' G2, ⟨c'', G2, rfl, hc⟩, by simp [Ctx.plug, hG], by simp [post, hβ]⟩
  | condR l c ih =>
    intro φ β G tl h
    cases G with
    | leaf l' => simp [pre, ser] at h
    | neg G => simp [pre, ser] at h
    | conj G1 G2 =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases ser_head G1 with ⟨x, r, e⟩ | ⟨r, e⟩ <;> simp [e] at h
    | disj G1 G2 =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and] at h
      rcases ser_head G1 with ⟨x, r, e⟩ | ⟨r, e⟩ <;> simp [e] at h
    | cond G1 G2 =>
      simp only [pre, ser, List.cons_append, List.cons.injEq, true_and, List.append_assoc] at h
      obtain ⟨e1, e2⟩ := ser_append_inj l G1 _ _ h
      subst e1
      simp only [List.cons.injEq, true_and] at e2
      obtain ⟨c'', hc, hG, hβ⟩ := ih φ β G2 (rp :: tl) (by simpa using e2)
      exact ⟨.condR l c'', ⟨c'', rfl, hc⟩, by simp [Ctx.plug, hG], by simp [post, hβ]⟩


/-! ### Occurrences: every initial string `α d̲d'` of `F` is the left string of a context -/

theorem split_two {T : Type} (A : List T) (op x : T) (hop : op ≠ x) (Z α rest : List T)
    (h : A ++ op :: Z = α ++ x :: rest) :
    (∃ rest', A = α ++ x :: rest' ∧ rest = rest' ++ op :: Z) ∨
    (∃ α'', α = A ++ op :: α'' ∧ Z = α'' ++ x :: rest) := by
  rcases List.append_eq_append_iff.1 h with ⟨a', ha, hb⟩ | ⟨c', ha, hb⟩
  · right
    cases a' with
    | nil => simp at hb; exact absurd hb.1 hop
    | cons y a'' =>
      simp at hb
      exact ⟨a'', by simp [ha, hb.1], hb.2⟩
  · left
    cases c' with
    | nil => simp at hb; exact absurd hb.1.symm hop
    | cons y c'' =>
      simp at hb
      obtain ⟨rfl, hb2⟩ := hb
      exact ⟨c'', by simp [ha], hb2⟩

theorem occurrence : ∀ (F : Fm L) (α rest : List (Tok L)) (l : L),
    ser F = α ++ lf l :: rest →
    ∃ π : Ctx L, π.plug (.leaf l) = F ∧ pre π = α ∧ post π = rest := by
  intro F
  induction F with
  | leaf x =>
    intro α rest l h
    cases α with
    | nil =>
      simp [ser] at h
      obtain ⟨rfl, rfl⟩ := h
      exact ⟨.hole, rfl, rfl, rfl⟩
    | cons a α' => simp [ser] at h
  | neg F ih =>
    intro α rest l h
    cases α with
    | nil => simp [ser] at h
    | cons a α1 =>
      cases α1 with
      | nil => simp [ser] at h
      | cons b α2 =>
        simp only [ser, List.cons_append, List.cons.injEq] at h
        obtain ⟨rfl, rfl, h⟩ := h
        rcases split_two (ser F) rp (lf l) (by simp) [] α2 rest (by simpa using h) with
          ⟨rest', h1, h2⟩ | ⟨α'', _, h3⟩
        · obtain ⟨π, hπ, hp, hq⟩ := ih α2 rest' l h1
          exact ⟨.negC π, by simp [Ctx.plug, hπ], by simp [pre, hp], by simp [post, hq, h2]⟩
        · simp at h3
  | conj F1 F2 ih1 ih2 =>
    intro α rest l h
    cases α with
    | nil => simp [ser] at h
    | cons a α' =>
      simp only [ser, List.cons_append, List.cons.injEq] at h
      obtain ⟨rfl, h⟩ := h
      rcases split_two (ser F1) kAnd (lf l) (by simp) (ser F2 ++ [rp]) α' rest h with
        ⟨rest', h1, h2⟩ | ⟨α'', h1, h2⟩
      · obtain ⟨π, hπ, hp, hq⟩ := ih1 α' rest' l h1
        exact ⟨.conjL π F2, by simp [Ctx.plug, hπ], by simp [pre, hp], by simp [post, hq, h2]⟩
      · rcases split_two (ser F2) rp (lf l) (by simp) [] α'' rest (by simpa using h2) with
          ⟨rest', h3, h4⟩ | ⟨α3, _, h5⟩
        · obtain ⟨π, hπ, hp, hq⟩ := ih2 α'' rest' l h3
          exact ⟨.conjR F1 π, by simp [Ctx.plug, hπ], by simp [pre, hp, h1], by simp [post, hq, h4]⟩
        · simp at h5
  | disj F1 F2 ih1 ih2 =>
    intro α rest l h
    cases α with
    | nil => simp [ser] at h
    | cons a α' =>
      simp only [ser, List.cons_append, List.cons.injEq] at h
      obtain ⟨rfl, h⟩ := h
      rcases split_two (ser F1) kOr (lf l) (by simp) (ser F2 ++ [rp]) α' rest h with
        ⟨rest', h1, h2⟩ | ⟨α'', h1, h2⟩
      · obtain ⟨π, hπ, hp, hq⟩ := ih1 α' rest' l h1
        exact ⟨.disjL π F2, by simp [Ctx.plug, hπ], by simp [pre, hp], by simp [post, hq, h2]⟩
      · rcases split_two (ser F2) rp (lf l) (by simp) [] α'' rest (by simpa using h2) with
          ⟨rest', h3, h4⟩ | ⟨α3, _, h5⟩
        · obtain ⟨π, hπ, hp, hq⟩ := ih2 α'' rest' l h3
          exact ⟨.disjR F1 π, by simp [Ctx.plug, hπ], by simp [pre, hp, h1], by simp [post, hq, h4]⟩
        · simp at h5
  | cond F1 F2 ih1 ih2 =>
    intro α rest l h
    cases α with
    | nil => simp [ser] at h
    | cons a α1 =>
      cases α1 with
      | nil => simp [ser] at h
      | cons b α' =>
        simp only [ser, List.cons_append, List.cons.injEq] at h
        obtain ⟨rfl, rfl, h⟩ := h
        rcases split_two (ser F1) kDot (lf l) (by simp) (ser F2 ++ [rp]) α' rest h with
          ⟨rest', h1, h2⟩ | ⟨α'', h1, h2⟩
        · obtain ⟨π, hπ, hp, hq⟩ := ih1 α' rest' l h1
          exact ⟨.condL π F2, by simp [Ctx.plug, hπ], by simp [pre, hp], by simp [post, hq, h2]⟩
        · rcases split_two (ser F2) rp (lf l) (by simp) [] α'' rest (by simpa using h2) with
            ⟨rest', h3, h4⟩ | ⟨α3, _, h5⟩
          · obtain ⟨π, hπ, hp, hq⟩ := ih2 α'' rest' l h3
            exact ⟨.condR F1 π, by simp [Ctx.plug, hπ], by simp [pre, hp, h1], by simp [post, hq, h4]⟩
          · simp at h5

/-! ### The literal string definition of Transparency (paper (26)) -/

namespace Sys

/-- **Transparency, literally as in (26)**: for every initial string `α d̲d'` of `F`
(`ser F = α ++ [d̲d'] ++ rest`), every replacement pair `(φ₁, φ₂)` of that clause
(`φ₁ = (d and γ)`, `φ₂ = γ`) and every string `β` such that `α φ₁ β` and `α φ₂ β` are formulas
(`F₁`, `F₂`), `C ⊨ α φ₁ β ⇔ α φ₂ β`. -/
def StrTransp (S : Sys W L) (C : WSet W) (F : Fm L) : Prop :=
  ∀ (α rest : List (Tok L)) (l : L), ser F = α ++ lf l :: rest →
    ∀ φ₁ φ₂, S.lvar l φ₁ φ₂ → ∀ (β : List (Tok L)) (F₁ F₂ : Fm L),
      ser F₁ = α ++ ser φ₁ ++ β → ser F₂ = α ++ ser φ₂ ++ β → S.CEquiv C F₁ F₂

/-- **The two definitions of Transparency coincide**: literal strings/completions
(`StrTransp`) versus contexts/completion contexts (`Transp`). -/
theorem strTransp_iff_transp (S : Sys W L) (C : WSet W) (F : Fm L) :
    S.StrTransp C F ↔ S.Transp C F := by
  constructor
  · intro h π l hπ π' hc φ₁ φ₂ hv
    have hs : ser F = pre π ++ lf l :: post π := by
      rw [← hπ, ser_plug]; simp [ser]
    exact h (pre π) (post π) l hs φ₁ φ₂ hv (post π') (π'.plug φ₁) (π'.plug φ₂)
      (by rw [ser_plug, pre_compl π π' hc]) (by rw [ser_plug, pre_compl π π' hc])
  · intro h α rest l hs φ₁ φ₂ hv β F₁ F₂ h1 h2
    obtain ⟨π, hπ, hpre, hpost⟩ := occurrence F α rest l hs
    subst hpre
    obtain ⟨c1, hc1, hF1, hβ1⟩ := syntactic_lemma_a π φ₁ β F₁ [] (by simpa using h1.symm)
    have e2 : ser (c1.plug φ₂) = ser F₂ := by
      rw [ser_plug, pre_compl π c1 hc1, h2, hβ1]; simp
    have hF2 : c1.plug φ₂ = F₂ := (ser_append_inj _ _ [] [] (by simpa using e2)).1
    subst hF1; subst hF2
    exact h π l hπ c1 hc1 φ₁ φ₂ hv

end Sys

end AntiDyn