Cryptids.Riemann104

Cryptids
Riemann104

Imports

/-
Copyright (c) 2026 Google LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
-/
module

public import Cryptids.Semantics.Riemann120.Backend

Riemann104

104-state Turing machine halting-equivalent to the 120-state Riemann machine.

@[expose] public sectionset_option linter.style.setOption falseset_option maxRecDepth 200000namespace ConjectureMachines.Riemann104open Turing StateTransition
                  120-state Riemann Hypothesis reference machine (riemann_120, Shunia 2026).
abbrev reference : BundledMachine 2 := Machines.riemann120.bundle
                  104-state Riemann Hypothesis candidate machine (riemann_104).
abbrev candidate : BundledMachine 2 := Machines.riemann104.bundle
                  Alias for Machines.riemann120.
abbrev refM : Machine 120 2 := Machines.riemann120
                  Alias for Machines.riemann104.
abbrev candM : Machine 104 2 := Machines.riemann104theorem candidate_fewer_states : candidate.states < reference.states := by⊢ candidate.states < reference.states
  decideAll goals completed! 🐙sectionopen Turing StateTransition ConjectureMachinesopen ConjectureMachines.Riemann120open ConjectureMachines.Riemann120.Layer2def embed104To121 (q : Fin 104) : Fin 121 :=
  if q.val < 1 then ⟨11, byq:Fin 104⊢ 11 < 121 omegaAll goals completed! 🐙⟩
  else if q.val < 2 then ⟨q.val + 3, byq:Fin 104⊢ ↑q + 3 < 121 omegaAll goals completed! 🐙⟩
  else if q.val < 7 then ⟨q.val + 4, byq:Fin 104⊢ ↑q + 4 < 121 omegaAll goals completed! 🐙⟩
  else if q.val < 17 then ⟨q.val + 5, byq:Fin 104⊢ ↑q + 5 < 121 omegaAll goals completed! 🐙⟩
  else if q.val < 19 then ⟨q.val + 6, byq:Fin 104⊢ ↑q + 6 < 121 omegaAll goals completed! 🐙⟩
  else if q.val < 20 then ⟨q.val + 8, byq:Fin 104⊢ ↑q + 8 < 121 omegaAll goals completed! 🐙⟩
  else if q.val < 28 then ⟨q.val + 9, byq:Fin 104⊢ ↑q + 9 < 121 omegaAll goals completed! 🐙⟩
  else if q.val < 75 then ⟨q.val + 10, byq:Fin 104⊢ ↑q + 10 < 121 omegaAll goals completed! 🐙⟩
  else if q.val < 79 then ⟨q.val + 11, byq:Fin 104⊢ ↑q + 11 < 121 omegaAll goals completed! 🐙⟩
  else if q.val < 83 then ⟨q.val + 13, byq:Fin 104⊢ ↑q + 13 < 121 omegaAll goals completed! 🐙⟩
  else if q.val < 92 then ⟨q.val + 15, byq:Fin 104⊢ ↑q + 15 < 121 omegaAll goals completed! 🐙⟩
  else if q.val < 96 then ⟨q.val + 16, byq:Fin 104⊢ ↑q + 16 < 121 omegaAll goals completed! 🐙⟩
  else ⟨q.val + 17, byq:Fin 104⊢ ↑q + 17 < 121 omegaAll goals completed! 🐙⟩def embedCfg (c : Cfg 104 2) : Cfg 121 2 :=
  ⟨embed104To121 c.state, c.tape⟩set_option maxHeartbeats 400000 in
-- Finite state-table decision procedure.
theorem embed_transition_eq (q : Fin 104) (a : Fin 2) :
    edited121.transition (embed104To121 q) a =
      (candM.transition q a).map fun t => (t.1, t.2.1, embed104To121 t.2.2) := byq:Fin 104a:Fin 2⊢ edited121.transition (embed104To121 q) a = Option.map (fun t ↦ (t.1, t.2.1, embed104To121 t.2.2)) (candM.transition q a)
  revert q a⊢ ∀ (q : Fin 104) (a : Fin 2),
  edited121.transition (embed104To121 q) a =
    Option.map (fun t ↦ (t.1, t.2.1, embed104To121 t.2.2)) (candM.transition q a); decideAll goals completed! 🐙theorem embedCfg_step (c : Cfg 104 2) :
    Option.map embedCfg (step candM c) = step edited121 (embedCfg c) := byc:Cfg 104 2⊢ Option.map embedCfg (step candM c) = step edited121 (embedCfg c)
  obtain ⟨q, t⟩ := cq:Fin 104t:Tape (Fin 2)⊢ Option.map embedCfg (step candM { state := q, tape := t }) = step edited121 (embedCfg { state := q, tape := t })
  dsimp only [step, embedCfg]q:Fin 104t:Tape (Fin 2)⊢ Option.map embedCfg
    (Option.map (fun x ↦ { state := x.2.2, tape := Tape.move x.2.1 (Tape.write x.1 t) }) (candM.transition q t.head)) =
  Option.map (fun x ↦ { state := x.2.2, tape := Tape.move x.2.1 (Tape.write x.1 t) })
    (edited121.transition (embed104To121 q) t.head)
  rw [embed_transition_eq q t.head,q:Fin 104t:Tape (Fin 2)⊢ Option.map embedCfg
    (Option.map (fun x ↦ { state := x.2.2, tape := Tape.move x.2.1 (Tape.write x.1 t) }) (candM.transition q t.head)) =
  Option.map (fun x ↦ { state := x.2.2, tape := Tape.move x.2.1 (Tape.write x.1 t) })
    (Option.map (fun t ↦ (t.1, t.2.1, embed104To121 t.2.2)) (candM.transition q t.head)) Option.map_map,q:Fin 104t:Tape (Fin 2)⊢ Option.map (embedCfg ∘ fun x ↦ { state := x.2.2, tape := Tape.move x.2.1 (Tape.write x.1 t) })
    (candM.transition q t.head) =
  Option.map (fun x ↦ { state := x.2.2, tape := Tape.move x.2.1 (Tape.write x.1 t) })
    (Option.map (fun t ↦ (t.1, t.2.1, embed104To121 t.2.2)) (candM.transition q t.head)) Option.map_mapq:Fin 104t:Tape (Fin 2)⊢ Option.map (embedCfg ∘ fun x ↦ { state := x.2.2, tape := Tape.move x.2.1 (Tape.write x.1 t) })
    (candM.transition q t.head) =
  Option.map
    ((fun x ↦ { state := x.2.2, tape := Tape.move x.2.1 (Tape.write x.1 t) }) ∘ fun t ↦
      (t.1, t.2.1, embed104To121 t.2.2))
    (candM.transition q t.head)]q:Fin 104t:Tape (Fin 2)⊢ Option.map (embedCfg ∘ fun x ↦ { state := x.2.2, tape := Tape.move x.2.1 (Tape.write x.1 t) })
    (candM.transition q t.head) =
  Option.map
    ((fun x ↦ { state := x.2.2, tape := Tape.move x.2.1 (Tape.write x.1 t) }) ∘ fun t ↦
      (t.1, t.2.1, embed104To121 t.2.2))
    (candM.transition q t.head)
  rflAll goals completed! 🐙theorem halts_candidate_iff_halts_edited121 :
    Halts candidate ↔ (StateTransition.eval (step edited121) ⟨11, default⟩).Dom := by⊢ candidate.Halts ↔ (eval (step edited121) { state := 11, tape := default }).Dom
  have hrel : Respects (step candM) (step edited121)
      (fun c₁ c₂ => c₂ = embedCfg c₁) := by
    intro c₁ c₂ hc₂c₁:Cfg 104 2c₂:Cfg 121 2hc₂:c₂ = embedCfg c₁⊢ match step candM c₁ with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ c₂ = embedCfg c₁) b₁ b₂ ∧ Reaches₁ (step edited121) c₂ b₂
| none => step edited121 c₂ = none
    subst hc₂c₁:Cfg 104 2⊢ match step candM c₁ with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ c₂ = embedCfg c₁) b₁ b₂ ∧ Reaches₁ (step edited121) (embedCfg c₁) b₂
| none => step edited121 (embedCfg c₁) = none
    have hst := embedCfg_step c₁c₁:Cfg 104 2hst:Option.map embedCfg (step candM c₁) = step edited121 (embedCfg c₁)⊢ match step candM c₁ with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ c₂ = embedCfg c₁) b₁ b₂ ∧ Reaches₁ (step edited121) (embedCfg c₁) b₂
| none => step edited121 (embedCfg c₁) = none
    rcases hs : step candM c₁ with _ | c₁'nonec₁:Cfg 104 2hst:Option.map embedCfg (step candM c₁) = step edited121 (embedCfg c₁)hs:step candM c₁ = none⊢ match none with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ c₂ = embedCfg c₁) b₁ b₂ ∧ Reaches₁ (step edited121) (embedCfg c₁) b₂
| none => step edited121 (embedCfg c₁) = nonesomec₁:Cfg 104 2hst:Option.map embedCfg (step candM c₁) = step edited121 (embedCfg c₁)c₁':Cfg 104 2hs:step candM c₁ = some c₁'⊢ match some c₁' with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ c₂ = embedCfg c₁) b₁ b₂ ∧ Reaches₁ (step edited121) (embedCfg c₁) b₂
| none => step edited121 (embedCfg c₁) = none
    ·nonec₁:Cfg 104 2hst:Option.map embedCfg (step candM c₁) = step edited121 (embedCfg c₁)hs:step candM c₁ = none⊢ match none with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ c₂ = embedCfg c₁) b₁ b₂ ∧ Reaches₁ (step edited121) (embedCfg c₁) b₂
