α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
e : List Nat
h : IsIdempotent ctx.op
⊢ evalList α ctx (mergeIdem e) = evalList α ctx e
α : Sort u_1
ctx : Context α
h : ContextInformation.isIdem ctx = true
e : List Nat
⊢ evalList α ctx (mergeIdem e) = evalList α ctx e
have h : IsIdempotent ctx.op := by simp [ContextInformation.isIdem, Option.isSome] at h; cases h₂ : ctx.idem <;> simp [h₂] at h; assumption
no goals
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
e : List Nat
h : IsIdempotent ctx.op
⊢ evalList α ctx (mergeIdem e) = evalList α ctx e
induction e using List.two_step_induction with
| empty => rfl
| single => rfl
| step x y ys ih =>
  cases ys with
  | nil =>
    simp [mergeIdem, mergeIdem.loop]
    split
    case inl h₂ => simp [evalList, h₂, h.1, EvalInformation.evalOp]
    rfl
  | cons z zs =>
    by_cases h₂ : x = y
    case inl =>
      rw [h₂, mergeIdem_head, ih]
      simp [evalList, ←ctx.assoc.1, h.1, EvalInformation.evalOp]
    case inr =>
      rw [mergeIdem_head2]
      by_cases h₃ : y = z
      case inl =>
        simp [mergeIdem_head, h₃, evalList]
        cases h₄ : mergeIdem (z :: zs) with
        | nil => apply absurd h₄; apply mergeIdem_nonEmpty; simp
        | cons u us => simp_all [mergeIdem, mergeIdem.loop, evalList]
      case inr =>
        simp [mergeIdem_head2, h₃, evalList] at *
        rw [ih]
      assumption
α : Sort u_1
ctx : Context α
h :
  (match ctx.idem with
    | some val => true
    | none => false) =
    true
e : List Nat
⊢ IsIdempotent ctx.op
α : Sort u_1
ctx : Context α
h : ContextInformation.isIdem ctx = true
e : List Nat
⊢ IsIdempotent ctx.op
simp [ContextInformation.isIdem, Option.isSome] at h
case some
α : Sort u_1
ctx : Context α
e : List Nat
val✝ : IsIdempotent ctx.op
h₂ : ctx.idem = some val✝
h : True
⊢ IsIdempotent ctx.op
α : Sort u_1
ctx : Context α
h :
  (match ctx.idem with
    | some val => true
    | none => false) =
    true
e : List Nat
⊢ IsIdempotent ctx.op
cases h₂ : ctx.idem <;> simp [h₂] at h
no goals
case some
α : Sort u_1
ctx : Context α
e : List Nat
val✝ : IsIdempotent ctx.op
h₂ : ctx.idem = some val✝
h : True
⊢ IsIdempotent ctx.op
assumption
no goals
case empty
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
⊢ evalList α ctx (mergeIdem []) = evalList α ctx []
rfl
no goals
case single
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
a✝ : Nat
⊢ evalList α ctx (mergeIdem [a✝]) = evalList α ctx [a✝]
rfl
no goals
case step
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y : Nat
ys : List Nat
ih : evalList α ctx (mergeIdem (y :: ys)) = evalList α ctx (y :: ys)
⊢ evalList α ctx (mergeIdem (x :: y :: ys)) = evalList α ctx (x :: y :: ys)
cases ys with
| nil =>
  simp [mergeIdem, mergeIdem.loop]
  split
  case inl h₂ => simp [evalList, h₂, h.1, EvalInformation.evalOp]
  rfl
| cons z zs =>
  by_cases h₂ : x = y
  case inl =>
    rw [h₂, mergeIdem_head, ih]
    simp [evalList, ←ctx.assoc.1, h.1, EvalInformation.evalOp]
  case inr =>
    rw [mergeIdem_head2]
    by_cases h₃ : y = z
    case inl =>
      simp [mergeIdem_head, h₃, evalList]
      cases h₄ : mergeIdem (z :: zs) with
      | nil => apply absurd h₄; apply mergeIdem_nonEmpty; simp
      | cons u us => simp_all [mergeIdem, mergeIdem.loop, evalList]
    case inr =>
      simp [mergeIdem_head2, h₃, evalList] at *
      rw [ih]
    assumption
case step.nil
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y : Nat
ih : evalList α ctx (mergeIdem [y]) = evalList α ctx [y]
⊢ evalList α ctx (if x = y then [x] else [x, y]) = evalList α ctx [x, y]
case step.nil
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y : Nat
ih : evalList α ctx (mergeIdem [y]) = evalList α ctx [y]
⊢ evalList α ctx (mergeIdem [x, y]) = evalList α ctx [x, y]
simp [mergeIdem, mergeIdem.loop]
case step.nil.inl
α : Sort u_1
ctx : Context α
h✝¹ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y : Nat
ih : evalList α ctx (mergeIdem [y]) = evalList α ctx [y]
h✝ : x = y
⊢ evalList α ctx [x] = evalList α ctx [x, y]

