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>
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)

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

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

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

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

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

abbrev ExtraDataT : Type := ℕ

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)

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

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

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

Finset.toList in Mathlib.Data.Finset.Dedup

Subtype.mk in Init.Prelude

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

def attackGameBlocks'!r (requests : List (Request K₁ K₂ C Sigma Pi V))
                        (σ : Scontract K₁ K₂ V C Sigma) : Scontract K₁ K₂ V C Sigma :=
  match requests with
  | [] => σ
  | hd :: tl => attackGameBlocks'!r tl (σ.appendBlock! hd)

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

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₊)

def Request.getWithdrawal (request : Request K₁ K₂ C Sigma Pi V) : Option (BalanceProof K₁ K₂ C Pi V) :=
  match request with
  | withdrawal π => .some π
  | transfer .. | deposit .. => .none

private instance : IsTotal (Key K₁ K₂) (·≤·) :=
  {
    total := λ a b ↦ by
      dsimp [(·≤·), Key.le]
      aesop (add simp le_total)
  }

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

DecidableEq in Init.Prelude

List.foldl in Init.Prelude

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

Classical.arbitrary in Mathlib.Logic.Nonempty

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

LE in Init.Prelude

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

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 -/
  ⟩

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

List.concat in Init.Prelude

IsLUB in Mathlib.Order.Bounds.Defs

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

private def TransactionsInBlocksFixed (π : BalanceProof K₁ K₂ C Pi V) (bs : List (Block K₁ K₂ C Sigma V)) :
  Vector (Τ K₁ K₂ V) (length_of_TransactionsInBlocks (Pi := Pi) bs).1 :=
  ⟨TransactionsInBlocks π bs, by admit /- proof elided -/
  ⟩

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

abbrev KₚT : Type := ℕ

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

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

def mergeR'' (πs : List (BalanceProof K₁ K₂ C Pi V)) (acc : BalanceProof K₁ K₂ C Pi V) : BalanceProof K₁ K₂ C Pi V :=
  match πs with
  | [] => acc
  | π :: πs => Dict.Merge acc (mergeR'' πs π)

IsLeast in Mathlib.Order.Bounds.Defs

Sigma.fst in Init.Core

Nonempty in Init.Prelude

Subtype in Init.Prelude

absurd in Init.Prelude

Zero in Init.Prelude

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

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

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

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

Bool in Init.Prelude

Std.Associative in Init.Core

Multiset.dedup in Mathlib.Data.Multiset.Dedup

Finite in Mathlib.Data.Finite.Defs

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

Preorder in Mathlib.Order.Defs.PartialOrder

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

Decidable in Init.Prelude

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

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

Sum in Init.Core

instance (priority := high) discreteOpreorderNnonnegV : Preorder V₊ := discretePreorder

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

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

noncomputable instance {α : Type} [Finite α] : Inhabited (UniquelyIndexed α) := ⟨attach α⟩

def initial : Scontract K₁ K₂ V C Sigma := []

instance : DecidableRel (lexLe (K₁ := K₁) (K₂ := K₂)) :=
  λ a b ↦ by unfold lexLe; infer_instance

CoeFun in Init.Coe

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

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

Prod.snd in Init.Prelude

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 -/
  ⟩

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)

LinearOrder in Mathlib.Order.Defs.LinearOrder

And in Init.Prelude

def Seed : Type := ℕ

instance : Preorder (Kbar K₁ K₂) := discretePreorder

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

Fintype in Mathlib.Data.Fintype.Defs

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 }

@[simp]
private def reindex : (a : ℕ) → a ∈ Finset.range (k + 1) \ {0} → ℕ :=
  λ a _ ↦ a.pred

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 -/

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

Fin in Init.Prelude

Option.isSome in Init.Data.Option.Basic

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

instance : Preorder (Key K₁ K₂ → V₊) := discretePreorder

instance latticePreorder : Preorder V := inferInstance

def Kbar.getK₁ (k : Kbar K₁ K₂) (_h : k.isK₁) : K₁ :=
  match h : k with
  | .key (.inl k₁) => k₁
  | .key (.inr _) | .Source => by admit /- proof elided -/

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

