GF002C

gaussian_subtract_exists

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

Every actual Gaussian difference has a constructed canonical code solving c+b=a, without assuming a subtraction 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. (exists ge_real_positive_subtract_first ge_real_negative_subtract_first ge_imaginary_positive_subtract_first ge_imaginary_negative_subtract_first. (exists ge_real_code_subtract_firstdecode ge_imaginary_code_subtract_firstdecode. (((a) = ((ge_real_code_subtract_firstdecode) + (ge_imaginary_code_subtract_firstdecode)) * S ((ge_real_code_subtract_firstdecode) + (ge_imaginary_code_subtract_firstdecode)) + ((ge_imaginary_code_subtract_firstdecode) + (ge_imaginary_code_subtract_firstdecode))) /\ (((((ge_real_code_subtract_firstdecode) = 2 * (ge_real_positive_subtract_first) /\ (ge_real_negative_subtract_first) = 0) \/ exists ge_signed_half_ge_subtract_firstdecode_real. (((ge_real_code_subtract_firstdecode) = 2 * ge_signed_half_ge_subtract_firstdecode_real + 1 /\ (ge_real_positive_subtract_first) = 0) /\ (ge_real_negative_subtract_first) = S ge_signed_half_ge_subtract_firstdecode_real))) /\ ((((ge_imaginary_code_subtract_firstdecode) = 2 * (ge_imaginary_positive_subtract_first) /\ (ge_imaginary_negative_subtract_first) = 0) \/ exists ge_signed_half_ge_subtract_firstdecode_imaginary. (((ge_imaginary_code_subtract_firstdecode) = 2 * ge_signed_half_ge_subtract_firstdecode_imaginary + 1 /\ (ge_imaginary_positive_subtract_first) = 0) /\ (ge_imaginary_negative_subtract_first) = S ge_signed_half_ge_subtract_firstdecode_imaginary))))))) -> (exists ge_real_positive_subtract_second ge_real_negative_subtract_second ge_imaginary_positive_subtract_second ge_imaginary_negative_subtract_second. (exists ge_real_code_subtract_seconddecode ge_imaginary_code_subtract_seconddecode. (((b) = ((ge_real_code_subtract_seconddecode) + (ge_imaginary_code_subtract_seconddecode)) * S ((ge_real_code_subtract_seconddecode) + (ge_imaginary_code_subtract_seconddecode)) + ((ge_imaginary_code_subtract_seconddecode) + (ge_imaginary_code_subtract_seconddecode))) /\ (((((ge_real_code_subtract_seconddecode) = 2 * (ge_real_positive_subtract_second) /\ (ge_real_negative_subtract_second) = 0) \/ exists ge_signed_half_ge_subtract_seconddecode_real. (((ge_real_code_subtract_seconddecode) = 2 * ge_signed_half_ge_subtract_seconddecode_real + 1 /\ (ge_real_positive_subtract_second) = 0) /\ (ge_real_negative_subtract_second) = S ge_signed_half_ge_subtract_seconddecode_real))) /\ ((((ge_imaginary_code_subtract_seconddecode) = 2 * (ge_imaginary_positive_subtract_second) /\ (ge_imaginary_negative_subtract_second) = 0) \/ exists ge_signed_half_ge_subtract_seconddecode_imaginary. (((ge_imaginary_code_subtract_seconddecode) = 2 * ge_signed_half_ge_subtract_seconddecode_imaginary + 1 /\ (ge_imaginary_positive_subtract_second) = 0) /\ (ge_imaginary_negative_subtract_second) = S ge_signed_half_ge_subtract_seconddecode_imaginary))))))) -> exists c. (exists ge_first_rp_subtract_equation ge_first_rn_subtract_equation ge_first_ip_subtract_equation ge_first_in_subtract_equation ge_second_rp_subtract_equation ge_second_rn_subtract_equation ge_second_ip_subtract_equation ge_second_in_subtract_equation. ((exists ge_representation_real_code_subtract_equationfirst ge_representation_imaginary_code_subtract_equationfirst. (((c) = ((ge_representation_real_code_subtract_equationfirst) + (ge_representation_imaginary_code_subtract_equationfirst)) * S ((ge_representation_real_code_subtract_equationfirst) + (ge_representation_imaginary_code_subtract_equationfirst)) + ((ge_representation_imaginary_code_subtract_equationfirst) + (ge_representation_imaginary_code_subtract_equationfirst))) /\ ((exists ge_balance_positive_subtract_equationfirstreal ge_balance_negative_subtract_equationfirstreal. (((((ge_representation_real_code_subtract_equationfirst) = 2 * (ge_balance_positive_subtract_equationfirstreal) /\ (ge_balance_negative_subtract_equationfirstreal) = 0) \/ exists ge_signed_half_subtract_equationfirstrealdecode. (((ge_representation_real_code_subtract_equationfirst) = 2 * ge_signed_half_subtract_equationfirstrealdecode + 1 /\ (ge_balance_positive_subtract_equationfirstreal) = 0) /\ (ge_balance_negative_subtract_equationfirstreal) = S ge_signed_half_subtract_equationfirstrealdecode))) /\ ((ge_first_rp_subtract_equation) + ge_balance_negative_subtract_equationfirstreal = (ge_first_rn_subtract_equation) + ge_balance_positive_subtract_equationfirstreal))) /\ (exists ge_balance_positive_subtract_equationfirstimaginary ge_balance_negative_subtract_equationfirstimaginary. (((((ge_representation_imaginary_code_subtract_equationfirst) = 2 * (ge_balance_positive_subtract_equationfirstimaginary) /\ (ge_balance_negative_subtract_equationfirstimaginary) = 0) \/ exists ge_signed_half_subtract_equationfirstimaginarydecode. (((ge_representation_imaginary_code_subtract_equationfirst) = 2 * ge_signed_half_subtract_equationfirstimaginarydecode + 1 /\ (ge_balance_positive_subtract_equationfirstimaginary) = 0) /\ (ge_balance_negative_subtract_equationfirstimaginary) = S ge_signed_half_subtract_equationfirstimaginarydecode))) /\ ((ge_first_ip_subtract_equation) + ge_balance_negative_subtract_equationfirstimaginary = (ge_first_in_subtract_equation) + ge_balance_positive_subtract_equationfirstimaginary)))))) /\ ((exists ge_representation_real_code_subtract_equationsecond ge_representation_imaginary_code_subtract_equationsecond. (((b) = ((ge_representation_real_code_subtract_equationsecond) + (ge_representation_imaginary_code_subtract_equationsecond)) * S ((ge_representation_real_code_subtract_equationsecond) + (ge_representation_imaginary_code_subtract_equationsecond)) + ((ge_representation_imaginary_code_subtract_equationsecond) + (ge_representation_imaginary_code_subtract_equationsecond))) /\ ((exists ge_balance_positive_subtract_equationsecondreal ge_balance_negative_subtract_equationsecondreal. (((((ge_representation_real_code_subtract_equationsecond) = 2 * (ge_balance_positive_subtract_equationsecondreal) /\ (ge_balance_negative_subtract_equationsecondreal) = 0) \/ exists ge_signed_half_subtract_equationsecondrealdecode. (((ge_representation_real_code_subtract_equationsecond) = 2 * ge_signed_half_subtract_equationsecondrealdecode + 1 /\ (ge_balance_positive_subtract_equationsecondreal) = 0) /\ (ge_balance_negative_subtract_equationsecondreal) = S ge_signed_half_subtract_equationsecondrealdecode))) /\ ((ge_second_rp_subtract_equation) + ge_balance_negative_subtract_equationsecondreal = (ge_second_rn_subtract_equation) + ge_balance_positive_subtract_equationsecondreal))) /\ (exists ge_balance_positive_subtract_equationsecondimaginary ge_balance_negative_subtract_equationsecondimaginary. (((((ge_representation_imaginary_code_subtract_equationsecond) = 2 * (ge_balance_positive_subtract_equationsecondimaginary) /\ (ge_balance_negative_subtract_equationsecondimaginary) = 0) \/ exists ge_signed_half_subtract_equationsecondimaginarydecode. (((ge_representation_imaginary_code_subtract_equationsecond) = 2 * ge_signed_half_subtract_equationsecondimaginarydecode + 1 /\ (ge_balance_positive_subtract_equationsecondimaginary) = 0) /\ (ge_balance_negative_subtract_equationsecondimaginary) = S ge_signed_half_subtract_equationsecondimaginarydecode))) /\ ((ge_second_ip_subtract_equation) + ge_balance_negative_subtract_equationsecondimaginary = (ge_second_in_subtract_equation) + ge_balance_positive_subtract_equationsecondimaginary)))))) /\ (exists ge_representation_real_code_subtract_equationoutput ge_representation_imaginary_code_subtract_equationoutput. (((a) = ((ge_representation_real_code_subtract_equationoutput) + (ge_representation_imaginary_code_subtract_equationoutput)) * S ((ge_representation_real_code_subtract_equationoutput) + (ge_representation_imaginary_code_subtract_equationoutput)) + ((ge_representation_imaginary_code_subtract_equationoutput) + (ge_representation_imaginary_code_subtract_equationoutput))) /\ ((exists ge_balance_positive_subtract_equationoutputreal ge_balance_negative_subtract_equationoutputreal. (((((ge_representation_real_code_subtract_equationoutput) = 2 * (ge_balance_positive_subtract_equationoutputreal) /\ (ge_balance_negative_subtract_equationoutputreal) = 0) \/ exists ge_signed_half_subtract_equationoutputrealdecode. (((ge_representation_real_code_subtract_equationoutput) = 2 * ge_signed_half_subtract_equationoutputrealdecode + 1 /\ (ge_balance_positive_subtract_equationoutputreal) = 0) /\ (ge_balance_negative_subtract_equationoutputreal) = S ge_signed_half_subtract_equationoutputrealdecode))) /\ ((((ge_first_rp_subtract_equation) + (ge_second_rp_subtract_equation))) + ge_balance_negative_subtract_equationoutputreal = (((ge_first_rn_subtract_equation) + (ge_second_rn_subtract_equation))) + ge_balance_positive_subtract_equationoutputreal))) /\ (exists ge_balance_positive_subtract_equationoutputimaginary ge_balance_negative_subtract_equationoutputimaginary. (((((ge_representation_imaginary_code_subtract_equationoutput) = 2 * (ge_balance_positive_subtract_equationoutputimaginary) /\ (ge_balance_negative_subtract_equationoutputimaginary) = 0) \/ exists ge_signed_half_subtract_equationoutputimaginarydecode. (((ge_representation_imaginary_code_subtract_equationoutput) = 2 * ge_signed_half_subtract_equationoutputimaginarydecode + 1 /\ (ge_balance_positive_subtract_equationoutputimaginary) = 0) /\ (ge_balance_negative_subtract_equationoutputimaginary) = S ge_signed_half_subtract_equationoutputimaginarydecode))) /\ ((((ge_first_ip_subtract_equation) + (ge_second_ip_subtract_equation))) + ge_balance_negative_subtract_equationoutputimaginary = (((ge_first_in_subtract_equation) + (ge_second_in_subtract_equation))) + ge_balance_positive_subtract_equationoutputimaginary)))))))))

