PA004W

finite_bounded_injective_surjective

Stable checked-use theorem · independently closed

Every bounded injective beta-coded prefix is surjective onto its finite interval.

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 PA statement

forall n b c. (forall fp_i_pigeon_bounded. (exists fp_gap_pigeon_bounded_index. fp_gap_pigeon_bounded_index + S fp_i_pigeon_bounded = n) -> exists fp_value_pigeon_bounded. ((((exists ff_h_pigeon_bounded_entry. ff_h_pigeon_bounded_entry + S (fp_value_pigeon_bounded) = S ((S (fp_i_pigeon_bounded)) * c)) /\ exists ff_q_pigeon_bounded_entry. b = ff_q_pigeon_bounded_entry * S ((S (fp_i_pigeon_bounded)) * c) + (fp_value_pigeon_bounded))) /\ (exists fp_gap_pigeon_bounded_value. fp_gap_pigeon_bounded_value + S fp_value_pigeon_bounded = n))) -> (forall fp_i_pigeon_injective fp_j_pigeon_injective fp_value_pigeon_injective. (exists fp_gap_pigeon_injective_i. fp_gap_pigeon_injective_i + S fp_i_pigeon_injective = n) -> (exists fp_gap_pigeon_injective_j. fp_gap_pigeon_injective_j + S fp_j_pigeon_injective = n) -> (((exists ff_h_pigeon_injective_left. ff_h_pigeon_injective_left + S (fp_value_pigeon_injective) = S ((S (fp_i_pigeon_injective)) * c)) /\ exists ff_q_pigeon_injective_left. b = ff_q_pigeon_injective_left * S ((S (fp_i_pigeon_injective)) * c) + (fp_value_pigeon_injective))) -> (((exists ff_h_pigeon_injective_right. ff_h_pigeon_injective_right + S (fp_value_pigeon_injective) = S ((S (fp_j_pigeon_injective)) * c)) /\ exists ff_q_pigeon_injective_right. b = ff_q_pigeon_injective_right * S ((S (fp_j_pigeon_injective)) * c) + (fp_value_pigeon_injective))) -> fp_i_pigeon_injective = fp_j_pigeon_injective) -> (forall fp_value_pigeon_surjective. (exists fp_gap_pigeon_surjective_value. fp_gap_pigeon_surjective_value + S fp_value_pigeon_surjective = n) -> exists fp_i_pigeon_surjective. ((exists fp_gap_pigeon_surjective_index. fp_gap_pigeon_surjective_index + S fp_i_pigeon_surjective = n) /\ (((exists ff_h_pigeon_surjective_entry. ff_h_pigeon_surjective_entry + S (fp_value_pigeon_surjective) = S ((S (fp_i_pigeon_surjective)) * c)) /\ exists ff_q_pigeon_surjective_entry. b = ff_q_pigeon_surjective_entry * S ((S (fp_i_pigeon_surjective)) * c) + (fp_value_pigeon_surjective)))))

Structural proof guide

Generated structural guide

Every bounded injective beta-coded prefix is surjective onto its finite interval.

Use the direct prerequisites finite_surjective_zero, finite_contains_decidable, finite_bounded_last_succ, beta_prefix_swap_last_from_entries, finite_swap_last_bounded, finite_swap_last_injective, finite_bounded_prefix_without_top, finite_injective_prefix_succ, finite_surjective_succ_from_prefix, finite_swap_last_surjective_back, finite_no_top_successor_gate, beta_at_unique, le_succ, le_refl, lt_irrefl_expanded as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (9), intermediate claims (13), equality transport (1).

Referenced ingredients

PA004F finite_surjective_zero PA004H finite_contains_decidable PA004I finite_bounded_last_succ PA004K beta_prefix_swap_last_from_entries PA004M finite_swap_last_bounded PA004O finite_swap_last_injective PA004P finite_bounded_prefix_without_top PA004Q finite_injective_prefix_succ PA004T finite_surjective_succ_from_prefix PA004U finite_swap_last_surjective_back PA004V finite_no_top_successor_gate PA002F beta_at_unique PA002O le_succ PA001A le_refl PA0010 lt_irrefl_expanded

Proof neighborhood

Direct dependencies

