FS0015 · theorem body

four_square_cross_pigeonhole

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

Two bounded injective equal-length prefixes whose covered interleaving overflows their finite codomain have an actual witnessed cross-family value collision.

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.

Statement with defined notation

∀ b. ∀ c. ∀ d. ∀ e. ∀ z. ∀ t. ∀ l. ∀ p. (∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,p)) → (∀ x. Lt(x,l) → ∃ y. BetaAt(d,e,x,y) ∧ Lt(y,p)) → InjectivePrefix(b,c,l) → InjectivePrefix(d,e,l) → (∀ x. ∀ y. Lt(x,l + l) → BetaAt(z,t,x,y) → (∃ n. Lt(n,l) ∧ (BetaAt(b,c,n,y) ∧ x = n + n)) ∨ (∃ n. Lt(n,l) ∧ (BetaAt(d,e,n,y) ∧ x = S (n + n)))) → Lt(p,l + l) → ∃ x. ∃ y. ∃ n. Lt(x,l) ∧ (Lt(y,l) ∧ (BetaAt(b,c,x,n) ∧ BetaAt(d,e,y,n)))

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt PD0025 InjectivePrefix

In local proof propositions

PD0002 Lt PD0013 BetaAt
Exact expanded first-order statement
forall b c d e z t l p. (forall fscp_index_left. (exists fscp_gap_left_index. fscp_gap_left_index + S (fscp_index_left) = (l)) -> exists fscp_value_left. ((((exists ff_h_fscp_left_entry. ff_h_fscp_left_entry + S (fscp_value_left) = S ((S (fscp_index_left)) * c)) /\ exists ff_q_fscp_left_entry. b = ff_q_fscp_left_entry * S ((S (fscp_index_left)) * c) + (fscp_value_left))) /\ (exists fscp_gap_left_value. fscp_gap_left_value + S (fscp_value_left) = (p)))) -> (forall fscp_index_right. (exists fscp_gap_right_index. fscp_gap_right_index + S (fscp_index_right) = (l)) -> exists fscp_value_right. ((((exists ff_h_fscp_right_entry. ff_h_fscp_right_entry + S (fscp_value_right) = S ((S (fscp_index_right)) * e)) /\ exists ff_q_fscp_right_entry. d = ff_q_fscp_right_entry * S ((S (fscp_index_right)) * e) + (fscp_value_right))) /\ (exists fscp_gap_right_value. fscp_gap_right_value + S (fscp_value_right) = (p)))) -> (forall fp_i_fscp_left fp_j_fscp_left fp_value_fscp_left. (exists fp_gap_fscp_left_i. fp_gap_fscp_left_i + S fp_i_fscp_left = l) -> (exists fp_gap_fscp_left_j. fp_gap_fscp_left_j + S fp_j_fscp_left = l) -> (((exists ff_h_fscp_left_left. ff_h_fscp_left_left + S (fp_value_fscp_left) = S ((S (fp_i_fscp_left)) * c)) /\ exists ff_q_fscp_left_left. b = ff_q_fscp_left_left * S ((S (fp_i_fscp_left)) * c) + (fp_value_fscp_left))) -> (((exists ff_h_fscp_left_right. ff_h_fscp_left_right + S (fp_value_fscp_left) = S ((S (fp_j_fscp_left)) * c)) /\ exists ff_q_fscp_left_right. b = ff_q_fscp_left_right * S ((S (fp_j_fscp_left)) * c) + (fp_value_fscp_left))) -> fp_i_fscp_left = fp_j_fscp_left) -> (forall fp_i_fscp_right fp_j_fscp_right fp_value_fscp_right. (exists fp_gap_fscp_right_i. fp_gap_fscp_right_i + S fp_i_fscp_right = l) -> (exists fp_gap_fscp_right_j. fp_gap_fscp_right_j + S fp_j_fscp_right = l) -> (((exists ff_h_fscp_right_left. ff_h_fscp_right_left + S (fp_value_fscp_right) = S ((S (fp_i_fscp_right)) * e)) /\ exists ff_q_fscp_right_left. d = ff_q_fscp_right_left * S ((S (fp_i_fscp_right)) * e) + (fp_value_fscp_right))) -> (((exists ff_h_fscp_right_right. ff_h_fscp_right_right + S (fp_value_fscp_right) = S ((S (fp_j_fscp_right)) * e)) /\ exists ff_q_fscp_right_right. d = ff_q_fscp_right_right * S ((S (fp_j_fscp_right)) * e) + (fp_value_fscp_right))) -> fp_i_fscp_right = fp_j_fscp_right) -> (forall fscp_index_merged fscp_value_merged. (exists fscp_gap_merged_index. fscp_gap_merged_index + S (fscp_index_merged) = (l + l)) -> (((exists ff_h_fscp_merged_source. ff_h_fscp_merged_source + S (fscp_value_merged) = S ((S (fscp_index_merged)) * t)) /\ exists ff_q_fscp_merged_source. z = ff_q_fscp_merged_source * S ((S (fscp_index_merged)) * t) + (fscp_value_merged))) -> (((exists fscp_left_merged. ((exists fscp_gap_merged_left_bound. fscp_gap_merged_left_bound + S (fscp_left_merged) = (l)) /\ ((((exists ff_h_fscp_merged_left. ff_h_fscp_merged_left + S (fscp_value_merged) = S ((S (fscp_left_merged)) * c)) /\ exists ff_q_fscp_merged_left. b = ff_q_fscp_merged_left * S ((S (fscp_left_merged)) * c) + (fscp_value_merged))) /\ fscp_index_merged = fscp_left_merged + fscp_left_merged))) \/ (exists fscp_right_merged. ((exists fscp_gap_merged_right_bound. fscp_gap_merged_right_bound + S (fscp_right_merged) = (l)) /\ ((((exists ff_h_fscp_merged_right. ff_h_fscp_merged_right + S (fscp_value_merged) = S ((S (fscp_right_merged)) * e)) /\ exists ff_q_fscp_merged_right. d = ff_q_fscp_merged_right * S ((S (fscp_right_merged)) * e) + (fscp_value_merged))) /\ fscp_index_merged = S (fscp_right_merged + fscp_right_merged))))))) -> (exists fscp_gap_overflow. fscp_gap_overflow + S (p) = (l + l)) -> (exists fscp_left_result fscp_right_result fscp_value_result. ((exists fscp_gap_result_left_bound. fscp_gap_result_left_bound + S (fscp_left_result) = (l)) /\ ((exists fscp_gap_result_right_bound. fscp_gap_result_right_bound + S (fscp_right_result) = (l)) /\ ((((exists ff_h_fscp_result_left. ff_h_fscp_result_left + S (fscp_value_result) = S ((S (fscp_left_result)) * c)) /\ exists ff_q_fscp_result_left. b = ff_q_fscp_result_left * S ((S (fscp_left_result)) * c) + (fscp_value_result))) /\ (((exists ff_h_fscp_result_right. ff_h_fscp_result_right + S (fscp_value_result) = S ((S (fscp_right_result)) * e)) /\ exists ff_q_fscp_result_right. d = ff_q_fscp_result_right * S ((S (fscp_right_result)) * e) + (fscp_value_result)))))))

