GI0032

gaussian_adjoint_product_is_norm_scale

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

The actual conjugate times a Gaussian product equals the genuine norm-scaled second factor.

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. (exists ge_real_square_adjoint_norm ge_imaginary_square_adjoint_norm. ((((((a) * (a))) + (((b) * (b)))) = ((ge_real_square_adjoint_norm) + (((((a) * (b))) + (((b) * (a))))))) /\ ((((((c) * (c))) + (((d) * (d)))) = ((ge_imaginary_square_adjoint_norm) + (((((c) * (d))) + (((d) * (c))))))) /\ ((N) = ge_real_square_adjoint_norm + ge_imaginary_square_adjoint_norm)))) -> (((((((((((a) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((b) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((d) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))) + (((c) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))))))) + (((N) * (f)))) = ((((N) * (e))) + (((((((a) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((b) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((d) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))) + (((c) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))))))))) /\ (((((((((a) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))) + (((b) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))))) + (((((d) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((N) * (h)))) = ((((N) * (g))) + (((((((a) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))) + (((b) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))))) + (((((d) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g)))))))))))))))))

Constructive proof overview

Generated structural guide

The actual conjugate times a Gaussian product equals the genuine norm-scaled second factor.

The unchanged tactic script uses 7 declared prerequisites and contains 97 exact native proof lines.

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

Proof neighborhood

Direct dependencies

GI002C gaussian_equal_transitive GI002B gaussian_equal_symmetric GI0028 gaussian_product_associate GI002D gaussian_product_integer_congruence GI0030 gaussian_conjugate_product_is_norm GI002A gaussian_equal_reflexive GI0031 gaussian_natural_scalar_product

Direct dependents

GI0033 gaussian_residual_conjugate_identity

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

97 script commands · 11 reading checkpoints · 2 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 (7)
gaussian equal transitivegaussian equal symmetricgaussian product associategaussian product integer congruencegaussian conjugate product is normgaussian equal reflexivegaussian natural scalar product
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 hnorm
02Establish hassociationL11–20

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

  1. L11
    have hassociation · expand full local formula (2,880 characters)have hassociation : ((((((((((a) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((b) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((d) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))) + (((c) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))))))) + (((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (g))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (h)))))))) = ((((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (h))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (g))))))) + (((((((a) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((b) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((d) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))) + (((c) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))))))))) /\ (((((((((a) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))) + (((b) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))))) + (((((d) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (f))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (e)))))))) = ((((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (e))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (f))))))) + (((((((a) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))) + (((b) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))))) + (((((d) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))))))
  2. L12
    specialize gaussian_equal_symmetric ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (h))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (g))))))
  3. L13
    specialize gaussian_equal_symmetric ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (g))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (h))))))
  4. L14
    specialize gaussian_equal_symmetric ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (e))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (f))))))
  5. L15
    specialize gaussian_equal_symmetric ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (f))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (e))))))
  6. L16
    specialize gaussian_equal_symmetric ((((((a) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((b) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((d) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))) + (((c) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))))))
  7. L17
    specialize gaussian_equal_symmetric ((((((a) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((b) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((d) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))) + (((c) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))))))
  8. L18
    specialize gaussian_equal_symmetric ((((((a) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))) + (((b) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))))) + (((((d) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  9. L19
    specialize gaussian_equal_symmetric ((((((a) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))) + (((b) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))))) + (((((d) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  10. L20
    apply gaussian_equal_symmetric
03Use earlier factsL21–30

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

  1. L21
    specialize gaussian_product_associate a
  2. L22
    specialize gaussian_product_associate b
  3. L23
    specialize gaussian_product_associate d
  4. L24
    specialize gaussian_product_associate c
  5. L25
    specialize gaussian_product_associate a
  6. L26
    specialize gaussian_product_associate b
  7. L27
    specialize gaussian_product_associate c
  8. L28
    specialize gaussian_product_associate d
  9. L29
    specialize gaussian_product_associate e
  10. L30
    specialize gaussian_product_associate f
04Use earlier factsL31–33

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

  1. L31
    specialize gaussian_product_associate g
  2. L32
    specialize gaussian_product_associate h
  3. L33
    apply gaussian_product_associate
05Establish hscalingL34–43

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

  1. L34
    have hscaling · expand full local formula (1,516 characters)have hscaling : ((((((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (h))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (g))))))) + (((N) * (f)))) = ((((N) * (e))) + (((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (g))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (h))))))))) /\ (((((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (e))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (f))))))) + (((N) * (h)))) = ((((N) * (g))) + (((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (f))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (e))))))))))
  2. L35
    specialize gaussian_equal_transitive ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (h))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (g))))))
  3. L36
    specialize gaussian_equal_transitive ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (g))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (h))))))
  4. L37
    specialize gaussian_equal_transitive ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (e))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (f))))))
  5. L38
    specialize gaussian_equal_transitive ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (f))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (e))))))
  6. L39
    specialize gaussian_equal_transitive ((((((N) * (e))) + (((0) * (f))))) + (((((0) * (h))) + (((0) * (g))))))
  7. L40
    specialize gaussian_equal_transitive ((((((N) * (f))) + (((0) * (e))))) + (((((0) * (g))) + (((0) * (h))))))
  8. L41
    specialize gaussian_equal_transitive ((((((N) * (g))) + (((0) * (h))))) + (((((0) * (e))) + (((0) * (f))))))
  9. L42
    specialize gaussian_equal_transitive ((((((N) * (h))) + (((0) * (g))))) + (((((0) * (f))) + (((0) * (e))))))
  10. L43
    specialize gaussian_equal_transitive ((N) * (e))
