PdlTestFree.Paths

PdlTestFree
Paths

Imports

module

public import Pdl.Semantics
public import Pdl.Vocab
public import PdlTestFree.Basic

@[expose] public section

Single-program test-free PDL and execution lengths

Write a for the atomic program ·0. For a test-free program α with voc α = {a} the relation of α in any Kripke model M is determined by the relation of a alone: α relates w to v iff there is an a-path from w to v of exactly n steps, for some possible execution length n of α (L α n). This is relate_iff, and box_iff is the resulting characterisation of [α]φ.

This is different from distance in Pdl.Local.Distance, which is the minimal number of atomic steps of an execution; here all possible numbers of steps matter, since [α] quantifies over the endpoints of all of them. The paths also differ from Walk there, which never visits a state twice, whereas the self-loops at m and u in PdlTestFree.NoInterpolation are exactly what lets us reach a state in every number of steps.

section Pathsvariable {S : Type}

NStep R n w v: w Rⁿ v, i.e. there is an R-path of exactly n steps from w to v (states may repeat).

def NStep (R : S → S → Prop) : ℕ → S → S → Prop
  | 0, w, v => w = v
  | n + 1, w, v => ∃ u, R w u ∧ NStep R n u v

variable {R : S → S → Prop}@[simp] lemma NStep_zero {w v : S} : NStep R 0 w v ↔ w = v := Iff.rfl@[simp] lemma NStep_succ {n : ℕ} {w v : S} :
    NStep R (n + 1) w v ↔ ∃ u, R w u ∧ NStep R n u v := Iff.rfllemma NStep_add (i j : ℕ) (w v : S) :
    NStep R (i + j) w v ↔ ∃ u, NStep R i w u ∧ NStep R j u v := byS:TypeR:S → S → Propi:ℕj:ℕw:Sv:S⊢ NStep R (i + j) w v ↔ ∃ u, NStep R i w u ∧ NStep R j u v
  induction i generalizing w with
  | zero =>zeroS:TypeR:S → S → Propj:ℕv:Sw:S⊢ NStep R (0 + j) w v ↔ ∃ u, NStep R 0 w u ∧ NStep R j u v simpAll goals completed! 🐙
  | succ i IH =>succS:TypeR:S → S → Propj:ℕv:Si:ℕIH:∀ (w : S), NStep R (i + j) w v ↔ ∃ u, NStep R i w u ∧ NStep R j u vw:S⊢ NStep R (i + 1 + j) w v ↔ ∃ u, NStep R (i + 1) w u ∧ NStep R j u v
      rw [Nat.succ_addsuccS:TypeR:S → S → Propj:ℕv:Si:ℕIH:∀ (w : S), NStep R (i + j) w v ↔ ∃ u, NStep R i w u ∧ NStep R j u vw:S⊢ NStep R (i + j).succ w v ↔ ∃ u, NStep R (i + 1) w u ∧ NStep R j u v]succS:TypeR:S → S → Propj:ℕv:Si:ℕIH:∀ (w : S), NStep R (i + j) w v ↔ ∃ u, NStep R i w u ∧ NStep R j u vw:S⊢ NStep R (i + j).succ w v ↔ ∃ u, NStep R (i + 1) w u ∧ NStep R j u v
      simp only [NStep_succ]succS:TypeR:S → S → Propj:ℕv:Si:ℕIH:∀ (w : S), NStep R (i + j) w v ↔ ∃ u, NStep R i w u ∧ NStep R j u vw:S⊢ (∃ u, R w u ∧ NStep R (i + j) u v) ↔ ∃ u, (∃ u_1, R w u_1 ∧ NStep R i u_1 u) ∧ NStep R j u v
      constructorsucc.mpS:TypeR:S → S → Propj:ℕv:Si:ℕIH:∀ (w : S), NStep R (i + j) w v ↔ ∃ u, NStep R i w u ∧ NStep R j u vw:S⊢ (∃ u, R w u ∧ NStep R (i + j) u v) → ∃ u, (∃ u_1, R w u_1 ∧ NStep R i u_1 u) ∧ NStep R j u vsucc.mprS:TypeR:S → S → Propj:ℕv:Si:ℕIH:∀ (w : S), NStep R (i + j) w v ↔ ∃ u, NStep R i w u ∧ NStep R j u vw:S⊢ (∃ u, (∃ u_1, R w u_1 ∧ NStep R i u_1 u) ∧ NStep R j u v) → ∃ u, R w u ∧ NStep R (i + j) u v
      ·succ.mpS:TypeR:S → S → Propj:ℕv:Si:ℕIH:∀ (w : S), NStep R (i + j) w v ↔ ∃ u, NStep R i w u ∧ NStep R j u vw:S⊢ (∃ u, R w u ∧ NStep R (i + j) u v) → ∃ u, (∃ u_1, R w u_1 ∧ NStep R i u_1 u) ∧ NStep R j u v rintro ⟨u, hwu, h⟩succ.mpS:TypeR:S → S → Propj:ℕv:Si:ℕIH:∀ (w : S), NStep R (i + j) w v ↔ ∃ u, NStep R i w u ∧ NStep R j u vw:Su:Shwu:R w uh:NStep R (i + j) u v⊢ ∃ u, (∃ u_1, R w u_1 ∧ NStep R i u_1 u) ∧ NStep R j u v
        obtain ⟨x, hux, hxv⟩ := (IH u).mp hsucc.mpS:TypeR:S → S → Propj:ℕv:Si:ℕIH:∀ (w : S), NStep R (i + j) w v ↔ ∃ u, NStep R i w u ∧ NStep R j u vw:Su:Shwu:R w uh:NStep R (i + j) u vx:Shux:NStep R i u xhxv:NStep R j x v⊢ ∃ u, (∃ u_1, R w u_1 ∧ NStep R i u_1 u) ∧ NStep R j u v
        exact ⟨x, ⟨u, hwu, hux⟩, hxv⟩All goals completed! 🐙
      ·succ.mprS:TypeR:S → S → Propj:ℕv:Si:ℕIH:∀ (w : S), NStep R (i + j) w v ↔ ∃ u, NStep R i w u ∧ NStep R j u vw:S⊢ (∃ u, (∃ u_1, R w u_1 ∧ NStep R i u_1 u) ∧ NStep R j u v) → ∃ u, R w u ∧ NStep R (i + j) u v rintro ⟨x, ⟨u, hwu, hux⟩, hxv⟩succ.mprS:TypeR:S → S → Propj:ℕv:Si:ℕIH:∀ (w : S), NStep R (i + j) w v ↔ ∃ u, NStep R i w u ∧ NStep R j u vw:Sx:Shxv:NStep R j x vu:Shwu:R w uhux:NStep R i u x⊢ ∃ u, R w u ∧ NStep R (i + j) u v
        exact ⟨u, hwu, (IH u).mpr ⟨x, hux, hxv⟩⟩All goals completed! 🐙

