GF003B

gaussian_multiply_cancel_left

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

A nonzero Gaussian factor cancels, using an actually constructed difference, distributivity and the proved absence of zero divisors.

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 t. ~(a=0) -> (exists ge_first_rp_cancel_product_first ge_first_rn_cancel_product_first ge_first_ip_cancel_product_first ge_first_in_cancel_product_first ge_second_rp_cancel_product_first ge_second_rn_cancel_product_first ge_second_ip_cancel_product_first ge_second_in_cancel_product_first. ((exists ge_representation_real_code_cancel_product_firstfirst ge_representation_imaginary_code_cancel_product_firstfirst. (((a) = ((ge_representation_real_code_cancel_product_firstfirst) + (ge_representation_imaginary_code_cancel_product_firstfirst)) * S ((ge_representation_real_code_cancel_product_firstfirst) + (ge_representation_imaginary_code_cancel_product_firstfirst)) + ((ge_representation_imaginary_code_cancel_product_firstfirst) + (ge_representation_imaginary_code_cancel_product_firstfirst))) /\ ((exists ge_balance_positive_cancel_product_firstfirstreal ge_balance_negative_cancel_product_firstfirstreal. (((((ge_representation_real_code_cancel_product_firstfirst) = 2 * (ge_balance_positive_cancel_product_firstfirstreal) /\ (ge_balance_negative_cancel_product_firstfirstreal) = 0) \/ exists ge_signed_half_cancel_product_firstfirstrealdecode. (((ge_representation_real_code_cancel_product_firstfirst) = 2 * ge_signed_half_cancel_product_firstfirstrealdecode + 1 /\ (ge_balance_positive_cancel_product_firstfirstreal) = 0) /\ (ge_balance_negative_cancel_product_firstfirstreal) = S ge_signed_half_cancel_product_firstfirstrealdecode))) /\ ((ge_first_rp_cancel_product_first) + ge_balance_negative_cancel_product_firstfirstreal = (ge_first_rn_cancel_product_first) + ge_balance_positive_cancel_product_firstfirstreal))) /\ (exists ge_balance_positive_cancel_product_firstfirstimaginary ge_balance_negative_cancel_product_firstfirstimaginary. (((((ge_representation_imaginary_code_cancel_product_firstfirst) = 2 * (ge_balance_positive_cancel_product_firstfirstimaginary) /\ (ge_balance_negative_cancel_product_firstfirstimaginary) = 0) \/ exists ge_signed_half_cancel_product_firstfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_product_firstfirst) = 2 * ge_signed_half_cancel_product_firstfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_product_firstfirstimaginary) = 0) /\ (ge_balance_negative_cancel_product_firstfirstimaginary) = S ge_signed_half_cancel_product_firstfirstimaginarydecode))) /\ ((ge_first_ip_cancel_product_first) + ge_balance_negative_cancel_product_firstfirstimaginary = (ge_first_in_cancel_product_first) + ge_balance_positive_cancel_product_firstfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_product_firstsecond ge_representation_imaginary_code_cancel_product_firstsecond. (((b) = ((ge_representation_real_code_cancel_product_firstsecond) + (ge_representation_imaginary_code_cancel_product_firstsecond)) * S ((ge_representation_real_code_cancel_product_firstsecond) + (ge_representation_imaginary_code_cancel_product_firstsecond)) + ((ge_representation_imaginary_code_cancel_product_firstsecond) + (ge_representation_imaginary_code_cancel_product_firstsecond))) /\ ((exists ge_balance_positive_cancel_product_firstsecondreal ge_balance_negative_cancel_product_firstsecondreal. (((((ge_representation_real_code_cancel_product_firstsecond) = 2 * (ge_balance_positive_cancel_product_firstsecondreal) /\ (ge_balance_negative_cancel_product_firstsecondreal) = 0) \/ exists ge_signed_half_cancel_product_firstsecondrealdecode. (((ge_representation_real_code_cancel_product_firstsecond) = 2 * ge_signed_half_cancel_product_firstsecondrealdecode + 1 /\ (ge_balance_positive_cancel_product_firstsecondreal) = 0) /\ (ge_balance_negative_cancel_product_firstsecondreal) = S ge_signed_half_cancel_product_firstsecondrealdecode))) /\ ((ge_second_rp_cancel_product_first) + ge_balance_negative_cancel_product_firstsecondreal = (ge_second_rn_cancel_product_first) + ge_balance_positive_cancel_product_firstsecondreal))) /\ (exists ge_balance_positive_cancel_product_firstsecondimaginary ge_balance_negative_cancel_product_firstsecondimaginary. (((((ge_representation_imaginary_code_cancel_product_firstsecond) = 2 * (ge_balance_positive_cancel_product_firstsecondimaginary) /\ (ge_balance_negative_cancel_product_firstsecondimaginary) = 0) \/ exists ge_signed_half_cancel_product_firstsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_product_firstsecond) = 2 * ge_signed_half_cancel_product_firstsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_product_firstsecondimaginary) = 0) /\ (ge_balance_negative_cancel_product_firstsecondimaginary) = S ge_signed_half_cancel_product_firstsecondimaginarydecode))) /\ ((ge_second_ip_cancel_product_first) + ge_balance_negative_cancel_product_firstsecondimaginary = (ge_second_in_cancel_product_first) + ge_balance_positive_cancel_product_firstsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_product_firstoutput ge_representation_imaginary_code_cancel_product_firstoutput. (((t) = ((ge_representation_real_code_cancel_product_firstoutput) + (ge_representation_imaginary_code_cancel_product_firstoutput)) * S ((ge_representation_real_code_cancel_product_firstoutput) + (ge_representation_imaginary_code_cancel_product_firstoutput)) + ((ge_representation_imaginary_code_cancel_product_firstoutput) + (ge_representation_imaginary_code_cancel_product_firstoutput))) /\ ((exists ge_balance_positive_cancel_product_firstoutputreal ge_balance_negative_cancel_product_firstoutputreal. (((((ge_representation_real_code_cancel_product_firstoutput) = 2 * (ge_balance_positive_cancel_product_firstoutputreal) /\ (ge_balance_negative_cancel_product_firstoutputreal) = 0) \/ exists ge_signed_half_cancel_product_firstoutputrealdecode. (((ge_representation_real_code_cancel_product_firstoutput) = 2 * ge_signed_half_cancel_product_firstoutputrealdecode + 1 /\ (ge_balance_positive_cancel_product_firstoutputreal) = 0) /\ (ge_balance_negative_cancel_product_firstoutputreal) = S ge_signed_half_cancel_product_firstoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_product_first) * (ge_second_rp_cancel_product_first))) + (((ge_first_rn_cancel_product_first) * (ge_second_rn_cancel_product_first))))) + (((((ge_first_ip_cancel_product_first) * (ge_second_in_cancel_product_first))) + (((ge_first_in_cancel_product_first) * (ge_second_ip_cancel_product_first))))))) + ge_balance_negative_cancel_product_firstoutputreal = (((((((ge_first_rp_cancel_product_first) * (ge_second_rn_cancel_product_first))) + (((ge_first_rn_cancel_product_first) * (ge_second_rp_cancel_product_first))))) + (((((ge_first_ip_cancel_product_first) * (ge_second_ip_cancel_product_first))) + (((ge_first_in_cancel_product_first) * (ge_second_in_cancel_product_first))))))) + ge_balance_positive_cancel_product_firstoutputreal))) /\ (exists ge_balance_positive_cancel_product_firstoutputimaginary ge_balance_negative_cancel_product_firstoutputimaginary. (((((ge_representation_imaginary_code_cancel_product_firstoutput) = 2 * (ge_balance_positive_cancel_product_firstoutputimaginary) /\ (ge_balance_negative_cancel_product_firstoutputimaginary) = 0) \/ exists ge_signed_half_cancel_product_firstoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_product_firstoutput) = 2 * ge_signed_half_cancel_product_firstoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_product_firstoutputimaginary) = 0) /\ (ge_balance_negative_cancel_product_firstoutputimaginary) = S ge_signed_half_cancel_product_firstoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_product_first) * (ge_second_ip_cancel_product_first))) + (((ge_first_rn_cancel_product_first) * (ge_second_in_cancel_product_first))))) + (((((ge_first_ip_cancel_product_first) * (ge_second_rp_cancel_product_first))) + (((ge_first_in_cancel_product_first) * (ge_second_rn_cancel_product_first))))))) + ge_balance_negative_cancel_product_firstoutputimaginary = (((((((ge_first_rp_cancel_product_first) * (ge_second_in_cancel_product_first))) + (((ge_first_rn_cancel_product_first) * (ge_second_ip_cancel_product_first))))) + (((((ge_first_ip_cancel_product_first) * (ge_second_rn_cancel_product_first))) + (((ge_first_in_cancel_product_first) * (ge_second_rp_cancel_product_first))))))) + ge_balance_positive_cancel_product_firstoutputimaginary))))))))) -> (exists ge_first_rp_cancel_product_second ge_first_rn_cancel_product_second ge_first_ip_cancel_product_second ge_first_in_cancel_product_second ge_second_rp_cancel_product_second ge_second_rn_cancel_product_second ge_second_ip_cancel_product_second ge_second_in_cancel_product_second. ((exists ge_representation_real_code_cancel_product_secondfirst ge_representation_imaginary_code_cancel_product_secondfirst. (((a) = ((ge_representation_real_code_cancel_product_secondfirst) + (ge_representation_imaginary_code_cancel_product_secondfirst)) * S ((ge_representation_real_code_cancel_product_secondfirst) + (ge_representation_imaginary_code_cancel_product_secondfirst)) + ((ge_representation_imaginary_code_cancel_product_secondfirst) + (ge_representation_imaginary_code_cancel_product_secondfirst))) /\ ((exists ge_balance_positive_cancel_product_secondfirstreal ge_balance_negative_cancel_product_secondfirstreal. (((((ge_representation_real_code_cancel_product_secondfirst) = 2 * (ge_balance_positive_cancel_product_secondfirstreal) /\ (ge_balance_negative_cancel_product_secondfirstreal) = 0) \/ exists ge_signed_half_cancel_product_secondfirstrealdecode. (((ge_representation_real_code_cancel_product_secondfirst) = 2 * ge_signed_half_cancel_product_secondfirstrealdecode + 1 /\ (ge_balance_positive_cancel_product_secondfirstreal) = 0) /\ (ge_balance_negative_cancel_product_secondfirstreal) = S ge_signed_half_cancel_product_secondfirstrealdecode))) /\ ((ge_first_rp_cancel_product_second) + ge_balance_negative_cancel_product_secondfirstreal = (ge_first_rn_cancel_product_second) + ge_balance_positive_cancel_product_secondfirstreal))) /\ (exists ge_balance_positive_cancel_product_secondfirstimaginary ge_balance_negative_cancel_product_secondfirstimaginary. (((((ge_representation_imaginary_code_cancel_product_secondfirst) = 2 * (ge_balance_positive_cancel_product_secondfirstimaginary) /\ (ge_balance_negative_cancel_product_secondfirstimaginary) = 0) \/ exists ge_signed_half_cancel_product_secondfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_product_secondfirst) = 2 * ge_signed_half_cancel_product_secondfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_product_secondfirstimaginary) = 0) /\ (ge_balance_negative_cancel_product_secondfirstimaginary) = S ge_signed_half_cancel_product_secondfirstimaginarydecode))) /\ ((ge_first_ip_cancel_product_second) + ge_balance_negative_cancel_product_secondfirstimaginary = (ge_first_in_cancel_product_second) + ge_balance_positive_cancel_product_secondfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_product_secondsecond ge_representation_imaginary_code_cancel_product_secondsecond. (((c) = ((ge_representation_real_code_cancel_product_secondsecond) + (ge_representation_imaginary_code_cancel_product_secondsecond)) * S ((ge_representation_real_code_cancel_product_secondsecond) + (ge_representation_imaginary_code_cancel_product_secondsecond)) + ((ge_representation_imaginary_code_cancel_product_secondsecond) + (ge_representation_imaginary_code_cancel_product_secondsecond))) /\ ((exists ge_balance_positive_cancel_product_secondsecondreal ge_balance_negative_cancel_product_secondsecondreal. (((((ge_representation_real_code_cancel_product_secondsecond) = 2 * (ge_balance_positive_cancel_product_secondsecondreal) /\ (ge_balance_negative_cancel_product_secondsecondreal) = 0) \/ exists ge_signed_half_cancel_product_secondsecondrealdecode. (((ge_representation_real_code_cancel_product_secondsecond) = 2 * ge_signed_half_cancel_product_secondsecondrealdecode + 1 /\ (ge_balance_positive_cancel_product_secondsecondreal) = 0) /\ (ge_balance_negative_cancel_product_secondsecondreal) = S ge_signed_half_cancel_product_secondsecondrealdecode))) /\ ((ge_second_rp_cancel_product_second) + ge_balance_negative_cancel_product_secondsecondreal = (ge_second_rn_cancel_product_second) + ge_balance_positive_cancel_product_secondsecondreal))) /\ (exists ge_balance_positive_cancel_product_secondsecondimaginary ge_balance_negative_cancel_product_secondsecondimaginary. (((((ge_representation_imaginary_code_cancel_product_secondsecond) = 2 * (ge_balance_positive_cancel_product_secondsecondimaginary) /\ (ge_balance_negative_cancel_product_secondsecondimaginary) = 0) \/ exists ge_signed_half_cancel_product_secondsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_product_secondsecond) = 2 * ge_signed_half_cancel_product_secondsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_product_secondsecondimaginary) = 0) /\ (ge_balance_negative_cancel_product_secondsecondimaginary) = S ge_signed_half_cancel_product_secondsecondimaginarydecode))) /\ ((ge_second_ip_cancel_product_second) + ge_balance_negative_cancel_product_secondsecondimaginary = (ge_second_in_cancel_product_second) + ge_balance_positive_cancel_product_secondsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_product_secondoutput ge_representation_imaginary_code_cancel_product_secondoutput. (((t) = ((ge_representation_real_code_cancel_product_secondoutput) + (ge_representation_imaginary_code_cancel_product_secondoutput)) * S ((ge_representation_real_code_cancel_product_secondoutput) + (ge_representation_imaginary_code_cancel_product_secondoutput)) + ((ge_representation_imaginary_code_cancel_product_secondoutput) + (ge_representation_imaginary_code_cancel_product_secondoutput))) /\ ((exists ge_balance_positive_cancel_product_secondoutputreal ge_balance_negative_cancel_product_secondoutputreal. (((((ge_representation_real_code_cancel_product_secondoutput) = 2 * (ge_balance_positive_cancel_product_secondoutputreal) /\ (ge_balance_negative_cancel_product_secondoutputreal) = 0) \/ exists ge_signed_half_cancel_product_secondoutputrealdecode. (((ge_representation_real_code_cancel_product_secondoutput) = 2 * ge_signed_half_cancel_product_secondoutputrealdecode + 1 /\ (ge_balance_positive_cancel_product_secondoutputreal) = 0) /\ (ge_balance_negative_cancel_product_secondoutputreal) = S ge_signed_half_cancel_product_secondoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_product_second) * (ge_second_rp_cancel_product_second))) + (((ge_first_rn_cancel_product_second) * (ge_second_rn_cancel_product_second))))) + (((((ge_first_ip_cancel_product_second) * (ge_second_in_cancel_product_second))) + (((ge_first_in_cancel_product_second) * (ge_second_ip_cancel_product_second))))))) + ge_balance_negative_cancel_product_secondoutputreal = (((((((ge_first_rp_cancel_product_second) * (ge_second_rn_cancel_product_second))) + (((ge_first_rn_cancel_product_second) * (ge_second_rp_cancel_product_second))))) + (((((ge_first_ip_cancel_product_second) * (ge_second_ip_cancel_product_second))) + (((ge_first_in_cancel_product_second) * (ge_second_in_cancel_product_second))))))) + ge_balance_positive_cancel_product_secondoutputreal))) /\ (exists ge_balance_positive_cancel_product_secondoutputimaginary ge_balance_negative_cancel_product_secondoutputimaginary. (((((ge_representation_imaginary_code_cancel_product_secondoutput) = 2 * (ge_balance_positive_cancel_product_secondoutputimaginary) /\ (ge_balance_negative_cancel_product_secondoutputimaginary) = 0) \/ exists ge_signed_half_cancel_product_secondoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_product_secondoutput) = 2 * ge_signed_half_cancel_product_secondoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_product_secondoutputimaginary) = 0) /\ (ge_balance_negative_cancel_product_secondoutputimaginary) = S ge_signed_half_cancel_product_secondoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_product_second) * (ge_second_ip_cancel_product_second))) + (((ge_first_rn_cancel_product_second) * (ge_second_in_cancel_product_second))))) + (((((ge_first_ip_cancel_product_second) * (ge_second_rp_cancel_product_second))) + (((ge_first_in_cancel_product_second) * (ge_second_rn_cancel_product_second))))))) + ge_balance_negative_cancel_product_secondoutputimaginary = (((((((ge_first_rp_cancel_product_second) * (ge_second_in_cancel_product_second))) + (((ge_first_rn_cancel_product_second) * (ge_second_ip_cancel_product_second))))) + (((((ge_first_ip_cancel_product_second) * (ge_second_rn_cancel_product_second))) + (((ge_first_in_cancel_product_second) * (ge_second_rp_cancel_product_second))))))) + ge_balance_positive_cancel_product_secondoutputimaginary))))))))) -> b=c