06Use earlier factsL44–53

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

  1. L44
    specialize gaussian_equal_transitive ((N) * (f))
  2. L45
    specialize gaussian_equal_transitive ((N) * (g))
  3. L46
    specialize gaussian_equal_transitive ((N) * (h))
  4. L47
    apply gaussian_equal_transitive
  5. L48
    specialize gaussian_product_integer_congruence ((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))
  6. L49
    specialize gaussian_product_integer_congruence ((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))
  7. L50
    specialize gaussian_product_integer_congruence ((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))
  8. L51
    specialize gaussian_product_integer_congruence ((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))
  9. L52
    specialize gaussian_product_integer_congruence N
  10. L53
    specialize gaussian_product_integer_congruence 0
07Use earlier factsL54–63

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

  1. L54
    specialize gaussian_product_integer_congruence 0
  2. L55
    specialize gaussian_product_integer_congruence 0
  3. L56
    specialize gaussian_product_integer_congruence e
  4. L57
    specialize gaussian_product_integer_congruence f
  5. L58
    specialize gaussian_product_integer_congruence g
  6. L59
    specialize gaussian_product_integer_congruence h
  7. L60
    specialize gaussian_product_integer_congruence e
  8. L61
    specialize gaussian_product_integer_congruence f
  9. L62
    specialize gaussian_product_integer_congruence g
  10. L63
    specialize gaussian_product_integer_congruence h
08Use earlier factsL64–73

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

  1. L64
    apply gaussian_product_integer_congruence
  2. L65
    specialize gaussian_conjugate_product_is_norm a
  3. L66
    specialize gaussian_conjugate_product_is_norm b
  4. L67
    specialize gaussian_conjugate_product_is_norm c
  5. L68
    specialize gaussian_conjugate_product_is_norm d
  6. L69
    specialize gaussian_conjugate_product_is_norm N
  7. L70
    apply gaussian_conjugate_product_is_norm
  8. L71
    exact hnorm
  9. L72
    specialize gaussian_equal_reflexive e
  10. L73
    specialize gaussian_equal_reflexive f
09Use earlier factsL74–83

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

  1. L74
    specialize gaussian_equal_reflexive g
  2. L75
    specialize gaussian_equal_reflexive h
  3. L76
    apply gaussian_equal_reflexive
  4. L77
    specialize gaussian_natural_scalar_product N
  5. L78
    specialize gaussian_natural_scalar_product e
  6. L79
    specialize gaussian_natural_scalar_product f
  7. L80
    specialize gaussian_natural_scalar_product g
  8. L81
    specialize gaussian_natural_scalar_product h
  9. L82
    apply gaussian_natural_scalar_product
  10. L83
    specialize gaussian_equal_transitive ((((((a) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((b) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((d) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))) + (((c) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))))))
