AF000E

factor_permutation_index_extend

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

Append the fresh top index to any actual finite permutation, construct the new beta code, and prove all three bijection conditions.

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 b c l. (((forall pfp_i_extend_oldbounded. (exists pfp_gap_extend_oldboundedindex. pfp_gap_extend_oldboundedindex + S (pfp_i_extend_oldbounded) = (l)) -> exists pfp_a_extend_oldbounded. (((exists ff_h_pfp_extend_oldboundedentry. ff_h_pfp_extend_oldboundedentry + S (pfp_a_extend_oldbounded) = S ((S (pfp_i_extend_oldbounded)) * c)) /\ exists ff_q_pfp_extend_oldboundedentry. b = ff_q_pfp_extend_oldboundedentry * S ((S (pfp_i_extend_oldbounded)) * c) + (pfp_a_extend_oldbounded))) /\ (exists pfp_gap_extend_oldboundedvalue. pfp_gap_extend_oldboundedvalue + S (pfp_a_extend_oldbounded) = (l))) /\ (((forall pfp_i_extend_oldinjective pfp_j_extend_oldinjective pfp_a_extend_oldinjective. (exists pfp_gap_extend_oldinjectivefirst. pfp_gap_extend_oldinjectivefirst + S (pfp_i_extend_oldinjective) = (l)) -> (exists pfp_gap_extend_oldinjectivesecond. pfp_gap_extend_oldinjectivesecond + S (pfp_j_extend_oldinjective) = (l)) -> (((exists ff_h_pfp_extend_oldinjectiveleft. ff_h_pfp_extend_oldinjectiveleft + S (pfp_a_extend_oldinjective) = S ((S (pfp_i_extend_oldinjective)) * c)) /\ exists ff_q_pfp_extend_oldinjectiveleft. b = ff_q_pfp_extend_oldinjectiveleft * S ((S (pfp_i_extend_oldinjective)) * c) + (pfp_a_extend_oldinjective))) -> (((exists ff_h_pfp_extend_oldinjectiveright. ff_h_pfp_extend_oldinjectiveright + S (pfp_a_extend_oldinjective) = S ((S (pfp_j_extend_oldinjective)) * c)) /\ exists ff_q_pfp_extend_oldinjectiveright. b = ff_q_pfp_extend_oldinjectiveright * S ((S (pfp_j_extend_oldinjective)) * c) + (pfp_a_extend_oldinjective))) -> pfp_i_extend_oldinjective = pfp_j_extend_oldinjective) /\ (forall pfp_a_extend_oldsurjective. (exists pfp_gap_extend_oldsurjectivevalue. pfp_gap_extend_oldsurjectivevalue + S (pfp_a_extend_oldsurjective) = (l)) -> exists pfp_i_extend_oldsurjective. (exists pfp_gap_extend_oldsurjectiveindex. pfp_gap_extend_oldsurjectiveindex + S (pfp_i_extend_oldsurjective) = (l)) /\ (((exists ff_h_pfp_extend_oldsurjectiveentry. ff_h_pfp_extend_oldsurjectiveentry + S (pfp_a_extend_oldsurjective) = S ((S (pfp_i_extend_oldsurjective)) * c)) /\ exists ff_q_pfp_extend_oldsurjectiveentry. b = ff_q_pfp_extend_oldsurjectiveentry * S ((S (pfp_i_extend_oldsurjective)) * c) + (pfp_a_extend_oldsurjective)))))))) -> exists d e. ((((forall pfp_i_extend_newbounded. (exists pfp_gap_extend_newboundedindex. pfp_gap_extend_newboundedindex + S (pfp_i_extend_newbounded) = (S l)) -> exists pfp_a_extend_newbounded. (((exists ff_h_pfp_extend_newboundedentry. ff_h_pfp_extend_newboundedentry + S (pfp_a_extend_newbounded) = S ((S (pfp_i_extend_newbounded)) * e)) /\ exists ff_q_pfp_extend_newboundedentry. d = ff_q_pfp_extend_newboundedentry * S ((S (pfp_i_extend_newbounded)) * e) + (pfp_a_extend_newbounded))) /\ (exists pfp_gap_extend_newboundedvalue. pfp_gap_extend_newboundedvalue + S (pfp_a_extend_newbounded) = (S l))) /\ (((forall pfp_i_extend_newinjective pfp_j_extend_newinjective pfp_a_extend_newinjective. (exists pfp_gap_extend_newinjectivefirst. pfp_gap_extend_newinjectivefirst + S (pfp_i_extend_newinjective) = (S l)) -> (exists pfp_gap_extend_newinjectivesecond. pfp_gap_extend_newinjectivesecond + S (pfp_j_extend_newinjective) = (S l)) -> (((exists ff_h_pfp_extend_newinjectiveleft. ff_h_pfp_extend_newinjectiveleft + S (pfp_a_extend_newinjective) = S ((S (pfp_i_extend_newinjective)) * e)) /\ exists ff_q_pfp_extend_newinjectiveleft. d = ff_q_pfp_extend_newinjectiveleft * S ((S (pfp_i_extend_newinjective)) * e) + (pfp_a_extend_newinjective))) -> (((exists ff_h_pfp_extend_newinjectiveright. ff_h_pfp_extend_newinjectiveright + S (pfp_a_extend_newinjective) = S ((S (pfp_j_extend_newinjective)) * e)) /\ exists ff_q_pfp_extend_newinjectiveright. d = ff_q_pfp_extend_newinjectiveright * S ((S (pfp_j_extend_newinjective)) * e) + (pfp_a_extend_newinjective))) -> pfp_i_extend_newinjective = pfp_j_extend_newinjective) /\ (forall pfp_a_extend_newsurjective. (exists pfp_gap_extend_newsurjectivevalue. pfp_gap_extend_newsurjectivevalue + S (pfp_a_extend_newsurjective) = (S l)) -> exists pfp_i_extend_newsurjective. (exists pfp_gap_extend_newsurjectiveindex. pfp_gap_extend_newsurjectiveindex + S (pfp_i_extend_newsurjective) = (S l)) /\ (((exists ff_h_pfp_extend_newsurjectiveentry. ff_h_pfp_extend_newsurjectiveentry + S (pfp_a_extend_newsurjective) = S ((S (pfp_i_extend_newsurjective)) * e)) /\ exists ff_q_pfp_extend_newsurjectiveentry. d = ff_q_pfp_extend_newsurjectiveentry * S ((S (pfp_i_extend_newsurjective)) * e) + (pfp_a_extend_newsurjective)))))))) /\ (((((exists ff_h_pfp_extensionlast. ff_h_pfp_extensionlast + S (l) = S ((S (l)) * e)) /\ exists ff_q_pfp_extensionlast. d = ff_q_pfp_extensionlast * S ((S (l)) * e) + (l))) /\ (forall pfp_i_extensionprefix pfp_a_extensionprefix. (exists pfp_gap_extensionprefixbound. pfp_gap_extensionprefixbound + S (pfp_i_extensionprefix) = (l)) -> (((exists ff_h_pfp_extensionprefixold. ff_h_pfp_extensionprefixold + S (pfp_a_extensionprefix) = S ((S (pfp_i_extensionprefix)) * c)) /\ exists ff_q_pfp_extensionprefixold. b = ff_q_pfp_extensionprefixold * S ((S (pfp_i_extensionprefix)) * c) + (pfp_a_extensionprefix))) -> (((exists ff_h_pfp_extensionprefixnew. ff_h_pfp_extensionprefixnew + S (pfp_a_extensionprefix) = S ((S (pfp_i_extensionprefix)) * e)) /\ exists ff_q_pfp_extensionprefixnew. d = ff_q_pfp_extensionprefixnew * S ((S (pfp_i_extensionprefix)) * e) + (pfp_a_extensionprefix)))))))

