BT00TB · Bertrand theorem

beta_pascal_table_row_pointwise_functional

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Corresponding decoded Pascal-table rows agree pointwise.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ bb. ∀ bc. ∀ sb. ∀ sc. ∀ w. ∀ r. ∀ db. ∀ dc. ∀ eb. ∀ ec. ∀ v. ∀ s. ∀ i. ∀ b. ∀ c. ∀ d. ∀ e. (∀ x. Lt(x,r) → ∃ y. ∃ z. BetaAt(bb,bc,x,y) ∧ (BetaAt(sb,sc,x,z) ∧ (x = 0 ∧ (∀ n. Lt(n,w) → ∃ m. BetaAt(y,z,n,m) ∧ (n = 0 ∧ m = 1 ∨ (∃ k. n = S k ∧ m = 0))) ∨ (∃ n. ∃ m. ∃ k. x = S n ∧ (BetaAt(bb,bc,n,m) ∧ (BetaAt(sb,sc,n,k) ∧ (∀ j. Lt(j,w) → ∃ u. BetaAt(y,z,j,u) ∧ (j = 0 ∧ u = 1 ∨ (∃ x0. ∃ x1. ∃ x2. j = S x0 ∧ (BetaAt(m,k,x0,x1) ∧ (BetaAt(m,k,S x0,x2) ∧ u = x1 + x2))))))))))) → (∀ x. Lt(x,s) → ∃ y. ∃ z. BetaAt(db,dc,x,y) ∧ (BetaAt(eb,ec,x,z) ∧ (x = 0 ∧ (∀ n. Lt(n,v) → ∃ m. BetaAt(y,z,n,m) ∧ (n = 0 ∧ m = 1 ∨ (∃ k. n = S k ∧ m = 0))) ∨ (∃ n. ∃ m. ∃ k. x = S n ∧ (BetaAt(db,dc,n,m) ∧ (BetaAt(eb,ec,n,k) ∧ (∀ j. Lt(j,v) → ∃ u. BetaAt(y,z,j,u) ∧ (j = 0 ∧ u = 1 ∨ (∃ x0. ∃ x1. ∃ x2. j = S x0 ∧ (BetaAt(m,k,x0,x1) ∧ (BetaAt(m,k,S x0,x2) ∧ u = x1 + x2))))))))))) → Lt(i,r) → Lt(i,s) → BetaAt(bb,bc,i,b) → BetaAt(sb,sc,i,c) → BetaAt(db,dc,i,d) → BetaAt(eb,ec,i,e) → ∀ x. ∀ y. ∀ z. Lt(x,w) → Lt(x,v) → BetaAt(b,c,x,y) → BetaAt(d,e,x,z) → y = z

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt

32 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

54 occurrences

Exact expanded native-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)

Proof neighborhood

Direct theorem prerequisites

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 theorem dependents

BT00TC choose_functional BT00TI choose_succ_succ_of_lt

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

313 script commands · 51 reading checkpoints · 27 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (6)
beta at uniquesucc ne zerosucc injectivelt to lebeta pascal zero row pointwise functionalbeta pascal row step pointwise functional
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro bb
  2. L2
    intro bc
  3. L3
    intro sb
  4. L4
    intro sc
  5. L5
    intro w
  6. L6
    intro r
  7. L7
    intro db
  8. L8
    intro dc
  9. L9
    intro eb
  10. L10
    intro ec
02Fix variables and assumptionsL11–13

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro v
  2. L12
    intro s
  3. L13
    intro i
03Induction on iL14–23

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L14
    induction i
  2. L15
    intro b
  3. L16
    intro c
  4. L17
    intro d
  5. L18
    intro e
  6. L19
    intro hleft_table
  7. L20
    intro hright_table
  8. L21
    intro hir
  9. L22
    intro his
  10. L23
    intro hbb
04Fix variables and assumptionsL24–26

Work with arbitrary variables or the premises of the current implication.

  1. L24
    intro hsb
  2. L25
    intro hdb
  3. L26
    intro heb