10Use earlier factsL84–93

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

  1. L84
    specialize gaussian_equal_transitive ((((((a) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((b) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((d) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))) + (((c) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))))))
  2. L85
    specialize gaussian_equal_transitive ((((((a) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))) + (((b) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))))) + (((((d) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  3. L86
    specialize gaussian_equal_transitive ((((((a) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))) + (((b) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))))) + (((((d) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  4. L87
    specialize gaussian_equal_transitive ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (h))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (g))))))
  5. L88
    specialize gaussian_equal_transitive ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (g))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (h))))))
  6. L89
    specialize gaussian_equal_transitive ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (e))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (f))))))
  7. L90
    specialize gaussian_equal_transitive ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (f))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (e))))))
  8. L91
    specialize gaussian_equal_transitive ((N) * (e))
  9. L92
    specialize gaussian_equal_transitive ((N) * (f))
  10. L93
    specialize gaussian_equal_transitive ((N) * (g))
11Use earlier factsL94–97

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

  1. L94
    specialize gaussian_equal_transitive ((N) * (h))
  2. L95
    apply gaussian_equal_transitive
  3. L96
    exact hassociation
  4. L97
    exact hscaling

Library-wide reading audit

Original exact command ledger · 97 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 hnorm
  11. 0011have hassociation : ((((((((((a) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((b) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((d) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))) + (((c) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))))))) + (((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (g))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (h)))))))) = ((((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (h))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (g))))))) + (((((((a) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((b) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((d) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))) + (((c) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))))))))) /\ (((((((((a) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))) + (((b) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))))) + (((((d) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))) + (((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (f))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (e)))))))) = ((((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (e))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (f))))))) + (((((((a) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))) + (((b) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))))) + (((((d) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))))))
  12. 0012specialize gaussian_equal_symmetric ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (h))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (g))))))
  13. 0013specialize gaussian_equal_symmetric ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (g))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (h))))))
  14. 0014specialize gaussian_equal_symmetric ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (e))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (f))))))
  15. 0015specialize gaussian_equal_symmetric ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (f))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (e))))))
  16. 0016specialize gaussian_equal_symmetric ((((((a) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((b) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((d) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))) + (((c) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))))))
  17. 0017specialize gaussian_equal_symmetric ((((((a) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((b) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((d) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))) + (((c) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))))))
  18. 0018specialize gaussian_equal_symmetric ((((((a) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))) + (((b) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))))) + (((((d) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  19. 0019specialize gaussian_equal_symmetric ((((((a) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))) + (((b) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))))) + (((((d) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  20. 0020apply gaussian_equal_symmetric
  21. 0021specialize gaussian_product_associate a
  22. 0022specialize gaussian_product_associate b
  23. 0023specialize gaussian_product_associate d
  24. 0024specialize gaussian_product_associate c
  25. 0025specialize gaussian_product_associate a
  26. 0026specialize gaussian_product_associate b
  27. 0027specialize gaussian_product_associate c
  28. 0028specialize gaussian_product_associate d
  29. 0029specialize gaussian_product_associate e
  30. 0030specialize gaussian_product_associate f
  31. 0031specialize gaussian_product_associate g
  32. 0032specialize gaussian_product_associate h
  33. 0033apply gaussian_product_associate
  34. 0034have hscaling : ((((((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (h))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (g))))))) + (((N) * (f)))) = ((((N) * (e))) + (((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (g))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (h))))))))) /\ (((((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (e))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (f))))))) + (((N) * (h)))) = ((((N) * (g))) + (((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (f))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (e))))))))))
  35. 0035specialize gaussian_equal_transitive ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (h))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (g))))))
  36. 0036specialize gaussian_equal_transitive ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (g))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (h))))))
  37. 0037specialize gaussian_equal_transitive ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (e))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (f))))))
  38. 0038specialize gaussian_equal_transitive ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (f))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (e))))))
  39. 0039specialize gaussian_equal_transitive ((((((N) * (e))) + (((0) * (f))))) + (((((0) * (h))) + (((0) * (g))))))
  40. 0040specialize gaussian_equal_transitive ((((((N) * (f))) + (((0) * (e))))) + (((((0) * (g))) + (((0) * (h))))))
  41. 0041specialize gaussian_equal_transitive ((((((N) * (g))) + (((0) * (h))))) + (((((0) * (e))) + (((0) * (f))))))
  42. 0042specialize gaussian_equal_transitive ((((((N) * (h))) + (((0) * (g))))) + (((((0) * (f))) + (((0) * (e))))))
  43. 0043specialize gaussian_equal_transitive ((N) * (e))
  44. 0044specialize gaussian_equal_transitive ((N) * (f))
  45. 0045specialize gaussian_equal_transitive ((N) * (g))
  46. 0046specialize gaussian_equal_transitive ((N) * (h))
  47. 0047apply gaussian_equal_transitive
  48. 0048specialize gaussian_product_integer_congruence ((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))
  49. 0049specialize gaussian_product_integer_congruence ((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))
  50. 0050specialize gaussian_product_integer_congruence ((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))
  51. 0051specialize gaussian_product_integer_congruence ((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))
  52. 0052specialize gaussian_product_integer_congruence N
  53. 0053specialize gaussian_product_integer_congruence 0
  54. 0054specialize gaussian_product_integer_congruence 0
  55. 0055specialize gaussian_product_integer_congruence 0
  56. 0056specialize gaussian_product_integer_congruence e
  57. 0057specialize gaussian_product_integer_congruence f
  58. 0058specialize gaussian_product_integer_congruence g
  59. 0059specialize gaussian_product_integer_congruence h
  60. 0060specialize gaussian_product_integer_congruence e
  61. 0061specialize gaussian_product_integer_congruence f
  62. 0062specialize gaussian_product_integer_congruence g
  63. 0063specialize gaussian_product_integer_congruence h
  64. 0064apply gaussian_product_integer_congruence
  65. 0065specialize gaussian_conjugate_product_is_norm a
  66. 0066specialize gaussian_conjugate_product_is_norm b
  67. 0067specialize gaussian_conjugate_product_is_norm c
  68. 0068specialize gaussian_conjugate_product_is_norm d
  69. 0069specialize gaussian_conjugate_product_is_norm N
  70. 0070apply gaussian_conjugate_product_is_norm
  71. 0071exact hnorm
  72. 0072specialize gaussian_equal_reflexive e
  73. 0073specialize gaussian_equal_reflexive f
  74. 0074specialize gaussian_equal_reflexive g
  75. 0075specialize gaussian_equal_reflexive h
  76. 0076apply gaussian_equal_reflexive
  77. 0077specialize gaussian_natural_scalar_product N
  78. 0078specialize gaussian_natural_scalar_product e
  79. 0079specialize gaussian_natural_scalar_product f
  80. 0080specialize gaussian_natural_scalar_product g
  81. 0081specialize gaussian_natural_scalar_product h
  82. 0082apply gaussian_natural_scalar_product
  83. 0083specialize gaussian_equal_transitive ((((((a) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((b) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))) + (((((d) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))) + (((c) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))))))
  84. 0084specialize gaussian_equal_transitive ((((((a) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((b) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))) + (((((d) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))) + (((c) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))))))
  85. 0085specialize gaussian_equal_transitive ((((((a) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))) + (((b) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))))) + (((((d) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))) + (((c) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))))))
  86. 0086specialize gaussian_equal_transitive ((((((a) * (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))))) + (((b) * (((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))))))) + (((((d) * (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))))) + (((c) * (((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))))))))
  87. 0087specialize gaussian_equal_transitive ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (e))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (f))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (h))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (g))))))
  88. 0088specialize gaussian_equal_transitive ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (f))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (e))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (g))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (h))))))
  89. 0089specialize gaussian_equal_transitive ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (g))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (h))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (e))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (f))))))
  90. 0090specialize gaussian_equal_transitive ((((((((((((a) * (a))) + (((b) * (b))))) + (((((d) * (d))) + (((c) * (c))))))) * (h))) + (((((((((a) * (b))) + (((b) * (a))))) + (((((d) * (c))) + (((c) * (d))))))) * (g))))) + (((((((((((a) * (c))) + (((b) * (d))))) + (((((d) * (a))) + (((c) * (b))))))) * (f))) + (((((((((a) * (d))) + (((b) * (c))))) + (((((d) * (b))) + (((c) * (a))))))) * (e))))))
  91. 0091specialize gaussian_equal_transitive ((N) * (e))
  92. 0092specialize gaussian_equal_transitive ((N) * (f))
  93. 0093specialize gaussian_equal_transitive ((N) * (g))
  94. 0094specialize gaussian_equal_transitive ((N) * (h))
  95. 0095apply gaussian_equal_transitive
  96. 0096exact hassociation
  97. 0097exact hscaling