EI002F

eisenstein_coordinate_norm_product

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

The genuine Eisenstein norm is multiplicative, from checked conjugation, commutativity and associativity, without a norm or polynomial oracle.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded first-order arithmetic statement

forall a b c d e f g h N M. (((((((((a) * (a))) + (((b) * (b))))) + (((((c) * (c))) + (((d) * (d))))))) + (((((a) * (d))) + (((b) * (c)))))) = ((((((((((a) * (b))) + (((b) * (a))))) + (((((c) * (d))) + (((d) * (c))))))) + (((((a) * (c))) + (((b) * (d))))))) + (N))) -> (((((((((e) * (e))) + (((f) * (f))))) + (((((g) * (g))) + (((h) * (h))))))) + (((((e) * (h))) + (((f) * (g)))))) = ((((((((((e) * (f))) + (((f) * (e))))) + (((((g) * (h))) + (((h) * (g))))))) + (((((e) * (g))) + (((f) * (h))))))) + (M))) -> (((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g)))))))))))) = ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (N * M)))

Constructive proof overview

Generated structural guide

The genuine Eisenstein norm is multiplicative, from checked conjugation, commutativity and associativity, without a norm or polynomial oracle.

The unchanged tactic script uses 10 declared prerequisites and contains 198 exact native proof lines.

Alpha v34 checked-use · first admitted v28 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

EI000C eisenstein_coordinate_norm_exists EI0028 eisenstein_conjugate_product_is_norm gaussian_equal_transitive Alpha theorem; checked-use authorized EI0023 eisenstein_product_integer_congruence EI002D eisenstein_product_conjugate gaussian_equal_reflexive Alpha theorem; checked-use authorized EI002E eisenstein_product_shuffle gaussian_equal_symmetric Alpha theorem; checked-use authorized mul_zero_left Stable theorem; checked-use authorized zero_add Stable theorem; checked-use authorized

Direct dependents

EI0033 eisenstein_signed_euclidean_division_exists EI003F eisenstein_norm_multiply

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

198 script commands · 30 reading checkpoints · 12 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (5)
eisenstein coordinate norm existseisenstein conjugate product is normeisenstein product integer congruenceeisenstein product conjugateeisenstein product shuffle

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro e
  6. L6
    intro f
  7. L7
    intro g
  8. L8
    intro h
  9. L9
    intro N
  10. L10
    intro M
02Fix variables and assumptionsL11–12

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro hfirst
  2. L12
    intro hsecond
03Establish hnormL13–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein coordinate norm exists.

  1. L13
    have hnorm : ∃ n. EisensteinCoordinateNorm(a · e + b · f + (c · h + d · g),a · f + b · e + (c · g + d · h),a · g + b · h + (c · e + d · f) + (c · h + d · g),a · h + b · g + (c · f + d · e) + (c · g + d · h),n)Definitions: EisensteinCoordinateNorm
  2. L14
    specialize eisenstein_coordinate_norm_exists ((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))
  3. L15
    specialize eisenstein_coordinate_norm_exists ((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))
  4. L16
    specialize eisenstein_coordinate_norm_exists ((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))
  5. L17
    specialize eisenstein_coordinate_norm_exists ((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))
  6. L18
    apply eisenstein_coordinate_norm_exists
04Separate the logical casesL19–19

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L19
    cases hnorm
05Establish hselfL20–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein conjugate product is norm.

  1. L20
    have hself : EisensteinCoordinateProduct(a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h)),a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g)),a · h + b · g + (c · f + d · e) + (c · g + d · h),a · g + b · h + (c · e + d · f) + (c · h + d · g),a · e + b · f + (c · h + d · g),a · f + b · e + (c · g + d · h),a · g + b · h + (c · e + d · f) + (c · h + d · g),a · h + b · g + (c · f + d · e) + (c · g + d · h),x,0,0,0)Definitions: EisensteinCoordinateProduct
  2. L21
    specialize eisenstein_conjugate_product_is_norm ((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))
  3. L22
    specialize eisenstein_conjugate_product_is_norm ((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))
  4. L23
    specialize eisenstein_conjugate_product_is_norm ((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))
  5. L24
    specialize eisenstein_conjugate_product_is_norm ((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))
  6. L25
    specialize eisenstein_conjugate_product_is_norm x
  7. L26
    apply eisenstein_conjugate_product_is_norm
  8. L27
    exact hnorm_witness
06Establish hproductL28–28

Establish this local claim before using it. It is not an additional assumption.

  1. L28
    have hproduct : EisensteinCoordinateProduct(a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h)),a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g)),a · h + b · g + (c · f + d · e) + (c · g + d · h),a · g + b · h + (c · e + d · f) + (c · h + d · g),a · e + b · f + (c · h + d · g),a · f + b · e + (c · g + d · h),a · g + b · h + (c · e + d · f) + (c · h + d · g),a · h + b · g + (c · f + d · e) + (c · g + d · h),N · M,0,0,0)Definitions: EisensteinCoordinateProduct
07Establish ee_chain_step_norm_0L29–38