Constructive proof overview

Generated structural guide

Append the fresh top index to any actual finite permutation, construct the new beta code, and prove all three bijection conditions.

The unchanged tactic script uses 9 declared prerequisites and contains 132 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_prefix_extend Stable theorem; checked-use authorized finite_lt_succ_eq_or_lt Stable theorem; checked-use authorized le_refl Stable theorem; checked-use authorized le_succ Stable theorem; checked-use authorized AF0006 factor_permutation_prefix_reflect finite_prefix_injective_extend_fresh Alpha theorem; checked-use authorized finite_bounded_entry_lt Stable theorem; checked-use authorized lt_irrefl_expanded Stable theorem; checked-use authorized finite_bounded_injective_surjective Stable theorem; checked-use authorized

Direct dependents

AF0010 factor_permutation_matched_append

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

132 script commands · 32 reading checkpoints · 6 local claims

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

Named ingredients (1)
factor permutation prefix reflect

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

01Fix variables and assumptionsL1–4

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro hp
02Separate the logical casesL5–6

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

  1. L5
    cases hp
  2. L6
    cases hp_right
03Establish hextL7–12

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

  1. L7
    have hext : ∃ d. ∃ e. BetaAt(d,e,l,l) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(d,e,x,y))Definitions: LtBetaAt
  2. L8
    specialize beta_prefix_extend (l)
  3. L9
    specialize beta_prefix_extend (b)
  4. L10
    specialize beta_prefix_extend (c)
  5. L11
    specialize beta_prefix_extend (l)
  6. L12
    apply beta_prefix_extend