05Establish hleft_rowL27–30

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hleft table.

  1. L27
    have hleft_row : ∃ bcf_row_code_bptrpf_left_base. ∃ bcf_row_scale_bptrpf_left_base. BetaAt(bb,bc,0,bcf_row_code_bptrpf_left_base) ∧ (BetaAt(sb,sc,0,bcf_row_scale_bptrpf_left_base) ∧ (0 = 0 ∧ (∀ x. Lt(x,w) → ∃ y. BetaAt(bcf_row_code_bptrpf_left_base,bcf_row_scale_bptrpf_left_base,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))) ∨ (∃ x. ∃ y. ∃ z. 0 = S x ∧ (BetaAt(bb,bc,x,y) ∧ (BetaAt(sb,sc,x,z) ∧ (∀ n. Lt(n,w) → ∃ m. BetaAt(bcf_row_code_bptrpf_left_base,bcf_row_scale_bptrpf_left_base,n,m) ∧ (n = 0 ∧ m = 1 ∨ (∃ k. ∃ i. ∃ j. n = S k ∧ (BetaAt(y,z,k,i) ∧ (BetaAt(y,z,S k,j) ∧ m = i + j))))))))))Definitions: BetaAt(bb,bc,0,bcf_row_code_bptrpf_left_base)BetaAt(sb,sc,0,bcf_row_scale_bptrpf_left_base)Lt(x,w)BetaAt(bcf_row_code_bptrpf_left_base,bcf_row_scale_bptrpf_left_base,x,y)BetaAt(bb,bc,x,y)BetaAt(sb,sc,x,z)Lt(n,w)BetaAt(bcf_row_code_bptrpf_left_base,bcf_row_scale_bptrpf_left_base,n,m)BetaAt(y,z,k,i)BetaAt(y,z,S k,j)Original native command in the exact edition
  2. L28
    specialize hleft_table 0
  3. L29
    apply hleft_table
  4. L30
    exact hir
06Separate the logical casesL31–34

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L31
    cases hleft_row
  2. L32
    cases hleft_row_witness
  3. L33
    cases hleft_row_witness_witness
  4. L34
    cases hleft_row_witness_witness_right
07Establish hright_rowL35–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hright table.

  1. L35
    have hright_row · expand full local formula (606 characters)have hright_row : ∃ bcf_row_code_bptrpf_right_base. ∃ bcf_row_scale_bptrpf_right_base. BetaAt(db,dc,0,bcf_row_code_bptrpf_right_base) ∧ (BetaAt(eb,ec,0,bcf_row_scale_bptrpf_right_base) ∧ (0 = 0 ∧ (∀ x. Lt(x,v) → ∃ y. BetaAt(bcf_row_code_bptrpf_right_base,bcf_row_scale_bptrpf_right_base,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))) ∨ (∃ x. ∃ y. ∃ z. 0 = S x ∧ (BetaAt(db,dc,x,y) ∧ (BetaAt(eb,ec,x,z) ∧ (∀ n. Lt(n,v) → ∃ m. BetaAt(bcf_row_code_bptrpf_right_base,bcf_row_scale_bptrpf_right_base,n,m) ∧ (n = 0 ∧ m = 1 ∨ (∃ k. ∃ i. ∃ j. n = S k ∧ (BetaAt(y,z,k,i) ∧ (BetaAt(y,z,S k,j) ∧ m = i + j))))))))))
    Definitions: BetaAt(db,dc,0,bcf_row_code_bptrpf_right_base)BetaAt(eb,ec,0,bcf_row_scale_bptrpf_right_base)Lt(x,v)BetaAt(bcf_row_code_bptrpf_right_base,bcf_row_scale_bptrpf_right_base,x,y)BetaAt(db,dc,x,y)BetaAt(eb,ec,x,z)Lt(n,v)BetaAt(bcf_row_code_bptrpf_right_base,bcf_row_scale_bptrpf_right_base,n,m)BetaAt(y,z,k,i)BetaAt(y,z,S k,j)Original native command in the exact edition
  2. L36
    specialize hright_table 0
  3. L37
    apply hright_table
  4. L38
    exact his
08Separate the logical casesL39–42

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L39
    cases hright_row
  2. L40
    cases hright_row_witness
  3. L41
    cases hright_row_witness_witness
  4. L42
    cases hright_row_witness_witness_right
09Establish hbL43–51

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L43
    have hb : b = x
  2. L44
    specialize beta_at_unique bb
  3. L45
    specialize beta_at_unique bc
  4. L46
    specialize beta_at_unique 0
  5. L47
    specialize beta_at_unique b
  6. L48
    specialize beta_at_unique x
  7. L49
    apply beta_at_unique
  8. L50
    exact hbb
  9. L51
    exact hleft_row_witness_witness_left
10Establish hcL52–60

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L52
    have hc : c = x1
  2. L53
    specialize beta_at_unique sb
  3. L54
    specialize beta_at_unique sc
  4. L55
    specialize beta_at_unique 0
  5. L56
    specialize beta_at_unique c
  6. L57
    specialize beta_at_unique x1
  7. L58
    apply beta_at_unique
  8. L59
    exact hsb
  9. L60
    exact hleft_row_witness_witness_right_left