Establish this local claim before using it. It is not an additional assumption.

  1. L29
    have ee_chain_step_norm_0 · expand full local formula (2,848 characters)have ee_chain_step_norm_0 : EisensteinCoordinateProduct(a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h)),a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g)),a · h + b · g + (c · f + d · e) + (c · g + d · h),a · g + b · h + (c · e + d · f) + (c · h + d · g),a · e + b · f + (c · h + d · g),a · f + b · e + (c · g + d · h),a · g + b · h + (c · e + d · f) + (c · h + d · g),a · h + b · g + (c · f + d · e) + (c · g + d · h),((a + d) · (e + h) + (b + c) · (f + g) + (d · g + c · h)) · (a · e + b · f + (c · h + d · g)) + ((a + d) · (f + g) + (b + c) · (e + h) + (d · h + c · g)) · (a · f + b · e + (c · g + d · h)) + (((a + d) · h + (b + c) · g + (d · (e + h) + c · (f + g)) + (d · g + c · h)) · (a · h + b · g + (c · f + d · e) + (c · g + d · h)) + ((a + d) · g + (b + c) · h + (d · (f + g) + c · (e + h)) + (d · h + c · g)) · (a · g + b · h + (c · e + d · f) + (c · h + d · g))),((a + d) · (e + h) + (b + c) · (f + g) + (d · g + c · h)) · (a · f + b · e + (c · g + d · h)) + ((a + d) · (f + g) + (b + c) · (e + h) + (d · h + c · g)) · (a · e + b · f + (c · h + d · g)) + (((a + d) · h + (b + c) · g + (d · (e + h) + c · (f + g)) + (d · g + c · h)) · (a · g + b · h + (c · e + d · f) + (c · h + d · g)) + ((a + d) · g + (b + c) · h + (d · (f + g) + c · (e + h)) + (d · h + c · g)) · (a · h + b · g + (c · f + d · e) + (c · g + d · h))),((a + d) · (e + h) + (b + c) · (f + g) + (d · g + c · h)) · (a · g + b · h + (c · e + d · f) + (c · h + d · g)) + ((a + d) · (f + g) + (b + c) · (e + h) + (d · h + c · g)) · (a · h + b · g + (c · f + d · e) + (c · g + d · h)) + (((a + d) · h + (b + c) · g + (d · (e + h) + c · (f + g)) + (d · g + c · h)) · (a · e + b · f + (c · h + d · g)) + ((a + d) · g + (b + c) · h + (d · (f + g) + c · (e + h)) + (d · h + c · g)) · (a · f + b · e + (c · g + d · h))) + (((a + d) · h + (b + c) · g + (d · (e + h) + c · (f + g)) + (d · g + c · h)) · (a · h + b · g + (c · f + d · e) + (c · g + d · h)) + ((a + d) · g + (b + c) · h + (d · (f + g) + c · (e + h)) + (d · h + c · g)) · (a · g + b · h + (c · e + d · f) + (c · h + d · g))),((a + d) · (e + h) + (b + c) · (f + g) + (d · g + c · h)) · (a · h + b · g + (c · f + d · e) + (c · g + d · h)) + ((a + d) · (f + g) + (b + c) · (e + h) + (d · h + c · g)) · (a · g + b · h + (c · e + d · f) + (c · h + d · g)) + (((a + d) · h + (b + c) · g + (d · (e + h) + c · (f + g)) + (d · g + c · h)) · (a · f + b · e + (c · g + d · h)) + ((a + d) · g + (b + c) · h + (d · (f + g) + c · (e + h)) + (d · h + c · g)) · (a · e + b · f + (c · h + d · g))) + (((a + d) · h + (b + c) · g + (d · (e + h) + c · (f + g)) + (d · g + c · h)) · (a · g + b · h + (c · e + d · f) + (c · h + d · g)) + ((a + d) · g + (b + c) · h + (d · (f + g) + c · (e + h)) + (d · h + c · g)) · (a · h + b · g + (c · f + d · e) + (c · g + d · h))))
    Definitions: EisensteinCoordinateProduct
  2. L30
    specialize eisenstein_product_integer_congruence ((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))
  3. L31
    specialize eisenstein_product_integer_congruence ((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))
  4. L32
    specialize eisenstein_product_integer_congruence ((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))
  5. L33
    specialize eisenstein_product_integer_congruence ((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))
  6. L34
    specialize eisenstein_product_integer_congruence ((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + (g))))))) + (((((d) * (g))) + (((c) * (h))))))
  7. L35
    specialize eisenstein_product_integer_congruence ((((((((a) + (d))) * (((f) + (g))))) + (((((b) + (c))) * (((e) + (h))))))) + (((((d) * (h))) + (((c) * (g))))))
  8. L36
    specialize eisenstein_product_integer_congruence ((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))
  9. L37
    specialize eisenstein_product_integer_congruence ((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))
  10. L38
    specialize eisenstein_product_integer_congruence ((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))
08Use earlier factsL39–48

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L39
    specialize eisenstein_product_integer_congruence ((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))
  2. L40
    specialize eisenstein_product_integer_congruence ((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))
  3. L41
    specialize eisenstein_product_integer_congruence ((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))
  4. L42
    specialize eisenstein_product_integer_congruence ((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))
  5. L43
    specialize eisenstein_product_integer_congruence ((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))
  6. L44
    specialize eisenstein_product_integer_congruence ((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))
  7. L45
    specialize eisenstein_product_integer_congruence ((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))
  8. L46
    apply eisenstein_product_integer_congruence
  9. L47
    specialize eisenstein_product_conjugate a
  10. L48
    specialize eisenstein_product_conjugate b
09Use earlier factsL49–58

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L49
    specialize eisenstein_product_conjugate c
  2. L50
    specialize eisenstein_product_conjugate d
  3. L51
    specialize eisenstein_product_conjugate e
  4. L52
    specialize eisenstein_product_conjugate f
  5. L53
    specialize eisenstein_product_conjugate g
  6. L54
    specialize eisenstein_product_conjugate h
  7. L55
    apply eisenstein_product_conjugate
  8. L56
    specialize gaussian_equal_reflexive ((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))
  9. L57
    specialize gaussian_equal_reflexive ((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))
  10. L58
    specialize gaussian_equal_reflexive ((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))
10Use earlier factsL59–60

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L59
    specialize gaussian_equal_reflexive ((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))
  2. L60
    apply gaussian_equal_reflexive
11Establish ee_chain_step_norm_1L61–70