Constructive proof overview

Generated structural guide

Every actual Gaussian difference has a constructed canonical code solving c+b=a, without assuming a subtraction oracle.

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

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

Proof neighborhood

Direct dependencies

GF0001 gaussian_valid_has_representation gaussian_representation_exists Alpha theorem; checked-use authorized GF0012 gaussian_add_commutative gaussian_add_of_representations Alpha theorem; checked-use authorized gaussian_representation_integer_transport Alpha theorem; checked-use authorized gaussian_equal_symmetric Alpha theorem; checked-use authorized gaussian_difference_reconstructs_dividend Alpha theorem; checked-use authorized

Direct dependents

GF003B gaussian_multiply_cancel_left GF004C gaussian_common_divisor_subtract GF0063 gaussian_bezout_euclidean_backward

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

75 script commands · 13 reading checkpoints · 3 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 (2)
gaussian valid has representationgaussian add commutative

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–4

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro ha
  4. L4
    intro hb
02Establish hAL5–8

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

  1. L5
    have hA : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(a,rp,rn,ip,inn)Definitions: ZPairRep
  2. L6
    specialize gaussian_valid_has_representation (a)
  3. L7
    apply gaussian_valid_has_representation
  4. L8
    exact ha
03Separate the logical casesL9–12

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

  1. L9
    cases hA
  2. L10
    cases hA_witness
  3. L11
    cases hA_witness_witness
  4. L12
    cases hA_witness_witness_witness
