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 l. (exists dst_positive_code_prefix_F dst_positive_scale_prefix_F dst_negative_code_prefix_F dst_negative_scale_prefix_F. (((F) = (((((dst_positive_code_prefix_F) + (dst_positive_scale_prefix_F)) * S ((dst_positive_code_prefix_F) + (dst_positive_scale_prefix_F)) + ((dst_positive_scale_prefix_F) + (dst_positive_scale_prefix_F))) + (((dst_negative_code_prefix_F) + (dst_negative_scale_prefix_F)) * S ((dst_negative_code_prefix_F) + (dst_negative_scale_prefix_F)) + ((dst_negative_scale_prefix_F) + (dst_negative_scale_prefix_F)))) * S ((((dst_positive_code_prefix_F) + (dst_positive_scale_prefix_F)) * S ((dst_positive_code_prefix_F) + (dst_positive_scale_prefix_F)) + ((dst_positive_scale_prefix_F) + (dst_positive_scale_prefix_F))) + (((dst_negative_code_prefix_F) + (dst_negative_scale_prefix_F)) * S ((dst_negative_code_prefix_F) + (dst_negative_scale_prefix_F)) + ((dst_negative_scale_prefix_F) + (dst_negative_scale_prefix_F)))) + ((((dst_negative_code_prefix_F) + (dst_negative_scale_prefix_F)) * S ((dst_negative_code_prefix_F) + (dst_negative_scale_prefix_F)) + ((dst_negative_scale_prefix_F) + (dst_negative_scale_prefix_F))) + (((dst_negative_code_prefix_F) + (dst_negative_scale_prefix_F)) * S ((dst_negative_code_prefix_F) + (dst_negative_scale_prefix_F)) + ((dst_negative_scale_prefix_F) + (dst_negative_scale_prefix_F)))))) /\ (forall dst_index_prefix_F. (exists pvs_le_gap_prefix_Fdomain. pvs_le_gap_prefix_Fdomain + (dst_index_prefix_F) = (0)) -> exists dst_positive_prefix_F dst_negative_prefix_F dst_value_prefix_F. ((((exists ff_h_pvs_prefix_Fentrypositive. ff_h_pvs_prefix_Fentrypositive + S (dst_positive_prefix_F) = S ((S (dst_index_prefix_F)) * dst_positive_scale_prefix_F)) /\ exists ff_q_pvs_prefix_Fentrypositive. dst_positive_code_prefix_F = ff_q_pvs_prefix_Fentrypositive * S ((S (dst_index_prefix_F)) * dst_positive_scale_prefix_F) + (dst_positive_prefix_F))) /\ (((((exists ff_h_pvs_prefix_Fentrynegative. ff_h_pvs_prefix_Fentrynegative + S (dst_negative_prefix_F) = S ((S (dst_index_prefix_F)) * dst_negative_scale_prefix_F)) /\ exists ff_q_pvs_prefix_Fentrynegative. dst_negative_code_prefix_F = ff_q_pvs_prefix_Fentrynegative * S ((S (dst_index_prefix_F)) * dst_negative_scale_prefix_F) + (dst_negative_prefix_F))) /\ (exists ge_balance_positive_prefix_Fentryvalue ge_balance_negative_prefix_Fentryvalue. (((((dst_value_prefix_F) = 2 * (ge_balance_positive_prefix_Fentryvalue) /\ (ge_balance_negative_prefix_Fentryvalue) = 0) \/ exists ge_signed_half_prefix_Fentryvaluedecode. (((dst_value_prefix_F) = 2 * ge_signed_half_prefix_Fentryvaluedecode + 1 /\ (ge_balance_positive_prefix_Fentryvalue) = 0) /\ (ge_balance_negative_prefix_Fentryvalue) = S ge_signed_half_prefix_Fentryvaluedecode))) /\ ((dst_positive_prefix_F) + ge_balance_negative_prefix_Fentryvalue = (dst_negative_prefix_F) + ge_balance_positive_prefix_Fentryvalue))))))))) -> (exists dst_positive_code_prefix_G dst_positive_scale_prefix_G dst_negative_code_prefix_G dst_negative_scale_prefix_G. (((G) = (((((dst_positive_code_prefix_G) + (dst_positive_scale_prefix_G)) * S ((dst_positive_code_prefix_G) + (dst_positive_scale_prefix_G)) + ((dst_positive_scale_prefix_G) + (dst_positive_scale_prefix_G))) + (((dst_negative_code_prefix_G) + (dst_negative_scale_prefix_G)) * S ((dst_negative_code_prefix_G) + (dst_negative_scale_prefix_G)) + ((dst_negative_scale_prefix_G) + (dst_negative_scale_prefix_G)))) * S ((((dst_positive_code_prefix_G) + (dst_positive_scale_prefix_G)) * S ((dst_positive_code_prefix_G) + (dst_positive_scale_prefix_G)) + ((dst_positive_scale_prefix_G) + (dst_positive_scale_prefix_G))) + (((dst_negative_code_prefix_G) + (dst_negative_scale_prefix_G)) * S ((dst_negative_code_prefix_G) + (dst_negative_scale_prefix_G)) + ((dst_negative_scale_prefix_G) + (dst_negative_scale_prefix_G)))) + ((((dst_negative_code_prefix_G) + (dst_negative_scale_prefix_G)) * S ((dst_negative_code_prefix_G) + (dst_negative_scale_prefix_G)) + ((dst_negative_scale_prefix_G) + (dst_negative_scale_prefix_G))) + (((dst_negative_code_prefix_G) + (dst_negative_scale_prefix_G)) * S ((dst_negative_code_prefix_G) + (dst_negative_scale_prefix_G)) + ((dst_negative_scale_prefix_G) + (dst_negative_scale_prefix_G)))))) /\ (forall dst_index_prefix_G. (exists pvs_le_gap_prefix_Gdomain. pvs_le_gap_prefix_Gdomain + (dst_index_prefix_G) = (0)) -> exists dst_positive_prefix_G dst_negative_prefix_G dst_value_prefix_G. ((((exists ff_h_pvs_prefix_Gentrypositive. ff_h_pvs_prefix_Gentrypositive + S (dst_positive_prefix_G) = S ((S (dst_index_prefix_G)) * dst_positive_scale_prefix_G)) /\ exists ff_q_pvs_prefix_Gentrypositive. dst_positive_code_prefix_G = ff_q_pvs_prefix_Gentrypositive * S ((S (dst_index_prefix_G)) * dst_positive_scale_prefix_G) + (dst_positive_prefix_G))) /\ (((((exists ff_h_pvs_prefix_Gentrynegative. ff_h_pvs_prefix_Gentrynegative + S (dst_negative_prefix_G) = S ((S (dst_index_prefix_G)) * dst_negative_scale_prefix_G)) /\ exists ff_q_pvs_prefix_Gentrynegative. dst_negative_code_prefix_G = ff_q_pvs_prefix_Gentrynegative * S ((S (dst_index_prefix_G)) * dst_negative_scale_prefix_G) + (dst_negative_prefix_G))) /\ (exists ge_balance_positive_prefix_Gentryvalue ge_balance_negative_prefix_Gentryvalue. (((((dst_value_prefix_G) = 2 * (ge_balance_positive_prefix_Gentryvalue) /\ (ge_balance_negative_prefix_Gentryvalue) = 0) \/ exists ge_signed_half_prefix_Gentryvaluedecode. (((dst_value_prefix_G) = 2 * ge_signed_half_prefix_Gentryvaluedecode + 1 /\ (ge_balance_positive_prefix_Gentryvalue) = 0) /\ (ge_balance_negative_prefix_Gentryvalue) = S ge_signed_half_prefix_Gentryvaluedecode))) /\ ((dst_positive_prefix_G) + ge_balance_negative_prefix_Gentryvalue = (dst_negative_prefix_G) + ge_balance_positive_prefix_Gentryvalue))))))))) -> (exists dst_positive_code_prefix_H dst_positive_scale_prefix_H dst_negative_code_prefix_H dst_negative_scale_prefix_H. (((H) = (((((dst_positive_code_prefix_H) + (dst_positive_scale_prefix_H)) * S ((dst_positive_code_prefix_H) + (dst_positive_scale_prefix_H)) + ((dst_positive_scale_prefix_H) + (dst_positive_scale_prefix_H))) + (((dst_negative_code_prefix_H) + (dst_negative_scale_prefix_H)) * S ((dst_negative_code_prefix_H) + (dst_negative_scale_prefix_H)) + ((dst_negative_scale_prefix_H) + (dst_negative_scale_prefix_H)))) * S ((((dst_positive_code_prefix_H) + (dst_positive_scale_prefix_H)) * S ((dst_positive_code_prefix_H) + (dst_positive_scale_prefix_H)) + ((dst_positive_scale_prefix_H) + (dst_positive_scale_prefix_H))) + (((dst_negative_code_prefix_H) + (dst_negative_scale_prefix_H)) * S ((dst_negative_code_prefix_H) + (dst_negative_scale_prefix_H)) + ((dst_negative_scale_prefix_H) + (dst_negative_scale_prefix_H)))) + ((((dst_negative_code_prefix_H) + (dst_negative_scale_prefix_H)) * S ((dst_negative_code_prefix_H) + (dst_negative_scale_prefix_H)) + ((dst_negative_scale_prefix_H) + (dst_negative_scale_prefix_H))) + (((dst_negative_code_prefix_H) + (dst_negative_scale_prefix_H)) * S ((dst_negative_code_prefix_H) + (dst_negative_scale_prefix_H)) + ((dst_negative_scale_prefix_H) + (dst_negative_scale_prefix_H)))))) /\ (forall dst_index_prefix_H. (exists pvs_le_gap_prefix_Hdomain. pvs_le_gap_prefix_Hdomain + (dst_index_prefix_H) = (0)) -> exists dst_positive_prefix_H dst_negative_prefix_H dst_value_prefix_H. ((((exists ff_h_pvs_prefix_Hentrypositive. ff_h_pvs_prefix_Hentrypositive + S (dst_positive_prefix_H) = S ((S (dst_index_prefix_H)) * dst_positive_scale_prefix_H)) /\ exists ff_q_pvs_prefix_Hentrypositive. dst_positive_code_prefix_H = ff_q_pvs_prefix_Hentrypositive * S ((S (dst_index_prefix_H)) * dst_positive_scale_prefix_H) + (dst_positive_prefix_H))) /\ (((((exists ff_h_pvs_prefix_Hentrynegative. ff_h_pvs_prefix_Hentrynegative + S (dst_negative_prefix_H) = S ((S (dst_index_prefix_H)) * dst_negative_scale_prefix_H)) /\ exists ff_q_pvs_prefix_Hentrynegative. dst_negative_code_prefix_H = ff_q_pvs_prefix_Hentrynegative * S ((S (dst_index_prefix_H)) * dst_negative_scale_prefix_H) + (dst_negative_prefix_H))) /\ (exists ge_balance_positive_prefix_Hentryvalue ge_balance_negative_prefix_Hentryvalue. (((((dst_value_prefix_H) = 2 * (ge_balance_positive_prefix_Hentryvalue) /\ (ge_balance_negative_prefix_Hentryvalue) = 0) \/ exists ge_signed_half_prefix_Hentryvaluedecode. (((dst_value_prefix_H) = 2 * ge_signed_half_prefix_Hentryvaluedecode + 1 /\ (ge_balance_positive_prefix_Hentryvalue) = 0) /\ (ge_balance_negative_prefix_Hentryvalue) = S ge_signed_half_prefix_Hentryvaluedecode))) /\ ((dst_positive_prefix_H) + ge_balance_negative_prefix_Hentryvalue = (dst_negative_prefix_H) + ge_balance_positive_prefix_Hentryvalue))))))))) -> exists T. (((exists dst_positive_code_prefix_resulttable dst_positive_scale_prefix_resulttable dst_negative_code_prefix_resulttable dst_negative_scale_prefix_resulttable. (((T) = (((((dst_positive_code_prefix_resulttable) + (dst_positive_scale_prefix_resulttable)) * S ((dst_positive_code_prefix_resulttable) + (dst_positive_scale_prefix_resulttable)) + ((dst_positive_scale_prefix_resulttable) + (dst_positive_scale_prefix_resulttable))) + (((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) * S ((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) + ((dst_negative_scale_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)))) * S ((((dst_positive_code_prefix_resulttable) + (dst_positive_scale_prefix_resulttable)) * S ((dst_positive_code_prefix_resulttable) + (dst_positive_scale_prefix_resulttable)) + ((dst_positive_scale_prefix_resulttable) + (dst_positive_scale_prefix_resulttable))) + (((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) * S ((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) + ((dst_negative_scale_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)))) + ((((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) * S ((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) + ((dst_negative_scale_prefix_resulttable) + (dst_negative_scale_prefix_resulttable))) + (((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) * S ((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) + ((dst_negative_scale_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)))))) /\ (forall dst_index_prefix_resulttable. (exists pvs_le_gap_prefix_resulttabledomain. pvs_le_gap_prefix_resulttabledomain + (dst_index_prefix_resulttable) = (l)) -> exists dst_positive_prefix_resulttable dst_negative_prefix_resulttable dst_value_prefix_resulttable. ((((exists ff_h_pvs_prefix_resulttableentrypositive. ff_h_pvs_prefix_resulttableentrypositive + S (dst_positive_prefix_resulttable) = S ((S (dst_index_prefix_resulttable)) * dst_positive_scale_prefix_resulttable)) /\ exists ff_q_pvs_prefix_resulttableentrypositive. dst_positive_code_prefix_resulttable = ff_q_pvs_prefix_resulttableentrypositive * S ((S (dst_index_prefix_resulttable)) * dst_positive_scale_prefix_resulttable) + (dst_positive_prefix_resulttable))) /\ (((((exists ff_h_pvs_prefix_resulttableentrynegative. ff_h_pvs_prefix_resulttableentrynegative + S (dst_negative_prefix_resulttable) = S ((S (dst_index_prefix_resulttable)) * dst_negative_scale_prefix_resulttable)) /\ exists ff_q_pvs_prefix_resulttableentrynegative. dst_negative_code_prefix_resulttable = ff_q_pvs_prefix_resulttableentrynegative * S ((S (dst_index_prefix_resulttable)) * dst_negative_scale_prefix_resulttable) + (dst_negative_prefix_resulttable))) /\ (exists ge_balance_positive_prefix_resulttableentryvalue ge_balance_negative_prefix_resulttableentryvalue. (((((dst_value_prefix_resulttable) = 2 * (ge_balance_positive_prefix_resulttableentryvalue) /\ (ge_balance_negative_prefix_resulttableentryvalue) = 0) \/ exists ge_signed_half_prefix_resulttableentryvaluedecode. (((dst_value_prefix_resulttable) = 2 * ge_signed_half_prefix_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_prefix_resulttableentryvalue) = 0) /\ (ge_balance_negative_prefix_resulttableentryvalue) = S ge_signed_half_prefix_resulttableentryvaluedecode))) /\ ((dst_positive_prefix_resulttable) + ge_balance_negative_prefix_resulttableentryvalue = (dst_negative_prefix_resulttable) + ge_balance_positive_prefix_resulttableentryvalue))))))))) /\ (forall dfg_flat_index_prefix_result dfg_flat_value_prefix_result. (exists pvs_le_gap_prefix_resultbound. pvs_le_gap_prefix_resultbound + (dfg_flat_index_prefix_result) = (l)) -> (exists dst_positive_code_prefix_resultlookup dst_positive_scale_prefix_resultlookup dst_negative_code_prefix_resultlookup dst_negative_scale_prefix_resultlookup dst_positive_prefix_resultlookup dst_negative_prefix_resultlookup. (((T) = (((((dst_positive_code_prefix_resultlookup) + (dst_positive_scale_prefix_resultlookup)) * S ((dst_positive_code_prefix_resultlookup) + (dst_positive_scale_prefix_resultlookup)) + ((dst_positive_scale_prefix_resultlookup) + (dst_positive_scale_prefix_resultlookup))) + (((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) * S ((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) + ((dst_negative_scale_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)))) * S ((((dst_positive_code_prefix_resultlookup) + (dst_positive_scale_prefix_resultlookup)) * S ((dst_positive_code_prefix_resultlookup) + (dst_positive_scale_prefix_resultlookup)) + ((dst_positive_scale_prefix_resultlookup) + (dst_positive_scale_prefix_resultlookup))) + (((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) * S ((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) + ((dst_negative_scale_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)))) + ((((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) * S ((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) + ((dst_negative_scale_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup))) + (((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) * S ((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) + ((dst_negative_scale_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)))))) /\ (((((exists ff_h_pvs_prefix_resultlookuppositive. ff_h_pvs_prefix_resultlookuppositive + S (dst_positive_prefix_resultlookup) = S ((S (dfg_flat_index_prefix_result)) * dst_positive_scale_prefix_resultlookup)) /\ exists ff_q_pvs_prefix_resultlookuppositive. dst_positive_code_prefix_resultlookup = ff_q_pvs_prefix_resultlookuppositive * S ((S (dfg_flat_index_prefix_result)) * dst_positive_scale_prefix_resultlookup) + (dst_positive_prefix_resultlookup))) /\ (((((exists ff_h_pvs_prefix_resultlookupnegative. ff_h_pvs_prefix_resultlookupnegative + S (dst_negative_prefix_resultlookup) = S ((S (dfg_flat_index_prefix_result)) * dst_negative_scale_prefix_resultlookup)) /\ exists ff_q_pvs_prefix_resultlookupnegative. dst_negative_code_prefix_resultlookup = ff_q_pvs_prefix_resultlookupnegative * S ((S (dfg_flat_index_prefix_result)) * dst_negative_scale_prefix_resultlookup) + (dst_negative_prefix_resultlookup))) /\ (exists ge_balance_positive_prefix_resultlookupvalue ge_balance_negative_prefix_resultlookupvalue. (((((dfg_flat_value_prefix_result) = 2 * (ge_balance_positive_prefix_resultlookupvalue) /\ (ge_balance_negative_prefix_resultlookupvalue) = 0) \/ exists ge_signed_half_prefix_resultlookupvaluedecode. (((dfg_flat_value_prefix_result) = 2 * ge_signed_half_prefix_resultlookupvaluedecode + 1 /\ (ge_balance_positive_prefix_resultlookupvalue) = 0) /\ (ge_balance_negative_prefix_resultlookupvalue) = S ge_signed_half_prefix_resultlookupvaluedecode))) /\ ((dst_positive_prefix_resultlookup) + ge_balance_negative_prefix_resultlookupvalue = (dst_negative_prefix_resultlookup) + ge_balance_positive_prefix_resultlookupvalue))))))))) -> (exists dfg_flat_row_prefix_resultentry dfg_flat_column_prefix_resultentry. (((dfg_flat_index_prefix_result)=((S (n))*(dfg_flat_row_prefix_resultentry)+(dfg_flat_column_prefix_resultentry))) /\ (((exists pvs_gap_prefix_resultentryremainder. pvs_gap_prefix_resultentryremainder + S (dfg_flat_column_prefix_resultentry) = (S (n))) /\ ((((~((dfg_flat_row_prefix_resultentry)=0)) /\ (((~((dfg_flat_column_prefix_resultentry)=0)) /\ (exists dfg_middle_prefix_resultentrycell dfg_first_prefix_resultentrycell dfg_last_prefix_resultentrycell dfg_value_prefix_resultentrycell. (((n)=((dfg_flat_row_prefix_resultentry)*(dfg_flat_column_prefix_resultentry))*dfg_middle_prefix_resultentrycell) /\ (((exists dst_positive_code_prefix_resultentrycellfirst dst_positive_scale_prefix_resultentrycellfirst dst_negative_code_prefix_resultentrycellfirst dst_negative_scale_prefix_resultentrycellfirst dst_positive_prefix_resultentrycellfirst dst_negative_prefix_resultentrycellfirst. (((F) = (((((dst_positive_code_prefix_resultentrycellfirst) + (dst_positive_scale_prefix_resultentrycellfirst)) * S ((dst_positive_code_prefix_resultentrycellfirst) + (dst_positive_scale_prefix_resultentrycellfirst)) + ((dst_positive_scale_prefix_resultentrycellfirst) + (dst_positive_scale_prefix_resultentrycellfirst))) + (((dst_negative_code_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)) * S ((dst_negative_code_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)) + ((dst_negative_scale_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)))) * S ((((dst_positive_code_prefix_resultentrycellfirst) + (dst_positive_scale_prefix_resultentrycellfirst)) * S ((dst_positive_code_prefix_resultentrycellfirst) + (dst_positive_scale_prefix_resultentrycellfirst)) + ((dst_positive_scale_prefix_resultentrycellfirst) + (dst_positive_scale_prefix_resultentrycellfirst))) + (((dst_negative_code_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)) * S ((dst_negative_code_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)) + ((dst_negative_scale_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)))) + ((((dst_negative_code_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)) * S ((dst_negative_code_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)) + ((dst_negative_scale_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst))) + (((dst_negative_code_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)) * S ((dst_negative_code_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)) + ((dst_negative_scale_prefix_resultentrycellfirst) + (dst_negative_scale_prefix_resultentrycellfirst)))))) /\ (((((exists ff_h_pvs_prefix_resultentrycellfirstpositive. ff_h_pvs_prefix_resultentrycellfirstpositive + S (dst_positive_prefix_resultentrycellfirst) = S ((S (dfg_flat_row_prefix_resultentry)) * dst_positive_scale_prefix_resultentrycellfirst)) /\ exists ff_q_pvs_prefix_resultentrycellfirstpositive. dst_positive_code_prefix_resultentrycellfirst = ff_q_pvs_prefix_resultentrycellfirstpositive * S ((S (dfg_flat_row_prefix_resultentry)) * dst_positive_scale_prefix_resultentrycellfirst) + (dst_positive_prefix_resultentrycellfirst))) /\ (((((exists ff_h_pvs_prefix_resultentrycellfirstnegative. ff_h_pvs_prefix_resultentrycellfirstnegative + S (dst_negative_prefix_resultentrycellfirst) = S ((S (dfg_flat_row_prefix_resultentry)) * dst_negative_scale_prefix_resultentrycellfirst)) /\ exists ff_q_pvs_prefix_resultentrycellfirstnegative. dst_negative_code_prefix_resultentrycellfirst = ff_q_pvs_prefix_resultentrycellfirstnegative * S ((S (dfg_flat_row_prefix_resultentry)) * dst_negative_scale_prefix_resultentrycellfirst) + (dst_negative_prefix_resultentrycellfirst))) /\ (exists ge_balance_positive_prefix_resultentrycellfirstvalue ge_balance_negative_prefix_resultentrycellfirstvalue. (((((dfg_first_prefix_resultentrycell) = 2 * (ge_balance_positive_prefix_resultentrycellfirstvalue) /\ (ge_balance_negative_prefix_resultentrycellfirstvalue) = 0) \/ exists ge_signed_half_prefix_resultentrycellfirstvaluedecode. (((dfg_first_prefix_resultentrycell) = 2 * ge_signed_half_prefix_resultentrycellfirstvaluedecode + 1 /\ (ge_balance_positive_prefix_resultentrycellfirstvalue) = 0) /\ (ge_balance_negative_prefix_resultentrycellfirstvalue) = S ge_signed_half_prefix_resultentrycellfirstvaluedecode))) /\ ((dst_positive_prefix_resultentrycellfirst) + ge_balance_negative_prefix_resultentrycellfirstvalue = (dst_negative_prefix_resultentrycellfirst) + ge_balance_positive_prefix_resultentrycellfirstvalue))))))))) /\ (((exists dst_positive_code_prefix_resultentrycelllast dst_positive_scale_prefix_resultentrycelllast dst_negative_code_prefix_resultentrycelllast dst_negative_scale_prefix_resultentrycelllast dst_positive_prefix_resultentrycelllast dst_negative_prefix_resultentrycelllast. (((H) = (((((dst_positive_code_prefix_resultentrycelllast) + (dst_positive_scale_prefix_resultentrycelllast)) * S ((dst_positive_code_prefix_resultentrycelllast) + (dst_positive_scale_prefix_resultentrycelllast)) + ((dst_positive_scale_prefix_resultentrycelllast) + (dst_positive_scale_prefix_resultentrycelllast))) + (((dst_negative_code_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)) * S ((dst_negative_code_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)) + ((dst_negative_scale_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)))) * S ((((dst_positive_code_prefix_resultentrycelllast) + (dst_positive_scale_prefix_resultentrycelllast)) * S ((dst_positive_code_prefix_resultentrycelllast) + (dst_positive_scale_prefix_resultentrycelllast)) + ((dst_positive_scale_prefix_resultentrycelllast) + (dst_positive_scale_prefix_resultentrycelllast))) + (((dst_negative_code_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)) * S ((dst_negative_code_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)) + ((dst_negative_scale_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)))) + ((((dst_negative_code_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)) * S ((dst_negative_code_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)) + ((dst_negative_scale_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast))) + (((dst_negative_code_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)) * S ((dst_negative_code_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)) + ((dst_negative_scale_prefix_resultentrycelllast) + (dst_negative_scale_prefix_resultentrycelllast)))))) /\ (((((exists ff_h_pvs_prefix_resultentrycelllastpositive. ff_h_pvs_prefix_resultentrycelllastpositive + S (dst_positive_prefix_resultentrycelllast) = S ((S (dfg_flat_column_prefix_resultentry)) * dst_positive_scale_prefix_resultentrycelllast)) /\ exists ff_q_pvs_prefix_resultentrycelllastpositive. dst_positive_code_prefix_resultentrycelllast = ff_q_pvs_prefix_resultentrycelllastpositive * S ((S (dfg_flat_column_prefix_resultentry)) * dst_positive_scale_prefix_resultentrycelllast) + (dst_positive_prefix_resultentrycelllast))) /\ (((((exists ff_h_pvs_prefix_resultentrycelllastnegative. ff_h_pvs_prefix_resultentrycelllastnegative + S (dst_negative_prefix_resultentrycelllast) = S ((S (dfg_flat_column_prefix_resultentry)) * dst_negative_scale_prefix_resultentrycelllast)) /\ exists ff_q_pvs_prefix_resultentrycelllastnegative. dst_negative_code_prefix_resultentrycelllast = ff_q_pvs_prefix_resultentrycelllastnegative * S ((S (dfg_flat_column_prefix_resultentry)) * dst_negative_scale_prefix_resultentrycelllast) + (dst_negative_prefix_resultentrycelllast))) /\ (exists ge_balance_positive_prefix_resultentrycelllastvalue ge_balance_negative_prefix_resultentrycelllastvalue. (((((dfg_last_prefix_resultentrycell) = 2 * (ge_balance_positive_prefix_resultentrycelllastvalue) /\ (ge_balance_negative_prefix_resultentrycelllastvalue) = 0) \/ exists ge_signed_half_prefix_resultentrycelllastvaluedecode. (((dfg_last_prefix_resultentrycell) = 2 * ge_signed_half_prefix_resultentrycelllastvaluedecode + 1 /\ (ge_balance_positive_prefix_resultentrycelllastvalue) = 0) /\ (ge_balance_negative_prefix_resultentrycelllastvalue) = S ge_signed_half_prefix_resultentrycelllastvaluedecode))) /\ ((dst_positive_prefix_resultentrycelllast) + ge_balance_negative_prefix_resultentrycelllastvalue = (dst_negative_prefix_resultentrycelllast) + ge_balance_positive_prefix_resultentrycelllastvalue))))))))) /\ (((exists dst_positive_code_prefix_resultentrycellmiddle dst_positive_scale_prefix_resultentrycellmiddle dst_negative_code_prefix_resultentrycellmiddle dst_negative_scale_prefix_resultentrycellmiddle dst_positive_prefix_resultentrycellmiddle dst_negative_prefix_resultentrycellmiddle. (((G) = (((((dst_positive_code_prefix_resultentrycellmiddle) + (dst_positive_scale_prefix_resultentrycellmiddle)) * S ((dst_positive_code_prefix_resultentrycellmiddle) + (dst_positive_scale_prefix_resultentrycellmiddle)) + ((dst_positive_scale_prefix_resultentrycellmiddle) + (dst_positive_scale_prefix_resultentrycellmiddle))) + (((dst_negative_code_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)) * S ((dst_negative_code_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)) + ((dst_negative_scale_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)))) * S ((((dst_positive_code_prefix_resultentrycellmiddle) + (dst_positive_scale_prefix_resultentrycellmiddle)) * S ((dst_positive_code_prefix_resultentrycellmiddle) + (dst_positive_scale_prefix_resultentrycellmiddle)) + ((dst_positive_scale_prefix_resultentrycellmiddle) + (dst_positive_scale_prefix_resultentrycellmiddle))) + (((dst_negative_code_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)) * S ((dst_negative_code_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)) + ((dst_negative_scale_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)))) + ((((dst_negative_code_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)) * S ((dst_negative_code_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)) + ((dst_negative_scale_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle))) + (((dst_negative_code_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)) * S ((dst_negative_code_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)) + ((dst_negative_scale_prefix_resultentrycellmiddle) + (dst_negative_scale_prefix_resultentrycellmiddle)))))) /\ (((((exists ff_h_pvs_prefix_resultentrycellmiddlepositive. ff_h_pvs_prefix_resultentrycellmiddlepositive + S (dst_positive_prefix_resultentrycellmiddle) = S ((S (dfg_middle_prefix_resultentrycell)) * dst_positive_scale_prefix_resultentrycellmiddle)) /\ exists ff_q_pvs_prefix_resultentrycellmiddlepositive. dst_positive_code_prefix_resultentrycellmiddle = ff_q_pvs_prefix_resultentrycellmiddlepositive * S ((S (dfg_middle_prefix_resultentrycell)) * dst_positive_scale_prefix_resultentrycellmiddle) + (dst_positive_prefix_resultentrycellmiddle))) /\ (((((exists ff_h_pvs_prefix_resultentrycellmiddlenegative. ff_h_pvs_prefix_resultentrycellmiddlenegative + S (dst_negative_prefix_resultentrycellmiddle) = S ((S (dfg_middle_prefix_resultentrycell)) * dst_negative_scale_prefix_resultentrycellmiddle)) /\ exists ff_q_pvs_prefix_resultentrycellmiddlenegative. dst_negative_code_prefix_resultentrycellmiddle = ff_q_pvs_prefix_resultentrycellmiddlenegative * S ((S (dfg_middle_prefix_resultentrycell)) * dst_negative_scale_prefix_resultentrycellmiddle) + (dst_negative_prefix_resultentrycellmiddle))) /\ (exists ge_balance_positive_prefix_resultentrycellmiddlevalue ge_balance_negative_prefix_resultentrycellmiddlevalue. (((((dfg_value_prefix_resultentrycell) = 2 * (ge_balance_positive_prefix_resultentrycellmiddlevalue) /\ (ge_balance_negative_prefix_resultentrycellmiddlevalue) = 0) \/ exists ge_signed_half_prefix_resultentrycellmiddlevaluedecode. (((dfg_value_prefix_resultentrycell) = 2 * ge_signed_half_prefix_resultentrycellmiddlevaluedecode + 1 /\ (ge_balance_positive_prefix_resultentrycellmiddlevalue) = 0) /\ (ge_balance_negative_prefix_resultentrycellmiddlevalue) = S ge_signed_half_prefix_resultentrycellmiddlevaluedecode))) /\ ((dst_positive_prefix_resultentrycellmiddle) + ge_balance_negative_prefix_resultentrycellmiddlevalue = (dst_negative_prefix_resultentrycellmiddle) + ge_balance_positive_prefix_resultentrycellmiddlevalue))))))))) /\ (exists dfg_inner_prefix_resultentrycellproduct. ((exists sto_ap_prefix_resultentrycellproductinner sto_an_prefix_resultentrycellproductinner sto_bp_prefix_resultentrycellproductinner sto_bn_prefix_resultentrycellproductinner sto_cp_prefix_resultentrycellproductinner sto_cn_prefix_resultentrycellproductinner. (((((dfg_last_prefix_resultentrycell) = 2 * (sto_ap_prefix_resultentrycellproductinner) /\ (sto_an_prefix_resultentrycellproductinner) = 0) \/ exists ge_signed_half_prefix_resultentrycellproductinnerleft. (((dfg_last_prefix_resultentrycell) = 2 * ge_signed_half_prefix_resultentrycellproductinnerleft + 1 /\ (sto_ap_prefix_resultentrycellproductinner) = 0) /\ (sto_an_prefix_resultentrycellproductinner) = S ge_signed_half_prefix_resultentrycellproductinnerleft))) /\ ((((((dfg_value_prefix_resultentrycell) = 2 * (sto_bp_prefix_resultentrycellproductinner) /\ (sto_bn_prefix_resultentrycellproductinner) = 0) \/ exists ge_signed_half_prefix_resultentrycellproductinnerright. (((dfg_value_prefix_resultentrycell) = 2 * ge_signed_half_prefix_resultentrycellproductinnerright + 1 /\ (sto_bp_prefix_resultentrycellproductinner) = 0) /\ (sto_bn_prefix_resultentrycellproductinner) = S ge_signed_half_prefix_resultentrycellproductinnerright))) /\ ((((((dfg_inner_prefix_resultentrycellproduct) = 2 * (sto_cp_prefix_resultentrycellproductinner) /\ (sto_cn_prefix_resultentrycellproductinner) = 0) \/ exists ge_signed_half_prefix_resultentrycellproductinneroutput. (((dfg_inner_prefix_resultentrycellproduct) = 2 * ge_signed_half_prefix_resultentrycellproductinneroutput + 1 /\ (sto_cp_prefix_resultentrycellproductinner) = 0) /\ (sto_cn_prefix_resultentrycellproductinner) = S ge_signed_half_prefix_resultentrycellproductinneroutput))) /\ ((sto_ap_prefix_resultentrycellproductinner * sto_bp_prefix_resultentrycellproductinner + sto_an_prefix_resultentrycellproductinner * sto_bn_prefix_resultentrycellproductinner) + sto_cn_prefix_resultentrycellproductinner = (sto_ap_prefix_resultentrycellproductinner * sto_bn_prefix_resultentrycellproductinner + sto_an_prefix_resultentrycellproductinner * sto_bp_prefix_resultentrycellproductinner) + sto_cp_prefix_resultentrycellproductinner))))))) /\ (exists sto_ap_prefix_resultentrycellproductouter sto_an_prefix_resultentrycellproductouter sto_bp_prefix_resultentrycellproductouter sto_bn_prefix_resultentrycellproductouter sto_cp_prefix_resultentrycellproductouter sto_cn_prefix_resultentrycellproductouter. (((((dfg_first_prefix_resultentrycell) = 2 * (sto_ap_prefix_resultentrycellproductouter) /\ (sto_an_prefix_resultentrycellproductouter) = 0) \/ exists ge_signed_half_prefix_resultentrycellproductouterleft. (((dfg_first_prefix_resultentrycell) = 2 * ge_signed_half_prefix_resultentrycellproductouterleft + 1 /\ (sto_ap_prefix_resultentrycellproductouter) = 0) /\ (sto_an_prefix_resultentrycellproductouter) = S ge_signed_half_prefix_resultentrycellproductouterleft))) /\ ((((((dfg_inner_prefix_resultentrycellproduct) = 2 * (sto_bp_prefix_resultentrycellproductouter) /\ (sto_bn_prefix_resultentrycellproductouter) = 0) \/ exists ge_signed_half_prefix_resultentrycellproductouterright. (((dfg_inner_prefix_resultentrycellproduct) = 2 * ge_signed_half_prefix_resultentrycellproductouterright + 1 /\ (sto_bp_prefix_resultentrycellproductouter) = 0) /\ (sto_bn_prefix_resultentrycellproductouter) = S ge_signed_half_prefix_resultentrycellproductouterright))) /\ ((((((dfg_flat_value_prefix_result) = 2 * (sto_cp_prefix_resultentrycellproductouter) /\ (sto_cn_prefix_resultentrycellproductouter) = 0) \/ exists ge_signed_half_prefix_resultentrycellproductouteroutput. (((dfg_flat_value_prefix_result) = 2 * ge_signed_half_prefix_resultentrycellproductouteroutput + 1 /\ (sto_cp_prefix_resultentrycellproductouter) = 0) /\ (sto_cn_prefix_resultentrycellproductouter) = S ge_signed_half_prefix_resultentrycellproductouteroutput))) /\ ((sto_ap_prefix_resultentrycellproductouter * sto_bp_prefix_resultentrycellproductouter + sto_an_prefix_resultentrycellproductouter * sto_bn_prefix_resultentrycellproductouter) + sto_cn_prefix_resultentrycellproductouter = (sto_ap_prefix_resultentrycellproductouter * sto_bn_prefix_resultentrycellproductouter + sto_an_prefix_resultentrycellproductouter * sto_bp_prefix_resultentrycellproductouter) + sto_cp_prefix_resultentrycellproductouter))))))))))))))))))))) \/ ((((dfg_flat_row_prefix_resultentry)=0 \/ ((dfg_flat_column_prefix_resultentry)=0 \/ ~(exists pvs_factor_prefix_resultentrycellomittednondivisor. (n) = ((dfg_flat_row_prefix_resultentry)*(dfg_flat_column_prefix_resultentry)) * pvs_factor_prefix_resultentrycellomittednondivisor))) /\ ((dfg_flat_value_prefix_result)=0)))))))))))Constructive proof overview
Generated structural guide
Ordinary induction constructs each actual inclusive flat prefix, with an independently witnessed quotient, remainder and signed value at every extension.
The unchanged tactic script uses 4 declared prerequisites and contains 71 exact native proof lines.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
DF0008 dirichlet_grid_flat_entry_exists arithmetic_signed_table_singleton Alpha theorem; checked-use authorized DF000A dirichlet_grid_flat_prefix_zero DF000B dirichlet_grid_flat_prefix_appendDirect dependents
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
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 (3)
01Fix variables and assumptionsL1–5
02Induction on lL6–9
03Establish hvL10–19
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet grid flat entry exists.
- L10
have hv : ∃ z. DirichletFlatEntry(F,G,H,n,0,z)Definitions: DirichletFlatEntry - L11
specialize dirichlet_grid_flat_entry_exists (F) - L12
specialize dirichlet_grid_flat_entry_exists (G) - L13
specialize dirichlet_grid_flat_entry_exists (H) - L14
specialize dirichlet_grid_flat_entry_exists (n) - L15
specialize dirichlet_grid_flat_entry_exists (0) - L16
apply dirichlet_grid_flat_entry_exists - L17
exact hF - L18
exact hG - L19
exact hH
04Separate the logical casesL20–20
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L20
cases hv
05Establish htL21–23
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply arithmetic signed table singleton.
- L21
have ht : ∃ T. ArithTable(0,T) ∧ ArithAt(T,0,x)Definitions: ArithTableArithAt - L22
specialize arithmetic_signed_table_singleton (x) - L23
apply arithmetic_signed_table_singleton
06Separate the logical casesL24–25
07Construct an explicit witnessL26–26
Supply the displayed value, then prove that it has the required property.
- L26
exists x1
08Use earlier factsL27–36
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L27
specialize dirichlet_grid_flat_prefix_zero (F) - L28
specialize dirichlet_grid_flat_prefix_zero (G) - L29
specialize dirichlet_grid_flat_prefix_zero (H) - L30
specialize dirichlet_grid_flat_prefix_zero (n) - L31
specialize dirichlet_grid_flat_prefix_zero (x1) - L32
specialize dirichlet_grid_flat_prefix_zero (x) - L33
apply dirichlet_grid_flat_prefix_zero - L34
exact ht_witness_left - L35
exact ht_witness_right - L36
exact hv_witness
09Fix variables and assumptionsL37–39
10Establish hpL40–44
11Separate the logical casesL45–45
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L45
cases hp
12Establish hvL46–55
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet grid flat entry exists.
- L46
have hv : ∃ z. DirichletFlatEntry(F,G,H,n,S l,z)Definitions: DirichletFlatEntry - L47
specialize dirichlet_grid_flat_entry_exists (F) - L48
specialize dirichlet_grid_flat_entry_exists (G) - L49
specialize dirichlet_grid_flat_entry_exists (H) - L50
specialize dirichlet_grid_flat_entry_exists (n) - L51
specialize dirichlet_grid_flat_entry_exists (S l) - L52
apply dirichlet_grid_flat_entry_exists - L53
exact hF - L54
exact hG - L55
exact hH
13Separate the logical casesL56–56
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L56
cases hv
14Establish hextL57–66
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet grid flat prefix append.
- L57
have hext : ∃ U. DirichletFlatPrefix(F,G,H,n,S l,U) ∧ (∀ y. ∀ z. ∀ m. Lt(y,S l) → ArithAt(x,y,z) → ArithAt(U,y,m) → z = m)Definitions: ArithAtDirichletFlatPrefixLt - L58
specialize dirichlet_grid_flat_prefix_append (F) - L59
specialize dirichlet_grid_flat_prefix_append (G) - L60
specialize dirichlet_grid_flat_prefix_append (H) - L61
specialize dirichlet_grid_flat_prefix_append (n) - L62
specialize dirichlet_grid_flat_prefix_append (l) - L63
specialize dirichlet_grid_flat_prefix_append (x) - L64
specialize dirichlet_grid_flat_prefix_append (x1) - L65
apply dirichlet_grid_flat_prefix_append - L66
exact hp_witness
15Use earlier factsL67–67
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L67
exact hv_witness
16Separate the logical casesL68–69
17Construct an explicit witnessL70–70
Supply the displayed value, then prove that it has the required property.
- L70
exists x2
18Use earlier factsL71–71
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L71
exact hext_witness_left
Original exact command ledger · 71 lines
- 0001
intro F - 0002
intro G - 0003
intro H - 0004
intro n - 0005
intro l - 0006
induction l - 0007
intro hF - 0008
intro hG - 0009
intro hH - 0010
have hv : exists z. (exists dfg_flat_row_prefix_base_value dfg_flat_column_prefix_base_value. (((0)=((S (n))*(dfg_flat_row_prefix_base_value)+(dfg_flat_column_prefix_base_value))) /\ (((exists pvs_gap_prefix_base_valueremainder. pvs_gap_prefix_base_valueremainder + S (dfg_flat_column_prefix_base_value) = (S (n))) /\ ((((~((dfg_flat_row_prefix_base_value)=0)) /\ (((~((dfg_flat_column_prefix_base_value)=0)) /\ (exists dfg_middle_prefix_base_valuecell dfg_first_prefix_base_valuecell dfg_last_prefix_base_valuecell dfg_value_prefix_base_valuecell. (((n)=((dfg_flat_row_prefix_base_value)*(dfg_flat_column_prefix_base_value))*dfg_middle_prefix_base_valuecell) /\ (((exists dst_positive_code_prefix_base_valuecellfirst dst_positive_scale_prefix_base_valuecellfirst dst_negative_code_prefix_base_valuecellfirst dst_negative_scale_prefix_base_valuecellfirst dst_positive_prefix_base_valuecellfirst dst_negative_prefix_base_valuecellfirst. (((F) = (((((dst_positive_code_prefix_base_valuecellfirst) + (dst_positive_scale_prefix_base_valuecellfirst)) * S ((dst_positive_code_prefix_base_valuecellfirst) + (dst_positive_scale_prefix_base_valuecellfirst)) + ((dst_positive_scale_prefix_base_valuecellfirst) + (dst_positive_scale_prefix_base_valuecellfirst))) + (((dst_negative_code_prefix_base_valuecellfirst) + (dst_negative_scale_prefix_base_valuecellfirst)) * S ((dst_negative_code_prefix_base_valuecellfirst) + (dst_negative_scale_prefix_base_valuecellfirst)) + ((dst_negative_scale_prefix_base_valuecellfirst) + (dst_negative_scale_prefix_base_valuecellfirst)))) * S ((((dst_positive_code_prefix_base_valuecellfirst) + (dst_positive_scale_prefix_base_valuecellfirst)) * S ((dst_positive_code_prefix_base_valuecellfirst) + (dst_positive_scale_prefix_base_valuecellfirst)) + ((dst_positive_scale_prefix_base_valuecellfirst) + (dst_positive_scale_prefix_base_valuecellfirst))) + (((dst_negative_code_prefix_base_valuecellfirst) + (dst_negative_scale_prefix_base_valuecellfirst)) * S ((dst_negative_code_prefix_base_valuecellfirst) + (dst_negative_scale_prefix_base_valuecellfirst)) + ((dst_negative_scale_prefix_base_valuecellfirst) + (dst_negative_scale_prefix_base_valuecellfirst)))) + ((((dst_negative_code_prefix_base_valuecellfirst) + (dst_negative_scale_prefix_base_valuecellfirst)) * S ((dst_negative_code_prefix_base_valuecellfirst) + (dst_negative_scale_prefix_base_valuecellfirst)) + ((dst_negative_scale_prefix_base_valuecellfirst) + (dst_negative_scale_prefix_base_valuecellfirst))) + (((dst_negative_code_prefix_base_valuecellfirst) + (dst_negative_scale_prefix_base_valuecellfirst)) * S ((dst_negative_code_prefix_base_valuecellfirst) + (dst_negative_scale_prefix_base_valuecellfirst)) + ((dst_negative_scale_prefix_base_valuecellfirst) + (dst_negative_scale_prefix_base_valuecellfirst)))))) /\ (((((exists ff_h_pvs_prefix_base_valuecellfirstpositive. ff_h_pvs_prefix_base_valuecellfirstpositive + S (dst_positive_prefix_base_valuecellfirst) = S ((S (dfg_flat_row_prefix_base_value)) * dst_positive_scale_prefix_base_valuecellfirst)) /\ exists ff_q_pvs_prefix_base_valuecellfirstpositive. dst_positive_code_prefix_base_valuecellfirst = ff_q_pvs_prefix_base_valuecellfirstpositive * S ((S (dfg_flat_row_prefix_base_value)) * dst_positive_scale_prefix_base_valuecellfirst) + (dst_positive_prefix_base_valuecellfirst))) /\ (((((exists ff_h_pvs_prefix_base_valuecellfirstnegative. ff_h_pvs_prefix_base_valuecellfirstnegative + S (dst_negative_prefix_base_valuecellfirst) = S ((S (dfg_flat_row_prefix_base_value)) * dst_negative_scale_prefix_base_valuecellfirst)) /\ exists ff_q_pvs_prefix_base_valuecellfirstnegative. dst_negative_code_prefix_base_valuecellfirst = ff_q_pvs_prefix_base_valuecellfirstnegative * S ((S (dfg_flat_row_prefix_base_value)) * dst_negative_scale_prefix_base_valuecellfirst) + (dst_negative_prefix_base_valuecellfirst))) /\ (exists ge_balance_positive_prefix_base_valuecellfirstvalue ge_balance_negative_prefix_base_valuecellfirstvalue. (((((dfg_first_prefix_base_valuecell) = 2 * (ge_balance_positive_prefix_base_valuecellfirstvalue) /\ (ge_balance_negative_prefix_base_valuecellfirstvalue) = 0) \/ exists ge_signed_half_prefix_base_valuecellfirstvaluedecode. (((dfg_first_prefix_base_valuecell) = 2 * ge_signed_half_prefix_base_valuecellfirstvaluedecode + 1 /\ (ge_balance_positive_prefix_base_valuecellfirstvalue) = 0) /\ (ge_balance_negative_prefix_base_valuecellfirstvalue) = S ge_signed_half_prefix_base_valuecellfirstvaluedecode))) /\ ((dst_positive_prefix_base_valuecellfirst) + ge_balance_negative_prefix_base_valuecellfirstvalue = (dst_negative_prefix_base_valuecellfirst) + ge_balance_positive_prefix_base_valuecellfirstvalue))))))))) /\ (((exists dst_positive_code_prefix_base_valuecelllast dst_positive_scale_prefix_base_valuecelllast dst_negative_code_prefix_base_valuecelllast dst_negative_scale_prefix_base_valuecelllast dst_positive_prefix_base_valuecelllast dst_negative_prefix_base_valuecelllast. (((H) = (((((dst_positive_code_prefix_base_valuecelllast) + (dst_positive_scale_prefix_base_valuecelllast)) * S ((dst_positive_code_prefix_base_valuecelllast) + (dst_positive_scale_prefix_base_valuecelllast)) + ((dst_positive_scale_prefix_base_valuecelllast) + (dst_positive_scale_prefix_base_valuecelllast))) + (((dst_negative_code_prefix_base_valuecelllast) + (dst_negative_scale_prefix_base_valuecelllast)) * S ((dst_negative_code_prefix_base_valuecelllast) + (dst_negative_scale_prefix_base_valuecelllast)) + ((dst_negative_scale_prefix_base_valuecelllast) + (dst_negative_scale_prefix_base_valuecelllast)))) * S ((((dst_positive_code_prefix_base_valuecelllast) + (dst_positive_scale_prefix_base_valuecelllast)) * S ((dst_positive_code_prefix_base_valuecelllast) + (dst_positive_scale_prefix_base_valuecelllast)) + ((dst_positive_scale_prefix_base_valuecelllast) + (dst_positive_scale_prefix_base_valuecelllast))) + (((dst_negative_code_prefix_base_valuecelllast) + (dst_negative_scale_prefix_base_valuecelllast)) * S ((dst_negative_code_prefix_base_valuecelllast) + (dst_negative_scale_prefix_base_valuecelllast)) + ((dst_negative_scale_prefix_base_valuecelllast) + (dst_negative_scale_prefix_base_valuecelllast)))) + ((((dst_negative_code_prefix_base_valuecelllast) + (dst_negative_scale_prefix_base_valuecelllast)) * S ((dst_negative_code_prefix_base_valuecelllast) + (dst_negative_scale_prefix_base_valuecelllast)) + ((dst_negative_scale_prefix_base_valuecelllast) + (dst_negative_scale_prefix_base_valuecelllast))) + (((dst_negative_code_prefix_base_valuecelllast) + (dst_negative_scale_prefix_base_valuecelllast)) * S ((dst_negative_code_prefix_base_valuecelllast) + (dst_negative_scale_prefix_base_valuecelllast)) + ((dst_negative_scale_prefix_base_valuecelllast) + (dst_negative_scale_prefix_base_valuecelllast)))))) /\ (((((exists ff_h_pvs_prefix_base_valuecelllastpositive. ff_h_pvs_prefix_base_valuecelllastpositive + S (dst_positive_prefix_base_valuecelllast) = S ((S (dfg_flat_column_prefix_base_value)) * dst_positive_scale_prefix_base_valuecelllast)) /\ exists ff_q_pvs_prefix_base_valuecelllastpositive. dst_positive_code_prefix_base_valuecelllast = ff_q_pvs_prefix_base_valuecelllastpositive * S ((S (dfg_flat_column_prefix_base_value)) * dst_positive_scale_prefix_base_valuecelllast) + (dst_positive_prefix_base_valuecelllast))) /\ (((((exists ff_h_pvs_prefix_base_valuecelllastnegative. ff_h_pvs_prefix_base_valuecelllastnegative + S (dst_negative_prefix_base_valuecelllast) = S ((S (dfg_flat_column_prefix_base_value)) * dst_negative_scale_prefix_base_valuecelllast)) /\ exists ff_q_pvs_prefix_base_valuecelllastnegative. dst_negative_code_prefix_base_valuecelllast = ff_q_pvs_prefix_base_valuecelllastnegative * S ((S (dfg_flat_column_prefix_base_value)) * dst_negative_scale_prefix_base_valuecelllast) + (dst_negative_prefix_base_valuecelllast))) /\ (exists ge_balance_positive_prefix_base_valuecelllastvalue ge_balance_negative_prefix_base_valuecelllastvalue. (((((dfg_last_prefix_base_valuecell) = 2 * (ge_balance_positive_prefix_base_valuecelllastvalue) /\ (ge_balance_negative_prefix_base_valuecelllastvalue) = 0) \/ exists ge_signed_half_prefix_base_valuecelllastvaluedecode. (((dfg_last_prefix_base_valuecell) = 2 * ge_signed_half_prefix_base_valuecelllastvaluedecode + 1 /\ (ge_balance_positive_prefix_base_valuecelllastvalue) = 0) /\ (ge_balance_negative_prefix_base_valuecelllastvalue) = S ge_signed_half_prefix_base_valuecelllastvaluedecode))) /\ ((dst_positive_prefix_base_valuecelllast) + ge_balance_negative_prefix_base_valuecelllastvalue = (dst_negative_prefix_base_valuecelllast) + ge_balance_positive_prefix_base_valuecelllastvalue))))))))) /\ (((exists dst_positive_code_prefix_base_valuecellmiddle dst_positive_scale_prefix_base_valuecellmiddle dst_negative_code_prefix_base_valuecellmiddle dst_negative_scale_prefix_base_valuecellmiddle dst_positive_prefix_base_valuecellmiddle dst_negative_prefix_base_valuecellmiddle. (((G) = (((((dst_positive_code_prefix_base_valuecellmiddle) + (dst_positive_scale_prefix_base_valuecellmiddle)) * S ((dst_positive_code_prefix_base_valuecellmiddle) + (dst_positive_scale_prefix_base_valuecellmiddle)) + ((dst_positive_scale_prefix_base_valuecellmiddle) + (dst_positive_scale_prefix_base_valuecellmiddle))) + (((dst_negative_code_prefix_base_valuecellmiddle) + (dst_negative_scale_prefix_base_valuecellmiddle)) * S ((dst_negative_code_prefix_base_valuecellmiddle) + (dst_negative_scale_prefix_base_valuecellmiddle)) + ((dst_negative_scale_prefix_base_valuecellmiddle) + (dst_negative_scale_prefix_base_valuecellmiddle)))) * S ((((dst_positive_code_prefix_base_valuecellmiddle) + (dst_positive_scale_prefix_base_valuecellmiddle)) * S ((dst_positive_code_prefix_base_valuecellmiddle) + (dst_positive_scale_prefix_base_valuecellmiddle)) + ((dst_positive_scale_prefix_base_valuecellmiddle) + (dst_positive_scale_prefix_base_valuecellmiddle))) + (((dst_negative_code_prefix_base_valuecellmiddle) + (dst_negative_scale_prefix_base_valuecellmiddle)) * S ((dst_negative_code_prefix_base_valuecellmiddle) + (dst_negative_scale_prefix_base_valuecellmiddle)) + ((dst_negative_scale_prefix_base_valuecellmiddle) + (dst_negative_scale_prefix_base_valuecellmiddle)))) + ((((dst_negative_code_prefix_base_valuecellmiddle) + (dst_negative_scale_prefix_base_valuecellmiddle)) * S ((dst_negative_code_prefix_base_valuecellmiddle) + (dst_negative_scale_prefix_base_valuecellmiddle)) + ((dst_negative_scale_prefix_base_valuecellmiddle) + (dst_negative_scale_prefix_base_valuecellmiddle))) + (((dst_negative_code_prefix_base_valuecellmiddle) + (dst_negative_scale_prefix_base_valuecellmiddle)) * S ((dst_negative_code_prefix_base_valuecellmiddle) + (dst_negative_scale_prefix_base_valuecellmiddle)) + ((dst_negative_scale_prefix_base_valuecellmiddle) + (dst_negative_scale_prefix_base_valuecellmiddle)))))) /\ (((((exists ff_h_pvs_prefix_base_valuecellmiddlepositive. ff_h_pvs_prefix_base_valuecellmiddlepositive + S (dst_positive_prefix_base_valuecellmiddle) = S ((S (dfg_middle_prefix_base_valuecell)) * dst_positive_scale_prefix_base_valuecellmiddle)) /\ exists ff_q_pvs_prefix_base_valuecellmiddlepositive. dst_positive_code_prefix_base_valuecellmiddle = ff_q_pvs_prefix_base_valuecellmiddlepositive * S ((S (dfg_middle_prefix_base_valuecell)) * dst_positive_scale_prefix_base_valuecellmiddle) + (dst_positive_prefix_base_valuecellmiddle))) /\ (((((exists ff_h_pvs_prefix_base_valuecellmiddlenegative. ff_h_pvs_prefix_base_valuecellmiddlenegative + S (dst_negative_prefix_base_valuecellmiddle) = S ((S (dfg_middle_prefix_base_valuecell)) * dst_negative_scale_prefix_base_valuecellmiddle)) /\ exists ff_q_pvs_prefix_base_valuecellmiddlenegative. dst_negative_code_prefix_base_valuecellmiddle = ff_q_pvs_prefix_base_valuecellmiddlenegative * S ((S (dfg_middle_prefix_base_valuecell)) * dst_negative_scale_prefix_base_valuecellmiddle) + (dst_negative_prefix_base_valuecellmiddle))) /\ (exists ge_balance_positive_prefix_base_valuecellmiddlevalue ge_balance_negative_prefix_base_valuecellmiddlevalue. (((((dfg_value_prefix_base_valuecell) = 2 * (ge_balance_positive_prefix_base_valuecellmiddlevalue) /\ (ge_balance_negative_prefix_base_valuecellmiddlevalue) = 0) \/ exists ge_signed_half_prefix_base_valuecellmiddlevaluedecode. (((dfg_value_prefix_base_valuecell) = 2 * ge_signed_half_prefix_base_valuecellmiddlevaluedecode + 1 /\ (ge_balance_positive_prefix_base_valuecellmiddlevalue) = 0) /\ (ge_balance_negative_prefix_base_valuecellmiddlevalue) = S ge_signed_half_prefix_base_valuecellmiddlevaluedecode))) /\ ((dst_positive_prefix_base_valuecellmiddle) + ge_balance_negative_prefix_base_valuecellmiddlevalue = (dst_negative_prefix_base_valuecellmiddle) + ge_balance_positive_prefix_base_valuecellmiddlevalue))))))))) /\ (exists dfg_inner_prefix_base_valuecellproduct. ((exists sto_ap_prefix_base_valuecellproductinner sto_an_prefix_base_valuecellproductinner sto_bp_prefix_base_valuecellproductinner sto_bn_prefix_base_valuecellproductinner sto_cp_prefix_base_valuecellproductinner sto_cn_prefix_base_valuecellproductinner. (((((dfg_last_prefix_base_valuecell) = 2 * (sto_ap_prefix_base_valuecellproductinner) /\ (sto_an_prefix_base_valuecellproductinner) = 0) \/ exists ge_signed_half_prefix_base_valuecellproductinnerleft. (((dfg_last_prefix_base_valuecell) = 2 * ge_signed_half_prefix_base_valuecellproductinnerleft + 1 /\ (sto_ap_prefix_base_valuecellproductinner) = 0) /\ (sto_an_prefix_base_valuecellproductinner) = S ge_signed_half_prefix_base_valuecellproductinnerleft))) /\ ((((((dfg_value_prefix_base_valuecell) = 2 * (sto_bp_prefix_base_valuecellproductinner) /\ (sto_bn_prefix_base_valuecellproductinner) = 0) \/ exists ge_signed_half_prefix_base_valuecellproductinnerright. (((dfg_value_prefix_base_valuecell) = 2 * ge_signed_half_prefix_base_valuecellproductinnerright + 1 /\ (sto_bp_prefix_base_valuecellproductinner) = 0) /\ (sto_bn_prefix_base_valuecellproductinner) = S ge_signed_half_prefix_base_valuecellproductinnerright))) /\ ((((((dfg_inner_prefix_base_valuecellproduct) = 2 * (sto_cp_prefix_base_valuecellproductinner) /\ (sto_cn_prefix_base_valuecellproductinner) = 0) \/ exists ge_signed_half_prefix_base_valuecellproductinneroutput. (((dfg_inner_prefix_base_valuecellproduct) = 2 * ge_signed_half_prefix_base_valuecellproductinneroutput + 1 /\ (sto_cp_prefix_base_valuecellproductinner) = 0) /\ (sto_cn_prefix_base_valuecellproductinner) = S ge_signed_half_prefix_base_valuecellproductinneroutput))) /\ ((sto_ap_prefix_base_valuecellproductinner * sto_bp_prefix_base_valuecellproductinner + sto_an_prefix_base_valuecellproductinner * sto_bn_prefix_base_valuecellproductinner) + sto_cn_prefix_base_valuecellproductinner = (sto_ap_prefix_base_valuecellproductinner * sto_bn_prefix_base_valuecellproductinner + sto_an_prefix_base_valuecellproductinner * sto_bp_prefix_base_valuecellproductinner) + sto_cp_prefix_base_valuecellproductinner))))))) /\ (exists sto_ap_prefix_base_valuecellproductouter sto_an_prefix_base_valuecellproductouter sto_bp_prefix_base_valuecellproductouter sto_bn_prefix_base_valuecellproductouter sto_cp_prefix_base_valuecellproductouter sto_cn_prefix_base_valuecellproductouter. (((((dfg_first_prefix_base_valuecell) = 2 * (sto_ap_prefix_base_valuecellproductouter) /\ (sto_an_prefix_base_valuecellproductouter) = 0) \/ exists ge_signed_half_prefix_base_valuecellproductouterleft. (((dfg_first_prefix_base_valuecell) = 2 * ge_signed_half_prefix_base_valuecellproductouterleft + 1 /\ (sto_ap_prefix_base_valuecellproductouter) = 0) /\ (sto_an_prefix_base_valuecellproductouter) = S ge_signed_half_prefix_base_valuecellproductouterleft))) /\ ((((((dfg_inner_prefix_base_valuecellproduct) = 2 * (sto_bp_prefix_base_valuecellproductouter) /\ (sto_bn_prefix_base_valuecellproductouter) = 0) \/ exists ge_signed_half_prefix_base_valuecellproductouterright. (((dfg_inner_prefix_base_valuecellproduct) = 2 * ge_signed_half_prefix_base_valuecellproductouterright + 1 /\ (sto_bp_prefix_base_valuecellproductouter) = 0) /\ (sto_bn_prefix_base_valuecellproductouter) = S ge_signed_half_prefix_base_valuecellproductouterright))) /\ ((((((z) = 2 * (sto_cp_prefix_base_valuecellproductouter) /\ (sto_cn_prefix_base_valuecellproductouter) = 0) \/ exists ge_signed_half_prefix_base_valuecellproductouteroutput. (((z) = 2 * ge_signed_half_prefix_base_valuecellproductouteroutput + 1 /\ (sto_cp_prefix_base_valuecellproductouter) = 0) /\ (sto_cn_prefix_base_valuecellproductouter) = S ge_signed_half_prefix_base_valuecellproductouteroutput))) /\ ((sto_ap_prefix_base_valuecellproductouter * sto_bp_prefix_base_valuecellproductouter + sto_an_prefix_base_valuecellproductouter * sto_bn_prefix_base_valuecellproductouter) + sto_cn_prefix_base_valuecellproductouter = (sto_ap_prefix_base_valuecellproductouter * sto_bn_prefix_base_valuecellproductouter + sto_an_prefix_base_valuecellproductouter * sto_bp_prefix_base_valuecellproductouter) + sto_cp_prefix_base_valuecellproductouter))))))))))))))))))))) \/ ((((dfg_flat_row_prefix_base_value)=0 \/ ((dfg_flat_column_prefix_base_value)=0 \/ ~(exists pvs_factor_prefix_base_valuecellomittednondivisor. (n) = ((dfg_flat_row_prefix_base_value)*(dfg_flat_column_prefix_base_value)) * pvs_factor_prefix_base_valuecellomittednondivisor))) /\ ((z)=0)))))))) - 0011
specialize dirichlet_grid_flat_entry_exists (F) - 0012
specialize dirichlet_grid_flat_entry_exists (G) - 0013
specialize dirichlet_grid_flat_entry_exists (H) - 0014
specialize dirichlet_grid_flat_entry_exists (n) - 0015
specialize dirichlet_grid_flat_entry_exists (0) - 0016
apply dirichlet_grid_flat_entry_exists - 0017
exact hF - 0018
exact hG - 0019
exact hH - 0020
cases hv - 0021
have ht : exists T. (((exists dst_positive_code_prefix_base_table dst_positive_scale_prefix_base_table dst_negative_code_prefix_base_table dst_negative_scale_prefix_base_table. (((T) = (((((dst_positive_code_prefix_base_table) + (dst_positive_scale_prefix_base_table)) * S ((dst_positive_code_prefix_base_table) + (dst_positive_scale_prefix_base_table)) + ((dst_positive_scale_prefix_base_table) + (dst_positive_scale_prefix_base_table))) + (((dst_negative_code_prefix_base_table) + (dst_negative_scale_prefix_base_table)) * S ((dst_negative_code_prefix_base_table) + (dst_negative_scale_prefix_base_table)) + ((dst_negative_scale_prefix_base_table) + (dst_negative_scale_prefix_base_table)))) * S ((((dst_positive_code_prefix_base_table) + (dst_positive_scale_prefix_base_table)) * S ((dst_positive_code_prefix_base_table) + (dst_positive_scale_prefix_base_table)) + ((dst_positive_scale_prefix_base_table) + (dst_positive_scale_prefix_base_table))) + (((dst_negative_code_prefix_base_table) + (dst_negative_scale_prefix_base_table)) * S ((dst_negative_code_prefix_base_table) + (dst_negative_scale_prefix_base_table)) + ((dst_negative_scale_prefix_base_table) + (dst_negative_scale_prefix_base_table)))) + ((((dst_negative_code_prefix_base_table) + (dst_negative_scale_prefix_base_table)) * S ((dst_negative_code_prefix_base_table) + (dst_negative_scale_prefix_base_table)) + ((dst_negative_scale_prefix_base_table) + (dst_negative_scale_prefix_base_table))) + (((dst_negative_code_prefix_base_table) + (dst_negative_scale_prefix_base_table)) * S ((dst_negative_code_prefix_base_table) + (dst_negative_scale_prefix_base_table)) + ((dst_negative_scale_prefix_base_table) + (dst_negative_scale_prefix_base_table)))))) /\ (forall dst_index_prefix_base_table. (exists pvs_le_gap_prefix_base_tabledomain. pvs_le_gap_prefix_base_tabledomain + (dst_index_prefix_base_table) = (0)) -> exists dst_positive_prefix_base_table dst_negative_prefix_base_table dst_value_prefix_base_table. ((((exists ff_h_pvs_prefix_base_tableentrypositive. ff_h_pvs_prefix_base_tableentrypositive + S (dst_positive_prefix_base_table) = S ((S (dst_index_prefix_base_table)) * dst_positive_scale_prefix_base_table)) /\ exists ff_q_pvs_prefix_base_tableentrypositive. dst_positive_code_prefix_base_table = ff_q_pvs_prefix_base_tableentrypositive * S ((S (dst_index_prefix_base_table)) * dst_positive_scale_prefix_base_table) + (dst_positive_prefix_base_table))) /\ (((((exists ff_h_pvs_prefix_base_tableentrynegative. ff_h_pvs_prefix_base_tableentrynegative + S (dst_negative_prefix_base_table) = S ((S (dst_index_prefix_base_table)) * dst_negative_scale_prefix_base_table)) /\ exists ff_q_pvs_prefix_base_tableentrynegative. dst_negative_code_prefix_base_table = ff_q_pvs_prefix_base_tableentrynegative * S ((S (dst_index_prefix_base_table)) * dst_negative_scale_prefix_base_table) + (dst_negative_prefix_base_table))) /\ (exists ge_balance_positive_prefix_base_tableentryvalue ge_balance_negative_prefix_base_tableentryvalue. (((((dst_value_prefix_base_table) = 2 * (ge_balance_positive_prefix_base_tableentryvalue) /\ (ge_balance_negative_prefix_base_tableentryvalue) = 0) \/ exists ge_signed_half_prefix_base_tableentryvaluedecode. (((dst_value_prefix_base_table) = 2 * ge_signed_half_prefix_base_tableentryvaluedecode + 1 /\ (ge_balance_positive_prefix_base_tableentryvalue) = 0) /\ (ge_balance_negative_prefix_base_tableentryvalue) = S ge_signed_half_prefix_base_tableentryvaluedecode))) /\ ((dst_positive_prefix_base_table) + ge_balance_negative_prefix_base_tableentryvalue = (dst_negative_prefix_base_table) + ge_balance_positive_prefix_base_tableentryvalue))))))))) /\ (exists dst_positive_code_prefix_base_entry dst_positive_scale_prefix_base_entry dst_negative_code_prefix_base_entry dst_negative_scale_prefix_base_entry dst_positive_prefix_base_entry dst_negative_prefix_base_entry. (((T) = (((((dst_positive_code_prefix_base_entry) + (dst_positive_scale_prefix_base_entry)) * S ((dst_positive_code_prefix_base_entry) + (dst_positive_scale_prefix_base_entry)) + ((dst_positive_scale_prefix_base_entry) + (dst_positive_scale_prefix_base_entry))) + (((dst_negative_code_prefix_base_entry) + (dst_negative_scale_prefix_base_entry)) * S ((dst_negative_code_prefix_base_entry) + (dst_negative_scale_prefix_base_entry)) + ((dst_negative_scale_prefix_base_entry) + (dst_negative_scale_prefix_base_entry)))) * S ((((dst_positive_code_prefix_base_entry) + (dst_positive_scale_prefix_base_entry)) * S ((dst_positive_code_prefix_base_entry) + (dst_positive_scale_prefix_base_entry)) + ((dst_positive_scale_prefix_base_entry) + (dst_positive_scale_prefix_base_entry))) + (((dst_negative_code_prefix_base_entry) + (dst_negative_scale_prefix_base_entry)) * S ((dst_negative_code_prefix_base_entry) + (dst_negative_scale_prefix_base_entry)) + ((dst_negative_scale_prefix_base_entry) + (dst_negative_scale_prefix_base_entry)))) + ((((dst_negative_code_prefix_base_entry) + (dst_negative_scale_prefix_base_entry)) * S ((dst_negative_code_prefix_base_entry) + (dst_negative_scale_prefix_base_entry)) + ((dst_negative_scale_prefix_base_entry) + (dst_negative_scale_prefix_base_entry))) + (((dst_negative_code_prefix_base_entry) + (dst_negative_scale_prefix_base_entry)) * S ((dst_negative_code_prefix_base_entry) + (dst_negative_scale_prefix_base_entry)) + ((dst_negative_scale_prefix_base_entry) + (dst_negative_scale_prefix_base_entry)))))) /\ (((((exists ff_h_pvs_prefix_base_entrypositive. ff_h_pvs_prefix_base_entrypositive + S (dst_positive_prefix_base_entry) = S ((S (0)) * dst_positive_scale_prefix_base_entry)) /\ exists ff_q_pvs_prefix_base_entrypositive. dst_positive_code_prefix_base_entry = ff_q_pvs_prefix_base_entrypositive * S ((S (0)) * dst_positive_scale_prefix_base_entry) + (dst_positive_prefix_base_entry))) /\ (((((exists ff_h_pvs_prefix_base_entrynegative. ff_h_pvs_prefix_base_entrynegative + S (dst_negative_prefix_base_entry) = S ((S (0)) * dst_negative_scale_prefix_base_entry)) /\ exists ff_q_pvs_prefix_base_entrynegative. dst_negative_code_prefix_base_entry = ff_q_pvs_prefix_base_entrynegative * S ((S (0)) * dst_negative_scale_prefix_base_entry) + (dst_negative_prefix_base_entry))) /\ (exists ge_balance_positive_prefix_base_entryvalue ge_balance_negative_prefix_base_entryvalue. (((((x) = 2 * (ge_balance_positive_prefix_base_entryvalue) /\ (ge_balance_negative_prefix_base_entryvalue) = 0) \/ exists ge_signed_half_prefix_base_entryvaluedecode. (((x) = 2 * ge_signed_half_prefix_base_entryvaluedecode + 1 /\ (ge_balance_positive_prefix_base_entryvalue) = 0) /\ (ge_balance_negative_prefix_base_entryvalue) = S ge_signed_half_prefix_base_entryvaluedecode))) /\ ((dst_positive_prefix_base_entry) + ge_balance_negative_prefix_base_entryvalue = (dst_negative_prefix_base_entry) + ge_balance_positive_prefix_base_entryvalue))))))))))) - 0022
specialize arithmetic_signed_table_singleton (x) - 0023
apply arithmetic_signed_table_singleton - 0024
cases ht - 0025
cases ht_witness - 0026
exists x1 - 0027
specialize dirichlet_grid_flat_prefix_zero (F) - 0028
specialize dirichlet_grid_flat_prefix_zero (G) - 0029
specialize dirichlet_grid_flat_prefix_zero (H) - 0030
specialize dirichlet_grid_flat_prefix_zero (n) - 0031
specialize dirichlet_grid_flat_prefix_zero (x1) - 0032
specialize dirichlet_grid_flat_prefix_zero (x) - 0033
apply dirichlet_grid_flat_prefix_zero - 0034
exact ht_witness_left - 0035
exact ht_witness_right - 0036
exact hv_witness - 0037
intro hF - 0038
intro hG - 0039
intro hH - 0040
have hp : exists T. (((exists dst_positive_code_prefix_previoustable dst_positive_scale_prefix_previoustable dst_negative_code_prefix_previoustable dst_negative_scale_prefix_previoustable. (((T) = (((((dst_positive_code_prefix_previoustable) + (dst_positive_scale_prefix_previoustable)) * S ((dst_positive_code_prefix_previoustable) + (dst_positive_scale_prefix_previoustable)) + ((dst_positive_scale_prefix_previoustable) + (dst_positive_scale_prefix_previoustable))) + (((dst_negative_code_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)) * S ((dst_negative_code_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)) + ((dst_negative_scale_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)))) * S ((((dst_positive_code_prefix_previoustable) + (dst_positive_scale_prefix_previoustable)) * S ((dst_positive_code_prefix_previoustable) + (dst_positive_scale_prefix_previoustable)) + ((dst_positive_scale_prefix_previoustable) + (dst_positive_scale_prefix_previoustable))) + (((dst_negative_code_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)) * S ((dst_negative_code_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)) + ((dst_negative_scale_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)))) + ((((dst_negative_code_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)) * S ((dst_negative_code_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)) + ((dst_negative_scale_prefix_previoustable) + (dst_negative_scale_prefix_previoustable))) + (((dst_negative_code_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)) * S ((dst_negative_code_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)) + ((dst_negative_scale_prefix_previoustable) + (dst_negative_scale_prefix_previoustable)))))) /\ (forall dst_index_prefix_previoustable. (exists pvs_le_gap_prefix_previoustabledomain. pvs_le_gap_prefix_previoustabledomain + (dst_index_prefix_previoustable) = (l)) -> exists dst_positive_prefix_previoustable dst_negative_prefix_previoustable dst_value_prefix_previoustable. ((((exists ff_h_pvs_prefix_previoustableentrypositive. ff_h_pvs_prefix_previoustableentrypositive + S (dst_positive_prefix_previoustable) = S ((S (dst_index_prefix_previoustable)) * dst_positive_scale_prefix_previoustable)) /\ exists ff_q_pvs_prefix_previoustableentrypositive. dst_positive_code_prefix_previoustable = ff_q_pvs_prefix_previoustableentrypositive * S ((S (dst_index_prefix_previoustable)) * dst_positive_scale_prefix_previoustable) + (dst_positive_prefix_previoustable))) /\ (((((exists ff_h_pvs_prefix_previoustableentrynegative. ff_h_pvs_prefix_previoustableentrynegative + S (dst_negative_prefix_previoustable) = S ((S (dst_index_prefix_previoustable)) * dst_negative_scale_prefix_previoustable)) /\ exists ff_q_pvs_prefix_previoustableentrynegative. dst_negative_code_prefix_previoustable = ff_q_pvs_prefix_previoustableentrynegative * S ((S (dst_index_prefix_previoustable)) * dst_negative_scale_prefix_previoustable) + (dst_negative_prefix_previoustable))) /\ (exists ge_balance_positive_prefix_previoustableentryvalue ge_balance_negative_prefix_previoustableentryvalue. (((((dst_value_prefix_previoustable) = 2 * (ge_balance_positive_prefix_previoustableentryvalue) /\ (ge_balance_negative_prefix_previoustableentryvalue) = 0) \/ exists ge_signed_half_prefix_previoustableentryvaluedecode. (((dst_value_prefix_previoustable) = 2 * ge_signed_half_prefix_previoustableentryvaluedecode + 1 /\ (ge_balance_positive_prefix_previoustableentryvalue) = 0) /\ (ge_balance_negative_prefix_previoustableentryvalue) = S ge_signed_half_prefix_previoustableentryvaluedecode))) /\ ((dst_positive_prefix_previoustable) + ge_balance_negative_prefix_previoustableentryvalue = (dst_negative_prefix_previoustable) + ge_balance_positive_prefix_previoustableentryvalue))))))))) /\ (forall dfg_flat_index_prefix_previous dfg_flat_value_prefix_previous. (exists pvs_le_gap_prefix_previousbound. pvs_le_gap_prefix_previousbound + (dfg_flat_index_prefix_previous) = (l)) -> (exists dst_positive_code_prefix_previouslookup dst_positive_scale_prefix_previouslookup dst_negative_code_prefix_previouslookup dst_negative_scale_prefix_previouslookup dst_positive_prefix_previouslookup dst_negative_prefix_previouslookup. (((T) = (((((dst_positive_code_prefix_previouslookup) + (dst_positive_scale_prefix_previouslookup)) * S ((dst_positive_code_prefix_previouslookup) + (dst_positive_scale_prefix_previouslookup)) + ((dst_positive_scale_prefix_previouslookup) + (dst_positive_scale_prefix_previouslookup))) + (((dst_negative_code_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)) * S ((dst_negative_code_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)) + ((dst_negative_scale_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)))) * S ((((dst_positive_code_prefix_previouslookup) + (dst_positive_scale_prefix_previouslookup)) * S ((dst_positive_code_prefix_previouslookup) + (dst_positive_scale_prefix_previouslookup)) + ((dst_positive_scale_prefix_previouslookup) + (dst_positive_scale_prefix_previouslookup))) + (((dst_negative_code_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)) * S ((dst_negative_code_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)) + ((dst_negative_scale_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)))) + ((((dst_negative_code_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)) * S ((dst_negative_code_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)) + ((dst_negative_scale_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup))) + (((dst_negative_code_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)) * S ((dst_negative_code_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)) + ((dst_negative_scale_prefix_previouslookup) + (dst_negative_scale_prefix_previouslookup)))))) /\ (((((exists ff_h_pvs_prefix_previouslookuppositive. ff_h_pvs_prefix_previouslookuppositive + S (dst_positive_prefix_previouslookup) = S ((S (dfg_flat_index_prefix_previous)) * dst_positive_scale_prefix_previouslookup)) /\ exists ff_q_pvs_prefix_previouslookuppositive. dst_positive_code_prefix_previouslookup = ff_q_pvs_prefix_previouslookuppositive * S ((S (dfg_flat_index_prefix_previous)) * dst_positive_scale_prefix_previouslookup) + (dst_positive_prefix_previouslookup))) /\ (((((exists ff_h_pvs_prefix_previouslookupnegative. ff_h_pvs_prefix_previouslookupnegative + S (dst_negative_prefix_previouslookup) = S ((S (dfg_flat_index_prefix_previous)) * dst_negative_scale_prefix_previouslookup)) /\ exists ff_q_pvs_prefix_previouslookupnegative. dst_negative_code_prefix_previouslookup = ff_q_pvs_prefix_previouslookupnegative * S ((S (dfg_flat_index_prefix_previous)) * dst_negative_scale_prefix_previouslookup) + (dst_negative_prefix_previouslookup))) /\ (exists ge_balance_positive_prefix_previouslookupvalue ge_balance_negative_prefix_previouslookupvalue. (((((dfg_flat_value_prefix_previous) = 2 * (ge_balance_positive_prefix_previouslookupvalue) /\ (ge_balance_negative_prefix_previouslookupvalue) = 0) \/ exists ge_signed_half_prefix_previouslookupvaluedecode. (((dfg_flat_value_prefix_previous) = 2 * ge_signed_half_prefix_previouslookupvaluedecode + 1 /\ (ge_balance_positive_prefix_previouslookupvalue) = 0) /\ (ge_balance_negative_prefix_previouslookupvalue) = S ge_signed_half_prefix_previouslookupvaluedecode))) /\ ((dst_positive_prefix_previouslookup) + ge_balance_negative_prefix_previouslookupvalue = (dst_negative_prefix_previouslookup) + ge_balance_positive_prefix_previouslookupvalue))))))))) -> (exists dfg_flat_row_prefix_previousentry dfg_flat_column_prefix_previousentry. (((dfg_flat_index_prefix_previous)=((S (n))*(dfg_flat_row_prefix_previousentry)+(dfg_flat_column_prefix_previousentry))) /\ (((exists pvs_gap_prefix_previousentryremainder. pvs_gap_prefix_previousentryremainder + S (dfg_flat_column_prefix_previousentry) = (S (n))) /\ ((((~((dfg_flat_row_prefix_previousentry)=0)) /\ (((~((dfg_flat_column_prefix_previousentry)=0)) /\ (exists dfg_middle_prefix_previousentrycell dfg_first_prefix_previousentrycell dfg_last_prefix_previousentrycell dfg_value_prefix_previousentrycell. (((n)=((dfg_flat_row_prefix_previousentry)*(dfg_flat_column_prefix_previousentry))*dfg_middle_prefix_previousentrycell) /\ (((exists dst_positive_code_prefix_previousentrycellfirst dst_positive_scale_prefix_previousentrycellfirst dst_negative_code_prefix_previousentrycellfirst dst_negative_scale_prefix_previousentrycellfirst dst_positive_prefix_previousentrycellfirst dst_negative_prefix_previousentrycellfirst. (((F) = (((((dst_positive_code_prefix_previousentrycellfirst) + (dst_positive_scale_prefix_previousentrycellfirst)) * S ((dst_positive_code_prefix_previousentrycellfirst) + (dst_positive_scale_prefix_previousentrycellfirst)) + ((dst_positive_scale_prefix_previousentrycellfirst) + (dst_positive_scale_prefix_previousentrycellfirst))) + (((dst_negative_code_prefix_previousentrycellfirst) + (dst_negative_scale_prefix_previousentrycellfirst)) * S ((dst_negative_code_prefix_previousentrycellfirst) + (dst_negative_scale_prefix_previousentrycellfirst)) + ((dst_negative_scale_prefix_previousentrycellfirst) + (dst_negative_scale_prefix_previousentrycellfirst)))) * S ((((dst_positive_code_prefix_previousentrycellfirst) + (dst_positive_scale_prefix_previousentrycellfirst)) * S ((dst_positive_code_prefix_previousentrycellfirst) + (dst_positive_scale_prefix_previousentrycellfirst)) + ((dst_positive_scale_prefix_previousentrycellfirst) + (dst_positive_scale_prefix_previousentrycellfirst))) + (((dst_negative_code_prefix_previousentrycellfirst) + (dst_negative_scale_prefix_previousentrycellfirst)) * S ((dst_negative_code_prefix_previousentrycellfirst) + (dst_negative_scale_prefix_previousentrycellfirst)) + ((dst_negative_scale_prefix_previousentrycellfirst) + (dst_negative_scale_prefix_previousentrycellfirst)))) + ((((dst_negative_code_prefix_previousentrycellfirst) + (dst_negative_scale_prefix_previousentrycellfirst)) * S ((dst_negative_code_prefix_previousentrycellfirst) + (dst_negative_scale_prefix_previousentrycellfirst)) + ((dst_negative_scale_prefix_previousentrycellfirst) + (dst_negative_scale_prefix_previousentrycellfirst))) + (((dst_negative_code_prefix_previousentrycellfirst) + (dst_negative_scale_prefix_previousentrycellfirst)) * S ((dst_negative_code_prefix_previousentrycellfirst) + (dst_negative_scale_prefix_previousentrycellfirst)) + ((dst_negative_scale_prefix_previousentrycellfirst) + (dst_negative_scale_prefix_previousentrycellfirst)))))) /\ (((((exists ff_h_pvs_prefix_previousentrycellfirstpositive. ff_h_pvs_prefix_previousentrycellfirstpositive + S (dst_positive_prefix_previousentrycellfirst) = S ((S (dfg_flat_row_prefix_previousentry)) * dst_positive_scale_prefix_previousentrycellfirst)) /\ exists ff_q_pvs_prefix_previousentrycellfirstpositive. dst_positive_code_prefix_previousentrycellfirst = ff_q_pvs_prefix_previousentrycellfirstpositive * S ((S (dfg_flat_row_prefix_previousentry)) * dst_positive_scale_prefix_previousentrycellfirst) + (dst_positive_prefix_previousentrycellfirst))) /\ (((((exists ff_h_pvs_prefix_previousentrycellfirstnegative. ff_h_pvs_prefix_previousentrycellfirstnegative + S (dst_negative_prefix_previousentrycellfirst) = S ((S (dfg_flat_row_prefix_previousentry)) * dst_negative_scale_prefix_previousentrycellfirst)) /\ exists ff_q_pvs_prefix_previousentrycellfirstnegative. dst_negative_code_prefix_previousentrycellfirst = ff_q_pvs_prefix_previousentrycellfirstnegative * S ((S (dfg_flat_row_prefix_previousentry)) * dst_negative_scale_prefix_previousentrycellfirst) + (dst_negative_prefix_previousentrycellfirst))) /\ (exists ge_balance_positive_prefix_previousentrycellfirstvalue ge_balance_negative_prefix_previousentrycellfirstvalue. (((((dfg_first_prefix_previousentrycell) = 2 * (ge_balance_positive_prefix_previousentrycellfirstvalue) /\ (ge_balance_negative_prefix_previousentrycellfirstvalue) = 0) \/ exists ge_signed_half_prefix_previousentrycellfirstvaluedecode. (((dfg_first_prefix_previousentrycell) = 2 * ge_signed_half_prefix_previousentrycellfirstvaluedecode + 1 /\ (ge_balance_positive_prefix_previousentrycellfirstvalue) = 0) /\ (ge_balance_negative_prefix_previousentrycellfirstvalue) = S ge_signed_half_prefix_previousentrycellfirstvaluedecode))) /\ ((dst_positive_prefix_previousentrycellfirst) + ge_balance_negative_prefix_previousentrycellfirstvalue = (dst_negative_prefix_previousentrycellfirst) + ge_balance_positive_prefix_previousentrycellfirstvalue))))))))) /\ (((exists dst_positive_code_prefix_previousentrycelllast dst_positive_scale_prefix_previousentrycelllast dst_negative_code_prefix_previousentrycelllast dst_negative_scale_prefix_previousentrycelllast dst_positive_prefix_previousentrycelllast dst_negative_prefix_previousentrycelllast. (((H) = (((((dst_positive_code_prefix_previousentrycelllast) + (dst_positive_scale_prefix_previousentrycelllast)) * S ((dst_positive_code_prefix_previousentrycelllast) + (dst_positive_scale_prefix_previousentrycelllast)) + ((dst_positive_scale_prefix_previousentrycelllast) + (dst_positive_scale_prefix_previousentrycelllast))) + (((dst_negative_code_prefix_previousentrycelllast) + (dst_negative_scale_prefix_previousentrycelllast)) * S ((dst_negative_code_prefix_previousentrycelllast) + (dst_negative_scale_prefix_previousentrycelllast)) + ((dst_negative_scale_prefix_previousentrycelllast) + (dst_negative_scale_prefix_previousentrycelllast)))) * S ((((dst_positive_code_prefix_previousentrycelllast) + (dst_positive_scale_prefix_previousentrycelllast)) * S ((dst_positive_code_prefix_previousentrycelllast) + (dst_positive_scale_prefix_previousentrycelllast)) + ((dst_positive_scale_prefix_previousentrycelllast) + (dst_positive_scale_prefix_previousentrycelllast))) + (((dst_negative_code_prefix_previousentrycelllast) + (dst_negative_scale_prefix_previousentrycelllast)) * S ((dst_negative_code_prefix_previousentrycelllast) + (dst_negative_scale_prefix_previousentrycelllast)) + ((dst_negative_scale_prefix_previousentrycelllast) + (dst_negative_scale_prefix_previousentrycelllast)))) + ((((dst_negative_code_prefix_previousentrycelllast) + (dst_negative_scale_prefix_previousentrycelllast)) * S ((dst_negative_code_prefix_previousentrycelllast) + (dst_negative_scale_prefix_previousentrycelllast)) + ((dst_negative_scale_prefix_previousentrycelllast) + (dst_negative_scale_prefix_previousentrycelllast))) + (((dst_negative_code_prefix_previousentrycelllast) + (dst_negative_scale_prefix_previousentrycelllast)) * S ((dst_negative_code_prefix_previousentrycelllast) + (dst_negative_scale_prefix_previousentrycelllast)) + ((dst_negative_scale_prefix_previousentrycelllast) + (dst_negative_scale_prefix_previousentrycelllast)))))) /\ (((((exists ff_h_pvs_prefix_previousentrycelllastpositive. ff_h_pvs_prefix_previousentrycelllastpositive + S (dst_positive_prefix_previousentrycelllast) = S ((S (dfg_flat_column_prefix_previousentry)) * dst_positive_scale_prefix_previousentrycelllast)) /\ exists ff_q_pvs_prefix_previousentrycelllastpositive. dst_positive_code_prefix_previousentrycelllast = ff_q_pvs_prefix_previousentrycelllastpositive * S ((S (dfg_flat_column_prefix_previousentry)) * dst_positive_scale_prefix_previousentrycelllast) + (dst_positive_prefix_previousentrycelllast))) /\ (((((exists ff_h_pvs_prefix_previousentrycelllastnegative. ff_h_pvs_prefix_previousentrycelllastnegative + S (dst_negative_prefix_previousentrycelllast) = S ((S (dfg_flat_column_prefix_previousentry)) * dst_negative_scale_prefix_previousentrycelllast)) /\ exists ff_q_pvs_prefix_previousentrycelllastnegative. dst_negative_code_prefix_previousentrycelllast = ff_q_pvs_prefix_previousentrycelllastnegative * S ((S (dfg_flat_column_prefix_previousentry)) * dst_negative_scale_prefix_previousentrycelllast) + (dst_negative_prefix_previousentrycelllast))) /\ (exists ge_balance_positive_prefix_previousentrycelllastvalue ge_balance_negative_prefix_previousentrycelllastvalue. (((((dfg_last_prefix_previousentrycell) = 2 * (ge_balance_positive_prefix_previousentrycelllastvalue) /\ (ge_balance_negative_prefix_previousentrycelllastvalue) = 0) \/ exists ge_signed_half_prefix_previousentrycelllastvaluedecode. (((dfg_last_prefix_previousentrycell) = 2 * ge_signed_half_prefix_previousentrycelllastvaluedecode + 1 /\ (ge_balance_positive_prefix_previousentrycelllastvalue) = 0) /\ (ge_balance_negative_prefix_previousentrycelllastvalue) = S ge_signed_half_prefix_previousentrycelllastvaluedecode))) /\ ((dst_positive_prefix_previousentrycelllast) + ge_balance_negative_prefix_previousentrycelllastvalue = (dst_negative_prefix_previousentrycelllast) + ge_balance_positive_prefix_previousentrycelllastvalue))))))))) /\ (((exists dst_positive_code_prefix_previousentrycellmiddle dst_positive_scale_prefix_previousentrycellmiddle dst_negative_code_prefix_previousentrycellmiddle dst_negative_scale_prefix_previousentrycellmiddle dst_positive_prefix_previousentrycellmiddle dst_negative_prefix_previousentrycellmiddle. (((G) = (((((dst_positive_code_prefix_previousentrycellmiddle) + (dst_positive_scale_prefix_previousentrycellmiddle)) * S ((dst_positive_code_prefix_previousentrycellmiddle) + (dst_positive_scale_prefix_previousentrycellmiddle)) + ((dst_positive_scale_prefix_previousentrycellmiddle) + (dst_positive_scale_prefix_previousentrycellmiddle))) + (((dst_negative_code_prefix_previousentrycellmiddle) + (dst_negative_scale_prefix_previousentrycellmiddle)) * S ((dst_negative_code_prefix_previousentrycellmiddle) + (dst_negative_scale_prefix_previousentrycellmiddle)) + ((dst_negative_scale_prefix_previousentrycellmiddle) + (dst_negative_scale_prefix_previousentrycellmiddle)))) * S ((((dst_positive_code_prefix_previousentrycellmiddle) + (dst_positive_scale_prefix_previousentrycellmiddle)) * S ((dst_positive_code_prefix_previousentrycellmiddle) + (dst_positive_scale_prefix_previousentrycellmiddle)) + ((dst_positive_scale_prefix_previousentrycellmiddle) + (dst_positive_scale_prefix_previousentrycellmiddle))) + (((dst_negative_code_prefix_previousentrycellmiddle) + (dst_negative_scale_prefix_previousentrycellmiddle)) * S ((dst_negative_code_prefix_previousentrycellmiddle) + (dst_negative_scale_prefix_previousentrycellmiddle)) + ((dst_negative_scale_prefix_previousentrycellmiddle) + (dst_negative_scale_prefix_previousentrycellmiddle)))) + ((((dst_negative_code_prefix_previousentrycellmiddle) + (dst_negative_scale_prefix_previousentrycellmiddle)) * S ((dst_negative_code_prefix_previousentrycellmiddle) + (dst_negative_scale_prefix_previousentrycellmiddle)) + ((dst_negative_scale_prefix_previousentrycellmiddle) + (dst_negative_scale_prefix_previousentrycellmiddle))) + (((dst_negative_code_prefix_previousentrycellmiddle) + (dst_negative_scale_prefix_previousentrycellmiddle)) * S ((dst_negative_code_prefix_previousentrycellmiddle) + (dst_negative_scale_prefix_previousentrycellmiddle)) + ((dst_negative_scale_prefix_previousentrycellmiddle) + (dst_negative_scale_prefix_previousentrycellmiddle)))))) /\ (((((exists ff_h_pvs_prefix_previousentrycellmiddlepositive. ff_h_pvs_prefix_previousentrycellmiddlepositive + S (dst_positive_prefix_previousentrycellmiddle) = S ((S (dfg_middle_prefix_previousentrycell)) * dst_positive_scale_prefix_previousentrycellmiddle)) /\ exists ff_q_pvs_prefix_previousentrycellmiddlepositive. dst_positive_code_prefix_previousentrycellmiddle = ff_q_pvs_prefix_previousentrycellmiddlepositive * S ((S (dfg_middle_prefix_previousentrycell)) * dst_positive_scale_prefix_previousentrycellmiddle) + (dst_positive_prefix_previousentrycellmiddle))) /\ (((((exists ff_h_pvs_prefix_previousentrycellmiddlenegative. ff_h_pvs_prefix_previousentrycellmiddlenegative + S (dst_negative_prefix_previousentrycellmiddle) = S ((S (dfg_middle_prefix_previousentrycell)) * dst_negative_scale_prefix_previousentrycellmiddle)) /\ exists ff_q_pvs_prefix_previousentrycellmiddlenegative. dst_negative_code_prefix_previousentrycellmiddle = ff_q_pvs_prefix_previousentrycellmiddlenegative * S ((S (dfg_middle_prefix_previousentrycell)) * dst_negative_scale_prefix_previousentrycellmiddle) + (dst_negative_prefix_previousentrycellmiddle))) /\ (exists ge_balance_positive_prefix_previousentrycellmiddlevalue ge_balance_negative_prefix_previousentrycellmiddlevalue. (((((dfg_value_prefix_previousentrycell) = 2 * (ge_balance_positive_prefix_previousentrycellmiddlevalue) /\ (ge_balance_negative_prefix_previousentrycellmiddlevalue) = 0) \/ exists ge_signed_half_prefix_previousentrycellmiddlevaluedecode. (((dfg_value_prefix_previousentrycell) = 2 * ge_signed_half_prefix_previousentrycellmiddlevaluedecode + 1 /\ (ge_balance_positive_prefix_previousentrycellmiddlevalue) = 0) /\ (ge_balance_negative_prefix_previousentrycellmiddlevalue) = S ge_signed_half_prefix_previousentrycellmiddlevaluedecode))) /\ ((dst_positive_prefix_previousentrycellmiddle) + ge_balance_negative_prefix_previousentrycellmiddlevalue = (dst_negative_prefix_previousentrycellmiddle) + ge_balance_positive_prefix_previousentrycellmiddlevalue))))))))) /\ (exists dfg_inner_prefix_previousentrycellproduct. ((exists sto_ap_prefix_previousentrycellproductinner sto_an_prefix_previousentrycellproductinner sto_bp_prefix_previousentrycellproductinner sto_bn_prefix_previousentrycellproductinner sto_cp_prefix_previousentrycellproductinner sto_cn_prefix_previousentrycellproductinner. (((((dfg_last_prefix_previousentrycell) = 2 * (sto_ap_prefix_previousentrycellproductinner) /\ (sto_an_prefix_previousentrycellproductinner) = 0) \/ exists ge_signed_half_prefix_previousentrycellproductinnerleft. (((dfg_last_prefix_previousentrycell) = 2 * ge_signed_half_prefix_previousentrycellproductinnerleft + 1 /\ (sto_ap_prefix_previousentrycellproductinner) = 0) /\ (sto_an_prefix_previousentrycellproductinner) = S ge_signed_half_prefix_previousentrycellproductinnerleft))) /\ ((((((dfg_value_prefix_previousentrycell) = 2 * (sto_bp_prefix_previousentrycellproductinner) /\ (sto_bn_prefix_previousentrycellproductinner) = 0) \/ exists ge_signed_half_prefix_previousentrycellproductinnerright. (((dfg_value_prefix_previousentrycell) = 2 * ge_signed_half_prefix_previousentrycellproductinnerright + 1 /\ (sto_bp_prefix_previousentrycellproductinner) = 0) /\ (sto_bn_prefix_previousentrycellproductinner) = S ge_signed_half_prefix_previousentrycellproductinnerright))) /\ ((((((dfg_inner_prefix_previousentrycellproduct) = 2 * (sto_cp_prefix_previousentrycellproductinner) /\ (sto_cn_prefix_previousentrycellproductinner) = 0) \/ exists ge_signed_half_prefix_previousentrycellproductinneroutput. (((dfg_inner_prefix_previousentrycellproduct) = 2 * ge_signed_half_prefix_previousentrycellproductinneroutput + 1 /\ (sto_cp_prefix_previousentrycellproductinner) = 0) /\ (sto_cn_prefix_previousentrycellproductinner) = S ge_signed_half_prefix_previousentrycellproductinneroutput))) /\ ((sto_ap_prefix_previousentrycellproductinner * sto_bp_prefix_previousentrycellproductinner + sto_an_prefix_previousentrycellproductinner * sto_bn_prefix_previousentrycellproductinner) + sto_cn_prefix_previousentrycellproductinner = (sto_ap_prefix_previousentrycellproductinner * sto_bn_prefix_previousentrycellproductinner + sto_an_prefix_previousentrycellproductinner * sto_bp_prefix_previousentrycellproductinner) + sto_cp_prefix_previousentrycellproductinner))))))) /\ (exists sto_ap_prefix_previousentrycellproductouter sto_an_prefix_previousentrycellproductouter sto_bp_prefix_previousentrycellproductouter sto_bn_prefix_previousentrycellproductouter sto_cp_prefix_previousentrycellproductouter sto_cn_prefix_previousentrycellproductouter. (((((dfg_first_prefix_previousentrycell) = 2 * (sto_ap_prefix_previousentrycellproductouter) /\ (sto_an_prefix_previousentrycellproductouter) = 0) \/ exists ge_signed_half_prefix_previousentrycellproductouterleft. (((dfg_first_prefix_previousentrycell) = 2 * ge_signed_half_prefix_previousentrycellproductouterleft + 1 /\ (sto_ap_prefix_previousentrycellproductouter) = 0) /\ (sto_an_prefix_previousentrycellproductouter) = S ge_signed_half_prefix_previousentrycellproductouterleft))) /\ ((((((dfg_inner_prefix_previousentrycellproduct) = 2 * (sto_bp_prefix_previousentrycellproductouter) /\ (sto_bn_prefix_previousentrycellproductouter) = 0) \/ exists ge_signed_half_prefix_previousentrycellproductouterright. (((dfg_inner_prefix_previousentrycellproduct) = 2 * ge_signed_half_prefix_previousentrycellproductouterright + 1 /\ (sto_bp_prefix_previousentrycellproductouter) = 0) /\ (sto_bn_prefix_previousentrycellproductouter) = S ge_signed_half_prefix_previousentrycellproductouterright))) /\ ((((((dfg_flat_value_prefix_previous) = 2 * (sto_cp_prefix_previousentrycellproductouter) /\ (sto_cn_prefix_previousentrycellproductouter) = 0) \/ exists ge_signed_half_prefix_previousentrycellproductouteroutput. (((dfg_flat_value_prefix_previous) = 2 * ge_signed_half_prefix_previousentrycellproductouteroutput + 1 /\ (sto_cp_prefix_previousentrycellproductouter) = 0) /\ (sto_cn_prefix_previousentrycellproductouter) = S ge_signed_half_prefix_previousentrycellproductouteroutput))) /\ ((sto_ap_prefix_previousentrycellproductouter * sto_bp_prefix_previousentrycellproductouter + sto_an_prefix_previousentrycellproductouter * sto_bn_prefix_previousentrycellproductouter) + sto_cn_prefix_previousentrycellproductouter = (sto_ap_prefix_previousentrycellproductouter * sto_bn_prefix_previousentrycellproductouter + sto_an_prefix_previousentrycellproductouter * sto_bp_prefix_previousentrycellproductouter) + sto_cp_prefix_previousentrycellproductouter))))))))))))))))))))) \/ ((((dfg_flat_row_prefix_previousentry)=0 \/ ((dfg_flat_column_prefix_previousentry)=0 \/ ~(exists pvs_factor_prefix_previousentrycellomittednondivisor. (n) = ((dfg_flat_row_prefix_previousentry)*(dfg_flat_column_prefix_previousentry)) * pvs_factor_prefix_previousentrycellomittednondivisor))) /\ ((dfg_flat_value_prefix_previous)=0))))))))))) - 0041
apply IH - 0042
exact hF - 0043
exact hG - 0044
exact hH - 0045
cases hp - 0046
have hv : exists z. (exists dfg_flat_row_prefix_next_value dfg_flat_column_prefix_next_value. (((S l)=((S (n))*(dfg_flat_row_prefix_next_value)+(dfg_flat_column_prefix_next_value))) /\ (((exists pvs_gap_prefix_next_valueremainder. pvs_gap_prefix_next_valueremainder + S (dfg_flat_column_prefix_next_value) = (S (n))) /\ ((((~((dfg_flat_row_prefix_next_value)=0)) /\ (((~((dfg_flat_column_prefix_next_value)=0)) /\ (exists dfg_middle_prefix_next_valuecell dfg_first_prefix_next_valuecell dfg_last_prefix_next_valuecell dfg_value_prefix_next_valuecell. (((n)=((dfg_flat_row_prefix_next_value)*(dfg_flat_column_prefix_next_value))*dfg_middle_prefix_next_valuecell) /\ (((exists dst_positive_code_prefix_next_valuecellfirst dst_positive_scale_prefix_next_valuecellfirst dst_negative_code_prefix_next_valuecellfirst dst_negative_scale_prefix_next_valuecellfirst dst_positive_prefix_next_valuecellfirst dst_negative_prefix_next_valuecellfirst. (((F) = (((((dst_positive_code_prefix_next_valuecellfirst) + (dst_positive_scale_prefix_next_valuecellfirst)) * S ((dst_positive_code_prefix_next_valuecellfirst) + (dst_positive_scale_prefix_next_valuecellfirst)) + ((dst_positive_scale_prefix_next_valuecellfirst) + (dst_positive_scale_prefix_next_valuecellfirst))) + (((dst_negative_code_prefix_next_valuecellfirst) + (dst_negative_scale_prefix_next_valuecellfirst)) * S ((dst_negative_code_prefix_next_valuecellfirst) + (dst_negative_scale_prefix_next_valuecellfirst)) + ((dst_negative_scale_prefix_next_valuecellfirst) + (dst_negative_scale_prefix_next_valuecellfirst)))) * S ((((dst_positive_code_prefix_next_valuecellfirst) + (dst_positive_scale_prefix_next_valuecellfirst)) * S ((dst_positive_code_prefix_next_valuecellfirst) + (dst_positive_scale_prefix_next_valuecellfirst)) + ((dst_positive_scale_prefix_next_valuecellfirst) + (dst_positive_scale_prefix_next_valuecellfirst))) + (((dst_negative_code_prefix_next_valuecellfirst) + (dst_negative_scale_prefix_next_valuecellfirst)) * S ((dst_negative_code_prefix_next_valuecellfirst) + (dst_negative_scale_prefix_next_valuecellfirst)) + ((dst_negative_scale_prefix_next_valuecellfirst) + (dst_negative_scale_prefix_next_valuecellfirst)))) + ((((dst_negative_code_prefix_next_valuecellfirst) + (dst_negative_scale_prefix_next_valuecellfirst)) * S ((dst_negative_code_prefix_next_valuecellfirst) + (dst_negative_scale_prefix_next_valuecellfirst)) + ((dst_negative_scale_prefix_next_valuecellfirst) + (dst_negative_scale_prefix_next_valuecellfirst))) + (((dst_negative_code_prefix_next_valuecellfirst) + (dst_negative_scale_prefix_next_valuecellfirst)) * S ((dst_negative_code_prefix_next_valuecellfirst) + (dst_negative_scale_prefix_next_valuecellfirst)) + ((dst_negative_scale_prefix_next_valuecellfirst) + (dst_negative_scale_prefix_next_valuecellfirst)))))) /\ (((((exists ff_h_pvs_prefix_next_valuecellfirstpositive. ff_h_pvs_prefix_next_valuecellfirstpositive + S (dst_positive_prefix_next_valuecellfirst) = S ((S (dfg_flat_row_prefix_next_value)) * dst_positive_scale_prefix_next_valuecellfirst)) /\ exists ff_q_pvs_prefix_next_valuecellfirstpositive. dst_positive_code_prefix_next_valuecellfirst = ff_q_pvs_prefix_next_valuecellfirstpositive * S ((S (dfg_flat_row_prefix_next_value)) * dst_positive_scale_prefix_next_valuecellfirst) + (dst_positive_prefix_next_valuecellfirst))) /\ (((((exists ff_h_pvs_prefix_next_valuecellfirstnegative. ff_h_pvs_prefix_next_valuecellfirstnegative + S (dst_negative_prefix_next_valuecellfirst) = S ((S (dfg_flat_row_prefix_next_value)) * dst_negative_scale_prefix_next_valuecellfirst)) /\ exists ff_q_pvs_prefix_next_valuecellfirstnegative. dst_negative_code_prefix_next_valuecellfirst = ff_q_pvs_prefix_next_valuecellfirstnegative * S ((S (dfg_flat_row_prefix_next_value)) * dst_negative_scale_prefix_next_valuecellfirst) + (dst_negative_prefix_next_valuecellfirst))) /\ (exists ge_balance_positive_prefix_next_valuecellfirstvalue ge_balance_negative_prefix_next_valuecellfirstvalue. (((((dfg_first_prefix_next_valuecell) = 2 * (ge_balance_positive_prefix_next_valuecellfirstvalue) /\ (ge_balance_negative_prefix_next_valuecellfirstvalue) = 0) \/ exists ge_signed_half_prefix_next_valuecellfirstvaluedecode. (((dfg_first_prefix_next_valuecell) = 2 * ge_signed_half_prefix_next_valuecellfirstvaluedecode + 1 /\ (ge_balance_positive_prefix_next_valuecellfirstvalue) = 0) /\ (ge_balance_negative_prefix_next_valuecellfirstvalue) = S ge_signed_half_prefix_next_valuecellfirstvaluedecode))) /\ ((dst_positive_prefix_next_valuecellfirst) + ge_balance_negative_prefix_next_valuecellfirstvalue = (dst_negative_prefix_next_valuecellfirst) + ge_balance_positive_prefix_next_valuecellfirstvalue))))))))) /\ (((exists dst_positive_code_prefix_next_valuecelllast dst_positive_scale_prefix_next_valuecelllast dst_negative_code_prefix_next_valuecelllast dst_negative_scale_prefix_next_valuecelllast dst_positive_prefix_next_valuecelllast dst_negative_prefix_next_valuecelllast. (((H) = (((((dst_positive_code_prefix_next_valuecelllast) + (dst_positive_scale_prefix_next_valuecelllast)) * S ((dst_positive_code_prefix_next_valuecelllast) + (dst_positive_scale_prefix_next_valuecelllast)) + ((dst_positive_scale_prefix_next_valuecelllast) + (dst_positive_scale_prefix_next_valuecelllast))) + (((dst_negative_code_prefix_next_valuecelllast) + (dst_negative_scale_prefix_next_valuecelllast)) * S ((dst_negative_code_prefix_next_valuecelllast) + (dst_negative_scale_prefix_next_valuecelllast)) + ((dst_negative_scale_prefix_next_valuecelllast) + (dst_negative_scale_prefix_next_valuecelllast)))) * S ((((dst_positive_code_prefix_next_valuecelllast) + (dst_positive_scale_prefix_next_valuecelllast)) * S ((dst_positive_code_prefix_next_valuecelllast) + (dst_positive_scale_prefix_next_valuecelllast)) + ((dst_positive_scale_prefix_next_valuecelllast) + (dst_positive_scale_prefix_next_valuecelllast))) + (((dst_negative_code_prefix_next_valuecelllast) + (dst_negative_scale_prefix_next_valuecelllast)) * S ((dst_negative_code_prefix_next_valuecelllast) + (dst_negative_scale_prefix_next_valuecelllast)) + ((dst_negative_scale_prefix_next_valuecelllast) + (dst_negative_scale_prefix_next_valuecelllast)))) + ((((dst_negative_code_prefix_next_valuecelllast) + (dst_negative_scale_prefix_next_valuecelllast)) * S ((dst_negative_code_prefix_next_valuecelllast) + (dst_negative_scale_prefix_next_valuecelllast)) + ((dst_negative_scale_prefix_next_valuecelllast) + (dst_negative_scale_prefix_next_valuecelllast))) + (((dst_negative_code_prefix_next_valuecelllast) + (dst_negative_scale_prefix_next_valuecelllast)) * S ((dst_negative_code_prefix_next_valuecelllast) + (dst_negative_scale_prefix_next_valuecelllast)) + ((dst_negative_scale_prefix_next_valuecelllast) + (dst_negative_scale_prefix_next_valuecelllast)))))) /\ (((((exists ff_h_pvs_prefix_next_valuecelllastpositive. ff_h_pvs_prefix_next_valuecelllastpositive + S (dst_positive_prefix_next_valuecelllast) = S ((S (dfg_flat_column_prefix_next_value)) * dst_positive_scale_prefix_next_valuecelllast)) /\ exists ff_q_pvs_prefix_next_valuecelllastpositive. dst_positive_code_prefix_next_valuecelllast = ff_q_pvs_prefix_next_valuecelllastpositive * S ((S (dfg_flat_column_prefix_next_value)) * dst_positive_scale_prefix_next_valuecelllast) + (dst_positive_prefix_next_valuecelllast))) /\ (((((exists ff_h_pvs_prefix_next_valuecelllastnegative. ff_h_pvs_prefix_next_valuecelllastnegative + S (dst_negative_prefix_next_valuecelllast) = S ((S (dfg_flat_column_prefix_next_value)) * dst_negative_scale_prefix_next_valuecelllast)) /\ exists ff_q_pvs_prefix_next_valuecelllastnegative. dst_negative_code_prefix_next_valuecelllast = ff_q_pvs_prefix_next_valuecelllastnegative * S ((S (dfg_flat_column_prefix_next_value)) * dst_negative_scale_prefix_next_valuecelllast) + (dst_negative_prefix_next_valuecelllast))) /\ (exists ge_balance_positive_prefix_next_valuecelllastvalue ge_balance_negative_prefix_next_valuecelllastvalue. (((((dfg_last_prefix_next_valuecell) = 2 * (ge_balance_positive_prefix_next_valuecelllastvalue) /\ (ge_balance_negative_prefix_next_valuecelllastvalue) = 0) \/ exists ge_signed_half_prefix_next_valuecelllastvaluedecode. (((dfg_last_prefix_next_valuecell) = 2 * ge_signed_half_prefix_next_valuecelllastvaluedecode + 1 /\ (ge_balance_positive_prefix_next_valuecelllastvalue) = 0) /\ (ge_balance_negative_prefix_next_valuecelllastvalue) = S ge_signed_half_prefix_next_valuecelllastvaluedecode))) /\ ((dst_positive_prefix_next_valuecelllast) + ge_balance_negative_prefix_next_valuecelllastvalue = (dst_negative_prefix_next_valuecelllast) + ge_balance_positive_prefix_next_valuecelllastvalue))))))))) /\ (((exists dst_positive_code_prefix_next_valuecellmiddle dst_positive_scale_prefix_next_valuecellmiddle dst_negative_code_prefix_next_valuecellmiddle dst_negative_scale_prefix_next_valuecellmiddle dst_positive_prefix_next_valuecellmiddle dst_negative_prefix_next_valuecellmiddle. (((G) = (((((dst_positive_code_prefix_next_valuecellmiddle) + (dst_positive_scale_prefix_next_valuecellmiddle)) * S ((dst_positive_code_prefix_next_valuecellmiddle) + (dst_positive_scale_prefix_next_valuecellmiddle)) + ((dst_positive_scale_prefix_next_valuecellmiddle) + (dst_positive_scale_prefix_next_valuecellmiddle))) + (((dst_negative_code_prefix_next_valuecellmiddle) + (dst_negative_scale_prefix_next_valuecellmiddle)) * S ((dst_negative_code_prefix_next_valuecellmiddle) + (dst_negative_scale_prefix_next_valuecellmiddle)) + ((dst_negative_scale_prefix_next_valuecellmiddle) + (dst_negative_scale_prefix_next_valuecellmiddle)))) * S ((((dst_positive_code_prefix_next_valuecellmiddle) + (dst_positive_scale_prefix_next_valuecellmiddle)) * S ((dst_positive_code_prefix_next_valuecellmiddle) + (dst_positive_scale_prefix_next_valuecellmiddle)) + ((dst_positive_scale_prefix_next_valuecellmiddle) + (dst_positive_scale_prefix_next_valuecellmiddle))) + (((dst_negative_code_prefix_next_valuecellmiddle) + (dst_negative_scale_prefix_next_valuecellmiddle)) * S ((dst_negative_code_prefix_next_valuecellmiddle) + (dst_negative_scale_prefix_next_valuecellmiddle)) + ((dst_negative_scale_prefix_next_valuecellmiddle) + (dst_negative_scale_prefix_next_valuecellmiddle)))) + ((((dst_negative_code_prefix_next_valuecellmiddle) + (dst_negative_scale_prefix_next_valuecellmiddle)) * S ((dst_negative_code_prefix_next_valuecellmiddle) + (dst_negative_scale_prefix_next_valuecellmiddle)) + ((dst_negative_scale_prefix_next_valuecellmiddle) + (dst_negative_scale_prefix_next_valuecellmiddle))) + (((dst_negative_code_prefix_next_valuecellmiddle) + (dst_negative_scale_prefix_next_valuecellmiddle)) * S ((dst_negative_code_prefix_next_valuecellmiddle) + (dst_negative_scale_prefix_next_valuecellmiddle)) + ((dst_negative_scale_prefix_next_valuecellmiddle) + (dst_negative_scale_prefix_next_valuecellmiddle)))))) /\ (((((exists ff_h_pvs_prefix_next_valuecellmiddlepositive. ff_h_pvs_prefix_next_valuecellmiddlepositive + S (dst_positive_prefix_next_valuecellmiddle) = S ((S (dfg_middle_prefix_next_valuecell)) * dst_positive_scale_prefix_next_valuecellmiddle)) /\ exists ff_q_pvs_prefix_next_valuecellmiddlepositive. dst_positive_code_prefix_next_valuecellmiddle = ff_q_pvs_prefix_next_valuecellmiddlepositive * S ((S (dfg_middle_prefix_next_valuecell)) * dst_positive_scale_prefix_next_valuecellmiddle) + (dst_positive_prefix_next_valuecellmiddle))) /\ (((((exists ff_h_pvs_prefix_next_valuecellmiddlenegative. ff_h_pvs_prefix_next_valuecellmiddlenegative + S (dst_negative_prefix_next_valuecellmiddle) = S ((S (dfg_middle_prefix_next_valuecell)) * dst_negative_scale_prefix_next_valuecellmiddle)) /\ exists ff_q_pvs_prefix_next_valuecellmiddlenegative. dst_negative_code_prefix_next_valuecellmiddle = ff_q_pvs_prefix_next_valuecellmiddlenegative * S ((S (dfg_middle_prefix_next_valuecell)) * dst_negative_scale_prefix_next_valuecellmiddle) + (dst_negative_prefix_next_valuecellmiddle))) /\ (exists ge_balance_positive_prefix_next_valuecellmiddlevalue ge_balance_negative_prefix_next_valuecellmiddlevalue. (((((dfg_value_prefix_next_valuecell) = 2 * (ge_balance_positive_prefix_next_valuecellmiddlevalue) /\ (ge_balance_negative_prefix_next_valuecellmiddlevalue) = 0) \/ exists ge_signed_half_prefix_next_valuecellmiddlevaluedecode. (((dfg_value_prefix_next_valuecell) = 2 * ge_signed_half_prefix_next_valuecellmiddlevaluedecode + 1 /\ (ge_balance_positive_prefix_next_valuecellmiddlevalue) = 0) /\ (ge_balance_negative_prefix_next_valuecellmiddlevalue) = S ge_signed_half_prefix_next_valuecellmiddlevaluedecode))) /\ ((dst_positive_prefix_next_valuecellmiddle) + ge_balance_negative_prefix_next_valuecellmiddlevalue = (dst_negative_prefix_next_valuecellmiddle) + ge_balance_positive_prefix_next_valuecellmiddlevalue))))))))) /\ (exists dfg_inner_prefix_next_valuecellproduct. ((exists sto_ap_prefix_next_valuecellproductinner sto_an_prefix_next_valuecellproductinner sto_bp_prefix_next_valuecellproductinner sto_bn_prefix_next_valuecellproductinner sto_cp_prefix_next_valuecellproductinner sto_cn_prefix_next_valuecellproductinner. (((((dfg_last_prefix_next_valuecell) = 2 * (sto_ap_prefix_next_valuecellproductinner) /\ (sto_an_prefix_next_valuecellproductinner) = 0) \/ exists ge_signed_half_prefix_next_valuecellproductinnerleft. (((dfg_last_prefix_next_valuecell) = 2 * ge_signed_half_prefix_next_valuecellproductinnerleft + 1 /\ (sto_ap_prefix_next_valuecellproductinner) = 0) /\ (sto_an_prefix_next_valuecellproductinner) = S ge_signed_half_prefix_next_valuecellproductinnerleft))) /\ ((((((dfg_value_prefix_next_valuecell) = 2 * (sto_bp_prefix_next_valuecellproductinner) /\ (sto_bn_prefix_next_valuecellproductinner) = 0) \/ exists ge_signed_half_prefix_next_valuecellproductinnerright. (((dfg_value_prefix_next_valuecell) = 2 * ge_signed_half_prefix_next_valuecellproductinnerright + 1 /\ (sto_bp_prefix_next_valuecellproductinner) = 0) /\ (sto_bn_prefix_next_valuecellproductinner) = S ge_signed_half_prefix_next_valuecellproductinnerright))) /\ ((((((dfg_inner_prefix_next_valuecellproduct) = 2 * (sto_cp_prefix_next_valuecellproductinner) /\ (sto_cn_prefix_next_valuecellproductinner) = 0) \/ exists ge_signed_half_prefix_next_valuecellproductinneroutput. (((dfg_inner_prefix_next_valuecellproduct) = 2 * ge_signed_half_prefix_next_valuecellproductinneroutput + 1 /\ (sto_cp_prefix_next_valuecellproductinner) = 0) /\ (sto_cn_prefix_next_valuecellproductinner) = S ge_signed_half_prefix_next_valuecellproductinneroutput))) /\ ((sto_ap_prefix_next_valuecellproductinner * sto_bp_prefix_next_valuecellproductinner + sto_an_prefix_next_valuecellproductinner * sto_bn_prefix_next_valuecellproductinner) + sto_cn_prefix_next_valuecellproductinner = (sto_ap_prefix_next_valuecellproductinner * sto_bn_prefix_next_valuecellproductinner + sto_an_prefix_next_valuecellproductinner * sto_bp_prefix_next_valuecellproductinner) + sto_cp_prefix_next_valuecellproductinner))))))) /\ (exists sto_ap_prefix_next_valuecellproductouter sto_an_prefix_next_valuecellproductouter sto_bp_prefix_next_valuecellproductouter sto_bn_prefix_next_valuecellproductouter sto_cp_prefix_next_valuecellproductouter sto_cn_prefix_next_valuecellproductouter. (((((dfg_first_prefix_next_valuecell) = 2 * (sto_ap_prefix_next_valuecellproductouter) /\ (sto_an_prefix_next_valuecellproductouter) = 0) \/ exists ge_signed_half_prefix_next_valuecellproductouterleft. (((dfg_first_prefix_next_valuecell) = 2 * ge_signed_half_prefix_next_valuecellproductouterleft + 1 /\ (sto_ap_prefix_next_valuecellproductouter) = 0) /\ (sto_an_prefix_next_valuecellproductouter) = S ge_signed_half_prefix_next_valuecellproductouterleft))) /\ ((((((dfg_inner_prefix_next_valuecellproduct) = 2 * (sto_bp_prefix_next_valuecellproductouter) /\ (sto_bn_prefix_next_valuecellproductouter) = 0) \/ exists ge_signed_half_prefix_next_valuecellproductouterright. (((dfg_inner_prefix_next_valuecellproduct) = 2 * ge_signed_half_prefix_next_valuecellproductouterright + 1 /\ (sto_bp_prefix_next_valuecellproductouter) = 0) /\ (sto_bn_prefix_next_valuecellproductouter) = S ge_signed_half_prefix_next_valuecellproductouterright))) /\ ((((((z) = 2 * (sto_cp_prefix_next_valuecellproductouter) /\ (sto_cn_prefix_next_valuecellproductouter) = 0) \/ exists ge_signed_half_prefix_next_valuecellproductouteroutput. (((z) = 2 * ge_signed_half_prefix_next_valuecellproductouteroutput + 1 /\ (sto_cp_prefix_next_valuecellproductouter) = 0) /\ (sto_cn_prefix_next_valuecellproductouter) = S ge_signed_half_prefix_next_valuecellproductouteroutput))) /\ ((sto_ap_prefix_next_valuecellproductouter * sto_bp_prefix_next_valuecellproductouter + sto_an_prefix_next_valuecellproductouter * sto_bn_prefix_next_valuecellproductouter) + sto_cn_prefix_next_valuecellproductouter = (sto_ap_prefix_next_valuecellproductouter * sto_bn_prefix_next_valuecellproductouter + sto_an_prefix_next_valuecellproductouter * sto_bp_prefix_next_valuecellproductouter) + sto_cp_prefix_next_valuecellproductouter))))))))))))))))))))) \/ ((((dfg_flat_row_prefix_next_value)=0 \/ ((dfg_flat_column_prefix_next_value)=0 \/ ~(exists pvs_factor_prefix_next_valuecellomittednondivisor. (n) = ((dfg_flat_row_prefix_next_value)*(dfg_flat_column_prefix_next_value)) * pvs_factor_prefix_next_valuecellomittednondivisor))) /\ ((z)=0)))))))) - 0047
specialize dirichlet_grid_flat_entry_exists (F) - 0048
specialize dirichlet_grid_flat_entry_exists (G) - 0049
specialize dirichlet_grid_flat_entry_exists (H) - 0050
specialize dirichlet_grid_flat_entry_exists (n) - 0051
specialize dirichlet_grid_flat_entry_exists (S l) - 0052
apply dirichlet_grid_flat_entry_exists - 0053
exact hF - 0054
exact hG - 0055
exact hH - 0056
cases hv - 0057
have hext : exists U. (((((exists dst_positive_code_prefix_nexttable dst_positive_scale_prefix_nexttable dst_negative_code_prefix_nexttable dst_negative_scale_prefix_nexttable. (((U) = (((((dst_positive_code_prefix_nexttable) + (dst_positive_scale_prefix_nexttable)) * S ((dst_positive_code_prefix_nexttable) + (dst_positive_scale_prefix_nexttable)) + ((dst_positive_scale_prefix_nexttable) + (dst_positive_scale_prefix_nexttable))) + (((dst_negative_code_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)) * S ((dst_negative_code_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)) + ((dst_negative_scale_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)))) * S ((((dst_positive_code_prefix_nexttable) + (dst_positive_scale_prefix_nexttable)) * S ((dst_positive_code_prefix_nexttable) + (dst_positive_scale_prefix_nexttable)) + ((dst_positive_scale_prefix_nexttable) + (dst_positive_scale_prefix_nexttable))) + (((dst_negative_code_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)) * S ((dst_negative_code_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)) + ((dst_negative_scale_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)))) + ((((dst_negative_code_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)) * S ((dst_negative_code_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)) + ((dst_negative_scale_prefix_nexttable) + (dst_negative_scale_prefix_nexttable))) + (((dst_negative_code_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)) * S ((dst_negative_code_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)) + ((dst_negative_scale_prefix_nexttable) + (dst_negative_scale_prefix_nexttable)))))) /\ (forall dst_index_prefix_nexttable. (exists pvs_le_gap_prefix_nexttabledomain. pvs_le_gap_prefix_nexttabledomain + (dst_index_prefix_nexttable) = (S l)) -> exists dst_positive_prefix_nexttable dst_negative_prefix_nexttable dst_value_prefix_nexttable. ((((exists ff_h_pvs_prefix_nexttableentrypositive. ff_h_pvs_prefix_nexttableentrypositive + S (dst_positive_prefix_nexttable) = S ((S (dst_index_prefix_nexttable)) * dst_positive_scale_prefix_nexttable)) /\ exists ff_q_pvs_prefix_nexttableentrypositive. dst_positive_code_prefix_nexttable = ff_q_pvs_prefix_nexttableentrypositive * S ((S (dst_index_prefix_nexttable)) * dst_positive_scale_prefix_nexttable) + (dst_positive_prefix_nexttable))) /\ (((((exists ff_h_pvs_prefix_nexttableentrynegative. ff_h_pvs_prefix_nexttableentrynegative + S (dst_negative_prefix_nexttable) = S ((S (dst_index_prefix_nexttable)) * dst_negative_scale_prefix_nexttable)) /\ exists ff_q_pvs_prefix_nexttableentrynegative. dst_negative_code_prefix_nexttable = ff_q_pvs_prefix_nexttableentrynegative * S ((S (dst_index_prefix_nexttable)) * dst_negative_scale_prefix_nexttable) + (dst_negative_prefix_nexttable))) /\ (exists ge_balance_positive_prefix_nexttableentryvalue ge_balance_negative_prefix_nexttableentryvalue. (((((dst_value_prefix_nexttable) = 2 * (ge_balance_positive_prefix_nexttableentryvalue) /\ (ge_balance_negative_prefix_nexttableentryvalue) = 0) \/ exists ge_signed_half_prefix_nexttableentryvaluedecode. (((dst_value_prefix_nexttable) = 2 * ge_signed_half_prefix_nexttableentryvaluedecode + 1 /\ (ge_balance_positive_prefix_nexttableentryvalue) = 0) /\ (ge_balance_negative_prefix_nexttableentryvalue) = S ge_signed_half_prefix_nexttableentryvaluedecode))) /\ ((dst_positive_prefix_nexttable) + ge_balance_negative_prefix_nexttableentryvalue = (dst_negative_prefix_nexttable) + ge_balance_positive_prefix_nexttableentryvalue))))))))) /\ (forall dfg_flat_index_prefix_next dfg_flat_value_prefix_next. (exists pvs_le_gap_prefix_nextbound. pvs_le_gap_prefix_nextbound + (dfg_flat_index_prefix_next) = (S l)) -> (exists dst_positive_code_prefix_nextlookup dst_positive_scale_prefix_nextlookup dst_negative_code_prefix_nextlookup dst_negative_scale_prefix_nextlookup dst_positive_prefix_nextlookup dst_negative_prefix_nextlookup. (((U) = (((((dst_positive_code_prefix_nextlookup) + (dst_positive_scale_prefix_nextlookup)) * S ((dst_positive_code_prefix_nextlookup) + (dst_positive_scale_prefix_nextlookup)) + ((dst_positive_scale_prefix_nextlookup) + (dst_positive_scale_prefix_nextlookup))) + (((dst_negative_code_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)) * S ((dst_negative_code_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)) + ((dst_negative_scale_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)))) * S ((((dst_positive_code_prefix_nextlookup) + (dst_positive_scale_prefix_nextlookup)) * S ((dst_positive_code_prefix_nextlookup) + (dst_positive_scale_prefix_nextlookup)) + ((dst_positive_scale_prefix_nextlookup) + (dst_positive_scale_prefix_nextlookup))) + (((dst_negative_code_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)) * S ((dst_negative_code_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)) + ((dst_negative_scale_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)))) + ((((dst_negative_code_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)) * S ((dst_negative_code_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)) + ((dst_negative_scale_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup))) + (((dst_negative_code_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)) * S ((dst_negative_code_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)) + ((dst_negative_scale_prefix_nextlookup) + (dst_negative_scale_prefix_nextlookup)))))) /\ (((((exists ff_h_pvs_prefix_nextlookuppositive. ff_h_pvs_prefix_nextlookuppositive + S (dst_positive_prefix_nextlookup) = S ((S (dfg_flat_index_prefix_next)) * dst_positive_scale_prefix_nextlookup)) /\ exists ff_q_pvs_prefix_nextlookuppositive. dst_positive_code_prefix_nextlookup = ff_q_pvs_prefix_nextlookuppositive * S ((S (dfg_flat_index_prefix_next)) * dst_positive_scale_prefix_nextlookup) + (dst_positive_prefix_nextlookup))) /\ (((((exists ff_h_pvs_prefix_nextlookupnegative. ff_h_pvs_prefix_nextlookupnegative + S (dst_negative_prefix_nextlookup) = S ((S (dfg_flat_index_prefix_next)) * dst_negative_scale_prefix_nextlookup)) /\ exists ff_q_pvs_prefix_nextlookupnegative. dst_negative_code_prefix_nextlookup = ff_q_pvs_prefix_nextlookupnegative * S ((S (dfg_flat_index_prefix_next)) * dst_negative_scale_prefix_nextlookup) + (dst_negative_prefix_nextlookup))) /\ (exists ge_balance_positive_prefix_nextlookupvalue ge_balance_negative_prefix_nextlookupvalue. (((((dfg_flat_value_prefix_next) = 2 * (ge_balance_positive_prefix_nextlookupvalue) /\ (ge_balance_negative_prefix_nextlookupvalue) = 0) \/ exists ge_signed_half_prefix_nextlookupvaluedecode. (((dfg_flat_value_prefix_next) = 2 * ge_signed_half_prefix_nextlookupvaluedecode + 1 /\ (ge_balance_positive_prefix_nextlookupvalue) = 0) /\ (ge_balance_negative_prefix_nextlookupvalue) = S ge_signed_half_prefix_nextlookupvaluedecode))) /\ ((dst_positive_prefix_nextlookup) + ge_balance_negative_prefix_nextlookupvalue = (dst_negative_prefix_nextlookup) + ge_balance_positive_prefix_nextlookupvalue))))))))) -> (exists dfg_flat_row_prefix_nextentry dfg_flat_column_prefix_nextentry. (((dfg_flat_index_prefix_next)=((S (n))*(dfg_flat_row_prefix_nextentry)+(dfg_flat_column_prefix_nextentry))) /\ (((exists pvs_gap_prefix_nextentryremainder. pvs_gap_prefix_nextentryremainder + S (dfg_flat_column_prefix_nextentry) = (S (n))) /\ ((((~((dfg_flat_row_prefix_nextentry)=0)) /\ (((~((dfg_flat_column_prefix_nextentry)=0)) /\ (exists dfg_middle_prefix_nextentrycell dfg_first_prefix_nextentrycell dfg_last_prefix_nextentrycell dfg_value_prefix_nextentrycell. (((n)=((dfg_flat_row_prefix_nextentry)*(dfg_flat_column_prefix_nextentry))*dfg_middle_prefix_nextentrycell) /\ (((exists dst_positive_code_prefix_nextentrycellfirst dst_positive_scale_prefix_nextentrycellfirst dst_negative_code_prefix_nextentrycellfirst dst_negative_scale_prefix_nextentrycellfirst dst_positive_prefix_nextentrycellfirst dst_negative_prefix_nextentrycellfirst. (((F) = (((((dst_positive_code_prefix_nextentrycellfirst) + (dst_positive_scale_prefix_nextentrycellfirst)) * S ((dst_positive_code_prefix_nextentrycellfirst) + (dst_positive_scale_prefix_nextentrycellfirst)) + ((dst_positive_scale_prefix_nextentrycellfirst) + (dst_positive_scale_prefix_nextentrycellfirst))) + (((dst_negative_code_prefix_nextentrycellfirst) + (dst_negative_scale_prefix_nextentrycellfirst)) * S ((dst_negative_code_prefix_nextentrycellfirst) + (dst_negative_scale_prefix_nextentrycellfirst)) + ((dst_negative_scale_prefix_nextentrycellfirst) + (dst_negative_scale_prefix_nextentrycellfirst)))) * S ((((dst_positive_code_prefix_nextentrycellfirst) + (dst_positive_scale_prefix_nextentrycellfirst)) * S ((dst_positive_code_prefix_nextentrycellfirst) + (dst_positive_scale_prefix_nextentrycellfirst)) + ((dst_positive_scale_prefix_nextentrycellfirst) + (dst_positive_scale_prefix_nextentrycellfirst))) + (((dst_negative_code_prefix_nextentrycellfirst) + (dst_negative_scale_prefix_nextentrycellfirst)) * S ((dst_negative_code_prefix_nextentrycellfirst) + (dst_negative_scale_prefix_nextentrycellfirst)) + ((dst_negative_scale_prefix_nextentrycellfirst) + (dst_negative_scale_prefix_nextentrycellfirst)))) + ((((dst_negative_code_prefix_nextentrycellfirst) + (dst_negative_scale_prefix_nextentrycellfirst)) * S ((dst_negative_code_prefix_nextentrycellfirst) + (dst_negative_scale_prefix_nextentrycellfirst)) + ((dst_negative_scale_prefix_nextentrycellfirst) + (dst_negative_scale_prefix_nextentrycellfirst))) + (((dst_negative_code_prefix_nextentrycellfirst) + (dst_negative_scale_prefix_nextentrycellfirst)) * S ((dst_negative_code_prefix_nextentrycellfirst) + (dst_negative_scale_prefix_nextentrycellfirst)) + ((dst_negative_scale_prefix_nextentrycellfirst) + (dst_negative_scale_prefix_nextentrycellfirst)))))) /\ (((((exists ff_h_pvs_prefix_nextentrycellfirstpositive. ff_h_pvs_prefix_nextentrycellfirstpositive + S (dst_positive_prefix_nextentrycellfirst) = S ((S (dfg_flat_row_prefix_nextentry)) * dst_positive_scale_prefix_nextentrycellfirst)) /\ exists ff_q_pvs_prefix_nextentrycellfirstpositive. dst_positive_code_prefix_nextentrycellfirst = ff_q_pvs_prefix_nextentrycellfirstpositive * S ((S (dfg_flat_row_prefix_nextentry)) * dst_positive_scale_prefix_nextentrycellfirst) + (dst_positive_prefix_nextentrycellfirst))) /\ (((((exists ff_h_pvs_prefix_nextentrycellfirstnegative. ff_h_pvs_prefix_nextentrycellfirstnegative + S (dst_negative_prefix_nextentrycellfirst) = S ((S (dfg_flat_row_prefix_nextentry)) * dst_negative_scale_prefix_nextentrycellfirst)) /\ exists ff_q_pvs_prefix_nextentrycellfirstnegative. dst_negative_code_prefix_nextentrycellfirst = ff_q_pvs_prefix_nextentrycellfirstnegative * S ((S (dfg_flat_row_prefix_nextentry)) * dst_negative_scale_prefix_nextentrycellfirst) + (dst_negative_prefix_nextentrycellfirst))) /\ (exists ge_balance_positive_prefix_nextentrycellfirstvalue ge_balance_negative_prefix_nextentrycellfirstvalue. (((((dfg_first_prefix_nextentrycell) = 2 * (ge_balance_positive_prefix_nextentrycellfirstvalue) /\ (ge_balance_negative_prefix_nextentrycellfirstvalue) = 0) \/ exists ge_signed_half_prefix_nextentrycellfirstvaluedecode. (((dfg_first_prefix_nextentrycell) = 2 * ge_signed_half_prefix_nextentrycellfirstvaluedecode + 1 /\ (ge_balance_positive_prefix_nextentrycellfirstvalue) = 0) /\ (ge_balance_negative_prefix_nextentrycellfirstvalue) = S ge_signed_half_prefix_nextentrycellfirstvaluedecode))) /\ ((dst_positive_prefix_nextentrycellfirst) + ge_balance_negative_prefix_nextentrycellfirstvalue = (dst_negative_prefix_nextentrycellfirst) + ge_balance_positive_prefix_nextentrycellfirstvalue))))))))) /\ (((exists dst_positive_code_prefix_nextentrycelllast dst_positive_scale_prefix_nextentrycelllast dst_negative_code_prefix_nextentrycelllast dst_negative_scale_prefix_nextentrycelllast dst_positive_prefix_nextentrycelllast dst_negative_prefix_nextentrycelllast. (((H) = (((((dst_positive_code_prefix_nextentrycelllast) + (dst_positive_scale_prefix_nextentrycelllast)) * S ((dst_positive_code_prefix_nextentrycelllast) + (dst_positive_scale_prefix_nextentrycelllast)) + ((dst_positive_scale_prefix_nextentrycelllast) + (dst_positive_scale_prefix_nextentrycelllast))) + (((dst_negative_code_prefix_nextentrycelllast) + (dst_negative_scale_prefix_nextentrycelllast)) * S ((dst_negative_code_prefix_nextentrycelllast) + (dst_negative_scale_prefix_nextentrycelllast)) + ((dst_negative_scale_prefix_nextentrycelllast) + (dst_negative_scale_prefix_nextentrycelllast)))) * S ((((dst_positive_code_prefix_nextentrycelllast) + (dst_positive_scale_prefix_nextentrycelllast)) * S ((dst_positive_code_prefix_nextentrycelllast) + (dst_positive_scale_prefix_nextentrycelllast)) + ((dst_positive_scale_prefix_nextentrycelllast) + (dst_positive_scale_prefix_nextentrycelllast))) + (((dst_negative_code_prefix_nextentrycelllast) + (dst_negative_scale_prefix_nextentrycelllast)) * S ((dst_negative_code_prefix_nextentrycelllast) + (dst_negative_scale_prefix_nextentrycelllast)) + ((dst_negative_scale_prefix_nextentrycelllast) + (dst_negative_scale_prefix_nextentrycelllast)))) + ((((dst_negative_code_prefix_nextentrycelllast) + (dst_negative_scale_prefix_nextentrycelllast)) * S ((dst_negative_code_prefix_nextentrycelllast) + (dst_negative_scale_prefix_nextentrycelllast)) + ((dst_negative_scale_prefix_nextentrycelllast) + (dst_negative_scale_prefix_nextentrycelllast))) + (((dst_negative_code_prefix_nextentrycelllast) + (dst_negative_scale_prefix_nextentrycelllast)) * S ((dst_negative_code_prefix_nextentrycelllast) + (dst_negative_scale_prefix_nextentrycelllast)) + ((dst_negative_scale_prefix_nextentrycelllast) + (dst_negative_scale_prefix_nextentrycelllast)))))) /\ (((((exists ff_h_pvs_prefix_nextentrycelllastpositive. ff_h_pvs_prefix_nextentrycelllastpositive + S (dst_positive_prefix_nextentrycelllast) = S ((S (dfg_flat_column_prefix_nextentry)) * dst_positive_scale_prefix_nextentrycelllast)) /\ exists ff_q_pvs_prefix_nextentrycelllastpositive. dst_positive_code_prefix_nextentrycelllast = ff_q_pvs_prefix_nextentrycelllastpositive * S ((S (dfg_flat_column_prefix_nextentry)) * dst_positive_scale_prefix_nextentrycelllast) + (dst_positive_prefix_nextentrycelllast))) /\ (((((exists ff_h_pvs_prefix_nextentrycelllastnegative. ff_h_pvs_prefix_nextentrycelllastnegative + S (dst_negative_prefix_nextentrycelllast) = S ((S (dfg_flat_column_prefix_nextentry)) * dst_negative_scale_prefix_nextentrycelllast)) /\ exists ff_q_pvs_prefix_nextentrycelllastnegative. dst_negative_code_prefix_nextentrycelllast = ff_q_pvs_prefix_nextentrycelllastnegative * S ((S (dfg_flat_column_prefix_nextentry)) * dst_negative_scale_prefix_nextentrycelllast) + (dst_negative_prefix_nextentrycelllast))) /\ (exists ge_balance_positive_prefix_nextentrycelllastvalue ge_balance_negative_prefix_nextentrycelllastvalue. (((((dfg_last_prefix_nextentrycell) = 2 * (ge_balance_positive_prefix_nextentrycelllastvalue) /\ (ge_balance_negative_prefix_nextentrycelllastvalue) = 0) \/ exists ge_signed_half_prefix_nextentrycelllastvaluedecode. (((dfg_last_prefix_nextentrycell) = 2 * ge_signed_half_prefix_nextentrycelllastvaluedecode + 1 /\ (ge_balance_positive_prefix_nextentrycelllastvalue) = 0) /\ (ge_balance_negative_prefix_nextentrycelllastvalue) = S ge_signed_half_prefix_nextentrycelllastvaluedecode))) /\ ((dst_positive_prefix_nextentrycelllast) + ge_balance_negative_prefix_nextentrycelllastvalue = (dst_negative_prefix_nextentrycelllast) + ge_balance_positive_prefix_nextentrycelllastvalue))))))))) /\ (((exists dst_positive_code_prefix_nextentrycellmiddle dst_positive_scale_prefix_nextentrycellmiddle dst_negative_code_prefix_nextentrycellmiddle dst_negative_scale_prefix_nextentrycellmiddle dst_positive_prefix_nextentrycellmiddle dst_negative_prefix_nextentrycellmiddle. (((G) = (((((dst_positive_code_prefix_nextentrycellmiddle) + (dst_positive_scale_prefix_nextentrycellmiddle)) * S ((dst_positive_code_prefix_nextentrycellmiddle) + (dst_positive_scale_prefix_nextentrycellmiddle)) + ((dst_positive_scale_prefix_nextentrycellmiddle) + (dst_positive_scale_prefix_nextentrycellmiddle))) + (((dst_negative_code_prefix_nextentrycellmiddle) + (dst_negative_scale_prefix_nextentrycellmiddle)) * S ((dst_negative_code_prefix_nextentrycellmiddle) + (dst_negative_scale_prefix_nextentrycellmiddle)) + ((dst_negative_scale_prefix_nextentrycellmiddle) + (dst_negative_scale_prefix_nextentrycellmiddle)))) * S ((((dst_positive_code_prefix_nextentrycellmiddle) + (dst_positive_scale_prefix_nextentrycellmiddle)) * S ((dst_positive_code_prefix_nextentrycellmiddle) + (dst_positive_scale_prefix_nextentrycellmiddle)) + ((dst_positive_scale_prefix_nextentrycellmiddle) + (dst_positive_scale_prefix_nextentrycellmiddle))) + (((dst_negative_code_prefix_nextentrycellmiddle) + (dst_negative_scale_prefix_nextentrycellmiddle)) * S ((dst_negative_code_prefix_nextentrycellmiddle) + (dst_negative_scale_prefix_nextentrycellmiddle)) + ((dst_negative_scale_prefix_nextentrycellmiddle) + (dst_negative_scale_prefix_nextentrycellmiddle)))) + ((((dst_negative_code_prefix_nextentrycellmiddle) + (dst_negative_scale_prefix_nextentrycellmiddle)) * S ((dst_negative_code_prefix_nextentrycellmiddle) + (dst_negative_scale_prefix_nextentrycellmiddle)) + ((dst_negative_scale_prefix_nextentrycellmiddle) + (dst_negative_scale_prefix_nextentrycellmiddle))) + (((dst_negative_code_prefix_nextentrycellmiddle) + (dst_negative_scale_prefix_nextentrycellmiddle)) * S ((dst_negative_code_prefix_nextentrycellmiddle) + (dst_negative_scale_prefix_nextentrycellmiddle)) + ((dst_negative_scale_prefix_nextentrycellmiddle) + (dst_negative_scale_prefix_nextentrycellmiddle)))))) /\ (((((exists ff_h_pvs_prefix_nextentrycellmiddlepositive. ff_h_pvs_prefix_nextentrycellmiddlepositive + S (dst_positive_prefix_nextentrycellmiddle) = S ((S (dfg_middle_prefix_nextentrycell)) * dst_positive_scale_prefix_nextentrycellmiddle)) /\ exists ff_q_pvs_prefix_nextentrycellmiddlepositive. dst_positive_code_prefix_nextentrycellmiddle = ff_q_pvs_prefix_nextentrycellmiddlepositive * S ((S (dfg_middle_prefix_nextentrycell)) * dst_positive_scale_prefix_nextentrycellmiddle) + (dst_positive_prefix_nextentrycellmiddle))) /\ (((((exists ff_h_pvs_prefix_nextentrycellmiddlenegative. ff_h_pvs_prefix_nextentrycellmiddlenegative + S (dst_negative_prefix_nextentrycellmiddle) = S ((S (dfg_middle_prefix_nextentrycell)) * dst_negative_scale_prefix_nextentrycellmiddle)) /\ exists ff_q_pvs_prefix_nextentrycellmiddlenegative. dst_negative_code_prefix_nextentrycellmiddle = ff_q_pvs_prefix_nextentrycellmiddlenegative * S ((S (dfg_middle_prefix_nextentrycell)) * dst_negative_scale_prefix_nextentrycellmiddle) + (dst_negative_prefix_nextentrycellmiddle))) /\ (exists ge_balance_positive_prefix_nextentrycellmiddlevalue ge_balance_negative_prefix_nextentrycellmiddlevalue. (((((dfg_value_prefix_nextentrycell) = 2 * (ge_balance_positive_prefix_nextentrycellmiddlevalue) /\ (ge_balance_negative_prefix_nextentrycellmiddlevalue) = 0) \/ exists ge_signed_half_prefix_nextentrycellmiddlevaluedecode. (((dfg_value_prefix_nextentrycell) = 2 * ge_signed_half_prefix_nextentrycellmiddlevaluedecode + 1 /\ (ge_balance_positive_prefix_nextentrycellmiddlevalue) = 0) /\ (ge_balance_negative_prefix_nextentrycellmiddlevalue) = S ge_signed_half_prefix_nextentrycellmiddlevaluedecode))) /\ ((dst_positive_prefix_nextentrycellmiddle) + ge_balance_negative_prefix_nextentrycellmiddlevalue = (dst_negative_prefix_nextentrycellmiddle) + ge_balance_positive_prefix_nextentrycellmiddlevalue))))))))) /\ (exists dfg_inner_prefix_nextentrycellproduct. ((exists sto_ap_prefix_nextentrycellproductinner sto_an_prefix_nextentrycellproductinner sto_bp_prefix_nextentrycellproductinner sto_bn_prefix_nextentrycellproductinner sto_cp_prefix_nextentrycellproductinner sto_cn_prefix_nextentrycellproductinner. (((((dfg_last_prefix_nextentrycell) = 2 * (sto_ap_prefix_nextentrycellproductinner) /\ (sto_an_prefix_nextentrycellproductinner) = 0) \/ exists ge_signed_half_prefix_nextentrycellproductinnerleft. (((dfg_last_prefix_nextentrycell) = 2 * ge_signed_half_prefix_nextentrycellproductinnerleft + 1 /\ (sto_ap_prefix_nextentrycellproductinner) = 0) /\ (sto_an_prefix_nextentrycellproductinner) = S ge_signed_half_prefix_nextentrycellproductinnerleft))) /\ ((((((dfg_value_prefix_nextentrycell) = 2 * (sto_bp_prefix_nextentrycellproductinner) /\ (sto_bn_prefix_nextentrycellproductinner) = 0) \/ exists ge_signed_half_prefix_nextentrycellproductinnerright. (((dfg_value_prefix_nextentrycell) = 2 * ge_signed_half_prefix_nextentrycellproductinnerright + 1 /\ (sto_bp_prefix_nextentrycellproductinner) = 0) /\ (sto_bn_prefix_nextentrycellproductinner) = S ge_signed_half_prefix_nextentrycellproductinnerright))) /\ ((((((dfg_inner_prefix_nextentrycellproduct) = 2 * (sto_cp_prefix_nextentrycellproductinner) /\ (sto_cn_prefix_nextentrycellproductinner) = 0) \/ exists ge_signed_half_prefix_nextentrycellproductinneroutput. (((dfg_inner_prefix_nextentrycellproduct) = 2 * ge_signed_half_prefix_nextentrycellproductinneroutput + 1 /\ (sto_cp_prefix_nextentrycellproductinner) = 0) /\ (sto_cn_prefix_nextentrycellproductinner) = S ge_signed_half_prefix_nextentrycellproductinneroutput))) /\ ((sto_ap_prefix_nextentrycellproductinner * sto_bp_prefix_nextentrycellproductinner + sto_an_prefix_nextentrycellproductinner * sto_bn_prefix_nextentrycellproductinner) + sto_cn_prefix_nextentrycellproductinner = (sto_ap_prefix_nextentrycellproductinner * sto_bn_prefix_nextentrycellproductinner + sto_an_prefix_nextentrycellproductinner * sto_bp_prefix_nextentrycellproductinner) + sto_cp_prefix_nextentrycellproductinner))))))) /\ (exists sto_ap_prefix_nextentrycellproductouter sto_an_prefix_nextentrycellproductouter sto_bp_prefix_nextentrycellproductouter sto_bn_prefix_nextentrycellproductouter sto_cp_prefix_nextentrycellproductouter sto_cn_prefix_nextentrycellproductouter. (((((dfg_first_prefix_nextentrycell) = 2 * (sto_ap_prefix_nextentrycellproductouter) /\ (sto_an_prefix_nextentrycellproductouter) = 0) \/ exists ge_signed_half_prefix_nextentrycellproductouterleft. (((dfg_first_prefix_nextentrycell) = 2 * ge_signed_half_prefix_nextentrycellproductouterleft + 1 /\ (sto_ap_prefix_nextentrycellproductouter) = 0) /\ (sto_an_prefix_nextentrycellproductouter) = S ge_signed_half_prefix_nextentrycellproductouterleft))) /\ ((((((dfg_inner_prefix_nextentrycellproduct) = 2 * (sto_bp_prefix_nextentrycellproductouter) /\ (sto_bn_prefix_nextentrycellproductouter) = 0) \/ exists ge_signed_half_prefix_nextentrycellproductouterright. (((dfg_inner_prefix_nextentrycellproduct) = 2 * ge_signed_half_prefix_nextentrycellproductouterright + 1 /\ (sto_bp_prefix_nextentrycellproductouter) = 0) /\ (sto_bn_prefix_nextentrycellproductouter) = S ge_signed_half_prefix_nextentrycellproductouterright))) /\ ((((((dfg_flat_value_prefix_next) = 2 * (sto_cp_prefix_nextentrycellproductouter) /\ (sto_cn_prefix_nextentrycellproductouter) = 0) \/ exists ge_signed_half_prefix_nextentrycellproductouteroutput. (((dfg_flat_value_prefix_next) = 2 * ge_signed_half_prefix_nextentrycellproductouteroutput + 1 /\ (sto_cp_prefix_nextentrycellproductouter) = 0) /\ (sto_cn_prefix_nextentrycellproductouter) = S ge_signed_half_prefix_nextentrycellproductouteroutput))) /\ ((sto_ap_prefix_nextentrycellproductouter * sto_bp_prefix_nextentrycellproductouter + sto_an_prefix_nextentrycellproductouter * sto_bn_prefix_nextentrycellproductouter) + sto_cn_prefix_nextentrycellproductouter = (sto_ap_prefix_nextentrycellproductouter * sto_bn_prefix_nextentrycellproductouter + sto_an_prefix_nextentrycellproductouter * sto_bp_prefix_nextentrycellproductouter) + sto_cp_prefix_nextentrycellproductouter))))))))))))))))))))) \/ ((((dfg_flat_row_prefix_nextentry)=0 \/ ((dfg_flat_column_prefix_nextentry)=0 \/ ~(exists pvs_factor_prefix_nextentrycellomittednondivisor. (n) = ((dfg_flat_row_prefix_nextentry)*(dfg_flat_column_prefix_nextentry)) * pvs_factor_prefix_nextentrycellomittednondivisor))) /\ ((dfg_flat_value_prefix_next)=0))))))))))) /\ (forall dst_index_prefix_preserved dst_first_prefix_preserved dst_second_prefix_preserved. (exists pvs_gap_prefix_preservedbound. pvs_gap_prefix_preservedbound + S (dst_index_prefix_preserved) = (S l)) -> (exists dst_positive_code_prefix_preservedfirst dst_positive_scale_prefix_preservedfirst dst_negative_code_prefix_preservedfirst dst_negative_scale_prefix_preservedfirst dst_positive_prefix_preservedfirst dst_negative_prefix_preservedfirst. (((x) = (((((dst_positive_code_prefix_preservedfirst) + (dst_positive_scale_prefix_preservedfirst)) * S ((dst_positive_code_prefix_preservedfirst) + (dst_positive_scale_prefix_preservedfirst)) + ((dst_positive_scale_prefix_preservedfirst) + (dst_positive_scale_prefix_preservedfirst))) + (((dst_negative_code_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)) * S ((dst_negative_code_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)) + ((dst_negative_scale_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)))) * S ((((dst_positive_code_prefix_preservedfirst) + (dst_positive_scale_prefix_preservedfirst)) * S ((dst_positive_code_prefix_preservedfirst) + (dst_positive_scale_prefix_preservedfirst)) + ((dst_positive_scale_prefix_preservedfirst) + (dst_positive_scale_prefix_preservedfirst))) + (((dst_negative_code_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)) * S ((dst_negative_code_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)) + ((dst_negative_scale_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)))) + ((((dst_negative_code_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)) * S ((dst_negative_code_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)) + ((dst_negative_scale_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst))) + (((dst_negative_code_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)) * S ((dst_negative_code_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)) + ((dst_negative_scale_prefix_preservedfirst) + (dst_negative_scale_prefix_preservedfirst)))))) /\ (((((exists ff_h_pvs_prefix_preservedfirstpositive. ff_h_pvs_prefix_preservedfirstpositive + S (dst_positive_prefix_preservedfirst) = S ((S (dst_index_prefix_preserved)) * dst_positive_scale_prefix_preservedfirst)) /\ exists ff_q_pvs_prefix_preservedfirstpositive. dst_positive_code_prefix_preservedfirst = ff_q_pvs_prefix_preservedfirstpositive * S ((S (dst_index_prefix_preserved)) * dst_positive_scale_prefix_preservedfirst) + (dst_positive_prefix_preservedfirst))) /\ (((((exists ff_h_pvs_prefix_preservedfirstnegative. ff_h_pvs_prefix_preservedfirstnegative + S (dst_negative_prefix_preservedfirst) = S ((S (dst_index_prefix_preserved)) * dst_negative_scale_prefix_preservedfirst)) /\ exists ff_q_pvs_prefix_preservedfirstnegative. dst_negative_code_prefix_preservedfirst = ff_q_pvs_prefix_preservedfirstnegative * S ((S (dst_index_prefix_preserved)) * dst_negative_scale_prefix_preservedfirst) + (dst_negative_prefix_preservedfirst))) /\ (exists ge_balance_positive_prefix_preservedfirstvalue ge_balance_negative_prefix_preservedfirstvalue. (((((dst_first_prefix_preserved) = 2 * (ge_balance_positive_prefix_preservedfirstvalue) /\ (ge_balance_negative_prefix_preservedfirstvalue) = 0) \/ exists ge_signed_half_prefix_preservedfirstvaluedecode. (((dst_first_prefix_preserved) = 2 * ge_signed_half_prefix_preservedfirstvaluedecode + 1 /\ (ge_balance_positive_prefix_preservedfirstvalue) = 0) /\ (ge_balance_negative_prefix_preservedfirstvalue) = S ge_signed_half_prefix_preservedfirstvaluedecode))) /\ ((dst_positive_prefix_preservedfirst) + ge_balance_negative_prefix_preservedfirstvalue = (dst_negative_prefix_preservedfirst) + ge_balance_positive_prefix_preservedfirstvalue))))))))) -> (exists dst_positive_code_prefix_preservedsecond dst_positive_scale_prefix_preservedsecond dst_negative_code_prefix_preservedsecond dst_negative_scale_prefix_preservedsecond dst_positive_prefix_preservedsecond dst_negative_prefix_preservedsecond. (((U) = (((((dst_positive_code_prefix_preservedsecond) + (dst_positive_scale_prefix_preservedsecond)) * S ((dst_positive_code_prefix_preservedsecond) + (dst_positive_scale_prefix_preservedsecond)) + ((dst_positive_scale_prefix_preservedsecond) + (dst_positive_scale_prefix_preservedsecond))) + (((dst_negative_code_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)) * S ((dst_negative_code_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)) + ((dst_negative_scale_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)))) * S ((((dst_positive_code_prefix_preservedsecond) + (dst_positive_scale_prefix_preservedsecond)) * S ((dst_positive_code_prefix_preservedsecond) + (dst_positive_scale_prefix_preservedsecond)) + ((dst_positive_scale_prefix_preservedsecond) + (dst_positive_scale_prefix_preservedsecond))) + (((dst_negative_code_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)) * S ((dst_negative_code_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)) + ((dst_negative_scale_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)))) + ((((dst_negative_code_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)) * S ((dst_negative_code_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)) + ((dst_negative_scale_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond))) + (((dst_negative_code_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)) * S ((dst_negative_code_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)) + ((dst_negative_scale_prefix_preservedsecond) + (dst_negative_scale_prefix_preservedsecond)))))) /\ (((((exists ff_h_pvs_prefix_preservedsecondpositive. ff_h_pvs_prefix_preservedsecondpositive + S (dst_positive_prefix_preservedsecond) = S ((S (dst_index_prefix_preserved)) * dst_positive_scale_prefix_preservedsecond)) /\ exists ff_q_pvs_prefix_preservedsecondpositive. dst_positive_code_prefix_preservedsecond = ff_q_pvs_prefix_preservedsecondpositive * S ((S (dst_index_prefix_preserved)) * dst_positive_scale_prefix_preservedsecond) + (dst_positive_prefix_preservedsecond))) /\ (((((exists ff_h_pvs_prefix_preservedsecondnegative. ff_h_pvs_prefix_preservedsecondnegative + S (dst_negative_prefix_preservedsecond) = S ((S (dst_index_prefix_preserved)) * dst_negative_scale_prefix_preservedsecond)) /\ exists ff_q_pvs_prefix_preservedsecondnegative. dst_negative_code_prefix_preservedsecond = ff_q_pvs_prefix_preservedsecondnegative * S ((S (dst_index_prefix_preserved)) * dst_negative_scale_prefix_preservedsecond) + (dst_negative_prefix_preservedsecond))) /\ (exists ge_balance_positive_prefix_preservedsecondvalue ge_balance_negative_prefix_preservedsecondvalue. (((((dst_second_prefix_preserved) = 2 * (ge_balance_positive_prefix_preservedsecondvalue) /\ (ge_balance_negative_prefix_preservedsecondvalue) = 0) \/ exists ge_signed_half_prefix_preservedsecondvaluedecode. (((dst_second_prefix_preserved) = 2 * ge_signed_half_prefix_preservedsecondvaluedecode + 1 /\ (ge_balance_positive_prefix_preservedsecondvalue) = 0) /\ (ge_balance_negative_prefix_preservedsecondvalue) = S ge_signed_half_prefix_preservedsecondvaluedecode))) /\ ((dst_positive_prefix_preservedsecond) + ge_balance_negative_prefix_preservedsecondvalue = (dst_negative_prefix_preservedsecond) + ge_balance_positive_prefix_preservedsecondvalue))))))))) -> dst_first_prefix_preserved = dst_second_prefix_preserved))) - 0058
specialize dirichlet_grid_flat_prefix_append (F) - 0059
specialize dirichlet_grid_flat_prefix_append (G) - 0060
specialize dirichlet_grid_flat_prefix_append (H) - 0061
specialize dirichlet_grid_flat_prefix_append (n) - 0062
specialize dirichlet_grid_flat_prefix_append (l) - 0063
specialize dirichlet_grid_flat_prefix_append (x) - 0064
specialize dirichlet_grid_flat_prefix_append (x1) - 0065
apply dirichlet_grid_flat_prefix_append - 0066
exact hp_witness - 0067
exact hv_witness - 0068
cases hext - 0069
cases hext_witness - 0070
exists x2 - 0071
exact hext_witness_left