AF0019

prime_factor_lists_matching_by_length

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.

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

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.

The original division, gcd, cancellation, and factor-existence foundations are exposed through checked wrappers. Unordered uniqueness adds an actual bounded, injective, surjective index map matching repeated prime occurrences. The empty factor list represents one, not zero.

Exact theorem in conservative defined notation

∀ l. ∀ n. ∀ b. ∀ c. ∀ m. ∀ d. ∀ e. PrimeFactorList(n,b,c,l) → PrimeFactorList(n,d,e,m) → l = m ∧ (∃ x. ∃ y. PermutationPrefix(x,y,l) ∧ FactorListMatching(b,c,d,e,x,y,l))

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

PermutationPrefix(b,c,l) · 3PrimeFactorList(n,b,c,l) · 7FactorListMatching(b,c,d,e,u,v,l) · 3Lt(a,b) · 6Prime(p) · 1BetaAt(b,c,i,x) · 17Product(b,c,l,z) · 1

Actual proof prerequisites

beta_product_zero · checked external prerequisitefactor_permutation_unit_length_zerofactor_permutation_empty_matchingfactor_permutation_successor_decomposefactor_permutation_prime_membermul_comm · checked external prerequisitefactor_permutation_below_zero_impossiblenonzero_is_succ · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisitefactor_permutation_cancel_lastfactor_permutation_matched_append_existsfactor_permutation_swapped_factorization_existsfactor_permutation_matched_unswap_exists
Original expanded first-order 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)))))))))

Complete tactic proof in conservative notation

All 227 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

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

Named ingredients (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
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(b,c,0,n)Original native command in the exact edition
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: Prime(p)BetaAt(b,c,l,p)PrimeFactorList(r,b,c,l)Original native command in the exact edition
  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 : ∃ i. Lt(i,m) ∧ BetaAt(d,e,i,x)Definitions: Lt(i,m)BetaAt(d,e,i,x)Original native command in the exact edition
  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(n,d,e,S x3)Original native command in the exact edition
  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 : Lt(x2,S x3)Definitions: Lt(x2,S x3)Original native command in the exact edition
  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 ∨ Lt(x2,x3)Definitions: Lt(x2,x3)Original native command in the exact edition
  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 : BetaAt(d,e,x3,x)Definitions: BetaAt(d,e,x3,x)Original native command in the exact edition
  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(x1,d,e,x3)Original native command in the exact edition
  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: PermutationPrefix(x,y,l)FactorListMatching(b,c,d,e,x,y,l)Original native command in the exact edition
  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 : BetaAt(d,e,l,x)Definitions: BetaAt(d,e,l,x)Original native command in the exact edition
  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: 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)Lt(y,S x3)BetaAt(d,e,y,z)BetaAt(B,C,y,z)Original native command in the exact edition
  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 : BetaAt(x4,x5,x3,x)Definitions: BetaAt(x4,x5,x3,x)Original native command in the exact edition
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(x1,x4,x5,x3)Original native command in the exact edition
  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: PermutationPrefix(x,y,l)FactorListMatching(b,c,x4,x5,x,y,l)Original native command in the exact edition
  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 : Lt(x2,l)Definitions: Lt(x2,l)Original native command in the exact edition
  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: BetaAt(d,e,x2,x)BetaAt(d,e,l,x6)BetaAt(x4,x5,x2,x6)BetaAt(x4,x5,l,x)Lt(y,S l)BetaAt(d,e,y,z)BetaAt(x4,x5,y,z)Original native command in the exact edition
  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 defined 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 : Product(b,c,0,n)
  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 : ∃ p. ∃ r. Prime(p) ∧ (BetaAt(b,c,l,p) ∧ (n = r · p ∧ PrimeFactorList(r,b,c,l)))
  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 : ∃ i. Lt(i,m) ∧ BetaAt(d,e,i,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 : PrimeFactorList(n,d,e,S x3)
  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 : Lt(x2,S x3)
  91. 0091rewrite hpredecessor_witness at hmember_witness_left
  92. 0092exact hmember_witness_left
  93. 0093have hposition : x2 = x3 ∨ Lt(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 : BetaAt(d,e,x3,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 : PrimeFactorList(x1,d,e,x3)
  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 ∧ (∃ x. ∃ y. PermutationPrefix(x,y,l) ∧ FactorListMatching(b,c,d,e,x,y,l))
  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 : BetaAt(d,e,l,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 : ∃ 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))))))
  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 : BetaAt(x4,x5,x3,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 : PrimeFactorList(x1,x4,x5,x3)
  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 ∧ (∃ x. ∃ y. PermutationPrefix(x,y,l) ∧ FactorListMatching(b,c,x4,x5,x,y,l))
  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 : Lt(x2,l)
  195. 0195rewrite hrec_left
  196. 0196exact hposition_right
  197. 0197have 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)))))
  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