Establish this local claim before using it. It is not an additional assumption.

  1. L61
    have ee_chain_step_norm_1 · expand full local formula (2,836 characters)have ee_chain_step_norm_1 : EisensteinCoordinateProduct((a + d) · (e + h) + (b + c) · (f + g) + (d · g + c · h),(a + d) · (f + g) + (b + c) · (e + h) + (d · h + c · g),(a + d) · h + (b + c) · g + (d · (e + h) + c · (f + g)) + (d · g + c · h),(a + d) · g + (b + c) · h + (d · (f + g) + c · (e + h)) + (d · h + c · g),a · e + b · f + (c · h + d · g),a · f + b · e + (c · g + d · h),a · g + b · h + (c · e + d · f) + (c · h + d · g),a · h + b · g + (c · f + d · e) + (c · g + d · h),((a + d) · a + (b + c) · b + (d · d + c · c)) · ((e + h) · e + (f + g) · f + (h · h + g · g)) + ((a + d) · b + (b + c) · a + (d · c + c · d)) · ((e + h) · f + (f + g) · e + (h · g + g · h)) + (((a + d) · c + (b + c) · d + (d · a + c · b) + (d · d + c · c)) · ((e + h) · h + (f + g) · g + (h · f + g · e) + (h · g + g · h)) + ((a + d) · d + (b + c) · c + (d · b + c · a) + (d · c + c · d)) · ((e + h) · g + (f + g) · h + (h · e + g · f) + (h · h + g · g))),((a + d) · a + (b + c) · b + (d · d + c · c)) · ((e + h) · f + (f + g) · e + (h · g + g · h)) + ((a + d) · b + (b + c) · a + (d · c + c · d)) · ((e + h) · e + (f + g) · f + (h · h + g · g)) + (((a + d) · c + (b + c) · d + (d · a + c · b) + (d · d + c · c)) · ((e + h) · g + (f + g) · h + (h · e + g · f) + (h · h + g · g)) + ((a + d) · d + (b + c) · c + (d · b + c · a) + (d · c + c · d)) · ((e + h) · h + (f + g) · g + (h · f + g · e) + (h · g + g · h))),((a + d) · a + (b + c) · b + (d · d + c · c)) · ((e + h) · g + (f + g) · h + (h · e + g · f) + (h · h + g · g)) + ((a + d) · b + (b + c) · a + (d · c + c · d)) · ((e + h) · h + (f + g) · g + (h · f + g · e) + (h · g + g · h)) + (((a + d) · c + (b + c) · d + (d · a + c · b) + (d · d + c · c)) · ((e + h) · e + (f + g) · f + (h · h + g · g)) + ((a + d) · d + (b + c) · c + (d · b + c · a) + (d · c + c · d)) · ((e + h) · f + (f + g) · e + (h · g + g · h))) + (((a + d) · c + (b + c) · d + (d · a + c · b) + (d · d + c · c)) · ((e + h) · h + (f + g) · g + (h · f + g · e) + (h · g + g · h)) + ((a + d) · d + (b + c) · c + (d · b + c · a) + (d · c + c · d)) · ((e + h) · g + (f + g) · h + (h · e + g · f) + (h · h + g · g))),((a + d) · a + (b + c) · b + (d · d + c · c)) · ((e + h) · h + (f + g) · g + (h · f + g · e) + (h · g + g · h)) + ((a + d) · b + (b + c) · a + (d · c + c · d)) · ((e + h) · g + (f + g) · h + (h · e + g · f) + (h · h + g · g)) + (((a + d) · c + (b + c) · d + (d · a + c · b) + (d · d + c · c)) · ((e + h) · f + (f + g) · e + (h · g + g · h)) + ((a + d) · d + (b + c) · c + (d · b + c · a) + (d · c + c · d)) · ((e + h) · e + (f + g) · f + (h · h + g · g))) + (((a + d) · c + (b + c) · d + (d · a + c · b) + (d · d + c · c)) · ((e + h) · g + (f + g) · h + (h · e + g · f) + (h · h + g · g)) + ((a + d) · d + (b + c) · c + (d · b + c · a) + (d · c + c · d)) · ((e + h) · h + (f + g) · g + (h · f + g · e) + (h · g + g · h))))
    Definitions: EisensteinCoordinateProduct
  2. L62
    specialize eisenstein_product_shuffle ((a) + (d))
  3. L63
    specialize eisenstein_product_shuffle ((b) + (c))
  4. L64
    specialize eisenstein_product_shuffle d
  5. L65
    specialize eisenstein_product_shuffle c
  6. L66
    specialize eisenstein_product_shuffle ((e) + (h))
  7. L67
    specialize eisenstein_product_shuffle ((f) + (g))
  8. L68
    specialize eisenstein_product_shuffle h
  9. L69
    specialize eisenstein_product_shuffle g
  10. L70
    specialize eisenstein_product_shuffle a
12Use earlier factsL71–78

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L71
    specialize eisenstein_product_shuffle b
  2. L72
    specialize eisenstein_product_shuffle c
  3. L73
    specialize eisenstein_product_shuffle d
  4. L74
    specialize eisenstein_product_shuffle e
  5. L75
    specialize eisenstein_product_shuffle f
  6. L76
    specialize eisenstein_product_shuffle g
  7. L77
    specialize eisenstein_product_shuffle h
  8. L78
    apply eisenstein_product_shuffle
13Establish ee_chain_path_norm_1L79–88

