Theorem: HMem.Encoding.encodeProgram_inj (HMem/Encoding/Emulator.lean)

State before:
p₀ p₁ : Program
⊢ encodeProgram p₀ = encodeProgram p₁ → p₀ = p₁
Tactic:
induction p₀ generalizing p₁ <;> cases p₁
State after:
case exit.exit

⊢ encodeProgram Program.exit = encodeProgram Program.exit → Program.exit = Program.exit

case exit.op
inst✝ : OpInstruction
next✝ : Program
⊢ encodeProgram Program.exit = encodeProgram (Program.op inst✝ next✝) → Program.exit = Program.op inst✝ next✝

case exit.branch
inst✝ : BranchInstruction
next✝ : Bool → Program
⊢ encodeProgram Program.exit = encodeProgram (Program.branch inst✝ next✝) → Program.exit = Program.branch inst✝ next✝

case exit.subroutine
dst✝ src✝ : Source
func✝ next✝ : Program
⊢ encodeProgram Program.exit = encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) →
    Program.exit = Program.subroutine dst✝ src✝ func✝ next✝

case exit.recurse
dst✝ src✝ : Source
next✝ : Program
⊢ encodeProgram Program.exit = encodeProgram (Program.recurse dst✝ src✝ next✝) →
    Program.exit = Program.recurse dst✝ src✝ next✝

case op.exit
inst✝ : OpInstruction
next✝ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝ = encodeProgram p₁ → next✝ = p₁
⊢ encodeProgram (Program.op inst✝ next✝) = encodeProgram Program.exit → Program.op inst✝ next✝ = Program.exit

case op.op
inst✝¹ : OpInstruction
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
inst✝ : OpInstruction
next✝ : Program
⊢ encodeProgram (Program.op inst✝¹ next✝¹) = encodeProgram (Program.op inst✝ next✝) →
    Program.op inst✝¹ next✝¹ = Program.op inst✝ next✝

case op.branch
inst✝¹ : OpInstruction
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
inst✝ : BranchInstruction
next✝ : Bool → Program
⊢ encodeProgram (Program.op inst✝¹ next✝¹) = encodeProgram (Program.branch inst✝ next✝) →
    Program.op inst✝¹ next✝¹ = Program.branch inst✝ next✝

case op.subroutine
inst✝ : OpInstruction
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
func✝ next✝ : Program
⊢ encodeProgram (Program.op inst✝ next✝¹) = encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) →
    Program.op inst✝ next✝¹ = Program.subroutine dst✝ src✝ func✝ next✝

case op.recurse
inst✝ : OpInstruction
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
next✝ : Program
⊢ encodeProgram (Program.op inst✝ next✝¹) = encodeProgram (Program.recurse dst✝ src✝ next✝) →
    Program.op inst✝ next✝¹ = Program.recurse dst✝ src✝ next✝

case branch.exit
inst✝ : BranchInstruction
next✝ : Bool → Program
next_ih✝ : ∀ (a : Bool) {p₁ : Program}, encodeProgram (next✝ a) = encodeProgram p₁ → next✝ a = p₁
⊢ encodeProgram (Program.branch inst✝ next✝) = encodeProgram Program.exit → Program.branch inst✝ next✝ = Program.exit

case branch.op
inst✝¹ : BranchInstruction
next✝¹ : Bool → Program
next_ih✝ : ∀ (a : Bool) {p₁ : Program}, encodeProgram (next✝¹ a) = encodeProgram p₁ → next✝¹ a = p₁
inst✝ : OpInstruction
next✝ : Program
⊢ encodeProgram (Program.branch inst✝¹ next✝¹) = encodeProgram (Program.op inst✝ next✝) →
    Program.branch inst✝¹ next✝¹ = Program.op inst✝ next✝

case branch.branch
inst✝¹ : BranchInstruction
next✝¹ : Bool → Program
next_ih✝ : ∀ (a : Bool) {p₁ : Program}, encodeProgram (next✝¹ a) = encodeProgram p₁ → next✝¹ a = p₁
inst✝ : BranchInstruction
next✝ : Bool → Program
⊢ encodeProgram (Program.branch inst✝¹ next✝¹) = encodeProgram (Program.branch inst✝ next✝) →
    Program.branch inst✝¹ next✝¹ = Program.branch inst✝ next✝