PA004F finite_surjective_zero PA004H finite_contains_decidable PA004I finite_bounded_last_succ PA004K beta_prefix_swap_last_from_entries PA004M finite_swap_last_bounded PA004O finite_swap_last_injective PA004P finite_bounded_prefix_without_top PA004Q finite_injective_prefix_succ PA004T finite_surjective_succ_from_prefix PA004U finite_swap_last_surjective_back PA004V finite_no_top_successor_gate PA002F beta_at_unique PA002O le_succ PA001A le_refl PA0010 lt_irrefl_expanded

Direct dependents

PA007X beta_product_permutation_invariant PA0097 finite_short_cover_impossible PA00B3 beta_magnitude_predecessor_recode_surjective PA00CX beta_sum_permutation_invariant

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

Read the argument

Proof checkpoints

178 script commands · 36 reading checkpoints · 13 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 (14)
finite surjective zerofinite contains decidablefinite bounded last succbeta prefix swap last from entriesfinite swap last boundedfinite swap last injectivefinite bounded prefix without topfinite injective prefix succfinite surjective succ from prefixfinite swap last surjective backfinite no top successor gatele succle refllt irrefl expanded

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

01Induction on nL1–10

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

  1. L1
    induction n
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro hbounded
  5. L5
    intro hinjective
  6. L6
    specialize finite_surjective_zero b
  7. L7
    specialize finite_surjective_zero c
  8. L8
    specialize finite_surjective_zero 0
  9. L9
    apply finite_surjective_zero
  10. L10
    refl
02Fix variables and assumptionsL11–14

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

  1. L11
    intro b
  2. L12
    intro c
  3. L13
    intro hbounded
  4. L14
    intro hinjective
03Establish hcontainsL15–20

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

  1. L15
    have hcontains : ContainsPrefix(b,c,n,n) ∨ ¬ContainsPrefix(b,c,n,n)Definitions: ContainsPrefix
  2. L16
    specialize finite_contains_decidable b
  3. L17
    specialize finite_contains_decidable c
  4. L18
    specialize finite_contains_decidable n
  5. L19
    specialize finite_contains_decidable n
  6. L20
    exact finite_contains_decidable
04Separate the logical casesL21–23

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

  1. L21
    cases hcontains
  2. L22
    cases hcontains_left
  3. L23
    cases hcontains_left_witness
05Establish hlastL24–31

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

  1. L24
    have hlast : exists y. (((exists h. h + S y = S ((S n) * c)) /\ exists q. b = q * S ((S n) * c) + y) /\ exists h. h + S y = S n)
  2. L25
    specialize finite_bounded_last_succ b
  3. L26
    specialize finite_bounded_last_succ c
  4. L27
    specialize finite_bounded_last_succ n
  5. L28
    specialize finite_bounded_last_succ (S n)
  6. L29
    apply finite_bounded_last_succ
  7. L30
    refl
  8. L31
    exact hbounded
06Separate the logical casesL32–33

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

  1. L32
    cases hlast
  2. L33
    cases hlast_witness
07Establish hswapL34–43

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

  1. L34
    have hswap : ∃ z. ∃ d. BetaAt(z,d,x,x1) ∧ (BetaAt(z,d,n,n) ∧ (∀ y. ∀ m. Lt(y,S n) → ¬y = x → ¬y = n → BetaAt(b,c,y,m) → BetaAt(z,d,y,m)))Definitions: LtBetaAt
  2. L35
    specialize beta_prefix_swap_last_from_entries b
  3. L36
    specialize beta_prefix_swap_last_from_entries c
  4. L37
    specialize beta_prefix_swap_last_from_entries n
  5. L38
    specialize beta_prefix_swap_last_from_entries x
  6. L39
    specialize beta_prefix_swap_last_from_entries n
  7. L40
    specialize beta_prefix_swap_last_from_entries x1
  8. L41
    apply beta_prefix_swap_last_from_entries
  9. L42
    exact hcontains_left_witness_left
  10. L43
    exact hcontains_left_witness_right
08Use earlier factsL44–44

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

  1. L44
    exact hlast_witness_left
09Separate the logical casesL45–48

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

  1. L45
    cases hswap
  2. L46
    cases hswap_witness
  3. L47
    cases hswap_witness_witness
  4. L48
    cases hswap_witness_witness_right