04Separate the logical casesL13–15

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

  1. L13
    cases hext
  2. L14
    cases hext_witness
  3. L15
    cases hext_witness_witness
05Establish hboundL16–18

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

  1. L16
    have hbound : forall pfp_i_extend_bounded. (exists pfp_gap_extend_boundedindex. pfp_gap_extend_boundedindex + S (pfp_i_extend_bounded) = (S l)) -> exists pfp_a_extend_bounded. (((exists ff_h_pfp_extend_boundedentry. ff_h_pfp_extend_boundedentry + S (pfp_a_extend_bounded) = S ((S (pfp_i_extend_bounded)) * x1)) /\ exists ff_q_pfp_extend_boundedentry. x = ff_q_pfp_extend_boundedentry * S ((S (pfp_i_extend_bounded)) * x1) + (pfp_a_extend_bounded))) /\ (exists pfp_gap_extend_boundedvalue. pfp_gap_extend_boundedvalue + S (pfp_a_extend_bounded) = (S l))
  2. L17
    intro i
  3. L18
    intro hi
06Establish hcaseL19–23

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. L19
    have hcase : i = l \/ (exists pfp_gap_extend_case. pfp_gap_extend_case + S (i) = (l))
  2. L20
    specialize finite_lt_succ_eq_or_lt (l)
  3. L21
    specialize finite_lt_succ_eq_or_lt (i)
  4. L22
    apply finite_lt_succ_eq_or_lt
  5. L23
    exact hi
07Separate the logical casesL24–24

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

  1. L24
    cases hcase
08Construct an explicit witnessL25–25

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

  1. L25
    exists l
09Separate the logical casesL26–26

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

  1. L26
    split
10Calculate and transport equalitiesL27–28

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

  1. L27
    rewrite hcase_left
  2. L28
    rewrite hcase_left
11Use earlier factsL29–31

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

  1. L29
    exact hext_witness_witness_left
  2. L30
    specialize le_refl (S l)
  3. L31
    apply le_refl
12Establish hvalueL32–35

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

  1. L32
    have hvalue : exists a. (((exists ff_h_pfp_extend_old_value. ff_h_pfp_extend_old_value + S (a) = S ((S (i)) * c)) /\ exists ff_q_pfp_extend_old_value. b = ff_q_pfp_extend_old_value * S ((S (i)) * c) + (a))) /\ (exists pfp_gap_extend_old_bound. pfp_gap_extend_old_bound + S (a) = (l))
  2. L33
    specialize hp_left (i)
  3. L34
    apply hp_left
  4. L35
    exact hcase_right
13Separate the logical casesL36–37

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

  1. L36
    cases hvalue
  2. L37
    cases hvalue_witness
14Construct an explicit witnessL38–38

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

  1. L38
    exists x2
15Separate the logical casesL39–39

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

  1. L39
    split
16Use earlier factsL40–48

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

  1. L40
    specialize hext_witness_witness_right (i)
  2. L41
    specialize hext_witness_witness_right (x2)
  3. L42
    apply hext_witness_witness_right
  4. L43
    exact hcase_right
  5. L44
    exact hvalue_witness_left
  6. L45
    specialize le_succ (S x2)
  7. L46
    specialize le_succ (l)
  8. L47
    apply le_succ
  9. L48
    exact hvalue_witness_right