Constructive proof overview

Generated structural guide

A nonzero Gaussian factor cancels, using an actually constructed difference, distributivity and the proved absence of zero divisors.

The unchanged tactic script uses 12 declared prerequisites and contains 93 exact native proof lines.

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

Proof neighborhood

Direct dependencies

GF002C gaussian_subtract_exists GF0007 gaussian_multiply_input_left_valid GF0008 gaussian_multiply_input_right_valid GF0009 gaussian_multiply_output_valid GF0004 gaussian_add_input_left_valid gaussian_multiply_exists Alpha theorem; checked-use authorized GF0038 gaussian_multiply_add_distribute GF0027 gaussian_add_zero_left GF003A gaussian_add_cancel_right GF002F gaussian_multiply_output_transport GF001F gaussian_multiply_zero_implies_zero_factor gaussian_add_functional Alpha theorem; checked-use authorized

Direct dependents

GF003C gaussian_multiply_cancel_right GF005A gaussian_mutual_divisibility_associate GF0068 gaussian_nonzero_product_divisor_unit_cofactor

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

93 script commands · 18 reading checkpoints · 5 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 (10)
gaussian subtract existsgaussian multiply input left validgaussian multiply input right validgaussian multiply output validgaussian add input left validgaussian multiply add distributegaussian add zero leftgaussian add cancel rightgaussian multiply output transportgaussian multiply zero implies zero factor

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

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 t
  5. L5
    intro hn
  6. L6
    intro hB
  7. L7
    intro hC