10Establish hswap_boundedL49–58

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

  1. L49
    have hswap_bounded : BoundedPrefix(x2,x3,S n)Definitions: BoundedPrefix
  2. L50
    specialize finite_swap_last_bounded b
  3. L51
    specialize finite_swap_last_bounded c
  4. L52
    specialize finite_swap_last_bounded x2
  5. L53
    specialize finite_swap_last_bounded x3
  6. L54
    specialize finite_swap_last_bounded n
  7. L55
    specialize finite_swap_last_bounded (S n)
  8. L56
    specialize finite_swap_last_bounded x
  9. L57
    specialize finite_swap_last_bounded n
  10. L58
    specialize finite_swap_last_bounded x1
11Use earlier factsL59–59

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

  1. L59
    apply finite_swap_last_bounded
12Calculate and transport equalitiesL60–60

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

  1. L60
    refl
13Use earlier factsL61–67

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

  1. L61
    exact hcontains_left_witness_left
  2. L62
    exact hbounded
  3. L63
    exact hcontains_left_witness_right
  4. L64
    exact hlast_witness_left
  5. L65
    exact hswap_witness_witness_left
  6. L66
    exact hswap_witness_witness_right_left
  7. L67
    exact hswap_witness_witness_right_right
14Establish hswap_injectiveL68–77

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

  1. L68
    have hswap_injective : InjectivePrefix(x2,x3,S n)Definitions: InjectivePrefix
  2. L69
    specialize finite_swap_last_injective b
  3. L70
    specialize finite_swap_last_injective c
  4. L71
    specialize finite_swap_last_injective x2
  5. L72
    specialize finite_swap_last_injective x3
  6. L73
    specialize finite_swap_last_injective n
  7. L74
    specialize finite_swap_last_injective (S n)
  8. L75
    specialize finite_swap_last_injective x
  9. L76
    specialize finite_swap_last_injective n
  10. L77
    specialize finite_swap_last_injective x1
15Use earlier factsL78–78

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

  1. L78
    apply finite_swap_last_injective
16Calculate and transport equalitiesL79–79

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

  1. L79
    refl
17Use earlier factsL80–86

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

  1. L80
    exact hcontains_left_witness_left
  2. L81
    exact hinjective
  3. L82
    exact hcontains_left_witness_right
  4. L83
    exact hlast_witness_left
  5. L84
    exact hswap_witness_witness_left
  6. L85
    exact hswap_witness_witness_right_left
  7. L86
    exact hswap_witness_witness_right_right
18Establish hnotopL87–90

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

  1. L87
    have hnotop : forall j. (exists h. h + S j = n) -> ~(((exists ff_h_pigeon_top_j. ff_h_pigeon_top_j + S (n) = S ((S (j)) * x3)) /\ exists ff_q_pigeon_top_j. x2 = ff_q_pigeon_top_j * S ((S (j)) * x3) + (n)))
  2. L88
    intro j
  3. L89
    intro hj
  4. L90
    intro htop
19Establish hjsnL91–95

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

  1. L91
    have hjsn : exists h. h + S j = S n
  2. L92
    specialize le_succ (S j)
  3. L93
    specialize le_succ n
  4. L94
    apply le_succ
  5. L95
    exact hj
20Establish hnsnL96–98

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

  1. L96
    have hnsn : exists h. h + S n = S n
  2. L97
    specialize le_refl (S n)
  3. L98
    exact le_refl
21Establish hjneqL99–108

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

  1. L99
    have hjneq : j = n
  2. L100
    specialize hswap_injective j
  3. L101
    specialize hswap_injective n
  4. L102
    specialize hswap_injective n
  5. L103
    apply hswap_injective
  6. L104
    exact hjsn
  7. L105
    exact hnsn
  8. L106
    exact htop
  9. L107
    exact hswap_witness_witness_right_left
  10. L108
    specialize lt_irrefl_expanded n
22Use earlier factsL109–109

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

  1. L109
    apply lt_irrefl_expanded
23Calculate and transport equalitiesL110–110

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

  1. L110
    rewrite hjneq at hj
24Use earlier factsL111–111

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

  1. L111
    exact hj
25Establish hprefix_boundedL112–120

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite bounded prefix without top.

  1. L112
    have hprefix_bounded : BoundedPrefix(x2,x3,n)Definitions: BoundedPrefix
  2. L113
    specialize finite_bounded_prefix_without_top x2
  3. L114
    specialize finite_bounded_prefix_without_top x3
  4. L115
    specialize finite_bounded_prefix_without_top n
  5. L116
    specialize finite_bounded_prefix_without_top (S n)
  6. L117
    apply finite_bounded_prefix_without_top
  7. L118
    refl
  8. L119
    exact hswap_bounded
  9. L120
    exact hnotop