17Establish hinjectiveprefixL49–58

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

  1. L49
    have hinjectiveprefix : InjectivePrefix(x,x1,l)Definitions: InjectivePrefix
  2. L50
    intro i
  3. L51
    intro j
  4. L52
    intro a
  5. L53
    intro hi
  6. L54
    intro hj
  7. L55
    intro hfirst
  8. L56
    intro hsecond
  9. L57
    specialize hp_right_left (i)
  10. L58
    specialize hp_right_left (j)
18Use earlier factsL59–68

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

  1. L59
    specialize hp_right_left (a)
  2. L60
    apply hp_right_left
  3. L61
    exact hi
  4. L62
    exact hj
  5. L63
    specialize factor_permutation_prefix_reflect (b)
  6. L64
    specialize factor_permutation_prefix_reflect (c)
  7. L65
    specialize factor_permutation_prefix_reflect (x)
  8. L66
    specialize factor_permutation_prefix_reflect (x1)
  9. L67
    specialize factor_permutation_prefix_reflect (l)
  10. L68
    specialize factor_permutation_prefix_reflect (i)
19Use earlier factsL69–78

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

  1. L69
    specialize factor_permutation_prefix_reflect (a)
  2. L70
    apply factor_permutation_prefix_reflect
  3. L71
    exact hext_witness_witness_right
  4. L72
    exact hi
  5. L73
    exact hfirst
  6. L74
    specialize factor_permutation_prefix_reflect (b)
  7. L75
    specialize factor_permutation_prefix_reflect (c)
  8. L76
    specialize factor_permutation_prefix_reflect (x)
  9. L77
    specialize factor_permutation_prefix_reflect (x1)
  10. L78
    specialize factor_permutation_prefix_reflect (l)
20Use earlier factsL79–84

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

  1. L79
    specialize factor_permutation_prefix_reflect (j)
  2. L80
    specialize factor_permutation_prefix_reflect (a)
  3. L81
    apply factor_permutation_prefix_reflect
  4. L82
    exact hext_witness_witness_right
  5. L83
    exact hj
  6. L84
    exact hsecond
21Establish hinjectiveL85–93

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite prefix injective extend fresh.

  1. L85
    have hinjective : InjectivePrefix(x,x1,S l)Definitions: InjectivePrefix
  2. L86
    specialize finite_prefix_injective_extend_fresh (x)
  3. L87
    specialize finite_prefix_injective_extend_fresh (x1)
  4. L88
    specialize finite_prefix_injective_extend_fresh (l)
  5. L89
    specialize finite_prefix_injective_extend_fresh (l)
  6. L90
    apply finite_prefix_injective_extend_fresh
  7. L91
    exact hinjectiveprefix
  8. L92
    exact hext_witness_witness_left
  9. L93
    intro hcontains
22Separate the logical casesL94–95

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

  1. L94
    cases hcontains
  2. L95
    cases hcontains_witness
23Use earlier factsL96–105

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

  1. L96
    specialize lt_irrefl_expanded (l)
  2. L97
    apply lt_irrefl_expanded
  3. L98
    specialize finite_bounded_entry_lt (b)
  4. L99
    specialize finite_bounded_entry_lt (c)
  5. L100
    specialize finite_bounded_entry_lt (l)
  6. L101
    specialize finite_bounded_entry_lt (x2)
  7. L102
    specialize finite_bounded_entry_lt (l)
  8. L103
    apply finite_bounded_entry_lt
  9. L104
    exact hp_left
  10. L105
    exact hcontains_witness_left
24Use earlier factsL106–115

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

  1. L106
    specialize factor_permutation_prefix_reflect (b)
  2. L107
    specialize factor_permutation_prefix_reflect (c)
  3. L108
    specialize factor_permutation_prefix_reflect (x)
  4. L109
    specialize factor_permutation_prefix_reflect (x1)
  5. L110
    specialize factor_permutation_prefix_reflect (l)
  6. L111
    specialize factor_permutation_prefix_reflect (x2)
  7. L112
    specialize factor_permutation_prefix_reflect (l)
  8. L113
    apply factor_permutation_prefix_reflect
  9. L114
    exact hext_witness_witness_right
  10. L115
    exact hcontains_witness_left