Sigma in Init.Core

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

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

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

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

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

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

abbrev Scontract (K₁ K₂ V : Type) [PreWithZero V] (C Sigma : Type) :=
  List (Block K₁ K₂ C Sigma V)

flip in Init.Core

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

Function.eval in Mathlib.Logic.Function.Basic

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

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

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 -/

Eq in Init.Prelude

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

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

List.map in Init.Prelude

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 -/

instance : Nonempty ExtraDataT := inferInstanceAs (Nonempty ℕ)

Multiset.Nodup 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)

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⟩

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

def TransactionsInBlocks
  (π : BalanceProof K₁ K₂ C Pi V) (bs : List (Block K₁ K₂ C Sigma V)) : List (Τ K₁ K₂ V) :=
  (bs.map (TransactionsInBlock π)).flatten

List.take in Init.Data.List.Basic

Prod in Init.Prelude

Preorder.toLE in Mathlib.Order.Defs.PartialOrder

List in Init.Prelude

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

Unit in Init.Prelude

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

Sum.inl in Init.Core

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

Function.RightInverse in Init.Data.Function

Inhabited in Init.Prelude

Set in Mathlib.Data.Set.Defs

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

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

DecidableRel in Init.Prelude

def attackGameRGo (requests : List (Request K₁ K₂ C Sigma Pi V))
                  (σ : Scontract K₁ K₂ V C Sigma) : Scontract K₁ K₂ V C Sigma :=
  match requests with
  | [] => []
  | hd :: tl => hd.toBlock! σ :: attackGameRGo tl (σ.appendBlock! hd)

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

Coe in Init.Coe

Multiset.keys in Mathlib.Data.Finmap

List.attach in Init.Data.List.Attach

Lattice in Mathlib.Order.Lattice

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

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

Prod.mk in Init.Prelude

Nat.card in Mathlib.SetTheory.Cardinal.Finite

List.zipWith in Init.Data.List.Basic

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

Fintype.ofFinite in Mathlib.Data.Fintype.EquivFin

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

id in Init.Prelude

Sum.inr in Init.Core

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

def isπ (requests : List (Request K₁ K₂ C Sigma Pi V)) :=
  ∀ (h₀ : ∀ request ∈ requests, request.isValid)
    (i : Fin (attackGameR requests []).length)
    (h : (attackGameR requests [])[i].isWithdrawalBlock),
    (attackGameR requests [])[i].getWithdrawal h =
    let π := getBalanceProof requests h₀ i h
    let σ := (attackGameR requests []).take i.1
    π.toBalanceF σ

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

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

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

Function.Injective in Init.Data.Function

LE.le in Init.Prelude

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

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₂)

Set.image in Mathlib.Data.Set.Defs

instance (priority := high) maybeInduced {α : Type} [Preorder α] : Preorder (Option α) :=
  let le : Option α → Option α → Prop := λ x y ↦
                                           match x, y with
                                           | .none, .none | .none, .some _ => True
                                           | .some x, .some y => x ≤ y
                                           | .some _, .none   => False
  {
    le := le
    lt := λ a b ↦ le a b ∧ ¬ le b a 
    le_refl := by admit /- proof elided -/

DecidablePred in Init.Prelude

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 isValid (τ : Τ' K₁ K₂ V) :=
  match τ with
  | (s, r, v) => s ≠ r ∧ (s matches .Source → v.isSome)

def BalanceProof.toBalanceF (π : BalanceProof K₁ K₂ C Pi V)
                            (σ : Scontract K₁ K₂ V C Sigma) : K₁ → V₊ :=
  λ k : K₁ ↦ ⟨Bal π σ k, by admit /- proof elided -/
  ⟩

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

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) }

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))

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

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

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

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

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

List.zip in Init.Data.List.Basic

LT in Init.Prelude

IsTotal in Mathlib.Order.Defs.Unbundled

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))

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)
  }

Multiset.filter in Mathlib.Data.Multiset.Filter

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

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

Set.range in Mathlib.Data.Set.Operations

