BT00TB

beta_pascal_table_row_pointwise_functional

Alpha body-checked · checked-use disabled

Corresponding decoded Pascal-table rows agree pointwise.

Exact expanded PA statement

forall bb bc sb sc w r db dc eb ec v s i b c d e. (forall bcf_row_index_bptrpf_left_table. (exists bcf_lt_gap_bptrpf_left_table_row_bound. bcf_lt_gap_bptrpf_left_table_row_bound + S (bcf_row_index_bptrpf_left_table) = r) -> exists bcf_row_code_bptrpf_left_table bcf_row_scale_bptrpf_left_table. ((((exists bcf_height_bptrpf_left_table_decoded_row_code. bcf_height_bptrpf_left_table_decoded_row_code + S (bcf_row_code_bptrpf_left_table) = S ((S (bcf_row_index_bptrpf_left_table)) * bc)) /\ exists bcf_quotient_bptrpf_left_table_decoded_row_code. bb = bcf_quotient_bptrpf_left_table_decoded_row_code * S ((S (bcf_row_index_bptrpf_left_table)) * bc) + (bcf_row_code_bptrpf_left_table))) /\ ((((exists bcf_height_bptrpf_left_table_decoded_row_scale. bcf_height_bptrpf_left_table_decoded_row_scale + S (bcf_row_scale_bptrpf_left_table) = S ((S (bcf_row_index_bptrpf_left_table)) * sc)) /\ exists bcf_quotient_bptrpf_left_table_decoded_row_scale. sb = bcf_quotient_bptrpf_left_table_decoded_row_scale * S ((S (bcf_row_index_bptrpf_left_table)) * sc) + (bcf_row_scale_bptrpf_left_table))) /\ ((bcf_row_index_bptrpf_left_table = 0 /\ (forall bcf_index_bptrpf_left_table_zero_row. (exists bcf_lt_gap_bptrpf_left_table_zero_row_bound. bcf_lt_gap_bptrpf_left_table_zero_row_bound + S (bcf_index_bptrpf_left_table_zero_row) = w) -> exists bcf_value_bptrpf_left_table_zero_row. ((((exists bcf_height_bptrpf_left_table_zero_row_entry. bcf_height_bptrpf_left_table_zero_row_entry + S (bcf_value_bptrpf_left_table_zero_row) = S ((S (bcf_index_bptrpf_left_table_zero_row)) * bcf_row_scale_bptrpf_left_table)) /\ exists bcf_quotient_bptrpf_left_table_zero_row_entry. bcf_row_code_bptrpf_left_table = bcf_quotient_bptrpf_left_table_zero_row_entry * S ((S (bcf_index_bptrpf_left_table_zero_row)) * bcf_row_scale_bptrpf_left_table) + (bcf_value_bptrpf_left_table_zero_row))) /\ ((bcf_index_bptrpf_left_table_zero_row = 0 /\ bcf_value_bptrpf_left_table_zero_row = 1) \/ exists bcf_predecessor_bptrpf_left_table_zero_row. bcf_index_bptrpf_left_table_zero_row = S bcf_predecessor_bptrpf_left_table_zero_row /\ bcf_value_bptrpf_left_table_zero_row = 0)))) \/ exists bcf_predecessor_bptrpf_left_table bcf_previous_code_bptrpf_left_table bcf_previous_scale_bptrpf_left_table. bcf_row_index_bptrpf_left_table = S bcf_predecessor_bptrpf_left_table /\ ((((exists bcf_height_bptrpf_left_table_decoded_previous_code. bcf_height_bptrpf_left_table_decoded_previous_code + S (bcf_previous_code_bptrpf_left_table) = S ((S (bcf_predecessor_bptrpf_left_table)) * bc)) /\ exists bcf_quotient_bptrpf_left_table_decoded_previous_code. bb = bcf_quotient_bptrpf_left_table_decoded_previous_code * S ((S (bcf_predecessor_bptrpf_left_table)) * bc) + (bcf_previous_code_bptrpf_left_table))) /\ ((((exists bcf_height_bptrpf_left_table_decoded_previous_scale. bcf_height_bptrpf_left_table_decoded_previous_scale + S (bcf_previous_scale_bptrpf_left_table) = S ((S (bcf_predecessor_bptrpf_left_table)) * sc)) /\ exists bcf_quotient_bptrpf_left_table_decoded_previous_scale. sb = bcf_quotient_bptrpf_left_table_decoded_previous_scale * S ((S (bcf_predecessor_bptrpf_left_table)) * sc) + (bcf_previous_scale_bptrpf_left_table))) /\ (forall bcf_index_bptrpf_left_table_row_step. (exists bcf_lt_gap_bptrpf_left_table_row_step_bound. bcf_lt_gap_bptrpf_left_table_row_step_bound + S (bcf_index_bptrpf_left_table_row_step) = w) -> exists bcf_value_bptrpf_left_table_row_step. ((((exists bcf_height_bptrpf_left_table_row_step_entry. bcf_height_bptrpf_left_table_row_step_entry + S (bcf_value_bptrpf_left_table_row_step) = S ((S (bcf_index_bptrpf_left_table_row_step)) * bcf_row_scale_bptrpf_left_table)) /\ exists bcf_quotient_bptrpf_left_table_row_step_entry. bcf_row_code_bptrpf_left_table = bcf_quotient_bptrpf_left_table_row_step_entry * S ((S (bcf_index_bptrpf_left_table_row_step)) * bcf_row_scale_bptrpf_left_table) + (bcf_value_bptrpf_left_table_row_step))) /\ ((bcf_index_bptrpf_left_table_row_step = 0 /\ bcf_value_bptrpf_left_table_row_step = 1) \/ exists bcf_predecessor_bptrpf_left_table_row_step bcf_left_bptrpf_left_table_row_step bcf_right_bptrpf_left_table_row_step. bcf_index_bptrpf_left_table_row_step = S bcf_predecessor_bptrpf_left_table_row_step /\ ((((exists bcf_height_bptrpf_left_table_row_step_previous_left. bcf_height_bptrpf_left_table_row_step_previous_left + S (bcf_left_bptrpf_left_table_row_step) = S ((S (bcf_predecessor_bptrpf_left_table_row_step)) * bcf_previous_scale_bptrpf_left_table)) /\ exists bcf_quotient_bptrpf_left_table_row_step_previous_left. bcf_previous_code_bptrpf_left_table = bcf_quotient_bptrpf_left_table_row_step_previous_left * S ((S (bcf_predecessor_bptrpf_left_table_row_step)) * bcf_previous_scale_bptrpf_left_table) + (bcf_left_bptrpf_left_table_row_step))) /\ ((((exists bcf_height_bptrpf_left_table_row_step_previous_right. bcf_height_bptrpf_left_table_row_step_previous_right + S (bcf_right_bptrpf_left_table_row_step) = S ((S (S (bcf_predecessor_bptrpf_left_table_row_step))) * bcf_previous_scale_bptrpf_left_table)) /\ exists bcf_quotient_bptrpf_left_table_row_step_previous_right. bcf_previous_code_bptrpf_left_table = bcf_quotient_bptrpf_left_table_row_step_previous_right * S ((S (S (bcf_predecessor_bptrpf_left_table_row_step))) * bcf_previous_scale_bptrpf_left_table) + (bcf_right_bptrpf_left_table_row_step))) /\ bcf_value_bptrpf_left_table_row_step = bcf_left_bptrpf_left_table_row_step + bcf_right_bptrpf_left_table_row_step))))))))))) -> (forall bcf_row_index_bptrpf_right_table. (exists bcf_lt_gap_bptrpf_right_table_row_bound. bcf_lt_gap_bptrpf_right_table_row_bound + S (bcf_row_index_bptrpf_right_table) = s) -> exists bcf_row_code_bptrpf_right_table bcf_row_scale_bptrpf_right_table. ((((exists bcf_height_bptrpf_right_table_decoded_row_code. bcf_height_bptrpf_right_table_decoded_row_code + S (bcf_row_code_bptrpf_right_table) = S ((S (bcf_row_index_bptrpf_right_table)) * dc)) /\ exists bcf_quotient_bptrpf_right_table_decoded_row_code. db = bcf_quotient_bptrpf_right_table_decoded_row_code * S ((S (bcf_row_index_bptrpf_right_table)) * dc) + (bcf_row_code_bptrpf_right_table))) /\ ((((exists bcf_height_bptrpf_right_table_decoded_row_scale. bcf_height_bptrpf_right_table_decoded_row_scale + S (bcf_row_scale_bptrpf_right_table) = S ((S (bcf_row_index_bptrpf_right_table)) * ec)) /\ exists bcf_quotient_bptrpf_right_table_decoded_row_scale. eb = bcf_quotient_bptrpf_right_table_decoded_row_scale * S ((S (bcf_row_index_bptrpf_right_table)) * ec) + (bcf_row_scale_bptrpf_right_table))) /\ ((bcf_row_index_bptrpf_right_table = 0 /\ (forall bcf_index_bptrpf_right_table_zero_row. (exists bcf_lt_gap_bptrpf_right_table_zero_row_bound. bcf_lt_gap_bptrpf_right_table_zero_row_bound + S (bcf_index_bptrpf_right_table_zero_row) = v) -> exists bcf_value_bptrpf_right_table_zero_row. ((((exists bcf_height_bptrpf_right_table_zero_row_entry. bcf_height_bptrpf_right_table_zero_row_entry + S (bcf_value_bptrpf_right_table_zero_row) = S ((S (bcf_index_bptrpf_right_table_zero_row)) * bcf_row_scale_bptrpf_right_table)) /\ exists bcf_quotient_bptrpf_right_table_zero_row_entry. bcf_row_code_bptrpf_right_table = bcf_quotient_bptrpf_right_table_zero_row_entry * S ((S (bcf_index_bptrpf_right_table_zero_row)) * bcf_row_scale_bptrpf_right_table) + (bcf_value_bptrpf_right_table_zero_row))) /\ ((bcf_index_bptrpf_right_table_zero_row = 0 /\ bcf_value_bptrpf_right_table_zero_row = 1) \/ exists bcf_predecessor_bptrpf_right_table_zero_row. bcf_index_bptrpf_right_table_zero_row = S bcf_predecessor_bptrpf_right_table_zero_row /\ bcf_value_bptrpf_right_table_zero_row = 0)))) \/ exists bcf_predecessor_bptrpf_right_table bcf_previous_code_bptrpf_right_table bcf_previous_scale_bptrpf_right_table. bcf_row_index_bptrpf_right_table = S bcf_predecessor_bptrpf_right_table /\ ((((exists bcf_height_bptrpf_right_table_decoded_previous_code. bcf_height_bptrpf_right_table_decoded_previous_code + S (bcf_previous_code_bptrpf_right_table) = S ((S (bcf_predecessor_bptrpf_right_table)) * dc)) /\ exists bcf_quotient_bptrpf_right_table_decoded_previous_code. db = bcf_quotient_bptrpf_right_table_decoded_previous_code * S ((S (bcf_predecessor_bptrpf_right_table)) * dc) + (bcf_previous_code_bptrpf_right_table))) /\ ((((exists bcf_height_bptrpf_right_table_decoded_previous_scale. bcf_height_bptrpf_right_table_decoded_previous_scale + S (bcf_previous_scale_bptrpf_right_table) = S ((S (bcf_predecessor_bptrpf_right_table)) * ec)) /\ exists bcf_quotient_bptrpf_right_table_decoded_previous_scale. eb = bcf_quotient_bptrpf_right_table_decoded_previous_scale * S ((S (bcf_predecessor_bptrpf_right_table)) * ec) + (bcf_previous_scale_bptrpf_right_table))) /\ (forall bcf_index_bptrpf_right_table_row_step. (exists bcf_lt_gap_bptrpf_right_table_row_step_bound. bcf_lt_gap_bptrpf_right_table_row_step_bound + S (bcf_index_bptrpf_right_table_row_step) = v) -> exists bcf_value_bptrpf_right_table_row_step. ((((exists bcf_height_bptrpf_right_table_row_step_entry. bcf_height_bptrpf_right_table_row_step_entry + S (bcf_value_bptrpf_right_table_row_step) = S ((S (bcf_index_bptrpf_right_table_row_step)) * bcf_row_scale_bptrpf_right_table)) /\ exists bcf_quotient_bptrpf_right_table_row_step_entry. bcf_row_code_bptrpf_right_table = bcf_quotient_bptrpf_right_table_row_step_entry * S ((S (bcf_index_bptrpf_right_table_row_step)) * bcf_row_scale_bptrpf_right_table) + (bcf_value_bptrpf_right_table_row_step))) /\ ((bcf_index_bptrpf_right_table_row_step = 0 /\ bcf_value_bptrpf_right_table_row_step = 1) \/ exists bcf_predecessor_bptrpf_right_table_row_step bcf_left_bptrpf_right_table_row_step bcf_right_bptrpf_right_table_row_step. bcf_index_bptrpf_right_table_row_step = S bcf_predecessor_bptrpf_right_table_row_step /\ ((((exists bcf_height_bptrpf_right_table_row_step_previous_left. bcf_height_bptrpf_right_table_row_step_previous_left + S (bcf_left_bptrpf_right_table_row_step) = S ((S (bcf_predecessor_bptrpf_right_table_row_step)) * bcf_previous_scale_bptrpf_right_table)) /\ exists bcf_quotient_bptrpf_right_table_row_step_previous_left. bcf_previous_code_bptrpf_right_table = bcf_quotient_bptrpf_right_table_row_step_previous_left * S ((S (bcf_predecessor_bptrpf_right_table_row_step)) * bcf_previous_scale_bptrpf_right_table) + (bcf_left_bptrpf_right_table_row_step))) /\ ((((exists bcf_height_bptrpf_right_table_row_step_previous_right. bcf_height_bptrpf_right_table_row_step_previous_right + S (bcf_right_bptrpf_right_table_row_step) = S ((S (S (bcf_predecessor_bptrpf_right_table_row_step))) * bcf_previous_scale_bptrpf_right_table)) /\ exists bcf_quotient_bptrpf_right_table_row_step_previous_right. bcf_previous_code_bptrpf_right_table = bcf_quotient_bptrpf_right_table_row_step_previous_right * S ((S (S (bcf_predecessor_bptrpf_right_table_row_step))) * bcf_previous_scale_bptrpf_right_table) + (bcf_right_bptrpf_right_table_row_step))) /\ bcf_value_bptrpf_right_table_row_step = bcf_left_bptrpf_right_table_row_step + bcf_right_bptrpf_right_table_row_step))))))))))) -> (exists bcf_lt_gap_bptrpf_left_row_bound. bcf_lt_gap_bptrpf_left_row_bound + S (i) = r) -> (exists bcf_lt_gap_bptrpf_right_row_bound. bcf_lt_gap_bptrpf_right_row_bound + S (i) = s) -> (((exists bcf_height_bptrpf_left_code_at. bcf_height_bptrpf_left_code_at + S (b) = S ((S (i)) * bc)) /\ exists bcf_quotient_bptrpf_left_code_at. bb = bcf_quotient_bptrpf_left_code_at * S ((S (i)) * bc) + (b))) -> (((exists bcf_height_bptrpf_left_scale_at. bcf_height_bptrpf_left_scale_at + S (c) = S ((S (i)) * sc)) /\ exists bcf_quotient_bptrpf_left_scale_at. sb = bcf_quotient_bptrpf_left_scale_at * S ((S (i)) * sc) + (c))) -> (((exists bcf_height_bptrpf_right_code_at. bcf_height_bptrpf_right_code_at + S (d) = S ((S (i)) * dc)) /\ exists bcf_quotient_bptrpf_right_code_at. db = bcf_quotient_bptrpf_right_code_at * S ((S (i)) * dc) + (d))) -> (((exists bcf_height_bptrpf_right_scale_at. bcf_height_bptrpf_right_scale_at + S (e) = S ((S (i)) * ec)) /\ exists bcf_quotient_bptrpf_right_scale_at. eb = bcf_quotient_bptrpf_right_scale_at * S ((S (i)) * ec) + (e))) -> (forall bcf_index_bptrpf_agree bcf_left_value_bptrpf_agree bcf_right_value_bptrpf_agree. (exists bcf_lt_gap_bptrpf_agree_left_bound. bcf_lt_gap_bptrpf_agree_left_bound + S (bcf_index_bptrpf_agree) = w) -> (exists bcf_lt_gap_bptrpf_agree_right_bound. bcf_lt_gap_bptrpf_agree_right_bound + S (bcf_index_bptrpf_agree) = v) -> (((exists bcf_height_bptrpf_agree_left_entry. bcf_height_bptrpf_agree_left_entry + S (bcf_left_value_bptrpf_agree) = S ((S (bcf_index_bptrpf_agree)) * c)) /\ exists bcf_quotient_bptrpf_agree_left_entry. b = bcf_quotient_bptrpf_agree_left_entry * S ((S (bcf_index_bptrpf_agree)) * c) + (bcf_left_value_bptrpf_agree))) -> (((exists bcf_height_bptrpf_agree_right_entry. bcf_height_bptrpf_agree_right_entry + S (bcf_right_value_bptrpf_agree) = S ((S (bcf_index_bptrpf_agree)) * e)) /\ exists bcf_quotient_bptrpf_agree_right_entry. d = bcf_quotient_bptrpf_agree_right_entry * S ((S (bcf_index_bptrpf_agree)) * e) + (bcf_right_value_bptrpf_agree))) -> bcf_left_value_bptrpf_agree = bcf_right_value_bptrpf_agree)