25Use earlier factsL116–116

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

  1. L116
    exact hcontains_witness_right
26Construct an explicit witnessL117–118

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

  1. L117
    exists x
  2. L118
    exists x1
27Separate the logical casesL119–120

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

  1. L119
    split
  2. L120
    split
28Use earlier factsL121–121

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

  1. L121
    exact hbound
29Separate the logical casesL122–122

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

  1. L122
    split
30Use earlier factsL123–129

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

  1. L123
    exact hinjective
  2. L124
    specialize finite_bounded_injective_surjective (S l)
  3. L125
    specialize finite_bounded_injective_surjective (x)
  4. L126
    specialize finite_bounded_injective_surjective (x1)
  5. L127
    apply finite_bounded_injective_surjective
  6. L128
    exact hbound
  7. L129
    exact hinjective
31Separate the logical casesL130–130

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

  1. L130
    split
32Use earlier factsL131–132

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

  1. L131
    exact hext_witness_witness_left
  2. L132
    exact hext_witness_witness_right

Library-wide reading audit

Original exact command ledger · 132 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro hp
  5. 0005cases hp
  6. 0006cases hp_right
  7. 0007have hext : exists d e. (((((exists ff_h_pfp_chosen_extensionlast. ff_h_pfp_chosen_extensionlast + S (l) = S ((S (l)) * e)) /\ exists ff_q_pfp_chosen_extensionlast. d = ff_q_pfp_chosen_extensionlast * S ((S (l)) * e) + (l))) /\ (forall pfp_i_chosen_extensionprefix pfp_a_chosen_extensionprefix. (exists pfp_gap_chosen_extensionprefixbound. pfp_gap_chosen_extensionprefixbound + S (pfp_i_chosen_extensionprefix) = (l)) -> (((exists ff_h_pfp_chosen_extensionprefixold. ff_h_pfp_chosen_extensionprefixold + S (pfp_a_chosen_extensionprefix) = S ((S (pfp_i_chosen_extensionprefix)) * c)) /\ exists ff_q_pfp_chosen_extensionprefixold. b = ff_q_pfp_chosen_extensionprefixold * S ((S (pfp_i_chosen_extensionprefix)) * c) + (pfp_a_chosen_extensionprefix))) -> (((exists ff_h_pfp_chosen_extensionprefixnew. ff_h_pfp_chosen_extensionprefixnew + S (pfp_a_chosen_extensionprefix) = S ((S (pfp_i_chosen_extensionprefix)) * e)) /\ exists ff_q_pfp_chosen_extensionprefixnew. d = ff_q_pfp_chosen_extensionprefixnew * S ((S (pfp_i_chosen_extensionprefix)) * e) + (pfp_a_chosen_extensionprefix))))))
  8. 0008specialize beta_prefix_extend (l)
  9. 0009specialize beta_prefix_extend (b)
  10. 0010specialize beta_prefix_extend (c)
  11. 0011specialize beta_prefix_extend (l)
  12. 0012apply beta_prefix_extend
  13. 0013cases hext
  14. 0014cases hext_witness
  15. 0015cases hext_witness_witness
  16. 0016have hbound : forall pfp_i_extend_bounded. (exists pfp_gap_extend_boundedindex. pfp_gap_extend_boundedindex + S (pfp_i_extend_bounded) = (S l)) -> exists pfp_a_extend_bounded. (((exists ff_h_pfp_extend_boundedentry. ff_h_pfp_extend_boundedentry + S (pfp_a_extend_bounded) = S ((S (pfp_i_extend_bounded)) * x1)) /\ exists ff_q_pfp_extend_boundedentry. x = ff_q_pfp_extend_boundedentry * S ((S (pfp_i_extend_bounded)) * x1) + (pfp_a_extend_bounded))) /\ (exists pfp_gap_extend_boundedvalue. pfp_gap_extend_boundedvalue + S (pfp_a_extend_bounded) = (S l))
  17. 0017intro i
  18. 0018intro hi
  19. 0019have hcase : i = l \/ (exists pfp_gap_extend_case. pfp_gap_extend_case + S (i) = (l))
  20. 0020specialize finite_lt_succ_eq_or_lt (l)
  21. 0021specialize finite_lt_succ_eq_or_lt (i)
  22. 0022apply finite_lt_succ_eq_or_lt
  23. 0023exact hi
  24. 0024cases hcase
  25. 0025exists l
  26. 0026split
  27. 0027rewrite hcase_left
  28. 0028rewrite hcase_left
  29. 0029exact hext_witness_witness_left
  30. 0030specialize le_refl (S l)
  31. 0031apply le_refl
  32. 0032have hvalue : exists a. (((exists ff_h_pfp_extend_old_value. ff_h_pfp_extend_old_value + S (a) = S ((S (i)) * c)) /\ exists ff_q_pfp_extend_old_value. b = ff_q_pfp_extend_old_value * S ((S (i)) * c) + (a))) /\ (exists pfp_gap_extend_old_bound. pfp_gap_extend_old_bound + S (a) = (l))
  33. 0033specialize hp_left (i)
  34. 0034apply hp_left
  35. 0035exact hcase_right
  36. 0036cases hvalue
  37. 0037cases hvalue_witness
  38. 0038exists x2
  39. 0039split
  40. 0040specialize hext_witness_witness_right (i)
  41. 0041specialize hext_witness_witness_right (x2)
  42. 0042apply hext_witness_witness_right
  43. 0043exact hcase_right
  44. 0044exact hvalue_witness_left
  45. 0045specialize le_succ (S x2)
  46. 0046specialize le_succ (l)
  47. 0047apply le_succ
  48. 0048exact hvalue_witness_right
  49. 0049have hinjectiveprefix : forall pfp_i_extend_injective_prefix pfp_j_extend_injective_prefix pfp_a_extend_injective_prefix. (exists pfp_gap_extend_injective_prefixfirst. pfp_gap_extend_injective_prefixfirst + S (pfp_i_extend_injective_prefix) = (l)) -> (exists pfp_gap_extend_injective_prefixsecond. pfp_gap_extend_injective_prefixsecond + S (pfp_j_extend_injective_prefix) = (l)) -> (((exists ff_h_pfp_extend_injective_prefixleft. ff_h_pfp_extend_injective_prefixleft + S (pfp_a_extend_injective_prefix) = S ((S (pfp_i_extend_injective_prefix)) * x1)) /\ exists ff_q_pfp_extend_injective_prefixleft. x = ff_q_pfp_extend_injective_prefixleft * S ((S (pfp_i_extend_injective_prefix)) * x1) + (pfp_a_extend_injective_prefix))) -> (((exists ff_h_pfp_extend_injective_prefixright. ff_h_pfp_extend_injective_prefixright + S (pfp_a_extend_injective_prefix) = S ((S (pfp_j_extend_injective_prefix)) * x1)) /\ exists ff_q_pfp_extend_injective_prefixright. x = ff_q_pfp_extend_injective_prefixright * S ((S (pfp_j_extend_injective_prefix)) * x1) + (pfp_a_extend_injective_prefix))) -> pfp_i_extend_injective_prefix = pfp_j_extend_injective_prefix
  50. 0050intro i
  51. 0051intro j
  52. 0052intro a
  53. 0053intro hi
  54. 0054intro hj
  55. 0055intro hfirst
  56. 0056intro hsecond
  57. 0057specialize hp_right_left (i)
  58. 0058specialize hp_right_left (j)
  59. 0059specialize hp_right_left (a)
  60. 0060apply hp_right_left
  61. 0061exact hi
  62. 0062exact hj
  63. 0063specialize factor_permutation_prefix_reflect (b)
  64. 0064specialize factor_permutation_prefix_reflect (c)
  65. 0065specialize factor_permutation_prefix_reflect (x)
  66. 0066specialize factor_permutation_prefix_reflect (x1)
  67. 0067specialize factor_permutation_prefix_reflect (l)
  68. 0068specialize factor_permutation_prefix_reflect (i)
  69. 0069specialize factor_permutation_prefix_reflect (a)
  70. 0070apply factor_permutation_prefix_reflect
  71. 0071exact hext_witness_witness_right
  72. 0072exact hi
  73. 0073exact hfirst
  74. 0074specialize factor_permutation_prefix_reflect (b)
  75. 0075specialize factor_permutation_prefix_reflect (c)
  76. 0076specialize factor_permutation_prefix_reflect (x)
  77. 0077specialize factor_permutation_prefix_reflect (x1)
  78. 0078specialize factor_permutation_prefix_reflect (l)
  79. 0079specialize factor_permutation_prefix_reflect (j)
  80. 0080specialize factor_permutation_prefix_reflect (a)
  81. 0081apply factor_permutation_prefix_reflect
  82. 0082exact hext_witness_witness_right
  83. 0083exact hj
  84. 0084exact hsecond
  85. 0085have hinjective : forall pfp_i_extend_injective pfp_j_extend_injective pfp_a_extend_injective. (exists pfp_gap_extend_injectivefirst. pfp_gap_extend_injectivefirst + S (pfp_i_extend_injective) = (S l)) -> (exists pfp_gap_extend_injectivesecond. pfp_gap_extend_injectivesecond + S (pfp_j_extend_injective) = (S l)) -> (((exists ff_h_pfp_extend_injectiveleft. ff_h_pfp_extend_injectiveleft + S (pfp_a_extend_injective) = S ((S (pfp_i_extend_injective)) * x1)) /\ exists ff_q_pfp_extend_injectiveleft. x = ff_q_pfp_extend_injectiveleft * S ((S (pfp_i_extend_injective)) * x1) + (pfp_a_extend_injective))) -> (((exists ff_h_pfp_extend_injectiveright. ff_h_pfp_extend_injectiveright + S (pfp_a_extend_injective) = S ((S (pfp_j_extend_injective)) * x1)) /\ exists ff_q_pfp_extend_injectiveright. x = ff_q_pfp_extend_injectiveright * S ((S (pfp_j_extend_injective)) * x1) + (pfp_a_extend_injective))) -> pfp_i_extend_injective = pfp_j_extend_injective
  86. 0086specialize finite_prefix_injective_extend_fresh (x)
  87. 0087specialize finite_prefix_injective_extend_fresh (x1)
  88. 0088specialize finite_prefix_injective_extend_fresh (l)
  89. 0089specialize finite_prefix_injective_extend_fresh (l)
  90. 0090apply finite_prefix_injective_extend_fresh
  91. 0091exact hinjectiveprefix
  92. 0092exact hext_witness_witness_left
  93. 0093intro hcontains
  94. 0094cases hcontains
  95. 0095cases hcontains_witness
  96. 0096specialize lt_irrefl_expanded (l)
  97. 0097apply lt_irrefl_expanded
  98. 0098specialize finite_bounded_entry_lt (b)
  99. 0099specialize finite_bounded_entry_lt (c)
  100. 0100specialize finite_bounded_entry_lt (l)
  101. 0101specialize finite_bounded_entry_lt (x2)
  102. 0102specialize finite_bounded_entry_lt (l)
  103. 0103apply finite_bounded_entry_lt
  104. 0104exact hp_left
  105. 0105exact hcontains_witness_left
  106. 0106specialize factor_permutation_prefix_reflect (b)
  107. 0107specialize factor_permutation_prefix_reflect (c)
  108. 0108specialize factor_permutation_prefix_reflect (x)
  109. 0109specialize factor_permutation_prefix_reflect (x1)
  110. 0110specialize factor_permutation_prefix_reflect (l)
  111. 0111specialize factor_permutation_prefix_reflect (x2)
  112. 0112specialize factor_permutation_prefix_reflect (l)
  113. 0113apply factor_permutation_prefix_reflect
  114. 0114exact hext_witness_witness_right
  115. 0115exact hcontains_witness_left
  116. 0116exact hcontains_witness_right
  117. 0117exists x
  118. 0118exists x1
  119. 0119split
  120. 0120split
  121. 0121exact hbound
  122. 0122split
  123. 0123exact hinjective
  124. 0124specialize finite_bounded_injective_surjective (S l)
  125. 0125specialize finite_bounded_injective_surjective (x)
  126. 0126specialize finite_bounded_injective_surjective (x1)
  127. 0127apply finite_bounded_injective_surjective
  128. 0128exact hbound
  129. 0129exact hinjective
  130. 0130split
  131. 0131exact hext_witness_witness_left
  132. 0132exact hext_witness_witness_right