Theorem: GGPR.soundness (FormalSnarksProject/SNARKs/GGPR.lean)

State before:
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
⊢ AGMProofSystemInstantiation.soundness F GGPR ((Fin n_wit → F) × (Fin m → F))
    (fun stmt wit =>
      let t := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i));
      ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
                (List.map (fun i => Polynomial.C (wit.1 i) * v_wit i) (List.finRange n_wit)).sum) *
              (w_0 + (List.map (fun i => Polynomial.C (wit.2 i) * w_wit i) (List.finRange m)).sum)).modByMonic
          t =
        0)
    fun prover =>
    (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
      prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i))
Tactic:
unfold AGMProofSystemInstantiation.soundness AGMProofSystemInstantiation.verify AGMProofSystemInstantiation.proof_element_G1_as_poly AGMProofSystemInstantiation.proof_element_G2_as_poly
State after:
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
⊢ ∀ (stmt : GGPR.Stmt) (prover : AGMProofSystemInstantiation.Prover F GGPR),
    ((∀ (check_idx : GGPR.EqualityChecks), GGPR.check_poly prover stmt check_idx = 0) ∧
        ∀ pfs ∈ GGPR.Identified_Proof_Elems,
          (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * GGPR.SRSElementValue_G1 SRS_elem)
                GGPR.ListSRSElements_G1).sum =
            (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * GGPR.SRSElementValue_G2 SRS_elem)
                GGPR.ListSRSElements_G2).sum) →
      (fun stmt wit =>
          let t := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i));
          ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
                    (List.map (fun i => Polynomial.C (wit.1 i) * v_wit i) (List.finRange n_wit)).sum) *
                  (w_0 + (List.map (fun i => Polynomial.C (wit.2 i) * w_wit i) (List.finRange m)).sum)).modByMonic
              t =
            0)
        stmt
        ((fun prover =>
            (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
              prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
          prover)

State before:
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
⊢ ∀ (stmt : GGPR.Stmt) (prover : AGMProofSystemInstantiation.Prover F GGPR),
    ((∀ (check_idx : GGPR.EqualityChecks), GGPR.check_poly prover stmt check_idx = 0) ∧
        ∀ pfs ∈ GGPR.Identified_Proof_Elems,
          (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * GGPR.SRSElementValue_G1 SRS_elem)
                GGPR.ListSRSElements_G1).sum =
            (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * GGPR.SRSElementValue_G2 SRS_elem)
                GGPR.ListSRSElements_G2).sum) →
      (fun stmt wit =>
          let t := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i));
          ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
                    (List.map (fun i => Polynomial.C (wit.1 i) * v_wit i) (List.finRange n_wit)).sum) *
                  (w_0 + (List.map (fun i => Polynomial.C (wit.2 i) * w_wit i) (List.finRange m)).sum)).modByMonic
              t =
            0)
        stmt
        ((fun prover =>
            (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
              prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
          prover)
Tactic:
intros stmt prover eqns'
State after:
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
stmt : GGPR.Stmt
prover : AGMProofSystemInstantiation.Prover F GGPR
eqns' :
  (∀ (check_idx : GGPR.EqualityChecks), GGPR.check_poly prover stmt check_idx = 0) ∧
    ∀ pfs ∈ GGPR.Identified_Proof_Elems,
      (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * GGPR.SRSElementValue_G1 SRS_elem)
            GGPR.ListSRSElements_G1).sum =
        (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * GGPR.SRSElementValue_G2 SRS_elem)
            GGPR.ListSRSElements_G2).sum
⊢ let t := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i));
  ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).1
                        i) *
                    v_wit i)
                (List.finRange n_wit)).sum) *
          (w_0 +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).2
                        i) *
                    w_wit i)
                (List.finRange m)).sum)).modByMonic
      t =
    0

State before:
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
stmt : GGPR.Stmt
prover : AGMProofSystemInstantiation.Prover F GGPR
eqns' :
  (∀ (check_idx : GGPR.EqualityChecks), GGPR.check_poly prover stmt check_idx = 0) ∧
    ∀ pfs ∈ GGPR.Identified_Proof_Elems,
      (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * GGPR.SRSElementValue_G1 SRS_elem)
            GGPR.ListSRSElements_G1).sum =
        (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * GGPR.SRSElementValue_G2 SRS_elem)
            GGPR.ListSRSElements_G2).sum
⊢ let t := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i));
  ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).1
                        i) *
                    v_wit i)
                (List.finRange n_wit)).sum) *
          (w_0 +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).2
                        i) *
                    w_wit i)
                (List.finRange m)).sum)).modByMonic
      t =
    0
Tactic:
rcases eqns' with ⟨eqns, null⟩
State after:
case intro
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
stmt : GGPR.Stmt
prover : AGMProofSystemInstantiation.Prover F GGPR
eqns : ∀ (check_idx : GGPR.EqualityChecks), GGPR.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ GGPR.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * GGPR.SRSElementValue_G1 SRS_elem)
          GGPR.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * GGPR.SRSElementValue_G2 SRS_elem)
          GGPR.ListSRSElements_G2).sum
⊢ let t := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i));
  ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).1
                        i) *
                    v_wit i)
                (List.finRange n_wit)).sum) *
          (w_0 +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).2
                        i) *
                    w_wit i)
                (List.finRange m)).sum)).modByMonic
      t =
    0

State before:
case intro
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
stmt : GGPR.Stmt
prover : AGMProofSystemInstantiation.Prover F GGPR
eqns : ∀ (check_idx : GGPR.EqualityChecks), GGPR.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ GGPR.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * GGPR.SRSElementValue_G1 SRS_elem)
          GGPR.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * GGPR.SRSElementValue_G2 SRS_elem)
          GGPR.ListSRSElements_G2).sum
⊢ let t := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i));
  ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).1
                        i) *
                    v_wit i)
                (List.finRange n_wit)).sum) *
          (w_0 +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).2
                        i) *
                    w_wit i)
                (List.finRange m)).sum)).modByMonic
      t =
    0
Tactic:
intro t
State after:
case intro
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
stmt : GGPR.Stmt
prover : AGMProofSystemInstantiation.Prover F GGPR
eqns : ∀ (check_idx : GGPR.EqualityChecks), GGPR.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ GGPR.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * GGPR.SRSElementValue_G1 SRS_elem)
          GGPR.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * GGPR.SRSElementValue_G2 SRS_elem)
          GGPR.ListSRSElements_G2).sum
t : Polynomial F := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i))
⊢ ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).1
                        i) *
                    v_wit i)
                (List.finRange n_wit)).sum) *
          (w_0 +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).2
                        i) *
                    w_wit i)
                (List.finRange m)).sum)).modByMonic
      t =
    0

State before:
case intro
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
stmt : GGPR.Stmt
prover : AGMProofSystemInstantiation.Prover F GGPR
eqns : ∀ (check_idx : GGPR.EqualityChecks), GGPR.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ GGPR.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * GGPR.SRSElementValue_G1 SRS_elem)
          GGPR.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * GGPR.SRSElementValue_G2 SRS_elem)
          GGPR.ListSRSElements_G2).sum
t : Polynomial F := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i))
⊢ ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).1
                        i) *
                    v_wit i)
                (List.finRange n_wit)).sum) *
          (w_0 +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).2
                        i) *
                    w_wit i)
                (List.finRange m)).sum)).modByMonic
      t =
    0
