PA00CX · theorem

beta_sum_permutation_invariant

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

A bounded injective beta-coded reindexing preserves the exact finite sum.

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

∀ l. ∀ r. ∀ s. ∀ b. ∀ c. ∀ z. ∀ d. ∀ p. ∀ q. BoundedPrefix(r,s,l) → InjectivePrefix(r,s,l) → (∀ x. ∀ y. ∀ n. Lt(x,l) → BetaAt(r,s,x,y) → BetaAt(b,c,y,n) → BetaAt(z,d,x,n)) → Sum(b,c,l,p) → Sum(z,d,l,q) → p = q

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 PD0015 Sum PD0024 BoundedPrefix PD0025 InjectivePrefix

8 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0015 Sum PD0024 BoundedPrefix PD0025 InjectivePrefix PD0026 SurjectivePrefix PD0027 ContainsPrefix

44 occurrences

Exact expanded native-PA statement
forall l r s b c z d p q. (forall fp_i_reindex_bounded. (exists fp_gap_reindex_bounded_index. fp_gap_reindex_bounded_index + S fp_i_reindex_bounded = l) -> exists fp_value_reindex_bounded. ((((exists ff_h_reindex_bounded_entry. ff_h_reindex_bounded_entry + S (fp_value_reindex_bounded) = S ((S (fp_i_reindex_bounded)) * s)) /\ exists ff_q_reindex_bounded_entry. r = ff_q_reindex_bounded_entry * S ((S (fp_i_reindex_bounded)) * s) + (fp_value_reindex_bounded))) /\ (exists fp_gap_reindex_bounded_value. fp_gap_reindex_bounded_value + S fp_value_reindex_bounded = l))) -> (forall fp_i_reindex_injective fp_j_reindex_injective fp_value_reindex_injective. (exists fp_gap_reindex_injective_i. fp_gap_reindex_injective_i + S fp_i_reindex_injective = l) -> (exists fp_gap_reindex_injective_j. fp_gap_reindex_injective_j + S fp_j_reindex_injective = l) -> (((exists ff_h_reindex_injective_left. ff_h_reindex_injective_left + S (fp_value_reindex_injective) = S ((S (fp_i_reindex_injective)) * s)) /\ exists ff_q_reindex_injective_left. r = ff_q_reindex_injective_left * S ((S (fp_i_reindex_injective)) * s) + (fp_value_reindex_injective))) -> (((exists ff_h_reindex_injective_right. ff_h_reindex_injective_right + S (fp_value_reindex_injective) = S ((S (fp_j_reindex_injective)) * s)) /\ exists ff_q_reindex_injective_right. r = ff_q_reindex_injective_right * S ((S (fp_j_reindex_injective)) * s) + (fp_value_reindex_injective))) -> fp_i_reindex_injective = fp_j_reindex_injective) -> (forall fpr_i_reindex_aligned fpr_j_reindex_aligned fpr_x_reindex_aligned. (exists fpr_h_reindex_aligned. fpr_h_reindex_aligned + S fpr_i_reindex_aligned = l) -> (((exists ff_h_reindex_aligned_map. ff_h_reindex_aligned_map + S (fpr_j_reindex_aligned) = S ((S (fpr_i_reindex_aligned)) * s)) /\ exists ff_q_reindex_aligned_map. r = ff_q_reindex_aligned_map * S ((S (fpr_i_reindex_aligned)) * s) + (fpr_j_reindex_aligned))) -> (((exists ff_h_reindex_aligned_source. ff_h_reindex_aligned_source + S (fpr_x_reindex_aligned) = S ((S (fpr_j_reindex_aligned)) * c)) /\ exists ff_q_reindex_aligned_source. b = ff_q_reindex_aligned_source * S ((S (fpr_j_reindex_aligned)) * c) + (fpr_x_reindex_aligned))) -> (((exists ff_h_reindex_aligned_target. ff_h_reindex_aligned_target + S (fpr_x_reindex_aligned) = S ((S (fpr_i_reindex_aligned)) * d)) /\ exists ff_q_reindex_aligned_target. z = ff_q_reindex_aligned_target * S ((S (fpr_i_reindex_aligned)) * d) + (fpr_x_reindex_aligned)))) -> (exists ff_u_reindex_source_product ff_v_reindex_source_product. ((((exists ff_h_reindex_source_product_start. ff_h_reindex_source_product_start + S (0) = S ((S (0)) * ff_v_reindex_source_product)) /\ exists ff_q_reindex_source_product_start. ff_u_reindex_source_product = ff_q_reindex_source_product_start * S ((S (0)) * ff_v_reindex_source_product) + (0))) /\ ((((exists ff_h_reindex_source_product_terminal. ff_h_reindex_source_product_terminal + S (p) = S ((S (l)) * ff_v_reindex_source_product)) /\ exists ff_q_reindex_source_product_terminal. ff_u_reindex_source_product = ff_q_reindex_source_product_terminal * S ((S (l)) * ff_v_reindex_source_product) + (p))) /\ forall ff_i_reindex_source_product. (exists ff_lt_reindex_source_product_bound. ff_lt_reindex_source_product_bound + S ff_i_reindex_source_product = l) -> exists ff_a_reindex_source_product ff_r_reindex_source_product ff_s_reindex_source_product. ((((exists ff_h_reindex_source_product_summand. ff_h_reindex_source_product_summand + S (ff_a_reindex_source_product) = S ((S (ff_i_reindex_source_product)) * c)) /\ exists ff_q_reindex_source_product_summand. b = ff_q_reindex_source_product_summand * S ((S (ff_i_reindex_source_product)) * c) + (ff_a_reindex_source_product))) /\ ((((exists ff_h_reindex_source_product_partial. ff_h_reindex_source_product_partial + S (ff_r_reindex_source_product) = S ((S (ff_i_reindex_source_product)) * ff_v_reindex_source_product)) /\ exists ff_q_reindex_source_product_partial. ff_u_reindex_source_product = ff_q_reindex_source_product_partial * S ((S (ff_i_reindex_source_product)) * ff_v_reindex_source_product) + (ff_r_reindex_source_product))) /\ ((((exists ff_h_reindex_source_product_successor. ff_h_reindex_source_product_successor + S (ff_s_reindex_source_product) = S ((S (S ff_i_reindex_source_product)) * ff_v_reindex_source_product)) /\ exists ff_q_reindex_source_product_successor. ff_u_reindex_source_product = ff_q_reindex_source_product_successor * S ((S (S ff_i_reindex_source_product)) * ff_v_reindex_source_product) + (ff_s_reindex_source_product))) /\ ff_s_reindex_source_product = ff_r_reindex_source_product + ff_a_reindex_source_product)))))) -> (exists ff_u_reindex_target_product ff_v_reindex_target_product. ((((exists ff_h_reindex_target_product_start. ff_h_reindex_target_product_start + S (0) = S ((S (0)) * ff_v_reindex_target_product)) /\ exists ff_q_reindex_target_product_start. ff_u_reindex_target_product = ff_q_reindex_target_product_start * S ((S (0)) * ff_v_reindex_target_product) + (0))) /\ ((((exists ff_h_reindex_target_product_terminal. ff_h_reindex_target_product_terminal + S (q) = S ((S (l)) * ff_v_reindex_target_product)) /\ exists ff_q_reindex_target_product_terminal. ff_u_reindex_target_product = ff_q_reindex_target_product_terminal * S ((S (l)) * ff_v_reindex_target_product) + (q))) /\ forall ff_i_reindex_target_product. (exists ff_lt_reindex_target_product_bound. ff_lt_reindex_target_product_bound + S ff_i_reindex_target_product = l) -> exists ff_a_reindex_target_product ff_r_reindex_target_product ff_s_reindex_target_product. ((((exists ff_h_reindex_target_product_summand. ff_h_reindex_target_product_summand + S (ff_a_reindex_target_product) = S ((S (ff_i_reindex_target_product)) * d)) /\ exists ff_q_reindex_target_product_summand. z = ff_q_reindex_target_product_summand * S ((S (ff_i_reindex_target_product)) * d) + (ff_a_reindex_target_product))) /\ ((((exists ff_h_reindex_target_product_partial. ff_h_reindex_target_product_partial + S (ff_r_reindex_target_product) = S ((S (ff_i_reindex_target_product)) * ff_v_reindex_target_product)) /\ exists ff_q_reindex_target_product_partial. ff_u_reindex_target_product = ff_q_reindex_target_product_partial * S ((S (ff_i_reindex_target_product)) * ff_v_reindex_target_product) + (ff_r_reindex_target_product))) /\ ((((exists ff_h_reindex_target_product_successor. ff_h_reindex_target_product_successor + S (ff_s_reindex_target_product) = S ((S (S ff_i_reindex_target_product)) * ff_v_reindex_target_product)) /\ exists ff_q_reindex_target_product_successor. ff_u_reindex_target_product = ff_q_reindex_target_product_successor * S ((S (S ff_i_reindex_target_product)) * ff_v_reindex_target_product) + (ff_s_reindex_target_product))) /\ ff_s_reindex_target_product = ff_r_reindex_target_product + ff_a_reindex_target_product)))))) -> p = q

Proof neighborhood

Direct theorem prerequisites

PA004W finite_bounded_injective_surjective PA003D finite_lt_succ_eq_or_lt PA004X finite_fixed_last_prefix_bounded PA004Q finite_injective_prefix_succ PA004K beta_prefix_swap_last_from_entries PA004M finite_swap_last_bounded PA004O finite_swap_last_injective PA00CV beta_sum_swap_last_invariant PA0047 beta_sum_zero PA003H beta_sum_exists PA0029 beta_at_exists PA002F beta_at_unique PA0054 beta_reindex_alignment_swap_last PA00CW beta_sum_reindex_fixed_last PA001A le_refl PA002O le_succ

Direct theorem dependents

PA00CY beta_magnitude_sum_permutation_exact

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

379 script commands · 67 reading checkpoints · 30 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 (16)
finite bounded injective surjectivefinite lt succ eq or ltfinite fixed last prefix boundedfinite injective prefix succbeta prefix swap last from entriesfinite swap last boundedfinite swap last injectivebeta sum swap last invariantbeta sum zerobeta sum existsbeta at existsbeta at uniquebeta reindex alignment swap lastbeta sum reindex fixed lastle reflle succ
01Induction on lL1–10

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

  1. L1
    induction l
  2. L2
    intro r
  3. L3
    intro s
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro z
  7. L7
    intro d
  8. L8
    intro p
  9. L9
    intro q
  10. L10
    intro hbounded
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hinjective
  2. L12
    intro haligned
  3. L13
    intro hsource_product
  4. L14
    intro htarget_product
03Establish hpL15–20

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

  1. L15
    have hp : p = 0
  2. L16
    specialize beta_sum_zero b
  3. L17
    specialize beta_sum_zero c
  4. L18
    specialize beta_sum_zero p
  5. L19
    apply beta_sum_zero
  6. L20
    exact hsource_product
04Establish hqL21–30

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

  1. L21
    have hq : q = 0
  2. L22
    specialize beta_sum_zero z
  3. L23
    specialize beta_sum_zero d
  4. L24
    specialize beta_sum_zero q
  5. L25
    apply beta_sum_zero
  6. L26
    exact htarget_product
  7. L27
    trans 0
  8. L28
    exact hp
  9. L29
    symm
  10. L30
    exact hq
05Fix variables and assumptionsL31–40

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

  1. L31
    intro r
  2. L32
    intro s
  3. L33
    intro b
  4. L34
    intro c
  5. L35
    intro z
  6. L36
    intro d
  7. L37
    intro p
  8. L38
    intro q
  9. L39
    intro hbounded
  10. L40
    intro hinjective
06Fix variables and assumptionsL41–43

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

  1. L41
    intro haligned
  2. L42
    intro hsource_product
  3. L43
    intro htarget_product
