GI0054

gaussian_add_for_representations

The canonical Gaussian add graph agrees with actual arithmetic on every chosen integer representative.

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

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.

The natural-code carrier consists of genuine pairs of the existing signed integers; no new primitive arithmetic is trusted. The theorem constructs quotient, remainder, and actual norm witnesses. Gaussian gcd, unique factorization, and prime classification are separate targets.

Exact theorem in conservative defined notation

∀ ac. ∀ bc. ∀ cc. ∀ a. ∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ h. ZPairRep(ac,a,b,c,d) → ZPairRep(bc,e,f,g,h) → ZPairAdd(ac,bc,cc) → ZPairRep(cc,a + e,b + f,c + g,d + h)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

ZPairRep(z,ap,an,bp,bn) · 3ZPairAdd(a,b,c) · 1

Actual proof prerequisites

gaussian_representation_integer_transportgaussian_sum_integer_congruencegaussian_representation_equal
Original expanded first-order statement 
forall ac bc cc a b c d e f g h. (exists ge_representation_real_code_add_fixed_first ge_representation_imaginary_code_add_fixed_first. (((ac) = ((ge_representation_real_code_add_fixed_first) + (ge_representation_imaginary_code_add_fixed_first)) * S ((ge_representation_real_code_add_fixed_first) + (ge_representation_imaginary_code_add_fixed_first)) + ((ge_representation_imaginary_code_add_fixed_first) + (ge_representation_imaginary_code_add_fixed_first))) /\ ((exists ge_balance_positive_add_fixed_firstreal ge_balance_negative_add_fixed_firstreal. (((((ge_representation_real_code_add_fixed_first) = 2 * (ge_balance_positive_add_fixed_firstreal) /\ (ge_balance_negative_add_fixed_firstreal) = 0) \/ exists ge_signed_half_add_fixed_firstrealdecode. (((ge_representation_real_code_add_fixed_first) = 2 * ge_signed_half_add_fixed_firstrealdecode + 1 /\ (ge_balance_positive_add_fixed_firstreal) = 0) /\ (ge_balance_negative_add_fixed_firstreal) = S ge_signed_half_add_fixed_firstrealdecode))) /\ ((a) + ge_balance_negative_add_fixed_firstreal = (b) + ge_balance_positive_add_fixed_firstreal))) /\ (exists ge_balance_positive_add_fixed_firstimaginary ge_balance_negative_add_fixed_firstimaginary. (((((ge_representation_imaginary_code_add_fixed_first) = 2 * (ge_balance_positive_add_fixed_firstimaginary) /\ (ge_balance_negative_add_fixed_firstimaginary) = 0) \/ exists ge_signed_half_add_fixed_firstimaginarydecode. (((ge_representation_imaginary_code_add_fixed_first) = 2 * ge_signed_half_add_fixed_firstimaginarydecode + 1 /\ (ge_balance_positive_add_fixed_firstimaginary) = 0) /\ (ge_balance_negative_add_fixed_firstimaginary) = S ge_signed_half_add_fixed_firstimaginarydecode))) /\ ((c) + ge_balance_negative_add_fixed_firstimaginary = (d) + ge_balance_positive_add_fixed_firstimaginary)))))) -> (exists ge_representation_real_code_add_fixed_second ge_representation_imaginary_code_add_fixed_second. (((bc) = ((ge_representation_real_code_add_fixed_second) + (ge_representation_imaginary_code_add_fixed_second)) * S ((ge_representation_real_code_add_fixed_second) + (ge_representation_imaginary_code_add_fixed_second)) + ((ge_representation_imaginary_code_add_fixed_second) + (ge_representation_imaginary_code_add_fixed_second))) /\ ((exists ge_balance_positive_add_fixed_secondreal ge_balance_negative_add_fixed_secondreal. (((((ge_representation_real_code_add_fixed_second) = 2 * (ge_balance_positive_add_fixed_secondreal) /\ (ge_balance_negative_add_fixed_secondreal) = 0) \/ exists ge_signed_half_add_fixed_secondrealdecode. (((ge_representation_real_code_add_fixed_second) = 2 * ge_signed_half_add_fixed_secondrealdecode + 1 /\ (ge_balance_positive_add_fixed_secondreal) = 0) /\ (ge_balance_negative_add_fixed_secondreal) = S ge_signed_half_add_fixed_secondrealdecode))) /\ ((e) + ge_balance_negative_add_fixed_secondreal = (f) + ge_balance_positive_add_fixed_secondreal))) /\ (exists ge_balance_positive_add_fixed_secondimaginary ge_balance_negative_add_fixed_secondimaginary. (((((ge_representation_imaginary_code_add_fixed_second) = 2 * (ge_balance_positive_add_fixed_secondimaginary) /\ (ge_balance_negative_add_fixed_secondimaginary) = 0) \/ exists ge_signed_half_add_fixed_secondimaginarydecode. (((ge_representation_imaginary_code_add_fixed_second) = 2 * ge_signed_half_add_fixed_secondimaginarydecode + 1 /\ (ge_balance_positive_add_fixed_secondimaginary) = 0) /\ (ge_balance_negative_add_fixed_secondimaginary) = S ge_signed_half_add_fixed_secondimaginarydecode))) /\ ((g) + ge_balance_negative_add_fixed_secondimaginary = (h) + ge_balance_positive_add_fixed_secondimaginary)))))) -> (exists ge_first_rp_add_fixed_graph ge_first_rn_add_fixed_graph ge_first_ip_add_fixed_graph ge_first_in_add_fixed_graph ge_second_rp_add_fixed_graph ge_second_rn_add_fixed_graph ge_second_ip_add_fixed_graph ge_second_in_add_fixed_graph. ((exists ge_representation_real_code_add_fixed_graphfirst ge_representation_imaginary_code_add_fixed_graphfirst. (((ac) = ((ge_representation_real_code_add_fixed_graphfirst) + (ge_representation_imaginary_code_add_fixed_graphfirst)) * S ((ge_representation_real_code_add_fixed_graphfirst) + (ge_representation_imaginary_code_add_fixed_graphfirst)) + ((ge_representation_imaginary_code_add_fixed_graphfirst) + (ge_representation_imaginary_code_add_fixed_graphfirst))) /\ ((exists ge_balance_positive_add_fixed_graphfirstreal ge_balance_negative_add_fixed_graphfirstreal. (((((ge_representation_real_code_add_fixed_graphfirst) = 2 * (ge_balance_positive_add_fixed_graphfirstreal) /\ (ge_balance_negative_add_fixed_graphfirstreal) = 0) \/ exists ge_signed_half_add_fixed_graphfirstrealdecode. (((ge_representation_real_code_add_fixed_graphfirst) = 2 * ge_signed_half_add_fixed_graphfirstrealdecode + 1 /\ (ge_balance_positive_add_fixed_graphfirstreal) = 0) /\ (ge_balance_negative_add_fixed_graphfirstreal) = S ge_signed_half_add_fixed_graphfirstrealdecode))) /\ ((ge_first_rp_add_fixed_graph) + ge_balance_negative_add_fixed_graphfirstreal = (ge_first_rn_add_fixed_graph) + ge_balance_positive_add_fixed_graphfirstreal))) /\ (exists ge_balance_positive_add_fixed_graphfirstimaginary ge_balance_negative_add_fixed_graphfirstimaginary. (((((ge_representation_imaginary_code_add_fixed_graphfirst) = 2 * (ge_balance_positive_add_fixed_graphfirstimaginary) /\ (ge_balance_negative_add_fixed_graphfirstimaginary) = 0) \/ exists ge_signed_half_add_fixed_graphfirstimaginarydecode. (((ge_representation_imaginary_code_add_fixed_graphfirst) = 2 * ge_signed_half_add_fixed_graphfirstimaginarydecode + 1 /\ (ge_balance_positive_add_fixed_graphfirstimaginary) = 0) /\ (ge_balance_negative_add_fixed_graphfirstimaginary) = S ge_signed_half_add_fixed_graphfirstimaginarydecode))) /\ ((ge_first_ip_add_fixed_graph) + ge_balance_negative_add_fixed_graphfirstimaginary = (ge_first_in_add_fixed_graph) + ge_balance_positive_add_fixed_graphfirstimaginary)))))) /\ ((exists ge_representation_real_code_add_fixed_graphsecond ge_representation_imaginary_code_add_fixed_graphsecond. (((bc) = ((ge_representation_real_code_add_fixed_graphsecond) + (ge_representation_imaginary_code_add_fixed_graphsecond)) * S ((ge_representation_real_code_add_fixed_graphsecond) + (ge_representation_imaginary_code_add_fixed_graphsecond)) + ((ge_representation_imaginary_code_add_fixed_graphsecond) + (ge_representation_imaginary_code_add_fixed_graphsecond))) /\ ((exists ge_balance_positive_add_fixed_graphsecondreal ge_balance_negative_add_fixed_graphsecondreal. (((((ge_representation_real_code_add_fixed_graphsecond) = 2 * (ge_balance_positive_add_fixed_graphsecondreal) /\ (ge_balance_negative_add_fixed_graphsecondreal) = 0) \/ exists ge_signed_half_add_fixed_graphsecondrealdecode. (((ge_representation_real_code_add_fixed_graphsecond) = 2 * ge_signed_half_add_fixed_graphsecondrealdecode + 1 /\ (ge_balance_positive_add_fixed_graphsecondreal) = 0) /\ (ge_balance_negative_add_fixed_graphsecondreal) = S ge_signed_half_add_fixed_graphsecondrealdecode))) /\ ((ge_second_rp_add_fixed_graph) + ge_balance_negative_add_fixed_graphsecondreal = (ge_second_rn_add_fixed_graph) + ge_balance_positive_add_fixed_graphsecondreal))) /\ (exists ge_balance_positive_add_fixed_graphsecondimaginary ge_balance_negative_add_fixed_graphsecondimaginary. (((((ge_representation_imaginary_code_add_fixed_graphsecond) = 2 * (ge_balance_positive_add_fixed_graphsecondimaginary) /\ (ge_balance_negative_add_fixed_graphsecondimaginary) = 0) \/ exists ge_signed_half_add_fixed_graphsecondimaginarydecode. (((ge_representation_imaginary_code_add_fixed_graphsecond) = 2 * ge_signed_half_add_fixed_graphsecondimaginarydecode + 1 /\ (ge_balance_positive_add_fixed_graphsecondimaginary) = 0) /\ (ge_balance_negative_add_fixed_graphsecondimaginary) = S ge_signed_half_add_fixed_graphsecondimaginarydecode))) /\ ((ge_second_ip_add_fixed_graph) + ge_balance_negative_add_fixed_graphsecondimaginary = (ge_second_in_add_fixed_graph) + ge_balance_positive_add_fixed_graphsecondimaginary)))))) /\ (exists ge_representation_real_code_add_fixed_graphoutput ge_representation_imaginary_code_add_fixed_graphoutput. (((cc) = ((ge_representation_real_code_add_fixed_graphoutput) + (ge_representation_imaginary_code_add_fixed_graphoutput)) * S ((ge_representation_real_code_add_fixed_graphoutput) + (ge_representation_imaginary_code_add_fixed_graphoutput)) + ((ge_representation_imaginary_code_add_fixed_graphoutput) + (ge_representation_imaginary_code_add_fixed_graphoutput))) /\ ((exists ge_balance_positive_add_fixed_graphoutputreal ge_balance_negative_add_fixed_graphoutputreal. (((((ge_representation_real_code_add_fixed_graphoutput) = 2 * (ge_balance_positive_add_fixed_graphoutputreal) /\ (ge_balance_negative_add_fixed_graphoutputreal) = 0) \/ exists ge_signed_half_add_fixed_graphoutputrealdecode. (((ge_representation_real_code_add_fixed_graphoutput) = 2 * ge_signed_half_add_fixed_graphoutputrealdecode + 1 /\ (ge_balance_positive_add_fixed_graphoutputreal) = 0) /\ (ge_balance_negative_add_fixed_graphoutputreal) = S ge_signed_half_add_fixed_graphoutputrealdecode))) /\ ((((ge_first_rp_add_fixed_graph) + (ge_second_rp_add_fixed_graph))) + ge_balance_negative_add_fixed_graphoutputreal = (((ge_first_rn_add_fixed_graph) + (ge_second_rn_add_fixed_graph))) + ge_balance_positive_add_fixed_graphoutputreal))) /\ (exists ge_balance_positive_add_fixed_graphoutputimaginary ge_balance_negative_add_fixed_graphoutputimaginary. (((((ge_representation_imaginary_code_add_fixed_graphoutput) = 2 * (ge_balance_positive_add_fixed_graphoutputimaginary) /\ (ge_balance_negative_add_fixed_graphoutputimaginary) = 0) \/ exists ge_signed_half_add_fixed_graphoutputimaginarydecode. (((ge_representation_imaginary_code_add_fixed_graphoutput) = 2 * ge_signed_half_add_fixed_graphoutputimaginarydecode + 1 /\ (ge_balance_positive_add_fixed_graphoutputimaginary) = 0) /\ (ge_balance_negative_add_fixed_graphoutputimaginary) = S ge_signed_half_add_fixed_graphoutputimaginarydecode))) /\ ((((ge_first_ip_add_fixed_graph) + (ge_second_ip_add_fixed_graph))) + ge_balance_negative_add_fixed_graphoutputimaginary = (((ge_first_in_add_fixed_graph) + (ge_second_in_add_fixed_graph))) + ge_balance_positive_add_fixed_graphoutputimaginary))))))))) -> (exists ge_representation_real_code_add_fixed_output ge_representation_imaginary_code_add_fixed_output. (((cc) = ((ge_representation_real_code_add_fixed_output) + (ge_representation_imaginary_code_add_fixed_output)) * S ((ge_representation_real_code_add_fixed_output) + (ge_representation_imaginary_code_add_fixed_output)) + ((ge_representation_imaginary_code_add_fixed_output) + (ge_representation_imaginary_code_add_fixed_output))) /\ ((exists ge_balance_positive_add_fixed_outputreal ge_balance_negative_add_fixed_outputreal. (((((ge_representation_real_code_add_fixed_output) = 2 * (ge_balance_positive_add_fixed_outputreal) /\ (ge_balance_negative_add_fixed_outputreal) = 0) \/ exists ge_signed_half_add_fixed_outputrealdecode. (((ge_representation_real_code_add_fixed_output) = 2 * ge_signed_half_add_fixed_outputrealdecode + 1 /\ (ge_balance_positive_add_fixed_outputreal) = 0) /\ (ge_balance_negative_add_fixed_outputreal) = S ge_signed_half_add_fixed_outputrealdecode))) /\ ((((a) + (e))) + ge_balance_negative_add_fixed_outputreal = (((b) + (f))) + ge_balance_positive_add_fixed_outputreal))) /\ (exists ge_balance_positive_add_fixed_outputimaginary ge_balance_negative_add_fixed_outputimaginary. (((((ge_representation_imaginary_code_add_fixed_output) = 2 * (ge_balance_positive_add_fixed_outputimaginary) /\ (ge_balance_negative_add_fixed_outputimaginary) = 0) \/ exists ge_signed_half_add_fixed_outputimaginarydecode. (((ge_representation_imaginary_code_add_fixed_output) = 2 * ge_signed_half_add_fixed_outputimaginarydecode + 1 /\ (ge_balance_positive_add_fixed_outputimaginary) = 0) /\ (ge_balance_negative_add_fixed_outputimaginary) = S ge_signed_half_add_fixed_outputimaginarydecode))) /\ ((((c) + (g))) + ge_balance_negative_add_fixed_outputimaginary = (((d) + (h))) + ge_balance_positive_add_fixed_outputimaginary))))))