26Establish hprefix_injectiveL121–128

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

  1. L121
    have hprefix_injective : InjectivePrefix(x2,x3,n)Definitions: InjectivePrefix
  2. L122
    specialize finite_injective_prefix_succ x2
  3. L123
    specialize finite_injective_prefix_succ x3
  4. L124
    specialize finite_injective_prefix_succ n
  5. L125
    specialize finite_injective_prefix_succ (S n)
  6. L126
    apply finite_injective_prefix_succ
  7. L127
    refl
  8. L128
    exact hswap_injective
27Establish hprefix_surjectiveL129–134

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

  1. L129
    have hprefix_surjective : SurjectivePrefix(x2,x3,n)Definitions: SurjectivePrefix
  2. L130
    specialize IH x2
  3. L131
    specialize IH x3
  4. L132
    apply IH
  5. L133
    exact hprefix_bounded
  6. L134
    exact hprefix_injective
28Establish hswap_surjectiveL135–144

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

  1. L135
    have hswap_surjective : SurjectivePrefix(x2,x3,S n)Definitions: SurjectivePrefix
  2. L136
    specialize finite_surjective_succ_from_prefix x2
  3. L137
    specialize finite_surjective_succ_from_prefix x3
  4. L138
    specialize finite_surjective_succ_from_prefix n
  5. L139
    specialize finite_surjective_succ_from_prefix (S n)
  6. L140
    apply finite_surjective_succ_from_prefix
  7. L141
    refl
  8. L142
    exact hswap_bounded
  9. L143
    exact hswap_injective
  10. L144
    exact hprefix_surjective
29Use earlier factsL145–154

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

  1. L145
    specialize finite_swap_last_surjective_back b
  2. L146
    specialize finite_swap_last_surjective_back c
  3. L147
    specialize finite_swap_last_surjective_back x2
  4. L148
    specialize finite_swap_last_surjective_back x3
  5. L149
    specialize finite_swap_last_surjective_back n
  6. L150
    specialize finite_swap_last_surjective_back (S n)
  7. L151
    specialize finite_swap_last_surjective_back x
  8. L152
    specialize finite_swap_last_surjective_back n
  9. L153
    specialize finite_swap_last_surjective_back x1
  10. L154
    apply finite_swap_last_surjective_back
30Calculate and transport equalitiesL155–155

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

  1. L155
    refl
31Use earlier factsL156–165

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

  1. L156
    exact hcontains_left_witness_left
  2. L157
    exact hcontains_left_witness_right
  3. L158
    exact hlast_witness_left
  4. L159
    exact hswap_witness_witness_left
  5. L160
    exact hswap_witness_witness_right_left
  6. L161
    exact hswap_witness_witness_right_right
  7. L162
    exact hswap_surjective
  8. L163
    specialize finite_no_top_successor_gate b
  9. L164
    specialize finite_no_top_successor_gate c
  10. L165
    specialize finite_no_top_successor_gate n
32Use earlier factsL166–167

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

  1. L166
    specialize finite_no_top_successor_gate (S n)
  2. L167
    apply finite_no_top_successor_gate
33Calculate and transport equalitiesL168–168

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

  1. L168
    refl
34Use earlier factsL169–171

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

  1. L169
    exact hbounded
  2. L170
    exact hinjective
  3. L171
    exact hcontains_right
35Fix variables and assumptionsL172–173

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

  1. L172
    intro hprefix_bounded
  2. L173
    intro hprefix_injective
36Use earlier factsL174–178

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

  1. L174
    specialize IH b
  2. L175
    specialize IH c
  3. L176
    apply IH
  4. L177
    exact hprefix_bounded
  5. L178
    exact hprefix_injective

Library-wide reading audit

