PA009S

adjacent_scaled_orbit_history_append

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

Append one adjacent pair while retaining its raw At(i,S j) scaled edge.

Exact expanded PA statement

forall u v b c z d m i j. (forall espi_pair_append_old_history. (exists wpo_gap_append_old_history_pair_bound. wpo_gap_append_old_history_pair_bound + S (espi_pair_append_old_history) = m) -> exists espi_left_append_old_history espi_right_append_old_history. (((((exists wpo_beta_height_append_old_history_left_entry. wpo_beta_height_append_old_history_left_entry + S (espi_left_append_old_history) = S ((S (espi_pair_append_old_history + espi_pair_append_old_history)) * c)) /\ exists wpo_beta_quotient_append_old_history_left_entry. b = wpo_beta_quotient_append_old_history_left_entry * S ((S (espi_pair_append_old_history + espi_pair_append_old_history)) * c) + (espi_left_append_old_history))) /\ (((((exists wpo_beta_height_append_old_history_right_entry. wpo_beta_height_append_old_history_right_entry + S (espi_right_append_old_history) = S ((S (S (espi_pair_append_old_history + espi_pair_append_old_history))) * c)) /\ exists wpo_beta_quotient_append_old_history_right_entry. b = wpo_beta_quotient_append_old_history_right_entry * S ((S (S (espi_pair_append_old_history + espi_pair_append_old_history))) * c) + (espi_right_append_old_history))) /\ (((exists wpo_beta_height_append_old_history_scaled_edge. wpo_beta_height_append_old_history_scaled_edge + S (S espi_right_append_old_history) = S ((S (espi_left_append_old_history)) * v)) /\ exists wpo_beta_quotient_append_old_history_scaled_edge. u = wpo_beta_quotient_append_old_history_scaled_edge * S ((S (espi_left_append_old_history)) * v) + (S espi_right_append_old_history)))))))) -> (((((exists wpo_beta_height_append_trace_first. wpo_beta_height_append_trace_first + S (i) = S ((S (m + m)) * d)) /\ exists wpo_beta_quotient_append_trace_first. z = wpo_beta_quotient_append_trace_first * S ((S (m + m)) * d) + (i))) /\ ((((exists wpo_beta_height_append_trace_second. wpo_beta_height_append_trace_second + S (j) = S ((S (S (m + m))) * d)) /\ exists wpo_beta_quotient_append_trace_second. z = wpo_beta_quotient_append_trace_second * S ((S (S (m + m))) * d) + (j))) /\ (forall wpo_old_index_append_trace wpo_old_value_append_trace. (exists wpo_gap_append_trace_old_bound. wpo_gap_append_trace_old_bound + S (wpo_old_index_append_trace) = m + m) -> (((exists wpo_beta_height_append_trace_old_entry. wpo_beta_height_append_trace_old_entry + S (wpo_old_value_append_trace) = S ((S (wpo_old_index_append_trace)) * c)) /\ exists wpo_beta_quotient_append_trace_old_entry. b = wpo_beta_quotient_append_trace_old_entry * S ((S (wpo_old_index_append_trace)) * c) + (wpo_old_value_append_trace))) -> (((exists wpo_beta_height_append_trace_new_entry. wpo_beta_height_append_trace_new_entry + S (wpo_old_value_append_trace) = S ((S (wpo_old_index_append_trace)) * d)) /\ exists wpo_beta_quotient_append_trace_new_entry. z = wpo_beta_quotient_append_trace_new_entry * S ((S (wpo_old_index_append_trace)) * d) + (wpo_old_value_append_trace))))))) -> (((exists wpo_beta_height_append_forward. wpo_beta_height_append_forward + S (S j) = S ((S (i)) * v)) /\ exists wpo_beta_quotient_append_forward. u = wpo_beta_quotient_append_forward * S ((S (i)) * v) + (S j))) -> (forall espi_pair_append_new_history. (exists wpo_gap_append_new_history_pair_bound. wpo_gap_append_new_history_pair_bound + S (espi_pair_append_new_history) = S m) -> exists espi_left_append_new_history espi_right_append_new_history. (((((exists wpo_beta_height_append_new_history_left_entry. wpo_beta_height_append_new_history_left_entry + S (espi_left_append_new_history) = S ((S (espi_pair_append_new_history + espi_pair_append_new_history)) * d)) /\ exists wpo_beta_quotient_append_new_history_left_entry. z = wpo_beta_quotient_append_new_history_left_entry * S ((S (espi_pair_append_new_history + espi_pair_append_new_history)) * d) + (espi_left_append_new_history))) /\ (((((exists wpo_beta_height_append_new_history_right_entry. wpo_beta_height_append_new_history_right_entry + S (espi_right_append_new_history) = S ((S (S (espi_pair_append_new_history + espi_pair_append_new_history))) * d)) /\ exists wpo_beta_quotient_append_new_history_right_entry. z = wpo_beta_quotient_append_new_history_right_entry * S ((S (S (espi_pair_append_new_history + espi_pair_append_new_history))) * d) + (espi_right_append_new_history))) /\ (((exists wpo_beta_height_append_new_history_scaled_edge. wpo_beta_height_append_new_history_scaled_edge + S (S espi_right_append_new_history) = S ((S (espi_left_append_new_history)) * v)) /\ exists wpo_beta_quotient_append_new_history_scaled_edge. u = wpo_beta_quotient_append_new_history_scaled_edge * S ((S (espi_left_append_new_history)) * v) + (S espi_right_append_new_history))))))))

