AF000E

factor_permutation_index_extend

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

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

∀ b. ∀ c. ∀ l. PermutationPrefix(b,c,l) → ∃ x. ∃ y. PermutationPrefix(x,y,S l) ∧ (BetaAt(x,y,l,l) ∧ (∀ z. ∀ n. Lt(z,l) → BetaAt(b,c,z,n) → BetaAt(x,y,z,n)))

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

Definition DAG

PermutationPrefix(b,c,l) · 2Lt(a,b) · 4BetaAt(b,c,i,x) · 7BoundedPrefix(b,c,l) · 1InjectivePrefix(b,c,l) · 2

Actual proof prerequisites

beta_prefix_extend · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisitele_refl · checked external prerequisitele_succ · checked external prerequisitefactor_permutation_prefix_reflectfinite_prefix_injective_extend_fresh · checked external prerequisitefinite_bounded_entry_lt · checked external prerequisitelt_irrefl_expanded · checked external prerequisitefinite_bounded_injective_surjective · checked external prerequisite
Original expanded first-order 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)))))))

Complete tactic proof in conservative notation

All 132 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

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.

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 (1)
factor permutation prefix reflect
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: BetaAt(d,e,l,l)Lt(x,l)BetaAt(b,c,x,y)BetaAt(d,e,x,y)Original native command in the exact edition
  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 : BoundedPrefix(x,x1,S l)Definitions: BoundedPrefix(x,x1,S l)Original native command in the exact edition
  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 ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  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 : ∃ a. BetaAt(b,c,i,a) ∧ Lt(a,l)Definitions: BetaAt(b,c,i,a)Lt(a,l)Original native command in the exact edition
  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(x,x1,l)Original native command in the exact edition
  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(x,x1,S l)Original native command in the exact edition
  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 defined 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 : ∃ d. ∃ e. BetaAt(d,e,l,l) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(d,e,x,y))
  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 : BoundedPrefix(x,x1,S l)
  17. 0017intro i
  18. 0018intro hi
  19. 0019have hcase : i = l ∨ Lt(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 : ∃ a. BetaAt(b,c,i,a) ∧ Lt(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 : InjectivePrefix(x,x1,l)
  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 : InjectivePrefix(x,x1,S l)
  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