Theorem: RegMachine.Prog.Start.eval_eq
Proof 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
Proof 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