DU0006

dirichlet_kronecker_delta_table_append

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

Append the separately chosen actual delta value, preserving every earlier signed entry rather than assuming a table oracle.

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 E z. (((exists dst_positive_code_delta_append_inputtable dst_positive_scale_delta_append_inputtable dst_negative_code_delta_append_inputtable dst_negative_scale_delta_append_inputtable. (((E) = (((((dst_positive_code_delta_append_inputtable) + (dst_positive_scale_delta_append_inputtable)) * S ((dst_positive_code_delta_append_inputtable) + (dst_positive_scale_delta_append_inputtable)) + ((dst_positive_scale_delta_append_inputtable) + (dst_positive_scale_delta_append_inputtable))) + (((dst_negative_code_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)) * S ((dst_negative_code_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)) + ((dst_negative_scale_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)))) * S ((((dst_positive_code_delta_append_inputtable) + (dst_positive_scale_delta_append_inputtable)) * S ((dst_positive_code_delta_append_inputtable) + (dst_positive_scale_delta_append_inputtable)) + ((dst_positive_scale_delta_append_inputtable) + (dst_positive_scale_delta_append_inputtable))) + (((dst_negative_code_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)) * S ((dst_negative_code_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)) + ((dst_negative_scale_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)))) + ((((dst_negative_code_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)) * S ((dst_negative_code_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)) + ((dst_negative_scale_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable))) + (((dst_negative_code_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)) * S ((dst_negative_code_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)) + ((dst_negative_scale_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)))))) /\ (forall dst_index_delta_append_inputtable. (exists pvs_le_gap_delta_append_inputtabledomain. pvs_le_gap_delta_append_inputtabledomain + (dst_index_delta_append_inputtable) = (N)) -> exists dst_positive_delta_append_inputtable dst_negative_delta_append_inputtable dst_value_delta_append_inputtable. ((((exists ff_h_pvs_delta_append_inputtableentrypositive. ff_h_pvs_delta_append_inputtableentrypositive + S (dst_positive_delta_append_inputtable) = S ((S (dst_index_delta_append_inputtable)) * dst_positive_scale_delta_append_inputtable)) /\ exists ff_q_pvs_delta_append_inputtableentrypositive. dst_positive_code_delta_append_inputtable = ff_q_pvs_delta_append_inputtableentrypositive * S ((S (dst_index_delta_append_inputtable)) * dst_positive_scale_delta_append_inputtable) + (dst_positive_delta_append_inputtable))) /\ (((((exists ff_h_pvs_delta_append_inputtableentrynegative. ff_h_pvs_delta_append_inputtableentrynegative + S (dst_negative_delta_append_inputtable) = S ((S (dst_index_delta_append_inputtable)) * dst_negative_scale_delta_append_inputtable)) /\ exists ff_q_pvs_delta_append_inputtableentrynegative. dst_negative_code_delta_append_inputtable = ff_q_pvs_delta_append_inputtableentrynegative * S ((S (dst_index_delta_append_inputtable)) * dst_negative_scale_delta_append_inputtable) + (dst_negative_delta_append_inputtable))) /\ (exists ge_balance_positive_delta_append_inputtableentryvalue ge_balance_negative_delta_append_inputtableentryvalue. (((((dst_value_delta_append_inputtable) = 2 * (ge_balance_positive_delta_append_inputtableentryvalue) /\ (ge_balance_negative_delta_append_inputtableentryvalue) = 0) \/ exists ge_signed_half_delta_append_inputtableentryvaluedecode. (((dst_value_delta_append_inputtable) = 2 * ge_signed_half_delta_append_inputtableentryvaluedecode + 1 /\ (ge_balance_positive_delta_append_inputtableentryvalue) = 0) /\ (ge_balance_negative_delta_append_inputtableentryvalue) = S ge_signed_half_delta_append_inputtableentryvaluedecode))) /\ ((dst_positive_delta_append_inputtable) + ge_balance_negative_delta_append_inputtableentryvalue = (dst_negative_delta_append_inputtable) + ge_balance_positive_delta_append_inputtableentryvalue))))))))) /\ (forall du_index_delta_append_input du_value_delta_append_input. ~(du_index_delta_append_input=0) -> (exists pvs_le_gap_delta_append_inputbound. pvs_le_gap_delta_append_inputbound + (du_index_delta_append_input) = (N)) -> (exists dst_positive_code_delta_append_inputentry dst_positive_scale_delta_append_inputentry dst_negative_code_delta_append_inputentry dst_negative_scale_delta_append_inputentry dst_positive_delta_append_inputentry dst_negative_delta_append_inputentry. (((E) = (((((dst_positive_code_delta_append_inputentry) + (dst_positive_scale_delta_append_inputentry)) * S ((dst_positive_code_delta_append_inputentry) + (dst_positive_scale_delta_append_inputentry)) + ((dst_positive_scale_delta_append_inputentry) + (dst_positive_scale_delta_append_inputentry))) + (((dst_negative_code_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)) * S ((dst_negative_code_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)) + ((dst_negative_scale_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)))) * S ((((dst_positive_code_delta_append_inputentry) + (dst_positive_scale_delta_append_inputentry)) * S ((dst_positive_code_delta_append_inputentry) + (dst_positive_scale_delta_append_inputentry)) + ((dst_positive_scale_delta_append_inputentry) + (dst_positive_scale_delta_append_inputentry))) + (((dst_negative_code_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)) * S ((dst_negative_code_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)) + ((dst_negative_scale_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)))) + ((((dst_negative_code_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)) * S ((dst_negative_code_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)) + ((dst_negative_scale_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry))) + (((dst_negative_code_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)) * S ((dst_negative_code_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)) + ((dst_negative_scale_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)))))) /\ (((((exists ff_h_pvs_delta_append_inputentrypositive. ff_h_pvs_delta_append_inputentrypositive + S (dst_positive_delta_append_inputentry) = S ((S (du_index_delta_append_input)) * dst_positive_scale_delta_append_inputentry)) /\ exists ff_q_pvs_delta_append_inputentrypositive. dst_positive_code_delta_append_inputentry = ff_q_pvs_delta_append_inputentrypositive * S ((S (du_index_delta_append_input)) * dst_positive_scale_delta_append_inputentry) + (dst_positive_delta_append_inputentry))) /\ (((((exists ff_h_pvs_delta_append_inputentrynegative. ff_h_pvs_delta_append_inputentrynegative + S (dst_negative_delta_append_inputentry) = S ((S (du_index_delta_append_input)) * dst_negative_scale_delta_append_inputentry)) /\ exists ff_q_pvs_delta_append_inputentrynegative. dst_negative_code_delta_append_inputentry = ff_q_pvs_delta_append_inputentrynegative * S ((S (du_index_delta_append_input)) * dst_negative_scale_delta_append_inputentry) + (dst_negative_delta_append_inputentry))) /\ (exists ge_balance_positive_delta_append_inputentryvalue ge_balance_negative_delta_append_inputentryvalue. (((((du_value_delta_append_input) = 2 * (ge_balance_positive_delta_append_inputentryvalue) /\ (ge_balance_negative_delta_append_inputentryvalue) = 0) \/ exists ge_signed_half_delta_append_inputentryvaluedecode. (((du_value_delta_append_input) = 2 * ge_signed_half_delta_append_inputentryvaluedecode + 1 /\ (ge_balance_positive_delta_append_inputentryvalue) = 0) /\ (ge_balance_negative_delta_append_inputentryvalue) = S ge_signed_half_delta_append_inputentryvaluedecode))) /\ ((dst_positive_delta_append_inputentry) + ge_balance_negative_delta_append_inputentryvalue = (dst_negative_delta_append_inputentry) + ge_balance_positive_delta_append_inputentryvalue))))))))) -> ((((du_index_delta_append_input)=1 -> (du_value_delta_append_input)=2) /\ (~((du_index_delta_append_input)=1) -> (du_value_delta_append_input)=0)))))) -> ((((S N)=1 -> (z)=2) /\ (~((S N)=1) -> (z)=0))) -> exists D. (((exists dst_positive_code_delta_append_outputtable dst_positive_scale_delta_append_outputtable dst_negative_code_delta_append_outputtable dst_negative_scale_delta_append_outputtable. (((D) = (((((dst_positive_code_delta_append_outputtable) + (dst_positive_scale_delta_append_outputtable)) * S ((dst_positive_code_delta_append_outputtable) + (dst_positive_scale_delta_append_outputtable)) + ((dst_positive_scale_delta_append_outputtable) + (dst_positive_scale_delta_append_outputtable))) + (((dst_negative_code_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)) * S ((dst_negative_code_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)) + ((dst_negative_scale_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)))) * S ((((dst_positive_code_delta_append_outputtable) + (dst_positive_scale_delta_append_outputtable)) * S ((dst_positive_code_delta_append_outputtable) + (dst_positive_scale_delta_append_outputtable)) + ((dst_positive_scale_delta_append_outputtable) + (dst_positive_scale_delta_append_outputtable))) + (((dst_negative_code_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)) * S ((dst_negative_code_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)) + ((dst_negative_scale_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)))) + ((((dst_negative_code_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)) * S ((dst_negative_code_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)) + ((dst_negative_scale_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable))) + (((dst_negative_code_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)) * S ((dst_negative_code_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)) + ((dst_negative_scale_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)))))) /\ (forall dst_index_delta_append_outputtable. (exists pvs_le_gap_delta_append_outputtabledomain. pvs_le_gap_delta_append_outputtabledomain + (dst_index_delta_append_outputtable) = (S N)) -> exists dst_positive_delta_append_outputtable dst_negative_delta_append_outputtable dst_value_delta_append_outputtable. ((((exists ff_h_pvs_delta_append_outputtableentrypositive. ff_h_pvs_delta_append_outputtableentrypositive + S (dst_positive_delta_append_outputtable) = S ((S (dst_index_delta_append_outputtable)) * dst_positive_scale_delta_append_outputtable)) /\ exists ff_q_pvs_delta_append_outputtableentrypositive. dst_positive_code_delta_append_outputtable = ff_q_pvs_delta_append_outputtableentrypositive * S ((S (dst_index_delta_append_outputtable)) * dst_positive_scale_delta_append_outputtable) + (dst_positive_delta_append_outputtable))) /\ (((((exists ff_h_pvs_delta_append_outputtableentrynegative. ff_h_pvs_delta_append_outputtableentrynegative + S (dst_negative_delta_append_outputtable) = S ((S (dst_index_delta_append_outputtable)) * dst_negative_scale_delta_append_outputtable)) /\ exists ff_q_pvs_delta_append_outputtableentrynegative. dst_negative_code_delta_append_outputtable = ff_q_pvs_delta_append_outputtableentrynegative * S ((S (dst_index_delta_append_outputtable)) * dst_negative_scale_delta_append_outputtable) + (dst_negative_delta_append_outputtable))) /\ (exists ge_balance_positive_delta_append_outputtableentryvalue ge_balance_negative_delta_append_outputtableentryvalue. (((((dst_value_delta_append_outputtable) = 2 * (ge_balance_positive_delta_append_outputtableentryvalue) /\ (ge_balance_negative_delta_append_outputtableentryvalue) = 0) \/ exists ge_signed_half_delta_append_outputtableentryvaluedecode. (((dst_value_delta_append_outputtable) = 2 * ge_signed_half_delta_append_outputtableentryvaluedecode + 1 /\ (ge_balance_positive_delta_append_outputtableentryvalue) = 0) /\ (ge_balance_negative_delta_append_outputtableentryvalue) = S ge_signed_half_delta_append_outputtableentryvaluedecode))) /\ ((dst_positive_delta_append_outputtable) + ge_balance_negative_delta_append_outputtableentryvalue = (dst_negative_delta_append_outputtable) + ge_balance_positive_delta_append_outputtableentryvalue))))))))) /\ (forall du_index_delta_append_output du_value_delta_append_output. ~(du_index_delta_append_output=0) -> (exists pvs_le_gap_delta_append_outputbound. pvs_le_gap_delta_append_outputbound + (du_index_delta_append_output) = (S N)) -> (exists dst_positive_code_delta_append_outputentry dst_positive_scale_delta_append_outputentry dst_negative_code_delta_append_outputentry dst_negative_scale_delta_append_outputentry dst_positive_delta_append_outputentry dst_negative_delta_append_outputentry. (((D) = (((((dst_positive_code_delta_append_outputentry) + (dst_positive_scale_delta_append_outputentry)) * S ((dst_positive_code_delta_append_outputentry) + (dst_positive_scale_delta_append_outputentry)) + ((dst_positive_scale_delta_append_outputentry) + (dst_positive_scale_delta_append_outputentry))) + (((dst_negative_code_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)) * S ((dst_negative_code_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)) + ((dst_negative_scale_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)))) * S ((((dst_positive_code_delta_append_outputentry) + (dst_positive_scale_delta_append_outputentry)) * S ((dst_positive_code_delta_append_outputentry) + (dst_positive_scale_delta_append_outputentry)) + ((dst_positive_scale_delta_append_outputentry) + (dst_positive_scale_delta_append_outputentry))) + (((dst_negative_code_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)) * S ((dst_negative_code_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)) + ((dst_negative_scale_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)))) + ((((dst_negative_code_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)) * S ((dst_negative_code_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)) + ((dst_negative_scale_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry))) + (((dst_negative_code_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)) * S ((dst_negative_code_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)) + ((dst_negative_scale_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)))))) /\ (((((exists ff_h_pvs_delta_append_outputentrypositive. ff_h_pvs_delta_append_outputentrypositive + S (dst_positive_delta_append_outputentry) = S ((S (du_index_delta_append_output)) * dst_positive_scale_delta_append_outputentry)) /\ exists ff_q_pvs_delta_append_outputentrypositive. dst_positive_code_delta_append_outputentry = ff_q_pvs_delta_append_outputentrypositive * S ((S (du_index_delta_append_output)) * dst_positive_scale_delta_append_outputentry) + (dst_positive_delta_append_outputentry))) /\ (((((exists ff_h_pvs_delta_append_outputentrynegative. ff_h_pvs_delta_append_outputentrynegative + S (dst_negative_delta_append_outputentry) = S ((S (du_index_delta_append_output)) * dst_negative_scale_delta_append_outputentry)) /\ exists ff_q_pvs_delta_append_outputentrynegative. dst_negative_code_delta_append_outputentry = ff_q_pvs_delta_append_outputentrynegative * S ((S (du_index_delta_append_output)) * dst_negative_scale_delta_append_outputentry) + (dst_negative_delta_append_outputentry))) /\ (exists ge_balance_positive_delta_append_outputentryvalue ge_balance_negative_delta_append_outputentryvalue. (((((du_value_delta_append_output) = 2 * (ge_balance_positive_delta_append_outputentryvalue) /\ (ge_balance_negative_delta_append_outputentryvalue) = 0) \/ exists ge_signed_half_delta_append_outputentryvaluedecode. (((du_value_delta_append_output) = 2 * ge_signed_half_delta_append_outputentryvaluedecode + 1 /\ (ge_balance_positive_delta_append_outputentryvalue) = 0) /\ (ge_balance_negative_delta_append_outputentryvalue) = S ge_signed_half_delta_append_outputentryvaluedecode))) /\ ((dst_positive_delta_append_outputentry) + ge_balance_negative_delta_append_outputentryvalue = (dst_negative_delta_append_outputentry) + ge_balance_positive_delta_append_outputentryvalue))))))))) -> ((((du_index_delta_append_output)=1 -> (du_value_delta_append_output)=2) /\ (~((du_index_delta_append_output)=1) -> (du_value_delta_append_output)=0)))))) /\ (forall dst_index_delta_append_prefix dst_first_delta_append_prefix dst_second_delta_append_prefix. (exists pvs_gap_delta_append_prefixbound. pvs_gap_delta_append_prefixbound + S (dst_index_delta_append_prefix) = (S N)) -> (exists dst_positive_code_delta_append_prefixfirst dst_positive_scale_delta_append_prefixfirst dst_negative_code_delta_append_prefixfirst dst_negative_scale_delta_append_prefixfirst dst_positive_delta_append_prefixfirst dst_negative_delta_append_prefixfirst. (((E) = (((((dst_positive_code_delta_append_prefixfirst) + (dst_positive_scale_delta_append_prefixfirst)) * S ((dst_positive_code_delta_append_prefixfirst) + (dst_positive_scale_delta_append_prefixfirst)) + ((dst_positive_scale_delta_append_prefixfirst) + (dst_positive_scale_delta_append_prefixfirst))) + (((dst_negative_code_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)) * S ((dst_negative_code_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)) + ((dst_negative_scale_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)))) * S ((((dst_positive_code_delta_append_prefixfirst) + (dst_positive_scale_delta_append_prefixfirst)) * S ((dst_positive_code_delta_append_prefixfirst) + (dst_positive_scale_delta_append_prefixfirst)) + ((dst_positive_scale_delta_append_prefixfirst) + (dst_positive_scale_delta_append_prefixfirst))) + (((dst_negative_code_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)) * S ((dst_negative_code_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)) + ((dst_negative_scale_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)))) + ((((dst_negative_code_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)) * S ((dst_negative_code_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)) + ((dst_negative_scale_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst))) + (((dst_negative_code_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)) * S ((dst_negative_code_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)) + ((dst_negative_scale_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)))))) /\ (((((exists ff_h_pvs_delta_append_prefixfirstpositive. ff_h_pvs_delta_append_prefixfirstpositive + S (dst_positive_delta_append_prefixfirst) = S ((S (dst_index_delta_append_prefix)) * dst_positive_scale_delta_append_prefixfirst)) /\ exists ff_q_pvs_delta_append_prefixfirstpositive. dst_positive_code_delta_append_prefixfirst = ff_q_pvs_delta_append_prefixfirstpositive * S ((S (dst_index_delta_append_prefix)) * dst_positive_scale_delta_append_prefixfirst) + (dst_positive_delta_append_prefixfirst))) /\ (((((exists ff_h_pvs_delta_append_prefixfirstnegative. ff_h_pvs_delta_append_prefixfirstnegative + S (dst_negative_delta_append_prefixfirst) = S ((S (dst_index_delta_append_prefix)) * dst_negative_scale_delta_append_prefixfirst)) /\ exists ff_q_pvs_delta_append_prefixfirstnegative. dst_negative_code_delta_append_prefixfirst = ff_q_pvs_delta_append_prefixfirstnegative * S ((S (dst_index_delta_append_prefix)) * dst_negative_scale_delta_append_prefixfirst) + (dst_negative_delta_append_prefixfirst))) /\ (exists ge_balance_positive_delta_append_prefixfirstvalue ge_balance_negative_delta_append_prefixfirstvalue. (((((dst_first_delta_append_prefix) = 2 * (ge_balance_positive_delta_append_prefixfirstvalue) /\ (ge_balance_negative_delta_append_prefixfirstvalue) = 0) \/ exists ge_signed_half_delta_append_prefixfirstvaluedecode. (((dst_first_delta_append_prefix) = 2 * ge_signed_half_delta_append_prefixfirstvaluedecode + 1 /\ (ge_balance_positive_delta_append_prefixfirstvalue) = 0) /\ (ge_balance_negative_delta_append_prefixfirstvalue) = S ge_signed_half_delta_append_prefixfirstvaluedecode))) /\ ((dst_positive_delta_append_prefixfirst) + ge_balance_negative_delta_append_prefixfirstvalue = (dst_negative_delta_append_prefixfirst) + ge_balance_positive_delta_append_prefixfirstvalue))))))))) -> (exists dst_positive_code_delta_append_prefixsecond dst_positive_scale_delta_append_prefixsecond dst_negative_code_delta_append_prefixsecond dst_negative_scale_delta_append_prefixsecond dst_positive_delta_append_prefixsecond dst_negative_delta_append_prefixsecond. (((D) = (((((dst_positive_code_delta_append_prefixsecond) + (dst_positive_scale_delta_append_prefixsecond)) * S ((dst_positive_code_delta_append_prefixsecond) + (dst_positive_scale_delta_append_prefixsecond)) + ((dst_positive_scale_delta_append_prefixsecond) + (dst_positive_scale_delta_append_prefixsecond))) + (((dst_negative_code_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)) * S ((dst_negative_code_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)) + ((dst_negative_scale_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)))) * S ((((dst_positive_code_delta_append_prefixsecond) + (dst_positive_scale_delta_append_prefixsecond)) * S ((dst_positive_code_delta_append_prefixsecond) + (dst_positive_scale_delta_append_prefixsecond)) + ((dst_positive_scale_delta_append_prefixsecond) + (dst_positive_scale_delta_append_prefixsecond))) + (((dst_negative_code_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)) * S ((dst_negative_code_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)) + ((dst_negative_scale_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)))) + ((((dst_negative_code_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)) * S ((dst_negative_code_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)) + ((dst_negative_scale_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond))) + (((dst_negative_code_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)) * S ((dst_negative_code_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)) + ((dst_negative_scale_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)))))) /\ (((((exists ff_h_pvs_delta_append_prefixsecondpositive. ff_h_pvs_delta_append_prefixsecondpositive + S (dst_positive_delta_append_prefixsecond) = S ((S (dst_index_delta_append_prefix)) * dst_positive_scale_delta_append_prefixsecond)) /\ exists ff_q_pvs_delta_append_prefixsecondpositive. dst_positive_code_delta_append_prefixsecond = ff_q_pvs_delta_append_prefixsecondpositive * S ((S (dst_index_delta_append_prefix)) * dst_positive_scale_delta_append_prefixsecond) + (dst_positive_delta_append_prefixsecond))) /\ (((((exists ff_h_pvs_delta_append_prefixsecondnegative. ff_h_pvs_delta_append_prefixsecondnegative + S (dst_negative_delta_append_prefixsecond) = S ((S (dst_index_delta_append_prefix)) * dst_negative_scale_delta_append_prefixsecond)) /\ exists ff_q_pvs_delta_append_prefixsecondnegative. dst_negative_code_delta_append_prefixsecond = ff_q_pvs_delta_append_prefixsecondnegative * S ((S (dst_index_delta_append_prefix)) * dst_negative_scale_delta_append_prefixsecond) + (dst_negative_delta_append_prefixsecond))) /\ (exists ge_balance_positive_delta_append_prefixsecondvalue ge_balance_negative_delta_append_prefixsecondvalue. (((((dst_second_delta_append_prefix) = 2 * (ge_balance_positive_delta_append_prefixsecondvalue) /\ (ge_balance_negative_delta_append_prefixsecondvalue) = 0) \/ exists ge_signed_half_delta_append_prefixsecondvaluedecode. (((dst_second_delta_append_prefix) = 2 * ge_signed_half_delta_append_prefixsecondvaluedecode + 1 /\ (ge_balance_positive_delta_append_prefixsecondvalue) = 0) /\ (ge_balance_negative_delta_append_prefixsecondvalue) = S ge_signed_half_delta_append_prefixsecondvaluedecode))) /\ ((dst_positive_delta_append_prefixsecond) + ge_balance_negative_delta_append_prefixsecondvalue = (dst_negative_delta_append_prefixsecond) + ge_balance_positive_delta_append_prefixsecondvalue))))))))) -> dst_first_delta_append_prefix = dst_second_delta_append_prefix)