11Establish hdL61–69

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L61
    have hd : d = x2
  2. L62
    specialize beta_at_unique db
  3. L63
    specialize beta_at_unique dc
  4. L64
    specialize beta_at_unique 0
  5. L65
    specialize beta_at_unique d
  6. L66
    specialize beta_at_unique x2
  7. L67
    apply beta_at_unique
  8. L68
    exact hdb
  9. L69
    exact hright_row_witness_witness_left
12Establish heL70–78

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L70
    have he : e = x3
  2. L71
    specialize beta_at_unique eb
  3. L72
    specialize beta_at_unique ec
  4. L73
    specialize beta_at_unique 0
  5. L74
    specialize beta_at_unique e
  6. L75
    specialize beta_at_unique x3
  7. L76
    apply beta_at_unique
  8. L77
    exact heb
  9. L78
    exact hright_row_witness_witness_right_left
13Separate the logical casesL79–82

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L79
    cases hleft_row_witness_witness_right_right
  2. L80
    cases hleft_row_witness_witness_right_right_left
  3. L81
    cases hright_row_witness_witness_right_right
  4. L82
    cases hright_row_witness_witness_right_right_left
14Fix variables and assumptionsL83–89

Work with arbitrary variables or the premises of the current implication.

  1. L83
    intro j
  2. L84
    intro u
  3. L85
    intro y
  4. L86
    intro hjw
  5. L87
    intro hjv
  6. L88
    intro hleft_entry
  7. L89
    intro hright_entry
15Establish hleft_semanticL90–94

Establish this local claim before using it. It is not an additional assumption.

  1. L90
    have hleft_semantic : BetaAt(x,x1,j,u)Definitions: BetaAt(x,x1,j,u)Original native command in the exact edition
  2. L91
    rewrite <- hb
  3. L92
    rewrite <- hc
  4. L93
    rewrite <- hc
  5. L94
    exact hleft_entry
16Establish hright_semanticL95–104

Establish this local claim before using it. It is not an additional assumption.

  1. L95
    have hright_semantic : BetaAt(x2,x3,j,y)Definitions: BetaAt(x2,x3,j,y)Original native command in the exact edition
  2. L96
    rewrite <- hd
  3. L97
    rewrite <- he
  4. L98
    rewrite <- he
  5. L99
    exact hright_entry
  6. L100
    specialize beta_pascal_zero_row_pointwise_functional x
  7. L101
    specialize beta_pascal_zero_row_pointwise_functional x1
  8. L102
    specialize beta_pascal_zero_row_pointwise_functional x2
  9. L103
    specialize beta_pascal_zero_row_pointwise_functional x3
  10. L104
    specialize beta_pascal_zero_row_pointwise_functional w
17Use earlier factsL105–114

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L105
    specialize beta_pascal_zero_row_pointwise_functional v
  2. L106
    specialize beta_pascal_zero_row_pointwise_functional j
  3. L107
    specialize beta_pascal_zero_row_pointwise_functional u
  4. L108
    specialize beta_pascal_zero_row_pointwise_functional y
  5. L109
    apply beta_pascal_zero_row_pointwise_functional
  6. L110
    exact hleft_row_witness_witness_right_right_left_right
  7. L111
    exact hright_row_witness_witness_right_right_left_right
  8. L112
    exact hjw
  9. L113
    exact hjv
  10. L114
    exact hleft_semantic
18Use earlier factsL115–115

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L115
    exact hright_semantic
19Separate the logical casesL116–120

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L116
    cases hright_row_witness_witness_right_right_right
  2. L117
    cases hright_row_witness_witness_right_right_right_witness
  3. L118
    cases hright_row_witness_witness_right_right_right_witness_witness
  4. L119
    cases hright_row_witness_witness_right_right_right_witness_witness_witness
  5. L120
    exfalso
20Establish hbadL121–126

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply succ ne zero.

  1. L121
    have hbad : S x4 = 0
  2. L122
    symm
  3. L123
    exact hright_row_witness_witness_right_right_right_witness_witness_witness_left
  4. L124
    specialize succ_ne_zero x4
  5. L125
    apply succ_ne_zero
  6. L126
    exact hbad
21Separate the logical casesL127–131

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L127
    cases hleft_row_witness_witness_right_right_right
  2. L128
    cases hleft_row_witness_witness_right_right_right_witness
  3. L129
    cases hleft_row_witness_witness_right_right_right_witness_witness
  4. L130
    cases hleft_row_witness_witness_right_right_right_witness_witness_witness
  5. L131
    exfalso
