BT00TG

choose_self

Alpha body-checked · checked-use disabled

The recurrence-defined diagonal binomial coefficient is one.

Exact expanded PA statement

forall n z. (((exists bcf_lt_gap_bcs_choose_out_of_range. bcf_lt_gap_bcs_choose_out_of_range + S (n) = n) /\ z = 0) \/ ((exists bcf_le_gap_bcs_choose_in_range. bcf_le_gap_bcs_choose_in_range + (n) = n) /\ (exists bcf_row_code_code_bcs_choose bcf_row_code_scale_bcs_choose bcf_row_scale_code_bcs_choose bcf_row_scale_scale_bcs_choose bcf_row_code_bcs_choose bcf_row_scale_bcs_choose. ((forall bcf_row_index_bcs_choose_table. (exists bcf_lt_gap_bcs_choose_table_row_bound. bcf_lt_gap_bcs_choose_table_row_bound + S (bcf_row_index_bcs_choose_table) = S (n)) -> exists bcf_row_code_bcs_choose_table bcf_row_scale_bcs_choose_table. ((((exists bcf_height_bcs_choose_table_decoded_row_code. bcf_height_bcs_choose_table_decoded_row_code + S (bcf_row_code_bcs_choose_table) = S ((S (bcf_row_index_bcs_choose_table)) * bcf_row_code_scale_bcs_choose)) /\ exists bcf_quotient_bcs_choose_table_decoded_row_code. bcf_row_code_code_bcs_choose = bcf_quotient_bcs_choose_table_decoded_row_code * S ((S (bcf_row_index_bcs_choose_table)) * bcf_row_code_scale_bcs_choose) + (bcf_row_code_bcs_choose_table))) /\ ((((exists bcf_height_bcs_choose_table_decoded_row_scale. bcf_height_bcs_choose_table_decoded_row_scale + S (bcf_row_scale_bcs_choose_table) = S ((S (bcf_row_index_bcs_choose_table)) * bcf_row_scale_scale_bcs_choose)) /\ exists bcf_quotient_bcs_choose_table_decoded_row_scale. bcf_row_scale_code_bcs_choose = bcf_quotient_bcs_choose_table_decoded_row_scale * S ((S (bcf_row_index_bcs_choose_table)) * bcf_row_scale_scale_bcs_choose) + (bcf_row_scale_bcs_choose_table))) /\ ((bcf_row_index_bcs_choose_table = 0 /\ (forall bcf_index_bcs_choose_table_zero_row. (exists bcf_lt_gap_bcs_choose_table_zero_row_bound. bcf_lt_gap_bcs_choose_table_zero_row_bound + S (bcf_index_bcs_choose_table_zero_row) = S (n)) -> exists bcf_value_bcs_choose_table_zero_row. ((((exists bcf_height_bcs_choose_table_zero_row_entry. bcf_height_bcs_choose_table_zero_row_entry + S (bcf_value_bcs_choose_table_zero_row) = S ((S (bcf_index_bcs_choose_table_zero_row)) * bcf_row_scale_bcs_choose_table)) /\ exists bcf_quotient_bcs_choose_table_zero_row_entry. bcf_row_code_bcs_choose_table = bcf_quotient_bcs_choose_table_zero_row_entry * S ((S (bcf_index_bcs_choose_table_zero_row)) * bcf_row_scale_bcs_choose_table) + (bcf_value_bcs_choose_table_zero_row))) /\ ((bcf_index_bcs_choose_table_zero_row = 0 /\ bcf_value_bcs_choose_table_zero_row = 1) \/ exists bcf_predecessor_bcs_choose_table_zero_row. bcf_index_bcs_choose_table_zero_row = S bcf_predecessor_bcs_choose_table_zero_row /\ bcf_value_bcs_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_bcs_choose_table bcf_previous_code_bcs_choose_table bcf_previous_scale_bcs_choose_table. bcf_row_index_bcs_choose_table = S bcf_predecessor_bcs_choose_table /\ ((((exists bcf_height_bcs_choose_table_decoded_previous_code. bcf_height_bcs_choose_table_decoded_previous_code + S (bcf_previous_code_bcs_choose_table) = S ((S (bcf_predecessor_bcs_choose_table)) * bcf_row_code_scale_bcs_choose)) /\ exists bcf_quotient_bcs_choose_table_decoded_previous_code. bcf_row_code_code_bcs_choose = bcf_quotient_bcs_choose_table_decoded_previous_code * S ((S (bcf_predecessor_bcs_choose_table)) * bcf_row_code_scale_bcs_choose) + (bcf_previous_code_bcs_choose_table))) /\ ((((exists bcf_height_bcs_choose_table_decoded_previous_scale. bcf_height_bcs_choose_table_decoded_previous_scale + S (bcf_previous_scale_bcs_choose_table) = S ((S (bcf_predecessor_bcs_choose_table)) * bcf_row_scale_scale_bcs_choose)) /\ exists bcf_quotient_bcs_choose_table_decoded_previous_scale. bcf_row_scale_code_bcs_choose = bcf_quotient_bcs_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_bcs_choose_table)) * bcf_row_scale_scale_bcs_choose) + (bcf_previous_scale_bcs_choose_table))) /\ (forall bcf_index_bcs_choose_table_row_step. (exists bcf_lt_gap_bcs_choose_table_row_step_bound. bcf_lt_gap_bcs_choose_table_row_step_bound + S (bcf_index_bcs_choose_table_row_step) = S (n)) -> exists bcf_value_bcs_choose_table_row_step. ((((exists bcf_height_bcs_choose_table_row_step_entry. bcf_height_bcs_choose_table_row_step_entry + S (bcf_value_bcs_choose_table_row_step) = S ((S (bcf_index_bcs_choose_table_row_step)) * bcf_row_scale_bcs_choose_table)) /\ exists bcf_quotient_bcs_choose_table_row_step_entry. bcf_row_code_bcs_choose_table = bcf_quotient_bcs_choose_table_row_step_entry * S ((S (bcf_index_bcs_choose_table_row_step)) * bcf_row_scale_bcs_choose_table) + (bcf_value_bcs_choose_table_row_step))) /\ ((bcf_index_bcs_choose_table_row_step = 0 /\ bcf_value_bcs_choose_table_row_step = 1) \/ exists bcf_predecessor_bcs_choose_table_row_step bcf_left_bcs_choose_table_row_step bcf_right_bcs_choose_table_row_step. bcf_index_bcs_choose_table_row_step = S bcf_predecessor_bcs_choose_table_row_step /\ ((((exists bcf_height_bcs_choose_table_row_step_previous_left. bcf_height_bcs_choose_table_row_step_previous_left + S (bcf_left_bcs_choose_table_row_step) = S ((S (bcf_predecessor_bcs_choose_table_row_step)) * bcf_previous_scale_bcs_choose_table)) /\ exists bcf_quotient_bcs_choose_table_row_step_previous_left. bcf_previous_code_bcs_choose_table = bcf_quotient_bcs_choose_table_row_step_previous_left * S ((S (bcf_predecessor_bcs_choose_table_row_step)) * bcf_previous_scale_bcs_choose_table) + (bcf_left_bcs_choose_table_row_step))) /\ ((((exists bcf_height_bcs_choose_table_row_step_previous_right. bcf_height_bcs_choose_table_row_step_previous_right + S (bcf_right_bcs_choose_table_row_step) = S ((S (S (bcf_predecessor_bcs_choose_table_row_step))) * bcf_previous_scale_bcs_choose_table)) /\ exists bcf_quotient_bcs_choose_table_row_step_previous_right. bcf_previous_code_bcs_choose_table = bcf_quotient_bcs_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcs_choose_table_row_step))) * bcf_previous_scale_bcs_choose_table) + (bcf_right_bcs_choose_table_row_step))) /\ bcf_value_bcs_choose_table_row_step = bcf_left_bcs_choose_table_row_step + bcf_right_bcs_choose_table_row_step))))))))))) /\ ((((exists bcf_height_bcs_choose_decoded_row_code. bcf_height_bcs_choose_decoded_row_code + S (bcf_row_code_bcs_choose) = S ((S (n)) * bcf_row_code_scale_bcs_choose)) /\ exists bcf_quotient_bcs_choose_decoded_row_code. bcf_row_code_code_bcs_choose = bcf_quotient_bcs_choose_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcs_choose) + (bcf_row_code_bcs_choose))) /\ ((((exists bcf_height_bcs_choose_decoded_row_scale. bcf_height_bcs_choose_decoded_row_scale + S (bcf_row_scale_bcs_choose) = S ((S (n)) * bcf_row_scale_scale_bcs_choose)) /\ exists bcf_quotient_bcs_choose_decoded_row_scale. bcf_row_scale_code_bcs_choose = bcf_quotient_bcs_choose_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcs_choose) + (bcf_row_scale_bcs_choose))) /\ (((exists bcf_height_bcs_choose_decoded_value. bcf_height_bcs_choose_decoded_value + S (z) = S ((S (n)) * bcf_row_scale_bcs_choose)) /\ exists bcf_quotient_bcs_choose_decoded_value. bcf_row_code_bcs_choose = bcf_quotient_bcs_choose_decoded_value * S ((S (n)) * bcf_row_scale_bcs_choose) + (z))))))))) -> z = 1