04Establish hBL13–16

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

  1. L13
    have hB : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(b,rp,rn,ip,inn)Definitions: ZPairRep
  2. L14
    specialize gaussian_valid_has_representation (b)
  3. L15
    apply gaussian_valid_has_representation
  4. L16
    exact hb
05Separate the logical casesL17–20

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

  1. L17
    cases hB
  2. L18
    cases hB_witness
  3. L19
    cases hB_witness_witness
  4. L20
    cases hB_witness_witness_witness
06Establish hCL21–26

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

  1. L21
    have hC : ∃ c. ZPairRep(c,x + x5,x1 + x4,x2 + x7,x3 + x6)Definitions: ZPairRep
  2. L22
    specialize gaussian_representation_exists (((x) + (x5)))
  3. L23
    specialize gaussian_representation_exists (((x1) + (x4)))
  4. L24
    specialize gaussian_representation_exists (((x2) + (x7)))
  5. L25
    specialize gaussian_representation_exists (((x3) + (x6)))
  6. L26
    apply gaussian_representation_exists
07Separate the logical casesL27–27

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

  1. L27
    cases hC
08Construct an explicit witnessL28–28

Supply the displayed value, then prove that it has the required property.

  1. L28
    exists (x8)
09Use earlier factsL29–38

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

  1. L29
    specialize gaussian_add_commutative (b)
  2. L30
    specialize gaussian_add_commutative (x8)
  3. L31
    specialize gaussian_add_commutative (a)
  4. L32
    apply gaussian_add_commutative
  5. L33
    specialize gaussian_add_of_representations (b)
  6. L34
    specialize gaussian_add_of_representations (x8)
  7. L35
    specialize gaussian_add_of_representations (a)
  8. L36
    specialize gaussian_add_of_representations (x4)
  9. L37
    specialize gaussian_add_of_representations (x5)
  10. L38
    specialize gaussian_add_of_representations (x6)