07Establish hsurjectiveL44–50

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

  1. L44
    have hsurjective : SurjectivePrefix(r,s,S l)Definitions: SurjectivePrefix(r,s,S l)Original native command in the exact edition
  2. L45
    specialize finite_bounded_injective_surjective (S l)
  3. L46
    specialize finite_bounded_injective_surjective r
  4. L47
    specialize finite_bounded_injective_surjective s
  5. L48
    apply finite_bounded_injective_surjective
  6. L49
    exact hbounded
  7. L50
    exact hinjective
08Establish hlast_boundL51–53

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

  1. L51
    have hlast_bound : Lt(l,S l)Definitions: Lt(l,S l)Original native command in the exact edition
  2. L52
    specialize le_refl (S l)
  3. L53
    exact le_refl
09Establish hpreimageL54–57

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

  1. L54
    have hpreimage : ContainsPrefix(r,s,S l,l)Definitions: ContainsPrefix(r,s,S l,l)Original native command in the exact edition
  2. L55
    specialize hsurjective l
  3. L56
    apply hsurjective
  4. L57
    exact hlast_bound
10Separate the logical casesL58–59

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

  1. L58
    cases hpreimage
  2. L59
    cases hpreimage_witness
11Establish hsource_lastL60–64

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

  1. L60
    have hsource_last : ∃ a. BetaAt(b,c,l,a)Definitions: BetaAt(b,c,l,a)Original native command in the exact edition
  2. L61
    specialize beta_at_exists b
  3. L62
    specialize beta_at_exists c
  4. L63
    specialize beta_at_exists l
  5. L64
    exact beta_at_exists
12Separate the logical casesL65–65

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

  1. L65
    cases hsource_last
13Establish htarget_at_preimageL66–73

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

  1. L66
    have htarget_at_preimage : BetaAt(z,d,x,x1)Definitions: BetaAt(z,d,x,x1)Original native command in the exact edition
  2. L67
    specialize haligned x
  3. L68
    specialize haligned l
  4. L69
    specialize haligned x1
  5. L70
    apply haligned
  6. L71
    exact hpreimage_witness_left
  7. L72
    exact hpreimage_witness_right
  8. L73
    exact hsource_last_witness
14Establish hsplitL74–78

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. L74
    have hsplit : x = l ∨ Lt(x,l)Definitions: Lt(x,l)Original native command in the exact edition
  2. L75
    specialize finite_lt_succ_eq_or_lt l
  3. L76
    specialize finite_lt_succ_eq_or_lt x
  4. L77
    apply finite_lt_succ_eq_or_lt
  5. L78
    exact hpreimage_witness_left
15Separate the logical casesL79–79

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

  1. L79
    cases hsplit
16Establish hmap_lastL80–83

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

  1. L80
    have hmap_last : BetaAt(r,s,l,l)Definitions: BetaAt(r,s,l,l)Original native command in the exact edition
  2. L81
    rewrite hsplit_left at hpreimage_witness_right
  3. L82
    rewrite hsplit_left at hpreimage_witness_right
  4. L83
    exact hpreimage_witness_right
17Establish hbounded_prefixL84–91

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

  1. L84
    have hbounded_prefix : BoundedPrefix(r,s,l)Definitions: BoundedPrefix(r,s,l)Original native command in the exact edition
  2. L85
    specialize finite_fixed_last_prefix_bounded r
  3. L86
    specialize finite_fixed_last_prefix_bounded s
  4. L87
    specialize finite_fixed_last_prefix_bounded l
  5. L88
    apply finite_fixed_last_prefix_bounded
  6. L89
    exact hbounded
  7. L90
    exact hinjective
  8. L91
    exact hmap_last
18Establish hinjective_prefixL92–99

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

  1. L92
    have hinjective_prefix : InjectivePrefix(r,s,l)Definitions: InjectivePrefix(r,s,l)Original native command in the exact edition
  2. L93
    specialize finite_injective_prefix_succ r
  3. L94
    specialize finite_injective_prefix_succ s
  4. L95
    specialize finite_injective_prefix_succ l
  5. L96
    specialize finite_injective_prefix_succ (S l)
  6. L97
    apply finite_injective_prefix_succ
  7. L98
    refl
  8. L99
    exact hinjective
19Establish haligned_prefixL100–109

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

  1. L100
    have haligned_prefix : ∀ fpr_i_reindex_aligned_prefix. ∀ fpr_j_reindex_aligned_prefix. ∀ fpr_x_reindex_aligned_prefix. Lt(fpr_i_reindex_aligned_prefix,l) → BetaAt(r,s,fpr_i_reindex_aligned_prefix,fpr_j_reindex_aligned_prefix) → BetaAt(b,c,fpr_j_reindex_aligned_prefix,fpr_x_reindex_aligned_prefix) → BetaAt(z,d,fpr_i_reindex_aligned_prefix,fpr_x_reindex_aligned_prefix)Definitions: Lt(fpr_i_reindex_aligned_prefix,l)BetaAt(r,s,fpr_i_reindex_aligned_prefix,fpr_j_reindex_aligned_prefix)BetaAt(b,c,fpr_j_reindex_aligned_prefix,fpr_x_reindex_aligned_prefix)BetaAt(z,d,fpr_i_reindex_aligned_prefix,fpr_x_reindex_aligned_prefix)Original native command in the exact edition
  2. L101
    intro i
  3. L102
    intro j
  4. L103
    intro a
  5. L104
    intro hi
  6. L105
    intro hmap
  7. L106
    intro hsource
  8. L107
    specialize haligned i
  9. L108
    specialize haligned j
  10. L109
    specialize haligned a
20Use earlier factsL110–116

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

  1. L110
    apply haligned
  2. L111
    specialize le_succ (S i)
  3. L112
    specialize le_succ l
  4. L113
    apply le_succ
  5. L114
    exact hi
  6. L115
    exact hmap
  7. L116
    exact hsource
21Establish hprefix_products_equalL117–126

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

  1. L117
    have hprefix_products_equal : ∀ u. ∀ v. Sum(b,c,l,u) → Sum(z,d,l,v) → u = vDefinitions: Sum(b,c,l,u)Sum(z,d,l,v)Original native command in the exact edition
  2. L118
    intro u
  3. L119
    intro v
  4. L120
    intro hsource_prefix_product
  5. L121
    intro htarget_prefix_product
  6. L122
    specialize IH r
  7. L123
    specialize IH s
  8. L124
    specialize IH b
  9. L125
    specialize IH c
  10. L126
    specialize IH z
22Use earlier factsL127–136

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

  1. L127
    specialize IH d
  2. L128
    specialize IH u
  3. L129
    specialize IH v
  4. L130
    apply IH
  5. L131
    exact hbounded_prefix
  6. L132
    exact hinjective_prefix
  7. L133
    exact haligned_prefix
  8. L134
    exact hsource_prefix_product
  9. L135
    exact htarget_prefix_product
  10. L136
    specialize beta_sum_reindex_fixed_last r
23Use earlier factsL137–146

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

  1. L137
    specialize beta_sum_reindex_fixed_last s
  2. L138
    specialize beta_sum_reindex_fixed_last b
  3. L139
    specialize beta_sum_reindex_fixed_last c
  4. L140
    specialize beta_sum_reindex_fixed_last z
  5. L141
    specialize beta_sum_reindex_fixed_last d
  6. L142
    specialize beta_sum_reindex_fixed_last l
  7. L143
    specialize beta_sum_reindex_fixed_last p
  8. L144
    specialize beta_sum_reindex_fixed_last q
  9. L145
    apply beta_sum_reindex_fixed_last
  10. L146
    exact haligned
24Use earlier factsL147–150

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

  1. L147
    exact hmap_last
  2. L148
    exact hsource_product
  3. L149
    exact htarget_product
  4. L150
    exact hprefix_products_equal
25Establish hmap_last_decodedL151–155

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

  1. L151
    have hmap_last_decoded : ∃ m. BetaAt(r,s,l,m)Definitions: BetaAt(r,s,l,m)Original native command in the exact edition
  2. L152
    specialize beta_at_exists r
  3. L153
    specialize beta_at_exists s
  4. L154
    specialize beta_at_exists l
  5. L155
    exact beta_at_exists
26Separate the logical casesL156–156

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

  1. L156
    cases hmap_last_decoded
27Establish htarget_last_decodedL157–161

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

  1. L157
    have htarget_last_decoded : ∃ w. BetaAt(z,d,l,w)Definitions: BetaAt(z,d,l,w)Original native command in the exact edition
  2. L158
    specialize beta_at_exists z
  3. L159
    specialize beta_at_exists d
  4. L160
    specialize beta_at_exists l
  5. L161
    exact beta_at_exists
28Separate the logical casesL162–162

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

  1. L162
    cases htarget_last_decoded
29Establish hmap_swapL163–172

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. L163
    have hmap_swap : ∃ rm. ∃ sm. BetaAt(rm,sm,x,x2) ∧ (BetaAt(rm,sm,l,l) ∧ (∀ y. ∀ z. Lt(y,S l) → ¬y = x → ¬y = l → BetaAt(r,s,y,z) → BetaAt(rm,sm,y,z)))Definitions: BetaAt(rm,sm,x,x2)BetaAt(rm,sm,l,l)Lt(y,S l)BetaAt(r,s,y,z)BetaAt(rm,sm,y,z)Original native command in the exact edition
  2. L164
    specialize beta_prefix_swap_last_from_entries r
  3. L165
    specialize beta_prefix_swap_last_from_entries s
  4. L166
    specialize beta_prefix_swap_last_from_entries l
  5. L167
    specialize beta_prefix_swap_last_from_entries x
  6. L168
    specialize beta_prefix_swap_last_from_entries l
  7. L169
    specialize beta_prefix_swap_last_from_entries x2
  8. L170
    apply beta_prefix_swap_last_from_entries
  9. L171
    exact hsplit_right
  10. L172
    exact hpreimage_witness_right
30Use earlier factsL173–173

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

  1. L173
    exact hmap_last_decoded_witness
31Separate the logical casesL174–177

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

  1. L174
    cases hmap_swap
  2. L175
    cases hmap_swap_witness
  3. L176
    cases hmap_swap_witness_witness
  4. L177
    cases hmap_swap_witness_witness_right
32Establish htarget_swapL178–187

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. L178
    have htarget_swap : ∃ tz. ∃ td. BetaAt(tz,td,x,x3) ∧ (BetaAt(tz,td,l,x1) ∧ (∀ y. ∀ n. Lt(y,S l) → ¬y = x → ¬y = l → BetaAt(z,d,y,n) → BetaAt(tz,td,y,n)))Definitions: BetaAt(tz,td,x,x3)BetaAt(tz,td,l,x1)Lt(y,S l)BetaAt(z,d,y,n)BetaAt(tz,td,y,n)Original native command in the exact edition
  2. L179
    specialize beta_prefix_swap_last_from_entries z
  3. L180
    specialize beta_prefix_swap_last_from_entries d
  4. L181
    specialize beta_prefix_swap_last_from_entries l
  5. L182
    specialize beta_prefix_swap_last_from_entries x
  6. L183
    specialize beta_prefix_swap_last_from_entries x1
  7. L184
    specialize beta_prefix_swap_last_from_entries x3
  8. L185
    apply beta_prefix_swap_last_from_entries
  9. L186
    exact hsplit_right
  10. L187
    exact htarget_at_preimage
33Use earlier factsL188–188

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

  1. L188
    exact htarget_last_decoded_witness
34Separate the logical casesL189–192

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

  1. L189
    cases htarget_swap
  2. L190
    cases htarget_swap_witness
  3. L191
    cases htarget_swap_witness_witness
  4. L192
    cases htarget_swap_witness_witness_right
