PA007W · theorem

beta_product_reindex_fixed_last

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

A fixed-final reindex reduces successor product equality to equality of the two prefix products.

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.

Statement with defined notation

∀ r. ∀ s. ∀ b. ∀ c. ∀ z. ∀ d. ∀ n. ∀ p. ∀ q. (∀ x. ∀ y. ∀ m. Lt(x,S n) → BetaAt(r,s,x,y) → BetaAt(b,c,y,m) → BetaAt(z,d,x,m)) → BetaAt(r,s,n,n) → Product(b,c,S n,p) → Product(z,d,S n,q) → (∀ x. ∀ y. Product(b,c,n,x) → Product(z,d,n,y) → x = y) → p = q

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt PD0014 Product

9 occurrences

In local proof propositions

PD0013 BetaAt PD0014 Product

5 occurrences

Exact expanded native-PA statement
forall r s b c z d n p q. (forall fpr_i_fra fpr_j_fra fpr_x_fra. (exists fpr_h_fra. fpr_h_fra + S fpr_i_fra = S n) -> (((exists ff_h_fra_map. ff_h_fra_map + S (fpr_j_fra) = S ((S (fpr_i_fra)) * s)) /\ exists ff_q_fra_map. r = ff_q_fra_map * S ((S (fpr_i_fra)) * s) + (fpr_j_fra))) -> (((exists ff_h_fra_source. ff_h_fra_source + S (fpr_x_fra) = S ((S (fpr_j_fra)) * c)) /\ exists ff_q_fra_source. b = ff_q_fra_source * S ((S (fpr_j_fra)) * c) + (fpr_x_fra))) -> (((exists ff_h_fra_target. ff_h_fra_target + S (fpr_x_fra) = S ((S (fpr_i_fra)) * d)) /\ exists ff_q_fra_target. z = ff_q_fra_target * S ((S (fpr_i_fra)) * d) + (fpr_x_fra)))) -> (((exists ff_h_frm. ff_h_frm + S (n) = S ((S (n)) * s)) /\ exists ff_q_frm. r = ff_q_frm * S ((S (n)) * s) + (n))) -> (exists ff_u_frs ff_v_frs. ((((exists ff_h_frs_start. ff_h_frs_start + S (1) = S ((S (0)) * ff_v_frs)) /\ exists ff_q_frs_start. ff_u_frs = ff_q_frs_start * S ((S (0)) * ff_v_frs) + (1))) /\ ((((exists ff_h_frs_terminal. ff_h_frs_terminal + S (p) = S ((S (S n)) * ff_v_frs)) /\ exists ff_q_frs_terminal. ff_u_frs = ff_q_frs_terminal * S ((S (S n)) * ff_v_frs) + (p))) /\ forall ff_i_frs. (exists ff_lt_frs_bound. ff_lt_frs_bound + S ff_i_frs = S n) -> exists ff_p_frs ff_r_frs ff_s_frs. ((((exists ff_h_frs_factor. ff_h_frs_factor + S (ff_p_frs) = S ((S (ff_i_frs)) * c)) /\ exists ff_q_frs_factor. b = ff_q_frs_factor * S ((S (ff_i_frs)) * c) + (ff_p_frs))) /\ ((((exists ff_h_frs_partial. ff_h_frs_partial + S (ff_r_frs) = S ((S (ff_i_frs)) * ff_v_frs)) /\ exists ff_q_frs_partial. ff_u_frs = ff_q_frs_partial * S ((S (ff_i_frs)) * ff_v_frs) + (ff_r_frs))) /\ ((((exists ff_h_frs_successor. ff_h_frs_successor + S (ff_s_frs) = S ((S (S ff_i_frs)) * ff_v_frs)) /\ exists ff_q_frs_successor. ff_u_frs = ff_q_frs_successor * S ((S (S ff_i_frs)) * ff_v_frs) + (ff_s_frs))) /\ ff_s_frs = ff_r_frs * ff_p_frs)))))) -> (exists ff_u_frt ff_v_frt. ((((exists ff_h_frt_start. ff_h_frt_start + S (1) = S ((S (0)) * ff_v_frt)) /\ exists ff_q_frt_start. ff_u_frt = ff_q_frt_start * S ((S (0)) * ff_v_frt) + (1))) /\ ((((exists ff_h_frt_terminal. ff_h_frt_terminal + S (q) = S ((S (S n)) * ff_v_frt)) /\ exists ff_q_frt_terminal. ff_u_frt = ff_q_frt_terminal * S ((S (S n)) * ff_v_frt) + (q))) /\ forall ff_i_frt. (exists ff_lt_frt_bound. ff_lt_frt_bound + S ff_i_frt = S n) -> exists ff_p_frt ff_r_frt ff_s_frt. ((((exists ff_h_frt_factor. ff_h_frt_factor + S (ff_p_frt) = S ((S (ff_i_frt)) * d)) /\ exists ff_q_frt_factor. z = ff_q_frt_factor * S ((S (ff_i_frt)) * d) + (ff_p_frt))) /\ ((((exists ff_h_frt_partial. ff_h_frt_partial + S (ff_r_frt) = S ((S (ff_i_frt)) * ff_v_frt)) /\ exists ff_q_frt_partial. ff_u_frt = ff_q_frt_partial * S ((S (ff_i_frt)) * ff_v_frt) + (ff_r_frt))) /\ ((((exists ff_h_frt_successor. ff_h_frt_successor + S (ff_s_frt) = S ((S (S ff_i_frt)) * ff_v_frt)) /\ exists ff_q_frt_successor. ff_u_frt = ff_q_frt_successor * S ((S (S ff_i_frt)) * ff_v_frt) + (ff_s_frt))) /\ ff_s_frt = ff_r_frt * ff_p_frt)))))) -> (forall u v. (exists ff_u_fru ff_v_fru. ((((exists ff_h_fru_start. ff_h_fru_start + S (1) = S ((S (0)) * ff_v_fru)) /\ exists ff_q_fru_start. ff_u_fru = ff_q_fru_start * S ((S (0)) * ff_v_fru) + (1))) /\ ((((exists ff_h_fru_terminal. ff_h_fru_terminal + S (u) = S ((S (n)) * ff_v_fru)) /\ exists ff_q_fru_terminal. ff_u_fru = ff_q_fru_terminal * S ((S (n)) * ff_v_fru) + (u))) /\ forall ff_i_fru. (exists ff_lt_fru_bound. ff_lt_fru_bound + S ff_i_fru = n) -> exists ff_p_fru ff_r_fru ff_s_fru. ((((exists ff_h_fru_factor. ff_h_fru_factor + S (ff_p_fru) = S ((S (ff_i_fru)) * c)) /\ exists ff_q_fru_factor. b = ff_q_fru_factor * S ((S (ff_i_fru)) * c) + (ff_p_fru))) /\ ((((exists ff_h_fru_partial. ff_h_fru_partial + S (ff_r_fru) = S ((S (ff_i_fru)) * ff_v_fru)) /\ exists ff_q_fru_partial. ff_u_fru = ff_q_fru_partial * S ((S (ff_i_fru)) * ff_v_fru) + (ff_r_fru))) /\ ((((exists ff_h_fru_successor. ff_h_fru_successor + S (ff_s_fru) = S ((S (S ff_i_fru)) * ff_v_fru)) /\ exists ff_q_fru_successor. ff_u_fru = ff_q_fru_successor * S ((S (S ff_i_fru)) * ff_v_fru) + (ff_s_fru))) /\ ff_s_fru = ff_r_fru * ff_p_fru)))))) -> (exists ff_u_frv ff_v_frv. ((((exists ff_h_frv_start. ff_h_frv_start + S (1) = S ((S (0)) * ff_v_frv)) /\ exists ff_q_frv_start. ff_u_frv = ff_q_frv_start * S ((S (0)) * ff_v_frv) + (1))) /\ ((((exists ff_h_frv_terminal. ff_h_frv_terminal + S (v) = S ((S (n)) * ff_v_frv)) /\ exists ff_q_frv_terminal. ff_u_frv = ff_q_frv_terminal * S ((S (n)) * ff_v_frv) + (v))) /\ forall ff_i_frv. (exists ff_lt_frv_bound. ff_lt_frv_bound + S ff_i_frv = n) -> exists ff_p_frv ff_r_frv ff_s_frv. ((((exists ff_h_frv_factor. ff_h_frv_factor + S (ff_p_frv) = S ((S (ff_i_frv)) * d)) /\ exists ff_q_frv_factor. z = ff_q_frv_factor * S ((S (ff_i_frv)) * d) + (ff_p_frv))) /\ ((((exists ff_h_frv_partial. ff_h_frv_partial + S (ff_r_frv) = S ((S (ff_i_frv)) * ff_v_frv)) /\ exists ff_q_frv_partial. ff_u_frv = ff_q_frv_partial * S ((S (ff_i_frv)) * ff_v_frv) + (ff_r_frv))) /\ ((((exists ff_h_frv_successor. ff_h_frv_successor + S (ff_s_frv) = S ((S (S ff_i_frv)) * ff_v_frv)) /\ exists ff_q_frv_successor. ff_u_frv = ff_q_frv_successor * S ((S (S ff_i_frv)) * ff_v_frv) + (ff_s_frv))) /\ ff_s_frv = ff_r_frv * ff_p_frv)))))) -> u = v) -> p = q

