AF0019

prime_factor_lists_matching_by_length

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

Full induction on an arbitrary source factor list: locate the last prime in the arbitrary target, genuinely swap and cancel it, recursively match the shorter lists, and construct the restored index bijection. Neither list is assumed sorted or distinct.

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 l n b c m d e. ((~(n = 0) /\ ((exists ff_u_fsat_uniqueness_source_product ff_v_fsat_uniqueness_source_product. ((((exists ff_h_fsat_uniqueness_source_product_start. ff_h_fsat_uniqueness_source_product_start + S (1) = S ((S (0)) * ff_v_fsat_uniqueness_source_product)) /\ exists ff_q_fsat_uniqueness_source_product_start. ff_u_fsat_uniqueness_source_product = ff_q_fsat_uniqueness_source_product_start * S ((S (0)) * ff_v_fsat_uniqueness_source_product) + (1))) /\ ((((exists ff_h_fsat_uniqueness_source_product_terminal. ff_h_fsat_uniqueness_source_product_terminal + S (n) = S ((S (l)) * ff_v_fsat_uniqueness_source_product)) /\ exists ff_q_fsat_uniqueness_source_product_terminal. ff_u_fsat_uniqueness_source_product = ff_q_fsat_uniqueness_source_product_terminal * S ((S (l)) * ff_v_fsat_uniqueness_source_product) + (n))) /\ forall ff_i_fsat_uniqueness_source_product. (exists ff_lt_fsat_uniqueness_source_product_bound. ff_lt_fsat_uniqueness_source_product_bound + S ff_i_fsat_uniqueness_source_product = l) -> exists ff_p_fsat_uniqueness_source_product ff_r_fsat_uniqueness_source_product ff_s_fsat_uniqueness_source_product. ((((exists ff_h_fsat_uniqueness_source_product_factor. ff_h_fsat_uniqueness_source_product_factor + S (ff_p_fsat_uniqueness_source_product) = S ((S (ff_i_fsat_uniqueness_source_product)) * c)) /\ exists ff_q_fsat_uniqueness_source_product_factor. b = ff_q_fsat_uniqueness_source_product_factor * S ((S (ff_i_fsat_uniqueness_source_product)) * c) + (ff_p_fsat_uniqueness_source_product))) /\ ((((exists ff_h_fsat_uniqueness_source_product_partial. ff_h_fsat_uniqueness_source_product_partial + S (ff_r_fsat_uniqueness_source_product) = S ((S (ff_i_fsat_uniqueness_source_product)) * ff_v_fsat_uniqueness_source_product)) /\ exists ff_q_fsat_uniqueness_source_product_partial. ff_u_fsat_uniqueness_source_product = ff_q_fsat_uniqueness_source_product_partial * S ((S (ff_i_fsat_uniqueness_source_product)) * ff_v_fsat_uniqueness_source_product) + (ff_r_fsat_uniqueness_source_product))) /\ ((((exists ff_h_fsat_uniqueness_source_product_successor. ff_h_fsat_uniqueness_source_product_successor + S (ff_s_fsat_uniqueness_source_product) = S ((S (S ff_i_fsat_uniqueness_source_product)) * ff_v_fsat_uniqueness_source_product)) /\ exists ff_q_fsat_uniqueness_source_product_successor. ff_u_fsat_uniqueness_source_product = ff_q_fsat_uniqueness_source_product_successor * S ((S (S ff_i_fsat_uniqueness_source_product)) * ff_v_fsat_uniqueness_source_product) + (ff_s_fsat_uniqueness_source_product))) /\ ff_s_fsat_uniqueness_source_product = ff_r_fsat_uniqueness_source_product * ff_p_fsat_uniqueness_source_product)))))) /\ (forall ftsf_index_fsat_uniqueness_source_primes. (exists ftsf_gap_fsat_uniqueness_source_primes_bound. ftsf_gap_fsat_uniqueness_source_primes_bound + S ftsf_index_fsat_uniqueness_source_primes = (l)) -> exists ftsf_factor_fsat_uniqueness_source_primes. ((((exists ff_h_ftsf_fsat_uniqueness_source_primes_entry. ff_h_ftsf_fsat_uniqueness_source_primes_entry + S (ftsf_factor_fsat_uniqueness_source_primes) = S ((S (ftsf_index_fsat_uniqueness_source_primes)) * c)) /\ exists ff_q_ftsf_fsat_uniqueness_source_primes_entry. b = ff_q_ftsf_fsat_uniqueness_source_primes_entry * S ((S (ftsf_index_fsat_uniqueness_source_primes)) * c) + (ftsf_factor_fsat_uniqueness_source_primes))) /\ ((~(ftsf_factor_fsat_uniqueness_source_primes = 1) /\ forall frm_prime_left_ftsf_fsat_uniqueness_source_primes_prime frm_prime_right_ftsf_fsat_uniqueness_source_primes_prime. ftsf_factor_fsat_uniqueness_source_primes = frm_prime_left_ftsf_fsat_uniqueness_source_primes_prime * frm_prime_right_ftsf_fsat_uniqueness_source_primes_prime -> frm_prime_left_ftsf_fsat_uniqueness_source_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_uniqueness_source_primes_prime = 1))))))) -> ((~(n = 0) /\ ((exists ff_u_fsat_uniqueness_target_product ff_v_fsat_uniqueness_target_product. ((((exists ff_h_fsat_uniqueness_target_product_start. ff_h_fsat_uniqueness_target_product_start + S (1) = S ((S (0)) * ff_v_fsat_uniqueness_target_product)) /\ exists ff_q_fsat_uniqueness_target_product_start. ff_u_fsat_uniqueness_target_product = ff_q_fsat_uniqueness_target_product_start * S ((S (0)) * ff_v_fsat_uniqueness_target_product) + (1))) /\ ((((exists ff_h_fsat_uniqueness_target_product_terminal. ff_h_fsat_uniqueness_target_product_terminal + S (n) = S ((S (m)) * ff_v_fsat_uniqueness_target_product)) /\ exists ff_q_fsat_uniqueness_target_product_terminal. ff_u_fsat_uniqueness_target_product = ff_q_fsat_uniqueness_target_product_terminal * S ((S (m)) * ff_v_fsat_uniqueness_target_product) + (n))) /\ forall ff_i_fsat_uniqueness_target_product. (exists ff_lt_fsat_uniqueness_target_product_bound. ff_lt_fsat_uniqueness_target_product_bound + S ff_i_fsat_uniqueness_target_product = m) -> exists ff_p_fsat_uniqueness_target_product ff_r_fsat_uniqueness_target_product ff_s_fsat_uniqueness_target_product. ((((exists ff_h_fsat_uniqueness_target_product_factor. ff_h_fsat_uniqueness_target_product_factor + S (ff_p_fsat_uniqueness_target_product) = S ((S (ff_i_fsat_uniqueness_target_product)) * e)) /\ exists ff_q_fsat_uniqueness_target_product_factor. d = ff_q_fsat_uniqueness_target_product_factor * S ((S (ff_i_fsat_uniqueness_target_product)) * e) + (ff_p_fsat_uniqueness_target_product))) /\ ((((exists ff_h_fsat_uniqueness_target_product_partial. ff_h_fsat_uniqueness_target_product_partial + S (ff_r_fsat_uniqueness_target_product) = S ((S (ff_i_fsat_uniqueness_target_product)) * ff_v_fsat_uniqueness_target_product)) /\ exists ff_q_fsat_uniqueness_target_product_partial. ff_u_fsat_uniqueness_target_product = ff_q_fsat_uniqueness_target_product_partial * S ((S (ff_i_fsat_uniqueness_target_product)) * ff_v_fsat_uniqueness_target_product) + (ff_r_fsat_uniqueness_target_product))) /\ ((((exists ff_h_fsat_uniqueness_target_product_successor. ff_h_fsat_uniqueness_target_product_successor + S (ff_s_fsat_uniqueness_target_product) = S ((S (S ff_i_fsat_uniqueness_target_product)) * ff_v_fsat_uniqueness_target_product)) /\ exists ff_q_fsat_uniqueness_target_product_successor. ff_u_fsat_uniqueness_target_product = ff_q_fsat_uniqueness_target_product_successor * S ((S (S ff_i_fsat_uniqueness_target_product)) * ff_v_fsat_uniqueness_target_product) + (ff_s_fsat_uniqueness_target_product))) /\ ff_s_fsat_uniqueness_target_product = ff_r_fsat_uniqueness_target_product * ff_p_fsat_uniqueness_target_product)))))) /\ (forall ftsf_index_fsat_uniqueness_target_primes. (exists ftsf_gap_fsat_uniqueness_target_primes_bound. ftsf_gap_fsat_uniqueness_target_primes_bound + S ftsf_index_fsat_uniqueness_target_primes = (m)) -> exists ftsf_factor_fsat_uniqueness_target_primes. ((((exists ff_h_ftsf_fsat_uniqueness_target_primes_entry. ff_h_ftsf_fsat_uniqueness_target_primes_entry + S (ftsf_factor_fsat_uniqueness_target_primes) = S ((S (ftsf_index_fsat_uniqueness_target_primes)) * e)) /\ exists ff_q_ftsf_fsat_uniqueness_target_primes_entry. d = ff_q_ftsf_fsat_uniqueness_target_primes_entry * S ((S (ftsf_index_fsat_uniqueness_target_primes)) * e) + (ftsf_factor_fsat_uniqueness_target_primes))) /\ ((~(ftsf_factor_fsat_uniqueness_target_primes = 1) /\ forall frm_prime_left_ftsf_fsat_uniqueness_target_primes_prime frm_prime_right_ftsf_fsat_uniqueness_target_primes_prime. ftsf_factor_fsat_uniqueness_target_primes = frm_prime_left_ftsf_fsat_uniqueness_target_primes_prime * frm_prime_right_ftsf_fsat_uniqueness_target_primes_prime -> frm_prime_left_ftsf_fsat_uniqueness_target_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_uniqueness_target_primes_prime = 1))))))) -> (((l = m) /\ (exists pfp_u_uniqueness_result pfp_v_uniqueness_result. (((((forall pfp_i_uniqueness_resultmatchingpermutationbounded. (exists pfp_gap_uniqueness_resultmatchingpermutationboundedindex. pfp_gap_uniqueness_resultmatchingpermutationboundedindex + S (pfp_i_uniqueness_resultmatchingpermutationbounded) = (l)) -> exists pfp_a_uniqueness_resultmatchingpermutationbounded. (((exists ff_h_pfp_uniqueness_resultmatchingpermutationboundedentry. ff_h_pfp_uniqueness_resultmatchingpermutationboundedentry + S (pfp_a_uniqueness_resultmatchingpermutationbounded) = S ((S (pfp_i_uniqueness_resultmatchingpermutationbounded)) * pfp_v_uniqueness_result)) /\ exists ff_q_pfp_uniqueness_resultmatchingpermutationboundedentry. pfp_u_uniqueness_result = ff_q_pfp_uniqueness_resultmatchingpermutationboundedentry * S ((S (pfp_i_uniqueness_resultmatchingpermutationbounded)) * pfp_v_uniqueness_result) + (pfp_a_uniqueness_resultmatchingpermutationbounded))) /\ (exists pfp_gap_uniqueness_resultmatchingpermutationboundedvalue. pfp_gap_uniqueness_resultmatchingpermutationboundedvalue + S (pfp_a_uniqueness_resultmatchingpermutationbounded) = (l))) /\ (((forall pfp_i_uniqueness_resultmatchingpermutationinjective pfp_j_uniqueness_resultmatchingpermutationinjective pfp_a_uniqueness_resultmatchingpermutationinjective. (exists pfp_gap_uniqueness_resultmatchingpermutationinjectivefirst. pfp_gap_uniqueness_resultmatchingpermutationinjectivefirst + S (pfp_i_uniqueness_resultmatchingpermutationinjective) = (l)) -> (exists pfp_gap_uniqueness_resultmatchingpermutationinjectivesecond. pfp_gap_uniqueness_resultmatchingpermutationinjectivesecond + S (pfp_j_uniqueness_resultmatchingpermutationinjective) = (l)) -> (((exists ff_h_pfp_uniqueness_resultmatchingpermutationinjectiveleft. ff_h_pfp_uniqueness_resultmatchingpermutationinjectiveleft + S (pfp_a_uniqueness_resultmatchingpermutationinjective) = S ((S (pfp_i_uniqueness_resultmatchingpermutationinjective)) * pfp_v_uniqueness_result)) /\ exists ff_q_pfp_uniqueness_resultmatchingpermutationinjectiveleft. pfp_u_uniqueness_result = ff_q_pfp_uniqueness_resultmatchingpermutationinjectiveleft * S ((S (pfp_i_uniqueness_resultmatchingpermutationinjective)) * pfp_v_uniqueness_result) + (pfp_a_uniqueness_resultmatchingpermutationinjective))) -> (((exists ff_h_pfp_uniqueness_resultmatchingpermutationinjectiveright. ff_h_pfp_uniqueness_resultmatchingpermutationinjectiveright + S (pfp_a_uniqueness_resultmatchingpermutationinjective) = S ((S (pfp_j_uniqueness_resultmatchingpermutationinjective)) * pfp_v_uniqueness_result)) /\ exists ff_q_pfp_uniqueness_resultmatchingpermutationinjectiveright. pfp_u_uniqueness_result = ff_q_pfp_uniqueness_resultmatchingpermutationinjectiveright * S ((S (pfp_j_uniqueness_resultmatchingpermutationinjective)) * pfp_v_uniqueness_result) + (pfp_a_uniqueness_resultmatchingpermutationinjective))) -> pfp_i_uniqueness_resultmatchingpermutationinjective = pfp_j_uniqueness_resultmatchingpermutationinjective) /\ (forall pfp_a_uniqueness_resultmatchingpermutationsurjective. (exists pfp_gap_uniqueness_resultmatchingpermutationsurjectivevalue. pfp_gap_uniqueness_resultmatchingpermutationsurjectivevalue + S (pfp_a_uniqueness_resultmatchingpermutationsurjective) = (l)) -> exists pfp_i_uniqueness_resultmatchingpermutationsurjective. (exists pfp_gap_uniqueness_resultmatchingpermutationsurjectiveindex. pfp_gap_uniqueness_resultmatchingpermutationsurjectiveindex + S (pfp_i_uniqueness_resultmatchingpermutationsurjective) = (l)) /\ (((exists ff_h_pfp_uniqueness_resultmatchingpermutationsurjectiveentry. ff_h_pfp_uniqueness_resultmatchingpermutationsurjectiveentry + S (pfp_a_uniqueness_resultmatchingpermutationsurjective) = S ((S (pfp_i_uniqueness_resultmatchingpermutationsurjective)) * pfp_v_uniqueness_result)) /\ exists ff_q_pfp_uniqueness_resultmatchingpermutationsurjectiveentry. pfp_u_uniqueness_result = ff_q_pfp_uniqueness_resultmatchingpermutationsurjectiveentry * S ((S (pfp_i_uniqueness_resultmatchingpermutationsurjective)) * pfp_v_uniqueness_result) + (pfp_a_uniqueness_resultmatchingpermutationsurjective)))))))) /\ (forall pfp_i_uniqueness_resultmatchingmatching pfp_j_uniqueness_resultmatchingmatching pfp_a_uniqueness_resultmatchingmatching. (exists pfp_gap_uniqueness_resultmatchingmatchingbound. pfp_gap_uniqueness_resultmatchingmatchingbound + S (pfp_i_uniqueness_resultmatchingmatching) = (l)) -> (((exists ff_h_pfp_uniqueness_resultmatchingmatchingmap. ff_h_pfp_uniqueness_resultmatchingmatchingmap + S (pfp_j_uniqueness_resultmatchingmatching) = S ((S (pfp_i_uniqueness_resultmatchingmatching)) * pfp_v_uniqueness_result)) /\ exists ff_q_pfp_uniqueness_resultmatchingmatchingmap. pfp_u_uniqueness_result = ff_q_pfp_uniqueness_resultmatchingmatchingmap * S ((S (pfp_i_uniqueness_resultmatchingmatching)) * pfp_v_uniqueness_result) + (pfp_j_uniqueness_resultmatchingmatching))) -> (((exists ff_h_pfp_uniqueness_resultmatchingmatchingsource. ff_h_pfp_uniqueness_resultmatchingmatchingsource + S (pfp_a_uniqueness_resultmatchingmatching) = S ((S (pfp_i_uniqueness_resultmatchingmatching)) * c)) /\ exists ff_q_pfp_uniqueness_resultmatchingmatchingsource. b = ff_q_pfp_uniqueness_resultmatchingmatchingsource * S ((S (pfp_i_uniqueness_resultmatchingmatching)) * c) + (pfp_a_uniqueness_resultmatchingmatching))) -> (((exists ff_h_pfp_uniqueness_resultmatchingmatchingtarget. ff_h_pfp_uniqueness_resultmatchingmatchingtarget + S (pfp_a_uniqueness_resultmatchingmatching) = S ((S (pfp_j_uniqueness_resultmatchingmatching)) * e)) /\ exists ff_q_pfp_uniqueness_resultmatchingmatchingtarget. d = ff_q_pfp_uniqueness_resultmatchingmatchingtarget * S ((S (pfp_j_uniqueness_resultmatchingmatching)) * e) + (pfp_a_uniqueness_resultmatchingmatching)))))))))