35Establish hswapped_boundedL193–202

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

  1. L193
    have hswapped_bounded : BoundedPrefix(x4,x5,S l)Definitions: BoundedPrefix(x4,x5,S l)Original native command in the exact edition
  2. L194
    specialize finite_swap_last_bounded r
  3. L195
    specialize finite_swap_last_bounded s
  4. L196
    specialize finite_swap_last_bounded x4
  5. L197
    specialize finite_swap_last_bounded x5
  6. L198
    specialize finite_swap_last_bounded l
  7. L199
    specialize finite_swap_last_bounded (S l)
  8. L200
    specialize finite_swap_last_bounded x
  9. L201
    specialize finite_swap_last_bounded l
  10. L202
    specialize finite_swap_last_bounded x2
36Use earlier factsL203–203

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

  1. L203
    apply finite_swap_last_bounded
37Calculate and transport equalitiesL204–204

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

  1. L204
    refl
38Use earlier factsL205–211

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

  1. L205
    exact hsplit_right
  2. L206
    exact hbounded
  3. L207
    exact hpreimage_witness_right
  4. L208
    exact hmap_last_decoded_witness
  5. L209
    exact hmap_swap_witness_witness_left
  6. L210
    exact hmap_swap_witness_witness_right_left
  7. L211
    exact hmap_swap_witness_witness_right_right
39Establish hswapped_injectiveL212–221

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

  1. L212
    have hswapped_injective : InjectivePrefix(x4,x5,S l)Definitions: InjectivePrefix(x4,x5,S l)Original native command in the exact edition
  2. L213
    specialize finite_swap_last_injective r
  3. L214
    specialize finite_swap_last_injective s
  4. L215
    specialize finite_swap_last_injective x4
  5. L216
    specialize finite_swap_last_injective x5
  6. L217
    specialize finite_swap_last_injective l
  7. L218
    specialize finite_swap_last_injective (S l)
  8. L219
    specialize finite_swap_last_injective x
  9. L220
    specialize finite_swap_last_injective l
  10. L221
    specialize finite_swap_last_injective x2
40Use earlier factsL222–222

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

  1. L222
    apply finite_swap_last_injective
41Calculate and transport equalitiesL223–223

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

  1. L223
    refl
42Use earlier factsL224–230

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

  1. L224
    exact hsplit_right
  2. L225
    exact hinjective
  3. L226
    exact hpreimage_witness_right
  4. L227
    exact hmap_last_decoded_witness
  5. L228
    exact hmap_swap_witness_witness_left
  6. L229
    exact hmap_swap_witness_witness_right_left
  7. L230
    exact hmap_swap_witness_witness_right_right
43Establish hswapped_target_product_existsL231–235

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

  1. L231
    have hswapped_target_product_exists : ∃ t. Sum(x6,x7,S l,t)Definitions: Sum(x6,x7,S l,t)Original native command in the exact edition
  2. L232
    specialize beta_sum_exists x6
  3. L233
    specialize beta_sum_exists x7
  4. L234
    specialize beta_sum_exists (S l)
  5. L235
    exact beta_sum_exists
44Separate the logical casesL236–236

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

  1. L236
    cases hswapped_target_product_exists
45Establish htarget_product_swapL237–246

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

  1. L237
    have htarget_product_swap : q = x8
  2. L238
    specialize beta_sum_swap_last_invariant z
  3. L239
    specialize beta_sum_swap_last_invariant d
  4. L240
    specialize beta_sum_swap_last_invariant x6
  5. L241
    specialize beta_sum_swap_last_invariant x7
  6. L242
    specialize beta_sum_swap_last_invariant l
  7. L243
    specialize beta_sum_swap_last_invariant x
  8. L244
    specialize beta_sum_swap_last_invariant x1
  9. L245
    specialize beta_sum_swap_last_invariant x3
  10. L246
    specialize beta_sum_swap_last_invariant q
46Use earlier factsL247–256

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

  1. L247
    specialize beta_sum_swap_last_invariant x8
  2. L248
    apply beta_sum_swap_last_invariant
  3. L249
    exact hsplit_right
  4. L250
    exact htarget_at_preimage
  5. L251
    exact htarget_last_decoded_witness
  6. L252
    exact htarget_swap_witness_witness_left
  7. L253
    exact htarget_swap_witness_witness_right_left
  8. L254
    exact htarget_swap_witness_witness_right_right
  9. L255
    exact htarget_product
  10. L256
    exact hswapped_target_product_exists_witness
47Establish hsource_at_map_lastL257–260

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

  1. L257
    have hsource_at_map_last : BetaAt(b,c,x2,x3)Definitions: BetaAt(b,c,x2,x3)Original native command in the exact edition
  2. L258
    specialize beta_at_exists b
  3. L259
    specialize beta_at_exists c
  4. L260
    specialize beta_at_exists x2
48Separate the logical casesL261–261

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

  1. L261
    cases beta_at_exists
49Establish htarget_from_map_lastL262–269

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

  1. L262
    have htarget_from_map_last : BetaAt(z,d,l,x9)Definitions: BetaAt(z,d,l,x9)Original native command in the exact edition
  2. L263
    specialize haligned l
  3. L264
    specialize haligned x2
  4. L265
    specialize haligned x9
  5. L266
    apply haligned
  6. L267
    exact hlast_bound
  7. L268
    exact hmap_last_decoded_witness
  8. L269
    exact beta_at_exists_witness
50Establish hmap_last_valueL270–279

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

  1. L270
    have hmap_last_value : x9 = x3
  2. L271
    specialize beta_at_unique z
  3. L272
    specialize beta_at_unique d
  4. L273
    specialize beta_at_unique l
  5. L274
    specialize beta_at_unique x9
  6. L275
    specialize beta_at_unique x3
  7. L276
    apply beta_at_unique
  8. L277
    exact htarget_from_map_last
  9. L278
    exact htarget_last_decoded_witness
  10. L279
    rewrite hmap_last_value at beta_at_exists_witness
51Calculate and transport equalitiesL280–280

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

  1. L280
    rewrite hmap_last_value at beta_at_exists_witness
52Use earlier factsL281–281

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

  1. L281
    exact beta_at_exists_witness
53Establish hswapped_alignedL282–291

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

  1. L282
    have hswapped_aligned : ∀ fpr_i_reindex_swapped_aligned. ∀ fpr_j_reindex_swapped_aligned. ∀ fpr_x_reindex_swapped_aligned. Lt(fpr_i_reindex_swapped_aligned,S l) → BetaAt(x4,x5,fpr_i_reindex_swapped_aligned,fpr_j_reindex_swapped_aligned) → BetaAt(b,c,fpr_j_reindex_swapped_aligned,fpr_x_reindex_swapped_aligned) → BetaAt(x6,x7,fpr_i_reindex_swapped_aligned,fpr_x_reindex_swapped_aligned)Definitions: Lt(fpr_i_reindex_swapped_aligned,S l)BetaAt(x4,x5,fpr_i_reindex_swapped_aligned,fpr_j_reindex_swapped_aligned)BetaAt(b,c,fpr_j_reindex_swapped_aligned,fpr_x_reindex_swapped_aligned)BetaAt(x6,x7,fpr_i_reindex_swapped_aligned,fpr_x_reindex_swapped_aligned)Original native command in the exact edition
  2. L283
    specialize beta_reindex_alignment_swap_last r
  3. L284
    specialize beta_reindex_alignment_swap_last s
  4. L285
    specialize beta_reindex_alignment_swap_last x4
  5. L286
    specialize beta_reindex_alignment_swap_last x5
  6. L287
    specialize beta_reindex_alignment_swap_last b
  7. L288
    specialize beta_reindex_alignment_swap_last c
  8. L289
    specialize beta_reindex_alignment_swap_last z
  9. L290
    specialize beta_reindex_alignment_swap_last d
  10. L291
    specialize beta_reindex_alignment_swap_last x6
54Use earlier factsL292–301

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

  1. L292
    specialize beta_reindex_alignment_swap_last x7
  2. L293
    specialize beta_reindex_alignment_swap_last l
  3. L294
    specialize beta_reindex_alignment_swap_last x
  4. L295
    specialize beta_reindex_alignment_swap_last x2
  5. L296
    specialize beta_reindex_alignment_swap_last x1
  6. L297
    specialize beta_reindex_alignment_swap_last x3
  7. L298
    apply beta_reindex_alignment_swap_last
  8. L299
    exact hmap_swap_witness_witness_left
  9. L300
    exact hmap_swap_witness_witness_right_left
  10. L301
    exact hmap_swap_witness_witness_right_right
55Use earlier factsL302–307

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

  1. L302
    exact hsource_at_map_last
  2. L303
    exact hsource_last_witness
  3. L304
    exact htarget_swap_witness_witness_left
  4. L305
    exact htarget_swap_witness_witness_right_left
  5. L306
    exact htarget_swap_witness_witness_right_right
  6. L307
    exact haligned
56Establish hswapped_bounded_prefixL308–315

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

  1. L308
    have hswapped_bounded_prefix : BoundedPrefix(x4,x5,l)Definitions: BoundedPrefix(x4,x5,l)Original native command in the exact edition
  2. L309
    specialize finite_fixed_last_prefix_bounded x4
  3. L310
    specialize finite_fixed_last_prefix_bounded x5
  4. L311
    specialize finite_fixed_last_prefix_bounded l
  5. L312
    apply finite_fixed_last_prefix_bounded
  6. L313
    exact hswapped_bounded
  7. L314
    exact hswapped_injective
  8. L315
    exact hmap_swap_witness_witness_right_left
57Establish hswapped_injective_prefixL316–323

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

  1. L316
    have hswapped_injective_prefix : InjectivePrefix(x4,x5,l)Definitions: InjectivePrefix(x4,x5,l)Original native command in the exact edition
  2. L317
    specialize finite_injective_prefix_succ x4
  3. L318
    specialize finite_injective_prefix_succ x5
  4. L319
    specialize finite_injective_prefix_succ l
  5. L320
    specialize finite_injective_prefix_succ (S l)
  6. L321
    apply finite_injective_prefix_succ
  7. L322
    refl
  8. L323
    exact hswapped_injective
58Establish hswapped_aligned_prefixL324–333

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

  1. L324
    have hswapped_aligned_prefix : ∀ fpr_i_reindex_swapped_aligned_prefix. ∀ fpr_j_reindex_swapped_aligned_prefix. ∀ fpr_x_reindex_swapped_aligned_prefix. Lt(fpr_i_reindex_swapped_aligned_prefix,l) → BetaAt(x4,x5,fpr_i_reindex_swapped_aligned_prefix,fpr_j_reindex_swapped_aligned_prefix) → BetaAt(b,c,fpr_j_reindex_swapped_aligned_prefix,fpr_x_reindex_swapped_aligned_prefix) → BetaAt(x6,x7,fpr_i_reindex_swapped_aligned_prefix,fpr_x_reindex_swapped_aligned_prefix)Definitions: Lt(fpr_i_reindex_swapped_aligned_prefix,l)BetaAt(x4,x5,fpr_i_reindex_swapped_aligned_prefix,fpr_j_reindex_swapped_aligned_prefix)BetaAt(b,c,fpr_j_reindex_swapped_aligned_prefix,fpr_x_reindex_swapped_aligned_prefix)BetaAt(x6,x7,fpr_i_reindex_swapped_aligned_prefix,fpr_x_reindex_swapped_aligned_prefix)Original native command in the exact edition
  2. L325
    intro i
  3. L326
    intro j
  4. L327
    intro a
  5. L328
    intro hi
  6. L329
    intro hmap
  7. L330
    intro hsource
  8. L331
    specialize hswapped_aligned i
  9. L332
    specialize hswapped_aligned j
  10. L333
    specialize hswapped_aligned a
