DF000E

dirichlet_grid_table_exists

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

Construct the entire real first/last-factor grid, including its harmless extra certified endpoint, from actual input tables.

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 F G H n. (exists dst_positive_code_grid_F dst_positive_scale_grid_F dst_negative_code_grid_F dst_negative_scale_grid_F. (((F) = (((((dst_positive_code_grid_F) + (dst_positive_scale_grid_F)) * S ((dst_positive_code_grid_F) + (dst_positive_scale_grid_F)) + ((dst_positive_scale_grid_F) + (dst_positive_scale_grid_F))) + (((dst_negative_code_grid_F) + (dst_negative_scale_grid_F)) * S ((dst_negative_code_grid_F) + (dst_negative_scale_grid_F)) + ((dst_negative_scale_grid_F) + (dst_negative_scale_grid_F)))) * S ((((dst_positive_code_grid_F) + (dst_positive_scale_grid_F)) * S ((dst_positive_code_grid_F) + (dst_positive_scale_grid_F)) + ((dst_positive_scale_grid_F) + (dst_positive_scale_grid_F))) + (((dst_negative_code_grid_F) + (dst_negative_scale_grid_F)) * S ((dst_negative_code_grid_F) + (dst_negative_scale_grid_F)) + ((dst_negative_scale_grid_F) + (dst_negative_scale_grid_F)))) + ((((dst_negative_code_grid_F) + (dst_negative_scale_grid_F)) * S ((dst_negative_code_grid_F) + (dst_negative_scale_grid_F)) + ((dst_negative_scale_grid_F) + (dst_negative_scale_grid_F))) + (((dst_negative_code_grid_F) + (dst_negative_scale_grid_F)) * S ((dst_negative_code_grid_F) + (dst_negative_scale_grid_F)) + ((dst_negative_scale_grid_F) + (dst_negative_scale_grid_F)))))) /\ (forall dst_index_grid_F. (exists pvs_le_gap_grid_Fdomain. pvs_le_gap_grid_Fdomain + (dst_index_grid_F) = (0)) -> exists dst_positive_grid_F dst_negative_grid_F dst_value_grid_F. ((((exists ff_h_pvs_grid_Fentrypositive. ff_h_pvs_grid_Fentrypositive + S (dst_positive_grid_F) = S ((S (dst_index_grid_F)) * dst_positive_scale_grid_F)) /\ exists ff_q_pvs_grid_Fentrypositive. dst_positive_code_grid_F = ff_q_pvs_grid_Fentrypositive * S ((S (dst_index_grid_F)) * dst_positive_scale_grid_F) + (dst_positive_grid_F))) /\ (((((exists ff_h_pvs_grid_Fentrynegative. ff_h_pvs_grid_Fentrynegative + S (dst_negative_grid_F) = S ((S (dst_index_grid_F)) * dst_negative_scale_grid_F)) /\ exists ff_q_pvs_grid_Fentrynegative. dst_negative_code_grid_F = ff_q_pvs_grid_Fentrynegative * S ((S (dst_index_grid_F)) * dst_negative_scale_grid_F) + (dst_negative_grid_F))) /\ (exists ge_balance_positive_grid_Fentryvalue ge_balance_negative_grid_Fentryvalue. (((((dst_value_grid_F) = 2 * (ge_balance_positive_grid_Fentryvalue) /\ (ge_balance_negative_grid_Fentryvalue) = 0) \/ exists ge_signed_half_grid_Fentryvaluedecode. (((dst_value_grid_F) = 2 * ge_signed_half_grid_Fentryvaluedecode + 1 /\ (ge_balance_positive_grid_Fentryvalue) = 0) /\ (ge_balance_negative_grid_Fentryvalue) = S ge_signed_half_grid_Fentryvaluedecode))) /\ ((dst_positive_grid_F) + ge_balance_negative_grid_Fentryvalue = (dst_negative_grid_F) + ge_balance_positive_grid_Fentryvalue))))))))) -> (exists dst_positive_code_grid_G dst_positive_scale_grid_G dst_negative_code_grid_G dst_negative_scale_grid_G. (((G) = (((((dst_positive_code_grid_G) + (dst_positive_scale_grid_G)) * S ((dst_positive_code_grid_G) + (dst_positive_scale_grid_G)) + ((dst_positive_scale_grid_G) + (dst_positive_scale_grid_G))) + (((dst_negative_code_grid_G) + (dst_negative_scale_grid_G)) * S ((dst_negative_code_grid_G) + (dst_negative_scale_grid_G)) + ((dst_negative_scale_grid_G) + (dst_negative_scale_grid_G)))) * S ((((dst_positive_code_grid_G) + (dst_positive_scale_grid_G)) * S ((dst_positive_code_grid_G) + (dst_positive_scale_grid_G)) + ((dst_positive_scale_grid_G) + (dst_positive_scale_grid_G))) + (((dst_negative_code_grid_G) + (dst_negative_scale_grid_G)) * S ((dst_negative_code_grid_G) + (dst_negative_scale_grid_G)) + ((dst_negative_scale_grid_G) + (dst_negative_scale_grid_G)))) + ((((dst_negative_code_grid_G) + (dst_negative_scale_grid_G)) * S ((dst_negative_code_grid_G) + (dst_negative_scale_grid_G)) + ((dst_negative_scale_grid_G) + (dst_negative_scale_grid_G))) + (((dst_negative_code_grid_G) + (dst_negative_scale_grid_G)) * S ((dst_negative_code_grid_G) + (dst_negative_scale_grid_G)) + ((dst_negative_scale_grid_G) + (dst_negative_scale_grid_G)))))) /\ (forall dst_index_grid_G. (exists pvs_le_gap_grid_Gdomain. pvs_le_gap_grid_Gdomain + (dst_index_grid_G) = (0)) -> exists dst_positive_grid_G dst_negative_grid_G dst_value_grid_G. ((((exists ff_h_pvs_grid_Gentrypositive. ff_h_pvs_grid_Gentrypositive + S (dst_positive_grid_G) = S ((S (dst_index_grid_G)) * dst_positive_scale_grid_G)) /\ exists ff_q_pvs_grid_Gentrypositive. dst_positive_code_grid_G = ff_q_pvs_grid_Gentrypositive * S ((S (dst_index_grid_G)) * dst_positive_scale_grid_G) + (dst_positive_grid_G))) /\ (((((exists ff_h_pvs_grid_Gentrynegative. ff_h_pvs_grid_Gentrynegative + S (dst_negative_grid_G) = S ((S (dst_index_grid_G)) * dst_negative_scale_grid_G)) /\ exists ff_q_pvs_grid_Gentrynegative. dst_negative_code_grid_G = ff_q_pvs_grid_Gentrynegative * S ((S (dst_index_grid_G)) * dst_negative_scale_grid_G) + (dst_negative_grid_G))) /\ (exists ge_balance_positive_grid_Gentryvalue ge_balance_negative_grid_Gentryvalue. (((((dst_value_grid_G) = 2 * (ge_balance_positive_grid_Gentryvalue) /\ (ge_balance_negative_grid_Gentryvalue) = 0) \/ exists ge_signed_half_grid_Gentryvaluedecode. (((dst_value_grid_G) = 2 * ge_signed_half_grid_Gentryvaluedecode + 1 /\ (ge_balance_positive_grid_Gentryvalue) = 0) /\ (ge_balance_negative_grid_Gentryvalue) = S ge_signed_half_grid_Gentryvaluedecode))) /\ ((dst_positive_grid_G) + ge_balance_negative_grid_Gentryvalue = (dst_negative_grid_G) + ge_balance_positive_grid_Gentryvalue))))))))) -> (exists dst_positive_code_grid_H dst_positive_scale_grid_H dst_negative_code_grid_H dst_negative_scale_grid_H. (((H) = (((((dst_positive_code_grid_H) + (dst_positive_scale_grid_H)) * S ((dst_positive_code_grid_H) + (dst_positive_scale_grid_H)) + ((dst_positive_scale_grid_H) + (dst_positive_scale_grid_H))) + (((dst_negative_code_grid_H) + (dst_negative_scale_grid_H)) * S ((dst_negative_code_grid_H) + (dst_negative_scale_grid_H)) + ((dst_negative_scale_grid_H) + (dst_negative_scale_grid_H)))) * S ((((dst_positive_code_grid_H) + (dst_positive_scale_grid_H)) * S ((dst_positive_code_grid_H) + (dst_positive_scale_grid_H)) + ((dst_positive_scale_grid_H) + (dst_positive_scale_grid_H))) + (((dst_negative_code_grid_H) + (dst_negative_scale_grid_H)) * S ((dst_negative_code_grid_H) + (dst_negative_scale_grid_H)) + ((dst_negative_scale_grid_H) + (dst_negative_scale_grid_H)))) + ((((dst_negative_code_grid_H) + (dst_negative_scale_grid_H)) * S ((dst_negative_code_grid_H) + (dst_negative_scale_grid_H)) + ((dst_negative_scale_grid_H) + (dst_negative_scale_grid_H))) + (((dst_negative_code_grid_H) + (dst_negative_scale_grid_H)) * S ((dst_negative_code_grid_H) + (dst_negative_scale_grid_H)) + ((dst_negative_scale_grid_H) + (dst_negative_scale_grid_H)))))) /\ (forall dst_index_grid_H. (exists pvs_le_gap_grid_Hdomain. pvs_le_gap_grid_Hdomain + (dst_index_grid_H) = (0)) -> exists dst_positive_grid_H dst_negative_grid_H dst_value_grid_H. ((((exists ff_h_pvs_grid_Hentrypositive. ff_h_pvs_grid_Hentrypositive + S (dst_positive_grid_H) = S ((S (dst_index_grid_H)) * dst_positive_scale_grid_H)) /\ exists ff_q_pvs_grid_Hentrypositive. dst_positive_code_grid_H = ff_q_pvs_grid_Hentrypositive * S ((S (dst_index_grid_H)) * dst_positive_scale_grid_H) + (dst_positive_grid_H))) /\ (((((exists ff_h_pvs_grid_Hentrynegative. ff_h_pvs_grid_Hentrynegative + S (dst_negative_grid_H) = S ((S (dst_index_grid_H)) * dst_negative_scale_grid_H)) /\ exists ff_q_pvs_grid_Hentrynegative. dst_negative_code_grid_H = ff_q_pvs_grid_Hentrynegative * S ((S (dst_index_grid_H)) * dst_negative_scale_grid_H) + (dst_negative_grid_H))) /\ (exists ge_balance_positive_grid_Hentryvalue ge_balance_negative_grid_Hentryvalue. (((((dst_value_grid_H) = 2 * (ge_balance_positive_grid_Hentryvalue) /\ (ge_balance_negative_grid_Hentryvalue) = 0) \/ exists ge_signed_half_grid_Hentryvaluedecode. (((dst_value_grid_H) = 2 * ge_signed_half_grid_Hentryvaluedecode + 1 /\ (ge_balance_positive_grid_Hentryvalue) = 0) /\ (ge_balance_negative_grid_Hentryvalue) = S ge_signed_half_grid_Hentryvaluedecode))) /\ ((dst_positive_grid_H) + ge_balance_negative_grid_Hentryvalue = (dst_negative_grid_H) + ge_balance_positive_grid_Hentryvalue))))))))) -> exists T. (((exists dst_positive_code_grid_totaltable dst_positive_scale_grid_totaltable dst_negative_code_grid_totaltable dst_negative_scale_grid_totaltable. (((T) = (((((dst_positive_code_grid_totaltable) + (dst_positive_scale_grid_totaltable)) * S ((dst_positive_code_grid_totaltable) + (dst_positive_scale_grid_totaltable)) + ((dst_positive_scale_grid_totaltable) + (dst_positive_scale_grid_totaltable))) + (((dst_negative_code_grid_totaltable) + (dst_negative_scale_grid_totaltable)) * S ((dst_negative_code_grid_totaltable) + (dst_negative_scale_grid_totaltable)) + ((dst_negative_scale_grid_totaltable) + (dst_negative_scale_grid_totaltable)))) * S ((((dst_positive_code_grid_totaltable) + (dst_positive_scale_grid_totaltable)) * S ((dst_positive_code_grid_totaltable) + (dst_positive_scale_grid_totaltable)) + ((dst_positive_scale_grid_totaltable) + (dst_positive_scale_grid_totaltable))) + (((dst_negative_code_grid_totaltable) + (dst_negative_scale_grid_totaltable)) * S ((dst_negative_code_grid_totaltable) + (dst_negative_scale_grid_totaltable)) + ((dst_negative_scale_grid_totaltable) + (dst_negative_scale_grid_totaltable)))) + ((((dst_negative_code_grid_totaltable) + (dst_negative_scale_grid_totaltable)) * S ((dst_negative_code_grid_totaltable) + (dst_negative_scale_grid_totaltable)) + ((dst_negative_scale_grid_totaltable) + (dst_negative_scale_grid_totaltable))) + (((dst_negative_code_grid_totaltable) + (dst_negative_scale_grid_totaltable)) * S ((dst_negative_code_grid_totaltable) + (dst_negative_scale_grid_totaltable)) + ((dst_negative_scale_grid_totaltable) + (dst_negative_scale_grid_totaltable)))))) /\ (forall dst_index_grid_totaltable. (exists pvs_le_gap_grid_totaltabledomain. pvs_le_gap_grid_totaltabledomain + (dst_index_grid_totaltable) = ((S (n))*(S (n)))) -> exists dst_positive_grid_totaltable dst_negative_grid_totaltable dst_value_grid_totaltable. ((((exists ff_h_pvs_grid_totaltableentrypositive. ff_h_pvs_grid_totaltableentrypositive + S (dst_positive_grid_totaltable) = S ((S (dst_index_grid_totaltable)) * dst_positive_scale_grid_totaltable)) /\ exists ff_q_pvs_grid_totaltableentrypositive. dst_positive_code_grid_totaltable = ff_q_pvs_grid_totaltableentrypositive * S ((S (dst_index_grid_totaltable)) * dst_positive_scale_grid_totaltable) + (dst_positive_grid_totaltable))) /\ (((((exists ff_h_pvs_grid_totaltableentrynegative. ff_h_pvs_grid_totaltableentrynegative + S (dst_negative_grid_totaltable) = S ((S (dst_index_grid_totaltable)) * dst_negative_scale_grid_totaltable)) /\ exists ff_q_pvs_grid_totaltableentrynegative. dst_negative_code_grid_totaltable = ff_q_pvs_grid_totaltableentrynegative * S ((S (dst_index_grid_totaltable)) * dst_negative_scale_grid_totaltable) + (dst_negative_grid_totaltable))) /\ (exists ge_balance_positive_grid_totaltableentryvalue ge_balance_negative_grid_totaltableentryvalue. (((((dst_value_grid_totaltable) = 2 * (ge_balance_positive_grid_totaltableentryvalue) /\ (ge_balance_negative_grid_totaltableentryvalue) = 0) \/ exists ge_signed_half_grid_totaltableentryvaluedecode. (((dst_value_grid_totaltable) = 2 * ge_signed_half_grid_totaltableentryvaluedecode + 1 /\ (ge_balance_positive_grid_totaltableentryvalue) = 0) /\ (ge_balance_negative_grid_totaltableentryvalue) = S ge_signed_half_grid_totaltableentryvaluedecode))) /\ ((dst_positive_grid_totaltable) + ge_balance_negative_grid_totaltableentryvalue = (dst_negative_grid_totaltable) + ge_balance_positive_grid_totaltableentryvalue))))))))) /\ (forall dfg_grid_row_grid_total dfg_grid_column_grid_total dfg_grid_value_grid_total. (exists pvs_le_gap_grid_totalrow. pvs_le_gap_grid_totalrow + (dfg_grid_row_grid_total) = (n)) -> (exists pvs_le_gap_grid_totalcolumn. pvs_le_gap_grid_totalcolumn + (dfg_grid_column_grid_total) = (n)) -> (exists dst_positive_code_grid_totallookup dst_positive_scale_grid_totallookup dst_negative_code_grid_totallookup dst_negative_scale_grid_totallookup dst_positive_grid_totallookup dst_negative_grid_totallookup. (((T) = (((((dst_positive_code_grid_totallookup) + (dst_positive_scale_grid_totallookup)) * S ((dst_positive_code_grid_totallookup) + (dst_positive_scale_grid_totallookup)) + ((dst_positive_scale_grid_totallookup) + (dst_positive_scale_grid_totallookup))) + (((dst_negative_code_grid_totallookup) + (dst_negative_scale_grid_totallookup)) * S ((dst_negative_code_grid_totallookup) + (dst_negative_scale_grid_totallookup)) + ((dst_negative_scale_grid_totallookup) + (dst_negative_scale_grid_totallookup)))) * S ((((dst_positive_code_grid_totallookup) + (dst_positive_scale_grid_totallookup)) * S ((dst_positive_code_grid_totallookup) + (dst_positive_scale_grid_totallookup)) + ((dst_positive_scale_grid_totallookup) + (dst_positive_scale_grid_totallookup))) + (((dst_negative_code_grid_totallookup) + (dst_negative_scale_grid_totallookup)) * S ((dst_negative_code_grid_totallookup) + (dst_negative_scale_grid_totallookup)) + ((dst_negative_scale_grid_totallookup) + (dst_negative_scale_grid_totallookup)))) + ((((dst_negative_code_grid_totallookup) + (dst_negative_scale_grid_totallookup)) * S ((dst_negative_code_grid_totallookup) + (dst_negative_scale_grid_totallookup)) + ((dst_negative_scale_grid_totallookup) + (dst_negative_scale_grid_totallookup))) + (((dst_negative_code_grid_totallookup) + (dst_negative_scale_grid_totallookup)) * S ((dst_negative_code_grid_totallookup) + (dst_negative_scale_grid_totallookup)) + ((dst_negative_scale_grid_totallookup) + (dst_negative_scale_grid_totallookup)))))) /\ (((((exists ff_h_pvs_grid_totallookuppositive. ff_h_pvs_grid_totallookuppositive + S (dst_positive_grid_totallookup) = S ((S ((S (n))*(dfg_grid_row_grid_total)+(dfg_grid_column_grid_total))) * dst_positive_scale_grid_totallookup)) /\ exists ff_q_pvs_grid_totallookuppositive. dst_positive_code_grid_totallookup = ff_q_pvs_grid_totallookuppositive * S ((S ((S (n))*(dfg_grid_row_grid_total)+(dfg_grid_column_grid_total))) * dst_positive_scale_grid_totallookup) + (dst_positive_grid_totallookup))) /\ (((((exists ff_h_pvs_grid_totallookupnegative. ff_h_pvs_grid_totallookupnegative + S (dst_negative_grid_totallookup) = S ((S ((S (n))*(dfg_grid_row_grid_total)+(dfg_grid_column_grid_total))) * dst_negative_scale_grid_totallookup)) /\ exists ff_q_pvs_grid_totallookupnegative. dst_negative_code_grid_totallookup = ff_q_pvs_grid_totallookupnegative * S ((S ((S (n))*(dfg_grid_row_grid_total)+(dfg_grid_column_grid_total))) * dst_negative_scale_grid_totallookup) + (dst_negative_grid_totallookup))) /\ (exists ge_balance_positive_grid_totallookupvalue ge_balance_negative_grid_totallookupvalue. (((((dfg_grid_value_grid_total) = 2 * (ge_balance_positive_grid_totallookupvalue) /\ (ge_balance_negative_grid_totallookupvalue) = 0) \/ exists ge_signed_half_grid_totallookupvaluedecode. (((dfg_grid_value_grid_total) = 2 * ge_signed_half_grid_totallookupvaluedecode + 1 /\ (ge_balance_positive_grid_totallookupvalue) = 0) /\ (ge_balance_negative_grid_totallookupvalue) = S ge_signed_half_grid_totallookupvaluedecode))) /\ ((dst_positive_grid_totallookup) + ge_balance_negative_grid_totallookupvalue = (dst_negative_grid_totallookup) + ge_balance_positive_grid_totallookupvalue))))))))) -> ((((~((dfg_grid_row_grid_total)=0)) /\ (((~((dfg_grid_column_grid_total)=0)) /\ (exists dfg_middle_grid_totalentry dfg_first_grid_totalentry dfg_last_grid_totalentry dfg_value_grid_totalentry. (((n)=((dfg_grid_row_grid_total)*(dfg_grid_column_grid_total))*dfg_middle_grid_totalentry) /\ (((exists dst_positive_code_grid_totalentryfirst dst_positive_scale_grid_totalentryfirst dst_negative_code_grid_totalentryfirst dst_negative_scale_grid_totalentryfirst dst_positive_grid_totalentryfirst dst_negative_grid_totalentryfirst. (((F) = (((((dst_positive_code_grid_totalentryfirst) + (dst_positive_scale_grid_totalentryfirst)) * S ((dst_positive_code_grid_totalentryfirst) + (dst_positive_scale_grid_totalentryfirst)) + ((dst_positive_scale_grid_totalentryfirst) + (dst_positive_scale_grid_totalentryfirst))) + (((dst_negative_code_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)) * S ((dst_negative_code_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)) + ((dst_negative_scale_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)))) * S ((((dst_positive_code_grid_totalentryfirst) + (dst_positive_scale_grid_totalentryfirst)) * S ((dst_positive_code_grid_totalentryfirst) + (dst_positive_scale_grid_totalentryfirst)) + ((dst_positive_scale_grid_totalentryfirst) + (dst_positive_scale_grid_totalentryfirst))) + (((dst_negative_code_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)) * S ((dst_negative_code_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)) + ((dst_negative_scale_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)))) + ((((dst_negative_code_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)) * S ((dst_negative_code_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)) + ((dst_negative_scale_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst))) + (((dst_negative_code_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)) * S ((dst_negative_code_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)) + ((dst_negative_scale_grid_totalentryfirst) + (dst_negative_scale_grid_totalentryfirst)))))) /\ (((((exists ff_h_pvs_grid_totalentryfirstpositive. ff_h_pvs_grid_totalentryfirstpositive + S (dst_positive_grid_totalentryfirst) = S ((S (dfg_grid_row_grid_total)) * dst_positive_scale_grid_totalentryfirst)) /\ exists ff_q_pvs_grid_totalentryfirstpositive. dst_positive_code_grid_totalentryfirst = ff_q_pvs_grid_totalentryfirstpositive * S ((S (dfg_grid_row_grid_total)) * dst_positive_scale_grid_totalentryfirst) + (dst_positive_grid_totalentryfirst))) /\ (((((exists ff_h_pvs_grid_totalentryfirstnegative. ff_h_pvs_grid_totalentryfirstnegative + S (dst_negative_grid_totalentryfirst) = S ((S (dfg_grid_row_grid_total)) * dst_negative_scale_grid_totalentryfirst)) /\ exists ff_q_pvs_grid_totalentryfirstnegative. dst_negative_code_grid_totalentryfirst = ff_q_pvs_grid_totalentryfirstnegative * S ((S (dfg_grid_row_grid_total)) * dst_negative_scale_grid_totalentryfirst) + (dst_negative_grid_totalentryfirst))) /\ (exists ge_balance_positive_grid_totalentryfirstvalue ge_balance_negative_grid_totalentryfirstvalue. (((((dfg_first_grid_totalentry) = 2 * (ge_balance_positive_grid_totalentryfirstvalue) /\ (ge_balance_negative_grid_totalentryfirstvalue) = 0) \/ exists ge_signed_half_grid_totalentryfirstvaluedecode. (((dfg_first_grid_totalentry) = 2 * ge_signed_half_grid_totalentryfirstvaluedecode + 1 /\ (ge_balance_positive_grid_totalentryfirstvalue) = 0) /\ (ge_balance_negative_grid_totalentryfirstvalue) = S ge_signed_half_grid_totalentryfirstvaluedecode))) /\ ((dst_positive_grid_totalentryfirst) + ge_balance_negative_grid_totalentryfirstvalue = (dst_negative_grid_totalentryfirst) + ge_balance_positive_grid_totalentryfirstvalue))))))))) /\ (((exists dst_positive_code_grid_totalentrylast dst_positive_scale_grid_totalentrylast dst_negative_code_grid_totalentrylast dst_negative_scale_grid_totalentrylast dst_positive_grid_totalentrylast dst_negative_grid_totalentrylast. (((H) = (((((dst_positive_code_grid_totalentrylast) + (dst_positive_scale_grid_totalentrylast)) * S ((dst_positive_code_grid_totalentrylast) + (dst_positive_scale_grid_totalentrylast)) + ((dst_positive_scale_grid_totalentrylast) + (dst_positive_scale_grid_totalentrylast))) + (((dst_negative_code_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)) * S ((dst_negative_code_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)) + ((dst_negative_scale_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)))) * S ((((dst_positive_code_grid_totalentrylast) + (dst_positive_scale_grid_totalentrylast)) * S ((dst_positive_code_grid_totalentrylast) + (dst_positive_scale_grid_totalentrylast)) + ((dst_positive_scale_grid_totalentrylast) + (dst_positive_scale_grid_totalentrylast))) + (((dst_negative_code_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)) * S ((dst_negative_code_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)) + ((dst_negative_scale_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)))) + ((((dst_negative_code_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)) * S ((dst_negative_code_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)) + ((dst_negative_scale_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast))) + (((dst_negative_code_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)) * S ((dst_negative_code_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)) + ((dst_negative_scale_grid_totalentrylast) + (dst_negative_scale_grid_totalentrylast)))))) /\ (((((exists ff_h_pvs_grid_totalentrylastpositive. ff_h_pvs_grid_totalentrylastpositive + S (dst_positive_grid_totalentrylast) = S ((S (dfg_grid_column_grid_total)) * dst_positive_scale_grid_totalentrylast)) /\ exists ff_q_pvs_grid_totalentrylastpositive. dst_positive_code_grid_totalentrylast = ff_q_pvs_grid_totalentrylastpositive * S ((S (dfg_grid_column_grid_total)) * dst_positive_scale_grid_totalentrylast) + (dst_positive_grid_totalentrylast))) /\ (((((exists ff_h_pvs_grid_totalentrylastnegative. ff_h_pvs_grid_totalentrylastnegative + S (dst_negative_grid_totalentrylast) = S ((S (dfg_grid_column_grid_total)) * dst_negative_scale_grid_totalentrylast)) /\ exists ff_q_pvs_grid_totalentrylastnegative. dst_negative_code_grid_totalentrylast = ff_q_pvs_grid_totalentrylastnegative * S ((S (dfg_grid_column_grid_total)) * dst_negative_scale_grid_totalentrylast) + (dst_negative_grid_totalentrylast))) /\ (exists ge_balance_positive_grid_totalentrylastvalue ge_balance_negative_grid_totalentrylastvalue. (((((dfg_last_grid_totalentry) = 2 * (ge_balance_positive_grid_totalentrylastvalue) /\ (ge_balance_negative_grid_totalentrylastvalue) = 0) \/ exists ge_signed_half_grid_totalentrylastvaluedecode. (((dfg_last_grid_totalentry) = 2 * ge_signed_half_grid_totalentrylastvaluedecode + 1 /\ (ge_balance_positive_grid_totalentrylastvalue) = 0) /\ (ge_balance_negative_grid_totalentrylastvalue) = S ge_signed_half_grid_totalentrylastvaluedecode))) /\ ((dst_positive_grid_totalentrylast) + ge_balance_negative_grid_totalentrylastvalue = (dst_negative_grid_totalentrylast) + ge_balance_positive_grid_totalentrylastvalue))))))))) /\ (((exists dst_positive_code_grid_totalentrymiddle dst_positive_scale_grid_totalentrymiddle dst_negative_code_grid_totalentrymiddle dst_negative_scale_grid_totalentrymiddle dst_positive_grid_totalentrymiddle dst_negative_grid_totalentrymiddle. (((G) = (((((dst_positive_code_grid_totalentrymiddle) + (dst_positive_scale_grid_totalentrymiddle)) * S ((dst_positive_code_grid_totalentrymiddle) + (dst_positive_scale_grid_totalentrymiddle)) + ((dst_positive_scale_grid_totalentrymiddle) + (dst_positive_scale_grid_totalentrymiddle))) + (((dst_negative_code_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)) * S ((dst_negative_code_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)) + ((dst_negative_scale_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)))) * S ((((dst_positive_code_grid_totalentrymiddle) + (dst_positive_scale_grid_totalentrymiddle)) * S ((dst_positive_code_grid_totalentrymiddle) + (dst_positive_scale_grid_totalentrymiddle)) + ((dst_positive_scale_grid_totalentrymiddle) + (dst_positive_scale_grid_totalentrymiddle))) + (((dst_negative_code_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)) * S ((dst_negative_code_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)) + ((dst_negative_scale_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)))) + ((((dst_negative_code_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)) * S ((dst_negative_code_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)) + ((dst_negative_scale_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle))) + (((dst_negative_code_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)) * S ((dst_negative_code_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)) + ((dst_negative_scale_grid_totalentrymiddle) + (dst_negative_scale_grid_totalentrymiddle)))))) /\ (((((exists ff_h_pvs_grid_totalentrymiddlepositive. ff_h_pvs_grid_totalentrymiddlepositive + S (dst_positive_grid_totalentrymiddle) = S ((S (dfg_middle_grid_totalentry)) * dst_positive_scale_grid_totalentrymiddle)) /\ exists ff_q_pvs_grid_totalentrymiddlepositive. dst_positive_code_grid_totalentrymiddle = ff_q_pvs_grid_totalentrymiddlepositive * S ((S (dfg_middle_grid_totalentry)) * dst_positive_scale_grid_totalentrymiddle) + (dst_positive_grid_totalentrymiddle))) /\ (((((exists ff_h_pvs_grid_totalentrymiddlenegative. ff_h_pvs_grid_totalentrymiddlenegative + S (dst_negative_grid_totalentrymiddle) = S ((S (dfg_middle_grid_totalentry)) * dst_negative_scale_grid_totalentrymiddle)) /\ exists ff_q_pvs_grid_totalentrymiddlenegative. dst_negative_code_grid_totalentrymiddle = ff_q_pvs_grid_totalentrymiddlenegative * S ((S (dfg_middle_grid_totalentry)) * dst_negative_scale_grid_totalentrymiddle) + (dst_negative_grid_totalentrymiddle))) /\ (exists ge_balance_positive_grid_totalentrymiddlevalue ge_balance_negative_grid_totalentrymiddlevalue. (((((dfg_value_grid_totalentry) = 2 * (ge_balance_positive_grid_totalentrymiddlevalue) /\ (ge_balance_negative_grid_totalentrymiddlevalue) = 0) \/ exists ge_signed_half_grid_totalentrymiddlevaluedecode. (((dfg_value_grid_totalentry) = 2 * ge_signed_half_grid_totalentrymiddlevaluedecode + 1 /\ (ge_balance_positive_grid_totalentrymiddlevalue) = 0) /\ (ge_balance_negative_grid_totalentrymiddlevalue) = S ge_signed_half_grid_totalentrymiddlevaluedecode))) /\ ((dst_positive_grid_totalentrymiddle) + ge_balance_negative_grid_totalentrymiddlevalue = (dst_negative_grid_totalentrymiddle) + ge_balance_positive_grid_totalentrymiddlevalue))))))))) /\ (exists dfg_inner_grid_totalentryproduct. ((exists sto_ap_grid_totalentryproductinner sto_an_grid_totalentryproductinner sto_bp_grid_totalentryproductinner sto_bn_grid_totalentryproductinner sto_cp_grid_totalentryproductinner sto_cn_grid_totalentryproductinner. (((((dfg_last_grid_totalentry) = 2 * (sto_ap_grid_totalentryproductinner) /\ (sto_an_grid_totalentryproductinner) = 0) \/ exists ge_signed_half_grid_totalentryproductinnerleft. (((dfg_last_grid_totalentry) = 2 * ge_signed_half_grid_totalentryproductinnerleft + 1 /\ (sto_ap_grid_totalentryproductinner) = 0) /\ (sto_an_grid_totalentryproductinner) = S ge_signed_half_grid_totalentryproductinnerleft))) /\ ((((((dfg_value_grid_totalentry) = 2 * (sto_bp_grid_totalentryproductinner) /\ (sto_bn_grid_totalentryproductinner) = 0) \/ exists ge_signed_half_grid_totalentryproductinnerright. (((dfg_value_grid_totalentry) = 2 * ge_signed_half_grid_totalentryproductinnerright + 1 /\ (sto_bp_grid_totalentryproductinner) = 0) /\ (sto_bn_grid_totalentryproductinner) = S ge_signed_half_grid_totalentryproductinnerright))) /\ ((((((dfg_inner_grid_totalentryproduct) = 2 * (sto_cp_grid_totalentryproductinner) /\ (sto_cn_grid_totalentryproductinner) = 0) \/ exists ge_signed_half_grid_totalentryproductinneroutput. (((dfg_inner_grid_totalentryproduct) = 2 * ge_signed_half_grid_totalentryproductinneroutput + 1 /\ (sto_cp_grid_totalentryproductinner) = 0) /\ (sto_cn_grid_totalentryproductinner) = S ge_signed_half_grid_totalentryproductinneroutput))) /\ ((sto_ap_grid_totalentryproductinner * sto_bp_grid_totalentryproductinner + sto_an_grid_totalentryproductinner * sto_bn_grid_totalentryproductinner) + sto_cn_grid_totalentryproductinner = (sto_ap_grid_totalentryproductinner * sto_bn_grid_totalentryproductinner + sto_an_grid_totalentryproductinner * sto_bp_grid_totalentryproductinner) + sto_cp_grid_totalentryproductinner))))))) /\ (exists sto_ap_grid_totalentryproductouter sto_an_grid_totalentryproductouter sto_bp_grid_totalentryproductouter sto_bn_grid_totalentryproductouter sto_cp_grid_totalentryproductouter sto_cn_grid_totalentryproductouter. (((((dfg_first_grid_totalentry) = 2 * (sto_ap_grid_totalentryproductouter) /\ (sto_an_grid_totalentryproductouter) = 0) \/ exists ge_signed_half_grid_totalentryproductouterleft. (((dfg_first_grid_totalentry) = 2 * ge_signed_half_grid_totalentryproductouterleft + 1 /\ (sto_ap_grid_totalentryproductouter) = 0) /\ (sto_an_grid_totalentryproductouter) = S ge_signed_half_grid_totalentryproductouterleft))) /\ ((((((dfg_inner_grid_totalentryproduct) = 2 * (sto_bp_grid_totalentryproductouter) /\ (sto_bn_grid_totalentryproductouter) = 0) \/ exists ge_signed_half_grid_totalentryproductouterright. (((dfg_inner_grid_totalentryproduct) = 2 * ge_signed_half_grid_totalentryproductouterright + 1 /\ (sto_bp_grid_totalentryproductouter) = 0) /\ (sto_bn_grid_totalentryproductouter) = S ge_signed_half_grid_totalentryproductouterright))) /\ ((((((dfg_grid_value_grid_total) = 2 * (sto_cp_grid_totalentryproductouter) /\ (sto_cn_grid_totalentryproductouter) = 0) \/ exists ge_signed_half_grid_totalentryproductouteroutput. (((dfg_grid_value_grid_total) = 2 * ge_signed_half_grid_totalentryproductouteroutput + 1 /\ (sto_cp_grid_totalentryproductouter) = 0) /\ (sto_cn_grid_totalentryproductouter) = S ge_signed_half_grid_totalentryproductouteroutput))) /\ ((sto_ap_grid_totalentryproductouter * sto_bp_grid_totalentryproductouter + sto_an_grid_totalentryproductouter * sto_bn_grid_totalentryproductouter) + sto_cn_grid_totalentryproductouter = (sto_ap_grid_totalentryproductouter * sto_bn_grid_totalentryproductouter + sto_an_grid_totalentryproductouter * sto_bp_grid_totalentryproductouter) + sto_cp_grid_totalentryproductouter))))))))))))))))))))) \/ ((((dfg_grid_row_grid_total)=0 \/ ((dfg_grid_column_grid_total)=0 \/ ~(exists pvs_factor_grid_totalentryomittednondivisor. (n) = ((dfg_grid_row_grid_total)*(dfg_grid_column_grid_total)) * pvs_factor_grid_totalentryomittednondivisor))) /\ ((dfg_grid_value_grid_total)=0)))))))

