Lemmas involving sizeOf, which are located here rather than in Cedar/Thm because they are needed for some definitions in Cedar/Spec and/or Cedar/Partial, and our convention prevents files in Cedar/Spec or Cedar/Partial from depending on lemmas in Cedar/Thm.

List

theorem Cedar.Data.List.sizeOf_attach₂ {α : Type u_1} {β : Type u_2} [SizeOf α] [SizeOf β] {a : α} {b : β} {l : List (α × β)} : (a, b) ∈ l → sizeOf (a, b).snd < 1 + sizeOf l

theorem Cedar.Data.List.sizeOf_attach₃ {α : Type u_1} {β : Type u_2} [SizeOf α] [SizeOf β] {a : α} {b : β} {l : List (α × β)} : (a, b) ∈ l → sizeOf (a, b).snd < 1 + (1 + sizeOf l)

Map

theorem Cedar.Data.Map.sizeOf_lt_of_value {α : Type u_1} {β : Type u_2} [SizeOf α] [SizeOf β] {m : Map α β} {k : α} {v : β} (h : (k, v) ∈ m.1) : sizeOf v < sizeOf m

theorem Cedar.Data.Map.sizeOf_lt_of_find? {α : Type u_1} {β : Type u_2} [SizeOf α] [SizeOf β] [DecidableEq α] {m : Map α β} {k : α} {v : β} (h : m.find? k = some v) : sizeOf v < sizeOf m

theorem Cedar.Data.Map.sizeOf_lt_of_toList {α : Type u_1} {β : Type u_2} [SizeOf α] [SizeOf β] (m : Map α β) : sizeOf m.toList < sizeOf m

theorem Cedar.Data.Map.sizeOf_lt_of_values {α : Type u_1} {β : Type u_2} {b : β} [SizeOf α] [SizeOf β] {m : Map α β} (h : b ∈ m.values) : sizeOf b < sizeOf m

theorem Cedar.Data.Map.sizeOf_lt_of_tl {α : Type u_1} {β : Type u_2} {k : α} {v : β} [SizeOf α] [SizeOf β] {m : Map α β} {tl : List (α × β)} (h : m.toList = (k, v) :: tl) : 1 + sizeOf tl < sizeOf m

Set

theorem Cedar.Data.Set.sizeOf_lt_of_mem {α : Type u_1} {a : α} [SizeOf α] {s : Set α} (h : a ∈ s) : sizeOf a < sizeOf s

theorem Cedar.Data.Set.sizeOf_lt_of_elts {α : Type u_1} [SizeOf α] (s : Set α) : sizeOf s.elts < sizeOf s

theorem Cedar.Data.Set.sizeOf_mk {α : Type u_1} [SizeOf α] (xs : List α) : sizeOf (mk xs) = 1 + sizeOf xs