59Use earlier factsL334–340

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

  1. L334
    apply hswapped_aligned
  2. L335
    specialize le_succ (S i)
  3. L336
    specialize le_succ l
  4. L337
    apply le_succ
  5. L338
    exact hi
  6. L339
    exact hmap
  7. L340
    exact hsource
60Establish hswapped_prefix_products_equalL341–350

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

  1. L341
    have hswapped_prefix_products_equal : ∀ u. ∀ v. Sum(b,c,l,u) → Sum(x6,x7,l,v) → u = vDefinitions: Sum(b,c,l,u)Sum(x6,x7,l,v)Original native command in the exact edition
  2. L342
    intro u
  3. L343
    intro v
  4. L344
    intro hsource_prefix_product
  5. L345
    intro htarget_prefix_product
  6. L346
    specialize IH x4
  7. L347
    specialize IH x5
  8. L348
    specialize IH b
  9. L349
    specialize IH c
  10. L350
    specialize IH x6
61Use earlier factsL351–359

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

  1. L351
    specialize IH x7
  2. L352
    specialize IH u
  3. L353
    specialize IH v
  4. L354
    apply IH
  5. L355
    exact hswapped_bounded_prefix
  6. L356
    exact hswapped_injective_prefix
  7. L357
    exact hswapped_aligned_prefix
  8. L358
    exact hsource_prefix_product
  9. L359
    exact htarget_prefix_product
62Establish hproduct_swappedL360–369

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

  1. L360
    have hproduct_swapped : p = x8
  2. L361
    specialize beta_sum_reindex_fixed_last x4
  3. L362
    specialize beta_sum_reindex_fixed_last x5
  4. L363
    specialize beta_sum_reindex_fixed_last b
  5. L364
    specialize beta_sum_reindex_fixed_last c
  6. L365
    specialize beta_sum_reindex_fixed_last x6
  7. L366
    specialize beta_sum_reindex_fixed_last x7
  8. L367
    specialize beta_sum_reindex_fixed_last l
  9. L368
    specialize beta_sum_reindex_fixed_last p
  10. L369
    specialize beta_sum_reindex_fixed_last x8
63Use earlier factsL370–375

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

  1. L370
    apply beta_sum_reindex_fixed_last
  2. L371
    exact hswapped_aligned
  3. L372
    exact hmap_swap_witness_witness_right_left
  4. L373
    exact hsource_product
  5. L374
    exact hswapped_target_product_exists_witness
  6. L375
    exact hswapped_prefix_products_equal
64Calculate and transport equalitiesL376–376

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

  1. L376
    trans x8
65Use earlier factsL377–377

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

  1. L377
    exact hproduct_swapped
66Calculate and transport equalitiesL378–378

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

  1. L378
    symm
67Use earlier factsL379–379

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

  1. L379
    exact htarget_product_swap

Library-wide reading audit