Complete tactic proof in conservative notation

All 76 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

76 script commands · 9 reading checkpoints · 0 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (3)
gaussian representation integer transportgaussian sum integer congruencegaussian representation equal
01Fix variables and assumptionsL1–10

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

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

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

  1. L11
    intro h
  2. L12
    intro hfirst
  3. L13
    intro hsecond
  4. L14
    intro hoperation
03Separate the logical casesL15–24

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

  1. L15
    cases hoperation
  2. L16
    cases hoperation_witness
  3. L17
    cases hoperation_witness_witness
  4. L18
    cases hoperation_witness_witness_witness
  5. L19
    cases hoperation_witness_witness_witness_witness
  6. L20
    cases hoperation_witness_witness_witness_witness_witness
  7. L21
    cases hoperation_witness_witness_witness_witness_witness_witness
  8. L22
    cases hoperation_witness_witness_witness_witness_witness_witness_witness
  9. L23
    cases hoperation_witness_witness_witness_witness_witness_witness_witness_witness
  10. L24
    cases hoperation_witness_witness_witness_witness_witness_witness_witness_witness_right
04Use earlier factsL25–34

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

  1. L25
    specialize gaussian_representation_integer_transport cc
  2. L26
    specialize gaussian_representation_integer_transport ((x) + (x4))
  3. L27
    specialize gaussian_representation_integer_transport ((x1) + (x5))
  4. L28
    specialize gaussian_representation_integer_transport ((x2) + (x6))
  5. L29
    specialize gaussian_representation_integer_transport ((x3) + (x7))
  6. L30
    specialize gaussian_representation_integer_transport ((a) + (e))
  7. L31
    specialize gaussian_representation_integer_transport ((b) + (f))
  8. L32
    specialize gaussian_representation_integer_transport ((c) + (g))
  9. L33
    specialize gaussian_representation_integer_transport ((d) + (h))
  10. L34
    apply gaussian_representation_integer_transport