Proof neighborhood

Direct theorem prerequisites

PA004A beta_product_succ_decompose PA002F beta_at_unique PA001A le_refl

Direct theorem dependents

PA007X beta_product_permutation_invariant

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

65 script commands · 9 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.

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

Named ingredients (3)
beta product succ decomposebeta at uniquele refl
01Fix variables and assumptionsL1–10

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

  1. L1
    intro r
  2. L2
    intro s
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro z
  6. L6
    intro d
  7. L7
    intro n
  8. L8
    intro p
  9. L9
    intro q
  10. L10
    intro haligned
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hmap_last
  2. L12
    intro hsource_product
  3. L13
    intro htarget_product
  4. L14
    intro hprefix_equal
03Establish hsource_decompL15–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product succ decompose.

  1. L15
    have hsource_decomp : ∃ a. ∃ u. BetaAt(b,c,n,a) ∧ (Product(b,c,n,u) ∧ p = u · a)Definitions: BetaAt(b,c,n,a)Product(b,c,n,u)Original native command in the exact edition
  2. L16
    specialize beta_product_succ_decompose b
  3. L17
    specialize beta_product_succ_decompose c
  4. L18
    specialize beta_product_succ_decompose n
  5. L19
    specialize beta_product_succ_decompose p
  6. L20
    apply beta_product_succ_decompose
  7. L21
    exact hsource_product
