PA00CQ

beta_sum_pointwise_mod_three_add

Alpha v16 checked-use theorem · independently closed; not Stable

Pointwise x==q+m+s congruence lifts to the four exact Sum endpoints.

Exact expanded PA statement

forall d b c qb qc mb mc sb sc l X Q M E. (exists ff_u_pointmod_source ff_v_pointmod_source. ((((exists ff_h_pointmod_source_start. ff_h_pointmod_source_start + S (0) = S ((S (0)) * ff_v_pointmod_source)) /\ exists ff_q_pointmod_source_start. ff_u_pointmod_source = ff_q_pointmod_source_start * S ((S (0)) * ff_v_pointmod_source) + (0))) /\ ((((exists ff_h_pointmod_source_terminal. ff_h_pointmod_source_terminal + S (X) = S ((S (l)) * ff_v_pointmod_source)) /\ exists ff_q_pointmod_source_terminal. ff_u_pointmod_source = ff_q_pointmod_source_terminal * S ((S (l)) * ff_v_pointmod_source) + (X))) /\ forall ff_i_pointmod_source. (exists ff_lt_pointmod_source_bound. ff_lt_pointmod_source_bound + S ff_i_pointmod_source = l) -> exists ff_a_pointmod_source ff_r_pointmod_source ff_s_pointmod_source. ((((exists ff_h_pointmod_source_summand. ff_h_pointmod_source_summand + S (ff_a_pointmod_source) = S ((S (ff_i_pointmod_source)) * c)) /\ exists ff_q_pointmod_source_summand. b = ff_q_pointmod_source_summand * S ((S (ff_i_pointmod_source)) * c) + (ff_a_pointmod_source))) /\ ((((exists ff_h_pointmod_source_partial. ff_h_pointmod_source_partial + S (ff_r_pointmod_source) = S ((S (ff_i_pointmod_source)) * ff_v_pointmod_source)) /\ exists ff_q_pointmod_source_partial. ff_u_pointmod_source = ff_q_pointmod_source_partial * S ((S (ff_i_pointmod_source)) * ff_v_pointmod_source) + (ff_r_pointmod_source))) /\ ((((exists ff_h_pointmod_source_successor. ff_h_pointmod_source_successor + S (ff_s_pointmod_source) = S ((S (S ff_i_pointmod_source)) * ff_v_pointmod_source)) /\ exists ff_q_pointmod_source_successor. ff_u_pointmod_source = ff_q_pointmod_source_successor * S ((S (S ff_i_pointmod_source)) * ff_v_pointmod_source) + (ff_s_pointmod_source))) /\ ff_s_pointmod_source = ff_r_pointmod_source + ff_a_pointmod_source)))))) -> (exists ff_u_pointmod_quotient ff_v_pointmod_quotient. ((((exists ff_h_pointmod_quotient_start. ff_h_pointmod_quotient_start + S (0) = S ((S (0)) * ff_v_pointmod_quotient)) /\ exists ff_q_pointmod_quotient_start. ff_u_pointmod_quotient = ff_q_pointmod_quotient_start * S ((S (0)) * ff_v_pointmod_quotient) + (0))) /\ ((((exists ff_h_pointmod_quotient_terminal. ff_h_pointmod_quotient_terminal + S (Q) = S ((S (l)) * ff_v_pointmod_quotient)) /\ exists ff_q_pointmod_quotient_terminal. ff_u_pointmod_quotient = ff_q_pointmod_quotient_terminal * S ((S (l)) * ff_v_pointmod_quotient) + (Q))) /\ forall ff_i_pointmod_quotient. (exists ff_lt_pointmod_quotient_bound. ff_lt_pointmod_quotient_bound + S ff_i_pointmod_quotient = l) -> exists ff_a_pointmod_quotient ff_r_pointmod_quotient ff_s_pointmod_quotient. ((((exists ff_h_pointmod_quotient_summand. ff_h_pointmod_quotient_summand + S (ff_a_pointmod_quotient) = S ((S (ff_i_pointmod_quotient)) * qc)) /\ exists ff_q_pointmod_quotient_summand. qb = ff_q_pointmod_quotient_summand * S ((S (ff_i_pointmod_quotient)) * qc) + (ff_a_pointmod_quotient))) /\ ((((exists ff_h_pointmod_quotient_partial. ff_h_pointmod_quotient_partial + S (ff_r_pointmod_quotient) = S ((S (ff_i_pointmod_quotient)) * ff_v_pointmod_quotient)) /\ exists ff_q_pointmod_quotient_partial. ff_u_pointmod_quotient = ff_q_pointmod_quotient_partial * S ((S (ff_i_pointmod_quotient)) * ff_v_pointmod_quotient) + (ff_r_pointmod_quotient))) /\ ((((exists ff_h_pointmod_quotient_successor. ff_h_pointmod_quotient_successor + S (ff_s_pointmod_quotient) = S ((S (S ff_i_pointmod_quotient)) * ff_v_pointmod_quotient)) /\ exists ff_q_pointmod_quotient_successor. ff_u_pointmod_quotient = ff_q_pointmod_quotient_successor * S ((S (S ff_i_pointmod_quotient)) * ff_v_pointmod_quotient) + (ff_s_pointmod_quotient))) /\ ff_s_pointmod_quotient = ff_r_pointmod_quotient + ff_a_pointmod_quotient)))))) -> (exists ff_u_pointmod_magnitude ff_v_pointmod_magnitude. ((((exists ff_h_pointmod_magnitude_start. ff_h_pointmod_magnitude_start + S (0) = S ((S (0)) * ff_v_pointmod_magnitude)) /\ exists ff_q_pointmod_magnitude_start. ff_u_pointmod_magnitude = ff_q_pointmod_magnitude_start * S ((S (0)) * ff_v_pointmod_magnitude) + (0))) /\ ((((exists ff_h_pointmod_magnitude_terminal. ff_h_pointmod_magnitude_terminal + S (M) = S ((S (l)) * ff_v_pointmod_magnitude)) /\ exists ff_q_pointmod_magnitude_terminal. ff_u_pointmod_magnitude = ff_q_pointmod_magnitude_terminal * S ((S (l)) * ff_v_pointmod_magnitude) + (M))) /\ forall ff_i_pointmod_magnitude. (exists ff_lt_pointmod_magnitude_bound. ff_lt_pointmod_magnitude_bound + S ff_i_pointmod_magnitude = l) -> exists ff_a_pointmod_magnitude ff_r_pointmod_magnitude ff_s_pointmod_magnitude. ((((exists ff_h_pointmod_magnitude_summand. ff_h_pointmod_magnitude_summand + S (ff_a_pointmod_magnitude) = S ((S (ff_i_pointmod_magnitude)) * mc)) /\ exists ff_q_pointmod_magnitude_summand. mb = ff_q_pointmod_magnitude_summand * S ((S (ff_i_pointmod_magnitude)) * mc) + (ff_a_pointmod_magnitude))) /\ ((((exists ff_h_pointmod_magnitude_partial. ff_h_pointmod_magnitude_partial + S (ff_r_pointmod_magnitude) = S ((S (ff_i_pointmod_magnitude)) * ff_v_pointmod_magnitude)) /\ exists ff_q_pointmod_magnitude_partial. ff_u_pointmod_magnitude = ff_q_pointmod_magnitude_partial * S ((S (ff_i_pointmod_magnitude)) * ff_v_pointmod_magnitude) + (ff_r_pointmod_magnitude))) /\ ((((exists ff_h_pointmod_magnitude_successor. ff_h_pointmod_magnitude_successor + S (ff_s_pointmod_magnitude) = S ((S (S ff_i_pointmod_magnitude)) * ff_v_pointmod_magnitude)) /\ exists ff_q_pointmod_magnitude_successor. ff_u_pointmod_magnitude = ff_q_pointmod_magnitude_successor * S ((S (S ff_i_pointmod_magnitude)) * ff_v_pointmod_magnitude) + (ff_s_pointmod_magnitude))) /\ ff_s_pointmod_magnitude = ff_r_pointmod_magnitude + ff_a_pointmod_magnitude)))))) -> (exists ff_u_pointmod_sign ff_v_pointmod_sign. ((((exists ff_h_pointmod_sign_start. ff_h_pointmod_sign_start + S (0) = S ((S (0)) * ff_v_pointmod_sign)) /\ exists ff_q_pointmod_sign_start. ff_u_pointmod_sign = ff_q_pointmod_sign_start * S ((S (0)) * ff_v_pointmod_sign) + (0))) /\ ((((exists ff_h_pointmod_sign_terminal. ff_h_pointmod_sign_terminal + S (E) = S ((S (l)) * ff_v_pointmod_sign)) /\ exists ff_q_pointmod_sign_terminal. ff_u_pointmod_sign = ff_q_pointmod_sign_terminal * S ((S (l)) * ff_v_pointmod_sign) + (E))) /\ forall ff_i_pointmod_sign. (exists ff_lt_pointmod_sign_bound. ff_lt_pointmod_sign_bound + S ff_i_pointmod_sign = l) -> exists ff_a_pointmod_sign ff_r_pointmod_sign ff_s_pointmod_sign. ((((exists ff_h_pointmod_sign_summand. ff_h_pointmod_sign_summand + S (ff_a_pointmod_sign) = S ((S (ff_i_pointmod_sign)) * sc)) /\ exists ff_q_pointmod_sign_summand. sb = ff_q_pointmod_sign_summand * S ((S (ff_i_pointmod_sign)) * sc) + (ff_a_pointmod_sign))) /\ ((((exists ff_h_pointmod_sign_partial. ff_h_pointmod_sign_partial + S (ff_r_pointmod_sign) = S ((S (ff_i_pointmod_sign)) * ff_v_pointmod_sign)) /\ exists ff_q_pointmod_sign_partial. ff_u_pointmod_sign = ff_q_pointmod_sign_partial * S ((S (ff_i_pointmod_sign)) * ff_v_pointmod_sign) + (ff_r_pointmod_sign))) /\ ((((exists ff_h_pointmod_sign_successor. ff_h_pointmod_sign_successor + S (ff_s_pointmod_sign) = S ((S (S ff_i_pointmod_sign)) * ff_v_pointmod_sign)) /\ exists ff_q_pointmod_sign_successor. ff_u_pointmod_sign = ff_q_pointmod_sign_successor * S ((S (S ff_i_pointmod_sign)) * ff_v_pointmod_sign) + (ff_s_pointmod_sign))) /\ ff_s_pointmod_sign = ff_r_pointmod_sign + ff_a_pointmod_sign)))))) -> (forall i x q m s. (exists h. h + S i = l) -> (((exists ff_h_pointmod_source_entry. ff_h_pointmod_source_entry + S (x) = S ((S (i)) * c)) /\ exists ff_q_pointmod_source_entry. b = ff_q_pointmod_source_entry * S ((S (i)) * c) + (x))) -> (((exists ff_h_pointmod_quotient_entry. ff_h_pointmod_quotient_entry + S (q) = S ((S (i)) * qc)) /\ exists ff_q_pointmod_quotient_entry. qb = ff_q_pointmod_quotient_entry * S ((S (i)) * qc) + (q))) -> (((exists ff_h_pointmod_magnitude_entry. ff_h_pointmod_magnitude_entry + S (m) = S ((S (i)) * mc)) /\ exists ff_q_pointmod_magnitude_entry. mb = ff_q_pointmod_magnitude_entry * S ((S (i)) * mc) + (m))) -> (((exists ff_h_pointmod_sign_entry. ff_h_pointmod_sign_entry + S (s) = S ((S (i)) * sc)) /\ exists ff_q_pointmod_sign_entry. sb = ff_q_pointmod_sign_entry * S ((S (i)) * sc) + (s))) -> (exists fspm_u_pointmod_entry fspm_v_pointmod_entry. (x) + d * fspm_u_pointmod_entry = (q + m + s) + d * fspm_v_pointmod_entry)) -> (exists fspm_u_pointmod_endpoint fspm_v_pointmod_endpoint. (X) + d * fspm_u_pointmod_endpoint = (Q + M + E) + d * fspm_v_pointmod_endpoint)

