AF0016

factor_permutation_swapped_factorization_exists

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

Construct a full recoded prime-factor list moving a selected interior prime to the last position, with exact swap witnesses and an unchanged actual product.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded first-order arithmetic statement

forall N b c l i p. ((~(N = 0) /\ ((exists ff_u_fsat_swap_exists_factor_product ff_v_fsat_swap_exists_factor_product. ((((exists ff_h_fsat_swap_exists_factor_product_start. ff_h_fsat_swap_exists_factor_product_start + S (1) = S ((S (0)) * ff_v_fsat_swap_exists_factor_product)) /\ exists ff_q_fsat_swap_exists_factor_product_start. ff_u_fsat_swap_exists_factor_product = ff_q_fsat_swap_exists_factor_product_start * S ((S (0)) * ff_v_fsat_swap_exists_factor_product) + (1))) /\ ((((exists ff_h_fsat_swap_exists_factor_product_terminal. ff_h_fsat_swap_exists_factor_product_terminal + S (N) = S ((S (S l)) * ff_v_fsat_swap_exists_factor_product)) /\ exists ff_q_fsat_swap_exists_factor_product_terminal. ff_u_fsat_swap_exists_factor_product = ff_q_fsat_swap_exists_factor_product_terminal * S ((S (S l)) * ff_v_fsat_swap_exists_factor_product) + (N))) /\ forall ff_i_fsat_swap_exists_factor_product. (exists ff_lt_fsat_swap_exists_factor_product_bound. ff_lt_fsat_swap_exists_factor_product_bound + S ff_i_fsat_swap_exists_factor_product = S l) -> exists ff_p_fsat_swap_exists_factor_product ff_r_fsat_swap_exists_factor_product ff_s_fsat_swap_exists_factor_product. ((((exists ff_h_fsat_swap_exists_factor_product_factor. ff_h_fsat_swap_exists_factor_product_factor + S (ff_p_fsat_swap_exists_factor_product) = S ((S (ff_i_fsat_swap_exists_factor_product)) * c)) /\ exists ff_q_fsat_swap_exists_factor_product_factor. b = ff_q_fsat_swap_exists_factor_product_factor * S ((S (ff_i_fsat_swap_exists_factor_product)) * c) + (ff_p_fsat_swap_exists_factor_product))) /\ ((((exists ff_h_fsat_swap_exists_factor_product_partial. ff_h_fsat_swap_exists_factor_product_partial + S (ff_r_fsat_swap_exists_factor_product) = S ((S (ff_i_fsat_swap_exists_factor_product)) * ff_v_fsat_swap_exists_factor_product)) /\ exists ff_q_fsat_swap_exists_factor_product_partial. ff_u_fsat_swap_exists_factor_product = ff_q_fsat_swap_exists_factor_product_partial * S ((S (ff_i_fsat_swap_exists_factor_product)) * ff_v_fsat_swap_exists_factor_product) + (ff_r_fsat_swap_exists_factor_product))) /\ ((((exists ff_h_fsat_swap_exists_factor_product_successor. ff_h_fsat_swap_exists_factor_product_successor + S (ff_s_fsat_swap_exists_factor_product) = S ((S (S ff_i_fsat_swap_exists_factor_product)) * ff_v_fsat_swap_exists_factor_product)) /\ exists ff_q_fsat_swap_exists_factor_product_successor. ff_u_fsat_swap_exists_factor_product = ff_q_fsat_swap_exists_factor_product_successor * S ((S (S ff_i_fsat_swap_exists_factor_product)) * ff_v_fsat_swap_exists_factor_product) + (ff_s_fsat_swap_exists_factor_product))) /\ ff_s_fsat_swap_exists_factor_product = ff_r_fsat_swap_exists_factor_product * ff_p_fsat_swap_exists_factor_product)))))) /\ (forall ftsf_index_fsat_swap_exists_factor_primes. (exists ftsf_gap_fsat_swap_exists_factor_primes_bound. ftsf_gap_fsat_swap_exists_factor_primes_bound + S ftsf_index_fsat_swap_exists_factor_primes = (S l)) -> exists ftsf_factor_fsat_swap_exists_factor_primes. ((((exists ff_h_ftsf_fsat_swap_exists_factor_primes_entry. ff_h_ftsf_fsat_swap_exists_factor_primes_entry + S (ftsf_factor_fsat_swap_exists_factor_primes) = S ((S (ftsf_index_fsat_swap_exists_factor_primes)) * c)) /\ exists ff_q_ftsf_fsat_swap_exists_factor_primes_entry. b = ff_q_ftsf_fsat_swap_exists_factor_primes_entry * S ((S (ftsf_index_fsat_swap_exists_factor_primes)) * c) + (ftsf_factor_fsat_swap_exists_factor_primes))) /\ ((~(ftsf_factor_fsat_swap_exists_factor_primes = 1) /\ forall frm_prime_left_ftsf_fsat_swap_exists_factor_primes_prime frm_prime_right_ftsf_fsat_swap_exists_factor_primes_prime. ftsf_factor_fsat_swap_exists_factor_primes = frm_prime_left_ftsf_fsat_swap_exists_factor_primes_prime * frm_prime_right_ftsf_fsat_swap_exists_factor_primes_prime -> frm_prime_left_ftsf_fsat_swap_exists_factor_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_swap_exists_factor_primes_prime = 1))))))) -> (exists pfp_gap_swap_exists_index. pfp_gap_swap_exists_index + S (i) = (l)) -> (((exists ff_h_pfp_swap_exists_selected. ff_h_pfp_swap_exists_selected + S (p) = S ((S (i)) * c)) /\ exists ff_q_pfp_swap_exists_selected. b = ff_q_pfp_swap_exists_selected * S ((S (i)) * c) + (p))) -> exists d e q. (((~(N = 0) /\ ((exists ff_u_fsat_swap_exists_result_product ff_v_fsat_swap_exists_result_product. ((((exists ff_h_fsat_swap_exists_result_product_start. ff_h_fsat_swap_exists_result_product_start + S (1) = S ((S (0)) * ff_v_fsat_swap_exists_result_product)) /\ exists ff_q_fsat_swap_exists_result_product_start. ff_u_fsat_swap_exists_result_product = ff_q_fsat_swap_exists_result_product_start * S ((S (0)) * ff_v_fsat_swap_exists_result_product) + (1))) /\ ((((exists ff_h_fsat_swap_exists_result_product_terminal. ff_h_fsat_swap_exists_result_product_terminal + S (N) = S ((S (S l)) * ff_v_fsat_swap_exists_result_product)) /\ exists ff_q_fsat_swap_exists_result_product_terminal. ff_u_fsat_swap_exists_result_product = ff_q_fsat_swap_exists_result_product_terminal * S ((S (S l)) * ff_v_fsat_swap_exists_result_product) + (N))) /\ forall ff_i_fsat_swap_exists_result_product. (exists ff_lt_fsat_swap_exists_result_product_bound. ff_lt_fsat_swap_exists_result_product_bound + S ff_i_fsat_swap_exists_result_product = S l) -> exists ff_p_fsat_swap_exists_result_product ff_r_fsat_swap_exists_result_product ff_s_fsat_swap_exists_result_product. ((((exists ff_h_fsat_swap_exists_result_product_factor. ff_h_fsat_swap_exists_result_product_factor + S (ff_p_fsat_swap_exists_result_product) = S ((S (ff_i_fsat_swap_exists_result_product)) * e)) /\ exists ff_q_fsat_swap_exists_result_product_factor. d = ff_q_fsat_swap_exists_result_product_factor * S ((S (ff_i_fsat_swap_exists_result_product)) * e) + (ff_p_fsat_swap_exists_result_product))) /\ ((((exists ff_h_fsat_swap_exists_result_product_partial. ff_h_fsat_swap_exists_result_product_partial + S (ff_r_fsat_swap_exists_result_product) = S ((S (ff_i_fsat_swap_exists_result_product)) * ff_v_fsat_swap_exists_result_product)) /\ exists ff_q_fsat_swap_exists_result_product_partial. ff_u_fsat_swap_exists_result_product = ff_q_fsat_swap_exists_result_product_partial * S ((S (ff_i_fsat_swap_exists_result_product)) * ff_v_fsat_swap_exists_result_product) + (ff_r_fsat_swap_exists_result_product))) /\ ((((exists ff_h_fsat_swap_exists_result_product_successor. ff_h_fsat_swap_exists_result_product_successor + S (ff_s_fsat_swap_exists_result_product) = S ((S (S ff_i_fsat_swap_exists_result_product)) * ff_v_fsat_swap_exists_result_product)) /\ exists ff_q_fsat_swap_exists_result_product_successor. ff_u_fsat_swap_exists_result_product = ff_q_fsat_swap_exists_result_product_successor * S ((S (S ff_i_fsat_swap_exists_result_product)) * ff_v_fsat_swap_exists_result_product) + (ff_s_fsat_swap_exists_result_product))) /\ ff_s_fsat_swap_exists_result_product = ff_r_fsat_swap_exists_result_product * ff_p_fsat_swap_exists_result_product)))))) /\ (forall ftsf_index_fsat_swap_exists_result_primes. (exists ftsf_gap_fsat_swap_exists_result_primes_bound. ftsf_gap_fsat_swap_exists_result_primes_bound + S ftsf_index_fsat_swap_exists_result_primes = (S l)) -> exists ftsf_factor_fsat_swap_exists_result_primes. ((((exists ff_h_ftsf_fsat_swap_exists_result_primes_entry. ff_h_ftsf_fsat_swap_exists_result_primes_entry + S (ftsf_factor_fsat_swap_exists_result_primes) = S ((S (ftsf_index_fsat_swap_exists_result_primes)) * e)) /\ exists ff_q_ftsf_fsat_swap_exists_result_primes_entry. d = ff_q_ftsf_fsat_swap_exists_result_primes_entry * S ((S (ftsf_index_fsat_swap_exists_result_primes)) * e) + (ftsf_factor_fsat_swap_exists_result_primes))) /\ ((~(ftsf_factor_fsat_swap_exists_result_primes = 1) /\ forall frm_prime_left_ftsf_fsat_swap_exists_result_primes_prime frm_prime_right_ftsf_fsat_swap_exists_result_primes_prime. ftsf_factor_fsat_swap_exists_result_primes = frm_prime_left_ftsf_fsat_swap_exists_result_primes_prime * frm_prime_right_ftsf_fsat_swap_exists_result_primes_prime -> frm_prime_left_ftsf_fsat_swap_exists_result_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_swap_exists_result_primes_prime = 1))))))) /\ (((((exists ff_h_pfp_swap_exists_witnessoldi. ff_h_pfp_swap_exists_witnessoldi + S (p) = S ((S (i)) * c)) /\ exists ff_q_pfp_swap_exists_witnessoldi. b = ff_q_pfp_swap_exists_witnessoldi * S ((S (i)) * c) + (p))) /\ (((((exists ff_h_pfp_swap_exists_witnessoldlast. ff_h_pfp_swap_exists_witnessoldlast + S (q) = S ((S (l)) * c)) /\ exists ff_q_pfp_swap_exists_witnessoldlast. b = ff_q_pfp_swap_exists_witnessoldlast * S ((S (l)) * c) + (q))) /\ (((((exists ff_h_pfp_swap_exists_witnessnewi. ff_h_pfp_swap_exists_witnessnewi + S (q) = S ((S (i)) * e)) /\ exists ff_q_pfp_swap_exists_witnessnewi. d = ff_q_pfp_swap_exists_witnessnewi * S ((S (i)) * e) + (q))) /\ (((((exists ff_h_pfp_swap_exists_witnessnewlast. ff_h_pfp_swap_exists_witnessnewlast + S (p) = S ((S (l)) * e)) /\ exists ff_q_pfp_swap_exists_witnessnewlast. d = ff_q_pfp_swap_exists_witnessnewlast * S ((S (l)) * e) + (p))) /\ (forall pfp_j_swap_exists_witness pfp_a_swap_exists_witness. (exists pfp_gap_swap_exists_witnessbound. pfp_gap_swap_exists_witnessbound + S (pfp_j_swap_exists_witness) = (S (l))) -> ~(pfp_j_swap_exists_witness = i) -> ~(pfp_j_swap_exists_witness = l) -> (((exists ff_h_pfp_swap_exists_witnessold. ff_h_pfp_swap_exists_witnessold + S (pfp_a_swap_exists_witness) = S ((S (pfp_j_swap_exists_witness)) * c)) /\ exists ff_q_pfp_swap_exists_witnessold. b = ff_q_pfp_swap_exists_witnessold * S ((S (pfp_j_swap_exists_witness)) * c) + (pfp_a_swap_exists_witness))) -> (((exists ff_h_pfp_swap_exists_witnessnew. ff_h_pfp_swap_exists_witnessnew + S (pfp_a_swap_exists_witness) = S ((S (pfp_j_swap_exists_witness)) * e)) /\ exists ff_q_pfp_swap_exists_witnessnew. d = ff_q_pfp_swap_exists_witnessnew * S ((S (pfp_j_swap_exists_witness)) * e) + (pfp_a_swap_exists_witness)))))))))))))

