Theorem: RegMachine.Prog.Start.eval_eq (RegMachine/Basic.lean)

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
n : ℕ
hn : haltsOn S n
m : ℕ
⊢ eval S n hn = m ↔ evals S n m
Tactic:
suffices ∀ c hc,
  eval.aux S.prog ⟨c,hc⟩ = m ↔
    ∃ regs, c [S.prog]==>* Config.haltedOn m regs
  from this _ _
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
n : ℕ
hn : haltsOn S n
m : ℕ
⊢ ∀ (c : Config (WithIO R) L) (hc : halts S.prog c),
    eval.aux S.prog { config := c, halts := hc } = m ↔ ∃ regs, c [S.prog]==>* Config.haltedOn m regs

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
n : ℕ
hn : haltsOn S n
m : ℕ
⊢ ∀ (c : Config (WithIO R) L) (hc : halts S.prog c),
    eval.aux S.prog { config := c, halts := hc } = m ↔ ∃ regs, c [S.prog]==>* Config.haltedOn m regs
Tactic:
clear hn n
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
⊢ ∀ (c : Config (WithIO R) L) (hc : halts S.prog c),
    eval.aux S.prog { config := c, halts := hc } = m ↔ ∃ regs, c [S.prog]==>* Config.haltedOn m regs

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
⊢ ∀ (c : Config (WithIO R) L) (hc : halts S.prog c),
    eval.aux S.prog { config := c, halts := hc } = m ↔ ∃ regs, c [S.prog]==>* Config.haltedOn m regs