Proof neighborhood

Direct theorem prerequisites

FS0014 four_square_cross_covered_prefix_bounded finite_bounded_into_oversized_collision · Alpha closed

Direct theorem dependents

FS0017 four_square_cross_intersection

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

134 script commands · 44 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)
four square cross covered prefix bounded
01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
  5. L5
    intro z
  6. L6
    intro t
  7. L7
    intro l
  8. L8
    intro p
  9. L9
    intro hleft
  10. L10
    intro hright
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hleft_injective
  2. L12
    intro hright_injective
  3. L13
    intro hcover
  4. L14
    intro hoverflow
03Establish hboundedL15–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square cross covered prefix bounded.

  1. L15
    have hbounded : ∀ fscp_index_merged. Lt(fscp_index_merged,l + l) → ∃ x. BetaAt(z,t,fscp_index_merged,x) ∧ Lt(x,p)Definitions: Lt(fscp_index_merged,l + l)BetaAt(z,t,fscp_index_merged,x)Lt(x,p)Original native command in the exact edition
  2. L16
    specialize four_square_cross_covered_prefix_bounded b
  3. L17
    specialize four_square_cross_covered_prefix_bounded c
  4. L18
    specialize four_square_cross_covered_prefix_bounded d
  5. L19
    specialize four_square_cross_covered_prefix_bounded e
  6. L20
    specialize four_square_cross_covered_prefix_bounded z
  7. L21
    specialize four_square_cross_covered_prefix_bounded t
  8. L22
    specialize four_square_cross_covered_prefix_bounded l
  9. L23
    specialize four_square_cross_covered_prefix_bounded p
  10. L24
    apply four_square_cross_covered_prefix_bounded