22Establish hbadL132–141

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply succ ne zero.

  1. L132
    have hbad : S x4 = 0
  2. L133
    symm
  3. L134
    exact hleft_row_witness_witness_right_right_right_witness_witness_witness_left
  4. L135
    specialize succ_ne_zero x4
  5. L136
    apply succ_ne_zero
  6. L137
    exact hbad
  7. L138
    intro b
  8. L139
    intro c
  9. L140
    intro d
  10. L141
    intro e
23Fix variables and assumptionsL142–149

Work with arbitrary variables or the premises of the current implication.

  1. L142
    intro hleft_table
  2. L143
    intro hright_table
  3. L144
    intro hir
  4. L145
    intro his
  5. L146
    intro hbb
  6. L147
    intro hsb
  7. L148
    intro hdb
  8. L149
    intro heb
24Establish hleft_rowL150–153

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hleft table.

  1. L150
    have hleft_row · expand full local formula (605 characters)have hleft_row : ∃ bcf_row_code_bptrpf_left_step. ∃ bcf_row_scale_bptrpf_left_step. BetaAt(bb,bc,S i,bcf_row_code_bptrpf_left_step) ∧ (BetaAt(sb,sc,S i,bcf_row_scale_bptrpf_left_step) ∧ (S i = 0 ∧ (∀ x. Lt(x,w) → ∃ y. BetaAt(bcf_row_code_bptrpf_left_step,bcf_row_scale_bptrpf_left_step,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))) ∨ (∃ x. ∃ y. ∃ z. S i = S x ∧ (BetaAt(bb,bc,x,y) ∧ (BetaAt(sb,sc,x,z) ∧ (∀ n. Lt(n,w) → ∃ m. BetaAt(bcf_row_code_bptrpf_left_step,bcf_row_scale_bptrpf_left_step,n,m) ∧ (n = 0 ∧ m = 1 ∨ (∃ k. ∃ j. ∃ u. n = S k ∧ (BetaAt(y,z,k,j) ∧ (BetaAt(y,z,S k,u) ∧ m = j + u))))))))))
    Definitions: BetaAt(bb,bc,S i,bcf_row_code_bptrpf_left_step)BetaAt(sb,sc,S i,bcf_row_scale_bptrpf_left_step)Lt(x,w)BetaAt(bcf_row_code_bptrpf_left_step,bcf_row_scale_bptrpf_left_step,x,y)BetaAt(bb,bc,x,y)BetaAt(sb,sc,x,z)Lt(n,w)BetaAt(bcf_row_code_bptrpf_left_step,bcf_row_scale_bptrpf_left_step,n,m)BetaAt(y,z,k,j)BetaAt(y,z,S k,u)Original native command in the exact edition
  2. L151
    specialize hleft_table (S i)
  3. L152
    apply hleft_table
  4. L153
    exact hir
25Separate the logical casesL154–157

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L154
    cases hleft_row
  2. L155
    cases hleft_row_witness
  3. L156
    cases hleft_row_witness_witness
  4. L157
    cases hleft_row_witness_witness_right
26Establish hright_rowL158–161

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hright table.

  1. L158
    have hright_row · expand full local formula (614 characters)have hright_row : ∃ bcf_row_code_bptrpf_right_step. ∃ bcf_row_scale_bptrpf_right_step. BetaAt(db,dc,S i,bcf_row_code_bptrpf_right_step) ∧ (BetaAt(eb,ec,S i,bcf_row_scale_bptrpf_right_step) ∧ (S i = 0 ∧ (∀ x. Lt(x,v) → ∃ y. BetaAt(bcf_row_code_bptrpf_right_step,bcf_row_scale_bptrpf_right_step,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))) ∨ (∃ x. ∃ y. ∃ z. S i = S x ∧ (BetaAt(db,dc,x,y) ∧ (BetaAt(eb,ec,x,z) ∧ (∀ n. Lt(n,v) → ∃ m. BetaAt(bcf_row_code_bptrpf_right_step,bcf_row_scale_bptrpf_right_step,n,m) ∧ (n = 0 ∧ m = 1 ∨ (∃ k. ∃ j. ∃ u. n = S k ∧ (BetaAt(y,z,k,j) ∧ (BetaAt(y,z,S k,u) ∧ m = j + u))))))))))
    Definitions: BetaAt(db,dc,S i,bcf_row_code_bptrpf_right_step)BetaAt(eb,ec,S i,bcf_row_scale_bptrpf_right_step)Lt(x,v)BetaAt(bcf_row_code_bptrpf_right_step,bcf_row_scale_bptrpf_right_step,x,y)BetaAt(db,dc,x,y)BetaAt(eb,ec,x,z)Lt(n,v)BetaAt(bcf_row_code_bptrpf_right_step,bcf_row_scale_bptrpf_right_step,n,m)BetaAt(y,z,k,j)BetaAt(y,z,S k,u)Original native command in the exact edition
  2. L159
    specialize hright_table (S i)
  3. L160
    apply hright_table
  4. L161
    exact his