case branch.subroutine
inst✝ : BranchInstruction
next✝¹ : Bool → Program
next_ih✝ : ∀ (a : Bool) {p₁ : Program}, encodeProgram (next✝¹ a) = encodeProgram p₁ → next✝¹ a = p₁
dst✝ src✝ : Source
func✝ next✝ : Program
⊢ encodeProgram (Program.branch inst✝ next✝¹) = encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) →
    Program.branch inst✝ next✝¹ = Program.subroutine dst✝ src✝ func✝ next✝

case branch.recurse
inst✝ : BranchInstruction
next✝¹ : Bool → Program
next_ih✝ : ∀ (a : Bool) {p₁ : Program}, encodeProgram (next✝¹ a) = encodeProgram p₁ → next✝¹ a = p₁
dst✝ src✝ : Source
next✝ : Program
⊢ encodeProgram (Program.branch inst✝ next✝¹) = encodeProgram (Program.recurse dst✝ src✝ next✝) →
    Program.branch inst✝ next✝¹ = Program.recurse dst✝ src✝ next✝

case subroutine.exit
dst✝ src✝ : Source
func✝ next✝ : Program
func_ih✝ : ∀ {p₁ : Program}, encodeProgram func✝ = encodeProgram p₁ → func✝ = p₁
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝ = encodeProgram p₁ → next✝ = p₁
⊢ encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) = encodeProgram Program.exit →
    Program.subroutine dst✝ src✝ func✝ next✝ = Program.exit

case subroutine.op
dst✝ src✝ : Source
func✝ next✝¹ : Program
func_ih✝ : ∀ {p₁ : Program}, encodeProgram func✝ = encodeProgram p₁ → func✝ = p₁
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
inst✝ : OpInstruction
next✝ : Program
⊢ encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝¹) = encodeProgram (Program.op inst✝ next✝) →
    Program.subroutine dst✝ src✝ func✝ next✝¹ = Program.op inst✝ next✝

case subroutine.branch
dst✝ src✝ : Source
func✝ next✝¹ : Program
func_ih✝ : ∀ {p₁ : Program}, encodeProgram func✝ = encodeProgram p₁ → func✝ = p₁
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
inst✝ : BranchInstruction
next✝ : Bool → Program
⊢ encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝¹) = encodeProgram (Program.branch inst✝ next✝) →
    Program.subroutine dst✝ src✝ func✝ next✝¹ = Program.branch inst✝ next✝

case subroutine.subroutine
dst✝¹ src✝¹ : Source
func✝¹ next✝¹ : Program
func_ih✝ : ∀ {p₁ : Program}, encodeProgram func✝¹ = encodeProgram p₁ → func✝¹ = p₁
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
func✝ next✝ : Program
⊢ encodeProgram (Program.subroutine dst✝¹ src✝¹ func✝¹ next✝¹) =
      encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) →
    Program.subroutine dst✝¹ src✝¹ func✝¹ next✝¹ = Program.subroutine dst✝ src✝ func✝ next✝

case subroutine.recurse
dst✝¹ src✝¹ : Source
func✝ next✝¹ : Program
func_ih✝ : ∀ {p₁ : Program}, encodeProgram func✝ = encodeProgram p₁ → func✝ = p₁
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
next✝ : Program
⊢ encodeProgram (Program.subroutine dst✝¹ src✝¹ func✝ next✝¹) = encodeProgram (Program.recurse dst✝ src✝ next✝) →
    Program.subroutine dst✝¹ src✝¹ func✝ next✝¹ = Program.recurse dst✝ src✝ next✝

case recurse.exit
dst✝ src✝ : Source
next✝ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝ = encodeProgram p₁ → next✝ = p₁
⊢ encodeProgram (Program.recurse dst✝ src✝ next✝) = encodeProgram Program.exit →
    Program.recurse dst✝ src✝ next✝ = Program.exit

case recurse.op
dst✝ src✝ : Source
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
inst✝ : OpInstruction
next✝ : Program
⊢ encodeProgram (Program.recurse dst✝ src✝ next✝¹) = encodeProgram (Program.op inst✝ next✝) →
    Program.recurse dst✝ src✝ next✝¹ = Program.op inst✝ next✝

case recurse.branch
dst✝ src✝ : Source
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
inst✝ : BranchInstruction
next✝ : Bool → Program
⊢ encodeProgram (Program.recurse dst✝ src✝ next✝¹) = encodeProgram (Program.branch inst✝ next✝) →
    Program.recurse dst✝ src✝ next✝¹ = Program.branch inst✝ next✝

case recurse.subroutine
dst✝¹ src✝¹ : Source
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
func✝ next✝ : Program
⊢ encodeProgram (Program.recurse dst✝¹ src✝¹ next✝¹) = encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) →
    Program.recurse dst✝¹ src✝¹ next✝¹ = Program.subroutine dst✝ src✝ func✝ next✝