Constructive proof overview

Generated structural guide

Construct the entire real first/last-factor grid, including its harmless extra certified endpoint, from actual input tables.

The unchanged tactic script uses 2 declared prerequisites and contains 26 exact native proof lines.

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

Proof neighborhood

Direct dependencies

DF000C dirichlet_grid_flat_prefix_exists DF000D dirichlet_grid_from_flat_prefix

Direct dependents

DF0017 dirichlet_grid_fubini_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

26 script commands · 5 reading checkpoints · 1 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.

Named ingredients (2)
dirichlet grid flat prefix existsdirichlet grid from flat prefix

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–7

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

  1. L1
    intro F
  2. L2
    intro G
  3. L3
    intro H
  4. L4
    intro n
  5. L5
    intro hF
  6. L6
    intro hG
  7. L7
    intro hH
02Establish hpL8–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet grid flat prefix exists.

  1. L8
    have hp : ∃ T. DirichletFlatPrefix(F,G,H,n,S n · S n,T)Definitions: DirichletFlatPrefix
  2. L9
    specialize dirichlet_grid_flat_prefix_exists (F)
  3. L10
    specialize dirichlet_grid_flat_prefix_exists (G)
  4. L11
    specialize dirichlet_grid_flat_prefix_exists (H)
  5. L12
    specialize dirichlet_grid_flat_prefix_exists (n)
  6. L13
    specialize dirichlet_grid_flat_prefix_exists ((S n)*(S n))
  7. L14
    apply dirichlet_grid_flat_prefix_exists
  8. L15
    exact hF
  9. L16
    exact hG
  10. L17
    exact hH
