PA00B4 · theorem

finite_bounded_nonendpoint_injective_coverage

Alpha v34 checked-use theorem · independently closed; not Stable

A bounded injective terminal prefix covers exactly every nonendpoint value below n = l+2.

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. ∀ l. (∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,S S l)) → (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → ¬y = 0 ∧ ¬S y = S S l) → InjectivePrefix(b,c,l) → ∀ x. Lt(x,S S l) → ¬x = 0 ∧ ¬S x = S S l → ContainsPrefix(b,c,l,x)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt PD0025 InjectivePrefix PD0027 ContainsPrefix

8 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0013 BetaAt PD0026 SurjectivePrefix PD0027 ContainsPrefix

20 occurrences

Exact expanded native-PA statement
forall b c l. (forall fom_index_wpoi_terminal_bounded. (exists fom_gap_wpoi_terminal_bounded_index_bound. fom_gap_wpoi_terminal_bounded_index_bound + S (fom_index_wpoi_terminal_bounded) = l) -> exists fom_value_wpoi_terminal_bounded. ((((exists fom_beta_height_wpoi_terminal_bounded_entry. fom_beta_height_wpoi_terminal_bounded_entry + S (fom_value_wpoi_terminal_bounded) = S ((S (fom_index_wpoi_terminal_bounded)) * c)) /\ exists fom_beta_quotient_wpoi_terminal_bounded_entry. b = fom_beta_quotient_wpoi_terminal_bounded_entry * S ((S (fom_index_wpoi_terminal_bounded)) * c) + (fom_value_wpoi_terminal_bounded))) /\ (exists fom_gap_wpoi_terminal_bounded_value_bound. fom_gap_wpoi_terminal_bounded_value_bound + S (fom_value_wpoi_terminal_bounded) = S (S l)))) -> (forall wpo_position_wpoi_terminal_nonendpoint wpo_value_wpoi_terminal_nonendpoint. (exists wpo_gap_wpoi_terminal_nonendpoint_position_bound. wpo_gap_wpoi_terminal_nonendpoint_position_bound + S (wpo_position_wpoi_terminal_nonendpoint) = l) -> (((exists wpo_beta_height_wpoi_terminal_nonendpoint_entry. wpo_beta_height_wpoi_terminal_nonendpoint_entry + S (wpo_value_wpoi_terminal_nonendpoint) = S ((S (wpo_position_wpoi_terminal_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_nonendpoint_entry. b = wpo_beta_quotient_wpoi_terminal_nonendpoint_entry * S ((S (wpo_position_wpoi_terminal_nonendpoint)) * c) + (wpo_value_wpoi_terminal_nonendpoint))) -> (~(wpo_value_wpoi_terminal_nonendpoint = 0) /\ ~((S wpo_value_wpoi_terminal_nonendpoint) = S (S l)))) -> (forall wpo_injective_left_wpoi_terminal_injective wpo_injective_right_wpoi_terminal_injective wpo_injective_value_wpoi_terminal_injective. (exists wpo_gap_wpoi_terminal_injective_left_bound. wpo_gap_wpoi_terminal_injective_left_bound + S (wpo_injective_left_wpoi_terminal_injective) = l) -> (exists wpo_gap_wpoi_terminal_injective_right_bound. wpo_gap_wpoi_terminal_injective_right_bound + S (wpo_injective_right_wpoi_terminal_injective) = l) -> (((exists wpo_beta_height_wpoi_terminal_injective_left_entry. wpo_beta_height_wpoi_terminal_injective_left_entry + S (wpo_injective_value_wpoi_terminal_injective) = S ((S (wpo_injective_left_wpoi_terminal_injective)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_injective_left_entry. b = wpo_beta_quotient_wpoi_terminal_injective_left_entry * S ((S (wpo_injective_left_wpoi_terminal_injective)) * c) + (wpo_injective_value_wpoi_terminal_injective))) -> (((exists wpo_beta_height_wpoi_terminal_injective_right_entry. wpo_beta_height_wpoi_terminal_injective_right_entry + S (wpo_injective_value_wpoi_terminal_injective) = S ((S (wpo_injective_right_wpoi_terminal_injective)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_injective_right_entry. b = wpo_beta_quotient_wpoi_terminal_injective_right_entry * S ((S (wpo_injective_right_wpoi_terminal_injective)) * c) + (wpo_injective_value_wpoi_terminal_injective))) -> wpo_injective_left_wpoi_terminal_injective = wpo_injective_right_wpoi_terminal_injective) -> forall s. (exists wpo_gap_wpoi_terminal_value_bound. wpo_gap_wpoi_terminal_value_bound + S (s) = S (S l)) -> (~(s = 0) /\ ~((S s) = S (S l))) -> (exists q. ((exists wpo_gap_wpoi_terminal_index_bound. wpo_gap_wpoi_terminal_index_bound + S (q) = l) /\ (((exists wpo_beta_height_wpoi_terminal_entry. wpo_beta_height_wpoi_terminal_entry + S (s) = S ((S (q)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_entry. b = wpo_beta_quotient_wpoi_terminal_entry * S ((S (q)) * c) + (s)))))

Proof neighborhood

Direct theorem prerequisites

PA002L one_le_of_ne_zero PA000V le_of_succ_le_succ PA000W le_eq_or_lt PA001V nonzero_is_succ PA007D beta_magnitude_predecessor_recode_exists PA00B3 beta_magnitude_predecessor_recode_surjective PA007T beta_magnitude_predecessor_recode_reflect

Direct theorem dependents

PA00B5 pair_order_state_terminal_coverage

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

126 script commands · 40 reading checkpoints · 14 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 (7)
one le of ne zerole of succ le succle eq or ltnonzero is succbeta magnitude predecessor recode existsbeta magnitude predecessor recode surjectivebeta magnitude predecessor recode reflect
01Fix variables and assumptionsL1–6

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 hbounded
  5. L5
    intro hnonendpoint
  6. L6
    intro hinjective
02Establish hmagnitudeL7–9

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

  1. L7
    have hmagnitude : ∀ gmp_index_wpoi_terminal_magnitude_range. Lt(gmp_index_wpoi_terminal_magnitude_range,l) → ∃ x. BetaAt(b,c,gmp_index_wpoi_terminal_magnitude_range,x) ∧ (Lt(0,x) ∧ Le(x,l))Definitions: Lt(gmp_index_wpoi_terminal_magnitude_range,l)BetaAt(b,c,gmp_index_wpoi_terminal_magnitude_range,x)Lt(0,x)Le(x,l)Original native command in the exact edition
  2. L8
    intro q
  3. L9
    intro hq
03Establish hbounded_entryL10–13

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

  1. L10
    have hbounded_entry : ∃ x. BetaAt(b,c,q,x) ∧ Lt(x,S S l)Definitions: BetaAt(b,c,q,x)Lt(x,S S l)Original native command in the exact edition
  2. L11
    specialize hbounded q
  3. L12
    apply hbounded
  4. L13
    exact hq
04Separate the logical casesL14–15

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

  1. L14
    cases hbounded_entry
  2. L15
    cases hbounded_entry_witness
05Establish hxnonendpointL16–21

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

  1. L16
    have hxnonendpoint : ~(x = 0) /\ ~((S x) = S (S l))
  2. L17
    specialize hnonendpoint q
  3. L18
    specialize hnonendpoint x
  4. L19
    apply hnonendpoint
  5. L20
    exact hq
  6. L21
    exact hbounded_entry_witness_left
06Separate the logical casesL22–22

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

  1. L22
    cases hxnonendpoint
07Construct an explicit witnessL23–23

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

  1. L23
    exists x
08Separate the logical casesL24–24

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

  1. L24
    split
09Use earlier factsL25–25

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

  1. L25
    exact hbounded_entry_witness_left
10Separate the logical casesL26–26

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

  1. L26
    split
11Use earlier factsL27–29

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

  1. L27
    specialize one_le_of_ne_zero x
  2. L28
    apply one_le_of_ne_zero
  3. L29
    exact hxnonendpoint_left
12Establish hxle_succL30–34

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

  1. L30
    have hxle_succ : Le(x,S l)Definitions: Le(x,S l)Original native command in the exact edition
  2. L31
    specialize le_of_succ_le_succ x
  3. L32
    specialize le_of_succ_le_succ (S l)
  4. L33
    apply le_of_succ_le_succ
  5. L34
    exact hbounded_entry_witness_right
13Establish hxsplitL35–39

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

  1. L35
    have hxsplit : x = S l ∨ Lt(x,S l)Definitions: Lt(x,S l)Original native command in the exact edition
  2. L36
    specialize le_eq_or_lt x
  3. L37
    specialize le_eq_or_lt (S l)
  4. L38
    apply le_eq_or_lt
  5. L39
    exact hxle_succ
14Separate the logical casesL40–41

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

  1. L40
    cases hxsplit
  2. L41
    exfalso
15Use earlier factsL42–42

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

  1. L42
    apply hxnonendpoint_right
16Calculate and transport equalitiesL43–44

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

  1. L43
    rewrite hxsplit_left
  2. L44
    refl
17Use earlier factsL45–48

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

  1. L45
    specialize le_of_succ_le_succ x
  2. L46
    specialize le_of_succ_le_succ l
  3. L47
    apply le_of_succ_le_succ
  4. L48
    exact hxsplit_right
18Establish hrecode_existsL49–55

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta magnitude predecessor recode exists.

  1. L49
    have hrecode_exists : ∃ rb. ∃ rc. ∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,S y) → BetaAt(rb,rc,x,y)Definitions: Lt(x,l)BetaAt(b,c,x,S y)BetaAt(rb,rc,x,y)Original native command in the exact edition
  2. L50
    specialize beta_magnitude_predecessor_recode_exists b
  3. L51
    specialize beta_magnitude_predecessor_recode_exists c
  4. L52
    specialize beta_magnitude_predecessor_recode_exists l
  5. L53
    specialize beta_magnitude_predecessor_recode_exists l
  6. L54
    apply beta_magnitude_predecessor_recode_exists
  7. L55
    exact hmagnitude
19Separate the logical casesL56–57

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

  1. L56
    cases hrecode_exists
  2. L57
    cases hrecode_exists_witness
20Establish hrecodeL58–59

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

  1. L58
    have hrecode : ∀ gmp_index_wpoi_terminal_recode_x. ∀ gmp_predecessor_wpoi_terminal_recode_x. Lt(gmp_index_wpoi_terminal_recode_x,l) → BetaAt(b,c,gmp_index_wpoi_terminal_recode_x,S gmp_predecessor_wpoi_terminal_recode_x) → BetaAt(x,x1,gmp_index_wpoi_terminal_recode_x,gmp_predecessor_wpoi_terminal_recode_x)Definitions: Lt(gmp_index_wpoi_terminal_recode_x,l)BetaAt(b,c,gmp_index_wpoi_terminal_recode_x,S gmp_predecessor_wpoi_terminal_recode_x)BetaAt(x,x1,gmp_index_wpoi_terminal_recode_x,gmp_predecessor_wpoi_terminal_recode_x)Original native command in the exact edition
  2. L59
    exact hrecode_exists_witness_witness
21Establish hsurjectiveL60–69

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta magnitude predecessor recode surjective.

  1. L60
    have hsurjective : SurjectivePrefix(x,x1,l)Definitions: SurjectivePrefix(x,x1,l)Original native command in the exact edition
  2. L61
    specialize beta_magnitude_predecessor_recode_surjective b
  3. L62
    specialize beta_magnitude_predecessor_recode_surjective c
  4. L63
    specialize beta_magnitude_predecessor_recode_surjective x
  5. L64
    specialize beta_magnitude_predecessor_recode_surjective x1
  6. L65
    specialize beta_magnitude_predecessor_recode_surjective l
  7. L66
    apply beta_magnitude_predecessor_recode_surjective
  8. L67
    exact hmagnitude
  9. L68
    exact hinjective
  10. L69
    exact hrecode
22Fix variables and assumptionsL70–72

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

  1. L70
    intro s
  2. L71
    intro hsbound
  3. L72
    intro hsendpoints
23Separate the logical casesL73–73

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

  1. L73
    cases hsendpoints
24Establish hspredL74–77

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

  1. L74
    have hspred : exists r. s = S r
  2. L75
    specialize nonzero_is_succ s
  3. L76
    apply nonzero_is_succ
  4. L77
    exact hsendpoints_left
25Separate the logical casesL78–78

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

  1. L78
    cases hspred
26Establish hsleL79–84

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

  1. L79
  2. L80
    specialize le_of_succ_le_succ s
  3. L81
    specialize le_of_succ_le_succ (S l)
  4. L82
    apply le_of_succ_le_succ
  5. L83
    exact hsbound
  6. L84
    rewrite hspred_witness at hsle
27Establish hrleL85–89

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

  1. L85
  2. L86
    specialize le_of_succ_le_succ x2
  3. L87
    specialize le_of_succ_le_succ l
  4. L88
    apply le_of_succ_le_succ
  5. L89
    exact hsle
28Establish hrsplitL90–94

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

  1. L90
    have hrsplit : x2 = l ∨ Lt(x2,l)Definitions: Lt(x2,l)Original native command in the exact edition
  2. L91
    specialize le_eq_or_lt x2
  3. L92
    specialize le_eq_or_lt l
  4. L93
    apply le_eq_or_lt
  5. L94
    exact hrle
29Separate the logical casesL95–96

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

  1. L95
    cases hrsplit
  2. L96
    exfalso
30Use earlier factsL97–97

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

  1. L97
    apply hsendpoints_right
31Calculate and transport equalitiesL98–100

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

  1. L98
    rewrite hspred_witness
  2. L99
    rewrite hrsplit_left
  3. L100
    refl
32Establish htargetL101–104

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

  1. L101
    have htarget : ContainsPrefix(x,x1,l,x2)Definitions: ContainsPrefix(x,x1,l,x2)Original native command in the exact edition
  2. L102
    specialize hsurjective x2
  3. L103
    apply hsurjective
  4. L104
    exact hrsplit_right
33Separate the logical casesL105–106

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

  1. L105
    cases htarget
  2. L106
    cases htarget_witness
34Establish hsourceL107–116

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta magnitude predecessor recode reflect.

  1. L107
    have hsource : BetaAt(b,c,x3,S x2)Definitions: BetaAt(b,c,x3,S x2)Original native command in the exact edition
  2. L108
    specialize beta_magnitude_predecessor_recode_reflect b
  3. L109
    specialize beta_magnitude_predecessor_recode_reflect c
  4. L110
    specialize beta_magnitude_predecessor_recode_reflect x
  5. L111
    specialize beta_magnitude_predecessor_recode_reflect x1
  6. L112
    specialize beta_magnitude_predecessor_recode_reflect l
  7. L113
    specialize beta_magnitude_predecessor_recode_reflect l
  8. L114
    specialize beta_magnitude_predecessor_recode_reflect x3
  9. L115
    specialize beta_magnitude_predecessor_recode_reflect x2
  10. L116
    apply beta_magnitude_predecessor_recode_reflect
35Use earlier factsL117–120

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

  1. L117
    exact hmagnitude
  2. L118
    exact hrecode
  3. L119
    exact htarget_witness_left
  4. L120
    exact htarget_witness_right
36Construct an explicit witnessL121–121

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

  1. L121
    exists x3
37Separate the logical casesL122–122

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

  1. L122
    split
38Use earlier factsL123–123

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

  1. L123
    exact htarget_witness_left
39Calculate and transport equalitiesL124–125

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

  1. L124
    rewrite hspred_witness
  2. L125
    rewrite hspred_witness
40Use earlier factsL126–126

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

  1. L126
    exact hsource

Library-wide reading audit

Original defined command ledger · 126 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro hbounded
  5. 0005intro hnonendpoint
  6. 0006intro hinjective
  7. 0007have hmagnitude : ∀ gmp_index_wpoi_terminal_magnitude_range. Lt(gmp_index_wpoi_terminal_magnitude_range,l) → ∃ x. BetaAt(b,c,gmp_index_wpoi_terminal_magnitude_range,x) ∧ (Lt(0,x) ∧ Le(x,l))
    Exact native replay linehave hmagnitude : forall gmp_index_wpoi_terminal_magnitude_range. (exists gsp_lt_gap_wpoi_terminal_magnitude_range_index_bound. gsp_lt_gap_wpoi_terminal_magnitude_range_index_bound + S gmp_index_wpoi_terminal_magnitude_range = l) -> exists gmp_magnitude_wpoi_terminal_magnitude_range. ((((exists ff_h_gmp_wpoi_terminal_magnitude_range_decoded. ff_h_gmp_wpoi_terminal_magnitude_range_decoded + S (gmp_magnitude_wpoi_terminal_magnitude_range) = S ((S (gmp_index_wpoi_terminal_magnitude_range)) * c)) /\ exists ff_q_gmp_wpoi_terminal_magnitude_range_decoded. b = ff_q_gmp_wpoi_terminal_magnitude_range_decoded * S ((S (gmp_index_wpoi_terminal_magnitude_range)) * c) + (gmp_magnitude_wpoi_terminal_magnitude_range))) /\ ((exists gsp_lt_gap_wpoi_terminal_magnitude_range_positive. gsp_lt_gap_wpoi_terminal_magnitude_range_positive + S 0 = gmp_magnitude_wpoi_terminal_magnitude_range) /\ (exists gsp_le_gap_wpoi_terminal_magnitude_range_bounded. gsp_le_gap_wpoi_terminal_magnitude_range_bounded + gmp_magnitude_wpoi_terminal_magnitude_range = l)))
  8. 0008intro q
  9. 0009intro hq
  10. 0010have hbounded_entry : ∃ x. BetaAt(b,c,q,x) ∧ Lt(x,S S l)
    Exact native replay linehave hbounded_entry : exists x. ((((exists wpo_beta_height_wpoi_terminal_source_entry_x. wpo_beta_height_wpoi_terminal_source_entry_x + S (x) = S ((S (q)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_source_entry_x. b = wpo_beta_quotient_wpoi_terminal_source_entry_x * S ((S (q)) * c) + (x))) /\ (exists wpo_gap_wpoi_terminal_source_bound_x. wpo_gap_wpoi_terminal_source_bound_x + S (x) = S (S l)))
  11. 0011specialize hbounded q
  12. 0012apply hbounded
  13. 0013exact hq
  14. 0014cases hbounded_entry
  15. 0015cases hbounded_entry_witness
  16. 0016have hxnonendpoint : ~(x = 0) /\ ~((S x) = S (S l))
  17. 0017specialize hnonendpoint q
  18. 0018specialize hnonendpoint x
  19. 0019apply hnonendpoint
  20. 0020exact hq
  21. 0021exact hbounded_entry_witness_left
  22. 0022cases hxnonendpoint
  23. 0023exists x
  24. 0024split
  25. 0025exact hbounded_entry_witness_left
  26. 0026split
  27. 0027specialize one_le_of_ne_zero x
  28. 0028apply one_le_of_ne_zero
  29. 0029exact hxnonendpoint_left
  30. 0030have hxle_succ : Le(x,S l)
    Exact native replay linehave hxle_succ : exists h. h + x = S l
  31. 0031specialize le_of_succ_le_succ x
  32. 0032specialize le_of_succ_le_succ (S l)
  33. 0033apply le_of_succ_le_succ
  34. 0034exact hbounded_entry_witness_right
  35. 0035have hxsplit : x = S l ∨ Lt(x,S l)
    Exact native replay linehave hxsplit : x = S l \/ exists h. h + S x = S l
  36. 0036specialize le_eq_or_lt x
  37. 0037specialize le_eq_or_lt (S l)
  38. 0038apply le_eq_or_lt
  39. 0039exact hxle_succ
  40. 0040cases hxsplit
  41. 0041exfalso
  42. 0042apply hxnonendpoint_right
  43. 0043rewrite hxsplit_left
  44. 0044refl
  45. 0045specialize le_of_succ_le_succ x
  46. 0046specialize le_of_succ_le_succ l
  47. 0047apply le_of_succ_le_succ
  48. 0048exact hxsplit_right
  49. 0049have hrecode_exists : ∃ rb. ∃ rc. ∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,S y) → BetaAt(rb,rc,x,y)
    Exact native replay linehave hrecode_exists : exists rb rc. (forall gmp_index_wpoi_terminal_recode gmp_predecessor_wpoi_terminal_recode. (exists gsp_lt_gap_wpoi_terminal_recode_index_bound. gsp_lt_gap_wpoi_terminal_recode_index_bound + S gmp_index_wpoi_terminal_recode = l) -> (((exists gsp_beta_height_gmp_wpoi_terminal_recode_source. gsp_beta_height_gmp_wpoi_terminal_recode_source + S (S gmp_predecessor_wpoi_terminal_recode) = S ((S (gmp_index_wpoi_terminal_recode)) * c)) /\ exists gsp_beta_quotient_gmp_wpoi_terminal_recode_source. b = gsp_beta_quotient_gmp_wpoi_terminal_recode_source * S ((S (gmp_index_wpoi_terminal_recode)) * c) + (S gmp_predecessor_wpoi_terminal_recode))) -> (((exists ff_h_gmp_wpoi_terminal_recode_target. ff_h_gmp_wpoi_terminal_recode_target + S (gmp_predecessor_wpoi_terminal_recode) = S ((S (gmp_index_wpoi_terminal_recode)) * rc)) /\ exists ff_q_gmp_wpoi_terminal_recode_target. rb = ff_q_gmp_wpoi_terminal_recode_target * S ((S (gmp_index_wpoi_terminal_recode)) * rc) + (gmp_predecessor_wpoi_terminal_recode))))
  50. 0050specialize beta_magnitude_predecessor_recode_exists b
  51. 0051specialize beta_magnitude_predecessor_recode_exists c
  52. 0052specialize beta_magnitude_predecessor_recode_exists l
  53. 0053specialize beta_magnitude_predecessor_recode_exists l
  54. 0054apply beta_magnitude_predecessor_recode_exists
  55. 0055exact hmagnitude
  56. 0056cases hrecode_exists
  57. 0057cases hrecode_exists_witness
  58. 0058have hrecode : ∀ gmp_index_wpoi_terminal_recode_x. ∀ gmp_predecessor_wpoi_terminal_recode_x. Lt(gmp_index_wpoi_terminal_recode_x,l) → BetaAt(b,c,gmp_index_wpoi_terminal_recode_x,S gmp_predecessor_wpoi_terminal_recode_x) → BetaAt(x,x1,gmp_index_wpoi_terminal_recode_x,gmp_predecessor_wpoi_terminal_recode_x)
    Exact native replay linehave hrecode : forall gmp_index_wpoi_terminal_recode_x gmp_predecessor_wpoi_terminal_recode_x. (exists gsp_lt_gap_wpoi_terminal_recode_x_index_bound. gsp_lt_gap_wpoi_terminal_recode_x_index_bound + S gmp_index_wpoi_terminal_recode_x = l) -> (((exists gsp_beta_height_gmp_wpoi_terminal_recode_x_source. gsp_beta_height_gmp_wpoi_terminal_recode_x_source + S (S gmp_predecessor_wpoi_terminal_recode_x) = S ((S (gmp_index_wpoi_terminal_recode_x)) * c)) /\ exists gsp_beta_quotient_gmp_wpoi_terminal_recode_x_source. b = gsp_beta_quotient_gmp_wpoi_terminal_recode_x_source * S ((S (gmp_index_wpoi_terminal_recode_x)) * c) + (S gmp_predecessor_wpoi_terminal_recode_x))) -> (((exists ff_h_gmp_wpoi_terminal_recode_x_target. ff_h_gmp_wpoi_terminal_recode_x_target + S (gmp_predecessor_wpoi_terminal_recode_x) = S ((S (gmp_index_wpoi_terminal_recode_x)) * x1)) /\ exists ff_q_gmp_wpoi_terminal_recode_x_target. x = ff_q_gmp_wpoi_terminal_recode_x_target * S ((S (gmp_index_wpoi_terminal_recode_x)) * x1) + (gmp_predecessor_wpoi_terminal_recode_x)))
  59. 0059exact hrecode_exists_witness_witness
  60. 0060have hsurjective : SurjectivePrefix(x,x1,l)
    Exact native replay linehave hsurjective : forall fp_value_wpoi_terminal_recode_surjective_x. (exists fp_gap_wpoi_terminal_recode_surjective_x_value. fp_gap_wpoi_terminal_recode_surjective_x_value + S fp_value_wpoi_terminal_recode_surjective_x = l) -> exists fp_i_wpoi_terminal_recode_surjective_x. ((exists fp_gap_wpoi_terminal_recode_surjective_x_index. fp_gap_wpoi_terminal_recode_surjective_x_index + S fp_i_wpoi_terminal_recode_surjective_x = l) /\ (((exists ff_h_wpoi_terminal_recode_surjective_x_entry. ff_h_wpoi_terminal_recode_surjective_x_entry + S (fp_value_wpoi_terminal_recode_surjective_x) = S ((S (fp_i_wpoi_terminal_recode_surjective_x)) * x1)) /\ exists ff_q_wpoi_terminal_recode_surjective_x_entry. x = ff_q_wpoi_terminal_recode_surjective_x_entry * S ((S (fp_i_wpoi_terminal_recode_surjective_x)) * x1) + (fp_value_wpoi_terminal_recode_surjective_x))))
  61. 0061specialize beta_magnitude_predecessor_recode_surjective b
  62. 0062specialize beta_magnitude_predecessor_recode_surjective c
  63. 0063specialize beta_magnitude_predecessor_recode_surjective x
  64. 0064specialize beta_magnitude_predecessor_recode_surjective x1
  65. 0065specialize beta_magnitude_predecessor_recode_surjective l
  66. 0066apply beta_magnitude_predecessor_recode_surjective
  67. 0067exact hmagnitude
  68. 0068exact hinjective
  69. 0069exact hrecode
  70. 0070intro s
  71. 0071intro hsbound
  72. 0072intro hsendpoints
  73. 0073cases hsendpoints
  74. 0074have hspred : exists r. s = S r
  75. 0075specialize nonzero_is_succ s
  76. 0076apply nonzero_is_succ
  77. 0077exact hsendpoints_left
  78. 0078cases hspred
  79. 0079have hsle : Le(s,S l)
    Exact native replay linehave hsle : exists h. h + s = S l
  80. 0080specialize le_of_succ_le_succ s
  81. 0081specialize le_of_succ_le_succ (S l)
  82. 0082apply le_of_succ_le_succ
  83. 0083exact hsbound
  84. 0084rewrite hspred_witness at hsle
  85. 0085have hrle : Le(x2,l)
    Exact native replay linehave hrle : exists h. h + x2 = l
  86. 0086specialize le_of_succ_le_succ x2
  87. 0087specialize le_of_succ_le_succ l
  88. 0088apply le_of_succ_le_succ
  89. 0089exact hsle
  90. 0090have hrsplit : x2 = l ∨ Lt(x2,l)
    Exact native replay linehave hrsplit : x2 = l \/ exists h. h + S x2 = l
  91. 0091specialize le_eq_or_lt x2
  92. 0092specialize le_eq_or_lt l
  93. 0093apply le_eq_or_lt
  94. 0094exact hrle
  95. 0095cases hrsplit
  96. 0096exfalso
  97. 0097apply hsendpoints_right
  98. 0098rewrite hspred_witness
  99. 0099rewrite hrsplit_left
  100. 0100refl
  101. 0101have htarget : ContainsPrefix(x,x1,l,x2)
    Exact native replay linehave htarget : exists q. ((exists wpo_gap_wpoi_terminal_target_occurrence_bound. wpo_gap_wpoi_terminal_target_occurrence_bound + S (q) = l) /\ (((exists wpo_beta_height_wpoi_terminal_target_occurrence_entry. wpo_beta_height_wpoi_terminal_target_occurrence_entry + S (x2) = S ((S (q)) * x1)) /\ exists wpo_beta_quotient_wpoi_terminal_target_occurrence_entry. x = wpo_beta_quotient_wpoi_terminal_target_occurrence_entry * S ((S (q)) * x1) + (x2))))
  102. 0102specialize hsurjective x2
  103. 0103apply hsurjective
  104. 0104exact hrsplit_right
  105. 0105cases htarget
  106. 0106cases htarget_witness
  107. 0107have hsource : BetaAt(b,c,x3,S x2)
    Exact native replay linehave hsource : ((exists wpo_beta_height_wpoi_terminal_source_entry_x2_succ_r. wpo_beta_height_wpoi_terminal_source_entry_x2_succ_r + S (S x2) = S ((S (x3)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_source_entry_x2_succ_r. b = wpo_beta_quotient_wpoi_terminal_source_entry_x2_succ_r * S ((S (x3)) * c) + (S x2))
  108. 0108specialize beta_magnitude_predecessor_recode_reflect b
  109. 0109specialize beta_magnitude_predecessor_recode_reflect c
  110. 0110specialize beta_magnitude_predecessor_recode_reflect x
  111. 0111specialize beta_magnitude_predecessor_recode_reflect x1
  112. 0112specialize beta_magnitude_predecessor_recode_reflect l
  113. 0113specialize beta_magnitude_predecessor_recode_reflect l
  114. 0114specialize beta_magnitude_predecessor_recode_reflect x3
  115. 0115specialize beta_magnitude_predecessor_recode_reflect x2
  116. 0116apply beta_magnitude_predecessor_recode_reflect
  117. 0117exact hmagnitude
  118. 0118exact hrecode
  119. 0119exact htarget_witness_left
  120. 0120exact htarget_witness_right
  121. 0121exists x3
  122. 0122split
  123. 0123exact htarget_witness_left
  124. 0124rewrite hspred_witness
  125. 0125rewrite hspred_witness
  126. 0126exact hsource