02Establish hdL8–17

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

  1. L8
    have hd : ∃ d. ZPairAdd(d,c,b)Definitions: ZPairAdd
  2. L9
    specialize gaussian_subtract_exists (b)
  3. L10
    specialize gaussian_subtract_exists (c)
  4. L11
    apply gaussian_subtract_exists
  5. L12
    specialize gaussian_multiply_input_right_valid (a)
  6. L13
    specialize gaussian_multiply_input_right_valid (b)
  7. L14
    specialize gaussian_multiply_input_right_valid (t)
  8. L15
    apply gaussian_multiply_input_right_valid
  9. L16
    exact hB
  10. L17
    specialize gaussian_multiply_input_right_valid (a)
03Use earlier factsL18–21

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

  1. L18
    specialize gaussian_multiply_input_right_valid (c)
  2. L19
    specialize gaussian_multiply_input_right_valid (t)
  3. L20
    apply gaussian_multiply_input_right_valid
  4. L21
    exact hC
04Separate the logical casesL22–22

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

  1. L22
    cases hd
05Establish hproductL23–32

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

  1. L23
    have hproduct : ∃ u. GMul(a,x,u)Definitions: GMul
  2. L24
    specialize gaussian_multiply_exists (a)
  3. L25
    specialize gaussian_multiply_exists (x)
  4. L26
    apply gaussian_multiply_exists
  5. L27
    specialize gaussian_multiply_input_left_valid (a)
  6. L28
    specialize gaussian_multiply_input_left_valid (b)
  7. L29
    specialize gaussian_multiply_input_left_valid (t)
  8. L30
    apply gaussian_multiply_input_left_valid
  9. L31
    exact hB
  10. L32
    specialize gaussian_add_input_left_valid (x)