Constructive proof overview

Generated structural guide

Append the separately chosen actual delta value, preserving every earlier signed entry rather than assuming a table oracle.

The unchanged tactic script uses 5 declared prerequisites and contains 77 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

DU0008 dirichlet_kronecker_delta_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

77 script commands · 19 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–5

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

  1. L1
    intro N
  2. L2
    intro F
  3. L3
    intro z
  4. L4
    intro hf
  5. L5
    intro hz
02Separate the logical casesL6–6

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

  1. L6
    cases hf
03Establish hxL7–12

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

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

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

  1. L13
    cases hx
  2. L14
    cases hx_witness
  3. L15
    cases hx_witness_right
05Construct an explicit witnessL16–16

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

  1. L16
    exists x
06Separate the logical casesL17–18

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

  1. L17
    split
  2. L18
    split
07Use earlier factsL19–19

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

  1. L19
    exact hx_witness_left
08Fix variables and assumptionsL20–24

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

  1. L20
    intro i
  2. L21
    intro a
  3. L22
    intro hi
  4. L23
    intro hb
  5. L24
    intro ha
09Establish hcL25–29

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

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

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

  1. L30
    cases hc
11Calculate and transport equalitiesL31–34

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

  1. L31
    rewrite hc_left at ha
  2. L32
    rewrite hc_left at ha
  3. L33
    rewrite hc_left at ha
  4. L34
    rewrite hc_left at ha
