You are an expert Lean4 and formal verification agent proving a Lean4 theorem. Your output **must** strictly adhere to the specified format.

### Input Information
You will receive the following components, relevant to the target theorem:
* <all_available_defs>: Definitions available from imported modules (either from the current Lean repository or from Mathlib)
* <all_available_lemmas>: Lemmas/theorems available that may assist the proof.
* <local_ctx>...</local_ctx>: The local file context (imports, namespaces, definitions, comments, etc.) from the top of the file up to—but not including—the target theorem or any previously defined local lemmas/theorems.
* <target_theorem>...</target_theorem>: The target theorem statement, ending with `:=`.

**Notes**
1. Definitions include their full bodies, but for definitions whose bodies contain proofs, the proof parts are replaced by `admit` (i.e., admit /- proof elided -/), while the rest of the definition is kept unchanged; lemmas include only their statements.
2. You may freely reference any definition or lemma contained in these tags without redefining them.
3. The tags for available definitions and lemmas (all_available_defs, all_available_lemmas) may be omitted if empty.

### Output Format & Requirements
Your output MUST contain a complete, syntactically correct Lean 4 proof for the target theorem.

**Strict Output Structure:**
<reasoning> 
...
</reasoning> 

<lean4_invented_lemmas>
-- each lemma is a full Lean 4 declaration with a complete proof
...
</lean4_invented_lemmas>

<lean4_proof>
-- Lean 4 proof body of the target theorem
...
</lean4_proof>

**Requirements:**
1. <reasoning> and <lean4_invented_lemmas> are OPTIONAL. Include them only if they aid proof construction.
2. <lean4_proof> MUST contain only the proof body (tactics/terms), starting by "by", NOT the theorem declaration.
3. <lean4_invented_lemmas> (if present) MUST contain syntactically correct lemma declarations that type checks AND complete proof bodies. Defining a lemma using `axiom` is NOT allowed.
4. <reasoning> contains high-level proof planning.
5. If you create a lemma under <lean4_invented_lemmas> whose name is namespaced (e.g., X.Y.Z), you MUST always refer to it using its fully qualified name. Do NOT rely on shortened names. For example, write rw [X.Y.Z], not rw [Z] for invented lemmas.
6. All Lean 4 code MUST be syntactically correct. No `sorry`, `admit`, or non-Lean text. Comments allowed using `--` or `/- ... -/`.
7. Follow the tags and structure EXACTLY. No extra text before, between, or after the sections.
8. Do NOT wrap invented lemmas in a `mutual` block unless they have genuine mutual recursion. Declare each lemma independently.

### Examples are provided here (example input are under "User Prompt", and example assistant response are under "Agent Response"):
Example 1 ------------------- 
User Prompt:
<all_available_defs>
structure BitVec (w : Nat) where
  /-- Construct a `BitVec w` from a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  ofFin ::

  /-- Interpret a bitvector as a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (hPow 2 w)
</all_available_defs>

<all_available_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) : (l₁ ++ l₂)[i] = l₁[i]
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
  x[i] = x.toNat.testBit i := rfl
@[simp, grind =] theorem toNat_cons (b : Bool) (x : BitVec w) :
    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat
@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i
</all_available_lemmas>

<local_ctx>
import Mathlib.Computability.NFA
import Mathlib.Data.FinEnum
import Mathlib.Data.Rel
import Mathlib.Data.Vector.Basic
import Blase.AutoStructs.ForLean

open Set
open Mathlib
open SetRel

-- this is better because card is defeq to n
instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩
instance (α : Type) : Union (Language α) := ⟨Set.union⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width.
-/
structure BitVecs (n : Nat) where
  w : Nat
  bvs : List.Vector (BitVec w) n

def BitVecs.cast (bvs : BitVecs n) (h : n = n') : BitVecs n' :=
  { w := bvs.w, bvs := h ▸ bvs.bvs }

abbrev BitVecs.empty : BitVecs n := ⟨0, List.Vector.replicate n .nil⟩
abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩
abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width, encoded as a list of
bit vectors of width `n`. The width of the encoded bit vectors is the length of
the list.
-/
abbrev BitVecs' (n : Nat) := List (BitVec n)

@[simps]
def dec (bvs' : BitVecs' n) : BitVecs n where
  w := bvs'.length
  bvs := List.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k

@[simp]
</local_ctx>

<target_theorem>
lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) :
  dec (bvs' ++ [a]) =
    { w := bvs'.length + 1
      bvs := List.Vector.ofFn fun k =>
        BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } :=
</target_theorem>

Agent Response:
<reasoning> 
The goal is to understand what `dec` does after appending one more bitvector `a` to `bvs'`. By definition, `dec` builds a width `= length` and a vector of bitvectors whose `i`-th bit at position `k` is `bvs'[i].getLsbD k`. So for `bvs' ++ [a]`, we expect the width to increase by 1 and each resulting bitvector to be `BitVec.cons` of the new bit coming from `a`.

First, I use `ext` twice: once on the record to focus on the `bvs` field, and once on the resulting bitvector. This reduces everything to a pointwise statement:
for fixed `k` and `i` with `i < bvs'.length + 1`,
the bit `(bvs' ++ [a])[i].getLsbD k` should match the bit at index `i` of `BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k)`.

At this point I need a clean description of indexing into `BitVec.cons`: if we have `x : BitVec n`, then `(cons b x)[i]` should give `b` at the new “last” index `n` and `x[i]` otherwise. That motivates an auxiliary lemma `getElem_cons` expressing exactly this behavior, proved via the `testBit`/`toNat` characterization and a case split on `i < n`, `i = n`, `i > n`.

Using `getElem_cons`, the RHS becomes an `if` on whether `i = bvs'.length`. So I split into cases:
- If `i = bvs'.length`, then `(bvs' ++ [a])[i]` is the appended `a`, so both sides reduce to `a.getLsbD k`.
- If `i ≠ bvs'.length`, the bound `i < bvs'.length + 1` forces `i < bvs'.length`. Then `(bvs' ++ [a])[i] = bvs'[i]` by `List.getElem_append_left`, and the RHS takes the “else” branch and likewise gives the bit from `bvs'[i]`. In both subcases, `simp` (plus the definition of `dec`) finishes.

So the whole proof is: `ext` to bit level, unfold `dec` with `simp_all`, rewrite with `getElem_cons`, split on the boundary index `i = length bvs'`, and in the “< length” branch use `List.getElem_append_left` and bounds to line up both sides.
</reasoning> 

<lean4_invented_lemmas>
@[grind =]
theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
    (cons b x)[i] = if h : i = n then b else x[i] := by
  simp only [BitVec.getElem_eq_testBit_toNat, BitVec.toNat_cons, Nat.testBit_or]
  rw [Nat.testBit_shiftLeft]
  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
  · have p1 : ¬(n ≤ i) := by omega
    have p2 : i ≠ n := by omega
    simp [p1, p2]
  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
    Bool.true_and, BitVec.testBit_toNat, BitVec.getLsbD_of_ge, Bool.or_false]
    cases b <;> trivial
  · have p1 : i ≠ n := by omega
    have p2 : i - n ≠ 0 := by omega
    simp [p1, p2, Nat.testBit_bool_toNat]
</lean4_invented_lemmas>

<lean4_proof>
by
  ext k i hi <;> simp_all
  rw [getElem_cons]
  split
  next heq => simp_all
  next h =>
    have hlt : i < List.length bvs' := by simp at hi; omega
    rw [List.getElem_append_left hlt]
    simp
</lean4_proof>

### Your task:
<all_available_defs>
structure CommitT (C K Pi : Type) where
  commitment : C
  dict       : Dict K Pi

abbrev keys (ct : CommitT C K Pi) := ct.dict.keys

inductive Block (K₁ K₂ : Type) (C Sigma : Type) (V : Type) [PreWithZero V] where
   
  | deposit (recipient : K₂) (amount : V₊)
   
  | transfer (aggregator : K₁) (extradata : ExtraDataT) (commitment : C) (senders : List K₂) (sigma : Sigma)
   
  | withdrawal (withdrawals : K₁ → V₊)

abbrev isDepositBlock (b : Block K₁ K₂ C Sigma V) := b matches (Block.deposit _ _)

abbrev isTransferBlock (b : Block K₁ K₂ C Sigma V) := b matches (Block.transfer _ _ _ _ _)

abbrev isWithdrawalBlock (b : Block K₁ K₂ C Sigma V) := b matches (Block.withdrawal _)

abbrev BalanceProof (K₁ K₂ : Type) [Finite K₁] [Finite K₂]
                    (C Pi V : Type) [PreWithZero V] : Type :=
  Dict (C × K₂) ((Pi × ExtraDataT) × TransactionBatch K₁ K₂ V)

abbrev Dict (α ω : Type) : Type := α → Option ω

def Dict.is_mem (m : Dict α ω) (x : α) : Prop := (m x).isSome

def keys (m : Dict α ω) : Set α := { x | Dict.is_mem m x }

abbrev Key (K₁ K₂ : Type) := K₁ ⊕ K₂

inductive Kbar (K₁ K₂ : Type) where
  | key (k : Key K₁ K₂)
  | Source
deriving DecidableEq

def lexLe (a b : K₂ × Key K₁ K₂) : Prop :=
  a.1 < b.1 ∨ (a.1 = b.1 ∧ a.2 ≤ b.2)

