case intro.intro
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
⊢ eval (TM2.step tr) (init c v) = halt <$> Code.eval c v
c : Code
v : List ℕ
⊢ eval (TM2.step tr) (init c v) = halt <$> Code.eval c v
obtain ⟨i, h₁, h₂⟩ := tr_init c v
case intro.intro
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x => Γ') Λ' (Option Γ')
⊢ x ∈ eval (TM2.step tr) (init c v) ↔ x ∈ halt <$> Code.eval c v
case intro.intro
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
⊢ eval (TM2.step tr) (init c v) = halt <$> Code.eval c v
refine' Part.ext fun x => _
case intro.intro
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x => Γ') Λ' (Option Γ')
⊢ x ∈ eval (fun a => TM2.step tr a) i ↔ x ∈ halt <$> Code.eval c v
case intro.intro
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x => Γ') Λ' (Option Γ')
⊢ x ∈ eval (TM2.step tr) (init c v) ↔ x ∈ halt <$> Code.eval c v
rw [reaches_eval h₂.to_reflTransGen]
case intro.intro
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x => Γ') Λ' (Option Γ')
⊢ x ∈ eval (fun a => TM2.step tr a) i ↔ ∃ a, a ∈ Code.eval c v ∧ halt a = x
case intro.intro
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x => Γ') Λ' (Option Γ')
⊢ x ∈ eval (fun a => TM2.step tr a) i ↔ x ∈ halt <$> Code.eval c v
simp [-TM2.step]
case intro.intro.refine'_1
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x => Γ') Λ' (Option Γ')
h : x ∈ eval (fun a => TM2.step tr a) i
⊢ ∃ a, a ∈ Code.eval c v ∧ halt a = x

case intro.intro.refine'_2
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x => Γ') Λ' (Option Γ')
⊢ (∃ a, a ∈ Code.eval c v ∧ halt a = x) → x ∈ eval (fun a => TM2.step tr a) i
case intro.intro
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x => Γ') Λ' (Option Γ')
⊢ x ∈ eval (fun a => TM2.step tr a) i ↔ ∃ a, a ∈ Code.eval c v ∧ halt a = x
refine' ⟨fun h => _, _⟩
case intro.intro.refine'_1.intro.intro
c✝ : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c✝ Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c✝ v) i
x : TM2.Cfg (fun x => Γ') Λ' (Option Γ')
h : x ∈ eval (fun a => TM2.step tr a) i
c : Cfg
hc₁ : TrCfg c x
hc₂ : c ∈ eval step (stepNormal c✝ Cont.halt v)
⊢ ∃ a, a ∈ Code.eval c✝ v ∧ halt a = x
case intro.intro.refine'_1
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x => Γ') Λ' (Option Γ')
h : x ∈ eval (fun a => TM2.step tr a) i
⊢ ∃ a, a ∈ Code.eval c v ∧ halt a = x
obtain ⟨c, hc₁, hc₂⟩ := tr_eval_rev tr_respects h₁ h
case intro.intro.refine'_1.intro.intro
c✝ : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c✝ Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c✝ v) i
x : TM2.Cfg (fun x => Γ') Λ' (Option Γ')
h : x ∈ eval (fun a => TM2.step tr a) i
c : Cfg
hc₁ : TrCfg c x
hc₂ : ∃ a, a ∈ Code.eval c✝ v ∧ Cfg.halt a = c
⊢ ∃ a, a ∈ Code.eval c✝ v ∧ halt a = x
case intro.intro.refine'_1.intro.intro
c✝ : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c✝ Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c✝ v) i
x : TM2.Cfg (fun x => Γ') Λ' (Option Γ')
h : x ∈ eval (fun a => TM2.step tr a) i
c : Cfg
hc₁ : TrCfg c x
hc₂ : c ∈ eval step (stepNormal c✝ Cont.halt v)
⊢ ∃ a, a ∈ Code.eval c✝ v ∧ halt a = x
simp [stepNormal_eval] at hc₂
case intro.intro.refine'_1.intro.intro.intro.intro
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x => Γ') Λ' (Option Γ')
h : x ∈ eval (fun a => TM2.step tr a) i
v' : List ℕ
hv : v' ∈ Code.eval c v
hc₁ : TrCfg (Cfg.halt v') x
⊢ ∃ a, a ∈ Code.eval c v ∧ halt a = x
case intro.intro.refine'_1.intro.intro
c✝ : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c✝ Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c✝ v) i
x : TM2.Cfg (fun x => Γ') Λ' (Option Γ')
h : x ∈ eval (fun a => TM2.step tr a) i
c : Cfg
hc₁ : TrCfg c x
hc₂ : ∃ a, a ∈ Code.eval c✝ v ∧ Cfg.halt a = c
⊢ ∃ a, a ∈ Code.eval c✝ v ∧ halt a = x
obtain ⟨v', hv, rfl⟩ := hc₂
no goals
case intro.intro.refine'_1.intro.intro.intro.intro
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x => Γ') Λ' (Option Γ')
h : x ∈ eval (fun a => TM2.step tr a) i
v' : List ℕ
hv : v' ∈ Code.eval c v
hc₁ : TrCfg (Cfg.halt v') x
⊢ ∃ a, a ∈ Code.eval c v ∧ halt a = x
exact ⟨_, hv, hc₁.symm⟩
case intro.intro.refine'_2.intro.intro
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
v' : List ℕ
hv : v' ∈ Code.eval c v
⊢ halt v' ∈ eval (fun a => TM2.step tr a) i
case intro.intro.refine'_2
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x => Γ') Λ' (Option Γ')
⊢ (∃ a, a ∈ Code.eval c v ∧ halt a = x) → x ∈ eval (fun a => TM2.step tr a) i
rintro ⟨v', hv, rfl⟩
case intro.intro.refine'_2.intro.intro
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
v' : List ℕ
hv : v' ∈ Code.eval c v
this : Cfg.halt v' ∈ eval step (stepNormal c Cont.halt v) → ∃ b₂, TrCfg (Cfg.halt v') b₂ ∧ b₂ ∈ eval (TM2.step tr) i
⊢ halt v' ∈ eval (fun a => TM2.step tr a) i
case intro.intro.refine'_2.intro.intro
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
v' : List ℕ
hv : v' ∈ Code.eval c v
⊢ halt v' ∈ eval (fun a => TM2.step tr a) i
have := Turing.tr_eval (b₁ := Cfg.halt v') tr_respects h₁
case intro.intro.refine'_2.intro.intro
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
v' : List ℕ
hv : v' ∈ Code.eval c v
this : v' ∈ Code.eval c v → ∃ b₂, TrCfg (Cfg.halt v') b₂ ∧ b₂ ∈ eval (TM2.step tr) i
⊢ halt v' ∈ eval (fun a => TM2.step tr a) i
case intro.intro.refine'_2.intro.intro
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
v' : List ℕ
hv : v' ∈ Code.eval c v
this : Cfg.halt v' ∈ eval step (stepNormal c Cont.halt v) → ∃ b₂, TrCfg (Cfg.halt v') b₂ ∧ b₂ ∈ eval (TM2.step tr) i
⊢ halt v' ∈ eval (fun a => TM2.step tr a) i
simp [stepNormal_eval, -TM2.step] at this
case intro.intro.refine'_2.intro.intro.intro.intro.refl
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
v' : List ℕ
hv : v' ∈ Code.eval c v
this : v' ∈ Code.eval c v → ∃ b₂, TrCfg (Cfg.halt v') b₂ ∧ b₂ ∈ eval (TM2.step tr) i
h : halt v' ∈ eval (TM2.step tr) i
⊢ halt v' ∈ eval (fun a => TM2.step tr a) i
case intro.intro.refine'_2.intro.intro
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
v' : List ℕ
hv : v' ∈ Code.eval c v
this : v' ∈ Code.eval c v → ∃ b₂, TrCfg (Cfg.halt v') b₂ ∧ b₂ ∈ eval (TM2.step tr) i
⊢ halt v' ∈ eval (fun a => TM2.step tr a) i
obtain ⟨_, ⟨⟩, h⟩ := this hv
no goals
case intro.intro.refine'_2.intro.intro.intro.intro.refl
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
v' : List ℕ
hv : v' ∈ Code.eval c v
this : v' ∈ Code.eval c v → ∃ b₂, TrCfg (Cfg.halt v') b₂ ∧ b₂ ∈ eval (TM2.step tr) i
h : halt v' ∈ eval (TM2.step tr) i
⊢ halt v' ∈ eval (fun a => TM2.step tr a) i
exact h