Establish this local claim before using it. It is not an additional assumption.

  1. L79
    have ee_chain_path_norm_1 · expand full local formula (2,848 characters)have ee_chain_path_norm_1 : EisensteinCoordinateProduct(a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h)),a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g)),a · h + b · g + (c · f + d · e) + (c · g + d · h),a · g + b · h + (c · e + d · f) + (c · h + d · g),a · e + b · f + (c · h + d · g),a · f + b · e + (c · g + d · h),a · g + b · h + (c · e + d · f) + (c · h + d · g),a · h + b · g + (c · f + d · e) + (c · g + d · h),((a + d) · a + (b + c) · b + (d · d + c · c)) · ((e + h) · e + (f + g) · f + (h · h + g · g)) + ((a + d) · b + (b + c) · a + (d · c + c · d)) · ((e + h) · f + (f + g) · e + (h · g + g · h)) + (((a + d) · c + (b + c) · d + (d · a + c · b) + (d · d + c · c)) · ((e + h) · h + (f + g) · g + (h · f + g · e) + (h · g + g · h)) + ((a + d) · d + (b + c) · c + (d · b + c · a) + (d · c + c · d)) · ((e + h) · g + (f + g) · h + (h · e + g · f) + (h · h + g · g))),((a + d) · a + (b + c) · b + (d · d + c · c)) · ((e + h) · f + (f + g) · e + (h · g + g · h)) + ((a + d) · b + (b + c) · a + (d · c + c · d)) · ((e + h) · e + (f + g) · f + (h · h + g · g)) + (((a + d) · c + (b + c) · d + (d · a + c · b) + (d · d + c · c)) · ((e + h) · g + (f + g) · h + (h · e + g · f) + (h · h + g · g)) + ((a + d) · d + (b + c) · c + (d · b + c · a) + (d · c + c · d)) · ((e + h) · h + (f + g) · g + (h · f + g · e) + (h · g + g · h))),((a + d) · a + (b + c) · b + (d · d + c · c)) · ((e + h) · g + (f + g) · h + (h · e + g · f) + (h · h + g · g)) + ((a + d) · b + (b + c) · a + (d · c + c · d)) · ((e + h) · h + (f + g) · g + (h · f + g · e) + (h · g + g · h)) + (((a + d) · c + (b + c) · d + (d · a + c · b) + (d · d + c · c)) · ((e + h) · e + (f + g) · f + (h · h + g · g)) + ((a + d) · d + (b + c) · c + (d · b + c · a) + (d · c + c · d)) · ((e + h) · f + (f + g) · e + (h · g + g · h))) + (((a + d) · c + (b + c) · d + (d · a + c · b) + (d · d + c · c)) · ((e + h) · h + (f + g) · g + (h · f + g · e) + (h · g + g · h)) + ((a + d) · d + (b + c) · c + (d · b + c · a) + (d · c + c · d)) · ((e + h) · g + (f + g) · h + (h · e + g · f) + (h · h + g · g))),((a + d) · a + (b + c) · b + (d · d + c · c)) · ((e + h) · h + (f + g) · g + (h · f + g · e) + (h · g + g · h)) + ((a + d) · b + (b + c) · a + (d · c + c · d)) · ((e + h) · g + (f + g) · h + (h · e + g · f) + (h · h + g · g)) + (((a + d) · c + (b + c) · d + (d · a + c · b) + (d · d + c · c)) · ((e + h) · f + (f + g) · e + (h · g + g · h)) + ((a + d) · d + (b + c) · c + (d · b + c · a) + (d · c + c · d)) · ((e + h) · e + (f + g) · f + (h · h + g · g))) + (((a + d) · c + (b + c) · d + (d · a + c · b) + (d · d + c · c)) · ((e + h) · g + (f + g) · h + (h · e + g · f) + (h · h + g · g)) + ((a + d) · d + (b + c) · c + (d · b + c · a) + (d · c + c · d)) · ((e + h) · h + (f + g) · g + (h · f + g · e) + (h · g + g · h))))
    Definitions: EisensteinCoordinateProduct
  2. L80
    specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g) · expand full local formula (1,068 characters)specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  3. L81
    specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g) · expand full local formula (1,068 characters)specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  4. L82
    specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * ( · expand full local formula (1,548 characters)specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  5. L83
    specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * ( · expand full local formula (1,548 characters)specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  6. L84
    specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + (g) · expand full local formula (988 characters)specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + (g))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) + (d))) * (((f) + (g))))) + (((((b) + (c))) * (((e) + (h))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  7. L85
    specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + (g) · expand full local formula (988 characters)specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + (g))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) + (d))) * (((f) + (g))))) + (((((b) + (c))) * (((e) + (h))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  8. L86
    specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + ( · expand full local formula (1,548 characters)specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + (g))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) + (d))) * (((f) + (g))))) + (((((b) + (c))) * (((e) + (h))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  9. L87
    specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + ( · expand full local formula (1,548 characters)specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + (g))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) + (d))) * (((f) + (g))))) + (((((b) + (c))) * (((e) + (h))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  10. L88
    specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * ( · expand full local formula (988 characters)specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))))))
14Use earlier factsL89–94

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L89
    specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * ( · expand full local formula (988 characters)specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))))))
  2. L90
    specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * · expand full local formula (1,548 characters)specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))))))
  3. L91
    specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * · expand full local formula (1,548 characters)specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))))))
  4. L92
    apply gaussian_equal_transitive
  5. L93
    exact ee_chain_step_norm_0
  6. L94
    exact ee_chain_step_norm_1
15Establish ee_chain_step_norm_2L95–104

Establish this local claim before using it. It is not an additional assumption.

  1. L95
    have ee_chain_step_norm_2 · expand full local formula (644 characters)have ee_chain_step_norm_2 : EisensteinCoordinateProduct((a + d) · a + (b + c) · b + (d · d + c · c),(a + d) · b + (b + c) · a + (d · c + c · d),(a + d) · c + (b + c) · d + (d · a + c · b) + (d · d + c · c),(a + d) · d + (b + c) · c + (d · b + c · a) + (d · c + c · d),(e + h) · e + (f + g) · f + (h · h + g · g),(e + h) · f + (f + g) · e + (h · g + g · h),(e + h) · g + (f + g) · h + (h · e + g · f) + (h · h + g · g),(e + h) · h + (f + g) · g + (h · f + g · e) + (h · g + g · h),N · M + 0 · 0 + (0 · 0 + 0 · 0),N · 0 + 0 · M + (0 · 0 + 0 · 0),N · 0 + 0 · 0 + (0 · M + 0 · 0) + (0 · 0 + 0 · 0),N · 0 + 0 · 0 + (0 · 0 + 0 · M) + (0 · 0 + 0 · 0))
    Definitions: EisensteinCoordinateProduct
  2. L96
    specialize eisenstein_product_integer_congruence ((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))
  3. L97
    specialize eisenstein_product_integer_congruence ((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))
  4. L98
    specialize eisenstein_product_integer_congruence ((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))
  5. L99
    specialize eisenstein_product_integer_congruence ((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))
  6. L100
    specialize eisenstein_product_integer_congruence N
  7. L101
    specialize eisenstein_product_integer_congruence 0
  8. L102
    specialize eisenstein_product_integer_congruence 0
  9. L103
    specialize eisenstein_product_integer_congruence 0
  10. L104
    specialize eisenstein_product_integer_congruence ((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))
16Use earlier factsL105–114

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L105
    specialize eisenstein_product_integer_congruence ((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))
  2. L106
    specialize eisenstein_product_integer_congruence ((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))
  3. L107
    specialize eisenstein_product_integer_congruence ((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))
  4. L108
    specialize eisenstein_product_integer_congruence M
  5. L109
    specialize eisenstein_product_integer_congruence 0
  6. L110
    specialize eisenstein_product_integer_congruence 0
  7. L111
    specialize eisenstein_product_integer_congruence 0
  8. L112
    apply eisenstein_product_integer_congruence
  9. L113
    specialize eisenstein_conjugate_product_is_norm a
  10. L114
    specialize eisenstein_conjugate_product_is_norm b
17Use earlier factsL115–124

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L115
    specialize eisenstein_conjugate_product_is_norm c
  2. L116
    specialize eisenstein_conjugate_product_is_norm d
  3. L117
    specialize eisenstein_conjugate_product_is_norm N
  4. L118
    apply eisenstein_conjugate_product_is_norm
  5. L119
    exact hfirst
  6. L120
    specialize eisenstein_conjugate_product_is_norm e
  7. L121
    specialize eisenstein_conjugate_product_is_norm f
  8. L122
    specialize eisenstein_conjugate_product_is_norm g
  9. L123
    specialize eisenstein_conjugate_product_is_norm h
  10. L124
    specialize eisenstein_conjugate_product_is_norm M