Constructive proof overview

Generated structural guide

Construct a full recoded prime-factor list moving a selected interior prime to the last position, with exact swap witnesses and an unchanged actual product.

The unchanged tactic script uses 3 declared prerequisites and contains 58 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_at_exists Stable theorem; checked-use authorized beta_prefix_swap_last_from_entries Stable theorem; checked-use authorized AF0015 factor_permutation_swap_factorization

Direct dependents

AF0019 prime_factor_lists_matching_by_length

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

58 script commands · 19 reading checkpoints · 3 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (1)
factor permutation swap factorization

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–9

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

  1. L1
    intro N
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro l
  5. L5
    intro i
  6. L6
    intro p
  7. L7
    intro hf
  8. L8
    intro hi
  9. L9
    intro hselected
02Establish hlastL10–14

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

  1. L10
    have hlast : exists q. (((exists ff_h_pfp_swap_exists_last. ff_h_pfp_swap_exists_last + S (q) = S ((S (l)) * c)) /\ exists ff_q_pfp_swap_exists_last. b = ff_q_pfp_swap_exists_last * S ((S (l)) * c) + (q)))
  2. L11
    specialize beta_at_exists (b)
  3. L12
    specialize beta_at_exists (c)
  4. L13
    specialize beta_at_exists (l)
  5. L14
    apply beta_at_exists
