Imports
/- Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.Mathematics.List import all Physlib.Mathematics.List

List lemmas

@[expose] public sectionlemma insertionSortMin_lt_length_succ {α : Type} (r : α α Prop) [DecidableRel r] (i : α) (l : List α) : insertionSortMinPos r i l < (insertionSortDropMinPos r i l).length.succ := α:Typer:α α Propinst✝:DecidableRel ri:αl:List α(insertionSortMinPos r i l) < (insertionSortDropMinPos r i l).length.succ All goals completed! 🐙

Given a list i :: l the left-most minimal position a of i :: l wrt r as an element of Fin (insertionSortDropMinPos r i l).length.succ.

def insertionSortMinPosFin {α : Type} (r : α α Prop) [DecidableRel r] (i : α) (l : List α) : Fin (insertionSortDropMinPos r i l).length.succ := insertionSortMinPos r i l, insertionSortMin_lt_length_succ r i l
α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αl:List αi:Fin (insertionSortDropMinPos r a l).lengthhl1:(∀ a' List.insertionSort r (insertionSortDropMinPos r a l), r (insertionSortMin r a l) a') List.Pairwise r (List.insertionSort r (insertionSortDropMinPos r a l))r (insertionSortMin r a l) (insertionSortDropMinPos r a l)[i] exact hl1.1 _ (α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αl:List αi:Fin (insertionSortDropMinPos r a l).lengthhl1:(∀ a' List.insertionSort r (insertionSortDropMinPos r a l), r (insertionSortMin r a l) a') List.Pairwise r (List.insertionSort r (insertionSortDropMinPos r a l))(insertionSortDropMinPos r a l)[i] List.insertionSort r (insertionSortDropMinPos r a l) All goals completed! 🐙)α:Typer:α α Propinst✝:DecidableRel ra:αl:List α(insertionSortEquiv r (a :: l)) ((insertionSortEquiv r (a :: l)).symm 0, ) = 0, All goals completed! 🐙lemma insertionSortEquiv_gt_zero_of_ne_insertionSortMinPos {α : Type} (r : α α Prop) [DecidableRel r] (a : α) (l : List α) (k : Fin (a :: l).length) (hk : k insertionSortMinPos r a l) : 0, n:α:Typer:α α Propinst✝:DecidableRel ra:αl:List αk:Fin (a :: l).lengthhk:k insertionSortMinPos r a l0 < (List.insertionSort r (a :: l)).length All goals completed! 🐙 < insertionSortEquiv r (a :: l) k := α:Typer:α α Propinst✝:DecidableRel ra:αl:List αk:Fin (a :: l).lengthhk:k insertionSortMinPos r a l0, < (insertionSortEquiv r (a :: l)) k α:Typer:α α Propinst✝:DecidableRel ra:αl:List αk:Fin (a :: l).lengthhk:k insertionSortMinPos r a lhn:¬0, < (insertionSortEquiv r (a :: l)) kFalse α:Typer:α α Propinst✝:DecidableRel ra:αl:List αk:Fin (a :: l).lengthhk:k insertionSortMinPos r a lhn:(insertionSortEquiv r (a :: l)) k 0, False α:Typer:α α Propinst✝:DecidableRel ra:αl:List αk:Fin (a :: l).lengthhk:k insertionSortMinPos r a lhn:(insertionSortEquiv r (a :: l)) k 0, (insertionSortEquiv r (a :: l)) k = 0, α:Typer:α α Propinst✝:DecidableRel ra:αl:List αk:Fin (a :: l).lengthhk:¬k = insertionSortMinPos r a lhn:((insertionSortEquiv r (a :: l)) k) = 0(insertionSortEquiv r (a :: l)) k = 0, All goals completed! 🐙α:Typer:α α Propinst✝:DecidableRel ra:αl:List αi:Fin (insertionSortDropMinPos r a l).lengthh:(insertionSortMinPosFin r a l).succAbove i < insertionSortMinPosFin r a lh1:(insertionSortDropMinPos r a l)[i] = (a :: l).get ((finCongr ) ((insertionSortMinPosFin r a l).succAbove i))hl:(insertionSortMinPos r a l) = (insertionSortMinPosFin r a l)¬((insertionSortMinPosFin r a l).succAbove i) = (insertionSortMinPos r a l) α:Typer:α α Propinst✝:DecidableRel ra:αl:List αi:Fin (insertionSortDropMinPos r a l).lengthh:(insertionSortMinPosFin r a l).succAbove i < insertionSortMinPosFin r a lh1:(insertionSortDropMinPos r a l)[i] = (a :: l).get ((finCongr ) ((insertionSortMinPosFin r a l).succAbove i))hl:(insertionSortMinPos r a l) = (insertionSortMinPosFin r a l)¬(insertionSortMinPosFin r a l).succAbove i = insertionSortMinPosFin r a l All goals completed! 🐙lemma insertionSort_insertionSort {α : Type} (r : α α Prop) [DecidableRel r] [Std.Total r] [IsTrans α r] (l1 : List α) : List.insertionSort r (List.insertionSort r l1) = List.insertionSort r l1 := α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α rl1:List αList.insertionSort r (List.insertionSort r l1) = List.insertionSort r l1 α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α rl1:List αList.Pairwise r (List.insertionSort r l1) All goals completed! 🐙α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrb:r b ah:r a cList.orderedInsert r a (b :: c :: l) = b :: a :: c :: l All goals completed! 🐙 α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrb:r b ah:¬r a cList.orderedInsert r a (if r b c then b :: c :: l else c :: List.orderedInsert r b l) = List.orderedInsert r b (if r a c then a :: c :: l else c :: List.orderedInsert r a l) α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrb:r b ah:¬r a cList.orderedInsert r a (if r b c then b :: c :: l else c :: List.orderedInsert r b l) = if r b c then b :: c :: List.orderedInsert r a l else c :: List.orderedInsert r b (List.orderedInsert r a l) α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrb:r b ah:¬r a chbc:r b cList.orderedInsert r a (if r b c then b :: c :: l else c :: List.orderedInsert r b l) = if r b c then b :: c :: List.orderedInsert r a l else c :: List.orderedInsert r b (List.orderedInsert r a l)α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrb:r b ah:¬r a chbc:¬r b cList.orderedInsert r a (if r b c then b :: c :: l else c :: List.orderedInsert r b l) = if r b c then b :: c :: List.orderedInsert r a l else c :: List.orderedInsert r b (List.orderedInsert r a l) α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrb:r b ah:¬r a chbc:r b cList.orderedInsert r a (if r b c then b :: c :: l else c :: List.orderedInsert r b l) = if r b c then b :: c :: List.orderedInsert r a l else c :: List.orderedInsert r b (List.orderedInsert r a l) All goals completed! 🐙 α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrb:r b ah:¬r a chbc:¬r b cList.orderedInsert r a (if r b c then b :: c :: l else c :: List.orderedInsert r b l) = if r b c then b :: c :: List.orderedInsert r a l else c :: List.orderedInsert r b (List.orderedInsert r a l) α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrb:r b ah:¬r a chbc:¬r b cList.orderedInsert r a (List.orderedInsert r b l) = List.orderedInsert r b (List.orderedInsert r a l) All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙@[simp] lemma orderedInsert_length {α : Type} (r : α α Prop) [DecidableRel r] (a : α) (l : List α) : (List.orderedInsert r a l).length = (a :: l).length := α:Typer:α α Propinst✝:DecidableRel ra:αl:List α(List.orderedInsert r a l).length = (a :: l).length α:Typer:α α Propinst✝:DecidableRel ra:αl:List α(List.orderedInsert r a l).Perm (a :: l) All goals completed! 🐙lemma takeWhile_orderedInsert {α : Type} (r : α α Prop) [DecidableRel r] [Std.Total r] [IsTrans α r] (a b : α) (hr : ¬ r a b) : (l : List α) (List.takeWhile (fun c => !decide (r a c)) (List.orderedInsert r b l)).length = (List.takeWhile (fun c => !decide (r a c)) l).length + 1 α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a b(List.takeWhile (fun c => !decide (r a c)) (List.orderedInsert r b [])).length = (List.takeWhile (fun c => !decide (r a c)) []).length + 1 α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a b(List.takeWhile (fun c => !decide (r a c)) (List.orderedInsert r b [])).length = (List.takeWhile (fun c => !decide (r a c)) []).length + 1 All goals completed! 🐙 α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List α(List.takeWhile (fun c => !decide (r a c)) (List.orderedInsert r b (c :: l))).length = (List.takeWhile (fun c => !decide (r a c)) (c :: l)).length + 1 α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List α(List.takeWhile (fun c => !decide (r a c)) (List.orderedInsert r b (c :: l))).length = (List.takeWhile (fun c => !decide (r a c)) (c :: l)).length + 1 α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List α(List.takeWhile (fun c => !decide (r a c)) (if r b c then b :: c :: l else c :: List.orderedInsert r b l)).length = (List.takeWhile (fun c => !decide (r a c)) (c :: l)).length + 1 α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αh:r b c(List.takeWhile (fun c => !decide (r a c)) (if r b c then b :: c :: l else c :: List.orderedInsert r b l)).length = (List.takeWhile (fun c => !decide (r a c)) (c :: l)).length + 1α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αh:¬r b c(List.takeWhile (fun c => !decide (r a c)) (if r b c then b :: c :: l else c :: List.orderedInsert r b l)).length = (List.takeWhile (fun c => !decide (r a c)) (c :: l)).length + 1 α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αh:r b c(List.takeWhile (fun c => !decide (r a c)) (if r b c then b :: c :: l else c :: List.orderedInsert r b l)).length = (List.takeWhile (fun c => !decide (r a c)) (c :: l)).length + 1 All goals completed! 🐙 α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αh:¬r b c(List.takeWhile (fun c => !decide (r a c)) (if r b c then b :: c :: l else c :: List.orderedInsert r b l)).length = (List.takeWhile (fun c => !decide (r a c)) (c :: l)).length + 1 α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αh:¬r b c(List.takeWhile (fun c => !decide (r a c)) (c :: List.orderedInsert r b l)).length = (List.takeWhile (fun c => !decide (r a c)) (c :: l)).length + 1 α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αh:¬r b chl:¬r a c(List.takeWhile (fun c => !decide (r a c)) (c :: List.orderedInsert r b l)).length = (List.takeWhile (fun c => !decide (r a c)) (c :: l)).length + 1 α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αh:¬r b chl:¬r a c(List.takeWhile (fun c => !decide (r a c)) (List.orderedInsert r b l)).length = (List.takeWhile (fun c => !decide (r a c)) l).length + 1 All goals completed! 🐙lemma takeWhile_orderedInsert' {α : Type} (r : α α Prop) [DecidableRel r] [Std.Total r] [IsTrans α r] (a b : α) (hr : ¬ r a b) : (l : List α) (List.takeWhile (fun c => !decide (r b c)) (List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) l).length α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a b(List.takeWhile (fun c => !decide (r b c)) (List.orderedInsert r a [])).length = (List.takeWhile (fun c => !decide (r b c)) []).length α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a b(List.takeWhile (fun c => !decide (r b c)) (List.orderedInsert r a [])).length = (List.takeWhile (fun c => !decide (r b c)) []).length All goals completed! 🐙 α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List α(List.takeWhile (fun c => !decide (r b c)) (List.orderedInsert r a (c :: l))).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List α(List.takeWhile (fun c => !decide (r b c)) (List.orderedInsert r a (c :: l))).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b a(List.takeWhile (fun c => !decide (r b c)) (List.orderedInsert r a (c :: l))).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b a(List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:r b c(List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).lengthα:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:¬r b c(List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:r b c(List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:r b chac:r a c(List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).lengthα:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:r b chac:¬r a c(List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:r b chac:r a c(List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).lengthα:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:r b chac:¬r a c(List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length All goals completed! 🐙 α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:¬r b c(List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:¬r b chac:r a c(List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).lengthα:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:¬r b chac:¬r a c(List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:¬r b chac:r a c(List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length All goals completed! 🐙 α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:¬r b chac:¬r a c(List.takeWhile (fun c => !decide (r b c)) (if r a c then a :: c :: l else c :: List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) (c :: l)).length α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bc:αl:List αhrba:r b ah:¬r b chac:¬r a c(List.takeWhile (fun c => !decide (r b c)) (List.orderedInsert r a l)).length = (List.takeWhile (fun c => !decide (r b c)) l).length All goals completed! 🐙α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1(a1.succAbove (b1.succAbove n), ) = (b2.succAbove (a2.succAbove n), ) α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1(if (if n < b2 then n else n + 1) < a2 + 1 then if n < b2 then n else n + 1 else (if n < b2 then n else n + 1) + 1) = if (if n < a2 then n else n + 1) < b2 then if n < a2 then n else n + 1 else (if n < a2 then n else n + 1) + 1 α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝²:n < b2h✝¹:n < a2 + 1h✝:n < a2n = nα:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝³:n < b2h✝²:n < a2 + 1h✝¹:¬n < a2h✝:n + 1 < b2n = n + 1α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝³:n < b2h✝²:n < a2 + 1h✝¹:¬n < a2h✝:¬n + 1 < b2n = n + 1 + 1α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝²:n < b2h✝¹:¬n < a2 + 1h✝:n < a2n + 1 = nα:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝³:n < b2h✝²:¬n < a2 + 1h✝¹:¬n < a2h✝:n + 1 < b2n + 1 = n + 1α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝³:n < b2h✝²:¬n < a2 + 1h✝¹:¬n < a2h✝:¬n + 1 < b2n + 1 = n + 1 + 1α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝²:¬n < b2h✝¹:n + 1 < a2 + 1h✝:n < a2n + 1 = n + 1α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝³:¬n < b2h✝²:n + 1 < a2 + 1h✝¹:¬n < a2h✝:n + 1 < b2n + 1 = n + 1α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝³:¬n < b2h✝²:n + 1 < a2 + 1h✝¹:¬n < a2h✝:¬n + 1 < b2n + 1 = n + 1 + 1α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝²:¬n < b2h✝¹:¬n + 1 < a2 + 1h✝:n < a2n + 1 + 1 = n + 1α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝³:¬n < b2h✝²:¬n + 1 < a2 + 1h✝¹:¬n < a2h✝:n + 1 < b2n + 1 + 1 = n + 1α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝³:¬n < b2h✝²:¬n + 1 < a2 + 1h✝¹:¬n < a2h✝:¬n + 1 < b2n + 1 + 1 = n + 1 + 1 α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝²:n < b2h✝¹:n < a2 + 1h✝:n < a2n = nα:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝³:n < b2h✝²:n < a2 + 1h✝¹:¬n < a2h✝:n + 1 < b2n = n + 1α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝³:n < b2h✝²:n < a2 + 1h✝¹:¬n < a2h✝:¬n + 1 < b2n = n + 1 + 1α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝²:n < b2h✝¹:¬n < a2 + 1h✝:n < a2n + 1 = nα:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝³:n < b2h✝²:¬n < a2 + 1h✝¹:¬n < a2h✝:n + 1 < b2n + 1 = n + 1α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝³:n < b2h✝²:¬n < a2 + 1h✝¹:¬n < a2h✝:¬n + 1 < b2n + 1 = n + 1 + 1α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝²:¬n < b2h✝¹:n + 1 < a2 + 1h✝:n < a2n + 1 = n + 1α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝³:¬n < b2h✝²:n + 1 < a2 + 1h✝¹:¬n < a2h✝:n + 1 < b2n + 1 = n + 1α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝³:¬n < b2h✝²:n + 1 < a2 + 1h✝¹:¬n < a2h✝:¬n + 1 < b2n + 1 = n + 1 + 1α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝²:¬n < b2h✝¹:¬n + 1 < a2 + 1h✝:n < a2n + 1 + 1 = n + 1α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝³:¬n < b2h✝²:¬n + 1 < a2 + 1h✝¹:¬n < a2h✝:n + 1 < b2n + 1 + 1 = n + 1α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αhr:¬r a bn✝:hrba:r b al:List αhn:n + 2 < (a :: b :: l).lengtha1:Fin ((List.orderedInsert r b (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r b (List.insertionSort r l)) a), b1:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) b), a2:Fin ((List.insertionSort r l).length + 1) := (orderedInsertPos r (List.insertionSort r l) a), b2:Fin ((List.orderedInsert r a (List.insertionSort r l)).length + 1) := (orderedInsertPos r (List.orderedInsert r a (List.insertionSort r l)) b), ht:List.takeWhile (fun c => !decide (r b c)) (List.insertionSort r l) = List.takeWhile (fun c => !decide (r b c)) (List.takeWhile (fun c => !decide (r a c)) (List.insertionSort r l))ha1:b1 a2ha2:a1 = a2 + 1hb:b1 = b2n:Fin (List.insertionSort r l).length := (insertionSortEquiv r l) n✝, hba:b2 a2val_succAbove: {m : } (p : Fin (m + 1)) (i : Fin m), (p.succAbove i) = if i < p then i else i + 1h✝³:¬n < b2h✝²:¬n + 1 < a2 + 1h✝¹:¬n < a2h✝:¬n + 1 < b2n + 1 + 1 = n + 1 + 1 All goals completed! 🐙α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αa2:αb:αl1:List αl2:List αh:¬r a bh1:List.orderedInsert r a (b :: l1) ++ a2 :: l2 = b :: List.orderedInsert r a l1 ++ a2 :: l2hl✝:List.insertionSort r (List.orderedInsert r a l1 ++ a2 :: l2) = List.insertionSort r (a :: l1 ++ a2 :: l2)hl:l1.length + 1 + 1 = l1.length + 2Fin.cast ((insertionSortEquiv r (b :: a :: (l1 ++ a2 :: l2))) l1.length + 2, ) = Fin.cast ((insertionSortEquiv r (a :: b :: (l1 ++ a2 :: l2))) l1.length + 1 + 1, ) α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αa2:αb:αl1:List αl2:List αh:¬r a bh1:List.orderedInsert r a (b :: l1) ++ a2 :: l2 = b :: List.orderedInsert r a l1 ++ a2 :: l2hl✝:List.insertionSort r (List.orderedInsert r a l1 ++ a2 :: l2) = List.insertionSort r (a :: l1 ++ a2 :: l2)hl:l1.length + 1 + 1 = l1.length + 2Fin.cast ((insertionSortEquiv r (b :: a :: (l1 ++ a2 :: l2))) l1.length + 2, ) = Fin.cast ((insertionSortEquiv r (a :: b :: (l1 ++ a2 :: l2))) l1.length + 2, ) conv_rhs => α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αa2:αb:αl1:List αl2:List αh:¬r a bh1:List.orderedInsert r a (b :: l1) ++ a2 :: l2 = b :: List.orderedInsert r a l1 ++ a2 :: l2hl✝:List.insertionSort r (List.orderedInsert r a l1 ++ a2 :: l2) = List.insertionSort r (a :: l1 ++ a2 :: l2)hl:l1.length + 1 + 1 = l1.length + 2| Fin.cast ((finCongr ) ((insertionSortEquiv r (b :: a :: (l1 ++ a2 :: l2))) l1.length + 2, )) α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αa2:αb:αl1:List αl2:List αh:¬r a bh1:List.orderedInsert r a (b :: l1) ++ a2 :: l2 = b :: List.orderedInsert r a l1 ++ a2 :: l2hl✝:List.insertionSort r (List.orderedInsert r a l1 ++ a2 :: l2) = List.insertionSort r (a :: l1 ++ a2 :: l2)hl:l1.length + 1 + 1 = l1.length + 2(insertionSortEquiv r (b :: a :: (l1 ++ a2 :: l2))) l1.length + 2, = (insertionSortEquiv r (b :: a :: (l1 ++ a2 :: l2))) l1.length + 2, All goals completed! 🐙α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αl1:List αl2:List αhl✝:(insertionSortEquiv r (List.orderedInsert r b (List.insertionSort r l1) ++ a :: l2)) l1.length + 1, = Fin.cast ((insertionSortEquiv r (b :: (List.insertionSort r l1 ++ a :: l2))) l1.length + 1, )ih:(insertionSortEquiv r (List.insertionSort r l1 ++ a :: l2)) l1.length, = (finCongr ) ((insertionSortEquiv r (l1 ++ a :: l2)) l1.length, )hl:List.insertionSort r (List.insertionSort r l1 ++ a :: l2) = List.insertionSort r (l1 ++ a :: l2)Fin.cast ((orderedInsertEquiv r (List.foldr (List.orderedInsert r) [] (List.foldr (List.orderedInsert r) [] l1 ++ a :: l2)) b) ((finCongr ) ((insertionSortEquiv r (l1 ++ a :: l2)) l1.length, )).succ) = Fin.cast ((orderedInsertEquiv r (List.foldr (List.orderedInsert r) [] (l1 ++ a :: l2)) b) ((insertionSortEquiv r (l1 ++ a :: l2)) l1.length, ).succ) erw [α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αl1:List αl2:List αhl✝:(insertionSortEquiv r (List.orderedInsert r b (List.insertionSort r l1) ++ a :: l2)) l1.length + 1, = Fin.cast ((insertionSortEquiv r (b :: (List.insertionSort r l1 ++ a :: l2))) l1.length + 1, )ih:(insertionSortEquiv r (List.insertionSort r l1 ++ a :: l2)) l1.length, = (finCongr ) ((insertionSortEquiv r (l1 ++ a :: l2)) l1.length, )hl:List.insertionSort r (List.insertionSort r l1 ++ a :: l2) = List.insertionSort r (l1 ++ a :: l2)Fin.cast (((Fin.castOrderIso ).trans ((orderedInsertEquiv r (List.insertionSort r (l1 ++ a :: l2)) b).trans (Fin.castOrderIso ).toEquiv)) ((finCongr ) ((insertionSortEquiv r (l1 ++ a :: l2)) l1.length, )).succ) = Fin.cast ((orderedInsertEquiv r (List.foldr (List.orderedInsert r) [] (l1 ++ a :: l2)) b) ((insertionSortEquiv r (l1 ++ a :: l2)) l1.length, ).succ)α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αl1:List αl2:List αhl✝:(insertionSortEquiv r (List.orderedInsert r b (List.insertionSort r l1) ++ a :: l2)) l1.length + 1, = Fin.cast ((insertionSortEquiv r (b :: (List.insertionSort r l1 ++ a :: l2))) l1.length + 1, )ih:(insertionSortEquiv r (List.insertionSort r l1 ++ a :: l2)) l1.length, = (finCongr ) ((insertionSortEquiv r (l1 ++ a :: l2)) l1.length, )hl:List.insertionSort r (List.insertionSort r l1 ++ a :: l2) = List.insertionSort r (l1 ++ a :: l2)Fin.cast (((Fin.castOrderIso ).trans ((orderedInsertEquiv r (List.insertionSort r (l1 ++ a :: l2)) b).trans (Fin.castOrderIso ).toEquiv)) ((finCongr ) ((insertionSortEquiv r (l1 ++ a :: l2)) l1.length, )).succ) = Fin.cast ((orderedInsertEquiv r (List.foldr (List.orderedInsert r) [] (l1 ++ a :: l2)) b) ((insertionSortEquiv r (l1 ++ a :: l2)) l1.length, ).succ) α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αl1:List αl2:List αhl✝:(insertionSortEquiv r (List.orderedInsert r b (List.insertionSort r l1) ++ a :: l2)) l1.length + 1, = Fin.cast ((insertionSortEquiv r (b :: (List.insertionSort r l1 ++ a :: l2))) l1.length + 1, )ih:(insertionSortEquiv r (List.insertionSort r l1 ++ a :: l2)) l1.length, = (finCongr ) ((insertionSortEquiv r (l1 ++ a :: l2)) l1.length, )hl:List.insertionSort r (List.insertionSort r l1 ++ a :: l2) = List.insertionSort r (l1 ++ a :: l2)Fin.cast (((Fin.castOrderIso ).trans ((orderedInsertEquiv r (List.insertionSort r (l1 ++ a :: l2)) b).trans (Fin.castOrderIso ).toEquiv)) (Fin.cast ((insertionSortEquiv r (l1 ++ a :: l2)) l1.length, )).succ) = Fin.cast ((orderedInsertEquiv r (List.foldr (List.orderedInsert r) [] (l1 ++ a :: l2)) b) ((insertionSortEquiv r (l1 ++ a :: l2)) l1.length, ).succ) All goals completed! 🐙