Tactic:
have eqnI := eqns ChecksIdx.CheckI
State after:
case intro
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
stmt : GGPR.Stmt
prover : AGMProofSystemInstantiation.Prover F GGPR
eqns : ∀ (check_idx : GGPR.EqualityChecks), GGPR.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ GGPR.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * GGPR.SRSElementValue_G1 SRS_elem)
          GGPR.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * GGPR.SRSElementValue_G2 SRS_elem)
          GGPR.ListSRSElements_G2).sum
t : Polynomial F := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i))
eqnI : GGPR.check_poly prover stmt ChecksIdx.CheckI = 0
⊢ ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).1
                        i) *
                    v_wit i)
                (List.finRange n_wit)).sum) *
          (w_0 +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).2
                        i) *
                    w_wit i)
                (List.finRange m)).sum)).modByMonic
      t =
    0

State before:
case intro
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
stmt : GGPR.Stmt
prover : AGMProofSystemInstantiation.Prover F GGPR
eqns : ∀ (check_idx : GGPR.EqualityChecks), GGPR.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ GGPR.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * GGPR.SRSElementValue_G1 SRS_elem)
          GGPR.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * GGPR.SRSElementValue_G2 SRS_elem)
          GGPR.ListSRSElements_G2).sum
t : Polynomial F := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i))
eqnI : GGPR.check_poly prover stmt ChecksIdx.CheckI = 0
⊢ ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).1
                        i) *
                    v_wit i)
                (List.finRange n_wit)).sum) *
          (w_0 +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).2
                        i) *
                    w_wit i)
                (List.finRange m)).sum)).modByMonic
      t =
    0
Tactic:
have eqnII := eqns ChecksIdx.CheckII
State after:
case intro
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
stmt : GGPR.Stmt
prover : AGMProofSystemInstantiation.Prover F GGPR
eqns : ∀ (check_idx : GGPR.EqualityChecks), GGPR.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ GGPR.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * GGPR.SRSElementValue_G1 SRS_elem)
          GGPR.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * GGPR.SRSElementValue_G2 SRS_elem)
          GGPR.ListSRSElements_G2).sum
t : Polynomial F := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i))
eqnI : GGPR.check_poly prover stmt ChecksIdx.CheckI = 0
eqnII : GGPR.check_poly prover stmt ChecksIdx.CheckII = 0
⊢ ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).1
                        i) *
                    v_wit i)
                (List.finRange n_wit)).sum) *
          (w_0 +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).2
                        i) *
                    w_wit i)
                (List.finRange m)).sum)).modByMonic
      t =
    0

State before:
case intro
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
stmt : GGPR.Stmt
prover : AGMProofSystemInstantiation.Prover F GGPR
eqns : ∀ (check_idx : GGPR.EqualityChecks), GGPR.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ GGPR.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * GGPR.SRSElementValue_G1 SRS_elem)
          GGPR.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * GGPR.SRSElementValue_G2 SRS_elem)
          GGPR.ListSRSElements_G2).sum
t : Polynomial F := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i))
eqnI : GGPR.check_poly prover stmt ChecksIdx.CheckI = 0
eqnII : GGPR.check_poly prover stmt ChecksIdx.CheckII = 0
⊢ ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).1
                        i) *
                    v_wit i)
                (List.finRange n_wit)).sum) *
          (w_0 +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).2
                        i) *
                    w_wit i)
                (List.finRange m)).sum)).modByMonic
      t =
    0
Tactic:
have eqnIII := eqns ChecksIdx.CheckIII
State after:
case intro
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
stmt : GGPR.Stmt
prover : AGMProofSystemInstantiation.Prover F GGPR
eqns : ∀ (check_idx : GGPR.EqualityChecks), GGPR.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ GGPR.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * GGPR.SRSElementValue_G1 SRS_elem)
          GGPR.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * GGPR.SRSElementValue_G2 SRS_elem)
          GGPR.ListSRSElements_G2).sum
t : Polynomial F := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i))
eqnI : GGPR.check_poly prover stmt ChecksIdx.CheckI = 0
eqnII : GGPR.check_poly prover stmt ChecksIdx.CheckII = 0
eqnIII : GGPR.check_poly prover stmt ChecksIdx.CheckIII = 0
⊢ ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).1
                        i) *
                    v_wit i)
                (List.finRange n_wit)).sum) *
          (w_0 +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).2
                        i) *
                    w_wit i)
                (List.finRange m)).sum)).modByMonic
      t =
    0

State before:
case intro
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
stmt : GGPR.Stmt
prover : AGMProofSystemInstantiation.Prover F GGPR
eqns : ∀ (check_idx : GGPR.EqualityChecks), GGPR.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ GGPR.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * GGPR.SRSElementValue_G1 SRS_elem)
          GGPR.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * GGPR.SRSElementValue_G2 SRS_elem)
          GGPR.ListSRSElements_G2).sum
t : Polynomial F := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i))
eqnI : GGPR.check_poly prover stmt ChecksIdx.CheckI = 0
eqnII : GGPR.check_poly prover stmt ChecksIdx.CheckII = 0
eqnIII : GGPR.check_poly prover stmt ChecksIdx.CheckIII = 0
⊢ ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).1
                        i) *
                    v_wit i)
                (List.finRange n_wit)).sum) *
          (w_0 +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).2
                        i) *
                    w_wit i)
                (List.finRange m)).sum)).modByMonic
      t =
    0
Tactic:
have eqnIV := eqns ChecksIdx.CheckIV
State after:
case intro
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
stmt : GGPR.Stmt
prover : AGMProofSystemInstantiation.Prover F GGPR
eqns : ∀ (check_idx : GGPR.EqualityChecks), GGPR.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ GGPR.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * GGPR.SRSElementValue_G1 SRS_elem)
          GGPR.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * GGPR.SRSElementValue_G2 SRS_elem)
          GGPR.ListSRSElements_G2).sum
t : Polynomial F := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i))
eqnI : GGPR.check_poly prover stmt ChecksIdx.CheckI = 0
eqnII : GGPR.check_poly prover stmt ChecksIdx.CheckII = 0
eqnIII : GGPR.check_poly prover stmt ChecksIdx.CheckIII = 0
eqnIV : GGPR.check_poly prover stmt ChecksIdx.CheckIV = 0
⊢ ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).1
                        i) *
                    v_wit i)
                (List.finRange n_wit)).sum) *
          (w_0 +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).2
                        i) *
                    w_wit i)
                (List.finRange m)).sum)).modByMonic
      t =
    0

State before:
case intro
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
stmt : GGPR.Stmt
prover : AGMProofSystemInstantiation.Prover F GGPR
eqns : ∀ (check_idx : GGPR.EqualityChecks), GGPR.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ GGPR.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * GGPR.SRSElementValue_G1 SRS_elem)
          GGPR.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * GGPR.SRSElementValue_G2 SRS_elem)
          GGPR.ListSRSElements_G2).sum
t : Polynomial F := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i))
eqnI : GGPR.check_poly prover stmt ChecksIdx.CheckI = 0
eqnII : GGPR.check_poly prover stmt ChecksIdx.CheckII = 0
eqnIII : GGPR.check_poly prover stmt ChecksIdx.CheckIII = 0
eqnIV : GGPR.check_poly prover stmt ChecksIdx.CheckIV = 0
⊢ ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).1
                        i) *
                    v_wit i)
                (List.finRange n_wit)).sum) *
          (w_0 +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).2
                        i) *
                    w_wit i)
                (List.finRange m)).sum)).modByMonic
      t =
    0