04Use earlier factsL25–27

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

  1. L25
    exact hleft
  2. L26
    exact hright
  3. L27
    exact hcover
05Establish hcollisionL28–35

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

  1. L28
    have hcollision : ∃ ftsp_first_fscp_merge. ∃ ftsp_second_fscp_merge. ∃ ftsp_value_fscp_merge. Lt(ftsp_first_fscp_merge,l + l) ∧ (Lt(ftsp_second_fscp_merge,l + l) ∧ (¬ftsp_first_fscp_merge = ftsp_second_fscp_merge ∧ (BetaAt(z,t,ftsp_first_fscp_merge,ftsp_value_fscp_merge) ∧ BetaAt(z,t,ftsp_second_fscp_merge,ftsp_value_fscp_merge))))Definitions: Lt(ftsp_first_fscp_merge,l + l)Lt(ftsp_second_fscp_merge,l + l)BetaAt(z,t,ftsp_first_fscp_merge,ftsp_value_fscp_merge)BetaAt(z,t,ftsp_second_fscp_merge,ftsp_value_fscp_merge)Original native command in the exact edition
  2. L29
    specialize finite_bounded_into_oversized_collision z
  3. L30
    specialize finite_bounded_into_oversized_collision t
  4. L31
    specialize finite_bounded_into_oversized_collision (l + l)
  5. L32
    specialize finite_bounded_into_oversized_collision p
  6. L33
    apply finite_bounded_into_oversized_collision
  7. L34
    exact hbounded
  8. L35
    exact hoverflow
06Separate the logical casesL36–42

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

  1. L36
    cases hcollision
  2. L37
    cases hcollision_witness
  3. L38
    cases hcollision_witness_witness
  4. L39
    cases hcollision_witness_witness_witness
  5. L40
    cases hcollision_witness_witness_witness_right
  6. L41
    cases hcollision_witness_witness_witness_right_right
  7. L42
    cases hcollision_witness_witness_witness_right_right_right
07Establish hfirst_caseL43–48

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

  1. L43
    have hfirst_case : (∃ y. Lt(y,l) ∧ (BetaAt(b,c,y,x2) ∧ x = y + y)) ∨ (∃ y. Lt(y,l) ∧ (BetaAt(d,e,y,x2) ∧ x = S (y + y)))Definitions: Lt(y,l)BetaAt(b,c,y,x2)BetaAt(d,e,y,x2)Original native command in the exact edition
  2. L44
    specialize hcover x
  3. L45
    specialize hcover x2
  4. L46
    apply hcover
  5. L47
    exact hcollision_witness_witness_witness_left
  6. L48
    exact hcollision_witness_witness_witness_right_right_right_left
08Establish hsecond_caseL49–54

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

  1. L49
    have hsecond_case : (∃ x. Lt(x,l) ∧ (BetaAt(b,c,x,x2) ∧ x1 = x + x)) ∨ (∃ x. Lt(x,l) ∧ (BetaAt(d,e,x,x2) ∧ x1 = S (x + x)))Definitions: Lt(x,l)BetaAt(b,c,x,x2)BetaAt(d,e,x,x2)Original native command in the exact edition
  2. L50
    specialize hcover x1
  3. L51
    specialize hcover x2
  4. L52
    apply hcover
  5. L53
    exact hcollision_witness_witness_witness_right_left
  6. L54
    exact hcollision_witness_witness_witness_right_right_right_right