inferInstanceAs in Init.Prelude

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

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 σ)

instance : Inhabited (S' K₁ K₂ V) := ⟨S'.initial K₁ K₂ V⟩

def toBlock (σ : Scontract K₁ K₂ V C Sigma)
            (request : Request K₁ K₂ C Sigma Pi V) : Option (Block K₁ K₂ C Sigma V) :=
  if ¬request.isValid
  then .none
  else .some <|
  match request with
   
  | .deposit r v            => .deposit r v
   
  | .transfer a e c s sigma => .transfer a e c s sigma
   
  | .withdrawal π           => .withdrawal (π.toBalanceF σ)

instance : Preorder (Option V₊) := inferInstance

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

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

structure CommitT (C K Pi : Type) where
  commitment : C
  dict       : Dict K Pi

Subtype.val in Init.Prelude

iInf in Mathlib.Order.SetNotation

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

Multiset in Mathlib.Data.Multiset.Defs

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

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 -/
  ⟩

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 -/

Finset.range in Mathlib.Data.Finset.Range

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

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

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

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₂'

Finset.sort in Mathlib.Data.Finset.Sort

Correctness : ∀ (l : List (Kₚ × Kₛ)) (_ : ∀ pair ∈ l, pair ←ᵣ KeyGen) (m : M),
                  let (kₚs, kₛs) := l.unzip
                  Verify kₚs m (Aggregate (kₚs.zip (kₛs.map (Sign · m)))) = true

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 -/
  ⟩

Unforgeability :
    ComputationallyInfeasible <|
      ∃ (k : List (Kₚ × Kₛ)) (m : M) (σ : Sigma),
        let kₚs := k.map Prod.fst
        Verify kₚs m σ = true ∧
        
        
        ∃ userIdx : Fin k.length,
          let (honestₚ, honestₛ) := k[userIdx]
          honestₚ ∈ kₚs ∧ ∃ key : Kₛ, key ≠ honestₛ ∧ Sign key m = σ

correct_keys_eq : ∀ {dict : Dict K M}, (Commit dict).keys = dict.keys

GetElem in Init.GetElem

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 -/

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

Multiset.map in Mathlib.Data.Multiset.MapFold

Option.get in Init.Data.Option.Basic

Sigma.mk in Init.Core

OfNat in Init.Prelude
</all_available_defs>

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

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 π₁ π₂)

@[simp]
lemma discretePreorder_eq_equality_Kbar {a b : Kbar K₁ K₂} : a ≤ b ↔ a = b

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

lemma length_transactionsInBlock :
  (TransactionsInBlock π₁ b).length = (TransactionsInBlock π₂ b).length

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

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

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

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

lemma le_of_ext_le {α : Type} [Preorder α] {v₁ v₂ : Vector α n}
  (h : ∀ i : Fin n, v₁.1[i] ≤ v₂.1[i]) : v₁ ≤ v₂

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

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

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

@[simp]
lemma discretePreorder_eq_equality_Vplus {a b : V₊} : a ≤ b ↔ a = b

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

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

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

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

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

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 computeBalance'_nil : computeBalance' ([] : Scontract K₁ K₂ V C Sigma) v = v

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

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

lemma f_transfer_block_source' (h : b.isTransferBlock) :
  ((TransactionsInBlock π b).foldl f σ).1 .Source = σ .Source

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

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

@[simp]
lemma attackGameBlocks'!_cons :
  attackGameBlocks'! (hd :: requests) σ = attackGameBlocks'! requests (σ ++ [hd.toBlock! σ])

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

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

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

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

@[simp]
lemma v'_cast_nonneg : 0 ≤ ↑(v' v b' s)

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

private lemma lemma5_aux {len : ℕ} {σ : Scontract K₁ K₂ V C Sigma}
  (hlen : len = σ.length) :
  (Bal π σ) Kbar.Source =
  (∑ x ∈ (Finset.univ : Finset (Fin σ.length)) ×ˢ Finset.univ,
      if h : σ[x.1].isWithdrawalBlock then
        (σ[x.1].getWithdrawal h x.2).1 ⊓ ((Bal π (List.take (x.1.1) σ)) x.2)
      else 0) -
  ∑ i : Fin (List.length σ), if h : σ[i].isDepositBlock then (σ[↑i].getDeposit h).2 else 0

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