case recurse.recurse
dst✝¹ src✝¹ : Source
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
next✝ : Program
⊢ encodeProgram (Program.recurse dst✝¹ src✝¹ next✝¹) = encodeProgram (Program.recurse dst✝ src✝ next✝) →
    Program.recurse dst✝¹ src✝¹ next✝¹ = Program.recurse dst✝ src✝ next✝

State before:
inst✝¹ : OpInstruction
next✝¹ : Program
ih : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
inst✝ : OpInstruction
next✝ : Program
⊢ encodeProgram (Program.op inst✝¹ next✝¹) = encodeProgram (Program.op inst✝ next✝) →
    Program.op inst✝¹ next✝¹ = Program.op inst✝ next✝
Tactic:
case op.op ih _ _ => simpa [encodeProgram] using λ x y ↦ ⟨x, ih y⟩
State after:
no goals

State before:
inst✝¹ : BranchInstruction
next✝¹ : Bool → Program
nih : ∀ (a : Bool) {p₁ : Program}, encodeProgram (next✝¹ a) = encodeProgram p₁ → next✝¹ a = p₁
inst✝ : BranchInstruction
next✝ : Bool → Program
⊢ encodeProgram (Program.branch inst✝¹ next✝¹) = encodeProgram (Program.branch inst✝ next✝) →
    Program.branch inst✝¹ next✝¹ = Program.branch inst✝ next✝
Tactic:
case branch.branch nih _ _ =>
  simpa [encodeProgram] using λ hop hf ht ↦
    ⟨ hop, funext λ | false => nih _ hf | true => nih _ ht ⟩
State after:
no goals

State before:
dst✝¹ src✝¹ : Source
func✝¹ next✝¹ : Program
fih : ∀ {p₁ : Program}, encodeProgram func✝¹ = encodeProgram p₁ → func✝¹ = p₁
nih : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
func✝ next✝ : Program
⊢ encodeProgram (Program.subroutine dst✝¹ src✝¹ func✝¹ next✝¹) =
      encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) →
    Program.subroutine dst✝¹ src✝¹ func✝¹ next✝¹ = Program.subroutine dst✝ src✝ func✝ next✝
Tactic:
case subroutine.subroutine fih nih _ _ _ _ =>
  simpa [encodeProgram] using λ hdst hsrc hfunc hnext ↦ ⟨ hdst, hsrc, fih hfunc, nih hnext ⟩
State after:
no goals

State before:
dst✝¹ src✝¹ : Source
next✝¹ : Program
ih : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
next✝ : Program
⊢ encodeProgram (Program.recurse dst✝¹ src✝¹ next✝¹) = encodeProgram (Program.recurse dst✝ src✝ next✝) →
    Program.recurse dst✝¹ src✝¹ next✝¹ = Program.recurse dst✝ src✝ next✝
Tactic:
case recurse.recurse ih _ _ _ =>
  simpa [encodeProgram] using λ hdst hsrc hnext ↦ ⟨hdst, hsrc, ih hnext⟩
State after:
no goals

State before:
case exit.exit

⊢ encodeProgram Program.exit = encodeProgram Program.exit → Program.exit = Program.exit

case exit.op
inst✝ : OpInstruction
next✝ : Program
⊢ encodeProgram Program.exit = encodeProgram (Program.op inst✝ next✝) → Program.exit = Program.op inst✝ next✝

case exit.branch
inst✝ : BranchInstruction
next✝ : Bool → Program
⊢ encodeProgram Program.exit = encodeProgram (Program.branch inst✝ next✝) → Program.exit = Program.branch inst✝ next✝

case exit.subroutine
dst✝ src✝ : Source
func✝ next✝ : Program
⊢ encodeProgram Program.exit = encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) →
    Program.exit = Program.subroutine dst✝ src✝ func✝ next✝

case exit.recurse
dst✝ src✝ : Source
next✝ : Program
⊢ encodeProgram Program.exit = encodeProgram (Program.recurse dst✝ src✝ next✝) →
    Program.exit = Program.recurse dst✝ src✝ next✝

case op.exit
inst✝ : OpInstruction
next✝ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝ = encodeProgram p₁ → next✝ = p₁
⊢ encodeProgram (Program.op inst✝ next✝) = encodeProgram Program.exit → Program.op inst✝ next✝ = Program.exit

