BT00SE

eisenstein_initial_segment_prefix_extend

Alpha body-checked · checked-use disabled

Append one exact threshold bit while preserving the old prefix.

Exact expanded PA statement

forall q b c l. (forall eis_index_initial_segment_extend_before. (exists eis_lt_gap_initial_segment_extend_before_bound. eis_lt_gap_initial_segment_extend_before_bound + S (eis_index_initial_segment_extend_before) = l) -> exists eis_bit_initial_segment_extend_before. ((((exists ff_h_eis_initial_segment_extend_before_decoded. ff_h_eis_initial_segment_extend_before_decoded + S (eis_bit_initial_segment_extend_before) = S ((S (eis_index_initial_segment_extend_before)) * c)) /\ exists ff_q_eis_initial_segment_extend_before_decoded. b = ff_q_eis_initial_segment_extend_before_decoded * S ((S (eis_index_initial_segment_extend_before)) * c) + (eis_bit_initial_segment_extend_before))) /\ (((eis_bit_initial_segment_extend_before = 1 /\ (exists eis_le_gap_initial_segment_extend_before_choice_inside. eis_le_gap_initial_segment_extend_before_choice_inside + (S eis_index_initial_segment_extend_before) = q)) \/ (eis_bit_initial_segment_extend_before = 0 /\ (exists eis_lt_gap_initial_segment_extend_before_choice_outside. eis_lt_gap_initial_segment_extend_before_choice_outside + S (q) = S eis_index_initial_segment_extend_before)))))) -> (exists bit. (((bit = 1 /\ (exists eis_le_gap_initial_segment_extend_last_inside. eis_le_gap_initial_segment_extend_last_inside + (S l) = q)) \/ (bit = 0 /\ (exists eis_lt_gap_initial_segment_extend_last_outside. eis_lt_gap_initial_segment_extend_last_outside + S (q) = S l))))) -> exists z d. (forall eis_index_initial_segment_extend_after. (exists eis_lt_gap_initial_segment_extend_after_bound. eis_lt_gap_initial_segment_extend_after_bound + S (eis_index_initial_segment_extend_after) = S l) -> exists eis_bit_initial_segment_extend_after. ((((exists ff_h_eis_initial_segment_extend_after_decoded. ff_h_eis_initial_segment_extend_after_decoded + S (eis_bit_initial_segment_extend_after) = S ((S (eis_index_initial_segment_extend_after)) * d)) /\ exists ff_q_eis_initial_segment_extend_after_decoded. z = ff_q_eis_initial_segment_extend_after_decoded * S ((S (eis_index_initial_segment_extend_after)) * d) + (eis_bit_initial_segment_extend_after))) /\ (((eis_bit_initial_segment_extend_after = 1 /\ (exists eis_le_gap_initial_segment_extend_after_choice_inside. eis_le_gap_initial_segment_extend_after_choice_inside + (S eis_index_initial_segment_extend_after) = q)) \/ (eis_bit_initial_segment_extend_after = 0 /\ (exists eis_lt_gap_initial_segment_extend_after_choice_outside. eis_lt_gap_initial_segment_extend_after_choice_outside + S (q) = S eis_index_initial_segment_extend_after))))))

Structural proof guide

Append one exact threshold bit while preserving the old prefix.

Direct prerequisites: beta_prefix_extend, finite_lt_succ_eq_or_lt. The authored body proceeds by case analysis (7), intermediate claims (2), equality transport (4).

Proof neighborhood

Direct dependencies

BT005D beta_prefix_extend BT00AA finite_lt_succ_eq_or_lt

Direct dependents

BT00SF eisenstein_initial_segment_prefix_exists

Formal native tactic body

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

  1. 0001intro q
  2. 0002intro b
  3. 0003intro c
  4. 0004intro l
  5. 0005intro hprefix
  6. 0006intro hchoice
  7. 0007cases hchoice
  8. 0008specialize beta_prefix_extend l
  9. 0009specialize beta_prefix_extend b
  10. 0010specialize beta_prefix_extend c
  11. 0011specialize beta_prefix_extend x
  12. 0012cases beta_prefix_extend
  13. 0013cases beta_prefix_extend_witness
  14. 0014cases beta_prefix_extend_witness_witness
  15. 0015exists x1
  16. 0016exists x2
  17. 0017intro j
  18. 0018intro hj
  19. 0019have hsplit : j = l \/ exists gap. gap + S j = l
  20. 0020specialize finite_lt_succ_eq_or_lt l
  21. 0021specialize finite_lt_succ_eq_or_lt j
  22. 0022apply finite_lt_succ_eq_or_lt
  23. 0023exact hj
  24. 0024cases hsplit
  25. 0025exists x
  26. 0026split
  27. 0027rewrite hsplit_left
  28. 0028rewrite hsplit_left
  29. 0029exact beta_prefix_extend_witness_witness_left
  30. 0030rewrite hsplit_left
  31. 0031rewrite hsplit_left
  32. 0032exact hchoice_witness
  33. 0033have hold : exists oldbit. ((((exists ff_h_initial_segment_old. ff_h_initial_segment_old + S (oldbit) = S ((S (j)) * c)) /\ exists ff_q_initial_segment_old. b = ff_q_initial_segment_old * S ((S (j)) * c) + (oldbit))) /\ (((oldbit = 1 /\ (exists eis_le_gap_initial_segment_extend_old_choice_inside. eis_le_gap_initial_segment_extend_old_choice_inside + (S j) = q)) \/ (oldbit = 0 /\ (exists eis_lt_gap_initial_segment_extend_old_choice_outside. eis_lt_gap_initial_segment_extend_old_choice_outside + S (q) = S j)))))
  34. 0034specialize hprefix j
  35. 0035apply hprefix
  36. 0036exact hsplit_right
  37. 0037cases hold
  38. 0038cases hold_witness
  39. 0039exists x3
  40. 0040split
  41. 0041specialize beta_prefix_extend_witness_witness_right j
  42. 0042specialize beta_prefix_extend_witness_witness_right x3
  43. 0043apply beta_prefix_extend_witness_witness_right
  44. 0044exact hsplit_right
  45. 0045exact hold_witness_left
  46. 0046exact hold_witness_right