Original defined command ledger · 379 lines
  1. 0001induction l
  2. 0002intro r
  3. 0003intro s
  4. 0004intro b
  5. 0005intro c
  6. 0006intro z
  7. 0007intro d
  8. 0008intro p
  9. 0009intro q
  10. 0010intro hbounded
  11. 0011intro hinjective
  12. 0012intro haligned
  13. 0013intro hsource_product
  14. 0014intro htarget_product
  15. 0015have hp : p = 0
  16. 0016specialize beta_sum_zero b
  17. 0017specialize beta_sum_zero c
  18. 0018specialize beta_sum_zero p
  19. 0019apply beta_sum_zero
  20. 0020exact hsource_product
  21. 0021have hq : q = 0
  22. 0022specialize beta_sum_zero z
  23. 0023specialize beta_sum_zero d
  24. 0024specialize beta_sum_zero q
  25. 0025apply beta_sum_zero
  26. 0026exact htarget_product
  27. 0027trans 0
  28. 0028exact hp
  29. 0029symm
  30. 0030exact hq
  31. 0031intro r
  32. 0032intro s
  33. 0033intro b
  34. 0034intro c
  35. 0035intro z
  36. 0036intro d
  37. 0037intro p
  38. 0038intro q
  39. 0039intro hbounded
  40. 0040intro hinjective
  41. 0041intro haligned
  42. 0042intro hsource_product
  43. 0043intro htarget_product
  44. 0044have hsurjective : SurjectivePrefix(r,s,S l)
    Exact native replay linehave hsurjective : forall fp_value_reindex_surjective_succ. (exists fp_gap_reindex_surjective_succ_value. fp_gap_reindex_surjective_succ_value + S fp_value_reindex_surjective_succ = S l) -> exists fp_i_reindex_surjective_succ. ((exists fp_gap_reindex_surjective_succ_index. fp_gap_reindex_surjective_succ_index + S fp_i_reindex_surjective_succ = S l) /\ (((exists ff_h_reindex_surjective_succ_entry. ff_h_reindex_surjective_succ_entry + S (fp_value_reindex_surjective_succ) = S ((S (fp_i_reindex_surjective_succ)) * s)) /\ exists ff_q_reindex_surjective_succ_entry. r = ff_q_reindex_surjective_succ_entry * S ((S (fp_i_reindex_surjective_succ)) * s) + (fp_value_reindex_surjective_succ))))
  45. 0045specialize finite_bounded_injective_surjective (S l)
  46. 0046specialize finite_bounded_injective_surjective r
  47. 0047specialize finite_bounded_injective_surjective s
  48. 0048apply finite_bounded_injective_surjective
  49. 0049exact hbounded
  50. 0050exact hinjective
  51. 0051have hlast_bound : Lt(l,S l)
    Exact native replay linehave hlast_bound : exists h. h + S l = S l
  52. 0052specialize le_refl (S l)
  53. 0053exact le_refl
  54. 0054have hpreimage : ContainsPrefix(r,s,S l,l)
    Exact native replay linehave hpreimage : exists k. ((exists h. h + S k = S l) /\ (((exists ff_h_reindex_map_preimage. ff_h_reindex_map_preimage + S (l) = S ((S (k)) * s)) /\ exists ff_q_reindex_map_preimage. r = ff_q_reindex_map_preimage * S ((S (k)) * s) + (l))))
  55. 0055specialize hsurjective l
  56. 0056apply hsurjective
  57. 0057exact hlast_bound
  58. 0058cases hpreimage
  59. 0059cases hpreimage_witness
  60. 0060have hsource_last : ∃ a. BetaAt(b,c,l,a)
    Exact native replay linehave hsource_last : exists a. (((exists ff_h_reindex_source_last. ff_h_reindex_source_last + S (a) = S ((S (l)) * c)) /\ exists ff_q_reindex_source_last. b = ff_q_reindex_source_last * S ((S (l)) * c) + (a)))
  61. 0061specialize beta_at_exists b
  62. 0062specialize beta_at_exists c
  63. 0063specialize beta_at_exists l
  64. 0064exact beta_at_exists
  65. 0065cases hsource_last
  66. 0066have htarget_at_preimage : BetaAt(z,d,x,x1)
    Exact native replay linehave htarget_at_preimage : ((exists ff_h_reindex_target_preimage. ff_h_reindex_target_preimage + S (x1) = S ((S (x)) * d)) /\ exists ff_q_reindex_target_preimage. z = ff_q_reindex_target_preimage * S ((S (x)) * d) + (x1))
  67. 0067specialize haligned x
  68. 0068specialize haligned l
  69. 0069specialize haligned x1
  70. 0070apply haligned
  71. 0071exact hpreimage_witness_left
  72. 0072exact hpreimage_witness_right
  73. 0073exact hsource_last_witness
  74. 0074have hsplit : x = l ∨ Lt(x,l)
    Exact native replay linehave hsplit : x = l \/ exists h. h + S x = l
  75. 0075specialize finite_lt_succ_eq_or_lt l
  76. 0076specialize finite_lt_succ_eq_or_lt x
  77. 0077apply finite_lt_succ_eq_or_lt
  78. 0078exact hpreimage_witness_left
  79. 0079cases hsplit
  80. 0080have hmap_last : BetaAt(r,s,l,l)
    Exact native replay linehave hmap_last : ((exists ff_h_reindex_map_last. ff_h_reindex_map_last + S (l) = S ((S (l)) * s)) /\ exists ff_q_reindex_map_last. r = ff_q_reindex_map_last * S ((S (l)) * s) + (l))
  81. 0081rewrite hsplit_left at hpreimage_witness_right
  82. 0082rewrite hsplit_left at hpreimage_witness_right
  83. 0083exact hpreimage_witness_right
  84. 0084have hbounded_prefix : BoundedPrefix(r,s,l)
    Exact native replay linehave hbounded_prefix : forall fp_i_reindex_bounded_prefix. (exists fp_gap_reindex_bounded_prefix_index. fp_gap_reindex_bounded_prefix_index + S fp_i_reindex_bounded_prefix = l) -> exists fp_value_reindex_bounded_prefix. ((((exists ff_h_reindex_bounded_prefix_entry. ff_h_reindex_bounded_prefix_entry + S (fp_value_reindex_bounded_prefix) = S ((S (fp_i_reindex_bounded_prefix)) * s)) /\ exists ff_q_reindex_bounded_prefix_entry. r = ff_q_reindex_bounded_prefix_entry * S ((S (fp_i_reindex_bounded_prefix)) * s) + (fp_value_reindex_bounded_prefix))) /\ (exists fp_gap_reindex_bounded_prefix_value. fp_gap_reindex_bounded_prefix_value + S fp_value_reindex_bounded_prefix = l))
  85. 0085specialize finite_fixed_last_prefix_bounded r
  86. 0086specialize finite_fixed_last_prefix_bounded s
  87. 0087specialize finite_fixed_last_prefix_bounded l
  88. 0088apply finite_fixed_last_prefix_bounded
  89. 0089exact hbounded
  90. 0090exact hinjective
  91. 0091exact hmap_last
  92. 0092have hinjective_prefix : InjectivePrefix(r,s,l)
    Exact native replay linehave hinjective_prefix : forall fp_i_reindex_injective_prefix fp_j_reindex_injective_prefix fp_value_reindex_injective_prefix. (exists fp_gap_reindex_injective_prefix_i. fp_gap_reindex_injective_prefix_i + S fp_i_reindex_injective_prefix = l) -> (exists fp_gap_reindex_injective_prefix_j. fp_gap_reindex_injective_prefix_j + S fp_j_reindex_injective_prefix = l) -> (((exists ff_h_reindex_injective_prefix_left. ff_h_reindex_injective_prefix_left + S (fp_value_reindex_injective_prefix) = S ((S (fp_i_reindex_injective_prefix)) * s)) /\ exists ff_q_reindex_injective_prefix_left. r = ff_q_reindex_injective_prefix_left * S ((S (fp_i_reindex_injective_prefix)) * s) + (fp_value_reindex_injective_prefix))) -> (((exists ff_h_reindex_injective_prefix_right. ff_h_reindex_injective_prefix_right + S (fp_value_reindex_injective_prefix) = S ((S (fp_j_reindex_injective_prefix)) * s)) /\ exists ff_q_reindex_injective_prefix_right. r = ff_q_reindex_injective_prefix_right * S ((S (fp_j_reindex_injective_prefix)) * s) + (fp_value_reindex_injective_prefix))) -> fp_i_reindex_injective_prefix = fp_j_reindex_injective_prefix
  93. 0093specialize finite_injective_prefix_succ r
  94. 0094specialize finite_injective_prefix_succ s
  95. 0095specialize finite_injective_prefix_succ l
  96. 0096specialize finite_injective_prefix_succ (S l)
  97. 0097apply finite_injective_prefix_succ
  98. 0098refl
  99. 0099exact hinjective
  100. 0100have haligned_prefix : ∀ fpr_i_reindex_aligned_prefix. ∀ fpr_j_reindex_aligned_prefix. ∀ fpr_x_reindex_aligned_prefix. Lt(fpr_i_reindex_aligned_prefix,l) → BetaAt(r,s,fpr_i_reindex_aligned_prefix,fpr_j_reindex_aligned_prefix) → BetaAt(b,c,fpr_j_reindex_aligned_prefix,fpr_x_reindex_aligned_prefix) → BetaAt(z,d,fpr_i_reindex_aligned_prefix,fpr_x_reindex_aligned_prefix)
    Exact native replay linehave haligned_prefix : forall fpr_i_reindex_aligned_prefix fpr_j_reindex_aligned_prefix fpr_x_reindex_aligned_prefix. (exists fpr_h_reindex_aligned_prefix. fpr_h_reindex_aligned_prefix + S fpr_i_reindex_aligned_prefix = l) -> (((exists ff_h_reindex_aligned_prefix_map. ff_h_reindex_aligned_prefix_map + S (fpr_j_reindex_aligned_prefix) = S ((S (fpr_i_reindex_aligned_prefix)) * s)) /\ exists ff_q_reindex_aligned_prefix_map. r = ff_q_reindex_aligned_prefix_map * S ((S (fpr_i_reindex_aligned_prefix)) * s) + (fpr_j_reindex_aligned_prefix))) -> (((exists ff_h_reindex_aligned_prefix_source. ff_h_reindex_aligned_prefix_source + S (fpr_x_reindex_aligned_prefix) = S ((S (fpr_j_reindex_aligned_prefix)) * c)) /\ exists ff_q_reindex_aligned_prefix_source. b = ff_q_reindex_aligned_prefix_source * S ((S (fpr_j_reindex_aligned_prefix)) * c) + (fpr_x_reindex_aligned_prefix))) -> (((exists ff_h_reindex_aligned_prefix_target. ff_h_reindex_aligned_prefix_target + S (fpr_x_reindex_aligned_prefix) = S ((S (fpr_i_reindex_aligned_prefix)) * d)) /\ exists ff_q_reindex_aligned_prefix_target. z = ff_q_reindex_aligned_prefix_target * S ((S (fpr_i_reindex_aligned_prefix)) * d) + (fpr_x_reindex_aligned_prefix)))
  101. 0101intro i
  102. 0102intro j
  103. 0103intro a
  104. 0104intro hi
  105. 0105intro hmap
  106. 0106intro hsource
  107. 0107specialize haligned i
  108. 0108specialize haligned j
  109. 0109specialize haligned a
  110. 0110apply haligned
  111. 0111specialize le_succ (S i)
  112. 0112specialize le_succ l
  113. 0113apply le_succ
  114. 0114exact hi
  115. 0115exact hmap
  116. 0116exact hsource
  117. 0117have hprefix_products_equal : ∀ u. ∀ v. Sum(b,c,l,u) → Sum(z,d,l,v) → u = v
    Exact native replay linehave hprefix_products_equal : forall u v. (exists ff_u_reindex_source_prefix_product ff_v_reindex_source_prefix_product. ((((exists ff_h_reindex_source_prefix_product_start. ff_h_reindex_source_prefix_product_start + S (0) = S ((S (0)) * ff_v_reindex_source_prefix_product)) /\ exists ff_q_reindex_source_prefix_product_start. ff_u_reindex_source_prefix_product = ff_q_reindex_source_prefix_product_start * S ((S (0)) * ff_v_reindex_source_prefix_product) + (0))) /\ ((((exists ff_h_reindex_source_prefix_product_terminal. ff_h_reindex_source_prefix_product_terminal + S (u) = S ((S (l)) * ff_v_reindex_source_prefix_product)) /\ exists ff_q_reindex_source_prefix_product_terminal. ff_u_reindex_source_prefix_product = ff_q_reindex_source_prefix_product_terminal * S ((S (l)) * ff_v_reindex_source_prefix_product) + (u))) /\ forall ff_i_reindex_source_prefix_product. (exists ff_lt_reindex_source_prefix_product_bound. ff_lt_reindex_source_prefix_product_bound + S ff_i_reindex_source_prefix_product = l) -> exists ff_a_reindex_source_prefix_product ff_r_reindex_source_prefix_product ff_s_reindex_source_prefix_product. ((((exists ff_h_reindex_source_prefix_product_summand. ff_h_reindex_source_prefix_product_summand + S (ff_a_reindex_source_prefix_product) = S ((S (ff_i_reindex_source_prefix_product)) * c)) /\ exists ff_q_reindex_source_prefix_product_summand. b = ff_q_reindex_source_prefix_product_summand * S ((S (ff_i_reindex_source_prefix_product)) * c) + (ff_a_reindex_source_prefix_product))) /\ ((((exists ff_h_reindex_source_prefix_product_partial. ff_h_reindex_source_prefix_product_partial + S (ff_r_reindex_source_prefix_product) = S ((S (ff_i_reindex_source_prefix_product)) * ff_v_reindex_source_prefix_product)) /\ exists ff_q_reindex_source_prefix_product_partial. ff_u_reindex_source_prefix_product = ff_q_reindex_source_prefix_product_partial * S ((S (ff_i_reindex_source_prefix_product)) * ff_v_reindex_source_prefix_product) + (ff_r_reindex_source_prefix_product))) /\ ((((exists ff_h_reindex_source_prefix_product_successor. ff_h_reindex_source_prefix_product_successor + S (ff_s_reindex_source_prefix_product) = S ((S (S ff_i_reindex_source_prefix_product)) * ff_v_reindex_source_prefix_product)) /\ exists ff_q_reindex_source_prefix_product_successor. ff_u_reindex_source_prefix_product = ff_q_reindex_source_prefix_product_successor * S ((S (S ff_i_reindex_source_prefix_product)) * ff_v_reindex_source_prefix_product) + (ff_s_reindex_source_prefix_product))) /\ ff_s_reindex_source_prefix_product = ff_r_reindex_source_prefix_product + ff_a_reindex_source_prefix_product)))))) -> (exists ff_u_reindex_target_prefix_product ff_v_reindex_target_prefix_product. ((((exists ff_h_reindex_target_prefix_product_start. ff_h_reindex_target_prefix_product_start + S (0) = S ((S (0)) * ff_v_reindex_target_prefix_product)) /\ exists ff_q_reindex_target_prefix_product_start. ff_u_reindex_target_prefix_product = ff_q_reindex_target_prefix_product_start * S ((S (0)) * ff_v_reindex_target_prefix_product) + (0))) /\ ((((exists ff_h_reindex_target_prefix_product_terminal. ff_h_reindex_target_prefix_product_terminal + S (v) = S ((S (l)) * ff_v_reindex_target_prefix_product)) /\ exists ff_q_reindex_target_prefix_product_terminal. ff_u_reindex_target_prefix_product = ff_q_reindex_target_prefix_product_terminal * S ((S (l)) * ff_v_reindex_target_prefix_product) + (v))) /\ forall ff_i_reindex_target_prefix_product. (exists ff_lt_reindex_target_prefix_product_bound. ff_lt_reindex_target_prefix_product_bound + S ff_i_reindex_target_prefix_product = l) -> exists ff_a_reindex_target_prefix_product ff_r_reindex_target_prefix_product ff_s_reindex_target_prefix_product. ((((exists ff_h_reindex_target_prefix_product_summand. ff_h_reindex_target_prefix_product_summand + S (ff_a_reindex_target_prefix_product) = S ((S (ff_i_reindex_target_prefix_product)) * d)) /\ exists ff_q_reindex_target_prefix_product_summand. z = ff_q_reindex_target_prefix_product_summand * S ((S (ff_i_reindex_target_prefix_product)) * d) + (ff_a_reindex_target_prefix_product))) /\ ((((exists ff_h_reindex_target_prefix_product_partial. ff_h_reindex_target_prefix_product_partial + S (ff_r_reindex_target_prefix_product) = S ((S (ff_i_reindex_target_prefix_product)) * ff_v_reindex_target_prefix_product)) /\ exists ff_q_reindex_target_prefix_product_partial. ff_u_reindex_target_prefix_product = ff_q_reindex_target_prefix_product_partial * S ((S (ff_i_reindex_target_prefix_product)) * ff_v_reindex_target_prefix_product) + (ff_r_reindex_target_prefix_product))) /\ ((((exists ff_h_reindex_target_prefix_product_successor. ff_h_reindex_target_prefix_product_successor + S (ff_s_reindex_target_prefix_product) = S ((S (S ff_i_reindex_target_prefix_product)) * ff_v_reindex_target_prefix_product)) /\ exists ff_q_reindex_target_prefix_product_successor. ff_u_reindex_target_prefix_product = ff_q_reindex_target_prefix_product_successor * S ((S (S ff_i_reindex_target_prefix_product)) * ff_v_reindex_target_prefix_product) + (ff_s_reindex_target_prefix_product))) /\ ff_s_reindex_target_prefix_product = ff_r_reindex_target_prefix_product + ff_a_reindex_target_prefix_product)))))) -> u = v
  118. 0118intro u
  119. 0119intro v
  120. 0120intro hsource_prefix_product
  121. 0121intro htarget_prefix_product
  122. 0122specialize IH r
  123. 0123specialize IH s
  124. 0124specialize IH b
  125. 0125specialize IH c
  126. 0126specialize IH z
  127. 0127specialize IH d
  128. 0128specialize IH u
  129. 0129specialize IH v
  130. 0130apply IH
  131. 0131exact hbounded_prefix
  132. 0132exact hinjective_prefix
  133. 0133exact haligned_prefix
  134. 0134exact hsource_prefix_product
  135. 0135exact htarget_prefix_product
  136. 0136specialize beta_sum_reindex_fixed_last r
  137. 0137specialize beta_sum_reindex_fixed_last s
  138. 0138specialize beta_sum_reindex_fixed_last b
  139. 0139specialize beta_sum_reindex_fixed_last c
  140. 0140specialize beta_sum_reindex_fixed_last z
  141. 0141specialize beta_sum_reindex_fixed_last d
  142. 0142specialize beta_sum_reindex_fixed_last l
  143. 0143specialize beta_sum_reindex_fixed_last p
  144. 0144specialize beta_sum_reindex_fixed_last q
  145. 0145apply beta_sum_reindex_fixed_last
  146. 0146exact haligned
  147. 0147exact hmap_last
  148. 0148exact hsource_product
  149. 0149exact htarget_product
  150. 0150exact hprefix_products_equal
  151. 0151have hmap_last_decoded : ∃ m. BetaAt(r,s,l,m)
    Exact native replay linehave hmap_last_decoded : exists m. (((exists ff_h_reindex_map_decoded_last. ff_h_reindex_map_decoded_last + S (m) = S ((S (l)) * s)) /\ exists ff_q_reindex_map_decoded_last. r = ff_q_reindex_map_decoded_last * S ((S (l)) * s) + (m)))
  152. 0152specialize beta_at_exists r
  153. 0153specialize beta_at_exists s
  154. 0154specialize beta_at_exists l
  155. 0155exact beta_at_exists
  156. 0156cases hmap_last_decoded
  157. 0157have htarget_last_decoded : ∃ w. BetaAt(z,d,l,w)
    Exact native replay linehave htarget_last_decoded : exists w. (((exists ff_h_reindex_target_decoded_last. ff_h_reindex_target_decoded_last + S (w) = S ((S (l)) * d)) /\ exists ff_q_reindex_target_decoded_last. z = ff_q_reindex_target_decoded_last * S ((S (l)) * d) + (w)))
  158. 0158specialize beta_at_exists z
  159. 0159specialize beta_at_exists d
  160. 0160specialize beta_at_exists l
  161. 0161exact beta_at_exists
  162. 0162cases htarget_last_decoded
  163. 0163have hmap_swap : ∃ rm. ∃ sm. BetaAt(rm,sm,x,x2) ∧ (BetaAt(rm,sm,l,l) ∧ (∀ y. ∀ z. Lt(y,S l) → ¬y = x → ¬y = l → BetaAt(r,s,y,z) → BetaAt(rm,sm,y,z)))
    Exact native replay linehave hmap_swap : exists rm sm. (((exists ff_h_reindex_map_swap_i. ff_h_reindex_map_swap_i + S (x2) = S ((S (x)) * sm)) /\ exists ff_q_reindex_map_swap_i. rm = ff_q_reindex_map_swap_i * S ((S (x)) * sm) + (x2))) /\ ((((exists ff_h_reindex_map_swap_last. ff_h_reindex_map_swap_last + S (l) = S ((S (l)) * sm)) /\ exists ff_q_reindex_map_swap_last. rm = ff_q_reindex_map_swap_last * S ((S (l)) * sm) + (l))) /\ forall j a. (exists h. h + S j = S l) -> ~(j = x) -> ~(j = l) -> (((exists ff_h_reindex_map_swap_old. ff_h_reindex_map_swap_old + S (a) = S ((S (j)) * s)) /\ exists ff_q_reindex_map_swap_old. r = ff_q_reindex_map_swap_old * S ((S (j)) * s) + (a))) -> (((exists ff_h_reindex_map_swap_new. ff_h_reindex_map_swap_new + S (a) = S ((S (j)) * sm)) /\ exists ff_q_reindex_map_swap_new. rm = ff_q_reindex_map_swap_new * S ((S (j)) * sm) + (a))))
  164. 0164specialize beta_prefix_swap_last_from_entries r
  165. 0165specialize beta_prefix_swap_last_from_entries s
  166. 0166specialize beta_prefix_swap_last_from_entries l
  167. 0167specialize beta_prefix_swap_last_from_entries x
  168. 0168specialize beta_prefix_swap_last_from_entries l
  169. 0169specialize beta_prefix_swap_last_from_entries x2
  170. 0170apply beta_prefix_swap_last_from_entries
  171. 0171exact hsplit_right
  172. 0172exact hpreimage_witness_right
  173. 0173exact hmap_last_decoded_witness
  174. 0174cases hmap_swap
  175. 0175cases hmap_swap_witness
  176. 0176cases hmap_swap_witness_witness
  177. 0177cases hmap_swap_witness_witness_right
  178. 0178have htarget_swap : ∃ tz. ∃ td. BetaAt(tz,td,x,x3) ∧ (BetaAt(tz,td,l,x1) ∧ (∀ y. ∀ n. Lt(y,S l) → ¬y = x → ¬y = l → BetaAt(z,d,y,n) → BetaAt(tz,td,y,n)))
    Exact native replay linehave htarget_swap : exists tz td. (((exists ff_h_reindex_target_swap_i. ff_h_reindex_target_swap_i + S (x3) = S ((S (x)) * td)) /\ exists ff_q_reindex_target_swap_i. tz = ff_q_reindex_target_swap_i * S ((S (x)) * td) + (x3))) /\ ((((exists ff_h_reindex_target_swap_last. ff_h_reindex_target_swap_last + S (x1) = S ((S (l)) * td)) /\ exists ff_q_reindex_target_swap_last. tz = ff_q_reindex_target_swap_last * S ((S (l)) * td) + (x1))) /\ forall j a. (exists h. h + S j = S l) -> ~(j = x) -> ~(j = l) -> (((exists ff_h_reindex_target_swap_old. ff_h_reindex_target_swap_old + S (a) = S ((S (j)) * d)) /\ exists ff_q_reindex_target_swap_old. z = ff_q_reindex_target_swap_old * S ((S (j)) * d) + (a))) -> (((exists ff_h_reindex_target_swap_new. ff_h_reindex_target_swap_new + S (a) = S ((S (j)) * td)) /\ exists ff_q_reindex_target_swap_new. tz = ff_q_reindex_target_swap_new * S ((S (j)) * td) + (a))))
  179. 0179specialize beta_prefix_swap_last_from_entries z
  180. 0180specialize beta_prefix_swap_last_from_entries d
  181. 0181specialize beta_prefix_swap_last_from_entries l
  182. 0182specialize beta_prefix_swap_last_from_entries x
  183. 0183specialize beta_prefix_swap_last_from_entries x1
  184. 0184specialize beta_prefix_swap_last_from_entries x3
  185. 0185apply beta_prefix_swap_last_from_entries
  186. 0186exact hsplit_right
  187. 0187exact htarget_at_preimage
  188. 0188exact htarget_last_decoded_witness
  189. 0189cases htarget_swap
  190. 0190cases htarget_swap_witness
  191. 0191cases htarget_swap_witness_witness
  192. 0192cases htarget_swap_witness_witness_right
  193. 0193have hswapped_bounded : BoundedPrefix(x4,x5,S l)
    Exact native replay linehave hswapped_bounded : forall fp_i_reindex_swapped_bounded. (exists fp_gap_reindex_swapped_bounded_index. fp_gap_reindex_swapped_bounded_index + S fp_i_reindex_swapped_bounded = S l) -> exists fp_value_reindex_swapped_bounded. ((((exists ff_h_reindex_swapped_bounded_entry. ff_h_reindex_swapped_bounded_entry + S (fp_value_reindex_swapped_bounded) = S ((S (fp_i_reindex_swapped_bounded)) * x5)) /\ exists ff_q_reindex_swapped_bounded_entry. x4 = ff_q_reindex_swapped_bounded_entry * S ((S (fp_i_reindex_swapped_bounded)) * x5) + (fp_value_reindex_swapped_bounded))) /\ (exists fp_gap_reindex_swapped_bounded_value. fp_gap_reindex_swapped_bounded_value + S fp_value_reindex_swapped_bounded = S l))
  194. 0194specialize finite_swap_last_bounded r
  195. 0195specialize finite_swap_last_bounded s
  196. 0196specialize finite_swap_last_bounded x4
  197. 0197specialize finite_swap_last_bounded x5
  198. 0198specialize finite_swap_last_bounded l
  199. 0199specialize finite_swap_last_bounded (S l)
  200. 0200specialize finite_swap_last_bounded x
  201. 0201specialize finite_swap_last_bounded l
  202. 0202specialize finite_swap_last_bounded x2
  203. 0203apply finite_swap_last_bounded
  204. 0204refl
  205. 0205exact hsplit_right
  206. 0206exact hbounded
  207. 0207exact hpreimage_witness_right
  208. 0208exact hmap_last_decoded_witness
  209. 0209exact hmap_swap_witness_witness_left
  210. 0210exact hmap_swap_witness_witness_right_left
  211. 0211exact hmap_swap_witness_witness_right_right
  212. 0212have hswapped_injective : InjectivePrefix(x4,x5,S l)
    Exact native replay linehave hswapped_injective : forall fp_i_reindex_swapped_injective fp_j_reindex_swapped_injective fp_value_reindex_swapped_injective. (exists fp_gap_reindex_swapped_injective_i. fp_gap_reindex_swapped_injective_i + S fp_i_reindex_swapped_injective = S l) -> (exists fp_gap_reindex_swapped_injective_j. fp_gap_reindex_swapped_injective_j + S fp_j_reindex_swapped_injective = S l) -> (((exists ff_h_reindex_swapped_injective_left. ff_h_reindex_swapped_injective_left + S (fp_value_reindex_swapped_injective) = S ((S (fp_i_reindex_swapped_injective)) * x5)) /\ exists ff_q_reindex_swapped_injective_left. x4 = ff_q_reindex_swapped_injective_left * S ((S (fp_i_reindex_swapped_injective)) * x5) + (fp_value_reindex_swapped_injective))) -> (((exists ff_h_reindex_swapped_injective_right. ff_h_reindex_swapped_injective_right + S (fp_value_reindex_swapped_injective) = S ((S (fp_j_reindex_swapped_injective)) * x5)) /\ exists ff_q_reindex_swapped_injective_right. x4 = ff_q_reindex_swapped_injective_right * S ((S (fp_j_reindex_swapped_injective)) * x5) + (fp_value_reindex_swapped_injective))) -> fp_i_reindex_swapped_injective = fp_j_reindex_swapped_injective
  213. 0213specialize finite_swap_last_injective r
  214. 0214specialize finite_swap_last_injective s
  215. 0215specialize finite_swap_last_injective x4
  216. 0216specialize finite_swap_last_injective x5
  217. 0217specialize finite_swap_last_injective l
  218. 0218specialize finite_swap_last_injective (S l)
  219. 0219specialize finite_swap_last_injective x
  220. 0220specialize finite_swap_last_injective l
  221. 0221specialize finite_swap_last_injective x2
  222. 0222apply finite_swap_last_injective
  223. 0223refl
  224. 0224exact hsplit_right
  225. 0225exact hinjective
  226. 0226exact hpreimage_witness_right
  227. 0227exact hmap_last_decoded_witness
  228. 0228exact hmap_swap_witness_witness_left
  229. 0229exact hmap_swap_witness_witness_right_left
  230. 0230exact hmap_swap_witness_witness_right_right
  231. 0231have hswapped_target_product_exists : ∃ t. Sum(x6,x7,S l,t)
    Exact native replay linehave hswapped_target_product_exists : exists t. (exists ff_u_reindex_swapped_target_exists ff_v_reindex_swapped_target_exists. ((((exists ff_h_reindex_swapped_target_exists_start. ff_h_reindex_swapped_target_exists_start + S (0) = S ((S (0)) * ff_v_reindex_swapped_target_exists)) /\ exists ff_q_reindex_swapped_target_exists_start. ff_u_reindex_swapped_target_exists = ff_q_reindex_swapped_target_exists_start * S ((S (0)) * ff_v_reindex_swapped_target_exists) + (0))) /\ ((((exists ff_h_reindex_swapped_target_exists_terminal. ff_h_reindex_swapped_target_exists_terminal + S (t) = S ((S (S l)) * ff_v_reindex_swapped_target_exists)) /\ exists ff_q_reindex_swapped_target_exists_terminal. ff_u_reindex_swapped_target_exists = ff_q_reindex_swapped_target_exists_terminal * S ((S (S l)) * ff_v_reindex_swapped_target_exists) + (t))) /\ forall ff_i_reindex_swapped_target_exists. (exists ff_lt_reindex_swapped_target_exists_bound. ff_lt_reindex_swapped_target_exists_bound + S ff_i_reindex_swapped_target_exists = S l) -> exists ff_a_reindex_swapped_target_exists ff_r_reindex_swapped_target_exists ff_s_reindex_swapped_target_exists. ((((exists ff_h_reindex_swapped_target_exists_summand. ff_h_reindex_swapped_target_exists_summand + S (ff_a_reindex_swapped_target_exists) = S ((S (ff_i_reindex_swapped_target_exists)) * x7)) /\ exists ff_q_reindex_swapped_target_exists_summand. x6 = ff_q_reindex_swapped_target_exists_summand * S ((S (ff_i_reindex_swapped_target_exists)) * x7) + (ff_a_reindex_swapped_target_exists))) /\ ((((exists ff_h_reindex_swapped_target_exists_partial. ff_h_reindex_swapped_target_exists_partial + S (ff_r_reindex_swapped_target_exists) = S ((S (ff_i_reindex_swapped_target_exists)) * ff_v_reindex_swapped_target_exists)) /\ exists ff_q_reindex_swapped_target_exists_partial. ff_u_reindex_swapped_target_exists = ff_q_reindex_swapped_target_exists_partial * S ((S (ff_i_reindex_swapped_target_exists)) * ff_v_reindex_swapped_target_exists) + (ff_r_reindex_swapped_target_exists))) /\ ((((exists ff_h_reindex_swapped_target_exists_successor. ff_h_reindex_swapped_target_exists_successor + S (ff_s_reindex_swapped_target_exists) = S ((S (S ff_i_reindex_swapped_target_exists)) * ff_v_reindex_swapped_target_exists)) /\ exists ff_q_reindex_swapped_target_exists_successor. ff_u_reindex_swapped_target_exists = ff_q_reindex_swapped_target_exists_successor * S ((S (S ff_i_reindex_swapped_target_exists)) * ff_v_reindex_swapped_target_exists) + (ff_s_reindex_swapped_target_exists))) /\ ff_s_reindex_swapped_target_exists = ff_r_reindex_swapped_target_exists + ff_a_reindex_swapped_target_exists))))))
  232. 0232specialize beta_sum_exists x6
  233. 0233specialize beta_sum_exists x7
  234. 0234specialize beta_sum_exists (S l)
  235. 0235exact beta_sum_exists
  236. 0236cases hswapped_target_product_exists
  237. 0237have htarget_product_swap : q = x8
  238. 0238specialize beta_sum_swap_last_invariant z
  239. 0239specialize beta_sum_swap_last_invariant d
  240. 0240specialize beta_sum_swap_last_invariant x6
  241. 0241specialize beta_sum_swap_last_invariant x7
  242. 0242specialize beta_sum_swap_last_invariant l
  243. 0243specialize beta_sum_swap_last_invariant x
  244. 0244specialize beta_sum_swap_last_invariant x1
  245. 0245specialize beta_sum_swap_last_invariant x3
  246. 0246specialize beta_sum_swap_last_invariant q
  247. 0247specialize beta_sum_swap_last_invariant x8
  248. 0248apply beta_sum_swap_last_invariant
  249. 0249exact hsplit_right
  250. 0250exact htarget_at_preimage
  251. 0251exact htarget_last_decoded_witness
  252. 0252exact htarget_swap_witness_witness_left
  253. 0253exact htarget_swap_witness_witness_right_left
  254. 0254exact htarget_swap_witness_witness_right_right
  255. 0255exact htarget_product
  256. 0256exact hswapped_target_product_exists_witness
  257. 0257have hsource_at_map_last : BetaAt(b,c,x2,x3)
    Exact native replay linehave hsource_at_map_last : ((exists ff_h_reindex_source_at_map_last. ff_h_reindex_source_at_map_last + S (x3) = S ((S (x2)) * c)) /\ exists ff_q_reindex_source_at_map_last. b = ff_q_reindex_source_at_map_last * S ((S (x2)) * c) + (x3))
  258. 0258specialize beta_at_exists b
  259. 0259specialize beta_at_exists c
  260. 0260specialize beta_at_exists x2
  261. 0261cases beta_at_exists
  262. 0262have htarget_from_map_last : BetaAt(z,d,l,x9)
    Exact native replay linehave htarget_from_map_last : ((exists ff_h_reindex_target_from_map_last. ff_h_reindex_target_from_map_last + S (x9) = S ((S (l)) * d)) /\ exists ff_q_reindex_target_from_map_last. z = ff_q_reindex_target_from_map_last * S ((S (l)) * d) + (x9))
  263. 0263specialize haligned l
  264. 0264specialize haligned x2
  265. 0265specialize haligned x9
  266. 0266apply haligned
  267. 0267exact hlast_bound
  268. 0268exact hmap_last_decoded_witness
  269. 0269exact beta_at_exists_witness
  270. 0270have hmap_last_value : x9 = x3
  271. 0271specialize beta_at_unique z
  272. 0272specialize beta_at_unique d
  273. 0273specialize beta_at_unique l
  274. 0274specialize beta_at_unique x9
  275. 0275specialize beta_at_unique x3
  276. 0276apply beta_at_unique
  277. 0277exact htarget_from_map_last
  278. 0278exact htarget_last_decoded_witness
  279. 0279rewrite hmap_last_value at beta_at_exists_witness
  280. 0280rewrite hmap_last_value at beta_at_exists_witness
  281. 0281exact beta_at_exists_witness
  282. 0282have hswapped_aligned : ∀ fpr_i_reindex_swapped_aligned. ∀ fpr_j_reindex_swapped_aligned. ∀ fpr_x_reindex_swapped_aligned. Lt(fpr_i_reindex_swapped_aligned,S l) → BetaAt(x4,x5,fpr_i_reindex_swapped_aligned,fpr_j_reindex_swapped_aligned) → BetaAt(b,c,fpr_j_reindex_swapped_aligned,fpr_x_reindex_swapped_aligned) → BetaAt(x6,x7,fpr_i_reindex_swapped_aligned,fpr_x_reindex_swapped_aligned)
    Exact native replay linehave hswapped_aligned : forall fpr_i_reindex_swapped_aligned fpr_j_reindex_swapped_aligned fpr_x_reindex_swapped_aligned. (exists fpr_h_reindex_swapped_aligned. fpr_h_reindex_swapped_aligned + S fpr_i_reindex_swapped_aligned = S l) -> (((exists ff_h_reindex_swapped_aligned_map. ff_h_reindex_swapped_aligned_map + S (fpr_j_reindex_swapped_aligned) = S ((S (fpr_i_reindex_swapped_aligned)) * x5)) /\ exists ff_q_reindex_swapped_aligned_map. x4 = ff_q_reindex_swapped_aligned_map * S ((S (fpr_i_reindex_swapped_aligned)) * x5) + (fpr_j_reindex_swapped_aligned))) -> (((exists ff_h_reindex_swapped_aligned_source. ff_h_reindex_swapped_aligned_source + S (fpr_x_reindex_swapped_aligned) = S ((S (fpr_j_reindex_swapped_aligned)) * c)) /\ exists ff_q_reindex_swapped_aligned_source. b = ff_q_reindex_swapped_aligned_source * S ((S (fpr_j_reindex_swapped_aligned)) * c) + (fpr_x_reindex_swapped_aligned))) -> (((exists ff_h_reindex_swapped_aligned_target. ff_h_reindex_swapped_aligned_target + S (fpr_x_reindex_swapped_aligned) = S ((S (fpr_i_reindex_swapped_aligned)) * x7)) /\ exists ff_q_reindex_swapped_aligned_target. x6 = ff_q_reindex_swapped_aligned_target * S ((S (fpr_i_reindex_swapped_aligned)) * x7) + (fpr_x_reindex_swapped_aligned)))
  283. 0283specialize beta_reindex_alignment_swap_last r
  284. 0284specialize beta_reindex_alignment_swap_last s
  285. 0285specialize beta_reindex_alignment_swap_last x4
  286. 0286specialize beta_reindex_alignment_swap_last x5
  287. 0287specialize beta_reindex_alignment_swap_last b
  288. 0288specialize beta_reindex_alignment_swap_last c
  289. 0289specialize beta_reindex_alignment_swap_last z
  290. 0290specialize beta_reindex_alignment_swap_last d
  291. 0291specialize beta_reindex_alignment_swap_last x6
  292. 0292specialize beta_reindex_alignment_swap_last x7
  293. 0293specialize beta_reindex_alignment_swap_last l
  294. 0294specialize beta_reindex_alignment_swap_last x
  295. 0295specialize beta_reindex_alignment_swap_last x2
  296. 0296specialize beta_reindex_alignment_swap_last x1
  297. 0297specialize beta_reindex_alignment_swap_last x3
  298. 0298apply beta_reindex_alignment_swap_last
  299. 0299exact hmap_swap_witness_witness_left
  300. 0300exact hmap_swap_witness_witness_right_left
  301. 0301exact hmap_swap_witness_witness_right_right
  302. 0302exact hsource_at_map_last
  303. 0303exact hsource_last_witness
  304. 0304exact htarget_swap_witness_witness_left
  305. 0305exact htarget_swap_witness_witness_right_left
  306. 0306exact htarget_swap_witness_witness_right_right
  307. 0307exact haligned
  308. 0308have hswapped_bounded_prefix : BoundedPrefix(x4,x5,l)
    Exact native replay linehave hswapped_bounded_prefix : forall fp_i_reindex_swapped_bounded_prefix. (exists fp_gap_reindex_swapped_bounded_prefix_index. fp_gap_reindex_swapped_bounded_prefix_index + S fp_i_reindex_swapped_bounded_prefix = l) -> exists fp_value_reindex_swapped_bounded_prefix. ((((exists ff_h_reindex_swapped_bounded_prefix_entry. ff_h_reindex_swapped_bounded_prefix_entry + S (fp_value_reindex_swapped_bounded_prefix) = S ((S (fp_i_reindex_swapped_bounded_prefix)) * x5)) /\ exists ff_q_reindex_swapped_bounded_prefix_entry. x4 = ff_q_reindex_swapped_bounded_prefix_entry * S ((S (fp_i_reindex_swapped_bounded_prefix)) * x5) + (fp_value_reindex_swapped_bounded_prefix))) /\ (exists fp_gap_reindex_swapped_bounded_prefix_value. fp_gap_reindex_swapped_bounded_prefix_value + S fp_value_reindex_swapped_bounded_prefix = l))
  309. 0309specialize finite_fixed_last_prefix_bounded x4
  310. 0310specialize finite_fixed_last_prefix_bounded x5
  311. 0311specialize finite_fixed_last_prefix_bounded l
  312. 0312apply finite_fixed_last_prefix_bounded
  313. 0313exact hswapped_bounded
  314. 0314exact hswapped_injective
  315. 0315exact hmap_swap_witness_witness_right_left
  316. 0316have hswapped_injective_prefix : InjectivePrefix(x4,x5,l)
    Exact native replay linehave hswapped_injective_prefix : forall fp_i_reindex_swapped_injective_prefix fp_j_reindex_swapped_injective_prefix fp_value_reindex_swapped_injective_prefix. (exists fp_gap_reindex_swapped_injective_prefix_i. fp_gap_reindex_swapped_injective_prefix_i + S fp_i_reindex_swapped_injective_prefix = l) -> (exists fp_gap_reindex_swapped_injective_prefix_j. fp_gap_reindex_swapped_injective_prefix_j + S fp_j_reindex_swapped_injective_prefix = l) -> (((exists ff_h_reindex_swapped_injective_prefix_left. ff_h_reindex_swapped_injective_prefix_left + S (fp_value_reindex_swapped_injective_prefix) = S ((S (fp_i_reindex_swapped_injective_prefix)) * x5)) /\ exists ff_q_reindex_swapped_injective_prefix_left. x4 = ff_q_reindex_swapped_injective_prefix_left * S ((S (fp_i_reindex_swapped_injective_prefix)) * x5) + (fp_value_reindex_swapped_injective_prefix))) -> (((exists ff_h_reindex_swapped_injective_prefix_right. ff_h_reindex_swapped_injective_prefix_right + S (fp_value_reindex_swapped_injective_prefix) = S ((S (fp_j_reindex_swapped_injective_prefix)) * x5)) /\ exists ff_q_reindex_swapped_injective_prefix_right. x4 = ff_q_reindex_swapped_injective_prefix_right * S ((S (fp_j_reindex_swapped_injective_prefix)) * x5) + (fp_value_reindex_swapped_injective_prefix))) -> fp_i_reindex_swapped_injective_prefix = fp_j_reindex_swapped_injective_prefix
  317. 0317specialize finite_injective_prefix_succ x4
  318. 0318specialize finite_injective_prefix_succ x5
  319. 0319specialize finite_injective_prefix_succ l
  320. 0320specialize finite_injective_prefix_succ (S l)
  321. 0321apply finite_injective_prefix_succ
  322. 0322refl
  323. 0323exact hswapped_injective
  324. 0324have hswapped_aligned_prefix : ∀ fpr_i_reindex_swapped_aligned_prefix. ∀ fpr_j_reindex_swapped_aligned_prefix. ∀ fpr_x_reindex_swapped_aligned_prefix. Lt(fpr_i_reindex_swapped_aligned_prefix,l) → BetaAt(x4,x5,fpr_i_reindex_swapped_aligned_prefix,fpr_j_reindex_swapped_aligned_prefix) → BetaAt(b,c,fpr_j_reindex_swapped_aligned_prefix,fpr_x_reindex_swapped_aligned_prefix) → BetaAt(x6,x7,fpr_i_reindex_swapped_aligned_prefix,fpr_x_reindex_swapped_aligned_prefix)
    Exact native replay linehave hswapped_aligned_prefix : forall fpr_i_reindex_swapped_aligned_prefix fpr_j_reindex_swapped_aligned_prefix fpr_x_reindex_swapped_aligned_prefix. (exists fpr_h_reindex_swapped_aligned_prefix. fpr_h_reindex_swapped_aligned_prefix + S fpr_i_reindex_swapped_aligned_prefix = l) -> (((exists ff_h_reindex_swapped_aligned_prefix_map. ff_h_reindex_swapped_aligned_prefix_map + S (fpr_j_reindex_swapped_aligned_prefix) = S ((S (fpr_i_reindex_swapped_aligned_prefix)) * x5)) /\ exists ff_q_reindex_swapped_aligned_prefix_map. x4 = ff_q_reindex_swapped_aligned_prefix_map * S ((S (fpr_i_reindex_swapped_aligned_prefix)) * x5) + (fpr_j_reindex_swapped_aligned_prefix))) -> (((exists ff_h_reindex_swapped_aligned_prefix_source. ff_h_reindex_swapped_aligned_prefix_source + S (fpr_x_reindex_swapped_aligned_prefix) = S ((S (fpr_j_reindex_swapped_aligned_prefix)) * c)) /\ exists ff_q_reindex_swapped_aligned_prefix_source. b = ff_q_reindex_swapped_aligned_prefix_source * S ((S (fpr_j_reindex_swapped_aligned_prefix)) * c) + (fpr_x_reindex_swapped_aligned_prefix))) -> (((exists ff_h_reindex_swapped_aligned_prefix_target. ff_h_reindex_swapped_aligned_prefix_target + S (fpr_x_reindex_swapped_aligned_prefix) = S ((S (fpr_i_reindex_swapped_aligned_prefix)) * x7)) /\ exists ff_q_reindex_swapped_aligned_prefix_target. x6 = ff_q_reindex_swapped_aligned_prefix_target * S ((S (fpr_i_reindex_swapped_aligned_prefix)) * x7) + (fpr_x_reindex_swapped_aligned_prefix)))
  325. 0325intro i
  326. 0326intro j
  327. 0327intro a
  328. 0328intro hi
  329. 0329intro hmap
  330. 0330intro hsource
  331. 0331specialize hswapped_aligned i
  332. 0332specialize hswapped_aligned j
  333. 0333specialize hswapped_aligned a
  334. 0334apply hswapped_aligned
  335. 0335specialize le_succ (S i)
  336. 0336specialize le_succ l
  337. 0337apply le_succ
  338. 0338exact hi
  339. 0339exact hmap
  340. 0340exact hsource
  341. 0341have hswapped_prefix_products_equal : ∀ u. ∀ v. Sum(b,c,l,u) → Sum(x6,x7,l,v) → u = v
    Exact native replay linehave hswapped_prefix_products_equal : forall u v. (exists ff_u_reindex_source_prefix_product ff_v_reindex_source_prefix_product. ((((exists ff_h_reindex_source_prefix_product_start. ff_h_reindex_source_prefix_product_start + S (0) = S ((S (0)) * ff_v_reindex_source_prefix_product)) /\ exists ff_q_reindex_source_prefix_product_start. ff_u_reindex_source_prefix_product = ff_q_reindex_source_prefix_product_start * S ((S (0)) * ff_v_reindex_source_prefix_product) + (0))) /\ ((((exists ff_h_reindex_source_prefix_product_terminal. ff_h_reindex_source_prefix_product_terminal + S (u) = S ((S (l)) * ff_v_reindex_source_prefix_product)) /\ exists ff_q_reindex_source_prefix_product_terminal. ff_u_reindex_source_prefix_product = ff_q_reindex_source_prefix_product_terminal * S ((S (l)) * ff_v_reindex_source_prefix_product) + (u))) /\ forall ff_i_reindex_source_prefix_product. (exists ff_lt_reindex_source_prefix_product_bound. ff_lt_reindex_source_prefix_product_bound + S ff_i_reindex_source_prefix_product = l) -> exists ff_a_reindex_source_prefix_product ff_r_reindex_source_prefix_product ff_s_reindex_source_prefix_product. ((((exists ff_h_reindex_source_prefix_product_summand. ff_h_reindex_source_prefix_product_summand + S (ff_a_reindex_source_prefix_product) = S ((S (ff_i_reindex_source_prefix_product)) * c)) /\ exists ff_q_reindex_source_prefix_product_summand. b = ff_q_reindex_source_prefix_product_summand * S ((S (ff_i_reindex_source_prefix_product)) * c) + (ff_a_reindex_source_prefix_product))) /\ ((((exists ff_h_reindex_source_prefix_product_partial. ff_h_reindex_source_prefix_product_partial + S (ff_r_reindex_source_prefix_product) = S ((S (ff_i_reindex_source_prefix_product)) * ff_v_reindex_source_prefix_product)) /\ exists ff_q_reindex_source_prefix_product_partial. ff_u_reindex_source_prefix_product = ff_q_reindex_source_prefix_product_partial * S ((S (ff_i_reindex_source_prefix_product)) * ff_v_reindex_source_prefix_product) + (ff_r_reindex_source_prefix_product))) /\ ((((exists ff_h_reindex_source_prefix_product_successor. ff_h_reindex_source_prefix_product_successor + S (ff_s_reindex_source_prefix_product) = S ((S (S ff_i_reindex_source_prefix_product)) * ff_v_reindex_source_prefix_product)) /\ exists ff_q_reindex_source_prefix_product_successor. ff_u_reindex_source_prefix_product = ff_q_reindex_source_prefix_product_successor * S ((S (S ff_i_reindex_source_prefix_product)) * ff_v_reindex_source_prefix_product) + (ff_s_reindex_source_prefix_product))) /\ ff_s_reindex_source_prefix_product = ff_r_reindex_source_prefix_product + ff_a_reindex_source_prefix_product)))))) -> (exists ff_u_reindex_swapped_target_prefix_product ff_v_reindex_swapped_target_prefix_product. ((((exists ff_h_reindex_swapped_target_prefix_product_start. ff_h_reindex_swapped_target_prefix_product_start + S (0) = S ((S (0)) * ff_v_reindex_swapped_target_prefix_product)) /\ exists ff_q_reindex_swapped_target_prefix_product_start. ff_u_reindex_swapped_target_prefix_product = ff_q_reindex_swapped_target_prefix_product_start * S ((S (0)) * ff_v_reindex_swapped_target_prefix_product) + (0))) /\ ((((exists ff_h_reindex_swapped_target_prefix_product_terminal. ff_h_reindex_swapped_target_prefix_product_terminal + S (v) = S ((S (l)) * ff_v_reindex_swapped_target_prefix_product)) /\ exists ff_q_reindex_swapped_target_prefix_product_terminal. ff_u_reindex_swapped_target_prefix_product = ff_q_reindex_swapped_target_prefix_product_terminal * S ((S (l)) * ff_v_reindex_swapped_target_prefix_product) + (v))) /\ forall ff_i_reindex_swapped_target_prefix_product. (exists ff_lt_reindex_swapped_target_prefix_product_bound. ff_lt_reindex_swapped_target_prefix_product_bound + S ff_i_reindex_swapped_target_prefix_product = l) -> exists ff_a_reindex_swapped_target_prefix_product ff_r_reindex_swapped_target_prefix_product ff_s_reindex_swapped_target_prefix_product. ((((exists ff_h_reindex_swapped_target_prefix_product_summand. ff_h_reindex_swapped_target_prefix_product_summand + S (ff_a_reindex_swapped_target_prefix_product) = S ((S (ff_i_reindex_swapped_target_prefix_product)) * x7)) /\ exists ff_q_reindex_swapped_target_prefix_product_summand. x6 = ff_q_reindex_swapped_target_prefix_product_summand * S ((S (ff_i_reindex_swapped_target_prefix_product)) * x7) + (ff_a_reindex_swapped_target_prefix_product))) /\ ((((exists ff_h_reindex_swapped_target_prefix_product_partial. ff_h_reindex_swapped_target_prefix_product_partial + S (ff_r_reindex_swapped_target_prefix_product) = S ((S (ff_i_reindex_swapped_target_prefix_product)) * ff_v_reindex_swapped_target_prefix_product)) /\ exists ff_q_reindex_swapped_target_prefix_product_partial. ff_u_reindex_swapped_target_prefix_product = ff_q_reindex_swapped_target_prefix_product_partial * S ((S (ff_i_reindex_swapped_target_prefix_product)) * ff_v_reindex_swapped_target_prefix_product) + (ff_r_reindex_swapped_target_prefix_product))) /\ ((((exists ff_h_reindex_swapped_target_prefix_product_successor. ff_h_reindex_swapped_target_prefix_product_successor + S (ff_s_reindex_swapped_target_prefix_product) = S ((S (S ff_i_reindex_swapped_target_prefix_product)) * ff_v_reindex_swapped_target_prefix_product)) /\ exists ff_q_reindex_swapped_target_prefix_product_successor. ff_u_reindex_swapped_target_prefix_product = ff_q_reindex_swapped_target_prefix_product_successor * S ((S (S ff_i_reindex_swapped_target_prefix_product)) * ff_v_reindex_swapped_target_prefix_product) + (ff_s_reindex_swapped_target_prefix_product))) /\ ff_s_reindex_swapped_target_prefix_product = ff_r_reindex_swapped_target_prefix_product + ff_a_reindex_swapped_target_prefix_product)))))) -> u = v
  342. 0342intro u
  343. 0343intro v
  344. 0344intro hsource_prefix_product
  345. 0345intro htarget_prefix_product
  346. 0346specialize IH x4
  347. 0347specialize IH x5
  348. 0348specialize IH b
  349. 0349specialize IH c
  350. 0350specialize IH x6
  351. 0351specialize IH x7
  352. 0352specialize IH u
  353. 0353specialize IH v
  354. 0354apply IH
  355. 0355exact hswapped_bounded_prefix
  356. 0356exact hswapped_injective_prefix
  357. 0357exact hswapped_aligned_prefix
  358. 0358exact hsource_prefix_product
  359. 0359exact htarget_prefix_product
  360. 0360have hproduct_swapped : p = x8
  361. 0361specialize beta_sum_reindex_fixed_last x4
  362. 0362specialize beta_sum_reindex_fixed_last x5
  363. 0363specialize beta_sum_reindex_fixed_last b
  364. 0364specialize beta_sum_reindex_fixed_last c
  365. 0365specialize beta_sum_reindex_fixed_last x6
  366. 0366specialize beta_sum_reindex_fixed_last x7
  367. 0367specialize beta_sum_reindex_fixed_last l
  368. 0368specialize beta_sum_reindex_fixed_last p
  369. 0369specialize beta_sum_reindex_fixed_last x8
  370. 0370apply beta_sum_reindex_fixed_last
  371. 0371exact hswapped_aligned
  372. 0372exact hmap_swap_witness_witness_right_left
  373. 0373exact hsource_product
  374. 0374exact hswapped_target_product_exists_witness
  375. 0375exact hswapped_prefix_products_equal
  376. 0376trans x8
  377. 0377exact hproduct_swapped
  378. 0378symm
  379. 0379exact htarget_product_swap