case op.branch
inst✝¹ : OpInstruction
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
inst✝ : BranchInstruction
next✝ : Bool → Program
⊢ encodeProgram (Program.op inst✝¹ next✝¹) = encodeProgram (Program.branch inst✝ next✝) →
    Program.op inst✝¹ next✝¹ = Program.branch inst✝ next✝

case op.subroutine
inst✝ : OpInstruction
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
func✝ next✝ : Program
⊢ encodeProgram (Program.op inst✝ next✝¹) = encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) →
    Program.op inst✝ next✝¹ = Program.subroutine dst✝ src✝ func✝ next✝

case op.recurse
inst✝ : OpInstruction
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
next✝ : Program
⊢ encodeProgram (Program.op inst✝ next✝¹) = encodeProgram (Program.recurse dst✝ src✝ next✝) →
    Program.op inst✝ next✝¹ = Program.recurse dst✝ src✝ next✝

case branch.exit
inst✝ : BranchInstruction
next✝ : Bool → Program
next_ih✝ : ∀ (a : Bool) {p₁ : Program}, encodeProgram (next✝ a) = encodeProgram p₁ → next✝ a = p₁
⊢ encodeProgram (Program.branch inst✝ next✝) = encodeProgram Program.exit → Program.branch inst✝ next✝ = Program.exit

case branch.op
inst✝¹ : BranchInstruction
next✝¹ : Bool → Program
next_ih✝ : ∀ (a : Bool) {p₁ : Program}, encodeProgram (next✝¹ a) = encodeProgram p₁ → next✝¹ a = p₁
inst✝ : OpInstruction
next✝ : Program
⊢ encodeProgram (Program.branch inst✝¹ next✝¹) = encodeProgram (Program.op inst✝ next✝) →
    Program.branch inst✝¹ next✝¹ = Program.op inst✝ next✝

case branch.subroutine
inst✝ : BranchInstruction
next✝¹ : Bool → Program
next_ih✝ : ∀ (a : Bool) {p₁ : Program}, encodeProgram (next✝¹ a) = encodeProgram p₁ → next✝¹ a = p₁
dst✝ src✝ : Source
func✝ next✝ : Program
⊢ encodeProgram (Program.branch inst✝ next✝¹) = encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) →
    Program.branch inst✝ next✝¹ = Program.subroutine dst✝ src✝ func✝ next✝

case branch.recurse
inst✝ : BranchInstruction
next✝¹ : Bool → Program
next_ih✝ : ∀ (a : Bool) {p₁ : Program}, encodeProgram (next✝¹ a) = encodeProgram p₁ → next✝¹ a = p₁
dst✝ src✝ : Source
next✝ : Program
⊢ encodeProgram (Program.branch inst✝ next✝¹) = encodeProgram (Program.recurse dst✝ src✝ next✝) →
    Program.branch inst✝ next✝¹ = Program.recurse dst✝ src✝ next✝

case subroutine.exit
dst✝ src✝ : Source
func✝ next✝ : Program
func_ih✝ : ∀ {p₁ : Program}, encodeProgram func✝ = encodeProgram p₁ → func✝ = p₁
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝ = encodeProgram p₁ → next✝ = p₁
⊢ encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) = encodeProgram Program.exit →
    Program.subroutine dst✝ src✝ func✝ next✝ = Program.exit

case subroutine.op
dst✝ src✝ : Source
func✝ next✝¹ : Program
func_ih✝ : ∀ {p₁ : Program}, encodeProgram func✝ = encodeProgram p₁ → func✝ = p₁
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
inst✝ : OpInstruction
next✝ : Program
⊢ encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝¹) = encodeProgram (Program.op inst✝ next✝) →
    Program.subroutine dst✝ src✝ func✝ next✝¹ = Program.op inst✝ next✝

case subroutine.branch
dst✝ src✝ : Source
func✝ next✝¹ : Program
func_ih✝ : ∀ {p₁ : Program}, encodeProgram func✝ = encodeProgram p₁ → func✝ = p₁
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
inst✝ : BranchInstruction
next✝ : Bool → Program
⊢ encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝¹) = encodeProgram (Program.branch inst✝ next✝) →
    Program.subroutine dst✝ src✝ func✝ next✝¹ = Program.branch inst✝ next✝

case subroutine.recurse
dst✝¹ src✝¹ : Source
func✝ next✝¹ : Program
func_ih✝ : ∀ {p₁ : Program}, encodeProgram func✝ = encodeProgram p₁ → func✝ = p₁
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
next✝ : Program
⊢ encodeProgram (Program.subroutine dst✝¹ src✝¹ func✝ next✝¹) = encodeProgram (Program.recurse dst✝ src✝ next✝) →
    Program.subroutine dst✝¹ src✝¹ func✝ next✝¹ = Program.recurse dst✝ src✝ next✝