18Use earlier factsL125–126

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L125
    apply eisenstein_conjugate_product_is_norm
  2. L126
    exact hsecond
19Establish ee_chain_path_norm_2L127–136

Establish this local claim before using it. It is not an additional assumption.

  1. L127
    have ee_chain_path_norm_2 · expand full local formula (656 characters)have ee_chain_path_norm_2 : EisensteinCoordinateProduct(a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h)),a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g)),a · h + b · g + (c · f + d · e) + (c · g + d · h),a · g + b · h + (c · e + d · f) + (c · h + d · g),a · e + b · f + (c · h + d · g),a · f + b · e + (c · g + d · h),a · g + b · h + (c · e + d · f) + (c · h + d · g),a · h + b · g + (c · f + d · e) + (c · g + d · h),N · M + 0 · 0 + (0 · 0 + 0 · 0),N · 0 + 0 · M + (0 · 0 + 0 · 0),N · 0 + 0 · 0 + (0 · M + 0 · 0) + (0 · 0 + 0 · 0),N · 0 + 0 · 0 + (0 · 0 + 0 · M) + (0 · 0 + 0 · 0))
    Definitions: EisensteinCoordinateProduct
  2. L128
    specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g) · expand full local formula (1,068 characters)specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  3. L129
    specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g) · expand full local formula (1,068 characters)specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  4. L130
    specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * ( · expand full local formula (1,548 characters)specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  5. L131
    specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * ( · expand full local formula (1,548 characters)specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  6. L132
    specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * ( · expand full local formula (988 characters)specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))))))
  7. L133
    specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * ( · expand full local formula (988 characters)specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))))))
  8. L134
    specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * · expand full local formula (1,548 characters)specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))))))
  9. L135
    specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * · expand full local formula (1,548 characters)specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))))))
  10. L136
    specialize gaussian_equal_transitive ((((((N) * (M))) + (((0) * (0))))) + (((((0) * (0))) + (((0) * (0))))))
20Use earlier factsL137–142

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L137
    specialize gaussian_equal_transitive ((((((N) * (0))) + (((0) * (M))))) + (((((0) * (0))) + (((0) * (0))))))
  2. L138
    specialize gaussian_equal_transitive ((((((((N) * (0))) + (((0) * (0))))) + (((((0) * (M))) + (((0) * (0))))))) + (((((0) * (0))) + (((0) * (0))))))
  3. L139
    specialize gaussian_equal_transitive ((((((((N) * (0))) + (((0) * (0))))) + (((((0) * (0))) + (((0) * (M))))))) + (((((0) * (0))) + (((0) * (0))))))
  4. L140
    apply gaussian_equal_transitive
  5. L141
    exact ee_chain_path_norm_1
  6. L142
    exact ee_chain_step_norm_2
21Establish ee_chain_step_norm_3L143–143

Establish this local claim before using it. It is not an additional assumption.

  1. L143
    have ee_chain_step_norm_3 : ((((((((((N) * (M))) + (((0) * (0))))) + (((((0) * (0))) + (((0) * (0))))))) + (0)) = ((N * M) + (((((((N) * (0))) + (((0) * (M))))) + (((((0) * (0))) + (((0) * (0))))))))) /\ (((((((((((N) * (0))) + (((0) * (0))))) + (((((0) * (M))) + (((0) * (0))))))) + (((((0) * (0))) + (((0) * (0))))))) + (0)) = ((0) + (((((((((N) * (0))) + (((0) * (0))))) + (((((0) * (0))) + (((0) * (M))))))) + (((((0) * (0))) + (((0) * (0))))))))))
22Separate the logical casesL144–144

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L144
    split
23Calculate and transport equalitiesL145–146

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L145
    simp [mul_zero_left, zero_add]
  2. L146
    simp [mul_zero_left, zero_add]
24Establish ee_chain_path_norm_3L147–156

Establish this local claim before using it. It is not an additional assumption.

  1. L147
    have ee_chain_path_norm_3 : EisensteinCoordinateProduct(a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h)),a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g)),a · h + b · g + (c · f + d · e) + (c · g + d · h),a · g + b · h + (c · e + d · f) + (c · h + d · g),a · e + b · f + (c · h + d · g),a · f + b · e + (c · g + d · h),a · g + b · h + (c · e + d · f) + (c · h + d · g),a · h + b · g + (c · f + d · e) + (c · g + d · h),N · M,0,0,0)Definitions: EisensteinCoordinateProduct
  2. L148
    specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g) · expand full local formula (1,068 characters)specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  3. L149
    specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g) · expand full local formula (1,068 characters)specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  4. L150
    specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * ( · expand full local formula (1,548 characters)specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  5. L151
    specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * ( · expand full local formula (1,548 characters)specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  6. L152
    specialize gaussian_equal_transitive ((((((N) * (M))) + (((0) * (0))))) + (((((0) * (0))) + (((0) * (0))))))
  7. L153
    specialize gaussian_equal_transitive ((((((N) * (0))) + (((0) * (M))))) + (((((0) * (0))) + (((0) * (0))))))
  8. L154
    specialize gaussian_equal_transitive ((((((((N) * (0))) + (((0) * (0))))) + (((((0) * (M))) + (((0) * (0))))))) + (((((0) * (0))) + (((0) * (0))))))
  9. L155
    specialize gaussian_equal_transitive ((((((((N) * (0))) + (((0) * (0))))) + (((((0) * (0))) + (((0) * (M))))))) + (((((0) * (0))) + (((0) * (0))))))
  10. L156
    specialize gaussian_equal_transitive N * M
25Use earlier factsL157–163

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L157
    specialize gaussian_equal_transitive 0
  2. L158
    specialize gaussian_equal_transitive 0
  3. L159
    specialize gaussian_equal_transitive 0
  4. L160
    apply gaussian_equal_transitive
  5. L161
    exact ee_chain_path_norm_2
  6. L162
    exact ee_chain_step_norm_3
  7. L163
    exact ee_chain_path_norm_3
26Establish hscalarL164–173

Establish this local claim before using it. It is not an additional assumption.

  1. L164
    have hscalar : ((((x) + (0)) = ((N * M) + (0))) /\ (((0) + (0)) = ((0) + (0))))
  2. L165
    specialize gaussian_equal_transitive x
  3. L166
    specialize gaussian_equal_transitive 0
  4. L167
    specialize gaussian_equal_transitive 0
  5. L168
    specialize gaussian_equal_transitive 0
  6. L169
    specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g) · expand full local formula (1,068 characters)specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  7. L170
    specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g) · expand full local formula (1,068 characters)specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  8. L171
    specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * ( · expand full local formula (1,548 characters)specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  9. L172
    specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * ( · expand full local formula (1,548 characters)specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  10. L173
    specialize gaussian_equal_transitive N * M
27Use earlier factsL174–183

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L174
    specialize gaussian_equal_transitive 0
  2. L175
    specialize gaussian_equal_transitive 0
  3. L176
    specialize gaussian_equal_transitive 0
  4. L177
    apply gaussian_equal_transitive
  5. L178
    specialize gaussian_equal_symmetric ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g)) · expand full local formula (1,067 characters)specialize gaussian_equal_symmetric ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  6. L179
    specialize gaussian_equal_symmetric ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g)) · expand full local formula (1,067 characters)specialize gaussian_equal_symmetric ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  7. L180
    specialize gaussian_equal_symmetric ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g · expand full local formula (1,547 characters)specialize gaussian_equal_symmetric ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  8. L181
    specialize gaussian_equal_symmetric ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g · expand full local formula (1,547 characters)specialize gaussian_equal_symmetric ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  9. L182
    specialize gaussian_equal_symmetric x
  10. L183
    specialize gaussian_equal_symmetric 0