lemma appendBlock_eq_appendBlock!_of_isValid (h : request.isValid) :
  appendBlock σ request = appendBlock! σ request

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

Option.isSome_iff_ne_none in Init.Data.Option.Lemmas

@[simp]
lemma fStar_nil : fStar [] s = s

@[simp]
lemma mem_list_singleton_iff : π ∈ ({acc} : List (BalanceProof K₁ K₂ C Pi V)) ↔ π = acc

omit [Finite K₁] [Finite K₂] in
private lemma fold_f_any_transaction_transfer {acc : S K₁ K₂ V} {l : List (Τ K₁ K₂ V)}
  (h : ∀ T ∈ l, (¬ T.1.1 matches .Source) ∧ (¬ T.1.2.1 matches .Source)) :
  (List.foldl f acc l) .Source = acc .Source

lemma sender_transactionsInBlocks {bs : List (Block K₁ K₂ C Sigma V)}
                                  {π₁ π₂ : BalanceProof K₁ K₂ C Pi V} :
  (TransactionsInBlocks π₁ bs).map (λ s ↦ s.1.1) =
  (TransactionsInBlocks π₂ bs).map (λ s ↦ s.1.1)

lemma attackGameR_eq_attackGameBlocks' :
  attackGameR requests σ = attackGameBlocks'!r requests σ

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

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

@[simp]
lemma transactionsInBlocks_nil :
  TransactionsInBlocks (Pi := Pi) (K₁ := K₁) (K₂ := K₂) (V := V) (C := C) (Sigma := Sigma) π [] = []

lemma f_deposit_source''
  (h : b.isDepositBlock) (h₁ : T ∈ TransactionsInBlock π b) : 
  (f σ T).1 .Source = σ .Source + -T.value.get (isSome_of_deposit ⟨⟨b, h⟩, h₁⟩)

lemma iso_K_merge_left_of_ne_none (h : π K ≠ none) : π K ≅ (π <+> acc) K

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

