WS000B

signed_table_scalar_lookup

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

Every supplied canonical lookup value satisfies the actual scalar graph, by lookup functionality and the witnessed pointwise entries.

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 a F G l i b c. (((exists dst_positive_code_scalar_lookup_relationinput_table dst_positive_scale_scalar_lookup_relationinput_table dst_negative_code_scalar_lookup_relationinput_table dst_negative_scale_scalar_lookup_relationinput_table. (((F) = (((((dst_positive_code_scalar_lookup_relationinput_table) + (dst_positive_scale_scalar_lookup_relationinput_table)) * S ((dst_positive_code_scalar_lookup_relationinput_table) + (dst_positive_scale_scalar_lookup_relationinput_table)) + ((dst_positive_scale_scalar_lookup_relationinput_table) + (dst_positive_scale_scalar_lookup_relationinput_table))) + (((dst_negative_code_scalar_lookup_relationinput_table) + (dst_negative_scale_scalar_lookup_relationinput_table)) * S ((dst_negative_code_scalar_lookup_relationinput_table) + (dst_negative_scale_scalar_lookup_relationinput_table)) + ((dst_negative_scale_scalar_lookup_relationinput_table) + (dst_negative_scale_scalar_lookup_relationinput_table)))) * S ((((dst_positive_code_scalar_lookup_relationinput_table) + (dst_positive_scale_scalar_lookup_relationinput_table)) * S ((dst_positive_code_scalar_lookup_relationinput_table) + (dst_positive_scale_scalar_lookup_relationinput_table)) + ((dst_positive_scale_scalar_lookup_relationinput_table) + (dst_positive_scale_scalar_lookup_relationinput_table))) + (((dst_negative_code_scalar_lookup_relationinput_table) + (dst_negative_scale_scalar_lookup_relationinput_table)) * S ((dst_negative_code_scalar_lookup_relationinput_table) + (dst_negative_scale_scalar_lookup_relationinput_table)) + ((dst_negative_scale_scalar_lookup_relationinput_table) + (dst_negative_scale_scalar_lookup_relationinput_table)))) + ((((dst_negative_code_scalar_lookup_relationinput_table) + (dst_negative_scale_scalar_lookup_relationinput_table)) * S ((dst_negative_code_scalar_lookup_relationinput_table) + (dst_negative_scale_scalar_lookup_relationinput_table)) + ((dst_negative_scale_scalar_lookup_relationinput_table) + (dst_negative_scale_scalar_lookup_relationinput_table))) + (((dst_negative_code_scalar_lookup_relationinput_table) + (dst_negative_scale_scalar_lookup_relationinput_table)) * S ((dst_negative_code_scalar_lookup_relationinput_table) + (dst_negative_scale_scalar_lookup_relationinput_table)) + ((dst_negative_scale_scalar_lookup_relationinput_table) + (dst_negative_scale_scalar_lookup_relationinput_table)))))) /\ (forall dst_index_scalar_lookup_relationinput_table. (exists pvs_le_gap_scalar_lookup_relationinput_tabledomain. pvs_le_gap_scalar_lookup_relationinput_tabledomain + (dst_index_scalar_lookup_relationinput_table) = (l)) -> exists dst_positive_scalar_lookup_relationinput_table dst_negative_scalar_lookup_relationinput_table dst_value_scalar_lookup_relationinput_table. ((((exists ff_h_pvs_scalar_lookup_relationinput_tableentrypositive. ff_h_pvs_scalar_lookup_relationinput_tableentrypositive + S (dst_positive_scalar_lookup_relationinput_table) = S ((S (dst_index_scalar_lookup_relationinput_table)) * dst_positive_scale_scalar_lookup_relationinput_table)) /\ exists ff_q_pvs_scalar_lookup_relationinput_tableentrypositive. dst_positive_code_scalar_lookup_relationinput_table = ff_q_pvs_scalar_lookup_relationinput_tableentrypositive * S ((S (dst_index_scalar_lookup_relationinput_table)) * dst_positive_scale_scalar_lookup_relationinput_table) + (dst_positive_scalar_lookup_relationinput_table))) /\ (((((exists ff_h_pvs_scalar_lookup_relationinput_tableentrynegative. ff_h_pvs_scalar_lookup_relationinput_tableentrynegative + S (dst_negative_scalar_lookup_relationinput_table) = S ((S (dst_index_scalar_lookup_relationinput_table)) * dst_negative_scale_scalar_lookup_relationinput_table)) /\ exists ff_q_pvs_scalar_lookup_relationinput_tableentrynegative. dst_negative_code_scalar_lookup_relationinput_table = ff_q_pvs_scalar_lookup_relationinput_tableentrynegative * S ((S (dst_index_scalar_lookup_relationinput_table)) * dst_negative_scale_scalar_lookup_relationinput_table) + (dst_negative_scalar_lookup_relationinput_table))) /\ (exists ge_balance_positive_scalar_lookup_relationinput_tableentryvalue ge_balance_negative_scalar_lookup_relationinput_tableentryvalue. (((((dst_value_scalar_lookup_relationinput_table) = 2 * (ge_balance_positive_scalar_lookup_relationinput_tableentryvalue) /\ (ge_balance_negative_scalar_lookup_relationinput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_lookup_relationinput_tableentryvaluedecode. (((dst_value_scalar_lookup_relationinput_table) = 2 * ge_signed_half_scalar_lookup_relationinput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_lookup_relationinput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_lookup_relationinput_tableentryvalue) = S ge_signed_half_scalar_lookup_relationinput_tableentryvaluedecode))) /\ ((dst_positive_scalar_lookup_relationinput_table) + ge_balance_negative_scalar_lookup_relationinput_tableentryvalue = (dst_negative_scalar_lookup_relationinput_table) + ge_balance_positive_scalar_lookup_relationinput_tableentryvalue))))))))) /\ (((exists dst_positive_code_scalar_lookup_relationoutput_table dst_positive_scale_scalar_lookup_relationoutput_table dst_negative_code_scalar_lookup_relationoutput_table dst_negative_scale_scalar_lookup_relationoutput_table. (((G) = (((((dst_positive_code_scalar_lookup_relationoutput_table) + (dst_positive_scale_scalar_lookup_relationoutput_table)) * S ((dst_positive_code_scalar_lookup_relationoutput_table) + (dst_positive_scale_scalar_lookup_relationoutput_table)) + ((dst_positive_scale_scalar_lookup_relationoutput_table) + (dst_positive_scale_scalar_lookup_relationoutput_table))) + (((dst_negative_code_scalar_lookup_relationoutput_table) + (dst_negative_scale_scalar_lookup_relationoutput_table)) * S ((dst_negative_code_scalar_lookup_relationoutput_table) + (dst_negative_scale_scalar_lookup_relationoutput_table)) + ((dst_negative_scale_scalar_lookup_relationoutput_table) + (dst_negative_scale_scalar_lookup_relationoutput_table)))) * S ((((dst_positive_code_scalar_lookup_relationoutput_table) + (dst_positive_scale_scalar_lookup_relationoutput_table)) * S ((dst_positive_code_scalar_lookup_relationoutput_table) + (dst_positive_scale_scalar_lookup_relationoutput_table)) + ((dst_positive_scale_scalar_lookup_relationoutput_table) + (dst_positive_scale_scalar_lookup_relationoutput_table))) + (((dst_negative_code_scalar_lookup_relationoutput_table) + (dst_negative_scale_scalar_lookup_relationoutput_table)) * S ((dst_negative_code_scalar_lookup_relationoutput_table) + (dst_negative_scale_scalar_lookup_relationoutput_table)) + ((dst_negative_scale_scalar_lookup_relationoutput_table) + (dst_negative_scale_scalar_lookup_relationoutput_table)))) + ((((dst_negative_code_scalar_lookup_relationoutput_table) + (dst_negative_scale_scalar_lookup_relationoutput_table)) * S ((dst_negative_code_scalar_lookup_relationoutput_table) + (dst_negative_scale_scalar_lookup_relationoutput_table)) + ((dst_negative_scale_scalar_lookup_relationoutput_table) + (dst_negative_scale_scalar_lookup_relationoutput_table))) + (((dst_negative_code_scalar_lookup_relationoutput_table) + (dst_negative_scale_scalar_lookup_relationoutput_table)) * S ((dst_negative_code_scalar_lookup_relationoutput_table) + (dst_negative_scale_scalar_lookup_relationoutput_table)) + ((dst_negative_scale_scalar_lookup_relationoutput_table) + (dst_negative_scale_scalar_lookup_relationoutput_table)))))) /\ (forall dst_index_scalar_lookup_relationoutput_table. (exists pvs_le_gap_scalar_lookup_relationoutput_tabledomain. pvs_le_gap_scalar_lookup_relationoutput_tabledomain + (dst_index_scalar_lookup_relationoutput_table) = (l)) -> exists dst_positive_scalar_lookup_relationoutput_table dst_negative_scalar_lookup_relationoutput_table dst_value_scalar_lookup_relationoutput_table. ((((exists ff_h_pvs_scalar_lookup_relationoutput_tableentrypositive. ff_h_pvs_scalar_lookup_relationoutput_tableentrypositive + S (dst_positive_scalar_lookup_relationoutput_table) = S ((S (dst_index_scalar_lookup_relationoutput_table)) * dst_positive_scale_scalar_lookup_relationoutput_table)) /\ exists ff_q_pvs_scalar_lookup_relationoutput_tableentrypositive. dst_positive_code_scalar_lookup_relationoutput_table = ff_q_pvs_scalar_lookup_relationoutput_tableentrypositive * S ((S (dst_index_scalar_lookup_relationoutput_table)) * dst_positive_scale_scalar_lookup_relationoutput_table) + (dst_positive_scalar_lookup_relationoutput_table))) /\ (((((exists ff_h_pvs_scalar_lookup_relationoutput_tableentrynegative. ff_h_pvs_scalar_lookup_relationoutput_tableentrynegative + S (dst_negative_scalar_lookup_relationoutput_table) = S ((S (dst_index_scalar_lookup_relationoutput_table)) * dst_negative_scale_scalar_lookup_relationoutput_table)) /\ exists ff_q_pvs_scalar_lookup_relationoutput_tableentrynegative. dst_negative_code_scalar_lookup_relationoutput_table = ff_q_pvs_scalar_lookup_relationoutput_tableentrynegative * S ((S (dst_index_scalar_lookup_relationoutput_table)) * dst_negative_scale_scalar_lookup_relationoutput_table) + (dst_negative_scalar_lookup_relationoutput_table))) /\ (exists ge_balance_positive_scalar_lookup_relationoutput_tableentryvalue ge_balance_negative_scalar_lookup_relationoutput_tableentryvalue. (((((dst_value_scalar_lookup_relationoutput_table) = 2 * (ge_balance_positive_scalar_lookup_relationoutput_tableentryvalue) /\ (ge_balance_negative_scalar_lookup_relationoutput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_lookup_relationoutput_tableentryvaluedecode. (((dst_value_scalar_lookup_relationoutput_table) = 2 * ge_signed_half_scalar_lookup_relationoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_lookup_relationoutput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_lookup_relationoutput_tableentryvalue) = S ge_signed_half_scalar_lookup_relationoutput_tableentryvaluedecode))) /\ ((dst_positive_scalar_lookup_relationoutput_table) + ge_balance_negative_scalar_lookup_relationoutput_tableentryvalue = (dst_negative_scalar_lookup_relationoutput_table) + ge_balance_positive_scalar_lookup_relationoutput_tableentryvalue))))))))) /\ (forall sto_index_scalar_lookup_relationentries. (exists pvs_gap_scalar_lookup_relationentriesbound. pvs_gap_scalar_lookup_relationentriesbound + S (sto_index_scalar_lookup_relationentries) = (l)) -> exists sto_input_scalar_lookup_relationentries sto_output_scalar_lookup_relationentries. ((exists dst_positive_code_scalar_lookup_relationentriesentryinput dst_positive_scale_scalar_lookup_relationentriesentryinput dst_negative_code_scalar_lookup_relationentriesentryinput dst_negative_scale_scalar_lookup_relationentriesentryinput dst_positive_scalar_lookup_relationentriesentryinput dst_negative_scalar_lookup_relationentriesentryinput. (((F) = (((((dst_positive_code_scalar_lookup_relationentriesentryinput) + (dst_positive_scale_scalar_lookup_relationentriesentryinput)) * S ((dst_positive_code_scalar_lookup_relationentriesentryinput) + (dst_positive_scale_scalar_lookup_relationentriesentryinput)) + ((dst_positive_scale_scalar_lookup_relationentriesentryinput) + (dst_positive_scale_scalar_lookup_relationentriesentryinput))) + (((dst_negative_code_scalar_lookup_relationentriesentryinput) + (dst_negative_scale_scalar_lookup_relationentriesentryinput)) * S ((dst_negative_code_scalar_lookup_relationentriesentryinput) + (dst_negative_scale_scalar_lookup_relationentriesentryinput)) + ((dst_negative_scale_scalar_lookup_relationentriesentryinput) + (dst_negative_scale_scalar_lookup_relationentriesentryinput)))) * S ((((dst_positive_code_scalar_lookup_relationentriesentryinput) + (dst_positive_scale_scalar_lookup_relationentriesentryinput)) * S ((dst_positive_code_scalar_lookup_relationentriesentryinput) + (dst_positive_scale_scalar_lookup_relationentriesentryinput)) + ((dst_positive_scale_scalar_lookup_relationentriesentryinput) + (dst_positive_scale_scalar_lookup_relationentriesentryinput))) + (((dst_negative_code_scalar_lookup_relationentriesentryinput) + (dst_negative_scale_scalar_lookup_relationentriesentryinput)) * S ((dst_negative_code_scalar_lookup_relationentriesentryinput) + (dst_negative_scale_scalar_lookup_relationentriesentryinput)) + ((dst_negative_scale_scalar_lookup_relationentriesentryinput) + (dst_negative_scale_scalar_lookup_relationentriesentryinput)))) + ((((dst_negative_code_scalar_lookup_relationentriesentryinput) + (dst_negative_scale_scalar_lookup_relationentriesentryinput)) * S ((dst_negative_code_scalar_lookup_relationentriesentryinput) + (dst_negative_scale_scalar_lookup_relationentriesentryinput)) + ((dst_negative_scale_scalar_lookup_relationentriesentryinput) + (dst_negative_scale_scalar_lookup_relationentriesentryinput))) + (((dst_negative_code_scalar_lookup_relationentriesentryinput) + (dst_negative_scale_scalar_lookup_relationentriesentryinput)) * S ((dst_negative_code_scalar_lookup_relationentriesentryinput) + (dst_negative_scale_scalar_lookup_relationentriesentryinput)) + ((dst_negative_scale_scalar_lookup_relationentriesentryinput) + (dst_negative_scale_scalar_lookup_relationentriesentryinput)))))) /\ (((((exists ff_h_pvs_scalar_lookup_relationentriesentryinputpositive. ff_h_pvs_scalar_lookup_relationentriesentryinputpositive + S (dst_positive_scalar_lookup_relationentriesentryinput) = S ((S (sto_index_scalar_lookup_relationentries)) * dst_positive_scale_scalar_lookup_relationentriesentryinput)) /\ exists ff_q_pvs_scalar_lookup_relationentriesentryinputpositive. dst_positive_code_scalar_lookup_relationentriesentryinput = ff_q_pvs_scalar_lookup_relationentriesentryinputpositive * S ((S (sto_index_scalar_lookup_relationentries)) * dst_positive_scale_scalar_lookup_relationentriesentryinput) + (dst_positive_scalar_lookup_relationentriesentryinput))) /\ (((((exists ff_h_pvs_scalar_lookup_relationentriesentryinputnegative. ff_h_pvs_scalar_lookup_relationentriesentryinputnegative + S (dst_negative_scalar_lookup_relationentriesentryinput) = S ((S (sto_index_scalar_lookup_relationentries)) * dst_negative_scale_scalar_lookup_relationentriesentryinput)) /\ exists ff_q_pvs_scalar_lookup_relationentriesentryinputnegative. dst_negative_code_scalar_lookup_relationentriesentryinput = ff_q_pvs_scalar_lookup_relationentriesentryinputnegative * S ((S (sto_index_scalar_lookup_relationentries)) * dst_negative_scale_scalar_lookup_relationentriesentryinput) + (dst_negative_scalar_lookup_relationentriesentryinput))) /\ (exists ge_balance_positive_scalar_lookup_relationentriesentryinputvalue ge_balance_negative_scalar_lookup_relationentriesentryinputvalue. (((((sto_input_scalar_lookup_relationentries) = 2 * (ge_balance_positive_scalar_lookup_relationentriesentryinputvalue) /\ (ge_balance_negative_scalar_lookup_relationentriesentryinputvalue) = 0) \/ exists ge_signed_half_scalar_lookup_relationentriesentryinputvaluedecode. (((sto_input_scalar_lookup_relationentries) = 2 * ge_signed_half_scalar_lookup_relationentriesentryinputvaluedecode + 1 /\ (ge_balance_positive_scalar_lookup_relationentriesentryinputvalue) = 0) /\ (ge_balance_negative_scalar_lookup_relationentriesentryinputvalue) = S ge_signed_half_scalar_lookup_relationentriesentryinputvaluedecode))) /\ ((dst_positive_scalar_lookup_relationentriesentryinput) + ge_balance_negative_scalar_lookup_relationentriesentryinputvalue = (dst_negative_scalar_lookup_relationentriesentryinput) + ge_balance_positive_scalar_lookup_relationentriesentryinputvalue))))))))) /\ (((exists dst_positive_code_scalar_lookup_relationentriesentryoutput dst_positive_scale_scalar_lookup_relationentriesentryoutput dst_negative_code_scalar_lookup_relationentriesentryoutput dst_negative_scale_scalar_lookup_relationentriesentryoutput dst_positive_scalar_lookup_relationentriesentryoutput dst_negative_scalar_lookup_relationentriesentryoutput. (((G) = (((((dst_positive_code_scalar_lookup_relationentriesentryoutput) + (dst_positive_scale_scalar_lookup_relationentriesentryoutput)) * S ((dst_positive_code_scalar_lookup_relationentriesentryoutput) + (dst_positive_scale_scalar_lookup_relationentriesentryoutput)) + ((dst_positive_scale_scalar_lookup_relationentriesentryoutput) + (dst_positive_scale_scalar_lookup_relationentriesentryoutput))) + (((dst_negative_code_scalar_lookup_relationentriesentryoutput) + (dst_negative_scale_scalar_lookup_relationentriesentryoutput)) * S ((dst_negative_code_scalar_lookup_relationentriesentryoutput) + (dst_negative_scale_scalar_lookup_relationentriesentryoutput)) + ((dst_negative_scale_scalar_lookup_relationentriesentryoutput) + (dst_negative_scale_scalar_lookup_relationentriesentryoutput)))) * S ((((dst_positive_code_scalar_lookup_relationentriesentryoutput) + (dst_positive_scale_scalar_lookup_relationentriesentryoutput)) * S ((dst_positive_code_scalar_lookup_relationentriesentryoutput) + (dst_positive_scale_scalar_lookup_relationentriesentryoutput)) + ((dst_positive_scale_scalar_lookup_relationentriesentryoutput) + (dst_positive_scale_scalar_lookup_relationentriesentryoutput))) + (((dst_negative_code_scalar_lookup_relationentriesentryoutput) + (dst_negative_scale_scalar_lookup_relationentriesentryoutput)) * S ((dst_negative_code_scalar_lookup_relationentriesentryoutput) + (dst_negative_scale_scalar_lookup_relationentriesentryoutput)) + ((dst_negative_scale_scalar_lookup_relationentriesentryoutput) + (dst_negative_scale_scalar_lookup_relationentriesentryoutput)))) + ((((dst_negative_code_scalar_lookup_relationentriesentryoutput) + (dst_negative_scale_scalar_lookup_relationentriesentryoutput)) * S ((dst_negative_code_scalar_lookup_relationentriesentryoutput) + (dst_negative_scale_scalar_lookup_relationentriesentryoutput)) + ((dst_negative_scale_scalar_lookup_relationentriesentryoutput) + (dst_negative_scale_scalar_lookup_relationentriesentryoutput))) + (((dst_negative_code_scalar_lookup_relationentriesentryoutput) + (dst_negative_scale_scalar_lookup_relationentriesentryoutput)) * S ((dst_negative_code_scalar_lookup_relationentriesentryoutput) + (dst_negative_scale_scalar_lookup_relationentriesentryoutput)) + ((dst_negative_scale_scalar_lookup_relationentriesentryoutput) + (dst_negative_scale_scalar_lookup_relationentriesentryoutput)))))) /\ (((((exists ff_h_pvs_scalar_lookup_relationentriesentryoutputpositive. ff_h_pvs_scalar_lookup_relationentriesentryoutputpositive + S (dst_positive_scalar_lookup_relationentriesentryoutput) = S ((S (sto_index_scalar_lookup_relationentries)) * dst_positive_scale_scalar_lookup_relationentriesentryoutput)) /\ exists ff_q_pvs_scalar_lookup_relationentriesentryoutputpositive. dst_positive_code_scalar_lookup_relationentriesentryoutput = ff_q_pvs_scalar_lookup_relationentriesentryoutputpositive * S ((S (sto_index_scalar_lookup_relationentries)) * dst_positive_scale_scalar_lookup_relationentriesentryoutput) + (dst_positive_scalar_lookup_relationentriesentryoutput))) /\ (((((exists ff_h_pvs_scalar_lookup_relationentriesentryoutputnegative. ff_h_pvs_scalar_lookup_relationentriesentryoutputnegative + S (dst_negative_scalar_lookup_relationentriesentryoutput) = S ((S (sto_index_scalar_lookup_relationentries)) * dst_negative_scale_scalar_lookup_relationentriesentryoutput)) /\ exists ff_q_pvs_scalar_lookup_relationentriesentryoutputnegative. dst_negative_code_scalar_lookup_relationentriesentryoutput = ff_q_pvs_scalar_lookup_relationentriesentryoutputnegative * S ((S (sto_index_scalar_lookup_relationentries)) * dst_negative_scale_scalar_lookup_relationentriesentryoutput) + (dst_negative_scalar_lookup_relationentriesentryoutput))) /\ (exists ge_balance_positive_scalar_lookup_relationentriesentryoutputvalue ge_balance_negative_scalar_lookup_relationentriesentryoutputvalue. (((((sto_output_scalar_lookup_relationentries) = 2 * (ge_balance_positive_scalar_lookup_relationentriesentryoutputvalue) /\ (ge_balance_negative_scalar_lookup_relationentriesentryoutputvalue) = 0) \/ exists ge_signed_half_scalar_lookup_relationentriesentryoutputvaluedecode. (((sto_output_scalar_lookup_relationentries) = 2 * ge_signed_half_scalar_lookup_relationentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_scalar_lookup_relationentriesentryoutputvalue) = 0) /\ (ge_balance_negative_scalar_lookup_relationentriesentryoutputvalue) = S ge_signed_half_scalar_lookup_relationentriesentryoutputvaluedecode))) /\ ((dst_positive_scalar_lookup_relationentriesentryoutput) + ge_balance_negative_scalar_lookup_relationentriesentryoutputvalue = (dst_negative_scalar_lookup_relationentriesentryoutput) + ge_balance_positive_scalar_lookup_relationentriesentryoutputvalue))))))))) /\ (exists sto_ap_scalar_lookup_relationentriesentryoperation sto_an_scalar_lookup_relationentriesentryoperation sto_bp_scalar_lookup_relationentriesentryoperation sto_bn_scalar_lookup_relationentriesentryoperation sto_cp_scalar_lookup_relationentriesentryoperation sto_cn_scalar_lookup_relationentriesentryoperation. (((((a) = 2 * (sto_ap_scalar_lookup_relationentriesentryoperation) /\ (sto_an_scalar_lookup_relationentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_lookup_relationentriesentryoperationleft. (((a) = 2 * ge_signed_half_scalar_lookup_relationentriesentryoperationleft + 1 /\ (sto_ap_scalar_lookup_relationentriesentryoperation) = 0) /\ (sto_an_scalar_lookup_relationentriesentryoperation) = S ge_signed_half_scalar_lookup_relationentriesentryoperationleft))) /\ ((((((sto_input_scalar_lookup_relationentries) = 2 * (sto_bp_scalar_lookup_relationentriesentryoperation) /\ (sto_bn_scalar_lookup_relationentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_lookup_relationentriesentryoperationright. (((sto_input_scalar_lookup_relationentries) = 2 * ge_signed_half_scalar_lookup_relationentriesentryoperationright + 1 /\ (sto_bp_scalar_lookup_relationentriesentryoperation) = 0) /\ (sto_bn_scalar_lookup_relationentriesentryoperation) = S ge_signed_half_scalar_lookup_relationentriesentryoperationright))) /\ ((((((sto_output_scalar_lookup_relationentries) = 2 * (sto_cp_scalar_lookup_relationentriesentryoperation) /\ (sto_cn_scalar_lookup_relationentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_lookup_relationentriesentryoperationoutput. (((sto_output_scalar_lookup_relationentries) = 2 * ge_signed_half_scalar_lookup_relationentriesentryoperationoutput + 1 /\ (sto_cp_scalar_lookup_relationentriesentryoperation) = 0) /\ (sto_cn_scalar_lookup_relationentriesentryoperation) = S ge_signed_half_scalar_lookup_relationentriesentryoperationoutput))) /\ ((sto_ap_scalar_lookup_relationentriesentryoperation * sto_bp_scalar_lookup_relationentriesentryoperation + sto_an_scalar_lookup_relationentriesentryoperation * sto_bn_scalar_lookup_relationentriesentryoperation) + sto_cn_scalar_lookup_relationentriesentryoperation = (sto_ap_scalar_lookup_relationentriesentryoperation * sto_bn_scalar_lookup_relationentriesentryoperation + sto_an_scalar_lookup_relationentriesentryoperation * sto_bp_scalar_lookup_relationentriesentryoperation) + sto_cp_scalar_lookup_relationentriesentryoperation))))))))))))))) -> (exists pvs_gap_scalar_lookup_bound. pvs_gap_scalar_lookup_bound + S (i) = (l)) -> (exists dst_positive_code_scalar_lookup_0 dst_positive_scale_scalar_lookup_0 dst_negative_code_scalar_lookup_0 dst_negative_scale_scalar_lookup_0 dst_positive_scalar_lookup_0 dst_negative_scalar_lookup_0. (((F) = (((((dst_positive_code_scalar_lookup_0) + (dst_positive_scale_scalar_lookup_0)) * S ((dst_positive_code_scalar_lookup_0) + (dst_positive_scale_scalar_lookup_0)) + ((dst_positive_scale_scalar_lookup_0) + (dst_positive_scale_scalar_lookup_0))) + (((dst_negative_code_scalar_lookup_0) + (dst_negative_scale_scalar_lookup_0)) * S ((dst_negative_code_scalar_lookup_0) + (dst_negative_scale_scalar_lookup_0)) + ((dst_negative_scale_scalar_lookup_0) + (dst_negative_scale_scalar_lookup_0)))) * S ((((dst_positive_code_scalar_lookup_0) + (dst_positive_scale_scalar_lookup_0)) * S ((dst_positive_code_scalar_lookup_0) + (dst_positive_scale_scalar_lookup_0)) + ((dst_positive_scale_scalar_lookup_0) + (dst_positive_scale_scalar_lookup_0))) + (((dst_negative_code_scalar_lookup_0) + (dst_negative_scale_scalar_lookup_0)) * S ((dst_negative_code_scalar_lookup_0) + (dst_negative_scale_scalar_lookup_0)) + ((dst_negative_scale_scalar_lookup_0) + (dst_negative_scale_scalar_lookup_0)))) + ((((dst_negative_code_scalar_lookup_0) + (dst_negative_scale_scalar_lookup_0)) * S ((dst_negative_code_scalar_lookup_0) + (dst_negative_scale_scalar_lookup_0)) + ((dst_negative_scale_scalar_lookup_0) + (dst_negative_scale_scalar_lookup_0))) + (((dst_negative_code_scalar_lookup_0) + (dst_negative_scale_scalar_lookup_0)) * S ((dst_negative_code_scalar_lookup_0) + (dst_negative_scale_scalar_lookup_0)) + ((dst_negative_scale_scalar_lookup_0) + (dst_negative_scale_scalar_lookup_0)))))) /\ (((((exists ff_h_pvs_scalar_lookup_0positive. ff_h_pvs_scalar_lookup_0positive + S (dst_positive_scalar_lookup_0) = S ((S (i)) * dst_positive_scale_scalar_lookup_0)) /\ exists ff_q_pvs_scalar_lookup_0positive. dst_positive_code_scalar_lookup_0 = ff_q_pvs_scalar_lookup_0positive * S ((S (i)) * dst_positive_scale_scalar_lookup_0) + (dst_positive_scalar_lookup_0))) /\ (((((exists ff_h_pvs_scalar_lookup_0negative. ff_h_pvs_scalar_lookup_0negative + S (dst_negative_scalar_lookup_0) = S ((S (i)) * dst_negative_scale_scalar_lookup_0)) /\ exists ff_q_pvs_scalar_lookup_0negative. dst_negative_code_scalar_lookup_0 = ff_q_pvs_scalar_lookup_0negative * S ((S (i)) * dst_negative_scale_scalar_lookup_0) + (dst_negative_scalar_lookup_0))) /\ (exists ge_balance_positive_scalar_lookup_0value ge_balance_negative_scalar_lookup_0value. (((((b) = 2 * (ge_balance_positive_scalar_lookup_0value) /\ (ge_balance_negative_scalar_lookup_0value) = 0) \/ exists ge_signed_half_scalar_lookup_0valuedecode. (((b) = 2 * ge_signed_half_scalar_lookup_0valuedecode + 1 /\ (ge_balance_positive_scalar_lookup_0value) = 0) /\ (ge_balance_negative_scalar_lookup_0value) = S ge_signed_half_scalar_lookup_0valuedecode))) /\ ((dst_positive_scalar_lookup_0) + ge_balance_negative_scalar_lookup_0value = (dst_negative_scalar_lookup_0) + ge_balance_positive_scalar_lookup_0value))))))))) -> (exists dst_positive_code_scalar_lookup_1 dst_positive_scale_scalar_lookup_1 dst_negative_code_scalar_lookup_1 dst_negative_scale_scalar_lookup_1 dst_positive_scalar_lookup_1 dst_negative_scalar_lookup_1. (((G) = (((((dst_positive_code_scalar_lookup_1) + (dst_positive_scale_scalar_lookup_1)) * S ((dst_positive_code_scalar_lookup_1) + (dst_positive_scale_scalar_lookup_1)) + ((dst_positive_scale_scalar_lookup_1) + (dst_positive_scale_scalar_lookup_1))) + (((dst_negative_code_scalar_lookup_1) + (dst_negative_scale_scalar_lookup_1)) * S ((dst_negative_code_scalar_lookup_1) + (dst_negative_scale_scalar_lookup_1)) + ((dst_negative_scale_scalar_lookup_1) + (dst_negative_scale_scalar_lookup_1)))) * S ((((dst_positive_code_scalar_lookup_1) + (dst_positive_scale_scalar_lookup_1)) * S ((dst_positive_code_scalar_lookup_1) + (dst_positive_scale_scalar_lookup_1)) + ((dst_positive_scale_scalar_lookup_1) + (dst_positive_scale_scalar_lookup_1))) + (((dst_negative_code_scalar_lookup_1) + (dst_negative_scale_scalar_lookup_1)) * S ((dst_negative_code_scalar_lookup_1) + (dst_negative_scale_scalar_lookup_1)) + ((dst_negative_scale_scalar_lookup_1) + (dst_negative_scale_scalar_lookup_1)))) + ((((dst_negative_code_scalar_lookup_1) + (dst_negative_scale_scalar_lookup_1)) * S ((dst_negative_code_scalar_lookup_1) + (dst_negative_scale_scalar_lookup_1)) + ((dst_negative_scale_scalar_lookup_1) + (dst_negative_scale_scalar_lookup_1))) + (((dst_negative_code_scalar_lookup_1) + (dst_negative_scale_scalar_lookup_1)) * S ((dst_negative_code_scalar_lookup_1) + (dst_negative_scale_scalar_lookup_1)) + ((dst_negative_scale_scalar_lookup_1) + (dst_negative_scale_scalar_lookup_1)))))) /\ (((((exists ff_h_pvs_scalar_lookup_1positive. ff_h_pvs_scalar_lookup_1positive + S (dst_positive_scalar_lookup_1) = S ((S (i)) * dst_positive_scale_scalar_lookup_1)) /\ exists ff_q_pvs_scalar_lookup_1positive. dst_positive_code_scalar_lookup_1 = ff_q_pvs_scalar_lookup_1positive * S ((S (i)) * dst_positive_scale_scalar_lookup_1) + (dst_positive_scalar_lookup_1))) /\ (((((exists ff_h_pvs_scalar_lookup_1negative. ff_h_pvs_scalar_lookup_1negative + S (dst_negative_scalar_lookup_1) = S ((S (i)) * dst_negative_scale_scalar_lookup_1)) /\ exists ff_q_pvs_scalar_lookup_1negative. dst_negative_code_scalar_lookup_1 = ff_q_pvs_scalar_lookup_1negative * S ((S (i)) * dst_negative_scale_scalar_lookup_1) + (dst_negative_scalar_lookup_1))) /\ (exists ge_balance_positive_scalar_lookup_1value ge_balance_negative_scalar_lookup_1value. (((((c) = 2 * (ge_balance_positive_scalar_lookup_1value) /\ (ge_balance_negative_scalar_lookup_1value) = 0) \/ exists ge_signed_half_scalar_lookup_1valuedecode. (((c) = 2 * ge_signed_half_scalar_lookup_1valuedecode + 1 /\ (ge_balance_positive_scalar_lookup_1value) = 0) /\ (ge_balance_negative_scalar_lookup_1value) = S ge_signed_half_scalar_lookup_1valuedecode))) /\ ((dst_positive_scalar_lookup_1) + ge_balance_negative_scalar_lookup_1value = (dst_negative_scalar_lookup_1) + ge_balance_positive_scalar_lookup_1value))))))))) -> (exists sto_ap_scalar_lookup_operation sto_an_scalar_lookup_operation sto_bp_scalar_lookup_operation sto_bn_scalar_lookup_operation sto_cp_scalar_lookup_operation sto_cn_scalar_lookup_operation. (((((a) = 2 * (sto_ap_scalar_lookup_operation) /\ (sto_an_scalar_lookup_operation) = 0) \/ exists ge_signed_half_scalar_lookup_operationleft. (((a) = 2 * ge_signed_half_scalar_lookup_operationleft + 1 /\ (sto_ap_scalar_lookup_operation) = 0) /\ (sto_an_scalar_lookup_operation) = S ge_signed_half_scalar_lookup_operationleft))) /\ ((((((b) = 2 * (sto_bp_scalar_lookup_operation) /\ (sto_bn_scalar_lookup_operation) = 0) \/ exists ge_signed_half_scalar_lookup_operationright. (((b) = 2 * ge_signed_half_scalar_lookup_operationright + 1 /\ (sto_bp_scalar_lookup_operation) = 0) /\ (sto_bn_scalar_lookup_operation) = S ge_signed_half_scalar_lookup_operationright))) /\ ((((((c) = 2 * (sto_cp_scalar_lookup_operation) /\ (sto_cn_scalar_lookup_operation) = 0) \/ exists ge_signed_half_scalar_lookup_operationoutput. (((c) = 2 * ge_signed_half_scalar_lookup_operationoutput + 1 /\ (sto_cp_scalar_lookup_operation) = 0) /\ (sto_cn_scalar_lookup_operation) = S ge_signed_half_scalar_lookup_operationoutput))) /\ ((sto_ap_scalar_lookup_operation * sto_bp_scalar_lookup_operation + sto_an_scalar_lookup_operation * sto_bn_scalar_lookup_operation) + sto_cn_scalar_lookup_operation = (sto_ap_scalar_lookup_operation * sto_bn_scalar_lookup_operation + sto_an_scalar_lookup_operation * sto_bp_scalar_lookup_operation) + sto_cp_scalar_lookup_operation)))))))

Constructive proof overview

Generated structural guide

Every supplied canonical lookup value satisfies the actual scalar graph, by lookup functionality and the witnessed pointwise entries.

The unchanged tactic script uses 1 declared prerequisite and contains 42 exact native proof lines.

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

Proof neighborhood

Direct dependencies

divisor_signed_table_at_functional Alpha theorem; checked-use authorized

Direct dependents

WS000E signed_table_scalar_extensional_unique WS001C signed_prefix_sum_scalar_multiply WS0026 signed_table_weighted_scalar_commute

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

42 script commands · 8 reading checkpoints · 3 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

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

01Fix variables and assumptionsL1–10

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

  1. L1
    intro a
  2. L2
    intro F
  3. L3
    intro G
  4. L4
    intro l
  5. L5
    intro i
  6. L6
    intro b
  7. L7
    intro c
  8. L8
    intro hop
  9. L9
    intro hi
  10. L10
    intro h0
02Fix variables and assumptionsL11–11

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

  1. L11
    intro h1
03Separate the logical casesL12–13

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

  1. L12
    cases hop
  2. L13
    cases hop_right
04Establish heL14–17

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

  1. L14
    have he : ∃ b. ∃ c. ArithAt(F,i,b) ∧ (ArithAt(G,i,c) ∧ SignedMul(a,b,c))Definitions: SignedMulArithAt
  2. L15
    specialize hop_right_right (i)
  3. L16
    apply hop_right_right
  4. L17
    exact hi
05Separate the logical casesL18–21

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

  1. L18
    cases he
  2. L19
    cases he_witness
  3. L20
    cases he_witness_witness
  4. L21
    cases he_witness_witness_right
06Establish heq0L22–31

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

  1. L22
    have heq0 : x = b
  2. L23
    specialize divisor_signed_table_at_functional (F)
  3. L24
    specialize divisor_signed_table_at_functional (i)
  4. L25
    specialize divisor_signed_table_at_functional (x)
  5. L26
    specialize divisor_signed_table_at_functional (b)
  6. L27
    apply divisor_signed_table_at_functional
  7. L28
    exact he_witness_witness_left
  8. L29
    exact h0
  9. L30
    rewrite heq0 at he_witness_witness_right_right
  10. L31
    rewrite heq0 at he_witness_witness_right_right
07Establish heq1L32–41

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

  1. L32
    have heq1 : x1 = c
  2. L33
    specialize divisor_signed_table_at_functional (G)
  3. L34
    specialize divisor_signed_table_at_functional (i)
  4. L35
    specialize divisor_signed_table_at_functional (x1)
  5. L36
    specialize divisor_signed_table_at_functional (c)
  6. L37
    apply divisor_signed_table_at_functional
  7. L38
    exact he_witness_witness_right_left
  8. L39
    exact h1
  9. L40
    rewrite heq1 at he_witness_witness_right_right
  10. L41
    rewrite heq1 at he_witness_witness_right_right
08Use earlier factsL42–42

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

  1. L42
    exact he_witness_witness_right_right

Library-wide reading audit

Original exact command ledger · 42 lines
  1. 0001intro a
  2. 0002intro F
  3. 0003intro G
  4. 0004intro l
  5. 0005intro i
  6. 0006intro b
  7. 0007intro c
  8. 0008intro hop
  9. 0009intro hi
  10. 0010intro h0
  11. 0011intro h1
  12. 0012cases hop
  13. 0013cases hop_right
  14. 0014have he : exists b c. ((exists dst_positive_code_scalar_lookup_valuesinput dst_positive_scale_scalar_lookup_valuesinput dst_negative_code_scalar_lookup_valuesinput dst_negative_scale_scalar_lookup_valuesinput dst_positive_scalar_lookup_valuesinput dst_negative_scalar_lookup_valuesinput. (((F) = (((((dst_positive_code_scalar_lookup_valuesinput) + (dst_positive_scale_scalar_lookup_valuesinput)) * S ((dst_positive_code_scalar_lookup_valuesinput) + (dst_positive_scale_scalar_lookup_valuesinput)) + ((dst_positive_scale_scalar_lookup_valuesinput) + (dst_positive_scale_scalar_lookup_valuesinput))) + (((dst_negative_code_scalar_lookup_valuesinput) + (dst_negative_scale_scalar_lookup_valuesinput)) * S ((dst_negative_code_scalar_lookup_valuesinput) + (dst_negative_scale_scalar_lookup_valuesinput)) + ((dst_negative_scale_scalar_lookup_valuesinput) + (dst_negative_scale_scalar_lookup_valuesinput)))) * S ((((dst_positive_code_scalar_lookup_valuesinput) + (dst_positive_scale_scalar_lookup_valuesinput)) * S ((dst_positive_code_scalar_lookup_valuesinput) + (dst_positive_scale_scalar_lookup_valuesinput)) + ((dst_positive_scale_scalar_lookup_valuesinput) + (dst_positive_scale_scalar_lookup_valuesinput))) + (((dst_negative_code_scalar_lookup_valuesinput) + (dst_negative_scale_scalar_lookup_valuesinput)) * S ((dst_negative_code_scalar_lookup_valuesinput) + (dst_negative_scale_scalar_lookup_valuesinput)) + ((dst_negative_scale_scalar_lookup_valuesinput) + (dst_negative_scale_scalar_lookup_valuesinput)))) + ((((dst_negative_code_scalar_lookup_valuesinput) + (dst_negative_scale_scalar_lookup_valuesinput)) * S ((dst_negative_code_scalar_lookup_valuesinput) + (dst_negative_scale_scalar_lookup_valuesinput)) + ((dst_negative_scale_scalar_lookup_valuesinput) + (dst_negative_scale_scalar_lookup_valuesinput))) + (((dst_negative_code_scalar_lookup_valuesinput) + (dst_negative_scale_scalar_lookup_valuesinput)) * S ((dst_negative_code_scalar_lookup_valuesinput) + (dst_negative_scale_scalar_lookup_valuesinput)) + ((dst_negative_scale_scalar_lookup_valuesinput) + (dst_negative_scale_scalar_lookup_valuesinput)))))) /\ (((((exists ff_h_pvs_scalar_lookup_valuesinputpositive. ff_h_pvs_scalar_lookup_valuesinputpositive + S (dst_positive_scalar_lookup_valuesinput) = S ((S (i)) * dst_positive_scale_scalar_lookup_valuesinput)) /\ exists ff_q_pvs_scalar_lookup_valuesinputpositive. dst_positive_code_scalar_lookup_valuesinput = ff_q_pvs_scalar_lookup_valuesinputpositive * S ((S (i)) * dst_positive_scale_scalar_lookup_valuesinput) + (dst_positive_scalar_lookup_valuesinput))) /\ (((((exists ff_h_pvs_scalar_lookup_valuesinputnegative. ff_h_pvs_scalar_lookup_valuesinputnegative + S (dst_negative_scalar_lookup_valuesinput) = S ((S (i)) * dst_negative_scale_scalar_lookup_valuesinput)) /\ exists ff_q_pvs_scalar_lookup_valuesinputnegative. dst_negative_code_scalar_lookup_valuesinput = ff_q_pvs_scalar_lookup_valuesinputnegative * S ((S (i)) * dst_negative_scale_scalar_lookup_valuesinput) + (dst_negative_scalar_lookup_valuesinput))) /\ (exists ge_balance_positive_scalar_lookup_valuesinputvalue ge_balance_negative_scalar_lookup_valuesinputvalue. (((((b) = 2 * (ge_balance_positive_scalar_lookup_valuesinputvalue) /\ (ge_balance_negative_scalar_lookup_valuesinputvalue) = 0) \/ exists ge_signed_half_scalar_lookup_valuesinputvaluedecode. (((b) = 2 * ge_signed_half_scalar_lookup_valuesinputvaluedecode + 1 /\ (ge_balance_positive_scalar_lookup_valuesinputvalue) = 0) /\ (ge_balance_negative_scalar_lookup_valuesinputvalue) = S ge_signed_half_scalar_lookup_valuesinputvaluedecode))) /\ ((dst_positive_scalar_lookup_valuesinput) + ge_balance_negative_scalar_lookup_valuesinputvalue = (dst_negative_scalar_lookup_valuesinput) + ge_balance_positive_scalar_lookup_valuesinputvalue))))))))) /\ (((exists dst_positive_code_scalar_lookup_valuesoutput dst_positive_scale_scalar_lookup_valuesoutput dst_negative_code_scalar_lookup_valuesoutput dst_negative_scale_scalar_lookup_valuesoutput dst_positive_scalar_lookup_valuesoutput dst_negative_scalar_lookup_valuesoutput. (((G) = (((((dst_positive_code_scalar_lookup_valuesoutput) + (dst_positive_scale_scalar_lookup_valuesoutput)) * S ((dst_positive_code_scalar_lookup_valuesoutput) + (dst_positive_scale_scalar_lookup_valuesoutput)) + ((dst_positive_scale_scalar_lookup_valuesoutput) + (dst_positive_scale_scalar_lookup_valuesoutput))) + (((dst_negative_code_scalar_lookup_valuesoutput) + (dst_negative_scale_scalar_lookup_valuesoutput)) * S ((dst_negative_code_scalar_lookup_valuesoutput) + (dst_negative_scale_scalar_lookup_valuesoutput)) + ((dst_negative_scale_scalar_lookup_valuesoutput) + (dst_negative_scale_scalar_lookup_valuesoutput)))) * S ((((dst_positive_code_scalar_lookup_valuesoutput) + (dst_positive_scale_scalar_lookup_valuesoutput)) * S ((dst_positive_code_scalar_lookup_valuesoutput) + (dst_positive_scale_scalar_lookup_valuesoutput)) + ((dst_positive_scale_scalar_lookup_valuesoutput) + (dst_positive_scale_scalar_lookup_valuesoutput))) + (((dst_negative_code_scalar_lookup_valuesoutput) + (dst_negative_scale_scalar_lookup_valuesoutput)) * S ((dst_negative_code_scalar_lookup_valuesoutput) + (dst_negative_scale_scalar_lookup_valuesoutput)) + ((dst_negative_scale_scalar_lookup_valuesoutput) + (dst_negative_scale_scalar_lookup_valuesoutput)))) + ((((dst_negative_code_scalar_lookup_valuesoutput) + (dst_negative_scale_scalar_lookup_valuesoutput)) * S ((dst_negative_code_scalar_lookup_valuesoutput) + (dst_negative_scale_scalar_lookup_valuesoutput)) + ((dst_negative_scale_scalar_lookup_valuesoutput) + (dst_negative_scale_scalar_lookup_valuesoutput))) + (((dst_negative_code_scalar_lookup_valuesoutput) + (dst_negative_scale_scalar_lookup_valuesoutput)) * S ((dst_negative_code_scalar_lookup_valuesoutput) + (dst_negative_scale_scalar_lookup_valuesoutput)) + ((dst_negative_scale_scalar_lookup_valuesoutput) + (dst_negative_scale_scalar_lookup_valuesoutput)))))) /\ (((((exists ff_h_pvs_scalar_lookup_valuesoutputpositive. ff_h_pvs_scalar_lookup_valuesoutputpositive + S (dst_positive_scalar_lookup_valuesoutput) = S ((S (i)) * dst_positive_scale_scalar_lookup_valuesoutput)) /\ exists ff_q_pvs_scalar_lookup_valuesoutputpositive. dst_positive_code_scalar_lookup_valuesoutput = ff_q_pvs_scalar_lookup_valuesoutputpositive * S ((S (i)) * dst_positive_scale_scalar_lookup_valuesoutput) + (dst_positive_scalar_lookup_valuesoutput))) /\ (((((exists ff_h_pvs_scalar_lookup_valuesoutputnegative. ff_h_pvs_scalar_lookup_valuesoutputnegative + S (dst_negative_scalar_lookup_valuesoutput) = S ((S (i)) * dst_negative_scale_scalar_lookup_valuesoutput)) /\ exists ff_q_pvs_scalar_lookup_valuesoutputnegative. dst_negative_code_scalar_lookup_valuesoutput = ff_q_pvs_scalar_lookup_valuesoutputnegative * S ((S (i)) * dst_negative_scale_scalar_lookup_valuesoutput) + (dst_negative_scalar_lookup_valuesoutput))) /\ (exists ge_balance_positive_scalar_lookup_valuesoutputvalue ge_balance_negative_scalar_lookup_valuesoutputvalue. (((((c) = 2 * (ge_balance_positive_scalar_lookup_valuesoutputvalue) /\ (ge_balance_negative_scalar_lookup_valuesoutputvalue) = 0) \/ exists ge_signed_half_scalar_lookup_valuesoutputvaluedecode. (((c) = 2 * ge_signed_half_scalar_lookup_valuesoutputvaluedecode + 1 /\ (ge_balance_positive_scalar_lookup_valuesoutputvalue) = 0) /\ (ge_balance_negative_scalar_lookup_valuesoutputvalue) = S ge_signed_half_scalar_lookup_valuesoutputvaluedecode))) /\ ((dst_positive_scalar_lookup_valuesoutput) + ge_balance_negative_scalar_lookup_valuesoutputvalue = (dst_negative_scalar_lookup_valuesoutput) + ge_balance_positive_scalar_lookup_valuesoutputvalue))))))))) /\ (exists sto_ap_scalar_lookup_valuesoperation sto_an_scalar_lookup_valuesoperation sto_bp_scalar_lookup_valuesoperation sto_bn_scalar_lookup_valuesoperation sto_cp_scalar_lookup_valuesoperation sto_cn_scalar_lookup_valuesoperation. (((((a) = 2 * (sto_ap_scalar_lookup_valuesoperation) /\ (sto_an_scalar_lookup_valuesoperation) = 0) \/ exists ge_signed_half_scalar_lookup_valuesoperationleft. (((a) = 2 * ge_signed_half_scalar_lookup_valuesoperationleft + 1 /\ (sto_ap_scalar_lookup_valuesoperation) = 0) /\ (sto_an_scalar_lookup_valuesoperation) = S ge_signed_half_scalar_lookup_valuesoperationleft))) /\ ((((((b) = 2 * (sto_bp_scalar_lookup_valuesoperation) /\ (sto_bn_scalar_lookup_valuesoperation) = 0) \/ exists ge_signed_half_scalar_lookup_valuesoperationright. (((b) = 2 * ge_signed_half_scalar_lookup_valuesoperationright + 1 /\ (sto_bp_scalar_lookup_valuesoperation) = 0) /\ (sto_bn_scalar_lookup_valuesoperation) = S ge_signed_half_scalar_lookup_valuesoperationright))) /\ ((((((c) = 2 * (sto_cp_scalar_lookup_valuesoperation) /\ (sto_cn_scalar_lookup_valuesoperation) = 0) \/ exists ge_signed_half_scalar_lookup_valuesoperationoutput. (((c) = 2 * ge_signed_half_scalar_lookup_valuesoperationoutput + 1 /\ (sto_cp_scalar_lookup_valuesoperation) = 0) /\ (sto_cn_scalar_lookup_valuesoperation) = S ge_signed_half_scalar_lookup_valuesoperationoutput))) /\ ((sto_ap_scalar_lookup_valuesoperation * sto_bp_scalar_lookup_valuesoperation + sto_an_scalar_lookup_valuesoperation * sto_bn_scalar_lookup_valuesoperation) + sto_cn_scalar_lookup_valuesoperation = (sto_ap_scalar_lookup_valuesoperation * sto_bn_scalar_lookup_valuesoperation + sto_an_scalar_lookup_valuesoperation * sto_bp_scalar_lookup_valuesoperation) + sto_cp_scalar_lookup_valuesoperation))))))))))
  15. 0015specialize hop_right_right (i)
  16. 0016apply hop_right_right
  17. 0017exact hi
  18. 0018cases he
  19. 0019cases he_witness
  20. 0020cases he_witness_witness
  21. 0021cases he_witness_witness_right
  22. 0022have heq0 : x = b
  23. 0023specialize divisor_signed_table_at_functional (F)
  24. 0024specialize divisor_signed_table_at_functional (i)
  25. 0025specialize divisor_signed_table_at_functional (x)
  26. 0026specialize divisor_signed_table_at_functional (b)
  27. 0027apply divisor_signed_table_at_functional
  28. 0028exact he_witness_witness_left
  29. 0029exact h0
  30. 0030rewrite heq0 at he_witness_witness_right_right
  31. 0031rewrite heq0 at he_witness_witness_right_right
  32. 0032have heq1 : x1 = c
  33. 0033specialize divisor_signed_table_at_functional (G)
  34. 0034specialize divisor_signed_table_at_functional (i)
  35. 0035specialize divisor_signed_table_at_functional (x1)
  36. 0036specialize divisor_signed_table_at_functional (c)
  37. 0037apply divisor_signed_table_at_functional
  38. 0038exact he_witness_witness_right_left
  39. 0039exact h1
  40. 0040rewrite heq1 at he_witness_witness_right_right
  41. 0041rewrite heq1 at he_witness_witness_right_right
  42. 0042exact he_witness_witness_right_right