DU0005

dirichlet_constant_one_table_append

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Actually append signed one at the next positive index by paired beta recoding, preserving the full previous prefix including zero.

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 expanded first-order arithmetic statement

forall N U. (((exists dst_positive_code_one_append_inputtable dst_positive_scale_one_append_inputtable dst_negative_code_one_append_inputtable dst_negative_scale_one_append_inputtable. (((U) = (((((dst_positive_code_one_append_inputtable) + (dst_positive_scale_one_append_inputtable)) * S ((dst_positive_code_one_append_inputtable) + (dst_positive_scale_one_append_inputtable)) + ((dst_positive_scale_one_append_inputtable) + (dst_positive_scale_one_append_inputtable))) + (((dst_negative_code_one_append_inputtable) + (dst_negative_scale_one_append_inputtable)) * S ((dst_negative_code_one_append_inputtable) + (dst_negative_scale_one_append_inputtable)) + ((dst_negative_scale_one_append_inputtable) + (dst_negative_scale_one_append_inputtable)))) * S ((((dst_positive_code_one_append_inputtable) + (dst_positive_scale_one_append_inputtable)) * S ((dst_positive_code_one_append_inputtable) + (dst_positive_scale_one_append_inputtable)) + ((dst_positive_scale_one_append_inputtable) + (dst_positive_scale_one_append_inputtable))) + (((dst_negative_code_one_append_inputtable) + (dst_negative_scale_one_append_inputtable)) * S ((dst_negative_code_one_append_inputtable) + (dst_negative_scale_one_append_inputtable)) + ((dst_negative_scale_one_append_inputtable) + (dst_negative_scale_one_append_inputtable)))) + ((((dst_negative_code_one_append_inputtable) + (dst_negative_scale_one_append_inputtable)) * S ((dst_negative_code_one_append_inputtable) + (dst_negative_scale_one_append_inputtable)) + ((dst_negative_scale_one_append_inputtable) + (dst_negative_scale_one_append_inputtable))) + (((dst_negative_code_one_append_inputtable) + (dst_negative_scale_one_append_inputtable)) * S ((dst_negative_code_one_append_inputtable) + (dst_negative_scale_one_append_inputtable)) + ((dst_negative_scale_one_append_inputtable) + (dst_negative_scale_one_append_inputtable)))))) /\ (forall dst_index_one_append_inputtable. (exists pvs_le_gap_one_append_inputtabledomain. pvs_le_gap_one_append_inputtabledomain + (dst_index_one_append_inputtable) = (N)) -> exists dst_positive_one_append_inputtable dst_negative_one_append_inputtable dst_value_one_append_inputtable. ((((exists ff_h_pvs_one_append_inputtableentrypositive. ff_h_pvs_one_append_inputtableentrypositive + S (dst_positive_one_append_inputtable) = S ((S (dst_index_one_append_inputtable)) * dst_positive_scale_one_append_inputtable)) /\ exists ff_q_pvs_one_append_inputtableentrypositive. dst_positive_code_one_append_inputtable = ff_q_pvs_one_append_inputtableentrypositive * S ((S (dst_index_one_append_inputtable)) * dst_positive_scale_one_append_inputtable) + (dst_positive_one_append_inputtable))) /\ (((((exists ff_h_pvs_one_append_inputtableentrynegative. ff_h_pvs_one_append_inputtableentrynegative + S (dst_negative_one_append_inputtable) = S ((S (dst_index_one_append_inputtable)) * dst_negative_scale_one_append_inputtable)) /\ exists ff_q_pvs_one_append_inputtableentrynegative. dst_negative_code_one_append_inputtable = ff_q_pvs_one_append_inputtableentrynegative * S ((S (dst_index_one_append_inputtable)) * dst_negative_scale_one_append_inputtable) + (dst_negative_one_append_inputtable))) /\ (exists ge_balance_positive_one_append_inputtableentryvalue ge_balance_negative_one_append_inputtableentryvalue. (((((dst_value_one_append_inputtable) = 2 * (ge_balance_positive_one_append_inputtableentryvalue) /\ (ge_balance_negative_one_append_inputtableentryvalue) = 0) \/ exists ge_signed_half_one_append_inputtableentryvaluedecode. (((dst_value_one_append_inputtable) = 2 * ge_signed_half_one_append_inputtableentryvaluedecode + 1 /\ (ge_balance_positive_one_append_inputtableentryvalue) = 0) /\ (ge_balance_negative_one_append_inputtableentryvalue) = S ge_signed_half_one_append_inputtableentryvaluedecode))) /\ ((dst_positive_one_append_inputtable) + ge_balance_negative_one_append_inputtableentryvalue = (dst_negative_one_append_inputtable) + ge_balance_positive_one_append_inputtableentryvalue))))))))) /\ (forall du_index_one_append_input du_value_one_append_input. ~(du_index_one_append_input=0) -> (exists pvs_le_gap_one_append_inputbound. pvs_le_gap_one_append_inputbound + (du_index_one_append_input) = (N)) -> (exists dst_positive_code_one_append_inputentry dst_positive_scale_one_append_inputentry dst_negative_code_one_append_inputentry dst_negative_scale_one_append_inputentry dst_positive_one_append_inputentry dst_negative_one_append_inputentry. (((U) = (((((dst_positive_code_one_append_inputentry) + (dst_positive_scale_one_append_inputentry)) * S ((dst_positive_code_one_append_inputentry) + (dst_positive_scale_one_append_inputentry)) + ((dst_positive_scale_one_append_inputentry) + (dst_positive_scale_one_append_inputentry))) + (((dst_negative_code_one_append_inputentry) + (dst_negative_scale_one_append_inputentry)) * S ((dst_negative_code_one_append_inputentry) + (dst_negative_scale_one_append_inputentry)) + ((dst_negative_scale_one_append_inputentry) + (dst_negative_scale_one_append_inputentry)))) * S ((((dst_positive_code_one_append_inputentry) + (dst_positive_scale_one_append_inputentry)) * S ((dst_positive_code_one_append_inputentry) + (dst_positive_scale_one_append_inputentry)) + ((dst_positive_scale_one_append_inputentry) + (dst_positive_scale_one_append_inputentry))) + (((dst_negative_code_one_append_inputentry) + (dst_negative_scale_one_append_inputentry)) * S ((dst_negative_code_one_append_inputentry) + (dst_negative_scale_one_append_inputentry)) + ((dst_negative_scale_one_append_inputentry) + (dst_negative_scale_one_append_inputentry)))) + ((((dst_negative_code_one_append_inputentry) + (dst_negative_scale_one_append_inputentry)) * S ((dst_negative_code_one_append_inputentry) + (dst_negative_scale_one_append_inputentry)) + ((dst_negative_scale_one_append_inputentry) + (dst_negative_scale_one_append_inputentry))) + (((dst_negative_code_one_append_inputentry) + (dst_negative_scale_one_append_inputentry)) * S ((dst_negative_code_one_append_inputentry) + (dst_negative_scale_one_append_inputentry)) + ((dst_negative_scale_one_append_inputentry) + (dst_negative_scale_one_append_inputentry)))))) /\ (((((exists ff_h_pvs_one_append_inputentrypositive. ff_h_pvs_one_append_inputentrypositive + S (dst_positive_one_append_inputentry) = S ((S (du_index_one_append_input)) * dst_positive_scale_one_append_inputentry)) /\ exists ff_q_pvs_one_append_inputentrypositive. dst_positive_code_one_append_inputentry = ff_q_pvs_one_append_inputentrypositive * S ((S (du_index_one_append_input)) * dst_positive_scale_one_append_inputentry) + (dst_positive_one_append_inputentry))) /\ (((((exists ff_h_pvs_one_append_inputentrynegative. ff_h_pvs_one_append_inputentrynegative + S (dst_negative_one_append_inputentry) = S ((S (du_index_one_append_input)) * dst_negative_scale_one_append_inputentry)) /\ exists ff_q_pvs_one_append_inputentrynegative. dst_negative_code_one_append_inputentry = ff_q_pvs_one_append_inputentrynegative * S ((S (du_index_one_append_input)) * dst_negative_scale_one_append_inputentry) + (dst_negative_one_append_inputentry))) /\ (exists ge_balance_positive_one_append_inputentryvalue ge_balance_negative_one_append_inputentryvalue. (((((du_value_one_append_input) = 2 * (ge_balance_positive_one_append_inputentryvalue) /\ (ge_balance_negative_one_append_inputentryvalue) = 0) \/ exists ge_signed_half_one_append_inputentryvaluedecode. (((du_value_one_append_input) = 2 * ge_signed_half_one_append_inputentryvaluedecode + 1 /\ (ge_balance_positive_one_append_inputentryvalue) = 0) /\ (ge_balance_negative_one_append_inputentryvalue) = S ge_signed_half_one_append_inputentryvaluedecode))) /\ ((dst_positive_one_append_inputentry) + ge_balance_negative_one_append_inputentryvalue = (dst_negative_one_append_inputentry) + ge_balance_positive_one_append_inputentryvalue))))))))) -> du_value_one_append_input=2))) -> exists V. (((exists dst_positive_code_one_append_outputtable dst_positive_scale_one_append_outputtable dst_negative_code_one_append_outputtable dst_negative_scale_one_append_outputtable. (((V) = (((((dst_positive_code_one_append_outputtable) + (dst_positive_scale_one_append_outputtable)) * S ((dst_positive_code_one_append_outputtable) + (dst_positive_scale_one_append_outputtable)) + ((dst_positive_scale_one_append_outputtable) + (dst_positive_scale_one_append_outputtable))) + (((dst_negative_code_one_append_outputtable) + (dst_negative_scale_one_append_outputtable)) * S ((dst_negative_code_one_append_outputtable) + (dst_negative_scale_one_append_outputtable)) + ((dst_negative_scale_one_append_outputtable) + (dst_negative_scale_one_append_outputtable)))) * S ((((dst_positive_code_one_append_outputtable) + (dst_positive_scale_one_append_outputtable)) * S ((dst_positive_code_one_append_outputtable) + (dst_positive_scale_one_append_outputtable)) + ((dst_positive_scale_one_append_outputtable) + (dst_positive_scale_one_append_outputtable))) + (((dst_negative_code_one_append_outputtable) + (dst_negative_scale_one_append_outputtable)) * S ((dst_negative_code_one_append_outputtable) + (dst_negative_scale_one_append_outputtable)) + ((dst_negative_scale_one_append_outputtable) + (dst_negative_scale_one_append_outputtable)))) + ((((dst_negative_code_one_append_outputtable) + (dst_negative_scale_one_append_outputtable)) * S ((dst_negative_code_one_append_outputtable) + (dst_negative_scale_one_append_outputtable)) + ((dst_negative_scale_one_append_outputtable) + (dst_negative_scale_one_append_outputtable))) + (((dst_negative_code_one_append_outputtable) + (dst_negative_scale_one_append_outputtable)) * S ((dst_negative_code_one_append_outputtable) + (dst_negative_scale_one_append_outputtable)) + ((dst_negative_scale_one_append_outputtable) + (dst_negative_scale_one_append_outputtable)))))) /\ (forall dst_index_one_append_outputtable. (exists pvs_le_gap_one_append_outputtabledomain. pvs_le_gap_one_append_outputtabledomain + (dst_index_one_append_outputtable) = (S N)) -> exists dst_positive_one_append_outputtable dst_negative_one_append_outputtable dst_value_one_append_outputtable. ((((exists ff_h_pvs_one_append_outputtableentrypositive. ff_h_pvs_one_append_outputtableentrypositive + S (dst_positive_one_append_outputtable) = S ((S (dst_index_one_append_outputtable)) * dst_positive_scale_one_append_outputtable)) /\ exists ff_q_pvs_one_append_outputtableentrypositive. dst_positive_code_one_append_outputtable = ff_q_pvs_one_append_outputtableentrypositive * S ((S (dst_index_one_append_outputtable)) * dst_positive_scale_one_append_outputtable) + (dst_positive_one_append_outputtable))) /\ (((((exists ff_h_pvs_one_append_outputtableentrynegative. ff_h_pvs_one_append_outputtableentrynegative + S (dst_negative_one_append_outputtable) = S ((S (dst_index_one_append_outputtable)) * dst_negative_scale_one_append_outputtable)) /\ exists ff_q_pvs_one_append_outputtableentrynegative. dst_negative_code_one_append_outputtable = ff_q_pvs_one_append_outputtableentrynegative * S ((S (dst_index_one_append_outputtable)) * dst_negative_scale_one_append_outputtable) + (dst_negative_one_append_outputtable))) /\ (exists ge_balance_positive_one_append_outputtableentryvalue ge_balance_negative_one_append_outputtableentryvalue. (((((dst_value_one_append_outputtable) = 2 * (ge_balance_positive_one_append_outputtableentryvalue) /\ (ge_balance_negative_one_append_outputtableentryvalue) = 0) \/ exists ge_signed_half_one_append_outputtableentryvaluedecode. (((dst_value_one_append_outputtable) = 2 * ge_signed_half_one_append_outputtableentryvaluedecode + 1 /\ (ge_balance_positive_one_append_outputtableentryvalue) = 0) /\ (ge_balance_negative_one_append_outputtableentryvalue) = S ge_signed_half_one_append_outputtableentryvaluedecode))) /\ ((dst_positive_one_append_outputtable) + ge_balance_negative_one_append_outputtableentryvalue = (dst_negative_one_append_outputtable) + ge_balance_positive_one_append_outputtableentryvalue))))))))) /\ (forall du_index_one_append_output du_value_one_append_output. ~(du_index_one_append_output=0) -> (exists pvs_le_gap_one_append_outputbound. pvs_le_gap_one_append_outputbound + (du_index_one_append_output) = (S N)) -> (exists dst_positive_code_one_append_outputentry dst_positive_scale_one_append_outputentry dst_negative_code_one_append_outputentry dst_negative_scale_one_append_outputentry dst_positive_one_append_outputentry dst_negative_one_append_outputentry. (((V) = (((((dst_positive_code_one_append_outputentry) + (dst_positive_scale_one_append_outputentry)) * S ((dst_positive_code_one_append_outputentry) + (dst_positive_scale_one_append_outputentry)) + ((dst_positive_scale_one_append_outputentry) + (dst_positive_scale_one_append_outputentry))) + (((dst_negative_code_one_append_outputentry) + (dst_negative_scale_one_append_outputentry)) * S ((dst_negative_code_one_append_outputentry) + (dst_negative_scale_one_append_outputentry)) + ((dst_negative_scale_one_append_outputentry) + (dst_negative_scale_one_append_outputentry)))) * S ((((dst_positive_code_one_append_outputentry) + (dst_positive_scale_one_append_outputentry)) * S ((dst_positive_code_one_append_outputentry) + (dst_positive_scale_one_append_outputentry)) + ((dst_positive_scale_one_append_outputentry) + (dst_positive_scale_one_append_outputentry))) + (((dst_negative_code_one_append_outputentry) + (dst_negative_scale_one_append_outputentry)) * S ((dst_negative_code_one_append_outputentry) + (dst_negative_scale_one_append_outputentry)) + ((dst_negative_scale_one_append_outputentry) + (dst_negative_scale_one_append_outputentry)))) + ((((dst_negative_code_one_append_outputentry) + (dst_negative_scale_one_append_outputentry)) * S ((dst_negative_code_one_append_outputentry) + (dst_negative_scale_one_append_outputentry)) + ((dst_negative_scale_one_append_outputentry) + (dst_negative_scale_one_append_outputentry))) + (((dst_negative_code_one_append_outputentry) + (dst_negative_scale_one_append_outputentry)) * S ((dst_negative_code_one_append_outputentry) + (dst_negative_scale_one_append_outputentry)) + ((dst_negative_scale_one_append_outputentry) + (dst_negative_scale_one_append_outputentry)))))) /\ (((((exists ff_h_pvs_one_append_outputentrypositive. ff_h_pvs_one_append_outputentrypositive + S (dst_positive_one_append_outputentry) = S ((S (du_index_one_append_output)) * dst_positive_scale_one_append_outputentry)) /\ exists ff_q_pvs_one_append_outputentrypositive. dst_positive_code_one_append_outputentry = ff_q_pvs_one_append_outputentrypositive * S ((S (du_index_one_append_output)) * dst_positive_scale_one_append_outputentry) + (dst_positive_one_append_outputentry))) /\ (((((exists ff_h_pvs_one_append_outputentrynegative. ff_h_pvs_one_append_outputentrynegative + S (dst_negative_one_append_outputentry) = S ((S (du_index_one_append_output)) * dst_negative_scale_one_append_outputentry)) /\ exists ff_q_pvs_one_append_outputentrynegative. dst_negative_code_one_append_outputentry = ff_q_pvs_one_append_outputentrynegative * S ((S (du_index_one_append_output)) * dst_negative_scale_one_append_outputentry) + (dst_negative_one_append_outputentry))) /\ (exists ge_balance_positive_one_append_outputentryvalue ge_balance_negative_one_append_outputentryvalue. (((((du_value_one_append_output) = 2 * (ge_balance_positive_one_append_outputentryvalue) /\ (ge_balance_negative_one_append_outputentryvalue) = 0) \/ exists ge_signed_half_one_append_outputentryvaluedecode. (((du_value_one_append_output) = 2 * ge_signed_half_one_append_outputentryvaluedecode + 1 /\ (ge_balance_positive_one_append_outputentryvalue) = 0) /\ (ge_balance_negative_one_append_outputentryvalue) = S ge_signed_half_one_append_outputentryvaluedecode))) /\ ((dst_positive_one_append_outputentry) + ge_balance_negative_one_append_outputentryvalue = (dst_negative_one_append_outputentry) + ge_balance_positive_one_append_outputentryvalue))))))))) -> du_value_one_append_output=2))) /\ (forall dst_index_one_append_prefix dst_first_one_append_prefix dst_second_one_append_prefix. (exists pvs_gap_one_append_prefixbound. pvs_gap_one_append_prefixbound + S (dst_index_one_append_prefix) = (S N)) -> (exists dst_positive_code_one_append_prefixfirst dst_positive_scale_one_append_prefixfirst dst_negative_code_one_append_prefixfirst dst_negative_scale_one_append_prefixfirst dst_positive_one_append_prefixfirst dst_negative_one_append_prefixfirst. (((U) = (((((dst_positive_code_one_append_prefixfirst) + (dst_positive_scale_one_append_prefixfirst)) * S ((dst_positive_code_one_append_prefixfirst) + (dst_positive_scale_one_append_prefixfirst)) + ((dst_positive_scale_one_append_prefixfirst) + (dst_positive_scale_one_append_prefixfirst))) + (((dst_negative_code_one_append_prefixfirst) + (dst_negative_scale_one_append_prefixfirst)) * S ((dst_negative_code_one_append_prefixfirst) + (dst_negative_scale_one_append_prefixfirst)) + ((dst_negative_scale_one_append_prefixfirst) + (dst_negative_scale_one_append_prefixfirst)))) * S ((((dst_positive_code_one_append_prefixfirst) + (dst_positive_scale_one_append_prefixfirst)) * S ((dst_positive_code_one_append_prefixfirst) + (dst_positive_scale_one_append_prefixfirst)) + ((dst_positive_scale_one_append_prefixfirst) + (dst_positive_scale_one_append_prefixfirst))) + (((dst_negative_code_one_append_prefixfirst) + (dst_negative_scale_one_append_prefixfirst)) * S ((dst_negative_code_one_append_prefixfirst) + (dst_negative_scale_one_append_prefixfirst)) + ((dst_negative_scale_one_append_prefixfirst) + (dst_negative_scale_one_append_prefixfirst)))) + ((((dst_negative_code_one_append_prefixfirst) + (dst_negative_scale_one_append_prefixfirst)) * S ((dst_negative_code_one_append_prefixfirst) + (dst_negative_scale_one_append_prefixfirst)) + ((dst_negative_scale_one_append_prefixfirst) + (dst_negative_scale_one_append_prefixfirst))) + (((dst_negative_code_one_append_prefixfirst) + (dst_negative_scale_one_append_prefixfirst)) * S ((dst_negative_code_one_append_prefixfirst) + (dst_negative_scale_one_append_prefixfirst)) + ((dst_negative_scale_one_append_prefixfirst) + (dst_negative_scale_one_append_prefixfirst)))))) /\ (((((exists ff_h_pvs_one_append_prefixfirstpositive. ff_h_pvs_one_append_prefixfirstpositive + S (dst_positive_one_append_prefixfirst) = S ((S (dst_index_one_append_prefix)) * dst_positive_scale_one_append_prefixfirst)) /\ exists ff_q_pvs_one_append_prefixfirstpositive. dst_positive_code_one_append_prefixfirst = ff_q_pvs_one_append_prefixfirstpositive * S ((S (dst_index_one_append_prefix)) * dst_positive_scale_one_append_prefixfirst) + (dst_positive_one_append_prefixfirst))) /\ (((((exists ff_h_pvs_one_append_prefixfirstnegative. ff_h_pvs_one_append_prefixfirstnegative + S (dst_negative_one_append_prefixfirst) = S ((S (dst_index_one_append_prefix)) * dst_negative_scale_one_append_prefixfirst)) /\ exists ff_q_pvs_one_append_prefixfirstnegative. dst_negative_code_one_append_prefixfirst = ff_q_pvs_one_append_prefixfirstnegative * S ((S (dst_index_one_append_prefix)) * dst_negative_scale_one_append_prefixfirst) + (dst_negative_one_append_prefixfirst))) /\ (exists ge_balance_positive_one_append_prefixfirstvalue ge_balance_negative_one_append_prefixfirstvalue. (((((dst_first_one_append_prefix) = 2 * (ge_balance_positive_one_append_prefixfirstvalue) /\ (ge_balance_negative_one_append_prefixfirstvalue) = 0) \/ exists ge_signed_half_one_append_prefixfirstvaluedecode. (((dst_first_one_append_prefix) = 2 * ge_signed_half_one_append_prefixfirstvaluedecode + 1 /\ (ge_balance_positive_one_append_prefixfirstvalue) = 0) /\ (ge_balance_negative_one_append_prefixfirstvalue) = S ge_signed_half_one_append_prefixfirstvaluedecode))) /\ ((dst_positive_one_append_prefixfirst) + ge_balance_negative_one_append_prefixfirstvalue = (dst_negative_one_append_prefixfirst) + ge_balance_positive_one_append_prefixfirstvalue))))))))) -> (exists dst_positive_code_one_append_prefixsecond dst_positive_scale_one_append_prefixsecond dst_negative_code_one_append_prefixsecond dst_negative_scale_one_append_prefixsecond dst_positive_one_append_prefixsecond dst_negative_one_append_prefixsecond. (((V) = (((((dst_positive_code_one_append_prefixsecond) + (dst_positive_scale_one_append_prefixsecond)) * S ((dst_positive_code_one_append_prefixsecond) + (dst_positive_scale_one_append_prefixsecond)) + ((dst_positive_scale_one_append_prefixsecond) + (dst_positive_scale_one_append_prefixsecond))) + (((dst_negative_code_one_append_prefixsecond) + (dst_negative_scale_one_append_prefixsecond)) * S ((dst_negative_code_one_append_prefixsecond) + (dst_negative_scale_one_append_prefixsecond)) + ((dst_negative_scale_one_append_prefixsecond) + (dst_negative_scale_one_append_prefixsecond)))) * S ((((dst_positive_code_one_append_prefixsecond) + (dst_positive_scale_one_append_prefixsecond)) * S ((dst_positive_code_one_append_prefixsecond) + (dst_positive_scale_one_append_prefixsecond)) + ((dst_positive_scale_one_append_prefixsecond) + (dst_positive_scale_one_append_prefixsecond))) + (((dst_negative_code_one_append_prefixsecond) + (dst_negative_scale_one_append_prefixsecond)) * S ((dst_negative_code_one_append_prefixsecond) + (dst_negative_scale_one_append_prefixsecond)) + ((dst_negative_scale_one_append_prefixsecond) + (dst_negative_scale_one_append_prefixsecond)))) + ((((dst_negative_code_one_append_prefixsecond) + (dst_negative_scale_one_append_prefixsecond)) * S ((dst_negative_code_one_append_prefixsecond) + (dst_negative_scale_one_append_prefixsecond)) + ((dst_negative_scale_one_append_prefixsecond) + (dst_negative_scale_one_append_prefixsecond))) + (((dst_negative_code_one_append_prefixsecond) + (dst_negative_scale_one_append_prefixsecond)) * S ((dst_negative_code_one_append_prefixsecond) + (dst_negative_scale_one_append_prefixsecond)) + ((dst_negative_scale_one_append_prefixsecond) + (dst_negative_scale_one_append_prefixsecond)))))) /\ (((((exists ff_h_pvs_one_append_prefixsecondpositive. ff_h_pvs_one_append_prefixsecondpositive + S (dst_positive_one_append_prefixsecond) = S ((S (dst_index_one_append_prefix)) * dst_positive_scale_one_append_prefixsecond)) /\ exists ff_q_pvs_one_append_prefixsecondpositive. dst_positive_code_one_append_prefixsecond = ff_q_pvs_one_append_prefixsecondpositive * S ((S (dst_index_one_append_prefix)) * dst_positive_scale_one_append_prefixsecond) + (dst_positive_one_append_prefixsecond))) /\ (((((exists ff_h_pvs_one_append_prefixsecondnegative. ff_h_pvs_one_append_prefixsecondnegative + S (dst_negative_one_append_prefixsecond) = S ((S (dst_index_one_append_prefix)) * dst_negative_scale_one_append_prefixsecond)) /\ exists ff_q_pvs_one_append_prefixsecondnegative. dst_negative_code_one_append_prefixsecond = ff_q_pvs_one_append_prefixsecondnegative * S ((S (dst_index_one_append_prefix)) * dst_negative_scale_one_append_prefixsecond) + (dst_negative_one_append_prefixsecond))) /\ (exists ge_balance_positive_one_append_prefixsecondvalue ge_balance_negative_one_append_prefixsecondvalue. (((((dst_second_one_append_prefix) = 2 * (ge_balance_positive_one_append_prefixsecondvalue) /\ (ge_balance_negative_one_append_prefixsecondvalue) = 0) \/ exists ge_signed_half_one_append_prefixsecondvaluedecode. (((dst_second_one_append_prefix) = 2 * ge_signed_half_one_append_prefixsecondvaluedecode + 1 /\ (ge_balance_positive_one_append_prefixsecondvalue) = 0) /\ (ge_balance_negative_one_append_prefixsecondvalue) = S ge_signed_half_one_append_prefixsecondvaluedecode))) /\ ((dst_positive_one_append_prefixsecond) + ge_balance_negative_one_append_prefixsecondvalue = (dst_negative_one_append_prefixsecond) + ge_balance_positive_one_append_prefixsecondvalue))))))))) -> dst_first_one_append_prefix = dst_second_one_append_prefix)