L α n: n is a possible execution length of α, i.e. α can be executed by exactly n atomic steps. A program may admit several such n, for example a ⋓ (a ;' a) admits 1 and 2, and ∗a admits every n. Tests never occur in test-free programs, so they admit nothing.

def L : Program → ℕ → Prop
  | ·_, n => n = 1
  | α ;' β, n => ∃ i j, L α i ∧ L β j ∧ n = i + j
  | α ⋓ β, n => L α n ∨ L β n
  | ∗α, n => ∃ l : List ℕ, (∀ i ∈ l, L α i) ∧ n = l.sum
  | ?'_, _ => False

variable (M : KripkeModel S)

A test-free program α with voc α = {a} relates w to v iff, for some possible execution length n of α, there is an a-path of exactly n steps from w to v. (For a test this fails: ?'φ relates w to itself iff φ holds at w.)

theorem relate_iff : ∀ (α : Program), α.testFree → α.voc ⊆ {Sum.inr 0} → ∀ (w v : S),
    relate M α w v ↔ ∃ n, L α n ∧ NStep (M.Rel 0) n w v
  | ?'_, hα, _, _, _ =>S:TypeM:KripkeModel Sa✝:Formulahα:(?'a✝).testFreex✝²:(?'a✝).voc ⊆ {Sum.inr 0}x✝¹:Sx✝:S⊢ relate M (?'a✝) x✝¹ x✝ ↔ ∃ n, L (?'a✝) n ∧ NStep (M.Rel 0) n x✝¹ x✝ byS:TypeM:KripkeModel Sa✝:Formulahα:(?'a✝).testFreex✝²:(?'a✝).voc ⊆ {Sum.inr 0}x✝¹:Sx✝:S⊢ relate M (?'a✝) x✝¹ x✝ ↔ ∃ n, L (?'a✝) n ∧ NStep (M.Rel 0) n x✝¹ x✝ simp only [Program.testFree] at hαAll goals completed! 🐙
  | ·c, _, hv, w, v =>S:TypeM:KripkeModel Sc:ℕx✝:(·c).testFreehv:(·c).voc ⊆ {Sum.inr 0}w:Sv:S⊢ relate M (·c) w v ↔ ∃ n, L (·c) n ∧ NStep (M.Rel 0) n w v byS:TypeM:KripkeModel Sc:ℕx✝:(·c).testFreehv:(·c).voc ⊆ {Sum.inr 0}w:Sv:S⊢ relate M (·c) w v ↔ ∃ n, L (·c) n ∧ NStep (M.Rel 0) n w v
      obtain rfl : c = 0 := byS:TypeM:KripkeModel Sc:ℕx✝:(·c).testFreehv:(·c).voc ⊆ {Sum.inr 0}w:Sv:S⊢ c = 0 simpa using hvS:TypeM:KripkeModel Sw:Sv:Sx✝:(·0).testFreehv:(·0).voc ⊆ {Sum.inr 0}⊢ relate M (·0) w v ↔ ∃ n, L (·0) n ∧ NStep (M.Rel 0) n w v
      simp only [relate, L]S:TypeM:KripkeModel Sw:Sv:Sx✝:(·0).testFreehv:(·0).voc ⊆ {Sum.inr 0}⊢ M.Rel 0 w v ↔ ∃ n, n = 1 ∧ NStep (M.Rel 0) n w v
      constructormpS:TypeM:KripkeModel Sw:Sv:Sx✝:(·0).testFreehv:(·0).voc ⊆ {Sum.inr 0}⊢ M.Rel 0 w v → ∃ n, n = 1 ∧ NStep (M.Rel 0) n w vmprS:TypeM:KripkeModel Sw:Sv:Sx✝:(·0).testFreehv:(·0).voc ⊆ {Sum.inr 0}⊢ (∃ n, n = 1 ∧ NStep (M.Rel 0) n w v) → M.Rel 0 w v
      ·mpS:TypeM:KripkeModel Sw:Sv:Sx✝:(·0).testFreehv:(·0).voc ⊆ {Sum.inr 0}⊢ M.Rel 0 w v → ∃ n, n = 1 ∧ NStep (M.Rel 0) n w v intro hmpS:TypeM:KripkeModel Sw:Sv:Sx✝:(·0).testFreehv:(·0).voc ⊆ {Sum.inr 0}h:M.Rel 0 w v⊢ ∃ n, n = 1 ∧ NStep (M.Rel 0) n w v; exact ⟨1, rfl, v, h, rfl⟩All goals completed! 🐙
      ·mprS:TypeM:KripkeModel Sw:Sv:Sx✝:(·0).testFreehv:(·0).voc ⊆ {Sum.inr 0}⊢ (∃ n, n = 1 ∧ NStep (M.Rel 0) n w v) → M.Rel 0 w v rintro ⟨n, rfl, u, h, rfl⟩mprS:TypeM:KripkeModel Sw:Sx✝:(·0).testFreehv:(·0).voc ⊆ {Sum.inr 0}u:Sh:M.Rel 0 w u⊢ M.Rel 0 w u; exact hAll goals completed! 🐙
  | α ;' β, hαβ, hv, w, v =>S:TypeM:KripkeModel Sα:Programβ:Programhαβ:(α;'β).testFreehv:(α;'β).voc ⊆ {Sum.inr 0}w:Sv:S⊢ relate M (α;'β) w v ↔ ∃ n, L (α;'β) n ∧ NStep (M.Rel 0) n w v byS:TypeM:KripkeModel Sα:Programβ:Programhαβ:(α;'β).testFreehv:(α;'β).voc ⊆ {Sum.inr 0}w:Sv:S⊢ relate M (α;'β) w v ↔ ∃ n, L (α;'β) n ∧ NStep (M.Rel 0) n w v
      simp only [Program.testFree] at hαβS:TypeM:KripkeModel Sα:Programβ:Programhαβ:α.testFree ∧ β.testFreehv:(α;'β).voc ⊆ {Sum.inr 0}w:Sv:S⊢ relate M (α;'β) w v ↔ ∃ n, L (α;'β) n ∧ NStep (M.Rel 0) n w v
      simp only [Program.voc, Finset.union_subset_iff] at hvS:TypeM:KripkeModel Sα:Programβ:Programhαβ:α.testFree ∧ β.testFreew:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}⊢ relate M (α;'β) w v ↔ ∃ n, L (α;'β) n ∧ NStep (M.Rel 0) n w v
      obtain ⟨hα, hβ⟩ := hαβS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFree⊢ relate M (α;'β) w v ↔ ∃ n, L (α;'β) n ∧ NStep (M.Rel 0) n w v
      simp only [relate, L]S:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFree⊢ (∃ y, relate M α w y ∧ relate M β y v) ↔ ∃ n, (∃ i j, L α i ∧ L β j ∧ n = i + j) ∧ NStep (M.Rel 0) n w v
      constructormpS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFree⊢ (∃ y, relate M α w y ∧ relate M β y v) → ∃ n, (∃ i j, L α i ∧ L β j ∧ n = i + j) ∧ NStep (M.Rel 0) n w vmprS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFree⊢ (∃ n, (∃ i j, L α i ∧ L β j ∧ n = i + j) ∧ NStep (M.Rel 0) n w v) → ∃ y, relate M α w y ∧ relate M β y v
      ·mpS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFree⊢ (∃ y, relate M α w y ∧ relate M β y v) → ∃ n, (∃ i j, L α i ∧ L β j ∧ n = i + j) ∧ NStep (M.Rel 0) n w v rintro ⟨y, h1, h2⟩mpS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFreey:Sh1:relate M α w yh2:relate M β y v⊢ ∃ n, (∃ i j, L α i ∧ L β j ∧ n = i + j) ∧ NStep (M.Rel 0) n w v
        obtain ⟨i, hi, hwy⟩ := (relate_iff α hα hv.1 w y).mp h1mpS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFreey:Sh1:relate M α w yh2:relate M β y vi:ℕhi:L α ihwy:NStep (M.Rel 0) i w y⊢ ∃ n, (∃ i j, L α i ∧ L β j ∧ n = i + j) ∧ NStep (M.Rel 0) n w v
        obtain ⟨j, hj, hyv⟩ := (relate_iff β hβ hv.2 y v).mp h2mpS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFreey:Sh1:relate M α w yh2:relate M β y vi:ℕhi:L α ihwy:NStep (M.Rel 0) i w yj:ℕhj:L β jhyv:NStep (M.Rel 0) j y v⊢ ∃ n, (∃ i j, L α i ∧ L β j ∧ n = i + j) ∧ NStep (M.Rel 0) n w v
        exact ⟨i + j, ⟨i, j, hi, hj, rfl⟩, (NStep_add i j w v).mpr ⟨y, hwy, hyv⟩⟩All goals completed! 🐙
      ·mprS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFree⊢ (∃ n, (∃ i j, L α i ∧ L β j ∧ n = i + j) ∧ NStep (M.Rel 0) n w v) → ∃ y, relate M α w y ∧ relate M β y v rintro ⟨n, ⟨i, j, hi, hj, rfl⟩, h⟩mprS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFreei:ℕj:ℕhi:L α ihj:L β jh:NStep (M.Rel 0) (i + j) w v⊢ ∃ y, relate M α w y ∧ relate M β y v
        obtain ⟨y, hwy, hyv⟩ := (NStep_add i j w v).mp hmprS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFreei:ℕj:ℕhi:L α ihj:L β jh:NStep (M.Rel 0) (i + j) w vy:Shwy:NStep (M.Rel 0) i w yhyv:NStep (M.Rel 0) j y v⊢ ∃ y, relate M α w y ∧ relate M β y v
        exact ⟨y, (relate_iff α hα hv.1 w y).mpr ⟨i, hi, hwy⟩,
          (relate_iff β hβ hv.2 y v).mpr ⟨j, hj, hyv⟩⟩All goals completed! 🐙
  | α ⋓ β, hαβ, hv, w, v =>S:TypeM:KripkeModel Sα:Programβ:Programhαβ:(α⋓β).testFreehv:(α⋓β).voc ⊆ {Sum.inr 0}w:Sv:S⊢ relate M (α⋓β) w v ↔ ∃ n, L (α⋓β) n ∧ NStep (M.Rel 0) n w v byS:TypeM:KripkeModel Sα:Programβ:Programhαβ:(α⋓β).testFreehv:(α⋓β).voc ⊆ {Sum.inr 0}w:Sv:S⊢ relate M (α⋓β) w v ↔ ∃ n, L (α⋓β) n ∧ NStep (M.Rel 0) n w v
      simp only [Program.testFree] at hαβS:TypeM:KripkeModel Sα:Programβ:Programhαβ:α.testFree ∧ β.testFreehv:(α⋓β).voc ⊆ {Sum.inr 0}w:Sv:S⊢ relate M (α⋓β) w v ↔ ∃ n, L (α⋓β) n ∧ NStep (M.Rel 0) n w v
      simp only [Program.voc, Finset.union_subset_iff] at hvS:TypeM:KripkeModel Sα:Programβ:Programhαβ:α.testFree ∧ β.testFreew:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}⊢ relate M (α⋓β) w v ↔ ∃ n, L (α⋓β) n ∧ NStep (M.Rel 0) n w v
      obtain ⟨hα, hβ⟩ := hαβS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFree⊢ relate M (α⋓β) w v ↔ ∃ n, L (α⋓β) n ∧ NStep (M.Rel 0) n w v
      simp only [relate, L]S:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFree⊢ relate M α w v ∨ relate M β w v ↔ ∃ n, (L α n ∨ L β n) ∧ NStep (M.Rel 0) n w v
      rw [relate_iff α hα hv.1 w v,S:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFree⊢ (∃ n, L α n ∧ NStep (M.Rel 0) n w v) ∨ relate M β w v ↔ ∃ n, (L α n ∨ L β n) ∧ NStep (M.Rel 0) n w v relate_iff β hβ hv.2 w vS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFree⊢ ((∃ n, L α n ∧ NStep (M.Rel 0) n w v) ∨ ∃ n, L β n ∧ NStep (M.Rel 0) n w v) ↔
  ∃ n, (L α n ∨ L β n) ∧ NStep (M.Rel 0) n w v]S:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFree⊢ ((∃ n, L α n ∧ NStep (M.Rel 0) n w v) ∨ ∃ n, L β n ∧ NStep (M.Rel 0) n w v) ↔
  ∃ n, (L α n ∨ L β n) ∧ NStep (M.Rel 0) n w v
      constructormpS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFree⊢ ((∃ n, L α n ∧ NStep (M.Rel 0) n w v) ∨ ∃ n, L β n ∧ NStep (M.Rel 0) n w v) →
  ∃ n, (L α n ∨ L β n) ∧ NStep (M.Rel 0) n w vmprS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFree⊢ (∃ n, (L α n ∨ L β n) ∧ NStep (M.Rel 0) n w v) →
  (∃ n, L α n ∧ NStep (M.Rel 0) n w v) ∨ ∃ n, L β n ∧ NStep (M.Rel 0) n w v
      ·mpS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFree⊢ ((∃ n, L α n ∧ NStep (M.Rel 0) n w v) ∨ ∃ n, L β n ∧ NStep (M.Rel 0) n w v) →
  ∃ n, (L α n ∨ L β n) ∧ NStep (M.Rel 0) n w v rintro (⟨n, h, hn⟩ | ⟨n, h, hn⟩)mp.inlS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFreen:ℕh:L α nhn:NStep (M.Rel 0) n w v⊢ ∃ n, (L α n ∨ L β n) ∧ NStep (M.Rel 0) n w vmp.inrS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFreen:ℕh:L β nhn:NStep (M.Rel 0) n w v⊢ ∃ n, (L α n ∨ L β n) ∧ NStep (M.Rel 0) n w v
        ·mp.inlS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFreen:ℕh:L α nhn:NStep (M.Rel 0) n w v⊢ ∃ n, (L α n ∨ L β n) ∧ NStep (M.Rel 0) n w v exact ⟨n, Or.inl h, hn⟩All goals completed! 🐙
        ·mp.inrS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFreen:ℕh:L β nhn:NStep (M.Rel 0) n w v⊢ ∃ n, (L α n ∨ L β n) ∧ NStep (M.Rel 0) n w v exact ⟨n, Or.inr h, hn⟩All goals completed! 🐙
      ·mprS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFree⊢ (∃ n, (L α n ∨ L β n) ∧ NStep (M.Rel 0) n w v) →
  (∃ n, L α n ∧ NStep (M.Rel 0) n w v) ∨ ∃ n, L β n ∧ NStep (M.Rel 0) n w v rintro ⟨n, h | h, hn⟩mpr.inlS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFreen:ℕhn:NStep (M.Rel 0) n w vh:L α n⊢ (∃ n, L α n ∧ NStep (M.Rel 0) n w v) ∨ ∃ n, L β n ∧ NStep (M.Rel 0) n w vmpr.inrS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFreen:ℕhn:NStep (M.Rel 0) n w vh:L β n⊢ (∃ n, L α n ∧ NStep (M.Rel 0) n w v) ∨ ∃ n, L β n ∧ NStep (M.Rel 0) n w v
        ·mpr.inlS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFreen:ℕhn:NStep (M.Rel 0) n w vh:L α n⊢ (∃ n, L α n ∧ NStep (M.Rel 0) n w v) ∨ ∃ n, L β n ∧ NStep (M.Rel 0) n w v exact Or.inl ⟨n, h, hn⟩All goals completed! 🐙
        ·mpr.inrS:TypeM:KripkeModel Sα:Programβ:Programw:Sv:Shv:α.voc ⊆ {Sum.inr 0} ∧ β.voc ⊆ {Sum.inr 0}hα:α.testFreehβ:β.testFreen:ℕhn:NStep (M.Rel 0) n w vh:L β n⊢ (∃ n, L α n ∧ NStep (M.Rel 0) n w v) ∨ ∃ n, L β n ∧ NStep (M.Rel 0) n w v exact Or.inr ⟨n, h, hn⟩All goals completed! 🐙
  | ∗α, hα, hv, w, v =>S:TypeM:KripkeModel Sα:Programhα:(∗α).testFreehv:(∗α).voc ⊆ {Sum.inr 0}w:Sv:S⊢ relate M (∗α) w v ↔ ∃ n, L (∗α) n ∧ NStep (M.Rel 0) n w v byS:TypeM:KripkeModel Sα:Programhα:(∗α).testFreehv:(∗α).voc ⊆ {Sum.inr 0}w:Sv:S⊢ relate M (∗α) w v ↔ ∃ n, L (∗α) n ∧ NStep (M.Rel 0) n w v
      simp only [Program.testFree] at hαS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:(∗α).voc ⊆ {Sum.inr 0}w:Sv:S⊢ relate M (∗α) w v ↔ ∃ n, L (∗α) n ∧ NStep (M.Rel 0) n w v
      simp only [Program.voc] at hvS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sv:S⊢ relate M (∗α) w v ↔ ∃ n, L (∗α) n ∧ NStep (M.Rel 0) n w v
      simp only [relate, L]S:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sv:S⊢ Relation.ReflTransGen (relate M α) w v ↔ ∃ n, (∃ l, (∀ i ∈ l, L α i) ∧ n = l.sum) ∧ NStep (M.Rel 0) n w v
      constructormpS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sv:S⊢ Relation.ReflTransGen (relate M α) w v → ∃ n, (∃ l, (∀ i ∈ l, L α i) ∧ n = l.sum) ∧ NStep (M.Rel 0) n w vmprS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sv:S⊢ (∃ n, (∃ l, (∀ i ∈ l, L α i) ∧ n = l.sum) ∧ NStep (M.Rel 0) n w v) → Relation.ReflTransGen (relate M α) w v
      ·mpS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sv:S⊢ Relation.ReflTransGen (relate M α) w v → ∃ n, (∃ l, (∀ i ∈ l, L α i) ∧ n = l.sum) ∧ NStep (M.Rel 0) n w v intro hmpS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sv:Sh:Relation.ReflTransGen (relate M α) w v⊢ ∃ n, (∃ l, (∀ i ∈ l, L α i) ∧ n = l.sum) ∧ NStep (M.Rel 0) n w v
        induction h with
        | refl =>mp.reflS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sv:S⊢ ∃ n, (∃ l, (∀ i ∈ l, L α i) ∧ n = l.sum) ∧ NStep (M.Rel 0) n w w exact ⟨0, ⟨[], byS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sv:S⊢ ∀ i ∈ [], L α i simpAll goals completed! 🐙, rfl⟩, rfl⟩
        | tail _ hstep IH =>mp.tailS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sv:Sb✝:Sc✝:Sa✝:Relation.ReflTransGen (relate M α) w b✝hstep:relate M α b✝ c✝IH:∃ n, (∃ l, (∀ i ∈ l, L α i) ∧ n = l.sum) ∧ NStep (M.Rel 0) n w b✝⊢ ∃ n, (∃ l, (∀ i ∈ l, L α i) ∧ n = l.sum) ∧ NStep (M.Rel 0) n w c✝
            obtain ⟨n, ⟨l, hl, rfl⟩, hn⟩ := IHmp.tailS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sv:Sb✝:Sc✝:Sa✝:Relation.ReflTransGen (relate M α) w b✝hstep:relate M α b✝ c✝l:List ℕhl:∀ i ∈ l, L α ihn:NStep (M.Rel 0) l.sum w b✝⊢ ∃ n, (∃ l, (∀ i ∈ l, L α i) ∧ n = l.sum) ∧ NStep (M.Rel 0) n w c✝
            obtain ⟨i, hi, hi'⟩ := (relate_iff α hα hv _ _).mp hstepmp.tailS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sv:Sb✝:Sc✝:Sa✝:Relation.ReflTransGen (relate M α) w b✝hstep:relate M α b✝ c✝l:List ℕhl:∀ i ∈ l, L α ihn:NStep (M.Rel 0) l.sum w b✝i:ℕhi:L α ihi':NStep (M.Rel 0) i b✝ c✝⊢ ∃ n, (∃ l, (∀ i ∈ l, L α i) ∧ n = l.sum) ∧ NStep (M.Rel 0) n w c✝
            refine ⟨l.sum + i, ⟨l ++ [i], ?_, byS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sv:Sb✝:Sc✝:Sa✝:Relation.ReflTransGen (relate M α) w b✝hstep:relate M α b✝ c✝l:List ℕhl:∀ i ∈ l, L α ihn:NStep (M.Rel 0) l.sum w b✝i:ℕhi:L α ihi':NStep (M.Rel 0) i b✝ c✝⊢ l.sum + i = (l ++ [i]).sum simpAll goals completed! 🐙⟩, (NStep_add _ _ _ _).mpr ⟨_, hn, hi'⟩⟩
            intro x hxmp.tailS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sv:Sb✝:Sc✝:Sa✝:Relation.ReflTransGen (relate M α) w b✝hstep:relate M α b✝ c✝l:List ℕhl:∀ i ∈ l, L α ihn:NStep (M.Rel 0) l.sum w b✝i:ℕhi:L α ihi':NStep (M.Rel 0) i b✝ c✝x:ℕhx:x ∈ l ++ [i]⊢ L α x
            simp only [List.mem_append, List.mem_singleton] at hxmp.tailS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sv:Sb✝:Sc✝:Sa✝:Relation.ReflTransGen (relate M α) w b✝hstep:relate M α b✝ c✝l:List ℕhl:∀ i ∈ l, L α ihn:NStep (M.Rel 0) l.sum w b✝i:ℕhi:L α ihi':NStep (M.Rel 0) i b✝ c✝x:ℕhx:x ∈ l ∨ x = i⊢ L α x
            rcases hx with hx | rflmp.tail.inlS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sv:Sb✝:Sc✝:Sa✝:Relation.ReflTransGen (relate M α) w b✝hstep:relate M α b✝ c✝l:List ℕhl:∀ i ∈ l, L α ihn:NStep (M.Rel 0) l.sum w b✝i:ℕhi:L α ihi':NStep (M.Rel 0) i b✝ c✝x:ℕhx:x ∈ l⊢ L α xmp.tail.inrS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sv:Sb✝:Sc✝:Sa✝:Relation.ReflTransGen (relate M α) w b✝hstep:relate M α b✝ c✝l:List ℕhl:∀ i ∈ l, L α ihn:NStep (M.Rel 0) l.sum w b✝x:ℕhi:L α xhi':NStep (M.Rel 0) x b✝ c✝⊢ L α x
            ·mp.tail.inlS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sv:Sb✝:Sc✝:Sa✝:Relation.ReflTransGen (relate M α) w b✝hstep:relate M α b✝ c✝l:List ℕhl:∀ i ∈ l, L α ihn:NStep (M.Rel 0) l.sum w b✝i:ℕhi:L α ihi':NStep (M.Rel 0) i b✝ c✝x:ℕhx:x ∈ l⊢ L α x exact hl x hxAll goals completed! 🐙
            ·mp.tail.inrS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sv:Sb✝:Sc✝:Sa✝:Relation.ReflTransGen (relate M α) w b✝hstep:relate M α b✝ c✝l:List ℕhl:∀ i ∈ l, L α ihn:NStep (M.Rel 0) l.sum w b✝x:ℕhi:L α xhi':NStep (M.Rel 0) x b✝ c✝⊢ L α x exact hiAll goals completed! 🐙
      ·mprS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sv:S⊢ (∃ n, (∃ l, (∀ i ∈ l, L α i) ∧ n = l.sum) ∧ NStep (M.Rel 0) n w v) → Relation.ReflTransGen (relate M α) w v rintro ⟨n, ⟨l, hl, rfl⟩, hn⟩mprS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sv:Sl:List ℕhl:∀ i ∈ l, L α ihn:NStep (M.Rel 0) l.sum w v⊢ Relation.ReflTransGen (relate M α) w v
        induction l generalizing w with
        | nil =>mpr.nilS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}v:Sw:Shl:∀ i ∈ [], L α ihn:NStep (M.Rel 0) [].sum w v⊢ Relation.ReflTransGen (relate M α) w v
            simp only [List.sum_nil, NStep_zero] at hnmpr.nilS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}v:Sw:Shl:∀ i ∈ [], L α ihn:w = v⊢ Relation.ReflTransGen (relate M α) w v
            subst hnmpr.nilS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Shl:∀ i ∈ [], L α i⊢ Relation.ReflTransGen (relate M α) w w
            exact Relation.ReflTransGen.reflAll goals completed! 🐙
        | cons i l IH =>mpr.consS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}v:Si:ℕl:List ℕIH:∀ (w : S), (∀ i ∈ l, L α i) → NStep (M.Rel 0) l.sum w v → Relation.ReflTransGen (relate M α) w vw:Shl:∀ i_1 ∈ i :: l, L α i_1hn:NStep (M.Rel 0) (i :: l).sum w v⊢ Relation.ReflTransGen (relate M α) w v
            rw [List.sum_cons,mpr.consS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}v:Si:ℕl:List ℕIH:∀ (w : S), (∀ i ∈ l, L α i) → NStep (M.Rel 0) l.sum w v → Relation.ReflTransGen (relate M α) w vw:Shl:∀ i_1 ∈ i :: l, L α i_1hn:NStep (M.Rel 0) (i + l.sum) w v⊢ Relation.ReflTransGen (relate M α) w v NStep_addmpr.consS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}v:Si:ℕl:List ℕIH:∀ (w : S), (∀ i ∈ l, L α i) → NStep (M.Rel 0) l.sum w v → Relation.ReflTransGen (relate M α) w vw:Shl:∀ i_1 ∈ i :: l, L α i_1hn:∃ u, NStep (M.Rel 0) i w u ∧ NStep (M.Rel 0) l.sum u v⊢ Relation.ReflTransGen (relate M α) w v] at hnmpr.consS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}v:Si:ℕl:List ℕIH:∀ (w : S), (∀ i ∈ l, L α i) → NStep (M.Rel 0) l.sum w v → Relation.ReflTransGen (relate M α) w vw:Shl:∀ i_1 ∈ i :: l, L α i_1hn:∃ u, NStep (M.Rel 0) i w u ∧ NStep (M.Rel 0) l.sum u v⊢ Relation.ReflTransGen (relate M α) w v
            obtain ⟨u, hwu, huv⟩ := hnmpr.consS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}v:Si:ℕl:List ℕIH:∀ (w : S), (∀ i ∈ l, L α i) → NStep (M.Rel 0) l.sum w v → Relation.ReflTransGen (relate M α) w vw:Shl:∀ i_1 ∈ i :: l, L α i_1u:Shwu:NStep (M.Rel 0) i w uhuv:NStep (M.Rel 0) l.sum u v⊢ Relation.ReflTransGen (relate M α) w v
            refine Relation.ReflTransGen.head ?_
              (IH u (fun x hx => hl x (List.mem_cons_of_mem _ hx)) huv)mpr.consS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}v:Si:ℕl:List ℕIH:∀ (w : S), (∀ i ∈ l, L α i) → NStep (M.Rel 0) l.sum w v → Relation.ReflTransGen (relate M α) w vw:Shl:∀ i_1 ∈ i :: l, L α i_1u:Shwu:NStep (M.Rel 0) i w uhuv:NStep (M.Rel 0) l.sum u v⊢ relate M α w u
            exact (relate_iff α hα hv w u).mpr ⟨i, hl i (List.mem_cons_self ..), hwu⟩All goals completed! 🐙

