Theorem: BabySNARK.is_sound
Proof state before:
case intro.intro.intro
F : Type
inst✝ : Field F
n_stmt n_wit n_var : ℕ
u_stmt : Fin n_stmt → Polynomial F
u_wit : Fin n_wit → Polynomial F
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_stmt : Fin n_stmt → Polynomial F
w_wit : Fin n_wit → Polynomial F
t : Polynomial F
ht : (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum = t
ht0 : t.Monic
stmt : BabySNARK.Stmt
prover : Prover F BabySNARK
hI_00 :
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
                (List.finRange n_var)).sum *
            (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum +
          (0 + (0 + 0)) +
        (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum *
          (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum +
      ((List.map (fun x => Polynomial.C (if ↑x = 0 then 1 else 0) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum *
          (List.map (fun x => Polynomial.C (if ↑x = 0 then 1 else 0) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum +
        (-0 + (-0 + (-0 + -0)) + -0 + (-0 + (-0 + (-0 + -0)) + -0) + (-0 + (-0 + (-0 + -0)) + -0) +
            (-((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
                        (List.finRange n_var)).sum *
                    (List.map
                        (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
                        (List.finRange n_var)).sum) +
                (-0 + (-0 + -0)) +
              -((List.map
                      (fun x =>
                        Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                          Polynomial.X ^ ↑x)
                      (List.finRange n_var)).sum *
                  (List.map
                      (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
                      (List.finRange n_var)).sum)) +
          ((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
                    (List.finRange n_var)).sum *
                (List.map
                    (fun x =>
                      -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                          Polynomial.X ^ ↑x))
                    (List.finRange n_var)).sum +
              (0 + (0 + 0)) +
            (List.map
                  (fun x =>
                    Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x)
                  (List.finRange n_var)).sum *
              (List.map
                  (fun x =>
                    -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                        Polynomial.X ^ ↑x))
                  (List.finRange n_var)).sum))) =
    0
hI_01 hI_02 :
  0 + (0 + (0 + 0)) + 0 +
      (0 +
        (-0 + (-0 + (-0 + -0)) + -0 + (-0 + (-0 + (-0 + -0)) + -0) + (-0 + (-0 + (-0 + -0)) + -0) +
            (0 + (-0 + (-0 + -0)) + 0) +
          (0 + (0 + (0 + 0)) + 0))) =
    0
hI_10 :
  0 +
          (Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) *
              (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum +
            (0 +
              (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
                    (List.finRange n_wit)).sum *
                (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum)) +
        0 +
      (0 +
        (-((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
                            (List.finRange n_var)).sum *
                        (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                            (List.finRange n_wit)).sum) +
                    (-0 + (-0 + -0)) +
                  -((List.map
                          (fun x =>
                            Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                              Polynomial.X ^ ↑x)
                          (List.finRange n_var)).sum *
                      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                          (List.finRange n_wit)).sum) +
                (-0 + (-0 + (-0 + -0)) + -0) +
              (-((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
                          (List.finRange n_var)).sum *
                      Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)) +
                  (-0 + (-0 + -0)) +
                -((List.map
                        (fun x =>
                          Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                            Polynomial.X ^ ↑x)
                        (List.finRange n_var)).sum *
                    Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ))) +
            (0 +
                (-(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
                      (List.map
                          (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
                          (List.finRange n_var)).sum) +
                  (-0 +
                    -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                            (List.finRange n_wit)).sum *
                        (List.map
                            (fun x =>
                              Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
                            (List.finRange n_var)).sum))) +
              0) +
          (0 +
              (Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
                  (List.map
                      (fun x =>
                        -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                            Polynomial.X ^ ↑x))
                      (List.finRange n_var)).sum +
                (0 +
                  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                        (List.finRange n_wit)).sum *
                    (List.map
                        (fun x =>
                          -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                              Polynomial.X ^ ↑x))
                        (List.finRange n_var)).sum)) +
            0))) =
    0
hI_11 :
  0 +
          (0 +
            (Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γβ) *
                (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum +
              0)) +
        0 +
      (0 +
        (-0 + (-0 + (-0 + -0)) + -0 +
                (-((List.map
                            (fun x =>
                              Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
                            (List.finRange n_var)).sum *
                        Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ)) +
                    (-0 + (-0 + -0)) +
                  -((List.map
                          (fun x =>
                            Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                              Polynomial.X ^ ↑x)
                          (List.finRange n_var)).sum *
                      Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ))) +
              (-0 + (-0 + (-0 + -0)) + -0) +
            (0 +
                (-0 +
                  (-(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) *
                        (List.map
                            (fun x =>
                              Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
                            (List.finRange n_var)).sum) +
                    -0)) +
              0) +
          (0 +
              (0 +
                (Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) *
                    (List.map
                        (fun x =>
                          -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                              Polynomial.X ^ ↑x))
                        (List.finRange n_var)).sum +
                  0)) +
            0))) =
    0
