PA009Y

beta_product_double_succ_decompose

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

A product of length S(S k) decomposes into its k-prefix and its final two factors.

Exact expanded PA statement

forall b c k l Q. l = S (S k) -> (exists wpp_trace_code_two_product wpp_trace_scale_two_product. ((((exists wpp_beta_height_two_product_start. wpp_beta_height_two_product_start + S (1) = S ((S (0)) * wpp_trace_scale_two_product)) /\ exists wpp_beta_quotient_two_product_start. wpp_trace_code_two_product = wpp_beta_quotient_two_product_start * S ((S (0)) * wpp_trace_scale_two_product) + (1))) /\ ((((exists wpp_beta_height_two_product_terminal. wpp_beta_height_two_product_terminal + S (Q) = S ((S (l)) * wpp_trace_scale_two_product)) /\ exists wpp_beta_quotient_two_product_terminal. wpp_trace_code_two_product = wpp_beta_quotient_two_product_terminal * S ((S (l)) * wpp_trace_scale_two_product) + (Q))) /\ forall wpp_index_two_product. (exists wpp_gap_two_product_bound. wpp_gap_two_product_bound + S (wpp_index_two_product) = l) -> exists wpp_factor_two_product wpp_prefix_two_product wpp_successor_two_product. ((((exists wpp_beta_height_two_product_factor. wpp_beta_height_two_product_factor + S (wpp_factor_two_product) = S ((S (wpp_index_two_product)) * c)) /\ exists wpp_beta_quotient_two_product_factor. b = wpp_beta_quotient_two_product_factor * S ((S (wpp_index_two_product)) * c) + (wpp_factor_two_product))) /\ ((((exists wpp_beta_height_two_product_prefix. wpp_beta_height_two_product_prefix + S (wpp_prefix_two_product) = S ((S (wpp_index_two_product)) * wpp_trace_scale_two_product)) /\ exists wpp_beta_quotient_two_product_prefix. wpp_trace_code_two_product = wpp_beta_quotient_two_product_prefix * S ((S (wpp_index_two_product)) * wpp_trace_scale_two_product) + (wpp_prefix_two_product))) /\ ((((exists wpp_beta_height_two_product_successor. wpp_beta_height_two_product_successor + S (wpp_successor_two_product) = S ((S (S (wpp_index_two_product))) * wpp_trace_scale_two_product)) /\ exists wpp_beta_quotient_two_product_successor. wpp_trace_code_two_product = wpp_beta_quotient_two_product_successor * S ((S (S (wpp_index_two_product))) * wpp_trace_scale_two_product) + (wpp_successor_two_product))) /\ wpp_successor_two_product = wpp_prefix_two_product * wpp_factor_two_product)))))) -> (exists wpp_left_factor_two_result wpp_right_factor_two_result wpp_prefix_product_two_result. (((exists wpp_beta_height_two_result_left_entry. wpp_beta_height_two_result_left_entry + S (wpp_left_factor_two_result) = S ((S (k)) * c)) /\ exists wpp_beta_quotient_two_result_left_entry. b = wpp_beta_quotient_two_result_left_entry * S ((S (k)) * c) + (wpp_left_factor_two_result))) /\ ((((exists wpp_beta_height_two_result_right_entry. wpp_beta_height_two_result_right_entry + S (wpp_right_factor_two_result) = S ((S (S (k))) * c)) /\ exists wpp_beta_quotient_two_result_right_entry. b = wpp_beta_quotient_two_result_right_entry * S ((S (S (k))) * c) + (wpp_right_factor_two_result))) /\ ((exists wpp_trace_code_two_result_prefix wpp_trace_scale_two_result_prefix. ((((exists wpp_beta_height_two_result_prefix_start. wpp_beta_height_two_result_prefix_start + S (1) = S ((S (0)) * wpp_trace_scale_two_result_prefix)) /\ exists wpp_beta_quotient_two_result_prefix_start. wpp_trace_code_two_result_prefix = wpp_beta_quotient_two_result_prefix_start * S ((S (0)) * wpp_trace_scale_two_result_prefix) + (1))) /\ ((((exists wpp_beta_height_two_result_prefix_terminal. wpp_beta_height_two_result_prefix_terminal + S (wpp_prefix_product_two_result) = S ((S (k)) * wpp_trace_scale_two_result_prefix)) /\ exists wpp_beta_quotient_two_result_prefix_terminal. wpp_trace_code_two_result_prefix = wpp_beta_quotient_two_result_prefix_terminal * S ((S (k)) * wpp_trace_scale_two_result_prefix) + (wpp_prefix_product_two_result))) /\ forall wpp_index_two_result_prefix. (exists wpp_gap_two_result_prefix_bound. wpp_gap_two_result_prefix_bound + S (wpp_index_two_result_prefix) = k) -> exists wpp_factor_two_result_prefix wpp_prefix_two_result_prefix wpp_successor_two_result_prefix. ((((exists wpp_beta_height_two_result_prefix_factor. wpp_beta_height_two_result_prefix_factor + S (wpp_factor_two_result_prefix) = S ((S (wpp_index_two_result_prefix)) * c)) /\ exists wpp_beta_quotient_two_result_prefix_factor. b = wpp_beta_quotient_two_result_prefix_factor * S ((S (wpp_index_two_result_prefix)) * c) + (wpp_factor_two_result_prefix))) /\ ((((exists wpp_beta_height_two_result_prefix_prefix. wpp_beta_height_two_result_prefix_prefix + S (wpp_prefix_two_result_prefix) = S ((S (wpp_index_two_result_prefix)) * wpp_trace_scale_two_result_prefix)) /\ exists wpp_beta_quotient_two_result_prefix_prefix. wpp_trace_code_two_result_prefix = wpp_beta_quotient_two_result_prefix_prefix * S ((S (wpp_index_two_result_prefix)) * wpp_trace_scale_two_result_prefix) + (wpp_prefix_two_result_prefix))) /\ ((((exists wpp_beta_height_two_result_prefix_successor. wpp_beta_height_two_result_prefix_successor + S (wpp_successor_two_result_prefix) = S ((S (S (wpp_index_two_result_prefix))) * wpp_trace_scale_two_result_prefix)) /\ exists wpp_beta_quotient_two_result_prefix_successor. wpp_trace_code_two_result_prefix = wpp_beta_quotient_two_result_prefix_successor * S ((S (S (wpp_index_two_result_prefix))) * wpp_trace_scale_two_result_prefix) + (wpp_successor_two_result_prefix))) /\ wpp_successor_two_result_prefix = wpp_prefix_two_result_prefix * wpp_factor_two_result_prefix)))))) /\ Q = (wpp_prefix_product_two_result * wpp_left_factor_two_result) * wpp_right_factor_two_result)))