09Separate the logical casesL55–62

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

  1. L55
    cases hfirst_case
  2. L56
    cases hfirst_case_left
  3. L57
    cases hfirst_case_left_witness
  4. L58
    cases hfirst_case_left_witness_right
  5. L59
    cases hsecond_case
  6. L60
    cases hsecond_case_left
  7. L61
    cases hsecond_case_left_witness
  8. L62
    cases hsecond_case_left_witness_right
10Establish hequalL63–71

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

  1. L63
    have hequal : x3 = x4
  2. L64
    specialize hleft_injective x3
  3. L65
    specialize hleft_injective x4
  4. L66
    specialize hleft_injective x2
  5. L67
    apply hleft_injective
  6. L68
    exact hfirst_case_left_witness_left
  7. L69
    exact hsecond_case_left_witness_left
  8. L70
    exact hfirst_case_left_witness_right_left
  9. L71
    exact hsecond_case_left_witness_right_left
11Separate the logical casesL72–72

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

  1. L72
    exfalso
12Use earlier factsL73–73

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

  1. L73
    apply hcollision_witness_witness_witness_right_right_left
13Calculate and transport equalitiesL74–74

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

  1. L74
    trans x3 + x3
14Use earlier factsL75–75

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

  1. L75
    exact hfirst_case_left_witness_right_right
15Calculate and transport equalitiesL76–77

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

  1. L76
    trans x4 + x4
  2. L77
    congr
16Use earlier factsL78–79

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

  1. L78
    exact hequal
  2. L79
    exact hequal
17Calculate and transport equalitiesL80–80

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

  1. L80
    symm
18Use earlier factsL81–81

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

  1. L81
    exact hsecond_case_left_witness_right_right
19Separate the logical casesL82–84

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

  1. L82
    cases hsecond_case_right
  2. L83
    cases hsecond_case_right_witness
  3. L84
    cases hsecond_case_right_witness_right
20Construct an explicit witnessL85–87

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

  1. L85
    exists x3
  2. L86
    exists x4
  3. L87
    exists x2
21Separate the logical casesL88–88

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

  1. L88
    split
22Use earlier factsL89–89

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

  1. L89
    exact hfirst_case_left_witness_left
23Separate the logical casesL90–90

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

  1. L90
    split
24Use earlier factsL91–91

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

  1. L91
    exact hsecond_case_right_witness_left
25Separate the logical casesL92–92

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

  1. L92
    split
26Use earlier factsL93–94

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

  1. L93
    exact hfirst_case_left_witness_right_left
  2. L94
    exact hsecond_case_right_witness_right_left
27Separate the logical casesL95–101

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

  1. L95
    cases hfirst_case_right
  2. L96
    cases hfirst_case_right_witness
  3. L97
    cases hfirst_case_right_witness_right
  4. L98
    cases hsecond_case
  5. L99
    cases hsecond_case_left
  6. L100
    cases hsecond_case_left_witness
  7. L101
    cases hsecond_case_left_witness_right
28Construct an explicit witnessL102–104

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

  1. L102
    exists x4
  2. L103
    exists x3
  3. L104
    exists x2
29Separate the logical casesL105–105

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

  1. L105
    split
30Use earlier factsL106–106

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

  1. L106
    exact hsecond_case_left_witness_left
31Separate the logical casesL107–107

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

  1. L107
    split
32Use earlier factsL108–108

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

  1. L108
    exact hfirst_case_right_witness_left
33Separate the logical casesL109–109

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

  1. L109
    split
34Use earlier factsL110–111

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

  1. L110
    exact hsecond_case_left_witness_right_left
  2. L111
    exact hfirst_case_right_witness_right_left
35Separate the logical casesL112–114

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

  1. L112
    cases hsecond_case_right
  2. L113
    cases hsecond_case_right_witness
  3. L114
    cases hsecond_case_right_witness_right
36Establish hequalL115–123

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

  1. L115
    have hequal : x3 = x4
  2. L116
    specialize hright_injective x3
  3. L117
    specialize hright_injective x4
  4. L118
    specialize hright_injective x2
  5. L119
    apply hright_injective
  6. L120
    exact hfirst_case_right_witness_left
  7. L121
    exact hsecond_case_right_witness_left
  8. L122
    exact hfirst_case_right_witness_right_left
  9. L123
    exact hsecond_case_right_witness_right_left