| none => step edited121 (embedCfg c₁) = none dsimp onlynonec₁:Cfg 104 2hst:Option.map embedCfg (step candM c₁) = step edited121 (embedCfg c₁)hs:step candM c₁ = none⊢ step edited121 (embedCfg c₁) = none
      rw [hsnonec₁:Cfg 104 2hst:Option.map embedCfg none = step edited121 (embedCfg c₁)hs:step candM c₁ = none⊢ step edited121 (embedCfg c₁) = none] at hstnonec₁:Cfg 104 2hst:Option.map embedCfg none = step edited121 (embedCfg c₁)hs:step candM c₁ = none⊢ step edited121 (embedCfg c₁) = none; simp only [Option.map_none] at hstnonec₁:Cfg 104 2hst:none = step edited121 (embedCfg c₁)hs:step candM c₁ = none⊢ step edited121 (embedCfg c₁) = none; exact hst.symmAll goals completed! 🐙
    ·somec₁:Cfg 104 2hst:Option.map embedCfg (step candM c₁) = step edited121 (embedCfg c₁)c₁':Cfg 104 2hs:step candM c₁ = some c₁'⊢ match some c₁' with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ c₂ = embedCfg c₁) b₁ b₂ ∧ Reaches₁ (step edited121) (embedCfg c₁) b₂
| none => step edited121 (embedCfg c₁) = none dsimp onlysomec₁:Cfg 104 2hst:Option.map embedCfg (step candM c₁) = step edited121 (embedCfg c₁)c₁':Cfg 104 2hs:step candM c₁ = some c₁'⊢ ∃ b₂, b₂ = embedCfg c₁' ∧ Reaches₁ (step edited121) (embedCfg c₁) b₂
      rw [hssomec₁:Cfg 104 2c₁':Cfg 104 2hst:Option.map embedCfg (some c₁') = step edited121 (embedCfg c₁)hs:step candM c₁ = some c₁'⊢ ∃ b₂, b₂ = embedCfg c₁' ∧ Reaches₁ (step edited121) (embedCfg c₁) b₂] at hstsomec₁:Cfg 104 2c₁':Cfg 104 2hst:Option.map embedCfg (some c₁') = step edited121 (embedCfg c₁)hs:step candM c₁ = some c₁'⊢ ∃ b₂, b₂ = embedCfg c₁' ∧ Reaches₁ (step edited121) (embedCfg c₁) b₂; simp only [Option.map_some] at hstsomec₁:Cfg 104 2c₁':Cfg 104 2hst:some (embedCfg c₁') = step edited121 (embedCfg c₁)hs:step candM c₁ = some c₁'⊢ ∃ b₂, b₂ = embedCfg c₁' ∧ Reaches₁ (step edited121) (embedCfg c₁) b₂
      exact ⟨embedCfg c₁', rfl, Relation.TransGen.single hst.symm⟩hrel:Respects (step candM) (step edited121) fun c₁ c₂ ↦ c₂ = embedCfg c₁⊢ candidate.Halts ↔ (eval (step edited121) { state := 11, tape := default }).Dom
  exact (StateTransition.tr_eval_dom hrel rfl).symmAll goals completed! 🐙def inCompare (bits : List (Fin 2)) : Bool :=
  bits == [1, 1, 1, 1, 1] ||
  bits == [1, 1, 1, 1, 1, 0, 1] ||
  bits == [1, 1, 1, 1, 1, 0, 1, 0, 1] ||
  bits == [1, 1, 1, 1, 1, 0, 1, 1]def inCompareStepOk (bits : List (Fin 2)) : Bool :=
  match evalStackOf false bits with
  | .halt => true
  | .jump s' => if inCompare s' then inCompare bits else true
  | .inc r s_succ => if inCompare s_succ then inCompare bits && decide (r ≠ 1) else true
  | .decnz r s_succ s_fail =>
    (if inCompare s_succ then inCompare bits && decide (r ≠ 1) else true) &&
    (if inCompare s_fail then inCompare bits || decide (r = 1) else true)set_option maxHeartbeats 800000 in