Constructive proof overview

Generated structural guide

Actually append signed one at the next positive index by paired beta recoding, preserving the full previous prefix including zero.

The unchanged tactic script uses 5 declared prerequisites and contains 71 exact native proof lines.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

arithmetic_signed_table_append Alpha theorem; checked-use authorized le_eq_or_lt Stable theorem; checked-use authorized divisor_signed_table_at_functional Alpha theorem; checked-use authorized le_of_succ_le_succ Stable theorem; checked-use authorized divisor_signed_table_lookup Alpha theorem; checked-use authorized

Direct dependents

DU0007 dirichlet_constant_one_table_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

71 script commands · 17 reading checkpoints · 6 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.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–3

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

  1. L1
    intro N
  2. L2
    intro F
  3. L3
    intro hf
02Separate the logical casesL4–4

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

  1. L4
    cases hf
03Establish hxL5–10

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

  1. L5
    have hx : ∃ G. ArithTable(S N,G) ∧ ((∀ x. ∀ y. ∀ z. Lt(x,S N) → ArithAt(F,x,y) → ArithAt(G,x,z) → y = z) ∧ ArithAt(G,S N,2))Definitions: ArithTableArithAtLt
  2. L6
    specialize arithmetic_signed_table_append (N)
  3. L7
    specialize arithmetic_signed_table_append (F)
  4. L8
    specialize arithmetic_signed_table_append (2)
  5. L9
    apply arithmetic_signed_table_append
  6. L10
    exact hf_left
