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 n l. (exists dst_positive_code_prefix_exists_F dst_positive_scale_prefix_exists_F dst_negative_code_prefix_exists_F dst_negative_scale_prefix_exists_F. (((F) = (((((dst_positive_code_prefix_exists_F) + (dst_positive_scale_prefix_exists_F)) * S ((dst_positive_code_prefix_exists_F) + (dst_positive_scale_prefix_exists_F)) + ((dst_positive_scale_prefix_exists_F) + (dst_positive_scale_prefix_exists_F))) + (((dst_negative_code_prefix_exists_F) + (dst_negative_scale_prefix_exists_F)) * S ((dst_negative_code_prefix_exists_F) + (dst_negative_scale_prefix_exists_F)) + ((dst_negative_scale_prefix_exists_F) + (dst_negative_scale_prefix_exists_F)))) * S ((((dst_positive_code_prefix_exists_F) + (dst_positive_scale_prefix_exists_F)) * S ((dst_positive_code_prefix_exists_F) + (dst_positive_scale_prefix_exists_F)) + ((dst_positive_scale_prefix_exists_F) + (dst_positive_scale_prefix_exists_F))) + (((dst_negative_code_prefix_exists_F) + (dst_negative_scale_prefix_exists_F)) * S ((dst_negative_code_prefix_exists_F) + (dst_negative_scale_prefix_exists_F)) + ((dst_negative_scale_prefix_exists_F) + (dst_negative_scale_prefix_exists_F)))) + ((((dst_negative_code_prefix_exists_F) + (dst_negative_scale_prefix_exists_F)) * S ((dst_negative_code_prefix_exists_F) + (dst_negative_scale_prefix_exists_F)) + ((dst_negative_scale_prefix_exists_F) + (dst_negative_scale_prefix_exists_F))) + (((dst_negative_code_prefix_exists_F) + (dst_negative_scale_prefix_exists_F)) * S ((dst_negative_code_prefix_exists_F) + (dst_negative_scale_prefix_exists_F)) + ((dst_negative_scale_prefix_exists_F) + (dst_negative_scale_prefix_exists_F)))))) /\ (forall dst_index_prefix_exists_F. (exists pvs_le_gap_prefix_exists_Fdomain. pvs_le_gap_prefix_exists_Fdomain + (dst_index_prefix_exists_F) = (0)) -> exists dst_positive_prefix_exists_F dst_negative_prefix_exists_F dst_value_prefix_exists_F. ((((exists ff_h_pvs_prefix_exists_Fentrypositive. ff_h_pvs_prefix_exists_Fentrypositive + S (dst_positive_prefix_exists_F) = S ((S (dst_index_prefix_exists_F)) * dst_positive_scale_prefix_exists_F)) /\ exists ff_q_pvs_prefix_exists_Fentrypositive. dst_positive_code_prefix_exists_F = ff_q_pvs_prefix_exists_Fentrypositive * S ((S (dst_index_prefix_exists_F)) * dst_positive_scale_prefix_exists_F) + (dst_positive_prefix_exists_F))) /\ (((((exists ff_h_pvs_prefix_exists_Fentrynegative. ff_h_pvs_prefix_exists_Fentrynegative + S (dst_negative_prefix_exists_F) = S ((S (dst_index_prefix_exists_F)) * dst_negative_scale_prefix_exists_F)) /\ exists ff_q_pvs_prefix_exists_Fentrynegative. dst_negative_code_prefix_exists_F = ff_q_pvs_prefix_exists_Fentrynegative * S ((S (dst_index_prefix_exists_F)) * dst_negative_scale_prefix_exists_F) + (dst_negative_prefix_exists_F))) /\ (exists ge_balance_positive_prefix_exists_Fentryvalue ge_balance_negative_prefix_exists_Fentryvalue. (((((dst_value_prefix_exists_F) = 2 * (ge_balance_positive_prefix_exists_Fentryvalue) /\ (ge_balance_negative_prefix_exists_Fentryvalue) = 0) \/ exists ge_signed_half_prefix_exists_Fentryvaluedecode. (((dst_value_prefix_exists_F) = 2 * ge_signed_half_prefix_exists_Fentryvaluedecode + 1 /\ (ge_balance_positive_prefix_exists_Fentryvalue) = 0) /\ (ge_balance_negative_prefix_exists_Fentryvalue) = S ge_signed_half_prefix_exists_Fentryvaluedecode))) /\ ((dst_positive_prefix_exists_F) + ge_balance_negative_prefix_exists_Fentryvalue = (dst_negative_prefix_exists_F) + ge_balance_positive_prefix_exists_Fentryvalue))))))))) -> (exists dst_positive_code_prefix_exists_G dst_positive_scale_prefix_exists_G dst_negative_code_prefix_exists_G dst_negative_scale_prefix_exists_G. (((G) = (((((dst_positive_code_prefix_exists_G) + (dst_positive_scale_prefix_exists_G)) * S ((dst_positive_code_prefix_exists_G) + (dst_positive_scale_prefix_exists_G)) + ((dst_positive_scale_prefix_exists_G) + (dst_positive_scale_prefix_exists_G))) + (((dst_negative_code_prefix_exists_G) + (dst_negative_scale_prefix_exists_G)) * S ((dst_negative_code_prefix_exists_G) + (dst_negative_scale_prefix_exists_G)) + ((dst_negative_scale_prefix_exists_G) + (dst_negative_scale_prefix_exists_G)))) * S ((((dst_positive_code_prefix_exists_G) + (dst_positive_scale_prefix_exists_G)) * S ((dst_positive_code_prefix_exists_G) + (dst_positive_scale_prefix_exists_G)) + ((dst_positive_scale_prefix_exists_G) + (dst_positive_scale_prefix_exists_G))) + (((dst_negative_code_prefix_exists_G) + (dst_negative_scale_prefix_exists_G)) * S ((dst_negative_code_prefix_exists_G) + (dst_negative_scale_prefix_exists_G)) + ((dst_negative_scale_prefix_exists_G) + (dst_negative_scale_prefix_exists_G)))) + ((((dst_negative_code_prefix_exists_G) + (dst_negative_scale_prefix_exists_G)) * S ((dst_negative_code_prefix_exists_G) + (dst_negative_scale_prefix_exists_G)) + ((dst_negative_scale_prefix_exists_G) + (dst_negative_scale_prefix_exists_G))) + (((dst_negative_code_prefix_exists_G) + (dst_negative_scale_prefix_exists_G)) * S ((dst_negative_code_prefix_exists_G) + (dst_negative_scale_prefix_exists_G)) + ((dst_negative_scale_prefix_exists_G) + (dst_negative_scale_prefix_exists_G)))))) /\ (forall dst_index_prefix_exists_G. (exists pvs_le_gap_prefix_exists_Gdomain. pvs_le_gap_prefix_exists_Gdomain + (dst_index_prefix_exists_G) = (0)) -> exists dst_positive_prefix_exists_G dst_negative_prefix_exists_G dst_value_prefix_exists_G. ((((exists ff_h_pvs_prefix_exists_Gentrypositive. ff_h_pvs_prefix_exists_Gentrypositive + S (dst_positive_prefix_exists_G) = S ((S (dst_index_prefix_exists_G)) * dst_positive_scale_prefix_exists_G)) /\ exists ff_q_pvs_prefix_exists_Gentrypositive. dst_positive_code_prefix_exists_G = ff_q_pvs_prefix_exists_Gentrypositive * S ((S (dst_index_prefix_exists_G)) * dst_positive_scale_prefix_exists_G) + (dst_positive_prefix_exists_G))) /\ (((((exists ff_h_pvs_prefix_exists_Gentrynegative. ff_h_pvs_prefix_exists_Gentrynegative + S (dst_negative_prefix_exists_G) = S ((S (dst_index_prefix_exists_G)) * dst_negative_scale_prefix_exists_G)) /\ exists ff_q_pvs_prefix_exists_Gentrynegative. dst_negative_code_prefix_exists_G = ff_q_pvs_prefix_exists_Gentrynegative * S ((S (dst_index_prefix_exists_G)) * dst_negative_scale_prefix_exists_G) + (dst_negative_prefix_exists_G))) /\ (exists ge_balance_positive_prefix_exists_Gentryvalue ge_balance_negative_prefix_exists_Gentryvalue. (((((dst_value_prefix_exists_G) = 2 * (ge_balance_positive_prefix_exists_Gentryvalue) /\ (ge_balance_negative_prefix_exists_Gentryvalue) = 0) \/ exists ge_signed_half_prefix_exists_Gentryvaluedecode. (((dst_value_prefix_exists_G) = 2 * ge_signed_half_prefix_exists_Gentryvaluedecode + 1 /\ (ge_balance_positive_prefix_exists_Gentryvalue) = 0) /\ (ge_balance_negative_prefix_exists_Gentryvalue) = S ge_signed_half_prefix_exists_Gentryvaluedecode))) /\ ((dst_positive_prefix_exists_G) + ge_balance_negative_prefix_exists_Gentryvalue = (dst_negative_prefix_exists_G) + ge_balance_positive_prefix_exists_Gentryvalue))))))))) -> ~(n=0) -> exists T. (((exists dst_positive_code_prefix_exists_resulttable dst_positive_scale_prefix_exists_resulttable dst_negative_code_prefix_exists_resulttable dst_negative_scale_prefix_exists_resulttable. (((T) = (((((dst_positive_code_prefix_exists_resulttable) + (dst_positive_scale_prefix_exists_resulttable)) * S ((dst_positive_code_prefix_exists_resulttable) + (dst_positive_scale_prefix_exists_resulttable)) + ((dst_positive_scale_prefix_exists_resulttable) + (dst_positive_scale_prefix_exists_resulttable))) + (((dst_negative_code_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)) * S ((dst_negative_code_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)) + ((dst_negative_scale_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)))) * S ((((dst_positive_code_prefix_exists_resulttable) + (dst_positive_scale_prefix_exists_resulttable)) * S ((dst_positive_code_prefix_exists_resulttable) + (dst_positive_scale_prefix_exists_resulttable)) + ((dst_positive_scale_prefix_exists_resulttable) + (dst_positive_scale_prefix_exists_resulttable))) + (((dst_negative_code_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)) * S ((dst_negative_code_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)) + ((dst_negative_scale_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)))) + ((((dst_negative_code_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)) * S ((dst_negative_code_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)) + ((dst_negative_scale_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable))) + (((dst_negative_code_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)) * S ((dst_negative_code_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)) + ((dst_negative_scale_prefix_exists_resulttable) + (dst_negative_scale_prefix_exists_resulttable)))))) /\ (forall dst_index_prefix_exists_resulttable. (exists pvs_le_gap_prefix_exists_resulttabledomain. pvs_le_gap_prefix_exists_resulttabledomain + (dst_index_prefix_exists_resulttable) = (l)) -> exists dst_positive_prefix_exists_resulttable dst_negative_prefix_exists_resulttable dst_value_prefix_exists_resulttable. ((((exists ff_h_pvs_prefix_exists_resulttableentrypositive. ff_h_pvs_prefix_exists_resulttableentrypositive + S (dst_positive_prefix_exists_resulttable) = S ((S (dst_index_prefix_exists_resulttable)) * dst_positive_scale_prefix_exists_resulttable)) /\ exists ff_q_pvs_prefix_exists_resulttableentrypositive. dst_positive_code_prefix_exists_resulttable = ff_q_pvs_prefix_exists_resulttableentrypositive * S ((S (dst_index_prefix_exists_resulttable)) * dst_positive_scale_prefix_exists_resulttable) + (dst_positive_prefix_exists_resulttable))) /\ (((((exists ff_h_pvs_prefix_exists_resulttableentrynegative. ff_h_pvs_prefix_exists_resulttableentrynegative + S (dst_negative_prefix_exists_resulttable) = S ((S (dst_index_prefix_exists_resulttable)) * dst_negative_scale_prefix_exists_resulttable)) /\ exists ff_q_pvs_prefix_exists_resulttableentrynegative. dst_negative_code_prefix_exists_resulttable = ff_q_pvs_prefix_exists_resulttableentrynegative * S ((S (dst_index_prefix_exists_resulttable)) * dst_negative_scale_prefix_exists_resulttable) + (dst_negative_prefix_exists_resulttable))) /\ (exists ge_balance_positive_prefix_exists_resulttableentryvalue ge_balance_negative_prefix_exists_resulttableentryvalue. (((((dst_value_prefix_exists_resulttable) = 2 * (ge_balance_positive_prefix_exists_resulttableentryvalue) /\ (ge_balance_negative_prefix_exists_resulttableentryvalue) = 0) \/ exists ge_signed_half_prefix_exists_resulttableentryvaluedecode. (((dst_value_prefix_exists_resulttable) = 2 * ge_signed_half_prefix_exists_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_prefix_exists_resulttableentryvalue) = 0) /\ (ge_balance_negative_prefix_exists_resulttableentryvalue) = S ge_signed_half_prefix_exists_resulttableentryvaluedecode))) /\ ((dst_positive_prefix_exists_resulttable) + ge_balance_negative_prefix_exists_resulttableentryvalue = (dst_negative_prefix_exists_resulttable) + ge_balance_positive_prefix_exists_resulttableentryvalue))))))))) /\ (forall scp_flat_index_prefix_exists_result scp_flat_value_prefix_exists_result. (exists pvs_le_gap_prefix_exists_resultbound. pvs_le_gap_prefix_exists_resultbound + (scp_flat_index_prefix_exists_result) = (l)) -> (exists dst_positive_code_prefix_exists_resultentry dst_positive_scale_prefix_exists_resultentry dst_negative_code_prefix_exists_resultentry dst_negative_scale_prefix_exists_resultentry dst_positive_prefix_exists_resultentry dst_negative_prefix_exists_resultentry. (((T) = (((((dst_positive_code_prefix_exists_resultentry) + (dst_positive_scale_prefix_exists_resultentry)) * S ((dst_positive_code_prefix_exists_resultentry) + (dst_positive_scale_prefix_exists_resultentry)) + ((dst_positive_scale_prefix_exists_resultentry) + (dst_positive_scale_prefix_exists_resultentry))) + (((dst_negative_code_prefix_exists_resultentry) + (dst_negative_scale_prefix_exists_resultentry)) * S ((dst_negative_code_prefix_exists_resultentry) + (dst_negative_scale_prefix_exists_resultentry)) + ((dst_negative_scale_prefix_exists_resultentry) + (dst_negative_scale_prefix_exists_resultentry)))) * S ((((dst_positive_code_prefix_exists_resultentry) + (dst_positive_scale_prefix_exists_resultentry)) * S ((dst_positive_code_prefix_exists_resultentry) + (dst_positive_scale_prefix_exists_resultentry)) + ((dst_positive_scale_prefix_exists_resultentry) + (dst_positive_scale_prefix_exists_resultentry))) + (((dst_negative_code_prefix_exists_resultentry) + (dst_negative_scale_prefix_exists_resultentry)) * S ((dst_negative_code_prefix_exists_resultentry) + (dst_negative_scale_prefix_exists_resultentry)) + ((dst_negative_scale_prefix_exists_resultentry) + (dst_negative_scale_prefix_exists_resultentry)))) + ((((dst_negative_code_prefix_exists_resultentry) + (dst_negative_scale_prefix_exists_resultentry)) * S ((dst_negative_code_prefix_exists_resultentry) + (dst_negative_scale_prefix_exists_resultentry)) + ((dst_negative_scale_prefix_exists_resultentry) + (dst_negative_scale_prefix_exists_resultentry))) + (((dst_negative_code_prefix_exists_resultentry) + (dst_negative_scale_prefix_exists_resultentry)) * S ((dst_negative_code_prefix_exists_resultentry) + (dst_negative_scale_prefix_exists_resultentry)) + ((dst_negative_scale_prefix_exists_resultentry) + (dst_negative_scale_prefix_exists_resultentry)))))) /\ (((((exists ff_h_pvs_prefix_exists_resultentrypositive. ff_h_pvs_prefix_exists_resultentrypositive + S (dst_positive_prefix_exists_resultentry) = S ((S (scp_flat_index_prefix_exists_result)) * dst_positive_scale_prefix_exists_resultentry)) /\ exists ff_q_pvs_prefix_exists_resultentrypositive. dst_positive_code_prefix_exists_resultentry = ff_q_pvs_prefix_exists_resultentrypositive * S ((S (scp_flat_index_prefix_exists_result)) * dst_positive_scale_prefix_exists_resultentry) + (dst_positive_prefix_exists_resultentry))) /\ (((((exists ff_h_pvs_prefix_exists_resultentrynegative. ff_h_pvs_prefix_exists_resultentrynegative + S (dst_negative_prefix_exists_resultentry) = S ((S (scp_flat_index_prefix_exists_result)) * dst_negative_scale_prefix_exists_resultentry)) /\ exists ff_q_pvs_prefix_exists_resultentrynegative. dst_negative_code_prefix_exists_resultentry = ff_q_pvs_prefix_exists_resultentrynegative * S ((S (scp_flat_index_prefix_exists_result)) * dst_negative_scale_prefix_exists_resultentry) + (dst_negative_prefix_exists_resultentry))) /\ (exists ge_balance_positive_prefix_exists_resultentryvalue ge_balance_negative_prefix_exists_resultentryvalue. (((((scp_flat_value_prefix_exists_result) = 2 * (ge_balance_positive_prefix_exists_resultentryvalue) /\ (ge_balance_negative_prefix_exists_resultentryvalue) = 0) \/ exists ge_signed_half_prefix_exists_resultentryvaluedecode. (((scp_flat_value_prefix_exists_result) = 2 * ge_signed_half_prefix_exists_resultentryvaluedecode + 1 /\ (ge_balance_positive_prefix_exists_resultentryvalue) = 0) /\ (ge_balance_negative_prefix_exists_resultentryvalue) = S ge_signed_half_prefix_exists_resultentryvaluedecode))) /\ ((dst_positive_prefix_exists_resultentry) + ge_balance_negative_prefix_exists_resultentryvalue = (dst_negative_prefix_exists_resultentry) + ge_balance_positive_prefix_exists_resultentryvalue))))))))) -> (exists scp_flat_row_prefix_exists_resultproduct scp_flat_column_prefix_exists_resultproduct scp_flat_first_prefix_exists_resultproduct scp_flat_second_prefix_exists_resultproduct. (((scp_flat_index_prefix_exists_result)=((n)*(scp_flat_row_prefix_exists_resultproduct)+(scp_flat_column_prefix_exists_resultproduct))) /\ (((exists pvs_gap_prefix_exists_resultproductremainder. pvs_gap_prefix_exists_resultproductremainder + S (scp_flat_column_prefix_exists_resultproduct) = (n)) /\ (((exists dst_positive_code_prefix_exists_resultproductF dst_positive_scale_prefix_exists_resultproductF dst_negative_code_prefix_exists_resultproductF dst_negative_scale_prefix_exists_resultproductF dst_positive_prefix_exists_resultproductF dst_negative_prefix_exists_resultproductF. (((F) = (((((dst_positive_code_prefix_exists_resultproductF) + (dst_positive_scale_prefix_exists_resultproductF)) * S ((dst_positive_code_prefix_exists_resultproductF) + (dst_positive_scale_prefix_exists_resultproductF)) + ((dst_positive_scale_prefix_exists_resultproductF) + (dst_positive_scale_prefix_exists_resultproductF))) + (((dst_negative_code_prefix_exists_resultproductF) + (dst_negative_scale_prefix_exists_resultproductF)) * S ((dst_negative_code_prefix_exists_resultproductF) + (dst_negative_scale_prefix_exists_resultproductF)) + ((dst_negative_scale_prefix_exists_resultproductF) + (dst_negative_scale_prefix_exists_resultproductF)))) * S ((((dst_positive_code_prefix_exists_resultproductF) + (dst_positive_scale_prefix_exists_resultproductF)) * S ((dst_positive_code_prefix_exists_resultproductF) + (dst_positive_scale_prefix_exists_resultproductF)) + ((dst_positive_scale_prefix_exists_resultproductF) + (dst_positive_scale_prefix_exists_resultproductF))) + (((dst_negative_code_prefix_exists_resultproductF) + (dst_negative_scale_prefix_exists_resultproductF)) * S ((dst_negative_code_prefix_exists_resultproductF) + (dst_negative_scale_prefix_exists_resultproductF)) + ((dst_negative_scale_prefix_exists_resultproductF) + (dst_negative_scale_prefix_exists_resultproductF)))) + ((((dst_negative_code_prefix_exists_resultproductF) + (dst_negative_scale_prefix_exists_resultproductF)) * S ((dst_negative_code_prefix_exists_resultproductF) + (dst_negative_scale_prefix_exists_resultproductF)) + ((dst_negative_scale_prefix_exists_resultproductF) + (dst_negative_scale_prefix_exists_resultproductF))) + (((dst_negative_code_prefix_exists_resultproductF) + (dst_negative_scale_prefix_exists_resultproductF)) * S ((dst_negative_code_prefix_exists_resultproductF) + (dst_negative_scale_prefix_exists_resultproductF)) + ((dst_negative_scale_prefix_exists_resultproductF) + (dst_negative_scale_prefix_exists_resultproductF)))))) /\ (((((exists ff_h_pvs_prefix_exists_resultproductFpositive. ff_h_pvs_prefix_exists_resultproductFpositive + S (dst_positive_prefix_exists_resultproductF) = S ((S (scp_flat_row_prefix_exists_resultproduct)) * dst_positive_scale_prefix_exists_resultproductF)) /\ exists ff_q_pvs_prefix_exists_resultproductFpositive. dst_positive_code_prefix_exists_resultproductF = ff_q_pvs_prefix_exists_resultproductFpositive * S ((S (scp_flat_row_prefix_exists_resultproduct)) * dst_positive_scale_prefix_exists_resultproductF) + (dst_positive_prefix_exists_resultproductF))) /\ (((((exists ff_h_pvs_prefix_exists_resultproductFnegative. ff_h_pvs_prefix_exists_resultproductFnegative + S (dst_negative_prefix_exists_resultproductF) = S ((S (scp_flat_row_prefix_exists_resultproduct)) * dst_negative_scale_prefix_exists_resultproductF)) /\ exists ff_q_pvs_prefix_exists_resultproductFnegative. dst_negative_code_prefix_exists_resultproductF = ff_q_pvs_prefix_exists_resultproductFnegative * S ((S (scp_flat_row_prefix_exists_resultproduct)) * dst_negative_scale_prefix_exists_resultproductF) + (dst_negative_prefix_exists_resultproductF))) /\ (exists ge_balance_positive_prefix_exists_resultproductFvalue ge_balance_negative_prefix_exists_resultproductFvalue. (((((scp_flat_first_prefix_exists_resultproduct) = 2 * (ge_balance_positive_prefix_exists_resultproductFvalue) /\ (ge_balance_negative_prefix_exists_resultproductFvalue) = 0) \/ exists ge_signed_half_prefix_exists_resultproductFvaluedecode. (((scp_flat_first_prefix_exists_resultproduct) = 2 * ge_signed_half_prefix_exists_resultproductFvaluedecode + 1 /\ (ge_balance_positive_prefix_exists_resultproductFvalue) = 0) /\ (ge_balance_negative_prefix_exists_resultproductFvalue) = S ge_signed_half_prefix_exists_resultproductFvaluedecode))) /\ ((dst_positive_prefix_exists_resultproductF) + ge_balance_negative_prefix_exists_resultproductFvalue = (dst_negative_prefix_exists_resultproductF) + ge_balance_positive_prefix_exists_resultproductFvalue))))))))) /\ (((exists dst_positive_code_prefix_exists_resultproductG dst_positive_scale_prefix_exists_resultproductG dst_negative_code_prefix_exists_resultproductG dst_negative_scale_prefix_exists_resultproductG dst_positive_prefix_exists_resultproductG dst_negative_prefix_exists_resultproductG. (((G) = (((((dst_positive_code_prefix_exists_resultproductG) + (dst_positive_scale_prefix_exists_resultproductG)) * S ((dst_positive_code_prefix_exists_resultproductG) + (dst_positive_scale_prefix_exists_resultproductG)) + ((dst_positive_scale_prefix_exists_resultproductG) + (dst_positive_scale_prefix_exists_resultproductG))) + (((dst_negative_code_prefix_exists_resultproductG) + (dst_negative_scale_prefix_exists_resultproductG)) * S ((dst_negative_code_prefix_exists_resultproductG) + (dst_negative_scale_prefix_exists_resultproductG)) + ((dst_negative_scale_prefix_exists_resultproductG) + (dst_negative_scale_prefix_exists_resultproductG)))) * S ((((dst_positive_code_prefix_exists_resultproductG) + (dst_positive_scale_prefix_exists_resultproductG)) * S ((dst_positive_code_prefix_exists_resultproductG) + (dst_positive_scale_prefix_exists_resultproductG)) + ((dst_positive_scale_prefix_exists_resultproductG) + (dst_positive_scale_prefix_exists_resultproductG))) + (((dst_negative_code_prefix_exists_resultproductG) + (dst_negative_scale_prefix_exists_resultproductG)) * S ((dst_negative_code_prefix_exists_resultproductG) + (dst_negative_scale_prefix_exists_resultproductG)) + ((dst_negative_scale_prefix_exists_resultproductG) + (dst_negative_scale_prefix_exists_resultproductG)))) + ((((dst_negative_code_prefix_exists_resultproductG) + (dst_negative_scale_prefix_exists_resultproductG)) * S ((dst_negative_code_prefix_exists_resultproductG) + (dst_negative_scale_prefix_exists_resultproductG)) + ((dst_negative_scale_prefix_exists_resultproductG) + (dst_negative_scale_prefix_exists_resultproductG))) + (((dst_negative_code_prefix_exists_resultproductG) + (dst_negative_scale_prefix_exists_resultproductG)) * S ((dst_negative_code_prefix_exists_resultproductG) + (dst_negative_scale_prefix_exists_resultproductG)) + ((dst_negative_scale_prefix_exists_resultproductG) + (dst_negative_scale_prefix_exists_resultproductG)))))) /\ (((((exists ff_h_pvs_prefix_exists_resultproductGpositive. ff_h_pvs_prefix_exists_resultproductGpositive + S (dst_positive_prefix_exists_resultproductG) = S ((S (scp_flat_column_prefix_exists_resultproduct)) * dst_positive_scale_prefix_exists_resultproductG)) /\ exists ff_q_pvs_prefix_exists_resultproductGpositive. dst_positive_code_prefix_exists_resultproductG = ff_q_pvs_prefix_exists_resultproductGpositive * S ((S (scp_flat_column_prefix_exists_resultproduct)) * dst_positive_scale_prefix_exists_resultproductG) + (dst_positive_prefix_exists_resultproductG))) /\ (((((exists ff_h_pvs_prefix_exists_resultproductGnegative. ff_h_pvs_prefix_exists_resultproductGnegative + S (dst_negative_prefix_exists_resultproductG) = S ((S (scp_flat_column_prefix_exists_resultproduct)) * dst_negative_scale_prefix_exists_resultproductG)) /\ exists ff_q_pvs_prefix_exists_resultproductGnegative. dst_negative_code_prefix_exists_resultproductG = ff_q_pvs_prefix_exists_resultproductGnegative * S ((S (scp_flat_column_prefix_exists_resultproduct)) * dst_negative_scale_prefix_exists_resultproductG) + (dst_negative_prefix_exists_resultproductG))) /\ (exists ge_balance_positive_prefix_exists_resultproductGvalue ge_balance_negative_prefix_exists_resultproductGvalue. (((((scp_flat_second_prefix_exists_resultproduct) = 2 * (ge_balance_positive_prefix_exists_resultproductGvalue) /\ (ge_balance_negative_prefix_exists_resultproductGvalue) = 0) \/ exists ge_signed_half_prefix_exists_resultproductGvaluedecode. (((scp_flat_second_prefix_exists_resultproduct) = 2 * ge_signed_half_prefix_exists_resultproductGvaluedecode + 1 /\ (ge_balance_positive_prefix_exists_resultproductGvalue) = 0) /\ (ge_balance_negative_prefix_exists_resultproductGvalue) = S ge_signed_half_prefix_exists_resultproductGvaluedecode))) /\ ((dst_positive_prefix_exists_resultproductG) + ge_balance_negative_prefix_exists_resultproductGvalue = (dst_negative_prefix_exists_resultproductG) + ge_balance_positive_prefix_exists_resultproductGvalue))))))))) /\ (exists sto_ap_prefix_exists_resultproductvalue sto_an_prefix_exists_resultproductvalue sto_bp_prefix_exists_resultproductvalue sto_bn_prefix_exists_resultproductvalue sto_cp_prefix_exists_resultproductvalue sto_cn_prefix_exists_resultproductvalue. (((((scp_flat_first_prefix_exists_resultproduct) = 2 * (sto_ap_prefix_exists_resultproductvalue) /\ (sto_an_prefix_exists_resultproductvalue) = 0) \/ exists ge_signed_half_prefix_exists_resultproductvalueleft. (((scp_flat_first_prefix_exists_resultproduct) = 2 * ge_signed_half_prefix_exists_resultproductvalueleft + 1 /\ (sto_ap_prefix_exists_resultproductvalue) = 0) /\ (sto_an_prefix_exists_resultproductvalue) = S ge_signed_half_prefix_exists_resultproductvalueleft))) /\ ((((((scp_flat_second_prefix_exists_resultproduct) = 2 * (sto_bp_prefix_exists_resultproductvalue) /\ (sto_bn_prefix_exists_resultproductvalue) = 0) \/ exists ge_signed_half_prefix_exists_resultproductvalueright. (((scp_flat_second_prefix_exists_resultproduct) = 2 * ge_signed_half_prefix_exists_resultproductvalueright + 1 /\ (sto_bp_prefix_exists_resultproductvalue) = 0) /\ (sto_bn_prefix_exists_resultproductvalue) = S ge_signed_half_prefix_exists_resultproductvalueright))) /\ ((((((scp_flat_value_prefix_exists_result) = 2 * (sto_cp_prefix_exists_resultproductvalue) /\ (sto_cn_prefix_exists_resultproductvalue) = 0) \/ exists ge_signed_half_prefix_exists_resultproductvalueoutput. (((scp_flat_value_prefix_exists_result) = 2 * ge_signed_half_prefix_exists_resultproductvalueoutput + 1 /\ (sto_cp_prefix_exists_resultproductvalue) = 0) /\ (sto_cn_prefix_exists_resultproductvalue) = S ge_signed_half_prefix_exists_resultproductvalueoutput))) /\ ((sto_ap_prefix_exists_resultproductvalue * sto_bp_prefix_exists_resultproductvalue + sto_an_prefix_exists_resultproductvalue * sto_bn_prefix_exists_resultproductvalue) + sto_cn_prefix_exists_resultproductvalue = (sto_ap_prefix_exists_resultproductvalue * sto_bn_prefix_exists_resultproductvalue + sto_an_prefix_exists_resultproductvalue * sto_bp_prefix_exists_resultproductvalue) + sto_cp_prefix_exists_resultproductvalue))))))))))))))))))Constructive proof overview
Generated structural guide
Ordinary induction constructs the entire actual finite flattened product prefix; no finite-choice or output-table oracle is supplied.
The unchanged tactic script uses 4 declared prerequisites and contains 66 exact native proof lines.
Alpha v34 checked-use · first admitted v32 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
MX001F signed_cartesian_flat_entry_exists arithmetic_signed_table_singleton Alpha theorem; checked-use authorized MX0021 signed_cartesian_flat_prefix_zero MX0022 signed_cartesian_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–4
02Induction on lL5–8
03Establish hvL9–17
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed cartesian flat entry exists.
04Separate the logical casesL18–18
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L18
cases hv
05Establish htL19–21
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply arithmetic signed table singleton.
- L19
have ht : ∃ T. ArithTable(0,T) ∧ ArithAt(T,0,x)Definitions: ArithTableArithAt - L20
specialize arithmetic_signed_table_singleton (x) - L21
apply arithmetic_signed_table_singleton
06Separate the logical casesL22–23
07Construct an explicit witnessL24–24
Supply the displayed value, then prove that it has the required property.
- L24
exists x1
08Use earlier factsL25–33
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L25
specialize signed_cartesian_flat_prefix_zero (F) - L26
specialize signed_cartesian_flat_prefix_zero (G) - L27
specialize signed_cartesian_flat_prefix_zero (n) - L28
specialize signed_cartesian_flat_prefix_zero (x1) - L29
specialize signed_cartesian_flat_prefix_zero (x) - L30
apply signed_cartesian_flat_prefix_zero - L31
exact ht_witness_left - L32
exact ht_witness_right - L33
exact hv_witness
09Fix variables and assumptionsL34–36
10Establish hpL37–41
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.
11Separate the logical casesL42–42
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L42
cases hp
12Establish hvL43–51
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed cartesian flat entry exists.
13Separate the logical casesL52–52
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L52
cases hv
14Establish heL53–62
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed cartesian flat prefix append.
- L53
have he : ∃ U. ArithTable(S l,U) ∧ (∀ y. ∀ z. Le(y,S l) → ArithAt(U,y,z) → ∃ m. ∃ k. ∃ i. ∃ j. y = n · m + k ∧ (Lt(k,n) ∧ (ArithAt(F,m,i) ∧ (ArithAt(G,k,j) ∧ SignedMul(i,j,z))))) ∧ ArithTableEqual(x,U,S l)Definitions: SignedMulArithTableArithAtArithTableEqualLeLt - L54
specialize signed_cartesian_flat_prefix_append (F) - L55
specialize signed_cartesian_flat_prefix_append (G) - L56
specialize signed_cartesian_flat_prefix_append (n) - L57
specialize signed_cartesian_flat_prefix_append (l) - L58
specialize signed_cartesian_flat_prefix_append (x) - L59
specialize signed_cartesian_flat_prefix_append (x1) - L60
apply signed_cartesian_flat_prefix_append - L61
exact hp_witness - L62
exact hv_witness
15Separate the logical casesL63–64
16Construct an explicit witnessL65–65
Supply the displayed value, then prove that it has the required property.
- L65
exists x2
17Use earlier factsL66–66
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L66
exact he_witness_left
Original exact command ledger · 66 lines
- 0001
intro F - 0002
intro G - 0003
intro n - 0004
intro l - 0005
induction l - 0006
intro hF - 0007
intro hG - 0008
intro hn - 0009
have hv : exists z. (exists scp_flat_row_prefix_base_value scp_flat_column_prefix_base_value scp_flat_first_prefix_base_value scp_flat_second_prefix_base_value. (((0)=((n)*(scp_flat_row_prefix_base_value)+(scp_flat_column_prefix_base_value))) /\ (((exists pvs_gap_prefix_base_valueremainder. pvs_gap_prefix_base_valueremainder + S (scp_flat_column_prefix_base_value) = (n)) /\ (((exists dst_positive_code_prefix_base_valueF dst_positive_scale_prefix_base_valueF dst_negative_code_prefix_base_valueF dst_negative_scale_prefix_base_valueF dst_positive_prefix_base_valueF dst_negative_prefix_base_valueF. (((F) = (((((dst_positive_code_prefix_base_valueF) + (dst_positive_scale_prefix_base_valueF)) * S ((dst_positive_code_prefix_base_valueF) + (dst_positive_scale_prefix_base_valueF)) + ((dst_positive_scale_prefix_base_valueF) + (dst_positive_scale_prefix_base_valueF))) + (((dst_negative_code_prefix_base_valueF) + (dst_negative_scale_prefix_base_valueF)) * S ((dst_negative_code_prefix_base_valueF) + (dst_negative_scale_prefix_base_valueF)) + ((dst_negative_scale_prefix_base_valueF) + (dst_negative_scale_prefix_base_valueF)))) * S ((((dst_positive_code_prefix_base_valueF) + (dst_positive_scale_prefix_base_valueF)) * S ((dst_positive_code_prefix_base_valueF) + (dst_positive_scale_prefix_base_valueF)) + ((dst_positive_scale_prefix_base_valueF) + (dst_positive_scale_prefix_base_valueF))) + (((dst_negative_code_prefix_base_valueF) + (dst_negative_scale_prefix_base_valueF)) * S ((dst_negative_code_prefix_base_valueF) + (dst_negative_scale_prefix_base_valueF)) + ((dst_negative_scale_prefix_base_valueF) + (dst_negative_scale_prefix_base_valueF)))) + ((((dst_negative_code_prefix_base_valueF) + (dst_negative_scale_prefix_base_valueF)) * S ((dst_negative_code_prefix_base_valueF) + (dst_negative_scale_prefix_base_valueF)) + ((dst_negative_scale_prefix_base_valueF) + (dst_negative_scale_prefix_base_valueF))) + (((dst_negative_code_prefix_base_valueF) + (dst_negative_scale_prefix_base_valueF)) * S ((dst_negative_code_prefix_base_valueF) + (dst_negative_scale_prefix_base_valueF)) + ((dst_negative_scale_prefix_base_valueF) + (dst_negative_scale_prefix_base_valueF)))))) /\ (((((exists ff_h_pvs_prefix_base_valueFpositive. ff_h_pvs_prefix_base_valueFpositive + S (dst_positive_prefix_base_valueF) = S ((S (scp_flat_row_prefix_base_value)) * dst_positive_scale_prefix_base_valueF)) /\ exists ff_q_pvs_prefix_base_valueFpositive. dst_positive_code_prefix_base_valueF = ff_q_pvs_prefix_base_valueFpositive * S ((S (scp_flat_row_prefix_base_value)) * dst_positive_scale_prefix_base_valueF) + (dst_positive_prefix_base_valueF))) /\ (((((exists ff_h_pvs_prefix_base_valueFnegative. ff_h_pvs_prefix_base_valueFnegative + S (dst_negative_prefix_base_valueF) = S ((S (scp_flat_row_prefix_base_value)) * dst_negative_scale_prefix_base_valueF)) /\ exists ff_q_pvs_prefix_base_valueFnegative. dst_negative_code_prefix_base_valueF = ff_q_pvs_prefix_base_valueFnegative * S ((S (scp_flat_row_prefix_base_value)) * dst_negative_scale_prefix_base_valueF) + (dst_negative_prefix_base_valueF))) /\ (exists ge_balance_positive_prefix_base_valueFvalue ge_balance_negative_prefix_base_valueFvalue. (((((scp_flat_first_prefix_base_value) = 2 * (ge_balance_positive_prefix_base_valueFvalue) /\ (ge_balance_negative_prefix_base_valueFvalue) = 0) \/ exists ge_signed_half_prefix_base_valueFvaluedecode. (((scp_flat_first_prefix_base_value) = 2 * ge_signed_half_prefix_base_valueFvaluedecode + 1 /\ (ge_balance_positive_prefix_base_valueFvalue) = 0) /\ (ge_balance_negative_prefix_base_valueFvalue) = S ge_signed_half_prefix_base_valueFvaluedecode))) /\ ((dst_positive_prefix_base_valueF) + ge_balance_negative_prefix_base_valueFvalue = (dst_negative_prefix_base_valueF) + ge_balance_positive_prefix_base_valueFvalue))))))))) /\ (((exists dst_positive_code_prefix_base_valueG dst_positive_scale_prefix_base_valueG dst_negative_code_prefix_base_valueG dst_negative_scale_prefix_base_valueG dst_positive_prefix_base_valueG dst_negative_prefix_base_valueG. (((G) = (((((dst_positive_code_prefix_base_valueG) + (dst_positive_scale_prefix_base_valueG)) * S ((dst_positive_code_prefix_base_valueG) + (dst_positive_scale_prefix_base_valueG)) + ((dst_positive_scale_prefix_base_valueG) + (dst_positive_scale_prefix_base_valueG))) + (((dst_negative_code_prefix_base_valueG) + (dst_negative_scale_prefix_base_valueG)) * S ((dst_negative_code_prefix_base_valueG) + (dst_negative_scale_prefix_base_valueG)) + ((dst_negative_scale_prefix_base_valueG) + (dst_negative_scale_prefix_base_valueG)))) * S ((((dst_positive_code_prefix_base_valueG) + (dst_positive_scale_prefix_base_valueG)) * S ((dst_positive_code_prefix_base_valueG) + (dst_positive_scale_prefix_base_valueG)) + ((dst_positive_scale_prefix_base_valueG) + (dst_positive_scale_prefix_base_valueG))) + (((dst_negative_code_prefix_base_valueG) + (dst_negative_scale_prefix_base_valueG)) * S ((dst_negative_code_prefix_base_valueG) + (dst_negative_scale_prefix_base_valueG)) + ((dst_negative_scale_prefix_base_valueG) + (dst_negative_scale_prefix_base_valueG)))) + ((((dst_negative_code_prefix_base_valueG) + (dst_negative_scale_prefix_base_valueG)) * S ((dst_negative_code_prefix_base_valueG) + (dst_negative_scale_prefix_base_valueG)) + ((dst_negative_scale_prefix_base_valueG) + (dst_negative_scale_prefix_base_valueG))) + (((dst_negative_code_prefix_base_valueG) + (dst_negative_scale_prefix_base_valueG)) * S ((dst_negative_code_prefix_base_valueG) + (dst_negative_scale_prefix_base_valueG)) + ((dst_negative_scale_prefix_base_valueG) + (dst_negative_scale_prefix_base_valueG)))))) /\ (((((exists ff_h_pvs_prefix_base_valueGpositive. ff_h_pvs_prefix_base_valueGpositive + S (dst_positive_prefix_base_valueG) = S ((S (scp_flat_column_prefix_base_value)) * dst_positive_scale_prefix_base_valueG)) /\ exists ff_q_pvs_prefix_base_valueGpositive. dst_positive_code_prefix_base_valueG = ff_q_pvs_prefix_base_valueGpositive * S ((S (scp_flat_column_prefix_base_value)) * dst_positive_scale_prefix_base_valueG) + (dst_positive_prefix_base_valueG))) /\ (((((exists ff_h_pvs_prefix_base_valueGnegative. ff_h_pvs_prefix_base_valueGnegative + S (dst_negative_prefix_base_valueG) = S ((S (scp_flat_column_prefix_base_value)) * dst_negative_scale_prefix_base_valueG)) /\ exists ff_q_pvs_prefix_base_valueGnegative. dst_negative_code_prefix_base_valueG = ff_q_pvs_prefix_base_valueGnegative * S ((S (scp_flat_column_prefix_base_value)) * dst_negative_scale_prefix_base_valueG) + (dst_negative_prefix_base_valueG))) /\ (exists ge_balance_positive_prefix_base_valueGvalue ge_balance_negative_prefix_base_valueGvalue. (((((scp_flat_second_prefix_base_value) = 2 * (ge_balance_positive_prefix_base_valueGvalue) /\ (ge_balance_negative_prefix_base_valueGvalue) = 0) \/ exists ge_signed_half_prefix_base_valueGvaluedecode. (((scp_flat_second_prefix_base_value) = 2 * ge_signed_half_prefix_base_valueGvaluedecode + 1 /\ (ge_balance_positive_prefix_base_valueGvalue) = 0) /\ (ge_balance_negative_prefix_base_valueGvalue) = S ge_signed_half_prefix_base_valueGvaluedecode))) /\ ((dst_positive_prefix_base_valueG) + ge_balance_negative_prefix_base_valueGvalue = (dst_negative_prefix_base_valueG) + ge_balance_positive_prefix_base_valueGvalue))))))))) /\ (exists sto_ap_prefix_base_valuevalue sto_an_prefix_base_valuevalue sto_bp_prefix_base_valuevalue sto_bn_prefix_base_valuevalue sto_cp_prefix_base_valuevalue sto_cn_prefix_base_valuevalue. (((((scp_flat_first_prefix_base_value) = 2 * (sto_ap_prefix_base_valuevalue) /\ (sto_an_prefix_base_valuevalue) = 0) \/ exists ge_signed_half_prefix_base_valuevalueleft. (((scp_flat_first_prefix_base_value) = 2 * ge_signed_half_prefix_base_valuevalueleft + 1 /\ (sto_ap_prefix_base_valuevalue) = 0) /\ (sto_an_prefix_base_valuevalue) = S ge_signed_half_prefix_base_valuevalueleft))) /\ ((((((scp_flat_second_prefix_base_value) = 2 * (sto_bp_prefix_base_valuevalue) /\ (sto_bn_prefix_base_valuevalue) = 0) \/ exists ge_signed_half_prefix_base_valuevalueright. (((scp_flat_second_prefix_base_value) = 2 * ge_signed_half_prefix_base_valuevalueright + 1 /\ (sto_bp_prefix_base_valuevalue) = 0) /\ (sto_bn_prefix_base_valuevalue) = S ge_signed_half_prefix_base_valuevalueright))) /\ ((((((z) = 2 * (sto_cp_prefix_base_valuevalue) /\ (sto_cn_prefix_base_valuevalue) = 0) \/ exists ge_signed_half_prefix_base_valuevalueoutput. (((z) = 2 * ge_signed_half_prefix_base_valuevalueoutput + 1 /\ (sto_cp_prefix_base_valuevalue) = 0) /\ (sto_cn_prefix_base_valuevalue) = S ge_signed_half_prefix_base_valuevalueoutput))) /\ ((sto_ap_prefix_base_valuevalue * sto_bp_prefix_base_valuevalue + sto_an_prefix_base_valuevalue * sto_bn_prefix_base_valuevalue) + sto_cn_prefix_base_valuevalue = (sto_ap_prefix_base_valuevalue * sto_bn_prefix_base_valuevalue + sto_an_prefix_base_valuevalue * sto_bp_prefix_base_valuevalue) + sto_cp_prefix_base_valuevalue))))))))))))))) - 0010
specialize signed_cartesian_flat_entry_exists (F) - 0011
specialize signed_cartesian_flat_entry_exists (G) - 0012
specialize signed_cartesian_flat_entry_exists (n) - 0013
specialize signed_cartesian_flat_entry_exists (0) - 0014
apply signed_cartesian_flat_entry_exists - 0015
exact hF - 0016
exact hG - 0017
exact hn - 0018
cases hv - 0019
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))))))))))) - 0020
specialize arithmetic_signed_table_singleton (x) - 0021
apply arithmetic_signed_table_singleton - 0022
cases ht - 0023
cases ht_witness - 0024
exists x1 - 0025
specialize signed_cartesian_flat_prefix_zero (F) - 0026
specialize signed_cartesian_flat_prefix_zero (G) - 0027
specialize signed_cartesian_flat_prefix_zero (n) - 0028
specialize signed_cartesian_flat_prefix_zero (x1) - 0029
specialize signed_cartesian_flat_prefix_zero (x) - 0030
apply signed_cartesian_flat_prefix_zero - 0031
exact ht_witness_left - 0032
exact ht_witness_right - 0033
exact hv_witness - 0034
intro hF - 0035
intro hG - 0036
intro hn - 0037
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 scp_flat_index_prefix_previous scp_flat_value_prefix_previous. (exists pvs_le_gap_prefix_previousbound. pvs_le_gap_prefix_previousbound + (scp_flat_index_prefix_previous) = (l)) -> (exists dst_positive_code_prefix_previousentry dst_positive_scale_prefix_previousentry dst_negative_code_prefix_previousentry dst_negative_scale_prefix_previousentry dst_positive_prefix_previousentry dst_negative_prefix_previousentry. (((T) = (((((dst_positive_code_prefix_previousentry) + (dst_positive_scale_prefix_previousentry)) * S ((dst_positive_code_prefix_previousentry) + (dst_positive_scale_prefix_previousentry)) + ((dst_positive_scale_prefix_previousentry) + (dst_positive_scale_prefix_previousentry))) + (((dst_negative_code_prefix_previousentry) + (dst_negative_scale_prefix_previousentry)) * S ((dst_negative_code_prefix_previousentry) + (dst_negative_scale_prefix_previousentry)) + ((dst_negative_scale_prefix_previousentry) + (dst_negative_scale_prefix_previousentry)))) * S ((((dst_positive_code_prefix_previousentry) + (dst_positive_scale_prefix_previousentry)) * S ((dst_positive_code_prefix_previousentry) + (dst_positive_scale_prefix_previousentry)) + ((dst_positive_scale_prefix_previousentry) + (dst_positive_scale_prefix_previousentry))) + (((dst_negative_code_prefix_previousentry) + (dst_negative_scale_prefix_previousentry)) * S ((dst_negative_code_prefix_previousentry) + (dst_negative_scale_prefix_previousentry)) + ((dst_negative_scale_prefix_previousentry) + (dst_negative_scale_prefix_previousentry)))) + ((((dst_negative_code_prefix_previousentry) + (dst_negative_scale_prefix_previousentry)) * S ((dst_negative_code_prefix_previousentry) + (dst_negative_scale_prefix_previousentry)) + ((dst_negative_scale_prefix_previousentry) + (dst_negative_scale_prefix_previousentry))) + (((dst_negative_code_prefix_previousentry) + (dst_negative_scale_prefix_previousentry)) * S ((dst_negative_code_prefix_previousentry) + (dst_negative_scale_prefix_previousentry)) + ((dst_negative_scale_prefix_previousentry) + (dst_negative_scale_prefix_previousentry)))))) /\ (((((exists ff_h_pvs_prefix_previousentrypositive. ff_h_pvs_prefix_previousentrypositive + S (dst_positive_prefix_previousentry) = S ((S (scp_flat_index_prefix_previous)) * dst_positive_scale_prefix_previousentry)) /\ exists ff_q_pvs_prefix_previousentrypositive. dst_positive_code_prefix_previousentry = ff_q_pvs_prefix_previousentrypositive * S ((S (scp_flat_index_prefix_previous)) * dst_positive_scale_prefix_previousentry) + (dst_positive_prefix_previousentry))) /\ (((((exists ff_h_pvs_prefix_previousentrynegative. ff_h_pvs_prefix_previousentrynegative + S (dst_negative_prefix_previousentry) = S ((S (scp_flat_index_prefix_previous)) * dst_negative_scale_prefix_previousentry)) /\ exists ff_q_pvs_prefix_previousentrynegative. dst_negative_code_prefix_previousentry = ff_q_pvs_prefix_previousentrynegative * S ((S (scp_flat_index_prefix_previous)) * dst_negative_scale_prefix_previousentry) + (dst_negative_prefix_previousentry))) /\ (exists ge_balance_positive_prefix_previousentryvalue ge_balance_negative_prefix_previousentryvalue. (((((scp_flat_value_prefix_previous) = 2 * (ge_balance_positive_prefix_previousentryvalue) /\ (ge_balance_negative_prefix_previousentryvalue) = 0) \/ exists ge_signed_half_prefix_previousentryvaluedecode. (((scp_flat_value_prefix_previous) = 2 * ge_signed_half_prefix_previousentryvaluedecode + 1 /\ (ge_balance_positive_prefix_previousentryvalue) = 0) /\ (ge_balance_negative_prefix_previousentryvalue) = S ge_signed_half_prefix_previousentryvaluedecode))) /\ ((dst_positive_prefix_previousentry) + ge_balance_negative_prefix_previousentryvalue = (dst_negative_prefix_previousentry) + ge_balance_positive_prefix_previousentryvalue))))))))) -> (exists scp_flat_row_prefix_previousproduct scp_flat_column_prefix_previousproduct scp_flat_first_prefix_previousproduct scp_flat_second_prefix_previousproduct. (((scp_flat_index_prefix_previous)=((n)*(scp_flat_row_prefix_previousproduct)+(scp_flat_column_prefix_previousproduct))) /\ (((exists pvs_gap_prefix_previousproductremainder. pvs_gap_prefix_previousproductremainder + S (scp_flat_column_prefix_previousproduct) = (n)) /\ (((exists dst_positive_code_prefix_previousproductF dst_positive_scale_prefix_previousproductF dst_negative_code_prefix_previousproductF dst_negative_scale_prefix_previousproductF dst_positive_prefix_previousproductF dst_negative_prefix_previousproductF. (((F) = (((((dst_positive_code_prefix_previousproductF) + (dst_positive_scale_prefix_previousproductF)) * S ((dst_positive_code_prefix_previousproductF) + (dst_positive_scale_prefix_previousproductF)) + ((dst_positive_scale_prefix_previousproductF) + (dst_positive_scale_prefix_previousproductF))) + (((dst_negative_code_prefix_previousproductF) + (dst_negative_scale_prefix_previousproductF)) * S ((dst_negative_code_prefix_previousproductF) + (dst_negative_scale_prefix_previousproductF)) + ((dst_negative_scale_prefix_previousproductF) + (dst_negative_scale_prefix_previousproductF)))) * S ((((dst_positive_code_prefix_previousproductF) + (dst_positive_scale_prefix_previousproductF)) * S ((dst_positive_code_prefix_previousproductF) + (dst_positive_scale_prefix_previousproductF)) + ((dst_positive_scale_prefix_previousproductF) + (dst_positive_scale_prefix_previousproductF))) + (((dst_negative_code_prefix_previousproductF) + (dst_negative_scale_prefix_previousproductF)) * S ((dst_negative_code_prefix_previousproductF) + (dst_negative_scale_prefix_previousproductF)) + ((dst_negative_scale_prefix_previousproductF) + (dst_negative_scale_prefix_previousproductF)))) + ((((dst_negative_code_prefix_previousproductF) + (dst_negative_scale_prefix_previousproductF)) * S ((dst_negative_code_prefix_previousproductF) + (dst_negative_scale_prefix_previousproductF)) + ((dst_negative_scale_prefix_previousproductF) + (dst_negative_scale_prefix_previousproductF))) + (((dst_negative_code_prefix_previousproductF) + (dst_negative_scale_prefix_previousproductF)) * S ((dst_negative_code_prefix_previousproductF) + (dst_negative_scale_prefix_previousproductF)) + ((dst_negative_scale_prefix_previousproductF) + (dst_negative_scale_prefix_previousproductF)))))) /\ (((((exists ff_h_pvs_prefix_previousproductFpositive. ff_h_pvs_prefix_previousproductFpositive + S (dst_positive_prefix_previousproductF) = S ((S (scp_flat_row_prefix_previousproduct)) * dst_positive_scale_prefix_previousproductF)) /\ exists ff_q_pvs_prefix_previousproductFpositive. dst_positive_code_prefix_previousproductF = ff_q_pvs_prefix_previousproductFpositive * S ((S (scp_flat_row_prefix_previousproduct)) * dst_positive_scale_prefix_previousproductF) + (dst_positive_prefix_previousproductF))) /\ (((((exists ff_h_pvs_prefix_previousproductFnegative. ff_h_pvs_prefix_previousproductFnegative + S (dst_negative_prefix_previousproductF) = S ((S (scp_flat_row_prefix_previousproduct)) * dst_negative_scale_prefix_previousproductF)) /\ exists ff_q_pvs_prefix_previousproductFnegative. dst_negative_code_prefix_previousproductF = ff_q_pvs_prefix_previousproductFnegative * S ((S (scp_flat_row_prefix_previousproduct)) * dst_negative_scale_prefix_previousproductF) + (dst_negative_prefix_previousproductF))) /\ (exists ge_balance_positive_prefix_previousproductFvalue ge_balance_negative_prefix_previousproductFvalue. (((((scp_flat_first_prefix_previousproduct) = 2 * (ge_balance_positive_prefix_previousproductFvalue) /\ (ge_balance_negative_prefix_previousproductFvalue) = 0) \/ exists ge_signed_half_prefix_previousproductFvaluedecode. (((scp_flat_first_prefix_previousproduct) = 2 * ge_signed_half_prefix_previousproductFvaluedecode + 1 /\ (ge_balance_positive_prefix_previousproductFvalue) = 0) /\ (ge_balance_negative_prefix_previousproductFvalue) = S ge_signed_half_prefix_previousproductFvaluedecode))) /\ ((dst_positive_prefix_previousproductF) + ge_balance_negative_prefix_previousproductFvalue = (dst_negative_prefix_previousproductF) + ge_balance_positive_prefix_previousproductFvalue))))))))) /\ (((exists dst_positive_code_prefix_previousproductG dst_positive_scale_prefix_previousproductG dst_negative_code_prefix_previousproductG dst_negative_scale_prefix_previousproductG dst_positive_prefix_previousproductG dst_negative_prefix_previousproductG. (((G) = (((((dst_positive_code_prefix_previousproductG) + (dst_positive_scale_prefix_previousproductG)) * S ((dst_positive_code_prefix_previousproductG) + (dst_positive_scale_prefix_previousproductG)) + ((dst_positive_scale_prefix_previousproductG) + (dst_positive_scale_prefix_previousproductG))) + (((dst_negative_code_prefix_previousproductG) + (dst_negative_scale_prefix_previousproductG)) * S ((dst_negative_code_prefix_previousproductG) + (dst_negative_scale_prefix_previousproductG)) + ((dst_negative_scale_prefix_previousproductG) + (dst_negative_scale_prefix_previousproductG)))) * S ((((dst_positive_code_prefix_previousproductG) + (dst_positive_scale_prefix_previousproductG)) * S ((dst_positive_code_prefix_previousproductG) + (dst_positive_scale_prefix_previousproductG)) + ((dst_positive_scale_prefix_previousproductG) + (dst_positive_scale_prefix_previousproductG))) + (((dst_negative_code_prefix_previousproductG) + (dst_negative_scale_prefix_previousproductG)) * S ((dst_negative_code_prefix_previousproductG) + (dst_negative_scale_prefix_previousproductG)) + ((dst_negative_scale_prefix_previousproductG) + (dst_negative_scale_prefix_previousproductG)))) + ((((dst_negative_code_prefix_previousproductG) + (dst_negative_scale_prefix_previousproductG)) * S ((dst_negative_code_prefix_previousproductG) + (dst_negative_scale_prefix_previousproductG)) + ((dst_negative_scale_prefix_previousproductG) + (dst_negative_scale_prefix_previousproductG))) + (((dst_negative_code_prefix_previousproductG) + (dst_negative_scale_prefix_previousproductG)) * S ((dst_negative_code_prefix_previousproductG) + (dst_negative_scale_prefix_previousproductG)) + ((dst_negative_scale_prefix_previousproductG) + (dst_negative_scale_prefix_previousproductG)))))) /\ (((((exists ff_h_pvs_prefix_previousproductGpositive. ff_h_pvs_prefix_previousproductGpositive + S (dst_positive_prefix_previousproductG) = S ((S (scp_flat_column_prefix_previousproduct)) * dst_positive_scale_prefix_previousproductG)) /\ exists ff_q_pvs_prefix_previousproductGpositive. dst_positive_code_prefix_previousproductG = ff_q_pvs_prefix_previousproductGpositive * S ((S (scp_flat_column_prefix_previousproduct)) * dst_positive_scale_prefix_previousproductG) + (dst_positive_prefix_previousproductG))) /\ (((((exists ff_h_pvs_prefix_previousproductGnegative. ff_h_pvs_prefix_previousproductGnegative + S (dst_negative_prefix_previousproductG) = S ((S (scp_flat_column_prefix_previousproduct)) * dst_negative_scale_prefix_previousproductG)) /\ exists ff_q_pvs_prefix_previousproductGnegative. dst_negative_code_prefix_previousproductG = ff_q_pvs_prefix_previousproductGnegative * S ((S (scp_flat_column_prefix_previousproduct)) * dst_negative_scale_prefix_previousproductG) + (dst_negative_prefix_previousproductG))) /\ (exists ge_balance_positive_prefix_previousproductGvalue ge_balance_negative_prefix_previousproductGvalue. (((((scp_flat_second_prefix_previousproduct) = 2 * (ge_balance_positive_prefix_previousproductGvalue) /\ (ge_balance_negative_prefix_previousproductGvalue) = 0) \/ exists ge_signed_half_prefix_previousproductGvaluedecode. (((scp_flat_second_prefix_previousproduct) = 2 * ge_signed_half_prefix_previousproductGvaluedecode + 1 /\ (ge_balance_positive_prefix_previousproductGvalue) = 0) /\ (ge_balance_negative_prefix_previousproductGvalue) = S ge_signed_half_prefix_previousproductGvaluedecode))) /\ ((dst_positive_prefix_previousproductG) + ge_balance_negative_prefix_previousproductGvalue = (dst_negative_prefix_previousproductG) + ge_balance_positive_prefix_previousproductGvalue))))))))) /\ (exists sto_ap_prefix_previousproductvalue sto_an_prefix_previousproductvalue sto_bp_prefix_previousproductvalue sto_bn_prefix_previousproductvalue sto_cp_prefix_previousproductvalue sto_cn_prefix_previousproductvalue. (((((scp_flat_first_prefix_previousproduct) = 2 * (sto_ap_prefix_previousproductvalue) /\ (sto_an_prefix_previousproductvalue) = 0) \/ exists ge_signed_half_prefix_previousproductvalueleft. (((scp_flat_first_prefix_previousproduct) = 2 * ge_signed_half_prefix_previousproductvalueleft + 1 /\ (sto_ap_prefix_previousproductvalue) = 0) /\ (sto_an_prefix_previousproductvalue) = S ge_signed_half_prefix_previousproductvalueleft))) /\ ((((((scp_flat_second_prefix_previousproduct) = 2 * (sto_bp_prefix_previousproductvalue) /\ (sto_bn_prefix_previousproductvalue) = 0) \/ exists ge_signed_half_prefix_previousproductvalueright. (((scp_flat_second_prefix_previousproduct) = 2 * ge_signed_half_prefix_previousproductvalueright + 1 /\ (sto_bp_prefix_previousproductvalue) = 0) /\ (sto_bn_prefix_previousproductvalue) = S ge_signed_half_prefix_previousproductvalueright))) /\ ((((((scp_flat_value_prefix_previous) = 2 * (sto_cp_prefix_previousproductvalue) /\ (sto_cn_prefix_previousproductvalue) = 0) \/ exists ge_signed_half_prefix_previousproductvalueoutput. (((scp_flat_value_prefix_previous) = 2 * ge_signed_half_prefix_previousproductvalueoutput + 1 /\ (sto_cp_prefix_previousproductvalue) = 0) /\ (sto_cn_prefix_previousproductvalue) = S ge_signed_half_prefix_previousproductvalueoutput))) /\ ((sto_ap_prefix_previousproductvalue * sto_bp_prefix_previousproductvalue + sto_an_prefix_previousproductvalue * sto_bn_prefix_previousproductvalue) + sto_cn_prefix_previousproductvalue = (sto_ap_prefix_previousproductvalue * sto_bn_prefix_previousproductvalue + sto_an_prefix_previousproductvalue * sto_bp_prefix_previousproductvalue) + sto_cp_prefix_previousproductvalue)))))))))))))))))) - 0038
apply IH - 0039
exact hF - 0040
exact hG - 0041
exact hn - 0042
cases hp - 0043
have hv : exists z. (exists scp_flat_row_prefix_next_value scp_flat_column_prefix_next_value scp_flat_first_prefix_next_value scp_flat_second_prefix_next_value. (((S l)=((n)*(scp_flat_row_prefix_next_value)+(scp_flat_column_prefix_next_value))) /\ (((exists pvs_gap_prefix_next_valueremainder. pvs_gap_prefix_next_valueremainder + S (scp_flat_column_prefix_next_value) = (n)) /\ (((exists dst_positive_code_prefix_next_valueF dst_positive_scale_prefix_next_valueF dst_negative_code_prefix_next_valueF dst_negative_scale_prefix_next_valueF dst_positive_prefix_next_valueF dst_negative_prefix_next_valueF. (((F) = (((((dst_positive_code_prefix_next_valueF) + (dst_positive_scale_prefix_next_valueF)) * S ((dst_positive_code_prefix_next_valueF) + (dst_positive_scale_prefix_next_valueF)) + ((dst_positive_scale_prefix_next_valueF) + (dst_positive_scale_prefix_next_valueF))) + (((dst_negative_code_prefix_next_valueF) + (dst_negative_scale_prefix_next_valueF)) * S ((dst_negative_code_prefix_next_valueF) + (dst_negative_scale_prefix_next_valueF)) + ((dst_negative_scale_prefix_next_valueF) + (dst_negative_scale_prefix_next_valueF)))) * S ((((dst_positive_code_prefix_next_valueF) + (dst_positive_scale_prefix_next_valueF)) * S ((dst_positive_code_prefix_next_valueF) + (dst_positive_scale_prefix_next_valueF)) + ((dst_positive_scale_prefix_next_valueF) + (dst_positive_scale_prefix_next_valueF))) + (((dst_negative_code_prefix_next_valueF) + (dst_negative_scale_prefix_next_valueF)) * S ((dst_negative_code_prefix_next_valueF) + (dst_negative_scale_prefix_next_valueF)) + ((dst_negative_scale_prefix_next_valueF) + (dst_negative_scale_prefix_next_valueF)))) + ((((dst_negative_code_prefix_next_valueF) + (dst_negative_scale_prefix_next_valueF)) * S ((dst_negative_code_prefix_next_valueF) + (dst_negative_scale_prefix_next_valueF)) + ((dst_negative_scale_prefix_next_valueF) + (dst_negative_scale_prefix_next_valueF))) + (((dst_negative_code_prefix_next_valueF) + (dst_negative_scale_prefix_next_valueF)) * S ((dst_negative_code_prefix_next_valueF) + (dst_negative_scale_prefix_next_valueF)) + ((dst_negative_scale_prefix_next_valueF) + (dst_negative_scale_prefix_next_valueF)))))) /\ (((((exists ff_h_pvs_prefix_next_valueFpositive. ff_h_pvs_prefix_next_valueFpositive + S (dst_positive_prefix_next_valueF) = S ((S (scp_flat_row_prefix_next_value)) * dst_positive_scale_prefix_next_valueF)) /\ exists ff_q_pvs_prefix_next_valueFpositive. dst_positive_code_prefix_next_valueF = ff_q_pvs_prefix_next_valueFpositive * S ((S (scp_flat_row_prefix_next_value)) * dst_positive_scale_prefix_next_valueF) + (dst_positive_prefix_next_valueF))) /\ (((((exists ff_h_pvs_prefix_next_valueFnegative. ff_h_pvs_prefix_next_valueFnegative + S (dst_negative_prefix_next_valueF) = S ((S (scp_flat_row_prefix_next_value)) * dst_negative_scale_prefix_next_valueF)) /\ exists ff_q_pvs_prefix_next_valueFnegative. dst_negative_code_prefix_next_valueF = ff_q_pvs_prefix_next_valueFnegative * S ((S (scp_flat_row_prefix_next_value)) * dst_negative_scale_prefix_next_valueF) + (dst_negative_prefix_next_valueF))) /\ (exists ge_balance_positive_prefix_next_valueFvalue ge_balance_negative_prefix_next_valueFvalue. (((((scp_flat_first_prefix_next_value) = 2 * (ge_balance_positive_prefix_next_valueFvalue) /\ (ge_balance_negative_prefix_next_valueFvalue) = 0) \/ exists ge_signed_half_prefix_next_valueFvaluedecode. (((scp_flat_first_prefix_next_value) = 2 * ge_signed_half_prefix_next_valueFvaluedecode + 1 /\ (ge_balance_positive_prefix_next_valueFvalue) = 0) /\ (ge_balance_negative_prefix_next_valueFvalue) = S ge_signed_half_prefix_next_valueFvaluedecode))) /\ ((dst_positive_prefix_next_valueF) + ge_balance_negative_prefix_next_valueFvalue = (dst_negative_prefix_next_valueF) + ge_balance_positive_prefix_next_valueFvalue))))))))) /\ (((exists dst_positive_code_prefix_next_valueG dst_positive_scale_prefix_next_valueG dst_negative_code_prefix_next_valueG dst_negative_scale_prefix_next_valueG dst_positive_prefix_next_valueG dst_negative_prefix_next_valueG. (((G) = (((((dst_positive_code_prefix_next_valueG) + (dst_positive_scale_prefix_next_valueG)) * S ((dst_positive_code_prefix_next_valueG) + (dst_positive_scale_prefix_next_valueG)) + ((dst_positive_scale_prefix_next_valueG) + (dst_positive_scale_prefix_next_valueG))) + (((dst_negative_code_prefix_next_valueG) + (dst_negative_scale_prefix_next_valueG)) * S ((dst_negative_code_prefix_next_valueG) + (dst_negative_scale_prefix_next_valueG)) + ((dst_negative_scale_prefix_next_valueG) + (dst_negative_scale_prefix_next_valueG)))) * S ((((dst_positive_code_prefix_next_valueG) + (dst_positive_scale_prefix_next_valueG)) * S ((dst_positive_code_prefix_next_valueG) + (dst_positive_scale_prefix_next_valueG)) + ((dst_positive_scale_prefix_next_valueG) + (dst_positive_scale_prefix_next_valueG))) + (((dst_negative_code_prefix_next_valueG) + (dst_negative_scale_prefix_next_valueG)) * S ((dst_negative_code_prefix_next_valueG) + (dst_negative_scale_prefix_next_valueG)) + ((dst_negative_scale_prefix_next_valueG) + (dst_negative_scale_prefix_next_valueG)))) + ((((dst_negative_code_prefix_next_valueG) + (dst_negative_scale_prefix_next_valueG)) * S ((dst_negative_code_prefix_next_valueG) + (dst_negative_scale_prefix_next_valueG)) + ((dst_negative_scale_prefix_next_valueG) + (dst_negative_scale_prefix_next_valueG))) + (((dst_negative_code_prefix_next_valueG) + (dst_negative_scale_prefix_next_valueG)) * S ((dst_negative_code_prefix_next_valueG) + (dst_negative_scale_prefix_next_valueG)) + ((dst_negative_scale_prefix_next_valueG) + (dst_negative_scale_prefix_next_valueG)))))) /\ (((((exists ff_h_pvs_prefix_next_valueGpositive. ff_h_pvs_prefix_next_valueGpositive + S (dst_positive_prefix_next_valueG) = S ((S (scp_flat_column_prefix_next_value)) * dst_positive_scale_prefix_next_valueG)) /\ exists ff_q_pvs_prefix_next_valueGpositive. dst_positive_code_prefix_next_valueG = ff_q_pvs_prefix_next_valueGpositive * S ((S (scp_flat_column_prefix_next_value)) * dst_positive_scale_prefix_next_valueG) + (dst_positive_prefix_next_valueG))) /\ (((((exists ff_h_pvs_prefix_next_valueGnegative. ff_h_pvs_prefix_next_valueGnegative + S (dst_negative_prefix_next_valueG) = S ((S (scp_flat_column_prefix_next_value)) * dst_negative_scale_prefix_next_valueG)) /\ exists ff_q_pvs_prefix_next_valueGnegative. dst_negative_code_prefix_next_valueG = ff_q_pvs_prefix_next_valueGnegative * S ((S (scp_flat_column_prefix_next_value)) * dst_negative_scale_prefix_next_valueG) + (dst_negative_prefix_next_valueG))) /\ (exists ge_balance_positive_prefix_next_valueGvalue ge_balance_negative_prefix_next_valueGvalue. (((((scp_flat_second_prefix_next_value) = 2 * (ge_balance_positive_prefix_next_valueGvalue) /\ (ge_balance_negative_prefix_next_valueGvalue) = 0) \/ exists ge_signed_half_prefix_next_valueGvaluedecode. (((scp_flat_second_prefix_next_value) = 2 * ge_signed_half_prefix_next_valueGvaluedecode + 1 /\ (ge_balance_positive_prefix_next_valueGvalue) = 0) /\ (ge_balance_negative_prefix_next_valueGvalue) = S ge_signed_half_prefix_next_valueGvaluedecode))) /\ ((dst_positive_prefix_next_valueG) + ge_balance_negative_prefix_next_valueGvalue = (dst_negative_prefix_next_valueG) + ge_balance_positive_prefix_next_valueGvalue))))))))) /\ (exists sto_ap_prefix_next_valuevalue sto_an_prefix_next_valuevalue sto_bp_prefix_next_valuevalue sto_bn_prefix_next_valuevalue sto_cp_prefix_next_valuevalue sto_cn_prefix_next_valuevalue. (((((scp_flat_first_prefix_next_value) = 2 * (sto_ap_prefix_next_valuevalue) /\ (sto_an_prefix_next_valuevalue) = 0) \/ exists ge_signed_half_prefix_next_valuevalueleft. (((scp_flat_first_prefix_next_value) = 2 * ge_signed_half_prefix_next_valuevalueleft + 1 /\ (sto_ap_prefix_next_valuevalue) = 0) /\ (sto_an_prefix_next_valuevalue) = S ge_signed_half_prefix_next_valuevalueleft))) /\ ((((((scp_flat_second_prefix_next_value) = 2 * (sto_bp_prefix_next_valuevalue) /\ (sto_bn_prefix_next_valuevalue) = 0) \/ exists ge_signed_half_prefix_next_valuevalueright. (((scp_flat_second_prefix_next_value) = 2 * ge_signed_half_prefix_next_valuevalueright + 1 /\ (sto_bp_prefix_next_valuevalue) = 0) /\ (sto_bn_prefix_next_valuevalue) = S ge_signed_half_prefix_next_valuevalueright))) /\ ((((((z) = 2 * (sto_cp_prefix_next_valuevalue) /\ (sto_cn_prefix_next_valuevalue) = 0) \/ exists ge_signed_half_prefix_next_valuevalueoutput. (((z) = 2 * ge_signed_half_prefix_next_valuevalueoutput + 1 /\ (sto_cp_prefix_next_valuevalue) = 0) /\ (sto_cn_prefix_next_valuevalue) = S ge_signed_half_prefix_next_valuevalueoutput))) /\ ((sto_ap_prefix_next_valuevalue * sto_bp_prefix_next_valuevalue + sto_an_prefix_next_valuevalue * sto_bn_prefix_next_valuevalue) + sto_cn_prefix_next_valuevalue = (sto_ap_prefix_next_valuevalue * sto_bn_prefix_next_valuevalue + sto_an_prefix_next_valuevalue * sto_bp_prefix_next_valuevalue) + sto_cp_prefix_next_valuevalue))))))))))))))) - 0044
specialize signed_cartesian_flat_entry_exists (F) - 0045
specialize signed_cartesian_flat_entry_exists (G) - 0046
specialize signed_cartesian_flat_entry_exists (n) - 0047
specialize signed_cartesian_flat_entry_exists (S l) - 0048
apply signed_cartesian_flat_entry_exists - 0049
exact hF - 0050
exact hG - 0051
exact hn - 0052
cases hv - 0053
have he : 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 scp_flat_index_prefix_next scp_flat_value_prefix_next. (exists pvs_le_gap_prefix_nextbound. pvs_le_gap_prefix_nextbound + (scp_flat_index_prefix_next) = (S l)) -> (exists dst_positive_code_prefix_nextentry dst_positive_scale_prefix_nextentry dst_negative_code_prefix_nextentry dst_negative_scale_prefix_nextentry dst_positive_prefix_nextentry dst_negative_prefix_nextentry. (((U) = (((((dst_positive_code_prefix_nextentry) + (dst_positive_scale_prefix_nextentry)) * S ((dst_positive_code_prefix_nextentry) + (dst_positive_scale_prefix_nextentry)) + ((dst_positive_scale_prefix_nextentry) + (dst_positive_scale_prefix_nextentry))) + (((dst_negative_code_prefix_nextentry) + (dst_negative_scale_prefix_nextentry)) * S ((dst_negative_code_prefix_nextentry) + (dst_negative_scale_prefix_nextentry)) + ((dst_negative_scale_prefix_nextentry) + (dst_negative_scale_prefix_nextentry)))) * S ((((dst_positive_code_prefix_nextentry) + (dst_positive_scale_prefix_nextentry)) * S ((dst_positive_code_prefix_nextentry) + (dst_positive_scale_prefix_nextentry)) + ((dst_positive_scale_prefix_nextentry) + (dst_positive_scale_prefix_nextentry))) + (((dst_negative_code_prefix_nextentry) + (dst_negative_scale_prefix_nextentry)) * S ((dst_negative_code_prefix_nextentry) + (dst_negative_scale_prefix_nextentry)) + ((dst_negative_scale_prefix_nextentry) + (dst_negative_scale_prefix_nextentry)))) + ((((dst_negative_code_prefix_nextentry) + (dst_negative_scale_prefix_nextentry)) * S ((dst_negative_code_prefix_nextentry) + (dst_negative_scale_prefix_nextentry)) + ((dst_negative_scale_prefix_nextentry) + (dst_negative_scale_prefix_nextentry))) + (((dst_negative_code_prefix_nextentry) + (dst_negative_scale_prefix_nextentry)) * S ((dst_negative_code_prefix_nextentry) + (dst_negative_scale_prefix_nextentry)) + ((dst_negative_scale_prefix_nextentry) + (dst_negative_scale_prefix_nextentry)))))) /\ (((((exists ff_h_pvs_prefix_nextentrypositive. ff_h_pvs_prefix_nextentrypositive + S (dst_positive_prefix_nextentry) = S ((S (scp_flat_index_prefix_next)) * dst_positive_scale_prefix_nextentry)) /\ exists ff_q_pvs_prefix_nextentrypositive. dst_positive_code_prefix_nextentry = ff_q_pvs_prefix_nextentrypositive * S ((S (scp_flat_index_prefix_next)) * dst_positive_scale_prefix_nextentry) + (dst_positive_prefix_nextentry))) /\ (((((exists ff_h_pvs_prefix_nextentrynegative. ff_h_pvs_prefix_nextentrynegative + S (dst_negative_prefix_nextentry) = S ((S (scp_flat_index_prefix_next)) * dst_negative_scale_prefix_nextentry)) /\ exists ff_q_pvs_prefix_nextentrynegative. dst_negative_code_prefix_nextentry = ff_q_pvs_prefix_nextentrynegative * S ((S (scp_flat_index_prefix_next)) * dst_negative_scale_prefix_nextentry) + (dst_negative_prefix_nextentry))) /\ (exists ge_balance_positive_prefix_nextentryvalue ge_balance_negative_prefix_nextentryvalue. (((((scp_flat_value_prefix_next) = 2 * (ge_balance_positive_prefix_nextentryvalue) /\ (ge_balance_negative_prefix_nextentryvalue) = 0) \/ exists ge_signed_half_prefix_nextentryvaluedecode. (((scp_flat_value_prefix_next) = 2 * ge_signed_half_prefix_nextentryvaluedecode + 1 /\ (ge_balance_positive_prefix_nextentryvalue) = 0) /\ (ge_balance_negative_prefix_nextentryvalue) = S ge_signed_half_prefix_nextentryvaluedecode))) /\ ((dst_positive_prefix_nextentry) + ge_balance_negative_prefix_nextentryvalue = (dst_negative_prefix_nextentry) + ge_balance_positive_prefix_nextentryvalue))))))))) -> (exists scp_flat_row_prefix_nextproduct scp_flat_column_prefix_nextproduct scp_flat_first_prefix_nextproduct scp_flat_second_prefix_nextproduct. (((scp_flat_index_prefix_next)=((n)*(scp_flat_row_prefix_nextproduct)+(scp_flat_column_prefix_nextproduct))) /\ (((exists pvs_gap_prefix_nextproductremainder. pvs_gap_prefix_nextproductremainder + S (scp_flat_column_prefix_nextproduct) = (n)) /\ (((exists dst_positive_code_prefix_nextproductF dst_positive_scale_prefix_nextproductF dst_negative_code_prefix_nextproductF dst_negative_scale_prefix_nextproductF dst_positive_prefix_nextproductF dst_negative_prefix_nextproductF. (((F) = (((((dst_positive_code_prefix_nextproductF) + (dst_positive_scale_prefix_nextproductF)) * S ((dst_positive_code_prefix_nextproductF) + (dst_positive_scale_prefix_nextproductF)) + ((dst_positive_scale_prefix_nextproductF) + (dst_positive_scale_prefix_nextproductF))) + (((dst_negative_code_prefix_nextproductF) + (dst_negative_scale_prefix_nextproductF)) * S ((dst_negative_code_prefix_nextproductF) + (dst_negative_scale_prefix_nextproductF)) + ((dst_negative_scale_prefix_nextproductF) + (dst_negative_scale_prefix_nextproductF)))) * S ((((dst_positive_code_prefix_nextproductF) + (dst_positive_scale_prefix_nextproductF)) * S ((dst_positive_code_prefix_nextproductF) + (dst_positive_scale_prefix_nextproductF)) + ((dst_positive_scale_prefix_nextproductF) + (dst_positive_scale_prefix_nextproductF))) + (((dst_negative_code_prefix_nextproductF) + (dst_negative_scale_prefix_nextproductF)) * S ((dst_negative_code_prefix_nextproductF) + (dst_negative_scale_prefix_nextproductF)) + ((dst_negative_scale_prefix_nextproductF) + (dst_negative_scale_prefix_nextproductF)))) + ((((dst_negative_code_prefix_nextproductF) + (dst_negative_scale_prefix_nextproductF)) * S ((dst_negative_code_prefix_nextproductF) + (dst_negative_scale_prefix_nextproductF)) + ((dst_negative_scale_prefix_nextproductF) + (dst_negative_scale_prefix_nextproductF))) + (((dst_negative_code_prefix_nextproductF) + (dst_negative_scale_prefix_nextproductF)) * S ((dst_negative_code_prefix_nextproductF) + (dst_negative_scale_prefix_nextproductF)) + ((dst_negative_scale_prefix_nextproductF) + (dst_negative_scale_prefix_nextproductF)))))) /\ (((((exists ff_h_pvs_prefix_nextproductFpositive. ff_h_pvs_prefix_nextproductFpositive + S (dst_positive_prefix_nextproductF) = S ((S (scp_flat_row_prefix_nextproduct)) * dst_positive_scale_prefix_nextproductF)) /\ exists ff_q_pvs_prefix_nextproductFpositive. dst_positive_code_prefix_nextproductF = ff_q_pvs_prefix_nextproductFpositive * S ((S (scp_flat_row_prefix_nextproduct)) * dst_positive_scale_prefix_nextproductF) + (dst_positive_prefix_nextproductF))) /\ (((((exists ff_h_pvs_prefix_nextproductFnegative. ff_h_pvs_prefix_nextproductFnegative + S (dst_negative_prefix_nextproductF) = S ((S (scp_flat_row_prefix_nextproduct)) * dst_negative_scale_prefix_nextproductF)) /\ exists ff_q_pvs_prefix_nextproductFnegative. dst_negative_code_prefix_nextproductF = ff_q_pvs_prefix_nextproductFnegative * S ((S (scp_flat_row_prefix_nextproduct)) * dst_negative_scale_prefix_nextproductF) + (dst_negative_prefix_nextproductF))) /\ (exists ge_balance_positive_prefix_nextproductFvalue ge_balance_negative_prefix_nextproductFvalue. (((((scp_flat_first_prefix_nextproduct) = 2 * (ge_balance_positive_prefix_nextproductFvalue) /\ (ge_balance_negative_prefix_nextproductFvalue) = 0) \/ exists ge_signed_half_prefix_nextproductFvaluedecode. (((scp_flat_first_prefix_nextproduct) = 2 * ge_signed_half_prefix_nextproductFvaluedecode + 1 /\ (ge_balance_positive_prefix_nextproductFvalue) = 0) /\ (ge_balance_negative_prefix_nextproductFvalue) = S ge_signed_half_prefix_nextproductFvaluedecode))) /\ ((dst_positive_prefix_nextproductF) + ge_balance_negative_prefix_nextproductFvalue = (dst_negative_prefix_nextproductF) + ge_balance_positive_prefix_nextproductFvalue))))))))) /\ (((exists dst_positive_code_prefix_nextproductG dst_positive_scale_prefix_nextproductG dst_negative_code_prefix_nextproductG dst_negative_scale_prefix_nextproductG dst_positive_prefix_nextproductG dst_negative_prefix_nextproductG. (((G) = (((((dst_positive_code_prefix_nextproductG) + (dst_positive_scale_prefix_nextproductG)) * S ((dst_positive_code_prefix_nextproductG) + (dst_positive_scale_prefix_nextproductG)) + ((dst_positive_scale_prefix_nextproductG) + (dst_positive_scale_prefix_nextproductG))) + (((dst_negative_code_prefix_nextproductG) + (dst_negative_scale_prefix_nextproductG)) * S ((dst_negative_code_prefix_nextproductG) + (dst_negative_scale_prefix_nextproductG)) + ((dst_negative_scale_prefix_nextproductG) + (dst_negative_scale_prefix_nextproductG)))) * S ((((dst_positive_code_prefix_nextproductG) + (dst_positive_scale_prefix_nextproductG)) * S ((dst_positive_code_prefix_nextproductG) + (dst_positive_scale_prefix_nextproductG)) + ((dst_positive_scale_prefix_nextproductG) + (dst_positive_scale_prefix_nextproductG))) + (((dst_negative_code_prefix_nextproductG) + (dst_negative_scale_prefix_nextproductG)) * S ((dst_negative_code_prefix_nextproductG) + (dst_negative_scale_prefix_nextproductG)) + ((dst_negative_scale_prefix_nextproductG) + (dst_negative_scale_prefix_nextproductG)))) + ((((dst_negative_code_prefix_nextproductG) + (dst_negative_scale_prefix_nextproductG)) * S ((dst_negative_code_prefix_nextproductG) + (dst_negative_scale_prefix_nextproductG)) + ((dst_negative_scale_prefix_nextproductG) + (dst_negative_scale_prefix_nextproductG))) + (((dst_negative_code_prefix_nextproductG) + (dst_negative_scale_prefix_nextproductG)) * S ((dst_negative_code_prefix_nextproductG) + (dst_negative_scale_prefix_nextproductG)) + ((dst_negative_scale_prefix_nextproductG) + (dst_negative_scale_prefix_nextproductG)))))) /\ (((((exists ff_h_pvs_prefix_nextproductGpositive. ff_h_pvs_prefix_nextproductGpositive + S (dst_positive_prefix_nextproductG) = S ((S (scp_flat_column_prefix_nextproduct)) * dst_positive_scale_prefix_nextproductG)) /\ exists ff_q_pvs_prefix_nextproductGpositive. dst_positive_code_prefix_nextproductG = ff_q_pvs_prefix_nextproductGpositive * S ((S (scp_flat_column_prefix_nextproduct)) * dst_positive_scale_prefix_nextproductG) + (dst_positive_prefix_nextproductG))) /\ (((((exists ff_h_pvs_prefix_nextproductGnegative. ff_h_pvs_prefix_nextproductGnegative + S (dst_negative_prefix_nextproductG) = S ((S (scp_flat_column_prefix_nextproduct)) * dst_negative_scale_prefix_nextproductG)) /\ exists ff_q_pvs_prefix_nextproductGnegative. dst_negative_code_prefix_nextproductG = ff_q_pvs_prefix_nextproductGnegative * S ((S (scp_flat_column_prefix_nextproduct)) * dst_negative_scale_prefix_nextproductG) + (dst_negative_prefix_nextproductG))) /\ (exists ge_balance_positive_prefix_nextproductGvalue ge_balance_negative_prefix_nextproductGvalue. (((((scp_flat_second_prefix_nextproduct) = 2 * (ge_balance_positive_prefix_nextproductGvalue) /\ (ge_balance_negative_prefix_nextproductGvalue) = 0) \/ exists ge_signed_half_prefix_nextproductGvaluedecode. (((scp_flat_second_prefix_nextproduct) = 2 * ge_signed_half_prefix_nextproductGvaluedecode + 1 /\ (ge_balance_positive_prefix_nextproductGvalue) = 0) /\ (ge_balance_negative_prefix_nextproductGvalue) = S ge_signed_half_prefix_nextproductGvaluedecode))) /\ ((dst_positive_prefix_nextproductG) + ge_balance_negative_prefix_nextproductGvalue = (dst_negative_prefix_nextproductG) + ge_balance_positive_prefix_nextproductGvalue))))))))) /\ (exists sto_ap_prefix_nextproductvalue sto_an_prefix_nextproductvalue sto_bp_prefix_nextproductvalue sto_bn_prefix_nextproductvalue sto_cp_prefix_nextproductvalue sto_cn_prefix_nextproductvalue. (((((scp_flat_first_prefix_nextproduct) = 2 * (sto_ap_prefix_nextproductvalue) /\ (sto_an_prefix_nextproductvalue) = 0) \/ exists ge_signed_half_prefix_nextproductvalueleft. (((scp_flat_first_prefix_nextproduct) = 2 * ge_signed_half_prefix_nextproductvalueleft + 1 /\ (sto_ap_prefix_nextproductvalue) = 0) /\ (sto_an_prefix_nextproductvalue) = S ge_signed_half_prefix_nextproductvalueleft))) /\ ((((((scp_flat_second_prefix_nextproduct) = 2 * (sto_bp_prefix_nextproductvalue) /\ (sto_bn_prefix_nextproductvalue) = 0) \/ exists ge_signed_half_prefix_nextproductvalueright. (((scp_flat_second_prefix_nextproduct) = 2 * ge_signed_half_prefix_nextproductvalueright + 1 /\ (sto_bp_prefix_nextproductvalue) = 0) /\ (sto_bn_prefix_nextproductvalue) = S ge_signed_half_prefix_nextproductvalueright))) /\ ((((((scp_flat_value_prefix_next) = 2 * (sto_cp_prefix_nextproductvalue) /\ (sto_cn_prefix_nextproductvalue) = 0) \/ exists ge_signed_half_prefix_nextproductvalueoutput. (((scp_flat_value_prefix_next) = 2 * ge_signed_half_prefix_nextproductvalueoutput + 1 /\ (sto_cp_prefix_nextproductvalue) = 0) /\ (sto_cn_prefix_nextproductvalue) = S ge_signed_half_prefix_nextproductvalueoutput))) /\ ((sto_ap_prefix_nextproductvalue * sto_bp_prefix_nextproductvalue + sto_an_prefix_nextproductvalue * sto_bn_prefix_nextproductvalue) + sto_cn_prefix_nextproductvalue = (sto_ap_prefix_nextproductvalue * sto_bn_prefix_nextproductvalue + sto_an_prefix_nextproductvalue * sto_bp_prefix_nextproductvalue) + sto_cp_prefix_nextproductvalue)))))))))))))))))) /\ (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))) - 0054
specialize signed_cartesian_flat_prefix_append (F) - 0055
specialize signed_cartesian_flat_prefix_append (G) - 0056
specialize signed_cartesian_flat_prefix_append (n) - 0057
specialize signed_cartesian_flat_prefix_append (l) - 0058
specialize signed_cartesian_flat_prefix_append (x) - 0059
specialize signed_cartesian_flat_prefix_append (x1) - 0060
apply signed_cartesian_flat_prefix_append - 0061
exact hp_witness - 0062
exact hv_witness - 0063
cases he - 0064
cases he_witness - 0065
exists x2 - 0066
exact he_witness_left