-- Finite state-table decision procedure.
theorem inCompareStepOk_all :
    ∀ bits ∈ allValidStacks, inCompareStepOk bits = true := by⊢ ∀ bits ∈ allValidStacks, inCompareStepOk bits = true
  decideAll goals completed! 🐙theorem getD_one_set_ne : ∀ (regs : List ℕ) (r : ℕ), r ≠ 1 → ∀ (v : ℕ),
    (regs.set r v).getD 1 0 = regs.getD 1 0
  | [], _, _, _ => rfl
  | _ :: [], r, _, _ =>head✝:ℕr:ℕx✝¹:r ≠ 1x✝:ℕ⊢ ([head✝].set r x✝).getD 1 0 = [head✝].getD 1 0 byhead✝:ℕr:ℕx✝¹:r ≠ 1x✝:ℕ⊢ ([head✝].set r x✝).getD 1 0 = [head✝].getD 1 0 cases rzerohead✝:ℕx✝¹:ℕx✝:0 ≠ 1⊢ ([head✝].set 0 x✝¹).getD 1 0 = [head✝].getD 1 0succhead✝:ℕx✝¹:ℕn✝:ℕx✝:n✝ + 1 ≠ 1⊢ ([head✝].set (n✝ + 1) x✝¹).getD 1 0 = [head✝].getD 1 0 <;>zerohead✝:ℕx✝¹:ℕx✝:0 ≠ 1⊢ ([head✝].set 0 x✝¹).getD 1 0 = [head✝].getD 1 0succhead✝:ℕx✝¹:ℕn✝:ℕx✝:n✝ + 1 ≠ 1⊢ ([head✝].set (n✝ + 1) x✝¹).getD 1 0 = [head✝].getD 1 0 rflAll goals completed! 🐙
  | _ :: _ :: _, 0, _, _ => rfl
  | _ :: _ :: _, 1, hr, _ => absurd rfl hr
  | _ :: _ :: _, _ + 2, _, _ => rfldef RhRegInv (c : RhRegCfg) : Prop :=
  isValidStack c.stack = true ∧ (inCompare c.stack = true → c.regs.getD 1 0 = 0)theorem rhRegInv_init : RhRegInv rhRegInit := by⊢ RhRegInv rhRegInit
  refine ⟨isValidStack_nil, ?_⟩⊢ inCompare rhRegInit.stack = true → rhRegInit.regs.getD 1 0 = 0
  intro hh:inCompare rhRegInit.stack = true⊢ rhRegInit.regs.getD 1 0 = 0; cases hAll goals completed! 🐙theorem rhRegInv_step {c c' : RhRegCfg} (hinv : RhRegInv c)
    (hs : rhRegStepOf false c = some c') : RhRegInv c' := byc:RhRegCfgc':RhRegCfghinv:RhRegInv chs:rhRegStepOf false c = some c'⊢ RhRegInv c'
  obtain ⟨stack, regs⟩ := cc':RhRegCfgstack:List (Fin 2)regs:List ℕhinv:RhRegInv { stack := stack, regs := regs }hs:rhRegStepOf false { stack := stack, regs := regs } = some c'⊢ RhRegInv c'
  obtain ⟨stack', regs'⟩ := c'stack:List (Fin 2)regs:List ℕhinv:RhRegInv { stack := stack, regs := regs }stack':List (Fin 2)regs':List ℕhs:rhRegStepOf false { stack := stack, regs := regs } = some { stack := stack', regs := regs' }⊢ RhRegInv { stack := stack', regs := regs' }
  obtain ⟨hv, hcmp⟩ := hinvstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhs:rhRegStepOf false { stack := stack, regs := regs } = some { stack := stack', regs := regs' }hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0⊢ RhRegInv { stack := stack', regs := regs' }
  have hv' := rhRegStepOf_valid false hv hsstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhs:rhRegStepOf false { stack := stack, regs := regs } = some { stack := stack', regs := regs' }hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = true⊢ RhRegInv { stack := stack', regs := regs' }
  refine ⟨hv', ?_⟩stack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhs:rhRegStepOf false { stack := stack, regs := regs } = some { stack := stack', regs := regs' }hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = true⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0
  have hmem : stack ∈ allValidStacks := List.contains_iff_mem.mp hvstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhs:rhRegStepOf false { stack := stack, regs := regs } = some { stack := stack', regs := regs' }hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStacks⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0
  have hok := inCompareStepOk_all stack hmemstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhs:rhRegStepOf false { stack := stack, regs := regs } = some { stack := stack', regs := regs' }hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshok:inCompareStepOk stack = true⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0
  unfold inCompareStepOk at hokstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhs:rhRegStepOf false { stack := stack, regs := regs } = some { stack := stack', regs := regs' }hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshok:(match evalStackOf false stack with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  true⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0
  have hstep_eq : rhRegStepOf false ⟨stack, regs⟩ =
      match evalStackOf false stack with
      | .halt => none
      | .jump s' => some ⟨s', regs⟩
      | .inc r s_succ => some ⟨s_succ, regs.set r (regs.getD r 0 + 1)⟩
      | .decnz r s_succ s_fail =>
        if regs.getD r 0 == 0 then some ⟨s_fail, regs⟩
        else some ⟨s_succ, regs.set r (regs.getD r 0 - 1)⟩ := rflstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhs:rhRegStepOf false { stack := stack, regs := regs } = some { stack := stack', regs := regs' }hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshok:(match evalStackOf false stack with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0
  rw [hstep_eqstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhs:(match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshok:(match evalStackOf false stack with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0] at hsstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhs:(match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshok:(match evalStackOf false stack with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0
  rcases hev : evalStackOf false stack with _ | s' | ⟨r, s_succ⟩ | ⟨r, s_succ, s_fail⟩haltstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhs:(match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshok:(match evalStackOf false stack with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }hev:evalStackOf false stack = RhInstr.halt⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0jumpstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhs:(match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshok:(match evalStackOf false stack with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }s':List (Fin 2)hev:evalStackOf false stack = RhInstr.jump s'⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0incstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhs:(match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshok:(match evalStackOf false stack with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)hev:evalStackOf false stack = RhInstr.inc r s_succ⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0decnzstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhs:(match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshok:(match evalStackOf false stack with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)s_fail:List (Fin 2)hev:evalStackOf false stack = RhInstr.decnz r s_succ s_fail⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0
  ·haltstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhs:(match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshok:(match evalStackOf false stack with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }hev:evalStackOf false stack = RhInstr.halt⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0 rw [hevhaltstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhs:(match RhInstr.halt with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshok:(match evalStackOf false stack with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }hev:evalStackOf false stack = RhInstr.halt⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0] at hshaltstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhs:(match RhInstr.halt with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshok:(match evalStackOf false stack with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }hev:evalStackOf false stack = RhInstr.halt⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0; cases hsAll goals completed! 🐙
  ·jumpstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhs:(match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshok:(match evalStackOf false stack with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }s':List (Fin 2)hev:evalStackOf false stack = RhInstr.jump s'⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0 rw [hevjumpstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }s':List (Fin 2)hok:(match RhInstr.jump s' with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehs:(match RhInstr.jump s' with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hev:evalStackOf false stack = RhInstr.jump s'⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0] at hs hokjumpstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }s':List (Fin 2)hok:(match RhInstr.jump s' with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehs:(match RhInstr.jump s' with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hev:evalStackOf false stack = RhInstr.jump s'⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0
    rcases Option.some.inj hs with ⟨rfl, rfl⟩jumpstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }hok:(match RhInstr.jump stack' with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehev:evalStackOf false stack = RhInstr.jump stack'hs:(match RhInstr.jump stack' with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs }⊢ inCompare { stack := stack', regs := regs }.stack = true → { stack := stack', regs := regs }.regs.getD 1 0 = 0
    intro hc'jumpstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }hok:(match RhInstr.jump stack' with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehev:evalStackOf false stack = RhInstr.jump stack'hs:(match RhInstr.jump stack' with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs }hc':inCompare { stack := stack', regs := regs }.stack = true⊢ { stack := stack', regs := regs }.regs.getD 1 0 = 0
    dsimp only at hok hc' ⊢jumpstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }hok:(if inCompare stack' = true then inCompare stack else true) = truehev:evalStackOf false stack = RhInstr.jump stack'hs:(match RhInstr.jump stack' with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs }hc':inCompare stack' = true⊢ regs.getD 1 0 = 0
    rw [hc',jumpstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }hok:(if true = true then inCompare stack else true) = truehev:evalStackOf false stack = RhInstr.jump stack'hs:(match RhInstr.jump stack' with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs }hc':inCompare stack' = true⊢ regs.getD 1 0 = 0 ite_eq_left rfljumpstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }hok:inCompare stack = truehev:evalStackOf false stack = RhInstr.jump stack'hs:(match RhInstr.jump stack' with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs }hc':inCompare stack' = true⊢ regs.getD 1 0 = 0] at hokjumpstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }hok:inCompare stack = truehev:evalStackOf false stack = RhInstr.jump stack'hs:(match RhInstr.jump stack' with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs }hc':inCompare stack' = true⊢ regs.getD 1 0 = 0
    exact hcmp hokAll goals completed! 🐙
  ·incstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhs:(match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshok:(match evalStackOf false stack with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)hev:evalStackOf false stack = RhInstr.inc r s_succ⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0 rw [hevincstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)hok:(match RhInstr.inc r s_succ with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehs:(match RhInstr.inc r s_succ with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hev:evalStackOf false stack = RhInstr.inc r s_succ⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0] at hs hokincstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)hok:(match RhInstr.inc r s_succ with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehs:(match RhInstr.inc r s_succ with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hev:evalStackOf false stack = RhInstr.inc r s_succ⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0
    rcases Option.some.inj hs with ⟨rfl, rfl⟩incstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕhok:(match RhInstr.inc r stack' with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehev:evalStackOf false stack = RhInstr.inc r stack'hs:(match RhInstr.inc r stack' with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs.set r (regs.getD r 0 + 1) }⊢ inCompare { stack := stack', regs := regs.set r (regs.getD r 0 + 1) }.stack = true →
  { stack := stack', regs := regs.set r (regs.getD r 0 + 1) }.regs.getD 1 0 = 0
    intro hc'incstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕhok:(match RhInstr.inc r stack' with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehev:evalStackOf false stack = RhInstr.inc r stack'hs:(match RhInstr.inc r stack' with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs.set r (regs.getD r 0 + 1) }hc':inCompare { stack := stack', regs := regs.set r (regs.getD r 0 + 1) }.stack = true⊢ { stack := stack', regs := regs.set r (regs.getD r 0 + 1) }.regs.getD 1 0 = 0
    dsimp only at hok hc' ⊢incstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕhok:(if inCompare stack' = true then inCompare stack && decide (r ≠ 1) else true) = truehev:evalStackOf false stack = RhInstr.inc r stack'hs:(match RhInstr.inc r stack' with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs.set r (regs.getD r 0 + 1) }hc':inCompare stack' = true⊢ (regs.set r (regs.getD r 0 + 1)).getD 1 0 = 0
    rw [hc',incstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕhok:(if true = true then inCompare stack && decide (r ≠ 1) else true) = truehev:evalStackOf false stack = RhInstr.inc r stack'hs:(match RhInstr.inc r stack' with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs.set r (regs.getD r 0 + 1) }hc':inCompare stack' = true⊢ (regs.set r (regs.getD r 0 + 1)).getD 1 0 = 0 ite_eq_left rfl,incstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕhok:(inCompare stack && decide (r ≠ 1)) = truehev:evalStackOf false stack = RhInstr.inc r stack'hs:(match RhInstr.inc r stack' with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs.set r (regs.getD r 0 + 1) }hc':inCompare stack' = true⊢ (regs.set r (regs.getD r 0 + 1)).getD 1 0 = 0 Bool.and_eq_trueincstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕhok:inCompare stack = true ∧ decide (r ≠ 1) = truehev:evalStackOf false stack = RhInstr.inc r stack'hs:(match RhInstr.inc r stack' with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs.set r (regs.getD r 0 + 1) }hc':inCompare stack' = true⊢ (regs.set r (regs.getD r 0 + 1)).getD 1 0 = 0] at hokincstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕhok:inCompare stack = true ∧ decide (r ≠ 1) = truehev:evalStackOf false stack = RhInstr.inc r stack'hs:(match RhInstr.inc r stack' with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs.set r (regs.getD r 0 + 1) }hc':inCompare stack' = true⊢ (regs.set r (regs.getD r 0 + 1)).getD 1 0 = 0
    rw [getD_one_set_ne regs r (of_decide_eq_true hok.2)incstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕhok:inCompare stack = true ∧ decide (r ≠ 1) = truehev:evalStackOf false stack = RhInstr.inc r stack'hs:(match RhInstr.inc r stack' with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs.set r (regs.getD r 0 + 1) }hc':inCompare stack' = true⊢ regs.getD 1 0 = 0]incstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕhok:inCompare stack = true ∧ decide (r ≠ 1) = truehev:evalStackOf false stack = RhInstr.inc r stack'hs:(match RhInstr.inc r stack' with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs.set r (regs.getD r 0 + 1) }hc':inCompare stack' = true⊢ regs.getD 1 0 = 0
    exact hcmp hok.1All goals completed! 🐙
  ·decnzstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhs:(match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshok:(match evalStackOf false stack with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)s_fail:List (Fin 2)hev:evalStackOf false stack = RhInstr.decnz r s_succ s_fail⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0 rw [hevdecnzstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)s_fail:List (Fin 2)hok:(match RhInstr.decnz r s_succ s_fail with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehs:(match RhInstr.decnz r s_succ s_fail with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hev:evalStackOf false stack = RhInstr.decnz r s_succ s_fail⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0] at hs hokdecnzstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)s_fail:List (Fin 2)hok:(match RhInstr.decnz r s_succ s_fail with
  | RhInstr.halt => true
  | RhInstr.jump s' => if inCompare s' = true then inCompare stack else true
  | RhInstr.inc r s_succ => if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true
  | RhInstr.decnz r s_succ s_fail =>
    (if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
      if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehs:(match RhInstr.decnz r s_succ s_fail with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hev:evalStackOf false stack = RhInstr.decnz r s_succ s_fail⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0
    dsimp only at hs hokdecnzstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)s_fail:List (Fin 2)hok:((if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) &&
    if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) =
  truehs:(if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
  else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hev:evalStackOf false stack = RhInstr.decnz r s_succ s_fail⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0
    rw [Bool.and_eq_truedecnzstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)s_fail:List (Fin 2)hok:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = true ∧
  (if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) = truehs:(if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
  else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hev:evalStackOf false stack = RhInstr.decnz r s_succ s_fail⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0] at hokdecnzstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)s_fail:List (Fin 2)hok:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = true ∧
  (if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) = truehs:(if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
  else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hev:evalStackOf false stack = RhInstr.decnz r s_succ s_fail⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0
    rcases hok with ⟨hok_succ, hok_fail⟩decnzstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)s_fail:List (Fin 2)hs:(if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
  else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hev:evalStackOf false stack = RhInstr.decnz r s_succ s_failhok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehok_fail:(if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) = true⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0
    by_cases hz : (regs.getD r 0 == 0) = trueposstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)s_fail:List (Fin 2)hs:(if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
  else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hev:evalStackOf false stack = RhInstr.decnz r s_succ s_failhok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehok_fail:(if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) = truehz:(regs.getD r 0 == 0) = true⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0negstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)s_fail:List (Fin 2)hs:(if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
  else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hev:evalStackOf false stack = RhInstr.decnz r s_succ s_failhok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehok_fail:(if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) = truehz:¬(regs.getD r 0 == 0) = true⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0
    ·posstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)s_fail:List (Fin 2)hs:(if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
  else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hev:evalStackOf false stack = RhInstr.decnz r s_succ s_failhok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehok_fail:(if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) = truehz:(regs.getD r 0 == 0) = true⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0 rw [hz,posstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)s_fail:List (Fin 2)hs:(if true = true then some { stack := s_fail, regs := regs }
  else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hev:evalStackOf false stack = RhInstr.decnz r s_succ s_failhok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehok_fail:(if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) = truehz:(regs.getD r 0 == 0) = true⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0 ite_eq_left rflposstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)s_fail:List (Fin 2)hs:some { stack := s_fail, regs := regs } = some { stack := stack', regs := regs' }hev:evalStackOf false stack = RhInstr.decnz r s_succ s_failhok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehok_fail:(if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) = truehz:(regs.getD r 0 == 0) = true⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0] at hsposstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)s_fail:List (Fin 2)hs:some { stack := s_fail, regs := regs } = some { stack := stack', regs := regs' }hev:evalStackOf false stack = RhInstr.decnz r s_succ s_failhok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehok_fail:(if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) = truehz:(regs.getD r 0 == 0) = true⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0
      rcases Option.some.inj hs with ⟨rfl, rfl⟩posstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)hok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehz:(regs.getD r 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz r s_succ stack'hok_fail:(if inCompare stack' = true then inCompare stack || decide (r = 1) else true) = truehs:some { stack := stack', regs := regs } = some { stack := stack', regs := regs }⊢ inCompare { stack := stack', regs := regs }.stack = true → { stack := stack', regs := regs }.regs.getD 1 0 = 0
      intro hc'posstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)hok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehz:(regs.getD r 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz r s_succ stack'hok_fail:(if inCompare stack' = true then inCompare stack || decide (r = 1) else true) = truehs:some { stack := stack', regs := regs } = some { stack := stack', regs := regs }hc':inCompare { stack := stack', regs := regs }.stack = true⊢ { stack := stack', regs := regs }.regs.getD 1 0 = 0
      dsimp only at hc' ⊢posstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)hok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehz:(regs.getD r 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz r s_succ stack'hok_fail:(if inCompare stack' = true then inCompare stack || decide (r = 1) else true) = truehs:some { stack := stack', regs := regs } = some { stack := stack', regs := regs }hc':inCompare stack' = true⊢ regs.getD 1 0 = 0
      rw [hc',posstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)hok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehz:(regs.getD r 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz r s_succ stack'hok_fail:(if true = true then inCompare stack || decide (r = 1) else true) = truehs:some { stack := stack', regs := regs } = some { stack := stack', regs := regs }hc':inCompare stack' = true⊢ regs.getD 1 0 = 0 ite_eq_left rfl,posstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)hok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehz:(regs.getD r 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz r s_succ stack'hok_fail:(inCompare stack || decide (r = 1)) = truehs:some { stack := stack', regs := regs } = some { stack := stack', regs := regs }hc':inCompare stack' = true⊢ regs.getD 1 0 = 0 Bool.or_eq_trueposstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)hok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehz:(regs.getD r 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz r s_succ stack'hok_fail:inCompare stack = true ∨ decide (r = 1) = truehs:some { stack := stack', regs := regs } = some { stack := stack', regs := regs }hc':inCompare stack' = true⊢ regs.getD 1 0 = 0] at hok_failposstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)hok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehz:(regs.getD r 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz r s_succ stack'hok_fail:inCompare stack = true ∨ decide (r = 1) = truehs:some { stack := stack', regs := regs } = some { stack := stack', regs := regs }hc':inCompare stack' = true⊢ regs.getD 1 0 = 0
      rcases hok_fail with hc | hr1pos.inlstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)hok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehz:(regs.getD r 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz r s_succ stack'hs:some { stack := stack', regs := regs } = some { stack := stack', regs := regs }hc':inCompare stack' = truehc:inCompare stack = true⊢ regs.getD 1 0 = 0pos.inrstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)hok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehz:(regs.getD r 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz r s_succ stack'hs:some { stack := stack', regs := regs } = some { stack := stack', regs := regs }hc':inCompare stack' = truehr1:decide (r = 1) = true⊢ regs.getD 1 0 = 0
      ·pos.inlstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)hok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehz:(regs.getD r 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz r s_succ stack'hs:some { stack := stack', regs := regs } = some { stack := stack', regs := regs }hc':inCompare stack' = truehc:inCompare stack = true⊢ regs.getD 1 0 = 0 exact hcmp hcAll goals completed! 🐙
      ·pos.inrstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)hok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehz:(regs.getD r 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz r s_succ stack'hs:some { stack := stack', regs := regs } = some { stack := stack', regs := regs }hc':inCompare stack' = truehr1:decide (r = 1) = true⊢ regs.getD 1 0 = 0 have hr_eq : r = 1 := of_decide_eq_true hr1pos.inrstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)hok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehz:(regs.getD r 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz r s_succ stack'hs:some { stack := stack', regs := regs } = some { stack := stack', regs := regs }hc':inCompare stack' = truehr1:decide (r = 1) = truehr_eq:r = 1⊢ regs.getD 1 0 = 0
        subst hr_eqpos.inrstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }s_succ:List (Fin 2)hs:some { stack := stack', regs := regs } = some { stack := stack', regs := regs }hc':inCompare stack' = truehok_succ:(if inCompare s_succ = true then inCompare stack && decide (1 ≠ 1) else true) = truehz:(regs.getD 1 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz 1 s_succ stack'hr1:decide (1 = 1) = true⊢ regs.getD 1 0 = 0
        exact beq_iff_eq.mp hzAll goals completed! 🐙
    ·negstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)s_fail:List (Fin 2)hs:(if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
  else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }) =
  some { stack := stack', regs := regs' }hev:evalStackOf false stack = RhInstr.decnz r s_succ s_failhok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehok_fail:(if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) = truehz:¬(regs.getD r 0 == 0) = true⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0 rw [ite_eq_right hznegstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)s_fail:List (Fin 2)hs:some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) } = some { stack := stack', regs := regs' }hev:evalStackOf false stack = RhInstr.decnz r s_succ s_failhok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehok_fail:(if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) = truehz:¬(regs.getD r 0 == 0) = true⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0] at hsnegstack:List (Fin 2)regs:List ℕstack':List (Fin 2)regs':List ℕhv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_succ:List (Fin 2)s_fail:List (Fin 2)hs:some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) } = some { stack := stack', regs := regs' }hev:evalStackOf false stack = RhInstr.decnz r s_succ s_failhok_succ:(if inCompare s_succ = true then inCompare stack && decide (r ≠ 1) else true) = truehok_fail:(if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) = truehz:¬(regs.getD r 0 == 0) = true⊢ inCompare { stack := stack', regs := regs' }.stack = true → { stack := stack', regs := regs' }.regs.getD 1 0 = 0
      rcases Option.some.inj hs with ⟨rfl, rfl⟩negstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_fail:List (Fin 2)hok_fail:(if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) = truehz:¬(regs.getD r 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz r stack' s_failhok_succ:(if inCompare stack' = true then inCompare stack && decide (r ≠ 1) else true) = truehs:some { stack := stack', regs := regs.set r (regs.getD r 0 - 1) } =
  some { stack := stack', regs := regs.set r (regs.getD r 0 - 1) }⊢ inCompare { stack := stack', regs := regs.set r (regs.getD r 0 - 1) }.stack = true →
  { stack := stack', regs := regs.set r (regs.getD r 0 - 1) }.regs.getD 1 0 = 0
      intro hc'negstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_fail:List (Fin 2)hok_fail:(if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) = truehz:¬(regs.getD r 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz r stack' s_failhok_succ:(if inCompare stack' = true then inCompare stack && decide (r ≠ 1) else true) = truehs:some { stack := stack', regs := regs.set r (regs.getD r 0 - 1) } =
  some { stack := stack', regs := regs.set r (regs.getD r 0 - 1) }hc':inCompare { stack := stack', regs := regs.set r (regs.getD r 0 - 1) }.stack = true⊢ { stack := stack', regs := regs.set r (regs.getD r 0 - 1) }.regs.getD 1 0 = 0
      dsimp only at hc' ⊢negstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_fail:List (Fin 2)hok_fail:(if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) = truehz:¬(regs.getD r 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz r stack' s_failhok_succ:(if inCompare stack' = true then inCompare stack && decide (r ≠ 1) else true) = truehs:some { stack := stack', regs := regs.set r (regs.getD r 0 - 1) } =
  some { stack := stack', regs := regs.set r (regs.getD r 0 - 1) }hc':inCompare stack' = true⊢ (regs.set r (regs.getD r 0 - 1)).getD 1 0 = 0
      rw [hc',negstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_fail:List (Fin 2)hok_fail:(if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) = truehz:¬(regs.getD r 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz r stack' s_failhok_succ:(if true = true then inCompare stack && decide (r ≠ 1) else true) = truehs:some { stack := stack', regs := regs.set r (regs.getD r 0 - 1) } =
  some { stack := stack', regs := regs.set r (regs.getD r 0 - 1) }hc':inCompare stack' = true⊢ (regs.set r (regs.getD r 0 - 1)).getD 1 0 = 0 ite_eq_left rfl,negstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_fail:List (Fin 2)hok_fail:(if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) = truehz:¬(regs.getD r 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz r stack' s_failhok_succ:(inCompare stack && decide (r ≠ 1)) = truehs:some { stack := stack', regs := regs.set r (regs.getD r 0 - 1) } =
  some { stack := stack', regs := regs.set r (regs.getD r 0 - 1) }hc':inCompare stack' = true⊢ (regs.set r (regs.getD r 0 - 1)).getD 1 0 = 0 Bool.and_eq_truenegstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_fail:List (Fin 2)hok_fail:(if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) = truehz:¬(regs.getD r 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz r stack' s_failhok_succ:inCompare stack = true ∧ decide (r ≠ 1) = truehs:some { stack := stack', regs := regs.set r (regs.getD r 0 - 1) } =
  some { stack := stack', regs := regs.set r (regs.getD r 0 - 1) }hc':inCompare stack' = true⊢ (regs.set r (regs.getD r 0 - 1)).getD 1 0 = 0] at hok_succnegstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_fail:List (Fin 2)hok_fail:(if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) = truehz:¬(regs.getD r 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz r stack' s_failhok_succ:inCompare stack = true ∧ decide (r ≠ 1) = truehs:some { stack := stack', regs := regs.set r (regs.getD r 0 - 1) } =
  some { stack := stack', regs := regs.set r (regs.getD r 0 - 1) }hc':inCompare stack' = true⊢ (regs.set r (regs.getD r 0 - 1)).getD 1 0 = 0
      rw [getD_one_set_ne regs r (of_decide_eq_true hok_succ.2)negstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_fail:List (Fin 2)hok_fail:(if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) = truehz:¬(regs.getD r 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz r stack' s_failhok_succ:inCompare stack = true ∧ decide (r ≠ 1) = truehs:some { stack := stack', regs := regs.set r (regs.getD r 0 - 1) } =
  some { stack := stack', regs := regs.set r (regs.getD r 0 - 1) }hc':inCompare stack' = true⊢ regs.getD 1 0 = 0]negstack:List (Fin 2)regs:List ℕstack':List (Fin 2)hv:isValidStack { stack := stack, regs := regs }.stack = truehcmp:inCompare { stack := stack, regs := regs }.stack = true → { stack := stack, regs := regs }.regs.getD 1 0 = 0hv':isValidStack stack' = truehmem:stack ∈ allValidStackshstep_eq:rhRegStepOf false { stack := stack, regs := regs } =
  match evalStackOf false stack with
  | RhInstr.halt => none
  | RhInstr.jump s' => some { stack := s', regs := regs }
  | RhInstr.inc r s_succ => some { stack := s_succ, regs := regs.set r (regs.getD r 0 + 1) }
  | RhInstr.decnz r s_succ s_fail =>
    if (regs.getD r 0 == 0) = true then some { stack := s_fail, regs := regs }
    else some { stack := s_succ, regs := regs.set r (regs.getD r 0 - 1) }r:ℕs_fail:List (Fin 2)hok_fail:(if inCompare s_fail = true then inCompare stack || decide (r = 1) else true) = truehz:¬(regs.getD r 0 == 0) = truehev:evalStackOf false stack = RhInstr.decnz r stack' s_failhok_succ:inCompare stack = true ∧ decide (r ≠ 1) = truehs:some { stack := stack', regs := regs.set r (regs.getD r 0 - 1) } =
  some { stack := stack', regs := regs.set r (regs.getD r 0 - 1) }hc':inCompare stack' = true⊢ regs.getD 1 0 = 0
      exact hcmp hok_succ.1All goals completed! 🐙theorem rhRegHalts_true_iff_false : RhRegHaltsOf true ↔ RhRegHaltsOf false := by⊢ RhRegHaltsOf true ↔ RhRegHaltsOf false
  have hrel : Respects (rhRegStepOf false) (rhRegStepOf true)
      (fun c₁ c₂ => RhRegInv c₁ ∧ c₁ = c₂) := by
    intro c₁ c₂ ⟨hinv, hc₂⟩c₁:RhRegCfgc₂:RhRegCfghinv:RhRegInv c₁hc₂:c₁ = c₂⊢ match rhRegStepOf false c₁ with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂) b₁ b₂ ∧ Reaches₁ (rhRegStepOf true) c₂ b₂
| none => rhRegStepOf true c₂ = none
    cases hc₂reflc₁:RhRegCfghinv:RhRegInv c₁⊢ match rhRegStepOf false c₁ with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂) b₁ b₂ ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
| none => rhRegStepOf true c₁ = none
    by_cases h11 : (c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = trueposc₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = true⊢ match rhRegStepOf false c₁ with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂) b₁ b₂ ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
| none => rhRegStepOf true c₁ = nonenegc₁:RhRegCfghinv:RhRegInv c₁h11:¬(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = true⊢ match rhRegStepOf false c₁ with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂) b₁ b₂ ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
| none => rhRegStepOf true c₁ = none
    ·posc₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = true⊢ match rhRegStepOf false c₁ with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂) b₁ b₂ ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
| none => rhRegStepOf true c₁ = none have hstk : c₁.stack = [1, 1, 1, 1, 1, 0, 1, 1] := beq_iff_eq.mp h11posc₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:c₁.stack = [1, 1, 1, 1, 1, 0, 1, 1]⊢ match rhRegStepOf false c₁ with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂) b₁ b₂ ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
| none => rhRegStepOf true c₁ = none
      have hcmp : inCompare c₁.stack = true := by⊢ RhRegHaltsOf true ↔ RhRegHaltsOf false rw [hstkc₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:c₁.stack = [1, 1, 1, 1, 1, 0, 1, 1]⊢ inCompare [1, 1, 1, 1, 1, 0, 1, 1] = true]c₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:c₁.stack = [1, 1, 1, 1, 1, 0, 1, 1]⊢ inCompare [1, 1, 1, 1, 1, 0, 1, 1] = true; decideposc₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:c₁.stack = [1, 1, 1, 1, 1, 0, 1, 1]hcmp:inCompare c₁.stack = true⊢ match rhRegStepOf false c₁ with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂) b₁ b₂ ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
| none => rhRegStepOf true c₁ = none
      have hj0 : c₁.regs.getD 1 0 = 0 := hinv.2 hcmpposc₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:c₁.stack = [1, 1, 1, 1, 1, 0, 1, 1]hcmp:inCompare c₁.stack = truehj0:c₁.regs.getD 1 0 = 0⊢ match rhRegStepOf false c₁ with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂) b₁ b₂ ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
| none => rhRegStepOf true c₁ = none
      have hj0_beq : (c₁.regs.getD 1 0 == 0) = true := beq_iff_eq.mpr hj0posc₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:c₁.stack = [1, 1, 1, 1, 1, 0, 1, 1]hcmp:inCompare c₁.stack = truehj0:c₁.regs.getD 1 0 = 0hj0_beq:(c₁.regs.getD 1 0 == 0) = true⊢ match rhRegStepOf false c₁ with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂) b₁ b₂ ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
| none => rhRegStepOf true c₁ = none
      have hs_false : rhRegStepOf false c₁ = some ⟨[1, 1, 1, 1, 1], c₁.regs⟩ := by⊢ RhRegHaltsOf true ↔ RhRegHaltsOf false
        obtain ⟨stk, rgs⟩ := c₁stk:List (Fin 2)rgs:List ℕhinv:RhRegInv { stack := stk, regs := rgs }h11:({ stack := stk, regs := rgs }.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:{ stack := stk, regs := rgs }.stack = [1, 1, 1, 1, 1, 0, 1, 1]hcmp:inCompare { stack := stk, regs := rgs }.stack = truehj0:{ stack := stk, regs := rgs }.regs.getD 1 0 = 0hj0_beq:({ stack := stk, regs := rgs }.regs.getD 1 0 == 0) = true⊢ rhRegStepOf false { stack := stk, regs := rgs } =
  some { stack := [1, 1, 1, 1, 1], regs := { stack := stk, regs := rgs }.regs }
        dsimp only at hstk ⊢stk:List (Fin 2)rgs:List ℕhinv:RhRegInv { stack := stk, regs := rgs }h11:({ stack := stk, regs := rgs }.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:stk = [1, 1, 1, 1, 1, 0, 1, 1]hcmp:inCompare { stack := stk, regs := rgs }.stack = truehj0:{ stack := stk, regs := rgs }.regs.getD 1 0 = 0hj0_beq:({ stack := stk, regs := rgs }.regs.getD 1 0 == 0) = true⊢ rhRegStepOf false { stack := stk, regs := rgs } = some { stack := [1, 1, 1, 1, 1], regs := rgs }
        subst hstkrgs:List ℕhinv:RhRegInv { stack := [1, 1, 1, 1, 1, 0, 1, 1], regs := rgs }h11:({ stack := [1, 1, 1, 1, 1, 0, 1, 1], regs := rgs }.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehcmp:inCompare { stack := [1, 1, 1, 1, 1, 0, 1, 1], regs := rgs }.stack = truehj0:{ stack := [1, 1, 1, 1, 1, 0, 1, 1], regs := rgs }.regs.getD 1 0 = 0hj0_beq:({ stack := [1, 1, 1, 1, 1, 0, 1, 1], regs := rgs }.regs.getD 1 0 == 0) = true⊢ rhRegStepOf false { stack := [1, 1, 1, 1, 1, 0, 1, 1], regs := rgs } = some { stack := [1, 1, 1, 1, 1], regs := rgs }
        rflposc₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:c₁.stack = [1, 1, 1, 1, 1, 0, 1, 1]hcmp:inCompare c₁.stack = truehj0:c₁.regs.getD 1 0 = 0hj0_beq:(c₁.regs.getD 1 0 == 0) = truehs_false:rhRegStepOf false c₁ = some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }⊢ match rhRegStepOf false c₁ with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂) b₁ b₂ ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
| none => rhRegStepOf true c₁ = none
      have hs_true1 : rhRegStepOf true c₁ = some ⟨[1, 1, 1, 1], c₁.regs⟩ := by⊢ RhRegHaltsOf true ↔ RhRegHaltsOf false
        obtain ⟨stk, rgs⟩ := c₁stk:List (Fin 2)rgs:List ℕhinv:RhRegInv { stack := stk, regs := rgs }h11:({ stack := stk, regs := rgs }.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:{ stack := stk, regs := rgs }.stack = [1, 1, 1, 1, 1, 0, 1, 1]hcmp:inCompare { stack := stk, regs := rgs }.stack = truehj0:{ stack := stk, regs := rgs }.regs.getD 1 0 = 0hj0_beq:({ stack := stk, regs := rgs }.regs.getD 1 0 == 0) = truehs_false:rhRegStepOf false { stack := stk, regs := rgs } =
  some { stack := [1, 1, 1, 1, 1], regs := { stack := stk, regs := rgs }.regs }⊢ rhRegStepOf true { stack := stk, regs := rgs } =
  some { stack := [1, 1, 1, 1], regs := { stack := stk, regs := rgs }.regs }
        dsimp only at hstk ⊢stk:List (Fin 2)rgs:List ℕhinv:RhRegInv { stack := stk, regs := rgs }h11:({ stack := stk, regs := rgs }.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:stk = [1, 1, 1, 1, 1, 0, 1, 1]hcmp:inCompare { stack := stk, regs := rgs }.stack = truehj0:{ stack := stk, regs := rgs }.regs.getD 1 0 = 0hj0_beq:({ stack := stk, regs := rgs }.regs.getD 1 0 == 0) = truehs_false:rhRegStepOf false { stack := stk, regs := rgs } =
  some { stack := [1, 1, 1, 1, 1], regs := { stack := stk, regs := rgs }.regs }⊢ rhRegStepOf true { stack := stk, regs := rgs } = some { stack := [1, 1, 1, 1], regs := rgs }
        subst hstkrgs:List ℕhinv:RhRegInv { stack := [1, 1, 1, 1, 1, 0, 1, 1], regs := rgs }h11:({ stack := [1, 1, 1, 1, 1, 0, 1, 1], regs := rgs }.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehcmp:inCompare { stack := [1, 1, 1, 1, 1, 0, 1, 1], regs := rgs }.stack = truehj0:{ stack := [1, 1, 1, 1, 1, 0, 1, 1], regs := rgs }.regs.getD 1 0 = 0hj0_beq:({ stack := [1, 1, 1, 1, 1, 0, 1, 1], regs := rgs }.regs.getD 1 0 == 0) = truehs_false:rhRegStepOf false { stack := [1, 1, 1, 1, 1, 0, 1, 1], regs := rgs } =
  some { stack := [1, 1, 1, 1, 1], regs := { stack := [1, 1, 1, 1, 1, 0, 1, 1], regs := rgs }.regs }⊢ rhRegStepOf true { stack := [1, 1, 1, 1, 1, 0, 1, 1], regs := rgs } = some { stack := [1, 1, 1, 1], regs := rgs }
        rflposc₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:c₁.stack = [1, 1, 1, 1, 1, 0, 1, 1]hcmp:inCompare c₁.stack = truehj0:c₁.regs.getD 1 0 = 0hj0_beq:(c₁.regs.getD 1 0 == 0) = truehs_false:rhRegStepOf false c₁ = some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }hs_true1:rhRegStepOf true c₁ = some { stack := [1, 1, 1, 1], regs := c₁.regs }⊢ match rhRegStepOf false c₁ with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂) b₁ b₂ ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
| none => rhRegStepOf true c₁ = none
      have hs_true2 : rhRegStepOf true ⟨[1, 1, 1, 1], c₁.regs⟩ =
          some ⟨[1, 1, 1, 1, 1], c₁.regs⟩ := by⊢ RhRegHaltsOf true ↔ RhRegHaltsOf false
        unfold rhRegStepOfc₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:c₁.stack = [1, 1, 1, 1, 1, 0, 1, 1]hcmp:inCompare c₁.stack = truehj0:c₁.regs.getD 1 0 = 0hj0_beq:(c₁.regs.getD 1 0 == 0) = truehs_false:rhRegStepOf false c₁ = some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }hs_true1:rhRegStepOf true c₁ = some { stack := [1, 1, 1, 1], regs := c₁.regs }⊢ (match evalStackOf true { stack := [1, 1, 1, 1], regs := c₁.regs }.stack with
  | RhInstr.halt => none
  | RhInstr.jump stack' => some { stack := stack', regs := { stack := [1, 1, 1, 1], regs := c₁.regs }.regs }
  | RhInstr.inc r stack_succ =>
    some
      { stack := stack_succ,
        regs :=
          { stack := [1, 1, 1, 1], regs := c₁.regs }.regs.set r
            ({ stack := [1, 1, 1, 1], regs := c₁.regs }.regs.getD r 0 + 1) }
  | RhInstr.decnz r stack_succ stack_fail =>
    if ({ stack := [1, 1, 1, 1], regs := c₁.regs }.regs.getD r 0 == 0) = true then
      some { stack := stack_fail, regs := { stack := [1, 1, 1, 1], regs := c₁.regs }.regs }
    else
      some
        { stack := stack_succ,
          regs :=
            { stack := [1, 1, 1, 1], regs := c₁.regs }.regs.set r
              ({ stack := [1, 1, 1, 1], regs := c₁.regs }.regs.getD r 0 - 1) }) =
  some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }
        have hev4 : evalStackOf true [1, 1, 1, 1] =
            .decnz 1 [1, 1, 1, 1, 0, 1] [1, 1, 1, 1, 1] := by⊢ RhRegHaltsOf true ↔ RhRegHaltsOf false decidec₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:c₁.stack = [1, 1, 1, 1, 1, 0, 1, 1]hcmp:inCompare c₁.stack = truehj0:c₁.regs.getD 1 0 = 0hj0_beq:(c₁.regs.getD 1 0 == 0) = truehs_false:rhRegStepOf false c₁ = some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }hs_true1:rhRegStepOf true c₁ = some { stack := [1, 1, 1, 1], regs := c₁.regs }hev4:evalStackOf true [1, 1, 1, 1] = RhInstr.decnz 1 [1, 1, 1, 1, 0, 1] [1, 1, 1, 1, 1]⊢ (match evalStackOf true { stack := [1, 1, 1, 1], regs := c₁.regs }.stack with
  | RhInstr.halt => none
  | RhInstr.jump stack' => some { stack := stack', regs := { stack := [1, 1, 1, 1], regs := c₁.regs }.regs }
  | RhInstr.inc r stack_succ =>
    some
      { stack := stack_succ,
        regs :=
          { stack := [1, 1, 1, 1], regs := c₁.regs }.regs.set r
            ({ stack := [1, 1, 1, 1], regs := c₁.regs }.regs.getD r 0 + 1) }
  | RhInstr.decnz r stack_succ stack_fail =>
    if ({ stack := [1, 1, 1, 1], regs := c₁.regs }.regs.getD r 0 == 0) = true then
      some { stack := stack_fail, regs := { stack := [1, 1, 1, 1], regs := c₁.regs }.regs }
    else
      some
        { stack := stack_succ,
          regs :=
            { stack := [1, 1, 1, 1], regs := c₁.regs }.regs.set r
              ({ stack := [1, 1, 1, 1], regs := c₁.regs }.regs.getD r 0 - 1) }) =
  some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }
        dsimp onlyc₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:c₁.stack = [1, 1, 1, 1, 1, 0, 1, 1]hcmp:inCompare c₁.stack = truehj0:c₁.regs.getD 1 0 = 0hj0_beq:(c₁.regs.getD 1 0 == 0) = truehs_false:rhRegStepOf false c₁ = some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }hs_true1:rhRegStepOf true c₁ = some { stack := [1, 1, 1, 1], regs := c₁.regs }hev4:evalStackOf true [1, 1, 1, 1] = RhInstr.decnz 1 [1, 1, 1, 1, 0, 1] [1, 1, 1, 1, 1]⊢ (match evalStackOf true [1, 1, 1, 1] with
  | RhInstr.halt => none
  | RhInstr.jump stack' => some { stack := stack', regs := c₁.regs }
  | RhInstr.inc r stack_succ => some { stack := stack_succ, regs := c₁.regs.set r (c₁.regs.getD r 0 + 1) }
  | RhInstr.decnz r stack_succ stack_fail =>
    if (c₁.regs.getD r 0 == 0) = true then some { stack := stack_fail, regs := c₁.regs }
    else some { stack := stack_succ, regs := c₁.regs.set r (c₁.regs.getD r 0 - 1) }) =
  some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }
        rw [hev4c₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:c₁.stack = [1, 1, 1, 1, 1, 0, 1, 1]hcmp:inCompare c₁.stack = truehj0:c₁.regs.getD 1 0 = 0hj0_beq:(c₁.regs.getD 1 0 == 0) = truehs_false:rhRegStepOf false c₁ = some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }hs_true1:rhRegStepOf true c₁ = some { stack := [1, 1, 1, 1], regs := c₁.regs }hev4:evalStackOf true [1, 1, 1, 1] = RhInstr.decnz 1 [1, 1, 1, 1, 0, 1] [1, 1, 1, 1, 1]⊢ (match RhInstr.decnz 1 [1, 1, 1, 1, 0, 1] [1, 1, 1, 1, 1] with
  | RhInstr.halt => none
  | RhInstr.jump stack' => some { stack := stack', regs := c₁.regs }
  | RhInstr.inc r stack_succ => some { stack := stack_succ, regs := c₁.regs.set r (c₁.regs.getD r 0 + 1) }
  | RhInstr.decnz r stack_succ stack_fail =>
    if (c₁.regs.getD r 0 == 0) = true then some { stack := stack_fail, regs := c₁.regs }
    else some { stack := stack_succ, regs := c₁.regs.set r (c₁.regs.getD r 0 - 1) }) =
  some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }]c₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:c₁.stack = [1, 1, 1, 1, 1, 0, 1, 1]hcmp:inCompare c₁.stack = truehj0:c₁.regs.getD 1 0 = 0hj0_beq:(c₁.regs.getD 1 0 == 0) = truehs_false:rhRegStepOf false c₁ = some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }hs_true1:rhRegStepOf true c₁ = some { stack := [1, 1, 1, 1], regs := c₁.regs }hev4:evalStackOf true [1, 1, 1, 1] = RhInstr.decnz 1 [1, 1, 1, 1, 0, 1] [1, 1, 1, 1, 1]⊢ (match RhInstr.decnz 1 [1, 1, 1, 1, 0, 1] [1, 1, 1, 1, 1] with
  | RhInstr.halt => none
  | RhInstr.jump stack' => some { stack := stack', regs := c₁.regs }
  | RhInstr.inc r stack_succ => some { stack := stack_succ, regs := c₁.regs.set r (c₁.regs.getD r 0 + 1) }
  | RhInstr.decnz r stack_succ stack_fail =>
    if (c₁.regs.getD r 0 == 0) = true then some { stack := stack_fail, regs := c₁.regs }
    else some { stack := stack_succ, regs := c₁.regs.set r (c₁.regs.getD r 0 - 1) }) =
  some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }
        dsimp onlyc₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:c₁.stack = [1, 1, 1, 1, 1, 0, 1, 1]hcmp:inCompare c₁.stack = truehj0:c₁.regs.getD 1 0 = 0hj0_beq:(c₁.regs.getD 1 0 == 0) = truehs_false:rhRegStepOf false c₁ = some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }hs_true1:rhRegStepOf true c₁ = some { stack := [1, 1, 1, 1], regs := c₁.regs }hev4:evalStackOf true [1, 1, 1, 1] = RhInstr.decnz 1 [1, 1, 1, 1, 0, 1] [1, 1, 1, 1, 1]⊢ (if (c₁.regs.getD 1 0 == 0) = true then some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }
  else some { stack := [1, 1, 1, 1, 0, 1], regs := c₁.regs.set 1 (c₁.regs.getD 1 0 - 1) }) =
  some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }
        rw [hj0_beq,c₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:c₁.stack = [1, 1, 1, 1, 1, 0, 1, 1]hcmp:inCompare c₁.stack = truehj0:c₁.regs.getD 1 0 = 0hj0_beq:(c₁.regs.getD 1 0 == 0) = truehs_false:rhRegStepOf false c₁ = some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }hs_true1:rhRegStepOf true c₁ = some { stack := [1, 1, 1, 1], regs := c₁.regs }hev4:evalStackOf true [1, 1, 1, 1] = RhInstr.decnz 1 [1, 1, 1, 1, 0, 1] [1, 1, 1, 1, 1]⊢ (if true = true then some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }
  else some { stack := [1, 1, 1, 1, 0, 1], regs := c₁.regs.set 1 (c₁.regs.getD 1 0 - 1) }) =
  some { stack := [1, 1, 1, 1, 1], regs := c₁.regs } ite_eq_left rflc₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:c₁.stack = [1, 1, 1, 1, 1, 0, 1, 1]hcmp:inCompare c₁.stack = truehj0:c₁.regs.getD 1 0 = 0hj0_beq:(c₁.regs.getD 1 0 == 0) = truehs_false:rhRegStepOf false c₁ = some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }hs_true1:rhRegStepOf true c₁ = some { stack := [1, 1, 1, 1], regs := c₁.regs }hev4:evalStackOf true [1, 1, 1, 1] = RhInstr.decnz 1 [1, 1, 1, 1, 0, 1] [1, 1, 1, 1, 1]⊢ some { stack := [1, 1, 1, 1, 1], regs := c₁.regs } = some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }]posc₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:c₁.stack = [1, 1, 1, 1, 1, 0, 1, 1]hcmp:inCompare c₁.stack = truehj0:c₁.regs.getD 1 0 = 0hj0_beq:(c₁.regs.getD 1 0 == 0) = truehs_false:rhRegStepOf false c₁ = some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }hs_true1:rhRegStepOf true c₁ = some { stack := [1, 1, 1, 1], regs := c₁.regs }hs_true2:rhRegStepOf true { stack := [1, 1, 1, 1], regs := c₁.regs } = some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }⊢ match rhRegStepOf false c₁ with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂) b₁ b₂ ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