04Separate the logical casesL11–13

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

  1. L11
    cases hx
  2. L12
    cases hx_witness
  3. L13
    cases hx_witness_right
05Construct an explicit witnessL14–14

Supply the displayed value, then prove that it has the required property.

  1. L14
    exists x
06Separate the logical casesL15–16

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

  1. L15
    split
  2. L16
    split
07Use earlier factsL17–17

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

  1. L17
    exact hx_witness_left
08Fix variables and assumptionsL18–22

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

  1. L18
    intro i
  2. L19
    intro a
  3. L20
    intro hi
  4. L21
    intro hb
  5. L22
    intro ha
09Establish hcL23–27

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

  1. L23
    have hc : i=S N \/ (exists pvs_gap_append_cases. pvs_gap_append_cases + S (i) = (S N))
  2. L24
    specialize le_eq_or_lt (i)
  3. L25
    specialize le_eq_or_lt (S N)
  4. L26
    apply le_eq_or_lt
  5. L27
    exact hb
10Separate the logical casesL28–28

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

  1. L28
    cases hc
11Calculate and transport equalitiesL29–32

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L29
    rewrite hc_left at ha
  2. L30
    rewrite hc_left at ha
  3. L31
    rewrite hc_left at ha
  4. L32
    rewrite hc_left at ha