37Separate the logical casesL124–124

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

  1. L124
    exfalso
38Use earlier factsL125–125

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

  1. L125
    apply hcollision_witness_witness_witness_right_right_left
39Calculate and transport equalitiesL126–126

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

  1. L126
    trans S (x3 + x3)
40Use earlier factsL127–127

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

  1. L127
    exact hfirst_case_right_witness_right_right
41Calculate and transport equalitiesL128–130

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

  1. L128
    trans S (x4 + x4)
  2. L129
    congr
  3. L130
    congr
42Use earlier factsL131–132

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

  1. L131
    exact hequal
  2. L132
    exact hequal
43Calculate and transport equalitiesL133–133

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

  1. L133
    symm
44Use earlier factsL134–134

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

  1. L134
    exact hsecond_case_right_witness_right_right

Library-wide reading audit

Original defined command ledger · 134 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro z
  6. 0006intro t
  7. 0007intro l
  8. 0008intro p
  9. 0009intro hleft
  10. 0010intro hright
  11. 0011intro hleft_injective
  12. 0012intro hright_injective
  13. 0013intro hcover
  14. 0014intro hoverflow
  15. 0015have hbounded : ∀ fscp_index_merged. Lt(fscp_index_merged,l + l) → ∃ x. BetaAt(z,t,fscp_index_merged,x) ∧ Lt(x,p)
    Exact native replay linehave hbounded : forall fscp_index_merged. (exists fscp_gap_merged_index. fscp_gap_merged_index + S (fscp_index_merged) = (l + l)) -> exists fscp_value_merged. ((((exists ff_h_fscp_merged_entry. ff_h_fscp_merged_entry + S (fscp_value_merged) = S ((S (fscp_index_merged)) * t)) /\ exists ff_q_fscp_merged_entry. z = ff_q_fscp_merged_entry * S ((S (fscp_index_merged)) * t) + (fscp_value_merged))) /\ (exists fscp_gap_merged_value. fscp_gap_merged_value + S (fscp_value_merged) = (p)))
  16. 0016specialize four_square_cross_covered_prefix_bounded b
  17. 0017specialize four_square_cross_covered_prefix_bounded c
  18. 0018specialize four_square_cross_covered_prefix_bounded d
  19. 0019specialize four_square_cross_covered_prefix_bounded e
  20. 0020specialize four_square_cross_covered_prefix_bounded z
  21. 0021specialize four_square_cross_covered_prefix_bounded t
  22. 0022specialize four_square_cross_covered_prefix_bounded l
  23. 0023specialize four_square_cross_covered_prefix_bounded p
  24. 0024apply four_square_cross_covered_prefix_bounded
  25. 0025exact hleft
  26. 0026exact hright
  27. 0027exact hcover
  28. 0028have hcollision : ∃ ftsp_first_fscp_merge. ∃ ftsp_second_fscp_merge. ∃ ftsp_value_fscp_merge. Lt(ftsp_first_fscp_merge,l + l) ∧ (Lt(ftsp_second_fscp_merge,l + l) ∧ (¬ftsp_first_fscp_merge = ftsp_second_fscp_merge ∧ (BetaAt(z,t,ftsp_first_fscp_merge,ftsp_value_fscp_merge) ∧ BetaAt(z,t,ftsp_second_fscp_merge,ftsp_value_fscp_merge))))
    Exact native replay linehave hcollision : exists ftsp_first_fscp_merge ftsp_second_fscp_merge ftsp_value_fscp_merge. ((exists ftsp_gap_fscp_merge_first. ftsp_gap_fscp_merge_first + S (ftsp_first_fscp_merge) = l + l) /\ ((exists ftsp_gap_fscp_merge_second. ftsp_gap_fscp_merge_second + S (ftsp_second_fscp_merge) = l + l) /\ (~(ftsp_first_fscp_merge = ftsp_second_fscp_merge) /\ ((((exists ff_h_ftsp_fscp_merge_left. ff_h_ftsp_fscp_merge_left + S (ftsp_value_fscp_merge) = S ((S (ftsp_first_fscp_merge)) * t)) /\ exists ff_q_ftsp_fscp_merge_left. z = ff_q_ftsp_fscp_merge_left * S ((S (ftsp_first_fscp_merge)) * t) + (ftsp_value_fscp_merge))) /\ (((exists ff_h_ftsp_fscp_merge_right. ff_h_ftsp_fscp_merge_right + S (ftsp_value_fscp_merge) = S ((S (ftsp_second_fscp_merge)) * t)) /\ exists ff_q_ftsp_fscp_merge_right. z = ff_q_ftsp_fscp_merge_right * S ((S (ftsp_second_fscp_merge)) * t) + (ftsp_value_fscp_merge)))))))
  29. 0029specialize finite_bounded_into_oversized_collision z
  30. 0030specialize finite_bounded_into_oversized_collision t
  31. 0031specialize finite_bounded_into_oversized_collision (l + l)
  32. 0032specialize finite_bounded_into_oversized_collision p
  33. 0033apply finite_bounded_into_oversized_collision
  34. 0034exact hbounded
  35. 0035exact hoverflow
  36. 0036cases hcollision
  37. 0037cases hcollision_witness
  38. 0038cases hcollision_witness_witness
  39. 0039cases hcollision_witness_witness_witness
  40. 0040cases hcollision_witness_witness_witness_right
  41. 0041cases hcollision_witness_witness_witness_right_right
  42. 0042cases hcollision_witness_witness_witness_right_right_right
  43. 0043have hfirst_case : (∃ y. Lt(y,l) ∧ (BetaAt(b,c,y,x2) ∧ x = y + y)) ∨ (∃ y. Lt(y,l) ∧ (BetaAt(d,e,y,x2) ∧ x = S (y + y)))
    Exact native replay linehave hfirst_case : ((exists fscp_left_first_case. ((exists fscp_gap_first_case_left_bound. fscp_gap_first_case_left_bound + S (fscp_left_first_case) = (l)) /\ ((((exists ff_h_fscp_first_case_left. ff_h_fscp_first_case_left + S (x2) = S ((S (fscp_left_first_case)) * c)) /\ exists ff_q_fscp_first_case_left. b = ff_q_fscp_first_case_left * S ((S (fscp_left_first_case)) * c) + (x2))) /\ x = fscp_left_first_case + fscp_left_first_case))) \/ (exists fscp_right_first_case. ((exists fscp_gap_first_case_right_bound. fscp_gap_first_case_right_bound + S (fscp_right_first_case) = (l)) /\ ((((exists ff_h_fscp_first_case_right. ff_h_fscp_first_case_right + S (x2) = S ((S (fscp_right_first_case)) * e)) /\ exists ff_q_fscp_first_case_right. d = ff_q_fscp_first_case_right * S ((S (fscp_right_first_case)) * e) + (x2))) /\ x = S (fscp_right_first_case + fscp_right_first_case)))))
  44. 0044specialize hcover x
  45. 0045specialize hcover x2
  46. 0046apply hcover
  47. 0047exact hcollision_witness_witness_witness_left
  48. 0048exact hcollision_witness_witness_witness_right_right_right_left
  49. 0049have hsecond_case : (∃ x. Lt(x,l) ∧ (BetaAt(b,c,x,x2) ∧ x1 = x + x)) ∨ (∃ x. Lt(x,l) ∧ (BetaAt(d,e,x,x2) ∧ x1 = S (x + x)))
    Exact native replay linehave hsecond_case : ((exists fscp_left_second_case. ((exists fscp_gap_second_case_left_bound. fscp_gap_second_case_left_bound + S (fscp_left_second_case) = (l)) /\ ((((exists ff_h_fscp_second_case_left. ff_h_fscp_second_case_left + S (x2) = S ((S (fscp_left_second_case)) * c)) /\ exists ff_q_fscp_second_case_left. b = ff_q_fscp_second_case_left * S ((S (fscp_left_second_case)) * c) + (x2))) /\ x1 = fscp_left_second_case + fscp_left_second_case))) \/ (exists fscp_right_second_case. ((exists fscp_gap_second_case_right_bound. fscp_gap_second_case_right_bound + S (fscp_right_second_case) = (l)) /\ ((((exists ff_h_fscp_second_case_right. ff_h_fscp_second_case_right + S (x2) = S ((S (fscp_right_second_case)) * e)) /\ exists ff_q_fscp_second_case_right. d = ff_q_fscp_second_case_right * S ((S (fscp_right_second_case)) * e) + (x2))) /\ x1 = S (fscp_right_second_case + fscp_right_second_case)))))
  50. 0050specialize hcover x1
  51. 0051specialize hcover x2
  52. 0052apply hcover
  53. 0053exact hcollision_witness_witness_witness_right_left
  54. 0054exact hcollision_witness_witness_witness_right_right_right_right
  55. 0055cases hfirst_case
  56. 0056cases hfirst_case_left
  57. 0057cases hfirst_case_left_witness
  58. 0058cases hfirst_case_left_witness_right
  59. 0059cases hsecond_case
  60. 0060cases hsecond_case_left
  61. 0061cases hsecond_case_left_witness
  62. 0062cases hsecond_case_left_witness_right
  63. 0063have hequal : x3 = x4
  64. 0064specialize hleft_injective x3
  65. 0065specialize hleft_injective x4
  66. 0066specialize hleft_injective x2
  67. 0067apply hleft_injective
  68. 0068exact hfirst_case_left_witness_left
  69. 0069exact hsecond_case_left_witness_left
  70. 0070exact hfirst_case_left_witness_right_left
  71. 0071exact hsecond_case_left_witness_right_left
  72. 0072exfalso
  73. 0073apply hcollision_witness_witness_witness_right_right_left
  74. 0074trans x3 + x3
  75. 0075exact hfirst_case_left_witness_right_right
  76. 0076trans x4 + x4
  77. 0077congr
  78. 0078exact hequal
  79. 0079exact hequal
  80. 0080symm
  81. 0081exact hsecond_case_left_witness_right_right
  82. 0082cases hsecond_case_right
  83. 0083cases hsecond_case_right_witness
  84. 0084cases hsecond_case_right_witness_right
  85. 0085exists x3
  86. 0086exists x4
  87. 0087exists x2
  88. 0088split
  89. 0089exact hfirst_case_left_witness_left
  90. 0090split
  91. 0091exact hsecond_case_right_witness_left
  92. 0092split
  93. 0093exact hfirst_case_left_witness_right_left
  94. 0094exact hsecond_case_right_witness_right_left
  95. 0095cases hfirst_case_right
  96. 0096cases hfirst_case_right_witness
  97. 0097cases hfirst_case_right_witness_right
  98. 0098cases hsecond_case
  99. 0099cases hsecond_case_left
  100. 0100cases hsecond_case_left_witness
  101. 0101cases hsecond_case_left_witness_right
  102. 0102exists x4
  103. 0103exists x3
  104. 0104exists x2
  105. 0105split
  106. 0106exact hsecond_case_left_witness_left
  107. 0107split
  108. 0108exact hfirst_case_right_witness_left
  109. 0109split
  110. 0110exact hsecond_case_left_witness_right_left
  111. 0111exact hfirst_case_right_witness_right_left
  112. 0112cases hsecond_case_right
  113. 0113cases hsecond_case_right_witness
  114. 0114cases hsecond_case_right_witness_right
  115. 0115have hequal : x3 = x4
  116. 0116specialize hright_injective x3
  117. 0117specialize hright_injective x4
  118. 0118specialize hright_injective x2
  119. 0119apply hright_injective
  120. 0120exact hfirst_case_right_witness_left
  121. 0121exact hsecond_case_right_witness_left
  122. 0122exact hfirst_case_right_witness_right_left
  123. 0123exact hsecond_case_right_witness_right_left
  124. 0124exfalso
  125. 0125apply hcollision_witness_witness_witness_right_right_left
  126. 0126trans S (x3 + x3)
  127. 0127exact hfirst_case_right_witness_right_right
  128. 0128trans S (x4 + x4)
  129. 0129congr
  130. 0130congr
  131. 0131exact hequal
  132. 0132exact hequal
  133. 0133symm
  134. 0134exact hsecond_case_right_witness_right_right