| none => rhRegStepOf true c₁ = none
      rw [hs_falseposc₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:c₁.stack = [1, 1, 1, 1, 1, 0, 1, 1]hcmp:inCompare c₁.stack = truehj0:c₁.regs.getD 1 0 = 0hj0_beq:(c₁.regs.getD 1 0 == 0) = truehs_false:rhRegStepOf false c₁ = some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }hs_true1:rhRegStepOf true c₁ = some { stack := [1, 1, 1, 1], regs := c₁.regs }hs_true2:rhRegStepOf true { stack := [1, 1, 1, 1], regs := c₁.regs } = some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }⊢ match some { stack := [1, 1, 1, 1, 1], regs := c₁.regs } with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂) b₁ b₂ ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
| none => rhRegStepOf true c₁ = none]posc₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:c₁.stack = [1, 1, 1, 1, 1, 0, 1, 1]hcmp:inCompare c₁.stack = truehj0:c₁.regs.getD 1 0 = 0hj0_beq:(c₁.regs.getD 1 0 == 0) = truehs_false:rhRegStepOf false c₁ = some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }hs_true1:rhRegStepOf true c₁ = some { stack := [1, 1, 1, 1], regs := c₁.regs }hs_true2:rhRegStepOf true { stack := [1, 1, 1, 1], regs := c₁.regs } = some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }⊢ match some { stack := [1, 1, 1, 1, 1], regs := c₁.regs } with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂) b₁ b₂ ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
| none => rhRegStepOf true c₁ = none
      dsimp onlyposc₁:RhRegCfghinv:RhRegInv c₁h11:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = truehstk:c₁.stack = [1, 1, 1, 1, 1, 0, 1, 1]hcmp:inCompare c₁.stack = truehj0:c₁.regs.getD 1 0 = 0hj0_beq:(c₁.regs.getD 1 0 == 0) = truehs_false:rhRegStepOf false c₁ = some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }hs_true1:rhRegStepOf true c₁ = some { stack := [1, 1, 1, 1], regs := c₁.regs }hs_true2:rhRegStepOf true { stack := [1, 1, 1, 1], regs := c₁.regs } = some { stack := [1, 1, 1, 1, 1], regs := c₁.regs }⊢ ∃ b₂,
  (RhRegInv { stack := [1, 1, 1, 1, 1], regs := c₁.regs } ∧ { stack := [1, 1, 1, 1, 1], regs := c₁.regs } = b₂) ∧
    Reaches₁ (rhRegStepOf true) c₁ b₂
      exact ⟨⟨[1, 1, 1, 1, 1], c₁.regs⟩, ⟨rhRegInv_step hinv hs_false, rfl⟩,
        Relation.TransGen.head' hs_true1 (Relation.ReflTransGen.single hs_true2)⟩All goals completed! 🐙
    ·negc₁:RhRegCfghinv:RhRegInv c₁h11:¬(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = true⊢ match rhRegStepOf false c₁ with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂) b₁ b₂ ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