Constructive proof overview

Generated structural guide

Full induction on an arbitrary source factor list: locate the last prime in the arbitrary target, genuinely swap and cancel it, recursively match the shorter lists, and construct the restored index bijection. Neither list is assumed sorted or distinct.

The unchanged tactic script uses 13 declared prerequisites and contains 227 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_product_zero Stable theorem; checked-use authorized AF000B factor_permutation_unit_length_zero AF000D factor_permutation_empty_matching AF000A factor_permutation_successor_decompose AF000C factor_permutation_prime_member mul_comm Stable theorem; checked-use authorized AF0005 factor_permutation_below_zero_impossible nonzero_is_succ Stable theorem; checked-use authorized finite_lt_succ_eq_or_lt Stable theorem; checked-use authorized AF0009 factor_permutation_cancel_last AF0011 factor_permutation_matched_append_exists AF0016 factor_permutation_swapped_factorization_exists AF0018 factor_permutation_matched_unswap_exists

Direct dependents

AF001A prime_factor_lists_permutation_exists

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

227 script commands · 56 reading checkpoints · 20 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 (9)
factor permutation unit length zerofactor permutation empty matchingfactor permutation successor decomposefactor permutation prime memberfactor permutation below zero impossiblefactor permutation cancel lastfactor permutation matched append existsfactor permutation swapped factorization existsfactor permutation matched unswap exists

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.

01Induction on lL1–9

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L1
    induction l
  2. L2
    intro n
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro m
  6. L6
    intro d
  7. L7
    intro e
  8. L8
    intro hA
  9. L9
    intro hB
02Establish hproductL10–10

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

  1. L10
    have hproduct : Product(b,c,0,n)Definitions: Product
03Separate the logical casesL11–12

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

  1. L11
    cases hA
  2. L12
    cases hA_right
04Use earlier factsL13–13

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

  1. L13
    exact hA_right_left
05Establish honeL14–19

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

  1. L14
    have hone : n = 1
  2. L15
    specialize beta_product_zero (b)
  3. L16
    specialize beta_product_zero (c)
  4. L17
    specialize beta_product_zero (n)
  5. L18
    apply beta_product_zero
  6. L19
    exact hproduct
06Establish hlengthL20–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor permutation unit length zero.

  1. L20
    have hlength : m = 0
  2. L21
    specialize factor_permutation_unit_length_zero (n)
  3. L22
    specialize factor_permutation_unit_length_zero (d)
  4. L23
    specialize factor_permutation_unit_length_zero (e)
  5. L24
    specialize factor_permutation_unit_length_zero (m)
  6. L25
    apply factor_permutation_unit_length_zero
  7. L26
    exact hB
  8. L27
    exact hone
07Separate the logical casesL28–28

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

  1. L28
    split
08Calculate and transport equalitiesL29–29

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

  1. L29
    symm
09Use earlier factsL30–30

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

  1. L30
    exact hlength
10Construct an explicit witnessL31–32

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

  1. L31
    exists 0
  2. L32
    exists 0
11Use earlier factsL33–37

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

  1. L33
    specialize factor_permutation_empty_matching (b)
  2. L34
    specialize factor_permutation_empty_matching (c)
  3. L35
    specialize factor_permutation_empty_matching (d)
  4. L36
    specialize factor_permutation_empty_matching (e)
  5. L37
    apply factor_permutation_empty_matching
12Fix variables and assumptionsL38–45

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

  1. L38
    intro n
  2. L39
    intro b
  3. L40
    intro c
  4. L41
    intro m
  5. L42
    intro d
  6. L43
    intro e
  7. L44
    intro hA
  8. L45
    intro hB
13Establish hdL46–52

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor permutation successor decompose.

  1. L46
    have hd : ∃ p. ∃ r. Prime(p) ∧ (BetaAt(b,c,l,p) ∧ (n = r · p ∧ PrimeFactorList(r,b,c,l)))Definitions: PrimeFactorListPrimeBetaAt
  2. L47
    specialize factor_permutation_successor_decompose (n)
  3. L48
    specialize factor_permutation_successor_decompose (b)
  4. L49
    specialize factor_permutation_successor_decompose (c)
  5. L50
    specialize factor_permutation_successor_decompose (l)
  6. L51
    apply factor_permutation_successor_decompose
  7. L52
    exact hA
14Separate the logical casesL53–57

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

  1. L53
    cases hd
  2. L54
    cases hd_witness
  3. L55
    cases hd_witness_witness
  4. L56
    cases hd_witness_witness_right
  5. L57
    cases hd_witness_witness_right_right
15Establish hmemberL58–66

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor permutation prime member.

  1. L58
    have hmember : exists i. (exists pfp_gap_induction_member_bound. pfp_gap_induction_member_bound + S (i) = (m)) /\ (((exists ff_h_pfp_induction_member_entry. ff_h_pfp_induction_member_entry + S (x) = S ((S (i)) * e)) /\ exists ff_q_pfp_induction_member_entry. d = ff_q_pfp_induction_member_entry * S ((S (i)) * e) + (x)))
  2. L59
    specialize factor_permutation_prime_member (n)
  3. L60
    specialize factor_permutation_prime_member (d)
  4. L61
    specialize factor_permutation_prime_member (e)
  5. L62
    specialize factor_permutation_prime_member (m)
  6. L63
    specialize factor_permutation_prime_member (x)
  7. L64
    apply factor_permutation_prime_member
  8. L65
    exact hB
  9. L66
    exact hd_witness_witness_left
16Construct an explicit witnessL67–67

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

  1. L67
    exists x1
17Calculate and transport equalitiesL68–68

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

  1. L68
    trans x1 * x
18Use earlier factsL69–70

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

  1. L69
    exact hd_witness_witness_right_right_left
  2. L70
    apply mul_comm
19Separate the logical casesL71–72

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

  1. L71
    cases hmember
  2. L72
    cases hmember_witness
20Establish hmnonzeroL73–78

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor permutation below zero impossible.

  1. L73
    have hmnonzero : ~(m = 0)
  2. L74
    intro hzero
  3. L75
    specialize factor_permutation_below_zero_impossible (x2)
  4. L76
    apply factor_permutation_below_zero_impossible
  5. L77
    rewrite hzero at hmember_witness_left
  6. L78
    exact hmember_witness_left
21Establish hpredecessorL79–82

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

  1. L79
    have hpredecessor : exists t. m = S t
  2. L80
    specialize nonzero_is_succ (m)
  3. L81
    apply nonzero_is_succ
  4. L82
    exact hmnonzero
22Separate the logical casesL83–83

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

  1. L83
    cases hpredecessor
23Establish hBsuccessorL84–89

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

  1. L84
    have hBsuccessor : PrimeFactorList(n,d,e,S x3)Definitions: PrimeFactorList
  2. L85
    rewrite hpredecessor_witness at hB
  3. L86
    rewrite hpredecessor_witness at hB
  4. L87
    rewrite hpredecessor_witness at hB
  5. L88
    rewrite hpredecessor_witness at hB
  6. L89
    exact hB
