BT008B

beta_sum_trace_functional

Stable · empty-context checked

Two exact prefix-sum traces over one decoded prefix have equal endpoints.

Exact expanded PA statement

forall b c l n u v m w d. (((((exists fs_h_functional_left_start. fs_h_functional_left_start + S (0) = S ((S (0)) * v)) /\ exists fs_q_functional_left_start. u = fs_q_functional_left_start * S ((S (0)) * v) + (0))) /\ ((((exists fs_h_functional_left_terminal. fs_h_functional_left_terminal + S (n) = S ((S (l)) * v)) /\ exists fs_q_functional_left_terminal. u = fs_q_functional_left_terminal * S ((S (l)) * v) + (n))) /\ forall fs_i_functional_left_steps. (exists fs_lt_functional_left_steps_bound. fs_lt_functional_left_steps_bound + S fs_i_functional_left_steps = l) -> exists fs_a_functional_left_steps fs_r_functional_left_steps fs_s_functional_left_steps. ((((exists fs_h_functional_left_steps_summand. fs_h_functional_left_steps_summand + S (fs_a_functional_left_steps) = S ((S (fs_i_functional_left_steps)) * c)) /\ exists fs_q_functional_left_steps_summand. b = fs_q_functional_left_steps_summand * S ((S (fs_i_functional_left_steps)) * c) + (fs_a_functional_left_steps))) /\ ((((exists fs_h_functional_left_steps_partial. fs_h_functional_left_steps_partial + S (fs_r_functional_left_steps) = S ((S (fs_i_functional_left_steps)) * v)) /\ exists fs_q_functional_left_steps_partial. u = fs_q_functional_left_steps_partial * S ((S (fs_i_functional_left_steps)) * v) + (fs_r_functional_left_steps))) /\ ((((exists fs_h_functional_left_steps_successor. fs_h_functional_left_steps_successor + S (fs_s_functional_left_steps) = S ((S (S fs_i_functional_left_steps)) * v)) /\ exists fs_q_functional_left_steps_successor. u = fs_q_functional_left_steps_successor * S ((S (S fs_i_functional_left_steps)) * v) + (fs_s_functional_left_steps))) /\ fs_s_functional_left_steps = fs_r_functional_left_steps + fs_a_functional_left_steps)))))) -> (((((exists fs_h_functional_right_start. fs_h_functional_right_start + S (0) = S ((S (0)) * d)) /\ exists fs_q_functional_right_start. w = fs_q_functional_right_start * S ((S (0)) * d) + (0))) /\ ((((exists fs_h_functional_right_terminal. fs_h_functional_right_terminal + S (m) = S ((S (l)) * d)) /\ exists fs_q_functional_right_terminal. w = fs_q_functional_right_terminal * S ((S (l)) * d) + (m))) /\ forall fs_i_functional_right_steps. (exists fs_lt_functional_right_steps_bound. fs_lt_functional_right_steps_bound + S fs_i_functional_right_steps = l) -> exists fs_a_functional_right_steps fs_r_functional_right_steps fs_s_functional_right_steps. ((((exists fs_h_functional_right_steps_summand. fs_h_functional_right_steps_summand + S (fs_a_functional_right_steps) = S ((S (fs_i_functional_right_steps)) * c)) /\ exists fs_q_functional_right_steps_summand. b = fs_q_functional_right_steps_summand * S ((S (fs_i_functional_right_steps)) * c) + (fs_a_functional_right_steps))) /\ ((((exists fs_h_functional_right_steps_partial. fs_h_functional_right_steps_partial + S (fs_r_functional_right_steps) = S ((S (fs_i_functional_right_steps)) * d)) /\ exists fs_q_functional_right_steps_partial. w = fs_q_functional_right_steps_partial * S ((S (fs_i_functional_right_steps)) * d) + (fs_r_functional_right_steps))) /\ ((((exists fs_h_functional_right_steps_successor. fs_h_functional_right_steps_successor + S (fs_s_functional_right_steps) = S ((S (S fs_i_functional_right_steps)) * d)) /\ exists fs_q_functional_right_steps_successor. w = fs_q_functional_right_steps_successor * S ((S (S fs_i_functional_right_steps)) * d) + (fs_s_functional_right_steps))) /\ fs_s_functional_right_steps = fs_r_functional_right_steps + fs_a_functional_right_steps)))))) -> n = m