10Use earlier factsL39–48

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

  1. L39
    specialize gaussian_add_of_representations (x7)
  2. L40
    specialize gaussian_add_of_representations (((x) + (x5)))
  3. L41
    specialize gaussian_add_of_representations (((x1) + (x4)))
  4. L42
    specialize gaussian_add_of_representations (((x2) + (x7)))
  5. L43
    specialize gaussian_add_of_representations (((x3) + (x6)))
  6. L44
    apply gaussian_add_of_representations
  7. L45
    exact hB_witness_witness_witness_witness
  8. L46
    exact hC_witness
  9. L47
    specialize gaussian_representation_integer_transport (a)
  10. L48
    specialize gaussian_representation_integer_transport (x)
11Use earlier factsL49–58

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

  1. L49
    specialize gaussian_representation_integer_transport (x1)
  2. L50
    specialize gaussian_representation_integer_transport (x2)
  3. L51
    specialize gaussian_representation_integer_transport (x3)
  4. L52
    specialize gaussian_representation_integer_transport (((x4) + (((x) + (x5)))))
  5. L53
    specialize gaussian_representation_integer_transport (((x5) + (((x1) + (x4)))))
  6. L54
    specialize gaussian_representation_integer_transport (((x6) + (((x2) + (x7)))))
  7. L55
    specialize gaussian_representation_integer_transport (((x7) + (((x3) + (x6)))))
  8. L56
    apply gaussian_representation_integer_transport
  9. L57
    specialize gaussian_equal_symmetric (((x4) + (((x) + (x5)))))
  10. L58
    specialize gaussian_equal_symmetric (((x5) + (((x1) + (x4)))))