Structural proof guide

Generated structural guide

A product of length S(S k) decomposes into its k-prefix and its final two factors.

Use the direct prerequisites beta_product_succ_decompose as previously established PA formulas.

The proof proceeds by case analysis (8), intermediate claims (2), equality transport (5).

Referenced ingredients

PA004A beta_product_succ_decompose

Proof neighborhood

Direct dependencies

PA004A beta_product_succ_decompose

Direct dependents

PA00A0 beta_adjacent_target_pairs_product_power PA00B9 beta_adjacent_unit_pairs_product_one

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 b
  2. 0002intro c
  3. 0003intro k
  4. 0004intro l
  5. 0005intro Q
  6. 0006intro hlength
  7. 0007intro hproduct
  8. 0008rewrite hlength at hproduct
  9. 0009rewrite hlength at hproduct
  10. 0010rewrite hlength at hproduct
  11. 0011have houter : exists wpp_factor_outer_decomposition wpp_prefix_product_outer_decomposition. (((exists wpp_beta_height_outer_decomposition_entry. wpp_beta_height_outer_decomposition_entry + S (wpp_factor_outer_decomposition) = S ((S (S k)) * c)) /\ exists wpp_beta_quotient_outer_decomposition_entry. b = wpp_beta_quotient_outer_decomposition_entry * S ((S (S k)) * c) + (wpp_factor_outer_decomposition))) /\ ((exists wpp_trace_code_outer_decomposition_prefix wpp_trace_scale_outer_decomposition_prefix. ((((exists wpp_beta_height_outer_decomposition_prefix_start. wpp_beta_height_outer_decomposition_prefix_start + S (1) = S ((S (0)) * wpp_trace_scale_outer_decomposition_prefix)) /\ exists wpp_beta_quotient_outer_decomposition_prefix_start. wpp_trace_code_outer_decomposition_prefix = wpp_beta_quotient_outer_decomposition_prefix_start * S ((S (0)) * wpp_trace_scale_outer_decomposition_prefix) + (1))) /\ ((((exists wpp_beta_height_outer_decomposition_prefix_terminal. wpp_beta_height_outer_decomposition_prefix_terminal + S (wpp_prefix_product_outer_decomposition) = S ((S (S k)) * wpp_trace_scale_outer_decomposition_prefix)) /\ exists wpp_beta_quotient_outer_decomposition_prefix_terminal. wpp_trace_code_outer_decomposition_prefix = wpp_beta_quotient_outer_decomposition_prefix_terminal * S ((S (S k)) * wpp_trace_scale_outer_decomposition_prefix) + (wpp_prefix_product_outer_decomposition))) /\ forall wpp_index_outer_decomposition_prefix. (exists wpp_gap_outer_decomposition_prefix_bound. wpp_gap_outer_decomposition_prefix_bound + S (wpp_index_outer_decomposition_prefix) = S k) -> exists wpp_factor_outer_decomposition_prefix wpp_prefix_outer_decomposition_prefix wpp_successor_outer_decomposition_prefix. ((((exists wpp_beta_height_outer_decomposition_prefix_factor. wpp_beta_height_outer_decomposition_prefix_factor + S (wpp_factor_outer_decomposition_prefix) = S ((S (wpp_index_outer_decomposition_prefix)) * c)) /\ exists wpp_beta_quotient_outer_decomposition_prefix_factor. b = wpp_beta_quotient_outer_decomposition_prefix_factor * S ((S (wpp_index_outer_decomposition_prefix)) * c) + (wpp_factor_outer_decomposition_prefix))) /\ ((((exists wpp_beta_height_outer_decomposition_prefix_prefix. wpp_beta_height_outer_decomposition_prefix_prefix + S (wpp_prefix_outer_decomposition_prefix) = S ((S (wpp_index_outer_decomposition_prefix)) * wpp_trace_scale_outer_decomposition_prefix)) /\ exists wpp_beta_quotient_outer_decomposition_prefix_prefix. wpp_trace_code_outer_decomposition_prefix = wpp_beta_quotient_outer_decomposition_prefix_prefix * S ((S (wpp_index_outer_decomposition_prefix)) * wpp_trace_scale_outer_decomposition_prefix) + (wpp_prefix_outer_decomposition_prefix))) /\ ((((exists wpp_beta_height_outer_decomposition_prefix_successor. wpp_beta_height_outer_decomposition_prefix_successor + S (wpp_successor_outer_decomposition_prefix) = S ((S (S (wpp_index_outer_decomposition_prefix))) * wpp_trace_scale_outer_decomposition_prefix)) /\ exists wpp_beta_quotient_outer_decomposition_prefix_successor. wpp_trace_code_outer_decomposition_prefix = wpp_beta_quotient_outer_decomposition_prefix_successor * S ((S (S (wpp_index_outer_decomposition_prefix))) * wpp_trace_scale_outer_decomposition_prefix) + (wpp_successor_outer_decomposition_prefix))) /\ wpp_successor_outer_decomposition_prefix = wpp_prefix_outer_decomposition_prefix * wpp_factor_outer_decomposition_prefix)))))) /\ Q = wpp_prefix_product_outer_decomposition * wpp_factor_outer_decomposition)
  12. 0012specialize beta_product_succ_decompose b
  13. 0013specialize beta_product_succ_decompose c
  14. 0014specialize beta_product_succ_decompose (S k)
  15. 0015specialize beta_product_succ_decompose Q
  16. 0016apply beta_product_succ_decompose
  17. 0017exact hproduct
  18. 0018cases houter
  19. 0019cases houter_witness
  20. 0020cases houter_witness_witness
  21. 0021cases houter_witness_witness_right
  22. 0022have hinner : exists wpp_factor_inner_decomposition wpp_prefix_product_inner_decomposition. (((exists wpp_beta_height_inner_decomposition_entry. wpp_beta_height_inner_decomposition_entry + S (wpp_factor_inner_decomposition) = S ((S (k)) * c)) /\ exists wpp_beta_quotient_inner_decomposition_entry. b = wpp_beta_quotient_inner_decomposition_entry * S ((S (k)) * c) + (wpp_factor_inner_decomposition))) /\ ((exists wpp_trace_code_inner_decomposition_prefix wpp_trace_scale_inner_decomposition_prefix. ((((exists wpp_beta_height_inner_decomposition_prefix_start. wpp_beta_height_inner_decomposition_prefix_start + S (1) = S ((S (0)) * wpp_trace_scale_inner_decomposition_prefix)) /\ exists wpp_beta_quotient_inner_decomposition_prefix_start. wpp_trace_code_inner_decomposition_prefix = wpp_beta_quotient_inner_decomposition_prefix_start * S ((S (0)) * wpp_trace_scale_inner_decomposition_prefix) + (1))) /\ ((((exists wpp_beta_height_inner_decomposition_prefix_terminal. wpp_beta_height_inner_decomposition_prefix_terminal + S (wpp_prefix_product_inner_decomposition) = S ((S (k)) * wpp_trace_scale_inner_decomposition_prefix)) /\ exists wpp_beta_quotient_inner_decomposition_prefix_terminal. wpp_trace_code_inner_decomposition_prefix = wpp_beta_quotient_inner_decomposition_prefix_terminal * S ((S (k)) * wpp_trace_scale_inner_decomposition_prefix) + (wpp_prefix_product_inner_decomposition))) /\ forall wpp_index_inner_decomposition_prefix. (exists wpp_gap_inner_decomposition_prefix_bound. wpp_gap_inner_decomposition_prefix_bound + S (wpp_index_inner_decomposition_prefix) = k) -> exists wpp_factor_inner_decomposition_prefix wpp_prefix_inner_decomposition_prefix wpp_successor_inner_decomposition_prefix. ((((exists wpp_beta_height_inner_decomposition_prefix_factor. wpp_beta_height_inner_decomposition_prefix_factor + S (wpp_factor_inner_decomposition_prefix) = S ((S (wpp_index_inner_decomposition_prefix)) * c)) /\ exists wpp_beta_quotient_inner_decomposition_prefix_factor. b = wpp_beta_quotient_inner_decomposition_prefix_factor * S ((S (wpp_index_inner_decomposition_prefix)) * c) + (wpp_factor_inner_decomposition_prefix))) /\ ((((exists wpp_beta_height_inner_decomposition_prefix_prefix. wpp_beta_height_inner_decomposition_prefix_prefix + S (wpp_prefix_inner_decomposition_prefix) = S ((S (wpp_index_inner_decomposition_prefix)) * wpp_trace_scale_inner_decomposition_prefix)) /\ exists wpp_beta_quotient_inner_decomposition_prefix_prefix. wpp_trace_code_inner_decomposition_prefix = wpp_beta_quotient_inner_decomposition_prefix_prefix * S ((S (wpp_index_inner_decomposition_prefix)) * wpp_trace_scale_inner_decomposition_prefix) + (wpp_prefix_inner_decomposition_prefix))) /\ ((((exists wpp_beta_height_inner_decomposition_prefix_successor. wpp_beta_height_inner_decomposition_prefix_successor + S (wpp_successor_inner_decomposition_prefix) = S ((S (S (wpp_index_inner_decomposition_prefix))) * wpp_trace_scale_inner_decomposition_prefix)) /\ exists wpp_beta_quotient_inner_decomposition_prefix_successor. wpp_trace_code_inner_decomposition_prefix = wpp_beta_quotient_inner_decomposition_prefix_successor * S ((S (S (wpp_index_inner_decomposition_prefix))) * wpp_trace_scale_inner_decomposition_prefix) + (wpp_successor_inner_decomposition_prefix))) /\ wpp_successor_inner_decomposition_prefix = wpp_prefix_inner_decomposition_prefix * wpp_factor_inner_decomposition_prefix)))))) /\ x1 = wpp_prefix_product_inner_decomposition * wpp_factor_inner_decomposition)
  23. 0023specialize beta_product_succ_decompose b
  24. 0024specialize beta_product_succ_decompose c
  25. 0025specialize beta_product_succ_decompose k
  26. 0026specialize beta_product_succ_decompose x1
  27. 0027apply beta_product_succ_decompose
  28. 0028exact houter_witness_witness_right_left
  29. 0029cases hinner
  30. 0030cases hinner_witness
  31. 0031cases hinner_witness_witness
  32. 0032cases hinner_witness_witness_right
  33. 0033exists x2
  34. 0034exists x
  35. 0035exists x3
  36. 0036split
  37. 0037exact hinner_witness_witness_left
  38. 0038split
  39. 0039exact houter_witness_witness_left
  40. 0040split
  41. 0041exact hinner_witness_witness_right_left
  42. 0042rewrite houter_witness_witness_right_right
  43. 0043rewrite hinner_witness_witness_right_right
  44. 0044refl