Tactic:
have eqnV := eqns ChecksIdx.CheckV
State after:
case intro
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
stmt : GGPR.Stmt
prover : AGMProofSystemInstantiation.Prover F GGPR
eqns : ∀ (check_idx : GGPR.EqualityChecks), GGPR.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ GGPR.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * GGPR.SRSElementValue_G1 SRS_elem)
          GGPR.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * GGPR.SRSElementValue_G2 SRS_elem)
          GGPR.ListSRSElements_G2).sum
t : Polynomial F := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i))
eqnI : GGPR.check_poly prover stmt ChecksIdx.CheckI = 0
eqnII : GGPR.check_poly prover stmt ChecksIdx.CheckII = 0
eqnIII : GGPR.check_poly prover stmt ChecksIdx.CheckIII = 0
eqnIV : GGPR.check_poly prover stmt ChecksIdx.CheckIV = 0
eqnV : GGPR.check_poly prover stmt ChecksIdx.CheckV = 0
⊢ ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).1
                        i) *
                    v_wit i)
                (List.finRange n_wit)).sum) *
          (w_0 +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).2
                        i) *
                    w_wit i)
                (List.finRange m)).sum)).modByMonic
      t =
    0

State before:
case intro
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
stmt : GGPR.Stmt
prover : AGMProofSystemInstantiation.Prover F GGPR
eqns : ∀ (check_idx : GGPR.EqualityChecks), GGPR.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ GGPR.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * GGPR.SRSElementValue_G1 SRS_elem)
          GGPR.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * GGPR.SRSElementValue_G2 SRS_elem)
          GGPR.ListSRSElements_G2).sum
t : Polynomial F := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i))
eqnI : GGPR.check_poly prover stmt ChecksIdx.CheckI = 0
eqnII : GGPR.check_poly prover stmt ChecksIdx.CheckII = 0
eqnIII : GGPR.check_poly prover stmt ChecksIdx.CheckIII = 0
eqnIV : GGPR.check_poly prover stmt ChecksIdx.CheckIV = 0
eqnV : GGPR.check_poly prover stmt ChecksIdx.CheckV = 0
⊢ ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).1
                        i) *
                    v_wit i)
                (List.finRange n_wit)).sum) *
          (w_0 +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).2
                        i) *
                    w_wit i)
                (List.finRange m)).sum)).modByMonic
      t =
    0
Tactic:
clear eqns null
State after:
case intro
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
stmt : GGPR.Stmt
prover : AGMProofSystemInstantiation.Prover F GGPR
t : Polynomial F := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i))
eqnI : GGPR.check_poly prover stmt ChecksIdx.CheckI = 0
eqnII : GGPR.check_poly prover stmt ChecksIdx.CheckII = 0
eqnIII : GGPR.check_poly prover stmt ChecksIdx.CheckIII = 0
eqnIV : GGPR.check_poly prover stmt ChecksIdx.CheckIV = 0
eqnV : GGPR.check_poly prover stmt ChecksIdx.CheckV = 0
⊢ ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).1
                        i) *
                    v_wit i)
                (List.finRange n_wit)).sum) *
          (w_0 +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).2
                        i) *
                    w_wit i)
                (List.finRange m)).sum)).modByMonic
      t =
    0

State before:
case intro
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
stmt : GGPR.Stmt
prover : AGMProofSystemInstantiation.Prover F GGPR
t : Polynomial F := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i))
eqnI : GGPR.check_poly prover stmt ChecksIdx.CheckI = 0
eqnII : GGPR.check_poly prover stmt ChecksIdx.CheckII = 0
eqnIII : GGPR.check_poly prover stmt ChecksIdx.CheckIII = 0
eqnIV : GGPR.check_poly prover stmt ChecksIdx.CheckIV = 0
eqnV : GGPR.check_poly prover stmt ChecksIdx.CheckV = 0
⊢ ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).1
                        i) *
                    v_wit i)
                (List.finRange n_wit)).sum) *
          (w_0 +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).2
                        i) *
                    w_wit i)
                (List.finRange m)).sum)).modByMonic
      t =
    0
