PA007X — beta_product_permutation

Exact expanded PA statement

forall l r s b c z d p q. (forall fp_i_reindex_bounded. (exists fp_gap_reindex_bounded_index. fp_gap_reindex_bounded_index + S fp_i_reindex_bounded = l) -> exists fp_value_reindex_bounded. ((((exists ff_h_reindex_bounded_entry. ff_h_reindex_bounded_entry + S (fp_value_reindex_bounded) = S ((S (fp_i_reindex_bounded)) * s)) /\ exists ff_q_reindex_bounded_entry. r = ff_q_reindex_bounded_entry * S ((S (fp_i_reindex_bounded)) * s) + (fp_value_reindex_bounded))) /\ (exists fp_gap_reindex_bounded_value. fp_gap_reindex_bounded_value + S fp_value_reindex_bounded = l))) -> (forall fp_i_reindex_injective fp_j_reindex_injective fp_value_reindex_injective. (exists fp_gap_reindex_injective_i. fp_gap_reindex_injective_i + S fp_i_reindex_injective = l) -> (exists fp_gap_reindex_injective_j. fp_gap_reindex_injective_j + S fp_j_reindex_injective = l) -> (((exists ff_h_reindex_injective_left. ff_h_reindex_injective_left + S (fp_value_reindex_injective) = S ((S (fp_i_reindex_injective)) * s)) /\ exists ff_q_reindex_injective_left. r = ff_q_reindex_injective_left * S ((S (fp_i_reindex_injective)) * s) + (fp_value_reindex_injective))) -> (((exists ff_h_reindex_injective_right. ff_h_reindex_injective_right + S (fp_value_reindex_injective) = S ((S (fp_j_reindex_injective)) * s)) /\ exists ff_q_reindex_injective_right. r = ff_q_reindex_injective_right * S ((S (fp_j_reindex_injective)) * s) + (fp_value_reindex_injective))) -> fp_i_reindex_injective = fp_j_reindex_injective) -> (forall fpr_i_reindex_aligned fpr_j_reindex_aligned fpr_x_reindex_aligned. (exists fpr_h_reindex_aligned. fpr_h_reindex_aligned + S fpr_i_reindex_aligned = l) -> (((exists ff_h_reindex_aligned_map. ff_h_reindex_aligned_map + S (fpr_j_reindex_aligned) = S ((S (fpr_i_reindex_aligned)) * s)) /\ exists ff_q_reindex_aligned_map. r = ff_q_reindex_aligned_map * S ((S (fpr_i_reindex_aligned)) * s) + (fpr_j_reindex_aligned))) -> (((exists ff_h_reindex_aligned_source. ff_h_reindex_aligned_source + S (fpr_x_reindex_aligned) = S ((S (fpr_j_reindex_aligned)) * c)) /\ exists ff_q_reindex_aligned_source. b = ff_q_reindex_aligned_source * S ((S (fpr_j_reindex_aligned)) * c) + (fpr_x_reindex_aligned))) -> (((exists ff_h_reindex_aligned_target. ff_h_reindex_aligned_target + S (fpr_x_reindex_aligned) = S ((S (fpr_i_reindex_aligned)) * d)) /\ exists ff_q_reindex_aligned_target. z = ff_q_reindex_aligned_target * S ((S (fpr_i_reindex_aligned)) * d) + (fpr_x_reindex_aligned)))) -> (exists ff_u_reindex_source_product ff_v_reindex_source_product. ((((exists ff_h_reindex_source_product_start. ff_h_reindex_source_product_start + S (1) = S ((S (0)) * ff_v_reindex_source_product)) /\ exists ff_q_reindex_source_product_start. ff_u_reindex_source_product = ff_q_reindex_source_product_start * S ((S (0)) * ff_v_reindex_source_product) + (1))) /\ ((((exists ff_h_reindex_source_product_terminal. ff_h_reindex_source_product_terminal + S (p) = S ((S (l)) * ff_v_reindex_source_product)) /\ exists ff_q_reindex_source_product_terminal. ff_u_reindex_source_product = ff_q_reindex_source_product_terminal * S ((S (l)) * ff_v_reindex_source_product) + (p))) /\ forall ff_i_reindex_source_product. (exists ff_lt_reindex_source_product_bound. ff_lt_reindex_source_product_bound + S ff_i_reindex_source_product = l) -> exists ff_p_reindex_source_product ff_r_reindex_source_product ff_s_reindex_source_product. ((((exists ff_h_reindex_source_product_factor. ff_h_reindex_source_product_factor + S (ff_p_reindex_source_product) = S ((S (ff_i_reindex_source_product)) * c)) /\ exists ff_q_reindex_source_product_factor. b = ff_q_reindex_source_product_factor * S ((S (ff_i_reindex_source_product)) * c) + (ff_p_reindex_source_product))) /\ ((((exists ff_h_reindex_source_product_partial. ff_h_reindex_source_product_partial + S (ff_r_reindex_source_product) = S ((S (ff_i_reindex_source_product)) * ff_v_reindex_source_product)) /\ exists ff_q_reindex_source_product_partial. ff_u_reindex_source_product = ff_q_reindex_source_product_partial * S ((S (ff_i_reindex_source_product)) * ff_v_reindex_source_product) + (ff_r_reindex_source_product))) /\ ((((exists ff_h_reindex_source_product_successor. ff_h_reindex_source_product_successor + S (ff_s_reindex_source_product) = S ((S (S ff_i_reindex_source_product)) * ff_v_reindex_source_product)) /\ exists ff_q_reindex_source_product_successor. ff_u_reindex_source_product = ff_q_reindex_source_product_successor * S ((S (S ff_i_reindex_source_product)) * ff_v_reindex_source_product) + (ff_s_reindex_source_product))) /\ ff_s_reindex_source_product = ff_r_reindex_source_product * ff_p_reindex_source_product)))))) -> (exists ff_u_reindex_target_product ff_v_reindex_target_product. ((((exists ff_h_reindex_target_product_start. ff_h_reindex_target_product_start + S (1) = S ((S (0)) * ff_v_reindex_target_product)) /\ exists ff_q_reindex_target_product_start. ff_u_reindex_target_product = ff_q_reindex_target_product_start * S ((S (0)) * ff_v_reindex_target_product) + (1))) /\ ((((exists ff_h_reindex_target_product_terminal. ff_h_reindex_target_product_terminal + S (q) = S ((S (l)) * ff_v_reindex_target_product)) /\ exists ff_q_reindex_target_product_terminal. ff_u_reindex_target_product = ff_q_reindex_target_product_terminal * S ((S (l)) * ff_v_reindex_target_product) + (q))) /\ forall ff_i_reindex_target_product. (exists ff_lt_reindex_target_product_bound. ff_lt_reindex_target_product_bound + S ff_i_reindex_target_product = l) -> exists ff_p_reindex_target_product ff_r_reindex_target_product ff_s_reindex_target_product. ((((exists ff_h_reindex_target_product_factor. ff_h_reindex_target_product_factor + S (ff_p_reindex_target_product) = S ((S (ff_i_reindex_target_product)) * d)) /\ exists ff_q_reindex_target_product_factor. z = ff_q_reindex_target_product_factor * S ((S (ff_i_reindex_target_product)) * d) + (ff_p_reindex_target_product))) /\ ((((exists ff_h_reindex_target_product_partial. ff_h_reindex_target_product_partial + S (ff_r_reindex_target_product) = S ((S (ff_i_reindex_target_product)) * ff_v_reindex_target_product)) /\ exists ff_q_reindex_target_product_partial. ff_u_reindex_target_product = ff_q_reindex_target_product_partial * S ((S (ff_i_reindex_target_product)) * ff_v_reindex_target_product) + (ff_r_reindex_target_product))) /\ ((((exists ff_h_reindex_target_product_successor. ff_h_reindex_target_product_successor + S (ff_s_reindex_target_product) = S ((S (S ff_i_reindex_target_product)) * ff_v_reindex_target_product)) /\ exists ff_q_reindex_target_product_successor. ff_u_reindex_target_product = ff_q_reindex_target_product_successor * S ((S (S ff_i_reindex_target_product)) * ff_v_reindex_target_product) + (ff_s_reindex_target_product))) /\ ff_s_reindex_target_product = ff_r_reindex_target_product * ff_p_reindex_target_product)))))) -> p = q