| none => rhRegStepOf true c₁ = none have h11_f : (c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = false :=
        Bool.eq_false_iff.mpr h11negc₁:RhRegCfghinv:RhRegInv c₁h11:¬(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = trueh11_f:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = false⊢ match rhRegStepOf false c₁ with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂) b₁ b₂ ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
| none => rhRegStepOf true c₁ = none
      have heq_step : rhRegStepOf true c₁ = rhRegStepOf false c₁ := by⊢ RhRegHaltsOf true ↔ RhRegHaltsOf false
        unfold rhRegStepOf evalStackOfc₁:RhRegCfghinv:RhRegInv c₁h11:¬(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = trueh11_f:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = false⊢ (match
    if (true && c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = true then RhInstr.jump [1, 1, 1, 1] else evalStack c₁.stack with
  | RhInstr.halt => none
  | RhInstr.jump stack' => some { stack := stack', regs := c₁.regs }
  | RhInstr.inc r stack_succ => some { stack := stack_succ, regs := c₁.regs.set r (c₁.regs.getD r 0 + 1) }
  | RhInstr.decnz r stack_succ stack_fail =>
    if (c₁.regs.getD r 0 == 0) = true then some { stack := stack_fail, regs := c₁.regs }
    else some { stack := stack_succ, regs := c₁.regs.set r (c₁.regs.getD r 0 - 1) }) =
  match
    if (false && c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = true then RhInstr.jump [1, 1, 1, 1]
    else evalStack c₁.stack with
  | RhInstr.halt => none
  | RhInstr.jump stack' => some { stack := stack', regs := c₁.regs }
  | RhInstr.inc r stack_succ => some { stack := stack_succ, regs := c₁.regs.set r (c₁.regs.getD r 0 + 1) }
  | RhInstr.decnz r stack_succ stack_fail =>
    if (c₁.regs.getD r 0 == 0) = true then some { stack := stack_fail, regs := c₁.regs }
    else some { stack := stack_succ, regs := c₁.regs.set r (c₁.regs.getD r 0 - 1) }
        rw [h11_fc₁:RhRegCfghinv:RhRegInv c₁h11:¬(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = trueh11_f:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = false⊢ (match if (true && false) = true then RhInstr.jump [1, 1, 1, 1] else evalStack c₁.stack with
  | RhInstr.halt => none
  | RhInstr.jump stack' => some { stack := stack', regs := c₁.regs }
  | RhInstr.inc r stack_succ => some { stack := stack_succ, regs := c₁.regs.set r (c₁.regs.getD r 0 + 1) }
  | RhInstr.decnz r stack_succ stack_fail =>
    if (c₁.regs.getD r 0 == 0) = true then some { stack := stack_fail, regs := c₁.regs }
    else some { stack := stack_succ, regs := c₁.regs.set r (c₁.regs.getD r 0 - 1) }) =
  match if (false && false) = true then RhInstr.jump [1, 1, 1, 1] else evalStack c₁.stack with
  | RhInstr.halt => none
  | RhInstr.jump stack' => some { stack := stack', regs := c₁.regs }
  | RhInstr.inc r stack_succ => some { stack := stack_succ, regs := c₁.regs.set r (c₁.regs.getD r 0 + 1) }
  | RhInstr.decnz r stack_succ stack_fail =>
    if (c₁.regs.getD r 0 == 0) = true then some { stack := stack_fail, regs := c₁.regs }
    else some { stack := stack_succ, regs := c₁.regs.set r (c₁.regs.getD r 0 - 1) }]c₁:RhRegCfghinv:RhRegInv c₁h11:¬(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = trueh11_f:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = false⊢ (match if (true && false) = true then RhInstr.jump [1, 1, 1, 1] else evalStack c₁.stack with
  | RhInstr.halt => none
  | RhInstr.jump stack' => some { stack := stack', regs := c₁.regs }
  | RhInstr.inc r stack_succ => some { stack := stack_succ, regs := c₁.regs.set r (c₁.regs.getD r 0 + 1) }
  | RhInstr.decnz r stack_succ stack_fail =>
    if (c₁.regs.getD r 0 == 0) = true then some { stack := stack_fail, regs := c₁.regs }
    else some { stack := stack_succ, regs := c₁.regs.set r (c₁.regs.getD r 0 - 1) }) =
  match if (false && false) = true then RhInstr.jump [1, 1, 1, 1] else evalStack c₁.stack with
  | RhInstr.halt => none
  | RhInstr.jump stack' => some { stack := stack', regs := c₁.regs }
  | RhInstr.inc r stack_succ => some { stack := stack_succ, regs := c₁.regs.set r (c₁.regs.getD r 0 + 1) }
  | RhInstr.decnz r stack_succ stack_fail =>
    if (c₁.regs.getD r 0 == 0) = true then some { stack := stack_fail, regs := c₁.regs }
    else some { stack := stack_succ, regs := c₁.regs.set r (c₁.regs.getD r 0 - 1) }; rflnegc₁:RhRegCfghinv:RhRegInv c₁h11:¬(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = trueh11_f:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = falseheq_step:rhRegStepOf true c₁ = rhRegStepOf false c₁⊢ match rhRegStepOf false c₁ with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂) b₁ b₂ ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