hI_12 :
  0 + (0 + (0 + 0)) + 0 +
      (0 +
        (-0 + (-0 + (-0 + -0)) + -0 + (-0 + (-0 + (-0 + -0)) + -0) + (-0 + (-0 + (-0 + -0)) + -0) +
            (0 + (-0 + (-0 + -0)) + 0) +
          (0 + (0 + (0 + 0)) + 0))) =
    0
hI_20 :
  0 + (0 + (0 + 0)) + 0 +
      (0 +
        (-0 +
                    (-(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
                          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                              (List.finRange n_wit)).sum) +
                      (-0 +
                        -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                                (List.finRange n_wit)).sum *
                            (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                                (List.finRange n_wit)).sum))) +
                  -0 +
                (-0 + (-0 + (-0 + -0)) + -0) +
              (-0 +
                  (-(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
                        Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)) +
                    (-0 +
                      -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                              (List.finRange n_wit)).sum *
                          Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)))) +
                -0) +
            (0 + (-0 + (-0 + -0)) + 0) +
          (0 + (0 + (0 + 0)) + 0))) =
    0
hI_21 :
  0 + (0 + (0 + 0)) + 0 +
      (0 +
        (-0 +
                    (-0 +
                      (-(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) *
                            (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                                (List.finRange n_wit)).sum) +
                        -0)) +
                  -0 +
                (-0 +
                    (-(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
                          Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ)) +
                      (-0 +
                        -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                                (List.finRange n_wit)).sum *
                            Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ)))) +
                  -0) +
              (-0 +
                  (-0 +
                    (-(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) *
                          Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)) +
                      -0)) +
                -0) +
            (0 + (-0 + (-0 + -0)) + 0) +
          (0 + (0 + (0 + 0)) + 0))) =
    0
hI_22 :
  0 + (0 + (0 + 0)) + 0 +
      (0 +
        (-0 + (-0 + (-0 + -0)) + -0 +
                (-0 +
                    (-0 +
                      (-(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) *
                            Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ)) +
                        -0)) +
                  -0) +
              (-0 + (-0 + (-0 + -0)) + -0) +
            (0 + (-0 + (-0 + -0)) + 0) +
          (0 + (0 + (0 + 0)) + 0))) =
    0
hII_00 hII_01 hII_02 : 0 + (0 + (0 + 0)) + (-0 + -0 + -0 + -0) = 0
hII_10 :
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
            (List.finRange n_var)).sum +
        (0 + (0 + 0)) +
      (-0 + -0 + -0 + -0) =
    0
hII_11 :
  0 + (0 + (0 + 0)) +
      (-0 + -0 + -0 +
        -(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum) =
    0
hII_12 : 0 + (0 + (0 + 0)) + (-0 + -0 + -0 + -0) = 0
hII_20 :
  0 +
        (Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γ) +
          (0 +
            (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum)) +
      (-0 + -0 + -0 + -0) =
    0
hII_21 :
  0 + (0 + (Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γβ) + 0)) +
      (-(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                  (List.finRange n_wit)).sum +
            -0 +
          -Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
        -0) =
    0
hII_22 : 0 + (0 + (0 + 0)) + (-0 + -Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ) + -0 + -0) = 0
hH_00 :
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
          (List.finRange n_var)).sum +
      (0 + (0 + 0)) =
    (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
          (List.finRange n_var)).sum +
      (0 + (0 + 0))