abbrev keysUneq (k₂ : K₂) (k : Key K₁ K₂) : Prop :=
  match k with
  | .inl _   => True
  | .inr k₂' => k₂ ≠ k₂'

abbrev ExtraDataT : Type := ℕ

abbrev Τ' (K₁ K₂ V : Type) [PreWithZero V] := Kbar K₁ K₂ × Kbar K₁ K₂ × Option V₊

abbrev Τ (K₁ K₂ V : Type) [PreWithZero V] := { τ : Τ' K₁ K₂ V // τ.isValid }

abbrev TransactionBatch (K₁ : Type) [Finite K₁]
                        (K₂ : Type) [Finite K₂]
                        (V : Type) [PreWithZero V] :=
  Key K₁ K₂ → V₊

class Injective {α ω : Type} (f : α → ω) where
  h : ComputationallyInfeasible (¬ Function.Injective f)

abbrev UniqueTokenT (α : Type) [Finite α] : Type := Fin (Finite.exists_equiv_fin α |>.choose)

abbrev UniquelyIndexed (α : Type) [Finite α] : Type := α ↪ !α

noncomputable def attach (α : Type) [Finite α] : UniquelyIndexed α :=
  have := Finite.exists_equiv_fin α
  this.choose_spec.some.toEmbedding

def NonNeg (α : Type) [PreWithZero α] := { a : α // 0 ≤ a }

local macro:max (priority := high) "↪" b:term : term => `(⟨$b, by admit /- proof elided -/
⟩)

Zero in Init.Prelude

Inhabited in Init.Prelude

def computeBalance (blocks : Scontract K₁ K₂ V C Sigma) : V :=
  computeBalance' blocks 0

class SignatureAggregation (M Kₚ Kₛ Sigma : Type) where
  KeyGen    : SimpleRandom.Seed → Kₚ × Kₛ
  Sign      : Kₛ → M → Sigma
  Aggregate : List (Kₚ × Sigma) → Sigma
  Verify    : List Kₚ → M → Sigma → Bool

Option in Init.Prelude

instance : Nonempty ExtraDataT := inferInstanceAs (Nonempty ℕ)

def BalanceProof.initial : BalanceProof K₁ K₂ C Pi V := λ _ ↦ .none

Int in Init.Data.Int.Basic

noncomputable instance : Fintype K₁ := Fintype.ofFinite _

def Key.lt (k₁ k₂ : Key K₁ K₂) : Prop :=
  match k₁, k₂ with
  | .inl k₁, .inl k₁' => k₁ < k₁'
  | .inl _,  .inr _   => True
  | .inr _,  .inl _   => False
  | .inr k₂, .inr k₂' => k₂ < k₂'

instance [Finite K₁] [Finite K₂] : Preorder (TransactionBatch K₁ K₂ V) := discretePreorder

def isValid (s : S' K₁ K₂ V) := ∀ k : Kbar K₁ K₂, k matches .Source ∨ 0 ≤ s k

noncomputable instance : Fintype K₂ := Fintype.ofFinite _

PartialOrder in Mathlib.Order.Defs.PartialOrder

Preorder in Mathlib.Order.Defs.PartialOrder

absurd in Init.Prelude

instance (priority := high) : LE (Kbar K₁ K₂) := ⟨(·=·)⟩

reduceDIte in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core

lowerBounds in Mathlib.Order.Bounds.Defs

def lookup_h [DecidableEq α] {a : α}
  (s : Finmap β) (h : a ∈ s) : β a := s.lookup a |>.get (Option.isSome_iff_exists.2 (Finmap.mem_iff.1 h))

def TransactionsInBlock_transfer 
  (π : BalanceProof K₁ K₂ C Pi V) (b : { b : Block K₁ K₂ C Sigma V // b.isTransferBlock }) : List (Τ K₁ K₂ V) :=
  match h : b.1 with
  | .transfer _ _ commitment S _ =>
     
    let senderRecipient : Finset (K₂ × Key K₁ K₂) := { (k₂, k) | (k₂ : K₂) (k : Key K₁ K₂) (_h : k₂ ≠ₖ k) }
    let sorted : List (K₂ × Key K₁ K₂) := senderRecipient.sort Key.lexLe 
     
    let v (s : K₂) (r : Key K₁ K₂) : Option V₊ :=
      if s ∉ S
      then .some 0
      else 
        if h : (commitment, s) ∈ π.keys
        then let (_, t) := π[(commitment, s)]
             t r
        else .none
    sorted.attach.map λ ⟨(s, r), h⟩ ↦ ⟨(s, r, v s r), by admit /- proof elided -/
    ⟩
  | .deposit .. | .withdrawal .. => by admit /- proof elided -/

Decidable in Init.Prelude

Finset in Mathlib.Data.Finset.Defs

private instance [(a b : K₁) → Decidable (a ≤ b)] [(a b : K₂) → Decidable (a ≤ b)] :
         (a b : Key K₁ K₂) → Decidable (a ≤ b) :=
  λ a b ↦ by
    dsimp [(·≤·), Key.le]
    rcases a with a | a <;> rcases b with b | b <;> infer_instance

noncomputable instance : Fintype (Key K₁ K₂) :=
  have := Fintype.ofFinite K₁
  have := Fintype.ofFinite K₂
  have : Finite (Key K₁ K₂) := inferInstance
  Fintype.ofFinite (Key K₁ K₂)

Finite in Mathlib.Data.Finite.Defs

LE in Init.Prelude

id in Init.Prelude

def isValid (τ : Τ' K₁ K₂ V) :=
  match τ with
  | (s, r, v) => s ≠ r ∧ (s matches .Source → v.isSome)

def attackGameR : Scontract K₁ K₂ V C Sigma :=
  σ ++ attackGameRGo requests σ

class ADScheme (K : Type)
               (M : Type)
               (C Pi : Type) where
  Commit : Dict K M → CommitT C K Pi
  Verify : Pi → K → M → C → Bool

instance [PreWithZero V] : Coe (Τc K₁ K₂ V) (Τ K₁ K₂ V) := ⟨(↑·)⟩

correct_consistent :
    ∀ {dict : Dict K M} {key : K} (h : key ∈ dict.keys), 
      Verify (Commit dict)[key] key dict[key] (Commit dict).commitment = true

def mkTransferBlock (aggregator : K₁) (extradata : ExtraDataT)
                    (commitment : C) (senders : List K₂) (sigma : Sigma) : Block K₁ K₂ C Sigma V :=
  transfer aggregator extradata commitment senders sigma

Sum in Init.Core

def Merge (D₁ D₂ : Dict α ω) : Dict α ω := D
  where D := λ x ↦ First (D₁ x) (D₂ x)

List.Ico in Mathlib.Data.List.Intervals

def aggregateWithdrawals' (σ : Scontract K₁ K₂ V C Sigma) : V :=
  ∑ (i : Fin σ.length × K₁),
    if h : σ[i.1].isWithdrawalBlock
    then (σ[i.1].getWithdrawal h) i.2
    else 0

instance : Preorder (Kbar K₁ K₂ × Kbar K₁ K₂) := inferInstance

def exists_inf (b : S K₁ K₂ V) (T : Τ K₁ K₂ V) : { s : S K₁ K₂ V // ∀ k, IsGLB (V' b T k) (s k) } :=
  ⟨
    f' b T,
    λ k ↦
      have f'_codomain : (f' b T) k ∈ V' b T k := by admit /- proof elided -/
  ⟩

def Bal (π : BalanceProof K₁ K₂ C Pi V) (bs : List (Block K₁ K₂ C Sigma V)) : S K₁ K₂ V :=
  fStar (TransactionsInBlocks π bs) (.initial K₁ K₂ V)

IsTrans in Mathlib.Order.Defs.Unbundled

Multiset in Mathlib.Data.Multiset.Defs

def getDeposit (b : Block K₁ K₂ C Sigma V) (_h : b.isDepositBlock) : K₂ × V₊ :=
  match b with | deposit r v => (r, v)

def mkDepositBlock (K₁ C Sigma : Type) (addr : K₂) (value : V₊) : Block K₁ K₂ C Sigma V :=
  deposit addr value

Multiset.dedup in Mathlib.Data.Multiset.Dedup

def Request.isValid (request : Request K₁ K₂ C Sigma Pi V) : Bool :=
  match request with
   
  | deposit .. =>
      true
   
  | transfer aggregator extradata commitment senders sigma =>
      let isValidSA := SA.Verify senders (commitment, aggregator, extradata) sigma
      let isValidAggregator := aggregator = AgreedUponAggregator
      isValidSA ∧ isValidAggregator
   
  | withdrawal π =>
      π.Verify (M := (C × K₁ × ExtraDataT))

Sum.inl in Init.Core

noncomputable instance {α : Type} [Lattice α] [Zero α] : PreWithZero α := inferInstance

def initial (K₁ K₂ V : Type) [PreWithZero V] : S K₁ K₂ V :=
  ⟨S'.initial K₁ K₂ V, S'.isValid_initial⟩

private instance [IsTrans K₁ (·≤·)] [IsTrans K₂ (·≤·)] : IsTrans (Key K₁ K₂) (·≤·) :=
  {
    trans := λ a b c ↦ by
      dsimp [(·≤·), Key.le]; intros h₁ h₂
      aesop (add safe forward IsTrans.trans)
  }

def attackGameBlocks'! : Scontract K₁ K₂ V C Sigma :=
  requests.foldl Scontract.appendBlock! σ

Subtype.mk in Init.Prelude

instance : Finite (Key K₁ K₂) :=

Sum.inr in Init.Core

IsTotal in Mathlib.Order.Defs.Unbundled

instance : Preorder (Option V₊) := inferInstance

List.zipWith in Init.Data.List.Basic

Int.reduceAdd in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int

Subtype.val in Init.Prelude

instance (priority := high) : LE (Vector α n) := ⟨le⟩

IsAntisymm in Mathlib.Order.Defs.Unbundled

List.zip in Init.Data.List.Basic

instance : Coe (Key K₁ K₂) (Kbar K₁ K₂) := ⟨.key⟩

Unit in Init.Prelude

Fin in Init.Prelude

instance : Preorder (Τ K₁ K₂ V) := inferInstance

def appendBlock! (σ : Scontract K₁ K₂ V C Sigma)
                 (request : Request K₁ K₂ C Sigma Pi V) : Scontract K₁ K₂ V C Sigma :=
  σ ++ [request.toBlock! σ]

Classical.arbitrary in Mathlib.Logic.Nonempty

def trivialPreorder {α : Type} : Preorder α :=
  {
    lt := λ _ _ ↦ False
    le := λ _ _ ↦ True
    le_refl := by admit /- proof elided -/

Coe in Init.Coe

instance : Coe K₂ (Key K₁ K₂) := ⟨.inr⟩

Finset.range in Mathlib.Data.Finset.Range

instance [Finite K₁] [Finite K₂] : Preorder (BalanceProof K₁ K₂ C Pi V) :=

def Key.le (k₁ k₂ : Key K₁ K₂) : Prop :=
  match k₁, k₂ with
  | .inl k₁, .inl k₁' => k₁ ≤ k₁'
  | .inl _,  .inr _   => True
  | .inr _,  .inl _   => False
  | .inr k₂, .inr k₂' => k₂ ≤ k₂'

Multiset.keys in Mathlib.Data.Finmap

abbrev KₛT : Type := ℕ

instance [Finite K₁] [Finite K₂] : Preorder ((Pi × ExtraDataT) × TransactionBatch K₁ K₂ V) := inferInstance

flip in Init.Core

def attackGameBlocks! (requests : List (Request K₁ K₂ C Sigma Pi V)) : Scontract K₁ K₂ V C Sigma :=
  attackGameBlocks'! requests []

instance {k₂ : K₂} {k : Key K₁ K₂} [DecidableEq K₂] : Decidable (k₂ ≠ₖ k) :=

Preorder.toLE in Mathlib.Order.Defs.PartialOrder

Finset.toList in Mathlib.Data.Finset.Dedup

InfSet in Mathlib.Order.SetNotation

def BalanceProof.compat (π₁ π₂ : BalanceProof K₁ K₂ C Pi V) : Prop :=
  ∀ k, π₁ k ≠ none ∧ π₂ k ≠ none → π₁ k ≅ π₂ k

def V' (b : S K₁ K₂ V) (T : Τ K₁ K₂ V) (k : Kbar K₁ K₂) : Set V :=
  { v : V | v ∈ (fc · k) '' boundedBelow b T }

def TransactionsInBlock_withdrawal 
  (b : { b : Block K₁ K₂ C Sigma V // b.isWithdrawalBlock }) : List (Τ K₁ K₂ V) :=
  match h : b.1 with
  | .withdrawal withdrawals =>
     
    let k₁InOrder := { s | s : K₁ }.toFinset.sort (·≤·)
    k₁InOrder.attach.map λ s : K₁ ↦ ⟨(s, .Source, withdrawals s), by admit /- proof elided -/
    ⟩
  | .deposit r v | .transfer .. => by admit /- proof elided -/

List.foldl in Init.Prelude

Set.Ici in Mathlib.Order.Interval.Set.Defs

def appendBlock (σ : Scontract K₁ K₂ V C Sigma)
                (request : Request K₁ K₂ C Sigma Pi V) : Scontract K₁ K₂ V C Sigma :=
  (request.toBlock σ).elim σ (σ ++ [·])

Prod.mk in Init.Prelude

Sigma in Init.Core

instance : Preorder (Kbar K₁ K₂ × Kbar K₁ K₂ × Option V₊) := inferInstance

Monotone in Mathlib.Order.Monotone.Defs

abbrev S' (K₁ K₂ V : Type) := Kbar K₁ K₂ → V

instance (priority := high) vectorPreorder : Preorder (Vector α n) where
  le_refl := λ _ ↦ Vec.le_refl
  le_trans := λ _ _ _ ↦ Vec.le_trans

abbrev boundedBelow (b : S K₁ K₂ V) (T : Τ K₁ K₂ V) :=
  { a : Τc K₁ K₂ V × S K₁ K₂ V | (T, b) ≤ (↑a.1, a.2) }

instance [CovariantClass V V (· + ·) (· ≤ ·)] : OrderedAddCommMonoid V := ⟨by admit /- proof elided -/
⟩

IsLeast in Mathlib.Order.Bounds.Defs

def f (b : S K₁ K₂ V) (T : Τ K₁ K₂ V) : S K₁ K₂ V :=
  ⟨
    λ k ↦
      have : InfSet V := infV b T k
      ⨅ x : boundedBelow b T, fc x.1 k,
    by admit /- proof elided -/
  ⟩

List.NodupKeys in Mathlib.Data.List.Sigma

private abbrev length_of_TransactionsInBlocks (bs : List (Block K₁ K₂ C Sigma V)) :
  { n : ℕ // n = (TransactionsInBlocks (Classical.arbitrary _ : BalanceProof K₁ K₂ C Pi V) bs).length } :=
  ⟨(TransactionsInBlocks (Classical.arbitrary _ : BalanceProof K₁ K₂ C Pi V) bs).length, rfl⟩

def Verify (π : BalanceProof K₁ K₂ C Pi V)
           [AD : ADScheme K₂ M C Pi] : Bool :=
  ∀ x, (h : x ∈ Dict.keys π) → let ((π', salt), t) := (π x).get (by admit /- proof elided -/
  )
                               AD.Verify π' x.2 (H _ (t, salt)) x.1

instance : LT (Key K₁ K₂) := ⟨Key.lt⟩

Multiset.Nodup in Mathlib.Data.Multiset.Defs

def normalise (requests : List (Request K₁ K₂ C Sigma Pi V)) : List (Request K₁ K₂ C Sigma Pi V) :=
  requests.filter Request.isValid

Multiset.ofList in Mathlib.Data.Multiset.Defs

Function.Injective in Init.Data.Function

instance : Coe K₁ (Key K₁ K₂) := ⟨.inl⟩

def isRandom (f : Seed → α) (x : α) := ∃ seed, x = f seed

abbrev KₚT : Type := ℕ

DecidableRel in Init.Prelude

reduceCtorEq in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core

List.attach in Init.Data.List.Attach

def adversaryWon (blocks : Scontract K₁ K₂ V C Sigma) : Prop :=
  ¬0 ≤ computeBalance blocks

Finset.sort in Mathlib.Data.Finset.Sort

def toBlock! (σ : Scontract K₁ K₂ V C Sigma)
             (request : Request K₁ K₂ C Sigma Pi V) : Block K₁ K₂ C Sigma V :=
  match request with
  | .deposit r v            => .deposit r v
  | .transfer a e c s sigma => .transfer a e c s sigma
  | .withdrawal π           => .withdrawal (π.toBalanceF σ)

private def BalFixed' (bs : List (Block K₁ K₂ C Sigma V)) : BalanceProof K₁ K₂ C Pi V → S K₁ K₂ V :=
  fStarFixed (n := (length_of_TransactionsInBlocks (Pi := Pi) bs).1)
             (s₀ := S.initial K₁ K₂ V) ∘ TransactionsInBlocksFixed (Pi := Pi) (bs := bs)

noncomputable def univFinmap (K : Type) [Fintype K] [DecidableEq K]
                             (V : Type) [DecidableEq V] :
  { m : Finmap (λ _ : K ↦ V) // ∀ k, k ∈ m } ≃ (K → V) :=
  {
    toFun := λ m k ↦ m.1.lookup_h (a := k) (m.2 k)
    invFun := λ f ↦
      let keys : Finset K := Finset.univ
      ⟨⟨
        Multiset.ofList <| keys.toList.zipWith (f := Sigma.mk) (keys.toList.map f),
        by admit /- proof elided -/
       ⟩,
        by admit /- proof elided -/
           ⟩
    left_inv := by admit /- proof elided -/

List.lookup in Init.Data.List.Basic

GetElem in Init.GetElem

instance [PreWithZero V] : Inhabited (S K₁ K₂ V) := ⟨S.initial K₁ K₂ V⟩

instance : Coe K₁ (Key K₁ K₂) := ⟨.inl⟩

Sigma.fst in Init.Core

def value (τ : Τ K₁ K₂ V) : Option V₊ := τ.1.2.2

instance : CoeFun (S K₁ K₂ V) λ _ ↦ Kbar K₁ K₂ → V :=
  ⟨λ s k ↦ s.1 k⟩

Finmap in Mathlib.Data.Finmap

abbrev Τc (K₁ K₂ V : Type) [PreWithZero V] : Type := { τ : Τ K₁ K₂ V // τ.isComplete }

IsBot in Mathlib.Order.Max

def univKbar : Kbar K₁ K₂ ≃ Key K₁ K₂ ⊕ Unit :=
  {
    toFun := λ kbar ↦ match kbar with | .key k => k | .Source => ()
    invFun := λ sum ↦ match sum with | .inl k => .key k | .inr _ => .Source
    left_inv := by admit /- proof elided -/

Fintype in Mathlib.Data.Fintype.Defs

List.flatten in Init.Prelude

def getBalanceProof (requests : List (Request K₁ K₂ C Sigma Pi V))
                    (h₀ : ∀ request ∈ requests, request.isValid)
                    (i : Fin (attackGameR requests []).length)
                    (h₁ : (attackGameR requests [])[i].isWithdrawalBlock) :
                    BalanceProof K₁ K₂ C Pi V :=
  let request := requests[i]'(by admit /- proof elided -/
  )
  have : request.getWithdrawal.isSome := by admit /- proof elided -/

def sender (τ : Τ K₁ K₂ V) : Kbar K₁ K₂ := τ.1.1

LE.le in Init.Prelude

DecidablePred in Init.Prelude

Lattice in Mathlib.Order.Lattice

def mergeR' (πs : List (BalanceProof K₁ K₂ C Pi V)) : Fin πs.length.succ → BalanceProof K₁ K₂ C Pi V :=
  λ i ↦ match h : i.1 with
        | 0 => .initial
        | k + 1 => Dict.Merge (mergeR' πs ⟨k, by admit /- proof elided -/
        ⟩) πs[k]
  termination_by i => i
  decreasing_by { simp_wf; next m => rcases m; aesop }

def codomainPred {α : Type} [DecidableEq α] {β : Type}
  (m : Finmap (λ _ : α ↦ β)) (P : β → Prop) : Prop :=
  ∀ key : α, (h : key ∈ m) → P (m.lookup_h h)

instance : Preorder (S K₁ K₂ V) := inferInstance

instance latticePreorder : Preorder V := inferInstance

Multiset.map in Mathlib.Data.Multiset.MapFold

instance : PreWithZero α₊ :=

Finset.univ in Mathlib.Data.Fintype.Defs

instance : Setoid' ((Pi × ExtraDataT) × TransactionBatch K₁ K₂ V) where
  isEquiv := by admit /- proof elided -/

def TransactionsInBlock_deposit
  (b : { b : Block K₁ K₂ C Sigma V // b.isDepositBlock }) : List (Τ K₁ K₂ V) :=
  match h : b.1 with
  | .deposit r v => [⟨(.Source, r, v), by admit /- proof elided -/
  ⟩]
  | .withdrawal .. | .transfer .. => by admit /- proof elided -/

LinearOrder in Mathlib.Order.Defs.LinearOrder

List.length in Init.Prelude

def mkWithdrawalBlock (K₂ C Sigma : Type) (withdrawals : K₁ → V₊) : Block K₁ K₂ C Sigma V :=
  withdrawal withdrawals

iInf in Mathlib.Order.SetNotation

private def fStarFixed {n : ℕ}
  (Ts : Vector (Τ K₁ K₂ V) n) (s₀ : S K₁ K₂ V) : S K₁ K₂ V :=
  fStar Ts.1 s₀

private def BalFixed (bs : List (Block K₁ K₂ C Sigma V)) : BalanceProof K₁ K₂ C Pi V → S K₁ K₂ V :=
  λ π ↦ fStarFixed (s₀ := S.initial K₁ K₂ V) (TransactionsInBlocksFixed π bs)

def getDeposit? (b : Block K₁ K₂ C Sigma V) : Option (K₂ × V₊) :=
  match b with
  | deposit r v => .some (r, v)
  | transfer .. | withdrawal .. => .none

Function.RightInverse in Init.Data.Function

def iso {X : Type} [Preorder X] (a b : X) := a ≤ b ∧ b ≤ a

def mergeR (πs : List (BalanceProof K₁ K₂ C Pi V)) (n : ℕ) : BalanceProof K₁ K₂ C Pi V :=
  if _ : n < πs.length.succ
  then match n with
       | 0 => .initial
       | k + 1 => Dict.Merge (mergeR πs k) πs[k]
  else .initial

Std.Associative in Init.Core

List.finRange in Init.Data.List.FinRange

def infV (b : S K₁ K₂ V) (T : Τ K₁ K₂ V) (k : Kbar K₁ K₂) :
  InfSet V where
    sInf := λ s ↦ if s = V' b T k
                  then (exists_inf b T).1 k
                  else 0

def isComplete (τ : Τ K₁ K₂ V) :=
  match τ with | ⟨(_, _, v), _⟩ => v.isSome

instance : IsTotal (K₂ × Key K₁ K₂) lexLe :=

Int.reduceNeg in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int

instance : Std.Associative
             (Dict.Merge (α := (C × K₂)) (ω := ((Pi × ExtraDataT) × TransactionBatch K₁ K₂ V))) :=
  ⟨λ _ _ _ ↦ Dict.Merge_assoc⟩

def mergeR''' (πs : List (BalanceProof K₁ K₂ C Pi V)) (acc : BalanceProof K₁ K₂ C Pi V) : BalanceProof K₁ K₂ C Pi V :=
  πs.foldl Dict.Merge acc

Option.isSome in Init.Data.Option.Basic

CoeFun in Init.Coe

def aggregateDeposits (σ : Scontract K₁ K₂ V C Sigma) : V :=
  ∑ i : Fin σ.length,
    if h : σ[i].isDepositBlock
    then (σ[i.1].getDeposit h).2.1
    else 0

instance : Coe (NonNeg α) α := ⟨(·.1)⟩

def Block.updateBalance (bal : V) (block : Block K₁ K₂ C Sigma V) : V :=
  match block with
   
  | .deposit _ v  => bal + v
   
  | .transfer ..  => bal
   
  | .withdrawal B => bal - ∑ k : K₁, (B k).1

def isCodomainNonneg {α : Type} [DecidableEq α] {β : Type} [LE β] [OfNat β 0]
  (m : Finmap (λ _ : α ↦ β)) : Prop := codomainPred m (0 ≤ ·)

def f' (b : S K₁ K₂ V) (T : Τ K₁ K₂ V) : S K₁ K₂ V := 
  ⟨
    λ k ↦
      match h : T with
      | ⟨(_, _, .some _), hT⟩ => fc (⟨T, by admit /- proof elided -/
      ⟩, b) k
      | ⟨(s, _, .none), _⟩ => if k = s then 0 else b k,
    by admit /- proof elided -/
  ⟩

def getWithdrawal (b : Block K₁ K₂ C Sigma V) (_h : b.isWithdrawalBlock) : K₁ → V₊ :=
  match b with | .withdrawal B => B

LT in Init.Prelude

Bool in Init.Prelude

def lookup (ct : CommitT C K Pi) {k : K} (h : k ∈ ct.dict) : Pi :=
  ct.dict[k]

Membership in Init.Prelude

instance : IsTrans (K₂ × Key K₁ K₂) lexLe :=

Iff in Init.Core

instance : Preorder (Pi × ExtraDataT) := trivialPreorder

instance : Inhabited (BalanceProof K₁ K₂ C Pi V) := ⟨BalanceProof.initial⟩

IsGLB in Mathlib.Order.Bounds.Defs

instance [Finite K₁] [Finite K₂] : Finite (Kbar K₁ K₂ : Type) :=
  Finite.of_equiv _ univKbar.symm

CovariantClass in Mathlib.Algebra.Order.Monoid.Unbundled.Defs

instance : GetElem (CommitT C K Pi) K Pi (λ ct k ↦ k ∈ ct.dict) := ⟨CommitT.lookup⟩

instance : LinearOrder (Key K₁ K₂) where
  le := Key.le
  le_refl := λ a ↦ by dsimp [Key.le]; aesop
  le_trans := IsTrans.trans
  le_antisymm := IsAntisymm.antisymm
  le_total := IsTotal.total
  decidableLE := inferInstance
  lt_iff_le_not_le := λ a b ↦ lt_iff_le_not_le

Nat in Init.Prelude

def First (x₁ x₂ : Option α) : Option α :=
  match x₁, x₂ with
  | .some x, .none => .some x
  | .some x, .some _ => .some x
  | .none, .some y => .some y
  | .none, .none => .none

binding : ComputationallyInfeasible <|
              ∃ (c : C) (k : K) (m₁ m₂ : M) (π₁ π₂ : Pi),
                Verify π₁ k m₁ c = true ∧
                Verify π₂ k m₂ c = true ∧
                m₁ ≠ m₂

def le (v₁ v₂ : Vector α n) :=
  ∀ x ∈ (v₁.1.zip v₂.1), x.1 ≤ x.2

Prod.fst in Init.Prelude

Prod.snd in Init.Prelude

Prod in Init.Prelude

Nonempty in Init.Prelude

def attackGameBlocks' : Scontract K₁ K₂ V C Sigma :=
  requests.foldl Scontract.appendBlock σ

private instance [IsAntisymm K₁ (·≤·)] [IsAntisymm K₂ (·≤·)] : IsAntisymm (Key K₁ K₂) (·≤·) :=
  {
    antisymm := λ a b ↦ by
      dsimp [(·≤·), Key.le]; intros h₁ h₂
      aesop (add safe forward IsAntisymm.antisymm)
  }

instance : Membership α (Dict α ω) := ⟨Dict.is_mem⟩

abbrev S (K₁ K₂ V : Type) [PreWithZero V] := { s : S' K₁ K₂ V // s.isValid }

def computeBalanceSum (σ : Scontract K₁ K₂ V C Sigma) :=
  let v_deposited : V := aggregateDeposits σ
  let v_withdrawn : V := aggregateWithdrawals σ
  v_deposited - v_withdrawn

Fintype.ofFinite in Mathlib.Data.Fintype.EquivFin

IsGreatest in Mathlib.Order.Bounds.Defs

def Kbar.isK₁ (k : Kbar K₁ K₂) := k matches key (.inl _)

Eq in Init.Prelude

Subtype in Init.Prelude

def TransactionsInBlock (π : BalanceProof K₁ K₂ C Pi V) (b : Block K₁ K₂ C Sigma V) : List (Τ K₁ K₂ V) := 
  match h : b with
  | .deposit ..    => TransactionsInBlock_deposit ↪b
  | .transfer ..   => TransactionsInBlock_transfer π ↪b
  | .withdrawal .. => TransactionsInBlock_withdrawal ↪b

def discretePreorder {α : Type} : Preorder α :=
  {
    lt := λ _ _ ↦ False
    le := (·=·)
    le_refl := Eq.refl
    le_trans := λ _ _ _ ↦ Eq.trans
    lt_iff_le_not_le := by admit /- proof elided -/

instance : LE (Key K₁ K₂) := ⟨Key.le⟩

inferInstanceAs in Init.Prelude

OfNat in Init.Prelude

Nat.card in Mathlib.SetTheory.Cardinal.Finite

inductive Request where
  | deposit (recipient : K₂) (amount : V₊)
  | transfer (aggregator : K₁) (extradata : ExtraDataT) (commitment : C) (senders : List K₂) (sigma : Sigma)
  | withdrawal (π : BalanceProof K₁ K₂ C Pi V)

def attackGame : Scontract K₁ K₂ V C Sigma :=
  attackGameBlocks' requests []

def v' (v : V₊) (b : S K₁ K₂ V) (s : Kbar K₁ K₂) : V₊ :=
  match h : s with
  | .Source => v
  | .key _  => ⟨v ⊓ b s, by admit /- proof elided -/
  ⟩

Vector in Init.Data.Vector.Basic

def fStar (Ts : List (Τ K₁ K₂ V)) (s₀ : S K₁ K₂ V) : S K₁ K₂ V :=
  Ts.foldl f s₀

class Setoid' (X : Type) extends Preorder X where
  isEquiv : IsEquivRel (X := X)

def Block.isValid (block : Block K₁ K₂ C Sigma V) (π : BalanceProof K₁ K₂ C Pi V) : Bool :=
  match block with
   
  | .deposit .. => true
   
  | .transfer aggregator extradata commitment senders sigma =>
      let isValidSA := SA.Verify senders (commitment, aggregator, extradata) sigma
      let isValidAggregator := aggregator = AgreedUponAggregator
      isValidSA ∧ isValidAggregator
   
  | .withdrawal _ => π.Verify (M := (C × K₁ × ExtraDataT))

DecidableEq in Init.Prelude

def fc (τcXb : Τc K₁ K₂ V × S K₁ K₂ V) : S K₁ K₂ V :=
  ⟨λ k : Kbar K₁ K₂ ↦
    match τcXb with
    | ⟨⟨⟨⟨s, r, v⟩, _⟩, hτ⟩, b⟩ =>
      let v' := v' (v.get hτ) b s
      b k + (e r - e s) k • v',
  by admit /- proof elided -/
  ⟩

Lean.Parser.Tactic.replace in Init.Tactics

Option.isNone in Init.Data.Option.Basic

Option.get in Init.Data.Option.Basic

upperBounds in Mathlib.Order.Bounds.Defs
</all_available_defs>

<all_available_lemmas>
@[simp]
lemma computeBalance'_cons : computeBalance' (hd :: σ) v =
                             computeBalance' σ (Block.updateBalance v hd)

@[simp]
lemma sum_fc_eq_sum : ∑ (k : Kbar K₁ K₂), fc (Tc, b) k = ∑ (k : Kbar K₁ K₂), b k

lemma merge_K : (π <+> acc) K = Dict.First (π K) (acc K)

lemma isValid_initial : (initial K₁ K₂ V).isValid

lemma lemma4 (h : π₁ ≤ π₂) : Bal π₁ bs ≤ Bal π₂ bs

lemma le_Merge_of_le_le
        {π π₁ π₂ : BalanceProof K₁ K₂ C Pi V}
        {k : C × K₂}
        (h : π k ≤ π₁ k)
        (h₁ : π k ≤ π₂ k) :
        π k ≤ Dict.Merge π₁ π₂ k

lemma attackGame_eq_attackGameBlocks!_normalise :
  attackGame requests = attackGameBlocks! (normalise requests)

@[simp]
lemma isLUB_some_some_none_some :
  IsLUB {some x, some y, none} (some join) ↔ ((join ≅ x) ∧ join ≅ y)

@[simp]
lemma deposit_ne_widthdrawal : 
  (deposit s v).isWithdrawalBlock (V := V) (Sigma := Sigma) (C := C) (K₁ := K₁) = False

@[simp]
lemma isLUB_some_none_of_some :
  IsLUB {.some x, none} y? ↔ IsLUB {.some x} y?

lemma isValid_some_of_ne {v : V₊} (h : s ≠ r) : Τ'.isValid (s, r, some v)

lemma compat_of_iso (h : π₁ ≅ π₂) : π₁ <≅> π₂

private lemma reindex_mem :
  ∀ (a : ℕ) (ha : a ∈ Finset.range (k + 1) \ {0}), reindex a ha ∈ Finset.range k

@[simp, refl]
lemma iso_rfl : a ≅ a

@[simp]
lemma mergeR''_eq_none' :
  (mergeR'' πs acc) K = none ↔ acc K = none ∧ ∀ π ∈ πs, π K = none

lemma isLUB_union_Merge_of_isLUB_isLUB_compat {A B : Set (BalanceProof K₁ K₂ C Pi V)}
  (h₁ : IsLUB A j₁) (h₂ : IsLUB B j₂) (h₃ : j₁ <≅> j₂) : IsLUB (A ∪ B) (j₁ <+> j₂)

lemma le_of_iso (h : π₂ ≅ π₃) (h₁ : π₁ ≤ π₂) : π₁ ≤ π₃

lemma compat_merge_of_compat :
  (∀ π', π' ∈ πs → π <≅> π') → π <≅> (mergeR'' πs .initial)

@[simp]
lemma some_le_none_eq_False : .some x ≤ none ↔ False

@[simp]
lemma attackGameRGo_cons :
  attackGameRGo (request :: requests) σ =
  request.toBlock! σ :: attackGameRGo requests (σ.appendBlock! request)

@[simp]
lemma length_attackGameRGo : (attackGameRGo requests σ).length = requests.length

private lemma le_cons_aux 
  (eq₁ : v₁ = ⟨hd₁ :: tl₁, len₁⟩) (eq₂ : v₂ = ⟨hd₂ :: tl₂, len₂⟩)
  (h : v₁ ≤ v₂) : hd₁ ≤ hd₂ ∧
  le ⟨tl₁, by simp at len₁; assumption⟩ ⟨tl₂, by simp at len₂; assumption⟩

lemma Merge_comm_of_compat (h : π₁ <≅> π₂) : π₁ <+> π₂ ≅ π₂ <+> π₁

@[simp]
lemma length_appendBlock :
  (appendBlock! σ request).length = σ.length + 1

@[simp]
lemma le_eq_iso [φ : Setoid' X] {a b : X} : a ≤ b ↔ a ≅ b

@[simp]
lemma aggregateDeposits_nil : aggregateDeposits ([] : Scontract K₁ K₂ V C Sigma) = 0

lemma computeBalance'_eq_zero : computeBalance' σ v = v + computeBalance' σ 0

theorem Function.injective_of_CryptInjective
  {α ω : Type} [Nonempty ω] {f : α → ω} [inj : Injective f] : Function.Injective f

@[simp]
lemma withdrawal_ne_deposit :
  (withdrawal ws).isDepositBlock (V := V) (Sigma := Sigma) (C := C) (K₂ := K₂) = False

@[simp]
lemma none_le : Option.none ≤ .some x

@[simp]
lemma nonneg {s : S K₁ K₂ V} {k : Key K₁ K₂} : 0 ≤ s k

lemma proposition5' [Preorder Y] {f g h join' : X → Y}
  (h₀ : IsLUB {f, g} join')
  (h₁ : ∀ x, h x ≅ join' x) :
  join' ≅ h

lemma map_eq_project_triple {β γ δ : Type}
                            {s : β} {r : γ} {v : δ}
                            {i : ℕ}
                            {P : (β × γ × δ) → Prop}
                            {l : List (Subtype P)}
                            {h₀}
                            {h : i < l.length} : 
  l[i]'h = ⟨(s, r, v), h₀⟩ → (l[i]'h).1.2.2 = v

lemma mergeR'_eq_mergeR_of_lt {n : ℕ} (h : n < πs.length.succ) :
  mergeR' πs ⟨n, h⟩ = mergeR πs n

lemma merge_le (h₁ : π₁ ≤ π₃) (h₂ : π₂ ≤ π₃) : π₁ <+> π₂ ≤ π₃

private theorem monotone_fStarFixed_aux (h : v₁ ≤ v₂) (h₂ : b₁ ≤ b₂) :
                                        v₁.1.foldl f b₁ ≤ v₂.1.foldl f b₂

lemma merge_left_none_eq_right (h : π K = none) : (π <+> acc) K = acc K

lemma zip_nodup_of_nodup_right {α β : Type} {l₁ : List α} {l₂ : List β}
  (h : l₂.Nodup) : (l₁.zip l₂).Nodup

lemma mergeR'_succ {πs : List (BalanceProof K₁ K₂ C Pi V)} {n : ℕ} (h : n + 1 < πs.length.succ) :
  mergeR' πs ⟨n + 1, h⟩ = (mergeR' πs ⟨n, by omega⟩).Merge (πs[n])

theorem keys_map_eq (h : ∀ x, Sigma.fst (f x) = x) : (Multiset.map f m).keys = m

lemma iso_of_isLUB [Setoid' X] {x y join : X} (h : IsLUB {x, y} join) : x ≅ y

@[simp]
lemma length_attackGameBlocks'! :
  (attackGameBlocks'! requests σ).length = σ.length + requests.length

private lemma Bal'_eq_Bal : Bal' bs π = Bal π bs

lemma proposition4 [Setoid' X] {x y : Option X} :
  (∃ join : Option X, IsLUB {x, y, .none} join) ↔ (x ≠ .none ∧ y ≠ .none → x ≅ y)

lemma toBlock!_of_deposit (h : request matches .deposit ..) :
  request.toBlock! σ matches .deposit ..

lemma monotone_TransactionsInBlocksFixed :
  Monotone λ (π : BalanceProof K₁ K₂ C Pi V) ↦ TransactionsInBlocksFixed π Bstar

lemma isSome_of_complete {t'} (h : isComplete ⟨⟨kb₁, kb₂, v?⟩, t'⟩) : v?.isSome

theorem nodup_map_of_pres_keys_nodup
  (h : ∀ x, Sigma.fst (f x) = x) (h₁ : m.Nodup) : (List.map f m).Nodup

lemma proposition1 [Preorder X] {x y : X} {s : Set X}
  (h₁ : IsLUB s x) (h₂ : IsLUB s y) : x ≅ y

private lemma valid_mergeR''_aux {π : BalanceProof K₁ K₂ C Pi V}
                                 {πs : List (BalanceProof K₁ K₂ C Pi V)}
                                 {n : ℕ}
  (hn : n < πs.length.succ)
  (h₀ : π.Verify (M := (C × K₁ × ExtraDataT)))
  (h : ∀ π ∈ πs, π.Verify (M := (C × K₁ × ExtraDataT))) :
  (mergeR'' (πs.take n) π).Verify (M := (C × K₁ × ExtraDataT))

@[simp]
lemma isLUB_some_some_none_none :
  IsLUB {some x, some y, none} .none ↔ False

@[simp]
lemma none_iso_some : (.none ≅ some x) ↔ False

lemma proposition4' [Setoid' X] {join x y : Option X} (h : IsLUB {x, y, .none} join) :
  join ≅ Dict.First x y

@[simp]
lemma isComplete_none {t'} : ¬isComplete ⟨⟨kb₁, kb₂, (.none : Option V₊)⟩, t'⟩

private lemma reindex_inj :
  ∀ (a₁ : ℕ) (ha₁ : a₁ ∈ Finset.range (k + 1) \ {0})
    (a₂ : ℕ) (ha₂ : a₂ ∈ Finset.range (k + 1) \ {0}),
  reindex a₁ ha₁ = reindex a₂ ha₂ → a₁ = a₂

lemma toBlock_σ_matches_withdrawal (σ σ' : Scontract K₁ K₂ V C Sigma) :
  request.toBlock! σ matches .withdrawal .. ↔
  request.toBlock! σ' matches .withdrawal ..

@[simp]
lemma computeBalance'_nil : computeBalance' ([] : Scontract K₁ K₂ V C Sigma) v = v

lemma Block.updateBalance_of_transfer (h : block.isTransferBlock) :
  block.updateBalance v = v

lemma batch?_neq_of_mem {π₁k π₂k : Option ((Pi × ExtraDataT) × TransactionBatch K₁ K₂ V)}
  (h₀ : π₁k ≠ .none ∧ π₂k ≠ .none)
  (h : ¬(π₁k ≅ π₂k)) : (π₁k.get (Option.isSome_iff_ne_none.2 h₀.1)).2 ≠
                       (π₂k.get (Option.isSome_iff_ne_none.2 h₀.2)).2

lemma merge_lem :
  mergeR'' (π :: πs) BalanceProof.initial = π <+> (mergeR'' πs BalanceProof.initial)

@[simp]
lemma initial_Merge {π : BalanceProof K₁ K₂ C Pi V} :
  BalanceProof.initial.Merge π = π

theorem theorem1 : ¬adversaryWon (attackGame requests)

lemma senderReceiver_transactionsInBlocks {s r v} {s' r' v'} {eq₁ eq₂} {i}
  (h₀ : i < (TransactionsInBlocks π bs).length)
  (h₁ : (TransactionsInBlocks π bs)[i] = ⟨(s, r, v), eq₁⟩)
  (h₂ : (TransactionsInBlocks π' bs)[i]'(by blast with π) = ⟨(s', r', v'), eq₂⟩) :
  s = s' ∧ r = r'

lemma sum_f_le_sum : ∑ (k : Kbar K₁ K₂), f b T k ≤ ∑ (k : Kbar K₁ K₂), b k

@[simp]
lemma isLUB_some_some_iff_iso :
  IsLUB {some x} (some y) ↔ some x ≅ some y

@[simp]
lemma withdrawal_ne_transfer : 
  (withdrawal ws).isTransferBlock (V := V) (Sigma := Sigma) (C := C) (K₂ := K₂) = False

lemma isLUB_of_isLUB_iso (h : IsLUB A π₁) (h₁ : π₁ ≅ π₂) : IsLUB A π₂

lemma aggregateWithdrawals_eq_aggregateWithdrawals' {σ : Scontract K₁ K₂ V C Sigma} :
  aggregateWithdrawals σ = aggregateWithdrawals' σ

lemma isValid_iff : isValid (s, r, v?) ↔ s ≠ r ∧ (s matches .Source → v?.isSome)

@[simp]
lemma isLUB_none_some_iff_False :
  IsLUB {.some x} none ↔ False

lemma map_join_unnecessarily_specific
  {α β γ δ Pi : Type}
  [LE δ]
  [LE Pi]
  {l : List α}
  {P : (β × γ × δ) → Prop}
  {π π' : Pi}
  {f : Pi → α → List (Subtype P)}
  {i : ℕ}
  (h₀ : (List.length ∘ f π) = (List.length ∘ f π'))
  (h₁ : ∀ (a : α)
          (i : ℕ) (h : i < (f π a).length),
          (f π a)[i].1.2.2 ≤ ((f π' a)[i]'(by apply congr_fun at h₀; aesop)).1.2.2)
  (h) :
  ((List.map (f π) l).flatten[i]'h).1.2.2 ≤
  ((List.map (f π') l).flatten[i]'(by aesop)).1.2.2

lemma Merge_iso_of_iso (h : π₁ ≅ π₂) :
  π₁ <+> π₃ ≅ π₂ <+> π₃

lemma sender_transactionsInBlock :
  (TransactionsInBlock π₁ b).map (λ s ↦ s.1.1) =
  (TransactionsInBlock π₂ b).map (λ s ↦ s.1.1)

@[simp]
lemma length_TransactionsInBlock_deposit
  {b : { b : Block K₁ K₂ C Sigma V // b.isDepositBlock }} :
  (TransactionsInBlock_deposit b).length = 1

lemma first_left (h : x₁.isSome) : First x₁ x₂ = x₁

@[simp]
lemma BalanceProof.valid_initial :
  BalanceProof.initial.Verify (K₁ := K₁) (AD := AD) (K₂ := K₂) (V := V) (M := (C × K₁ × ExtraDataT))

lemma v_transactionsInBlocks {s r v v'} {eq₁ eq₂} {i}
  (h : π ≤ π')
  (h₀ : i < (TransactionsInBlocks π Bstar).length)
  (h₁ : (TransactionsInBlocks π Bstar)[i] = ⟨(s, r, v), eq₁⟩)
  (h₂ : (TransactionsInBlocks π' Bstar)[i]'(by blast with π) = ⟨(s, r, v'), eq₂⟩) :
  v ≤ v'

theorem keys_dedup_map_pres_univ
  (h : m.Nodup) [DecidableEq (Sigma β)] (h₁ : ∀ x, Sigma.fst (f x) = x) :
  (Multiset.map f m).dedup.keys = m

@[simp]
lemma mergeR''_append :
  mergeR'' (πs ++ πs') acc = mergeR'' πs' (mergeR'' πs acc)

@[simp]
lemma Block.updateBalance_deposit {r : K₂} {v : V} {vplus : V₊} :
  (Block.deposit r vplus).updateBalance (K₁ := K₁) (C := C) (Sigma := Sigma) v = v + vplus

@[simp]
lemma some_le_some :
  Option.some x ≤ .some y ↔ x ≤ y

@[simp]
lemma isLUB_any_any_none_of_any_any :
  IsLUB {x?, y?, none} join? ↔ IsLUB {x?, y?} join?

@[simp]
lemma transfer_ne_deposit :
  (transfer aggregator extradata commitment senders sigma).isDepositBlock (V := V) = False

lemma TransactionsInBlocksFixed_le_of_TransactionsInBlocks
  (h : ∀ i : Fin (length_of_TransactionsInBlocks bs).1,
    (TransactionsInBlocks π bs)[i]'(by blast with π i) ≤
    (TransactionsInBlocks π' bs)[i]'(by blast with π' i)) :
  TransactionsInBlocksFixed π bs ≤ TransactionsInBlocksFixed π' bs

lemma proposition1' [PartialOrder X] {x y : X} {s : Set X}
  (h₁ : IsLUB s x) (h₂ : IsLUB s y) : x = y

lemma ne_none_of_ne_iso [Setoid' Y] {D₁ D₂ : Dict X Y} {k : X}
  (h : D₁ k ≠ .none) (h₁ : D₁ ≅ D₂) : D₂ k ≠ .none

@[simp]
lemma isLUB_some_none_iff_False :
  IsLUB {none} (.some x) ↔ False

private lemma prop6_general_aux :
  (∀ π π' : BalanceProof K₁ K₂ C Pi V, π ∈ πs ∧ π' ∈ πs → π <≅> π') →
     IsLUB {π | π ∈ πs} (mergeR'' πs .initial)

lemma proposition2' [Setoid' X] {join x y : X} (h : IsLUB {x, y} join) :
  (x ≅ join) ∧ y ≅ join

lemma attackGameBlocks'r_eq_attackGameBlocks' :
  attackGameBlocks'! requests σ = attackGameBlocks'!r requests σ

@[simp]
lemma length_initial : (@initial K₁ K₂ C Sigma V _).length = 0

@[simp]
lemma mergeR''_cons :
  mergeR'' (π :: πs) acc = Dict.Merge acc (mergeR'' πs π)

lemma compat_comm : (π₁ <≅> π₂) ↔ π₂ <≅> π₁

lemma attackGameBlocks'_eq_attackGameBlocks'!_normalise :
  attackGameBlocks' requests σ = attackGameBlocks'! (normalise requests) σ

lemma valid_mergeR' {πs : List (BalanceProof K₁ K₂ C Pi V)} {n : Fin πs.length.succ}
  (h : ∀ π ∈ πs, π.Verify (M := (C × K₁ × ExtraDataT))) :
  (mergeR' πs n).Verify (M := (C × K₁ × ExtraDataT))

@[simp]
lemma mergeR''_nil : mergeR'' [] acc = acc

@[simp]
lemma appendBlock!_nil : Scontract.appendBlock! [] request = [request.toBlock! []]

lemma getElem_Ico_of_lt {m n : ℕ} (h : n < m) : (List.Ico 0 m)[n]'(by simp [h]) = n

lemma proposition6_aux [Setoid' Y] {D₁ D₂ : Dict X Y}
  (h : ∀ k, D₁ k ≠ .none ∧ D₂ k ≠ .none → D₁ k ≅ D₂ k) : IsLUB {D₁, D₂} (Dict.Merge D₁ D₂)

lemma valid_mergeR'' {πs : List (BalanceProof K₁ K₂ C Pi V)} {n : ℕ}
  (hn : n < πs.length.succ)
  (h : ∀ π ∈ πs, π.Verify (M := (C × K₁ × ExtraDataT))) :
  (mergeR'' (πs.take n) .initial).Verify (M := (C × K₁ × ExtraDataT))

lemma Block.updateBalance_eq_zero :
  block.updateBalance v = v + block.updateBalance 0

@[simp]
lemma snd_eq_of_iso {d₁ d₂ : (Pi × ExtraDataT) × TransactionBatch K₁ K₂ V} :
  d₁.2 = d₂.2 ↔ (d₁ ≅ d₂)

@[simp]
lemma Block.updateBalance_withdrawal {B : K₁ → V₊} :
  (Block.withdrawal B).updateBalance (K₁ := K₁) (K₂ := K₂) (C := C) (Sigma := Sigma) v = v - ∑ (k : K₁), (B k).1

lemma exists_key_of_isValid (h : isValid (s, r, (none : Option V₊))) : ∃ k : Key K₁ K₂, s = k

@[simp]
lemma mergeR''_eq_some {x} :
  acc K = some x → (mergeR'' πs acc) K = acc K

private lemma sum_fStar_le_zero_aux (h : ∑ (k : Kbar K₁ K₂), b k ≤ 0) :
  ∑ (k : Kbar K₁ K₂), fStar Tstar b k ≤ 0

lemma monotone_f (h₁ : b₁ ≤ b₂) (h₂ : T₁ ≤ T₂) : f b₁ T₁ k ≤ f b₂ T₂ k

lemma Merge_mergeR''_comm {πs : List (BalanceProof K₁ K₂ C Pi V)} (h : π <≅> acc) :
  acc <+> (mergeR'' πs π) ≅ π <+> (mergeR'' πs acc)

lemma keys_Merge_left {x : α} (h : x ∈ D₁) : Merge D₁ D₂ x = D₁ x

@[simp]
lemma attackGameRGo_nil :
  attackGameRGo ([] : List (Request K₁ K₂ C Sigma Pi V)) σ = []

lemma lemma3 : Bal π bs .Source ≤ 0

lemma s_ne_r_of_isValid (h : isValid ⟨s, r, v?⟩) : s ≠ r

omit Hinj in
private theorem not_adversaryWon_attackGame_of_exists_LUB
  (eqrequests : requests! = normalise requests)
  (hValid     : ∀ request ∈ requests!, request.isValid)
  (eqI        : I = (List.finRange (attackGameR requests! []).length).filter ((attackGameR requests! [])[·].isWithdrawalBlock))
  (hI         : ∀ {i : Fin (attackGameR requests! []).length}, i ∈ I ↔ (attackGameR requests! [])[i].isWithdrawalBlock)
  (hgetπ      : getπ =
                λ i : {i : Fin (attackGameR requests! []).length // i ∈ I} ↦
                  (i, getBalanceProof requests! hValid ⟨i.1.1, i.1.2⟩ (hI.1 i.2)))
  (eqπs       : πs = I.attach.map getπ)
  (hlen       : πs.length ≤ n)
  (hπs        : ∀ (i : {i // i ∈ I}), (List.lookup i πs).isSome)
  (eqπproofs  : πproofs = πs.map Prod.snd)
  (πproofslen : πproofs.length = πs.length)
  (isπ        : ∀ (i : Fin (List.length (attackGameR requests! [])))
                  (h : (attackGameR requests! [])[i.1].isWithdrawalBlock),
                  (attackGameR requests! [])[i.1].getWithdrawal h =
                  (getBalanceProof requests! hValid i h).toBalanceF ((attackGameR requests! []).take i.1))
  (contra     : ¬0 ≤ computeBalanceSum (attackGameR requests! []))
  (existsLUB  : ∃ join, IsLUB {π | π ∈ πproofs} join) : False

@[simp]
lemma length_attackGameR : (attackGameR requests σ).length = σ.length + requests.length

lemma merge_ne_none_of_join_ne_none_iso [Setoid' Y] {D₁ D₂ join : Dict X Y} {k}
  (hk : join k ≠ .none) (h : IsLUB {D₁, D₂} join) : Dict.Merge D₁ D₂ k ≠ .none

lemma isSome_getDeposit?_of_isDepositBlock {b : Block K₁ K₂ C Sigma V}
  (h : b.isDepositBlock) : b.getDeposit?.isSome

@[simp]
lemma attackGameR_cons :
  attackGameR (request :: requests) σ =
  σ ++ attackGameRGo (request :: requests) σ

lemma proposition6 [Setoid' Y] {D₁ D₂ : Dict X Y} :
  (∃ join, IsLUB {D₁, D₂} join) ↔ ∀ x, D₁ x ≠ .none ∧ D₂ x ≠ .none → D₁ x ≅ D₂ x

private theorem lt_iff_le_not_le {k₁ k₂ : Key K₁ K₂} : k₁ < k₂ ↔ k₁ ≤ k₂ ∧ ¬k₂ ≤ k₁

lemma isWithdrawalRequest_of_isWithdrawalBlock
  (h₀ : ∀ request ∈ requests, request.isValid)
  (i : Fin (attackGameR requests []).length)
  (h₁ : ((attackGameR requests [])[i]'(by simp; rcases i with ⟨i, hi⟩; simp at hi; exact hi)).isWithdrawalBlock) :
  (requests[i]'(by rcases i with ⟨h, hi⟩; rcases requests with _ | ⟨hd, tl⟩
                   · simp at hi
                   · simp at hi ⊢; omega)) matches .withdrawal ..

lemma proposition2 [Setoid' X] {x y : X} :
  (∃ join : X, IsLUB {x, y} join) ↔ x ≅ y

@[simp]
lemma getWithdrawal_isSome :
  request.getWithdrawal.isSome ↔ request matches .withdrawal ..

congr_fun in Batteries.Logic

lemma proposition3' : 
  (∃ join : X, IsLUB {x, y} join) ↔ (∃ join : Option X, IsLUB {.some x, .some y, .none} join)

lemma verify_merge_of_valid {π₁ π₂ : BalanceProof K₁ K₂ C Pi V}
                            (h₁ : π₁.Verify (M := (C × K₁ × ExtraDataT)))
                            (h₂ : π₂.Verify (M := (C × K₁ × ExtraDataT))) :
                            BalanceProof.Verify (M := (C × K₁ × ExtraDataT)) (Dict.Merge π₁ π₂)

@[symm]
lemma iso_symm : (a ≅ b) ↔ b ≅ a

@[simp]
lemma getDeposit_deposit {r : K₂} {v : V₊} :
  getDeposit (.deposit r v) (by aesop) = (r, v)

lemma computeBalance_eq_sum : computeBalance σ = computeBalanceSum σ

@[simp]
lemma Block.updateBalance_transfer {a : K₁} {b : ExtraDataT} {c : C} {d : List K₂} (e : Sigma) :
  (Block.transfer a b c d e).updateBalance v = v

lemma proposition3''
  (h : IsLUB {x, y} join)
  (h' : IsLUB {.some x, .some y, .none} join'?) :
  .some join ≅ join'?

@[simp]
lemma isLUB_some_some_none_of_some :
  IsLUB {.some x, .some y, none} y? ↔ IsLUB {.some x, .some y} y?

@[simp]
lemma isComplete_some {t'} : isComplete ⟨⟨kb₁, kb₂, .some v⟩, t'⟩

lemma existsLUB_iff_compat :
  (∃ join, IsLUB {π₁, π₂} join) ↔ π₁ <≅> π₂

lemma s_ne_r_of_complete {t'} (h : isComplete ⟨⟨kb₁, kb₂, v?⟩, t'⟩) : kb₁ ≠ kb₂

@[aesop safe apply]
lemma nonneg_key_of_isValid {b : S' K₁ K₂ V} {k} (h : b.isValid) : 0 ≤ b (.key k)

@[simp]
lemma initial_eq_zero {k : Kbar K₁ K₂} : initial K₁ K₂ V k = 0

lemma lemma5 (π : BalanceProof K₁ K₂ C Pi V) :
  Bal π σ .Source =
  (∑ (i : Fin σ.length) (k : K₁),
     if h : σ[i].isWithdrawalBlock
     then let w := σ[i].getWithdrawal h
          w k ⊓ Bal π (σ.take i.1) k
     else 0)
  -
  aggregateDeposits σ

lemma proposition6' [Setoid' Y] {D₁ D₂ join : Dict X Y} (h : IsLUB {D₁, D₂} join) :
  join ≅ Dict.Merge D₁ D₂

theorem nodup_map_of_pres_keys_nodup
  (h : ∀ x, Sigma.fst (f x) = x) (h₁ : m.Nodup) : (Multiset.map f m).Nodup

@[trans]
lemma iso_trans : (a ≅ b) → (b ≅ c) → a ≅ c

lemma attackGameBlocks_eq_attackGameR :
  attackGameBlocks! requests = attackGameR requests []

lemma attackGameRGo_isWithdrawal_iff (σ σ' : Scontract K₁ K₂ V C Sigma)
                                     (h : i < (attackGameRGo requests σ).length) :
  (attackGameRGo requests σ)[i].isWithdrawalBlock ↔
  (attackGameRGo requests σ')[i].isWithdrawalBlock

lemma mergeR''_eq_foldl :
  mergeR'' πs acc = mergeR''' πs acc

@[simp]
lemma mergeR''_concat {π} {πs : List (BalanceProof K₁ K₂ C Pi V)} {acc} :
  mergeR'' (πs.concat π) acc = ((mergeR'' πs acc) <+> π)

private lemma delta_TransactionsInBlock_transfer
  {b : { b : Block K₁ K₂ C Sigma V // b.isTransferBlock }}
  (h : π ≤ π') : 
  ∀ i : ℕ, (hlen : i < (TransactionsInBlock_transfer π b).length) →
    (TransactionsInBlock_transfer π b)[i]'hlen =
    (TransactionsInBlock_transfer π' b)[i]'(by rwa [length_TransactionsInBlock_transfer _ π]) ∨
    ((TransactionsInBlock_transfer π b)[i]'hlen).1.2.2.isNone

theorem List.keys_zipWith_sigma {l₁ : List α} {l₂ : List β}
  (h : l₁.length = l₂.length) : (List.zipWith Sigma.mk l₁ l₂).keys = l₁

lemma keys_Merge_left' (h : ∀ x, x ∈ D₁) : Merge D₁ D₂ = D₁

@[simp]
lemma isLUB_some_some_some :
  IsLUB {some x, some y} (some join) ↔ ((join ≅ x) ∧ join ≅ y)

@[simp]
lemma bs_initial : (@initial K₁ K₂ C Sigma V _) = []

lemma keys_Merge_right' (h : ∀ x : α, x ∉ D₁) : Merge D₁ D₂ = D₂

Option.isSome_iff_ne_none in Init.Data.Option.Lemmas

lemma compat_lem {π π' π'': BalanceProof K₁ K₂ C Pi V} :
  π <≅> π' → π <≅> π'' → π <≅> (π' <+> π'')

theorem nodup_filter_of_nodup [DecidableEq α] [DecidablePred P]
  (h : m.Nodup) : (Multiset.filter P m).Nodup

lemma toBlock_eq_id_of_not_isValid (h : ¬request.isValid) :
  (toBlock σ request) = .none
</all_available_lemmas>

<local_ctx>
import Mathlib

import Mathlib.Algebra.Group.Int

import FVIntmax.BalanceProof

import FVIntmax.Block

import FVIntmax.Key

import FVIntmax.Propositions

import FVIntmax.State

import FVIntmax.Transaction

import FVIntmax.Wheels

import FVIntmax.Wheels.Dictionary

namespace Intmax

noncomputable section

open Classical

section Balance

variable {Pi K₁ K₂ V C Sigma : Type}

section Extraction

section Deposit

variable [PreWithZero V]

def TransactionsInBlock_deposit
  (b : { b : Block K₁ K₂ C Sigma V // b.isDepositBlock }) : List (Τ K₁ K₂ V) :=
  match h : b.1 with
  | .deposit r v => [⟨(.Source, r, v), by admit /- proof elided -/
  ⟩]
  | .withdrawal .. | .transfer .. => by admit /- proof elided -/

end Deposit

section Transfer

variable [Finite K₁] [Finite K₂]
         [LinearOrder K₁] [LinearOrder K₂] [PreWithZero V]

def TransactionsInBlock_transfer 
  (π : BalanceProof K₁ K₂ C Pi V) (b : { b : Block K₁ K₂ C Sigma V // b.isTransferBlock }) : List (Τ K₁ K₂ V) :=
  match h : b.1 with
  | .transfer _ _ commitment S _ =>
     
    let senderRecipient : Finset (K₂ × Key K₁ K₂) := { (k₂, k) | (k₂ : K₂) (k : Key K₁ K₂) (_h : k₂ ≠ₖ k) }
    let sorted : List (K₂ × Key K₁ K₂) := senderRecipient.sort Key.lexLe 
     
    let v (s : K₂) (r : Key K₁ K₂) : Option V₊ :=
      if s ∉ S
      then .some 0
      else 
        if h : (commitment, s) ∈ π.keys
        then let (_, t) := π[(commitment, s)]
             t r
        else .none
    sorted.attach.map λ ⟨(s, r), h⟩ ↦ ⟨(s, r, v s r), by admit /- proof elided -/
    ⟩
  | .deposit .. | .withdrawal .. => by admit /- proof elided -/

end Transfer

section Withdrawal

variable [LinearOrder K₁] [Finite K₁] [PreWithZero V]

def TransactionsInBlock_withdrawal 
  (b : { b : Block K₁ K₂ C Sigma V // b.isWithdrawalBlock }) : List (Τ K₁ K₂ V) :=
  match h : b.1 with
  | .withdrawal withdrawals =>
     
    let k₁InOrder := { s | s : K₁ }.toFinset.sort (·≤·)
    k₁InOrder.attach.map λ s : K₁ ↦ ⟨(s, .Source, withdrawals s), by admit /- proof elided -/
    ⟩
  | .deposit r v | .transfer .. => by admit /- proof elided -/

end Withdrawal

variable [Finite K₁] [LinearOrder K₁]
         [Finite K₂] [LinearOrder K₂]
         [PreWithZero V]
         {b : Block K₁ K₂ C Sigma V}
         {bs : List (Block K₁ K₂ C Sigma V)}
         {π₁ π₂ : BalanceProof K₁ K₂ C Pi V}

def TransactionsInBlock (π : BalanceProof K₁ K₂ C Pi V) (b : Block K₁ K₂ C Sigma V) : List (Τ K₁ K₂ V) := 
  match h : b with
  | .deposit ..    => TransactionsInBlock_deposit ↪b
  | .transfer ..   => TransactionsInBlock_transfer π ↪b
  | .withdrawal .. => TransactionsInBlock_withdrawal ↪b
</local_ctx>

<target_theorem>
lemma receiver_transactionsInBlock :
  (TransactionsInBlock π₁ b).map (λ s ↦ s.1.2.1) =
  (TransactionsInBlock π₂ b).map (λ s ↦ s.1.2.1) :=
</target_theorem>