case step.nil.inr
α : Sort u_1
ctx : Context α
h✝¹ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y : Nat
ih : evalList α ctx (mergeIdem [y]) = evalList α ctx [y]
h✝ : ¬x = y
⊢ evalList α ctx [x, y] = evalList α ctx [x, y]
case step.nil
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y : Nat
ih : evalList α ctx (mergeIdem [y]) = evalList α ctx [y]
⊢ evalList α ctx (if x = y then [x] else [x, y]) = evalList α ctx [x, y]
split
case step.nil.inr
α : Sort u_1
ctx : Context α
h✝¹ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y : Nat
ih : evalList α ctx (mergeIdem [y]) = evalList α ctx [y]
h✝ : ¬x = y
⊢ evalList α ctx [x, y] = evalList α ctx [x, y]
case step.nil.inl
α : Sort u_1
ctx : Context α
h✝¹ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y : Nat
ih : evalList α ctx (mergeIdem [y]) = evalList α ctx [y]
h✝ : x = y
⊢ evalList α ctx [x] = evalList α ctx [x, y]

case step.nil.inr
α : Sort u_1
ctx : Context α
h✝¹ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y : Nat
ih : evalList α ctx (mergeIdem [y]) = evalList α ctx [y]
h✝ : ¬x = y
⊢ evalList α ctx [x, y] = evalList α ctx [x, y]
case inl h₂ => simp [evalList, h₂, h.1, EvalInformation.evalOp]
no goals
case step.nil.inr
α : Sort u_1
ctx : Context α
h✝¹ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y : Nat
ih : evalList α ctx (mergeIdem [y]) = evalList α ctx [y]
h✝ : ¬x = y
⊢ evalList α ctx [x, y] = evalList α ctx [x, y]
rfl
no goals
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y : Nat
ih : evalList α ctx (mergeIdem [y]) = evalList α ctx [y]
h₂ : x = y
⊢ evalList α ctx [x] = evalList α ctx [x, y]
simp [evalList, h₂, h.1, EvalInformation.evalOp]
case step.cons.inl
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : x = y
⊢ evalList α ctx (mergeIdem (x :: y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)

case step.cons.inr
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
⊢ evalList α ctx (mergeIdem (x :: y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)
case step.cons
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
⊢ evalList α ctx (mergeIdem (x :: y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)
by_cases h₂ : x = y
case step.cons.inr
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
⊢ evalList α ctx (mergeIdem (x :: y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)
case step.cons.inl
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : x = y
⊢ evalList α ctx (mergeIdem (x :: y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)

case step.cons.inr
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
⊢ evalList α ctx (mergeIdem (x :: y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)
case inl =>
  rw [h₂, mergeIdem_head, ih]
  simp [evalList, ←ctx.assoc.1, h.1, EvalInformation.evalOp]
no goals
case step.cons.inr
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
⊢ evalList α ctx (mergeIdem (x :: y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)
case inr =>
  rw [mergeIdem_head2]
  by_cases h₃ : y = z
  case inl =>
    simp [mergeIdem_head, h₃, evalList]
    cases h₄ : mergeIdem (z :: zs) with
    | nil => apply absurd h₄; apply mergeIdem_nonEmpty; simp
    | cons u us => simp_all [mergeIdem, mergeIdem.loop, evalList]
  case inr =>
    simp [mergeIdem_head2, h₃, evalList] at *
    rw [ih]
  assumption
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : x = y
⊢ evalList α ctx (y :: z :: zs) = evalList α ctx (y :: y :: z :: zs)
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : x = y
⊢ evalList α ctx (mergeIdem (x :: y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)
rw [h₂, mergeIdem_head, ih]
no goals
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : x = y
⊢ evalList α ctx (y :: z :: zs) = evalList α ctx (y :: y :: z :: zs)
simp [evalList, ←ctx.assoc.1, h.1, EvalInformation.evalOp]
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
⊢ evalList α ctx (x :: mergeIdem (y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)

α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
⊢ x ≠ y
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
⊢ evalList α ctx (mergeIdem (x :: y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)
rw [mergeIdem_head2]
case inl
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : y = z
⊢ evalList α ctx (x :: mergeIdem (y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)

case inr
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : ¬y = z
⊢ evalList α ctx (x :: mergeIdem (y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)

α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
⊢ x ≠ y
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
⊢ evalList α ctx (x :: mergeIdem (y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)

α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
⊢ x ≠ y
by_cases h₃ : y = z
case inr
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : ¬y = z
⊢ evalList α ctx (x :: mergeIdem (y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)

α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
⊢ x ≠ y
case inl
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : y = z
⊢ evalList α ctx (x :: mergeIdem (y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)

case inr
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : ¬y = z
⊢ evalList α ctx (x :: mergeIdem (y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)

α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
⊢ x ≠ y
case inl =>
  simp [mergeIdem_head, h₃, evalList]
  cases h₄ : mergeIdem (z :: zs) with
  | nil => apply absurd h₄; apply mergeIdem_nonEmpty; simp
  | cons u us => simp_all [mergeIdem, mergeIdem.loop, evalList]
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
⊢ x ≠ y
case inr
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : ¬y = z
⊢ evalList α ctx (x :: mergeIdem (y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)

α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
⊢ x ≠ y
case inr =>
  simp [mergeIdem_head2, h₃, evalList] at *
  rw [ih]
no goals
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
⊢ x ≠ y
assumption
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : y = z
⊢ evalList α ctx (x :: mergeIdem (z :: zs)) =
    EvalInformation.evalOp ctx (EvalInformation.evalVar ctx x)
      (EvalInformation.evalOp ctx (EvalInformation.evalVar ctx z) (evalList α ctx (z :: zs)))
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : y = z
⊢ evalList α ctx (x :: mergeIdem (y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)
simp [mergeIdem_head, h₃, evalList]
no goals
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : y = z
⊢ evalList α ctx (x :: mergeIdem (z :: zs)) =
    EvalInformation.evalOp ctx (EvalInformation.evalVar ctx x)
      (EvalInformation.evalOp ctx (EvalInformation.evalVar ctx z) (evalList α ctx (z :: zs)))
cases h₄ : mergeIdem (z :: zs) with
| nil => apply absurd h₄; apply mergeIdem_nonEmpty; simp
| cons u us => simp_all [mergeIdem, mergeIdem.loop, evalList]
case nil
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : y = z
h₄ : mergeIdem (z :: zs) = []
⊢ ¬mergeIdem (z :: zs) = []
case nil
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : y = z
h₄ : mergeIdem (z :: zs) = []
⊢ evalList α ctx [x] =
    EvalInformation.evalOp ctx (EvalInformation.evalVar ctx x)
      (EvalInformation.evalOp ctx (EvalInformation.evalVar ctx z) (evalList α ctx (z :: zs)))
apply absurd h₄
case nil.h
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : y = z
h₄ : mergeIdem (z :: zs) = []
⊢ z :: zs ≠ []
case nil
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : y = z
h₄ : mergeIdem (z :: zs) = []
⊢ ¬mergeIdem (z :: zs) = []
apply mergeIdem_nonEmpty
no goals
case nil.h
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : y = z
h₄ : mergeIdem (z :: zs) = []
⊢ z :: zs ≠ []
simp
no goals
case cons
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : y = z
u : Nat
us : List Nat
h₄ : mergeIdem (z :: zs) = u :: us
⊢ evalList α ctx (x :: u :: us) =
    EvalInformation.evalOp ctx (EvalInformation.evalVar ctx x)
      (EvalInformation.evalOp ctx (EvalInformation.evalVar ctx z) (evalList α ctx (z :: zs)))
simp_all [mergeIdem, mergeIdem.loop, evalList]
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
h₂ : ¬x = y
ih :
  evalList α ctx (y :: mergeIdem (z :: zs)) =
    EvalInformation.evalOp ctx (EvalInformation.evalVar ctx y) (evalList α ctx (z :: zs))
h₃ : True
⊢ EvalInformation.evalOp ctx (EvalInformation.evalVar ctx x) (evalList α ctx (y :: mergeIdem (z :: zs))) =
    EvalInformation.evalOp ctx (EvalInformation.evalVar ctx x)
      (EvalInformation.evalOp ctx (EvalInformation.evalVar ctx y) (evalList α ctx (z :: zs)))
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
ih : evalList α ctx (mergeIdem (y :: z :: zs)) = evalList α ctx (y :: z :: zs)
h₂ : ¬x = y
h₃ : ¬y = z
⊢ evalList α ctx (x :: mergeIdem (y :: z :: zs)) = evalList α ctx (x :: y :: z :: zs)
simp [mergeIdem_head2, h₃, evalList] at *
no goals
α : Sort u_1
ctx : Context α
h✝ : ContextInformation.isIdem ctx = true
h : IsIdempotent ctx.op
x y z : Nat
zs : List Nat
h₂ : ¬x = y
ih :
  evalList α ctx (y :: mergeIdem (z :: zs)) =
    EvalInformation.evalOp ctx (EvalInformation.evalVar ctx y) (evalList α ctx (z :: zs))
h₃ : True
⊢ EvalInformation.evalOp ctx (EvalInformation.evalVar ctx x) (evalList α ctx (y :: mergeIdem (z :: zs))) =
    EvalInformation.evalOp ctx (EvalInformation.evalVar ctx x)
      (EvalInformation.evalOp ctx (EvalInformation.evalVar ctx y) (evalList α ctx (z :: zs)))
rw [ih]