Structural proof guide

Two exact prefix-sum traces over one decoded prefix have equal endpoints.

Direct prerequisites: beta_at_unique, le_refl, le_succ, add_congr. The authored body proceeds by structural induction (1), case analysis (20), intermediate claims (11).

Proof neighborhood

Direct dependencies

BT0042 beta_at_unique BT000E le_refl BT0018 le_succ BT000S add_congr

Direct dependents

BT008C beta_sum_functional

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro b
  2. 0002intro c
  3. 0003induction l
  4. 0004intro n
  5. 0005intro u
  6. 0006intro v
  7. 0007intro m
  8. 0008intro w
  9. 0009intro d
  10. 0010intro h1
  11. 0011intro h2
  12. 0012cases h1
  13. 0013cases h1_right
  14. 0014cases h2
  15. 0015cases h2_right
  16. 0016have hn : n = 0
  17. 0017specialize beta_at_unique u
  18. 0018specialize beta_at_unique v
  19. 0019specialize beta_at_unique 0
  20. 0020specialize beta_at_unique n
  21. 0021specialize beta_at_unique 0
  22. 0022apply beta_at_unique
  23. 0023exact h1_right_left
  24. 0024exact h1_left
  25. 0025have hm : m = 0
  26. 0026specialize beta_at_unique w
  27. 0027specialize beta_at_unique d
  28. 0028specialize beta_at_unique 0
  29. 0029specialize beta_at_unique m
  30. 0030specialize beta_at_unique 0
  31. 0031apply beta_at_unique
  32. 0032exact h2_right_left
  33. 0033exact h2_left
  34. 0034trans 0
  35. 0035exact hn
  36. 0036symm
  37. 0037exact hm
  38. 0038intro n
  39. 0039intro u
  40. 0040intro v
  41. 0041intro m
  42. 0042intro w
  43. 0043intro d
  44. 0044intro h1
  45. 0045intro h2
  46. 0046cases h1
  47. 0047cases h1_right
  48. 0048cases h2
  49. 0049cases h2_right
  50. 0050have hstep1 : exists a r s. ((((exists fs_h_functional_step1_factor. fs_h_functional_step1_factor + S (a) = S ((S (l)) * c)) /\ exists fs_q_functional_step1_factor. b = fs_q_functional_step1_factor * S ((S (l)) * c) + (a))) /\ ((((exists fs_h_functional_step1_partial. fs_h_functional_step1_partial + S (r) = S ((S (l)) * v)) /\ exists fs_q_functional_step1_partial. u = fs_q_functional_step1_partial * S ((S (l)) * v) + (r))) /\ ((((exists fs_h_functional_step1_successor. fs_h_functional_step1_successor + S (s) = S ((S (S l)) * v)) /\ exists fs_q_functional_step1_successor. u = fs_q_functional_step1_successor * S ((S (S l)) * v) + (s))) /\ s = r + a)))
  51. 0051specialize h1_right_right l
  52. 0052apply h1_right_right
  53. 0053specialize le_refl (S l)
  54. 0054exact le_refl
  55. 0055cases hstep1
  56. 0056cases hstep1_witness
  57. 0057cases hstep1_witness_witness
  58. 0058cases hstep1_witness_witness_witness
  59. 0059cases hstep1_witness_witness_witness_right
  60. 0060cases hstep1_witness_witness_witness_right_right
  61. 0061have hstep2 : exists a r s. ((((exists fs_h_functional_step2_factor. fs_h_functional_step2_factor + S (a) = S ((S (l)) * c)) /\ exists fs_q_functional_step2_factor. b = fs_q_functional_step2_factor * S ((S (l)) * c) + (a))) /\ ((((exists fs_h_functional_step2_partial. fs_h_functional_step2_partial + S (r) = S ((S (l)) * d)) /\ exists fs_q_functional_step2_partial. w = fs_q_functional_step2_partial * S ((S (l)) * d) + (r))) /\ ((((exists fs_h_functional_step2_successor. fs_h_functional_step2_successor + S (s) = S ((S (S l)) * d)) /\ exists fs_q_functional_step2_successor. w = fs_q_functional_step2_successor * S ((S (S l)) * d) + (s))) /\ s = r + a)))
  62. 0062specialize h2_right_right l
  63. 0063apply h2_right_right
  64. 0064specialize le_refl (S l)
  65. 0065exact le_refl
  66. 0066cases hstep2
  67. 0067cases hstep2_witness
  68. 0068cases hstep2_witness_witness
  69. 0069cases hstep2_witness_witness_witness
  70. 0070cases hstep2_witness_witness_witness_right
  71. 0071cases hstep2_witness_witness_witness_right_right
  72. 0072have hn : n = x2
  73. 0073specialize beta_at_unique u
  74. 0074specialize beta_at_unique v
  75. 0075specialize beta_at_unique (S l)
  76. 0076specialize beta_at_unique n
  77. 0077specialize beta_at_unique x2
  78. 0078apply beta_at_unique
  79. 0079exact h1_right_left
  80. 0080exact hstep1_witness_witness_witness_right_right_left
  81. 0081have hm : m = x5
  82. 0082specialize beta_at_unique w
  83. 0083specialize beta_at_unique d
  84. 0084specialize beta_at_unique (S l)
  85. 0085specialize beta_at_unique m
  86. 0086specialize beta_at_unique x5
  87. 0087apply beta_at_unique
  88. 0088exact h2_right_left
  89. 0089exact hstep2_witness_witness_witness_right_right_left
  90. 0090have ha : x = x3
  91. 0091specialize beta_at_unique b
  92. 0092specialize beta_at_unique c
  93. 0093specialize beta_at_unique l
  94. 0094specialize beta_at_unique x
  95. 0095specialize beta_at_unique x3
  96. 0096apply beta_at_unique
  97. 0097exact hstep1_witness_witness_witness_left
  98. 0098exact hstep2_witness_witness_witness_left
  99. 0099have hsum1 : ((((exists fs_h_functional_prefix1_start. fs_h_functional_prefix1_start + S (0) = S ((S (0)) * v)) /\ exists fs_q_functional_prefix1_start. u = fs_q_functional_prefix1_start * S ((S (0)) * v) + (0))) /\ ((((exists fs_h_functional_prefix1_terminal. fs_h_functional_prefix1_terminal + S (x1) = S ((S (l)) * v)) /\ exists fs_q_functional_prefix1_terminal. u = fs_q_functional_prefix1_terminal * S ((S (l)) * v) + (x1))) /\ forall fs_i_functional_prefix1_steps. (exists fs_lt_functional_prefix1_steps_bound. fs_lt_functional_prefix1_steps_bound + S fs_i_functional_prefix1_steps = l) -> exists fs_a_functional_prefix1_steps fs_r_functional_prefix1_steps fs_s_functional_prefix1_steps. ((((exists fs_h_functional_prefix1_steps_summand. fs_h_functional_prefix1_steps_summand + S (fs_a_functional_prefix1_steps) = S ((S (fs_i_functional_prefix1_steps)) * c)) /\ exists fs_q_functional_prefix1_steps_summand. b = fs_q_functional_prefix1_steps_summand * S ((S (fs_i_functional_prefix1_steps)) * c) + (fs_a_functional_prefix1_steps))) /\ ((((exists fs_h_functional_prefix1_steps_partial. fs_h_functional_prefix1_steps_partial + S (fs_r_functional_prefix1_steps) = S ((S (fs_i_functional_prefix1_steps)) * v)) /\ exists fs_q_functional_prefix1_steps_partial. u = fs_q_functional_prefix1_steps_partial * S ((S (fs_i_functional_prefix1_steps)) * v) + (fs_r_functional_prefix1_steps))) /\ ((((exists fs_h_functional_prefix1_steps_successor. fs_h_functional_prefix1_steps_successor + S (fs_s_functional_prefix1_steps) = S ((S (S fs_i_functional_prefix1_steps)) * v)) /\ exists fs_q_functional_prefix1_steps_successor. u = fs_q_functional_prefix1_steps_successor * S ((S (S fs_i_functional_prefix1_steps)) * v) + (fs_s_functional_prefix1_steps))) /\ fs_s_functional_prefix1_steps = fs_r_functional_prefix1_steps + fs_a_functional_prefix1_steps)))))
  100. 0100split
  101. 0101exact h1_left
  102. 0102split
  103. 0103exact hstep1_witness_witness_witness_right_left
  104. 0104intro i
  105. 0105intro hi
  106. 0106specialize h1_right_right i
  107. 0107apply h1_right_right
  108. 0108specialize le_succ (S i)
  109. 0109specialize le_succ l
  110. 0110apply le_succ
  111. 0111exact hi
  112. 0112have hsum2 : ((((exists fs_h_functional_prefix2_start. fs_h_functional_prefix2_start + S (0) = S ((S (0)) * d)) /\ exists fs_q_functional_prefix2_start. w = fs_q_functional_prefix2_start * S ((S (0)) * d) + (0))) /\ ((((exists fs_h_functional_prefix2_terminal. fs_h_functional_prefix2_terminal + S (x4) = S ((S (l)) * d)) /\ exists fs_q_functional_prefix2_terminal. w = fs_q_functional_prefix2_terminal * S ((S (l)) * d) + (x4))) /\ forall fs_i_functional_prefix2_steps. (exists fs_lt_functional_prefix2_steps_bound. fs_lt_functional_prefix2_steps_bound + S fs_i_functional_prefix2_steps = l) -> exists fs_a_functional_prefix2_steps fs_r_functional_prefix2_steps fs_s_functional_prefix2_steps. ((((exists fs_h_functional_prefix2_steps_summand. fs_h_functional_prefix2_steps_summand + S (fs_a_functional_prefix2_steps) = S ((S (fs_i_functional_prefix2_steps)) * c)) /\ exists fs_q_functional_prefix2_steps_summand. b = fs_q_functional_prefix2_steps_summand * S ((S (fs_i_functional_prefix2_steps)) * c) + (fs_a_functional_prefix2_steps))) /\ ((((exists fs_h_functional_prefix2_steps_partial. fs_h_functional_prefix2_steps_partial + S (fs_r_functional_prefix2_steps) = S ((S (fs_i_functional_prefix2_steps)) * d)) /\ exists fs_q_functional_prefix2_steps_partial. w = fs_q_functional_prefix2_steps_partial * S ((S (fs_i_functional_prefix2_steps)) * d) + (fs_r_functional_prefix2_steps))) /\ ((((exists fs_h_functional_prefix2_steps_successor. fs_h_functional_prefix2_steps_successor + S (fs_s_functional_prefix2_steps) = S ((S (S fs_i_functional_prefix2_steps)) * d)) /\ exists fs_q_functional_prefix2_steps_successor. w = fs_q_functional_prefix2_steps_successor * S ((S (S fs_i_functional_prefix2_steps)) * d) + (fs_s_functional_prefix2_steps))) /\ fs_s_functional_prefix2_steps = fs_r_functional_prefix2_steps + fs_a_functional_prefix2_steps)))))
  113. 0113split
  114. 0114exact h2_left
  115. 0115split
  116. 0116exact hstep2_witness_witness_witness_right_left
  117. 0117intro i
  118. 0118intro hi
  119. 0119specialize h2_right_right i
  120. 0120apply h2_right_right
  121. 0121specialize le_succ (S i)
  122. 0122specialize le_succ l
  123. 0123apply le_succ
  124. 0124exact hi
  125. 0125have hprev : x1 = x4
  126. 0126specialize IH x1
  127. 0127specialize IH u
  128. 0128specialize IH v
  129. 0129specialize IH x4
  130. 0130specialize IH w
  131. 0131specialize IH d
  132. 0132apply IH
  133. 0133exact hsum1
  134. 0134exact hsum2
  135. 0135have hadd : x1 + x = x4 + x3
  136. 0136specialize add_congr x1
  137. 0137specialize add_congr x4
  138. 0138specialize add_congr x
  139. 0139specialize add_congr x3
  140. 0140apply add_congr
  141. 0141exact hprev
  142. 0142exact ha
  143. 0143trans x2
  144. 0144exact hn
  145. 0145trans x1 + x
  146. 0146exact hstep1_witness_witness_witness_right_right_right
  147. 0147trans x4 + x3
  148. 0148exact hadd
  149. 0149trans x5
  150. 0150symm
  151. 0151exact hstep2_witness_witness_witness_right_right_right
  152. 0152symm
  153. 0153exact hm