Structural proof guide

Corresponding decoded Pascal-table rows agree pointwise.

Direct prerequisites: beta_at_unique, succ_ne_zero, succ_injective, lt_to_le, beta_pascal_zero_row_pointwise_functional, beta_pascal_row_step_pointwise_functional. The authored body proceeds by structural induction (1), case analysis (44), intermediate claims (27), equality transport (20).

Proof neighborhood

Direct dependencies

BT0042 beta_at_unique BT000C succ_ne_zero BT000D succ_injective BT0019 lt_to_le BT00T9 beta_pascal_zero_row_pointwise_functional BT00TA beta_pascal_row_step_pointwise_functional

Direct dependents

BT00TC choose_functional BT00TI choose_succ_succ_of_lt

Formal native tactic body

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

  1. 0001intro bb
  2. 0002intro bc
  3. 0003intro sb
  4. 0004intro sc
  5. 0005intro w
  6. 0006intro r
  7. 0007intro db
  8. 0008intro dc
  9. 0009intro eb
  10. 0010intro ec
  11. 0011intro v
  12. 0012intro s
  13. 0013intro i
  14. 0014induction i
  15. 0015intro b
  16. 0016intro c
  17. 0017intro d
  18. 0018intro e
  19. 0019intro hleft_table
  20. 0020intro hright_table
  21. 0021intro hir
  22. 0022intro his
  23. 0023intro hbb
  24. 0024intro hsb
  25. 0025intro hdb
  26. 0026intro heb
  27. 0027have hleft_row : exists bcf_row_code_bptrpf_left_base bcf_row_scale_bptrpf_left_base. ((((exists bcf_height_bptrpf_left_base_decoded_row_code. bcf_height_bptrpf_left_base_decoded_row_code + S (bcf_row_code_bptrpf_left_base) = S ((S (0)) * bc)) /\ exists bcf_quotient_bptrpf_left_base_decoded_row_code. bb = bcf_quotient_bptrpf_left_base_decoded_row_code * S ((S (0)) * bc) + (bcf_row_code_bptrpf_left_base))) /\ ((((exists bcf_height_bptrpf_left_base_decoded_row_scale. bcf_height_bptrpf_left_base_decoded_row_scale + S (bcf_row_scale_bptrpf_left_base) = S ((S (0)) * sc)) /\ exists bcf_quotient_bptrpf_left_base_decoded_row_scale. sb = bcf_quotient_bptrpf_left_base_decoded_row_scale * S ((S (0)) * sc) + (bcf_row_scale_bptrpf_left_base))) /\ ((0 = 0 /\ (forall bcf_index_bptrpf_left_base_zero_row. (exists bcf_lt_gap_bptrpf_left_base_zero_row_bound. bcf_lt_gap_bptrpf_left_base_zero_row_bound + S (bcf_index_bptrpf_left_base_zero_row) = w) -> exists bcf_value_bptrpf_left_base_zero_row. ((((exists bcf_height_bptrpf_left_base_zero_row_entry. bcf_height_bptrpf_left_base_zero_row_entry + S (bcf_value_bptrpf_left_base_zero_row) = S ((S (bcf_index_bptrpf_left_base_zero_row)) * bcf_row_scale_bptrpf_left_base)) /\ exists bcf_quotient_bptrpf_left_base_zero_row_entry. bcf_row_code_bptrpf_left_base = bcf_quotient_bptrpf_left_base_zero_row_entry * S ((S (bcf_index_bptrpf_left_base_zero_row)) * bcf_row_scale_bptrpf_left_base) + (bcf_value_bptrpf_left_base_zero_row))) /\ ((bcf_index_bptrpf_left_base_zero_row = 0 /\ bcf_value_bptrpf_left_base_zero_row = 1) \/ exists bcf_predecessor_bptrpf_left_base_zero_row. bcf_index_bptrpf_left_base_zero_row = S bcf_predecessor_bptrpf_left_base_zero_row /\ bcf_value_bptrpf_left_base_zero_row = 0)))) \/ exists bcf_predecessor_bptrpf_left_base bcf_previous_code_bptrpf_left_base bcf_previous_scale_bptrpf_left_base. 0 = S bcf_predecessor_bptrpf_left_base /\ ((((exists bcf_height_bptrpf_left_base_decoded_previous_code. bcf_height_bptrpf_left_base_decoded_previous_code + S (bcf_previous_code_bptrpf_left_base) = S ((S (bcf_predecessor_bptrpf_left_base)) * bc)) /\ exists bcf_quotient_bptrpf_left_base_decoded_previous_code. bb = bcf_quotient_bptrpf_left_base_decoded_previous_code * S ((S (bcf_predecessor_bptrpf_left_base)) * bc) + (bcf_previous_code_bptrpf_left_base))) /\ ((((exists bcf_height_bptrpf_left_base_decoded_previous_scale. bcf_height_bptrpf_left_base_decoded_previous_scale + S (bcf_previous_scale_bptrpf_left_base) = S ((S (bcf_predecessor_bptrpf_left_base)) * sc)) /\ exists bcf_quotient_bptrpf_left_base_decoded_previous_scale. sb = bcf_quotient_bptrpf_left_base_decoded_previous_scale * S ((S (bcf_predecessor_bptrpf_left_base)) * sc) + (bcf_previous_scale_bptrpf_left_base))) /\ (forall bcf_index_bptrpf_left_base_row_step. (exists bcf_lt_gap_bptrpf_left_base_row_step_bound. bcf_lt_gap_bptrpf_left_base_row_step_bound + S (bcf_index_bptrpf_left_base_row_step) = w) -> exists bcf_value_bptrpf_left_base_row_step. ((((exists bcf_height_bptrpf_left_base_row_step_entry. bcf_height_bptrpf_left_base_row_step_entry + S (bcf_value_bptrpf_left_base_row_step) = S ((S (bcf_index_bptrpf_left_base_row_step)) * bcf_row_scale_bptrpf_left_base)) /\ exists bcf_quotient_bptrpf_left_base_row_step_entry. bcf_row_code_bptrpf_left_base = bcf_quotient_bptrpf_left_base_row_step_entry * S ((S (bcf_index_bptrpf_left_base_row_step)) * bcf_row_scale_bptrpf_left_base) + (bcf_value_bptrpf_left_base_row_step))) /\ ((bcf_index_bptrpf_left_base_row_step = 0 /\ bcf_value_bptrpf_left_base_row_step = 1) \/ exists bcf_predecessor_bptrpf_left_base_row_step bcf_left_bptrpf_left_base_row_step bcf_right_bptrpf_left_base_row_step. bcf_index_bptrpf_left_base_row_step = S bcf_predecessor_bptrpf_left_base_row_step /\ ((((exists bcf_height_bptrpf_left_base_row_step_previous_left. bcf_height_bptrpf_left_base_row_step_previous_left + S (bcf_left_bptrpf_left_base_row_step) = S ((S (bcf_predecessor_bptrpf_left_base_row_step)) * bcf_previous_scale_bptrpf_left_base)) /\ exists bcf_quotient_bptrpf_left_base_row_step_previous_left. bcf_previous_code_bptrpf_left_base = bcf_quotient_bptrpf_left_base_row_step_previous_left * S ((S (bcf_predecessor_bptrpf_left_base_row_step)) * bcf_previous_scale_bptrpf_left_base) + (bcf_left_bptrpf_left_base_row_step))) /\ ((((exists bcf_height_bptrpf_left_base_row_step_previous_right. bcf_height_bptrpf_left_base_row_step_previous_right + S (bcf_right_bptrpf_left_base_row_step) = S ((S (S (bcf_predecessor_bptrpf_left_base_row_step))) * bcf_previous_scale_bptrpf_left_base)) /\ exists bcf_quotient_bptrpf_left_base_row_step_previous_right. bcf_previous_code_bptrpf_left_base = bcf_quotient_bptrpf_left_base_row_step_previous_right * S ((S (S (bcf_predecessor_bptrpf_left_base_row_step))) * bcf_previous_scale_bptrpf_left_base) + (bcf_right_bptrpf_left_base_row_step))) /\ bcf_value_bptrpf_left_base_row_step = bcf_left_bptrpf_left_base_row_step + bcf_right_bptrpf_left_base_row_step))))))))))
  28. 0028specialize hleft_table 0
  29. 0029apply hleft_table
  30. 0030exact hir
  31. 0031cases hleft_row
  32. 0032cases hleft_row_witness
  33. 0033cases hleft_row_witness_witness
  34. 0034cases hleft_row_witness_witness_right
  35. 0035have hright_row : exists bcf_row_code_bptrpf_right_base bcf_row_scale_bptrpf_right_base. ((((exists bcf_height_bptrpf_right_base_decoded_row_code. bcf_height_bptrpf_right_base_decoded_row_code + S (bcf_row_code_bptrpf_right_base) = S ((S (0)) * dc)) /\ exists bcf_quotient_bptrpf_right_base_decoded_row_code. db = bcf_quotient_bptrpf_right_base_decoded_row_code * S ((S (0)) * dc) + (bcf_row_code_bptrpf_right_base))) /\ ((((exists bcf_height_bptrpf_right_base_decoded_row_scale. bcf_height_bptrpf_right_base_decoded_row_scale + S (bcf_row_scale_bptrpf_right_base) = S ((S (0)) * ec)) /\ exists bcf_quotient_bptrpf_right_base_decoded_row_scale. eb = bcf_quotient_bptrpf_right_base_decoded_row_scale * S ((S (0)) * ec) + (bcf_row_scale_bptrpf_right_base))) /\ ((0 = 0 /\ (forall bcf_index_bptrpf_right_base_zero_row. (exists bcf_lt_gap_bptrpf_right_base_zero_row_bound. bcf_lt_gap_bptrpf_right_base_zero_row_bound + S (bcf_index_bptrpf_right_base_zero_row) = v) -> exists bcf_value_bptrpf_right_base_zero_row. ((((exists bcf_height_bptrpf_right_base_zero_row_entry. bcf_height_bptrpf_right_base_zero_row_entry + S (bcf_value_bptrpf_right_base_zero_row) = S ((S (bcf_index_bptrpf_right_base_zero_row)) * bcf_row_scale_bptrpf_right_base)) /\ exists bcf_quotient_bptrpf_right_base_zero_row_entry. bcf_row_code_bptrpf_right_base = bcf_quotient_bptrpf_right_base_zero_row_entry * S ((S (bcf_index_bptrpf_right_base_zero_row)) * bcf_row_scale_bptrpf_right_base) + (bcf_value_bptrpf_right_base_zero_row))) /\ ((bcf_index_bptrpf_right_base_zero_row = 0 /\ bcf_value_bptrpf_right_base_zero_row = 1) \/ exists bcf_predecessor_bptrpf_right_base_zero_row. bcf_index_bptrpf_right_base_zero_row = S bcf_predecessor_bptrpf_right_base_zero_row /\ bcf_value_bptrpf_right_base_zero_row = 0)))) \/ exists bcf_predecessor_bptrpf_right_base bcf_previous_code_bptrpf_right_base bcf_previous_scale_bptrpf_right_base. 0 = S bcf_predecessor_bptrpf_right_base /\ ((((exists bcf_height_bptrpf_right_base_decoded_previous_code. bcf_height_bptrpf_right_base_decoded_previous_code + S (bcf_previous_code_bptrpf_right_base) = S ((S (bcf_predecessor_bptrpf_right_base)) * dc)) /\ exists bcf_quotient_bptrpf_right_base_decoded_previous_code. db = bcf_quotient_bptrpf_right_base_decoded_previous_code * S ((S (bcf_predecessor_bptrpf_right_base)) * dc) + (bcf_previous_code_bptrpf_right_base))) /\ ((((exists bcf_height_bptrpf_right_base_decoded_previous_scale. bcf_height_bptrpf_right_base_decoded_previous_scale + S (bcf_previous_scale_bptrpf_right_base) = S ((S (bcf_predecessor_bptrpf_right_base)) * ec)) /\ exists bcf_quotient_bptrpf_right_base_decoded_previous_scale. eb = bcf_quotient_bptrpf_right_base_decoded_previous_scale * S ((S (bcf_predecessor_bptrpf_right_base)) * ec) + (bcf_previous_scale_bptrpf_right_base))) /\ (forall bcf_index_bptrpf_right_base_row_step. (exists bcf_lt_gap_bptrpf_right_base_row_step_bound. bcf_lt_gap_bptrpf_right_base_row_step_bound + S (bcf_index_bptrpf_right_base_row_step) = v) -> exists bcf_value_bptrpf_right_base_row_step. ((((exists bcf_height_bptrpf_right_base_row_step_entry. bcf_height_bptrpf_right_base_row_step_entry + S (bcf_value_bptrpf_right_base_row_step) = S ((S (bcf_index_bptrpf_right_base_row_step)) * bcf_row_scale_bptrpf_right_base)) /\ exists bcf_quotient_bptrpf_right_base_row_step_entry. bcf_row_code_bptrpf_right_base = bcf_quotient_bptrpf_right_base_row_step_entry * S ((S (bcf_index_bptrpf_right_base_row_step)) * bcf_row_scale_bptrpf_right_base) + (bcf_value_bptrpf_right_base_row_step))) /\ ((bcf_index_bptrpf_right_base_row_step = 0 /\ bcf_value_bptrpf_right_base_row_step = 1) \/ exists bcf_predecessor_bptrpf_right_base_row_step bcf_left_bptrpf_right_base_row_step bcf_right_bptrpf_right_base_row_step. bcf_index_bptrpf_right_base_row_step = S bcf_predecessor_bptrpf_right_base_row_step /\ ((((exists bcf_height_bptrpf_right_base_row_step_previous_left. bcf_height_bptrpf_right_base_row_step_previous_left + S (bcf_left_bptrpf_right_base_row_step) = S ((S (bcf_predecessor_bptrpf_right_base_row_step)) * bcf_previous_scale_bptrpf_right_base)) /\ exists bcf_quotient_bptrpf_right_base_row_step_previous_left. bcf_previous_code_bptrpf_right_base = bcf_quotient_bptrpf_right_base_row_step_previous_left * S ((S (bcf_predecessor_bptrpf_right_base_row_step)) * bcf_previous_scale_bptrpf_right_base) + (bcf_left_bptrpf_right_base_row_step))) /\ ((((exists bcf_height_bptrpf_right_base_row_step_previous_right. bcf_height_bptrpf_right_base_row_step_previous_right + S (bcf_right_bptrpf_right_base_row_step) = S ((S (S (bcf_predecessor_bptrpf_right_base_row_step))) * bcf_previous_scale_bptrpf_right_base)) /\ exists bcf_quotient_bptrpf_right_base_row_step_previous_right. bcf_previous_code_bptrpf_right_base = bcf_quotient_bptrpf_right_base_row_step_previous_right * S ((S (S (bcf_predecessor_bptrpf_right_base_row_step))) * bcf_previous_scale_bptrpf_right_base) + (bcf_right_bptrpf_right_base_row_step))) /\ bcf_value_bptrpf_right_base_row_step = bcf_left_bptrpf_right_base_row_step + bcf_right_bptrpf_right_base_row_step))))))))))
  36. 0036specialize hright_table 0
  37. 0037apply hright_table
  38. 0038exact his
  39. 0039cases hright_row
  40. 0040cases hright_row_witness
  41. 0041cases hright_row_witness_witness
  42. 0042cases hright_row_witness_witness_right
  43. 0043have hb : b = x
  44. 0044specialize beta_at_unique bb
  45. 0045specialize beta_at_unique bc
  46. 0046specialize beta_at_unique 0
  47. 0047specialize beta_at_unique b
  48. 0048specialize beta_at_unique x
  49. 0049apply beta_at_unique
  50. 0050exact hbb
  51. 0051exact hleft_row_witness_witness_left
  52. 0052have hc : c = x1
  53. 0053specialize beta_at_unique sb
  54. 0054specialize beta_at_unique sc
  55. 0055specialize beta_at_unique 0
  56. 0056specialize beta_at_unique c
  57. 0057specialize beta_at_unique x1
  58. 0058apply beta_at_unique
  59. 0059exact hsb
  60. 0060exact hleft_row_witness_witness_right_left
  61. 0061have hd : d = x2
  62. 0062specialize beta_at_unique db
  63. 0063specialize beta_at_unique dc
  64. 0064specialize beta_at_unique 0
  65. 0065specialize beta_at_unique d
  66. 0066specialize beta_at_unique x2
  67. 0067apply beta_at_unique
  68. 0068exact hdb
  69. 0069exact hright_row_witness_witness_left
  70. 0070have he : e = x3
  71. 0071specialize beta_at_unique eb
  72. 0072specialize beta_at_unique ec
  73. 0073specialize beta_at_unique 0
  74. 0074specialize beta_at_unique e
  75. 0075specialize beta_at_unique x3
  76. 0076apply beta_at_unique
  77. 0077exact heb
  78. 0078exact hright_row_witness_witness_right_left
  79. 0079cases hleft_row_witness_witness_right_right
  80. 0080cases hleft_row_witness_witness_right_right_left
  81. 0081cases hright_row_witness_witness_right_right
  82. 0082cases hright_row_witness_witness_right_right_left
  83. 0083intro j
  84. 0084intro u
  85. 0085intro y
  86. 0086intro hjw
  87. 0087intro hjv
  88. 0088intro hleft_entry
  89. 0089intro hright_entry
  90. 0090have hleft_semantic : ((exists bcf_height_bptrpf_base_left_semantic. bcf_height_bptrpf_base_left_semantic + S (u) = S ((S (j)) * x1)) /\ exists bcf_quotient_bptrpf_base_left_semantic. x = bcf_quotient_bptrpf_base_left_semantic * S ((S (j)) * x1) + (u))
  91. 0091rewrite <- hb
  92. 0092rewrite <- hc
  93. 0093rewrite <- hc
  94. 0094exact hleft_entry
  95. 0095have hright_semantic : ((exists bcf_height_bptrpf_base_right_semantic. bcf_height_bptrpf_base_right_semantic + S (y) = S ((S (j)) * x3)) /\ exists bcf_quotient_bptrpf_base_right_semantic. x2 = bcf_quotient_bptrpf_base_right_semantic * S ((S (j)) * x3) + (y))
  96. 0096rewrite <- hd
  97. 0097rewrite <- he
  98. 0098rewrite <- he
  99. 0099exact hright_entry
  100. 0100specialize beta_pascal_zero_row_pointwise_functional x
  101. 0101specialize beta_pascal_zero_row_pointwise_functional x1
  102. 0102specialize beta_pascal_zero_row_pointwise_functional x2
  103. 0103specialize beta_pascal_zero_row_pointwise_functional x3
  104. 0104specialize beta_pascal_zero_row_pointwise_functional w
  105. 0105specialize beta_pascal_zero_row_pointwise_functional v
  106. 0106specialize beta_pascal_zero_row_pointwise_functional j
  107. 0107specialize beta_pascal_zero_row_pointwise_functional u
  108. 0108specialize beta_pascal_zero_row_pointwise_functional y
  109. 0109apply beta_pascal_zero_row_pointwise_functional
  110. 0110exact hleft_row_witness_witness_right_right_left_right
  111. 0111exact hright_row_witness_witness_right_right_left_right
  112. 0112exact hjw
  113. 0113exact hjv
  114. 0114exact hleft_semantic
  115. 0115exact hright_semantic
  116. 0116cases hright_row_witness_witness_right_right_right
  117. 0117cases hright_row_witness_witness_right_right_right_witness
  118. 0118cases hright_row_witness_witness_right_right_right_witness_witness
  119. 0119cases hright_row_witness_witness_right_right_right_witness_witness_witness
  120. 0120exfalso
  121. 0121have hbad : S x4 = 0
  122. 0122symm
  123. 0123exact hright_row_witness_witness_right_right_right_witness_witness_witness_left
  124. 0124specialize succ_ne_zero x4
  125. 0125apply succ_ne_zero
  126. 0126exact hbad
  127. 0127cases hleft_row_witness_witness_right_right_right
  128. 0128cases hleft_row_witness_witness_right_right_right_witness
  129. 0129cases hleft_row_witness_witness_right_right_right_witness_witness
  130. 0130cases hleft_row_witness_witness_right_right_right_witness_witness_witness
  131. 0131exfalso
  132. 0132have hbad : S x4 = 0
  133. 0133symm
  134. 0134exact hleft_row_witness_witness_right_right_right_witness_witness_witness_left
  135. 0135specialize succ_ne_zero x4
  136. 0136apply succ_ne_zero
  137. 0137exact hbad
  138. 0138intro b
  139. 0139intro c
  140. 0140intro d
  141. 0141intro e
  142. 0142intro hleft_table
  143. 0143intro hright_table
  144. 0144intro hir
  145. 0145intro his
  146. 0146intro hbb
  147. 0147intro hsb
  148. 0148intro hdb
  149. 0149intro heb
  150. 0150have hleft_row : exists bcf_row_code_bptrpf_left_step bcf_row_scale_bptrpf_left_step. ((((exists bcf_height_bptrpf_left_step_decoded_row_code. bcf_height_bptrpf_left_step_decoded_row_code + S (bcf_row_code_bptrpf_left_step) = S ((S (S i)) * bc)) /\ exists bcf_quotient_bptrpf_left_step_decoded_row_code. bb = bcf_quotient_bptrpf_left_step_decoded_row_code * S ((S (S i)) * bc) + (bcf_row_code_bptrpf_left_step))) /\ ((((exists bcf_height_bptrpf_left_step_decoded_row_scale. bcf_height_bptrpf_left_step_decoded_row_scale + S (bcf_row_scale_bptrpf_left_step) = S ((S (S i)) * sc)) /\ exists bcf_quotient_bptrpf_left_step_decoded_row_scale. sb = bcf_quotient_bptrpf_left_step_decoded_row_scale * S ((S (S i)) * sc) + (bcf_row_scale_bptrpf_left_step))) /\ ((S i = 0 /\ (forall bcf_index_bptrpf_left_step_zero_row. (exists bcf_lt_gap_bptrpf_left_step_zero_row_bound. bcf_lt_gap_bptrpf_left_step_zero_row_bound + S (bcf_index_bptrpf_left_step_zero_row) = w) -> exists bcf_value_bptrpf_left_step_zero_row. ((((exists bcf_height_bptrpf_left_step_zero_row_entry. bcf_height_bptrpf_left_step_zero_row_entry + S (bcf_value_bptrpf_left_step_zero_row) = S ((S (bcf_index_bptrpf_left_step_zero_row)) * bcf_row_scale_bptrpf_left_step)) /\ exists bcf_quotient_bptrpf_left_step_zero_row_entry. bcf_row_code_bptrpf_left_step = bcf_quotient_bptrpf_left_step_zero_row_entry * S ((S (bcf_index_bptrpf_left_step_zero_row)) * bcf_row_scale_bptrpf_left_step) + (bcf_value_bptrpf_left_step_zero_row))) /\ ((bcf_index_bptrpf_left_step_zero_row = 0 /\ bcf_value_bptrpf_left_step_zero_row = 1) \/ exists bcf_predecessor_bptrpf_left_step_zero_row. bcf_index_bptrpf_left_step_zero_row = S bcf_predecessor_bptrpf_left_step_zero_row /\ bcf_value_bptrpf_left_step_zero_row = 0)))) \/ exists bcf_predecessor_bptrpf_left_step bcf_previous_code_bptrpf_left_step bcf_previous_scale_bptrpf_left_step. S i = S bcf_predecessor_bptrpf_left_step /\ ((((exists bcf_height_bptrpf_left_step_decoded_previous_code. bcf_height_bptrpf_left_step_decoded_previous_code + S (bcf_previous_code_bptrpf_left_step) = S ((S (bcf_predecessor_bptrpf_left_step)) * bc)) /\ exists bcf_quotient_bptrpf_left_step_decoded_previous_code. bb = bcf_quotient_bptrpf_left_step_decoded_previous_code * S ((S (bcf_predecessor_bptrpf_left_step)) * bc) + (bcf_previous_code_bptrpf_left_step))) /\ ((((exists bcf_height_bptrpf_left_step_decoded_previous_scale. bcf_height_bptrpf_left_step_decoded_previous_scale + S (bcf_previous_scale_bptrpf_left_step) = S ((S (bcf_predecessor_bptrpf_left_step)) * sc)) /\ exists bcf_quotient_bptrpf_left_step_decoded_previous_scale. sb = bcf_quotient_bptrpf_left_step_decoded_previous_scale * S ((S (bcf_predecessor_bptrpf_left_step)) * sc) + (bcf_previous_scale_bptrpf_left_step))) /\ (forall bcf_index_bptrpf_left_step_row_step. (exists bcf_lt_gap_bptrpf_left_step_row_step_bound. bcf_lt_gap_bptrpf_left_step_row_step_bound + S (bcf_index_bptrpf_left_step_row_step) = w) -> exists bcf_value_bptrpf_left_step_row_step. ((((exists bcf_height_bptrpf_left_step_row_step_entry. bcf_height_bptrpf_left_step_row_step_entry + S (bcf_value_bptrpf_left_step_row_step) = S ((S (bcf_index_bptrpf_left_step_row_step)) * bcf_row_scale_bptrpf_left_step)) /\ exists bcf_quotient_bptrpf_left_step_row_step_entry. bcf_row_code_bptrpf_left_step = bcf_quotient_bptrpf_left_step_row_step_entry * S ((S (bcf_index_bptrpf_left_step_row_step)) * bcf_row_scale_bptrpf_left_step) + (bcf_value_bptrpf_left_step_row_step))) /\ ((bcf_index_bptrpf_left_step_row_step = 0 /\ bcf_value_bptrpf_left_step_row_step = 1) \/ exists bcf_predecessor_bptrpf_left_step_row_step bcf_left_bptrpf_left_step_row_step bcf_right_bptrpf_left_step_row_step. bcf_index_bptrpf_left_step_row_step = S bcf_predecessor_bptrpf_left_step_row_step /\ ((((exists bcf_height_bptrpf_left_step_row_step_previous_left. bcf_height_bptrpf_left_step_row_step_previous_left + S (bcf_left_bptrpf_left_step_row_step) = S ((S (bcf_predecessor_bptrpf_left_step_row_step)) * bcf_previous_scale_bptrpf_left_step)) /\ exists bcf_quotient_bptrpf_left_step_row_step_previous_left. bcf_previous_code_bptrpf_left_step = bcf_quotient_bptrpf_left_step_row_step_previous_left * S ((S (bcf_predecessor_bptrpf_left_step_row_step)) * bcf_previous_scale_bptrpf_left_step) + (bcf_left_bptrpf_left_step_row_step))) /\ ((((exists bcf_height_bptrpf_left_step_row_step_previous_right. bcf_height_bptrpf_left_step_row_step_previous_right + S (bcf_right_bptrpf_left_step_row_step) = S ((S (S (bcf_predecessor_bptrpf_left_step_row_step))) * bcf_previous_scale_bptrpf_left_step)) /\ exists bcf_quotient_bptrpf_left_step_row_step_previous_right. bcf_previous_code_bptrpf_left_step = bcf_quotient_bptrpf_left_step_row_step_previous_right * S ((S (S (bcf_predecessor_bptrpf_left_step_row_step))) * bcf_previous_scale_bptrpf_left_step) + (bcf_right_bptrpf_left_step_row_step))) /\ bcf_value_bptrpf_left_step_row_step = bcf_left_bptrpf_left_step_row_step + bcf_right_bptrpf_left_step_row_step))))))))))
  151. 0151specialize hleft_table (S i)
  152. 0152apply hleft_table
  153. 0153exact hir
  154. 0154cases hleft_row
  155. 0155cases hleft_row_witness
  156. 0156cases hleft_row_witness_witness
  157. 0157cases hleft_row_witness_witness_right
  158. 0158have hright_row : exists bcf_row_code_bptrpf_right_step bcf_row_scale_bptrpf_right_step. ((((exists bcf_height_bptrpf_right_step_decoded_row_code. bcf_height_bptrpf_right_step_decoded_row_code + S (bcf_row_code_bptrpf_right_step) = S ((S (S i)) * dc)) /\ exists bcf_quotient_bptrpf_right_step_decoded_row_code. db = bcf_quotient_bptrpf_right_step_decoded_row_code * S ((S (S i)) * dc) + (bcf_row_code_bptrpf_right_step))) /\ ((((exists bcf_height_bptrpf_right_step_decoded_row_scale. bcf_height_bptrpf_right_step_decoded_row_scale + S (bcf_row_scale_bptrpf_right_step) = S ((S (S i)) * ec)) /\ exists bcf_quotient_bptrpf_right_step_decoded_row_scale. eb = bcf_quotient_bptrpf_right_step_decoded_row_scale * S ((S (S i)) * ec) + (bcf_row_scale_bptrpf_right_step))) /\ ((S i = 0 /\ (forall bcf_index_bptrpf_right_step_zero_row. (exists bcf_lt_gap_bptrpf_right_step_zero_row_bound. bcf_lt_gap_bptrpf_right_step_zero_row_bound + S (bcf_index_bptrpf_right_step_zero_row) = v) -> exists bcf_value_bptrpf_right_step_zero_row. ((((exists bcf_height_bptrpf_right_step_zero_row_entry. bcf_height_bptrpf_right_step_zero_row_entry + S (bcf_value_bptrpf_right_step_zero_row) = S ((S (bcf_index_bptrpf_right_step_zero_row)) * bcf_row_scale_bptrpf_right_step)) /\ exists bcf_quotient_bptrpf_right_step_zero_row_entry. bcf_row_code_bptrpf_right_step = bcf_quotient_bptrpf_right_step_zero_row_entry * S ((S (bcf_index_bptrpf_right_step_zero_row)) * bcf_row_scale_bptrpf_right_step) + (bcf_value_bptrpf_right_step_zero_row))) /\ ((bcf_index_bptrpf_right_step_zero_row = 0 /\ bcf_value_bptrpf_right_step_zero_row = 1) \/ exists bcf_predecessor_bptrpf_right_step_zero_row. bcf_index_bptrpf_right_step_zero_row = S bcf_predecessor_bptrpf_right_step_zero_row /\ bcf_value_bptrpf_right_step_zero_row = 0)))) \/ exists bcf_predecessor_bptrpf_right_step bcf_previous_code_bptrpf_right_step bcf_previous_scale_bptrpf_right_step. S i = S bcf_predecessor_bptrpf_right_step /\ ((((exists bcf_height_bptrpf_right_step_decoded_previous_code. bcf_height_bptrpf_right_step_decoded_previous_code + S (bcf_previous_code_bptrpf_right_step) = S ((S (bcf_predecessor_bptrpf_right_step)) * dc)) /\ exists bcf_quotient_bptrpf_right_step_decoded_previous_code. db = bcf_quotient_bptrpf_right_step_decoded_previous_code * S ((S (bcf_predecessor_bptrpf_right_step)) * dc) + (bcf_previous_code_bptrpf_right_step))) /\ ((((exists bcf_height_bptrpf_right_step_decoded_previous_scale. bcf_height_bptrpf_right_step_decoded_previous_scale + S (bcf_previous_scale_bptrpf_right_step) = S ((S (bcf_predecessor_bptrpf_right_step)) * ec)) /\ exists bcf_quotient_bptrpf_right_step_decoded_previous_scale. eb = bcf_quotient_bptrpf_right_step_decoded_previous_scale * S ((S (bcf_predecessor_bptrpf_right_step)) * ec) + (bcf_previous_scale_bptrpf_right_step))) /\ (forall bcf_index_bptrpf_right_step_row_step. (exists bcf_lt_gap_bptrpf_right_step_row_step_bound. bcf_lt_gap_bptrpf_right_step_row_step_bound + S (bcf_index_bptrpf_right_step_row_step) = v) -> exists bcf_value_bptrpf_right_step_row_step. ((((exists bcf_height_bptrpf_right_step_row_step_entry. bcf_height_bptrpf_right_step_row_step_entry + S (bcf_value_bptrpf_right_step_row_step) = S ((S (bcf_index_bptrpf_right_step_row_step)) * bcf_row_scale_bptrpf_right_step)) /\ exists bcf_quotient_bptrpf_right_step_row_step_entry. bcf_row_code_bptrpf_right_step = bcf_quotient_bptrpf_right_step_row_step_entry * S ((S (bcf_index_bptrpf_right_step_row_step)) * bcf_row_scale_bptrpf_right_step) + (bcf_value_bptrpf_right_step_row_step))) /\ ((bcf_index_bptrpf_right_step_row_step = 0 /\ bcf_value_bptrpf_right_step_row_step = 1) \/ exists bcf_predecessor_bptrpf_right_step_row_step bcf_left_bptrpf_right_step_row_step bcf_right_bptrpf_right_step_row_step. bcf_index_bptrpf_right_step_row_step = S bcf_predecessor_bptrpf_right_step_row_step /\ ((((exists bcf_height_bptrpf_right_step_row_step_previous_left. bcf_height_bptrpf_right_step_row_step_previous_left + S (bcf_left_bptrpf_right_step_row_step) = S ((S (bcf_predecessor_bptrpf_right_step_row_step)) * bcf_previous_scale_bptrpf_right_step)) /\ exists bcf_quotient_bptrpf_right_step_row_step_previous_left. bcf_previous_code_bptrpf_right_step = bcf_quotient_bptrpf_right_step_row_step_previous_left * S ((S (bcf_predecessor_bptrpf_right_step_row_step)) * bcf_previous_scale_bptrpf_right_step) + (bcf_left_bptrpf_right_step_row_step))) /\ ((((exists bcf_height_bptrpf_right_step_row_step_previous_right. bcf_height_bptrpf_right_step_row_step_previous_right + S (bcf_right_bptrpf_right_step_row_step) = S ((S (S (bcf_predecessor_bptrpf_right_step_row_step))) * bcf_previous_scale_bptrpf_right_step)) /\ exists bcf_quotient_bptrpf_right_step_row_step_previous_right. bcf_previous_code_bptrpf_right_step = bcf_quotient_bptrpf_right_step_row_step_previous_right * S ((S (S (bcf_predecessor_bptrpf_right_step_row_step))) * bcf_previous_scale_bptrpf_right_step) + (bcf_right_bptrpf_right_step_row_step))) /\ bcf_value_bptrpf_right_step_row_step = bcf_left_bptrpf_right_step_row_step + bcf_right_bptrpf_right_step_row_step))))))))))
  159. 0159specialize hright_table (S i)
  160. 0160apply hright_table
  161. 0161exact his
  162. 0162cases hright_row
  163. 0163cases hright_row_witness
  164. 0164cases hright_row_witness_witness
  165. 0165cases hright_row_witness_witness_right
  166. 0166have hb : b = x
  167. 0167specialize beta_at_unique bb
  168. 0168specialize beta_at_unique bc
  169. 0169specialize beta_at_unique (S i)
  170. 0170specialize beta_at_unique b
  171. 0171specialize beta_at_unique x
  172. 0172apply beta_at_unique
  173. 0173exact hbb
  174. 0174exact hleft_row_witness_witness_left
  175. 0175have hc : c = x1
  176. 0176specialize beta_at_unique sb
  177. 0177specialize beta_at_unique sc
  178. 0178specialize beta_at_unique (S i)
  179. 0179specialize beta_at_unique c
  180. 0180specialize beta_at_unique x1
  181. 0181apply beta_at_unique
  182. 0182exact hsb
  183. 0183exact hleft_row_witness_witness_right_left
  184. 0184have hd : d = x2
  185. 0185specialize beta_at_unique db
  186. 0186specialize beta_at_unique dc
  187. 0187specialize beta_at_unique (S i)
  188. 0188specialize beta_at_unique d
  189. 0189specialize beta_at_unique x2
  190. 0190apply beta_at_unique
  191. 0191exact hdb
  192. 0192exact hright_row_witness_witness_left
  193. 0193have he : e = x3
  194. 0194specialize beta_at_unique eb
  195. 0195specialize beta_at_unique ec
  196. 0196specialize beta_at_unique (S i)
  197. 0197specialize beta_at_unique e
  198. 0198specialize beta_at_unique x3
  199. 0199apply beta_at_unique
  200. 0200exact heb
  201. 0201exact hright_row_witness_witness_right_left
  202. 0202cases hleft_row_witness_witness_right_right
  203. 0203cases hleft_row_witness_witness_right_right_left
  204. 0204exfalso
  205. 0205specialize succ_ne_zero i
  206. 0206apply succ_ne_zero
  207. 0207exact hleft_row_witness_witness_right_right_left_left
  208. 0208cases hleft_row_witness_witness_right_right_right
  209. 0209cases hleft_row_witness_witness_right_right_right_witness
  210. 0210cases hleft_row_witness_witness_right_right_right_witness_witness
  211. 0211cases hleft_row_witness_witness_right_right_right_witness_witness_witness
  212. 0212cases hleft_row_witness_witness_right_right_right_witness_witness_witness_right
  213. 0213cases hleft_row_witness_witness_right_right_right_witness_witness_witness_right_right
  214. 0214cases hright_row_witness_witness_right_right
  215. 0215cases hright_row_witness_witness_right_right_left
  216. 0216exfalso
  217. 0217specialize succ_ne_zero i
  218. 0218apply succ_ne_zero
  219. 0219exact hright_row_witness_witness_right_right_left_left
  220. 0220cases hright_row_witness_witness_right_right_right
  221. 0221cases hright_row_witness_witness_right_right_right_witness
  222. 0222cases hright_row_witness_witness_right_right_right_witness_witness
  223. 0223cases hright_row_witness_witness_right_right_right_witness_witness_witness
  224. 0224cases hright_row_witness_witness_right_right_right_witness_witness_witness_right
  225. 0225cases hright_row_witness_witness_right_right_right_witness_witness_witness_right_right
  226. 0226have hleft_predecessor : i = x4
  227. 0227specialize succ_injective i
  228. 0228specialize succ_injective x4
  229. 0229apply succ_injective
  230. 0230exact hleft_row_witness_witness_right_right_right_witness_witness_witness_left
  231. 0231have hright_predecessor : i = x7
  232. 0232specialize succ_injective i
  233. 0233specialize succ_injective x7
  234. 0234apply succ_injective
  235. 0235exact hright_row_witness_witness_right_right_right_witness_witness_witness_left
  236. 0236have hprevious_left_bound : exists bcf_lt_gap_bptrpf_previous_left_bound. bcf_lt_gap_bptrpf_previous_left_bound + S (i) = r
  237. 0237specialize lt_to_le (S i)
  238. 0238specialize lt_to_le r
  239. 0239apply lt_to_le
  240. 0240exact hir
  241. 0241have hprevious_right_bound : exists bcf_lt_gap_bptrpf_previous_right_bound. bcf_lt_gap_bptrpf_previous_right_bound + S (i) = s
  242. 0242specialize lt_to_le (S i)
  243. 0243specialize lt_to_le s
  244. 0244apply lt_to_le
  245. 0245exact his
  246. 0246have hprevious_left_code : ((exists bcf_height_bptrpf_previous_left_code_at. bcf_height_bptrpf_previous_left_code_at + S (x5) = S ((S (i)) * bc)) /\ exists bcf_quotient_bptrpf_previous_left_code_at. bb = bcf_quotient_bptrpf_previous_left_code_at * S ((S (i)) * bc) + (x5))
  247. 0247rewrite hleft_predecessor
  248. 0248rewrite hleft_predecessor
  249. 0249exact hleft_row_witness_witness_right_right_right_witness_witness_witness_right_left
  250. 0250have hprevious_left_scale : ((exists bcf_height_bptrpf_previous_left_scale_at. bcf_height_bptrpf_previous_left_scale_at + S (x6) = S ((S (i)) * sc)) /\ exists bcf_quotient_bptrpf_previous_left_scale_at. sb = bcf_quotient_bptrpf_previous_left_scale_at * S ((S (i)) * sc) + (x6))
  251. 0251rewrite hleft_predecessor
  252. 0252rewrite hleft_predecessor
  253. 0253exact hleft_row_witness_witness_right_right_right_witness_witness_witness_right_right_left
  254. 0254have hprevious_right_code : ((exists bcf_height_bptrpf_previous_right_code_at. bcf_height_bptrpf_previous_right_code_at + S (x8) = S ((S (i)) * dc)) /\ exists bcf_quotient_bptrpf_previous_right_code_at. db = bcf_quotient_bptrpf_previous_right_code_at * S ((S (i)) * dc) + (x8))
  255. 0255rewrite hright_predecessor
  256. 0256rewrite hright_predecessor
  257. 0257exact hright_row_witness_witness_right_right_right_witness_witness_witness_right_left
  258. 0258have hprevious_right_scale : ((exists bcf_height_bptrpf_previous_right_scale_at. bcf_height_bptrpf_previous_right_scale_at + S (x9) = S ((S (i)) * ec)) /\ exists bcf_quotient_bptrpf_previous_right_scale_at. eb = bcf_quotient_bptrpf_previous_right_scale_at * S ((S (i)) * ec) + (x9))
  259. 0259rewrite hright_predecessor
  260. 0260rewrite hright_predecessor
  261. 0261exact hright_row_witness_witness_right_right_right_witness_witness_witness_right_right_left
  262. 0262have hcurrent_semantic : forall bcf_index_bptrpf_step_semantic_agree bcf_left_value_bptrpf_step_semantic_agree bcf_right_value_bptrpf_step_semantic_agree. (exists bcf_lt_gap_bptrpf_step_semantic_agree_left_bound. bcf_lt_gap_bptrpf_step_semantic_agree_left_bound + S (bcf_index_bptrpf_step_semantic_agree) = w) -> (exists bcf_lt_gap_bptrpf_step_semantic_agree_right_bound. bcf_lt_gap_bptrpf_step_semantic_agree_right_bound + S (bcf_index_bptrpf_step_semantic_agree) = v) -> (((exists bcf_height_bptrpf_step_semantic_agree_left_entry. bcf_height_bptrpf_step_semantic_agree_left_entry + S (bcf_left_value_bptrpf_step_semantic_agree) = S ((S (bcf_index_bptrpf_step_semantic_agree)) * x1)) /\ exists bcf_quotient_bptrpf_step_semantic_agree_left_entry. x = bcf_quotient_bptrpf_step_semantic_agree_left_entry * S ((S (bcf_index_bptrpf_step_semantic_agree)) * x1) + (bcf_left_value_bptrpf_step_semantic_agree))) -> (((exists bcf_height_bptrpf_step_semantic_agree_right_entry. bcf_height_bptrpf_step_semantic_agree_right_entry + S (bcf_right_value_bptrpf_step_semantic_agree) = S ((S (bcf_index_bptrpf_step_semantic_agree)) * x3)) /\ exists bcf_quotient_bptrpf_step_semantic_agree_right_entry. x2 = bcf_quotient_bptrpf_step_semantic_agree_right_entry * S ((S (bcf_index_bptrpf_step_semantic_agree)) * x3) + (bcf_right_value_bptrpf_step_semantic_agree))) -> bcf_left_value_bptrpf_step_semantic_agree = bcf_right_value_bptrpf_step_semantic_agree
  263. 0263specialize beta_pascal_row_step_pointwise_functional x5
  264. 0264specialize beta_pascal_row_step_pointwise_functional x6
  265. 0265specialize beta_pascal_row_step_pointwise_functional x8
  266. 0266specialize beta_pascal_row_step_pointwise_functional x9
  267. 0267specialize beta_pascal_row_step_pointwise_functional x
  268. 0268specialize beta_pascal_row_step_pointwise_functional x1
  269. 0269specialize beta_pascal_row_step_pointwise_functional x2
  270. 0270specialize beta_pascal_row_step_pointwise_functional x3
  271. 0271specialize beta_pascal_row_step_pointwise_functional w
  272. 0272specialize beta_pascal_row_step_pointwise_functional v
  273. 0273apply beta_pascal_row_step_pointwise_functional
  274. 0274exact hleft_row_witness_witness_right_right_right_witness_witness_witness_right_right_right
  275. 0275exact hright_row_witness_witness_right_right_right_witness_witness_witness_right_right_right
  276. 0276specialize IH x5
  277. 0277specialize IH x6
  278. 0278specialize IH x8
  279. 0279specialize IH x9
  280. 0280apply IH
  281. 0281exact hleft_table
  282. 0282exact hright_table
  283. 0283exact hprevious_left_bound
  284. 0284exact hprevious_right_bound
  285. 0285exact hprevious_left_code
  286. 0286exact hprevious_left_scale
  287. 0287exact hprevious_right_code
  288. 0288exact hprevious_right_scale
  289. 0289intro j
  290. 0290intro u
  291. 0291intro y
  292. 0292intro hjw
  293. 0293intro hjv
  294. 0294intro hleft_entry
  295. 0295intro hright_entry
  296. 0296have hleft_semantic : ((exists bcf_height_bptrpf_step_left_semantic. bcf_height_bptrpf_step_left_semantic + S (u) = S ((S (j)) * x1)) /\ exists bcf_quotient_bptrpf_step_left_semantic. x = bcf_quotient_bptrpf_step_left_semantic * S ((S (j)) * x1) + (u))
  297. 0297rewrite <- hb
  298. 0298rewrite <- hc
  299. 0299rewrite <- hc
  300. 0300exact hleft_entry
  301. 0301have hright_semantic : ((exists bcf_height_bptrpf_step_right_semantic. bcf_height_bptrpf_step_right_semantic + S (y) = S ((S (j)) * x3)) /\ exists bcf_quotient_bptrpf_step_right_semantic. x2 = bcf_quotient_bptrpf_step_right_semantic * S ((S (j)) * x3) + (y))
  302. 0302rewrite <- hd
  303. 0303rewrite <- he
  304. 0304rewrite <- he
  305. 0305exact hright_entry
  306. 0306specialize hcurrent_semantic j
  307. 0307specialize hcurrent_semantic u
  308. 0308specialize hcurrent_semantic y
  309. 0309apply hcurrent_semantic
  310. 0310exact hjw
  311. 0311exact hjv
  312. 0312exact hleft_semantic
  313. 0313exact hright_semantic