03Separate the logical casesL15–15

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

  1. L15
    cases hlast
04Establish hnewL16–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta prefix swap last from entries.

  1. L16
    have hnew : ∃ d. ∃ e. BetaAt(d,e,i,x) ∧ (BetaAt(d,e,l,p) ∧ (∀ y. ∀ z. Lt(y,S l) → ¬y = i → ¬y = l → BetaAt(b,c,y,z) → BetaAt(d,e,y,z)))Definitions: LtBetaAt
  2. L17
    specialize beta_prefix_swap_last_from_entries (b)
  3. L18
    specialize beta_prefix_swap_last_from_entries (c)
  4. L19
    specialize beta_prefix_swap_last_from_entries (l)
  5. L20
    specialize beta_prefix_swap_last_from_entries (i)
  6. L21
    specialize beta_prefix_swap_last_from_entries (p)
  7. L22
    specialize beta_prefix_swap_last_from_entries (x)
  8. L23
    apply beta_prefix_swap_last_from_entries
  9. L24
    exact hi
  10. L25
    exact hselected
05Use earlier factsL26–26

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

  1. L26
    exact hlast_witness
06Separate the logical casesL27–30

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

  1. L27
    cases hnew
  2. L28
    cases hnew_witness
  3. L29
    cases hnew_witness_witness
  4. L30
    cases hnew_witness_witness_right