27Separate the logical casesL162–165

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L162
    cases hright_row
  2. L163
    cases hright_row_witness
  3. L164
    cases hright_row_witness_witness
  4. L165
    cases hright_row_witness_witness_right
28Establish hbL166–174

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L166
    have hb : b = x
  2. L167
    specialize beta_at_unique bb
  3. L168
    specialize beta_at_unique bc
  4. L169
    specialize beta_at_unique (S i)
  5. L170
    specialize beta_at_unique b
  6. L171
    specialize beta_at_unique x
  7. L172
    apply beta_at_unique
  8. L173
    exact hbb
  9. L174
    exact hleft_row_witness_witness_left
29Establish hcL175–183

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L175
    have hc : c = x1
  2. L176
    specialize beta_at_unique sb
  3. L177
    specialize beta_at_unique sc
  4. L178
    specialize beta_at_unique (S i)
  5. L179
    specialize beta_at_unique c
  6. L180
    specialize beta_at_unique x1
  7. L181
    apply beta_at_unique
  8. L182
    exact hsb
  9. L183
    exact hleft_row_witness_witness_right_left
30Establish hdL184–192

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L184
    have hd : d = x2
  2. L185
    specialize beta_at_unique db
  3. L186
    specialize beta_at_unique dc
  4. L187
    specialize beta_at_unique (S i)
  5. L188
    specialize beta_at_unique d
  6. L189
    specialize beta_at_unique x2
  7. L190
    apply beta_at_unique
  8. L191
    exact hdb
  9. L192
    exact hright_row_witness_witness_left
31Establish heL193–201

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L193
    have he : e = x3
  2. L194
    specialize beta_at_unique eb
  3. L195
    specialize beta_at_unique ec
  4. L196
    specialize beta_at_unique (S i)
  5. L197
    specialize beta_at_unique e
  6. L198
    specialize beta_at_unique x3
  7. L199
    apply beta_at_unique
  8. L200
    exact heb
  9. L201
    exact hright_row_witness_witness_right_left
32Separate the logical casesL202–204

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L202
    cases hleft_row_witness_witness_right_right
  2. L203
    cases hleft_row_witness_witness_right_right_left
  3. L204
    exfalso
33Use earlier factsL205–207

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L205
    specialize succ_ne_zero i
  2. L206
    apply succ_ne_zero
  3. L207
    exact hleft_row_witness_witness_right_right_left_left
34Separate the logical casesL208–216

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L208
    cases hleft_row_witness_witness_right_right_right
  2. L209
    cases hleft_row_witness_witness_right_right_right_witness
  3. L210
    cases hleft_row_witness_witness_right_right_right_witness_witness
  4. L211
    cases hleft_row_witness_witness_right_right_right_witness_witness_witness
  5. L212
    cases hleft_row_witness_witness_right_right_right_witness_witness_witness_right
  6. L213
    cases hleft_row_witness_witness_right_right_right_witness_witness_witness_right_right
  7. L214
    cases hright_row_witness_witness_right_right
  8. L215
    cases hright_row_witness_witness_right_right_left
  9. L216
    exfalso
35Use earlier factsL217–219

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L217
    specialize succ_ne_zero i
  2. L218
    apply succ_ne_zero
  3. L219
    exact hright_row_witness_witness_right_right_left_left
36Separate the logical casesL220–225

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L220
    cases hright_row_witness_witness_right_right_right
  2. L221
    cases hright_row_witness_witness_right_right_right_witness
  3. L222
    cases hright_row_witness_witness_right_right_right_witness_witness
  4. L223
    cases hright_row_witness_witness_right_right_right_witness_witness_witness
  5. L224
    cases hright_row_witness_witness_right_right_right_witness_witness_witness_right
  6. L225
    cases hright_row_witness_witness_right_right_right_witness_witness_witness_right_right
37Establish hleft_predecessorL226–230

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply succ injective.

  1. L226
    have hleft_predecessor : i = x4
  2. L227
    specialize succ_injective i
  3. L228
    specialize succ_injective x4
  4. L229
    apply succ_injective
  5. L230
    exact hleft_row_witness_witness_right_right_right_witness_witness_witness_left