28Use earlier factsL184–188

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L184
    specialize gaussian_equal_symmetric 0
  2. L185
    specialize gaussian_equal_symmetric 0
  3. L186
    apply gaussian_equal_symmetric
  4. L187
    exact hself
  5. L188
    exact hproduct
29Separate the logical casesL189–189

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L189
    cases hscalar
30Establish hvalueL190–198

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply PA3.

  1. L190
    have hvalue : x = N * M
  2. L191
    trans x + 0
  3. L192
    symm
  4. L193
    apply PA3
  5. L194
    trans (N * M) + 0
  6. L195
    exact hscalar_left
  7. L196
    apply PA3
  8. L197
    rewrite <- hvalue
  9. L198
    exact hnorm_witness

Library-wide reading audit

Original exact command ledger · 198 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro e
  6. 0006intro f
  7. 0007intro g
  8. 0008intro h
  9. 0009intro N
  10. 0010intro M
  11. 0011intro hfirst
  12. 0012intro hsecond
  13. 0013have hnorm : exists n. (((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g)))))))))))) = ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (n)))
  14. 0014specialize eisenstein_coordinate_norm_exists ((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))
  15. 0015specialize eisenstein_coordinate_norm_exists ((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))
  16. 0016specialize eisenstein_coordinate_norm_exists ((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))
  17. 0017specialize eisenstein_coordinate_norm_exists ((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))
  18. 0018apply eisenstein_coordinate_norm_exists
  19. 0019cases hnorm
  20. 0020have hself : ((((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (0)) = ((x) + (((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))))) /\ (((((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (0)) = ((0) + (((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))))))
  21. 0021specialize eisenstein_conjugate_product_is_norm ((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))
  22. 0022specialize eisenstein_conjugate_product_is_norm ((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))
  23. 0023specialize eisenstein_conjugate_product_is_norm ((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))
  24. 0024specialize eisenstein_conjugate_product_is_norm ((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))
  25. 0025specialize eisenstein_conjugate_product_is_norm x
  26. 0026apply eisenstein_conjugate_product_is_norm
  27. 0027exact hnorm_witness
  28. 0028have hproduct : ((((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (0)) = ((N * M) + (((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))))) /\ (((((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (0)) = ((0) + (((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))))))
  29. 0029have ee_chain_step_norm_0 : ((((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + (g))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) + (d))) * (((f) + (g))))) + (((((b) + (c))) * (((e) + (h))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h)))))))))))))) = ((((((((((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + (g))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) + (d))) * (((f) + (g))))) + (((((b) + (c))) * (((e) + (h))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))))) /\ (((((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + (g))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) + (d))) * (((f) + (g))))) + (((((b) + (c))) * (((e) + (h))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h)))))))))))))) = ((((((((((((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + (g))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) + (d))) * (((f) + (g))))) + (((((b) + (c))) * (((e) + (h))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))))))
  30. 0030specialize eisenstein_product_integer_congruence ((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))
  31. 0031specialize eisenstein_product_integer_congruence ((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))
  32. 0032specialize eisenstein_product_integer_congruence ((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))
  33. 0033specialize eisenstein_product_integer_congruence ((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))
  34. 0034specialize eisenstein_product_integer_congruence ((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + (g))))))) + (((((d) * (g))) + (((c) * (h))))))
  35. 0035specialize eisenstein_product_integer_congruence ((((((((a) + (d))) * (((f) + (g))))) + (((((b) + (c))) * (((e) + (h))))))) + (((((d) * (h))) + (((c) * (g))))))
  36. 0036specialize eisenstein_product_integer_congruence ((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))
  37. 0037specialize eisenstein_product_integer_congruence ((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))
  38. 0038specialize eisenstein_product_integer_congruence ((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))
  39. 0039specialize eisenstein_product_integer_congruence ((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))
  40. 0040specialize eisenstein_product_integer_congruence ((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))
  41. 0041specialize eisenstein_product_integer_congruence ((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))
  42. 0042specialize eisenstein_product_integer_congruence ((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))
  43. 0043specialize eisenstein_product_integer_congruence ((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))
  44. 0044specialize eisenstein_product_integer_congruence ((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))
  45. 0045specialize eisenstein_product_integer_congruence ((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))
  46. 0046apply eisenstein_product_integer_congruence
  47. 0047specialize eisenstein_product_conjugate a
  48. 0048specialize eisenstein_product_conjugate b
  49. 0049specialize eisenstein_product_conjugate c
  50. 0050specialize eisenstein_product_conjugate d
  51. 0051specialize eisenstein_product_conjugate e
  52. 0052specialize eisenstein_product_conjugate f
  53. 0053specialize eisenstein_product_conjugate g
  54. 0054specialize eisenstein_product_conjugate h
  55. 0055apply eisenstein_product_conjugate
  56. 0056specialize gaussian_equal_reflexive ((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))
  57. 0057specialize gaussian_equal_reflexive ((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))
  58. 0058specialize gaussian_equal_reflexive ((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))
  59. 0059specialize gaussian_equal_reflexive ((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))
  60. 0060apply gaussian_equal_reflexive
  61. 0061have ee_chain_step_norm_1 : ((((((((((((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + (g))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) + (d))) * (((f) + (g))))) + (((((b) + (c))) * (((e) + (h))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h)))))))))))))) = ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))))))) + (((((((((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + (g))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) + (d))) * (((f) + (g))))) + (((((b) + (c))) * (((e) + (h))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))))) /\ (((((((((((((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + (g))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) + (d))) * (((f) + (g))))) + (((((b) + (c))) * (((e) + (h))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h)))))))))))))) = ((((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))))))) + (((((((((((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + (g))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) + (d))) * (((f) + (g))))) + (((((b) + (c))) * (((e) + (h))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))))))
  62. 0062specialize eisenstein_product_shuffle ((a) + (d))
  63. 0063specialize eisenstein_product_shuffle ((b) + (c))
  64. 0064specialize eisenstein_product_shuffle d
  65. 0065specialize eisenstein_product_shuffle c
  66. 0066specialize eisenstein_product_shuffle ((e) + (h))
  67. 0067specialize eisenstein_product_shuffle ((f) + (g))
  68. 0068specialize eisenstein_product_shuffle h
  69. 0069specialize eisenstein_product_shuffle g
  70. 0070specialize eisenstein_product_shuffle a
  71. 0071specialize eisenstein_product_shuffle b
  72. 0072specialize eisenstein_product_shuffle c
  73. 0073specialize eisenstein_product_shuffle d
  74. 0074specialize eisenstein_product_shuffle e
  75. 0075specialize eisenstein_product_shuffle f
  76. 0076specialize eisenstein_product_shuffle g
  77. 0077specialize eisenstein_product_shuffle h
  78. 0078apply eisenstein_product_shuffle
  79. 0079have ee_chain_path_norm_1 : ((((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h)))))))))))))) = ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))))))) + (((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))))) /\ (((((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h)))))))))))))) = ((((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))))))) + (((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))))))
  80. 0080specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  81. 0081specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  82. 0082specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  83. 0083specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  84. 0084specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + (g))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) + (d))) * (((f) + (g))))) + (((((b) + (c))) * (((e) + (h))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  85. 0085specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + (g))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) + (d))) * (((f) + (g))))) + (((((b) + (c))) * (((e) + (h))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  86. 0086specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + (g))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) + (d))) * (((f) + (g))))) + (((((b) + (c))) * (((e) + (h))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  87. 0087specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (((e) + (h))))) + (((((b) + (c))) * (((f) + (g))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) + (d))) * (((f) + (g))))) + (((((b) + (c))) * (((e) + (h))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((((a) + (d))) * (h))) + (((((b) + (c))) * (g))))) + (((((d) * (((e) + (h))))) + (((c) * (((f) + (g))))))))) + (((((d) * (g))) + (((c) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((((a) + (d))) * (g))) + (((((b) + (c))) * (h))))) + (((((d) * (((f) + (g))))) + (((c) * (((e) + (h))))))))) + (((((d) * (h))) + (((c) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  88. 0088specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))))))
  89. 0089specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))))))
  90. 0090specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))))))
  91. 0091specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))))))
  92. 0092apply gaussian_equal_transitive
  93. 0093exact ee_chain_step_norm_0
  94. 0094exact ee_chain_step_norm_1
  95. 0095have ee_chain_step_norm_2 : ((((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))))))) + (((((((N) * (0))) + (((0) * (M))))) + (((((0) * (0))) + (((0) * (0)))))))) = ((((((((N) * (M))) + (((0) * (0))))) + (((((0) * (0))) + (((0) * (0))))))) + (((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))))))))) /\ (((((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))))))) + (((((((((N) * (0))) + (((0) * (0))))) + (((((0) * (0))) + (((0) * (M))))))) + (((((0) * (0))) + (((0) * (0)))))))) = ((((((((((N) * (0))) + (((0) * (0))))) + (((((0) * (M))) + (((0) * (0))))))) + (((((0) * (0))) + (((0) * (0))))))) + (((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))))))))))
  96. 0096specialize eisenstein_product_integer_congruence ((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))
  97. 0097specialize eisenstein_product_integer_congruence ((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))
  98. 0098specialize eisenstein_product_integer_congruence ((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))
  99. 0099specialize eisenstein_product_integer_congruence ((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))
  100. 0100specialize eisenstein_product_integer_congruence N
  101. 0101specialize eisenstein_product_integer_congruence 0
  102. 0102specialize eisenstein_product_integer_congruence 0
  103. 0103specialize eisenstein_product_integer_congruence 0
  104. 0104specialize eisenstein_product_integer_congruence ((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))
  105. 0105specialize eisenstein_product_integer_congruence ((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))
  106. 0106specialize eisenstein_product_integer_congruence ((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))
  107. 0107specialize eisenstein_product_integer_congruence ((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))
  108. 0108specialize eisenstein_product_integer_congruence M
  109. 0109specialize eisenstein_product_integer_congruence 0
  110. 0110specialize eisenstein_product_integer_congruence 0
  111. 0111specialize eisenstein_product_integer_congruence 0
  112. 0112apply eisenstein_product_integer_congruence
  113. 0113specialize eisenstein_conjugate_product_is_norm a
  114. 0114specialize eisenstein_conjugate_product_is_norm b
  115. 0115specialize eisenstein_conjugate_product_is_norm c
  116. 0116specialize eisenstein_conjugate_product_is_norm d
  117. 0117specialize eisenstein_conjugate_product_is_norm N
  118. 0118apply eisenstein_conjugate_product_is_norm
  119. 0119exact hfirst
  120. 0120specialize eisenstein_conjugate_product_is_norm e
  121. 0121specialize eisenstein_conjugate_product_is_norm f
  122. 0122specialize eisenstein_conjugate_product_is_norm g
  123. 0123specialize eisenstein_conjugate_product_is_norm h
  124. 0124specialize eisenstein_conjugate_product_is_norm M
  125. 0125apply eisenstein_conjugate_product_is_norm
  126. 0126exact hsecond
  127. 0127have ee_chain_path_norm_2 : ((((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((N) * (0))) + (((0) * (M))))) + (((((0) * (0))) + (((0) * (0)))))))) = ((((((((N) * (M))) + (((0) * (0))))) + (((((0) * (0))) + (((0) * (0))))))) + (((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))))) /\ (((((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((N) * (0))) + (((0) * (0))))) + (((((0) * (0))) + (((0) * (M))))))) + (((((0) * (0))) + (((0) * (0)))))))) = ((((((((((N) * (0))) + (((0) * (0))))) + (((((0) * (M))) + (((0) * (0))))))) + (((((0) * (0))) + (((0) * (0))))))) + (((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))))))
  128. 0128specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  129. 0129specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  130. 0130specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  131. 0131specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  132. 0132specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))))))
  133. 0133specialize gaussian_equal_transitive ((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))))))
  134. 0134specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))))))
  135. 0135specialize gaussian_equal_transitive ((((((((((((((((a) + (d))) * (a))) + (((((b) + (c))) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((a) + (d))) * (b))) + (((((b) + (c))) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((e) + (h))) * (f))) + (((((f) + (g))) * (e))))) + (((((h) * (g))) + (((g) * (h))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((e) + (h))) * (e))) + (((((f) + (g))) * (f))))) + (((((h) * (h))) + (((g) * (g))))))))))))) + (((((((((((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) + (((((d) * (d))) + (((c) * (c))))))) * (((((((((((e) + (h))) * (g))) + (((((f) + (g))) * (h))))) + (((((h) * (e))) + (((g) * (f))))))) + (((((h) * (h))) + (((g) * (g))))))))) + (((((((((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) + (((((d) * (c))) + (((c) * (d))))))) * (((((((((((e) + (h))) * (h))) + (((((f) + (g))) * (g))))) + (((((h) * (f))) + (((g) * (e))))))) + (((((h) * (g))) + (((g) * (h))))))))))))
  136. 0136specialize gaussian_equal_transitive ((((((N) * (M))) + (((0) * (0))))) + (((((0) * (0))) + (((0) * (0))))))
  137. 0137specialize gaussian_equal_transitive ((((((N) * (0))) + (((0) * (M))))) + (((((0) * (0))) + (((0) * (0))))))
  138. 0138specialize gaussian_equal_transitive ((((((((N) * (0))) + (((0) * (0))))) + (((((0) * (M))) + (((0) * (0))))))) + (((((0) * (0))) + (((0) * (0))))))
  139. 0139specialize gaussian_equal_transitive ((((((((N) * (0))) + (((0) * (0))))) + (((((0) * (0))) + (((0) * (M))))))) + (((((0) * (0))) + (((0) * (0))))))
  140. 0140apply gaussian_equal_transitive
  141. 0141exact ee_chain_path_norm_1
  142. 0142exact ee_chain_step_norm_2
  143. 0143have ee_chain_step_norm_3 : ((((((((((N) * (M))) + (((0) * (0))))) + (((((0) * (0))) + (((0) * (0))))))) + (0)) = ((N * M) + (((((((N) * (0))) + (((0) * (M))))) + (((((0) * (0))) + (((0) * (0))))))))) /\ (((((((((((N) * (0))) + (((0) * (0))))) + (((((0) * (M))) + (((0) * (0))))))) + (((((0) * (0))) + (((0) * (0))))))) + (0)) = ((0) + (((((((((N) * (0))) + (((0) * (0))))) + (((((0) * (0))) + (((0) * (M))))))) + (((((0) * (0))) + (((0) * (0))))))))))
  144. 0144split
  145. 0145simp [mul_zero_left, zero_add]
  146. 0146simp [mul_zero_left, zero_add]
  147. 0147have ee_chain_path_norm_3 : ((((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (0)) = ((N * M) + (((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))))) /\ (((((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (0)) = ((0) + (((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))))))
  148. 0148specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  149. 0149specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  150. 0150specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  151. 0151specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  152. 0152specialize gaussian_equal_transitive ((((((N) * (M))) + (((0) * (0))))) + (((((0) * (0))) + (((0) * (0))))))
  153. 0153specialize gaussian_equal_transitive ((((((N) * (0))) + (((0) * (M))))) + (((((0) * (0))) + (((0) * (0))))))
  154. 0154specialize gaussian_equal_transitive ((((((((N) * (0))) + (((0) * (0))))) + (((((0) * (M))) + (((0) * (0))))))) + (((((0) * (0))) + (((0) * (0))))))
  155. 0155specialize gaussian_equal_transitive ((((((((N) * (0))) + (((0) * (0))))) + (((((0) * (0))) + (((0) * (M))))))) + (((((0) * (0))) + (((0) * (0))))))
  156. 0156specialize gaussian_equal_transitive N * M
  157. 0157specialize gaussian_equal_transitive 0
  158. 0158specialize gaussian_equal_transitive 0
  159. 0159specialize gaussian_equal_transitive 0
  160. 0160apply gaussian_equal_transitive
  161. 0161exact ee_chain_path_norm_2
  162. 0162exact ee_chain_step_norm_3
  163. 0163exact ee_chain_path_norm_3
  164. 0164have hscalar : ((((x) + (0)) = ((N * M) + (0))) /\ (((0) + (0)) = ((0) + (0))))
  165. 0165specialize gaussian_equal_transitive x
  166. 0166specialize gaussian_equal_transitive 0
  167. 0167specialize gaussian_equal_transitive 0
  168. 0168specialize gaussian_equal_transitive 0
  169. 0169specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  170. 0170specialize gaussian_equal_transitive ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  171. 0171specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  172. 0172specialize gaussian_equal_transitive ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  173. 0173specialize gaussian_equal_transitive N * M
  174. 0174specialize gaussian_equal_transitive 0
  175. 0175specialize gaussian_equal_transitive 0
  176. 0176specialize gaussian_equal_transitive 0
  177. 0177apply gaussian_equal_transitive
  178. 0178specialize gaussian_equal_symmetric ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  179. 0179specialize gaussian_equal_symmetric ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  180. 0180specialize gaussian_equal_symmetric ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  181. 0181specialize gaussian_equal_symmetric ((((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))) + (((((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  182. 0182specialize gaussian_equal_symmetric x
  183. 0183specialize gaussian_equal_symmetric 0
  184. 0184specialize gaussian_equal_symmetric 0
  185. 0185specialize gaussian_equal_symmetric 0
  186. 0186apply gaussian_equal_symmetric
  187. 0187exact hself
  188. 0188exact hproduct
  189. 0189cases hscalar
  190. 0190have hvalue : x = N * M
  191. 0191trans x + 0
  192. 0192symm
  193. 0193apply PA3
  194. 0194trans (N * M) + 0
  195. 0195exact hscalar_left
  196. 0196apply PA3
  197. 0197rewrite <- hvalue
  198. 0198exact hnorm_witness