For a test-free program α with voc α = {a}, the formula [α]φ holds at w iff φ holds at all states reachable from w by an a-path of exactly n steps, for all possible execution lengths n of α.

theorem box_iff (α : Program) (hα : α.testFree) (hv : α.voc ⊆ {Sum.inr 0}) (w : S)
    (φ : Formula) :
    evaluate M w (⌈α⌉φ) ↔ ∀ n, L α n → ∀ v, NStep (M.Rel 0) n w v → evaluate M v φ := byS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sφ:Formula⊢ evaluate M w (⌈α⌉φ) ↔ ∀ (n : ℕ), L α n → ∀ (v : S), NStep (M.Rel 0) n w v → evaluate M v φ
  simp only [evaluate]S:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sφ:Formula⊢ (∀ (v : S), relate M α w v → evaluate M v φ) ↔ ∀ (n : ℕ), L α n → ∀ (v : S), NStep (M.Rel 0) n w v → evaluate M v φ
  constructormpS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sφ:Formula⊢ (∀ (v : S), relate M α w v → evaluate M v φ) → ∀ (n : ℕ), L α n → ∀ (v : S), NStep (M.Rel 0) n w v → evaluate M v φmprS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sφ:Formula⊢ (∀ (n : ℕ), L α n → ∀ (v : S), NStep (M.Rel 0) n w v → evaluate M v φ) → ∀ (v : S), relate M α w v → evaluate M v φ
  ·mpS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sφ:Formula⊢ (∀ (v : S), relate M α w v → evaluate M v φ) → ∀ (n : ℕ), L α n → ∀ (v : S), NStep (M.Rel 0) n w v → evaluate M v φ intro h n hn v hnvmpS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sφ:Formulah:∀ (v : S), relate M α w v → evaluate M v φn:ℕhn:L α nv:Shnv:NStep (M.Rel 0) n w v⊢ evaluate M v φ; exact h v ((relate_iff M α hα hv w v).mpr ⟨n, hn, hnv⟩)All goals completed! 🐙
  ·mprS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sφ:Formula⊢ (∀ (n : ℕ), L α n → ∀ (v : S), NStep (M.Rel 0) n w v → evaluate M v φ) → ∀ (v : S), relate M α w v → evaluate M v φ intro h v hwvmprS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sφ:Formulah:∀ (n : ℕ), L α n → ∀ (v : S), NStep (M.Rel 0) n w v → evaluate M v φv:Shwv:relate M α w v⊢ evaluate M v φ
    obtain ⟨n, hn, hnv⟩ := (relate_iff M α hα hv w v).mp hwvmprS:TypeM:KripkeModel Sα:Programhα:α.testFreehv:α.voc ⊆ {Sum.inr 0}w:Sφ:Formulah:∀ (n : ℕ), L α n → ∀ (v : S), NStep (M.Rel 0) n w v → evaluate M v φv:Shwv:relate M α w vn:ℕhn:L α nhnv:NStep (M.Rel 0) n w v⊢ evaluate M v φ
    exact h n hn v hnvAll goals completed! 🐙

end Paths