05Use earlier factsL35–44

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

  1. L35
    specialize gaussian_sum_integer_congruence x
  2. L36
    specialize gaussian_sum_integer_congruence x1
  3. L37
    specialize gaussian_sum_integer_congruence x2
  4. L38
    specialize gaussian_sum_integer_congruence x3
  5. L39
    specialize gaussian_sum_integer_congruence x4
  6. L40
    specialize gaussian_sum_integer_congruence x5
  7. L41
    specialize gaussian_sum_integer_congruence x6
  8. L42
    specialize gaussian_sum_integer_congruence x7
  9. L43
    specialize gaussian_sum_integer_congruence a
  10. L44
    specialize gaussian_sum_integer_congruence b
06Use earlier factsL45–54

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

  1. L45
    specialize gaussian_sum_integer_congruence c
  2. L46
    specialize gaussian_sum_integer_congruence d
  3. L47
    specialize gaussian_sum_integer_congruence e
  4. L48
    specialize gaussian_sum_integer_congruence f
  5. L49
    specialize gaussian_sum_integer_congruence g
  6. L50
    specialize gaussian_sum_integer_congruence h
  7. L51
    apply gaussian_sum_integer_congruence
  8. L52
    specialize gaussian_representation_equal ac
  9. L53
    specialize gaussian_representation_equal x
  10. L54
    specialize gaussian_representation_equal x1