38Establish hright_predecessorL231–235

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply succ injective.

  1. L231
    have hright_predecessor : i = x7
  2. L232
    specialize succ_injective i
  3. L233
    specialize succ_injective x7
  4. L234
    apply succ_injective
  5. L235
    exact hright_row_witness_witness_right_right_right_witness_witness_witness_left
39Establish hprevious_left_boundL236–240

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt to le.

  1. L236
    have hprevious_left_bound : Lt(i,r)Definitions: Lt(i,r)Original native command in the exact edition
  2. L237
    specialize lt_to_le (S i)
  3. L238
    specialize lt_to_le r
  4. L239
    apply lt_to_le
  5. L240
    exact hir
40Establish hprevious_right_boundL241–245

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt to le.

  1. L241
    have hprevious_right_bound : Lt(i,s)Definitions: Lt(i,s)Original native command in the exact edition
  2. L242
    specialize lt_to_le (S i)
  3. L243
    specialize lt_to_le s
  4. L244
    apply lt_to_le
  5. L245
    exact his
41Establish hprevious_left_codeL246–249

Establish this local claim before using it. It is not an additional assumption.

  1. L246
    have hprevious_left_code : BetaAt(bb,bc,i,x5)Definitions: BetaAt(bb,bc,i,x5)Original native command in the exact edition
  2. L247
    rewrite hleft_predecessor
  3. L248
    rewrite hleft_predecessor
  4. L249
    exact hleft_row_witness_witness_right_right_right_witness_witness_witness_right_left
42Establish hprevious_left_scaleL250–253

Establish this local claim before using it. It is not an additional assumption.

  1. L250
    have hprevious_left_scale : BetaAt(sb,sc,i,x6)Definitions: BetaAt(sb,sc,i,x6)Original native command in the exact edition
  2. L251
    rewrite hleft_predecessor
  3. L252
    rewrite hleft_predecessor
  4. L253
    exact hleft_row_witness_witness_right_right_right_witness_witness_witness_right_right_left
43Establish hprevious_right_codeL254–257

Establish this local claim before using it. It is not an additional assumption.

  1. L254
    have hprevious_right_code : BetaAt(db,dc,i,x8)Definitions: BetaAt(db,dc,i,x8)Original native command in the exact edition
  2. L255
    rewrite hright_predecessor
  3. L256
    rewrite hright_predecessor
  4. L257
    exact hright_row_witness_witness_right_right_right_witness_witness_witness_right_left
44Establish hprevious_right_scaleL258–261

Establish this local claim before using it. It is not an additional assumption.

  1. L258
    have hprevious_right_scale : BetaAt(eb,ec,i,x9)Definitions: BetaAt(eb,ec,i,x9)Original native command in the exact edition
  2. L259
    rewrite hright_predecessor
  3. L260
    rewrite hright_predecessor
  4. L261
    exact hright_row_witness_witness_right_right_right_witness_witness_witness_right_right_left
45Establish hcurrent_semanticL262–271

Establish this local claim before using it. It is not an additional assumption.

  1. L262
    have hcurrent_semantic : ∀ bcf_index_bptrpf_step_semantic_agree. ∀ bcf_left_value_bptrpf_step_semantic_agree. ∀ bcf_right_value_bptrpf_step_semantic_agree. Lt(bcf_index_bptrpf_step_semantic_agree,w) → Lt(bcf_index_bptrpf_step_semantic_agree,v) → BetaAt(x,x1,bcf_index_bptrpf_step_semantic_agree,bcf_left_value_bptrpf_step_semantic_agree) → BetaAt(x2,x3,bcf_index_bptrpf_step_semantic_agree,bcf_right_value_bptrpf_step_semantic_agree) → bcf_left_value_bptrpf_step_semantic_agree = bcf_right_value_bptrpf_step_semantic_agreeDefinitions: Lt(bcf_index_bptrpf_step_semantic_agree,w)Lt(bcf_index_bptrpf_step_semantic_agree,v)BetaAt(x,x1,bcf_index_bptrpf_step_semantic_agree,bcf_left_value_bptrpf_step_semantic_agree)BetaAt(x2,x3,bcf_index_bptrpf_step_semantic_agree,bcf_right_value_bptrpf_step_semantic_agree)Original native command in the exact edition
  2. L263
    specialize beta_pascal_row_step_pointwise_functional x5
  3. L264
    specialize beta_pascal_row_step_pointwise_functional x6
  4. L265
    specialize beta_pascal_row_step_pointwise_functional x8
  5. L266
    specialize beta_pascal_row_step_pointwise_functional x9
  6. L267
    specialize beta_pascal_row_step_pointwise_functional x
  7. L268
    specialize beta_pascal_row_step_pointwise_functional x1
  8. L269
    specialize beta_pascal_row_step_pointwise_functional x2
  9. L270
    specialize beta_pascal_row_step_pointwise_functional x3
  10. L271
    specialize beta_pascal_row_step_pointwise_functional w