lemma mem_of_BalanceProof_le (h : π ≤ π') (h₁ : k ∈ π) : k ∈ π'

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

@[simp]
lemma aggregateDeposits_cons {hd} {tl : List (Block K₁ K₂ C Sigma V)} :
  aggregateDeposits (hd :: tl) =
  (if h : hd.isDepositBlock
   then (hd.getDeposit h).2.1
   else 0) +
  aggregateDeposits tl

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

lemma f_withdraw_source'
  (h : ∃ block : {b : Block K₁ K₂ C Sigma V // b.isWithdrawalBlock},
         T ∈ TransactionsInBlock π block.1) :
  (f σ T).1 .Source = σ .Source + (↑(T.value.get (isSome_of_withdrawal h)) ⊓ σ T.sender)

@[simp]
lemma fc_key : 0 ≤ fc (τc, b) (.key k)

lemma f_transfer_block_source (h : b.isTransferBlock) :
  ((TransactionsInBlock π b).foldl f σ) .Source = σ .Source

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

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

@[simp]
lemma BalanceProof.compat_rfl : π₁ <≅> π₁

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

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

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

lemma computeBalance_eq_sum : computeBalance σ = computeBalanceSum σ

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

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

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

lemma f_transfer_source
  (h : ∃ block : {b : Block K₁ K₂ C Sigma V // b.isTransferBlock},
         T ∈ TransactionsInBlock π block.1) :
  (f σ T) .Source = σ .Source

lemma proposition4W {x y : Option ((Pi × ExtraDataT) × TransactionBatch K₁ K₂ V)}
  (h : x.isSome ∧ y.isSome → x = y) : IsLUB {x, y} (Dict.First x y)

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

@[simp]
lemma v'_zero : v' 0 b s = 0

@[simp]
lemma transactionsInBlock_deposit {r : K₂} {v : V₊} :
  TransactionsInBlock (K₁ := K₁) (Sigma := Sigma) π (Block.deposit r v) =
  [⟨(.Source, r, v), by simp [Τ'.isValid]⟩]

lemma toBlock_eq_toBlock!_of_isValid (h : request.isValid) :
  (toBlock σ request) = toBlock! σ request

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

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

lemma f_withdraw_source
  (h : ∃ block : {b : Block K₁ K₂ C Sigma V // b.isWithdrawalBlock},
         T ∈ TransactionsInBlock π block.1) :
  (f σ T) .Source = σ .Source + (↑(T.value.get (isSome_of_withdrawal h)) ⊓ σ T.sender)

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

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

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

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

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

private lemma V'_eq_range {b : S K₁ K₂ V} {T : Τ K₁ K₂ V} {k : Kbar K₁ K₂} :
  V' b T k =
  Set.range λ (x : { x : (Τc K₁ K₂ V × S K₁ K₂ V) // (T, b) ≤ (↑x.1, x.2) }) ↦ fc ↑x k

omit [Finite K₂] [LinearOrder K₂] in
private lemma f_withdrawal_block_source_aux {l : List K₁}
  (h₀ : l.Nodup) (h : b.isWithdrawalBlock) :
  (List.foldl f' σ
    (List.map (λ s : K₁ ↦ ⟨(s, Kbar.Source, some (b.getWithdrawal h s)), by unfold Τ'.isValid; aesop⟩) l)).1
                            .Source = σ .Source + ∑ x : K₁, if x ∈ l then (↑(b.getWithdrawal h x) ⊓ σ x) else 0

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

lemma f_IsGLB_of_V' {b : S K₁ K₂ V} {T : Τ K₁ K₂ V} {k : Kbar K₁ K₂} :
  IsGLB (V' b T k) (f b T k)

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

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

@[simp]
lemma v'_source_eq_v : v' v b .Source = v

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

lemma V'_sset_V'_of_le {b₁ b₂ : S K₁ K₂ V} {T₁ T₂ : Τ K₁ K₂ V} {k : Kbar K₁ K₂}
  (h : b₁ ≤ b₂) (h₁ : T₁ ≤ T₂) : 
  V' b₂ T₂ k ⊆ V' b₁ T₁ k

@[simp]
lemma isValid_coe {s : S K₁ K₂ V} : S'.isValid (V := V) (K₁ := K₁) (K₂ := K₂) ↑s

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

@[mono]
lemma fc_mono {τc τc' : Τc K₁ K₂ V} {b₁ b₂ : S K₁ K₂ V}
              (h : (τc, b₁) ≤ (τc', b₂)) : fc (τc, b₁) ≤ fc (τc', b₂)

lemma toBlock_σ_isWithdrawalBlock (σ σ' : Scontract K₁ K₂ V C Sigma) :
  (request.toBlock! σ).isWithdrawalBlock ↔
  (request.toBlock! σ').isWithdrawalBlock

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

lemma appendBlock_eq_id_of_not_isValid (h : ¬request.isValid) :
  appendBlock σ request = σ

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

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

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

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

lemma first_right (h : x₁.isNone) : First x₁ x₂ = x₂

lemma nonneg_e : 0 ≤ e i j

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

@[simp]
lemma discretePreorder_eq_equality_TransactionBatch [Finite K₁] [Finite K₂]
  {a b : TransactionBatch K₁ K₂ V} : a ≤ b ↔ a = b

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

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 ..

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

@[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

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

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

lemma f_transfer_source'
  (h : ∃ block : {b : Block K₁ K₂ C Sigma V // b.isTransferBlock},
         T ∈ TransactionsInBlock π block.1) :
  (f σ T) .Source = σ .Source

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

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

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

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

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

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

lemma sum_fStar_le_zero : ∑ (k : Kbar K₁ K₂), fStar Tstar (S.initial K₁ K₂ V) k ≤ 0

lemma toBlock!_of_transfer (h : request matches .transfer ..) :
  request.toBlock! σ matches .transfer ..

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'

@[simp]
lemma BalanceProof.snd_discrete {x y : TransactionBatch K₁ K₂ V} :
  @LE.le (TransactionBatch K₁ K₂ V) Preorder.toLE x y ↔ x = y

lemma length_TransactionsInBlock_transfer
  {b : { b : Block K₁ K₂ C Sigma V // b.isTransferBlock }} :
  ∀ (π₁ π₂ : BalanceProof K₁ K₂ C Pi V),
    (TransactionsInBlock_transfer π₁ b).length =
    (TransactionsInBlock_transfer π₂ b).length

lemma Merge_split (h₀ : 0 < i) (h₁ : i ≤ πs.length) :
  mergeR'' (πs.take i) acc =
  mergeR'' (πs.take (i - 1)) acc <+> πs[i - 1]

lemma isSome_of_withdrawal
  (h : ∃ block : {b : Block K₁ K₂ C Sigma V // b.isWithdrawalBlock},
         T ∈ TransactionsInBlock π block.1) : T.value.isSome

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

congr_fun in Batteries.Logic

lemma batch_eq_iff {π₁k π₂k : (Pi × ExtraDataT) × TransactionBatch K₁ K₂ V} :
  (π₁k ≅ π₂k) ↔ π₁k.2 = π₂k.2

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 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 s_ne_r_of_isValid (h : isValid ⟨s, r, v?⟩) : s ≠ r

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

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

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

lemma f_withdrawal_block_source (h : b.isWithdrawalBlock) :
  ((TransactionsInBlock π b).foldl f σ) .Source = σ .Source + ∑ k : K₁, (b.getWithdrawal h k).1 ⊓ σ k

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

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

theorem injective {α : Type} [Finite α]
  (f : UniquelyIndexed α) : Function.Injective f

@[simp]
lemma discretePreorder_eq_equality_Pi_Prod_ExtraDataT {a b : (Pi × ExtraDataT)} : a ≤ b

lemma f_deposit_source
  (h : ∃ block : {b : Block K₁ K₂ C Sigma V // b.isDepositBlock},
         T ∈ TransactionsInBlock π block.1) :
  (f σ T) .Source = σ .Source + -T.value.get (isSome_of_deposit h)

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

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 zip_nodup_of_nodup_right {α β : Type} {l₁ : List α} {l₂ : List β}
  (h : l₂.Nodup) : (l₁.zip l₂).Nodup

lemma le_mergeR''_aux {π acc : BalanceProof K₁ K₂ C Pi V}
                      {πs : List (BalanceProof K₁ K₂ C Pi V)}
                      {k : C × K₂}
                      (h₀ : π k ≤ acc k)
                      (h : ∀ acc : BalanceProof K₁ K₂ C Pi V, acc ∈ πs → π k ≤ acc k) :
                      π k ≤ mergeR'' πs acc k

@[simp]
lemma some_iso_some :
  (Option.some x ≅ .some y) ↔ x ≅ y

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

@[simp]
lemma bal_nil : Bal (Sigma := Sigma) π [] = S.initial K₁ K₂ V

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

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))

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

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

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

private lemma BalFixed_eq_BalFixed' : BalFixed bs π = BalFixed' bs π

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

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

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

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

@[simp]
lemma fStar_cons {hd : Τ K₁ K₂ V} {tl : List (Τ K₁ K₂ V)} :
  fStar (hd :: tl) s = fStar tl (f s hd)

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

lemma toBlock!_of_withdrawal (h : request matches .withdrawal ..) :
  request.toBlock! σ matches .withdrawal ..

@[simp]
lemma discretePreorder_eq_equality_Key_Map_Vplus {a b : Key K₁ K₂ → V₊} : a ≤ b ↔ a = b

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

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

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

lemma notin_of_BalanceProof_le_notin (h : π ≤ π') (h₁ : k ∉ π') : k ∉ π

@[simp]
lemma length_TransactionsInBlock_withdrawal
  {b : { b : Block K₁ K₂ C Sigma V // b.isWithdrawalBlock }} :
  (TransactionsInBlock_withdrawal b).length = Nat.card K₁

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

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

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 f_transfer_source''
  (h : b.isTransferBlock) (h₁ : T ∈ TransactionsInBlock π b) : 
  (f σ T) .Source = σ .Source

lemma eq_of_BalanceProof_le (h : π ≤ π') (h₁ : k ∈ π) (h₂ : k ∈ π') :
  ((π k).get h₁).2 = ((π' k).get h₂).2

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

lemma f_eq_f' : f = f' (K₁ := K₁) (K₂ := K₂) (V := V)

lemma proposition5 [Preorder Y] {f g : X → Y} {join : X → Y} :
  IsLUB {f, g} join ↔ ∀ x : X, IsLUB {f x, g x} (join x)

lemma lemma3 : Bal π bs .Source ≤ 0

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

@[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

lemma isValid_iff : isValid (s, r, v?) ↔ s ≠ r ∧ (s matches .Source → 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 length_transactionsInBlocks {bs : List (Block K₁ K₂ C Sigma V)}
                                  {π₁ π₂ : BalanceProof K₁ K₂ C Pi V} :
  (TransactionsInBlocks π₁ bs).length = (TransactionsInBlocks π₂ bs).length

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

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 v'_key_eq_meet {k : Key K₁ K₂} : v' v b (Kbar.key k) = ⟨v ⊓ b k, by simp⟩

@[simp]
lemma transactionsInBlocks_append_singleton :
  TransactionsInBlocks π (bs ++ [b]) =
  (TransactionsInBlocks π bs) ++ (TransactionsInBlock π b)

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

@[simp]
lemma merge_eq_none :
  (π <+> acc) K = none ↔ π K = none ∧ acc K = none

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

<local_ctx>
import FVIntmax.AttackGame

import FVIntmax.Lemma3

import FVIntmax.Lemma4

import FVIntmax.Lemma5

import FVIntmax.Propositions

import FVIntmax.Request

import FVIntmax.Wheels

import FVIntmax.Wheels.AuthenticatedDictionary

import FVIntmax.Wheels.SignatureAggregation

import Mathlib

namespace Intmax

open Classical

noncomputable section Intmax

noncomputable section theorem1

section AttackGame

variable {Sigma Pi M : Type}
         {C : Type} [Nonempty C]
         {V : Type}
         [Lattice V] [AddCommGroup V]
         [CovariantClass V V (· + ·) (· ≤ ·)]
         [CovariantClass V V (Function.swap (· + ·)) (· ≤ ·)]
         {K₁ : Type} [Nonempty K₁] [Finite K₁] [LinearOrder K₁]
         {K₂ : Type} [Finite K₂] [LinearOrder K₂]
         {Kₚ : Type} [Nonempty Kₚ]
         {Kₛ : Type} [Nonempty Kₛ]

def mergeR'' (πs : List (BalanceProof K₁ K₂ C Pi V)) (acc : BalanceProof K₁ K₂ C Pi V) : BalanceProof K₁ K₂ C Pi V :=
  match πs with
  | [] => acc
  | π :: πs => Dict.Merge acc (mergeR'' πs π)

section MergeLemmas

variable {acc π : BalanceProof K₁ K₂ C Pi V} {πs πs : List (BalanceProof K₁ K₂ C Pi V)}

end MergeLemmas

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

notation:51 π₁:52 " <≅> " π₂:52 => BalanceProof.compat π₁ π₂

notation:65 π₁:65 " <+> " π₂:66 => Dict.Merge π₁ π₂

section Compat

variable {π₁ π₂ π₃ : BalanceProof K₁ K₂ C Pi V}

end Compat

section MergeLemmas

variable {π acc : BalanceProof K₁ K₂ C Pi V}
         {πs : List (BalanceProof K₁ K₂ C Pi V)}

end MergeLemmas

variable [AD : ADScheme K₂ (C × K₁ × ExtraDataT) C Pi]

section MergeLemmas

variable {π acc : BalanceProof K₁ K₂ C Pi V}
         {πs : List (BalanceProof K₁ K₂ C Pi V)}
</local_ctx>

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

