Theorem: RegMachine.stepsTo_functional (RegMachine/Basic.lean)

State before:
R✝ L✝ : Type
Start✝ : ?m.35746
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.35760) true
R L : Type
x✝ : Sort ?u.35745
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.35760) true
c d1 d2 : Config R L
h1 : c [P]==> d1
h2 : c [P]==> d2
⊢ d1 = d2
Tactic:
match c with
| {ip,regs} =>
  cases ip <;>
    (simp [step] at h1 h2; cases h1; cases h2; rfl)
State after:
no goals

State before:
R✝ L✝ : Type
Start✝ : ?m.35746
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.35760) true
R L : Type
x✝ : Sort ?u.35745
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.35760) true
c d1 d2 : Config R L
ip : Option L
regs : R → ℕ
h1 : { ip := ip, regs := regs } [P]==> d1
h2 : { ip := ip, regs := regs } [P]==> d2
⊢ d1 = d2
Tactic:
cases ip <;>
  (simp [step] at h1 h2; cases h1; cases h2; rfl)
State after:
no goals

State before:
case some
R✝ L✝ : Type
Start✝ : ?m.35746
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.35760) true
R L : Type
x✝ : Sort ?u.35745
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.35760) true
c d1 d2 : Config R L
regs : R → ℕ
val✝ : L
h1 : { ip := some val✝, regs := regs } [P]==> d1
h2 : { ip := some val✝, regs := regs } [P]==> d2
⊢ d1 = d2
Tactic:
simp [step] at h1 h2
State after:
case some
R✝ L✝ : Type
Start✝ : ?m.35746
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.35760) true
R L : Type
x✝ : Sort ?u.35745
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.35760) true
c d1 d2 : Config R L
regs : R → ℕ
val✝ : L
h1 :
  (match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }) =
    d1
h2 :
  (match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }) =
    d2
⊢ d1 = d2

State before:
case some
R✝ L✝ : Type
Start✝ : ?m.35746
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.35760) true
R L : Type
x✝ : Sort ?u.35745
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.35760) true
c d1 d2 : Config R L
regs : R → ℕ
val✝ : L
h1 :
  (match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }) =
    d1
h2 :
  (match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }) =
    d2
⊢ d1 = d2
Tactic:
cases h1
State after:
case some.refl
R✝ L✝ : Type
Start✝ : ?m.35746
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.35760) true
R L : Type
x✝ : Sort ?u.35745
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.35760) true
c d2 : Config R L
regs : R → ℕ
val✝ : L
h2 :
  (match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }) =
    d2
⊢ (match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }) =
    d2

State before:
case some.refl
R✝ L✝ : Type
Start✝ : ?m.35746
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.35760) true
R L : Type
x✝ : Sort ?u.35745
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.35760) true
c d2 : Config R L
regs : R → ℕ
val✝ : L
h2 :
  (match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }) =
    d2
⊢ (match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }) =
    d2
Tactic:
cases h2
State after:
case some.refl.refl
R✝ L✝ : Type
Start✝ : ?m.35746
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.35760) true
R L : Type
x✝ : Sort ?u.35745
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.35760) true
c : Config R L
regs : R → ℕ
val✝ : L
⊢ (match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }) =
    match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }

State before:
case some.refl.refl
R✝ L✝ : Type
Start✝ : ?m.35746
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.35760) true
R L : Type
x✝ : Sort ?u.35745
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.35760) true
c : Config R L
regs : R → ℕ
val✝ : L
⊢ (match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }) =
    match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }
Tactic:
rfl
State after:
no goals