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
∀ p. ∀ q. ∀ h. ∀ sh. ∀ bb. ∀ bc. ∀ db. ∀ dc. ∀ tb. ∀ tc. ∀ l. ∀ i. ∀ n. ∀ r. ∀ a. (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ m. BetaAt(bb,bc,x,y) ∧ BetaAt(db,dc,x,z) ∧ BetaAt(tb,tc,x,m) ∧ (∃ k. ∃ j. (∀ u. Lt(u,sh) → ∃ v. BetaAt(k,j,u,v) ∧ (v = 0 ∧ (Lt(q · S x,p · S u) ∧ ¬Lt(p · S u,q · S x)) ∨ v = 1 ∧ (Lt(p · S u,q · S x) ∧ ¬Lt(q · S x,p · S u)))) ∧ BitCount(k,j,sh,y) ∧ ((∀ u. Lt(u,h) → ∃ v. BetaAt(k,j,u,v) ∧ (v = 0 ∧ (Lt(q · S x,p · S u) ∧ ¬Lt(p · S u,q · S x)) ∨ v = 1 ∧ (Lt(p · S u,q · S x) ∧ ¬Lt(q · S x,p · S u)))) ∧ BetaAt(k,j,h,m)) ∧ (BitCount(k,j,h,z) ∧ (m = 0 ∨ m = 1) ∧ y = z + m))) → Lt(i,l) → BetaAt(bb,bc,i,n) → BetaAt(db,dc,i,r) → BetaAt(tb,tc,i,a) → n = r + aEvery purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.
Definitions used by this theorem
In the theorem statement
23 occurrences
In local proof propositions
18 occurrences
Exact expanded native-PA statement
forall p q h sh bb bc db dc tb tc l i n r a. (forall efrd_row_index_fubini_row_split_semantic_prefix. (exists efrd_lt_gap_fubini_row_split_semantic_prefix_bound. efrd_lt_gap_fubini_row_split_semantic_prefix_bound + S (efrd_row_index_fubini_row_split_semantic_prefix) = l) -> exists efrd_count_fubini_row_split_semantic_prefix efrd_reduced_count_fubini_row_split_semantic_prefix efrd_terminal_bit_fubini_row_split_semantic_prefix. (((((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_outer_entry. ff_h_efrd_fubini_row_split_semantic_prefix_entry_outer_entry + S (efrd_count_fubini_row_split_semantic_prefix) = S ((S (efrd_row_index_fubini_row_split_semantic_prefix)) * bc)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_outer_entry. bb = ff_q_efrd_fubini_row_split_semantic_prefix_entry_outer_entry * S ((S (efrd_row_index_fubini_row_split_semantic_prefix)) * bc) + (efrd_count_fubini_row_split_semantic_prefix))) /\ (((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_reduced_entry. ff_h_efrd_fubini_row_split_semantic_prefix_entry_reduced_entry + S (efrd_reduced_count_fubini_row_split_semantic_prefix) = S ((S (efrd_row_index_fubini_row_split_semantic_prefix)) * dc)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_reduced_entry. db = ff_q_efrd_fubini_row_split_semantic_prefix_entry_reduced_entry * S ((S (efrd_row_index_fubini_row_split_semantic_prefix)) * dc) + (efrd_reduced_count_fubini_row_split_semantic_prefix)))) /\ (((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_terminal_entry. ff_h_efrd_fubini_row_split_semantic_prefix_entry_terminal_entry + S (efrd_terminal_bit_fubini_row_split_semantic_prefix) = S ((S (efrd_row_index_fubini_row_split_semantic_prefix)) * tc)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_terminal_entry. tb = ff_q_efrd_fubini_row_split_semantic_prefix_entry_terminal_entry * S ((S (efrd_row_index_fubini_row_split_semantic_prefix)) * tc) + (efrd_terminal_bit_fubini_row_split_semantic_prefix)))) /\ (exists efrd_row_code_fubini_row_split_semantic_prefix_entry_split efrd_row_scale_fubini_row_split_semantic_prefix_entry_split. (((((forall eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix. (exists eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_bound. eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_bound + S (eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix) = sh) -> exists eri_bit_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_decoded. ff_h_eri_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_decoded + S (eri_bit_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix) = S ((S (eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split)) /\ exists ff_q_eri_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_decoded. efrd_row_code_fubini_row_split_semantic_prefix_entry_split = ff_q_eri_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split) + (eri_bit_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix))) /\ (((eri_bit_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_semantic_prefix) = p * S eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix) = q * S efrd_row_index_fubini_row_split_semantic_prefix))) \/ (eri_bit_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix) = q * S efrd_row_index_fubini_row_split_semantic_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_semantic_prefix) = p * S eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_successor_prefix))))))) /\ (((exists ff_u_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_start. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_start. ff_u_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_terminal. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_terminal + S (efrd_count_fubini_row_split_semantic_prefix) = S ((S (sh)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_terminal. ff_u_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_terminal * S ((S (sh)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum) + (efrd_count_fubini_row_split_semantic_prefix))) /\ forall ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum. (exists ff_lt_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_bound. ff_lt_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_bound + S ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum = sh) -> exists ff_a_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum ff_r_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum ff_s_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_summand. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_summand + S (ff_a_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_summand. efrd_row_code_fubini_row_split_semantic_prefix_entry_split = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split) + (ff_a_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_partial. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_partial + S (ff_r_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_partial. ff_u_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum) + (ff_r_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_successor. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_successor + S (ff_s_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_successor. ff_u_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum) + (ff_s_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum))) /\ ff_s_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum = ff_r_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum + ff_a_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits. (exists ff_lt_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits_bound. ff_lt_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits_bound + S ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits = sh) -> exists ff_bit_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits. ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits_decoded. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits) = S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits_decoded. efrd_row_code_fubini_row_split_semantic_prefix_entry_split = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split) + (ff_bit_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits))) /\ (ff_bit_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_semantic_prefix_entry_split_successor_count_bits = 1)))))) /\ ((forall eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix. (exists eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_bound. eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_bound + S (eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix) = h) -> exists eri_bit_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_decoded. ff_h_eri_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_decoded + S (eri_bit_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix) = S ((S (eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split)) /\ exists ff_q_eri_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_decoded. efrd_row_code_fubini_row_split_semantic_prefix_entry_split = ff_q_eri_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split) + (eri_bit_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix))) /\ (((eri_bit_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_semantic_prefix) = p * S eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix) = q * S efrd_row_index_fubini_row_split_semantic_prefix))) \/ (eri_bit_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix) = q * S efrd_row_index_fubini_row_split_semantic_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix_choice_left + S (q * S efrd_row_index_fubini_row_split_semantic_prefix) = p * S eri_column_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_prefix))))))) /\ (((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_terminal_entry. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_terminal_entry + S (efrd_terminal_bit_fubini_row_split_semantic_prefix) = S ((S (h)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_terminal_entry. efrd_row_code_fubini_row_split_semantic_prefix_entry_split = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_terminal_entry * S ((S (h)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split) + (efrd_terminal_bit_fubini_row_split_semantic_prefix))))) /\ (((((exists ff_u_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_start. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_start. ff_u_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_terminal. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_terminal + S (efrd_reduced_count_fubini_row_split_semantic_prefix) = S ((S (h)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_terminal. ff_u_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_terminal * S ((S (h)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum) + (efrd_reduced_count_fubini_row_split_semantic_prefix))) /\ forall ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum. (exists ff_lt_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_bound. ff_lt_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_bound + S ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum = h) -> exists ff_a_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum ff_r_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum ff_s_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_summand. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_summand + S (ff_a_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_summand. efrd_row_code_fubini_row_split_semantic_prefix_entry_split = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split) + (ff_a_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_partial. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_partial + S (ff_r_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_partial. ff_u_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum) + (ff_r_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_successor. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_successor + S (ff_s_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_successor. ff_u_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum) + (ff_s_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum))) /\ ff_s_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum = ff_r_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum + ff_a_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits. (exists ff_lt_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits_bound. ff_lt_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits_bound + S ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits = h) -> exists ff_bit_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits. ((((exists ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits_decoded. ff_h_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits) = S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split)) /\ exists ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits_decoded. efrd_row_code_fubini_row_split_semantic_prefix_entry_split = ff_q_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_semantic_prefix_entry_split) + (ff_bit_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits))) /\ (ff_bit_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_semantic_prefix_entry_split_reduced_count_bits = 1))))) /\ (efrd_terminal_bit_fubini_row_split_semantic_prefix = 0 \/ efrd_terminal_bit_fubini_row_split_semantic_prefix = 1)) /\ efrd_count_fubini_row_split_semantic_prefix = efrd_reduced_count_fubini_row_split_semantic_prefix + efrd_terminal_bit_fubini_row_split_semantic_prefix))))))) -> (exists efrd_lt_gap_fubini_row_split_semantic_bound. efrd_lt_gap_fubini_row_split_semantic_bound + S (i) = l) -> (((exists ff_h_fubini_row_split_semantic_source. ff_h_fubini_row_split_semantic_source + S (n) = S ((S (i)) * bc)) /\ exists ff_q_fubini_row_split_semantic_source. bb = ff_q_fubini_row_split_semantic_source * S ((S (i)) * bc) + (n))) -> (((exists ff_h_fubini_row_split_semantic_reduced. ff_h_fubini_row_split_semantic_reduced + S (r) = S ((S (i)) * dc)) /\ exists ff_q_fubini_row_split_semantic_reduced. db = ff_q_fubini_row_split_semantic_reduced * S ((S (i)) * dc) + (r))) -> (((exists ff_h_fubini_row_split_semantic_terminal. ff_h_fubini_row_split_semantic_terminal + S (a) = S ((S (i)) * tc)) /\ exists ff_q_fubini_row_split_semantic_terminal. tb = ff_q_fubini_row_split_semantic_terminal * S ((S (i)) * tc) + (a))) -> n = r + aProof neighborhood
Direct theorem prerequisites
Direct theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.
Read the argument
Proof checkpoints
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.
Named ingredients (1)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–20
03Establish hstoredL21–24
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hprefix.
- L21
have hstored : ∃ storedn. ∃ storedr. ∃ storeda. BetaAt(bb,bc,i,storedn) ∧ BetaAt(db,dc,i,storedr) ∧ BetaAt(tb,tc,i,storeda) ∧ (∃ x. ∃ y. (∀ z. Lt(z,sh) → ∃ n. BetaAt(x,y,z,n) ∧ (n = 0 ∧ (Lt(q · S i,p · S z) ∧ ¬Lt(p · S z,q · S i)) ∨ n = 1 ∧ (Lt(p · S z,q · S i) ∧ ¬Lt(q · S i,p · S z)))) ∧ BitCount(x,y,sh,storedn) ∧ ((∀ z. Lt(z,h) → ∃ n. BetaAt(x,y,z,n) ∧ (n = 0 ∧ (Lt(q · S i,p · S z) ∧ ¬Lt(p · S z,q · S i)) ∨ n = 1 ∧ (Lt(p · S z,q · S i) ∧ ¬Lt(q · S i,p · S z)))) ∧ BetaAt(x,y,h,storeda)) ∧ (BitCount(x,y,h,storedr) ∧ (storeda = 0 ∨ storeda = 1) ∧ storedn = storedr + storeda))Definitions: BetaAt(bb,bc,i,storedn)BetaAt(db,dc,i,storedr)BetaAt(tb,tc,i,storeda)Lt(z,sh)BetaAt(x,y,z,n)Lt(q · S i,p · S z)Lt(p · S z,q · S i)BitCount(x,y,sh,storedn)Lt(z,h)BetaAt(x,y,h,storeda)BitCount(x,y,h,storedr)Original native command in the exact edition - L22
specialize hprefix i - L23
apply hprefix - L24
exact hi
04Separate the logical casesL25–30
05Establish hsource_eqL31–39
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
06Establish hreduced_eqL40–48
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
07Establish hterminal_eqL49–57
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
08Separate the logical casesL58–61
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
Original defined command ledger · 67 lines
- 0001
intro p - 0002
intro q - 0003
intro h - 0004
intro sh - 0005
intro bb - 0006
intro bc - 0007
intro db - 0008
intro dc - 0009
intro tb - 0010
intro tc - 0011
intro l - 0012
intro i - 0013
intro n - 0014
intro r - 0015
intro a - 0016
intro hprefix - 0017
intro hi - 0018
intro hn - 0019
intro hr - 0020
intro ha - 0021
have hstored : ∃ storedn. ∃ storedr. ∃ storeda. BetaAt(bb,bc,i,storedn) ∧ BetaAt(db,dc,i,storedr) ∧ BetaAt(tb,tc,i,storeda) ∧ (∃ x. ∃ y. (∀ z. Lt(z,sh) → ∃ n. BetaAt(x,y,z,n) ∧ (n = 0 ∧ (Lt(q · S i,p · S z) ∧ ¬Lt(p · S z,q · S i)) ∨ n = 1 ∧ (Lt(p · S z,q · S i) ∧ ¬Lt(q · S i,p · S z)))) ∧ BitCount(x,y,sh,storedn) ∧ ((∀ z. Lt(z,h) → ∃ n. BetaAt(x,y,z,n) ∧ (n = 0 ∧ (Lt(q · S i,p · S z) ∧ ¬Lt(p · S z,q · S i)) ∨ n = 1 ∧ (Lt(p · S z,q · S i) ∧ ¬Lt(q · S i,p · S z)))) ∧ BetaAt(x,y,h,storeda)) ∧ (BitCount(x,y,h,storedr) ∧ (storeda = 0 ∨ storeda = 1) ∧ storedn = storedr + storeda))Exact native replay line
have hstored : exists storedn storedr storeda. (((((((exists ff_h_efrd_fubini_row_split_semantic_stored_outer_entry. ff_h_efrd_fubini_row_split_semantic_stored_outer_entry + S (storedn) = S ((S (i)) * bc)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_outer_entry. bb = ff_q_efrd_fubini_row_split_semantic_stored_outer_entry * S ((S (i)) * bc) + (storedn))) /\ (((exists ff_h_efrd_fubini_row_split_semantic_stored_reduced_entry. ff_h_efrd_fubini_row_split_semantic_stored_reduced_entry + S (storedr) = S ((S (i)) * dc)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_reduced_entry. db = ff_q_efrd_fubini_row_split_semantic_stored_reduced_entry * S ((S (i)) * dc) + (storedr)))) /\ (((exists ff_h_efrd_fubini_row_split_semantic_stored_terminal_entry. ff_h_efrd_fubini_row_split_semantic_stored_terminal_entry + S (storeda) = S ((S (i)) * tc)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_terminal_entry. tb = ff_q_efrd_fubini_row_split_semantic_stored_terminal_entry * S ((S (i)) * tc) + (storeda)))) /\ (exists efrd_row_code_fubini_row_split_semantic_stored_split efrd_row_scale_fubini_row_split_semantic_stored_split. (((((forall eri_column_efrd_fubini_row_split_semantic_stored_split_successor_prefix. (exists eri_gap_efrd_fubini_row_split_semantic_stored_split_successor_prefix_bound. eri_gap_efrd_fubini_row_split_semantic_stored_split_successor_prefix_bound + S (eri_column_efrd_fubini_row_split_semantic_stored_split_successor_prefix) = sh) -> exists eri_bit_efrd_fubini_row_split_semantic_stored_split_successor_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_semantic_stored_split_successor_prefix_decoded. ff_h_eri_efrd_fubini_row_split_semantic_stored_split_successor_prefix_decoded + S (eri_bit_efrd_fubini_row_split_semantic_stored_split_successor_prefix) = S ((S (eri_column_efrd_fubini_row_split_semantic_stored_split_successor_prefix)) * efrd_row_scale_fubini_row_split_semantic_stored_split)) /\ exists ff_q_eri_efrd_fubini_row_split_semantic_stored_split_successor_prefix_decoded. efrd_row_code_fubini_row_split_semantic_stored_split = ff_q_eri_efrd_fubini_row_split_semantic_stored_split_successor_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_semantic_stored_split_successor_prefix)) * efrd_row_scale_fubini_row_split_semantic_stored_split) + (eri_bit_efrd_fubini_row_split_semantic_stored_split_successor_prefix))) /\ (((eri_bit_efrd_fubini_row_split_semantic_stored_split_successor_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_semantic_stored_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_semantic_stored_split_successor_prefix_choice_left + S (q * S i) = p * S eri_column_efrd_fubini_row_split_semantic_stored_split_successor_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_semantic_stored_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_semantic_stored_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_semantic_stored_split_successor_prefix) = q * S i))) \/ (eri_bit_efrd_fubini_row_split_semantic_stored_split_successor_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_semantic_stored_split_successor_prefix_choice_right. eri_gap_efrd_fubini_row_split_semantic_stored_split_successor_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_semantic_stored_split_successor_prefix) = q * S i) /\ ~(exists eri_gap_efrd_fubini_row_split_semantic_stored_split_successor_prefix_choice_left. eri_gap_efrd_fubini_row_split_semantic_stored_split_successor_prefix_choice_left + S (q * S i) = p * S eri_column_efrd_fubini_row_split_semantic_stored_split_successor_prefix))))))) /\ (((exists ff_u_efrd_fubini_row_split_semantic_stored_split_successor_count_sum ff_v_efrd_fubini_row_split_semantic_stored_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_start. ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_start. ff_u_efrd_fubini_row_split_semantic_stored_split_successor_count_sum = ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_semantic_stored_split_successor_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_terminal. ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_terminal + S (storedn) = S ((S (sh)) * ff_v_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_terminal. ff_u_efrd_fubini_row_split_semantic_stored_split_successor_count_sum = ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_terminal * S ((S (sh)) * ff_v_efrd_fubini_row_split_semantic_stored_split_successor_count_sum) + (storedn))) /\ forall ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_sum. (exists ff_lt_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_bound. ff_lt_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_bound + S ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_sum = sh) -> exists ff_a_efrd_fubini_row_split_semantic_stored_split_successor_count_sum ff_r_efrd_fubini_row_split_semantic_stored_split_successor_count_sum ff_s_efrd_fubini_row_split_semantic_stored_split_successor_count_sum. ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_summand. ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_summand + S (ff_a_efrd_fubini_row_split_semantic_stored_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_semantic_stored_split)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_summand. efrd_row_code_fubini_row_split_semantic_stored_split = ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)) * efrd_row_scale_fubini_row_split_semantic_stored_split) + (ff_a_efrd_fubini_row_split_semantic_stored_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_partial. ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_partial + S (ff_r_efrd_fubini_row_split_semantic_stored_split_successor_count_sum) = S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_partial. ff_u_efrd_fubini_row_split_semantic_stored_split_successor_count_sum = ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_semantic_stored_split_successor_count_sum) + (ff_r_efrd_fubini_row_split_semantic_stored_split_successor_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_successor. ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_successor + S (ff_s_efrd_fubini_row_split_semantic_stored_split_successor_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_successor. ff_u_efrd_fubini_row_split_semantic_stored_split_successor_count_sum = ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)) * ff_v_efrd_fubini_row_split_semantic_stored_split_successor_count_sum) + (ff_s_efrd_fubini_row_split_semantic_stored_split_successor_count_sum))) /\ ff_s_efrd_fubini_row_split_semantic_stored_split_successor_count_sum = ff_r_efrd_fubini_row_split_semantic_stored_split_successor_count_sum + ff_a_efrd_fubini_row_split_semantic_stored_split_successor_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_bits. (exists ff_lt_efrd_fubini_row_split_semantic_stored_split_successor_count_bits_bound. ff_lt_efrd_fubini_row_split_semantic_stored_split_successor_count_bits_bound + S ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_bits = sh) -> exists ff_bit_efrd_fubini_row_split_semantic_stored_split_successor_count_bits. ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_bits_decoded. ff_h_efrd_fubini_row_split_semantic_stored_split_successor_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_semantic_stored_split_successor_count_bits) = S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_semantic_stored_split)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_bits_decoded. efrd_row_code_fubini_row_split_semantic_stored_split = ff_q_efrd_fubini_row_split_semantic_stored_split_successor_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_successor_count_bits)) * efrd_row_scale_fubini_row_split_semantic_stored_split) + (ff_bit_efrd_fubini_row_split_semantic_stored_split_successor_count_bits))) /\ (ff_bit_efrd_fubini_row_split_semantic_stored_split_successor_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_semantic_stored_split_successor_count_bits = 1)))))) /\ ((forall eri_column_efrd_fubini_row_split_semantic_stored_split_reduced_prefix. (exists eri_gap_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_bound. eri_gap_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_bound + S (eri_column_efrd_fubini_row_split_semantic_stored_split_reduced_prefix) = h) -> exists eri_bit_efrd_fubini_row_split_semantic_stored_split_reduced_prefix. ((((exists ff_h_eri_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_decoded. ff_h_eri_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_decoded + S (eri_bit_efrd_fubini_row_split_semantic_stored_split_reduced_prefix) = S ((S (eri_column_efrd_fubini_row_split_semantic_stored_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_semantic_stored_split)) /\ exists ff_q_eri_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_decoded. efrd_row_code_fubini_row_split_semantic_stored_split = ff_q_eri_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_decoded * S ((S (eri_column_efrd_fubini_row_split_semantic_stored_split_reduced_prefix)) * efrd_row_scale_fubini_row_split_semantic_stored_split) + (eri_bit_efrd_fubini_row_split_semantic_stored_split_reduced_prefix))) /\ (((eri_bit_efrd_fubini_row_split_semantic_stored_split_reduced_prefix = 0 /\ ((exists eri_gap_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_choice_left + S (q * S i) = p * S eri_column_efrd_fubini_row_split_semantic_stored_split_reduced_prefix) /\ ~(exists eri_gap_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_semantic_stored_split_reduced_prefix) = q * S i))) \/ (eri_bit_efrd_fubini_row_split_semantic_stored_split_reduced_prefix = 1 /\ ((exists eri_gap_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_choice_right. eri_gap_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_choice_right + S (p * S eri_column_efrd_fubini_row_split_semantic_stored_split_reduced_prefix) = q * S i) /\ ~(exists eri_gap_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_choice_left. eri_gap_efrd_fubini_row_split_semantic_stored_split_reduced_prefix_choice_left + S (q * S i) = p * S eri_column_efrd_fubini_row_split_semantic_stored_split_reduced_prefix))))))) /\ (((exists ff_h_efrd_fubini_row_split_semantic_stored_split_terminal_entry. ff_h_efrd_fubini_row_split_semantic_stored_split_terminal_entry + S (storeda) = S ((S (h)) * efrd_row_scale_fubini_row_split_semantic_stored_split)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_terminal_entry. efrd_row_code_fubini_row_split_semantic_stored_split = ff_q_efrd_fubini_row_split_semantic_stored_split_terminal_entry * S ((S (h)) * efrd_row_scale_fubini_row_split_semantic_stored_split) + (storeda))))) /\ (((((exists ff_u_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum ff_v_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_start. ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_start + S (0) = S ((S (0)) * ff_v_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_start. ff_u_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum = ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_start * S ((S (0)) * ff_v_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum) + (0))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_terminal. ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_terminal + S (storedr) = S ((S (h)) * ff_v_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_terminal. ff_u_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum = ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_terminal * S ((S (h)) * ff_v_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum) + (storedr))) /\ forall ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum. (exists ff_lt_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_bound. ff_lt_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_bound + S ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum = h) -> exists ff_a_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum ff_r_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum ff_s_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum. ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_summand. ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_summand + S (ff_a_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_semantic_stored_split)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_summand. efrd_row_code_fubini_row_split_semantic_stored_split = ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_summand * S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)) * efrd_row_scale_fubini_row_split_semantic_stored_split) + (ff_a_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_partial. ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_partial + S (ff_r_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum) = S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_partial. ff_u_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum = ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_partial * S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum) + (ff_r_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum))) /\ ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_successor. ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_successor + S (ff_s_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum) = S ((S (S ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_successor. ff_u_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum = ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum_successor * S ((S (S ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)) * ff_v_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum) + (ff_s_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum))) /\ ff_s_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum = ff_r_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum + ff_a_efrd_fubini_row_split_semantic_stored_split_reduced_count_sum)))))) /\ (forall ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits. (exists ff_lt_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits_bound. ff_lt_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits_bound + S ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits = h) -> exists ff_bit_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits. ((((exists ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits_decoded. ff_h_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits_decoded + S (ff_bit_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits) = S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_semantic_stored_split)) /\ exists ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits_decoded. efrd_row_code_fubini_row_split_semantic_stored_split = ff_q_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits_decoded * S ((S (ff_i_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits)) * efrd_row_scale_fubini_row_split_semantic_stored_split) + (ff_bit_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits))) /\ (ff_bit_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits = 0 \/ ff_bit_efrd_fubini_row_split_semantic_stored_split_reduced_count_bits = 1))))) /\ (storeda = 0 \/ storeda = 1)) /\ storedn = storedr + storeda)))))) - 0022
specialize hprefix i - 0023
apply hprefix - 0024
exact hi - 0025
cases hstored - 0026
cases hstored_witness - 0027
cases hstored_witness_witness - 0028
cases hstored_witness_witness_witness - 0029
cases hstored_witness_witness_witness_left - 0030
cases hstored_witness_witness_witness_left_left - 0031
have hsource_eq : x = n - 0032
specialize beta_at_unique bb - 0033
specialize beta_at_unique bc - 0034
specialize beta_at_unique i - 0035
specialize beta_at_unique x - 0036
specialize beta_at_unique n - 0037
apply beta_at_unique - 0038
exact hstored_witness_witness_witness_left_left_left - 0039
exact hn - 0040
have hreduced_eq : x1 = r - 0041
specialize beta_at_unique db - 0042
specialize beta_at_unique dc - 0043
specialize beta_at_unique i - 0044
specialize beta_at_unique x1 - 0045
specialize beta_at_unique r - 0046
apply beta_at_unique - 0047
exact hstored_witness_witness_witness_left_left_right - 0048
exact hr - 0049
have hterminal_eq : x2 = a - 0050
specialize beta_at_unique tb - 0051
specialize beta_at_unique tc - 0052
specialize beta_at_unique i - 0053
specialize beta_at_unique x2 - 0054
specialize beta_at_unique a - 0055
apply beta_at_unique - 0056
exact hstored_witness_witness_witness_left_right - 0057
exact ha - 0058
cases hstored_witness_witness_witness_right - 0059
cases hstored_witness_witness_witness_right_witness - 0060
cases hstored_witness_witness_witness_right_witness_witness - 0061
cases hstored_witness_witness_witness_right_witness_witness_right - 0062
have heq : x = x1 + x2 - 0063
exact hstored_witness_witness_witness_right_witness_witness_right_right - 0064
rewrite hsource_eq at heq - 0065
rewrite hreduced_eq at heq - 0066
rewrite hterminal_eq at heq - 0067
exact heq