12Establish hvL33–41

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

  1. L33
    have hv : a=2
  2. L34
    specialize divisor_signed_table_at_functional (x)
  3. L35
    specialize divisor_signed_table_at_functional (S N)
  4. L36
    specialize divisor_signed_table_at_functional (a)
  5. L37
    specialize divisor_signed_table_at_functional (2)
  6. L38
    apply divisor_signed_table_at_functional
  7. L39
    exact ha
  8. L40
    exact hx_witness_right_right
  9. L41
    exact hv
13Establish hibL42–46

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

  1. L42
    have hib : exists pvs_le_gap_append_old_bound. pvs_le_gap_append_old_bound + (i) = (N)
  2. L43
    specialize le_of_succ_le_succ (i)
  3. L44
    specialize le_of_succ_le_succ (N)
  4. L45
    apply le_of_succ_le_succ
  5. L46
    exact hc_right
14Establish hvL47–53

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

  1. L47
    have hv : ∃ v. ArithAt(F,i,v)Definitions: ArithAt
  2. L48
    specialize divisor_signed_table_lookup (N)
  3. L49
    specialize divisor_signed_table_lookup (F)
  4. L50
    specialize divisor_signed_table_lookup (i)
  5. L51
    apply divisor_signed_table_lookup
  6. L52
    exact hf_left
  7. L53
    exact hib