Insertion sort with equal fields

α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:IsTrans α ra:αp:α Propinst✝:DecidablePred ph:p ab:αl:List αhl:List.Pairwise r (b :: l)hpb:¬p bhab:¬r a bList.filter (fun b => decide (p b)) (List.orderedInsert r a l) = List.orderedInsert r a (List.filter (fun b => decide (p b)) l) α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:IsTrans α ra:αp:α Propinst✝:DecidablePred ph:p ab:αl:List αhpb:¬p bhab:¬r a bhl:(∀ a' l, r b a') List.Pairwise r lList.filter (fun b => decide (p b)) (List.orderedInsert r a l) = List.orderedInsert r a (List.filter (fun b => decide (p b)) l) All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙lemma takeWhile_sorted_eq_filter {α : Type} (r : α α Prop) [DecidableRel r] [IsTrans α r] (a : α) : (l : List α) (hl : l.Pairwise r) List.takeWhile (fun c => ¬ r a c) l = List.filter (fun c => ¬ r a c) l α:Typer:α α Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αx✝:List.Pairwise r []List.takeWhile (fun c => decide ¬r a c) [] = List.filter (fun c => decide ¬r a c) [] α:Typer:α α Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αx✝:List.Pairwise r []List.takeWhile (fun c => decide ¬r a c) [] = List.filter (fun c => decide ¬r a c) [] All goals completed! 🐙 α:Typer:α α Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:List.Pairwise r (b :: l)List.takeWhile (fun c => decide ¬r a c) (b :: l) = List.filter (fun c => decide ¬r a c) (b :: l) α:Typer:α α Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:List.Pairwise r (b :: l)List.takeWhile (fun c => decide ¬r a c) (b :: l) = List.filter (fun c => decide ¬r a c) (b :: l) α:Typer:α α Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' l, r b a') List.Pairwise r lList.takeWhile (fun c => decide ¬r a c) (b :: l) = List.filter (fun c => decide ¬r a c) (b :: l) α:Typer:α α Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' l, r b a') List.Pairwise r lhb:¬r a bList.takeWhile (fun c => decide ¬r a c) (b :: l) = List.filter (fun c => decide ¬r a c) (b :: l)α:Typer:α α Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' l, r b a') List.Pairwise r lhb:¬¬r a bList.takeWhile (fun c => decide ¬r a c) (b :: l) = List.filter (fun c => decide ¬r a c) (b :: l) α:Typer:α α Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' l, r b a') List.Pairwise r lhb:¬r a bList.takeWhile (fun c => decide ¬r a c) (b :: l) = List.filter (fun c => decide ¬r a c) (b :: l) α:Typer:α α Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' l, r b a') List.Pairwise r lhb:¬r a bList.takeWhile (fun c => !decide (r a c)) l = List.filter (fun c => !decide (r a c)) l All goals completed! 🐙 α:Typer:α α Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' l, r b a') List.Pairwise r lhb:¬¬r a bList.takeWhile (fun c => decide ¬r a c) (b :: l) = List.filter (fun c => decide ¬r a c) (b :: l) α:Typer:α α Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' l, r b a') List.Pairwise r lhb:r a b a_1 l, r a a_1 All goals completed! 🐙α:Typer:α α Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' l, r b a') List.Pairwise r lhb:r a b a_1 l, decide (r a a_1) = true α:Typer:α α Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' l, r b a') List.Pairwise r lhb:r a bc:αhc:c ldecide (r a c) = true All goals completed! 🐙α:Typer:α α Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' l, r b a') List.Pairwise r lhb:r a bhba:¬r b ah1:List.filter (fun c => decide (r a c) && decide (r c a)) l = [](decide (r a b) && !decide (r b a)) = trueα:Typer:α α Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' l, r b a') List.Pairwise r lhb:r a bhba:¬r b ah1:List.filter (fun c => decide (r a c) && decide (r c a)) l = []List.Pairwise r l α:Typer:α α Propinst✝¹:DecidableRel rinst✝:IsTrans α ra:αb:αl:List αhl:(∀ a' l, r b a') List.Pairwise r lhb:r a bhba:¬r b ah1:List.filter (fun c => decide (r a c) && decide (r c a)) l = []List.Pairwise r l All goals completed! 🐙α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αl:List αh:¬(r a b r b a)hl:List.filter (fun b => decide (r a b) && decide (r b a)) (List.orderedInsert r b (List.insertionSort r l)) = List.filter (fun b => decide (r a b) && decide (r b a)) (List.insertionSort r l)List.filter (fun b => decide (r a b) && decide (r b a)) (List.insertionSort r l) = List.filter (fun c => decide (r a c) && decide (r c a)) lα:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αl:List αh:¬(r a b r b a)hl:List.filter (fun b => decide (r a b) && decide (r b a)) (List.orderedInsert r b (List.insertionSort r l)) = List.filter (fun b => decide (r a b) && decide (r b a)) (List.insertionSort r l)¬(decide (r a b) && decide (r b a)) = true α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αl:List αh:¬(r a b r b a)hl:List.filter (fun b => decide (r a b) && decide (r b a)) (List.orderedInsert r b (List.insertionSort r l)) = List.filter (fun b => decide (r a b) && decide (r b a)) (List.insertionSort r l)ih:List.filter (fun c => decide (r a c r c a)) (List.insertionSort r l) = List.filter (fun c => decide (r a c r c a)) lList.filter (fun b => decide (r a b) && decide (r b a)) (List.insertionSort r l) = List.filter (fun c => decide (r a c) && decide (r c a)) lα:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αl:List αh:¬(r a b r b a)hl:List.filter (fun b => decide (r a b) && decide (r b a)) (List.orderedInsert r b (List.insertionSort r l)) = List.filter (fun b => decide (r a b) && decide (r b a)) (List.insertionSort r l)¬(decide (r a b) && decide (r b a)) = true α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αb:αl:List αh:¬(r a b r b a)hl:List.filter (fun b => decide (r a b) && decide (r b a)) (List.orderedInsert r b (List.insertionSort r l)) = List.filter (fun b => decide (r a b) && decide (r b a)) (List.insertionSort r l)¬(decide (r a b) && decide (r b a)) = true All goals completed! 🐙α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αl1:List αl:List αl2:List αh: b l, r a b r b ahlt:List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l ++ l2)) = List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l2))h1✝:List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2))) List.dropWhile (fun c => !decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2))) = List.filter (fun c => decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2)))h1:List.insertionSort r (List.filter (fun b => decide (r a b) && !decide (r b a)) l1 ++ (List.filter (fun b => decide (r a b) && !decide (r b a)) l ++ List.filter (fun b => decide (r a b) && !decide (r b a)) l2)) = List.filter (fun b => decide (r a b) && !decide (r b a)) (List.insertionSort r (l1 ++ (l ++ l2)))h2:List.insertionSort r (List.filter (fun b => decide (r a b) && !decide (r b a)) l1 ++ List.filter (fun b => decide (r a b) && !decide (r b a)) l2) = List.filter (fun b => decide (r a b) && !decide (r b a)) (List.insertionSort r (l1 ++ l2))hl:List.filter (fun b => decide (r a b) && !decide (r b a)) l = [][] ++ List.filter (fun b => decide (r a b) && !decide (r b a)) l2 = List.filter (fun b => decide (r a b) && !decide (r b a)) l2α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αl1:List αl:List αl2:List αh: b l, r a b r b ahlt:List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l ++ l2)) = List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l2))h1:List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2))) List.dropWhile (fun c => !decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2))) = List.filter (fun c => decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2)))List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2)))α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αl1:List αl:List αl2:List αh: b l, r a b r b ahlt:List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l ++ l2)) = List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l2))h1:List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2))) List.dropWhile (fun c => !decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2))) = List.filter (fun c => decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2)))List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2))) α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αl1:List αl:List αl2:List αh: b l, r a b r b ahlt:List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l ++ l2)) = List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l2))h1:List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2))) List.dropWhile (fun c => !decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2))) = List.filter (fun c => decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2)))List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2)))α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αl1:List αl:List αl2:List αh: b l, r a b r b ahlt:List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l ++ l2)) = List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l2))h1:List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2))) List.dropWhile (fun c => !decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2))) = List.filter (fun c => decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2)))List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2))) α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αl1:List αl:List αl2:List αh: b l, r a b r b ahlt:List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l ++ l2)) = List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l2))h1:List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2))) List.dropWhile (fun c => !decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2))) = List.filter (fun c => decide (r a c)) (List.insertionSort r (l1 ++ (l ++ l2)))List.Pairwise r (List.insertionSort r (l1 ++ (l ++ l2))) All goals completed! 🐙lemma insertionSort_of_takeWhile_filter {α : Type} (r : α α Prop) [DecidableRel r] [Std.Total r] [IsTrans α r] (a : α) (l1 l2 : List α) : List.insertionSort r (l1 ++ l2) = (List.takeWhile (fun c => ¬ r a c) ((l1 ++ l2).insertionSort r)) ++ (List.filter (fun c => r a c r c a) l1) ++ (List.filter (fun c => r a c r c a) l2) ++ (List.filter (fun c => r a c ¬ r c a) ((l1 ++ l2).insertionSort r)) := α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αl1:List αl2:List αList.insertionSort r (l1 ++ l2) = List.takeWhile (fun c => decide ¬r a c) (List.insertionSort r (l1 ++ l2)) ++ List.filter (fun c => decide (r a c r c a)) l1 ++ List.filter (fun c => decide (r a c r c a)) l2 ++ List.filter (fun c => decide (r a c ¬r c a)) (List.insertionSort r (l1 ++ l2)) simpa using insertionSort_of_eq_list r a l1 [] l2 (α:Typer:α α Propinst✝²:DecidableRel rinst✝¹:Std.Total rinst✝:IsTrans α ra:αl1:List αl2:List α b [], r a b r b a All goals completed! 🐙)