04Establish htarget_decompL22–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product succ decompose.

  1. L22
    have htarget_decomp : ∃ a. ∃ v. BetaAt(z,d,n,a) ∧ (Product(z,d,n,v) ∧ q = v · a)Definitions: BetaAt(z,d,n,a)Product(z,d,n,v)Original native command in the exact edition
  2. L23
    specialize beta_product_succ_decompose z
  3. L24
    specialize beta_product_succ_decompose d
  4. L25
    specialize beta_product_succ_decompose n
  5. L26
    specialize beta_product_succ_decompose q
  6. L27
    apply beta_product_succ_decompose
  7. L28
    exact htarget_product
05Separate the logical casesL29–36

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

  1. L29
    cases hsource_decomp
  2. L30
    cases hsource_decomp_witness
  3. L31
    cases hsource_decomp_witness_witness
  4. L32
    cases hsource_decomp_witness_witness_right
  5. L33
    cases htarget_decomp
  6. L34
    cases htarget_decomp_witness
  7. L35
    cases htarget_decomp_witness_witness
  8. L36
    cases htarget_decomp_witness_witness_right
06Establish htarget_source_lastL37–45

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

  1. L37
    have htarget_source_last : BetaAt(z,d,n,x)Definitions: BetaAt(z,d,n,x)Original native command in the exact edition
  2. L38
    specialize haligned n
  3. L39
    specialize haligned n
  4. L40
    specialize haligned x
  5. L41
    apply haligned
  6. L42
    specialize le_refl (S n)
  7. L43
    exact le_refl
  8. L44
    exact hmap_last
  9. L45
    exact hsource_decomp_witness_witness_left