06Use earlier factsL33–36

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

  1. L33
    specialize gaussian_add_input_left_valid (c)
  2. L34
    specialize gaussian_add_input_left_valid (b)
  3. L35
    apply gaussian_add_input_left_valid
  4. L36
    exact hd_witness
07Separate the logical casesL37–37

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

  1. L37
    cases hproduct
08Establish hsumL38–47

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

  1. L38
    have hsum : ZPairAdd(x1,t,t)Definitions: ZPairAdd
  2. L39
    specialize gaussian_multiply_add_distribute (a)
  3. L40
    specialize gaussian_multiply_add_distribute (x)
  4. L41
    specialize gaussian_multiply_add_distribute (c)
  5. L42
    specialize gaussian_multiply_add_distribute (b)
  6. L43
    specialize gaussian_multiply_add_distribute (x1)
  7. L44
    specialize gaussian_multiply_add_distribute (t)
  8. L45
    specialize gaussian_multiply_add_distribute (t)
  9. L46
    apply gaussian_multiply_add_distribute
  10. L47
    exact hd_witness
09Use earlier factsL48–50

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

  1. L48
    exact hproduct_witness
  2. L49
    exact hC
  3. L50
    exact hB
10Establish hzeroL51–60

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

  1. L51
    have hzero : x1=0
  2. L52
    specialize gaussian_add_cancel_right (x1)
  3. L53
    specialize gaussian_add_cancel_right (0)
  4. L54
    specialize gaussian_add_cancel_right (t)
  5. L55
    specialize gaussian_add_cancel_right (t)
  6. L56
    apply gaussian_add_cancel_right
  7. L57
    exact hsum
  8. L58
    specialize gaussian_add_zero_left (t)
  9. L59
    apply gaussian_add_zero_left
  10. L60
    specialize gaussian_multiply_output_valid (a)
11Use earlier factsL61–64

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

  1. L61
    specialize gaussian_multiply_output_valid (b)
  2. L62
    specialize gaussian_multiply_output_valid (t)
  3. L63
    apply gaussian_multiply_output_valid
  4. L64
    exact hB
12Establish hcasesL65–74

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian multiply zero implies zero factor.

  1. L65
    have hcases : a=0 \/ x=0
  2. L66
    specialize gaussian_multiply_zero_implies_zero_factor (a)
  3. L67
    specialize gaussian_multiply_zero_implies_zero_factor (x)
  4. L68
    apply gaussian_multiply_zero_implies_zero_factor
  5. L69
    specialize gaussian_multiply_output_transport (a)
  6. L70
    specialize gaussian_multiply_output_transport (x)
  7. L71
    specialize gaussian_multiply_output_transport (x1)
  8. L72
    specialize gaussian_multiply_output_transport (0)
  9. L73
    apply gaussian_multiply_output_transport
  10. L74
    exact hzero
13Use earlier factsL75–75

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

  1. L75
    exact hproduct_witness
14Separate the logical casesL76–77

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

  1. L76
    cases hcases
  2. L77
    exfalso
15Use earlier factsL78–79

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

  1. L78
    apply hn
  2. L79
    exact hcases_left
16Calculate and transport equalitiesL80–80

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

  1. L80
    rewrite hcases_right at hd_witness
17Use earlier factsL81–90

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

  1. L81
    specialize gaussian_add_functional (0)
  2. L82
    specialize gaussian_add_functional (c)
  3. L83
    specialize gaussian_add_functional (b)
  4. L84
    specialize gaussian_add_functional (c)
  5. L85
    apply gaussian_add_functional
  6. L86
    exact hd_witness
  7. L87
    specialize gaussian_add_zero_left (c)
  8. L88
    apply gaussian_add_zero_left
  9. L89
    specialize gaussian_multiply_input_right_valid (a)
  10. L90
    specialize gaussian_multiply_input_right_valid (c)
18Use earlier factsL91–93

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

  1. L91
    specialize gaussian_multiply_input_right_valid (t)
  2. L92
    apply gaussian_multiply_input_right_valid
  3. L93
    exact hC

Library-wide reading audit