Tactic:
intro c hc
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
hc : halts S.prog c
⊢ eval.aux S.prog { config := c, halts := hc } = m ↔ ∃ regs, c [S.prog]==>* Config.haltedOn m regs

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
hc : halts S.prog c
⊢ eval.aux S.prog { config := c, halts := hc } = m ↔ ∃ regs, c [S.prog]==>* Config.haltedOn m regs
Tactic:
rcases hc with ⟨d,h,hd⟩
State after:
case intro.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
h : c [S.prog]==>* d
hd : Config.is_halted d = true
⊢ eval.aux S.prog { config := c, halts := (_ : ∃ d, (c [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, c [S.prog]==>* Config.haltedOn m regs

State before:
case intro.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
h : c [S.prog]==>* d
hd : Config.is_halted d = true
⊢ eval.aux S.prog { config := c, halts := (_ : ∃ d, (c [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, c [S.prog]==>* Config.haltedOn m regs
Tactic:
induction h using Relation.ReflTransGen.head_induction_on
State after:
case intro.intro.refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
⊢ eval.aux S.prog { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) } = m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs

case intro.intro.head
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
a✝¹ c✝ : Config (WithIO R) L
h'✝ : a✝¹ [S.prog]==> c✝
h✝ : Relation.ReflTransGen (stepsTo S.prog) c✝ d
a✝ :
  eval.aux S.prog { config := c✝, halts := (_ : ∃ d, (c✝ [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, c✝ [S.prog]==>* Config.haltedOn m regs
⊢ eval.aux S.prog { config := a✝¹, halts := (_ : ∃ d, (a✝¹ [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, a✝¹ [S.prog]==>* Config.haltedOn m regs

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
⊢ eval.aux S.prog { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) } = m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs
Tactic:
case refl =>
  unfold eval.aux
  split
  case h_2 h =>
    rw [hd] at h
    contradiction
  next h =>
  clear h
  simp
  constructor <;> intro h
  . use fun r => d.regs (.internal r)
    have : d = Config.haltedOn m (fun r => d.regs (.internal r)) := by
      rcases d with ⟨ip,regs⟩
      simp at hd; cases hd
      simp [Config.haltedOn]
      funext r
      cases r <;> simp at h ⊢
      . exact h
    rw [this] at *
    cases this
    exact .refl
  . rcases h with ⟨regs,h⟩
    have := halt_is_fixpoint _ h hd
    clear h hd
    cases this
    simp
State after:
no goals

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
⊢ eval.aux S.prog { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) } = m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs
Tactic:
unfold eval.aux
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
⊢ (match hc :
        Config.is_halted
          { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config with
      | true =>
        Config.regs { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config
          WithIO.io
      | false =>
        let c' :=
          {
            config :=
              step S.prog
                { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config,
            halts :=
              (_ :
                halts S.prog
                  (step S.prog
                    { config := d,
                        halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config)) };
        let_fun this :=
          (_ :
            { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config.ip = none →
              False);
        eval.aux S.prog c') =
      m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
⊢ (match hc :
        Config.is_halted
          { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config with
      | true =>
        Config.regs { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config
          WithIO.io
      | false =>
        let c' :=
          {
            config :=
              step S.prog
                { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config,
            halts :=
              (_ :
                halts S.prog
                  (step S.prog
                    { config := d,
                        halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config)) };
        let_fun this :=
          (_ :
            { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config.ip = none →
              False);
        eval.aux S.prog c') =
      m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs
Tactic:
split
State after:
case h_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
heq✝ :
  Config.is_halted { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config =
    true
⊢ Config.regs { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config
        WithIO.io =
      m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs

case h_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
heq✝ :
  Config.is_halted { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config =
    false
⊢ (let c' :=
        {
          config :=
            step S.prog
              { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config)) };
      let_fun this :=
        (_ :
          { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config.ip = none →
            False);
      eval.aux S.prog c') =
      m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h :
  Config.is_halted { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config =
    false
⊢ (let c' :=
        {
          config :=
            step S.prog
              { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config)) };
      let_fun this :=
        (_ :
          { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config.ip = none →
            False);
      eval.aux S.prog c') =
      m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs
Tactic:
case h_2 h =>
  rw [hd] at h
  contradiction
State after:
no goals

State before:
case h_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
heq✝ :
  Config.is_halted { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config =
    true
⊢ Config.regs { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config
        WithIO.io =
      m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs
Tactic:
next h =>
clear h
simp
constructor <;> intro h
. use fun r => d.regs (.internal r)
  have : d = Config.haltedOn m (fun r => d.regs (.internal r)) := by
    rcases d with ⟨ip,regs⟩
    simp at hd; cases hd
    simp [Config.haltedOn]
    funext r
    cases r <;> simp at h ⊢
    . exact h
  rw [this] at *
  cases this
  exact .refl
. rcases h with ⟨regs,h⟩
  have := halt_is_fixpoint _ h hd
  clear h hd
  cases this
  simp
State after:
no goals

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h :
  Config.is_halted { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config =
    false
⊢ (let c' :=
        {
          config :=
            step S.prog
              { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config)) };
      let_fun this :=
        (_ :
          { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config.ip = none →
            False);
      eval.aux S.prog c') =
      m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs
Tactic:
rw [hd] at h
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h✝ :
  Config.is_halted { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config =
    false
h : true = false
⊢ (let c' :=
        {
          config :=
            step S.prog
              { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config)) };
      let_fun this :=
        (_ :
          { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config.ip = none →
            False);
      eval.aux S.prog c') =
      m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h✝ :
  Config.is_halted { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config =
    false
h : true = false
⊢ (let c' :=
        {
          config :=
            step S.prog
              { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config)) };
      let_fun this :=
        (_ :
          { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config.ip = none →
            False);
      eval.aux S.prog c') =
      m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs
Tactic:
contradiction
State after:
no goals

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h :
  Config.is_halted { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config =
    true
⊢ Config.regs { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config
        WithIO.io =
      m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs
Tactic:
clear h
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
⊢ Config.regs { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config
        WithIO.io =
      m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
⊢ Config.regs { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config
        WithIO.io =
      m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs
Tactic:
simp
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
⊢ Config.regs d WithIO.io = m ↔ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
⊢ Config.regs d WithIO.io = m ↔ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)
Tactic:
constructor <;> intro h
State after:
case mp
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : Config.regs d WithIO.io = m
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)

case mpr
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)
⊢ Config.regs d WithIO.io = m

State before:
case mp
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : Config.regs d WithIO.io = m
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)

case mpr
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)
⊢ Config.regs d WithIO.io = m
Tactic:
. use fun r => d.regs (.internal r)
  have : d = Config.haltedOn m (fun r => d.regs (.internal r)) := by
    rcases d with ⟨ip,regs⟩
    simp at hd; cases hd
    simp [Config.haltedOn]
    funext r
    cases r <;> simp at h ⊢
    . exact h
  rw [this] at *
  cases this
  exact .refl
State after:
case mpr
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)
⊢ Config.regs d WithIO.io = m

State before:
case mpr
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)
⊢ Config.regs d WithIO.io = m
Tactic:
. rcases h with ⟨regs,h⟩
  have := halt_is_fixpoint _ h hd
  clear h hd
  cases this
  simp
State after:
no goals

State before:
case mp
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : Config.regs d WithIO.io = m
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)
Tactic:
use fun r => d.regs (.internal r)
State after:
case mp
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : Config.regs d WithIO.io = m
⊢ Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m fun r => Config.regs d (WithIO.internal r))

State before:
case mp
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : Config.regs d WithIO.io = m
⊢ Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m fun r => Config.regs d (WithIO.internal r))
Tactic:
have : d = Config.haltedOn m (fun r => d.regs (.internal r)) := by
  rcases d with ⟨ip,regs⟩
  simp at hd; cases hd
  simp [Config.haltedOn]
  funext r
  cases r <;> simp at h ⊢
  . exact h
State after:
case mp
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : Config.regs d WithIO.io = m
this : d = Config.haltedOn m fun r => Config.regs d (WithIO.internal r)
⊢ Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m fun r => Config.regs d (WithIO.internal r))

State before:
case mp
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : Config.regs d WithIO.io = m
this : d = Config.haltedOn m fun r => Config.regs d (WithIO.internal r)
⊢ Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m fun r => Config.regs d (WithIO.internal r))
Tactic:
rw [this] at *
State after:
case mp
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : Config.regs d WithIO.io = m
this :
  (Config.haltedOn m fun r => Config.regs d (WithIO.internal r)) =
    Config.haltedOn m fun r =>
      Config.regs (Config.haltedOn m fun r => Config.regs d (WithIO.internal r)) (WithIO.internal r)
⊢ Relation.ReflTransGen (fun c d => step S.prog c = d) (Config.haltedOn m fun r => Config.regs d (WithIO.internal r))
    (Config.haltedOn m fun r =>
      Config.regs (Config.haltedOn m fun r => Config.regs d (WithIO.internal r)) (WithIO.internal r))

State before:
case mp
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : Config.regs d WithIO.io = m
this :
  (Config.haltedOn m fun r => Config.regs d (WithIO.internal r)) =
    Config.haltedOn m fun r =>
      Config.regs (Config.haltedOn m fun r => Config.regs d (WithIO.internal r)) (WithIO.internal r)
⊢ Relation.ReflTransGen (fun c d => step S.prog c = d) (Config.haltedOn m fun r => Config.regs d (WithIO.internal r))
    (Config.haltedOn m fun r =>
      Config.regs (Config.haltedOn m fun r => Config.regs d (WithIO.internal r)) (WithIO.internal r))
Tactic:
cases this
State after:
case mp.refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : Config.regs d WithIO.io = m
⊢ Relation.ReflTransGen (fun c d => step S.prog c = d) (Config.haltedOn m fun r => Config.regs d (WithIO.internal r))
    (Config.haltedOn m fun r =>
      Config.regs (Config.haltedOn m fun r => Config.regs d (WithIO.internal r)) (WithIO.internal r))

State before:
case mp.refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : Config.regs d WithIO.io = m
⊢ Relation.ReflTransGen (fun c d => step S.prog c = d) (Config.haltedOn m fun r => Config.regs d (WithIO.internal r))
    (Config.haltedOn m fun r =>
      Config.regs (Config.haltedOn m fun r => Config.regs d (WithIO.internal r)) (WithIO.internal r))
Tactic:
exact .refl
State after:
no goals

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : Config.regs d WithIO.io = m
⊢ d = Config.haltedOn m fun r => Config.regs d (WithIO.internal r)
Tactic:
rcases d with ⟨ip,regs⟩
State after:
case mk
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
ip : Option L
regs : WithIO R → ℕ
hd : Config.is_halted { ip := ip, regs := regs } = true
h : Config.regs { ip := ip, regs := regs } WithIO.io = m
⊢ { ip := ip, regs := regs } = Config.haltedOn m fun r => Config.regs { ip := ip, regs := regs } (WithIO.internal r)

State before:
case mk
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
ip : Option L
regs : WithIO R → ℕ
hd : Config.is_halted { ip := ip, regs := regs } = true
h : Config.regs { ip := ip, regs := regs } WithIO.io = m
⊢ { ip := ip, regs := regs } = Config.haltedOn m fun r => Config.regs { ip := ip, regs := regs } (WithIO.internal r)
Tactic:
simp at hd
State after:
case mk
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
ip : Option L
regs : WithIO R → ℕ
h : Config.regs { ip := ip, regs := regs } WithIO.io = m
hd : ip = none
⊢ { ip := ip, regs := regs } = Config.haltedOn m fun r => Config.regs { ip := ip, regs := regs } (WithIO.internal r)

State before:
case mk
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
ip : Option L
regs : WithIO R → ℕ
h : Config.regs { ip := ip, regs := regs } WithIO.io = m
hd : ip = none
⊢ { ip := ip, regs := regs } = Config.haltedOn m fun r => Config.regs { ip := ip, regs := regs } (WithIO.internal r)
Tactic:
cases hd
State after:
case mk.refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : WithIO R → ℕ
h : Config.regs { ip := none, regs := regs } WithIO.io = m
⊢ { ip := none, regs := regs } = Config.haltedOn m fun r => Config.regs { ip := none, regs := regs } (WithIO.internal r)

State before:
case mk.refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : WithIO R → ℕ
h : Config.regs { ip := none, regs := regs } WithIO.io = m
⊢ { ip := none, regs := regs } = Config.haltedOn m fun r => Config.regs { ip := none, regs := regs } (WithIO.internal r)
Tactic:
simp [Config.haltedOn]
State after:
case mk.refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : WithIO R → ℕ
h : Config.regs { ip := none, regs := regs } WithIO.io = m
⊢ regs = fun x =>
    match x with
    | WithIO.io => m
    | WithIO.internal r => regs (WithIO.internal r)

State before:
case mk.refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : WithIO R → ℕ
h : Config.regs { ip := none, regs := regs } WithIO.io = m
⊢ regs = fun x =>
    match x with
    | WithIO.io => m
    | WithIO.internal r => regs (WithIO.internal r)
Tactic:
funext r
State after:
case mk.refl.h
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : WithIO R → ℕ
h : Config.regs { ip := none, regs := regs } WithIO.io = m
r : WithIO R
⊢ regs r =
    match r with
    | WithIO.io => m
    | WithIO.internal r => regs (WithIO.internal r)

State before:
case mk.refl.h
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : WithIO R → ℕ
h : Config.regs { ip := none, regs := regs } WithIO.io = m
r : WithIO R
⊢ regs r =
    match r with
    | WithIO.io => m
    | WithIO.internal r => regs (WithIO.internal r)
Tactic:
cases r <;> simp at h ⊢
State after:
case mk.refl.h.io
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : WithIO R → ℕ
h : regs WithIO.io = m
⊢ regs WithIO.io = m

State before:
case mk.refl.h.io
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : WithIO R → ℕ
h : regs WithIO.io = m
⊢ regs WithIO.io = m
Tactic:
. exact h
State after:
no goals

State before:
case mk.refl.h.io
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : WithIO R → ℕ
h : regs WithIO.io = m
⊢ regs WithIO.io = m
Tactic:
exact h
State after:
no goals

State before:
case mpr
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)
⊢ Config.regs d WithIO.io = m
Tactic:
rcases h with ⟨regs,h⟩
State after:
case mpr.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
regs : R → ℕ
h : Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)
⊢ Config.regs d WithIO.io = m

State before:
case mpr.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
regs : R → ℕ
h : Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)
⊢ Config.regs d WithIO.io = m
Tactic:
have := halt_is_fixpoint _ h hd
State after:
case mpr.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
regs : R → ℕ
h : Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)
this : d = Config.haltedOn m regs
⊢ Config.regs d WithIO.io = m

State before:
case mpr.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
regs : R → ℕ
h : Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)
this : d = Config.haltedOn m regs
⊢ Config.regs d WithIO.io = m
Tactic:
clear h hd
State after:
case mpr.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
regs : R → ℕ
this : d = Config.haltedOn m regs
⊢ Config.regs d WithIO.io = m

State before:
case mpr.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
regs : R → ℕ
this : d = Config.haltedOn m regs
⊢ Config.regs d WithIO.io = m
Tactic:
cases this
State after:
case mpr.intro.refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : R → ℕ
⊢ Config.regs (Config.haltedOn m regs) WithIO.io = m

State before:
case mpr.intro.refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : R → ℕ
⊢ Config.regs (Config.haltedOn m regs) WithIO.io = m
Tactic:
simp
State after:
no goals

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
⊢ eval.aux S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, a [S.prog]==>* Config.haltedOn m regs
Tactic:
clear c
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
⊢ eval.aux S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, a [S.prog]==>* Config.haltedOn m regs

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
⊢ eval.aux S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, a [S.prog]==>* Config.haltedOn m regs
Tactic:
unfold eval.aux
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
⊢ (match hc :
        Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config with
      | true =>
        Config.regs { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config WithIO.io
      | false =>
        let c' :=
          {
            config :=
              step S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config,
            halts :=
              (_ :
                halts S.prog
                  (step S.prog
                    { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) };
        let_fun this :=
          (_ :
            { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config.ip = none →
              False);
        eval.aux S.prog c') =
      m ↔
    ∃ regs, a [S.prog]==>* Config.haltedOn m regs

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
⊢ (match hc :
        Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config with
      | true =>
        Config.regs { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config WithIO.io
      | false =>
        let c' :=
          {
            config :=
              step S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config,
            halts :=
              (_ :
                halts S.prog
                  (step S.prog
                    { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) };
        let_fun this :=
          (_ :
            { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config.ip = none →
              False);
        eval.aux S.prog c') =
      m ↔
    ∃ regs, a [S.prog]==>* Config.haltedOn m regs
Tactic:
constructor <;> intro h
State after:
case mp
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
h :
  (match hc :
      Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config with
    | true =>
      Config.regs { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config WithIO.io
    | false =>
      let c' :=
        {
          config :=
            step S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) };
      let_fun this :=
        (_ :
          { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config.ip = none → False);
      eval.aux S.prog c') =
    m
⊢ ∃ regs, a [S.prog]==>* Config.haltedOn m regs

case mpr
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
h : ∃ regs, a [S.prog]==>* Config.haltedOn m regs
⊢ (match hc :
      Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config with
    | true =>
      Config.regs { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config WithIO.io
    | false =>
      let c' :=
        {
          config :=
            step S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) };
      let_fun this :=
        (_ :
          { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config.ip = none → False);
      eval.aux S.prog c') =
    m

State before:
case mpr
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
h : ∃ regs, a [S.prog]==>* Config.haltedOn m regs
⊢ (match hc :
      Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config with
    | true =>
      Config.regs { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config WithIO.io
    | false =>
      let c' :=
        {
          config :=
            step S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) };
      let_fun this :=
        (_ :
          { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config.ip = none → False);
      eval.aux S.prog c') =
    m
Tactic:
. rcases h with ⟨regs,h⟩
  split
  next ha =>
    simp only at *
    have := halt_is_fixpoint _ h ha
    simp [this]
  next ha =>
    simp
    cases ha_to_b
    apply ih.mpr
    use regs
    have := stepsToTrans_of_not_halts_stepsToTransRefl_halts _ h ?_ ?_
    . rcases Relation.TransGen.head'_iff.mp this with ⟨e,rfl,he⟩
      exact he
    . simp at ha; simp [ha]
    . simp
State after:
no goals

State before:
case mp
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
h :
  (match hc :
      Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config with
    | true =>
      Config.regs { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config WithIO.io
    | false =>
      let c' :=
        {
          config :=
            step S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) };
      let_fun this :=
        (_ :
          { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config.ip = none → False);
      eval.aux S.prog c') =
    m
this : ∃ regs, b [S.prog]==>* Config.haltedOn m regs
⊢ ∃ regs, a [S.prog]==>* Config.haltedOn m regs
Tactic:
rcases this with ⟨regs,h⟩
State after:
case mp.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
h✝ :
  (match hc :
      Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config with
    | true =>
      Config.regs { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config WithIO.io
    | false =>
      let c' :=
        {
          config :=
            step S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) };
      let_fun this :=
        (_ :
          { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config.ip = none → False);
      eval.aux S.prog c') =
    m
regs : R → ℕ
h : b [S.prog]==>* Config.haltedOn m regs
⊢ ∃ regs, a [S.prog]==>* Config.haltedOn m regs

State before:
case mp.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
h✝ :
  (match hc :
      Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config with
    | true =>
      Config.regs { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config WithIO.io
    | false =>
      let c' :=
        {
          config :=
            step S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) };
      let_fun this :=
        (_ :
          { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config.ip = none → False);
      eval.aux S.prog c') =
    m
regs : R → ℕ
h : b [S.prog]==>* Config.haltedOn m regs
⊢ ∃ regs, a [S.prog]==>* Config.haltedOn m regs
Tactic:
use regs
State after:
case mp.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
h✝ :
  (match hc :
      Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config with
    | true =>
      Config.regs { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config WithIO.io
    | false =>
      let c' :=
        {
          config :=
            step S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) };
      let_fun this :=
        (_ :
          { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config.ip = none → False);
      eval.aux S.prog c') =
    m
regs : R → ℕ
h : b [S.prog]==>* Config.haltedOn m regs
⊢ a [S.prog]==>* Config.haltedOn m regs

State before:
case mp.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
h✝ :
  (match hc :
      Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config with
    | true =>
      Config.regs { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config WithIO.io
    | false =>
      let c' :=
        {
          config :=
            step S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) };
      let_fun this :=
        (_ :
          { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config.ip = none → False);
      eval.aux S.prog c') =
    m
regs : R → ℕ
h : b [S.prog]==>* Config.haltedOn m regs
⊢ a [S.prog]==>* Config.haltedOn m regs
Tactic:
exact .head ha_to_b h
State after:
no goals

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
h :
  (match hc :
      Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config with
    | true =>
      Config.regs { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config WithIO.io
    | false =>
      let c' :=
        {
          config :=
            step S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) };
      let_fun this :=
        (_ :
          { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config.ip = none → False);
      eval.aux S.prog c') =
    m
⊢ ∃ regs, b [S.prog]==>* Config.haltedOn m regs
Tactic:
simp at *
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
h :
  (match hc : Config.is_halted a with
    | true => Config.regs a WithIO.io
    | false =>
      eval.aux S.prog
        { config := step S.prog a,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) }) =
    m
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
h :
  (match hc : Config.is_halted a with
    | true => Config.regs a WithIO.io
    | false =>
      eval.aux S.prog
        { config := step S.prog a,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) }) =
    m
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
Tactic:
split at h
State after:
case h_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
heq✝ : Config.is_halted a = true
h : Config.regs a WithIO.io = m
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)

case h_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
heq✝ : Config.is_halted a = false
h :
  eval.aux S.prog
      { config := step S.prog a,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) } =
    m
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)

State before:
case h_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
heq✝ : Config.is_halted a = false
h :
  eval.aux S.prog
      { config := step S.prog a,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) } =
    m
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
Tactic:
. apply ih.mp
  cases ha_to_b
  exact h
State after:
no goals

State before:
case h_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
heq✝ : Config.is_halted a = true
h : Config.regs a WithIO.io = m
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
Tactic:
have : a = b := halt_is_fixpoint _ (.single ha_to_b) ‹_›
State after:
case h_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
heq✝ : Config.is_halted a = true
h : Config.regs a WithIO.io = m
this : a = b
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)

State before:
case h_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
heq✝ : Config.is_halted a = true
h : Config.regs a WithIO.io = m
this : a = b
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
Tactic:
cases this
State after:
case h_1.refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
heq✝ : Config.is_halted a = true
h : Config.regs a WithIO.io = m
ha_to_b : a [S.prog]==> a
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) a d
ih :
  eval.aux S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) a (Config.haltedOn m regs)
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) a (Config.haltedOn m regs)

State before:
case h_1.refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
heq✝ : Config.is_halted a = true
h : Config.regs a WithIO.io = m
ha_to_b : a [S.prog]==> a
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) a d
ih :
  eval.aux S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) a (Config.haltedOn m regs)
this : a = Config.haltedOn m fun x => Config.regs a (WithIO.internal x)
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) a (Config.haltedOn m regs)
Tactic:
rw [this]
State after:
case h_1.refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
heq✝ : Config.is_halted a = true
h : Config.regs a WithIO.io = m
ha_to_b : a [S.prog]==> a
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) a d
ih :
  eval.aux S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) a (Config.haltedOn m regs)
this : a = Config.haltedOn m fun x => Config.regs a (WithIO.internal x)
⊢ ∃ regs,
    Relation.ReflTransGen (fun c d => step S.prog c = d) (Config.haltedOn m fun x => Config.regs a (WithIO.internal x))
      (Config.haltedOn m regs)

State before:
case h_1.refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
heq✝ : Config.is_halted a = true
h : Config.regs a WithIO.io = m
ha_to_b : a [S.prog]==> a
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) a d
ih :
  eval.aux S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) a (Config.haltedOn m regs)
this : a = Config.haltedOn m fun x => Config.regs a (WithIO.internal x)
⊢ ∃ regs,
    Relation.ReflTransGen (fun c d => step S.prog c = d) (Config.haltedOn m fun x => Config.regs a (WithIO.internal x))
      (Config.haltedOn m regs)
Tactic:
refine ⟨_, Relation.ReflTransGen.refl⟩
State after:
no goals

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
heq✝ : Config.is_halted a = true
h : Config.regs a WithIO.io = m
ha_to_b : a [S.prog]==> a
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) a d
ih :
  eval.aux S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) a (Config.haltedOn m regs)
⊢ a = Config.haltedOn m fun x => Config.regs a (WithIO.internal x)
Tactic:
cases a
State after:
case mk
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
ip✝ : Option L
regs✝ : WithIO R → ℕ
heq✝ : Config.is_halted { ip := ip✝, regs := regs✝ } = true
h : Config.regs { ip := ip✝, regs := regs✝ } WithIO.io = m
ha_to_b : { ip := ip✝, regs := regs✝ } [S.prog]==> { ip := ip✝, regs := regs✝ }
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) { ip := ip✝, regs := regs✝ } d
ih :
  eval.aux S.prog
        { config := { ip := ip✝, regs := regs✝ },
          halts := (_ : ∃ d, ({ ip := ip✝, regs := regs✝ } [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) { ip := ip✝, regs := regs✝ } (Config.haltedOn m regs)
⊢ { ip := ip✝, regs := regs✝ } = Config.haltedOn m fun x => Config.regs { ip := ip✝, regs := regs✝ } (WithIO.internal x)

State before:
case mk
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
ip✝ : Option L
regs✝ : WithIO R → ℕ
heq✝ : Config.is_halted { ip := ip✝, regs := regs✝ } = true
h : Config.regs { ip := ip✝, regs := regs✝ } WithIO.io = m
ha_to_b : { ip := ip✝, regs := regs✝ } [S.prog]==> { ip := ip✝, regs := regs✝ }
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) { ip := ip✝, regs := regs✝ } d
ih :
  eval.aux S.prog
        { config := { ip := ip✝, regs := regs✝ },
          halts := (_ : ∃ d, ({ ip := ip✝, regs := regs✝ } [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) { ip := ip✝, regs := regs✝ } (Config.haltedOn m regs)
⊢ { ip := ip✝, regs := regs✝ } = Config.haltedOn m fun x => Config.regs { ip := ip✝, regs := regs✝ } (WithIO.internal x)
Tactic:
simp at *
State after:
case mk
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
ip✝ : Option L
regs✝ : WithIO R → ℕ
h : regs✝ WithIO.io = m
ha_to_b : step S.prog { ip := ip✝, regs := regs✝ } = { ip := ip✝, regs := regs✝ }
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) { ip := ip✝, regs := regs✝ } d
ih :
  eval.aux S.prog
        { config := { ip := ip✝, regs := regs✝ },
          halts := (_ : ∃ d, ({ ip := ip✝, regs := regs✝ } [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) { ip := ip✝, regs := regs✝ } (Config.haltedOn m regs)
heq✝ : ip✝ = none
⊢ { ip := ip✝, regs := regs✝ } = Config.haltedOn m fun x => regs✝ (WithIO.internal x)

State before:
case mk
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
ip✝ : Option L
regs✝ : WithIO R → ℕ
h : regs✝ WithIO.io = m
ha_to_b : step S.prog { ip := ip✝, regs := regs✝ } = { ip := ip✝, regs := regs✝ }
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) { ip := ip✝, regs := regs✝ } d
ih :
  eval.aux S.prog
        { config := { ip := ip✝, regs := regs✝ },
          halts := (_ : ∃ d, ({ ip := ip✝, regs := regs✝ } [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) { ip := ip✝, regs := regs✝ } (Config.haltedOn m regs)
heq✝ : ip✝ = none
⊢ { ip := ip✝, regs := regs✝ } = Config.haltedOn m fun x => regs✝ (WithIO.internal x)
Tactic:
simp [Config.haltedOn, *]
State after:
case mk
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
ip✝ : Option L
regs✝ : WithIO R → ℕ
h : regs✝ WithIO.io = m
ha_to_b : step S.prog { ip := ip✝, regs := regs✝ } = { ip := ip✝, regs := regs✝ }
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) { ip := ip✝, regs := regs✝ } d
ih :
  eval.aux S.prog
        { config := { ip := ip✝, regs := regs✝ },
          halts := (_ : ∃ d, ({ ip := ip✝, regs := regs✝ } [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) { ip := ip✝, regs := regs✝ } (Config.haltedOn m regs)
heq✝ : ip✝ = none
⊢ regs✝ = fun x =>
    match x with
    | WithIO.io => m
    | WithIO.internal r => regs✝ (WithIO.internal r)

State before:
case mk
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
ip✝ : Option L
regs✝ : WithIO R → ℕ
h : regs✝ WithIO.io = m
ha_to_b : step S.prog { ip := ip✝, regs := regs✝ } = { ip := ip✝, regs := regs✝ }
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) { ip := ip✝, regs := regs✝ } d
ih :
  eval.aux S.prog
        { config := { ip := ip✝, regs := regs✝ },
          halts := (_ : ∃ d, ({ ip := ip✝, regs := regs✝ } [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) { ip := ip✝, regs := regs✝ } (Config.haltedOn m regs)
heq✝ : ip✝ = none
⊢ regs✝ = fun x =>
    match x with
    | WithIO.io => m
    | WithIO.internal r => regs✝ (WithIO.internal r)
Tactic:
funext x
State after:
case mk.h
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
ip✝ : Option L
regs✝ : WithIO R → ℕ
h : regs✝ WithIO.io = m
ha_to_b : step S.prog { ip := ip✝, regs := regs✝ } = { ip := ip✝, regs := regs✝ }
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) { ip := ip✝, regs := regs✝ } d
ih :
  eval.aux S.prog
        { config := { ip := ip✝, regs := regs✝ },
          halts := (_ : ∃ d, ({ ip := ip✝, regs := regs✝ } [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) { ip := ip✝, regs := regs✝ } (Config.haltedOn m regs)
heq✝ : ip✝ = none
x : WithIO R
⊢ regs✝ x =
    match x with
    | WithIO.io => m
    | WithIO.internal r => regs✝ (WithIO.internal r)

State before:
case mk.h
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
ip✝ : Option L
regs✝ : WithIO R → ℕ
h : regs✝ WithIO.io = m
ha_to_b : step S.prog { ip := ip✝, regs := regs✝ } = { ip := ip✝, regs := regs✝ }
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) { ip := ip✝, regs := regs✝ } d
ih :
  eval.aux S.prog
        { config := { ip := ip✝, regs := regs✝ },
          halts := (_ : ∃ d, ({ ip := ip✝, regs := regs✝ } [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) { ip := ip✝, regs := regs✝ } (Config.haltedOn m regs)
heq✝ : ip✝ = none
x : WithIO R
⊢ regs✝ x =
    match x with
    | WithIO.io => m
    | WithIO.internal r => regs✝ (WithIO.internal r)
Tactic:
split <;> simp [*]
State after:
no goals

State before:
case h_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
heq✝ : Config.is_halted a = false
h :
  eval.aux S.prog
      { config := step S.prog a,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) } =
    m
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
Tactic:
apply ih.mp
State after:
case h_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
heq✝ : Config.is_halted a = false
h :
  eval.aux S.prog
      { config := step S.prog a,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) } =
    m
⊢ eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m

State before:
case h_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
heq✝ : Config.is_halted a = false
h :
  eval.aux S.prog
      { config := step S.prog a,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) } =
    m
⊢ eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m
Tactic:
cases ha_to_b
State after:
case h_2.refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
heq✝ : Config.is_halted a = false
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) (step S.prog a) (Config.haltedOn m regs)
h :
  eval.aux S.prog
      { config := step S.prog a,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) } =
    m
⊢ eval.aux S.prog
      { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
    m

State before:
case h_2.refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
heq✝ : Config.is_halted a = false
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) (step S.prog a) (Config.haltedOn m regs)
h :
  eval.aux S.prog
      { config := step S.prog a,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) } =
    m
⊢ eval.aux S.prog
      { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
    m
Tactic:
exact h
State after:
no goals

State before:
case mpr
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
h : ∃ regs, a [S.prog]==>* Config.haltedOn m regs
⊢ (match hc :
      Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config with
    | true =>
      Config.regs { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config WithIO.io
    | false =>
      let c' :=
        {
          config :=
            step S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) };
      let_fun this :=
        (_ :
          { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config.ip = none → False);
      eval.aux S.prog c') =
    m
Tactic:
rcases h with ⟨regs,h⟩
State after:
case mpr.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
⊢ (match hc :
      Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config with
    | true =>
      Config.regs { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config WithIO.io
    | false =>
      let c' :=
        {
          config :=
            step S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) };
      let_fun this :=
        (_ :
          { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config.ip = none → False);
      eval.aux S.prog c') =
    m

State before:
case mpr.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
⊢ (match hc :
      Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config with
    | true =>
      Config.regs { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config WithIO.io
    | false =>
      let c' :=
        {
          config :=
            step S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) };
      let_fun this :=
        (_ :
          { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config.ip = none → False);
      eval.aux S.prog c') =
    m
Tactic:
split
State after:
case mpr.intro.h_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
heq✝ :
  Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = true
⊢ Config.regs { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config WithIO.io = m

case mpr.intro.h_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
heq✝ :
  Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ (let c' :=
      {
        config :=
          step S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) };
    let_fun this :=
      (_ :
        { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config.ip = none → False);
    eval.aux S.prog c') =
    m

State before:
case mpr.intro.h_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
heq✝ :
  Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = true
⊢ Config.regs { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config WithIO.io = m

case mpr.intro.h_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
heq✝ :
  Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ (let c' :=
      {
        config :=
          step S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) };
    let_fun this :=
      (_ :
        { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config.ip = none → False);
    eval.aux S.prog c') =
    m
Tactic:
next ha =>
  simp only at *
  have := halt_is_fixpoint _ h ha
  simp [this]
State after:
case mpr.intro.h_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
heq✝ :
  Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ (let c' :=
      {
        config :=
          step S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) };
    let_fun this :=
      (_ :
        { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config.ip = none → False);
    eval.aux S.prog c') =
    m

State before:
case mpr.intro.h_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
heq✝ :
  Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ (let c' :=
      {
        config :=
          step S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) };
    let_fun this :=
      (_ :
        { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config.ip = none → False);
    eval.aux S.prog c') =
    m
Tactic:
next ha =>
  simp
  cases ha_to_b
  apply ih.mpr
  use regs
  have := stepsToTrans_of_not_halts_stepsToTransRefl_halts _ h ?_ ?_
  . rcases Relation.TransGen.head'_iff.mp this with ⟨e,rfl,he⟩
    exact he
  . simp at ha; simp [ha]
  . simp
State after:
no goals

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = true
⊢ Config.regs { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config WithIO.io = m
Tactic:
simp only at *
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted a = true
⊢ Config.regs a WithIO.io = m

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted a = true
⊢ Config.regs a WithIO.io = m
Tactic:
have := halt_is_fixpoint _ h ha
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted a = true
this : a = Config.haltedOn m regs
⊢ Config.regs a WithIO.io = m

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted a = true
this : a = Config.haltedOn m regs
⊢ Config.regs a WithIO.io = m
Tactic:
simp [this]
State after:
no goals

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ (let c' :=
      {
        config :=
          step S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) };
    let_fun this :=
      (_ :
        { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config.ip = none → False);
    eval.aux S.prog c') =
    m
Tactic:
simp
State after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ eval.aux S.prog
      { config := step S.prog a,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) } =
    m

State before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ eval.aux S.prog
      { config := step S.prog a,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) } =
    m
Tactic:
cases ha_to_b
State after:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ eval.aux S.prog
      { config := step S.prog a,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) } =
    m

State before:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ eval.aux S.prog
      { config := step S.prog a,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) } =
    m
Tactic:
apply ih.mpr
State after:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs

State before:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
Tactic:
use regs
State after:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ step S.prog a [S.prog]==>* Config.haltedOn m regs

State before:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ step S.prog a [S.prog]==>* Config.haltedOn m regs
Tactic:
have := stepsToTrans_of_not_halts_stepsToTransRefl_halts _ h ?_ ?_
State after:
case refl.refine_3
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
this : a [S.prog]==>+ Config.haltedOn m regs
⊢ step S.prog a [S.prog]==>* Config.haltedOn m regs

case refl.refine_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ ¬Config.is_halted a = true

case refl.refine_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ Config.is_halted (Config.haltedOn m regs) = true

State before:
case refl.refine_3
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
this : a [S.prog]==>+ Config.haltedOn m regs
⊢ step S.prog a [S.prog]==>* Config.haltedOn m regs

case refl.refine_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ ¬Config.is_halted a = true

case refl.refine_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ Config.is_halted (Config.haltedOn m regs) = true
Tactic:
. rcases Relation.TransGen.head'_iff.mp this with ⟨e,rfl,he⟩
  exact he
State after:
case refl.refine_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ ¬Config.is_halted a = true

case refl.refine_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ Config.is_halted (Config.haltedOn m regs) = true

State before:
case refl.refine_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ ¬Config.is_halted a = true

case refl.refine_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ Config.is_halted (Config.haltedOn m regs) = true
Tactic:
. simp at ha; simp [ha]
State after:
case refl.refine_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ Config.is_halted (Config.haltedOn m regs) = true

State before:
case refl.refine_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ Config.is_halted (Config.haltedOn m regs) = true
Tactic:
. simp
State after:
no goals

State before:
case refl.refine_3
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
this : a [S.prog]==>+ Config.haltedOn m regs
⊢ step S.prog a [S.prog]==>* Config.haltedOn m regs
Tactic:
rcases Relation.TransGen.head'_iff.mp this with ⟨e,rfl,he⟩
State after:
case refl.refine_3.intro.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
this : a [S.prog]==>+ Config.haltedOn m regs
he : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) (Config.haltedOn m regs)
⊢ step S.prog a [S.prog]==>* Config.haltedOn m regs

State before:
case refl.refine_3.intro.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
this : a [S.prog]==>+ Config.haltedOn m regs
he : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) (Config.haltedOn m regs)
⊢ step S.prog a [S.prog]==>* Config.haltedOn m regs
Tactic:
exact he
State after:
no goals

State before:
case refl.refine_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ ¬Config.is_halted a = true
Tactic:
simp at ha
State after:
case refl.refine_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted a = false
⊢ ¬Config.is_halted a = true

State before:
case refl.refine_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted a = false
⊢ ¬Config.is_halted a = true
Tactic:
simp [ha]
State after:
no goals

State before:
case refl.refine_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ Config.is_halted (Config.haltedOn m regs) = true
Tactic:
simp
State after:
no goals