24Establish hboundL90–92

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

  1. L90
    have hbound : exists pfp_gap_induction_target_index. pfp_gap_induction_target_index + S (x2) = (S x3)
  2. L91
    rewrite hpredecessor_witness at hmember_witness_left
  3. L92
    exact hmember_witness_left
25Establish hpositionL93–97

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L93
    have hposition : x2 = x3 \/ (exists pfp_gap_induction_target_position. pfp_gap_induction_target_position + S (x2) = (x3))
  2. L94
    specialize finite_lt_succ_eq_or_lt (x3)
  3. L95
    specialize finite_lt_succ_eq_or_lt (x2)
  4. L96
    apply finite_lt_succ_eq_or_lt
  5. L97
    exact hbound
26Separate the logical casesL98–98

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

  1. L98
    cases hposition
27Establish hlastL99–102

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

  1. L99
    have hlast : ((exists ff_h_pfp_induction_already_last. ff_h_pfp_induction_already_last + S (x) = S ((S (x3)) * e)) /\ exists ff_q_pfp_induction_already_last. d = ff_q_pfp_induction_already_last * S ((S (x3)) * e) + (x))
  2. L100
    rewrite hposition_left at hmember_witness_right
  3. L101
    rewrite hposition_left at hmember_witness_right
  4. L102
    exact hmember_witness_right
28Establish hprefixL103–112

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor permutation cancel last.

  1. L103
    have hprefix : PrimeFactorList(x1,d,e,x3)Definitions: PrimeFactorList
  2. L104
    specialize factor_permutation_cancel_last (n)
  3. L105
    specialize factor_permutation_cancel_last (x)
  4. L106
    specialize factor_permutation_cancel_last (x1)
  5. L107
    specialize factor_permutation_cancel_last (d)
  6. L108
    specialize factor_permutation_cancel_last (e)
  7. L109
    specialize factor_permutation_cancel_last (x3)
  8. L110
    apply factor_permutation_cancel_last
  9. L111
    exact hBsuccessor
  10. L112
    exact hlast
29Use earlier factsL113–113

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

  1. L113
    exact hd_witness_witness_right_right_left
30Establish hrecL114–123

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

  1. L114
    have hrec : l = x3 ∧ (∃ x. ∃ y. PermutationPrefix(x,y,l) ∧ FactorListMatching(b,c,d,e,x,y,l))Definitions: PermutationPrefixFactorListMatching
  2. L115
    specialize IH (x1)
  3. L116
    specialize IH (b)
  4. L117
    specialize IH (c)
  5. L118
    specialize IH (x3)
  6. L119
    specialize IH (d)
  7. L120
    specialize IH (e)
  8. L121
    apply IH
  9. L122
    exact hd_witness_witness_right_right_right
  10. L123
    exact hprefix
31Separate the logical casesL124–126

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

  1. L124
    cases hrec
  2. L125
    cases hrec_right
  3. L126
    cases hrec_right_witness
32Establish hlastalignedL127–130

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

  1. L127
    have hlastaligned : ((exists ff_h_pfp_induction_direct_aligned_last. ff_h_pfp_induction_direct_aligned_last + S (x) = S ((S (l)) * e)) /\ exists ff_q_pfp_induction_direct_aligned_last. d = ff_q_pfp_induction_direct_aligned_last * S ((S (l)) * e) + (x))
  2. L128
    rewrite hrec_left
  3. L129
    rewrite hrec_left
  4. L130
    exact hlast
33Separate the logical casesL131–131

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

  1. L131
    split
34Calculate and transport equalitiesL132–133

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

  1. L132
    trans S x3
  2. L133
    congr
35Use earlier factsL134–134

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

  1. L134
    exact hrec_left
36Calculate and transport equalitiesL135–135

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

  1. L135
    symm
37Use earlier factsL136–145

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

  1. L136
    exact hpredecessor_witness
  2. L137
    specialize factor_permutation_matched_append_exists (b)
  3. L138
    specialize factor_permutation_matched_append_exists (c)
  4. L139
    specialize factor_permutation_matched_append_exists (d)
  5. L140
    specialize factor_permutation_matched_append_exists (e)
  6. L141
    specialize factor_permutation_matched_append_exists (x4)
  7. L142
    specialize factor_permutation_matched_append_exists (x5)
  8. L143
    specialize factor_permutation_matched_append_exists (l)
  9. L144
    specialize factor_permutation_matched_append_exists (x)
  10. L145
    apply factor_permutation_matched_append_exists
38Use earlier factsL146–148

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

  1. L146
    exact hrec_right_witness_witness
  2. L147
    exact hd_witness_witness_right_left
  3. L148
    exact hlastaligned
39Establish hswapL149–158

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor permutation swapped factorization exists.

  1. L149
    have hswap : ∃ B. ∃ C. ∃ q. PrimeFactorList(n,B,C,S x3) ∧ (BetaAt(d,e,x2,x) ∧ (BetaAt(d,e,x3,q) ∧ (BetaAt(B,C,x2,q) ∧ (BetaAt(B,C,x3,x) ∧ (∀ y. ∀ z. Lt(y,S x3) → ¬y = x2 → ¬y = x3 → BetaAt(d,e,y,z) → BetaAt(B,C,y,z))))))Definitions: PrimeFactorListLtBetaAt
  2. L150
    specialize factor_permutation_swapped_factorization_exists (n)
  3. L151
    specialize factor_permutation_swapped_factorization_exists (d)
  4. L152
    specialize factor_permutation_swapped_factorization_exists (e)
  5. L153
    specialize factor_permutation_swapped_factorization_exists (x3)
  6. L154
    specialize factor_permutation_swapped_factorization_exists (x2)
  7. L155
    specialize factor_permutation_swapped_factorization_exists (x)
  8. L156
    apply factor_permutation_swapped_factorization_exists
  9. L157
    exact hBsuccessor
  10. L158
    exact hposition_right
40Use earlier factsL159–159

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

  1. L159
    exact hmember_witness_right
41Separate the logical casesL160–163

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

  1. L160
    cases hswap
  2. L161
    cases hswap_witness
  3. L162
    cases hswap_witness_witness
  4. L163
    cases hswap_witness_witness_witness
42Establish hlastL164–164

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

  1. L164
    have hlast : ((exists ff_h_pfp_induction_recoded_last. ff_h_pfp_induction_recoded_last + S (x) = S ((S (x3)) * x5)) /\ exists ff_q_pfp_induction_recoded_last. x4 = ff_q_pfp_induction_recoded_last * S ((S (x3)) * x5) + (x))
43Separate the logical casesL165–168

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

  1. L165
    cases hswap_witness_witness_witness_right
  2. L166
    cases hswap_witness_witness_witness_right_right
  3. L167
    cases hswap_witness_witness_witness_right_right_right
  4. L168
    cases hswap_witness_witness_witness_right_right_right_right
44Use earlier factsL169–169

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

  1. L169
    exact hswap_witness_witness_witness_right_right_right_right_left
45Establish hprefixL170–179

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor permutation cancel last.

  1. L170
    have hprefix : PrimeFactorList(x1,x4,x5,x3)Definitions: PrimeFactorList
  2. L171
    specialize factor_permutation_cancel_last (n)
  3. L172
    specialize factor_permutation_cancel_last (x)
  4. L173
    specialize factor_permutation_cancel_last (x1)
  5. L174
    specialize factor_permutation_cancel_last (x4)
  6. L175
    specialize factor_permutation_cancel_last (x5)
  7. L176
    specialize factor_permutation_cancel_last (x3)
  8. L177
    apply factor_permutation_cancel_last
  9. L178
    exact hswap_witness_witness_witness_left
  10. L179
    exact hlast
46Use earlier factsL180–180

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

  1. L180
    exact hd_witness_witness_right_right_left
47Establish hrecL181–190

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

  1. L181
    have hrec : l = x3 ∧ (∃ x. ∃ y. PermutationPrefix(x,y,l) ∧ FactorListMatching(b,c,x4,x5,x,y,l))Definitions: PermutationPrefixFactorListMatching
  2. L182
    specialize IH (x1)
  3. L183
    specialize IH (b)
  4. L184
    specialize IH (c)
  5. L185
    specialize IH (x3)
  6. L186
    specialize IH (x4)
  7. L187
    specialize IH (x5)
  8. L188
    apply IH
  9. L189
    exact hd_witness_witness_right_right_right
  10. L190
    exact hprefix
48Separate the logical casesL191–193

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

  1. L191
    cases hrec
  2. L192
    cases hrec_right
  3. L193
    cases hrec_right_witness
49Establish hpivotL194–196

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

  1. L194
    have hpivot : exists pfp_gap_induction_pivot_aligned. pfp_gap_induction_pivot_aligned + S (x2) = (l)
  2. L195
    rewrite hrec_left
  3. L196
    exact hposition_right
50Establish hswapalignedL197–204

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

  1. L197
    have hswapaligned : BetaAt(d,e,x2,x) ∧ (BetaAt(d,e,l,x6) ∧ (BetaAt(x4,x5,x2,x6) ∧ (BetaAt(x4,x5,l,x) ∧ (∀ y. ∀ z. Lt(y,S l) → ¬y = x2 → ¬y = l → BetaAt(d,e,y,z) → BetaAt(x4,x5,y,z)))))Definitions: LtBetaAt
  2. L198
    rewrite hrec_left
  3. L199
    rewrite hrec_left
  4. L200
    rewrite hrec_left
  5. L201
    rewrite hrec_left
  6. L202
    rewrite hrec_left
  7. L203
    rewrite hrec_left
  8. L204
    exact hswap_witness_witness_witness_right
51Separate the logical casesL205–205

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

  1. L205
    split
52Calculate and transport equalitiesL206–207

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

  1. L206
    trans S x3
  2. L207
    congr
53Use earlier factsL208–208

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

  1. L208
    exact hrec_left
54Calculate and transport equalitiesL209–209

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

  1. L209
    symm
55Use earlier factsL210–219

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

  1. L210
    exact hpredecessor_witness
  2. L211
    specialize factor_permutation_matched_unswap_exists (b)
  3. L212
    specialize factor_permutation_matched_unswap_exists (c)
  4. L213
    specialize factor_permutation_matched_unswap_exists (d)
  5. L214
    specialize factor_permutation_matched_unswap_exists (e)
  6. L215
    specialize factor_permutation_matched_unswap_exists (x4)
  7. L216
    specialize factor_permutation_matched_unswap_exists (x5)
  8. L217
    specialize factor_permutation_matched_unswap_exists (x7)
  9. L218
    specialize factor_permutation_matched_unswap_exists (x8)
  10. L219
    specialize factor_permutation_matched_unswap_exists (l)
56Use earlier factsL220–227

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

  1. L220
    specialize factor_permutation_matched_unswap_exists (x2)
  2. L221
    specialize factor_permutation_matched_unswap_exists (x)
  3. L222
    specialize factor_permutation_matched_unswap_exists (x6)
  4. L223
    apply factor_permutation_matched_unswap_exists
  5. L224
    exact hpivot
  6. L225
    exact hrec_right_witness_witness
  7. L226
    exact hd_witness_witness_right_left
  8. L227
    exact hswapaligned

Library-wide reading audit