03Separate the logical casesL18–18

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

  1. L18
    cases hp
04Construct an explicit witnessL19–19

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

  1. L19
    exists x
05Use earlier factsL20–26

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

  1. L20
    specialize dirichlet_grid_from_flat_prefix (F)
  2. L21
    specialize dirichlet_grid_from_flat_prefix (G)
  3. L22
    specialize dirichlet_grid_from_flat_prefix (H)
  4. L23
    specialize dirichlet_grid_from_flat_prefix (n)
  5. L24
    specialize dirichlet_grid_from_flat_prefix (x)
  6. L25
    apply dirichlet_grid_from_flat_prefix
  7. L26
    exact hp_witness

Library-wide reading audit

Original exact command ledger · 26 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro H
  4. 0004intro n
  5. 0005intro hF
  6. 0006intro hG
  7. 0007intro hH
  8. 0008have hp : exists T. (((exists dst_positive_code_grid_flattable dst_positive_scale_grid_flattable dst_negative_code_grid_flattable dst_negative_scale_grid_flattable. (((T) = (((((dst_positive_code_grid_flattable) + (dst_positive_scale_grid_flattable)) * S ((dst_positive_code_grid_flattable) + (dst_positive_scale_grid_flattable)) + ((dst_positive_scale_grid_flattable) + (dst_positive_scale_grid_flattable))) + (((dst_negative_code_grid_flattable) + (dst_negative_scale_grid_flattable)) * S ((dst_negative_code_grid_flattable) + (dst_negative_scale_grid_flattable)) + ((dst_negative_scale_grid_flattable) + (dst_negative_scale_grid_flattable)))) * S ((((dst_positive_code_grid_flattable) + (dst_positive_scale_grid_flattable)) * S ((dst_positive_code_grid_flattable) + (dst_positive_scale_grid_flattable)) + ((dst_positive_scale_grid_flattable) + (dst_positive_scale_grid_flattable))) + (((dst_negative_code_grid_flattable) + (dst_negative_scale_grid_flattable)) * S ((dst_negative_code_grid_flattable) + (dst_negative_scale_grid_flattable)) + ((dst_negative_scale_grid_flattable) + (dst_negative_scale_grid_flattable)))) + ((((dst_negative_code_grid_flattable) + (dst_negative_scale_grid_flattable)) * S ((dst_negative_code_grid_flattable) + (dst_negative_scale_grid_flattable)) + ((dst_negative_scale_grid_flattable) + (dst_negative_scale_grid_flattable))) + (((dst_negative_code_grid_flattable) + (dst_negative_scale_grid_flattable)) * S ((dst_negative_code_grid_flattable) + (dst_negative_scale_grid_flattable)) + ((dst_negative_scale_grid_flattable) + (dst_negative_scale_grid_flattable)))))) /\ (forall dst_index_grid_flattable. (exists pvs_le_gap_grid_flattabledomain. pvs_le_gap_grid_flattabledomain + (dst_index_grid_flattable) = ((S n)*(S n))) -> exists dst_positive_grid_flattable dst_negative_grid_flattable dst_value_grid_flattable. ((((exists ff_h_pvs_grid_flattableentrypositive. ff_h_pvs_grid_flattableentrypositive + S (dst_positive_grid_flattable) = S ((S (dst_index_grid_flattable)) * dst_positive_scale_grid_flattable)) /\ exists ff_q_pvs_grid_flattableentrypositive. dst_positive_code_grid_flattable = ff_q_pvs_grid_flattableentrypositive * S ((S (dst_index_grid_flattable)) * dst_positive_scale_grid_flattable) + (dst_positive_grid_flattable))) /\ (((((exists ff_h_pvs_grid_flattableentrynegative. ff_h_pvs_grid_flattableentrynegative + S (dst_negative_grid_flattable) = S ((S (dst_index_grid_flattable)) * dst_negative_scale_grid_flattable)) /\ exists ff_q_pvs_grid_flattableentrynegative. dst_negative_code_grid_flattable = ff_q_pvs_grid_flattableentrynegative * S ((S (dst_index_grid_flattable)) * dst_negative_scale_grid_flattable) + (dst_negative_grid_flattable))) /\ (exists ge_balance_positive_grid_flattableentryvalue ge_balance_negative_grid_flattableentryvalue. (((((dst_value_grid_flattable) = 2 * (ge_balance_positive_grid_flattableentryvalue) /\ (ge_balance_negative_grid_flattableentryvalue) = 0) \/ exists ge_signed_half_grid_flattableentryvaluedecode. (((dst_value_grid_flattable) = 2 * ge_signed_half_grid_flattableentryvaluedecode + 1 /\ (ge_balance_positive_grid_flattableentryvalue) = 0) /\ (ge_balance_negative_grid_flattableentryvalue) = S ge_signed_half_grid_flattableentryvaluedecode))) /\ ((dst_positive_grid_flattable) + ge_balance_negative_grid_flattableentryvalue = (dst_negative_grid_flattable) + ge_balance_positive_grid_flattableentryvalue))))))))) /\ (forall dfg_flat_index_grid_flat dfg_flat_value_grid_flat. (exists pvs_le_gap_grid_flatbound. pvs_le_gap_grid_flatbound + (dfg_flat_index_grid_flat) = ((S n)*(S n))) -> (exists dst_positive_code_grid_flatlookup dst_positive_scale_grid_flatlookup dst_negative_code_grid_flatlookup dst_negative_scale_grid_flatlookup dst_positive_grid_flatlookup dst_negative_grid_flatlookup. (((T) = (((((dst_positive_code_grid_flatlookup) + (dst_positive_scale_grid_flatlookup)) * S ((dst_positive_code_grid_flatlookup) + (dst_positive_scale_grid_flatlookup)) + ((dst_positive_scale_grid_flatlookup) + (dst_positive_scale_grid_flatlookup))) + (((dst_negative_code_grid_flatlookup) + (dst_negative_scale_grid_flatlookup)) * S ((dst_negative_code_grid_flatlookup) + (dst_negative_scale_grid_flatlookup)) + ((dst_negative_scale_grid_flatlookup) + (dst_negative_scale_grid_flatlookup)))) * S ((((dst_positive_code_grid_flatlookup) + (dst_positive_scale_grid_flatlookup)) * S ((dst_positive_code_grid_flatlookup) + (dst_positive_scale_grid_flatlookup)) + ((dst_positive_scale_grid_flatlookup) + (dst_positive_scale_grid_flatlookup))) + (((dst_negative_code_grid_flatlookup) + (dst_negative_scale_grid_flatlookup)) * S ((dst_negative_code_grid_flatlookup) + (dst_negative_scale_grid_flatlookup)) + ((dst_negative_scale_grid_flatlookup) + (dst_negative_scale_grid_flatlookup)))) + ((((dst_negative_code_grid_flatlookup) + (dst_negative_scale_grid_flatlookup)) * S ((dst_negative_code_grid_flatlookup) + (dst_negative_scale_grid_flatlookup)) + ((dst_negative_scale_grid_flatlookup) + (dst_negative_scale_grid_flatlookup))) + (((dst_negative_code_grid_flatlookup) + (dst_negative_scale_grid_flatlookup)) * S ((dst_negative_code_grid_flatlookup) + (dst_negative_scale_grid_flatlookup)) + ((dst_negative_scale_grid_flatlookup) + (dst_negative_scale_grid_flatlookup)))))) /\ (((((exists ff_h_pvs_grid_flatlookuppositive. ff_h_pvs_grid_flatlookuppositive + S (dst_positive_grid_flatlookup) = S ((S (dfg_flat_index_grid_flat)) * dst_positive_scale_grid_flatlookup)) /\ exists ff_q_pvs_grid_flatlookuppositive. dst_positive_code_grid_flatlookup = ff_q_pvs_grid_flatlookuppositive * S ((S (dfg_flat_index_grid_flat)) * dst_positive_scale_grid_flatlookup) + (dst_positive_grid_flatlookup))) /\ (((((exists ff_h_pvs_grid_flatlookupnegative. ff_h_pvs_grid_flatlookupnegative + S (dst_negative_grid_flatlookup) = S ((S (dfg_flat_index_grid_flat)) * dst_negative_scale_grid_flatlookup)) /\ exists ff_q_pvs_grid_flatlookupnegative. dst_negative_code_grid_flatlookup = ff_q_pvs_grid_flatlookupnegative * S ((S (dfg_flat_index_grid_flat)) * dst_negative_scale_grid_flatlookup) + (dst_negative_grid_flatlookup))) /\ (exists ge_balance_positive_grid_flatlookupvalue ge_balance_negative_grid_flatlookupvalue. (((((dfg_flat_value_grid_flat) = 2 * (ge_balance_positive_grid_flatlookupvalue) /\ (ge_balance_negative_grid_flatlookupvalue) = 0) \/ exists ge_signed_half_grid_flatlookupvaluedecode. (((dfg_flat_value_grid_flat) = 2 * ge_signed_half_grid_flatlookupvaluedecode + 1 /\ (ge_balance_positive_grid_flatlookupvalue) = 0) /\ (ge_balance_negative_grid_flatlookupvalue) = S ge_signed_half_grid_flatlookupvaluedecode))) /\ ((dst_positive_grid_flatlookup) + ge_balance_negative_grid_flatlookupvalue = (dst_negative_grid_flatlookup) + ge_balance_positive_grid_flatlookupvalue))))))))) -> (exists dfg_flat_row_grid_flatentry dfg_flat_column_grid_flatentry. (((dfg_flat_index_grid_flat)=((S (n))*(dfg_flat_row_grid_flatentry)+(dfg_flat_column_grid_flatentry))) /\ (((exists pvs_gap_grid_flatentryremainder. pvs_gap_grid_flatentryremainder + S (dfg_flat_column_grid_flatentry) = (S (n))) /\ ((((~((dfg_flat_row_grid_flatentry)=0)) /\ (((~((dfg_flat_column_grid_flatentry)=0)) /\ (exists dfg_middle_grid_flatentrycell dfg_first_grid_flatentrycell dfg_last_grid_flatentrycell dfg_value_grid_flatentrycell. (((n)=((dfg_flat_row_grid_flatentry)*(dfg_flat_column_grid_flatentry))*dfg_middle_grid_flatentrycell) /\ (((exists dst_positive_code_grid_flatentrycellfirst dst_positive_scale_grid_flatentrycellfirst dst_negative_code_grid_flatentrycellfirst dst_negative_scale_grid_flatentrycellfirst dst_positive_grid_flatentrycellfirst dst_negative_grid_flatentrycellfirst. (((F) = (((((dst_positive_code_grid_flatentrycellfirst) + (dst_positive_scale_grid_flatentrycellfirst)) * S ((dst_positive_code_grid_flatentrycellfirst) + (dst_positive_scale_grid_flatentrycellfirst)) + ((dst_positive_scale_grid_flatentrycellfirst) + (dst_positive_scale_grid_flatentrycellfirst))) + (((dst_negative_code_grid_flatentrycellfirst) + (dst_negative_scale_grid_flatentrycellfirst)) * S ((dst_negative_code_grid_flatentrycellfirst) + (dst_negative_scale_grid_flatentrycellfirst)) + ((dst_negative_scale_grid_flatentrycellfirst) + (dst_negative_scale_grid_flatentrycellfirst)))) * S ((((dst_positive_code_grid_flatentrycellfirst) + (dst_positive_scale_grid_flatentrycellfirst)) * S ((dst_positive_code_grid_flatentrycellfirst) + (dst_positive_scale_grid_flatentrycellfirst)) + ((dst_positive_scale_grid_flatentrycellfirst) + (dst_positive_scale_grid_flatentrycellfirst))) + (((dst_negative_code_grid_flatentrycellfirst) + (dst_negative_scale_grid_flatentrycellfirst)) * S ((dst_negative_code_grid_flatentrycellfirst) + (dst_negative_scale_grid_flatentrycellfirst)) + ((dst_negative_scale_grid_flatentrycellfirst) + (dst_negative_scale_grid_flatentrycellfirst)))) + ((((dst_negative_code_grid_flatentrycellfirst) + (dst_negative_scale_grid_flatentrycellfirst)) * S ((dst_negative_code_grid_flatentrycellfirst) + (dst_negative_scale_grid_flatentrycellfirst)) + ((dst_negative_scale_grid_flatentrycellfirst) + (dst_negative_scale_grid_flatentrycellfirst))) + (((dst_negative_code_grid_flatentrycellfirst) + (dst_negative_scale_grid_flatentrycellfirst)) * S ((dst_negative_code_grid_flatentrycellfirst) + (dst_negative_scale_grid_flatentrycellfirst)) + ((dst_negative_scale_grid_flatentrycellfirst) + (dst_negative_scale_grid_flatentrycellfirst)))))) /\ (((((exists ff_h_pvs_grid_flatentrycellfirstpositive. ff_h_pvs_grid_flatentrycellfirstpositive + S (dst_positive_grid_flatentrycellfirst) = S ((S (dfg_flat_row_grid_flatentry)) * dst_positive_scale_grid_flatentrycellfirst)) /\ exists ff_q_pvs_grid_flatentrycellfirstpositive. dst_positive_code_grid_flatentrycellfirst = ff_q_pvs_grid_flatentrycellfirstpositive * S ((S (dfg_flat_row_grid_flatentry)) * dst_positive_scale_grid_flatentrycellfirst) + (dst_positive_grid_flatentrycellfirst))) /\ (((((exists ff_h_pvs_grid_flatentrycellfirstnegative. ff_h_pvs_grid_flatentrycellfirstnegative + S (dst_negative_grid_flatentrycellfirst) = S ((S (dfg_flat_row_grid_flatentry)) * dst_negative_scale_grid_flatentrycellfirst)) /\ exists ff_q_pvs_grid_flatentrycellfirstnegative. dst_negative_code_grid_flatentrycellfirst = ff_q_pvs_grid_flatentrycellfirstnegative * S ((S (dfg_flat_row_grid_flatentry)) * dst_negative_scale_grid_flatentrycellfirst) + (dst_negative_grid_flatentrycellfirst))) /\ (exists ge_balance_positive_grid_flatentrycellfirstvalue ge_balance_negative_grid_flatentrycellfirstvalue. (((((dfg_first_grid_flatentrycell) = 2 * (ge_balance_positive_grid_flatentrycellfirstvalue) /\ (ge_balance_negative_grid_flatentrycellfirstvalue) = 0) \/ exists ge_signed_half_grid_flatentrycellfirstvaluedecode. (((dfg_first_grid_flatentrycell) = 2 * ge_signed_half_grid_flatentrycellfirstvaluedecode + 1 /\ (ge_balance_positive_grid_flatentrycellfirstvalue) = 0) /\ (ge_balance_negative_grid_flatentrycellfirstvalue) = S ge_signed_half_grid_flatentrycellfirstvaluedecode))) /\ ((dst_positive_grid_flatentrycellfirst) + ge_balance_negative_grid_flatentrycellfirstvalue = (dst_negative_grid_flatentrycellfirst) + ge_balance_positive_grid_flatentrycellfirstvalue))))))))) /\ (((exists dst_positive_code_grid_flatentrycelllast dst_positive_scale_grid_flatentrycelllast dst_negative_code_grid_flatentrycelllast dst_negative_scale_grid_flatentrycelllast dst_positive_grid_flatentrycelllast dst_negative_grid_flatentrycelllast. (((H) = (((((dst_positive_code_grid_flatentrycelllast) + (dst_positive_scale_grid_flatentrycelllast)) * S ((dst_positive_code_grid_flatentrycelllast) + (dst_positive_scale_grid_flatentrycelllast)) + ((dst_positive_scale_grid_flatentrycelllast) + (dst_positive_scale_grid_flatentrycelllast))) + (((dst_negative_code_grid_flatentrycelllast) + (dst_negative_scale_grid_flatentrycelllast)) * S ((dst_negative_code_grid_flatentrycelllast) + (dst_negative_scale_grid_flatentrycelllast)) + ((dst_negative_scale_grid_flatentrycelllast) + (dst_negative_scale_grid_flatentrycelllast)))) * S ((((dst_positive_code_grid_flatentrycelllast) + (dst_positive_scale_grid_flatentrycelllast)) * S ((dst_positive_code_grid_flatentrycelllast) + (dst_positive_scale_grid_flatentrycelllast)) + ((dst_positive_scale_grid_flatentrycelllast) + (dst_positive_scale_grid_flatentrycelllast))) + (((dst_negative_code_grid_flatentrycelllast) + (dst_negative_scale_grid_flatentrycelllast)) * S ((dst_negative_code_grid_flatentrycelllast) + (dst_negative_scale_grid_flatentrycelllast)) + ((dst_negative_scale_grid_flatentrycelllast) + (dst_negative_scale_grid_flatentrycelllast)))) + ((((dst_negative_code_grid_flatentrycelllast) + (dst_negative_scale_grid_flatentrycelllast)) * S ((dst_negative_code_grid_flatentrycelllast) + (dst_negative_scale_grid_flatentrycelllast)) + ((dst_negative_scale_grid_flatentrycelllast) + (dst_negative_scale_grid_flatentrycelllast))) + (((dst_negative_code_grid_flatentrycelllast) + (dst_negative_scale_grid_flatentrycelllast)) * S ((dst_negative_code_grid_flatentrycelllast) + (dst_negative_scale_grid_flatentrycelllast)) + ((dst_negative_scale_grid_flatentrycelllast) + (dst_negative_scale_grid_flatentrycelllast)))))) /\ (((((exists ff_h_pvs_grid_flatentrycelllastpositive. ff_h_pvs_grid_flatentrycelllastpositive + S (dst_positive_grid_flatentrycelllast) = S ((S (dfg_flat_column_grid_flatentry)) * dst_positive_scale_grid_flatentrycelllast)) /\ exists ff_q_pvs_grid_flatentrycelllastpositive. dst_positive_code_grid_flatentrycelllast = ff_q_pvs_grid_flatentrycelllastpositive * S ((S (dfg_flat_column_grid_flatentry)) * dst_positive_scale_grid_flatentrycelllast) + (dst_positive_grid_flatentrycelllast))) /\ (((((exists ff_h_pvs_grid_flatentrycelllastnegative. ff_h_pvs_grid_flatentrycelllastnegative + S (dst_negative_grid_flatentrycelllast) = S ((S (dfg_flat_column_grid_flatentry)) * dst_negative_scale_grid_flatentrycelllast)) /\ exists ff_q_pvs_grid_flatentrycelllastnegative. dst_negative_code_grid_flatentrycelllast = ff_q_pvs_grid_flatentrycelllastnegative * S ((S (dfg_flat_column_grid_flatentry)) * dst_negative_scale_grid_flatentrycelllast) + (dst_negative_grid_flatentrycelllast))) /\ (exists ge_balance_positive_grid_flatentrycelllastvalue ge_balance_negative_grid_flatentrycelllastvalue. (((((dfg_last_grid_flatentrycell) = 2 * (ge_balance_positive_grid_flatentrycelllastvalue) /\ (ge_balance_negative_grid_flatentrycelllastvalue) = 0) \/ exists ge_signed_half_grid_flatentrycelllastvaluedecode. (((dfg_last_grid_flatentrycell) = 2 * ge_signed_half_grid_flatentrycelllastvaluedecode + 1 /\ (ge_balance_positive_grid_flatentrycelllastvalue) = 0) /\ (ge_balance_negative_grid_flatentrycelllastvalue) = S ge_signed_half_grid_flatentrycelllastvaluedecode))) /\ ((dst_positive_grid_flatentrycelllast) + ge_balance_negative_grid_flatentrycelllastvalue = (dst_negative_grid_flatentrycelllast) + ge_balance_positive_grid_flatentrycelllastvalue))))))))) /\ (((exists dst_positive_code_grid_flatentrycellmiddle dst_positive_scale_grid_flatentrycellmiddle dst_negative_code_grid_flatentrycellmiddle dst_negative_scale_grid_flatentrycellmiddle dst_positive_grid_flatentrycellmiddle dst_negative_grid_flatentrycellmiddle. (((G) = (((((dst_positive_code_grid_flatentrycellmiddle) + (dst_positive_scale_grid_flatentrycellmiddle)) * S ((dst_positive_code_grid_flatentrycellmiddle) + (dst_positive_scale_grid_flatentrycellmiddle)) + ((dst_positive_scale_grid_flatentrycellmiddle) + (dst_positive_scale_grid_flatentrycellmiddle))) + (((dst_negative_code_grid_flatentrycellmiddle) + (dst_negative_scale_grid_flatentrycellmiddle)) * S ((dst_negative_code_grid_flatentrycellmiddle) + (dst_negative_scale_grid_flatentrycellmiddle)) + ((dst_negative_scale_grid_flatentrycellmiddle) + (dst_negative_scale_grid_flatentrycellmiddle)))) * S ((((dst_positive_code_grid_flatentrycellmiddle) + (dst_positive_scale_grid_flatentrycellmiddle)) * S ((dst_positive_code_grid_flatentrycellmiddle) + (dst_positive_scale_grid_flatentrycellmiddle)) + ((dst_positive_scale_grid_flatentrycellmiddle) + (dst_positive_scale_grid_flatentrycellmiddle))) + (((dst_negative_code_grid_flatentrycellmiddle) + (dst_negative_scale_grid_flatentrycellmiddle)) * S ((dst_negative_code_grid_flatentrycellmiddle) + (dst_negative_scale_grid_flatentrycellmiddle)) + ((dst_negative_scale_grid_flatentrycellmiddle) + (dst_negative_scale_grid_flatentrycellmiddle)))) + ((((dst_negative_code_grid_flatentrycellmiddle) + (dst_negative_scale_grid_flatentrycellmiddle)) * S ((dst_negative_code_grid_flatentrycellmiddle) + (dst_negative_scale_grid_flatentrycellmiddle)) + ((dst_negative_scale_grid_flatentrycellmiddle) + (dst_negative_scale_grid_flatentrycellmiddle))) + (((dst_negative_code_grid_flatentrycellmiddle) + (dst_negative_scale_grid_flatentrycellmiddle)) * S ((dst_negative_code_grid_flatentrycellmiddle) + (dst_negative_scale_grid_flatentrycellmiddle)) + ((dst_negative_scale_grid_flatentrycellmiddle) + (dst_negative_scale_grid_flatentrycellmiddle)))))) /\ (((((exists ff_h_pvs_grid_flatentrycellmiddlepositive. ff_h_pvs_grid_flatentrycellmiddlepositive + S (dst_positive_grid_flatentrycellmiddle) = S ((S (dfg_middle_grid_flatentrycell)) * dst_positive_scale_grid_flatentrycellmiddle)) /\ exists ff_q_pvs_grid_flatentrycellmiddlepositive. dst_positive_code_grid_flatentrycellmiddle = ff_q_pvs_grid_flatentrycellmiddlepositive * S ((S (dfg_middle_grid_flatentrycell)) * dst_positive_scale_grid_flatentrycellmiddle) + (dst_positive_grid_flatentrycellmiddle))) /\ (((((exists ff_h_pvs_grid_flatentrycellmiddlenegative. ff_h_pvs_grid_flatentrycellmiddlenegative + S (dst_negative_grid_flatentrycellmiddle) = S ((S (dfg_middle_grid_flatentrycell)) * dst_negative_scale_grid_flatentrycellmiddle)) /\ exists ff_q_pvs_grid_flatentrycellmiddlenegative. dst_negative_code_grid_flatentrycellmiddle = ff_q_pvs_grid_flatentrycellmiddlenegative * S ((S (dfg_middle_grid_flatentrycell)) * dst_negative_scale_grid_flatentrycellmiddle) + (dst_negative_grid_flatentrycellmiddle))) /\ (exists ge_balance_positive_grid_flatentrycellmiddlevalue ge_balance_negative_grid_flatentrycellmiddlevalue. (((((dfg_value_grid_flatentrycell) = 2 * (ge_balance_positive_grid_flatentrycellmiddlevalue) /\ (ge_balance_negative_grid_flatentrycellmiddlevalue) = 0) \/ exists ge_signed_half_grid_flatentrycellmiddlevaluedecode. (((dfg_value_grid_flatentrycell) = 2 * ge_signed_half_grid_flatentrycellmiddlevaluedecode + 1 /\ (ge_balance_positive_grid_flatentrycellmiddlevalue) = 0) /\ (ge_balance_negative_grid_flatentrycellmiddlevalue) = S ge_signed_half_grid_flatentrycellmiddlevaluedecode))) /\ ((dst_positive_grid_flatentrycellmiddle) + ge_balance_negative_grid_flatentrycellmiddlevalue = (dst_negative_grid_flatentrycellmiddle) + ge_balance_positive_grid_flatentrycellmiddlevalue))))))))) /\ (exists dfg_inner_grid_flatentrycellproduct. ((exists sto_ap_grid_flatentrycellproductinner sto_an_grid_flatentrycellproductinner sto_bp_grid_flatentrycellproductinner sto_bn_grid_flatentrycellproductinner sto_cp_grid_flatentrycellproductinner sto_cn_grid_flatentrycellproductinner. (((((dfg_last_grid_flatentrycell) = 2 * (sto_ap_grid_flatentrycellproductinner) /\ (sto_an_grid_flatentrycellproductinner) = 0) \/ exists ge_signed_half_grid_flatentrycellproductinnerleft. (((dfg_last_grid_flatentrycell) = 2 * ge_signed_half_grid_flatentrycellproductinnerleft + 1 /\ (sto_ap_grid_flatentrycellproductinner) = 0) /\ (sto_an_grid_flatentrycellproductinner) = S ge_signed_half_grid_flatentrycellproductinnerleft))) /\ ((((((dfg_value_grid_flatentrycell) = 2 * (sto_bp_grid_flatentrycellproductinner) /\ (sto_bn_grid_flatentrycellproductinner) = 0) \/ exists ge_signed_half_grid_flatentrycellproductinnerright. (((dfg_value_grid_flatentrycell) = 2 * ge_signed_half_grid_flatentrycellproductinnerright + 1 /\ (sto_bp_grid_flatentrycellproductinner) = 0) /\ (sto_bn_grid_flatentrycellproductinner) = S ge_signed_half_grid_flatentrycellproductinnerright))) /\ ((((((dfg_inner_grid_flatentrycellproduct) = 2 * (sto_cp_grid_flatentrycellproductinner) /\ (sto_cn_grid_flatentrycellproductinner) = 0) \/ exists ge_signed_half_grid_flatentrycellproductinneroutput. (((dfg_inner_grid_flatentrycellproduct) = 2 * ge_signed_half_grid_flatentrycellproductinneroutput + 1 /\ (sto_cp_grid_flatentrycellproductinner) = 0) /\ (sto_cn_grid_flatentrycellproductinner) = S ge_signed_half_grid_flatentrycellproductinneroutput))) /\ ((sto_ap_grid_flatentrycellproductinner * sto_bp_grid_flatentrycellproductinner + sto_an_grid_flatentrycellproductinner * sto_bn_grid_flatentrycellproductinner) + sto_cn_grid_flatentrycellproductinner = (sto_ap_grid_flatentrycellproductinner * sto_bn_grid_flatentrycellproductinner + sto_an_grid_flatentrycellproductinner * sto_bp_grid_flatentrycellproductinner) + sto_cp_grid_flatentrycellproductinner))))))) /\ (exists sto_ap_grid_flatentrycellproductouter sto_an_grid_flatentrycellproductouter sto_bp_grid_flatentrycellproductouter sto_bn_grid_flatentrycellproductouter sto_cp_grid_flatentrycellproductouter sto_cn_grid_flatentrycellproductouter. (((((dfg_first_grid_flatentrycell) = 2 * (sto_ap_grid_flatentrycellproductouter) /\ (sto_an_grid_flatentrycellproductouter) = 0) \/ exists ge_signed_half_grid_flatentrycellproductouterleft. (((dfg_first_grid_flatentrycell) = 2 * ge_signed_half_grid_flatentrycellproductouterleft + 1 /\ (sto_ap_grid_flatentrycellproductouter) = 0) /\ (sto_an_grid_flatentrycellproductouter) = S ge_signed_half_grid_flatentrycellproductouterleft))) /\ ((((((dfg_inner_grid_flatentrycellproduct) = 2 * (sto_bp_grid_flatentrycellproductouter) /\ (sto_bn_grid_flatentrycellproductouter) = 0) \/ exists ge_signed_half_grid_flatentrycellproductouterright. (((dfg_inner_grid_flatentrycellproduct) = 2 * ge_signed_half_grid_flatentrycellproductouterright + 1 /\ (sto_bp_grid_flatentrycellproductouter) = 0) /\ (sto_bn_grid_flatentrycellproductouter) = S ge_signed_half_grid_flatentrycellproductouterright))) /\ ((((((dfg_flat_value_grid_flat) = 2 * (sto_cp_grid_flatentrycellproductouter) /\ (sto_cn_grid_flatentrycellproductouter) = 0) \/ exists ge_signed_half_grid_flatentrycellproductouteroutput. (((dfg_flat_value_grid_flat) = 2 * ge_signed_half_grid_flatentrycellproductouteroutput + 1 /\ (sto_cp_grid_flatentrycellproductouter) = 0) /\ (sto_cn_grid_flatentrycellproductouter) = S ge_signed_half_grid_flatentrycellproductouteroutput))) /\ ((sto_ap_grid_flatentrycellproductouter * sto_bp_grid_flatentrycellproductouter + sto_an_grid_flatentrycellproductouter * sto_bn_grid_flatentrycellproductouter) + sto_cn_grid_flatentrycellproductouter = (sto_ap_grid_flatentrycellproductouter * sto_bn_grid_flatentrycellproductouter + sto_an_grid_flatentrycellproductouter * sto_bp_grid_flatentrycellproductouter) + sto_cp_grid_flatentrycellproductouter))))))))))))))))))))) \/ ((((dfg_flat_row_grid_flatentry)=0 \/ ((dfg_flat_column_grid_flatentry)=0 \/ ~(exists pvs_factor_grid_flatentrycellomittednondivisor. (n) = ((dfg_flat_row_grid_flatentry)*(dfg_flat_column_grid_flatentry)) * pvs_factor_grid_flatentrycellomittednondivisor))) /\ ((dfg_flat_value_grid_flat)=0)))))))))))
  9. 0009specialize dirichlet_grid_flat_prefix_exists (F)
  10. 0010specialize dirichlet_grid_flat_prefix_exists (G)
  11. 0011specialize dirichlet_grid_flat_prefix_exists (H)
  12. 0012specialize dirichlet_grid_flat_prefix_exists (n)
  13. 0013specialize dirichlet_grid_flat_prefix_exists ((S n)*(S n))
  14. 0014apply dirichlet_grid_flat_prefix_exists
  15. 0015exact hF
  16. 0016exact hG
  17. 0017exact hH
  18. 0018cases hp
  19. 0019exists x
  20. 0020specialize dirichlet_grid_from_flat_prefix (F)
  21. 0021specialize dirichlet_grid_from_flat_prefix (G)
  22. 0022specialize dirichlet_grid_from_flat_prefix (H)
  23. 0023specialize dirichlet_grid_from_flat_prefix (n)
  24. 0024specialize dirichlet_grid_from_flat_prefix (x)
  25. 0025apply dirichlet_grid_from_flat_prefix
  26. 0026exact hp_witness