12Use earlier factsL59–68

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

  1. L59
    specialize gaussian_equal_symmetric (((x6) + (((x2) + (x7)))))
  2. L60
    specialize gaussian_equal_symmetric (((x7) + (((x3) + (x6)))))
  3. L61
    specialize gaussian_equal_symmetric (x)
  4. L62
    specialize gaussian_equal_symmetric (x1)
  5. L63
    specialize gaussian_equal_symmetric (x2)
  6. L64
    specialize gaussian_equal_symmetric (x3)
  7. L65
    apply gaussian_equal_symmetric
  8. L66
    specialize gaussian_difference_reconstructs_dividend (x)
  9. L67
    specialize gaussian_difference_reconstructs_dividend (x1)
  10. L68
    specialize gaussian_difference_reconstructs_dividend (x2)
13Use earlier factsL69–75

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

  1. L69
    specialize gaussian_difference_reconstructs_dividend (x3)
  2. L70
    specialize gaussian_difference_reconstructs_dividend (x4)
  3. L71
    specialize gaussian_difference_reconstructs_dividend (x5)
  4. L72
    specialize gaussian_difference_reconstructs_dividend (x6)
  5. L73
    specialize gaussian_difference_reconstructs_dividend (x7)
  6. L74
    apply gaussian_difference_reconstructs_dividend
  7. L75
    exact hA_witness_witness_witness_witness

Library-wide reading audit