12Establish hvL35–44

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

  1. L35
    have hv : a=z
  2. L36
    specialize divisor_signed_table_at_functional (x)
  3. L37
    specialize divisor_signed_table_at_functional (S N)
  4. L38
    specialize divisor_signed_table_at_functional (a)
  5. L39
    specialize divisor_signed_table_at_functional (z)
  6. L40
    apply divisor_signed_table_at_functional
  7. L41
    exact ha
  8. L42
    exact hx_witness_right_right
  9. L43
    rewrite hc_left
  10. L44
    rewrite hc_left
13Calculate and transport equalitiesL45–46

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

  1. L45
    rewrite hv
  2. L46
    rewrite hv
14Use earlier factsL47–47

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

  1. L47
    exact hz
15Establish hibL48–52

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

  1. L48
    have hib : exists pvs_le_gap_append_old_bound. pvs_le_gap_append_old_bound + (i) = (N)
  2. L49
    specialize le_of_succ_le_succ (i)
  3. L50
    specialize le_of_succ_le_succ (N)
  4. L51
    apply le_of_succ_le_succ
  5. L52
    exact hc_right
16Establish hvL53–59

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

  1. L53
    have hv : ∃ v. ArithAt(F,i,v)Definitions: ArithAt
  2. L54
    specialize divisor_signed_table_lookup (N)
  3. L55
    specialize divisor_signed_table_lookup (F)
  4. L56
    specialize divisor_signed_table_lookup (i)
  5. L57
    apply divisor_signed_table_lookup
  6. L58
    exact hf_left
  7. L59
    exact hib