Original exact command ledger · 93 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro t
  5. 0005intro hn
  6. 0006intro hB
  7. 0007intro hC
  8. 0008have hd : exists d. (exists ge_first_rp_cancel_product_difference ge_first_rn_cancel_product_difference ge_first_ip_cancel_product_difference ge_first_in_cancel_product_difference ge_second_rp_cancel_product_difference ge_second_rn_cancel_product_difference ge_second_ip_cancel_product_difference ge_second_in_cancel_product_difference. ((exists ge_representation_real_code_cancel_product_differencefirst ge_representation_imaginary_code_cancel_product_differencefirst. (((d) = ((ge_representation_real_code_cancel_product_differencefirst) + (ge_representation_imaginary_code_cancel_product_differencefirst)) * S ((ge_representation_real_code_cancel_product_differencefirst) + (ge_representation_imaginary_code_cancel_product_differencefirst)) + ((ge_representation_imaginary_code_cancel_product_differencefirst) + (ge_representation_imaginary_code_cancel_product_differencefirst))) /\ ((exists ge_balance_positive_cancel_product_differencefirstreal ge_balance_negative_cancel_product_differencefirstreal. (((((ge_representation_real_code_cancel_product_differencefirst) = 2 * (ge_balance_positive_cancel_product_differencefirstreal) /\ (ge_balance_negative_cancel_product_differencefirstreal) = 0) \/ exists ge_signed_half_cancel_product_differencefirstrealdecode. (((ge_representation_real_code_cancel_product_differencefirst) = 2 * ge_signed_half_cancel_product_differencefirstrealdecode + 1 /\ (ge_balance_positive_cancel_product_differencefirstreal) = 0) /\ (ge_balance_negative_cancel_product_differencefirstreal) = S ge_signed_half_cancel_product_differencefirstrealdecode))) /\ ((ge_first_rp_cancel_product_difference) + ge_balance_negative_cancel_product_differencefirstreal = (ge_first_rn_cancel_product_difference) + ge_balance_positive_cancel_product_differencefirstreal))) /\ (exists ge_balance_positive_cancel_product_differencefirstimaginary ge_balance_negative_cancel_product_differencefirstimaginary. (((((ge_representation_imaginary_code_cancel_product_differencefirst) = 2 * (ge_balance_positive_cancel_product_differencefirstimaginary) /\ (ge_balance_negative_cancel_product_differencefirstimaginary) = 0) \/ exists ge_signed_half_cancel_product_differencefirstimaginarydecode. (((ge_representation_imaginary_code_cancel_product_differencefirst) = 2 * ge_signed_half_cancel_product_differencefirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_product_differencefirstimaginary) = 0) /\ (ge_balance_negative_cancel_product_differencefirstimaginary) = S ge_signed_half_cancel_product_differencefirstimaginarydecode))) /\ ((ge_first_ip_cancel_product_difference) + ge_balance_negative_cancel_product_differencefirstimaginary = (ge_first_in_cancel_product_difference) + ge_balance_positive_cancel_product_differencefirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_product_differencesecond ge_representation_imaginary_code_cancel_product_differencesecond. (((c) = ((ge_representation_real_code_cancel_product_differencesecond) + (ge_representation_imaginary_code_cancel_product_differencesecond)) * S ((ge_representation_real_code_cancel_product_differencesecond) + (ge_representation_imaginary_code_cancel_product_differencesecond)) + ((ge_representation_imaginary_code_cancel_product_differencesecond) + (ge_representation_imaginary_code_cancel_product_differencesecond))) /\ ((exists ge_balance_positive_cancel_product_differencesecondreal ge_balance_negative_cancel_product_differencesecondreal. (((((ge_representation_real_code_cancel_product_differencesecond) = 2 * (ge_balance_positive_cancel_product_differencesecondreal) /\ (ge_balance_negative_cancel_product_differencesecondreal) = 0) \/ exists ge_signed_half_cancel_product_differencesecondrealdecode. (((ge_representation_real_code_cancel_product_differencesecond) = 2 * ge_signed_half_cancel_product_differencesecondrealdecode + 1 /\ (ge_balance_positive_cancel_product_differencesecondreal) = 0) /\ (ge_balance_negative_cancel_product_differencesecondreal) = S ge_signed_half_cancel_product_differencesecondrealdecode))) /\ ((ge_second_rp_cancel_product_difference) + ge_balance_negative_cancel_product_differencesecondreal = (ge_second_rn_cancel_product_difference) + ge_balance_positive_cancel_product_differencesecondreal))) /\ (exists ge_balance_positive_cancel_product_differencesecondimaginary ge_balance_negative_cancel_product_differencesecondimaginary. (((((ge_representation_imaginary_code_cancel_product_differencesecond) = 2 * (ge_balance_positive_cancel_product_differencesecondimaginary) /\ (ge_balance_negative_cancel_product_differencesecondimaginary) = 0) \/ exists ge_signed_half_cancel_product_differencesecondimaginarydecode. (((ge_representation_imaginary_code_cancel_product_differencesecond) = 2 * ge_signed_half_cancel_product_differencesecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_product_differencesecondimaginary) = 0) /\ (ge_balance_negative_cancel_product_differencesecondimaginary) = S ge_signed_half_cancel_product_differencesecondimaginarydecode))) /\ ((ge_second_ip_cancel_product_difference) + ge_balance_negative_cancel_product_differencesecondimaginary = (ge_second_in_cancel_product_difference) + ge_balance_positive_cancel_product_differencesecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_product_differenceoutput ge_representation_imaginary_code_cancel_product_differenceoutput. (((b) = ((ge_representation_real_code_cancel_product_differenceoutput) + (ge_representation_imaginary_code_cancel_product_differenceoutput)) * S ((ge_representation_real_code_cancel_product_differenceoutput) + (ge_representation_imaginary_code_cancel_product_differenceoutput)) + ((ge_representation_imaginary_code_cancel_product_differenceoutput) + (ge_representation_imaginary_code_cancel_product_differenceoutput))) /\ ((exists ge_balance_positive_cancel_product_differenceoutputreal ge_balance_negative_cancel_product_differenceoutputreal. (((((ge_representation_real_code_cancel_product_differenceoutput) = 2 * (ge_balance_positive_cancel_product_differenceoutputreal) /\ (ge_balance_negative_cancel_product_differenceoutputreal) = 0) \/ exists ge_signed_half_cancel_product_differenceoutputrealdecode. (((ge_representation_real_code_cancel_product_differenceoutput) = 2 * ge_signed_half_cancel_product_differenceoutputrealdecode + 1 /\ (ge_balance_positive_cancel_product_differenceoutputreal) = 0) /\ (ge_balance_negative_cancel_product_differenceoutputreal) = S ge_signed_half_cancel_product_differenceoutputrealdecode))) /\ ((((ge_first_rp_cancel_product_difference) + (ge_second_rp_cancel_product_difference))) + ge_balance_negative_cancel_product_differenceoutputreal = (((ge_first_rn_cancel_product_difference) + (ge_second_rn_cancel_product_difference))) + ge_balance_positive_cancel_product_differenceoutputreal))) /\ (exists ge_balance_positive_cancel_product_differenceoutputimaginary ge_balance_negative_cancel_product_differenceoutputimaginary. (((((ge_representation_imaginary_code_cancel_product_differenceoutput) = 2 * (ge_balance_positive_cancel_product_differenceoutputimaginary) /\ (ge_balance_negative_cancel_product_differenceoutputimaginary) = 0) \/ exists ge_signed_half_cancel_product_differenceoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_product_differenceoutput) = 2 * ge_signed_half_cancel_product_differenceoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_product_differenceoutputimaginary) = 0) /\ (ge_balance_negative_cancel_product_differenceoutputimaginary) = S ge_signed_half_cancel_product_differenceoutputimaginarydecode))) /\ ((((ge_first_ip_cancel_product_difference) + (ge_second_ip_cancel_product_difference))) + ge_balance_negative_cancel_product_differenceoutputimaginary = (((ge_first_in_cancel_product_difference) + (ge_second_in_cancel_product_difference))) + ge_balance_positive_cancel_product_differenceoutputimaginary)))))))))
  9. 0009specialize gaussian_subtract_exists (b)
  10. 0010specialize gaussian_subtract_exists (c)
  11. 0011apply gaussian_subtract_exists
  12. 0012specialize gaussian_multiply_input_right_valid (a)
  13. 0013specialize gaussian_multiply_input_right_valid (b)
  14. 0014specialize gaussian_multiply_input_right_valid (t)
  15. 0015apply gaussian_multiply_input_right_valid
  16. 0016exact hB
  17. 0017specialize gaussian_multiply_input_right_valid (a)
  18. 0018specialize gaussian_multiply_input_right_valid (c)
  19. 0019specialize gaussian_multiply_input_right_valid (t)
  20. 0020apply gaussian_multiply_input_right_valid
  21. 0021exact hC
  22. 0022cases hd
  23. 0023have hproduct : exists u. (exists ge_first_rp_cancel_product_construct ge_first_rn_cancel_product_construct ge_first_ip_cancel_product_construct ge_first_in_cancel_product_construct ge_second_rp_cancel_product_construct ge_second_rn_cancel_product_construct ge_second_ip_cancel_product_construct ge_second_in_cancel_product_construct. ((exists ge_representation_real_code_cancel_product_constructfirst ge_representation_imaginary_code_cancel_product_constructfirst. (((a) = ((ge_representation_real_code_cancel_product_constructfirst) + (ge_representation_imaginary_code_cancel_product_constructfirst)) * S ((ge_representation_real_code_cancel_product_constructfirst) + (ge_representation_imaginary_code_cancel_product_constructfirst)) + ((ge_representation_imaginary_code_cancel_product_constructfirst) + (ge_representation_imaginary_code_cancel_product_constructfirst))) /\ ((exists ge_balance_positive_cancel_product_constructfirstreal ge_balance_negative_cancel_product_constructfirstreal. (((((ge_representation_real_code_cancel_product_constructfirst) = 2 * (ge_balance_positive_cancel_product_constructfirstreal) /\ (ge_balance_negative_cancel_product_constructfirstreal) = 0) \/ exists ge_signed_half_cancel_product_constructfirstrealdecode. (((ge_representation_real_code_cancel_product_constructfirst) = 2 * ge_signed_half_cancel_product_constructfirstrealdecode + 1 /\ (ge_balance_positive_cancel_product_constructfirstreal) = 0) /\ (ge_balance_negative_cancel_product_constructfirstreal) = S ge_signed_half_cancel_product_constructfirstrealdecode))) /\ ((ge_first_rp_cancel_product_construct) + ge_balance_negative_cancel_product_constructfirstreal = (ge_first_rn_cancel_product_construct) + ge_balance_positive_cancel_product_constructfirstreal))) /\ (exists ge_balance_positive_cancel_product_constructfirstimaginary ge_balance_negative_cancel_product_constructfirstimaginary. (((((ge_representation_imaginary_code_cancel_product_constructfirst) = 2 * (ge_balance_positive_cancel_product_constructfirstimaginary) /\ (ge_balance_negative_cancel_product_constructfirstimaginary) = 0) \/ exists ge_signed_half_cancel_product_constructfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_product_constructfirst) = 2 * ge_signed_half_cancel_product_constructfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_product_constructfirstimaginary) = 0) /\ (ge_balance_negative_cancel_product_constructfirstimaginary) = S ge_signed_half_cancel_product_constructfirstimaginarydecode))) /\ ((ge_first_ip_cancel_product_construct) + ge_balance_negative_cancel_product_constructfirstimaginary = (ge_first_in_cancel_product_construct) + ge_balance_positive_cancel_product_constructfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_product_constructsecond ge_representation_imaginary_code_cancel_product_constructsecond. (((x) = ((ge_representation_real_code_cancel_product_constructsecond) + (ge_representation_imaginary_code_cancel_product_constructsecond)) * S ((ge_representation_real_code_cancel_product_constructsecond) + (ge_representation_imaginary_code_cancel_product_constructsecond)) + ((ge_representation_imaginary_code_cancel_product_constructsecond) + (ge_representation_imaginary_code_cancel_product_constructsecond))) /\ ((exists ge_balance_positive_cancel_product_constructsecondreal ge_balance_negative_cancel_product_constructsecondreal. (((((ge_representation_real_code_cancel_product_constructsecond) = 2 * (ge_balance_positive_cancel_product_constructsecondreal) /\ (ge_balance_negative_cancel_product_constructsecondreal) = 0) \/ exists ge_signed_half_cancel_product_constructsecondrealdecode. (((ge_representation_real_code_cancel_product_constructsecond) = 2 * ge_signed_half_cancel_product_constructsecondrealdecode + 1 /\ (ge_balance_positive_cancel_product_constructsecondreal) = 0) /\ (ge_balance_negative_cancel_product_constructsecondreal) = S ge_signed_half_cancel_product_constructsecondrealdecode))) /\ ((ge_second_rp_cancel_product_construct) + ge_balance_negative_cancel_product_constructsecondreal = (ge_second_rn_cancel_product_construct) + ge_balance_positive_cancel_product_constructsecondreal))) /\ (exists ge_balance_positive_cancel_product_constructsecondimaginary ge_balance_negative_cancel_product_constructsecondimaginary. (((((ge_representation_imaginary_code_cancel_product_constructsecond) = 2 * (ge_balance_positive_cancel_product_constructsecondimaginary) /\ (ge_balance_negative_cancel_product_constructsecondimaginary) = 0) \/ exists ge_signed_half_cancel_product_constructsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_product_constructsecond) = 2 * ge_signed_half_cancel_product_constructsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_product_constructsecondimaginary) = 0) /\ (ge_balance_negative_cancel_product_constructsecondimaginary) = S ge_signed_half_cancel_product_constructsecondimaginarydecode))) /\ ((ge_second_ip_cancel_product_construct) + ge_balance_negative_cancel_product_constructsecondimaginary = (ge_second_in_cancel_product_construct) + ge_balance_positive_cancel_product_constructsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_product_constructoutput ge_representation_imaginary_code_cancel_product_constructoutput. (((u) = ((ge_representation_real_code_cancel_product_constructoutput) + (ge_representation_imaginary_code_cancel_product_constructoutput)) * S ((ge_representation_real_code_cancel_product_constructoutput) + (ge_representation_imaginary_code_cancel_product_constructoutput)) + ((ge_representation_imaginary_code_cancel_product_constructoutput) + (ge_representation_imaginary_code_cancel_product_constructoutput))) /\ ((exists ge_balance_positive_cancel_product_constructoutputreal ge_balance_negative_cancel_product_constructoutputreal. (((((ge_representation_real_code_cancel_product_constructoutput) = 2 * (ge_balance_positive_cancel_product_constructoutputreal) /\ (ge_balance_negative_cancel_product_constructoutputreal) = 0) \/ exists ge_signed_half_cancel_product_constructoutputrealdecode. (((ge_representation_real_code_cancel_product_constructoutput) = 2 * ge_signed_half_cancel_product_constructoutputrealdecode + 1 /\ (ge_balance_positive_cancel_product_constructoutputreal) = 0) /\ (ge_balance_negative_cancel_product_constructoutputreal) = S ge_signed_half_cancel_product_constructoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_product_construct) * (ge_second_rp_cancel_product_construct))) + (((ge_first_rn_cancel_product_construct) * (ge_second_rn_cancel_product_construct))))) + (((((ge_first_ip_cancel_product_construct) * (ge_second_in_cancel_product_construct))) + (((ge_first_in_cancel_product_construct) * (ge_second_ip_cancel_product_construct))))))) + ge_balance_negative_cancel_product_constructoutputreal = (((((((ge_first_rp_cancel_product_construct) * (ge_second_rn_cancel_product_construct))) + (((ge_first_rn_cancel_product_construct) * (ge_second_rp_cancel_product_construct))))) + (((((ge_first_ip_cancel_product_construct) * (ge_second_ip_cancel_product_construct))) + (((ge_first_in_cancel_product_construct) * (ge_second_in_cancel_product_construct))))))) + ge_balance_positive_cancel_product_constructoutputreal))) /\ (exists ge_balance_positive_cancel_product_constructoutputimaginary ge_balance_negative_cancel_product_constructoutputimaginary. (((((ge_representation_imaginary_code_cancel_product_constructoutput) = 2 * (ge_balance_positive_cancel_product_constructoutputimaginary) /\ (ge_balance_negative_cancel_product_constructoutputimaginary) = 0) \/ exists ge_signed_half_cancel_product_constructoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_product_constructoutput) = 2 * ge_signed_half_cancel_product_constructoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_product_constructoutputimaginary) = 0) /\ (ge_balance_negative_cancel_product_constructoutputimaginary) = S ge_signed_half_cancel_product_constructoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_product_construct) * (ge_second_ip_cancel_product_construct))) + (((ge_first_rn_cancel_product_construct) * (ge_second_in_cancel_product_construct))))) + (((((ge_first_ip_cancel_product_construct) * (ge_second_rp_cancel_product_construct))) + (((ge_first_in_cancel_product_construct) * (ge_second_rn_cancel_product_construct))))))) + ge_balance_negative_cancel_product_constructoutputimaginary = (((((((ge_first_rp_cancel_product_construct) * (ge_second_in_cancel_product_construct))) + (((ge_first_rn_cancel_product_construct) * (ge_second_ip_cancel_product_construct))))) + (((((ge_first_ip_cancel_product_construct) * (ge_second_rn_cancel_product_construct))) + (((ge_first_in_cancel_product_construct) * (ge_second_rp_cancel_product_construct))))))) + ge_balance_positive_cancel_product_constructoutputimaginary)))))))))
  24. 0024specialize gaussian_multiply_exists (a)
  25. 0025specialize gaussian_multiply_exists (x)
  26. 0026apply gaussian_multiply_exists
  27. 0027specialize gaussian_multiply_input_left_valid (a)
  28. 0028specialize gaussian_multiply_input_left_valid (b)
  29. 0029specialize gaussian_multiply_input_left_valid (t)
  30. 0030apply gaussian_multiply_input_left_valid
  31. 0031exact hB
  32. 0032specialize gaussian_add_input_left_valid (x)
  33. 0033specialize gaussian_add_input_left_valid (c)
  34. 0034specialize gaussian_add_input_left_valid (b)
  35. 0035apply gaussian_add_input_left_valid
  36. 0036exact hd_witness
  37. 0037cases hproduct
  38. 0038have hsum : exists ge_first_rp_cancel_product_sum ge_first_rn_cancel_product_sum ge_first_ip_cancel_product_sum ge_first_in_cancel_product_sum ge_second_rp_cancel_product_sum ge_second_rn_cancel_product_sum ge_second_ip_cancel_product_sum ge_second_in_cancel_product_sum. ((exists ge_representation_real_code_cancel_product_sumfirst ge_representation_imaginary_code_cancel_product_sumfirst. (((x1) = ((ge_representation_real_code_cancel_product_sumfirst) + (ge_representation_imaginary_code_cancel_product_sumfirst)) * S ((ge_representation_real_code_cancel_product_sumfirst) + (ge_representation_imaginary_code_cancel_product_sumfirst)) + ((ge_representation_imaginary_code_cancel_product_sumfirst) + (ge_representation_imaginary_code_cancel_product_sumfirst))) /\ ((exists ge_balance_positive_cancel_product_sumfirstreal ge_balance_negative_cancel_product_sumfirstreal. (((((ge_representation_real_code_cancel_product_sumfirst) = 2 * (ge_balance_positive_cancel_product_sumfirstreal) /\ (ge_balance_negative_cancel_product_sumfirstreal) = 0) \/ exists ge_signed_half_cancel_product_sumfirstrealdecode. (((ge_representation_real_code_cancel_product_sumfirst) = 2 * ge_signed_half_cancel_product_sumfirstrealdecode + 1 /\ (ge_balance_positive_cancel_product_sumfirstreal) = 0) /\ (ge_balance_negative_cancel_product_sumfirstreal) = S ge_signed_half_cancel_product_sumfirstrealdecode))) /\ ((ge_first_rp_cancel_product_sum) + ge_balance_negative_cancel_product_sumfirstreal = (ge_first_rn_cancel_product_sum) + ge_balance_positive_cancel_product_sumfirstreal))) /\ (exists ge_balance_positive_cancel_product_sumfirstimaginary ge_balance_negative_cancel_product_sumfirstimaginary. (((((ge_representation_imaginary_code_cancel_product_sumfirst) = 2 * (ge_balance_positive_cancel_product_sumfirstimaginary) /\ (ge_balance_negative_cancel_product_sumfirstimaginary) = 0) \/ exists ge_signed_half_cancel_product_sumfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_product_sumfirst) = 2 * ge_signed_half_cancel_product_sumfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_product_sumfirstimaginary) = 0) /\ (ge_balance_negative_cancel_product_sumfirstimaginary) = S ge_signed_half_cancel_product_sumfirstimaginarydecode))) /\ ((ge_first_ip_cancel_product_sum) + ge_balance_negative_cancel_product_sumfirstimaginary = (ge_first_in_cancel_product_sum) + ge_balance_positive_cancel_product_sumfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_product_sumsecond ge_representation_imaginary_code_cancel_product_sumsecond. (((t) = ((ge_representation_real_code_cancel_product_sumsecond) + (ge_representation_imaginary_code_cancel_product_sumsecond)) * S ((ge_representation_real_code_cancel_product_sumsecond) + (ge_representation_imaginary_code_cancel_product_sumsecond)) + ((ge_representation_imaginary_code_cancel_product_sumsecond) + (ge_representation_imaginary_code_cancel_product_sumsecond))) /\ ((exists ge_balance_positive_cancel_product_sumsecondreal ge_balance_negative_cancel_product_sumsecondreal. (((((ge_representation_real_code_cancel_product_sumsecond) = 2 * (ge_balance_positive_cancel_product_sumsecondreal) /\ (ge_balance_negative_cancel_product_sumsecondreal) = 0) \/ exists ge_signed_half_cancel_product_sumsecondrealdecode. (((ge_representation_real_code_cancel_product_sumsecond) = 2 * ge_signed_half_cancel_product_sumsecondrealdecode + 1 /\ (ge_balance_positive_cancel_product_sumsecondreal) = 0) /\ (ge_balance_negative_cancel_product_sumsecondreal) = S ge_signed_half_cancel_product_sumsecondrealdecode))) /\ ((ge_second_rp_cancel_product_sum) + ge_balance_negative_cancel_product_sumsecondreal = (ge_second_rn_cancel_product_sum) + ge_balance_positive_cancel_product_sumsecondreal))) /\ (exists ge_balance_positive_cancel_product_sumsecondimaginary ge_balance_negative_cancel_product_sumsecondimaginary. (((((ge_representation_imaginary_code_cancel_product_sumsecond) = 2 * (ge_balance_positive_cancel_product_sumsecondimaginary) /\ (ge_balance_negative_cancel_product_sumsecondimaginary) = 0) \/ exists ge_signed_half_cancel_product_sumsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_product_sumsecond) = 2 * ge_signed_half_cancel_product_sumsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_product_sumsecondimaginary) = 0) /\ (ge_balance_negative_cancel_product_sumsecondimaginary) = S ge_signed_half_cancel_product_sumsecondimaginarydecode))) /\ ((ge_second_ip_cancel_product_sum) + ge_balance_negative_cancel_product_sumsecondimaginary = (ge_second_in_cancel_product_sum) + ge_balance_positive_cancel_product_sumsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_product_sumoutput ge_representation_imaginary_code_cancel_product_sumoutput. (((t) = ((ge_representation_real_code_cancel_product_sumoutput) + (ge_representation_imaginary_code_cancel_product_sumoutput)) * S ((ge_representation_real_code_cancel_product_sumoutput) + (ge_representation_imaginary_code_cancel_product_sumoutput)) + ((ge_representation_imaginary_code_cancel_product_sumoutput) + (ge_representation_imaginary_code_cancel_product_sumoutput))) /\ ((exists ge_balance_positive_cancel_product_sumoutputreal ge_balance_negative_cancel_product_sumoutputreal. (((((ge_representation_real_code_cancel_product_sumoutput) = 2 * (ge_balance_positive_cancel_product_sumoutputreal) /\ (ge_balance_negative_cancel_product_sumoutputreal) = 0) \/ exists ge_signed_half_cancel_product_sumoutputrealdecode. (((ge_representation_real_code_cancel_product_sumoutput) = 2 * ge_signed_half_cancel_product_sumoutputrealdecode + 1 /\ (ge_balance_positive_cancel_product_sumoutputreal) = 0) /\ (ge_balance_negative_cancel_product_sumoutputreal) = S ge_signed_half_cancel_product_sumoutputrealdecode))) /\ ((((ge_first_rp_cancel_product_sum) + (ge_second_rp_cancel_product_sum))) + ge_balance_negative_cancel_product_sumoutputreal = (((ge_first_rn_cancel_product_sum) + (ge_second_rn_cancel_product_sum))) + ge_balance_positive_cancel_product_sumoutputreal))) /\ (exists ge_balance_positive_cancel_product_sumoutputimaginary ge_balance_negative_cancel_product_sumoutputimaginary. (((((ge_representation_imaginary_code_cancel_product_sumoutput) = 2 * (ge_balance_positive_cancel_product_sumoutputimaginary) /\ (ge_balance_negative_cancel_product_sumoutputimaginary) = 0) \/ exists ge_signed_half_cancel_product_sumoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_product_sumoutput) = 2 * ge_signed_half_cancel_product_sumoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_product_sumoutputimaginary) = 0) /\ (ge_balance_negative_cancel_product_sumoutputimaginary) = S ge_signed_half_cancel_product_sumoutputimaginarydecode))) /\ ((((ge_first_ip_cancel_product_sum) + (ge_second_ip_cancel_product_sum))) + ge_balance_negative_cancel_product_sumoutputimaginary = (((ge_first_in_cancel_product_sum) + (ge_second_in_cancel_product_sum))) + ge_balance_positive_cancel_product_sumoutputimaginary))))))))
  39. 0039specialize gaussian_multiply_add_distribute (a)
  40. 0040specialize gaussian_multiply_add_distribute (x)
  41. 0041specialize gaussian_multiply_add_distribute (c)
  42. 0042specialize gaussian_multiply_add_distribute (b)
  43. 0043specialize gaussian_multiply_add_distribute (x1)
  44. 0044specialize gaussian_multiply_add_distribute (t)
  45. 0045specialize gaussian_multiply_add_distribute (t)
  46. 0046apply gaussian_multiply_add_distribute
  47. 0047exact hd_witness
  48. 0048exact hproduct_witness
  49. 0049exact hC
  50. 0050exact hB
  51. 0051have hzero : x1=0
  52. 0052specialize gaussian_add_cancel_right (x1)
  53. 0053specialize gaussian_add_cancel_right (0)
  54. 0054specialize gaussian_add_cancel_right (t)
  55. 0055specialize gaussian_add_cancel_right (t)
  56. 0056apply gaussian_add_cancel_right
  57. 0057exact hsum
  58. 0058specialize gaussian_add_zero_left (t)
  59. 0059apply gaussian_add_zero_left
  60. 0060specialize gaussian_multiply_output_valid (a)
  61. 0061specialize gaussian_multiply_output_valid (b)
  62. 0062specialize gaussian_multiply_output_valid (t)
  63. 0063apply gaussian_multiply_output_valid
  64. 0064exact hB
  65. 0065have hcases : a=0 \/ x=0
  66. 0066specialize gaussian_multiply_zero_implies_zero_factor (a)
  67. 0067specialize gaussian_multiply_zero_implies_zero_factor (x)
  68. 0068apply gaussian_multiply_zero_implies_zero_factor
  69. 0069specialize gaussian_multiply_output_transport (a)
  70. 0070specialize gaussian_multiply_output_transport (x)
  71. 0071specialize gaussian_multiply_output_transport (x1)
  72. 0072specialize gaussian_multiply_output_transport (0)
  73. 0073apply gaussian_multiply_output_transport
  74. 0074exact hzero
  75. 0075exact hproduct_witness
  76. 0076cases hcases
  77. 0077exfalso
  78. 0078apply hn
  79. 0079exact hcases_left
  80. 0080rewrite hcases_right at hd_witness
  81. 0081specialize gaussian_add_functional (0)
  82. 0082specialize gaussian_add_functional (c)
  83. 0083specialize gaussian_add_functional (b)
  84. 0084specialize gaussian_add_functional (c)
  85. 0085apply gaussian_add_functional
  86. 0086exact hd_witness
  87. 0087specialize gaussian_add_zero_left (c)
  88. 0088apply gaussian_add_zero_left
  89. 0089specialize gaussian_multiply_input_right_valid (a)
  90. 0090specialize gaussian_multiply_input_right_valid (c)
  91. 0091specialize gaussian_multiply_input_right_valid (t)
  92. 0092apply gaussian_multiply_input_right_valid
  93. 0093exact hC