Original exact command ledger · 75 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro ha
  4. 0004intro hb
  5. 0005have hA : exists rp rn ip inn. (exists ge_representation_real_code_chosen_hA ge_representation_imaginary_code_chosen_hA. (((a) = ((ge_representation_real_code_chosen_hA) + (ge_representation_imaginary_code_chosen_hA)) * S ((ge_representation_real_code_chosen_hA) + (ge_representation_imaginary_code_chosen_hA)) + ((ge_representation_imaginary_code_chosen_hA) + (ge_representation_imaginary_code_chosen_hA))) /\ ((exists ge_balance_positive_chosen_hAreal ge_balance_negative_chosen_hAreal. (((((ge_representation_real_code_chosen_hA) = 2 * (ge_balance_positive_chosen_hAreal) /\ (ge_balance_negative_chosen_hAreal) = 0) \/ exists ge_signed_half_chosen_hArealdecode. (((ge_representation_real_code_chosen_hA) = 2 * ge_signed_half_chosen_hArealdecode + 1 /\ (ge_balance_positive_chosen_hAreal) = 0) /\ (ge_balance_negative_chosen_hAreal) = S ge_signed_half_chosen_hArealdecode))) /\ ((rp) + ge_balance_negative_chosen_hAreal = (rn) + ge_balance_positive_chosen_hAreal))) /\ (exists ge_balance_positive_chosen_hAimaginary ge_balance_negative_chosen_hAimaginary. (((((ge_representation_imaginary_code_chosen_hA) = 2 * (ge_balance_positive_chosen_hAimaginary) /\ (ge_balance_negative_chosen_hAimaginary) = 0) \/ exists ge_signed_half_chosen_hAimaginarydecode. (((ge_representation_imaginary_code_chosen_hA) = 2 * ge_signed_half_chosen_hAimaginarydecode + 1 /\ (ge_balance_positive_chosen_hAimaginary) = 0) /\ (ge_balance_negative_chosen_hAimaginary) = S ge_signed_half_chosen_hAimaginarydecode))) /\ ((ip) + ge_balance_negative_chosen_hAimaginary = (inn) + ge_balance_positive_chosen_hAimaginary))))))
  6. 0006specialize gaussian_valid_has_representation (a)
  7. 0007apply gaussian_valid_has_representation
  8. 0008exact ha
  9. 0009cases hA
  10. 0010cases hA_witness
  11. 0011cases hA_witness_witness
  12. 0012cases hA_witness_witness_witness
  13. 0013have hB : exists rp rn ip inn. (exists ge_representation_real_code_chosen_hB ge_representation_imaginary_code_chosen_hB. (((b) = ((ge_representation_real_code_chosen_hB) + (ge_representation_imaginary_code_chosen_hB)) * S ((ge_representation_real_code_chosen_hB) + (ge_representation_imaginary_code_chosen_hB)) + ((ge_representation_imaginary_code_chosen_hB) + (ge_representation_imaginary_code_chosen_hB))) /\ ((exists ge_balance_positive_chosen_hBreal ge_balance_negative_chosen_hBreal. (((((ge_representation_real_code_chosen_hB) = 2 * (ge_balance_positive_chosen_hBreal) /\ (ge_balance_negative_chosen_hBreal) = 0) \/ exists ge_signed_half_chosen_hBrealdecode. (((ge_representation_real_code_chosen_hB) = 2 * ge_signed_half_chosen_hBrealdecode + 1 /\ (ge_balance_positive_chosen_hBreal) = 0) /\ (ge_balance_negative_chosen_hBreal) = S ge_signed_half_chosen_hBrealdecode))) /\ ((rp) + ge_balance_negative_chosen_hBreal = (rn) + ge_balance_positive_chosen_hBreal))) /\ (exists ge_balance_positive_chosen_hBimaginary ge_balance_negative_chosen_hBimaginary. (((((ge_representation_imaginary_code_chosen_hB) = 2 * (ge_balance_positive_chosen_hBimaginary) /\ (ge_balance_negative_chosen_hBimaginary) = 0) \/ exists ge_signed_half_chosen_hBimaginarydecode. (((ge_representation_imaginary_code_chosen_hB) = 2 * ge_signed_half_chosen_hBimaginarydecode + 1 /\ (ge_balance_positive_chosen_hBimaginary) = 0) /\ (ge_balance_negative_chosen_hBimaginary) = S ge_signed_half_chosen_hBimaginarydecode))) /\ ((ip) + ge_balance_negative_chosen_hBimaginary = (inn) + ge_balance_positive_chosen_hBimaginary))))))
  14. 0014specialize gaussian_valid_has_representation (b)
  15. 0015apply gaussian_valid_has_representation
  16. 0016exact hb
  17. 0017cases hB
  18. 0018cases hB_witness
  19. 0019cases hB_witness_witness
  20. 0020cases hB_witness_witness_witness
  21. 0021have hC : exists c. (exists ge_representation_real_code_subtract_constructed ge_representation_imaginary_code_subtract_constructed. (((c) = ((ge_representation_real_code_subtract_constructed) + (ge_representation_imaginary_code_subtract_constructed)) * S ((ge_representation_real_code_subtract_constructed) + (ge_representation_imaginary_code_subtract_constructed)) + ((ge_representation_imaginary_code_subtract_constructed) + (ge_representation_imaginary_code_subtract_constructed))) /\ ((exists ge_balance_positive_subtract_constructedreal ge_balance_negative_subtract_constructedreal. (((((ge_representation_real_code_subtract_constructed) = 2 * (ge_balance_positive_subtract_constructedreal) /\ (ge_balance_negative_subtract_constructedreal) = 0) \/ exists ge_signed_half_subtract_constructedrealdecode. (((ge_representation_real_code_subtract_constructed) = 2 * ge_signed_half_subtract_constructedrealdecode + 1 /\ (ge_balance_positive_subtract_constructedreal) = 0) /\ (ge_balance_negative_subtract_constructedreal) = S ge_signed_half_subtract_constructedrealdecode))) /\ ((((x) + (x5))) + ge_balance_negative_subtract_constructedreal = (((x1) + (x4))) + ge_balance_positive_subtract_constructedreal))) /\ (exists ge_balance_positive_subtract_constructedimaginary ge_balance_negative_subtract_constructedimaginary. (((((ge_representation_imaginary_code_subtract_constructed) = 2 * (ge_balance_positive_subtract_constructedimaginary) /\ (ge_balance_negative_subtract_constructedimaginary) = 0) \/ exists ge_signed_half_subtract_constructedimaginarydecode. (((ge_representation_imaginary_code_subtract_constructed) = 2 * ge_signed_half_subtract_constructedimaginarydecode + 1 /\ (ge_balance_positive_subtract_constructedimaginary) = 0) /\ (ge_balance_negative_subtract_constructedimaginary) = S ge_signed_half_subtract_constructedimaginarydecode))) /\ ((((x2) + (x7))) + ge_balance_negative_subtract_constructedimaginary = (((x3) + (x6))) + ge_balance_positive_subtract_constructedimaginary))))))
  22. 0022specialize gaussian_representation_exists (((x) + (x5)))
  23. 0023specialize gaussian_representation_exists (((x1) + (x4)))
  24. 0024specialize gaussian_representation_exists (((x2) + (x7)))
  25. 0025specialize gaussian_representation_exists (((x3) + (x6)))
  26. 0026apply gaussian_representation_exists
  27. 0027cases hC
  28. 0028exists (x8)
  29. 0029specialize gaussian_add_commutative (b)
  30. 0030specialize gaussian_add_commutative (x8)
  31. 0031specialize gaussian_add_commutative (a)
  32. 0032apply gaussian_add_commutative
  33. 0033specialize gaussian_add_of_representations (b)
  34. 0034specialize gaussian_add_of_representations (x8)
  35. 0035specialize gaussian_add_of_representations (a)
  36. 0036specialize gaussian_add_of_representations (x4)
  37. 0037specialize gaussian_add_of_representations (x5)
  38. 0038specialize gaussian_add_of_representations (x6)
  39. 0039specialize gaussian_add_of_representations (x7)
  40. 0040specialize gaussian_add_of_representations (((x) + (x5)))
  41. 0041specialize gaussian_add_of_representations (((x1) + (x4)))
  42. 0042specialize gaussian_add_of_representations (((x2) + (x7)))
  43. 0043specialize gaussian_add_of_representations (((x3) + (x6)))
  44. 0044apply gaussian_add_of_representations
  45. 0045exact hB_witness_witness_witness_witness
  46. 0046exact hC_witness
  47. 0047specialize gaussian_representation_integer_transport (a)
  48. 0048specialize gaussian_representation_integer_transport (x)
  49. 0049specialize gaussian_representation_integer_transport (x1)
  50. 0050specialize gaussian_representation_integer_transport (x2)
  51. 0051specialize gaussian_representation_integer_transport (x3)
  52. 0052specialize gaussian_representation_integer_transport (((x4) + (((x) + (x5)))))
  53. 0053specialize gaussian_representation_integer_transport (((x5) + (((x1) + (x4)))))
  54. 0054specialize gaussian_representation_integer_transport (((x6) + (((x2) + (x7)))))
  55. 0055specialize gaussian_representation_integer_transport (((x7) + (((x3) + (x6)))))
  56. 0056apply gaussian_representation_integer_transport
  57. 0057specialize gaussian_equal_symmetric (((x4) + (((x) + (x5)))))
  58. 0058specialize gaussian_equal_symmetric (((x5) + (((x1) + (x4)))))
  59. 0059specialize gaussian_equal_symmetric (((x6) + (((x2) + (x7)))))
  60. 0060specialize gaussian_equal_symmetric (((x7) + (((x3) + (x6)))))
  61. 0061specialize gaussian_equal_symmetric (x)
  62. 0062specialize gaussian_equal_symmetric (x1)
  63. 0063specialize gaussian_equal_symmetric (x2)
  64. 0064specialize gaussian_equal_symmetric (x3)
  65. 0065apply gaussian_equal_symmetric
  66. 0066specialize gaussian_difference_reconstructs_dividend (x)
  67. 0067specialize gaussian_difference_reconstructs_dividend (x1)
  68. 0068specialize gaussian_difference_reconstructs_dividend (x2)
  69. 0069specialize gaussian_difference_reconstructs_dividend (x3)
  70. 0070specialize gaussian_difference_reconstructs_dividend (x4)
  71. 0071specialize gaussian_difference_reconstructs_dividend (x5)
  72. 0072specialize gaussian_difference_reconstructs_dividend (x6)
  73. 0073specialize gaussian_difference_reconstructs_dividend (x7)
  74. 0074apply gaussian_difference_reconstructs_dividend
  75. 0075exact hA_witness_witness_witness_witness