Structural proof guide

Generated structural guide

A bounded injective beta-coded reindexing preserves the exact finite product.

Use the direct prerequisites finite_bounded_injective_surjective, finite_lt_succ_eq_or_lt, finite_fixed_last_prefix_bounded, finite_injective_prefix_succ, beta_prefix_swap_last_from_entries, finite_swap_last_bounded, finite_swap_last_injective, beta_product_swap_last_invariant, beta_product_zero, beta_product_exists, beta_at_exists, beta_at_unique, beta_reindex_alignment_swap_last, beta_product_reindex_fixed_last, le_refl, le_succ as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (16), intermediate claims (30), equality transport (4).

Referenced ingredients

PA004W finite_bounded_injective_surjective PA003D finite_lt_succ_eq_or_lt PA004X finite_fixed_last_prefix_bounded PA004Q finite_injective_prefix_succ PA004K beta_prefix_swap_last_from_entries PA004M finite_swap_last_bounded PA004O finite_swap_last_injective PA0053 beta_product_swap_last_invariant PA0049 beta_product_zero PA003X beta_product_exists PA0029 beta_at_exists PA002F beta_at_unique PA0054 beta_reindex_alignment_swap_last PA007W beta_product_reindex_fixed_last PA001A le_refl PA002O le_succ

Proof neighborhood

Direct dependencies

Direct dependents

PA007Y gauss_magnitude_product_eq_half_range PA008J prime_mul_residue_product_balance PA00A1 scaled_pair_order_successor_lift_product_is_factorial PA00BD pair_order_terminal_successor_product_eq_range_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.