46Use earlier factsL272–281

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L272
    specialize beta_pascal_row_step_pointwise_functional v
  2. L273
    apply beta_pascal_row_step_pointwise_functional
  3. L274
    exact hleft_row_witness_witness_right_right_right_witness_witness_witness_right_right_right
  4. L275
    exact hright_row_witness_witness_right_right_right_witness_witness_witness_right_right_right
  5. L276
    specialize IH x5
  6. L277
    specialize IH x6
  7. L278
    specialize IH x8
  8. L279
    specialize IH x9
  9. L280
    apply IH
  10. L281
    exact hleft_table
47Use earlier factsL282–288

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L282
    exact hright_table
  2. L283
    exact hprevious_left_bound
  3. L284
    exact hprevious_right_bound
  4. L285
    exact hprevious_left_code
  5. L286
    exact hprevious_left_scale
  6. L287
    exact hprevious_right_code
  7. L288
    exact hprevious_right_scale
48Fix variables and assumptionsL289–295

Work with arbitrary variables or the premises of the current implication.

  1. L289
    intro j
  2. L290
    intro u
  3. L291
    intro y
  4. L292
    intro hjw
  5. L293
    intro hjv
  6. L294
    intro hleft_entry
  7. L295
    intro hright_entry
49Establish hleft_semanticL296–300

Establish this local claim before using it. It is not an additional assumption.

  1. L296
    have hleft_semantic : BetaAt(x,x1,j,u)Definitions: BetaAt(x,x1,j,u)Original native command in the exact edition
  2. L297
    rewrite <- hb
  3. L298
    rewrite <- hc
  4. L299
    rewrite <- hc
  5. L300
    exact hleft_entry
50Establish hright_semanticL301–310

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hcurrent semantic.

  1. L301
    have hright_semantic : BetaAt(x2,x3,j,y)Definitions: BetaAt(x2,x3,j,y)Original native command in the exact edition
  2. L302
    rewrite <- hd
  3. L303
    rewrite <- he
  4. L304
    rewrite <- he
  5. L305
    exact hright_entry
  6. L306
    specialize hcurrent_semantic j
  7. L307
    specialize hcurrent_semantic u
  8. L308
    specialize hcurrent_semantic y
  9. L309
    apply hcurrent_semantic
  10. L310
    exact hjw
51Use earlier factsL311–313

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L311
    exact hjv
  2. L312
    exact hleft_semantic
  3. L313
    exact hright_semantic

Library-wide reading audit