case recurse.exit
dst✝ src✝ : Source
next✝ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝ = encodeProgram p₁ → next✝ = p₁
⊢ encodeProgram (Program.recurse dst✝ src✝ next✝) = encodeProgram Program.exit →
    Program.recurse dst✝ src✝ next✝ = Program.exit

case recurse.op
dst✝ src✝ : Source
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
inst✝ : OpInstruction
next✝ : Program
⊢ encodeProgram (Program.recurse dst✝ src✝ next✝¹) = encodeProgram (Program.op inst✝ next✝) →
    Program.recurse dst✝ src✝ next✝¹ = Program.op inst✝ next✝

case recurse.branch
dst✝ src✝ : Source
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
inst✝ : BranchInstruction
next✝ : Bool → Program
⊢ encodeProgram (Program.recurse dst✝ src✝ next✝¹) = encodeProgram (Program.branch inst✝ next✝) →
    Program.recurse dst✝ src✝ next✝¹ = Program.branch inst✝ next✝

case recurse.subroutine
dst✝¹ src✝¹ : Source
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
func✝ next✝ : Program
⊢ encodeProgram (Program.recurse dst✝¹ src✝¹ next✝¹) = encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) →
    Program.recurse dst✝¹ src✝¹ next✝¹ = Program.subroutine dst✝ src✝ func✝ next✝
Tactic:
all_goals simp [encodeProgram]
State after:
no goals

State before:
inst✝¹ : OpInstruction
next✝¹ : Program
ih : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
inst✝ : OpInstruction
next✝ : Program
⊢ encodeProgram (Program.op inst✝¹ next✝¹) = encodeProgram (Program.op inst✝ next✝) →
    Program.op inst✝¹ next✝¹ = Program.op inst✝ next✝
Tactic:
simpa [encodeProgram] using λ x y ↦ ⟨x, ih y⟩
State after:
no goals

State before:
inst✝¹ : BranchInstruction
next✝¹ : Bool → Program
nih : ∀ (a : Bool) {p₁ : Program}, encodeProgram (next✝¹ a) = encodeProgram p₁ → next✝¹ a = p₁
inst✝ : BranchInstruction
next✝ : Bool → Program
⊢ encodeProgram (Program.branch inst✝¹ next✝¹) = encodeProgram (Program.branch inst✝ next✝) →
    Program.branch inst✝¹ next✝¹ = Program.branch inst✝ next✝
Tactic:
simpa [encodeProgram] using λ hop hf ht ↦
  ⟨ hop, funext λ | false => nih _ hf | true => nih _ ht ⟩
State after:
no goals

State before:
dst✝¹ src✝¹ : Source
func✝¹ next✝¹ : Program
fih : ∀ {p₁ : Program}, encodeProgram func✝¹ = encodeProgram p₁ → func✝¹ = p₁
nih : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
func✝ next✝ : Program
⊢ encodeProgram (Program.subroutine dst✝¹ src✝¹ func✝¹ next✝¹) =
      encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) →
    Program.subroutine dst✝¹ src✝¹ func✝¹ next✝¹ = Program.subroutine dst✝ src✝ func✝ next✝
Tactic:
simpa [encodeProgram] using λ hdst hsrc hfunc hnext ↦ ⟨ hdst, hsrc, fih hfunc, nih hnext ⟩
State after:
no goals

State before:
dst✝¹ src✝¹ : Source
next✝¹ : Program
ih : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
next✝ : Program
⊢ encodeProgram (Program.recurse dst✝¹ src✝¹ next✝¹) = encodeProgram (Program.recurse dst✝ src✝ next✝) →
    Program.recurse dst✝¹ src✝¹ next✝¹ = Program.recurse dst✝ src✝ next✝
Tactic:
simpa [encodeProgram] using λ hdst hsrc hnext ↦ ⟨hdst, hsrc, ih hnext⟩
State after:
no goals

State before:
case recurse.subroutine
dst✝¹ src✝¹ : Source
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
func✝ next✝ : Program
⊢ encodeProgram (Program.recurse dst✝¹ src✝¹ next✝¹) = encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) →
    Program.recurse dst✝¹ src✝¹ next✝¹ = Program.subroutine dst✝ src✝ func✝ next✝
Tactic:
simp [encodeProgram]
State after:
no goals