hH_01 hH_02 : True
hH_10 :
  0 +
      (Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) +
        (0 +
          (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum)) =
    0 +
      (Polynomial.C (prover.2 Proof_Idx.H SRS_Elements_Idx.γ) +
        (0 +
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum))
hH_11 :
  0 + (0 + (Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γβ) + 0)) =
    0 + (0 + (Polynomial.C (prover.2 Proof_Idx.H SRS_Elements_Idx.γβ) + 0))
hH_12 hH_20 hH_21 hH_22 : True
hV_00 :
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
          (List.finRange n_var)).sum +
      (0 + (0 + 0)) =
    (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
          (List.finRange n_var)).sum +
      (0 + (0 + 0))
hV_01 hV_02 : True
hV_10 :
  0 +
      (Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) +
        (0 +
          (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum)) =
    0 +
      (Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
        (0 +
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum))
hV_11 :
  0 + (0 + (Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) + 0)) =
    0 + (0 + (Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ) + 0))
hV_12 hV_20 hV_21 hV_22 : True
hB_00 :
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
          (List.finRange n_var)).sum +
      (0 + (0 + 0)) =
    (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
          (List.finRange n_var)).sum +
      (0 + (0 + 0))
hB_01 hB_02 : True
hB_10 :
  0 +
      (Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γ) +
        (0 +
          (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum)) =
    0 +
      (Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γ) +
        (0 +
          (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum))
hB_11 :
  0 + (0 + (Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γβ) + 0)) =
    0 + (0 + (Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γβ) + 0))
hB_12 hB_20 hB_21 hB_22 : True
⊢ ((List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)).sum +
          (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu i)) * u_wit i)
              (List.finRange n_wit)).sum) ^
        2 -
      1 =
    t *
      (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu i)) * u_wit i)
          (List.finRange n_wit)).sum
Tactic:
simp only [neg_zero, add_zero, zero_add] at hI_00 hI_01 hI_02 hI_10 hI_11 hI_12 hI_20 hI_21 hI_22 hII_00 hII_01 hII_02 hII_10 hII_11 hII_12 hII_20 hII_21 hII_22 hH_00 hH_01 hH_02 hH_10 hH_11 hH_12 hH_20 hH_21 hH_22 hV_00 hV_01 hV_02 hV_10 hV_11 hV_12 hV_20 hV_21 hV_22 hB_00 hB_01 hB_02 hB_10 hB_11 hB_12 hB_20 hB_21 hB_22
Proof state after:
case intro.intro.intro
F : Type
inst✝ : Field F
n_stmt n_wit n_var : ℕ
u_stmt : Fin n_stmt → Polynomial F
u_wit : Fin n_wit → Polynomial F
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_stmt : Fin n_stmt → Polynomial F
w_wit : Fin n_wit → Polynomial F
t : Polynomial F
ht : (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum = t
ht0 : t.Monic
stmt : BabySNARK.Stmt
prover : Prover F BabySNARK
hH_01 hH_02 hH_12 hH_20 hH_21 hH_22 hV_01 hV_02 hV_12 hV_20 hV_21 hV_22 hB_01 hB_02 hB_12 hB_20 hB_21 hB_22 : True
hI_00 :
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
              (List.finRange n_var)).sum *
          (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum +
        (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum *
          (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum +
      ((List.map (fun x => Polynomial.C (if ↑x = 0 then 1 else 0) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum *
          (List.map (fun x => Polynomial.C (if ↑x = 0 then 1 else 0) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum +
        (-((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
                    (List.finRange n_var)).sum *
                (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
                    (List.finRange n_var)).sum) +
            -((List.map
                    (fun x =>
                      Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                        Polynomial.X ^ ↑x)
                    (List.finRange n_var)).sum *
                (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
                    (List.finRange n_var)).sum) +
          ((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
                  (List.finRange n_var)).sum *
              (List.map
                  (fun x =>
                    -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                        Polynomial.X ^ ↑x))
                  (List.finRange n_var)).sum +
            (List.map
                  (fun x =>
                    Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x)
                  (List.finRange n_var)).sum *
              (List.map
                  (fun x =>
                    -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                        Polynomial.X ^ ↑x))
                  (List.finRange n_var)).sum))) =
    0
hI_01 hI_02 : True
hI_10 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) *
          (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum +
        (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum *
          (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum +
      (-((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
                      (List.finRange n_var)).sum *
                  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                      (List.finRange n_wit)).sum) +
              -((List.map
                      (fun x =>
                        Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                          Polynomial.X ^ ↑x)
                      (List.finRange n_var)).sum *
                  (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                      (List.finRange n_wit)).sum) +
            (-((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
                      (List.finRange n_var)).sum *
                  Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)) +
              -((List.map
                      (fun x =>
                        Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                          Polynomial.X ^ ↑x)
                      (List.finRange n_var)).sum *
                  Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ))) +
          (-(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
                (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
                    (List.finRange n_var)).sum) +
            -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                    (List.finRange n_wit)).sum *
                (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
                    (List.finRange n_var)).sum)) +
        (Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
            (List.map
                (fun x =>
                  -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x))
                (List.finRange n_var)).sum +
          (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum *
            (List.map
                (fun x =>
                  -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                      Polynomial.X ^ ↑x))
                (List.finRange n_var)).sum)) =
    0
hI_11 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γβ) *
        (List.map (fun x => Polynomial.C (t.coeff ↑x) * Polynomial.X ^ ↑x) (List.finRange n_var)).sum +
      (-((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
                    (List.finRange n_var)).sum *
                Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ)) +
            -((List.map
                    (fun x =>
                      Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                        Polynomial.X ^ ↑x)
                    (List.finRange n_var)).sum *
                Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ)) +
          -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) *
              (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
                  (List.finRange n_var)).sum) +
        Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) *
          (List.map
              (fun x =>
                -(Polynomial.C (List.map (fun j => stmt j * (u_stmt j).coeff ↑x) (List.finRange n_stmt)).sum *
                    Polynomial.X ^ ↑x))
              (List.finRange n_var)).sum) =
    0