17Separate the logical casesL60–60

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

  1. L60
    cases hv
18Establish heqL61–70

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

  1. L61
    have heq : x1=a
  2. L62
    specialize hx_witness_right_left (i)
  3. L63
    specialize hx_witness_right_left (x1)
  4. L64
    specialize hx_witness_right_left (a)
  5. L65
    apply hx_witness_right_left
  6. L66
    exact hc_right
  7. L67
    exact hv_witness
  8. L68
    exact ha
  9. L69
    rewrite heq at hv_witness
  10. L70
    rewrite heq at hv_witness
19Use earlier factsL71–77

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

  1. L71
    specialize hf_right (i)
  2. L72
    specialize hf_right (a)
  3. L73
    apply hf_right
  4. L74
    exact hi
  5. L75
    exact hib
  6. L76
    exact hv_witness
  7. L77
    exact hx_witness_right_left

Library-wide reading audit

Original exact command ledger · 77 lines
  1. 0001intro N
  2. 0002intro F
  3. 0003intro z
  4. 0004intro hf
  5. 0005intro hz
  6. 0006cases hf
  7. 0007have 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. (((((z) = 2 * (ge_balance_positive_append_actuallastvalue) /\ (ge_balance_negative_append_actuallastvalue) = 0) \/ exists ge_signed_half_append_actuallastvaluedecode. (((z) = 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)))))))))))))
  8. 0008specialize arithmetic_signed_table_append (N)
  9. 0009specialize arithmetic_signed_table_append (F)
  10. 0010specialize arithmetic_signed_table_append (z)
  11. 0011apply arithmetic_signed_table_append
  12. 0012exact hf_left
  13. 0013cases hx
  14. 0014cases hx_witness
  15. 0015cases hx_witness_right
  16. 0016exists x
  17. 0017split
  18. 0018split
  19. 0019exact hx_witness_left
  20. 0020intro i
  21. 0021intro a
  22. 0022intro hi
  23. 0023intro hb
  24. 0024intro ha
  25. 0025have hc : i=S N \/ (exists pvs_gap_append_cases. pvs_gap_append_cases + S (i) = (S N))
  26. 0026specialize le_eq_or_lt (i)
  27. 0027specialize le_eq_or_lt (S N)
  28. 0028apply le_eq_or_lt
  29. 0029exact hb
  30. 0030cases hc
  31. 0031rewrite hc_left at ha
  32. 0032rewrite hc_left at ha
  33. 0033rewrite hc_left at ha
  34. 0034rewrite hc_left at ha
  35. 0035have hv : a=z
  36. 0036specialize divisor_signed_table_at_functional (x)
  37. 0037specialize divisor_signed_table_at_functional (S N)
  38. 0038specialize divisor_signed_table_at_functional (a)
  39. 0039specialize divisor_signed_table_at_functional (z)
  40. 0040apply divisor_signed_table_at_functional
  41. 0041exact ha
  42. 0042exact hx_witness_right_right
  43. 0043rewrite hc_left
  44. 0044rewrite hc_left
  45. 0045rewrite hv
  46. 0046rewrite hv
  47. 0047exact hz
  48. 0048have hib : exists pvs_le_gap_append_old_bound. pvs_le_gap_append_old_bound + (i) = (N)
  49. 0049specialize le_of_succ_le_succ (i)
  50. 0050specialize le_of_succ_le_succ (N)
  51. 0051apply le_of_succ_le_succ
  52. 0052exact hc_right
  53. 0053have 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)))))))))
  54. 0054specialize divisor_signed_table_lookup (N)
  55. 0055specialize divisor_signed_table_lookup (F)
  56. 0056specialize divisor_signed_table_lookup (i)
  57. 0057apply divisor_signed_table_lookup
  58. 0058exact hf_left
  59. 0059exact hib
  60. 0060cases hv
  61. 0061have heq : x1=a
  62. 0062specialize hx_witness_right_left (i)
  63. 0063specialize hx_witness_right_left (x1)
  64. 0064specialize hx_witness_right_left (a)
  65. 0065apply hx_witness_right_left
  66. 0066exact hc_right
  67. 0067exact hv_witness
  68. 0068exact ha
  69. 0069rewrite heq at hv_witness
  70. 0070rewrite heq at hv_witness
  71. 0071specialize hf_right (i)
  72. 0072specialize hf_right (a)
  73. 0073apply hf_right
  74. 0074exact hi
  75. 0075exact hib
  76. 0076exact hv_witness
  77. 0077exact hx_witness_right_left