Original exact command ledger · 227 lines
  1. 0001induction l
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro m
  6. 0006intro d
  7. 0007intro e
  8. 0008intro hA
  9. 0009intro hB
  10. 0010have hproduct : exists ff_u_fsat_zero_source_product ff_v_fsat_zero_source_product. ((((exists ff_h_fsat_zero_source_product_start. ff_h_fsat_zero_source_product_start + S (1) = S ((S (0)) * ff_v_fsat_zero_source_product)) /\ exists ff_q_fsat_zero_source_product_start. ff_u_fsat_zero_source_product = ff_q_fsat_zero_source_product_start * S ((S (0)) * ff_v_fsat_zero_source_product) + (1))) /\ ((((exists ff_h_fsat_zero_source_product_terminal. ff_h_fsat_zero_source_product_terminal + S (n) = S ((S (0)) * ff_v_fsat_zero_source_product)) /\ exists ff_q_fsat_zero_source_product_terminal. ff_u_fsat_zero_source_product = ff_q_fsat_zero_source_product_terminal * S ((S (0)) * ff_v_fsat_zero_source_product) + (n))) /\ forall ff_i_fsat_zero_source_product. (exists ff_lt_fsat_zero_source_product_bound. ff_lt_fsat_zero_source_product_bound + S ff_i_fsat_zero_source_product = 0) -> exists ff_p_fsat_zero_source_product ff_r_fsat_zero_source_product ff_s_fsat_zero_source_product. ((((exists ff_h_fsat_zero_source_product_factor. ff_h_fsat_zero_source_product_factor + S (ff_p_fsat_zero_source_product) = S ((S (ff_i_fsat_zero_source_product)) * c)) /\ exists ff_q_fsat_zero_source_product_factor. b = ff_q_fsat_zero_source_product_factor * S ((S (ff_i_fsat_zero_source_product)) * c) + (ff_p_fsat_zero_source_product))) /\ ((((exists ff_h_fsat_zero_source_product_partial. ff_h_fsat_zero_source_product_partial + S (ff_r_fsat_zero_source_product) = S ((S (ff_i_fsat_zero_source_product)) * ff_v_fsat_zero_source_product)) /\ exists ff_q_fsat_zero_source_product_partial. ff_u_fsat_zero_source_product = ff_q_fsat_zero_source_product_partial * S ((S (ff_i_fsat_zero_source_product)) * ff_v_fsat_zero_source_product) + (ff_r_fsat_zero_source_product))) /\ ((((exists ff_h_fsat_zero_source_product_successor. ff_h_fsat_zero_source_product_successor + S (ff_s_fsat_zero_source_product) = S ((S (S ff_i_fsat_zero_source_product)) * ff_v_fsat_zero_source_product)) /\ exists ff_q_fsat_zero_source_product_successor. ff_u_fsat_zero_source_product = ff_q_fsat_zero_source_product_successor * S ((S (S ff_i_fsat_zero_source_product)) * ff_v_fsat_zero_source_product) + (ff_s_fsat_zero_source_product))) /\ ff_s_fsat_zero_source_product = ff_r_fsat_zero_source_product * ff_p_fsat_zero_source_product)))))
  11. 0011cases hA
  12. 0012cases hA_right
  13. 0013exact hA_right_left
  14. 0014have hone : n = 1
  15. 0015specialize beta_product_zero (b)
  16. 0016specialize beta_product_zero (c)
  17. 0017specialize beta_product_zero (n)
  18. 0018apply beta_product_zero
  19. 0019exact hproduct
  20. 0020have hlength : m = 0
  21. 0021specialize factor_permutation_unit_length_zero (n)
  22. 0022specialize factor_permutation_unit_length_zero (d)
  23. 0023specialize factor_permutation_unit_length_zero (e)
  24. 0024specialize factor_permutation_unit_length_zero (m)
  25. 0025apply factor_permutation_unit_length_zero
  26. 0026exact hB
  27. 0027exact hone
  28. 0028split
  29. 0029symm
  30. 0030exact hlength
  31. 0031exists 0
  32. 0032exists 0
  33. 0033specialize factor_permutation_empty_matching (b)
  34. 0034specialize factor_permutation_empty_matching (c)
  35. 0035specialize factor_permutation_empty_matching (d)
  36. 0036specialize factor_permutation_empty_matching (e)
  37. 0037apply factor_permutation_empty_matching
  38. 0038intro n
  39. 0039intro b
  40. 0040intro c
  41. 0041intro m
  42. 0042intro d
  43. 0043intro e
  44. 0044intro hA
  45. 0045intro hB
  46. 0046have hd : exists p r. ((((~(p = 1) /\ forall frm_prime_left_pfp_induction_prime frm_prime_right_pfp_induction_prime. p = frm_prime_left_pfp_induction_prime * frm_prime_right_pfp_induction_prime -> frm_prime_left_pfp_induction_prime = 1 \/ frm_prime_right_pfp_induction_prime = 1)) /\ (((((exists ff_h_pfp_induction_last. ff_h_pfp_induction_last + S (p) = S ((S (l)) * c)) /\ exists ff_q_pfp_induction_last. b = ff_q_pfp_induction_last * S ((S (l)) * c) + (p))) /\ (((n = r * p) /\ ((~(r = 0) /\ ((exists ff_u_fsat_induction_source_prefix_product ff_v_fsat_induction_source_prefix_product. ((((exists ff_h_fsat_induction_source_prefix_product_start. ff_h_fsat_induction_source_prefix_product_start + S (1) = S ((S (0)) * ff_v_fsat_induction_source_prefix_product)) /\ exists ff_q_fsat_induction_source_prefix_product_start. ff_u_fsat_induction_source_prefix_product = ff_q_fsat_induction_source_prefix_product_start * S ((S (0)) * ff_v_fsat_induction_source_prefix_product) + (1))) /\ ((((exists ff_h_fsat_induction_source_prefix_product_terminal. ff_h_fsat_induction_source_prefix_product_terminal + S (r) = S ((S (l)) * ff_v_fsat_induction_source_prefix_product)) /\ exists ff_q_fsat_induction_source_prefix_product_terminal. ff_u_fsat_induction_source_prefix_product = ff_q_fsat_induction_source_prefix_product_terminal * S ((S (l)) * ff_v_fsat_induction_source_prefix_product) + (r))) /\ forall ff_i_fsat_induction_source_prefix_product. (exists ff_lt_fsat_induction_source_prefix_product_bound. ff_lt_fsat_induction_source_prefix_product_bound + S ff_i_fsat_induction_source_prefix_product = l) -> exists ff_p_fsat_induction_source_prefix_product ff_r_fsat_induction_source_prefix_product ff_s_fsat_induction_source_prefix_product. ((((exists ff_h_fsat_induction_source_prefix_product_factor. ff_h_fsat_induction_source_prefix_product_factor + S (ff_p_fsat_induction_source_prefix_product) = S ((S (ff_i_fsat_induction_source_prefix_product)) * c)) /\ exists ff_q_fsat_induction_source_prefix_product_factor. b = ff_q_fsat_induction_source_prefix_product_factor * S ((S (ff_i_fsat_induction_source_prefix_product)) * c) + (ff_p_fsat_induction_source_prefix_product))) /\ ((((exists ff_h_fsat_induction_source_prefix_product_partial. ff_h_fsat_induction_source_prefix_product_partial + S (ff_r_fsat_induction_source_prefix_product) = S ((S (ff_i_fsat_induction_source_prefix_product)) * ff_v_fsat_induction_source_prefix_product)) /\ exists ff_q_fsat_induction_source_prefix_product_partial. ff_u_fsat_induction_source_prefix_product = ff_q_fsat_induction_source_prefix_product_partial * S ((S (ff_i_fsat_induction_source_prefix_product)) * ff_v_fsat_induction_source_prefix_product) + (ff_r_fsat_induction_source_prefix_product))) /\ ((((exists ff_h_fsat_induction_source_prefix_product_successor. ff_h_fsat_induction_source_prefix_product_successor + S (ff_s_fsat_induction_source_prefix_product) = S ((S (S ff_i_fsat_induction_source_prefix_product)) * ff_v_fsat_induction_source_prefix_product)) /\ exists ff_q_fsat_induction_source_prefix_product_successor. ff_u_fsat_induction_source_prefix_product = ff_q_fsat_induction_source_prefix_product_successor * S ((S (S ff_i_fsat_induction_source_prefix_product)) * ff_v_fsat_induction_source_prefix_product) + (ff_s_fsat_induction_source_prefix_product))) /\ ff_s_fsat_induction_source_prefix_product = ff_r_fsat_induction_source_prefix_product * ff_p_fsat_induction_source_prefix_product)))))) /\ (forall ftsf_index_fsat_induction_source_prefix_primes. (exists ftsf_gap_fsat_induction_source_prefix_primes_bound. ftsf_gap_fsat_induction_source_prefix_primes_bound + S ftsf_index_fsat_induction_source_prefix_primes = (l)) -> exists ftsf_factor_fsat_induction_source_prefix_primes. ((((exists ff_h_ftsf_fsat_induction_source_prefix_primes_entry. ff_h_ftsf_fsat_induction_source_prefix_primes_entry + S (ftsf_factor_fsat_induction_source_prefix_primes) = S ((S (ftsf_index_fsat_induction_source_prefix_primes)) * c)) /\ exists ff_q_ftsf_fsat_induction_source_prefix_primes_entry. b = ff_q_ftsf_fsat_induction_source_prefix_primes_entry * S ((S (ftsf_index_fsat_induction_source_prefix_primes)) * c) + (ftsf_factor_fsat_induction_source_prefix_primes))) /\ ((~(ftsf_factor_fsat_induction_source_prefix_primes = 1) /\ forall frm_prime_left_ftsf_fsat_induction_source_prefix_primes_prime frm_prime_right_ftsf_fsat_induction_source_prefix_primes_prime. ftsf_factor_fsat_induction_source_prefix_primes = frm_prime_left_ftsf_fsat_induction_source_prefix_primes_prime * frm_prime_right_ftsf_fsat_induction_source_prefix_primes_prime -> frm_prime_left_ftsf_fsat_induction_source_prefix_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_induction_source_prefix_primes_prime = 1)))))))))))))
  47. 0047specialize factor_permutation_successor_decompose (n)
  48. 0048specialize factor_permutation_successor_decompose (b)
  49. 0049specialize factor_permutation_successor_decompose (c)
  50. 0050specialize factor_permutation_successor_decompose (l)
  51. 0051apply factor_permutation_successor_decompose
  52. 0052exact hA
  53. 0053cases hd
  54. 0054cases hd_witness
  55. 0055cases hd_witness_witness
  56. 0056cases hd_witness_witness_right
  57. 0057cases hd_witness_witness_right_right
  58. 0058have hmember : exists i. (exists pfp_gap_induction_member_bound. pfp_gap_induction_member_bound + S (i) = (m)) /\ (((exists ff_h_pfp_induction_member_entry. ff_h_pfp_induction_member_entry + S (x) = S ((S (i)) * e)) /\ exists ff_q_pfp_induction_member_entry. d = ff_q_pfp_induction_member_entry * S ((S (i)) * e) + (x)))
  59. 0059specialize factor_permutation_prime_member (n)
  60. 0060specialize factor_permutation_prime_member (d)
  61. 0061specialize factor_permutation_prime_member (e)
  62. 0062specialize factor_permutation_prime_member (m)
  63. 0063specialize factor_permutation_prime_member (x)
  64. 0064apply factor_permutation_prime_member
  65. 0065exact hB
  66. 0066exact hd_witness_witness_left
  67. 0067exists x1
  68. 0068trans x1 * x
  69. 0069exact hd_witness_witness_right_right_left
  70. 0070apply mul_comm
  71. 0071cases hmember
  72. 0072cases hmember_witness
  73. 0073have hmnonzero : ~(m = 0)
  74. 0074intro hzero
  75. 0075specialize factor_permutation_below_zero_impossible (x2)
  76. 0076apply factor_permutation_below_zero_impossible
  77. 0077rewrite hzero at hmember_witness_left
  78. 0078exact hmember_witness_left
  79. 0079have hpredecessor : exists t. m = S t
  80. 0080specialize nonzero_is_succ (m)
  81. 0081apply nonzero_is_succ
  82. 0082exact hmnonzero
  83. 0083cases hpredecessor
  84. 0084have hBsuccessor : (~(n = 0) /\ ((exists ff_u_fsat_induction_target_successor_product ff_v_fsat_induction_target_successor_product. ((((exists ff_h_fsat_induction_target_successor_product_start. ff_h_fsat_induction_target_successor_product_start + S (1) = S ((S (0)) * ff_v_fsat_induction_target_successor_product)) /\ exists ff_q_fsat_induction_target_successor_product_start. ff_u_fsat_induction_target_successor_product = ff_q_fsat_induction_target_successor_product_start * S ((S (0)) * ff_v_fsat_induction_target_successor_product) + (1))) /\ ((((exists ff_h_fsat_induction_target_successor_product_terminal. ff_h_fsat_induction_target_successor_product_terminal + S (n) = S ((S (S x3)) * ff_v_fsat_induction_target_successor_product)) /\ exists ff_q_fsat_induction_target_successor_product_terminal. ff_u_fsat_induction_target_successor_product = ff_q_fsat_induction_target_successor_product_terminal * S ((S (S x3)) * ff_v_fsat_induction_target_successor_product) + (n))) /\ forall ff_i_fsat_induction_target_successor_product. (exists ff_lt_fsat_induction_target_successor_product_bound. ff_lt_fsat_induction_target_successor_product_bound + S ff_i_fsat_induction_target_successor_product = S x3) -> exists ff_p_fsat_induction_target_successor_product ff_r_fsat_induction_target_successor_product ff_s_fsat_induction_target_successor_product. ((((exists ff_h_fsat_induction_target_successor_product_factor. ff_h_fsat_induction_target_successor_product_factor + S (ff_p_fsat_induction_target_successor_product) = S ((S (ff_i_fsat_induction_target_successor_product)) * e)) /\ exists ff_q_fsat_induction_target_successor_product_factor. d = ff_q_fsat_induction_target_successor_product_factor * S ((S (ff_i_fsat_induction_target_successor_product)) * e) + (ff_p_fsat_induction_target_successor_product))) /\ ((((exists ff_h_fsat_induction_target_successor_product_partial. ff_h_fsat_induction_target_successor_product_partial + S (ff_r_fsat_induction_target_successor_product) = S ((S (ff_i_fsat_induction_target_successor_product)) * ff_v_fsat_induction_target_successor_product)) /\ exists ff_q_fsat_induction_target_successor_product_partial. ff_u_fsat_induction_target_successor_product = ff_q_fsat_induction_target_successor_product_partial * S ((S (ff_i_fsat_induction_target_successor_product)) * ff_v_fsat_induction_target_successor_product) + (ff_r_fsat_induction_target_successor_product))) /\ ((((exists ff_h_fsat_induction_target_successor_product_successor. ff_h_fsat_induction_target_successor_product_successor + S (ff_s_fsat_induction_target_successor_product) = S ((S (S ff_i_fsat_induction_target_successor_product)) * ff_v_fsat_induction_target_successor_product)) /\ exists ff_q_fsat_induction_target_successor_product_successor. ff_u_fsat_induction_target_successor_product = ff_q_fsat_induction_target_successor_product_successor * S ((S (S ff_i_fsat_induction_target_successor_product)) * ff_v_fsat_induction_target_successor_product) + (ff_s_fsat_induction_target_successor_product))) /\ ff_s_fsat_induction_target_successor_product = ff_r_fsat_induction_target_successor_product * ff_p_fsat_induction_target_successor_product)))))) /\ (forall ftsf_index_fsat_induction_target_successor_primes. (exists ftsf_gap_fsat_induction_target_successor_primes_bound. ftsf_gap_fsat_induction_target_successor_primes_bound + S ftsf_index_fsat_induction_target_successor_primes = (S x3)) -> exists ftsf_factor_fsat_induction_target_successor_primes. ((((exists ff_h_ftsf_fsat_induction_target_successor_primes_entry. ff_h_ftsf_fsat_induction_target_successor_primes_entry + S (ftsf_factor_fsat_induction_target_successor_primes) = S ((S (ftsf_index_fsat_induction_target_successor_primes)) * e)) /\ exists ff_q_ftsf_fsat_induction_target_successor_primes_entry. d = ff_q_ftsf_fsat_induction_target_successor_primes_entry * S ((S (ftsf_index_fsat_induction_target_successor_primes)) * e) + (ftsf_factor_fsat_induction_target_successor_primes))) /\ ((~(ftsf_factor_fsat_induction_target_successor_primes = 1) /\ forall frm_prime_left_ftsf_fsat_induction_target_successor_primes_prime frm_prime_right_ftsf_fsat_induction_target_successor_primes_prime. ftsf_factor_fsat_induction_target_successor_primes = frm_prime_left_ftsf_fsat_induction_target_successor_primes_prime * frm_prime_right_ftsf_fsat_induction_target_successor_primes_prime -> frm_prime_left_ftsf_fsat_induction_target_successor_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_induction_target_successor_primes_prime = 1))))))
  85. 0085rewrite hpredecessor_witness at hB
  86. 0086rewrite hpredecessor_witness at hB
  87. 0087rewrite hpredecessor_witness at hB
  88. 0088rewrite hpredecessor_witness at hB
  89. 0089exact hB
  90. 0090have hbound : exists pfp_gap_induction_target_index. pfp_gap_induction_target_index + S (x2) = (S x3)
  91. 0091rewrite hpredecessor_witness at hmember_witness_left
  92. 0092exact hmember_witness_left
  93. 0093have hposition : x2 = x3 \/ (exists pfp_gap_induction_target_position. pfp_gap_induction_target_position + S (x2) = (x3))
  94. 0094specialize finite_lt_succ_eq_or_lt (x3)
  95. 0095specialize finite_lt_succ_eq_or_lt (x2)
  96. 0096apply finite_lt_succ_eq_or_lt
  97. 0097exact hbound
  98. 0098cases hposition
  99. 0099have hlast : ((exists ff_h_pfp_induction_already_last. ff_h_pfp_induction_already_last + S (x) = S ((S (x3)) * e)) /\ exists ff_q_pfp_induction_already_last. d = ff_q_pfp_induction_already_last * S ((S (x3)) * e) + (x))
  100. 0100rewrite hposition_left at hmember_witness_right
  101. 0101rewrite hposition_left at hmember_witness_right
  102. 0102exact hmember_witness_right
  103. 0103have hprefix : (~(x1 = 0) /\ ((exists ff_u_fsat_induction_direct_prefix_product ff_v_fsat_induction_direct_prefix_product. ((((exists ff_h_fsat_induction_direct_prefix_product_start. ff_h_fsat_induction_direct_prefix_product_start + S (1) = S ((S (0)) * ff_v_fsat_induction_direct_prefix_product)) /\ exists ff_q_fsat_induction_direct_prefix_product_start. ff_u_fsat_induction_direct_prefix_product = ff_q_fsat_induction_direct_prefix_product_start * S ((S (0)) * ff_v_fsat_induction_direct_prefix_product) + (1))) /\ ((((exists ff_h_fsat_induction_direct_prefix_product_terminal. ff_h_fsat_induction_direct_prefix_product_terminal + S (x1) = S ((S (x3)) * ff_v_fsat_induction_direct_prefix_product)) /\ exists ff_q_fsat_induction_direct_prefix_product_terminal. ff_u_fsat_induction_direct_prefix_product = ff_q_fsat_induction_direct_prefix_product_terminal * S ((S (x3)) * ff_v_fsat_induction_direct_prefix_product) + (x1))) /\ forall ff_i_fsat_induction_direct_prefix_product. (exists ff_lt_fsat_induction_direct_prefix_product_bound. ff_lt_fsat_induction_direct_prefix_product_bound + S ff_i_fsat_induction_direct_prefix_product = x3) -> exists ff_p_fsat_induction_direct_prefix_product ff_r_fsat_induction_direct_prefix_product ff_s_fsat_induction_direct_prefix_product. ((((exists ff_h_fsat_induction_direct_prefix_product_factor. ff_h_fsat_induction_direct_prefix_product_factor + S (ff_p_fsat_induction_direct_prefix_product) = S ((S (ff_i_fsat_induction_direct_prefix_product)) * e)) /\ exists ff_q_fsat_induction_direct_prefix_product_factor. d = ff_q_fsat_induction_direct_prefix_product_factor * S ((S (ff_i_fsat_induction_direct_prefix_product)) * e) + (ff_p_fsat_induction_direct_prefix_product))) /\ ((((exists ff_h_fsat_induction_direct_prefix_product_partial. ff_h_fsat_induction_direct_prefix_product_partial + S (ff_r_fsat_induction_direct_prefix_product) = S ((S (ff_i_fsat_induction_direct_prefix_product)) * ff_v_fsat_induction_direct_prefix_product)) /\ exists ff_q_fsat_induction_direct_prefix_product_partial. ff_u_fsat_induction_direct_prefix_product = ff_q_fsat_induction_direct_prefix_product_partial * S ((S (ff_i_fsat_induction_direct_prefix_product)) * ff_v_fsat_induction_direct_prefix_product) + (ff_r_fsat_induction_direct_prefix_product))) /\ ((((exists ff_h_fsat_induction_direct_prefix_product_successor. ff_h_fsat_induction_direct_prefix_product_successor + S (ff_s_fsat_induction_direct_prefix_product) = S ((S (S ff_i_fsat_induction_direct_prefix_product)) * ff_v_fsat_induction_direct_prefix_product)) /\ exists ff_q_fsat_induction_direct_prefix_product_successor. ff_u_fsat_induction_direct_prefix_product = ff_q_fsat_induction_direct_prefix_product_successor * S ((S (S ff_i_fsat_induction_direct_prefix_product)) * ff_v_fsat_induction_direct_prefix_product) + (ff_s_fsat_induction_direct_prefix_product))) /\ ff_s_fsat_induction_direct_prefix_product = ff_r_fsat_induction_direct_prefix_product * ff_p_fsat_induction_direct_prefix_product)))))) /\ (forall ftsf_index_fsat_induction_direct_prefix_primes. (exists ftsf_gap_fsat_induction_direct_prefix_primes_bound. ftsf_gap_fsat_induction_direct_prefix_primes_bound + S ftsf_index_fsat_induction_direct_prefix_primes = (x3)) -> exists ftsf_factor_fsat_induction_direct_prefix_primes. ((((exists ff_h_ftsf_fsat_induction_direct_prefix_primes_entry. ff_h_ftsf_fsat_induction_direct_prefix_primes_entry + S (ftsf_factor_fsat_induction_direct_prefix_primes) = S ((S (ftsf_index_fsat_induction_direct_prefix_primes)) * e)) /\ exists ff_q_ftsf_fsat_induction_direct_prefix_primes_entry. d = ff_q_ftsf_fsat_induction_direct_prefix_primes_entry * S ((S (ftsf_index_fsat_induction_direct_prefix_primes)) * e) + (ftsf_factor_fsat_induction_direct_prefix_primes))) /\ ((~(ftsf_factor_fsat_induction_direct_prefix_primes = 1) /\ forall frm_prime_left_ftsf_fsat_induction_direct_prefix_primes_prime frm_prime_right_ftsf_fsat_induction_direct_prefix_primes_prime. ftsf_factor_fsat_induction_direct_prefix_primes = frm_prime_left_ftsf_fsat_induction_direct_prefix_primes_prime * frm_prime_right_ftsf_fsat_induction_direct_prefix_primes_prime -> frm_prime_left_ftsf_fsat_induction_direct_prefix_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_induction_direct_prefix_primes_prime = 1))))))
  104. 0104specialize factor_permutation_cancel_last (n)
  105. 0105specialize factor_permutation_cancel_last (x)
  106. 0106specialize factor_permutation_cancel_last (x1)
  107. 0107specialize factor_permutation_cancel_last (d)
  108. 0108specialize factor_permutation_cancel_last (e)
  109. 0109specialize factor_permutation_cancel_last (x3)
  110. 0110apply factor_permutation_cancel_last
  111. 0111exact hBsuccessor
  112. 0112exact hlast
  113. 0113exact hd_witness_witness_right_right_left
  114. 0114have hrec : ((l = x3) /\ (exists pfp_u_induction_direct_recursion pfp_v_induction_direct_recursion. (((((forall pfp_i_induction_direct_recursionmatchingpermutationbounded. (exists pfp_gap_induction_direct_recursionmatchingpermutationboundedindex. pfp_gap_induction_direct_recursionmatchingpermutationboundedindex + S (pfp_i_induction_direct_recursionmatchingpermutationbounded) = (l)) -> exists pfp_a_induction_direct_recursionmatchingpermutationbounded. (((exists ff_h_pfp_induction_direct_recursionmatchingpermutationboundedentry. ff_h_pfp_induction_direct_recursionmatchingpermutationboundedentry + S (pfp_a_induction_direct_recursionmatchingpermutationbounded) = S ((S (pfp_i_induction_direct_recursionmatchingpermutationbounded)) * pfp_v_induction_direct_recursion)) /\ exists ff_q_pfp_induction_direct_recursionmatchingpermutationboundedentry. pfp_u_induction_direct_recursion = ff_q_pfp_induction_direct_recursionmatchingpermutationboundedentry * S ((S (pfp_i_induction_direct_recursionmatchingpermutationbounded)) * pfp_v_induction_direct_recursion) + (pfp_a_induction_direct_recursionmatchingpermutationbounded))) /\ (exists pfp_gap_induction_direct_recursionmatchingpermutationboundedvalue. pfp_gap_induction_direct_recursionmatchingpermutationboundedvalue + S (pfp_a_induction_direct_recursionmatchingpermutationbounded) = (l))) /\ (((forall pfp_i_induction_direct_recursionmatchingpermutationinjective pfp_j_induction_direct_recursionmatchingpermutationinjective pfp_a_induction_direct_recursionmatchingpermutationinjective. (exists pfp_gap_induction_direct_recursionmatchingpermutationinjectivefirst. pfp_gap_induction_direct_recursionmatchingpermutationinjectivefirst + S (pfp_i_induction_direct_recursionmatchingpermutationinjective) = (l)) -> (exists pfp_gap_induction_direct_recursionmatchingpermutationinjectivesecond. pfp_gap_induction_direct_recursionmatchingpermutationinjectivesecond + S (pfp_j_induction_direct_recursionmatchingpermutationinjective) = (l)) -> (((exists ff_h_pfp_induction_direct_recursionmatchingpermutationinjectiveleft. ff_h_pfp_induction_direct_recursionmatchingpermutationinjectiveleft + S (pfp_a_induction_direct_recursionmatchingpermutationinjective) = S ((S (pfp_i_induction_direct_recursionmatchingpermutationinjective)) * pfp_v_induction_direct_recursion)) /\ exists ff_q_pfp_induction_direct_recursionmatchingpermutationinjectiveleft. pfp_u_induction_direct_recursion = ff_q_pfp_induction_direct_recursionmatchingpermutationinjectiveleft * S ((S (pfp_i_induction_direct_recursionmatchingpermutationinjective)) * pfp_v_induction_direct_recursion) + (pfp_a_induction_direct_recursionmatchingpermutationinjective))) -> (((exists ff_h_pfp_induction_direct_recursionmatchingpermutationinjectiveright. ff_h_pfp_induction_direct_recursionmatchingpermutationinjectiveright + S (pfp_a_induction_direct_recursionmatchingpermutationinjective) = S ((S (pfp_j_induction_direct_recursionmatchingpermutationinjective)) * pfp_v_induction_direct_recursion)) /\ exists ff_q_pfp_induction_direct_recursionmatchingpermutationinjectiveright. pfp_u_induction_direct_recursion = ff_q_pfp_induction_direct_recursionmatchingpermutationinjectiveright * S ((S (pfp_j_induction_direct_recursionmatchingpermutationinjective)) * pfp_v_induction_direct_recursion) + (pfp_a_induction_direct_recursionmatchingpermutationinjective))) -> pfp_i_induction_direct_recursionmatchingpermutationinjective = pfp_j_induction_direct_recursionmatchingpermutationinjective) /\ (forall pfp_a_induction_direct_recursionmatchingpermutationsurjective. (exists pfp_gap_induction_direct_recursionmatchingpermutationsurjectivevalue. pfp_gap_induction_direct_recursionmatchingpermutationsurjectivevalue + S (pfp_a_induction_direct_recursionmatchingpermutationsurjective) = (l)) -> exists pfp_i_induction_direct_recursionmatchingpermutationsurjective. (exists pfp_gap_induction_direct_recursionmatchingpermutationsurjectiveindex. pfp_gap_induction_direct_recursionmatchingpermutationsurjectiveindex + S (pfp_i_induction_direct_recursionmatchingpermutationsurjective) = (l)) /\ (((exists ff_h_pfp_induction_direct_recursionmatchingpermutationsurjectiveentry. ff_h_pfp_induction_direct_recursionmatchingpermutationsurjectiveentry + S (pfp_a_induction_direct_recursionmatchingpermutationsurjective) = S ((S (pfp_i_induction_direct_recursionmatchingpermutationsurjective)) * pfp_v_induction_direct_recursion)) /\ exists ff_q_pfp_induction_direct_recursionmatchingpermutationsurjectiveentry. pfp_u_induction_direct_recursion = ff_q_pfp_induction_direct_recursionmatchingpermutationsurjectiveentry * S ((S (pfp_i_induction_direct_recursionmatchingpermutationsurjective)) * pfp_v_induction_direct_recursion) + (pfp_a_induction_direct_recursionmatchingpermutationsurjective)))))))) /\ (forall pfp_i_induction_direct_recursionmatchingmatching pfp_j_induction_direct_recursionmatchingmatching pfp_a_induction_direct_recursionmatchingmatching. (exists pfp_gap_induction_direct_recursionmatchingmatchingbound. pfp_gap_induction_direct_recursionmatchingmatchingbound + S (pfp_i_induction_direct_recursionmatchingmatching) = (l)) -> (((exists ff_h_pfp_induction_direct_recursionmatchingmatchingmap. ff_h_pfp_induction_direct_recursionmatchingmatchingmap + S (pfp_j_induction_direct_recursionmatchingmatching) = S ((S (pfp_i_induction_direct_recursionmatchingmatching)) * pfp_v_induction_direct_recursion)) /\ exists ff_q_pfp_induction_direct_recursionmatchingmatchingmap. pfp_u_induction_direct_recursion = ff_q_pfp_induction_direct_recursionmatchingmatchingmap * S ((S (pfp_i_induction_direct_recursionmatchingmatching)) * pfp_v_induction_direct_recursion) + (pfp_j_induction_direct_recursionmatchingmatching))) -> (((exists ff_h_pfp_induction_direct_recursionmatchingmatchingsource. ff_h_pfp_induction_direct_recursionmatchingmatchingsource + S (pfp_a_induction_direct_recursionmatchingmatching) = S ((S (pfp_i_induction_direct_recursionmatchingmatching)) * c)) /\ exists ff_q_pfp_induction_direct_recursionmatchingmatchingsource. b = ff_q_pfp_induction_direct_recursionmatchingmatchingsource * S ((S (pfp_i_induction_direct_recursionmatchingmatching)) * c) + (pfp_a_induction_direct_recursionmatchingmatching))) -> (((exists ff_h_pfp_induction_direct_recursionmatchingmatchingtarget. ff_h_pfp_induction_direct_recursionmatchingmatchingtarget + S (pfp_a_induction_direct_recursionmatchingmatching) = S ((S (pfp_j_induction_direct_recursionmatchingmatching)) * e)) /\ exists ff_q_pfp_induction_direct_recursionmatchingmatchingtarget. d = ff_q_pfp_induction_direct_recursionmatchingmatchingtarget * S ((S (pfp_j_induction_direct_recursionmatchingmatching)) * e) + (pfp_a_induction_direct_recursionmatchingmatching))))))))
  115. 0115specialize IH (x1)
  116. 0116specialize IH (b)
  117. 0117specialize IH (c)
  118. 0118specialize IH (x3)
  119. 0119specialize IH (d)
  120. 0120specialize IH (e)
  121. 0121apply IH
  122. 0122exact hd_witness_witness_right_right_right
  123. 0123exact hprefix
  124. 0124cases hrec
  125. 0125cases hrec_right
  126. 0126cases hrec_right_witness
  127. 0127have hlastaligned : ((exists ff_h_pfp_induction_direct_aligned_last. ff_h_pfp_induction_direct_aligned_last + S (x) = S ((S (l)) * e)) /\ exists ff_q_pfp_induction_direct_aligned_last. d = ff_q_pfp_induction_direct_aligned_last * S ((S (l)) * e) + (x))
  128. 0128rewrite hrec_left
  129. 0129rewrite hrec_left
  130. 0130exact hlast
  131. 0131split
  132. 0132trans S x3
  133. 0133congr
  134. 0134exact hrec_left
  135. 0135symm
  136. 0136exact hpredecessor_witness
  137. 0137specialize factor_permutation_matched_append_exists (b)
  138. 0138specialize factor_permutation_matched_append_exists (c)
  139. 0139specialize factor_permutation_matched_append_exists (d)
  140. 0140specialize factor_permutation_matched_append_exists (e)
  141. 0141specialize factor_permutation_matched_append_exists (x4)
  142. 0142specialize factor_permutation_matched_append_exists (x5)
  143. 0143specialize factor_permutation_matched_append_exists (l)
  144. 0144specialize factor_permutation_matched_append_exists (x)
  145. 0145apply factor_permutation_matched_append_exists
  146. 0146exact hrec_right_witness_witness
  147. 0147exact hd_witness_witness_right_left
  148. 0148exact hlastaligned
  149. 0149have hswap : exists B C q. ((((~(n = 0) /\ ((exists ff_u_fsat_induction_recoded_factorization_product ff_v_fsat_induction_recoded_factorization_product. ((((exists ff_h_fsat_induction_recoded_factorization_product_start. ff_h_fsat_induction_recoded_factorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_induction_recoded_factorization_product)) /\ exists ff_q_fsat_induction_recoded_factorization_product_start. ff_u_fsat_induction_recoded_factorization_product = ff_q_fsat_induction_recoded_factorization_product_start * S ((S (0)) * ff_v_fsat_induction_recoded_factorization_product) + (1))) /\ ((((exists ff_h_fsat_induction_recoded_factorization_product_terminal. ff_h_fsat_induction_recoded_factorization_product_terminal + S (n) = S ((S (S x3)) * ff_v_fsat_induction_recoded_factorization_product)) /\ exists ff_q_fsat_induction_recoded_factorization_product_terminal. ff_u_fsat_induction_recoded_factorization_product = ff_q_fsat_induction_recoded_factorization_product_terminal * S ((S (S x3)) * ff_v_fsat_induction_recoded_factorization_product) + (n))) /\ forall ff_i_fsat_induction_recoded_factorization_product. (exists ff_lt_fsat_induction_recoded_factorization_product_bound. ff_lt_fsat_induction_recoded_factorization_product_bound + S ff_i_fsat_induction_recoded_factorization_product = S x3) -> exists ff_p_fsat_induction_recoded_factorization_product ff_r_fsat_induction_recoded_factorization_product ff_s_fsat_induction_recoded_factorization_product. ((((exists ff_h_fsat_induction_recoded_factorization_product_factor. ff_h_fsat_induction_recoded_factorization_product_factor + S (ff_p_fsat_induction_recoded_factorization_product) = S ((S (ff_i_fsat_induction_recoded_factorization_product)) * C)) /\ exists ff_q_fsat_induction_recoded_factorization_product_factor. B = ff_q_fsat_induction_recoded_factorization_product_factor * S ((S (ff_i_fsat_induction_recoded_factorization_product)) * C) + (ff_p_fsat_induction_recoded_factorization_product))) /\ ((((exists ff_h_fsat_induction_recoded_factorization_product_partial. ff_h_fsat_induction_recoded_factorization_product_partial + S (ff_r_fsat_induction_recoded_factorization_product) = S ((S (ff_i_fsat_induction_recoded_factorization_product)) * ff_v_fsat_induction_recoded_factorization_product)) /\ exists ff_q_fsat_induction_recoded_factorization_product_partial. ff_u_fsat_induction_recoded_factorization_product = ff_q_fsat_induction_recoded_factorization_product_partial * S ((S (ff_i_fsat_induction_recoded_factorization_product)) * ff_v_fsat_induction_recoded_factorization_product) + (ff_r_fsat_induction_recoded_factorization_product))) /\ ((((exists ff_h_fsat_induction_recoded_factorization_product_successor. ff_h_fsat_induction_recoded_factorization_product_successor + S (ff_s_fsat_induction_recoded_factorization_product) = S ((S (S ff_i_fsat_induction_recoded_factorization_product)) * ff_v_fsat_induction_recoded_factorization_product)) /\ exists ff_q_fsat_induction_recoded_factorization_product_successor. ff_u_fsat_induction_recoded_factorization_product = ff_q_fsat_induction_recoded_factorization_product_successor * S ((S (S ff_i_fsat_induction_recoded_factorization_product)) * ff_v_fsat_induction_recoded_factorization_product) + (ff_s_fsat_induction_recoded_factorization_product))) /\ ff_s_fsat_induction_recoded_factorization_product = ff_r_fsat_induction_recoded_factorization_product * ff_p_fsat_induction_recoded_factorization_product)))))) /\ (forall ftsf_index_fsat_induction_recoded_factorization_primes. (exists ftsf_gap_fsat_induction_recoded_factorization_primes_bound. ftsf_gap_fsat_induction_recoded_factorization_primes_bound + S ftsf_index_fsat_induction_recoded_factorization_primes = (S x3)) -> exists ftsf_factor_fsat_induction_recoded_factorization_primes. ((((exists ff_h_ftsf_fsat_induction_recoded_factorization_primes_entry. ff_h_ftsf_fsat_induction_recoded_factorization_primes_entry + S (ftsf_factor_fsat_induction_recoded_factorization_primes) = S ((S (ftsf_index_fsat_induction_recoded_factorization_primes)) * C)) /\ exists ff_q_ftsf_fsat_induction_recoded_factorization_primes_entry. B = ff_q_ftsf_fsat_induction_recoded_factorization_primes_entry * S ((S (ftsf_index_fsat_induction_recoded_factorization_primes)) * C) + (ftsf_factor_fsat_induction_recoded_factorization_primes))) /\ ((~(ftsf_factor_fsat_induction_recoded_factorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_induction_recoded_factorization_primes_prime frm_prime_right_ftsf_fsat_induction_recoded_factorization_primes_prime. ftsf_factor_fsat_induction_recoded_factorization_primes = frm_prime_left_ftsf_fsat_induction_recoded_factorization_primes_prime * frm_prime_right_ftsf_fsat_induction_recoded_factorization_primes_prime -> frm_prime_left_ftsf_fsat_induction_recoded_factorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_induction_recoded_factorization_primes_prime = 1))))))) /\ (((((exists ff_h_pfp_induction_target_swapoldi. ff_h_pfp_induction_target_swapoldi + S (x) = S ((S (x2)) * e)) /\ exists ff_q_pfp_induction_target_swapoldi. d = ff_q_pfp_induction_target_swapoldi * S ((S (x2)) * e) + (x))) /\ (((((exists ff_h_pfp_induction_target_swapoldlast. ff_h_pfp_induction_target_swapoldlast + S (q) = S ((S (x3)) * e)) /\ exists ff_q_pfp_induction_target_swapoldlast. d = ff_q_pfp_induction_target_swapoldlast * S ((S (x3)) * e) + (q))) /\ (((((exists ff_h_pfp_induction_target_swapnewi. ff_h_pfp_induction_target_swapnewi + S (q) = S ((S (x2)) * C)) /\ exists ff_q_pfp_induction_target_swapnewi. B = ff_q_pfp_induction_target_swapnewi * S ((S (x2)) * C) + (q))) /\ (((((exists ff_h_pfp_induction_target_swapnewlast. ff_h_pfp_induction_target_swapnewlast + S (x) = S ((S (x3)) * C)) /\ exists ff_q_pfp_induction_target_swapnewlast. B = ff_q_pfp_induction_target_swapnewlast * S ((S (x3)) * C) + (x))) /\ (forall pfp_j_induction_target_swap pfp_a_induction_target_swap. (exists pfp_gap_induction_target_swapbound. pfp_gap_induction_target_swapbound + S (pfp_j_induction_target_swap) = (S (x3))) -> ~(pfp_j_induction_target_swap = x2) -> ~(pfp_j_induction_target_swap = x3) -> (((exists ff_h_pfp_induction_target_swapold. ff_h_pfp_induction_target_swapold + S (pfp_a_induction_target_swap) = S ((S (pfp_j_induction_target_swap)) * e)) /\ exists ff_q_pfp_induction_target_swapold. d = ff_q_pfp_induction_target_swapold * S ((S (pfp_j_induction_target_swap)) * e) + (pfp_a_induction_target_swap))) -> (((exists ff_h_pfp_induction_target_swapnew. ff_h_pfp_induction_target_swapnew + S (pfp_a_induction_target_swap) = S ((S (pfp_j_induction_target_swap)) * C)) /\ exists ff_q_pfp_induction_target_swapnew. B = ff_q_pfp_induction_target_swapnew * S ((S (pfp_j_induction_target_swap)) * C) + (pfp_a_induction_target_swap))))))))))))))
  150. 0150specialize factor_permutation_swapped_factorization_exists (n)
  151. 0151specialize factor_permutation_swapped_factorization_exists (d)
  152. 0152specialize factor_permutation_swapped_factorization_exists (e)
  153. 0153specialize factor_permutation_swapped_factorization_exists (x3)
  154. 0154specialize factor_permutation_swapped_factorization_exists (x2)
  155. 0155specialize factor_permutation_swapped_factorization_exists (x)
  156. 0156apply factor_permutation_swapped_factorization_exists
  157. 0157exact hBsuccessor
  158. 0158exact hposition_right
  159. 0159exact hmember_witness_right
  160. 0160cases hswap
  161. 0161cases hswap_witness
  162. 0162cases hswap_witness_witness
  163. 0163cases hswap_witness_witness_witness
  164. 0164have hlast : ((exists ff_h_pfp_induction_recoded_last. ff_h_pfp_induction_recoded_last + S (x) = S ((S (x3)) * x5)) /\ exists ff_q_pfp_induction_recoded_last. x4 = ff_q_pfp_induction_recoded_last * S ((S (x3)) * x5) + (x))
  165. 0165cases hswap_witness_witness_witness_right
  166. 0166cases hswap_witness_witness_witness_right_right
  167. 0167cases hswap_witness_witness_witness_right_right_right
  168. 0168cases hswap_witness_witness_witness_right_right_right_right
  169. 0169exact hswap_witness_witness_witness_right_right_right_right_left
  170. 0170have hprefix : (~(x1 = 0) /\ ((exists ff_u_fsat_induction_recoded_prefix_product ff_v_fsat_induction_recoded_prefix_product. ((((exists ff_h_fsat_induction_recoded_prefix_product_start. ff_h_fsat_induction_recoded_prefix_product_start + S (1) = S ((S (0)) * ff_v_fsat_induction_recoded_prefix_product)) /\ exists ff_q_fsat_induction_recoded_prefix_product_start. ff_u_fsat_induction_recoded_prefix_product = ff_q_fsat_induction_recoded_prefix_product_start * S ((S (0)) * ff_v_fsat_induction_recoded_prefix_product) + (1))) /\ ((((exists ff_h_fsat_induction_recoded_prefix_product_terminal. ff_h_fsat_induction_recoded_prefix_product_terminal + S (x1) = S ((S (x3)) * ff_v_fsat_induction_recoded_prefix_product)) /\ exists ff_q_fsat_induction_recoded_prefix_product_terminal. ff_u_fsat_induction_recoded_prefix_product = ff_q_fsat_induction_recoded_prefix_product_terminal * S ((S (x3)) * ff_v_fsat_induction_recoded_prefix_product) + (x1))) /\ forall ff_i_fsat_induction_recoded_prefix_product. (exists ff_lt_fsat_induction_recoded_prefix_product_bound. ff_lt_fsat_induction_recoded_prefix_product_bound + S ff_i_fsat_induction_recoded_prefix_product = x3) -> exists ff_p_fsat_induction_recoded_prefix_product ff_r_fsat_induction_recoded_prefix_product ff_s_fsat_induction_recoded_prefix_product. ((((exists ff_h_fsat_induction_recoded_prefix_product_factor. ff_h_fsat_induction_recoded_prefix_product_factor + S (ff_p_fsat_induction_recoded_prefix_product) = S ((S (ff_i_fsat_induction_recoded_prefix_product)) * x5)) /\ exists ff_q_fsat_induction_recoded_prefix_product_factor. x4 = ff_q_fsat_induction_recoded_prefix_product_factor * S ((S (ff_i_fsat_induction_recoded_prefix_product)) * x5) + (ff_p_fsat_induction_recoded_prefix_product))) /\ ((((exists ff_h_fsat_induction_recoded_prefix_product_partial. ff_h_fsat_induction_recoded_prefix_product_partial + S (ff_r_fsat_induction_recoded_prefix_product) = S ((S (ff_i_fsat_induction_recoded_prefix_product)) * ff_v_fsat_induction_recoded_prefix_product)) /\ exists ff_q_fsat_induction_recoded_prefix_product_partial. ff_u_fsat_induction_recoded_prefix_product = ff_q_fsat_induction_recoded_prefix_product_partial * S ((S (ff_i_fsat_induction_recoded_prefix_product)) * ff_v_fsat_induction_recoded_prefix_product) + (ff_r_fsat_induction_recoded_prefix_product))) /\ ((((exists ff_h_fsat_induction_recoded_prefix_product_successor. ff_h_fsat_induction_recoded_prefix_product_successor + S (ff_s_fsat_induction_recoded_prefix_product) = S ((S (S ff_i_fsat_induction_recoded_prefix_product)) * ff_v_fsat_induction_recoded_prefix_product)) /\ exists ff_q_fsat_induction_recoded_prefix_product_successor. ff_u_fsat_induction_recoded_prefix_product = ff_q_fsat_induction_recoded_prefix_product_successor * S ((S (S ff_i_fsat_induction_recoded_prefix_product)) * ff_v_fsat_induction_recoded_prefix_product) + (ff_s_fsat_induction_recoded_prefix_product))) /\ ff_s_fsat_induction_recoded_prefix_product = ff_r_fsat_induction_recoded_prefix_product * ff_p_fsat_induction_recoded_prefix_product)))))) /\ (forall ftsf_index_fsat_induction_recoded_prefix_primes. (exists ftsf_gap_fsat_induction_recoded_prefix_primes_bound. ftsf_gap_fsat_induction_recoded_prefix_primes_bound + S ftsf_index_fsat_induction_recoded_prefix_primes = (x3)) -> exists ftsf_factor_fsat_induction_recoded_prefix_primes. ((((exists ff_h_ftsf_fsat_induction_recoded_prefix_primes_entry. ff_h_ftsf_fsat_induction_recoded_prefix_primes_entry + S (ftsf_factor_fsat_induction_recoded_prefix_primes) = S ((S (ftsf_index_fsat_induction_recoded_prefix_primes)) * x5)) /\ exists ff_q_ftsf_fsat_induction_recoded_prefix_primes_entry. x4 = ff_q_ftsf_fsat_induction_recoded_prefix_primes_entry * S ((S (ftsf_index_fsat_induction_recoded_prefix_primes)) * x5) + (ftsf_factor_fsat_induction_recoded_prefix_primes))) /\ ((~(ftsf_factor_fsat_induction_recoded_prefix_primes = 1) /\ forall frm_prime_left_ftsf_fsat_induction_recoded_prefix_primes_prime frm_prime_right_ftsf_fsat_induction_recoded_prefix_primes_prime. ftsf_factor_fsat_induction_recoded_prefix_primes = frm_prime_left_ftsf_fsat_induction_recoded_prefix_primes_prime * frm_prime_right_ftsf_fsat_induction_recoded_prefix_primes_prime -> frm_prime_left_ftsf_fsat_induction_recoded_prefix_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_induction_recoded_prefix_primes_prime = 1))))))
  171. 0171specialize factor_permutation_cancel_last (n)
  172. 0172specialize factor_permutation_cancel_last (x)
  173. 0173specialize factor_permutation_cancel_last (x1)
  174. 0174specialize factor_permutation_cancel_last (x4)
  175. 0175specialize factor_permutation_cancel_last (x5)
  176. 0176specialize factor_permutation_cancel_last (x3)
  177. 0177apply factor_permutation_cancel_last
  178. 0178exact hswap_witness_witness_witness_left
  179. 0179exact hlast
  180. 0180exact hd_witness_witness_right_right_left
  181. 0181have hrec : ((l = x3) /\ (exists pfp_u_induction_recoded_recursion pfp_v_induction_recoded_recursion. (((((forall pfp_i_induction_recoded_recursionmatchingpermutationbounded. (exists pfp_gap_induction_recoded_recursionmatchingpermutationboundedindex. pfp_gap_induction_recoded_recursionmatchingpermutationboundedindex + S (pfp_i_induction_recoded_recursionmatchingpermutationbounded) = (l)) -> exists pfp_a_induction_recoded_recursionmatchingpermutationbounded. (((exists ff_h_pfp_induction_recoded_recursionmatchingpermutationboundedentry. ff_h_pfp_induction_recoded_recursionmatchingpermutationboundedentry + S (pfp_a_induction_recoded_recursionmatchingpermutationbounded) = S ((S (pfp_i_induction_recoded_recursionmatchingpermutationbounded)) * pfp_v_induction_recoded_recursion)) /\ exists ff_q_pfp_induction_recoded_recursionmatchingpermutationboundedentry. pfp_u_induction_recoded_recursion = ff_q_pfp_induction_recoded_recursionmatchingpermutationboundedentry * S ((S (pfp_i_induction_recoded_recursionmatchingpermutationbounded)) * pfp_v_induction_recoded_recursion) + (pfp_a_induction_recoded_recursionmatchingpermutationbounded))) /\ (exists pfp_gap_induction_recoded_recursionmatchingpermutationboundedvalue. pfp_gap_induction_recoded_recursionmatchingpermutationboundedvalue + S (pfp_a_induction_recoded_recursionmatchingpermutationbounded) = (l))) /\ (((forall pfp_i_induction_recoded_recursionmatchingpermutationinjective pfp_j_induction_recoded_recursionmatchingpermutationinjective pfp_a_induction_recoded_recursionmatchingpermutationinjective. (exists pfp_gap_induction_recoded_recursionmatchingpermutationinjectivefirst. pfp_gap_induction_recoded_recursionmatchingpermutationinjectivefirst + S (pfp_i_induction_recoded_recursionmatchingpermutationinjective) = (l)) -> (exists pfp_gap_induction_recoded_recursionmatchingpermutationinjectivesecond. pfp_gap_induction_recoded_recursionmatchingpermutationinjectivesecond + S (pfp_j_induction_recoded_recursionmatchingpermutationinjective) = (l)) -> (((exists ff_h_pfp_induction_recoded_recursionmatchingpermutationinjectiveleft. ff_h_pfp_induction_recoded_recursionmatchingpermutationinjectiveleft + S (pfp_a_induction_recoded_recursionmatchingpermutationinjective) = S ((S (pfp_i_induction_recoded_recursionmatchingpermutationinjective)) * pfp_v_induction_recoded_recursion)) /\ exists ff_q_pfp_induction_recoded_recursionmatchingpermutationinjectiveleft. pfp_u_induction_recoded_recursion = ff_q_pfp_induction_recoded_recursionmatchingpermutationinjectiveleft * S ((S (pfp_i_induction_recoded_recursionmatchingpermutationinjective)) * pfp_v_induction_recoded_recursion) + (pfp_a_induction_recoded_recursionmatchingpermutationinjective))) -> (((exists ff_h_pfp_induction_recoded_recursionmatchingpermutationinjectiveright. ff_h_pfp_induction_recoded_recursionmatchingpermutationinjectiveright + S (pfp_a_induction_recoded_recursionmatchingpermutationinjective) = S ((S (pfp_j_induction_recoded_recursionmatchingpermutationinjective)) * pfp_v_induction_recoded_recursion)) /\ exists ff_q_pfp_induction_recoded_recursionmatchingpermutationinjectiveright. pfp_u_induction_recoded_recursion = ff_q_pfp_induction_recoded_recursionmatchingpermutationinjectiveright * S ((S (pfp_j_induction_recoded_recursionmatchingpermutationinjective)) * pfp_v_induction_recoded_recursion) + (pfp_a_induction_recoded_recursionmatchingpermutationinjective))) -> pfp_i_induction_recoded_recursionmatchingpermutationinjective = pfp_j_induction_recoded_recursionmatchingpermutationinjective) /\ (forall pfp_a_induction_recoded_recursionmatchingpermutationsurjective. (exists pfp_gap_induction_recoded_recursionmatchingpermutationsurjectivevalue. pfp_gap_induction_recoded_recursionmatchingpermutationsurjectivevalue + S (pfp_a_induction_recoded_recursionmatchingpermutationsurjective) = (l)) -> exists pfp_i_induction_recoded_recursionmatchingpermutationsurjective. (exists pfp_gap_induction_recoded_recursionmatchingpermutationsurjectiveindex. pfp_gap_induction_recoded_recursionmatchingpermutationsurjectiveindex + S (pfp_i_induction_recoded_recursionmatchingpermutationsurjective) = (l)) /\ (((exists ff_h_pfp_induction_recoded_recursionmatchingpermutationsurjectiveentry. ff_h_pfp_induction_recoded_recursionmatchingpermutationsurjectiveentry + S (pfp_a_induction_recoded_recursionmatchingpermutationsurjective) = S ((S (pfp_i_induction_recoded_recursionmatchingpermutationsurjective)) * pfp_v_induction_recoded_recursion)) /\ exists ff_q_pfp_induction_recoded_recursionmatchingpermutationsurjectiveentry. pfp_u_induction_recoded_recursion = ff_q_pfp_induction_recoded_recursionmatchingpermutationsurjectiveentry * S ((S (pfp_i_induction_recoded_recursionmatchingpermutationsurjective)) * pfp_v_induction_recoded_recursion) + (pfp_a_induction_recoded_recursionmatchingpermutationsurjective)))))))) /\ (forall pfp_i_induction_recoded_recursionmatchingmatching pfp_j_induction_recoded_recursionmatchingmatching pfp_a_induction_recoded_recursionmatchingmatching. (exists pfp_gap_induction_recoded_recursionmatchingmatchingbound. pfp_gap_induction_recoded_recursionmatchingmatchingbound + S (pfp_i_induction_recoded_recursionmatchingmatching) = (l)) -> (((exists ff_h_pfp_induction_recoded_recursionmatchingmatchingmap. ff_h_pfp_induction_recoded_recursionmatchingmatchingmap + S (pfp_j_induction_recoded_recursionmatchingmatching) = S ((S (pfp_i_induction_recoded_recursionmatchingmatching)) * pfp_v_induction_recoded_recursion)) /\ exists ff_q_pfp_induction_recoded_recursionmatchingmatchingmap. pfp_u_induction_recoded_recursion = ff_q_pfp_induction_recoded_recursionmatchingmatchingmap * S ((S (pfp_i_induction_recoded_recursionmatchingmatching)) * pfp_v_induction_recoded_recursion) + (pfp_j_induction_recoded_recursionmatchingmatching))) -> (((exists ff_h_pfp_induction_recoded_recursionmatchingmatchingsource. ff_h_pfp_induction_recoded_recursionmatchingmatchingsource + S (pfp_a_induction_recoded_recursionmatchingmatching) = S ((S (pfp_i_induction_recoded_recursionmatchingmatching)) * c)) /\ exists ff_q_pfp_induction_recoded_recursionmatchingmatchingsource. b = ff_q_pfp_induction_recoded_recursionmatchingmatchingsource * S ((S (pfp_i_induction_recoded_recursionmatchingmatching)) * c) + (pfp_a_induction_recoded_recursionmatchingmatching))) -> (((exists ff_h_pfp_induction_recoded_recursionmatchingmatchingtarget. ff_h_pfp_induction_recoded_recursionmatchingmatchingtarget + S (pfp_a_induction_recoded_recursionmatchingmatching) = S ((S (pfp_j_induction_recoded_recursionmatchingmatching)) * x5)) /\ exists ff_q_pfp_induction_recoded_recursionmatchingmatchingtarget. x4 = ff_q_pfp_induction_recoded_recursionmatchingmatchingtarget * S ((S (pfp_j_induction_recoded_recursionmatchingmatching)) * x5) + (pfp_a_induction_recoded_recursionmatchingmatching))))))))
  182. 0182specialize IH (x1)
  183. 0183specialize IH (b)
  184. 0184specialize IH (c)
  185. 0185specialize IH (x3)
  186. 0186specialize IH (x4)
  187. 0187specialize IH (x5)
  188. 0188apply IH
  189. 0189exact hd_witness_witness_right_right_right
  190. 0190exact hprefix
  191. 0191cases hrec
  192. 0192cases hrec_right
  193. 0193cases hrec_right_witness
  194. 0194have hpivot : exists pfp_gap_induction_pivot_aligned. pfp_gap_induction_pivot_aligned + S (x2) = (l)
  195. 0195rewrite hrec_left
  196. 0196exact hposition_right
  197. 0197have hswapaligned : ((((exists ff_h_pfp_induction_swap_alignedoldi. ff_h_pfp_induction_swap_alignedoldi + S (x) = S ((S (x2)) * e)) /\ exists ff_q_pfp_induction_swap_alignedoldi. d = ff_q_pfp_induction_swap_alignedoldi * S ((S (x2)) * e) + (x))) /\ (((((exists ff_h_pfp_induction_swap_alignedoldlast. ff_h_pfp_induction_swap_alignedoldlast + S (x6) = S ((S (l)) * e)) /\ exists ff_q_pfp_induction_swap_alignedoldlast. d = ff_q_pfp_induction_swap_alignedoldlast * S ((S (l)) * e) + (x6))) /\ (((((exists ff_h_pfp_induction_swap_alignednewi. ff_h_pfp_induction_swap_alignednewi + S (x6) = S ((S (x2)) * x5)) /\ exists ff_q_pfp_induction_swap_alignednewi. x4 = ff_q_pfp_induction_swap_alignednewi * S ((S (x2)) * x5) + (x6))) /\ (((((exists ff_h_pfp_induction_swap_alignednewlast. ff_h_pfp_induction_swap_alignednewlast + S (x) = S ((S (l)) * x5)) /\ exists ff_q_pfp_induction_swap_alignednewlast. x4 = ff_q_pfp_induction_swap_alignednewlast * S ((S (l)) * x5) + (x))) /\ (forall pfp_j_induction_swap_aligned pfp_a_induction_swap_aligned. (exists pfp_gap_induction_swap_alignedbound. pfp_gap_induction_swap_alignedbound + S (pfp_j_induction_swap_aligned) = (S (l))) -> ~(pfp_j_induction_swap_aligned = x2) -> ~(pfp_j_induction_swap_aligned = l) -> (((exists ff_h_pfp_induction_swap_alignedold. ff_h_pfp_induction_swap_alignedold + S (pfp_a_induction_swap_aligned) = S ((S (pfp_j_induction_swap_aligned)) * e)) /\ exists ff_q_pfp_induction_swap_alignedold. d = ff_q_pfp_induction_swap_alignedold * S ((S (pfp_j_induction_swap_aligned)) * e) + (pfp_a_induction_swap_aligned))) -> (((exists ff_h_pfp_induction_swap_alignednew. ff_h_pfp_induction_swap_alignednew + S (pfp_a_induction_swap_aligned) = S ((S (pfp_j_induction_swap_aligned)) * x5)) /\ exists ff_q_pfp_induction_swap_alignednew. x4 = ff_q_pfp_induction_swap_alignednew * S ((S (pfp_j_induction_swap_aligned)) * x5) + (pfp_a_induction_swap_aligned)))))))))))
  198. 0198rewrite hrec_left
  199. 0199rewrite hrec_left
  200. 0200rewrite hrec_left
  201. 0201rewrite hrec_left
  202. 0202rewrite hrec_left
  203. 0203rewrite hrec_left
  204. 0204exact hswap_witness_witness_witness_right
  205. 0205split
  206. 0206trans S x3
  207. 0207congr
  208. 0208exact hrec_left
  209. 0209symm
  210. 0210exact hpredecessor_witness
  211. 0211specialize factor_permutation_matched_unswap_exists (b)
  212. 0212specialize factor_permutation_matched_unswap_exists (c)
  213. 0213specialize factor_permutation_matched_unswap_exists (d)
  214. 0214specialize factor_permutation_matched_unswap_exists (e)
  215. 0215specialize factor_permutation_matched_unswap_exists (x4)
  216. 0216specialize factor_permutation_matched_unswap_exists (x5)
  217. 0217specialize factor_permutation_matched_unswap_exists (x7)
  218. 0218specialize factor_permutation_matched_unswap_exists (x8)
  219. 0219specialize factor_permutation_matched_unswap_exists (l)
  220. 0220specialize factor_permutation_matched_unswap_exists (x2)
  221. 0221specialize factor_permutation_matched_unswap_exists (x)
  222. 0222specialize factor_permutation_matched_unswap_exists (x6)
  223. 0223apply factor_permutation_matched_unswap_exists
  224. 0224exact hpivot
  225. 0225exact hrec_right_witness_witness
  226. 0226exact hd_witness_witness_right_left
  227. 0227exact hswapaligned