| none => rhRegStepOf true c₁ = none
      rcases hs : rhRegStepOf false c₁ with _ | c₁'neg.nonec₁:RhRegCfghinv:RhRegInv c₁h11:¬(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = trueh11_f:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = falseheq_step:rhRegStepOf true c₁ = rhRegStepOf false c₁hs:rhRegStepOf false c₁ = none⊢ match none with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂) b₁ b₂ ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
| none => rhRegStepOf true c₁ = noneneg.somec₁:RhRegCfghinv:RhRegInv c₁h11:¬(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = trueh11_f:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = falseheq_step:rhRegStepOf true c₁ = rhRegStepOf false c₁c₁':RhRegCfghs:rhRegStepOf false c₁ = some c₁'⊢ match some c₁' with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂) b₁ b₂ ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
| none => rhRegStepOf true c₁ = none
      ·neg.nonec₁:RhRegCfghinv:RhRegInv c₁h11:¬(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = trueh11_f:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = falseheq_step:rhRegStepOf true c₁ = rhRegStepOf false c₁hs:rhRegStepOf false c₁ = none⊢ match none with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂) b₁ b₂ ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
| none => rhRegStepOf true c₁ = none dsimp onlyneg.nonec₁:RhRegCfghinv:RhRegInv c₁h11:¬(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = trueh11_f:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = falseheq_step:rhRegStepOf true c₁ = rhRegStepOf false c₁hs:rhRegStepOf false c₁ = none⊢ rhRegStepOf true c₁ = none
        rw [heq_step,neg.nonec₁:RhRegCfghinv:RhRegInv c₁h11:¬(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = trueh11_f:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = falseheq_step:rhRegStepOf true c₁ = rhRegStepOf false c₁hs:rhRegStepOf false c₁ = none⊢ rhRegStepOf false c₁ = none hsneg.nonec₁:RhRegCfghinv:RhRegInv c₁h11:¬(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = trueh11_f:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = falseheq_step:rhRegStepOf true c₁ = rhRegStepOf false c₁hs:rhRegStepOf false c₁ = none⊢ none = none]All goals completed! 🐙
      ·neg.somec₁:RhRegCfghinv:RhRegInv c₁h11:¬(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = trueh11_f:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = falseheq_step:rhRegStepOf true c₁ = rhRegStepOf false c₁c₁':RhRegCfghs:rhRegStepOf false c₁ = some c₁'⊢ match some c₁' with
| some b₁ => ∃ b₂, (fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂) b₁ b₂ ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
| none => rhRegStepOf true c₁ = none dsimp onlyneg.somec₁:RhRegCfghinv:RhRegInv c₁h11:¬(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = trueh11_f:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = falseheq_step:rhRegStepOf true c₁ = rhRegStepOf false c₁c₁':RhRegCfghs:rhRegStepOf false c₁ = some c₁'⊢ ∃ b₂, (RhRegInv c₁' ∧ c₁' = b₂) ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
        have hs_true : rhRegStepOf true c₁ = some c₁' := by⊢ RhRegHaltsOf true ↔ RhRegHaltsOf false rw [heq_step,c₁:RhRegCfghinv:RhRegInv c₁h11:¬(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = trueh11_f:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = falseheq_step:rhRegStepOf true c₁ = rhRegStepOf false c₁c₁':RhRegCfghs:rhRegStepOf false c₁ = some c₁'⊢ rhRegStepOf false c₁ = some c₁' hsc₁:RhRegCfghinv:RhRegInv c₁h11:¬(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = trueh11_f:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = falseheq_step:rhRegStepOf true c₁ = rhRegStepOf false c₁c₁':RhRegCfghs:rhRegStepOf false c₁ = some c₁'⊢ some c₁' = some c₁']neg.somec₁:RhRegCfghinv:RhRegInv c₁h11:¬(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = trueh11_f:(c₁.stack == [1, 1, 1, 1, 1, 0, 1, 1]) = falseheq_step:rhRegStepOf true c₁ = rhRegStepOf false c₁c₁':RhRegCfghs:rhRegStepOf false c₁ = some c₁'hs_true:rhRegStepOf true c₁ = some c₁'⊢ ∃ b₂, (RhRegInv c₁' ∧ c₁' = b₂) ∧ Reaches₁ (rhRegStepOf true) c₁ b₂
        exact ⟨c₁', ⟨rhRegInv_step hinv hs, rfl⟩,
          Relation.TransGen.single hs_true⟩hrel:Respects (rhRegStepOf false) (rhRegStepOf true) fun c₁ c₂ ↦ RhRegInv c₁ ∧ c₁ = c₂⊢ RhRegHaltsOf true ↔ RhRegHaltsOf false
  exact StateTransition.tr_eval_dom hrel ⟨rhRegInv_init, rfl⟩All goals completed! 🐙endtheorem candidate_equivalent : Halts candidate ↔ Halts reference :=
  halts_candidate_iff_halts_edited121
    |>.trans (ConjectureMachines.Riemann120.halts_tm_iff_rhRegHaltsOf true)
    |>.trans rhRegHalts_true_iff_false
    |>.trans (ConjectureMachines.Riemann120.halts_tm_iff_rhRegHaltsOf false).symm
    |>.trans ConjectureMachines.Riemann120.halts_riemann120_iff_halts_riemann121.symmend ConjectureMachines.Riemann104