07Establish hswapL31–31

Establish this local claim before using it. It is not an additional assumption.

  1. L31
    have hswap : BetaAt(b,c,i,p) ∧ (BetaAt(b,c,l,x) ∧ (BetaAt(x1,x2,i,x) ∧ (BetaAt(x1,x2,l,p) ∧ (∀ y. ∀ z. Lt(y,S l) → ¬y = i → ¬y = l → BetaAt(b,c,y,z) → BetaAt(x1,x2,y,z)))))Definitions: LtBetaAt
08Separate the logical casesL32–32

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

  1. L32
    split
09Use earlier factsL33–33

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

  1. L33
    exact hselected
10Separate the logical casesL34–34

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

  1. L34
    split
11Use earlier factsL35–35

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

  1. L35
    exact hlast_witness
12Separate the logical casesL36–36

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

  1. L36
    split
13Use earlier factsL37–37

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

  1. L37
    exact hnew_witness_witness_left
14Separate the logical casesL38–38

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

  1. L38
    split
15Use earlier factsL39–40

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

  1. L39
    exact hnew_witness_witness_right_left
  2. L40
    exact hnew_witness_witness_right_right
16Construct an explicit witnessL41–43

Supply the displayed value, then prove that it has the required property.

  1. L41
    exists x1
  2. L42
    exists x2
  3. L43
    exists x