Original defined command ledger · 313 lines
  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 : ∃ bcf_row_code_bptrpf_left_base. ∃ bcf_row_scale_bptrpf_left_base. BetaAt(bb,bc,0,bcf_row_code_bptrpf_left_base) ∧ (BetaAt(sb,sc,0,bcf_row_scale_bptrpf_left_base) ∧ (0 = 0 ∧ (∀ x. Lt(x,w) → ∃ y. BetaAt(bcf_row_code_bptrpf_left_base,bcf_row_scale_bptrpf_left_base,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))) ∨ (∃ x. ∃ y. ∃ z. 0 = S x ∧ (BetaAt(bb,bc,x,y) ∧ (BetaAt(sb,sc,x,z) ∧ (∀ n. Lt(n,w) → ∃ m. BetaAt(bcf_row_code_bptrpf_left_base,bcf_row_scale_bptrpf_left_base,n,m) ∧ (n = 0 ∧ m = 1 ∨ (∃ k. ∃ i. ∃ j. n = S k ∧ (BetaAt(y,z,k,i) ∧ (BetaAt(y,z,S k,j) ∧ m = i + j))))))))))
    Exact native replay linehave 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 : ∃ bcf_row_code_bptrpf_right_base. ∃ bcf_row_scale_bptrpf_right_base. BetaAt(db,dc,0,bcf_row_code_bptrpf_right_base) ∧ (BetaAt(eb,ec,0,bcf_row_scale_bptrpf_right_base) ∧ (0 = 0 ∧ (∀ x. Lt(x,v) → ∃ y. BetaAt(bcf_row_code_bptrpf_right_base,bcf_row_scale_bptrpf_right_base,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))) ∨ (∃ x. ∃ y. ∃ z. 0 = S x ∧ (BetaAt(db,dc,x,y) ∧ (BetaAt(eb,ec,x,z) ∧ (∀ n. Lt(n,v) → ∃ m. BetaAt(bcf_row_code_bptrpf_right_base,bcf_row_scale_bptrpf_right_base,n,m) ∧ (n = 0 ∧ m = 1 ∨ (∃ k. ∃ i. ∃ j. n = S k ∧ (BetaAt(y,z,k,i) ∧ (BetaAt(y,z,S k,j) ∧ m = i + j))))))))))
    Exact native replay linehave 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 : BetaAt(x,x1,j,u)
    Exact native replay linehave 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 : BetaAt(x2,x3,j,y)
    Exact native replay linehave 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 : ∃ bcf_row_code_bptrpf_left_step. ∃ bcf_row_scale_bptrpf_left_step. BetaAt(bb,bc,S i,bcf_row_code_bptrpf_left_step) ∧ (BetaAt(sb,sc,S i,bcf_row_scale_bptrpf_left_step) ∧ (S i = 0 ∧ (∀ x. Lt(x,w) → ∃ y. BetaAt(bcf_row_code_bptrpf_left_step,bcf_row_scale_bptrpf_left_step,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))) ∨ (∃ x. ∃ y. ∃ z. S i = S x ∧ (BetaAt(bb,bc,x,y) ∧ (BetaAt(sb,sc,x,z) ∧ (∀ n. Lt(n,w) → ∃ m. BetaAt(bcf_row_code_bptrpf_left_step,bcf_row_scale_bptrpf_left_step,n,m) ∧ (n = 0 ∧ m = 1 ∨ (∃ k. ∃ j. ∃ u. n = S k ∧ (BetaAt(y,z,k,j) ∧ (BetaAt(y,z,S k,u) ∧ m = j + u))))))))))
    Exact native replay linehave 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 : ∃ bcf_row_code_bptrpf_right_step. ∃ bcf_row_scale_bptrpf_right_step. BetaAt(db,dc,S i,bcf_row_code_bptrpf_right_step) ∧ (BetaAt(eb,ec,S i,bcf_row_scale_bptrpf_right_step) ∧ (S i = 0 ∧ (∀ x. Lt(x,v) → ∃ y. BetaAt(bcf_row_code_bptrpf_right_step,bcf_row_scale_bptrpf_right_step,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))) ∨ (∃ x. ∃ y. ∃ z. S i = S x ∧ (BetaAt(db,dc,x,y) ∧ (BetaAt(eb,ec,x,z) ∧ (∀ n. Lt(n,v) → ∃ m. BetaAt(bcf_row_code_bptrpf_right_step,bcf_row_scale_bptrpf_right_step,n,m) ∧ (n = 0 ∧ m = 1 ∨ (∃ k. ∃ j. ∃ u. n = S k ∧ (BetaAt(y,z,k,j) ∧ (BetaAt(y,z,S k,u) ∧ m = j + u))))))))))
    Exact native replay linehave 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 : Lt(i,r)
    Exact native replay linehave 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 : Lt(i,s)
    Exact native replay linehave 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 : BetaAt(bb,bc,i,x5)
    Exact native replay linehave 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 : BetaAt(sb,sc,i,x6)
    Exact native replay linehave 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 : BetaAt(db,dc,i,x8)
    Exact native replay linehave 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 : BetaAt(eb,ec,i,x9)
    Exact native replay linehave 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 : ∀ bcf_index_bptrpf_step_semantic_agree. ∀ bcf_left_value_bptrpf_step_semantic_agree. ∀ bcf_right_value_bptrpf_step_semantic_agree. Lt(bcf_index_bptrpf_step_semantic_agree,w) → Lt(bcf_index_bptrpf_step_semantic_agree,v) → BetaAt(x,x1,bcf_index_bptrpf_step_semantic_agree,bcf_left_value_bptrpf_step_semantic_agree) → BetaAt(x2,x3,bcf_index_bptrpf_step_semantic_agree,bcf_right_value_bptrpf_step_semantic_agree) → bcf_left_value_bptrpf_step_semantic_agree = bcf_right_value_bptrpf_step_semantic_agree
    Exact native replay linehave 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 : BetaAt(x,x1,j,u)
    Exact native replay linehave 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 : BetaAt(x2,x3,j,y)
    Exact native replay linehave 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