15Separate the logical casesL54–54

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

  1. L54
    cases hv
16Establish heqL55–64

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hx witness right left.

  1. L55
    have heq : x1=a
  2. L56
    specialize hx_witness_right_left (i)
  3. L57
    specialize hx_witness_right_left (x1)
  4. L58
    specialize hx_witness_right_left (a)
  5. L59
    apply hx_witness_right_left
  6. L60
    exact hc_right
  7. L61
    exact hv_witness
  8. L62
    exact ha
  9. L63
    rewrite heq at hv_witness
  10. L64
    rewrite heq at hv_witness
17Use earlier factsL65–71

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

  1. L65
    specialize hf_right (i)
  2. L66
    specialize hf_right (a)
  3. L67
    apply hf_right
  4. L68
    exact hi
  5. L69
    exact hib
  6. L70
    exact hv_witness
  7. L71
    exact hx_witness_right_left

Library-wide reading audit

Original exact command ledger · 71 lines
  1. 0001intro N
  2. 0002intro F
  3. 0003intro hf
  4. 0004cases hf
  5. 0005have hx : exists G. (((exists dst_positive_code_append_actualtable dst_positive_scale_append_actualtable dst_negative_code_append_actualtable dst_negative_scale_append_actualtable. (((G) = (((((dst_positive_code_append_actualtable) + (dst_positive_scale_append_actualtable)) * S ((dst_positive_code_append_actualtable) + (dst_positive_scale_append_actualtable)) + ((dst_positive_scale_append_actualtable) + (dst_positive_scale_append_actualtable))) + (((dst_negative_code_append_actualtable) + (dst_negative_scale_append_actualtable)) * S ((dst_negative_code_append_actualtable) + (dst_negative_scale_append_actualtable)) + ((dst_negative_scale_append_actualtable) + (dst_negative_scale_append_actualtable)))) * S ((((dst_positive_code_append_actualtable) + (dst_positive_scale_append_actualtable)) * S ((dst_positive_code_append_actualtable) + (dst_positive_scale_append_actualtable)) + ((dst_positive_scale_append_actualtable) + (dst_positive_scale_append_actualtable))) + (((dst_negative_code_append_actualtable) + (dst_negative_scale_append_actualtable)) * S ((dst_negative_code_append_actualtable) + (dst_negative_scale_append_actualtable)) + ((dst_negative_scale_append_actualtable) + (dst_negative_scale_append_actualtable)))) + ((((dst_negative_code_append_actualtable) + (dst_negative_scale_append_actualtable)) * S ((dst_negative_code_append_actualtable) + (dst_negative_scale_append_actualtable)) + ((dst_negative_scale_append_actualtable) + (dst_negative_scale_append_actualtable))) + (((dst_negative_code_append_actualtable) + (dst_negative_scale_append_actualtable)) * S ((dst_negative_code_append_actualtable) + (dst_negative_scale_append_actualtable)) + ((dst_negative_scale_append_actualtable) + (dst_negative_scale_append_actualtable)))))) /\ (forall dst_index_append_actualtable. (exists pvs_le_gap_append_actualtabledomain. pvs_le_gap_append_actualtabledomain + (dst_index_append_actualtable) = (S N)) -> exists dst_positive_append_actualtable dst_negative_append_actualtable dst_value_append_actualtable. ((((exists ff_h_pvs_append_actualtableentrypositive. ff_h_pvs_append_actualtableentrypositive + S (dst_positive_append_actualtable) = S ((S (dst_index_append_actualtable)) * dst_positive_scale_append_actualtable)) /\ exists ff_q_pvs_append_actualtableentrypositive. dst_positive_code_append_actualtable = ff_q_pvs_append_actualtableentrypositive * S ((S (dst_index_append_actualtable)) * dst_positive_scale_append_actualtable) + (dst_positive_append_actualtable))) /\ (((((exists ff_h_pvs_append_actualtableentrynegative. ff_h_pvs_append_actualtableentrynegative + S (dst_negative_append_actualtable) = S ((S (dst_index_append_actualtable)) * dst_negative_scale_append_actualtable)) /\ exists ff_q_pvs_append_actualtableentrynegative. dst_negative_code_append_actualtable = ff_q_pvs_append_actualtableentrynegative * S ((S (dst_index_append_actualtable)) * dst_negative_scale_append_actualtable) + (dst_negative_append_actualtable))) /\ (exists ge_balance_positive_append_actualtableentryvalue ge_balance_negative_append_actualtableentryvalue. (((((dst_value_append_actualtable) = 2 * (ge_balance_positive_append_actualtableentryvalue) /\ (ge_balance_negative_append_actualtableentryvalue) = 0) \/ exists ge_signed_half_append_actualtableentryvaluedecode. (((dst_value_append_actualtable) = 2 * ge_signed_half_append_actualtableentryvaluedecode + 1 /\ (ge_balance_positive_append_actualtableentryvalue) = 0) /\ (ge_balance_negative_append_actualtableentryvalue) = S ge_signed_half_append_actualtableentryvaluedecode))) /\ ((dst_positive_append_actualtable) + ge_balance_negative_append_actualtableentryvalue = (dst_negative_append_actualtable) + ge_balance_positive_append_actualtableentryvalue))))))))) /\ (((forall dst_index_append_actualprefix dst_first_append_actualprefix dst_second_append_actualprefix. (exists pvs_gap_append_actualprefixbound. pvs_gap_append_actualprefixbound + S (dst_index_append_actualprefix) = (S N)) -> (exists dst_positive_code_append_actualprefixfirst dst_positive_scale_append_actualprefixfirst dst_negative_code_append_actualprefixfirst dst_negative_scale_append_actualprefixfirst dst_positive_append_actualprefixfirst dst_negative_append_actualprefixfirst. (((F) = (((((dst_positive_code_append_actualprefixfirst) + (dst_positive_scale_append_actualprefixfirst)) * S ((dst_positive_code_append_actualprefixfirst) + (dst_positive_scale_append_actualprefixfirst)) + ((dst_positive_scale_append_actualprefixfirst) + (dst_positive_scale_append_actualprefixfirst))) + (((dst_negative_code_append_actualprefixfirst) + (dst_negative_scale_append_actualprefixfirst)) * S ((dst_negative_code_append_actualprefixfirst) + (dst_negative_scale_append_actualprefixfirst)) + ((dst_negative_scale_append_actualprefixfirst) + (dst_negative_scale_append_actualprefixfirst)))) * S ((((dst_positive_code_append_actualprefixfirst) + (dst_positive_scale_append_actualprefixfirst)) * S ((dst_positive_code_append_actualprefixfirst) + (dst_positive_scale_append_actualprefixfirst)) + ((dst_positive_scale_append_actualprefixfirst) + (dst_positive_scale_append_actualprefixfirst))) + (((dst_negative_code_append_actualprefixfirst) + (dst_negative_scale_append_actualprefixfirst)) * S ((dst_negative_code_append_actualprefixfirst) + (dst_negative_scale_append_actualprefixfirst)) + ((dst_negative_scale_append_actualprefixfirst) + (dst_negative_scale_append_actualprefixfirst)))) + ((((dst_negative_code_append_actualprefixfirst) + (dst_negative_scale_append_actualprefixfirst)) * S ((dst_negative_code_append_actualprefixfirst) + (dst_negative_scale_append_actualprefixfirst)) + ((dst_negative_scale_append_actualprefixfirst) + (dst_negative_scale_append_actualprefixfirst))) + (((dst_negative_code_append_actualprefixfirst) + (dst_negative_scale_append_actualprefixfirst)) * S ((dst_negative_code_append_actualprefixfirst) + (dst_negative_scale_append_actualprefixfirst)) + ((dst_negative_scale_append_actualprefixfirst) + (dst_negative_scale_append_actualprefixfirst)))))) /\ (((((exists ff_h_pvs_append_actualprefixfirstpositive. ff_h_pvs_append_actualprefixfirstpositive + S (dst_positive_append_actualprefixfirst) = S ((S (dst_index_append_actualprefix)) * dst_positive_scale_append_actualprefixfirst)) /\ exists ff_q_pvs_append_actualprefixfirstpositive. dst_positive_code_append_actualprefixfirst = ff_q_pvs_append_actualprefixfirstpositive * S ((S (dst_index_append_actualprefix)) * dst_positive_scale_append_actualprefixfirst) + (dst_positive_append_actualprefixfirst))) /\ (((((exists ff_h_pvs_append_actualprefixfirstnegative. ff_h_pvs_append_actualprefixfirstnegative + S (dst_negative_append_actualprefixfirst) = S ((S (dst_index_append_actualprefix)) * dst_negative_scale_append_actualprefixfirst)) /\ exists ff_q_pvs_append_actualprefixfirstnegative. dst_negative_code_append_actualprefixfirst = ff_q_pvs_append_actualprefixfirstnegative * S ((S (dst_index_append_actualprefix)) * dst_negative_scale_append_actualprefixfirst) + (dst_negative_append_actualprefixfirst))) /\ (exists ge_balance_positive_append_actualprefixfirstvalue ge_balance_negative_append_actualprefixfirstvalue. (((((dst_first_append_actualprefix) = 2 * (ge_balance_positive_append_actualprefixfirstvalue) /\ (ge_balance_negative_append_actualprefixfirstvalue) = 0) \/ exists ge_signed_half_append_actualprefixfirstvaluedecode. (((dst_first_append_actualprefix) = 2 * ge_signed_half_append_actualprefixfirstvaluedecode + 1 /\ (ge_balance_positive_append_actualprefixfirstvalue) = 0) /\ (ge_balance_negative_append_actualprefixfirstvalue) = S ge_signed_half_append_actualprefixfirstvaluedecode))) /\ ((dst_positive_append_actualprefixfirst) + ge_balance_negative_append_actualprefixfirstvalue = (dst_negative_append_actualprefixfirst) + ge_balance_positive_append_actualprefixfirstvalue))))))))) -> (exists dst_positive_code_append_actualprefixsecond dst_positive_scale_append_actualprefixsecond dst_negative_code_append_actualprefixsecond dst_negative_scale_append_actualprefixsecond dst_positive_append_actualprefixsecond dst_negative_append_actualprefixsecond. (((G) = (((((dst_positive_code_append_actualprefixsecond) + (dst_positive_scale_append_actualprefixsecond)) * S ((dst_positive_code_append_actualprefixsecond) + (dst_positive_scale_append_actualprefixsecond)) + ((dst_positive_scale_append_actualprefixsecond) + (dst_positive_scale_append_actualprefixsecond))) + (((dst_negative_code_append_actualprefixsecond) + (dst_negative_scale_append_actualprefixsecond)) * S ((dst_negative_code_append_actualprefixsecond) + (dst_negative_scale_append_actualprefixsecond)) + ((dst_negative_scale_append_actualprefixsecond) + (dst_negative_scale_append_actualprefixsecond)))) * S ((((dst_positive_code_append_actualprefixsecond) + (dst_positive_scale_append_actualprefixsecond)) * S ((dst_positive_code_append_actualprefixsecond) + (dst_positive_scale_append_actualprefixsecond)) + ((dst_positive_scale_append_actualprefixsecond) + (dst_positive_scale_append_actualprefixsecond))) + (((dst_negative_code_append_actualprefixsecond) + (dst_negative_scale_append_actualprefixsecond)) * S ((dst_negative_code_append_actualprefixsecond) + (dst_negative_scale_append_actualprefixsecond)) + ((dst_negative_scale_append_actualprefixsecond) + (dst_negative_scale_append_actualprefixsecond)))) + ((((dst_negative_code_append_actualprefixsecond) + (dst_negative_scale_append_actualprefixsecond)) * S ((dst_negative_code_append_actualprefixsecond) + (dst_negative_scale_append_actualprefixsecond)) + ((dst_negative_scale_append_actualprefixsecond) + (dst_negative_scale_append_actualprefixsecond))) + (((dst_negative_code_append_actualprefixsecond) + (dst_negative_scale_append_actualprefixsecond)) * S ((dst_negative_code_append_actualprefixsecond) + (dst_negative_scale_append_actualprefixsecond)) + ((dst_negative_scale_append_actualprefixsecond) + (dst_negative_scale_append_actualprefixsecond)))))) /\ (((((exists ff_h_pvs_append_actualprefixsecondpositive. ff_h_pvs_append_actualprefixsecondpositive + S (dst_positive_append_actualprefixsecond) = S ((S (dst_index_append_actualprefix)) * dst_positive_scale_append_actualprefixsecond)) /\ exists ff_q_pvs_append_actualprefixsecondpositive. dst_positive_code_append_actualprefixsecond = ff_q_pvs_append_actualprefixsecondpositive * S ((S (dst_index_append_actualprefix)) * dst_positive_scale_append_actualprefixsecond) + (dst_positive_append_actualprefixsecond))) /\ (((((exists ff_h_pvs_append_actualprefixsecondnegative. ff_h_pvs_append_actualprefixsecondnegative + S (dst_negative_append_actualprefixsecond) = S ((S (dst_index_append_actualprefix)) * dst_negative_scale_append_actualprefixsecond)) /\ exists ff_q_pvs_append_actualprefixsecondnegative. dst_negative_code_append_actualprefixsecond = ff_q_pvs_append_actualprefixsecondnegative * S ((S (dst_index_append_actualprefix)) * dst_negative_scale_append_actualprefixsecond) + (dst_negative_append_actualprefixsecond))) /\ (exists ge_balance_positive_append_actualprefixsecondvalue ge_balance_negative_append_actualprefixsecondvalue. (((((dst_second_append_actualprefix) = 2 * (ge_balance_positive_append_actualprefixsecondvalue) /\ (ge_balance_negative_append_actualprefixsecondvalue) = 0) \/ exists ge_signed_half_append_actualprefixsecondvaluedecode. (((dst_second_append_actualprefix) = 2 * ge_signed_half_append_actualprefixsecondvaluedecode + 1 /\ (ge_balance_positive_append_actualprefixsecondvalue) = 0) /\ (ge_balance_negative_append_actualprefixsecondvalue) = S ge_signed_half_append_actualprefixsecondvaluedecode))) /\ ((dst_positive_append_actualprefixsecond) + ge_balance_negative_append_actualprefixsecondvalue = (dst_negative_append_actualprefixsecond) + ge_balance_positive_append_actualprefixsecondvalue))))))))) -> dst_first_append_actualprefix = dst_second_append_actualprefix) /\ (exists dst_positive_code_append_actuallast dst_positive_scale_append_actuallast dst_negative_code_append_actuallast dst_negative_scale_append_actuallast dst_positive_append_actuallast dst_negative_append_actuallast. (((G) = (((((dst_positive_code_append_actuallast) + (dst_positive_scale_append_actuallast)) * S ((dst_positive_code_append_actuallast) + (dst_positive_scale_append_actuallast)) + ((dst_positive_scale_append_actuallast) + (dst_positive_scale_append_actuallast))) + (((dst_negative_code_append_actuallast) + (dst_negative_scale_append_actuallast)) * S ((dst_negative_code_append_actuallast) + (dst_negative_scale_append_actuallast)) + ((dst_negative_scale_append_actuallast) + (dst_negative_scale_append_actuallast)))) * S ((((dst_positive_code_append_actuallast) + (dst_positive_scale_append_actuallast)) * S ((dst_positive_code_append_actuallast) + (dst_positive_scale_append_actuallast)) + ((dst_positive_scale_append_actuallast) + (dst_positive_scale_append_actuallast))) + (((dst_negative_code_append_actuallast) + (dst_negative_scale_append_actuallast)) * S ((dst_negative_code_append_actuallast) + (dst_negative_scale_append_actuallast)) + ((dst_negative_scale_append_actuallast) + (dst_negative_scale_append_actuallast)))) + ((((dst_negative_code_append_actuallast) + (dst_negative_scale_append_actuallast)) * S ((dst_negative_code_append_actuallast) + (dst_negative_scale_append_actuallast)) + ((dst_negative_scale_append_actuallast) + (dst_negative_scale_append_actuallast))) + (((dst_negative_code_append_actuallast) + (dst_negative_scale_append_actuallast)) * S ((dst_negative_code_append_actuallast) + (dst_negative_scale_append_actuallast)) + ((dst_negative_scale_append_actuallast) + (dst_negative_scale_append_actuallast)))))) /\ (((((exists ff_h_pvs_append_actuallastpositive. ff_h_pvs_append_actuallastpositive + S (dst_positive_append_actuallast) = S ((S (S N)) * dst_positive_scale_append_actuallast)) /\ exists ff_q_pvs_append_actuallastpositive. dst_positive_code_append_actuallast = ff_q_pvs_append_actuallastpositive * S ((S (S N)) * dst_positive_scale_append_actuallast) + (dst_positive_append_actuallast))) /\ (((((exists ff_h_pvs_append_actuallastnegative. ff_h_pvs_append_actuallastnegative + S (dst_negative_append_actuallast) = S ((S (S N)) * dst_negative_scale_append_actuallast)) /\ exists ff_q_pvs_append_actuallastnegative. dst_negative_code_append_actuallast = ff_q_pvs_append_actuallastnegative * S ((S (S N)) * dst_negative_scale_append_actuallast) + (dst_negative_append_actuallast))) /\ (exists ge_balance_positive_append_actuallastvalue ge_balance_negative_append_actuallastvalue. (((((2) = 2 * (ge_balance_positive_append_actuallastvalue) /\ (ge_balance_negative_append_actuallastvalue) = 0) \/ exists ge_signed_half_append_actuallastvaluedecode. (((2) = 2 * ge_signed_half_append_actuallastvaluedecode + 1 /\ (ge_balance_positive_append_actuallastvalue) = 0) /\ (ge_balance_negative_append_actuallastvalue) = S ge_signed_half_append_actuallastvaluedecode))) /\ ((dst_positive_append_actuallast) + ge_balance_negative_append_actuallastvalue = (dst_negative_append_actuallast) + ge_balance_positive_append_actuallastvalue)))))))))))))
  6. 0006specialize arithmetic_signed_table_append (N)
  7. 0007specialize arithmetic_signed_table_append (F)
  8. 0008specialize arithmetic_signed_table_append (2)
  9. 0009apply arithmetic_signed_table_append
  10. 0010exact hf_left
  11. 0011cases hx
  12. 0012cases hx_witness
  13. 0013cases hx_witness_right
  14. 0014exists x
  15. 0015split
  16. 0016split
  17. 0017exact hx_witness_left
  18. 0018intro i
  19. 0019intro a
  20. 0020intro hi
  21. 0021intro hb
  22. 0022intro ha
  23. 0023have hc : i=S N \/ (exists pvs_gap_append_cases. pvs_gap_append_cases + S (i) = (S N))
  24. 0024specialize le_eq_or_lt (i)
  25. 0025specialize le_eq_or_lt (S N)
  26. 0026apply le_eq_or_lt
  27. 0027exact hb
  28. 0028cases hc
  29. 0029rewrite hc_left at ha
  30. 0030rewrite hc_left at ha
  31. 0031rewrite hc_left at ha
  32. 0032rewrite hc_left at ha
  33. 0033have hv : a=2
  34. 0034specialize divisor_signed_table_at_functional (x)
  35. 0035specialize divisor_signed_table_at_functional (S N)
  36. 0036specialize divisor_signed_table_at_functional (a)
  37. 0037specialize divisor_signed_table_at_functional (2)
  38. 0038apply divisor_signed_table_at_functional
  39. 0039exact ha
  40. 0040exact hx_witness_right_right
  41. 0041exact hv
  42. 0042have hib : exists pvs_le_gap_append_old_bound. pvs_le_gap_append_old_bound + (i) = (N)
  43. 0043specialize le_of_succ_le_succ (i)
  44. 0044specialize le_of_succ_le_succ (N)
  45. 0045apply le_of_succ_le_succ
  46. 0046exact hc_right
  47. 0047have hv : exists v. (exists dst_positive_code_append_old_lookup dst_positive_scale_append_old_lookup dst_negative_code_append_old_lookup dst_negative_scale_append_old_lookup dst_positive_append_old_lookup dst_negative_append_old_lookup. (((F) = (((((dst_positive_code_append_old_lookup) + (dst_positive_scale_append_old_lookup)) * S ((dst_positive_code_append_old_lookup) + (dst_positive_scale_append_old_lookup)) + ((dst_positive_scale_append_old_lookup) + (dst_positive_scale_append_old_lookup))) + (((dst_negative_code_append_old_lookup) + (dst_negative_scale_append_old_lookup)) * S ((dst_negative_code_append_old_lookup) + (dst_negative_scale_append_old_lookup)) + ((dst_negative_scale_append_old_lookup) + (dst_negative_scale_append_old_lookup)))) * S ((((dst_positive_code_append_old_lookup) + (dst_positive_scale_append_old_lookup)) * S ((dst_positive_code_append_old_lookup) + (dst_positive_scale_append_old_lookup)) + ((dst_positive_scale_append_old_lookup) + (dst_positive_scale_append_old_lookup))) + (((dst_negative_code_append_old_lookup) + (dst_negative_scale_append_old_lookup)) * S ((dst_negative_code_append_old_lookup) + (dst_negative_scale_append_old_lookup)) + ((dst_negative_scale_append_old_lookup) + (dst_negative_scale_append_old_lookup)))) + ((((dst_negative_code_append_old_lookup) + (dst_negative_scale_append_old_lookup)) * S ((dst_negative_code_append_old_lookup) + (dst_negative_scale_append_old_lookup)) + ((dst_negative_scale_append_old_lookup) + (dst_negative_scale_append_old_lookup))) + (((dst_negative_code_append_old_lookup) + (dst_negative_scale_append_old_lookup)) * S ((dst_negative_code_append_old_lookup) + (dst_negative_scale_append_old_lookup)) + ((dst_negative_scale_append_old_lookup) + (dst_negative_scale_append_old_lookup)))))) /\ (((((exists ff_h_pvs_append_old_lookuppositive. ff_h_pvs_append_old_lookuppositive + S (dst_positive_append_old_lookup) = S ((S (i)) * dst_positive_scale_append_old_lookup)) /\ exists ff_q_pvs_append_old_lookuppositive. dst_positive_code_append_old_lookup = ff_q_pvs_append_old_lookuppositive * S ((S (i)) * dst_positive_scale_append_old_lookup) + (dst_positive_append_old_lookup))) /\ (((((exists ff_h_pvs_append_old_lookupnegative. ff_h_pvs_append_old_lookupnegative + S (dst_negative_append_old_lookup) = S ((S (i)) * dst_negative_scale_append_old_lookup)) /\ exists ff_q_pvs_append_old_lookupnegative. dst_negative_code_append_old_lookup = ff_q_pvs_append_old_lookupnegative * S ((S (i)) * dst_negative_scale_append_old_lookup) + (dst_negative_append_old_lookup))) /\ (exists ge_balance_positive_append_old_lookupvalue ge_balance_negative_append_old_lookupvalue. (((((v) = 2 * (ge_balance_positive_append_old_lookupvalue) /\ (ge_balance_negative_append_old_lookupvalue) = 0) \/ exists ge_signed_half_append_old_lookupvaluedecode. (((v) = 2 * ge_signed_half_append_old_lookupvaluedecode + 1 /\ (ge_balance_positive_append_old_lookupvalue) = 0) /\ (ge_balance_negative_append_old_lookupvalue) = S ge_signed_half_append_old_lookupvaluedecode))) /\ ((dst_positive_append_old_lookup) + ge_balance_negative_append_old_lookupvalue = (dst_negative_append_old_lookup) + ge_balance_positive_append_old_lookupvalue)))))))))
  48. 0048specialize divisor_signed_table_lookup (N)
  49. 0049specialize divisor_signed_table_lookup (F)
  50. 0050specialize divisor_signed_table_lookup (i)
  51. 0051apply divisor_signed_table_lookup
  52. 0052exact hf_left
  53. 0053exact hib
  54. 0054cases hv
  55. 0055have heq : x1=a
  56. 0056specialize hx_witness_right_left (i)
  57. 0057specialize hx_witness_right_left (x1)
  58. 0058specialize hx_witness_right_left (a)
  59. 0059apply hx_witness_right_left
  60. 0060exact hc_right
  61. 0061exact hv_witness
  62. 0062exact ha
  63. 0063rewrite heq at hv_witness
  64. 0064rewrite heq at hv_witness
  65. 0065specialize hf_right (i)
  66. 0066specialize hf_right (a)
  67. 0067apply hf_right
  68. 0068exact hi
  69. 0069exact hib
  70. 0070exact hv_witness
  71. 0071exact hx_witness_right_left