Tactic:
simp_rw [GGPR] at eqnI eqnII eqnIII eqnIV eqnV
State after:
case intro
F : Type
inst✝ : Field F
n_stmt n_wit m d : ℕ
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_wit : Fin m → Polynomial F
v_0 w_0 : Polynomial F
r : Fin n_wit → F
stmt : GGPR.Stmt
prover : AGMProofSystemInstantiation.Prover F GGPR
t : Polynomial F := ∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i))
eqnI :
  { Stmt := Fin n_stmt → F, Sample := Option Vars, SRSElements_G1 := SRS_Elements_Idx,
          ListSRSElements_G1 :=
            List.map (fun i => SRS_Elements_Idx.EK_s_pow i) (List.finRange d) ++
                              List.map (fun i => SRS_Elements_Idx.EK_α_s_pow i) (List.finRange d) ++
                            List.map (fun i => SRS_Elements_Idx.EK_v i) (List.finRange n_wit) ++
                          List.map (fun i => SRS_Elements_Idx.EK_w i) (List.finRange m) ++
                        List.map (fun i => SRS_Elements_Idx.EK_α_v i) (List.finRange n_wit) ++
                      List.map (fun i => SRS_Elements_Idx.EK_α_w i) (List.finRange m) ++
                    List.map (fun i => SRS_Elements_Idx.EK_β_v i) (List.finRange n_wit) ++
                  List.map (fun i => SRS_Elements_Idx.EK_β_w i) (List.finRange m) ++
                [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ,
                  SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t] ++
              List.map (fun i => SRS_Elements_Idx.VK_v_stmt i) (List.finRange n_stmt),
          SRSElements_G2 := SRS_Elements_Idx,
          ListSRSElements_G2 :=
            List.map (fun i => SRS_Elements_Idx.EK_s_pow i) (List.finRange d) ++
                              List.map (fun i => SRS_Elements_Idx.EK_α_s_pow i) (List.finRange d) ++
                            List.map (fun i => SRS_Elements_Idx.EK_v i) (List.finRange n_wit) ++
                          List.map (fun i => SRS_Elements_Idx.EK_w i) (List.finRange m) ++
                        List.map (fun i => SRS_Elements_Idx.EK_α_v i) (List.finRange n_wit) ++
                      List.map (fun i => SRS_Elements_Idx.EK_α_w i) (List.finRange m) ++
                    List.map (fun i => SRS_Elements_Idx.EK_β_v i) (List.finRange n_wit) ++
                  List.map (fun i => SRS_Elements_Idx.EK_β_w i) (List.finRange m) ++
                [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ,
                  SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t] ++
              List.map (fun i => SRS_Elements_Idx.VK_v_stmt i) (List.finRange n_stmt),
          SRSElementValue_G1 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_Idx.EK_s_pow i => poly_s ^ ↑i
            | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ ↑i
            | SRS_Elements_Idx.EK_v i => (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_w i => (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_α_v i => poly_α * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_α_w i => poly_α * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_β_v i => poly_β_v * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_β_w i => poly_β_w * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.VK_1 => 1
            | SRS_Elements_Idx.VK_α => poly_α
            | SRS_Elements_Idx.VK_γ => poly_γ
            | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
            | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
            | SRS_Elements_Idx.VK_v_0 => (to_MvPolynomial_Option Vars) v_0
            | SRS_Elements_Idx.VK_w_0 => (to_MvPolynomial_Option Vars) w_0
            | SRS_Elements_Idx.VK_t =>
              (to_MvPolynomial_Option Vars) (∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i)))
            | SRS_Elements_Idx.VK_v_stmt i => (to_MvPolynomial_Option Vars) (v_stmt i),
          SRSElementValue_G2 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_Idx.EK_s_pow i => poly_s ^ ↑i
            | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ ↑i
            | SRS_Elements_Idx.EK_v i => (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_w i => (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_α_v i => poly_α * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_α_w i => poly_α * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_β_v i => poly_β_v * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_β_w i => poly_β_w * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.VK_1 => 1
            | SRS_Elements_Idx.VK_α => poly_α
            | SRS_Elements_Idx.VK_γ => poly_γ
            | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
            | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
            | SRS_Elements_Idx.VK_v_0 => (to_MvPolynomial_Option Vars) v_0
            | SRS_Elements_Idx.VK_w_0 => (to_MvPolynomial_Option Vars) w_0
            | SRS_Elements_Idx.VK_t =>
              (to_MvPolynomial_Option Vars) (∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i)))
            | SRS_Elements_Idx.VK_v_stmt i => (to_MvPolynomial_Option Vars) (v_stmt i),
          Proof_G1 := Proof_G1_Idx,
          ListProof_G1 := [Proof_G1_Idx.V_mid, Proof_G1_Idx.V_mid', Proof_G1_Idx.W', Proof_G1_Idx.Y, Proof_G1_Idx.H'],
          Proof_G2 := Proof_G2_Idx, ListProof_G2 := [Proof_G2_Idx.W, Proof_G2_Idx.H], EqualityChecks := ChecksIdx,
          Pairings := fun check_idx =>
            match check_idx with
            | ChecksIdx.CheckI => PairingsI_Idx
            | ChecksIdx.CheckII => PairingsII_Idx
            | ChecksIdx.CheckIII => PairingsIII_Idx
            | ChecksIdx.CheckIV => PairingsIV_Idx
            | ChecksIdx.CheckV => PairingsV_Idx,
          ListPairings := fun check_idx =>
            match check_idx with
            | ChecksIdx.CheckI => [PairingsI_Idx.lhs, PairingsI_Idx.rhs]
            | ChecksIdx.CheckII => [PairingsII_Idx.lhs, PairingsII_Idx.rhs]
            | ChecksIdx.CheckIII => [PairingsIII_Idx.lhs, PairingsIII_Idx.rhs]
            | ChecksIdx.CheckIV => [PairingsIV_Idx.lhs, PairingsIV_Idx.rhs]
            | ChecksIdx.CheckV => [PairingsV_Idx.lhs, PairingsV_Idx.rhs1, PairingsV_Idx.rhs2],
          verificationPairingSRS_G1 := fun stmt check_idx i SRS_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_v_0 => 1
                | SRS_Elements_Idx.VK_v_stmt k => stmt k
                | x => 0
              | PairingsI_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_t => 1
                | x => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs => 0
              | PairingsII_Idx.rhs => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs => 0
              | PairingsIII_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => 1
                | x => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs => 0
              | PairingsIV_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => 1
                | x => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs => 0
              | PairingsV_Idx.rhs1 => 0
              | PairingsV_Idx.rhs2 =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_βw_γ => 1
                | x => 0,
          verificationPairingSRS_G2 := fun stmt check_idx i SRS_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_w_0 => 1
                | x => 0
              | PairingsI_Idx.rhs => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsII_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => -1
                | x => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsIII_Idx.rhs => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsIV_Idx.rhs => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_γ => 1
                | x => 0
              | PairingsV_Idx.rhs1 =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_βv_γ => -1
                | x => 0
              | PairingsV_Idx.rhs2 => 0,
          verificationPairingProof_G1 := fun stmt check_idx i pf_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
              | PairingsI_Idx.rhs => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid' => 1
                | x => 0
              | PairingsII_Idx.rhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.W' => 1
                | x => 0
              | PairingsIII_Idx.rhs => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.H' => 1
                | x => 0
              | PairingsIV_Idx.rhs => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.Y => 1
                | x => 0
              | PairingsV_Idx.rhs1 =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
              | PairingsV_Idx.rhs2 => 0,
          verificationPairingProof_G2 := fun stmt check_idx i pf_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match pf_idx with
                | Proof_G2_Idx.W => 1
                | x => 0
              | PairingsI_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.H => -1
                | x => 0
            | ChecksIdx.CheckII, i => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs => 0
              | PairingsIII_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.W => -1
                | x => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs => 0
              | PairingsIV_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.H => -1
                | x => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs => 0
              | PairingsV_Idx.rhs1 => 0
              | PairingsV_Idx.rhs2 =>
                match pf_idx with
                | Proof_G2_Idx.W => -1
                | x => 0,
          Identified_Proof_Elems := [] }.check_poly
      prover stmt ChecksIdx.CheckI =
    0
eqnII :
  { Stmt := Fin n_stmt → F, Sample := Option Vars, SRSElements_G1 := SRS_Elements_Idx,
          ListSRSElements_G1 :=
            List.map (fun i => SRS_Elements_Idx.EK_s_pow i) (List.finRange d) ++
                              List.map (fun i => SRS_Elements_Idx.EK_α_s_pow i) (List.finRange d) ++
                            List.map (fun i => SRS_Elements_Idx.EK_v i) (List.finRange n_wit) ++
                          List.map (fun i => SRS_Elements_Idx.EK_w i) (List.finRange m) ++
                        List.map (fun i => SRS_Elements_Idx.EK_α_v i) (List.finRange n_wit) ++
                      List.map (fun i => SRS_Elements_Idx.EK_α_w i) (List.finRange m) ++
                    List.map (fun i => SRS_Elements_Idx.EK_β_v i) (List.finRange n_wit) ++
                  List.map (fun i => SRS_Elements_Idx.EK_β_w i) (List.finRange m) ++
                [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ,
                  SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t] ++
              List.map (fun i => SRS_Elements_Idx.VK_v_stmt i) (List.finRange n_stmt),
          SRSElements_G2 := SRS_Elements_Idx,
          ListSRSElements_G2 :=
            List.map (fun i => SRS_Elements_Idx.EK_s_pow i) (List.finRange d) ++
                              List.map (fun i => SRS_Elements_Idx.EK_α_s_pow i) (List.finRange d) ++
                            List.map (fun i => SRS_Elements_Idx.EK_v i) (List.finRange n_wit) ++
                          List.map (fun i => SRS_Elements_Idx.EK_w i) (List.finRange m) ++
                        List.map (fun i => SRS_Elements_Idx.EK_α_v i) (List.finRange n_wit) ++
                      List.map (fun i => SRS_Elements_Idx.EK_α_w i) (List.finRange m) ++
                    List.map (fun i => SRS_Elements_Idx.EK_β_v i) (List.finRange n_wit) ++
                  List.map (fun i => SRS_Elements_Idx.EK_β_w i) (List.finRange m) ++
                [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ,
                  SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t] ++
              List.map (fun i => SRS_Elements_Idx.VK_v_stmt i) (List.finRange n_stmt),
          SRSElementValue_G1 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_Idx.EK_s_pow i => poly_s ^ ↑i
            | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ ↑i
            | SRS_Elements_Idx.EK_v i => (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_w i => (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_α_v i => poly_α * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_α_w i => poly_α * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_β_v i => poly_β_v * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_β_w i => poly_β_w * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.VK_1 => 1
            | SRS_Elements_Idx.VK_α => poly_α
            | SRS_Elements_Idx.VK_γ => poly_γ
            | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
            | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
            | SRS_Elements_Idx.VK_v_0 => (to_MvPolynomial_Option Vars) v_0
            | SRS_Elements_Idx.VK_w_0 => (to_MvPolynomial_Option Vars) w_0
            | SRS_Elements_Idx.VK_t =>
              (to_MvPolynomial_Option Vars) (∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i)))
            | SRS_Elements_Idx.VK_v_stmt i => (to_MvPolynomial_Option Vars) (v_stmt i),
          SRSElementValue_G2 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_Idx.EK_s_pow i => poly_s ^ ↑i
            | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ ↑i
            | SRS_Elements_Idx.EK_v i => (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_w i => (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_α_v i => poly_α * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_α_w i => poly_α * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_β_v i => poly_β_v * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_β_w i => poly_β_w * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.VK_1 => 1
            | SRS_Elements_Idx.VK_α => poly_α
            | SRS_Elements_Idx.VK_γ => poly_γ
            | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
            | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
            | SRS_Elements_Idx.VK_v_0 => (to_MvPolynomial_Option Vars) v_0
            | SRS_Elements_Idx.VK_w_0 => (to_MvPolynomial_Option Vars) w_0
            | SRS_Elements_Idx.VK_t =>
              (to_MvPolynomial_Option Vars) (∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i)))
            | SRS_Elements_Idx.VK_v_stmt i => (to_MvPolynomial_Option Vars) (v_stmt i),
          Proof_G1 := Proof_G1_Idx,
          ListProof_G1 := [Proof_G1_Idx.V_mid, Proof_G1_Idx.V_mid', Proof_G1_Idx.W', Proof_G1_Idx.Y, Proof_G1_Idx.H'],
          Proof_G2 := Proof_G2_Idx, ListProof_G2 := [Proof_G2_Idx.W, Proof_G2_Idx.H], EqualityChecks := ChecksIdx,
          Pairings := fun check_idx =>
            match check_idx with
            | ChecksIdx.CheckI => PairingsI_Idx
            | ChecksIdx.CheckII => PairingsII_Idx
            | ChecksIdx.CheckIII => PairingsIII_Idx
            | ChecksIdx.CheckIV => PairingsIV_Idx
            | ChecksIdx.CheckV => PairingsV_Idx,
          ListPairings := fun check_idx =>
            match check_idx with
            | ChecksIdx.CheckI => [PairingsI_Idx.lhs, PairingsI_Idx.rhs]
            | ChecksIdx.CheckII => [PairingsII_Idx.lhs, PairingsII_Idx.rhs]
            | ChecksIdx.CheckIII => [PairingsIII_Idx.lhs, PairingsIII_Idx.rhs]
            | ChecksIdx.CheckIV => [PairingsIV_Idx.lhs, PairingsIV_Idx.rhs]
            | ChecksIdx.CheckV => [PairingsV_Idx.lhs, PairingsV_Idx.rhs1, PairingsV_Idx.rhs2],
          verificationPairingSRS_G1 := fun stmt check_idx i SRS_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_v_0 => 1
                | SRS_Elements_Idx.VK_v_stmt k => stmt k
                | x => 0
              | PairingsI_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_t => 1
                | x => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs => 0
              | PairingsII_Idx.rhs => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs => 0
              | PairingsIII_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => 1
                | x => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs => 0
              | PairingsIV_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => 1
                | x => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs => 0
              | PairingsV_Idx.rhs1 => 0
              | PairingsV_Idx.rhs2 =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_βw_γ => 1
                | x => 0,
          verificationPairingSRS_G2 := fun stmt check_idx i SRS_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_w_0 => 1
                | x => 0
              | PairingsI_Idx.rhs => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsII_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => -1
                | x => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsIII_Idx.rhs => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsIV_Idx.rhs => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_γ => 1
                | x => 0
              | PairingsV_Idx.rhs1 =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_βv_γ => -1
                | x => 0
              | PairingsV_Idx.rhs2 => 0,
          verificationPairingProof_G1 := fun stmt check_idx i pf_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
              | PairingsI_Idx.rhs => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid' => 1
                | x => 0
              | PairingsII_Idx.rhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.W' => 1
                | x => 0
              | PairingsIII_Idx.rhs => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.H' => 1
                | x => 0
              | PairingsIV_Idx.rhs => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.Y => 1
                | x => 0
              | PairingsV_Idx.rhs1 =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
              | PairingsV_Idx.rhs2 => 0,
          verificationPairingProof_G2 := fun stmt check_idx i pf_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match pf_idx with
                | Proof_G2_Idx.W => 1
                | x => 0
              | PairingsI_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.H => -1
                | x => 0
            | ChecksIdx.CheckII, i => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs => 0
              | PairingsIII_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.W => -1
                | x => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs => 0
              | PairingsIV_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.H => -1
                | x => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs => 0
              | PairingsV_Idx.rhs1 => 0
              | PairingsV_Idx.rhs2 =>
                match pf_idx with
                | Proof_G2_Idx.W => -1
                | x => 0,
          Identified_Proof_Elems := [] }.check_poly
      prover stmt ChecksIdx.CheckII =
    0
eqnIII :
  { Stmt := Fin n_stmt → F, Sample := Option Vars, SRSElements_G1 := SRS_Elements_Idx,
          ListSRSElements_G1 :=
            List.map (fun i => SRS_Elements_Idx.EK_s_pow i) (List.finRange d) ++
                              List.map (fun i => SRS_Elements_Idx.EK_α_s_pow i) (List.finRange d) ++
                            List.map (fun i => SRS_Elements_Idx.EK_v i) (List.finRange n_wit) ++
                          List.map (fun i => SRS_Elements_Idx.EK_w i) (List.finRange m) ++
                        List.map (fun i => SRS_Elements_Idx.EK_α_v i) (List.finRange n_wit) ++
                      List.map (fun i => SRS_Elements_Idx.EK_α_w i) (List.finRange m) ++
                    List.map (fun i => SRS_Elements_Idx.EK_β_v i) (List.finRange n_wit) ++
                  List.map (fun i => SRS_Elements_Idx.EK_β_w i) (List.finRange m) ++
                [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ,
                  SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t] ++
              List.map (fun i => SRS_Elements_Idx.VK_v_stmt i) (List.finRange n_stmt),
          SRSElements_G2 := SRS_Elements_Idx,
          ListSRSElements_G2 :=
            List.map (fun i => SRS_Elements_Idx.EK_s_pow i) (List.finRange d) ++
                              List.map (fun i => SRS_Elements_Idx.EK_α_s_pow i) (List.finRange d) ++
                            List.map (fun i => SRS_Elements_Idx.EK_v i) (List.finRange n_wit) ++
                          List.map (fun i => SRS_Elements_Idx.EK_w i) (List.finRange m) ++
                        List.map (fun i => SRS_Elements_Idx.EK_α_v i) (List.finRange n_wit) ++
                      List.map (fun i => SRS_Elements_Idx.EK_α_w i) (List.finRange m) ++
                    List.map (fun i => SRS_Elements_Idx.EK_β_v i) (List.finRange n_wit) ++
                  List.map (fun i => SRS_Elements_Idx.EK_β_w i) (List.finRange m) ++
                [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ,
                  SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t] ++
              List.map (fun i => SRS_Elements_Idx.VK_v_stmt i) (List.finRange n_stmt),
          SRSElementValue_G1 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_Idx.EK_s_pow i => poly_s ^ ↑i
            | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ ↑i
            | SRS_Elements_Idx.EK_v i => (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_w i => (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_α_v i => poly_α * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_α_w i => poly_α * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_β_v i => poly_β_v * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_β_w i => poly_β_w * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.VK_1 => 1
            | SRS_Elements_Idx.VK_α => poly_α
            | SRS_Elements_Idx.VK_γ => poly_γ
            | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
            | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
            | SRS_Elements_Idx.VK_v_0 => (to_MvPolynomial_Option Vars) v_0
            | SRS_Elements_Idx.VK_w_0 => (to_MvPolynomial_Option Vars) w_0
            | SRS_Elements_Idx.VK_t =>
              (to_MvPolynomial_Option Vars) (∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i)))
            | SRS_Elements_Idx.VK_v_stmt i => (to_MvPolynomial_Option Vars) (v_stmt i),
          SRSElementValue_G2 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_Idx.EK_s_pow i => poly_s ^ ↑i
            | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ ↑i
            | SRS_Elements_Idx.EK_v i => (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_w i => (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_α_v i => poly_α * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_α_w i => poly_α * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_β_v i => poly_β_v * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_β_w i => poly_β_w * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.VK_1 => 1
            | SRS_Elements_Idx.VK_α => poly_α
            | SRS_Elements_Idx.VK_γ => poly_γ
            | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
            | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
            | SRS_Elements_Idx.VK_v_0 => (to_MvPolynomial_Option Vars) v_0
            | SRS_Elements_Idx.VK_w_0 => (to_MvPolynomial_Option Vars) w_0
            | SRS_Elements_Idx.VK_t =>
              (to_MvPolynomial_Option Vars) (∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i)))
            | SRS_Elements_Idx.VK_v_stmt i => (to_MvPolynomial_Option Vars) (v_stmt i),
          Proof_G1 := Proof_G1_Idx,
          ListProof_G1 := [Proof_G1_Idx.V_mid, Proof_G1_Idx.V_mid', Proof_G1_Idx.W', Proof_G1_Idx.Y, Proof_G1_Idx.H'],
          Proof_G2 := Proof_G2_Idx, ListProof_G2 := [Proof_G2_Idx.W, Proof_G2_Idx.H], EqualityChecks := ChecksIdx,
          Pairings := fun check_idx =>
            match check_idx with
            | ChecksIdx.CheckI => PairingsI_Idx
            | ChecksIdx.CheckII => PairingsII_Idx
            | ChecksIdx.CheckIII => PairingsIII_Idx
            | ChecksIdx.CheckIV => PairingsIV_Idx
            | ChecksIdx.CheckV => PairingsV_Idx,
          ListPairings := fun check_idx =>
            match check_idx with
            | ChecksIdx.CheckI => [PairingsI_Idx.lhs, PairingsI_Idx.rhs]
            | ChecksIdx.CheckII => [PairingsII_Idx.lhs, PairingsII_Idx.rhs]
            | ChecksIdx.CheckIII => [PairingsIII_Idx.lhs, PairingsIII_Idx.rhs]
            | ChecksIdx.CheckIV => [PairingsIV_Idx.lhs, PairingsIV_Idx.rhs]
            | ChecksIdx.CheckV => [PairingsV_Idx.lhs, PairingsV_Idx.rhs1, PairingsV_Idx.rhs2],
          verificationPairingSRS_G1 := fun stmt check_idx i SRS_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_v_0 => 1
                | SRS_Elements_Idx.VK_v_stmt k => stmt k
                | x => 0
              | PairingsI_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_t => 1
                | x => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs => 0
              | PairingsII_Idx.rhs => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs => 0
              | PairingsIII_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => 1
                | x => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs => 0
              | PairingsIV_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => 1
                | x => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs => 0
              | PairingsV_Idx.rhs1 => 0
              | PairingsV_Idx.rhs2 =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_βw_γ => 1
                | x => 0,
          verificationPairingSRS_G2 := fun stmt check_idx i SRS_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_w_0 => 1
                | x => 0
              | PairingsI_Idx.rhs => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsII_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => -1
                | x => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsIII_Idx.rhs => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsIV_Idx.rhs => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_γ => 1
                | x => 0
              | PairingsV_Idx.rhs1 =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_βv_γ => -1
                | x => 0
              | PairingsV_Idx.rhs2 => 0,
          verificationPairingProof_G1 := fun stmt check_idx i pf_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
              | PairingsI_Idx.rhs => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid' => 1
                | x => 0
              | PairingsII_Idx.rhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.W' => 1
                | x => 0
              | PairingsIII_Idx.rhs => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.H' => 1
                | x => 0
              | PairingsIV_Idx.rhs => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.Y => 1
                | x => 0
              | PairingsV_Idx.rhs1 =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
              | PairingsV_Idx.rhs2 => 0,
          verificationPairingProof_G2 := fun stmt check_idx i pf_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match pf_idx with
                | Proof_G2_Idx.W => 1
                | x => 0
              | PairingsI_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.H => -1
                | x => 0
            | ChecksIdx.CheckII, i => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs => 0
              | PairingsIII_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.W => -1
                | x => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs => 0
              | PairingsIV_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.H => -1
                | x => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs => 0
              | PairingsV_Idx.rhs1 => 0
              | PairingsV_Idx.rhs2 =>
                match pf_idx with
                | Proof_G2_Idx.W => -1
                | x => 0,
          Identified_Proof_Elems := [] }.check_poly
      prover stmt ChecksIdx.CheckIII =
    0
eqnIV :
  { Stmt := Fin n_stmt → F, Sample := Option Vars, SRSElements_G1 := SRS_Elements_Idx,
          ListSRSElements_G1 :=
            List.map (fun i => SRS_Elements_Idx.EK_s_pow i) (List.finRange d) ++
                              List.map (fun i => SRS_Elements_Idx.EK_α_s_pow i) (List.finRange d) ++
                            List.map (fun i => SRS_Elements_Idx.EK_v i) (List.finRange n_wit) ++
                          List.map (fun i => SRS_Elements_Idx.EK_w i) (List.finRange m) ++
                        List.map (fun i => SRS_Elements_Idx.EK_α_v i) (List.finRange n_wit) ++
                      List.map (fun i => SRS_Elements_Idx.EK_α_w i) (List.finRange m) ++
                    List.map (fun i => SRS_Elements_Idx.EK_β_v i) (List.finRange n_wit) ++
                  List.map (fun i => SRS_Elements_Idx.EK_β_w i) (List.finRange m) ++
                [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ,
                  SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t] ++
              List.map (fun i => SRS_Elements_Idx.VK_v_stmt i) (List.finRange n_stmt),
          SRSElements_G2 := SRS_Elements_Idx,
          ListSRSElements_G2 :=
            List.map (fun i => SRS_Elements_Idx.EK_s_pow i) (List.finRange d) ++
                              List.map (fun i => SRS_Elements_Idx.EK_α_s_pow i) (List.finRange d) ++
                            List.map (fun i => SRS_Elements_Idx.EK_v i) (List.finRange n_wit) ++
                          List.map (fun i => SRS_Elements_Idx.EK_w i) (List.finRange m) ++
                        List.map (fun i => SRS_Elements_Idx.EK_α_v i) (List.finRange n_wit) ++
                      List.map (fun i => SRS_Elements_Idx.EK_α_w i) (List.finRange m) ++
                    List.map (fun i => SRS_Elements_Idx.EK_β_v i) (List.finRange n_wit) ++
                  List.map (fun i => SRS_Elements_Idx.EK_β_w i) (List.finRange m) ++
                [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ,
                  SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t] ++
              List.map (fun i => SRS_Elements_Idx.VK_v_stmt i) (List.finRange n_stmt),
          SRSElementValue_G1 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_Idx.EK_s_pow i => poly_s ^ ↑i
            | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ ↑i
            | SRS_Elements_Idx.EK_v i => (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_w i => (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_α_v i => poly_α * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_α_w i => poly_α * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_β_v i => poly_β_v * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_β_w i => poly_β_w * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.VK_1 => 1
            | SRS_Elements_Idx.VK_α => poly_α
            | SRS_Elements_Idx.VK_γ => poly_γ
            | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
            | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
            | SRS_Elements_Idx.VK_v_0 => (to_MvPolynomial_Option Vars) v_0
            | SRS_Elements_Idx.VK_w_0 => (to_MvPolynomial_Option Vars) w_0
            | SRS_Elements_Idx.VK_t =>
              (to_MvPolynomial_Option Vars) (∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i)))
            | SRS_Elements_Idx.VK_v_stmt i => (to_MvPolynomial_Option Vars) (v_stmt i),
          SRSElementValue_G2 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_Idx.EK_s_pow i => poly_s ^ ↑i
            | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ ↑i
            | SRS_Elements_Idx.EK_v i => (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_w i => (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_α_v i => poly_α * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_α_w i => poly_α * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_β_v i => poly_β_v * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_β_w i => poly_β_w * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.VK_1 => 1
            | SRS_Elements_Idx.VK_α => poly_α
            | SRS_Elements_Idx.VK_γ => poly_γ
            | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
            | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
            | SRS_Elements_Idx.VK_v_0 => (to_MvPolynomial_Option Vars) v_0
            | SRS_Elements_Idx.VK_w_0 => (to_MvPolynomial_Option Vars) w_0
            | SRS_Elements_Idx.VK_t =>
              (to_MvPolynomial_Option Vars) (∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i)))
            | SRS_Elements_Idx.VK_v_stmt i => (to_MvPolynomial_Option Vars) (v_stmt i),
          Proof_G1 := Proof_G1_Idx,
          ListProof_G1 := [Proof_G1_Idx.V_mid, Proof_G1_Idx.V_mid', Proof_G1_Idx.W', Proof_G1_Idx.Y, Proof_G1_Idx.H'],
          Proof_G2 := Proof_G2_Idx, ListProof_G2 := [Proof_G2_Idx.W, Proof_G2_Idx.H], EqualityChecks := ChecksIdx,
          Pairings := fun check_idx =>
            match check_idx with
            | ChecksIdx.CheckI => PairingsI_Idx
            | ChecksIdx.CheckII => PairingsII_Idx
            | ChecksIdx.CheckIII => PairingsIII_Idx
            | ChecksIdx.CheckIV => PairingsIV_Idx
            | ChecksIdx.CheckV => PairingsV_Idx,
          ListPairings := fun check_idx =>
            match check_idx with
            | ChecksIdx.CheckI => [PairingsI_Idx.lhs, PairingsI_Idx.rhs]
            | ChecksIdx.CheckII => [PairingsII_Idx.lhs, PairingsII_Idx.rhs]
            | ChecksIdx.CheckIII => [PairingsIII_Idx.lhs, PairingsIII_Idx.rhs]
            | ChecksIdx.CheckIV => [PairingsIV_Idx.lhs, PairingsIV_Idx.rhs]
            | ChecksIdx.CheckV => [PairingsV_Idx.lhs, PairingsV_Idx.rhs1, PairingsV_Idx.rhs2],
          verificationPairingSRS_G1 := fun stmt check_idx i SRS_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_v_0 => 1
                | SRS_Elements_Idx.VK_v_stmt k => stmt k
                | x => 0
              | PairingsI_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_t => 1
                | x => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs => 0
              | PairingsII_Idx.rhs => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs => 0
              | PairingsIII_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => 1
                | x => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs => 0
              | PairingsIV_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => 1
                | x => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs => 0
              | PairingsV_Idx.rhs1 => 0
              | PairingsV_Idx.rhs2 =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_βw_γ => 1
                | x => 0,
          verificationPairingSRS_G2 := fun stmt check_idx i SRS_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_w_0 => 1
                | x => 0
              | PairingsI_Idx.rhs => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsII_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => -1
                | x => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsIII_Idx.rhs => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsIV_Idx.rhs => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_γ => 1
                | x => 0
              | PairingsV_Idx.rhs1 =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_βv_γ => -1
                | x => 0
              | PairingsV_Idx.rhs2 => 0,
          verificationPairingProof_G1 := fun stmt check_idx i pf_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
              | PairingsI_Idx.rhs => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid' => 1
                | x => 0
              | PairingsII_Idx.rhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.W' => 1
                | x => 0
              | PairingsIII_Idx.rhs => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.H' => 1
                | x => 0
              | PairingsIV_Idx.rhs => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.Y => 1
                | x => 0
              | PairingsV_Idx.rhs1 =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
              | PairingsV_Idx.rhs2 => 0,
          verificationPairingProof_G2 := fun stmt check_idx i pf_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match pf_idx with
                | Proof_G2_Idx.W => 1
                | x => 0
              | PairingsI_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.H => -1
                | x => 0
            | ChecksIdx.CheckII, i => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs => 0
              | PairingsIII_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.W => -1
                | x => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs => 0
              | PairingsIV_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.H => -1
                | x => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs => 0
              | PairingsV_Idx.rhs1 => 0
              | PairingsV_Idx.rhs2 =>
                match pf_idx with
                | Proof_G2_Idx.W => -1
                | x => 0,
          Identified_Proof_Elems := [] }.check_poly
      prover stmt ChecksIdx.CheckIV =
    0
eqnV :
  { Stmt := Fin n_stmt → F, Sample := Option Vars, SRSElements_G1 := SRS_Elements_Idx,
          ListSRSElements_G1 :=
            List.map (fun i => SRS_Elements_Idx.EK_s_pow i) (List.finRange d) ++
                              List.map (fun i => SRS_Elements_Idx.EK_α_s_pow i) (List.finRange d) ++
                            List.map (fun i => SRS_Elements_Idx.EK_v i) (List.finRange n_wit) ++
                          List.map (fun i => SRS_Elements_Idx.EK_w i) (List.finRange m) ++
                        List.map (fun i => SRS_Elements_Idx.EK_α_v i) (List.finRange n_wit) ++
                      List.map (fun i => SRS_Elements_Idx.EK_α_w i) (List.finRange m) ++
                    List.map (fun i => SRS_Elements_Idx.EK_β_v i) (List.finRange n_wit) ++
                  List.map (fun i => SRS_Elements_Idx.EK_β_w i) (List.finRange m) ++
                [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ,
                  SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t] ++
              List.map (fun i => SRS_Elements_Idx.VK_v_stmt i) (List.finRange n_stmt),
          SRSElements_G2 := SRS_Elements_Idx,
          ListSRSElements_G2 :=
            List.map (fun i => SRS_Elements_Idx.EK_s_pow i) (List.finRange d) ++
                              List.map (fun i => SRS_Elements_Idx.EK_α_s_pow i) (List.finRange d) ++
                            List.map (fun i => SRS_Elements_Idx.EK_v i) (List.finRange n_wit) ++
                          List.map (fun i => SRS_Elements_Idx.EK_w i) (List.finRange m) ++
                        List.map (fun i => SRS_Elements_Idx.EK_α_v i) (List.finRange n_wit) ++
                      List.map (fun i => SRS_Elements_Idx.EK_α_w i) (List.finRange m) ++
                    List.map (fun i => SRS_Elements_Idx.EK_β_v i) (List.finRange n_wit) ++
                  List.map (fun i => SRS_Elements_Idx.EK_β_w i) (List.finRange m) ++
                [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βv_γ,
                  SRS_Elements_Idx.VK_βw_γ, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_t] ++
              List.map (fun i => SRS_Elements_Idx.VK_v_stmt i) (List.finRange n_stmt),
          SRSElementValue_G1 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_Idx.EK_s_pow i => poly_s ^ ↑i
            | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ ↑i
            | SRS_Elements_Idx.EK_v i => (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_w i => (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_α_v i => poly_α * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_α_w i => poly_α * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_β_v i => poly_β_v * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_β_w i => poly_β_w * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.VK_1 => 1
            | SRS_Elements_Idx.VK_α => poly_α
            | SRS_Elements_Idx.VK_γ => poly_γ
            | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
            | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
            | SRS_Elements_Idx.VK_v_0 => (to_MvPolynomial_Option Vars) v_0
            | SRS_Elements_Idx.VK_w_0 => (to_MvPolynomial_Option Vars) w_0
            | SRS_Elements_Idx.VK_t =>
              (to_MvPolynomial_Option Vars) (∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i)))
            | SRS_Elements_Idx.VK_v_stmt i => (to_MvPolynomial_Option Vars) (v_stmt i),
          SRSElementValue_G2 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_Idx.EK_s_pow i => poly_s ^ ↑i
            | SRS_Elements_Idx.EK_α_s_pow i => poly_α * poly_s ^ ↑i
            | SRS_Elements_Idx.EK_v i => (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_w i => (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_α_v i => poly_α * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_α_w i => poly_α * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.EK_β_v i => poly_β_v * (to_MvPolynomial_Option Vars) (v_wit i)
            | SRS_Elements_Idx.EK_β_w i => poly_β_w * (to_MvPolynomial_Option Vars) (w_wit i)
            | SRS_Elements_Idx.VK_1 => 1
            | SRS_Elements_Idx.VK_α => poly_α
            | SRS_Elements_Idx.VK_γ => poly_γ
            | SRS_Elements_Idx.VK_βv_γ => poly_β_v * poly_γ
            | SRS_Elements_Idx.VK_βw_γ => poly_β_w * poly_γ
            | SRS_Elements_Idx.VK_v_0 => (to_MvPolynomial_Option Vars) v_0
            | SRS_Elements_Idx.VK_w_0 => (to_MvPolynomial_Option Vars) w_0
            | SRS_Elements_Idx.VK_t =>
              (to_MvPolynomial_Option Vars) (∏ i : Fin n_wit, (Polynomial.X - Polynomial.C (r i)))
            | SRS_Elements_Idx.VK_v_stmt i => (to_MvPolynomial_Option Vars) (v_stmt i),
          Proof_G1 := Proof_G1_Idx,
          ListProof_G1 := [Proof_G1_Idx.V_mid, Proof_G1_Idx.V_mid', Proof_G1_Idx.W', Proof_G1_Idx.Y, Proof_G1_Idx.H'],
          Proof_G2 := Proof_G2_Idx, ListProof_G2 := [Proof_G2_Idx.W, Proof_G2_Idx.H], EqualityChecks := ChecksIdx,
          Pairings := fun check_idx =>
            match check_idx with
            | ChecksIdx.CheckI => PairingsI_Idx
            | ChecksIdx.CheckII => PairingsII_Idx
            | ChecksIdx.CheckIII => PairingsIII_Idx
            | ChecksIdx.CheckIV => PairingsIV_Idx
            | ChecksIdx.CheckV => PairingsV_Idx,
          ListPairings := fun check_idx =>
            match check_idx with
            | ChecksIdx.CheckI => [PairingsI_Idx.lhs, PairingsI_Idx.rhs]
            | ChecksIdx.CheckII => [PairingsII_Idx.lhs, PairingsII_Idx.rhs]
            | ChecksIdx.CheckIII => [PairingsIII_Idx.lhs, PairingsIII_Idx.rhs]
            | ChecksIdx.CheckIV => [PairingsIV_Idx.lhs, PairingsIV_Idx.rhs]
            | ChecksIdx.CheckV => [PairingsV_Idx.lhs, PairingsV_Idx.rhs1, PairingsV_Idx.rhs2],
          verificationPairingSRS_G1 := fun stmt check_idx i SRS_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_v_0 => 1
                | SRS_Elements_Idx.VK_v_stmt k => stmt k
                | x => 0
              | PairingsI_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_t => 1
                | x => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs => 0
              | PairingsII_Idx.rhs => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs => 0
              | PairingsIII_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => 1
                | x => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs => 0
              | PairingsIV_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => 1
                | x => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs => 0
              | PairingsV_Idx.rhs1 => 0
              | PairingsV_Idx.rhs2 =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_βw_γ => 1
                | x => 0,
          verificationPairingSRS_G2 := fun stmt check_idx i SRS_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_w_0 => 1
                | x => 0
              | PairingsI_Idx.rhs => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsII_Idx.rhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_α => -1
                | x => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsIII_Idx.rhs => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_1 => 1
                | x => 0
              | PairingsIV_Idx.rhs => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_γ => 1
                | x => 0
              | PairingsV_Idx.rhs1 =>
                match SRS_idx with
                | SRS_Elements_Idx.VK_βv_γ => -1
                | x => 0
              | PairingsV_Idx.rhs2 => 0,
          verificationPairingProof_G1 := fun stmt check_idx i pf_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
              | PairingsI_Idx.rhs => 0
            | ChecksIdx.CheckII, i =>
              match i with
              | PairingsII_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid' => 1
                | x => 0
              | PairingsII_Idx.rhs =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.W' => 1
                | x => 0
              | PairingsIII_Idx.rhs => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.H' => 1
                | x => 0
              | PairingsIV_Idx.rhs => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs =>
                match pf_idx with
                | Proof_G1_Idx.Y => 1
                | x => 0
              | PairingsV_Idx.rhs1 =>
                match pf_idx with
                | Proof_G1_Idx.V_mid => 1
                | x => 0
              | PairingsV_Idx.rhs2 => 0,
          verificationPairingProof_G2 := fun stmt check_idx i pf_idx =>
            match check_idx, i with
            | ChecksIdx.CheckI, i =>
              match i with
              | PairingsI_Idx.lhs =>
                match pf_idx with
                | Proof_G2_Idx.W => 1
                | x => 0
              | PairingsI_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.H => -1
                | x => 0
            | ChecksIdx.CheckII, i => 0
            | ChecksIdx.CheckIII, i =>
              match i with
              | PairingsIII_Idx.lhs => 0
              | PairingsIII_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.W => -1
                | x => 0
            | ChecksIdx.CheckIV, i =>
              match i with
              | PairingsIV_Idx.lhs => 0
              | PairingsIV_Idx.rhs =>
                match pf_idx with
                | Proof_G2_Idx.H => -1
                | x => 0
            | ChecksIdx.CheckV, i =>
              match i with
              | PairingsV_Idx.lhs => 0
              | PairingsV_Idx.rhs1 => 0
              | PairingsV_Idx.rhs2 =>
                match pf_idx with
                | Proof_G2_Idx.W => -1
                | x => 0,
          Identified_Proof_Elems := [] }.check_poly
      prover stmt ChecksIdx.CheckV =
    0
⊢ ((v_0 + (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)).sum +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).1
                        i) *
                    v_wit i)
                (List.finRange n_wit)).sum) *
          (w_0 +
            (List.map
                (fun i =>
                  Polynomial.C
                      (((fun prover =>
                              (fun i => prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_v i), fun i =>
                                prover.2 Proof_G2_Idx.H (SRS_Elements_Idx.EK_β_w i)))
                            prover).2
                        i) *
                    w_wit i)
                (List.finRange m)).sum)).modByMonic
      t =
    0