Structural proof guide

Generated structural guide

Append one adjacent pair while retaining its raw At(i,S j) scaled edge.

Use the direct prerequisites finite_lt_succ_eq_or_lt, pair_index_left_below_double, pair_index_right_below_double as previously established PA formulas.

The proof proceeds by case analysis (7), intermediate claims (6), equality transport (6).

Referenced ingredients

PA003D finite_lt_succ_eq_or_lt PA009Q pair_index_left_below_double PA009R pair_index_right_below_double

Proof neighborhood

Direct dependencies

PA003D finite_lt_succ_eq_or_lt PA009Q pair_index_left_below_double PA009R pair_index_right_below_double

Direct dependents

PA009T scaled_inverse_pair_order_paired_state_step

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro u
  2. 0002intro v
  3. 0003intro b
  4. 0004intro c
  5. 0005intro z
  6. 0006intro d
  7. 0007intro m
  8. 0008intro i
  9. 0009intro j
  10. 0010intro hold
  11. 0011intro htrace
  12. 0012intro hforward
  13. 0013cases htrace
  14. 0014cases htrace_right
  15. 0015intro t
  16. 0016intro ht
  17. 0017have hsplit : t = m \/ exists h. h + S t = m
  18. 0018specialize finite_lt_succ_eq_or_lt m
  19. 0019specialize finite_lt_succ_eq_or_lt t
  20. 0020apply finite_lt_succ_eq_or_lt
  21. 0021exact ht
  22. 0022cases hsplit
  23. 0023have hleft_position : t + t = m + m
  24. 0024rewrite hsplit_left
  25. 0025rewrite hsplit_left
  26. 0026refl
  27. 0027have hright_position : S (t + t) = S (m + m)
  28. 0028congr
  29. 0029exact hleft_position
  30. 0030exists i
  31. 0031exists j
  32. 0032split
  33. 0033rewrite hleft_position
  34. 0034rewrite hleft_position
  35. 0035exact htrace_left
  36. 0036split
  37. 0037rewrite hright_position
  38. 0038rewrite hright_position
  39. 0039exact htrace_right_left
  40. 0040exact hforward
  41. 0041have hold_at : exists oi oj. ((((exists wpo_beta_height_old_history_left. wpo_beta_height_old_history_left + S (oi) = S ((S (t + t)) * c)) /\ exists wpo_beta_quotient_old_history_left. b = wpo_beta_quotient_old_history_left * S ((S (t + t)) * c) + (oi))) /\ (((((exists wpo_beta_height_old_history_right. wpo_beta_height_old_history_right + S (oj) = S ((S (S (t + t))) * c)) /\ exists wpo_beta_quotient_old_history_right. b = wpo_beta_quotient_old_history_right * S ((S (S (t + t))) * c) + (oj))) /\ (((exists wpo_beta_height_old_history_edge. wpo_beta_height_old_history_edge + S (S oj) = S ((S (oi)) * v)) /\ exists wpo_beta_quotient_old_history_edge. u = wpo_beta_quotient_old_history_edge * S ((S (oi)) * v) + (S oj))))))
  42. 0042specialize hold t
  43. 0043apply hold
  44. 0044exact hsplit_right
  45. 0045cases hold_at
  46. 0046cases hold_at_witness
  47. 0047cases hold_at_witness_witness
  48. 0048cases hold_at_witness_witness_right
  49. 0049have hleft_bound : exists h. h + S (t + t) = m + m
  50. 0050specialize pair_index_left_below_double t
  51. 0051specialize pair_index_left_below_double m
  52. 0052apply pair_index_left_below_double
  53. 0053exact hsplit_right
  54. 0054have hright_bound : exists h. h + S (S (t + t)) = m + m
  55. 0055specialize pair_index_right_below_double t
  56. 0056specialize pair_index_right_below_double m
  57. 0057apply pair_index_right_below_double
  58. 0058exact hsplit_right
  59. 0059exists x
  60. 0060exists x1
  61. 0061split
  62. 0062specialize htrace_right_right (t + t)
  63. 0063specialize htrace_right_right x
  64. 0064apply htrace_right_right
  65. 0065exact hleft_bound
  66. 0066exact hold_at_witness_witness_left
  67. 0067split
  68. 0068specialize htrace_right_right (S (t + t))
  69. 0069specialize htrace_right_right x1
  70. 0070apply htrace_right_right
  71. 0071exact hright_bound
  72. 0072exact hold_at_witness_witness_right_left
  73. 0073exact hold_at_witness_witness_right_right