0001induction l
0002intro r
0003intro s
0004intro b
0005intro c
0006intro z
0007intro d
0008intro p
0009intro q
0010intro hbounded
0011intro hinjective
0012intro haligned
0013intro hsource_product
0014intro htarget_product
0015have hp : p = 1
0016specialize beta_product_zero b
0017specialize beta_product_zero c
0018specialize beta_product_zero p
0019apply beta_product_zero
0020exact hsource_product
0021have hq : q = 1
0022specialize beta_product_zero z
0023specialize beta_product_zero d
0024specialize beta_product_zero q
0025apply beta_product_zero
0026exact htarget_product
0027trans 1
0028exact hp
0029symm
0030exact hq
0031intro r
0032intro s
0033intro b
0034intro c
0035intro z
0036intro d
0037intro p
0038intro q
0039intro hbounded
0040intro hinjective
0041intro haligned
0042intro hsource_product
0043intro htarget_product
0044have hsurjective : forall fp_value_reindex_surjective_succ. (exists fp_gap_reindex_surjective_succ_value. fp_gap_reindex_surjective_succ_value + S fp_value_reindex_surjective_succ = S l) -> exists fp_i_reindex_surjective_succ. ((exists fp_gap_reindex_surjective_succ_index. fp_gap_reindex_surjective_succ_index + S fp_i_reindex_surjective_succ = S l) /\ (((exists ff_h_reindex_surjective_succ_entry. ff_h_reindex_surjective_succ_entry + S (fp_value_reindex_surjective_succ) = S ((S (fp_i_reindex_surjective_succ)) * s)) /\ exists ff_q_reindex_surjective_succ_entry. r = ff_q_reindex_surjective_succ_entry * S ((S (fp_i_reindex_surjective_succ)) * s) + (fp_value_reindex_surjective_succ))))
0045specialize finite_bounded_injective_surjective (S l)
0046specialize finite_bounded_injective_surjective r
0047specialize finite_bounded_injective_surjective s
0048apply finite_bounded_injective_surjective
0049exact hbounded
0050exact hinjective
0051have hlast_bound : exists h. h + S l = S l
0052specialize le_refl (S l)
0053exact le_refl
0054have hpreimage : exists k. ((exists h. h + S k = S l) /\ (((exists ff_h_reindex_map_preimage. ff_h_reindex_map_preimage + S (l) = S ((S (k)) * s)) /\ exists ff_q_reindex_map_preimage. r = ff_q_reindex_map_preimage * S ((S (k)) * s) + (l))))
0055specialize hsurjective l
0056apply hsurjective
0057exact hlast_bound
0058cases hpreimage
0059cases hpreimage_witness
0060have hsource_last : exists a. (((exists ff_h_reindex_source_last. ff_h_reindex_source_last + S (a) = S ((S (l)) * c)) /\ exists ff_q_reindex_source_last. b = ff_q_reindex_source_last * S ((S (l)) * c) + (a)))
0061specialize beta_at_exists b
0062specialize beta_at_exists c
0063specialize beta_at_exists l
0064exact beta_at_exists
0065cases hsource_last
0066have htarget_at_preimage : ((exists ff_h_reindex_target_preimage. ff_h_reindex_target_preimage + S (x1) = S ((S (x)) * d)) /\ exists ff_q_reindex_target_preimage. z = ff_q_reindex_target_preimage * S ((S (x)) * d) + (x1))
0067specialize haligned x
0068specialize haligned l
0069specialize haligned x1
0070apply haligned
0071exact hpreimage_witness_left
0072exact hpreimage_witness_right
0073exact hsource_last_witness
0074have hsplit : x = l \/ exists h. h + S x = l
0075specialize finite_lt_succ_eq_or_lt l
0076specialize finite_lt_succ_eq_or_lt x
0077apply finite_lt_succ_eq_or_lt
0078exact hpreimage_witness_left
0079cases hsplit
0080have hmap_last : ((exists ff_h_reindex_map_last. ff_h_reindex_map_last + S (l) = S ((S (l)) * s)) /\ exists ff_q_reindex_map_last. r = ff_q_reindex_map_last * S ((S (l)) * s) + (l))
0081rewrite hsplit_left at hpreimage_witness_right
0082rewrite hsplit_left at hpreimage_witness_right
0083exact hpreimage_witness_right
0084have hbounded_prefix : forall fp_i_reindex_bounded_prefix. (exists fp_gap_reindex_bounded_prefix_index. fp_gap_reindex_bounded_prefix_index + S fp_i_reindex_bounded_prefix = l) -> exists fp_value_reindex_bounded_prefix. ((((exists ff_h_reindex_bounded_prefix_entry. ff_h_reindex_bounded_prefix_entry + S (fp_value_reindex_bounded_prefix) = S ((S (fp_i_reindex_bounded_prefix)) * s)) /\ exists ff_q_reindex_bounded_prefix_entry. r = ff_q_reindex_bounded_prefix_entry * S ((S (fp_i_reindex_bounded_prefix)) * s) + (fp_value_reindex_bounded_prefix))) /\ (exists fp_gap_reindex_bounded_prefix_value. fp_gap_reindex_bounded_prefix_value + S fp_value_reindex_bounded_prefix = l))
0085specialize finite_fixed_last_prefix_bounded r
0086specialize finite_fixed_last_prefix_bounded s
0087specialize finite_fixed_last_prefix_bounded l
0088apply finite_fixed_last_prefix_bounded
0089exact hbounded
0090exact hinjective
0091exact hmap_last
0092have hinjective_prefix : forall fp_i_reindex_injective_prefix fp_j_reindex_injective_prefix fp_value_reindex_injective_prefix. (exists fp_gap_reindex_injective_prefix_i. fp_gap_reindex_injective_prefix_i + S fp_i_reindex_injective_prefix = l) -> (exists fp_gap_reindex_injective_prefix_j. fp_gap_reindex_injective_prefix_j + S fp_j_reindex_injective_prefix = l) -> (((exists ff_h_reindex_injective_prefix_left. ff_h_reindex_injective_prefix_left + S (fp_value_reindex_injective_prefix) = S ((S (fp_i_reindex_injective_prefix)) * s)) /\ exists ff_q_reindex_injective_prefix_left. r = ff_q_reindex_injective_prefix_left * S ((S (fp_i_reindex_injective_prefix)) * s) + (fp_value_reindex_injective_prefix))) -> (((exists ff_h_reindex_injective_prefix_right. ff_h_reindex_injective_prefix_right + S (fp_value_reindex_injective_prefix) = S ((S (fp_j_reindex_injective_prefix)) * s)) /\ exists ff_q_reindex_injective_prefix_right. r = ff_q_reindex_injective_prefix_right * S ((S (fp_j_reindex_injective_prefix)) * s) + (fp_value_reindex_injective_prefix))) -> fp_i_reindex_injective_prefix = fp_j_reindex_injective_prefix
0093specialize finite_injective_prefix_succ r
0094specialize finite_injective_prefix_succ s
0095specialize finite_injective_prefix_succ l
0096specialize finite_injective_prefix_succ (S l)
0097apply finite_injective_prefix_succ
0098refl
0099exact hinjective
0100have haligned_prefix : forall fpr_i_reindex_aligned_prefix fpr_j_reindex_aligned_prefix fpr_x_reindex_aligned_prefix. (exists fpr_h_reindex_aligned_prefix. fpr_h_reindex_aligned_prefix + S fpr_i_reindex_aligned_prefix = l) -> (((exists ff_h_reindex_aligned_prefix_map. ff_h_reindex_aligned_prefix_map + S (fpr_j_reindex_aligned_prefix) = S ((S (fpr_i_reindex_aligned_prefix)) * s)) /\ exists ff_q_reindex_aligned_prefix_map. r = ff_q_reindex_aligned_prefix_map * S ((S (fpr_i_reindex_aligned_prefix)) * s) + (fpr_j_reindex_aligned_prefix))) -> (((exists ff_h_reindex_aligned_prefix_source. ff_h_reindex_aligned_prefix_source + S (fpr_x_reindex_aligned_prefix) = S ((S (fpr_j_reindex_aligned_prefix)) * c)) /\ exists ff_q_reindex_aligned_prefix_source. b = ff_q_reindex_aligned_prefix_source * S ((S (fpr_j_reindex_aligned_prefix)) * c) + (fpr_x_reindex_aligned_prefix))) -> (((exists ff_h_reindex_aligned_prefix_target. ff_h_reindex_aligned_prefix_target + S (fpr_x_reindex_aligned_prefix) = S ((S (fpr_i_reindex_aligned_prefix)) * d)) /\ exists ff_q_reindex_aligned_prefix_target. z = ff_q_reindex_aligned_prefix_target * S ((S (fpr_i_reindex_aligned_prefix)) * d) + (fpr_x_reindex_aligned_prefix)))
0101intro i
0102intro j
0103intro a
0104intro hi
0105intro hmap
0106intro hsource
0107specialize haligned i
0108specialize haligned j
0109specialize haligned a
0110apply haligned
0111specialize le_succ (S i)
0112specialize le_succ l
0113apply le_succ
0114exact hi
0115exact hmap
0116exact hsource
0117have hprefix_products_equal : forall u v. (exists ff_u_reindex_source_prefix_product ff_v_reindex_source_prefix_product. ((((exists ff_h_reindex_source_prefix_product_start. ff_h_reindex_source_prefix_product_start + S (1) = S ((S (0)) * ff_v_reindex_source_prefix_product)) /\ exists ff_q_reindex_source_prefix_product_start. ff_u_reindex_source_prefix_product = ff_q_reindex_source_prefix_product_start * S ((S (0)) * ff_v_reindex_source_prefix_product) + (1))) /\ ((((exists ff_h_reindex_source_prefix_product_terminal. ff_h_reindex_source_prefix_product_terminal + S (u) = S ((S (l)) * ff_v_reindex_source_prefix_product)) /\ exists ff_q_reindex_source_prefix_product_terminal. ff_u_reindex_source_prefix_product = ff_q_reindex_source_prefix_product_terminal * S ((S (l)) * ff_v_reindex_source_prefix_product) + (u))) /\ forall ff_i_reindex_source_prefix_product. (exists ff_lt_reindex_source_prefix_product_bound. ff_lt_reindex_source_prefix_product_bound + S ff_i_reindex_source_prefix_product = l) -> exists ff_p_reindex_source_prefix_product ff_r_reindex_source_prefix_product ff_s_reindex_source_prefix_product. ((((exists ff_h_reindex_source_prefix_product_factor. ff_h_reindex_source_prefix_product_factor + S (ff_p_reindex_source_prefix_product) = S ((S (ff_i_reindex_source_prefix_product)) * c)) /\ exists ff_q_reindex_source_prefix_product_factor. b = ff_q_reindex_source_prefix_product_factor * S ((S (ff_i_reindex_source_prefix_product)) * c) + (ff_p_reindex_source_prefix_product))) /\ ((((exists ff_h_reindex_source_prefix_product_partial. ff_h_reindex_source_prefix_product_partial + S (ff_r_reindex_source_prefix_product) = S ((S (ff_i_reindex_source_prefix_product)) * ff_v_reindex_source_prefix_product)) /\ exists ff_q_reindex_source_prefix_product_partial. ff_u_reindex_source_prefix_product = ff_q_reindex_source_prefix_product_partial * S ((S (ff_i_reindex_source_prefix_product)) * ff_v_reindex_source_prefix_product) + (ff_r_reindex_source_prefix_product))) /\ ((((exists ff_h_reindex_source_prefix_product_successor. ff_h_reindex_source_prefix_product_successor + S (ff_s_reindex_source_prefix_product) = S ((S (S ff_i_reindex_source_prefix_product)) * ff_v_reindex_source_prefix_product)) /\ exists ff_q_reindex_source_prefix_product_successor. ff_u_reindex_source_prefix_product = ff_q_reindex_source_prefix_product_successor * S ((S (S ff_i_reindex_source_prefix_product)) * ff_v_reindex_source_prefix_product) + (ff_s_reindex_source_prefix_product))) /\ ff_s_reindex_source_prefix_product = ff_r_reindex_source_prefix_product * ff_p_reindex_source_prefix_product)))))) -> (exists ff_u_reindex_target_prefix_product ff_v_reindex_target_prefix_product. ((((exists ff_h_reindex_target_prefix_product_start. ff_h_reindex_target_prefix_product_start + S (1) = S ((S (0)) * ff_v_reindex_target_prefix_product)) /\ exists ff_q_reindex_target_prefix_product_start. ff_u_reindex_target_prefix_product = ff_q_reindex_target_prefix_product_start * S ((S (0)) * ff_v_reindex_target_prefix_product) + (1))) /\ ((((exists ff_h_reindex_target_prefix_product_terminal. ff_h_reindex_target_prefix_product_terminal + S (v) = S ((S (l)) * ff_v_reindex_target_prefix_product)) /\ exists ff_q_reindex_target_prefix_product_terminal. ff_u_reindex_target_prefix_product = ff_q_reindex_target_prefix_product_terminal * S ((S (l)) * ff_v_reindex_target_prefix_product) + (v))) /\ forall ff_i_reindex_target_prefix_product. (exists ff_lt_reindex_target_prefix_product_bound. ff_lt_reindex_target_prefix_product_bound + S ff_i_reindex_target_prefix_product = l) -> exists ff_p_reindex_target_prefix_product ff_r_reindex_target_prefix_product ff_s_reindex_target_prefix_product. ((((exists ff_h_reindex_target_prefix_product_factor. ff_h_reindex_target_prefix_product_factor + S (ff_p_reindex_target_prefix_product) = S ((S (ff_i_reindex_target_prefix_product)) * d)) /\ exists ff_q_reindex_target_prefix_product_factor. z = ff_q_reindex_target_prefix_product_factor * S ((S (ff_i_reindex_target_prefix_product)) * d) + (ff_p_reindex_target_prefix_product))) /\ ((((exists ff_h_reindex_target_prefix_product_partial. ff_h_reindex_target_prefix_product_partial + S (ff_r_reindex_target_prefix_product) = S ((S (ff_i_reindex_target_prefix_product)) * ff_v_reindex_target_prefix_product)) /\ exists ff_q_reindex_target_prefix_product_partial. ff_u_reindex_target_prefix_product = ff_q_reindex_target_prefix_product_partial * S ((S (ff_i_reindex_target_prefix_product)) * ff_v_reindex_target_prefix_product) + (ff_r_reindex_target_prefix_product))) /\ ((((exists ff_h_reindex_target_prefix_product_successor. ff_h_reindex_target_prefix_product_successor + S (ff_s_reindex_target_prefix_product) = S ((S (S ff_i_reindex_target_prefix_product)) * ff_v_reindex_target_prefix_product)) /\ exists ff_q_reindex_target_prefix_product_successor. ff_u_reindex_target_prefix_product = ff_q_reindex_target_prefix_product_successor * S ((S (S ff_i_reindex_target_prefix_product)) * ff_v_reindex_target_prefix_product) + (ff_s_reindex_target_prefix_product))) /\ ff_s_reindex_target_prefix_product = ff_r_reindex_target_prefix_product * ff_p_reindex_target_prefix_product)))))) -> u = v
0118intro u
0119intro v
0120intro hsource_prefix_product
0121intro htarget_prefix_product
0122specialize IH r
0123specialize IH s
0124specialize IH b
0125specialize IH c
0126specialize IH z
0127specialize IH d
0128specialize IH u
0129specialize IH v
0130apply IH
0131exact hbounded_prefix
0132exact hinjective_prefix
0133exact haligned_prefix
0134exact hsource_prefix_product
0135exact htarget_prefix_product
0136specialize beta_product_reindex_fixed_last r
0137specialize beta_product_reindex_fixed_last s
0138specialize beta_product_reindex_fixed_last b
0139specialize beta_product_reindex_fixed_last c
0140specialize beta_product_reindex_fixed_last z
0141specialize beta_product_reindex_fixed_last d
0142specialize beta_product_reindex_fixed_last l
0143specialize beta_product_reindex_fixed_last p
0144specialize beta_product_reindex_fixed_last q
0145apply beta_product_reindex_fixed_last
0146exact haligned
0147exact hmap_last
0148exact hsource_product
0149exact htarget_product
0150exact hprefix_products_equal
0151have hmap_last_decoded : exists m. (((exists ff_h_reindex_map_decoded_last. ff_h_reindex_map_decoded_last + S (m) = S ((S (l)) * s)) /\ exists ff_q_reindex_map_decoded_last. r = ff_q_reindex_map_decoded_last * S ((S (l)) * s) + (m)))
0152specialize beta_at_exists r
0153specialize beta_at_exists s
0154specialize beta_at_exists l
0155exact beta_at_exists
0156cases hmap_last_decoded
0157have htarget_last_decoded : exists w. (((exists ff_h_reindex_target_decoded_last. ff_h_reindex_target_decoded_last + S (w) = S ((S (l)) * d)) /\ exists ff_q_reindex_target_decoded_last. z = ff_q_reindex_target_decoded_last * S ((S (l)) * d) + (w)))
0158specialize beta_at_exists z
0159specialize beta_at_exists d
0160specialize beta_at_exists l
0161exact beta_at_exists
0162cases htarget_last_decoded
0163have hmap_swap : exists rm sm. (((exists ff_h_reindex_map_swap_i. ff_h_reindex_map_swap_i + S (x2) = S ((S (x)) * sm)) /\ exists ff_q_reindex_map_swap_i. rm = ff_q_reindex_map_swap_i * S ((S (x)) * sm) + (x2))) /\ ((((exists ff_h_reindex_map_swap_last. ff_h_reindex_map_swap_last + S (l) = S ((S (l)) * sm)) /\ exists ff_q_reindex_map_swap_last. rm = ff_q_reindex_map_swap_last * S ((S (l)) * sm) + (l))) /\ forall j a. (exists h. h + S j = S l) -> ~(j = x) -> ~(j = l) -> (((exists ff_h_reindex_map_swap_old. ff_h_reindex_map_swap_old + S (a) = S ((S (j)) * s)) /\ exists ff_q_reindex_map_swap_old. r = ff_q_reindex_map_swap_old * S ((S (j)) * s) + (a))) -> (((exists ff_h_reindex_map_swap_new. ff_h_reindex_map_swap_new + S (a) = S ((S (j)) * sm)) /\ exists ff_q_reindex_map_swap_new. rm = ff_q_reindex_map_swap_new * S ((S (j)) * sm) + (a))))
0164specialize beta_prefix_swap_last_from_entries r
0165specialize beta_prefix_swap_last_from_entries s
0166specialize beta_prefix_swap_last_from_entries l
0167specialize beta_prefix_swap_last_from_entries x
0168specialize beta_prefix_swap_last_from_entries l
0169specialize beta_prefix_swap_last_from_entries x2
0170apply beta_prefix_swap_last_from_entries
0171exact hsplit_right
0172exact hpreimage_witness_right
0173exact hmap_last_decoded_witness
0174cases hmap_swap
0175cases hmap_swap_witness
0176cases hmap_swap_witness_witness
0177cases hmap_swap_witness_witness_right
0178have htarget_swap : exists tz td. (((exists ff_h_reindex_target_swap_i. ff_h_reindex_target_swap_i + S (x3) = S ((S (x)) * td)) /\ exists ff_q_reindex_target_swap_i. tz = ff_q_reindex_target_swap_i * S ((S (x)) * td) + (x3))) /\ ((((exists ff_h_reindex_target_swap_last. ff_h_reindex_target_swap_last + S (x1) = S ((S (l)) * td)) /\ exists ff_q_reindex_target_swap_last. tz = ff_q_reindex_target_swap_last * S ((S (l)) * td) + (x1))) /\ forall j a. (exists h. h + S j = S l) -> ~(j = x) -> ~(j = l) -> (((exists ff_h_reindex_target_swap_old. ff_h_reindex_target_swap_old + S (a) = S ((S (j)) * d)) /\ exists ff_q_reindex_target_swap_old. z = ff_q_reindex_target_swap_old * S ((S (j)) * d) + (a))) -> (((exists ff_h_reindex_target_swap_new. ff_h_reindex_target_swap_new + S (a) = S ((S (j)) * td)) /\ exists ff_q_reindex_target_swap_new. tz = ff_q_reindex_target_swap_new * S ((S (j)) * td) + (a))))
0179specialize beta_prefix_swap_last_from_entries z
0180specialize beta_prefix_swap_last_from_entries d
0181specialize beta_prefix_swap_last_from_entries l
0182specialize beta_prefix_swap_last_from_entries x
0183specialize beta_prefix_swap_last_from_entries x1
0184specialize beta_prefix_swap_last_from_entries x3
0185apply beta_prefix_swap_last_from_entries
0186exact hsplit_right
0187exact htarget_at_preimage
0188exact htarget_last_decoded_witness
0189cases htarget_swap
0190cases htarget_swap_witness
0191cases htarget_swap_witness_witness
0192cases htarget_swap_witness_witness_right
0193have hswapped_bounded : forall fp_i_reindex_swapped_bounded. (exists fp_gap_reindex_swapped_bounded_index. fp_gap_reindex_swapped_bounded_index + S fp_i_reindex_swapped_bounded = S l) -> exists fp_value_reindex_swapped_bounded. ((((exists ff_h_reindex_swapped_bounded_entry. ff_h_reindex_swapped_bounded_entry + S (fp_value_reindex_swapped_bounded) = S ((S (fp_i_reindex_swapped_bounded)) * x5)) /\ exists ff_q_reindex_swapped_bounded_entry. x4 = ff_q_reindex_swapped_bounded_entry * S ((S (fp_i_reindex_swapped_bounded)) * x5) + (fp_value_reindex_swapped_bounded))) /\ (exists fp_gap_reindex_swapped_bounded_value. fp_gap_reindex_swapped_bounded_value + S fp_value_reindex_swapped_bounded = S l))
0194specialize finite_swap_last_bounded r
0195specialize finite_swap_last_bounded s
0196specialize finite_swap_last_bounded x4
0197specialize finite_swap_last_bounded x5
0198specialize finite_swap_last_bounded l
0199specialize finite_swap_last_bounded (S l)
0200specialize finite_swap_last_bounded x
0201specialize finite_swap_last_bounded l
0202specialize finite_swap_last_bounded x2
0203apply finite_swap_last_bounded
0204refl
0205exact hsplit_right
0206exact hbounded
0207exact hpreimage_witness_right
0208exact hmap_last_decoded_witness
0209exact hmap_swap_witness_witness_left
0210exact hmap_swap_witness_witness_right_left
0211exact hmap_swap_witness_witness_right_right
0212have hswapped_injective : forall fp_i_reindex_swapped_injective fp_j_reindex_swapped_injective fp_value_reindex_swapped_injective. (exists fp_gap_reindex_swapped_injective_i. fp_gap_reindex_swapped_injective_i + S fp_i_reindex_swapped_injective = S l) -> (exists fp_gap_reindex_swapped_injective_j. fp_gap_reindex_swapped_injective_j + S fp_j_reindex_swapped_injective = S l) -> (((exists ff_h_reindex_swapped_injective_left. ff_h_reindex_swapped_injective_left + S (fp_value_reindex_swapped_injective) = S ((S (fp_i_reindex_swapped_injective)) * x5)) /\ exists ff_q_reindex_swapped_injective_left. x4 = ff_q_reindex_swapped_injective_left * S ((S (fp_i_reindex_swapped_injective)) * x5) + (fp_value_reindex_swapped_injective))) -> (((exists ff_h_reindex_swapped_injective_right. ff_h_reindex_swapped_injective_right + S (fp_value_reindex_swapped_injective) = S ((S (fp_j_reindex_swapped_injective)) * x5)) /\ exists ff_q_reindex_swapped_injective_right. x4 = ff_q_reindex_swapped_injective_right * S ((S (fp_j_reindex_swapped_injective)) * x5) + (fp_value_reindex_swapped_injective))) -> fp_i_reindex_swapped_injective = fp_j_reindex_swapped_injective
0213specialize finite_swap_last_injective r
0214specialize finite_swap_last_injective s
0215specialize finite_swap_last_injective x4
0216specialize finite_swap_last_injective x5
0217specialize finite_swap_last_injective l
0218specialize finite_swap_last_injective (S l)
0219specialize finite_swap_last_injective x
0220specialize finite_swap_last_injective l
0221specialize finite_swap_last_injective x2
0222apply finite_swap_last_injective
0223refl
0224exact hsplit_right
0225exact hinjective
0226exact hpreimage_witness_right
0227exact hmap_last_decoded_witness
0228exact hmap_swap_witness_witness_left
0229exact hmap_swap_witness_witness_right_left
0230exact hmap_swap_witness_witness_right_right
0231have hswapped_target_product_exists : exists t. (exists ff_u_reindex_swapped_target_exists ff_v_reindex_swapped_target_exists. ((((exists ff_h_reindex_swapped_target_exists_start. ff_h_reindex_swapped_target_exists_start + S (1) = S ((S (0)) * ff_v_reindex_swapped_target_exists)) /\ exists ff_q_reindex_swapped_target_exists_start. ff_u_reindex_swapped_target_exists = ff_q_reindex_swapped_target_exists_start * S ((S (0)) * ff_v_reindex_swapped_target_exists) + (1))) /\ ((((exists ff_h_reindex_swapped_target_exists_terminal. ff_h_reindex_swapped_target_exists_terminal + S (t) = S ((S (S l)) * ff_v_reindex_swapped_target_exists)) /\ exists ff_q_reindex_swapped_target_exists_terminal. ff_u_reindex_swapped_target_exists = ff_q_reindex_swapped_target_exists_terminal * S ((S (S l)) * ff_v_reindex_swapped_target_exists) + (t))) /\ forall ff_i_reindex_swapped_target_exists. (exists ff_lt_reindex_swapped_target_exists_bound. ff_lt_reindex_swapped_target_exists_bound + S ff_i_reindex_swapped_target_exists = S l) -> exists ff_p_reindex_swapped_target_exists ff_r_reindex_swapped_target_exists ff_s_reindex_swapped_target_exists. ((((exists ff_h_reindex_swapped_target_exists_factor. ff_h_reindex_swapped_target_exists_factor + S (ff_p_reindex_swapped_target_exists) = S ((S (ff_i_reindex_swapped_target_exists)) * x7)) /\ exists ff_q_reindex_swapped_target_exists_factor. x6 = ff_q_reindex_swapped_target_exists_factor * S ((S (ff_i_reindex_swapped_target_exists)) * x7) + (ff_p_reindex_swapped_target_exists))) /\ ((((exists ff_h_reindex_swapped_target_exists_partial. ff_h_reindex_swapped_target_exists_partial + S (ff_r_reindex_swapped_target_exists) = S ((S (ff_i_reindex_swapped_target_exists)) * ff_v_reindex_swapped_target_exists)) /\ exists ff_q_reindex_swapped_target_exists_partial. ff_u_reindex_swapped_target_exists = ff_q_reindex_swapped_target_exists_partial * S ((S (ff_i_reindex_swapped_target_exists)) * ff_v_reindex_swapped_target_exists) + (ff_r_reindex_swapped_target_exists))) /\ ((((exists ff_h_reindex_swapped_target_exists_successor. ff_h_reindex_swapped_target_exists_successor + S (ff_s_reindex_swapped_target_exists) = S ((S (S ff_i_reindex_swapped_target_exists)) * ff_v_reindex_swapped_target_exists)) /\ exists ff_q_reindex_swapped_target_exists_successor. ff_u_reindex_swapped_target_exists = ff_q_reindex_swapped_target_exists_successor * S ((S (S ff_i_reindex_swapped_target_exists)) * ff_v_reindex_swapped_target_exists) + (ff_s_reindex_swapped_target_exists))) /\ ff_s_reindex_swapped_target_exists = ff_r_reindex_swapped_target_exists * ff_p_reindex_swapped_target_exists))))))
0232specialize beta_product_exists x6
0233specialize beta_product_exists x7
0234specialize beta_product_exists (S l)
0235exact beta_product_exists
0236cases hswapped_target_product_exists
0237have htarget_product_swap : q = x8
0238specialize beta_product_swap_last_invariant z
0239specialize beta_product_swap_last_invariant d
0240specialize beta_product_swap_last_invariant x6
0241specialize beta_product_swap_last_invariant x7
0242specialize beta_product_swap_last_invariant l
0243specialize beta_product_swap_last_invariant x
0244specialize beta_product_swap_last_invariant x1
0245specialize beta_product_swap_last_invariant x3
0246specialize beta_product_swap_last_invariant q
0247specialize beta_product_swap_last_invariant x8
0248apply beta_product_swap_last_invariant
0249exact hsplit_right
0250exact htarget_at_preimage
0251exact htarget_last_decoded_witness
0252exact htarget_swap_witness_witness_left
0253exact htarget_swap_witness_witness_right_left
0254exact htarget_swap_witness_witness_right_right
0255exact htarget_product
0256exact hswapped_target_product_exists_witness
0257have hsource_at_map_last : ((exists ff_h_reindex_source_at_map_last. ff_h_reindex_source_at_map_last + S (x3) = S ((S (x2)) * c)) /\ exists ff_q_reindex_source_at_map_last. b = ff_q_reindex_source_at_map_last * S ((S (x2)) * c) + (x3))
0258specialize beta_at_exists b
0259specialize beta_at_exists c
0260specialize beta_at_exists x2
0261cases beta_at_exists
0262have htarget_from_map_last : ((exists ff_h_reindex_target_from_map_last. ff_h_reindex_target_from_map_last + S (x9) = S ((S (l)) * d)) /\ exists ff_q_reindex_target_from_map_last. z = ff_q_reindex_target_from_map_last * S ((S (l)) * d) + (x9))
0263specialize haligned l
0264specialize haligned x2
0265specialize haligned x9
0266apply haligned
0267exact hlast_bound
0268exact hmap_last_decoded_witness
0269exact beta_at_exists_witness
0270have hmap_last_value : x9 = x3
0271specialize beta_at_unique z
0272specialize beta_at_unique d
0273specialize beta_at_unique l
0274specialize beta_at_unique x9
0275specialize beta_at_unique x3
0276apply beta_at_unique
0277exact htarget_from_map_last
0278exact htarget_last_decoded_witness
0279rewrite hmap_last_value at beta_at_exists_witness
0280rewrite hmap_last_value at beta_at_exists_witness
0281exact beta_at_exists_witness
0282have hswapped_aligned : forall fpr_i_reindex_swapped_aligned fpr_j_reindex_swapped_aligned fpr_x_reindex_swapped_aligned. (exists fpr_h_reindex_swapped_aligned. fpr_h_reindex_swapped_aligned + S fpr_i_reindex_swapped_aligned = S l) -> (((exists ff_h_reindex_swapped_aligned_map. ff_h_reindex_swapped_aligned_map + S (fpr_j_reindex_swapped_aligned) = S ((S (fpr_i_reindex_swapped_aligned)) * x5)) /\ exists ff_q_reindex_swapped_aligned_map. x4 = ff_q_reindex_swapped_aligned_map * S ((S (fpr_i_reindex_swapped_aligned)) * x5) + (fpr_j_reindex_swapped_aligned))) -> (((exists ff_h_reindex_swapped_aligned_source. ff_h_reindex_swapped_aligned_source + S (fpr_x_reindex_swapped_aligned) = S ((S (fpr_j_reindex_swapped_aligned)) * c)) /\ exists ff_q_reindex_swapped_aligned_source. b = ff_q_reindex_swapped_aligned_source * S ((S (fpr_j_reindex_swapped_aligned)) * c) + (fpr_x_reindex_swapped_aligned))) -> (((exists ff_h_reindex_swapped_aligned_target. ff_h_reindex_swapped_aligned_target + S (fpr_x_reindex_swapped_aligned) = S ((S (fpr_i_reindex_swapped_aligned)) * x7)) /\ exists ff_q_reindex_swapped_aligned_target. x6 = ff_q_reindex_swapped_aligned_target * S ((S (fpr_i_reindex_swapped_aligned)) * x7) + (fpr_x_reindex_swapped_aligned)))
0283specialize beta_reindex_alignment_swap_last r
0284specialize beta_reindex_alignment_swap_last s
0285specialize beta_reindex_alignment_swap_last x4
0286specialize beta_reindex_alignment_swap_last x5
0287specialize beta_reindex_alignment_swap_last b
0288specialize beta_reindex_alignment_swap_last c
0289specialize beta_reindex_alignment_swap_last z
0290specialize beta_reindex_alignment_swap_last d
0291specialize beta_reindex_alignment_swap_last x6
0292specialize beta_reindex_alignment_swap_last x7
0293specialize beta_reindex_alignment_swap_last l
0294specialize beta_reindex_alignment_swap_last x
0295specialize beta_reindex_alignment_swap_last x2
0296specialize beta_reindex_alignment_swap_last x1
0297specialize beta_reindex_alignment_swap_last x3
0298apply beta_reindex_alignment_swap_last
0299exact hmap_swap_witness_witness_left
0300exact hmap_swap_witness_witness_right_left
0301exact hmap_swap_witness_witness_right_right
0302exact hsource_at_map_last
0303exact hsource_last_witness
0304exact htarget_swap_witness_witness_left
0305exact htarget_swap_witness_witness_right_left
0306exact htarget_swap_witness_witness_right_right
0307exact haligned
0308have hswapped_bounded_prefix : forall fp_i_reindex_swapped_bounded_prefix. (exists fp_gap_reindex_swapped_bounded_prefix_index. fp_gap_reindex_swapped_bounded_prefix_index + S fp_i_reindex_swapped_bounded_prefix = l) -> exists fp_value_reindex_swapped_bounded_prefix. ((((exists ff_h_reindex_swapped_bounded_prefix_entry. ff_h_reindex_swapped_bounded_prefix_entry + S (fp_value_reindex_swapped_bounded_prefix) = S ((S (fp_i_reindex_swapped_bounded_prefix)) * x5)) /\ exists ff_q_reindex_swapped_bounded_prefix_entry. x4 = ff_q_reindex_swapped_bounded_prefix_entry * S ((S (fp_i_reindex_swapped_bounded_prefix)) * x5) + (fp_value_reindex_swapped_bounded_prefix))) /\ (exists fp_gap_reindex_swapped_bounded_prefix_value. fp_gap_reindex_swapped_bounded_prefix_value + S fp_value_reindex_swapped_bounded_prefix = l))
0309specialize finite_fixed_last_prefix_bounded x4
0310specialize finite_fixed_last_prefix_bounded x5
0311specialize finite_fixed_last_prefix_bounded l
0312apply finite_fixed_last_prefix_bounded
0313exact hswapped_bounded
0314exact hswapped_injective
0315exact hmap_swap_witness_witness_right_left
0316have hswapped_injective_prefix : forall fp_i_reindex_swapped_injective_prefix fp_j_reindex_swapped_injective_prefix fp_value_reindex_swapped_injective_prefix. (exists fp_gap_reindex_swapped_injective_prefix_i. fp_gap_reindex_swapped_injective_prefix_i + S fp_i_reindex_swapped_injective_prefix = l) -> (exists fp_gap_reindex_swapped_injective_prefix_j. fp_gap_reindex_swapped_injective_prefix_j + S fp_j_reindex_swapped_injective_prefix = l) -> (((exists ff_h_reindex_swapped_injective_prefix_left. ff_h_reindex_swapped_injective_prefix_left + S (fp_value_reindex_swapped_injective_prefix) = S ((S (fp_i_reindex_swapped_injective_prefix)) * x5)) /\ exists ff_q_reindex_swapped_injective_prefix_left. x4 = ff_q_reindex_swapped_injective_prefix_left * S ((S (fp_i_reindex_swapped_injective_prefix)) * x5) + (fp_value_reindex_swapped_injective_prefix))) -> (((exists ff_h_reindex_swapped_injective_prefix_right. ff_h_reindex_swapped_injective_prefix_right + S (fp_value_reindex_swapped_injective_prefix) = S ((S (fp_j_reindex_swapped_injective_prefix)) * x5)) /\ exists ff_q_reindex_swapped_injective_prefix_right. x4 = ff_q_reindex_swapped_injective_prefix_right * S ((S (fp_j_reindex_swapped_injective_prefix)) * x5) + (fp_value_reindex_swapped_injective_prefix))) -> fp_i_reindex_swapped_injective_prefix = fp_j_reindex_swapped_injective_prefix
0317specialize finite_injective_prefix_succ x4
0318specialize finite_injective_prefix_succ x5
0319specialize finite_injective_prefix_succ l
0320specialize finite_injective_prefix_succ (S l)
0321apply finite_injective_prefix_succ
0322refl
0323exact hswapped_injective
0324have hswapped_aligned_prefix : forall fpr_i_reindex_swapped_aligned_prefix fpr_j_reindex_swapped_aligned_prefix fpr_x_reindex_swapped_aligned_prefix. (exists fpr_h_reindex_swapped_aligned_prefix. fpr_h_reindex_swapped_aligned_prefix + S fpr_i_reindex_swapped_aligned_prefix = l) -> (((exists ff_h_reindex_swapped_aligned_prefix_map. ff_h_reindex_swapped_aligned_prefix_map + S (fpr_j_reindex_swapped_aligned_prefix) = S ((S (fpr_i_reindex_swapped_aligned_prefix)) * x5)) /\ exists ff_q_reindex_swapped_aligned_prefix_map. x4 = ff_q_reindex_swapped_aligned_prefix_map * S ((S (fpr_i_reindex_swapped_aligned_prefix)) * x5) + (fpr_j_reindex_swapped_aligned_prefix))) -> (((exists ff_h_reindex_swapped_aligned_prefix_source. ff_h_reindex_swapped_aligned_prefix_source + S (fpr_x_reindex_swapped_aligned_prefix) = S ((S (fpr_j_reindex_swapped_aligned_prefix)) * c)) /\ exists ff_q_reindex_swapped_aligned_prefix_source. b = ff_q_reindex_swapped_aligned_prefix_source * S ((S (fpr_j_reindex_swapped_aligned_prefix)) * c) + (fpr_x_reindex_swapped_aligned_prefix))) -> (((exists ff_h_reindex_swapped_aligned_prefix_target. ff_h_reindex_swapped_aligned_prefix_target + S (fpr_x_reindex_swapped_aligned_prefix) = S ((S (fpr_i_reindex_swapped_aligned_prefix)) * x7)) /\ exists ff_q_reindex_swapped_aligned_prefix_target. x6 = ff_q_reindex_swapped_aligned_prefix_target * S ((S (fpr_i_reindex_swapped_aligned_prefix)) * x7) + (fpr_x_reindex_swapped_aligned_prefix)))
0325intro i
0326intro j
0327intro a
0328intro hi
0329intro hmap
0330intro hsource
0331specialize hswapped_aligned i
0332specialize hswapped_aligned j
0333specialize hswapped_aligned a
0334apply hswapped_aligned
0335specialize le_succ (S i)
0336specialize le_succ l
0337apply le_succ
0338exact hi
0339exact hmap
0340exact hsource
0341have hswapped_prefix_products_equal : forall u v. (exists ff_u_reindex_source_prefix_product ff_v_reindex_source_prefix_product. ((((exists ff_h_reindex_source_prefix_product_start. ff_h_reindex_source_prefix_product_start + S (1) = S ((S (0)) * ff_v_reindex_source_prefix_product)) /\ exists ff_q_reindex_source_prefix_product_start. ff_u_reindex_source_prefix_product = ff_q_reindex_source_prefix_product_start * S ((S (0)) * ff_v_reindex_source_prefix_product) + (1))) /\ ((((exists ff_h_reindex_source_prefix_product_terminal. ff_h_reindex_source_prefix_product_terminal + S (u) = S ((S (l)) * ff_v_reindex_source_prefix_product)) /\ exists ff_q_reindex_source_prefix_product_terminal. ff_u_reindex_source_prefix_product = ff_q_reindex_source_prefix_product_terminal * S ((S (l)) * ff_v_reindex_source_prefix_product) + (u))) /\ forall ff_i_reindex_source_prefix_product. (exists ff_lt_reindex_source_prefix_product_bound. ff_lt_reindex_source_prefix_product_bound + S ff_i_reindex_source_prefix_product = l) -> exists ff_p_reindex_source_prefix_product ff_r_reindex_source_prefix_product ff_s_reindex_source_prefix_product. ((((exists ff_h_reindex_source_prefix_product_factor. ff_h_reindex_source_prefix_product_factor + S (ff_p_reindex_source_prefix_product) = S ((S (ff_i_reindex_source_prefix_product)) * c)) /\ exists ff_q_reindex_source_prefix_product_factor. b = ff_q_reindex_source_prefix_product_factor * S ((S (ff_i_reindex_source_prefix_product)) * c) + (ff_p_reindex_source_prefix_product))) /\ ((((exists ff_h_reindex_source_prefix_product_partial. ff_h_reindex_source_prefix_product_partial + S (ff_r_reindex_source_prefix_product) = S ((S (ff_i_reindex_source_prefix_product)) * ff_v_reindex_source_prefix_product)) /\ exists ff_q_reindex_source_prefix_product_partial. ff_u_reindex_source_prefix_product = ff_q_reindex_source_prefix_product_partial * S ((S (ff_i_reindex_source_prefix_product)) * ff_v_reindex_source_prefix_product) + (ff_r_reindex_source_prefix_product))) /\ ((((exists ff_h_reindex_source_prefix_product_successor. ff_h_reindex_source_prefix_product_successor + S (ff_s_reindex_source_prefix_product) = S ((S (S ff_i_reindex_source_prefix_product)) * ff_v_reindex_source_prefix_product)) /\ exists ff_q_reindex_source_prefix_product_successor. ff_u_reindex_source_prefix_product = ff_q_reindex_source_prefix_product_successor * S ((S (S ff_i_reindex_source_prefix_product)) * ff_v_reindex_source_prefix_product) + (ff_s_reindex_source_prefix_product))) /\ ff_s_reindex_source_prefix_product = ff_r_reindex_source_prefix_product * ff_p_reindex_source_prefix_product)))))) -> (exists ff_u_reindex_swapped_target_prefix_product ff_v_reindex_swapped_target_prefix_product. ((((exists ff_h_reindex_swapped_target_prefix_product_start. ff_h_reindex_swapped_target_prefix_product_start + S (1) = S ((S (0)) * ff_v_reindex_swapped_target_prefix_product)) /\ exists ff_q_reindex_swapped_target_prefix_product_start. ff_u_reindex_swapped_target_prefix_product = ff_q_reindex_swapped_target_prefix_product_start * S ((S (0)) * ff_v_reindex_swapped_target_prefix_product) + (1))) /\ ((((exists ff_h_reindex_swapped_target_prefix_product_terminal. ff_h_reindex_swapped_target_prefix_product_terminal + S (v) = S ((S (l)) * ff_v_reindex_swapped_target_prefix_product)) /\ exists ff_q_reindex_swapped_target_prefix_product_terminal. ff_u_reindex_swapped_target_prefix_product = ff_q_reindex_swapped_target_prefix_product_terminal * S ((S (l)) * ff_v_reindex_swapped_target_prefix_product) + (v))) /\ forall ff_i_reindex_swapped_target_prefix_product. (exists ff_lt_reindex_swapped_target_prefix_product_bound. ff_lt_reindex_swapped_target_prefix_product_bound + S ff_i_reindex_swapped_target_prefix_product = l) -> exists ff_p_reindex_swapped_target_prefix_product ff_r_reindex_swapped_target_prefix_product ff_s_reindex_swapped_target_prefix_product. ((((exists ff_h_reindex_swapped_target_prefix_product_factor. ff_h_reindex_swapped_target_prefix_product_factor + S (ff_p_reindex_swapped_target_prefix_product) = S ((S (ff_i_reindex_swapped_target_prefix_product)) * x7)) /\ exists ff_q_reindex_swapped_target_prefix_product_factor. x6 = ff_q_reindex_swapped_target_prefix_product_factor * S ((S (ff_i_reindex_swapped_target_prefix_product)) * x7) + (ff_p_reindex_swapped_target_prefix_product))) /\ ((((exists ff_h_reindex_swapped_target_prefix_product_partial. ff_h_reindex_swapped_target_prefix_product_partial + S (ff_r_reindex_swapped_target_prefix_product) = S ((S (ff_i_reindex_swapped_target_prefix_product)) * ff_v_reindex_swapped_target_prefix_product)) /\ exists ff_q_reindex_swapped_target_prefix_product_partial. ff_u_reindex_swapped_target_prefix_product = ff_q_reindex_swapped_target_prefix_product_partial * S ((S (ff_i_reindex_swapped_target_prefix_product)) * ff_v_reindex_swapped_target_prefix_product) + (ff_r_reindex_swapped_target_prefix_product))) /\ ((((exists ff_h_reindex_swapped_target_prefix_product_successor. ff_h_reindex_swapped_target_prefix_product_successor + S (ff_s_reindex_swapped_target_prefix_product) = S ((S (S ff_i_reindex_swapped_target_prefix_product)) * ff_v_reindex_swapped_target_prefix_product)) /\ exists ff_q_reindex_swapped_target_prefix_product_successor. ff_u_reindex_swapped_target_prefix_product = ff_q_reindex_swapped_target_prefix_product_successor * S ((S (S ff_i_reindex_swapped_target_prefix_product)) * ff_v_reindex_swapped_target_prefix_product) + (ff_s_reindex_swapped_target_prefix_product))) /\ ff_s_reindex_swapped_target_prefix_product = ff_r_reindex_swapped_target_prefix_product * ff_p_reindex_swapped_target_prefix_product)))))) -> u = v
0342intro u
0343intro v
0344intro hsource_prefix_product
0345intro htarget_prefix_product
0346specialize IH x4
0347specialize IH x5
0348specialize IH b
0349specialize IH c
0350specialize IH x6
0351specialize IH x7
0352specialize IH u
0353specialize IH v
0354apply IH
0355exact hswapped_bounded_prefix
0356exact hswapped_injective_prefix
0357exact hswapped_aligned_prefix
0358exact hsource_prefix_product
0359exact htarget_prefix_product
0360have hproduct_swapped : p = x8
0361specialize beta_product_reindex_fixed_last x4
0362specialize beta_product_reindex_fixed_last x5
0363specialize beta_product_reindex_fixed_last b
0364specialize beta_product_reindex_fixed_last c
0365specialize beta_product_reindex_fixed_last x6
0366specialize beta_product_reindex_fixed_last x7
0367specialize beta_product_reindex_fixed_last l
0368specialize beta_product_reindex_fixed_last p
0369specialize beta_product_reindex_fixed_last x8
0370apply beta_product_reindex_fixed_last
0371exact hswapped_aligned
0372exact hmap_swap_witness_witness_right_left
0373exact hsource_product
0374exact hswapped_target_product_exists_witness
0375exact hswapped_prefix_products_equal
0376trans x8
0377exact hproduct_swapped
0378symm
0379exact htarget_product_swap