hI_12 : True
hI_20 :
  -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
            (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum) +
        -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum *
            (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum) +
      (-(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
            Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)) +
        -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum *
            Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ))) =
    0
hI_21 :
  -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) *
            (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                (List.finRange n_wit)).sum) +
        (-(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) *
              Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ)) +
          -((List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
                  (List.finRange n_wit)).sum *
              Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ))) +
      -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) *
          Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)) =
    0
hI_22 :
  -(Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) * Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ)) =
    0
hII_00 hII_01 hII_02 : True
hII_10 :
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
        (List.finRange n_var)).sum =
    0
hII_11 :
  -(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
          (List.finRange n_var)).sum =
    0
hII_12 : True
hII_20 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    0
hII_21 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γβ) +
      (-(List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
              (List.finRange n_wit)).sum +
        -Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ)) =
    0
hII_22 : -Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ) = 0
hH_00 :
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
        (List.finRange n_var)).sum =
    (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
        (List.finRange n_var)).sum
hH_10 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.H SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.H (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hH_11 :
  Polynomial.C (prover.1 Proof_Idx.H SRS_Elements_Idx.γβ) = Polynomial.C (prover.2 Proof_Idx.H SRS_Elements_Idx.γβ)
hV_00 :
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
        (List.finRange n_var)).sum =
    (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
        (List.finRange n_var)).sum
hV_10 :
  Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.V (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hV_11 :
  Polynomial.C (prover.1 Proof_Idx.V SRS_Elements_Idx.γβ) = Polynomial.C (prover.2 Proof_Idx.V SRS_Elements_Idx.γβ)
hB_00 :
  (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
        (List.finRange n_var)).sum =
    (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.τ_pow x)) * Polynomial.X ^ ↑x)
        (List.finRange n_var)).sum
hB_10 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum =
    Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γ) +
      (List.map (fun x => Polynomial.C (prover.2 Proof_Idx.B (SRS_Elements_Idx.βu x)) * u_wit x)
          (List.finRange n_wit)).sum
hB_11 :
  Polynomial.C (prover.1 Proof_Idx.B SRS_Elements_Idx.γβ) = Polynomial.C (prover.2 Proof_Idx.B SRS_Elements_Idx.γβ)
⊢ ((List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)).sum +
          (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.B (SRS_Elements_Idx.βu i)) * u_wit i)
              (List.finRange n_wit)).sum) ^
        2 -
      1 =
    t *
      (List.map (fun i => Polynomial.C (prover.1 Proof_Idx.H (SRS_Elements_Idx.βu i)) * u_wit i)
          (List.finRange n_wit)).sum