17Separate the logical casesL44–44

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

  1. L44
    split
18Use earlier factsL45–54

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

  1. L45
    specialize factor_permutation_swap_factorization (N)
  2. L46
    specialize factor_permutation_swap_factorization (b)
  3. L47
    specialize factor_permutation_swap_factorization (c)
  4. L48
    specialize factor_permutation_swap_factorization (x1)
  5. L49
    specialize factor_permutation_swap_factorization (x2)
  6. L50
    specialize factor_permutation_swap_factorization (l)
  7. L51
    specialize factor_permutation_swap_factorization (i)
  8. L52
    specialize factor_permutation_swap_factorization (p)
  9. L53
    specialize factor_permutation_swap_factorization (x)
  10. L54
    apply factor_permutation_swap_factorization
19Use earlier factsL55–58

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

  1. L55
    exact hf
  2. L56
    exact hi
  3. L57
    exact hswap
  4. L58
    exact hswap

Library-wide reading audit

Original exact command ledger · 58 lines
  1. 0001intro N
  2. 0002intro b
  3. 0003intro c
  4. 0004intro l
  5. 0005intro i
  6. 0006intro p
  7. 0007intro hf
  8. 0008intro hi
  9. 0009intro hselected
  10. 0010have hlast : exists q. (((exists ff_h_pfp_swap_exists_last. ff_h_pfp_swap_exists_last + S (q) = S ((S (l)) * c)) /\ exists ff_q_pfp_swap_exists_last. b = ff_q_pfp_swap_exists_last * S ((S (l)) * c) + (q)))
  11. 0011specialize beta_at_exists (b)
  12. 0012specialize beta_at_exists (c)
  13. 0013specialize beta_at_exists (l)
  14. 0014apply beta_at_exists
  15. 0015cases hlast
  16. 0016have hnew : exists d e. ((((exists ff_h_pfp_swap_new_i. ff_h_pfp_swap_new_i + S (x) = S ((S (i)) * e)) /\ exists ff_q_pfp_swap_new_i. d = ff_q_pfp_swap_new_i * S ((S (i)) * e) + (x))) /\ (((((exists ff_h_pfp_swap_new_last. ff_h_pfp_swap_new_last + S (p) = S ((S (l)) * e)) /\ exists ff_q_pfp_swap_new_last. d = ff_q_pfp_swap_new_last * S ((S (l)) * e) + (p))) /\ (forall j a. (exists pfp_gap_swap_new_bound. pfp_gap_swap_new_bound + S (j) = (S l)) -> ~(j = i) -> ~(j = l) -> (((exists ff_h_pfp_swap_new_old. ff_h_pfp_swap_new_old + S (a) = S ((S (j)) * c)) /\ exists ff_q_pfp_swap_new_old. b = ff_q_pfp_swap_new_old * S ((S (j)) * c) + (a))) -> (((exists ff_h_pfp_swap_new_new. ff_h_pfp_swap_new_new + S (a) = S ((S (j)) * e)) /\ exists ff_q_pfp_swap_new_new. d = ff_q_pfp_swap_new_new * S ((S (j)) * e) + (a)))))))
  17. 0017specialize beta_prefix_swap_last_from_entries (b)
  18. 0018specialize beta_prefix_swap_last_from_entries (c)
  19. 0019specialize beta_prefix_swap_last_from_entries (l)
  20. 0020specialize beta_prefix_swap_last_from_entries (i)
  21. 0021specialize beta_prefix_swap_last_from_entries (p)
  22. 0022specialize beta_prefix_swap_last_from_entries (x)
  23. 0023apply beta_prefix_swap_last_from_entries
  24. 0024exact hi
  25. 0025exact hselected
  26. 0026exact hlast_witness
  27. 0027cases hnew
  28. 0028cases hnew_witness
  29. 0029cases hnew_witness_witness
  30. 0030cases hnew_witness_witness_right
  31. 0031have hswap : ((((exists ff_h_pfp_swap_constructedoldi. ff_h_pfp_swap_constructedoldi + S (p) = S ((S (i)) * c)) /\ exists ff_q_pfp_swap_constructedoldi. b = ff_q_pfp_swap_constructedoldi * S ((S (i)) * c) + (p))) /\ (((((exists ff_h_pfp_swap_constructedoldlast. ff_h_pfp_swap_constructedoldlast + S (x) = S ((S (l)) * c)) /\ exists ff_q_pfp_swap_constructedoldlast. b = ff_q_pfp_swap_constructedoldlast * S ((S (l)) * c) + (x))) /\ (((((exists ff_h_pfp_swap_constructednewi. ff_h_pfp_swap_constructednewi + S (x) = S ((S (i)) * x2)) /\ exists ff_q_pfp_swap_constructednewi. x1 = ff_q_pfp_swap_constructednewi * S ((S (i)) * x2) + (x))) /\ (((((exists ff_h_pfp_swap_constructednewlast. ff_h_pfp_swap_constructednewlast + S (p) = S ((S (l)) * x2)) /\ exists ff_q_pfp_swap_constructednewlast. x1 = ff_q_pfp_swap_constructednewlast * S ((S (l)) * x2) + (p))) /\ (forall pfp_j_swap_constructed pfp_a_swap_constructed. (exists pfp_gap_swap_constructedbound. pfp_gap_swap_constructedbound + S (pfp_j_swap_constructed) = (S (l))) -> ~(pfp_j_swap_constructed = i) -> ~(pfp_j_swap_constructed = l) -> (((exists ff_h_pfp_swap_constructedold. ff_h_pfp_swap_constructedold + S (pfp_a_swap_constructed) = S ((S (pfp_j_swap_constructed)) * c)) /\ exists ff_q_pfp_swap_constructedold. b = ff_q_pfp_swap_constructedold * S ((S (pfp_j_swap_constructed)) * c) + (pfp_a_swap_constructed))) -> (((exists ff_h_pfp_swap_constructednew. ff_h_pfp_swap_constructednew + S (pfp_a_swap_constructed) = S ((S (pfp_j_swap_constructed)) * x2)) /\ exists ff_q_pfp_swap_constructednew. x1 = ff_q_pfp_swap_constructednew * S ((S (pfp_j_swap_constructed)) * x2) + (pfp_a_swap_constructed)))))))))))
  32. 0032split
  33. 0033exact hselected
  34. 0034split
  35. 0035exact hlast_witness
  36. 0036split
  37. 0037exact hnew_witness_witness_left
  38. 0038split
  39. 0039exact hnew_witness_witness_right_left
  40. 0040exact hnew_witness_witness_right_right
  41. 0041exists x1
  42. 0042exists x2
  43. 0043exists x
  44. 0044split
  45. 0045specialize factor_permutation_swap_factorization (N)
  46. 0046specialize factor_permutation_swap_factorization (b)
  47. 0047specialize factor_permutation_swap_factorization (c)
  48. 0048specialize factor_permutation_swap_factorization (x1)
  49. 0049specialize factor_permutation_swap_factorization (x2)
  50. 0050specialize factor_permutation_swap_factorization (l)
  51. 0051specialize factor_permutation_swap_factorization (i)
  52. 0052specialize factor_permutation_swap_factorization (p)
  53. 0053specialize factor_permutation_swap_factorization (x)
  54. 0054apply factor_permutation_swap_factorization
  55. 0055exact hf
  56. 0056exact hi
  57. 0057exact hswap
  58. 0058exact hswap