Structural proof guide

The recurrence-defined diagonal binomial coefficient is one.

Direct prerequisites: lt_irrefl_expanded, le_refl, beta_pascal_table_diagonal_boundary. The authored body proceeds by case analysis (13), intermediate claims (5).

Proof neighborhood

Direct dependencies

BT001B lt_irrefl_expanded BT000E le_refl BT00TF beta_pascal_table_diagonal_boundary

Direct dependents

BT00TJ choose_succ_succ BT00TK choose_self_of_eq

Formal native tactic body

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

  1. 0001intro n
  2. 0002intro z
  3. 0003intro hchoose
  4. 0004cases hchoose
  5. 0005cases hchoose_left
  6. 0006exfalso
  7. 0007specialize lt_irrefl_expanded n
  8. 0008apply lt_irrefl_expanded
  9. 0009exact hchoose_left_left
  10. 0010cases hchoose_right
  11. 0011cases hchoose_right_right
  12. 0012cases hchoose_right_right_witness
  13. 0013cases hchoose_right_right_witness_witness
  14. 0014cases hchoose_right_right_witness_witness_witness
  15. 0015cases hchoose_right_right_witness_witness_witness_witness
  16. 0016cases hchoose_right_right_witness_witness_witness_witness_witness
  17. 0017cases hchoose_right_right_witness_witness_witness_witness_witness_witness
  18. 0018cases hchoose_right_right_witness_witness_witness_witness_witness_witness_right
  19. 0019cases hchoose_right_right_witness_witness_witness_witness_witness_witness_right_right
  20. 0020have hbound : exists bcf_lt_gap_bcs_row_bound. bcf_lt_gap_bcs_row_bound + S (n) = S n
  21. 0021specialize le_refl (S n)
  22. 0022exact le_refl
  23. 0023have htable_family : forall bcf_row_index_bcs_table_family. (exists bcf_lt_gap_bcs_table_family_bound. bcf_lt_gap_bcs_table_family_bound + S (bcf_row_index_bcs_table_family) = S n) -> (forall bcf_row_code_bcs_table_family_rows bcf_row_scale_bcs_table_family_rows. (((exists bcf_height_bcs_table_family_rows_code_at. bcf_height_bcs_table_family_rows_code_at + S (bcf_row_code_bcs_table_family_rows) = S ((S (bcf_row_index_bcs_table_family)) * x1)) /\ exists bcf_quotient_bcs_table_family_rows_code_at. x = bcf_quotient_bcs_table_family_rows_code_at * S ((S (bcf_row_index_bcs_table_family)) * x1) + (bcf_row_code_bcs_table_family_rows))) -> (((exists bcf_height_bcs_table_family_rows_scale_at. bcf_height_bcs_table_family_rows_scale_at + S (bcf_row_scale_bcs_table_family_rows) = S ((S (bcf_row_index_bcs_table_family)) * x3)) /\ exists bcf_quotient_bcs_table_family_rows_scale_at. x2 = bcf_quotient_bcs_table_family_rows_scale_at * S ((S (bcf_row_index_bcs_table_family)) * x3) + (bcf_row_scale_bcs_table_family_rows))) -> ((((exists bcf_lt_gap_bcs_table_family_rows_boundary_diagonal_bound. bcf_lt_gap_bcs_table_family_rows_boundary_diagonal_bound + S (bcf_row_index_bcs_table_family) = S n) -> forall bcf_diagonal_value_bcs_table_family_rows_boundary. (((exists bcf_height_bcs_table_family_rows_boundary_diagonal_at. bcf_height_bcs_table_family_rows_boundary_diagonal_at + S (bcf_diagonal_value_bcs_table_family_rows_boundary) = S ((S (bcf_row_index_bcs_table_family)) * bcf_row_scale_bcs_table_family_rows)) /\ exists bcf_quotient_bcs_table_family_rows_boundary_diagonal_at. bcf_row_code_bcs_table_family_rows = bcf_quotient_bcs_table_family_rows_boundary_diagonal_at * S ((S (bcf_row_index_bcs_table_family)) * bcf_row_scale_bcs_table_family_rows) + (bcf_diagonal_value_bcs_table_family_rows_boundary))) -> bcf_diagonal_value_bcs_table_family_rows_boundary = 1) /\ forall bcf_above_index_bcs_table_family_rows_boundary bcf_above_value_bcs_table_family_rows_boundary. (exists bcf_lt_gap_bcs_table_family_rows_boundary_above_order. bcf_lt_gap_bcs_table_family_rows_boundary_above_order + S (bcf_row_index_bcs_table_family) = bcf_above_index_bcs_table_family_rows_boundary) -> (exists bcf_lt_gap_bcs_table_family_rows_boundary_above_bound. bcf_lt_gap_bcs_table_family_rows_boundary_above_bound + S (bcf_above_index_bcs_table_family_rows_boundary) = S n) -> (((exists bcf_height_bcs_table_family_rows_boundary_above_at. bcf_height_bcs_table_family_rows_boundary_above_at + S (bcf_above_value_bcs_table_family_rows_boundary) = S ((S (bcf_above_index_bcs_table_family_rows_boundary)) * bcf_row_scale_bcs_table_family_rows)) /\ exists bcf_quotient_bcs_table_family_rows_boundary_above_at. bcf_row_code_bcs_table_family_rows = bcf_quotient_bcs_table_family_rows_boundary_above_at * S ((S (bcf_above_index_bcs_table_family_rows_boundary)) * bcf_row_scale_bcs_table_family_rows) + (bcf_above_value_bcs_table_family_rows_boundary))) -> bcf_above_value_bcs_table_family_rows_boundary = 0)))
  24. 0024specialize beta_pascal_table_diagonal_boundary x
  25. 0025specialize beta_pascal_table_diagonal_boundary x1
  26. 0026specialize beta_pascal_table_diagonal_boundary x2
  27. 0027specialize beta_pascal_table_diagonal_boundary x3
  28. 0028specialize beta_pascal_table_diagonal_boundary (S n)
  29. 0029specialize beta_pascal_table_diagonal_boundary (S n)
  30. 0030apply beta_pascal_table_diagonal_boundary
  31. 0031exact hchoose_right_right_witness_witness_witness_witness_witness_witness_left
  32. 0032have hrow_family : forall bcf_row_code_bcs_row_family bcf_row_scale_bcs_row_family. (((exists bcf_height_bcs_row_family_code_at. bcf_height_bcs_row_family_code_at + S (bcf_row_code_bcs_row_family) = S ((S (n)) * x1)) /\ exists bcf_quotient_bcs_row_family_code_at. x = bcf_quotient_bcs_row_family_code_at * S ((S (n)) * x1) + (bcf_row_code_bcs_row_family))) -> (((exists bcf_height_bcs_row_family_scale_at. bcf_height_bcs_row_family_scale_at + S (bcf_row_scale_bcs_row_family) = S ((S (n)) * x3)) /\ exists bcf_quotient_bcs_row_family_scale_at. x2 = bcf_quotient_bcs_row_family_scale_at * S ((S (n)) * x3) + (bcf_row_scale_bcs_row_family))) -> ((((exists bcf_lt_gap_bcs_row_family_boundary_diagonal_bound. bcf_lt_gap_bcs_row_family_boundary_diagonal_bound + S (n) = S n) -> forall bcf_diagonal_value_bcs_row_family_boundary. (((exists bcf_height_bcs_row_family_boundary_diagonal_at. bcf_height_bcs_row_family_boundary_diagonal_at + S (bcf_diagonal_value_bcs_row_family_boundary) = S ((S (n)) * bcf_row_scale_bcs_row_family)) /\ exists bcf_quotient_bcs_row_family_boundary_diagonal_at. bcf_row_code_bcs_row_family = bcf_quotient_bcs_row_family_boundary_diagonal_at * S ((S (n)) * bcf_row_scale_bcs_row_family) + (bcf_diagonal_value_bcs_row_family_boundary))) -> bcf_diagonal_value_bcs_row_family_boundary = 1) /\ forall bcf_above_index_bcs_row_family_boundary bcf_above_value_bcs_row_family_boundary. (exists bcf_lt_gap_bcs_row_family_boundary_above_order. bcf_lt_gap_bcs_row_family_boundary_above_order + S (n) = bcf_above_index_bcs_row_family_boundary) -> (exists bcf_lt_gap_bcs_row_family_boundary_above_bound. bcf_lt_gap_bcs_row_family_boundary_above_bound + S (bcf_above_index_bcs_row_family_boundary) = S n) -> (((exists bcf_height_bcs_row_family_boundary_above_at. bcf_height_bcs_row_family_boundary_above_at + S (bcf_above_value_bcs_row_family_boundary) = S ((S (bcf_above_index_bcs_row_family_boundary)) * bcf_row_scale_bcs_row_family)) /\ exists bcf_quotient_bcs_row_family_boundary_above_at. bcf_row_code_bcs_row_family = bcf_quotient_bcs_row_family_boundary_above_at * S ((S (bcf_above_index_bcs_row_family_boundary)) * bcf_row_scale_bcs_row_family) + (bcf_above_value_bcs_row_family_boundary))) -> bcf_above_value_bcs_row_family_boundary = 0))
  33. 0033specialize htable_family n
  34. 0034apply htable_family
  35. 0035exact hbound
  36. 0036have hboundary : (((exists bcf_lt_gap_bcs_boundary_diagonal_bound. bcf_lt_gap_bcs_boundary_diagonal_bound + S (n) = S n) -> forall bcf_diagonal_value_bcs_boundary. (((exists bcf_height_bcs_boundary_diagonal_at. bcf_height_bcs_boundary_diagonal_at + S (bcf_diagonal_value_bcs_boundary) = S ((S (n)) * x5)) /\ exists bcf_quotient_bcs_boundary_diagonal_at. x4 = bcf_quotient_bcs_boundary_diagonal_at * S ((S (n)) * x5) + (bcf_diagonal_value_bcs_boundary))) -> bcf_diagonal_value_bcs_boundary = 1) /\ forall bcf_above_index_bcs_boundary bcf_above_value_bcs_boundary. (exists bcf_lt_gap_bcs_boundary_above_order. bcf_lt_gap_bcs_boundary_above_order + S (n) = bcf_above_index_bcs_boundary) -> (exists bcf_lt_gap_bcs_boundary_above_bound. bcf_lt_gap_bcs_boundary_above_bound + S (bcf_above_index_bcs_boundary) = S n) -> (((exists bcf_height_bcs_boundary_above_at. bcf_height_bcs_boundary_above_at + S (bcf_above_value_bcs_boundary) = S ((S (bcf_above_index_bcs_boundary)) * x5)) /\ exists bcf_quotient_bcs_boundary_above_at. x4 = bcf_quotient_bcs_boundary_above_at * S ((S (bcf_above_index_bcs_boundary)) * x5) + (bcf_above_value_bcs_boundary))) -> bcf_above_value_bcs_boundary = 0)
  37. 0037specialize hrow_family x4
  38. 0038specialize hrow_family x5
  39. 0039apply hrow_family
  40. 0040exact hchoose_right_right_witness_witness_witness_witness_witness_witness_right_left
  41. 0041exact hchoose_right_right_witness_witness_witness_witness_witness_witness_right_right_left
  42. 0042cases hboundary
  43. 0043have hdiagonal : forall z. (((exists bcf_height_bcs_diagonal_family. bcf_height_bcs_diagonal_family + S (z) = S ((S (n)) * x5)) /\ exists bcf_quotient_bcs_diagonal_family. x4 = bcf_quotient_bcs_diagonal_family * S ((S (n)) * x5) + (z))) -> z = 1
  44. 0044apply hboundary_left
  45. 0045exact hbound
  46. 0046specialize hdiagonal z
  47. 0047apply hdiagonal
  48. 0048exact hchoose_right_right_witness_witness_witness_witness_witness_witness_right_right_right