07Establish hlast_equalL46–54

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L46
    have hlast_equal : x2 = x
  2. L47
    specialize beta_at_unique z
  3. L48
    specialize beta_at_unique d
  4. L49
    specialize beta_at_unique n
  5. L50
    specialize beta_at_unique x2
  6. L51
    specialize beta_at_unique x
  7. L52
    apply beta_at_unique
  8. L53
    exact htarget_decomp_witness_witness_left
  9. L54
    exact htarget_source_last
08Establish hprefixes_equalL55–64

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hprefix equal.

  1. L55
    have hprefixes_equal : x1 = x3
  2. L56
    specialize hprefix_equal x1
  3. L57
    specialize hprefix_equal x3
  4. L58
    apply hprefix_equal
  5. L59
    exact hsource_decomp_witness_witness_right_left
  6. L60
    exact htarget_decomp_witness_witness_right_left
  7. L61
    rewrite hsource_decomp_witness_witness_right_right
  8. L62
    rewrite htarget_decomp_witness_witness_right_right
  9. L63
    rewrite hlast_equal
  10. L64
    rewrite hprefixes_equal
09Calculate and transport equalitiesL65–65

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

  1. L65
    refl

Library-wide reading audit

Original defined command ledger · 65 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro z
  6. 0006intro d
  7. 0007intro n
  8. 0008intro p
  9. 0009intro q
  10. 0010intro haligned
  11. 0011intro hmap_last
  12. 0012intro hsource_product
  13. 0013intro htarget_product
  14. 0014intro hprefix_equal
  15. 0015have hsource_decomp : ∃ a. ∃ u. BetaAt(b,c,n,a) ∧ (Product(b,c,n,u) ∧ p = u · a)
    Exact native replay linehave hsource_decomp : exists a u. (((exists ff_h_fixed_reindex_source_last. ff_h_fixed_reindex_source_last + S (a) = S ((S (n)) * c)) /\ exists ff_q_fixed_reindex_source_last. b = ff_q_fixed_reindex_source_last * S ((S (n)) * c) + (a))) /\ ((exists ff_u_fixed_reindex_source_prefix_witness ff_v_fixed_reindex_source_prefix_witness. ((((exists ff_h_fixed_reindex_source_prefix_witness_start. ff_h_fixed_reindex_source_prefix_witness_start + S (1) = S ((S (0)) * ff_v_fixed_reindex_source_prefix_witness)) /\ exists ff_q_fixed_reindex_source_prefix_witness_start. ff_u_fixed_reindex_source_prefix_witness = ff_q_fixed_reindex_source_prefix_witness_start * S ((S (0)) * ff_v_fixed_reindex_source_prefix_witness) + (1))) /\ ((((exists ff_h_fixed_reindex_source_prefix_witness_terminal. ff_h_fixed_reindex_source_prefix_witness_terminal + S (u) = S ((S (n)) * ff_v_fixed_reindex_source_prefix_witness)) /\ exists ff_q_fixed_reindex_source_prefix_witness_terminal. ff_u_fixed_reindex_source_prefix_witness = ff_q_fixed_reindex_source_prefix_witness_terminal * S ((S (n)) * ff_v_fixed_reindex_source_prefix_witness) + (u))) /\ forall ff_i_fixed_reindex_source_prefix_witness. (exists ff_lt_fixed_reindex_source_prefix_witness_bound. ff_lt_fixed_reindex_source_prefix_witness_bound + S ff_i_fixed_reindex_source_prefix_witness = n) -> exists ff_p_fixed_reindex_source_prefix_witness ff_r_fixed_reindex_source_prefix_witness ff_s_fixed_reindex_source_prefix_witness. ((((exists ff_h_fixed_reindex_source_prefix_witness_factor. ff_h_fixed_reindex_source_prefix_witness_factor + S (ff_p_fixed_reindex_source_prefix_witness) = S ((S (ff_i_fixed_reindex_source_prefix_witness)) * c)) /\ exists ff_q_fixed_reindex_source_prefix_witness_factor. b = ff_q_fixed_reindex_source_prefix_witness_factor * S ((S (ff_i_fixed_reindex_source_prefix_witness)) * c) + (ff_p_fixed_reindex_source_prefix_witness))) /\ ((((exists ff_h_fixed_reindex_source_prefix_witness_partial. ff_h_fixed_reindex_source_prefix_witness_partial + S (ff_r_fixed_reindex_source_prefix_witness) = S ((S (ff_i_fixed_reindex_source_prefix_witness)) * ff_v_fixed_reindex_source_prefix_witness)) /\ exists ff_q_fixed_reindex_source_prefix_witness_partial. ff_u_fixed_reindex_source_prefix_witness = ff_q_fixed_reindex_source_prefix_witness_partial * S ((S (ff_i_fixed_reindex_source_prefix_witness)) * ff_v_fixed_reindex_source_prefix_witness) + (ff_r_fixed_reindex_source_prefix_witness))) /\ ((((exists ff_h_fixed_reindex_source_prefix_witness_successor. ff_h_fixed_reindex_source_prefix_witness_successor + S (ff_s_fixed_reindex_source_prefix_witness) = S ((S (S ff_i_fixed_reindex_source_prefix_witness)) * ff_v_fixed_reindex_source_prefix_witness)) /\ exists ff_q_fixed_reindex_source_prefix_witness_successor. ff_u_fixed_reindex_source_prefix_witness = ff_q_fixed_reindex_source_prefix_witness_successor * S ((S (S ff_i_fixed_reindex_source_prefix_witness)) * ff_v_fixed_reindex_source_prefix_witness) + (ff_s_fixed_reindex_source_prefix_witness))) /\ ff_s_fixed_reindex_source_prefix_witness = ff_r_fixed_reindex_source_prefix_witness * ff_p_fixed_reindex_source_prefix_witness)))))) /\ p = u * a)
  16. 0016specialize beta_product_succ_decompose b
  17. 0017specialize beta_product_succ_decompose c
  18. 0018specialize beta_product_succ_decompose n
  19. 0019specialize beta_product_succ_decompose p
  20. 0020apply beta_product_succ_decompose
  21. 0021exact hsource_product
  22. 0022have htarget_decomp : ∃ a. ∃ v. BetaAt(z,d,n,a) ∧ (Product(z,d,n,v) ∧ q = v · a)
    Exact native replay linehave htarget_decomp : exists a v. (((exists ff_h_fixed_reindex_target_last. ff_h_fixed_reindex_target_last + S (a) = S ((S (n)) * d)) /\ exists ff_q_fixed_reindex_target_last. z = ff_q_fixed_reindex_target_last * S ((S (n)) * d) + (a))) /\ ((exists ff_u_fixed_reindex_target_prefix_witness ff_v_fixed_reindex_target_prefix_witness. ((((exists ff_h_fixed_reindex_target_prefix_witness_start. ff_h_fixed_reindex_target_prefix_witness_start + S (1) = S ((S (0)) * ff_v_fixed_reindex_target_prefix_witness)) /\ exists ff_q_fixed_reindex_target_prefix_witness_start. ff_u_fixed_reindex_target_prefix_witness = ff_q_fixed_reindex_target_prefix_witness_start * S ((S (0)) * ff_v_fixed_reindex_target_prefix_witness) + (1))) /\ ((((exists ff_h_fixed_reindex_target_prefix_witness_terminal. ff_h_fixed_reindex_target_prefix_witness_terminal + S (v) = S ((S (n)) * ff_v_fixed_reindex_target_prefix_witness)) /\ exists ff_q_fixed_reindex_target_prefix_witness_terminal. ff_u_fixed_reindex_target_prefix_witness = ff_q_fixed_reindex_target_prefix_witness_terminal * S ((S (n)) * ff_v_fixed_reindex_target_prefix_witness) + (v))) /\ forall ff_i_fixed_reindex_target_prefix_witness. (exists ff_lt_fixed_reindex_target_prefix_witness_bound. ff_lt_fixed_reindex_target_prefix_witness_bound + S ff_i_fixed_reindex_target_prefix_witness = n) -> exists ff_p_fixed_reindex_target_prefix_witness ff_r_fixed_reindex_target_prefix_witness ff_s_fixed_reindex_target_prefix_witness. ((((exists ff_h_fixed_reindex_target_prefix_witness_factor. ff_h_fixed_reindex_target_prefix_witness_factor + S (ff_p_fixed_reindex_target_prefix_witness) = S ((S (ff_i_fixed_reindex_target_prefix_witness)) * d)) /\ exists ff_q_fixed_reindex_target_prefix_witness_factor. z = ff_q_fixed_reindex_target_prefix_witness_factor * S ((S (ff_i_fixed_reindex_target_prefix_witness)) * d) + (ff_p_fixed_reindex_target_prefix_witness))) /\ ((((exists ff_h_fixed_reindex_target_prefix_witness_partial. ff_h_fixed_reindex_target_prefix_witness_partial + S (ff_r_fixed_reindex_target_prefix_witness) = S ((S (ff_i_fixed_reindex_target_prefix_witness)) * ff_v_fixed_reindex_target_prefix_witness)) /\ exists ff_q_fixed_reindex_target_prefix_witness_partial. ff_u_fixed_reindex_target_prefix_witness = ff_q_fixed_reindex_target_prefix_witness_partial * S ((S (ff_i_fixed_reindex_target_prefix_witness)) * ff_v_fixed_reindex_target_prefix_witness) + (ff_r_fixed_reindex_target_prefix_witness))) /\ ((((exists ff_h_fixed_reindex_target_prefix_witness_successor. ff_h_fixed_reindex_target_prefix_witness_successor + S (ff_s_fixed_reindex_target_prefix_witness) = S ((S (S ff_i_fixed_reindex_target_prefix_witness)) * ff_v_fixed_reindex_target_prefix_witness)) /\ exists ff_q_fixed_reindex_target_prefix_witness_successor. ff_u_fixed_reindex_target_prefix_witness = ff_q_fixed_reindex_target_prefix_witness_successor * S ((S (S ff_i_fixed_reindex_target_prefix_witness)) * ff_v_fixed_reindex_target_prefix_witness) + (ff_s_fixed_reindex_target_prefix_witness))) /\ ff_s_fixed_reindex_target_prefix_witness = ff_r_fixed_reindex_target_prefix_witness * ff_p_fixed_reindex_target_prefix_witness)))))) /\ q = v * a)
  23. 0023specialize beta_product_succ_decompose z
  24. 0024specialize beta_product_succ_decompose d
  25. 0025specialize beta_product_succ_decompose n
  26. 0026specialize beta_product_succ_decompose q
  27. 0027apply beta_product_succ_decompose
  28. 0028exact htarget_product
  29. 0029cases hsource_decomp
  30. 0030cases hsource_decomp_witness
  31. 0031cases hsource_decomp_witness_witness
  32. 0032cases hsource_decomp_witness_witness_right
  33. 0033cases htarget_decomp
  34. 0034cases htarget_decomp_witness
  35. 0035cases htarget_decomp_witness_witness
  36. 0036cases htarget_decomp_witness_witness_right
  37. 0037have htarget_source_last : BetaAt(z,d,n,x)
    Exact native replay linehave htarget_source_last : ((exists ff_h_fixed_target_source_last. ff_h_fixed_target_source_last + S (x) = S ((S (n)) * d)) /\ exists ff_q_fixed_target_source_last. z = ff_q_fixed_target_source_last * S ((S (n)) * d) + (x))
  38. 0038specialize haligned n
  39. 0039specialize haligned n
  40. 0040specialize haligned x
  41. 0041apply haligned
  42. 0042specialize le_refl (S n)
  43. 0043exact le_refl
  44. 0044exact hmap_last
  45. 0045exact hsource_decomp_witness_witness_left
  46. 0046have hlast_equal : x2 = x
  47. 0047specialize beta_at_unique z
  48. 0048specialize beta_at_unique d
  49. 0049specialize beta_at_unique n
  50. 0050specialize beta_at_unique x2
  51. 0051specialize beta_at_unique x
  52. 0052apply beta_at_unique
  53. 0053exact htarget_decomp_witness_witness_left
  54. 0054exact htarget_source_last
  55. 0055have hprefixes_equal : x1 = x3
  56. 0056specialize hprefix_equal x1
  57. 0057specialize hprefix_equal x3
  58. 0058apply hprefix_equal
  59. 0059exact hsource_decomp_witness_witness_right_left
  60. 0060exact htarget_decomp_witness_witness_right_left
  61. 0061rewrite hsource_decomp_witness_witness_right_right
  62. 0062rewrite htarget_decomp_witness_witness_right_right
  63. 0063rewrite hlast_equal
  64. 0064rewrite hprefixes_equal
  65. 0065refl