Original exact command ledger · 178 lines
  1. 0001induction n
  2. 0002intro b
  3. 0003intro c
  4. 0004intro hbounded
  5. 0005intro hinjective
  6. 0006specialize finite_surjective_zero b
  7. 0007specialize finite_surjective_zero c
  8. 0008specialize finite_surjective_zero 0
  9. 0009apply finite_surjective_zero
  10. 0010refl
  11. 0011intro b
  12. 0012intro c
  13. 0013intro hbounded
  14. 0014intro hinjective
  15. 0015have hcontains : (exists fp_i_contains_top. ((exists fp_gap_contains_top_index. fp_gap_contains_top_index + S fp_i_contains_top = n) /\ (((exists ff_h_contains_top_entry. ff_h_contains_top_entry + S (n) = S ((S (fp_i_contains_top)) * c)) /\ exists ff_q_contains_top_entry. b = ff_q_contains_top_entry * S ((S (fp_i_contains_top)) * c) + (n))))) \/ ~(exists fp_i_contains_top. ((exists fp_gap_contains_top_index. fp_gap_contains_top_index + S fp_i_contains_top = n) /\ (((exists ff_h_contains_top_entry. ff_h_contains_top_entry + S (n) = S ((S (fp_i_contains_top)) * c)) /\ exists ff_q_contains_top_entry. b = ff_q_contains_top_entry * S ((S (fp_i_contains_top)) * c) + (n)))))
  16. 0016specialize finite_contains_decidable b
  17. 0017specialize finite_contains_decidable c
  18. 0018specialize finite_contains_decidable n
  19. 0019specialize finite_contains_decidable n
  20. 0020exact finite_contains_decidable
  21. 0021cases hcontains
  22. 0022cases hcontains_left
  23. 0023cases hcontains_left_witness
  24. 0024have hlast : exists y. (((exists h. h + S y = S ((S n) * c)) /\ exists q. b = q * S ((S n) * c) + y) /\ exists h. h + S y = S n)
  25. 0025specialize finite_bounded_last_succ b
  26. 0026specialize finite_bounded_last_succ c
  27. 0027specialize finite_bounded_last_succ n
  28. 0028specialize finite_bounded_last_succ (S n)
  29. 0029apply finite_bounded_last_succ
  30. 0030refl
  31. 0031exact hbounded
  32. 0032cases hlast
  33. 0033cases hlast_witness
  34. 0034have hswap : exists z d. ((((exists ff_h_pigeon_swap_new_i. ff_h_pigeon_swap_new_i + S (x1) = S ((S (x)) * d)) /\ exists ff_q_pigeon_swap_new_i. z = ff_q_pigeon_swap_new_i * S ((S (x)) * d) + (x1))) /\ ((((exists ff_h_pigeon_swap_new_n. ff_h_pigeon_swap_new_n + S (n) = S ((S (n)) * d)) /\ exists ff_q_pigeon_swap_new_n. z = ff_q_pigeon_swap_new_n * S ((S (n)) * d) + (n))) /\ forall j a. (exists h. h + S j = S n) -> ~(j = x) -> ~(j = n) -> (((exists ff_h_pigeon_swap_old_other. ff_h_pigeon_swap_old_other + S (a) = S ((S (j)) * c)) /\ exists ff_q_pigeon_swap_old_other. b = ff_q_pigeon_swap_old_other * S ((S (j)) * c) + (a))) -> (((exists ff_h_pigeon_swap_new_other. ff_h_pigeon_swap_new_other + S (a) = S ((S (j)) * d)) /\ exists ff_q_pigeon_swap_new_other. z = ff_q_pigeon_swap_new_other * S ((S (j)) * d) + (a)))))
  35. 0035specialize beta_prefix_swap_last_from_entries b
  36. 0036specialize beta_prefix_swap_last_from_entries c
  37. 0037specialize beta_prefix_swap_last_from_entries n
  38. 0038specialize beta_prefix_swap_last_from_entries x
  39. 0039specialize beta_prefix_swap_last_from_entries n
  40. 0040specialize beta_prefix_swap_last_from_entries x1
  41. 0041apply beta_prefix_swap_last_from_entries
  42. 0042exact hcontains_left_witness_left
  43. 0043exact hcontains_left_witness_right
  44. 0044exact hlast_witness_left
  45. 0045cases hswap
  46. 0046cases hswap_witness
  47. 0047cases hswap_witness_witness
  48. 0048cases hswap_witness_witness_right
  49. 0049have hswap_bounded : forall fp_i_pigeon_swapped_bounded. (exists fp_gap_pigeon_swapped_bounded_index. fp_gap_pigeon_swapped_bounded_index + S fp_i_pigeon_swapped_bounded = S n) -> exists fp_value_pigeon_swapped_bounded. ((((exists ff_h_pigeon_swapped_bounded_entry. ff_h_pigeon_swapped_bounded_entry + S (fp_value_pigeon_swapped_bounded) = S ((S (fp_i_pigeon_swapped_bounded)) * x3)) /\ exists ff_q_pigeon_swapped_bounded_entry. x2 = ff_q_pigeon_swapped_bounded_entry * S ((S (fp_i_pigeon_swapped_bounded)) * x3) + (fp_value_pigeon_swapped_bounded))) /\ (exists fp_gap_pigeon_swapped_bounded_value. fp_gap_pigeon_swapped_bounded_value + S fp_value_pigeon_swapped_bounded = S n))
  50. 0050specialize finite_swap_last_bounded b
  51. 0051specialize finite_swap_last_bounded c
  52. 0052specialize finite_swap_last_bounded x2
  53. 0053specialize finite_swap_last_bounded x3
  54. 0054specialize finite_swap_last_bounded n
  55. 0055specialize finite_swap_last_bounded (S n)
  56. 0056specialize finite_swap_last_bounded x
  57. 0057specialize finite_swap_last_bounded n
  58. 0058specialize finite_swap_last_bounded x1
  59. 0059apply finite_swap_last_bounded
  60. 0060refl
  61. 0061exact hcontains_left_witness_left
  62. 0062exact hbounded
  63. 0063exact hcontains_left_witness_right
  64. 0064exact hlast_witness_left
  65. 0065exact hswap_witness_witness_left
  66. 0066exact hswap_witness_witness_right_left
  67. 0067exact hswap_witness_witness_right_right
  68. 0068have hswap_injective : forall fp_i_pigeon_swapped_injective fp_j_pigeon_swapped_injective fp_value_pigeon_swapped_injective. (exists fp_gap_pigeon_swapped_injective_i. fp_gap_pigeon_swapped_injective_i + S fp_i_pigeon_swapped_injective = S n) -> (exists fp_gap_pigeon_swapped_injective_j. fp_gap_pigeon_swapped_injective_j + S fp_j_pigeon_swapped_injective = S n) -> (((exists ff_h_pigeon_swapped_injective_left. ff_h_pigeon_swapped_injective_left + S (fp_value_pigeon_swapped_injective) = S ((S (fp_i_pigeon_swapped_injective)) * x3)) /\ exists ff_q_pigeon_swapped_injective_left. x2 = ff_q_pigeon_swapped_injective_left * S ((S (fp_i_pigeon_swapped_injective)) * x3) + (fp_value_pigeon_swapped_injective))) -> (((exists ff_h_pigeon_swapped_injective_right. ff_h_pigeon_swapped_injective_right + S (fp_value_pigeon_swapped_injective) = S ((S (fp_j_pigeon_swapped_injective)) * x3)) /\ exists ff_q_pigeon_swapped_injective_right. x2 = ff_q_pigeon_swapped_injective_right * S ((S (fp_j_pigeon_swapped_injective)) * x3) + (fp_value_pigeon_swapped_injective))) -> fp_i_pigeon_swapped_injective = fp_j_pigeon_swapped_injective
  69. 0069specialize finite_swap_last_injective b
  70. 0070specialize finite_swap_last_injective c
  71. 0071specialize finite_swap_last_injective x2
  72. 0072specialize finite_swap_last_injective x3
  73. 0073specialize finite_swap_last_injective n
  74. 0074specialize finite_swap_last_injective (S n)
  75. 0075specialize finite_swap_last_injective x
  76. 0076specialize finite_swap_last_injective n
  77. 0077specialize finite_swap_last_injective x1
  78. 0078apply finite_swap_last_injective
  79. 0079refl
  80. 0080exact hcontains_left_witness_left
  81. 0081exact hinjective
  82. 0082exact hcontains_left_witness_right
  83. 0083exact hlast_witness_left
  84. 0084exact hswap_witness_witness_left
  85. 0085exact hswap_witness_witness_right_left
  86. 0086exact hswap_witness_witness_right_right
  87. 0087have hnotop : forall j. (exists h. h + S j = n) -> ~(((exists ff_h_pigeon_top_j. ff_h_pigeon_top_j + S (n) = S ((S (j)) * x3)) /\ exists ff_q_pigeon_top_j. x2 = ff_q_pigeon_top_j * S ((S (j)) * x3) + (n)))
  88. 0088intro j
  89. 0089intro hj
  90. 0090intro htop
  91. 0091have hjsn : exists h. h + S j = S n
  92. 0092specialize le_succ (S j)
  93. 0093specialize le_succ n
  94. 0094apply le_succ
  95. 0095exact hj
  96. 0096have hnsn : exists h. h + S n = S n
  97. 0097specialize le_refl (S n)
  98. 0098exact le_refl
  99. 0099have hjneq : j = n
  100. 0100specialize hswap_injective j
  101. 0101specialize hswap_injective n
  102. 0102specialize hswap_injective n
  103. 0103apply hswap_injective
  104. 0104exact hjsn
  105. 0105exact hnsn
  106. 0106exact htop
  107. 0107exact hswap_witness_witness_right_left
  108. 0108specialize lt_irrefl_expanded n
  109. 0109apply lt_irrefl_expanded
  110. 0110rewrite hjneq at hj
  111. 0111exact hj
  112. 0112have hprefix_bounded : forall fp_i_pigeon_swapped_prefix_bounded. (exists fp_gap_pigeon_swapped_prefix_bounded_index. fp_gap_pigeon_swapped_prefix_bounded_index + S fp_i_pigeon_swapped_prefix_bounded = n) -> exists fp_value_pigeon_swapped_prefix_bounded. ((((exists ff_h_pigeon_swapped_prefix_bounded_entry. ff_h_pigeon_swapped_prefix_bounded_entry + S (fp_value_pigeon_swapped_prefix_bounded) = S ((S (fp_i_pigeon_swapped_prefix_bounded)) * x3)) /\ exists ff_q_pigeon_swapped_prefix_bounded_entry. x2 = ff_q_pigeon_swapped_prefix_bounded_entry * S ((S (fp_i_pigeon_swapped_prefix_bounded)) * x3) + (fp_value_pigeon_swapped_prefix_bounded))) /\ (exists fp_gap_pigeon_swapped_prefix_bounded_value. fp_gap_pigeon_swapped_prefix_bounded_value + S fp_value_pigeon_swapped_prefix_bounded = n))
  113. 0113specialize finite_bounded_prefix_without_top x2
  114. 0114specialize finite_bounded_prefix_without_top x3
  115. 0115specialize finite_bounded_prefix_without_top n
  116. 0116specialize finite_bounded_prefix_without_top (S n)
  117. 0117apply finite_bounded_prefix_without_top
  118. 0118refl
  119. 0119exact hswap_bounded
  120. 0120exact hnotop
  121. 0121have hprefix_injective : forall fp_i_pigeon_swapped_prefix_injective fp_j_pigeon_swapped_prefix_injective fp_value_pigeon_swapped_prefix_injective. (exists fp_gap_pigeon_swapped_prefix_injective_i. fp_gap_pigeon_swapped_prefix_injective_i + S fp_i_pigeon_swapped_prefix_injective = n) -> (exists fp_gap_pigeon_swapped_prefix_injective_j. fp_gap_pigeon_swapped_prefix_injective_j + S fp_j_pigeon_swapped_prefix_injective = n) -> (((exists ff_h_pigeon_swapped_prefix_injective_left. ff_h_pigeon_swapped_prefix_injective_left + S (fp_value_pigeon_swapped_prefix_injective) = S ((S (fp_i_pigeon_swapped_prefix_injective)) * x3)) /\ exists ff_q_pigeon_swapped_prefix_injective_left. x2 = ff_q_pigeon_swapped_prefix_injective_left * S ((S (fp_i_pigeon_swapped_prefix_injective)) * x3) + (fp_value_pigeon_swapped_prefix_injective))) -> (((exists ff_h_pigeon_swapped_prefix_injective_right. ff_h_pigeon_swapped_prefix_injective_right + S (fp_value_pigeon_swapped_prefix_injective) = S ((S (fp_j_pigeon_swapped_prefix_injective)) * x3)) /\ exists ff_q_pigeon_swapped_prefix_injective_right. x2 = ff_q_pigeon_swapped_prefix_injective_right * S ((S (fp_j_pigeon_swapped_prefix_injective)) * x3) + (fp_value_pigeon_swapped_prefix_injective))) -> fp_i_pigeon_swapped_prefix_injective = fp_j_pigeon_swapped_prefix_injective
  122. 0122specialize finite_injective_prefix_succ x2
  123. 0123specialize finite_injective_prefix_succ x3
  124. 0124specialize finite_injective_prefix_succ n
  125. 0125specialize finite_injective_prefix_succ (S n)
  126. 0126apply finite_injective_prefix_succ
  127. 0127refl
  128. 0128exact hswap_injective
  129. 0129have hprefix_surjective : forall fp_value_pigeon_swapped_prefix_surjective. (exists fp_gap_pigeon_swapped_prefix_surjective_value. fp_gap_pigeon_swapped_prefix_surjective_value + S fp_value_pigeon_swapped_prefix_surjective = n) -> exists fp_i_pigeon_swapped_prefix_surjective. ((exists fp_gap_pigeon_swapped_prefix_surjective_index. fp_gap_pigeon_swapped_prefix_surjective_index + S fp_i_pigeon_swapped_prefix_surjective = n) /\ (((exists ff_h_pigeon_swapped_prefix_surjective_entry. ff_h_pigeon_swapped_prefix_surjective_entry + S (fp_value_pigeon_swapped_prefix_surjective) = S ((S (fp_i_pigeon_swapped_prefix_surjective)) * x3)) /\ exists ff_q_pigeon_swapped_prefix_surjective_entry. x2 = ff_q_pigeon_swapped_prefix_surjective_entry * S ((S (fp_i_pigeon_swapped_prefix_surjective)) * x3) + (fp_value_pigeon_swapped_prefix_surjective))))
  130. 0130specialize IH x2
  131. 0131specialize IH x3
  132. 0132apply IH
  133. 0133exact hprefix_bounded
  134. 0134exact hprefix_injective
  135. 0135have hswap_surjective : forall fp_value_pigeon_swapped_surjective. (exists fp_gap_pigeon_swapped_surjective_value. fp_gap_pigeon_swapped_surjective_value + S fp_value_pigeon_swapped_surjective = S n) -> exists fp_i_pigeon_swapped_surjective. ((exists fp_gap_pigeon_swapped_surjective_index. fp_gap_pigeon_swapped_surjective_index + S fp_i_pigeon_swapped_surjective = S n) /\ (((exists ff_h_pigeon_swapped_surjective_entry. ff_h_pigeon_swapped_surjective_entry + S (fp_value_pigeon_swapped_surjective) = S ((S (fp_i_pigeon_swapped_surjective)) * x3)) /\ exists ff_q_pigeon_swapped_surjective_entry. x2 = ff_q_pigeon_swapped_surjective_entry * S ((S (fp_i_pigeon_swapped_surjective)) * x3) + (fp_value_pigeon_swapped_surjective))))
  136. 0136specialize finite_surjective_succ_from_prefix x2
  137. 0137specialize finite_surjective_succ_from_prefix x3
  138. 0138specialize finite_surjective_succ_from_prefix n
  139. 0139specialize finite_surjective_succ_from_prefix (S n)
  140. 0140apply finite_surjective_succ_from_prefix
  141. 0141refl
  142. 0142exact hswap_bounded
  143. 0143exact hswap_injective
  144. 0144exact hprefix_surjective
  145. 0145specialize finite_swap_last_surjective_back b
  146. 0146specialize finite_swap_last_surjective_back c
  147. 0147specialize finite_swap_last_surjective_back x2
  148. 0148specialize finite_swap_last_surjective_back x3
  149. 0149specialize finite_swap_last_surjective_back n
  150. 0150specialize finite_swap_last_surjective_back (S n)
  151. 0151specialize finite_swap_last_surjective_back x
  152. 0152specialize finite_swap_last_surjective_back n
  153. 0153specialize finite_swap_last_surjective_back x1
  154. 0154apply finite_swap_last_surjective_back
  155. 0155refl
  156. 0156exact hcontains_left_witness_left
  157. 0157exact hcontains_left_witness_right
  158. 0158exact hlast_witness_left
  159. 0159exact hswap_witness_witness_left
  160. 0160exact hswap_witness_witness_right_left
  161. 0161exact hswap_witness_witness_right_right
  162. 0162exact hswap_surjective
  163. 0163specialize finite_no_top_successor_gate b
  164. 0164specialize finite_no_top_successor_gate c
  165. 0165specialize finite_no_top_successor_gate n
  166. 0166specialize finite_no_top_successor_gate (S n)
  167. 0167apply finite_no_top_successor_gate
  168. 0168refl
  169. 0169exact hbounded
  170. 0170exact hinjective
  171. 0171exact hcontains_right
  172. 0172intro hprefix_bounded
  173. 0173intro hprefix_injective
  174. 0174specialize IH b
  175. 0175specialize IH c
  176. 0176apply IH
  177. 0177exact hprefix_bounded
  178. 0178exact hprefix_injective