07Use earlier factsL55–64

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

  1. L55
    specialize gaussian_representation_equal x2
  2. L56
    specialize gaussian_representation_equal x3
  3. L57
    specialize gaussian_representation_equal a
  4. L58
    specialize gaussian_representation_equal b
  5. L59
    specialize gaussian_representation_equal c
  6. L60
    specialize gaussian_representation_equal d
  7. L61
    apply gaussian_representation_equal
  8. L62
    exact hoperation_witness_witness_witness_witness_witness_witness_witness_witness_left
  9. L63
    exact hfirst
  10. L64
    specialize gaussian_representation_equal bc
08Use earlier factsL65–74

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

  1. L65
    specialize gaussian_representation_equal x4
  2. L66
    specialize gaussian_representation_equal x5
  3. L67
    specialize gaussian_representation_equal x6
  4. L68
    specialize gaussian_representation_equal x7
  5. L69
    specialize gaussian_representation_equal e
  6. L70
    specialize gaussian_representation_equal f
  7. L71
    specialize gaussian_representation_equal g
  8. L72
    specialize gaussian_representation_equal h
  9. L73
    apply gaussian_representation_equal
  10. L74
    exact hoperation_witness_witness_witness_witness_witness_witness_witness_witness_right_left
09Use earlier factsL75–76

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

  1. L75
    exact hsecond
  2. L76
    exact hoperation_witness_witness_witness_witness_witness_witness_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 76 lines
  1. 0001intro ac
  2. 0002intro bc
  3. 0003intro cc
  4. 0004intro a
  5. 0005intro b
  6. 0006intro c
  7. 0007intro d
  8. 0008intro e
  9. 0009intro f
  10. 0010intro g
  11. 0011intro h
  12. 0012intro hfirst
  13. 0013intro hsecond
  14. 0014intro hoperation
  15. 0015cases hoperation
  16. 0016cases hoperation_witness
  17. 0017cases hoperation_witness_witness
  18. 0018cases hoperation_witness_witness_witness
  19. 0019cases hoperation_witness_witness_witness_witness
  20. 0020cases hoperation_witness_witness_witness_witness_witness
  21. 0021cases hoperation_witness_witness_witness_witness_witness_witness
  22. 0022cases hoperation_witness_witness_witness_witness_witness_witness_witness
  23. 0023cases hoperation_witness_witness_witness_witness_witness_witness_witness_witness
  24. 0024cases hoperation_witness_witness_witness_witness_witness_witness_witness_witness_right
  25. 0025specialize gaussian_representation_integer_transport cc
  26. 0026specialize gaussian_representation_integer_transport ((x) + (x4))
  27. 0027specialize gaussian_representation_integer_transport ((x1) + (x5))
  28. 0028specialize gaussian_representation_integer_transport ((x2) + (x6))
  29. 0029specialize gaussian_representation_integer_transport ((x3) + (x7))
  30. 0030specialize gaussian_representation_integer_transport ((a) + (e))
  31. 0031specialize gaussian_representation_integer_transport ((b) + (f))
  32. 0032specialize gaussian_representation_integer_transport ((c) + (g))
  33. 0033specialize gaussian_representation_integer_transport ((d) + (h))
  34. 0034apply gaussian_representation_integer_transport
  35. 0035specialize gaussian_sum_integer_congruence x
  36. 0036specialize gaussian_sum_integer_congruence x1
  37. 0037specialize gaussian_sum_integer_congruence x2
  38. 0038specialize gaussian_sum_integer_congruence x3
  39. 0039specialize gaussian_sum_integer_congruence x4
  40. 0040specialize gaussian_sum_integer_congruence x5
  41. 0041specialize gaussian_sum_integer_congruence x6
  42. 0042specialize gaussian_sum_integer_congruence x7
  43. 0043specialize gaussian_sum_integer_congruence a
  44. 0044specialize gaussian_sum_integer_congruence b
  45. 0045specialize gaussian_sum_integer_congruence c
  46. 0046specialize gaussian_sum_integer_congruence d
  47. 0047specialize gaussian_sum_integer_congruence e
  48. 0048specialize gaussian_sum_integer_congruence f
  49. 0049specialize gaussian_sum_integer_congruence g
  50. 0050specialize gaussian_sum_integer_congruence h
  51. 0051apply gaussian_sum_integer_congruence
  52. 0052specialize gaussian_representation_equal ac
  53. 0053specialize gaussian_representation_equal x
  54. 0054specialize gaussian_representation_equal x1
  55. 0055specialize gaussian_representation_equal x2
  56. 0056specialize gaussian_representation_equal x3
  57. 0057specialize gaussian_representation_equal a
  58. 0058specialize gaussian_representation_equal b
  59. 0059specialize gaussian_representation_equal c
  60. 0060specialize gaussian_representation_equal d
  61. 0061apply gaussian_representation_equal
  62. 0062exact hoperation_witness_witness_witness_witness_witness_witness_witness_witness_left
  63. 0063exact hfirst
  64. 0064specialize gaussian_representation_equal bc
  65. 0065specialize gaussian_representation_equal x4
  66. 0066specialize gaussian_representation_equal x5
  67. 0067specialize gaussian_representation_equal x6
  68. 0068specialize gaussian_representation_equal x7
  69. 0069specialize gaussian_representation_equal e
  70. 0070specialize gaussian_representation_equal f
  71. 0071specialize gaussian_representation_equal g
  72. 0072specialize gaussian_representation_equal h
  73. 0073apply gaussian_representation_equal
  74. 0074exact hoperation_witness_witness_witness_witness_witness_witness_witness_witness_right_left
  75. 0075exact hsecond
  76. 0076exact hoperation_witness_witness_witness_witness_witness_witness_witness_witness_right_right