Structural proof guide

Generated structural guide

Pointwise x==q+m+s congruence lifts to the four exact Sum endpoints.

Use the direct prerequisites beta_sum_zero, beta_sum_succ_decompose, mod_eq_add, le_succ, le_refl, add_assoc, add_comm, add_permute_outer as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (16), intermediate claims (13), equality transport (9), certified simplification (1), closed numeral normalization (1).

Referenced ingredients

PA0047 beta_sum_zero PA003Y beta_sum_succ_decompose PA0022 mod_eq_add PA002O le_succ PA001A le_refl PA0009 add_assoc PA000F add_comm PA001I add_permute_outer

Proof neighborhood

Direct dependencies

PA0047 beta_sum_zero PA003Y beta_sum_succ_decompose PA0022 mod_eq_add PA002O le_succ PA001A le_refl PA0009 add_assoc PA000F add_comm PA001I add_permute_outer

Direct dependents

PA00CR gauss_eisenstein_terminal_sums_mod_two

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro d
  2. 0002intro b
  3. 0003intro c
  4. 0004intro qb
  5. 0005intro qc
  6. 0006intro mb
  7. 0007intro mc
  8. 0008intro sb
  9. 0009intro sc
  10. 0010induction l
  11. 0011intro X
  12. 0012intro Q
  13. 0013intro M
  14. 0014intro E
  15. 0015intro hsource
  16. 0016intro hquotient
  17. 0017intro hmagnitude
  18. 0018intro hsign
  19. 0019intro hpointwise
  20. 0020have hX : X = 0
  21. 0021specialize beta_sum_zero b
  22. 0022specialize beta_sum_zero c
  23. 0023specialize beta_sum_zero X
  24. 0024apply beta_sum_zero
  25. 0025exact hsource
  26. 0026have hQ : Q = 0
  27. 0027specialize beta_sum_zero qb
  28. 0028specialize beta_sum_zero qc
  29. 0029specialize beta_sum_zero Q
  30. 0030apply beta_sum_zero
  31. 0031exact hquotient
  32. 0032have hM : M = 0
  33. 0033specialize beta_sum_zero mb
  34. 0034specialize beta_sum_zero mc
  35. 0035specialize beta_sum_zero M
  36. 0036apply beta_sum_zero
  37. 0037exact hmagnitude
  38. 0038have hE : E = 0
  39. 0039specialize beta_sum_zero sb
  40. 0040specialize beta_sum_zero sc
  41. 0041specialize beta_sum_zero E
  42. 0042apply beta_sum_zero
  43. 0043exact hsign
  44. 0044rewrite hX
  45. 0045rewrite hQ
  46. 0046rewrite hM
  47. 0047rewrite hE
  48. 0048exists 0
  49. 0049exists 0
  50. 0050norm_num
  51. 0051intro X
  52. 0052intro Q
  53. 0053intro M
  54. 0054intro E
  55. 0055intro hsource
  56. 0056intro hquotient
  57. 0057intro hmagnitude
  58. 0058intro hsign
  59. 0059intro hpointwise
  60. 0060have hsource_decomp : exists a r. (((exists ff_h_pointmod_source_decomp_entry. ff_h_pointmod_source_decomp_entry + S (a) = S ((S (l)) * c)) /\ exists ff_q_pointmod_source_decomp_entry. b = ff_q_pointmod_source_decomp_entry * S ((S (l)) * c) + (a))) /\ ((exists ff_u_pointmod_source_decomp_prefix ff_v_pointmod_source_decomp_prefix. ((((exists ff_h_pointmod_source_decomp_prefix_start. ff_h_pointmod_source_decomp_prefix_start + S (0) = S ((S (0)) * ff_v_pointmod_source_decomp_prefix)) /\ exists ff_q_pointmod_source_decomp_prefix_start. ff_u_pointmod_source_decomp_prefix = ff_q_pointmod_source_decomp_prefix_start * S ((S (0)) * ff_v_pointmod_source_decomp_prefix) + (0))) /\ ((((exists ff_h_pointmod_source_decomp_prefix_terminal. ff_h_pointmod_source_decomp_prefix_terminal + S (r) = S ((S (l)) * ff_v_pointmod_source_decomp_prefix)) /\ exists ff_q_pointmod_source_decomp_prefix_terminal. ff_u_pointmod_source_decomp_prefix = ff_q_pointmod_source_decomp_prefix_terminal * S ((S (l)) * ff_v_pointmod_source_decomp_prefix) + (r))) /\ forall ff_i_pointmod_source_decomp_prefix. (exists ff_lt_pointmod_source_decomp_prefix_bound. ff_lt_pointmod_source_decomp_prefix_bound + S ff_i_pointmod_source_decomp_prefix = l) -> exists ff_a_pointmod_source_decomp_prefix ff_r_pointmod_source_decomp_prefix ff_s_pointmod_source_decomp_prefix. ((((exists ff_h_pointmod_source_decomp_prefix_summand. ff_h_pointmod_source_decomp_prefix_summand + S (ff_a_pointmod_source_decomp_prefix) = S ((S (ff_i_pointmod_source_decomp_prefix)) * c)) /\ exists ff_q_pointmod_source_decomp_prefix_summand. b = ff_q_pointmod_source_decomp_prefix_summand * S ((S (ff_i_pointmod_source_decomp_prefix)) * c) + (ff_a_pointmod_source_decomp_prefix))) /\ ((((exists ff_h_pointmod_source_decomp_prefix_partial. ff_h_pointmod_source_decomp_prefix_partial + S (ff_r_pointmod_source_decomp_prefix) = S ((S (ff_i_pointmod_source_decomp_prefix)) * ff_v_pointmod_source_decomp_prefix)) /\ exists ff_q_pointmod_source_decomp_prefix_partial. ff_u_pointmod_source_decomp_prefix = ff_q_pointmod_source_decomp_prefix_partial * S ((S (ff_i_pointmod_source_decomp_prefix)) * ff_v_pointmod_source_decomp_prefix) + (ff_r_pointmod_source_decomp_prefix))) /\ ((((exists ff_h_pointmod_source_decomp_prefix_successor. ff_h_pointmod_source_decomp_prefix_successor + S (ff_s_pointmod_source_decomp_prefix) = S ((S (S ff_i_pointmod_source_decomp_prefix)) * ff_v_pointmod_source_decomp_prefix)) /\ exists ff_q_pointmod_source_decomp_prefix_successor. ff_u_pointmod_source_decomp_prefix = ff_q_pointmod_source_decomp_prefix_successor * S ((S (S ff_i_pointmod_source_decomp_prefix)) * ff_v_pointmod_source_decomp_prefix) + (ff_s_pointmod_source_decomp_prefix))) /\ ff_s_pointmod_source_decomp_prefix = ff_r_pointmod_source_decomp_prefix + ff_a_pointmod_source_decomp_prefix)))))) /\ X = r + a)
  61. 0061specialize beta_sum_succ_decompose b
  62. 0062specialize beta_sum_succ_decompose c
  63. 0063specialize beta_sum_succ_decompose l
  64. 0064specialize beta_sum_succ_decompose X
  65. 0065apply beta_sum_succ_decompose
  66. 0066exact hsource
  67. 0067cases hsource_decomp
  68. 0068cases hsource_decomp_witness
  69. 0069cases hsource_decomp_witness_witness
  70. 0070cases hsource_decomp_witness_witness_right
  71. 0071have hquotient_decomp : exists a r. (((exists ff_h_pointmod_quotient_decomp_entry. ff_h_pointmod_quotient_decomp_entry + S (a) = S ((S (l)) * qc)) /\ exists ff_q_pointmod_quotient_decomp_entry. qb = ff_q_pointmod_quotient_decomp_entry * S ((S (l)) * qc) + (a))) /\ ((exists ff_u_pointmod_quotient_decomp_prefix ff_v_pointmod_quotient_decomp_prefix. ((((exists ff_h_pointmod_quotient_decomp_prefix_start. ff_h_pointmod_quotient_decomp_prefix_start + S (0) = S ((S (0)) * ff_v_pointmod_quotient_decomp_prefix)) /\ exists ff_q_pointmod_quotient_decomp_prefix_start. ff_u_pointmod_quotient_decomp_prefix = ff_q_pointmod_quotient_decomp_prefix_start * S ((S (0)) * ff_v_pointmod_quotient_decomp_prefix) + (0))) /\ ((((exists ff_h_pointmod_quotient_decomp_prefix_terminal. ff_h_pointmod_quotient_decomp_prefix_terminal + S (r) = S ((S (l)) * ff_v_pointmod_quotient_decomp_prefix)) /\ exists ff_q_pointmod_quotient_decomp_prefix_terminal. ff_u_pointmod_quotient_decomp_prefix = ff_q_pointmod_quotient_decomp_prefix_terminal * S ((S (l)) * ff_v_pointmod_quotient_decomp_prefix) + (r))) /\ forall ff_i_pointmod_quotient_decomp_prefix. (exists ff_lt_pointmod_quotient_decomp_prefix_bound. ff_lt_pointmod_quotient_decomp_prefix_bound + S ff_i_pointmod_quotient_decomp_prefix = l) -> exists ff_a_pointmod_quotient_decomp_prefix ff_r_pointmod_quotient_decomp_prefix ff_s_pointmod_quotient_decomp_prefix. ((((exists ff_h_pointmod_quotient_decomp_prefix_summand. ff_h_pointmod_quotient_decomp_prefix_summand + S (ff_a_pointmod_quotient_decomp_prefix) = S ((S (ff_i_pointmod_quotient_decomp_prefix)) * qc)) /\ exists ff_q_pointmod_quotient_decomp_prefix_summand. qb = ff_q_pointmod_quotient_decomp_prefix_summand * S ((S (ff_i_pointmod_quotient_decomp_prefix)) * qc) + (ff_a_pointmod_quotient_decomp_prefix))) /\ ((((exists ff_h_pointmod_quotient_decomp_prefix_partial. ff_h_pointmod_quotient_decomp_prefix_partial + S (ff_r_pointmod_quotient_decomp_prefix) = S ((S (ff_i_pointmod_quotient_decomp_prefix)) * ff_v_pointmod_quotient_decomp_prefix)) /\ exists ff_q_pointmod_quotient_decomp_prefix_partial. ff_u_pointmod_quotient_decomp_prefix = ff_q_pointmod_quotient_decomp_prefix_partial * S ((S (ff_i_pointmod_quotient_decomp_prefix)) * ff_v_pointmod_quotient_decomp_prefix) + (ff_r_pointmod_quotient_decomp_prefix))) /\ ((((exists ff_h_pointmod_quotient_decomp_prefix_successor. ff_h_pointmod_quotient_decomp_prefix_successor + S (ff_s_pointmod_quotient_decomp_prefix) = S ((S (S ff_i_pointmod_quotient_decomp_prefix)) * ff_v_pointmod_quotient_decomp_prefix)) /\ exists ff_q_pointmod_quotient_decomp_prefix_successor. ff_u_pointmod_quotient_decomp_prefix = ff_q_pointmod_quotient_decomp_prefix_successor * S ((S (S ff_i_pointmod_quotient_decomp_prefix)) * ff_v_pointmod_quotient_decomp_prefix) + (ff_s_pointmod_quotient_decomp_prefix))) /\ ff_s_pointmod_quotient_decomp_prefix = ff_r_pointmod_quotient_decomp_prefix + ff_a_pointmod_quotient_decomp_prefix)))))) /\ Q = r + a)
  72. 0072specialize beta_sum_succ_decompose qb
  73. 0073specialize beta_sum_succ_decompose qc
  74. 0074specialize beta_sum_succ_decompose l
  75. 0075specialize beta_sum_succ_decompose Q
  76. 0076apply beta_sum_succ_decompose
  77. 0077exact hquotient
  78. 0078cases hquotient_decomp
  79. 0079cases hquotient_decomp_witness
  80. 0080cases hquotient_decomp_witness_witness
  81. 0081cases hquotient_decomp_witness_witness_right
  82. 0082have hmagnitude_decomp : exists a r. (((exists ff_h_pointmod_magnitude_decomp_entry. ff_h_pointmod_magnitude_decomp_entry + S (a) = S ((S (l)) * mc)) /\ exists ff_q_pointmod_magnitude_decomp_entry. mb = ff_q_pointmod_magnitude_decomp_entry * S ((S (l)) * mc) + (a))) /\ ((exists ff_u_pointmod_magnitude_decomp_prefix ff_v_pointmod_magnitude_decomp_prefix. ((((exists ff_h_pointmod_magnitude_decomp_prefix_start. ff_h_pointmod_magnitude_decomp_prefix_start + S (0) = S ((S (0)) * ff_v_pointmod_magnitude_decomp_prefix)) /\ exists ff_q_pointmod_magnitude_decomp_prefix_start. ff_u_pointmod_magnitude_decomp_prefix = ff_q_pointmod_magnitude_decomp_prefix_start * S ((S (0)) * ff_v_pointmod_magnitude_decomp_prefix) + (0))) /\ ((((exists ff_h_pointmod_magnitude_decomp_prefix_terminal. ff_h_pointmod_magnitude_decomp_prefix_terminal + S (r) = S ((S (l)) * ff_v_pointmod_magnitude_decomp_prefix)) /\ exists ff_q_pointmod_magnitude_decomp_prefix_terminal. ff_u_pointmod_magnitude_decomp_prefix = ff_q_pointmod_magnitude_decomp_prefix_terminal * S ((S (l)) * ff_v_pointmod_magnitude_decomp_prefix) + (r))) /\ forall ff_i_pointmod_magnitude_decomp_prefix. (exists ff_lt_pointmod_magnitude_decomp_prefix_bound. ff_lt_pointmod_magnitude_decomp_prefix_bound + S ff_i_pointmod_magnitude_decomp_prefix = l) -> exists ff_a_pointmod_magnitude_decomp_prefix ff_r_pointmod_magnitude_decomp_prefix ff_s_pointmod_magnitude_decomp_prefix. ((((exists ff_h_pointmod_magnitude_decomp_prefix_summand. ff_h_pointmod_magnitude_decomp_prefix_summand + S (ff_a_pointmod_magnitude_decomp_prefix) = S ((S (ff_i_pointmod_magnitude_decomp_prefix)) * mc)) /\ exists ff_q_pointmod_magnitude_decomp_prefix_summand. mb = ff_q_pointmod_magnitude_decomp_prefix_summand * S ((S (ff_i_pointmod_magnitude_decomp_prefix)) * mc) + (ff_a_pointmod_magnitude_decomp_prefix))) /\ ((((exists ff_h_pointmod_magnitude_decomp_prefix_partial. ff_h_pointmod_magnitude_decomp_prefix_partial + S (ff_r_pointmod_magnitude_decomp_prefix) = S ((S (ff_i_pointmod_magnitude_decomp_prefix)) * ff_v_pointmod_magnitude_decomp_prefix)) /\ exists ff_q_pointmod_magnitude_decomp_prefix_partial. ff_u_pointmod_magnitude_decomp_prefix = ff_q_pointmod_magnitude_decomp_prefix_partial * S ((S (ff_i_pointmod_magnitude_decomp_prefix)) * ff_v_pointmod_magnitude_decomp_prefix) + (ff_r_pointmod_magnitude_decomp_prefix))) /\ ((((exists ff_h_pointmod_magnitude_decomp_prefix_successor. ff_h_pointmod_magnitude_decomp_prefix_successor + S (ff_s_pointmod_magnitude_decomp_prefix) = S ((S (S ff_i_pointmod_magnitude_decomp_prefix)) * ff_v_pointmod_magnitude_decomp_prefix)) /\ exists ff_q_pointmod_magnitude_decomp_prefix_successor. ff_u_pointmod_magnitude_decomp_prefix = ff_q_pointmod_magnitude_decomp_prefix_successor * S ((S (S ff_i_pointmod_magnitude_decomp_prefix)) * ff_v_pointmod_magnitude_decomp_prefix) + (ff_s_pointmod_magnitude_decomp_prefix))) /\ ff_s_pointmod_magnitude_decomp_prefix = ff_r_pointmod_magnitude_decomp_prefix + ff_a_pointmod_magnitude_decomp_prefix)))))) /\ M = r + a)
  83. 0083specialize beta_sum_succ_decompose mb
  84. 0084specialize beta_sum_succ_decompose mc
  85. 0085specialize beta_sum_succ_decompose l
  86. 0086specialize beta_sum_succ_decompose M
  87. 0087apply beta_sum_succ_decompose
  88. 0088exact hmagnitude
  89. 0089cases hmagnitude_decomp
  90. 0090cases hmagnitude_decomp_witness
  91. 0091cases hmagnitude_decomp_witness_witness
  92. 0092cases hmagnitude_decomp_witness_witness_right
  93. 0093have hsign_decomp : exists a r. (((exists ff_h_pointmod_sign_decomp_entry. ff_h_pointmod_sign_decomp_entry + S (a) = S ((S (l)) * sc)) /\ exists ff_q_pointmod_sign_decomp_entry. sb = ff_q_pointmod_sign_decomp_entry * S ((S (l)) * sc) + (a))) /\ ((exists ff_u_pointmod_sign_decomp_prefix ff_v_pointmod_sign_decomp_prefix. ((((exists ff_h_pointmod_sign_decomp_prefix_start. ff_h_pointmod_sign_decomp_prefix_start + S (0) = S ((S (0)) * ff_v_pointmod_sign_decomp_prefix)) /\ exists ff_q_pointmod_sign_decomp_prefix_start. ff_u_pointmod_sign_decomp_prefix = ff_q_pointmod_sign_decomp_prefix_start * S ((S (0)) * ff_v_pointmod_sign_decomp_prefix) + (0))) /\ ((((exists ff_h_pointmod_sign_decomp_prefix_terminal. ff_h_pointmod_sign_decomp_prefix_terminal + S (r) = S ((S (l)) * ff_v_pointmod_sign_decomp_prefix)) /\ exists ff_q_pointmod_sign_decomp_prefix_terminal. ff_u_pointmod_sign_decomp_prefix = ff_q_pointmod_sign_decomp_prefix_terminal * S ((S (l)) * ff_v_pointmod_sign_decomp_prefix) + (r))) /\ forall ff_i_pointmod_sign_decomp_prefix. (exists ff_lt_pointmod_sign_decomp_prefix_bound. ff_lt_pointmod_sign_decomp_prefix_bound + S ff_i_pointmod_sign_decomp_prefix = l) -> exists ff_a_pointmod_sign_decomp_prefix ff_r_pointmod_sign_decomp_prefix ff_s_pointmod_sign_decomp_prefix. ((((exists ff_h_pointmod_sign_decomp_prefix_summand. ff_h_pointmod_sign_decomp_prefix_summand + S (ff_a_pointmod_sign_decomp_prefix) = S ((S (ff_i_pointmod_sign_decomp_prefix)) * sc)) /\ exists ff_q_pointmod_sign_decomp_prefix_summand. sb = ff_q_pointmod_sign_decomp_prefix_summand * S ((S (ff_i_pointmod_sign_decomp_prefix)) * sc) + (ff_a_pointmod_sign_decomp_prefix))) /\ ((((exists ff_h_pointmod_sign_decomp_prefix_partial. ff_h_pointmod_sign_decomp_prefix_partial + S (ff_r_pointmod_sign_decomp_prefix) = S ((S (ff_i_pointmod_sign_decomp_prefix)) * ff_v_pointmod_sign_decomp_prefix)) /\ exists ff_q_pointmod_sign_decomp_prefix_partial. ff_u_pointmod_sign_decomp_prefix = ff_q_pointmod_sign_decomp_prefix_partial * S ((S (ff_i_pointmod_sign_decomp_prefix)) * ff_v_pointmod_sign_decomp_prefix) + (ff_r_pointmod_sign_decomp_prefix))) /\ ((((exists ff_h_pointmod_sign_decomp_prefix_successor. ff_h_pointmod_sign_decomp_prefix_successor + S (ff_s_pointmod_sign_decomp_prefix) = S ((S (S ff_i_pointmod_sign_decomp_prefix)) * ff_v_pointmod_sign_decomp_prefix)) /\ exists ff_q_pointmod_sign_decomp_prefix_successor. ff_u_pointmod_sign_decomp_prefix = ff_q_pointmod_sign_decomp_prefix_successor * S ((S (S ff_i_pointmod_sign_decomp_prefix)) * ff_v_pointmod_sign_decomp_prefix) + (ff_s_pointmod_sign_decomp_prefix))) /\ ff_s_pointmod_sign_decomp_prefix = ff_r_pointmod_sign_decomp_prefix + ff_a_pointmod_sign_decomp_prefix)))))) /\ E = r + a)
  94. 0094specialize beta_sum_succ_decompose sb
  95. 0095specialize beta_sum_succ_decompose sc
  96. 0096specialize beta_sum_succ_decompose l
  97. 0097specialize beta_sum_succ_decompose E
  98. 0098apply beta_sum_succ_decompose
  99. 0099exact hsign
  100. 0100cases hsign_decomp
  101. 0101cases hsign_decomp_witness
  102. 0102cases hsign_decomp_witness_witness
  103. 0103cases hsign_decomp_witness_witness_right
  104. 0104have hprefix_pointwise : forall i x q m s. (exists h. h + S i = l) -> (((exists ff_h_pointmod_prefix_source_entry. ff_h_pointmod_prefix_source_entry + S (x) = S ((S (i)) * c)) /\ exists ff_q_pointmod_prefix_source_entry. b = ff_q_pointmod_prefix_source_entry * S ((S (i)) * c) + (x))) -> (((exists ff_h_pointmod_prefix_quotient_entry. ff_h_pointmod_prefix_quotient_entry + S (q) = S ((S (i)) * qc)) /\ exists ff_q_pointmod_prefix_quotient_entry. qb = ff_q_pointmod_prefix_quotient_entry * S ((S (i)) * qc) + (q))) -> (((exists ff_h_pointmod_prefix_magnitude_entry. ff_h_pointmod_prefix_magnitude_entry + S (m) = S ((S (i)) * mc)) /\ exists ff_q_pointmod_prefix_magnitude_entry. mb = ff_q_pointmod_prefix_magnitude_entry * S ((S (i)) * mc) + (m))) -> (((exists ff_h_pointmod_prefix_sign_entry. ff_h_pointmod_prefix_sign_entry + S (s) = S ((S (i)) * sc)) /\ exists ff_q_pointmod_prefix_sign_entry. sb = ff_q_pointmod_prefix_sign_entry * S ((S (i)) * sc) + (s))) -> (exists fspm_u_pointmod_prefix_entry fspm_v_pointmod_prefix_entry. (x) + d * fspm_u_pointmod_prefix_entry = (q + m + s) + d * fspm_v_pointmod_prefix_entry)
  105. 0105intro i
  106. 0106intro y
  107. 0107intro q
  108. 0108intro m
  109. 0109intro s
  110. 0110intro hi
  111. 0111intro hy
  112. 0112intro hq
  113. 0113intro hm
  114. 0114intro hs
  115. 0115specialize hpointwise i
  116. 0116specialize hpointwise y
  117. 0117specialize hpointwise q
  118. 0118specialize hpointwise m
  119. 0119specialize hpointwise s
  120. 0120apply hpointwise
  121. 0121specialize le_succ (S i)
  122. 0122specialize le_succ l
  123. 0123apply le_succ
  124. 0124exact hi
  125. 0125exact hy
  126. 0126exact hq
  127. 0127exact hm
  128. 0128exact hs
  129. 0129have hprefix : exists fspm_u_pointmod_prefix fspm_v_pointmod_prefix. (x1) + d * fspm_u_pointmod_prefix = (x3 + x5 + x7) + d * fspm_v_pointmod_prefix
  130. 0130specialize IH x1
  131. 0131specialize IH x3
  132. 0132specialize IH x5
  133. 0133specialize IH x7
  134. 0134apply IH
  135. 0135exact hsource_decomp_witness_witness_right_left
  136. 0136exact hquotient_decomp_witness_witness_right_left
  137. 0137exact hmagnitude_decomp_witness_witness_right_left
  138. 0138exact hsign_decomp_witness_witness_right_left
  139. 0139exact hprefix_pointwise
  140. 0140have hlast : exists fspm_u_pointmod_last fspm_v_pointmod_last. (x) + d * fspm_u_pointmod_last = (x2 + x4 + x6) + d * fspm_v_pointmod_last
  141. 0141specialize hpointwise l
  142. 0142specialize hpointwise x
  143. 0143specialize hpointwise x2
  144. 0144specialize hpointwise x4
  145. 0145specialize hpointwise x6
  146. 0146apply hpointwise
  147. 0147specialize le_refl (S l)
  148. 0148exact le_refl
  149. 0149exact hsource_decomp_witness_witness_left
  150. 0150exact hquotient_decomp_witness_witness_left
  151. 0151exact hmagnitude_decomp_witness_witness_left
  152. 0152exact hsign_decomp_witness_witness_left
  153. 0153have hcombined : exists fspm_u_pointmod_combined fspm_v_pointmod_combined. (x1 + x) + d * fspm_u_pointmod_combined = ((x3 + x5 + x7) + (x2 + x4 + x6)) + d * fspm_v_pointmod_combined
  154. 0154specialize mod_eq_add d
  155. 0155specialize mod_eq_add x1
  156. 0156specialize mod_eq_add (x3 + x5 + x7)
  157. 0157specialize mod_eq_add x
  158. 0158specialize mod_eq_add (x2 + x4 + x6)
  159. 0159apply mod_eq_add
  160. 0160exact hprefix
  161. 0161exact hlast
  162. 0162have hreorder : (x3 + x5 + x7) + (x2 + x4 + x6) = (x3 + x2) + (x5 + x4) + (x7 + x6)
  163. 0163simp [add_assoc, add_comm, add_permute_outer]
  164. 0164congr
  165. 0165refl
  166. 0166congr
  167. 0167refl
  168. 0168trans (x7 + x4) + (x6 + x2)
  169. 0169symm
  170. 0170apply add_assoc
  171. 0171trans (x4 + x7) + (x6 + x2)
  172. 0172congr
  173. 0173apply add_comm
  174. 0174refl
  175. 0175apply add_assoc
  176. 0176rewrite hreorder at hcombined
  177. 0177rewrite hsource_decomp_witness_witness_right_right
  178. 0178rewrite hquotient_decomp_witness_witness_right_right
  179. 0179rewrite hmagnitude_decomp_witness_witness_right_right
  180. 0180rewrite hsign_decomp_witness_witness_right_right
  181. 0181exact hcombined