Constructed Dirichlet convolution — exact evidence

Current Alpha v34 checked use; first admitted v31; not Stable. Original HA and the independently compiled Lean checker have freshly verified the complete bundle before this page was generated.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

270 checked bundle nodes · 712 proof edges · 18180 body proof nodes.

Literal self-contained proof bundle · SHA-256 313316e788a10dc281dfb0541a447bad9b7b26bbbd68b1030db89d8d28c5a38b

dirichlet_commutativity_candidate.py · dirichlet_convolution_candidate.py

Unchanged historical local checkpoint record · Historical snapshot manifest. Those records retain their original non-admitting flags; current authority comes from the separate freshly verified v31 release.

Exact theorem nodes and inherited prerequisites

DC0001 dirichlet_convolution_entry_zero · actual bundle node 229
DC0002 dirichlet_convolution_entry_from_quotient · actual bundle node 230
DC0003 dirichlet_convolution_entry_from_nondivisor · actual bundle node 231
DC0004 dirichlet_convolution_entry_omitted_value · actual bundle node 232
DC0005 dirichlet_convolution_entry_quotient_product · actual bundle node 233
DC0006 dirichlet_convolution_entry_functional · actual bundle node 234
DC0007 dirichlet_convolution_entry_exists · actual bundle node 235
DC0008 dirichlet_convolution_prefix_zero_constructor · actual bundle node 236
DC0009 dirichlet_convolution_prefix_append · actual bundle node 237
DC000A dirichlet_convolution_prefix_exists · actual bundle node 238
DC000B dirichlet_convolution_prefix_lookup · actual bundle node 239
DC000C dirichlet_convolution_prefix_extensional · actual bundle node 240
DC000D dirichlet_convolution_prefix_restrict · actual bundle node 241
DC000E dirichlet_convolution_prefix_quotient_entry · actual bundle node 242
DC000F dirichlet_convolution_prefix_omitted_entry · actual bundle node 243
DC0010 dirichlet_convolution_sum_exists · actual bundle node 244
DC0011 dirichlet_convolution_sum_functional · actual bundle node 245
DC0012 dirichlet_convolution_sum_exists_unique · actual bundle node 246
DC0013 dirichlet_convolution_sum_zero_excluded · actual bundle node 247
DC0014 dirichlet_convolution_entry_positive_source_extensional · actual bundle node 248
DC0015 dirichlet_convolution_prefix_positive_source_extensional · actual bundle node 249
DC0016 dirichlet_convolution_positive_source_extensional · actual bundle node 250
DC0017 dirichlet_convolution_positive_source_transport · actual bundle node 251
DC0018 dirichlet_convolution_table_zero_constructor · actual bundle node 252
DC0019 dirichlet_convolution_table_append · actual bundle node 253
DC001A dirichlet_convolution_table_exists · actual bundle node 254
DC001B dirichlet_convolution_table_lookup · actual bundle node 255
DC001C dirichlet_convolution_table_extensional · actual bundle node 256
DC001D dirichlet_convolution_table_exists_extensionally_unique · actual bundle node 257
DC001E dirichlet_convolution_table_restrict · actual bundle node 258
DC001F dirichlet_convolution_entry_complement · actual bundle node 259
DC0020 dirichlet_convolution_prefix_value_from_entry · actual bundle node 260
DC0021 dirichlet_convolution_prefix_complement_reindex · actual bundle node 261
DC0022 dirichlet_convolution_sum_commutative · actual bundle node 262
DC0023 dirichlet_convolution_sum_swap · actual bundle node 263
DC0024 dirichlet_convolution_table_commutative · actual bundle node 264
DC0025 dirichlet_convolution_entry_past_support_zero · actual bundle node 265
DC0026 dirichlet_convolution_prefix_zero_tail · actual bundle node 266
DC0027 dirichlet_convolution_from_padded_prefix · actual bundle node 267
DC0028 dirichlet_convolution_padded_prefix_iff · actual bundle node 268

arithmetic_signed_sum_exists · checked inherited prerequisite

Exact statement in the checked dependency cone

forall N F l. (exists dst_positive_code_sum_exists_input dst_positive_scale_sum_exists_input dst_negative_code_sum_exists_input dst_negative_scale_sum_exists_input. (((F) = (((((dst_positive_code_sum_exists_input) + (dst_positive_scale_sum_exists_input)) * S ((dst_positive_code_sum_exists_input) + (dst_positive_scale_sum_exists_input)) + ((dst_positive_scale_sum_exists_input) + (dst_positive_scale_sum_exists_input))) + (((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) * S ((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) + ((dst_negative_scale_sum_exists_input) + (dst_negative_scale_sum_exists_input)))) * S ((((dst_positive_code_sum_exists_input) + (dst_positive_scale_sum_exists_input)) * S ((dst_positive_code_sum_exists_input) + (dst_positive_scale_sum_exists_input)) + ((dst_positive_scale_sum_exists_input) + (dst_positive_scale_sum_exists_input))) + (((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) * S ((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) + ((dst_negative_scale_sum_exists_input) + (dst_negative_scale_sum_exists_input)))) + ((((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) * S ((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) + ((dst_negative_scale_sum_exists_input) + (dst_negative_scale_sum_exists_input))) + (((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) * S ((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) + ((dst_negative_scale_sum_exists_input) + (dst_negative_scale_sum_exists_input)))))) /\ (forall dst_index_sum_exists_input. (exists pvs_le_gap_sum_exists_inputdomain. pvs_le_gap_sum_exists_inputdomain + (dst_index_sum_exists_input) = (N)) -> exists dst_positive_sum_exists_input dst_negative_sum_exists_input dst_value_sum_exists_input. ((((exists ff_h_pvs_sum_exists_inputentrypositive. ff_h_pvs_sum_exists_inputentrypositive + S (dst_positive_sum_exists_input) = S ((S (dst_index_sum_exists_input)) * dst_positive_scale_sum_exists_input)) /\ exists ff_q_pvs_sum_exists_inputentrypositive. dst_positive_code_sum_exists_input = ff_q_pvs_sum_exists_inputentrypositive * S ((S (dst_index_sum_exists_input)) * dst_positive_scale_sum_exists_input) + (dst_positive_sum_exists_input))) /\ (((((exists ff_h_pvs_sum_exists_inputentrynegative. ff_h_pvs_sum_exists_inputentrynegative + S (dst_negative_sum_exists_input) = S ((S (dst_index_sum_exists_input)) * dst_negative_scale_sum_exists_input)) /\ exists ff_q_pvs_sum_exists_inputentrynegative. dst_negative_code_sum_exists_input = ff_q_pvs_sum_exists_inputentrynegative * S ((S (dst_index_sum_exists_input)) * dst_negative_scale_sum_exists_input) + (dst_negative_sum_exists_input))) /\ (exists ge_balance_positive_sum_exists_inputentryvalue ge_balance_negative_sum_exists_inputentryvalue. (((((dst_value_sum_exists_input) = 2 * (ge_balance_positive_sum_exists_inputentryvalue) /\ (ge_balance_negative_sum_exists_inputentryvalue) = 0) \/ exists ge_signed_half_sum_exists_inputentryvaluedecode. (((dst_value_sum_exists_input) = 2 * ge_signed_half_sum_exists_inputentryvaluedecode + 1 /\ (ge_balance_positive_sum_exists_inputentryvalue) = 0) /\ (ge_balance_negative_sum_exists_inputentryvalue) = S ge_signed_half_sum_exists_inputentryvaluedecode))) /\ ((dst_positive_sum_exists_input) + ge_balance_negative_sum_exists_inputentryvalue = (dst_negative_sum_exists_input) + ge_balance_positive_sum_exists_inputentryvalue))))))))) -> exists z. (exists dst_positive_code_sum_exists_output dst_positive_scale_sum_exists_output dst_negative_code_sum_exists_output dst_negative_scale_sum_exists_output dst_positive_sum_sum_exists_output dst_negative_sum_sum_exists_output. (((F) = (((((dst_positive_code_sum_exists_output) + (dst_positive_scale_sum_exists_output)) * S ((dst_positive_code_sum_exists_output) + (dst_positive_scale_sum_exists_output)) + ((dst_positive_scale_sum_exists_output) + (dst_positive_scale_sum_exists_output))) + (((dst_negative_code_sum_exists_output) + (dst_negative_scale_sum_exists_output)) * S ((dst_negative_code_sum_exists_output) + (dst_negative_scale_sum_exists_output)) + ((dst_negative_scale_sum_exists_output) + (dst_negative_scale_sum_exists_output)))) * S ((((dst_positive_code_sum_exists_output) + (dst_positive_scale_sum_exists_output)) * S ((dst_positive_code_sum_exists_output) + (dst_positive_scale_sum_exists_output)) + ((dst_positive_scale_sum_exists_output) + (dst_positive_scale_sum_exists_output))) + (((dst_negative_code_sum_exists_output) + (dst_negative_scale_sum_exists_output)) * S ((dst_negative_code_sum_exists_output) + (dst_negative_scale_sum_exists_output)) + ((dst_negative_scale_sum_exists_output) + (dst_negative_scale_sum_exists_output)))) + ((((dst_negative_code_sum_exists_output) + (dst_negative_scale_sum_exists_output)) * S ((dst_negative_code_sum_exists_output) + (dst_negative_scale_sum_exists_output)) + ((dst_negative_scale_sum_exists_output) + (dst_negative_scale_sum_exists_output))) + (((dst_negative_code_sum_exists_output) + (dst_negative_scale_sum_exists_output)) * S ((dst_negative_code_sum_exists_output) + (dst_negative_scale_sum_exists_output)) + ((dst_negative_scale_sum_exists_output) + (dst_negative_scale_sum_exists_output)))))) /\ (((exists fs_u_dst_sum_exists_outputpositive fs_v_dst_sum_exists_outputpositive. ((((exists fs_h_dst_sum_exists_outputpositive_body_start. fs_h_dst_sum_exists_outputpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_exists_outputpositive)) /\ exists fs_q_dst_sum_exists_outputpositive_body_start. fs_u_dst_sum_exists_outputpositive = fs_q_dst_sum_exists_outputpositive_body_start * S ((S (0)) * fs_v_dst_sum_exists_outputpositive) + (0))) /\ ((((exists fs_h_dst_sum_exists_outputpositive_body_terminal. fs_h_dst_sum_exists_outputpositive_body_terminal + S (dst_positive_sum_sum_exists_output) = S ((S (l)) * fs_v_dst_sum_exists_outputpositive)) /\ exists fs_q_dst_sum_exists_outputpositive_body_terminal. fs_u_dst_sum_exists_outputpositive = fs_q_dst_sum_exists_outputpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_exists_outputpositive) + (dst_positive_sum_sum_exists_output))) /\ forall fs_i_dst_sum_exists_outputpositive_body_steps. (exists fs_lt_dst_sum_exists_outputpositive_body_steps_bound. fs_lt_dst_sum_exists_outputpositive_body_steps_bound + S fs_i_dst_sum_exists_outputpositive_body_steps = l) -> exists fs_a_dst_sum_exists_outputpositive_body_steps fs_r_dst_sum_exists_outputpositive_body_steps fs_s_dst_sum_exists_outputpositive_body_steps. ((((exists fs_h_dst_sum_exists_outputpositive_body_steps_summand. fs_h_dst_sum_exists_outputpositive_body_steps_summand + S (fs_a_dst_sum_exists_outputpositive_body_steps) = S ((S (fs_i_dst_sum_exists_outputpositive_body_steps)) * dst_positive_scale_sum_exists_output)) /\ exists fs_q_dst_sum_exists_outputpositive_body_steps_summand. dst_positive_code_sum_exists_output = fs_q_dst_sum_exists_outputpositive_body_steps_summand * S ((S (fs_i_dst_sum_exists_outputpositive_body_steps)) * dst_positive_scale_sum_exists_output) + (fs_a_dst_sum_exists_outputpositive_body_steps))) /\ ((((exists fs_h_dst_sum_exists_outputpositive_body_steps_partial. fs_h_dst_sum_exists_outputpositive_body_steps_partial + S (fs_r_dst_sum_exists_outputpositive_body_steps) = S ((S (fs_i_dst_sum_exists_outputpositive_body_steps)) * fs_v_dst_sum_exists_outputpositive)) /\ exists fs_q_dst_sum_exists_outputpositive_body_steps_partial. fs_u_dst_sum_exists_outputpositive = fs_q_dst_sum_exists_outputpositive_body_steps_partial * S ((S (fs_i_dst_sum_exists_outputpositive_body_steps)) * fs_v_dst_sum_exists_outputpositive) + (fs_r_dst_sum_exists_outputpositive_body_steps))) /\ ((((exists fs_h_dst_sum_exists_outputpositive_body_steps_successor. fs_h_dst_sum_exists_outputpositive_body_steps_successor + S (fs_s_dst_sum_exists_outputpositive_body_steps) = S ((S (S fs_i_dst_sum_exists_outputpositive_body_steps)) * fs_v_dst_sum_exists_outputpositive)) /\ exists fs_q_dst_sum_exists_outputpositive_body_steps_successor. fs_u_dst_sum_exists_outputpositive = fs_q_dst_sum_exists_outputpositive_body_steps_successor * S ((S (S fs_i_dst_sum_exists_outputpositive_body_steps)) * fs_v_dst_sum_exists_outputpositive) + (fs_s_dst_sum_exists_outputpositive_body_steps))) /\ fs_s_dst_sum_exists_outputpositive_body_steps = fs_r_dst_sum_exists_outputpositive_body_steps + fs_a_dst_sum_exists_outputpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_exists_outputnegative fs_v_dst_sum_exists_outputnegative. ((((exists fs_h_dst_sum_exists_outputnegative_body_start. fs_h_dst_sum_exists_outputnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_exists_outputnegative)) /\ exists fs_q_dst_sum_exists_outputnegative_body_start. fs_u_dst_sum_exists_outputnegative = fs_q_dst_sum_exists_outputnegative_body_start * S ((S (0)) * fs_v_dst_sum_exists_outputnegative) + (0))) /\ ((((exists fs_h_dst_sum_exists_outputnegative_body_terminal. fs_h_dst_sum_exists_outputnegative_body_terminal + S (dst_negative_sum_sum_exists_output) = S ((S (l)) * fs_v_dst_sum_exists_outputnegative)) /\ exists fs_q_dst_sum_exists_outputnegative_body_terminal. fs_u_dst_sum_exists_outputnegative = fs_q_dst_sum_exists_outputnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_exists_outputnegative) + (dst_negative_sum_sum_exists_output))) /\ forall fs_i_dst_sum_exists_outputnegative_body_steps. (exists fs_lt_dst_sum_exists_outputnegative_body_steps_bound. fs_lt_dst_sum_exists_outputnegative_body_steps_bound + S fs_i_dst_sum_exists_outputnegative_body_steps = l) -> exists fs_a_dst_sum_exists_outputnegative_body_steps fs_r_dst_sum_exists_outputnegative_body_steps fs_s_dst_sum_exists_outputnegative_body_steps. ((((exists fs_h_dst_sum_exists_outputnegative_body_steps_summand. fs_h_dst_sum_exists_outputnegative_body_steps_summand + S (fs_a_dst_sum_exists_outputnegative_body_steps) = S ((S (fs_i_dst_sum_exists_outputnegative_body_steps)) * dst_negative_scale_sum_exists_output)) /\ exists fs_q_dst_sum_exists_outputnegative_body_steps_summand. dst_negative_code_sum_exists_output = fs_q_dst_sum_exists_outputnegative_body_steps_summand * S ((S (fs_i_dst_sum_exists_outputnegative_body_steps)) * dst_negative_scale_sum_exists_output) + (fs_a_dst_sum_exists_outputnegative_body_steps))) /\ ((((exists fs_h_dst_sum_exists_outputnegative_body_steps_partial. fs_h_dst_sum_exists_outputnegative_body_steps_partial + S (fs_r_dst_sum_exists_outputnegative_body_steps) = S ((S (fs_i_dst_sum_exists_outputnegative_body_steps)) * fs_v_dst_sum_exists_outputnegative)) /\ exists fs_q_dst_sum_exists_outputnegative_body_steps_partial. fs_u_dst_sum_exists_outputnegative = fs_q_dst_sum_exists_outputnegative_body_steps_partial * S ((S (fs_i_dst_sum_exists_outputnegative_body_steps)) * fs_v_dst_sum_exists_outputnegative) + (fs_r_dst_sum_exists_outputnegative_body_steps))) /\ ((((exists fs_h_dst_sum_exists_outputnegative_body_steps_successor. fs_h_dst_sum_exists_outputnegative_body_steps_successor + S (fs_s_dst_sum_exists_outputnegative_body_steps) = S ((S (S fs_i_dst_sum_exists_outputnegative_body_steps)) * fs_v_dst_sum_exists_outputnegative)) /\ exists fs_q_dst_sum_exists_outputnegative_body_steps_successor. fs_u_dst_sum_exists_outputnegative = fs_q_dst_sum_exists_outputnegative_body_steps_successor * S ((S (S fs_i_dst_sum_exists_outputnegative_body_steps)) * fs_v_dst_sum_exists_outputnegative) + (fs_s_dst_sum_exists_outputnegative_body_steps))) /\ fs_s_dst_sum_exists_outputnegative_body_steps = fs_r_dst_sum_exists_outputnegative_body_steps + fs_a_dst_sum_exists_outputnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_exists_outputresult ge_balance_negative_sum_exists_outputresult. (((((z) = 2 * (ge_balance_positive_sum_exists_outputresult) /\ (ge_balance_negative_sum_exists_outputresult) = 0) \/ exists ge_signed_half_sum_exists_outputresultdecode. (((z) = 2 * ge_signed_half_sum_exists_outputresultdecode + 1 /\ (ge_balance_positive_sum_exists_outputresult) = 0) /\ (ge_balance_negative_sum_exists_outputresult) = S ge_signed_half_sum_exists_outputresultdecode))) /\ ((dst_positive_sum_sum_exists_output) + ge_balance_negative_sum_exists_outputresult = (dst_negative_sum_sum_exists_output) + ge_balance_positive_sum_exists_outputresult)))))))))

arithmetic_signed_table_append · checked inherited prerequisite

Exact statement in the checked dependency cone

forall N F z. (exists dst_positive_code_append_input dst_positive_scale_append_input dst_negative_code_append_input dst_negative_scale_append_input. (((F) = (((((dst_positive_code_append_input) + (dst_positive_scale_append_input)) * S ((dst_positive_code_append_input) + (dst_positive_scale_append_input)) + ((dst_positive_scale_append_input) + (dst_positive_scale_append_input))) + (((dst_negative_code_append_input) + (dst_negative_scale_append_input)) * S ((dst_negative_code_append_input) + (dst_negative_scale_append_input)) + ((dst_negative_scale_append_input) + (dst_negative_scale_append_input)))) * S ((((dst_positive_code_append_input) + (dst_positive_scale_append_input)) * S ((dst_positive_code_append_input) + (dst_positive_scale_append_input)) + ((dst_positive_scale_append_input) + (dst_positive_scale_append_input))) + (((dst_negative_code_append_input) + (dst_negative_scale_append_input)) * S ((dst_negative_code_append_input) + (dst_negative_scale_append_input)) + ((dst_negative_scale_append_input) + (dst_negative_scale_append_input)))) + ((((dst_negative_code_append_input) + (dst_negative_scale_append_input)) * S ((dst_negative_code_append_input) + (dst_negative_scale_append_input)) + ((dst_negative_scale_append_input) + (dst_negative_scale_append_input))) + (((dst_negative_code_append_input) + (dst_negative_scale_append_input)) * S ((dst_negative_code_append_input) + (dst_negative_scale_append_input)) + ((dst_negative_scale_append_input) + (dst_negative_scale_append_input)))))) /\ (forall dst_index_append_input. (exists pvs_le_gap_append_inputdomain. pvs_le_gap_append_inputdomain + (dst_index_append_input) = (N)) -> exists dst_positive_append_input dst_negative_append_input dst_value_append_input. ((((exists ff_h_pvs_append_inputentrypositive. ff_h_pvs_append_inputentrypositive + S (dst_positive_append_input) = S ((S (dst_index_append_input)) * dst_positive_scale_append_input)) /\ exists ff_q_pvs_append_inputentrypositive. dst_positive_code_append_input = ff_q_pvs_append_inputentrypositive * S ((S (dst_index_append_input)) * dst_positive_scale_append_input) + (dst_positive_append_input))) /\ (((((exists ff_h_pvs_append_inputentrynegative. ff_h_pvs_append_inputentrynegative + S (dst_negative_append_input) = S ((S (dst_index_append_input)) * dst_negative_scale_append_input)) /\ exists ff_q_pvs_append_inputentrynegative. dst_negative_code_append_input = ff_q_pvs_append_inputentrynegative * S ((S (dst_index_append_input)) * dst_negative_scale_append_input) + (dst_negative_append_input))) /\ (exists ge_balance_positive_append_inputentryvalue ge_balance_negative_append_inputentryvalue. (((((dst_value_append_input) = 2 * (ge_balance_positive_append_inputentryvalue) /\ (ge_balance_negative_append_inputentryvalue) = 0) \/ exists ge_signed_half_append_inputentryvaluedecode. (((dst_value_append_input) = 2 * ge_signed_half_append_inputentryvaluedecode + 1 /\ (ge_balance_positive_append_inputentryvalue) = 0) /\ (ge_balance_negative_append_inputentryvalue) = S ge_signed_half_append_inputentryvaluedecode))) /\ ((dst_positive_append_input) + ge_balance_negative_append_inputentryvalue = (dst_negative_append_input) + ge_balance_positive_append_inputentryvalue))))))))) -> exists G. (((exists dst_positive_code_append_outputtable dst_positive_scale_append_outputtable dst_negative_code_append_outputtable dst_negative_scale_append_outputtable. (((G) = (((((dst_positive_code_append_outputtable) + (dst_positive_scale_append_outputtable)) * S ((dst_positive_code_append_outputtable) + (dst_positive_scale_append_outputtable)) + ((dst_positive_scale_append_outputtable) + (dst_positive_scale_append_outputtable))) + (((dst_negative_code_append_outputtable) + (dst_negative_scale_append_outputtable)) * S ((dst_negative_code_append_outputtable) + (dst_negative_scale_append_outputtable)) + ((dst_negative_scale_append_outputtable) + (dst_negative_scale_append_outputtable)))) * S ((((dst_positive_code_append_outputtable) + (dst_positive_scale_append_outputtable)) * S ((dst_positive_code_append_outputtable) + (dst_positive_scale_append_outputtable)) + ((dst_positive_scale_append_outputtable) + (dst_positive_scale_append_outputtable))) + (((dst_negative_code_append_outputtable) + (dst_negative_scale_append_outputtable)) * S ((dst_negative_code_append_outputtable) + (dst_negative_scale_append_outputtable)) + ((dst_negative_scale_append_outputtable) + (dst_negative_scale_append_outputtable)))) + ((((dst_negative_code_append_outputtable) + (dst_negative_scale_append_outputtable)) * S ((dst_negative_code_append_outputtable) + (dst_negative_scale_append_outputtable)) + ((dst_negative_scale_append_outputtable) + (dst_negative_scale_append_outputtable))) + (((dst_negative_code_append_outputtable) + (dst_negative_scale_append_outputtable)) * S ((dst_negative_code_append_outputtable) + (dst_negative_scale_append_outputtable)) + ((dst_negative_scale_append_outputtable) + (dst_negative_scale_append_outputtable)))))) /\ (forall dst_index_append_outputtable. (exists pvs_le_gap_append_outputtabledomain. pvs_le_gap_append_outputtabledomain + (dst_index_append_outputtable) = (S N)) -> exists dst_positive_append_outputtable dst_negative_append_outputtable dst_value_append_outputtable. ((((exists ff_h_pvs_append_outputtableentrypositive. ff_h_pvs_append_outputtableentrypositive + S (dst_positive_append_outputtable) = S ((S (dst_index_append_outputtable)) * dst_positive_scale_append_outputtable)) /\ exists ff_q_pvs_append_outputtableentrypositive. dst_positive_code_append_outputtable = ff_q_pvs_append_outputtableentrypositive * S ((S (dst_index_append_outputtable)) * dst_positive_scale_append_outputtable) + (dst_positive_append_outputtable))) /\ (((((exists ff_h_pvs_append_outputtableentrynegative. ff_h_pvs_append_outputtableentrynegative + S (dst_negative_append_outputtable) = S ((S (dst_index_append_outputtable)) * dst_negative_scale_append_outputtable)) /\ exists ff_q_pvs_append_outputtableentrynegative. dst_negative_code_append_outputtable = ff_q_pvs_append_outputtableentrynegative * S ((S (dst_index_append_outputtable)) * dst_negative_scale_append_outputtable) + (dst_negative_append_outputtable))) /\ (exists ge_balance_positive_append_outputtableentryvalue ge_balance_negative_append_outputtableentryvalue. (((((dst_value_append_outputtable) = 2 * (ge_balance_positive_append_outputtableentryvalue) /\ (ge_balance_negative_append_outputtableentryvalue) = 0) \/ exists ge_signed_half_append_outputtableentryvaluedecode. (((dst_value_append_outputtable) = 2 * ge_signed_half_append_outputtableentryvaluedecode + 1 /\ (ge_balance_positive_append_outputtableentryvalue) = 0) /\ (ge_balance_negative_append_outputtableentryvalue) = S ge_signed_half_append_outputtableentryvaluedecode))) /\ ((dst_positive_append_outputtable) + ge_balance_negative_append_outputtableentryvalue = (dst_negative_append_outputtable) + ge_balance_positive_append_outputtableentryvalue))))))))) /\ (((forall dst_index_append_outputprefix dst_first_append_outputprefix dst_second_append_outputprefix. (exists pvs_gap_append_outputprefixbound. pvs_gap_append_outputprefixbound + S (dst_index_append_outputprefix) = (S N)) -> (exists dst_positive_code_append_outputprefixfirst dst_positive_scale_append_outputprefixfirst dst_negative_code_append_outputprefixfirst dst_negative_scale_append_outputprefixfirst dst_positive_append_outputprefixfirst dst_negative_append_outputprefixfirst. (((F) = (((((dst_positive_code_append_outputprefixfirst) + (dst_positive_scale_append_outputprefixfirst)) * S ((dst_positive_code_append_outputprefixfirst) + (dst_positive_scale_append_outputprefixfirst)) + ((dst_positive_scale_append_outputprefixfirst) + (dst_positive_scale_append_outputprefixfirst))) + (((dst_negative_code_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)) * S ((dst_negative_code_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)) + ((dst_negative_scale_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)))) * S ((((dst_positive_code_append_outputprefixfirst) + (dst_positive_scale_append_outputprefixfirst)) * S ((dst_positive_code_append_outputprefixfirst) + (dst_positive_scale_append_outputprefixfirst)) + ((dst_positive_scale_append_outputprefixfirst) + (dst_positive_scale_append_outputprefixfirst))) + (((dst_negative_code_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)) * S ((dst_negative_code_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)) + ((dst_negative_scale_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)))) + ((((dst_negative_code_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)) * S ((dst_negative_code_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)) + ((dst_negative_scale_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst))) + (((dst_negative_code_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)) * S ((dst_negative_code_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)) + ((dst_negative_scale_append_outputprefixfirst) + (dst_negative_scale_append_outputprefixfirst)))))) /\ (((((exists ff_h_pvs_append_outputprefixfirstpositive. ff_h_pvs_append_outputprefixfirstpositive + S (dst_positive_append_outputprefixfirst) = S ((S (dst_index_append_outputprefix)) * dst_positive_scale_append_outputprefixfirst)) /\ exists ff_q_pvs_append_outputprefixfirstpositive. dst_positive_code_append_outputprefixfirst = ff_q_pvs_append_outputprefixfirstpositive * S ((S (dst_index_append_outputprefix)) * dst_positive_scale_append_outputprefixfirst) + (dst_positive_append_outputprefixfirst))) /\ (((((exists ff_h_pvs_append_outputprefixfirstnegative. ff_h_pvs_append_outputprefixfirstnegative + S (dst_negative_append_outputprefixfirst) = S ((S (dst_index_append_outputprefix)) * dst_negative_scale_append_outputprefixfirst)) /\ exists ff_q_pvs_append_outputprefixfirstnegative. dst_negative_code_append_outputprefixfirst = ff_q_pvs_append_outputprefixfirstnegative * S ((S (dst_index_append_outputprefix)) * dst_negative_scale_append_outputprefixfirst) + (dst_negative_append_outputprefixfirst))) /\ (exists ge_balance_positive_append_outputprefixfirstvalue ge_balance_negative_append_outputprefixfirstvalue. (((((dst_first_append_outputprefix) = 2 * (ge_balance_positive_append_outputprefixfirstvalue) /\ (ge_balance_negative_append_outputprefixfirstvalue) = 0) \/ exists ge_signed_half_append_outputprefixfirstvaluedecode. (((dst_first_append_outputprefix) = 2 * ge_signed_half_append_outputprefixfirstvaluedecode + 1 /\ (ge_balance_positive_append_outputprefixfirstvalue) = 0) /\ (ge_balance_negative_append_outputprefixfirstvalue) = S ge_signed_half_append_outputprefixfirstvaluedecode))) /\ ((dst_positive_append_outputprefixfirst) + ge_balance_negative_append_outputprefixfirstvalue = (dst_negative_append_outputprefixfirst) + ge_balance_positive_append_outputprefixfirstvalue))))))))) -> (exists dst_positive_code_append_outputprefixsecond dst_positive_scale_append_outputprefixsecond dst_negative_code_append_outputprefixsecond dst_negative_scale_append_outputprefixsecond dst_positive_append_outputprefixsecond dst_negative_append_outputprefixsecond. (((G) = (((((dst_positive_code_append_outputprefixsecond) + (dst_positive_scale_append_outputprefixsecond)) * S ((dst_positive_code_append_outputprefixsecond) + (dst_positive_scale_append_outputprefixsecond)) + ((dst_positive_scale_append_outputprefixsecond) + (dst_positive_scale_append_outputprefixsecond))) + (((dst_negative_code_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)) * S ((dst_negative_code_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)) + ((dst_negative_scale_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)))) * S ((((dst_positive_code_append_outputprefixsecond) + (dst_positive_scale_append_outputprefixsecond)) * S ((dst_positive_code_append_outputprefixsecond) + (dst_positive_scale_append_outputprefixsecond)) + ((dst_positive_scale_append_outputprefixsecond) + (dst_positive_scale_append_outputprefixsecond))) + (((dst_negative_code_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)) * S ((dst_negative_code_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)) + ((dst_negative_scale_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)))) + ((((dst_negative_code_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)) * S ((dst_negative_code_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)) + ((dst_negative_scale_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond))) + (((dst_negative_code_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)) * S ((dst_negative_code_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)) + ((dst_negative_scale_append_outputprefixsecond) + (dst_negative_scale_append_outputprefixsecond)))))) /\ (((((exists ff_h_pvs_append_outputprefixsecondpositive. ff_h_pvs_append_outputprefixsecondpositive + S (dst_positive_append_outputprefixsecond) = S ((S (dst_index_append_outputprefix)) * dst_positive_scale_append_outputprefixsecond)) /\ exists ff_q_pvs_append_outputprefixsecondpositive. dst_positive_code_append_outputprefixsecond = ff_q_pvs_append_outputprefixsecondpositive * S ((S (dst_index_append_outputprefix)) * dst_positive_scale_append_outputprefixsecond) + (dst_positive_append_outputprefixsecond))) /\ (((((exists ff_h_pvs_append_outputprefixsecondnegative. ff_h_pvs_append_outputprefixsecondnegative + S (dst_negative_append_outputprefixsecond) = S ((S (dst_index_append_outputprefix)) * dst_negative_scale_append_outputprefixsecond)) /\ exists ff_q_pvs_append_outputprefixsecondnegative. dst_negative_code_append_outputprefixsecond = ff_q_pvs_append_outputprefixsecondnegative * S ((S (dst_index_append_outputprefix)) * dst_negative_scale_append_outputprefixsecond) + (dst_negative_append_outputprefixsecond))) /\ (exists ge_balance_positive_append_outputprefixsecondvalue ge_balance_negative_append_outputprefixsecondvalue. (((((dst_second_append_outputprefix) = 2 * (ge_balance_positive_append_outputprefixsecondvalue) /\ (ge_balance_negative_append_outputprefixsecondvalue) = 0) \/ exists ge_signed_half_append_outputprefixsecondvaluedecode. (((dst_second_append_outputprefix) = 2 * ge_signed_half_append_outputprefixsecondvaluedecode + 1 /\ (ge_balance_positive_append_outputprefixsecondvalue) = 0) /\ (ge_balance_negative_append_outputprefixsecondvalue) = S ge_signed_half_append_outputprefixsecondvaluedecode))) /\ ((dst_positive_append_outputprefixsecond) + ge_balance_negative_append_outputprefixsecondvalue = (dst_negative_append_outputprefixsecond) + ge_balance_positive_append_outputprefixsecondvalue))))))))) -> dst_first_append_outputprefix = dst_second_append_outputprefix) /\ (exists dst_positive_code_append_outputlast dst_positive_scale_append_outputlast dst_negative_code_append_outputlast dst_negative_scale_append_outputlast dst_positive_append_outputlast dst_negative_append_outputlast. (((G) = (((((dst_positive_code_append_outputlast) + (dst_positive_scale_append_outputlast)) * S ((dst_positive_code_append_outputlast) + (dst_positive_scale_append_outputlast)) + ((dst_positive_scale_append_outputlast) + (dst_positive_scale_append_outputlast))) + (((dst_negative_code_append_outputlast) + (dst_negative_scale_append_outputlast)) * S ((dst_negative_code_append_outputlast) + (dst_negative_scale_append_outputlast)) + ((dst_negative_scale_append_outputlast) + (dst_negative_scale_append_outputlast)))) * S ((((dst_positive_code_append_outputlast) + (dst_positive_scale_append_outputlast)) * S ((dst_positive_code_append_outputlast) + (dst_positive_scale_append_outputlast)) + ((dst_positive_scale_append_outputlast) + (dst_positive_scale_append_outputlast))) + (((dst_negative_code_append_outputlast) + (dst_negative_scale_append_outputlast)) * S ((dst_negative_code_append_outputlast) + (dst_negative_scale_append_outputlast)) + ((dst_negative_scale_append_outputlast) + (dst_negative_scale_append_outputlast)))) + ((((dst_negative_code_append_outputlast) + (dst_negative_scale_append_outputlast)) * S ((dst_negative_code_append_outputlast) + (dst_negative_scale_append_outputlast)) + ((dst_negative_scale_append_outputlast) + (dst_negative_scale_append_outputlast))) + (((dst_negative_code_append_outputlast) + (dst_negative_scale_append_outputlast)) * S ((dst_negative_code_append_outputlast) + (dst_negative_scale_append_outputlast)) + ((dst_negative_scale_append_outputlast) + (dst_negative_scale_append_outputlast)))))) /\ (((((exists ff_h_pvs_append_outputlastpositive. ff_h_pvs_append_outputlastpositive + S (dst_positive_append_outputlast) = S ((S (S N)) * dst_positive_scale_append_outputlast)) /\ exists ff_q_pvs_append_outputlastpositive. dst_positive_code_append_outputlast = ff_q_pvs_append_outputlastpositive * S ((S (S N)) * dst_positive_scale_append_outputlast) + (dst_positive_append_outputlast))) /\ (((((exists ff_h_pvs_append_outputlastnegative. ff_h_pvs_append_outputlastnegative + S (dst_negative_append_outputlast) = S ((S (S N)) * dst_negative_scale_append_outputlast)) /\ exists ff_q_pvs_append_outputlastnegative. dst_negative_code_append_outputlast = ff_q_pvs_append_outputlastnegative * S ((S (S N)) * dst_negative_scale_append_outputlast) + (dst_negative_append_outputlast))) /\ (exists ge_balance_positive_append_outputlastvalue ge_balance_negative_append_outputlastvalue. (((((z) = 2 * (ge_balance_positive_append_outputlastvalue) /\ (ge_balance_negative_append_outputlastvalue) = 0) \/ exists ge_signed_half_append_outputlastvaluedecode. (((z) = 2 * ge_signed_half_append_outputlastvaluedecode + 1 /\ (ge_balance_positive_append_outputlastvalue) = 0) /\ (ge_balance_negative_append_outputlastvalue) = S ge_signed_half_append_outputlastvaluedecode))) /\ ((dst_positive_append_outputlast) + ge_balance_negative_append_outputlastvalue = (dst_negative_append_outputlast) + ge_balance_positive_append_outputlastvalue)))))))))))))

arithmetic_signed_table_singleton · checked inherited prerequisite

Exact statement in the checked dependency cone

forall z. exists F. (exists dst_positive_code_singleton_valid dst_positive_scale_singleton_valid dst_negative_code_singleton_valid dst_negative_scale_singleton_valid. (((F) = (((((dst_positive_code_singleton_valid) + (dst_positive_scale_singleton_valid)) * S ((dst_positive_code_singleton_valid) + (dst_positive_scale_singleton_valid)) + ((dst_positive_scale_singleton_valid) + (dst_positive_scale_singleton_valid))) + (((dst_negative_code_singleton_valid) + (dst_negative_scale_singleton_valid)) * S ((dst_negative_code_singleton_valid) + (dst_negative_scale_singleton_valid)) + ((dst_negative_scale_singleton_valid) + (dst_negative_scale_singleton_valid)))) * S ((((dst_positive_code_singleton_valid) + (dst_positive_scale_singleton_valid)) * S ((dst_positive_code_singleton_valid) + (dst_positive_scale_singleton_valid)) + ((dst_positive_scale_singleton_valid) + (dst_positive_scale_singleton_valid))) + (((dst_negative_code_singleton_valid) + (dst_negative_scale_singleton_valid)) * S ((dst_negative_code_singleton_valid) + (dst_negative_scale_singleton_valid)) + ((dst_negative_scale_singleton_valid) + (dst_negative_scale_singleton_valid)))) + ((((dst_negative_code_singleton_valid) + (dst_negative_scale_singleton_valid)) * S ((dst_negative_code_singleton_valid) + (dst_negative_scale_singleton_valid)) + ((dst_negative_scale_singleton_valid) + (dst_negative_scale_singleton_valid))) + (((dst_negative_code_singleton_valid) + (dst_negative_scale_singleton_valid)) * S ((dst_negative_code_singleton_valid) + (dst_negative_scale_singleton_valid)) + ((dst_negative_scale_singleton_valid) + (dst_negative_scale_singleton_valid)))))) /\ (forall dst_index_singleton_valid. (exists pvs_le_gap_singleton_validdomain. pvs_le_gap_singleton_validdomain + (dst_index_singleton_valid) = (0)) -> exists dst_positive_singleton_valid dst_negative_singleton_valid dst_value_singleton_valid. ((((exists ff_h_pvs_singleton_validentrypositive. ff_h_pvs_singleton_validentrypositive + S (dst_positive_singleton_valid) = S ((S (dst_index_singleton_valid)) * dst_positive_scale_singleton_valid)) /\ exists ff_q_pvs_singleton_validentrypositive. dst_positive_code_singleton_valid = ff_q_pvs_singleton_validentrypositive * S ((S (dst_index_singleton_valid)) * dst_positive_scale_singleton_valid) + (dst_positive_singleton_valid))) /\ (((((exists ff_h_pvs_singleton_validentrynegative. ff_h_pvs_singleton_validentrynegative + S (dst_negative_singleton_valid) = S ((S (dst_index_singleton_valid)) * dst_negative_scale_singleton_valid)) /\ exists ff_q_pvs_singleton_validentrynegative. dst_negative_code_singleton_valid = ff_q_pvs_singleton_validentrynegative * S ((S (dst_index_singleton_valid)) * dst_negative_scale_singleton_valid) + (dst_negative_singleton_valid))) /\ (exists ge_balance_positive_singleton_validentryvalue ge_balance_negative_singleton_validentryvalue. (((((dst_value_singleton_valid) = 2 * (ge_balance_positive_singleton_validentryvalue) /\ (ge_balance_negative_singleton_validentryvalue) = 0) \/ exists ge_signed_half_singleton_validentryvaluedecode. (((dst_value_singleton_valid) = 2 * ge_signed_half_singleton_validentryvaluedecode + 1 /\ (ge_balance_positive_singleton_validentryvalue) = 0) /\ (ge_balance_negative_singleton_validentryvalue) = S ge_signed_half_singleton_validentryvaluedecode))) /\ ((dst_positive_singleton_valid) + ge_balance_negative_singleton_validentryvalue = (dst_negative_singleton_valid) + ge_balance_positive_singleton_validentryvalue))))))))) /\ (exists dst_positive_code_singleton_value dst_positive_scale_singleton_value dst_negative_code_singleton_value dst_negative_scale_singleton_value dst_positive_singleton_value dst_negative_singleton_value. (((F) = (((((dst_positive_code_singleton_value) + (dst_positive_scale_singleton_value)) * S ((dst_positive_code_singleton_value) + (dst_positive_scale_singleton_value)) + ((dst_positive_scale_singleton_value) + (dst_positive_scale_singleton_value))) + (((dst_negative_code_singleton_value) + (dst_negative_scale_singleton_value)) * S ((dst_negative_code_singleton_value) + (dst_negative_scale_singleton_value)) + ((dst_negative_scale_singleton_value) + (dst_negative_scale_singleton_value)))) * S ((((dst_positive_code_singleton_value) + (dst_positive_scale_singleton_value)) * S ((dst_positive_code_singleton_value) + (dst_positive_scale_singleton_value)) + ((dst_positive_scale_singleton_value) + (dst_positive_scale_singleton_value))) + (((dst_negative_code_singleton_value) + (dst_negative_scale_singleton_value)) * S ((dst_negative_code_singleton_value) + (dst_negative_scale_singleton_value)) + ((dst_negative_scale_singleton_value) + (dst_negative_scale_singleton_value)))) + ((((dst_negative_code_singleton_value) + (dst_negative_scale_singleton_value)) * S ((dst_negative_code_singleton_value) + (dst_negative_scale_singleton_value)) + ((dst_negative_scale_singleton_value) + (dst_negative_scale_singleton_value))) + (((dst_negative_code_singleton_value) + (dst_negative_scale_singleton_value)) * S ((dst_negative_code_singleton_value) + (dst_negative_scale_singleton_value)) + ((dst_negative_scale_singleton_value) + (dst_negative_scale_singleton_value)))))) /\ (((((exists ff_h_pvs_singleton_valuepositive. ff_h_pvs_singleton_valuepositive + S (dst_positive_singleton_value) = S ((S (0)) * dst_positive_scale_singleton_value)) /\ exists ff_q_pvs_singleton_valuepositive. dst_positive_code_singleton_value = ff_q_pvs_singleton_valuepositive * S ((S (0)) * dst_positive_scale_singleton_value) + (dst_positive_singleton_value))) /\ (((((exists ff_h_pvs_singleton_valuenegative. ff_h_pvs_singleton_valuenegative + S (dst_negative_singleton_value) = S ((S (0)) * dst_negative_scale_singleton_value)) /\ exists ff_q_pvs_singleton_valuenegative. dst_negative_code_singleton_value = ff_q_pvs_singleton_valuenegative * S ((S (0)) * dst_negative_scale_singleton_value) + (dst_negative_singleton_value))) /\ (exists ge_balance_positive_singleton_valuevalue ge_balance_negative_singleton_valuevalue. (((((z) = 2 * (ge_balance_positive_singleton_valuevalue) /\ (ge_balance_negative_singleton_valuevalue) = 0) \/ exists ge_signed_half_singleton_valuevaluedecode. (((z) = 2 * ge_signed_half_singleton_valuevaluedecode + 1 /\ (ge_balance_positive_singleton_valuevalue) = 0) /\ (ge_balance_negative_singleton_valuevalue) = S ge_signed_half_singleton_valuevaluedecode))) /\ ((dst_positive_singleton_value) + ge_balance_negative_singleton_valuevalue = (dst_negative_singleton_value) + ge_balance_positive_singleton_valuevalue)))))))))

divisor_complement_bounded · checked inherited prerequisite

Exact statement in the checked dependency cone

forall n d q. ~(n=0) -> (exists pvs_le_gap_bounded_input. pvs_le_gap_bounded_input + (d) = (n)) -> ((((~((d)=0)) /\ ((n)=(d)*(q)))) \/ ((((d)=0 \/ ~(exists pvs_factor_bounded_graphnondivisor. (n) = (d) * pvs_factor_bounded_graphnondivisor)) /\ ((q)=(d))))) -> (exists pvs_le_gap_bounded_result. pvs_le_gap_bounded_result + (q) = (n))

divisor_complement_prefix_lookup · checked inherited prerequisite

Exact statement in the checked dependency cone

forall n b c l i q. (forall dvi_index_lookup_prefix. (exists pvs_gap_lookup_prefixdomain. pvs_gap_lookup_prefixdomain + S (dvi_index_lookup_prefix) = (l)) -> exists dvi_value_lookup_prefix. ((((exists ff_h_pvs_lookup_prefixentry. ff_h_pvs_lookup_prefixentry + S (dvi_value_lookup_prefix) = S ((S (dvi_index_lookup_prefix)) * c)) /\ exists ff_q_pvs_lookup_prefixentry. b = ff_q_pvs_lookup_prefixentry * S ((S (dvi_index_lookup_prefix)) * c) + (dvi_value_lookup_prefix))) /\ ((((~((dvi_index_lookup_prefix)=0)) /\ ((n)=(dvi_index_lookup_prefix)*(dvi_value_lookup_prefix)))) \/ ((((dvi_index_lookup_prefix)=0 \/ ~(exists pvs_factor_lookup_prefixgraphnondivisor. (n) = (dvi_index_lookup_prefix) * pvs_factor_lookup_prefixgraphnondivisor)) /\ ((dvi_value_lookup_prefix)=(dvi_index_lookup_prefix))))))) -> (exists pvs_gap_lookup_index. pvs_gap_lookup_index + S (i) = (l)) -> (((exists ff_h_pvs_lookup_beta. ff_h_pvs_lookup_beta + S (q) = S ((S (i)) * c)) /\ exists ff_q_pvs_lookup_beta. b = ff_q_pvs_lookup_beta * S ((S (i)) * c) + (q))) -> ((((~((i)=0)) /\ ((n)=(i)*(q)))) \/ ((((i)=0 \/ ~(exists pvs_factor_lookup_resultnondivisor. (n) = (i) * pvs_factor_lookup_resultnondivisor)) /\ ((q)=(i)))))

divisor_le_nonzero · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall d n. ~(n = 0) -> (exists q. n = d * q) -> exists k. k + d = n
```

divisor_signed_sum_extensional · checked inherited prerequisite

Exact statement in the checked dependency cone

forall F G l a b. (forall dst_index_sum_ext_entries dst_first_sum_ext_entries dst_second_sum_ext_entries. (exists pvs_gap_sum_ext_entriesbound. pvs_gap_sum_ext_entriesbound + S (dst_index_sum_ext_entries) = (l)) -> (exists dst_positive_code_sum_ext_entriesfirst dst_positive_scale_sum_ext_entriesfirst dst_negative_code_sum_ext_entriesfirst dst_negative_scale_sum_ext_entriesfirst dst_positive_sum_ext_entriesfirst dst_negative_sum_ext_entriesfirst. (((F) = (((((dst_positive_code_sum_ext_entriesfirst) + (dst_positive_scale_sum_ext_entriesfirst)) * S ((dst_positive_code_sum_ext_entriesfirst) + (dst_positive_scale_sum_ext_entriesfirst)) + ((dst_positive_scale_sum_ext_entriesfirst) + (dst_positive_scale_sum_ext_entriesfirst))) + (((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) * S ((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) + ((dst_negative_scale_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)))) * S ((((dst_positive_code_sum_ext_entriesfirst) + (dst_positive_scale_sum_ext_entriesfirst)) * S ((dst_positive_code_sum_ext_entriesfirst) + (dst_positive_scale_sum_ext_entriesfirst)) + ((dst_positive_scale_sum_ext_entriesfirst) + (dst_positive_scale_sum_ext_entriesfirst))) + (((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) * S ((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) + ((dst_negative_scale_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)))) + ((((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) * S ((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) + ((dst_negative_scale_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst))) + (((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) * S ((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) + ((dst_negative_scale_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)))))) /\ (((((exists ff_h_pvs_sum_ext_entriesfirstpositive. ff_h_pvs_sum_ext_entriesfirstpositive + S (dst_positive_sum_ext_entriesfirst) = S ((S (dst_index_sum_ext_entries)) * dst_positive_scale_sum_ext_entriesfirst)) /\ exists ff_q_pvs_sum_ext_entriesfirstpositive. dst_positive_code_sum_ext_entriesfirst = ff_q_pvs_sum_ext_entriesfirstpositive * S ((S (dst_index_sum_ext_entries)) * dst_positive_scale_sum_ext_entriesfirst) + (dst_positive_sum_ext_entriesfirst))) /\ (((((exists ff_h_pvs_sum_ext_entriesfirstnegative. ff_h_pvs_sum_ext_entriesfirstnegative + S (dst_negative_sum_ext_entriesfirst) = S ((S (dst_index_sum_ext_entries)) * dst_negative_scale_sum_ext_entriesfirst)) /\ exists ff_q_pvs_sum_ext_entriesfirstnegative. dst_negative_code_sum_ext_entriesfirst = ff_q_pvs_sum_ext_entriesfirstnegative * S ((S (dst_index_sum_ext_entries)) * dst_negative_scale_sum_ext_entriesfirst) + (dst_negative_sum_ext_entriesfirst))) /\ (exists ge_balance_positive_sum_ext_entriesfirstvalue ge_balance_negative_sum_ext_entriesfirstvalue. (((((dst_first_sum_ext_entries) = 2 * (ge_balance_positive_sum_ext_entriesfirstvalue) /\ (ge_balance_negative_sum_ext_entriesfirstvalue) = 0) \/ exists ge_signed_half_sum_ext_entriesfirstvaluedecode. (((dst_first_sum_ext_entries) = 2 * ge_signed_half_sum_ext_entriesfirstvaluedecode + 1 /\ (ge_balance_positive_sum_ext_entriesfirstvalue) = 0) /\ (ge_balance_negative_sum_ext_entriesfirstvalue) = S ge_signed_half_sum_ext_entriesfirstvaluedecode))) /\ ((dst_positive_sum_ext_entriesfirst) + ge_balance_negative_sum_ext_entriesfirstvalue = (dst_negative_sum_ext_entriesfirst) + ge_balance_positive_sum_ext_entriesfirstvalue))))))))) -> (exists dst_positive_code_sum_ext_entriessecond dst_positive_scale_sum_ext_entriessecond dst_negative_code_sum_ext_entriessecond dst_negative_scale_sum_ext_entriessecond dst_positive_sum_ext_entriessecond dst_negative_sum_ext_entriessecond. (((G) = (((((dst_positive_code_sum_ext_entriessecond) + (dst_positive_scale_sum_ext_entriessecond)) * S ((dst_positive_code_sum_ext_entriessecond) + (dst_positive_scale_sum_ext_entriessecond)) + ((dst_positive_scale_sum_ext_entriessecond) + (dst_positive_scale_sum_ext_entriessecond))) + (((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) * S ((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) + ((dst_negative_scale_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)))) * S ((((dst_positive_code_sum_ext_entriessecond) + (dst_positive_scale_sum_ext_entriessecond)) * S ((dst_positive_code_sum_ext_entriessecond) + (dst_positive_scale_sum_ext_entriessecond)) + ((dst_positive_scale_sum_ext_entriessecond) + (dst_positive_scale_sum_ext_entriessecond))) + (((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) * S ((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) + ((dst_negative_scale_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)))) + ((((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) * S ((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) + ((dst_negative_scale_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond))) + (((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) * S ((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) + ((dst_negative_scale_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)))))) /\ (((((exists ff_h_pvs_sum_ext_entriessecondpositive. ff_h_pvs_sum_ext_entriessecondpositive + S (dst_positive_sum_ext_entriessecond) = S ((S (dst_index_sum_ext_entries)) * dst_positive_scale_sum_ext_entriessecond)) /\ exists ff_q_pvs_sum_ext_entriessecondpositive. dst_positive_code_sum_ext_entriessecond = ff_q_pvs_sum_ext_entriessecondpositive * S ((S (dst_index_sum_ext_entries)) * dst_positive_scale_sum_ext_entriessecond) + (dst_positive_sum_ext_entriessecond))) /\ (((((exists ff_h_pvs_sum_ext_entriessecondnegative. ff_h_pvs_sum_ext_entriessecondnegative + S (dst_negative_sum_ext_entriessecond) = S ((S (dst_index_sum_ext_entries)) * dst_negative_scale_sum_ext_entriessecond)) /\ exists ff_q_pvs_sum_ext_entriessecondnegative. dst_negative_code_sum_ext_entriessecond = ff_q_pvs_sum_ext_entriessecondnegative * S ((S (dst_index_sum_ext_entries)) * dst_negative_scale_sum_ext_entriessecond) + (dst_negative_sum_ext_entriessecond))) /\ (exists ge_balance_positive_sum_ext_entriessecondvalue ge_balance_negative_sum_ext_entriessecondvalue. (((((dst_second_sum_ext_entries) = 2 * (ge_balance_positive_sum_ext_entriessecondvalue) /\ (ge_balance_negative_sum_ext_entriessecondvalue) = 0) \/ exists ge_signed_half_sum_ext_entriessecondvaluedecode. (((dst_second_sum_ext_entries) = 2 * ge_signed_half_sum_ext_entriessecondvaluedecode + 1 /\ (ge_balance_positive_sum_ext_entriessecondvalue) = 0) /\ (ge_balance_negative_sum_ext_entriessecondvalue) = S ge_signed_half_sum_ext_entriessecondvaluedecode))) /\ ((dst_positive_sum_ext_entriessecond) + ge_balance_negative_sum_ext_entriessecondvalue = (dst_negative_sum_ext_entriessecond) + ge_balance_positive_sum_ext_entriessecondvalue))))))))) -> dst_first_sum_ext_entries = dst_second_sum_ext_entries) -> (exists dst_positive_code_sum_ext_first dst_positive_scale_sum_ext_first dst_negative_code_sum_ext_first dst_negative_scale_sum_ext_first dst_positive_sum_sum_ext_first dst_negative_sum_sum_ext_first. (((F) = (((((dst_positive_code_sum_ext_first) + (dst_positive_scale_sum_ext_first)) * S ((dst_positive_code_sum_ext_first) + (dst_positive_scale_sum_ext_first)) + ((dst_positive_scale_sum_ext_first) + (dst_positive_scale_sum_ext_first))) + (((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) * S ((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) + ((dst_negative_scale_sum_ext_first) + (dst_negative_scale_sum_ext_first)))) * S ((((dst_positive_code_sum_ext_first) + (dst_positive_scale_sum_ext_first)) * S ((dst_positive_code_sum_ext_first) + (dst_positive_scale_sum_ext_first)) + ((dst_positive_scale_sum_ext_first) + (dst_positive_scale_sum_ext_first))) + (((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) * S ((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) + ((dst_negative_scale_sum_ext_first) + (dst_negative_scale_sum_ext_first)))) + ((((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) * S ((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) + ((dst_negative_scale_sum_ext_first) + (dst_negative_scale_sum_ext_first))) + (((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) * S ((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) + ((dst_negative_scale_sum_ext_first) + (dst_negative_scale_sum_ext_first)))))) /\ (((exists fs_u_dst_sum_ext_firstpositive fs_v_dst_sum_ext_firstpositive. ((((exists fs_h_dst_sum_ext_firstpositive_body_start. fs_h_dst_sum_ext_firstpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_ext_firstpositive)) /\ exists fs_q_dst_sum_ext_firstpositive_body_start. fs_u_dst_sum_ext_firstpositive = fs_q_dst_sum_ext_firstpositive_body_start * S ((S (0)) * fs_v_dst_sum_ext_firstpositive) + (0))) /\ ((((exists fs_h_dst_sum_ext_firstpositive_body_terminal. fs_h_dst_sum_ext_firstpositive_body_terminal + S (dst_positive_sum_sum_ext_first) = S ((S (l)) * fs_v_dst_sum_ext_firstpositive)) /\ exists fs_q_dst_sum_ext_firstpositive_body_terminal. fs_u_dst_sum_ext_firstpositive = fs_q_dst_sum_ext_firstpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_ext_firstpositive) + (dst_positive_sum_sum_ext_first))) /\ forall fs_i_dst_sum_ext_firstpositive_body_steps. (exists fs_lt_dst_sum_ext_firstpositive_body_steps_bound. fs_lt_dst_sum_ext_firstpositive_body_steps_bound + S fs_i_dst_sum_ext_firstpositive_body_steps = l) -> exists fs_a_dst_sum_ext_firstpositive_body_steps fs_r_dst_sum_ext_firstpositive_body_steps fs_s_dst_sum_ext_firstpositive_body_steps. ((((exists fs_h_dst_sum_ext_firstpositive_body_steps_summand. fs_h_dst_sum_ext_firstpositive_body_steps_summand + S (fs_a_dst_sum_ext_firstpositive_body_steps) = S ((S (fs_i_dst_sum_ext_firstpositive_body_steps)) * dst_positive_scale_sum_ext_first)) /\ exists fs_q_dst_sum_ext_firstpositive_body_steps_summand. dst_positive_code_sum_ext_first = fs_q_dst_sum_ext_firstpositive_body_steps_summand * S ((S (fs_i_dst_sum_ext_firstpositive_body_steps)) * dst_positive_scale_sum_ext_first) + (fs_a_dst_sum_ext_firstpositive_body_steps))) /\ ((((exists fs_h_dst_sum_ext_firstpositive_body_steps_partial. fs_h_dst_sum_ext_firstpositive_body_steps_partial + S (fs_r_dst_sum_ext_firstpositive_body_steps) = S ((S (fs_i_dst_sum_ext_firstpositive_body_steps)) * fs_v_dst_sum_ext_firstpositive)) /\ exists fs_q_dst_sum_ext_firstpositive_body_steps_partial. fs_u_dst_sum_ext_firstpositive = fs_q_dst_sum_ext_firstpositive_body_steps_partial * S ((S (fs_i_dst_sum_ext_firstpositive_body_steps)) * fs_v_dst_sum_ext_firstpositive) + (fs_r_dst_sum_ext_firstpositive_body_steps))) /\ ((((exists fs_h_dst_sum_ext_firstpositive_body_steps_successor. fs_h_dst_sum_ext_firstpositive_body_steps_successor + S (fs_s_dst_sum_ext_firstpositive_body_steps) = S ((S (S fs_i_dst_sum_ext_firstpositive_body_steps)) * fs_v_dst_sum_ext_firstpositive)) /\ exists fs_q_dst_sum_ext_firstpositive_body_steps_successor. fs_u_dst_sum_ext_firstpositive = fs_q_dst_sum_ext_firstpositive_body_steps_successor * S ((S (S fs_i_dst_sum_ext_firstpositive_body_steps)) * fs_v_dst_sum_ext_firstpositive) + (fs_s_dst_sum_ext_firstpositive_body_steps))) /\ fs_s_dst_sum_ext_firstpositive_body_steps = fs_r_dst_sum_ext_firstpositive_body_steps + fs_a_dst_sum_ext_firstpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_ext_firstnegative fs_v_dst_sum_ext_firstnegative. ((((exists fs_h_dst_sum_ext_firstnegative_body_start. fs_h_dst_sum_ext_firstnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_ext_firstnegative)) /\ exists fs_q_dst_sum_ext_firstnegative_body_start. fs_u_dst_sum_ext_firstnegative = fs_q_dst_sum_ext_firstnegative_body_start * S ((S (0)) * fs_v_dst_sum_ext_firstnegative) + (0))) /\ ((((exists fs_h_dst_sum_ext_firstnegative_body_terminal. fs_h_dst_sum_ext_firstnegative_body_terminal + S (dst_negative_sum_sum_ext_first) = S ((S (l)) * fs_v_dst_sum_ext_firstnegative)) /\ exists fs_q_dst_sum_ext_firstnegative_body_terminal. fs_u_dst_sum_ext_firstnegative = fs_q_dst_sum_ext_firstnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_ext_firstnegative) + (dst_negative_sum_sum_ext_first))) /\ forall fs_i_dst_sum_ext_firstnegative_body_steps. (exists fs_lt_dst_sum_ext_firstnegative_body_steps_bound. fs_lt_dst_sum_ext_firstnegative_body_steps_bound + S fs_i_dst_sum_ext_firstnegative_body_steps = l) -> exists fs_a_dst_sum_ext_firstnegative_body_steps fs_r_dst_sum_ext_firstnegative_body_steps fs_s_dst_sum_ext_firstnegative_body_steps. ((((exists fs_h_dst_sum_ext_firstnegative_body_steps_summand. fs_h_dst_sum_ext_firstnegative_body_steps_summand + S (fs_a_dst_sum_ext_firstnegative_body_steps) = S ((S (fs_i_dst_sum_ext_firstnegative_body_steps)) * dst_negative_scale_sum_ext_first)) /\ exists fs_q_dst_sum_ext_firstnegative_body_steps_summand. dst_negative_code_sum_ext_first = fs_q_dst_sum_ext_firstnegative_body_steps_summand * S ((S (fs_i_dst_sum_ext_firstnegative_body_steps)) * dst_negative_scale_sum_ext_first) + (fs_a_dst_sum_ext_firstnegative_body_steps))) /\ ((((exists fs_h_dst_sum_ext_firstnegative_body_steps_partial. fs_h_dst_sum_ext_firstnegative_body_steps_partial + S (fs_r_dst_sum_ext_firstnegative_body_steps) = S ((S (fs_i_dst_sum_ext_firstnegative_body_steps)) * fs_v_dst_sum_ext_firstnegative)) /\ exists fs_q_dst_sum_ext_firstnegative_body_steps_partial. fs_u_dst_sum_ext_firstnegative = fs_q_dst_sum_ext_firstnegative_body_steps_partial * S ((S (fs_i_dst_sum_ext_firstnegative_body_steps)) * fs_v_dst_sum_ext_firstnegative) + (fs_r_dst_sum_ext_firstnegative_body_steps))) /\ ((((exists fs_h_dst_sum_ext_firstnegative_body_steps_successor. fs_h_dst_sum_ext_firstnegative_body_steps_successor + S (fs_s_dst_sum_ext_firstnegative_body_steps) = S ((S (S fs_i_dst_sum_ext_firstnegative_body_steps)) * fs_v_dst_sum_ext_firstnegative)) /\ exists fs_q_dst_sum_ext_firstnegative_body_steps_successor. fs_u_dst_sum_ext_firstnegative = fs_q_dst_sum_ext_firstnegative_body_steps_successor * S ((S (S fs_i_dst_sum_ext_firstnegative_body_steps)) * fs_v_dst_sum_ext_firstnegative) + (fs_s_dst_sum_ext_firstnegative_body_steps))) /\ fs_s_dst_sum_ext_firstnegative_body_steps = fs_r_dst_sum_ext_firstnegative_body_steps + fs_a_dst_sum_ext_firstnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_ext_firstresult ge_balance_negative_sum_ext_firstresult. (((((a) = 2 * (ge_balance_positive_sum_ext_firstresult) /\ (ge_balance_negative_sum_ext_firstresult) = 0) \/ exists ge_signed_half_sum_ext_firstresultdecode. (((a) = 2 * ge_signed_half_sum_ext_firstresultdecode + 1 /\ (ge_balance_positive_sum_ext_firstresult) = 0) /\ (ge_balance_negative_sum_ext_firstresult) = S ge_signed_half_sum_ext_firstresultdecode))) /\ ((dst_positive_sum_sum_ext_first) + ge_balance_negative_sum_ext_firstresult = (dst_negative_sum_sum_ext_first) + ge_balance_positive_sum_ext_firstresult))))))))) -> (exists dst_positive_code_sum_ext_second dst_positive_scale_sum_ext_second dst_negative_code_sum_ext_second dst_negative_scale_sum_ext_second dst_positive_sum_sum_ext_second dst_negative_sum_sum_ext_second. (((G) = (((((dst_positive_code_sum_ext_second) + (dst_positive_scale_sum_ext_second)) * S ((dst_positive_code_sum_ext_second) + (dst_positive_scale_sum_ext_second)) + ((dst_positive_scale_sum_ext_second) + (dst_positive_scale_sum_ext_second))) + (((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) * S ((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) + ((dst_negative_scale_sum_ext_second) + (dst_negative_scale_sum_ext_second)))) * S ((((dst_positive_code_sum_ext_second) + (dst_positive_scale_sum_ext_second)) * S ((dst_positive_code_sum_ext_second) + (dst_positive_scale_sum_ext_second)) + ((dst_positive_scale_sum_ext_second) + (dst_positive_scale_sum_ext_second))) + (((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) * S ((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) + ((dst_negative_scale_sum_ext_second) + (dst_negative_scale_sum_ext_second)))) + ((((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) * S ((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) + ((dst_negative_scale_sum_ext_second) + (dst_negative_scale_sum_ext_second))) + (((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) * S ((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) + ((dst_negative_scale_sum_ext_second) + (dst_negative_scale_sum_ext_second)))))) /\ (((exists fs_u_dst_sum_ext_secondpositive fs_v_dst_sum_ext_secondpositive. ((((exists fs_h_dst_sum_ext_secondpositive_body_start. fs_h_dst_sum_ext_secondpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_ext_secondpositive)) /\ exists fs_q_dst_sum_ext_secondpositive_body_start. fs_u_dst_sum_ext_secondpositive = fs_q_dst_sum_ext_secondpositive_body_start * S ((S (0)) * fs_v_dst_sum_ext_secondpositive) + (0))) /\ ((((exists fs_h_dst_sum_ext_secondpositive_body_terminal. fs_h_dst_sum_ext_secondpositive_body_terminal + S (dst_positive_sum_sum_ext_second) = S ((S (l)) * fs_v_dst_sum_ext_secondpositive)) /\ exists fs_q_dst_sum_ext_secondpositive_body_terminal. fs_u_dst_sum_ext_secondpositive = fs_q_dst_sum_ext_secondpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_ext_secondpositive) + (dst_positive_sum_sum_ext_second))) /\ forall fs_i_dst_sum_ext_secondpositive_body_steps. (exists fs_lt_dst_sum_ext_secondpositive_body_steps_bound. fs_lt_dst_sum_ext_secondpositive_body_steps_bound + S fs_i_dst_sum_ext_secondpositive_body_steps = l) -> exists fs_a_dst_sum_ext_secondpositive_body_steps fs_r_dst_sum_ext_secondpositive_body_steps fs_s_dst_sum_ext_secondpositive_body_steps. ((((exists fs_h_dst_sum_ext_secondpositive_body_steps_summand. fs_h_dst_sum_ext_secondpositive_body_steps_summand + S (fs_a_dst_sum_ext_secondpositive_body_steps) = S ((S (fs_i_dst_sum_ext_secondpositive_body_steps)) * dst_positive_scale_sum_ext_second)) /\ exists fs_q_dst_sum_ext_secondpositive_body_steps_summand. dst_positive_code_sum_ext_second = fs_q_dst_sum_ext_secondpositive_body_steps_summand * S ((S (fs_i_dst_sum_ext_secondpositive_body_steps)) * dst_positive_scale_sum_ext_second) + (fs_a_dst_sum_ext_secondpositive_body_steps))) /\ ((((exists fs_h_dst_sum_ext_secondpositive_body_steps_partial. fs_h_dst_sum_ext_secondpositive_body_steps_partial + S (fs_r_dst_sum_ext_secondpositive_body_steps) = S ((S (fs_i_dst_sum_ext_secondpositive_body_steps)) * fs_v_dst_sum_ext_secondpositive)) /\ exists fs_q_dst_sum_ext_secondpositive_body_steps_partial. fs_u_dst_sum_ext_secondpositive = fs_q_dst_sum_ext_secondpositive_body_steps_partial * S ((S (fs_i_dst_sum_ext_secondpositive_body_steps)) * fs_v_dst_sum_ext_secondpositive) + (fs_r_dst_sum_ext_secondpositive_body_steps))) /\ ((((exists fs_h_dst_sum_ext_secondpositive_body_steps_successor. fs_h_dst_sum_ext_secondpositive_body_steps_successor + S (fs_s_dst_sum_ext_secondpositive_body_steps) = S ((S (S fs_i_dst_sum_ext_secondpositive_body_steps)) * fs_v_dst_sum_ext_secondpositive)) /\ exists fs_q_dst_sum_ext_secondpositive_body_steps_successor. fs_u_dst_sum_ext_secondpositive = fs_q_dst_sum_ext_secondpositive_body_steps_successor * S ((S (S fs_i_dst_sum_ext_secondpositive_body_steps)) * fs_v_dst_sum_ext_secondpositive) + (fs_s_dst_sum_ext_secondpositive_body_steps))) /\ fs_s_dst_sum_ext_secondpositive_body_steps = fs_r_dst_sum_ext_secondpositive_body_steps + fs_a_dst_sum_ext_secondpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_ext_secondnegative fs_v_dst_sum_ext_secondnegative. ((((exists fs_h_dst_sum_ext_secondnegative_body_start. fs_h_dst_sum_ext_secondnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_ext_secondnegative)) /\ exists fs_q_dst_sum_ext_secondnegative_body_start. fs_u_dst_sum_ext_secondnegative = fs_q_dst_sum_ext_secondnegative_body_start * S ((S (0)) * fs_v_dst_sum_ext_secondnegative) + (0))) /\ ((((exists fs_h_dst_sum_ext_secondnegative_body_terminal. fs_h_dst_sum_ext_secondnegative_body_terminal + S (dst_negative_sum_sum_ext_second) = S ((S (l)) * fs_v_dst_sum_ext_secondnegative)) /\ exists fs_q_dst_sum_ext_secondnegative_body_terminal. fs_u_dst_sum_ext_secondnegative = fs_q_dst_sum_ext_secondnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_ext_secondnegative) + (dst_negative_sum_sum_ext_second))) /\ forall fs_i_dst_sum_ext_secondnegative_body_steps. (exists fs_lt_dst_sum_ext_secondnegative_body_steps_bound. fs_lt_dst_sum_ext_secondnegative_body_steps_bound + S fs_i_dst_sum_ext_secondnegative_body_steps = l) -> exists fs_a_dst_sum_ext_secondnegative_body_steps fs_r_dst_sum_ext_secondnegative_body_steps fs_s_dst_sum_ext_secondnegative_body_steps. ((((exists fs_h_dst_sum_ext_secondnegative_body_steps_summand. fs_h_dst_sum_ext_secondnegative_body_steps_summand + S (fs_a_dst_sum_ext_secondnegative_body_steps) = S ((S (fs_i_dst_sum_ext_secondnegative_body_steps)) * dst_negative_scale_sum_ext_second)) /\ exists fs_q_dst_sum_ext_secondnegative_body_steps_summand. dst_negative_code_sum_ext_second = fs_q_dst_sum_ext_secondnegative_body_steps_summand * S ((S (fs_i_dst_sum_ext_secondnegative_body_steps)) * dst_negative_scale_sum_ext_second) + (fs_a_dst_sum_ext_secondnegative_body_steps))) /\ ((((exists fs_h_dst_sum_ext_secondnegative_body_steps_partial. fs_h_dst_sum_ext_secondnegative_body_steps_partial + S (fs_r_dst_sum_ext_secondnegative_body_steps) = S ((S (fs_i_dst_sum_ext_secondnegative_body_steps)) * fs_v_dst_sum_ext_secondnegative)) /\ exists fs_q_dst_sum_ext_secondnegative_body_steps_partial. fs_u_dst_sum_ext_secondnegative = fs_q_dst_sum_ext_secondnegative_body_steps_partial * S ((S (fs_i_dst_sum_ext_secondnegative_body_steps)) * fs_v_dst_sum_ext_secondnegative) + (fs_r_dst_sum_ext_secondnegative_body_steps))) /\ ((((exists fs_h_dst_sum_ext_secondnegative_body_steps_successor. fs_h_dst_sum_ext_secondnegative_body_steps_successor + S (fs_s_dst_sum_ext_secondnegative_body_steps) = S ((S (S fs_i_dst_sum_ext_secondnegative_body_steps)) * fs_v_dst_sum_ext_secondnegative)) /\ exists fs_q_dst_sum_ext_secondnegative_body_steps_successor. fs_u_dst_sum_ext_secondnegative = fs_q_dst_sum_ext_secondnegative_body_steps_successor * S ((S (S fs_i_dst_sum_ext_secondnegative_body_steps)) * fs_v_dst_sum_ext_secondnegative) + (fs_s_dst_sum_ext_secondnegative_body_steps))) /\ fs_s_dst_sum_ext_secondnegative_body_steps = fs_r_dst_sum_ext_secondnegative_body_steps + fs_a_dst_sum_ext_secondnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_ext_secondresult ge_balance_negative_sum_ext_secondresult. (((((b) = 2 * (ge_balance_positive_sum_ext_secondresult) /\ (ge_balance_negative_sum_ext_secondresult) = 0) \/ exists ge_signed_half_sum_ext_secondresultdecode. (((b) = 2 * ge_signed_half_sum_ext_secondresultdecode + 1 /\ (ge_balance_positive_sum_ext_secondresult) = 0) /\ (ge_balance_negative_sum_ext_secondresult) = S ge_signed_half_sum_ext_secondresultdecode))) /\ ((dst_positive_sum_sum_ext_second) + ge_balance_negative_sum_ext_secondresult = (dst_negative_sum_sum_ext_second) + ge_balance_positive_sum_ext_secondresult))))))))) -> a = b

divisor_signed_sum_permutation_invariant · checked inherited prerequisite

Exact statement in the checked dependency cone

forall F G r s l u v. (forall pfp_i_permutation_bound. (exists pfp_gap_permutation_boundindex. pfp_gap_permutation_boundindex + S (pfp_i_permutation_bound) = (l)) -> exists pfp_a_permutation_bound. (((exists ff_h_pfp_permutation_boundentry. ff_h_pfp_permutation_boundentry + S (pfp_a_permutation_bound) = S ((S (pfp_i_permutation_bound)) * s)) /\ exists ff_q_pfp_permutation_boundentry. r = ff_q_pfp_permutation_boundentry * S ((S (pfp_i_permutation_bound)) * s) + (pfp_a_permutation_bound))) /\ (exists pfp_gap_permutation_boundvalue. pfp_gap_permutation_boundvalue + S (pfp_a_permutation_bound) = (l))) -> (forall pfp_i_permutation_injective pfp_j_permutation_injective pfp_a_permutation_injective. (exists pfp_gap_permutation_injectivefirst. pfp_gap_permutation_injectivefirst + S (pfp_i_permutation_injective) = (l)) -> (exists pfp_gap_permutation_injectivesecond. pfp_gap_permutation_injectivesecond + S (pfp_j_permutation_injective) = (l)) -> (((exists ff_h_pfp_permutation_injectiveleft. ff_h_pfp_permutation_injectiveleft + S (pfp_a_permutation_injective) = S ((S (pfp_i_permutation_injective)) * s)) /\ exists ff_q_pfp_permutation_injectiveleft. r = ff_q_pfp_permutation_injectiveleft * S ((S (pfp_i_permutation_injective)) * s) + (pfp_a_permutation_injective))) -> (((exists ff_h_pfp_permutation_injectiveright. ff_h_pfp_permutation_injectiveright + S (pfp_a_permutation_injective) = S ((S (pfp_j_permutation_injective)) * s)) /\ exists ff_q_pfp_permutation_injectiveright. r = ff_q_pfp_permutation_injectiveright * S ((S (pfp_j_permutation_injective)) * s) + (pfp_a_permutation_injective))) -> pfp_i_permutation_injective = pfp_j_permutation_injective) -> (forall dsr_index_permutation_pullback dsr_image_permutation_pullback dsr_value_permutation_pullback. (exists pvs_gap_permutation_pullbackbound. pvs_gap_permutation_pullbackbound + S (dsr_index_permutation_pullback) = (l)) -> (((exists ff_h_pvs_permutation_pullbackmap. ff_h_pvs_permutation_pullbackmap + S (dsr_image_permutation_pullback) = S ((S (dsr_index_permutation_pullback)) * s)) /\ exists ff_q_pvs_permutation_pullbackmap. r = ff_q_pvs_permutation_pullbackmap * S ((S (dsr_index_permutation_pullback)) * s) + (dsr_image_permutation_pullback))) -> (exists dst_positive_code_permutation_pullbacksource dst_positive_scale_permutation_pullbacksource dst_negative_code_permutation_pullbacksource dst_negative_scale_permutation_pullbacksource dst_positive_permutation_pullbacksource dst_negative_permutation_pullbacksource. (((F) = (((((dst_positive_code_permutation_pullbacksource) + (dst_positive_scale_permutation_pullbacksource)) * S ((dst_positive_code_permutation_pullbacksource) + (dst_positive_scale_permutation_pullbacksource)) + ((dst_positive_scale_permutation_pullbacksource) + (dst_positive_scale_permutation_pullbacksource))) + (((dst_negative_code_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)) * S ((dst_negative_code_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)) + ((dst_negative_scale_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)))) * S ((((dst_positive_code_permutation_pullbacksource) + (dst_positive_scale_permutation_pullbacksource)) * S ((dst_positive_code_permutation_pullbacksource) + (dst_positive_scale_permutation_pullbacksource)) + ((dst_positive_scale_permutation_pullbacksource) + (dst_positive_scale_permutation_pullbacksource))) + (((dst_negative_code_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)) * S ((dst_negative_code_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)) + ((dst_negative_scale_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)))) + ((((dst_negative_code_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)) * S ((dst_negative_code_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)) + ((dst_negative_scale_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource))) + (((dst_negative_code_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)) * S ((dst_negative_code_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)) + ((dst_negative_scale_permutation_pullbacksource) + (dst_negative_scale_permutation_pullbacksource)))))) /\ (((((exists ff_h_pvs_permutation_pullbacksourcepositive. ff_h_pvs_permutation_pullbacksourcepositive + S (dst_positive_permutation_pullbacksource) = S ((S (dsr_image_permutation_pullback)) * dst_positive_scale_permutation_pullbacksource)) /\ exists ff_q_pvs_permutation_pullbacksourcepositive. dst_positive_code_permutation_pullbacksource = ff_q_pvs_permutation_pullbacksourcepositive * S ((S (dsr_image_permutation_pullback)) * dst_positive_scale_permutation_pullbacksource) + (dst_positive_permutation_pullbacksource))) /\ (((((exists ff_h_pvs_permutation_pullbacksourcenegative. ff_h_pvs_permutation_pullbacksourcenegative + S (dst_negative_permutation_pullbacksource) = S ((S (dsr_image_permutation_pullback)) * dst_negative_scale_permutation_pullbacksource)) /\ exists ff_q_pvs_permutation_pullbacksourcenegative. dst_negative_code_permutation_pullbacksource = ff_q_pvs_permutation_pullbacksourcenegative * S ((S (dsr_image_permutation_pullback)) * dst_negative_scale_permutation_pullbacksource) + (dst_negative_permutation_pullbacksource))) /\ (exists ge_balance_positive_permutation_pullbacksourcevalue ge_balance_negative_permutation_pullbacksourcevalue. (((((dsr_value_permutation_pullback) = 2 * (ge_balance_positive_permutation_pullbacksourcevalue) /\ (ge_balance_negative_permutation_pullbacksourcevalue) = 0) \/ exists ge_signed_half_permutation_pullbacksourcevaluedecode. (((dsr_value_permutation_pullback) = 2 * ge_signed_half_permutation_pullbacksourcevaluedecode + 1 /\ (ge_balance_positive_permutation_pullbacksourcevalue) = 0) /\ (ge_balance_negative_permutation_pullbacksourcevalue) = S ge_signed_half_permutation_pullbacksourcevaluedecode))) /\ ((dst_positive_permutation_pullbacksource) + ge_balance_negative_permutation_pullbacksourcevalue = (dst_negative_permutation_pullbacksource) + ge_balance_positive_permutation_pullbacksourcevalue))))))))) -> (exists dst_positive_code_permutation_pullbacktarget dst_positive_scale_permutation_pullbacktarget dst_negative_code_permutation_pullbacktarget dst_negative_scale_permutation_pullbacktarget dst_positive_permutation_pullbacktarget dst_negative_permutation_pullbacktarget. (((G) = (((((dst_positive_code_permutation_pullbacktarget) + (dst_positive_scale_permutation_pullbacktarget)) * S ((dst_positive_code_permutation_pullbacktarget) + (dst_positive_scale_permutation_pullbacktarget)) + ((dst_positive_scale_permutation_pullbacktarget) + (dst_positive_scale_permutation_pullbacktarget))) + (((dst_negative_code_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)) * S ((dst_negative_code_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)) + ((dst_negative_scale_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)))) * S ((((dst_positive_code_permutation_pullbacktarget) + (dst_positive_scale_permutation_pullbacktarget)) * S ((dst_positive_code_permutation_pullbacktarget) + (dst_positive_scale_permutation_pullbacktarget)) + ((dst_positive_scale_permutation_pullbacktarget) + (dst_positive_scale_permutation_pullbacktarget))) + (((dst_negative_code_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)) * S ((dst_negative_code_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)) + ((dst_negative_scale_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)))) + ((((dst_negative_code_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)) * S ((dst_negative_code_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)) + ((dst_negative_scale_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget))) + (((dst_negative_code_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)) * S ((dst_negative_code_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)) + ((dst_negative_scale_permutation_pullbacktarget) + (dst_negative_scale_permutation_pullbacktarget)))))) /\ (((((exists ff_h_pvs_permutation_pullbacktargetpositive. ff_h_pvs_permutation_pullbacktargetpositive + S (dst_positive_permutation_pullbacktarget) = S ((S (dsr_index_permutation_pullback)) * dst_positive_scale_permutation_pullbacktarget)) /\ exists ff_q_pvs_permutation_pullbacktargetpositive. dst_positive_code_permutation_pullbacktarget = ff_q_pvs_permutation_pullbacktargetpositive * S ((S (dsr_index_permutation_pullback)) * dst_positive_scale_permutation_pullbacktarget) + (dst_positive_permutation_pullbacktarget))) /\ (((((exists ff_h_pvs_permutation_pullbacktargetnegative. ff_h_pvs_permutation_pullbacktargetnegative + S (dst_negative_permutation_pullbacktarget) = S ((S (dsr_index_permutation_pullback)) * dst_negative_scale_permutation_pullbacktarget)) /\ exists ff_q_pvs_permutation_pullbacktargetnegative. dst_negative_code_permutation_pullbacktarget = ff_q_pvs_permutation_pullbacktargetnegative * S ((S (dsr_index_permutation_pullback)) * dst_negative_scale_permutation_pullbacktarget) + (dst_negative_permutation_pullbacktarget))) /\ (exists ge_balance_positive_permutation_pullbacktargetvalue ge_balance_negative_permutation_pullbacktargetvalue. (((((dsr_value_permutation_pullback) = 2 * (ge_balance_positive_permutation_pullbacktargetvalue) /\ (ge_balance_negative_permutation_pullbacktargetvalue) = 0) \/ exists ge_signed_half_permutation_pullbacktargetvaluedecode. (((dsr_value_permutation_pullback) = 2 * ge_signed_half_permutation_pullbacktargetvaluedecode + 1 /\ (ge_balance_positive_permutation_pullbacktargetvalue) = 0) /\ (ge_balance_negative_permutation_pullbacktargetvalue) = S ge_signed_half_permutation_pullbacktargetvaluedecode))) /\ ((dst_positive_permutation_pullbacktarget) + ge_balance_negative_permutation_pullbacktargetvalue = (dst_negative_permutation_pullbacktarget) + ge_balance_positive_permutation_pullbacktargetvalue)))))))))) -> (exists dst_positive_code_permutation_source dst_positive_scale_permutation_source dst_negative_code_permutation_source dst_negative_scale_permutation_source dst_positive_sum_permutation_source dst_negative_sum_permutation_source. (((F) = (((((dst_positive_code_permutation_source) + (dst_positive_scale_permutation_source)) * S ((dst_positive_code_permutation_source) + (dst_positive_scale_permutation_source)) + ((dst_positive_scale_permutation_source) + (dst_positive_scale_permutation_source))) + (((dst_negative_code_permutation_source) + (dst_negative_scale_permutation_source)) * S ((dst_negative_code_permutation_source) + (dst_negative_scale_permutation_source)) + ((dst_negative_scale_permutation_source) + (dst_negative_scale_permutation_source)))) * S ((((dst_positive_code_permutation_source) + (dst_positive_scale_permutation_source)) * S ((dst_positive_code_permutation_source) + (dst_positive_scale_permutation_source)) + ((dst_positive_scale_permutation_source) + (dst_positive_scale_permutation_source))) + (((dst_negative_code_permutation_source) + (dst_negative_scale_permutation_source)) * S ((dst_negative_code_permutation_source) + (dst_negative_scale_permutation_source)) + ((dst_negative_scale_permutation_source) + (dst_negative_scale_permutation_source)))) + ((((dst_negative_code_permutation_source) + (dst_negative_scale_permutation_source)) * S ((dst_negative_code_permutation_source) + (dst_negative_scale_permutation_source)) + ((dst_negative_scale_permutation_source) + (dst_negative_scale_permutation_source))) + (((dst_negative_code_permutation_source) + (dst_negative_scale_permutation_source)) * S ((dst_negative_code_permutation_source) + (dst_negative_scale_permutation_source)) + ((dst_negative_scale_permutation_source) + (dst_negative_scale_permutation_source)))))) /\ (((exists fs_u_dst_permutation_sourcepositive fs_v_dst_permutation_sourcepositive. ((((exists fs_h_dst_permutation_sourcepositive_body_start. fs_h_dst_permutation_sourcepositive_body_start + S (0) = S ((S (0)) * fs_v_dst_permutation_sourcepositive)) /\ exists fs_q_dst_permutation_sourcepositive_body_start. fs_u_dst_permutation_sourcepositive = fs_q_dst_permutation_sourcepositive_body_start * S ((S (0)) * fs_v_dst_permutation_sourcepositive) + (0))) /\ ((((exists fs_h_dst_permutation_sourcepositive_body_terminal. fs_h_dst_permutation_sourcepositive_body_terminal + S (dst_positive_sum_permutation_source) = S ((S (l)) * fs_v_dst_permutation_sourcepositive)) /\ exists fs_q_dst_permutation_sourcepositive_body_terminal. fs_u_dst_permutation_sourcepositive = fs_q_dst_permutation_sourcepositive_body_terminal * S ((S (l)) * fs_v_dst_permutation_sourcepositive) + (dst_positive_sum_permutation_source))) /\ forall fs_i_dst_permutation_sourcepositive_body_steps. (exists fs_lt_dst_permutation_sourcepositive_body_steps_bound. fs_lt_dst_permutation_sourcepositive_body_steps_bound + S fs_i_dst_permutation_sourcepositive_body_steps = l) -> exists fs_a_dst_permutation_sourcepositive_body_steps fs_r_dst_permutation_sourcepositive_body_steps fs_s_dst_permutation_sourcepositive_body_steps. ((((exists fs_h_dst_permutation_sourcepositive_body_steps_summand. fs_h_dst_permutation_sourcepositive_body_steps_summand + S (fs_a_dst_permutation_sourcepositive_body_steps) = S ((S (fs_i_dst_permutation_sourcepositive_body_steps)) * dst_positive_scale_permutation_source)) /\ exists fs_q_dst_permutation_sourcepositive_body_steps_summand. dst_positive_code_permutation_source = fs_q_dst_permutation_sourcepositive_body_steps_summand * S ((S (fs_i_dst_permutation_sourcepositive_body_steps)) * dst_positive_scale_permutation_source) + (fs_a_dst_permutation_sourcepositive_body_steps))) /\ ((((exists fs_h_dst_permutation_sourcepositive_body_steps_partial. fs_h_dst_permutation_sourcepositive_body_steps_partial + S (fs_r_dst_permutation_sourcepositive_body_steps) = S ((S (fs_i_dst_permutation_sourcepositive_body_steps)) * fs_v_dst_permutation_sourcepositive)) /\ exists fs_q_dst_permutation_sourcepositive_body_steps_partial. fs_u_dst_permutation_sourcepositive = fs_q_dst_permutation_sourcepositive_body_steps_partial * S ((S (fs_i_dst_permutation_sourcepositive_body_steps)) * fs_v_dst_permutation_sourcepositive) + (fs_r_dst_permutation_sourcepositive_body_steps))) /\ ((((exists fs_h_dst_permutation_sourcepositive_body_steps_successor. fs_h_dst_permutation_sourcepositive_body_steps_successor + S (fs_s_dst_permutation_sourcepositive_body_steps) = S ((S (S fs_i_dst_permutation_sourcepositive_body_steps)) * fs_v_dst_permutation_sourcepositive)) /\ exists fs_q_dst_permutation_sourcepositive_body_steps_successor. fs_u_dst_permutation_sourcepositive = fs_q_dst_permutation_sourcepositive_body_steps_successor * S ((S (S fs_i_dst_permutation_sourcepositive_body_steps)) * fs_v_dst_permutation_sourcepositive) + (fs_s_dst_permutation_sourcepositive_body_steps))) /\ fs_s_dst_permutation_sourcepositive_body_steps = fs_r_dst_permutation_sourcepositive_body_steps + fs_a_dst_permutation_sourcepositive_body_steps)))))) /\ (((exists fs_u_dst_permutation_sourcenegative fs_v_dst_permutation_sourcenegative. ((((exists fs_h_dst_permutation_sourcenegative_body_start. fs_h_dst_permutation_sourcenegative_body_start + S (0) = S ((S (0)) * fs_v_dst_permutation_sourcenegative)) /\ exists fs_q_dst_permutation_sourcenegative_body_start. fs_u_dst_permutation_sourcenegative = fs_q_dst_permutation_sourcenegative_body_start * S ((S (0)) * fs_v_dst_permutation_sourcenegative) + (0))) /\ ((((exists fs_h_dst_permutation_sourcenegative_body_terminal. fs_h_dst_permutation_sourcenegative_body_terminal + S (dst_negative_sum_permutation_source) = S ((S (l)) * fs_v_dst_permutation_sourcenegative)) /\ exists fs_q_dst_permutation_sourcenegative_body_terminal. fs_u_dst_permutation_sourcenegative = fs_q_dst_permutation_sourcenegative_body_terminal * S ((S (l)) * fs_v_dst_permutation_sourcenegative) + (dst_negative_sum_permutation_source))) /\ forall fs_i_dst_permutation_sourcenegative_body_steps. (exists fs_lt_dst_permutation_sourcenegative_body_steps_bound. fs_lt_dst_permutation_sourcenegative_body_steps_bound + S fs_i_dst_permutation_sourcenegative_body_steps = l) -> exists fs_a_dst_permutation_sourcenegative_body_steps fs_r_dst_permutation_sourcenegative_body_steps fs_s_dst_permutation_sourcenegative_body_steps. ((((exists fs_h_dst_permutation_sourcenegative_body_steps_summand. fs_h_dst_permutation_sourcenegative_body_steps_summand + S (fs_a_dst_permutation_sourcenegative_body_steps) = S ((S (fs_i_dst_permutation_sourcenegative_body_steps)) * dst_negative_scale_permutation_source)) /\ exists fs_q_dst_permutation_sourcenegative_body_steps_summand. dst_negative_code_permutation_source = fs_q_dst_permutation_sourcenegative_body_steps_summand * S ((S (fs_i_dst_permutation_sourcenegative_body_steps)) * dst_negative_scale_permutation_source) + (fs_a_dst_permutation_sourcenegative_body_steps))) /\ ((((exists fs_h_dst_permutation_sourcenegative_body_steps_partial. fs_h_dst_permutation_sourcenegative_body_steps_partial + S (fs_r_dst_permutation_sourcenegative_body_steps) = S ((S (fs_i_dst_permutation_sourcenegative_body_steps)) * fs_v_dst_permutation_sourcenegative)) /\ exists fs_q_dst_permutation_sourcenegative_body_steps_partial. fs_u_dst_permutation_sourcenegative = fs_q_dst_permutation_sourcenegative_body_steps_partial * S ((S (fs_i_dst_permutation_sourcenegative_body_steps)) * fs_v_dst_permutation_sourcenegative) + (fs_r_dst_permutation_sourcenegative_body_steps))) /\ ((((exists fs_h_dst_permutation_sourcenegative_body_steps_successor. fs_h_dst_permutation_sourcenegative_body_steps_successor + S (fs_s_dst_permutation_sourcenegative_body_steps) = S ((S (S fs_i_dst_permutation_sourcenegative_body_steps)) * fs_v_dst_permutation_sourcenegative)) /\ exists fs_q_dst_permutation_sourcenegative_body_steps_successor. fs_u_dst_permutation_sourcenegative = fs_q_dst_permutation_sourcenegative_body_steps_successor * S ((S (S fs_i_dst_permutation_sourcenegative_body_steps)) * fs_v_dst_permutation_sourcenegative) + (fs_s_dst_permutation_sourcenegative_body_steps))) /\ fs_s_dst_permutation_sourcenegative_body_steps = fs_r_dst_permutation_sourcenegative_body_steps + fs_a_dst_permutation_sourcenegative_body_steps)))))) /\ (exists ge_balance_positive_permutation_sourceresult ge_balance_negative_permutation_sourceresult. (((((u) = 2 * (ge_balance_positive_permutation_sourceresult) /\ (ge_balance_negative_permutation_sourceresult) = 0) \/ exists ge_signed_half_permutation_sourceresultdecode. (((u) = 2 * ge_signed_half_permutation_sourceresultdecode + 1 /\ (ge_balance_positive_permutation_sourceresult) = 0) /\ (ge_balance_negative_permutation_sourceresult) = S ge_signed_half_permutation_sourceresultdecode))) /\ ((dst_positive_sum_permutation_source) + ge_balance_negative_permutation_sourceresult = (dst_negative_sum_permutation_source) + ge_balance_positive_permutation_sourceresult))))))))) -> (exists dst_positive_code_permutation_target dst_positive_scale_permutation_target dst_negative_code_permutation_target dst_negative_scale_permutation_target dst_positive_sum_permutation_target dst_negative_sum_permutation_target. (((G) = (((((dst_positive_code_permutation_target) + (dst_positive_scale_permutation_target)) * S ((dst_positive_code_permutation_target) + (dst_positive_scale_permutation_target)) + ((dst_positive_scale_permutation_target) + (dst_positive_scale_permutation_target))) + (((dst_negative_code_permutation_target) + (dst_negative_scale_permutation_target)) * S ((dst_negative_code_permutation_target) + (dst_negative_scale_permutation_target)) + ((dst_negative_scale_permutation_target) + (dst_negative_scale_permutation_target)))) * S ((((dst_positive_code_permutation_target) + (dst_positive_scale_permutation_target)) * S ((dst_positive_code_permutation_target) + (dst_positive_scale_permutation_target)) + ((dst_positive_scale_permutation_target) + (dst_positive_scale_permutation_target))) + (((dst_negative_code_permutation_target) + (dst_negative_scale_permutation_target)) * S ((dst_negative_code_permutation_target) + (dst_negative_scale_permutation_target)) + ((dst_negative_scale_permutation_target) + (dst_negative_scale_permutation_target)))) + ((((dst_negative_code_permutation_target) + (dst_negative_scale_permutation_target)) * S ((dst_negative_code_permutation_target) + (dst_negative_scale_permutation_target)) + ((dst_negative_scale_permutation_target) + (dst_negative_scale_permutation_target))) + (((dst_negative_code_permutation_target) + (dst_negative_scale_permutation_target)) * S ((dst_negative_code_permutation_target) + (dst_negative_scale_permutation_target)) + ((dst_negative_scale_permutation_target) + (dst_negative_scale_permutation_target)))))) /\ (((exists fs_u_dst_permutation_targetpositive fs_v_dst_permutation_targetpositive. ((((exists fs_h_dst_permutation_targetpositive_body_start. fs_h_dst_permutation_targetpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_permutation_targetpositive)) /\ exists fs_q_dst_permutation_targetpositive_body_start. fs_u_dst_permutation_targetpositive = fs_q_dst_permutation_targetpositive_body_start * S ((S (0)) * fs_v_dst_permutation_targetpositive) + (0))) /\ ((((exists fs_h_dst_permutation_targetpositive_body_terminal. fs_h_dst_permutation_targetpositive_body_terminal + S (dst_positive_sum_permutation_target) = S ((S (l)) * fs_v_dst_permutation_targetpositive)) /\ exists fs_q_dst_permutation_targetpositive_body_terminal. fs_u_dst_permutation_targetpositive = fs_q_dst_permutation_targetpositive_body_terminal * S ((S (l)) * fs_v_dst_permutation_targetpositive) + (dst_positive_sum_permutation_target))) /\ forall fs_i_dst_permutation_targetpositive_body_steps. (exists fs_lt_dst_permutation_targetpositive_body_steps_bound. fs_lt_dst_permutation_targetpositive_body_steps_bound + S fs_i_dst_permutation_targetpositive_body_steps = l) -> exists fs_a_dst_permutation_targetpositive_body_steps fs_r_dst_permutation_targetpositive_body_steps fs_s_dst_permutation_targetpositive_body_steps. ((((exists fs_h_dst_permutation_targetpositive_body_steps_summand. fs_h_dst_permutation_targetpositive_body_steps_summand + S (fs_a_dst_permutation_targetpositive_body_steps) = S ((S (fs_i_dst_permutation_targetpositive_body_steps)) * dst_positive_scale_permutation_target)) /\ exists fs_q_dst_permutation_targetpositive_body_steps_summand. dst_positive_code_permutation_target = fs_q_dst_permutation_targetpositive_body_steps_summand * S ((S (fs_i_dst_permutation_targetpositive_body_steps)) * dst_positive_scale_permutation_target) + (fs_a_dst_permutation_targetpositive_body_steps))) /\ ((((exists fs_h_dst_permutation_targetpositive_body_steps_partial. fs_h_dst_permutation_targetpositive_body_steps_partial + S (fs_r_dst_permutation_targetpositive_body_steps) = S ((S (fs_i_dst_permutation_targetpositive_body_steps)) * fs_v_dst_permutation_targetpositive)) /\ exists fs_q_dst_permutation_targetpositive_body_steps_partial. fs_u_dst_permutation_targetpositive = fs_q_dst_permutation_targetpositive_body_steps_partial * S ((S (fs_i_dst_permutation_targetpositive_body_steps)) * fs_v_dst_permutation_targetpositive) + (fs_r_dst_permutation_targetpositive_body_steps))) /\ ((((exists fs_h_dst_permutation_targetpositive_body_steps_successor. fs_h_dst_permutation_targetpositive_body_steps_successor + S (fs_s_dst_permutation_targetpositive_body_steps) = S ((S (S fs_i_dst_permutation_targetpositive_body_steps)) * fs_v_dst_permutation_targetpositive)) /\ exists fs_q_dst_permutation_targetpositive_body_steps_successor. fs_u_dst_permutation_targetpositive = fs_q_dst_permutation_targetpositive_body_steps_successor * S ((S (S fs_i_dst_permutation_targetpositive_body_steps)) * fs_v_dst_permutation_targetpositive) + (fs_s_dst_permutation_targetpositive_body_steps))) /\ fs_s_dst_permutation_targetpositive_body_steps = fs_r_dst_permutation_targetpositive_body_steps + fs_a_dst_permutation_targetpositive_body_steps)))))) /\ (((exists fs_u_dst_permutation_targetnegative fs_v_dst_permutation_targetnegative. ((((exists fs_h_dst_permutation_targetnegative_body_start. fs_h_dst_permutation_targetnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_permutation_targetnegative)) /\ exists fs_q_dst_permutation_targetnegative_body_start. fs_u_dst_permutation_targetnegative = fs_q_dst_permutation_targetnegative_body_start * S ((S (0)) * fs_v_dst_permutation_targetnegative) + (0))) /\ ((((exists fs_h_dst_permutation_targetnegative_body_terminal. fs_h_dst_permutation_targetnegative_body_terminal + S (dst_negative_sum_permutation_target) = S ((S (l)) * fs_v_dst_permutation_targetnegative)) /\ exists fs_q_dst_permutation_targetnegative_body_terminal. fs_u_dst_permutation_targetnegative = fs_q_dst_permutation_targetnegative_body_terminal * S ((S (l)) * fs_v_dst_permutation_targetnegative) + (dst_negative_sum_permutation_target))) /\ forall fs_i_dst_permutation_targetnegative_body_steps. (exists fs_lt_dst_permutation_targetnegative_body_steps_bound. fs_lt_dst_permutation_targetnegative_body_steps_bound + S fs_i_dst_permutation_targetnegative_body_steps = l) -> exists fs_a_dst_permutation_targetnegative_body_steps fs_r_dst_permutation_targetnegative_body_steps fs_s_dst_permutation_targetnegative_body_steps. ((((exists fs_h_dst_permutation_targetnegative_body_steps_summand. fs_h_dst_permutation_targetnegative_body_steps_summand + S (fs_a_dst_permutation_targetnegative_body_steps) = S ((S (fs_i_dst_permutation_targetnegative_body_steps)) * dst_negative_scale_permutation_target)) /\ exists fs_q_dst_permutation_targetnegative_body_steps_summand. dst_negative_code_permutation_target = fs_q_dst_permutation_targetnegative_body_steps_summand * S ((S (fs_i_dst_permutation_targetnegative_body_steps)) * dst_negative_scale_permutation_target) + (fs_a_dst_permutation_targetnegative_body_steps))) /\ ((((exists fs_h_dst_permutation_targetnegative_body_steps_partial. fs_h_dst_permutation_targetnegative_body_steps_partial + S (fs_r_dst_permutation_targetnegative_body_steps) = S ((S (fs_i_dst_permutation_targetnegative_body_steps)) * fs_v_dst_permutation_targetnegative)) /\ exists fs_q_dst_permutation_targetnegative_body_steps_partial. fs_u_dst_permutation_targetnegative = fs_q_dst_permutation_targetnegative_body_steps_partial * S ((S (fs_i_dst_permutation_targetnegative_body_steps)) * fs_v_dst_permutation_targetnegative) + (fs_r_dst_permutation_targetnegative_body_steps))) /\ ((((exists fs_h_dst_permutation_targetnegative_body_steps_successor. fs_h_dst_permutation_targetnegative_body_steps_successor + S (fs_s_dst_permutation_targetnegative_body_steps) = S ((S (S fs_i_dst_permutation_targetnegative_body_steps)) * fs_v_dst_permutation_targetnegative)) /\ exists fs_q_dst_permutation_targetnegative_body_steps_successor. fs_u_dst_permutation_targetnegative = fs_q_dst_permutation_targetnegative_body_steps_successor * S ((S (S fs_i_dst_permutation_targetnegative_body_steps)) * fs_v_dst_permutation_targetnegative) + (fs_s_dst_permutation_targetnegative_body_steps))) /\ fs_s_dst_permutation_targetnegative_body_steps = fs_r_dst_permutation_targetnegative_body_steps + fs_a_dst_permutation_targetnegative_body_steps)))))) /\ (exists ge_balance_positive_permutation_targetresult ge_balance_negative_permutation_targetresult. (((((v) = 2 * (ge_balance_positive_permutation_targetresult) /\ (ge_balance_negative_permutation_targetresult) = 0) \/ exists ge_signed_half_permutation_targetresultdecode. (((v) = 2 * ge_signed_half_permutation_targetresultdecode + 1 /\ (ge_balance_positive_permutation_targetresult) = 0) /\ (ge_balance_negative_permutation_targetresult) = S ge_signed_half_permutation_targetresultdecode))) /\ ((dst_positive_sum_permutation_target) + ge_balance_negative_permutation_targetresult = (dst_negative_sum_permutation_target) + ge_balance_positive_permutation_targetresult))))))))) -> u = v

divisor_signed_table_at_functional · checked inherited prerequisite

Exact statement in the checked dependency cone

forall F i a b. (exists dst_positive_code_functional_first dst_positive_scale_functional_first dst_negative_code_functional_first dst_negative_scale_functional_first dst_positive_functional_first dst_negative_functional_first. (((F) = (((((dst_positive_code_functional_first) + (dst_positive_scale_functional_first)) * S ((dst_positive_code_functional_first) + (dst_positive_scale_functional_first)) + ((dst_positive_scale_functional_first) + (dst_positive_scale_functional_first))) + (((dst_negative_code_functional_first) + (dst_negative_scale_functional_first)) * S ((dst_negative_code_functional_first) + (dst_negative_scale_functional_first)) + ((dst_negative_scale_functional_first) + (dst_negative_scale_functional_first)))) * S ((((dst_positive_code_functional_first) + (dst_positive_scale_functional_first)) * S ((dst_positive_code_functional_first) + (dst_positive_scale_functional_first)) + ((dst_positive_scale_functional_first) + (dst_positive_scale_functional_first))) + (((dst_negative_code_functional_first) + (dst_negative_scale_functional_first)) * S ((dst_negative_code_functional_first) + (dst_negative_scale_functional_first)) + ((dst_negative_scale_functional_first) + (dst_negative_scale_functional_first)))) + ((((dst_negative_code_functional_first) + (dst_negative_scale_functional_first)) * S ((dst_negative_code_functional_first) + (dst_negative_scale_functional_first)) + ((dst_negative_scale_functional_first) + (dst_negative_scale_functional_first))) + (((dst_negative_code_functional_first) + (dst_negative_scale_functional_first)) * S ((dst_negative_code_functional_first) + (dst_negative_scale_functional_first)) + ((dst_negative_scale_functional_first) + (dst_negative_scale_functional_first)))))) /\ (((((exists ff_h_pvs_functional_firstpositive. ff_h_pvs_functional_firstpositive + S (dst_positive_functional_first) = S ((S (i)) * dst_positive_scale_functional_first)) /\ exists ff_q_pvs_functional_firstpositive. dst_positive_code_functional_first = ff_q_pvs_functional_firstpositive * S ((S (i)) * dst_positive_scale_functional_first) + (dst_positive_functional_first))) /\ (((((exists ff_h_pvs_functional_firstnegative. ff_h_pvs_functional_firstnegative + S (dst_negative_functional_first) = S ((S (i)) * dst_negative_scale_functional_first)) /\ exists ff_q_pvs_functional_firstnegative. dst_negative_code_functional_first = ff_q_pvs_functional_firstnegative * S ((S (i)) * dst_negative_scale_functional_first) + (dst_negative_functional_first))) /\ (exists ge_balance_positive_functional_firstvalue ge_balance_negative_functional_firstvalue. (((((a) = 2 * (ge_balance_positive_functional_firstvalue) /\ (ge_balance_negative_functional_firstvalue) = 0) \/ exists ge_signed_half_functional_firstvaluedecode. (((a) = 2 * ge_signed_half_functional_firstvaluedecode + 1 /\ (ge_balance_positive_functional_firstvalue) = 0) /\ (ge_balance_negative_functional_firstvalue) = S ge_signed_half_functional_firstvaluedecode))) /\ ((dst_positive_functional_first) + ge_balance_negative_functional_firstvalue = (dst_negative_functional_first) + ge_balance_positive_functional_firstvalue))))))))) -> (exists dst_positive_code_functional_second dst_positive_scale_functional_second dst_negative_code_functional_second dst_negative_scale_functional_second dst_positive_functional_second dst_negative_functional_second. (((F) = (((((dst_positive_code_functional_second) + (dst_positive_scale_functional_second)) * S ((dst_positive_code_functional_second) + (dst_positive_scale_functional_second)) + ((dst_positive_scale_functional_second) + (dst_positive_scale_functional_second))) + (((dst_negative_code_functional_second) + (dst_negative_scale_functional_second)) * S ((dst_negative_code_functional_second) + (dst_negative_scale_functional_second)) + ((dst_negative_scale_functional_second) + (dst_negative_scale_functional_second)))) * S ((((dst_positive_code_functional_second) + (dst_positive_scale_functional_second)) * S ((dst_positive_code_functional_second) + (dst_positive_scale_functional_second)) + ((dst_positive_scale_functional_second) + (dst_positive_scale_functional_second))) + (((dst_negative_code_functional_second) + (dst_negative_scale_functional_second)) * S ((dst_negative_code_functional_second) + (dst_negative_scale_functional_second)) + ((dst_negative_scale_functional_second) + (dst_negative_scale_functional_second)))) + ((((dst_negative_code_functional_second) + (dst_negative_scale_functional_second)) * S ((dst_negative_code_functional_second) + (dst_negative_scale_functional_second)) + ((dst_negative_scale_functional_second) + (dst_negative_scale_functional_second))) + (((dst_negative_code_functional_second) + (dst_negative_scale_functional_second)) * S ((dst_negative_code_functional_second) + (dst_negative_scale_functional_second)) + ((dst_negative_scale_functional_second) + (dst_negative_scale_functional_second)))))) /\ (((((exists ff_h_pvs_functional_secondpositive. ff_h_pvs_functional_secondpositive + S (dst_positive_functional_second) = S ((S (i)) * dst_positive_scale_functional_second)) /\ exists ff_q_pvs_functional_secondpositive. dst_positive_code_functional_second = ff_q_pvs_functional_secondpositive * S ((S (i)) * dst_positive_scale_functional_second) + (dst_positive_functional_second))) /\ (((((exists ff_h_pvs_functional_secondnegative. ff_h_pvs_functional_secondnegative + S (dst_negative_functional_second) = S ((S (i)) * dst_negative_scale_functional_second)) /\ exists ff_q_pvs_functional_secondnegative. dst_negative_code_functional_second = ff_q_pvs_functional_secondnegative * S ((S (i)) * dst_negative_scale_functional_second) + (dst_negative_functional_second))) /\ (exists ge_balance_positive_functional_secondvalue ge_balance_negative_functional_secondvalue. (((((b) = 2 * (ge_balance_positive_functional_secondvalue) /\ (ge_balance_negative_functional_secondvalue) = 0) \/ exists ge_signed_half_functional_secondvaluedecode. (((b) = 2 * ge_signed_half_functional_secondvaluedecode + 1 /\ (ge_balance_positive_functional_secondvalue) = 0) /\ (ge_balance_negative_functional_secondvalue) = S ge_signed_half_functional_secondvaluedecode))) /\ ((dst_positive_functional_second) + ge_balance_negative_functional_secondvalue = (dst_negative_functional_second) + ge_balance_positive_functional_secondvalue))))))))) -> a = b

divisor_signed_table_lookup · checked inherited prerequisite

Exact statement in the checked dependency cone

forall N F i. (exists dst_positive_code_lookup_table dst_positive_scale_lookup_table dst_negative_code_lookup_table dst_negative_scale_lookup_table. (((F) = (((((dst_positive_code_lookup_table) + (dst_positive_scale_lookup_table)) * S ((dst_positive_code_lookup_table) + (dst_positive_scale_lookup_table)) + ((dst_positive_scale_lookup_table) + (dst_positive_scale_lookup_table))) + (((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) * S ((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) + ((dst_negative_scale_lookup_table) + (dst_negative_scale_lookup_table)))) * S ((((dst_positive_code_lookup_table) + (dst_positive_scale_lookup_table)) * S ((dst_positive_code_lookup_table) + (dst_positive_scale_lookup_table)) + ((dst_positive_scale_lookup_table) + (dst_positive_scale_lookup_table))) + (((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) * S ((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) + ((dst_negative_scale_lookup_table) + (dst_negative_scale_lookup_table)))) + ((((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) * S ((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) + ((dst_negative_scale_lookup_table) + (dst_negative_scale_lookup_table))) + (((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) * S ((dst_negative_code_lookup_table) + (dst_negative_scale_lookup_table)) + ((dst_negative_scale_lookup_table) + (dst_negative_scale_lookup_table)))))) /\ (forall dst_index_lookup_table. (exists pvs_le_gap_lookup_tabledomain. pvs_le_gap_lookup_tabledomain + (dst_index_lookup_table) = (N)) -> exists dst_positive_lookup_table dst_negative_lookup_table dst_value_lookup_table. ((((exists ff_h_pvs_lookup_tableentrypositive. ff_h_pvs_lookup_tableentrypositive + S (dst_positive_lookup_table) = S ((S (dst_index_lookup_table)) * dst_positive_scale_lookup_table)) /\ exists ff_q_pvs_lookup_tableentrypositive. dst_positive_code_lookup_table = ff_q_pvs_lookup_tableentrypositive * S ((S (dst_index_lookup_table)) * dst_positive_scale_lookup_table) + (dst_positive_lookup_table))) /\ (((((exists ff_h_pvs_lookup_tableentrynegative. ff_h_pvs_lookup_tableentrynegative + S (dst_negative_lookup_table) = S ((S (dst_index_lookup_table)) * dst_negative_scale_lookup_table)) /\ exists ff_q_pvs_lookup_tableentrynegative. dst_negative_code_lookup_table = ff_q_pvs_lookup_tableentrynegative * S ((S (dst_index_lookup_table)) * dst_negative_scale_lookup_table) + (dst_negative_lookup_table))) /\ (exists ge_balance_positive_lookup_tableentryvalue ge_balance_negative_lookup_tableentryvalue. (((((dst_value_lookup_table) = 2 * (ge_balance_positive_lookup_tableentryvalue) /\ (ge_balance_negative_lookup_tableentryvalue) = 0) \/ exists ge_signed_half_lookup_tableentryvaluedecode. (((dst_value_lookup_table) = 2 * ge_signed_half_lookup_tableentryvaluedecode + 1 /\ (ge_balance_positive_lookup_tableentryvalue) = 0) /\ (ge_balance_negative_lookup_tableentryvalue) = S ge_signed_half_lookup_tableentryvaluedecode))) /\ ((dst_positive_lookup_table) + ge_balance_negative_lookup_tableentryvalue = (dst_negative_lookup_table) + ge_balance_positive_lookup_tableentryvalue))))))))) -> (exists pvs_le_gap_lookup_domain. pvs_le_gap_lookup_domain + (i) = (N)) -> exists z. (exists dst_positive_code_lookup_result dst_positive_scale_lookup_result dst_negative_code_lookup_result dst_negative_scale_lookup_result dst_positive_lookup_result dst_negative_lookup_result. (((F) = (((((dst_positive_code_lookup_result) + (dst_positive_scale_lookup_result)) * S ((dst_positive_code_lookup_result) + (dst_positive_scale_lookup_result)) + ((dst_positive_scale_lookup_result) + (dst_positive_scale_lookup_result))) + (((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) * S ((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) + ((dst_negative_scale_lookup_result) + (dst_negative_scale_lookup_result)))) * S ((((dst_positive_code_lookup_result) + (dst_positive_scale_lookup_result)) * S ((dst_positive_code_lookup_result) + (dst_positive_scale_lookup_result)) + ((dst_positive_scale_lookup_result) + (dst_positive_scale_lookup_result))) + (((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) * S ((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) + ((dst_negative_scale_lookup_result) + (dst_negative_scale_lookup_result)))) + ((((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) * S ((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) + ((dst_negative_scale_lookup_result) + (dst_negative_scale_lookup_result))) + (((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) * S ((dst_negative_code_lookup_result) + (dst_negative_scale_lookup_result)) + ((dst_negative_scale_lookup_result) + (dst_negative_scale_lookup_result)))))) /\ (((((exists ff_h_pvs_lookup_resultpositive. ff_h_pvs_lookup_resultpositive + S (dst_positive_lookup_result) = S ((S (i)) * dst_positive_scale_lookup_result)) /\ exists ff_q_pvs_lookup_resultpositive. dst_positive_code_lookup_result = ff_q_pvs_lookup_resultpositive * S ((S (i)) * dst_positive_scale_lookup_result) + (dst_positive_lookup_result))) /\ (((((exists ff_h_pvs_lookup_resultnegative. ff_h_pvs_lookup_resultnegative + S (dst_negative_lookup_result) = S ((S (i)) * dst_negative_scale_lookup_result)) /\ exists ff_q_pvs_lookup_resultnegative. dst_negative_code_lookup_result = ff_q_pvs_lookup_resultnegative * S ((S (i)) * dst_negative_scale_lookup_result) + (dst_negative_lookup_result))) /\ (exists ge_balance_positive_lookup_resultvalue ge_balance_negative_lookup_resultvalue. (((((z) = 2 * (ge_balance_positive_lookup_resultvalue) /\ (ge_balance_negative_lookup_resultvalue) = 0) \/ exists ge_signed_half_lookup_resultvaluedecode. (((z) = 2 * ge_signed_half_lookup_resultvaluedecode + 1 /\ (ge_balance_positive_lookup_resultvalue) = 0) /\ (ge_balance_negative_lookup_resultvalue) = S ge_signed_half_lookup_resultvaluedecode))) /\ ((dst_positive_lookup_result) + ge_balance_negative_lookup_resultvalue = (dst_negative_lookup_result) + ge_balance_positive_lookup_resultvalue)))))))))

divisor_signed_table_restrict · checked inherited prerequisite

Exact statement in the checked dependency cone

forall N K F. (exists dst_positive_code_restriction_source dst_positive_scale_restriction_source dst_negative_code_restriction_source dst_negative_scale_restriction_source. (((F) = (((((dst_positive_code_restriction_source) + (dst_positive_scale_restriction_source)) * S ((dst_positive_code_restriction_source) + (dst_positive_scale_restriction_source)) + ((dst_positive_scale_restriction_source) + (dst_positive_scale_restriction_source))) + (((dst_negative_code_restriction_source) + (dst_negative_scale_restriction_source)) * S ((dst_negative_code_restriction_source) + (dst_negative_scale_restriction_source)) + ((dst_negative_scale_restriction_source) + (dst_negative_scale_restriction_source)))) * S ((((dst_positive_code_restriction_source) + (dst_positive_scale_restriction_source)) * S ((dst_positive_code_restriction_source) + (dst_positive_scale_restriction_source)) + ((dst_positive_scale_restriction_source) + (dst_positive_scale_restriction_source))) + (((dst_negative_code_restriction_source) + (dst_negative_scale_restriction_source)) * S ((dst_negative_code_restriction_source) + (dst_negative_scale_restriction_source)) + ((dst_negative_scale_restriction_source) + (dst_negative_scale_restriction_source)))) + ((((dst_negative_code_restriction_source) + (dst_negative_scale_restriction_source)) * S ((dst_negative_code_restriction_source) + (dst_negative_scale_restriction_source)) + ((dst_negative_scale_restriction_source) + (dst_negative_scale_restriction_source))) + (((dst_negative_code_restriction_source) + (dst_negative_scale_restriction_source)) * S ((dst_negative_code_restriction_source) + (dst_negative_scale_restriction_source)) + ((dst_negative_scale_restriction_source) + (dst_negative_scale_restriction_source)))))) /\ (forall dst_index_restriction_source. (exists pvs_le_gap_restriction_sourcedomain. pvs_le_gap_restriction_sourcedomain + (dst_index_restriction_source) = (N)) -> exists dst_positive_restriction_source dst_negative_restriction_source dst_value_restriction_source. ((((exists ff_h_pvs_restriction_sourceentrypositive. ff_h_pvs_restriction_sourceentrypositive + S (dst_positive_restriction_source) = S ((S (dst_index_restriction_source)) * dst_positive_scale_restriction_source)) /\ exists ff_q_pvs_restriction_sourceentrypositive. dst_positive_code_restriction_source = ff_q_pvs_restriction_sourceentrypositive * S ((S (dst_index_restriction_source)) * dst_positive_scale_restriction_source) + (dst_positive_restriction_source))) /\ (((((exists ff_h_pvs_restriction_sourceentrynegative. ff_h_pvs_restriction_sourceentrynegative + S (dst_negative_restriction_source) = S ((S (dst_index_restriction_source)) * dst_negative_scale_restriction_source)) /\ exists ff_q_pvs_restriction_sourceentrynegative. dst_negative_code_restriction_source = ff_q_pvs_restriction_sourceentrynegative * S ((S (dst_index_restriction_source)) * dst_negative_scale_restriction_source) + (dst_negative_restriction_source))) /\ (exists ge_balance_positive_restriction_sourceentryvalue ge_balance_negative_restriction_sourceentryvalue. (((((dst_value_restriction_source) = 2 * (ge_balance_positive_restriction_sourceentryvalue) /\ (ge_balance_negative_restriction_sourceentryvalue) = 0) \/ exists ge_signed_half_restriction_sourceentryvaluedecode. (((dst_value_restriction_source) = 2 * ge_signed_half_restriction_sourceentryvaluedecode + 1 /\ (ge_balance_positive_restriction_sourceentryvalue) = 0) /\ (ge_balance_negative_restriction_sourceentryvalue) = S ge_signed_half_restriction_sourceentryvaluedecode))) /\ ((dst_positive_restriction_source) + ge_balance_negative_restriction_sourceentryvalue = (dst_negative_restriction_source) + ge_balance_positive_restriction_sourceentryvalue))))))))) -> (exists pvs_le_gap_restriction_bound. pvs_le_gap_restriction_bound + (K) = (N)) -> (exists dst_positive_code_restriction_target dst_positive_scale_restriction_target dst_negative_code_restriction_target dst_negative_scale_restriction_target. (((F) = (((((dst_positive_code_restriction_target) + (dst_positive_scale_restriction_target)) * S ((dst_positive_code_restriction_target) + (dst_positive_scale_restriction_target)) + ((dst_positive_scale_restriction_target) + (dst_positive_scale_restriction_target))) + (((dst_negative_code_restriction_target) + (dst_negative_scale_restriction_target)) * S ((dst_negative_code_restriction_target) + (dst_negative_scale_restriction_target)) + ((dst_negative_scale_restriction_target) + (dst_negative_scale_restriction_target)))) * S ((((dst_positive_code_restriction_target) + (dst_positive_scale_restriction_target)) * S ((dst_positive_code_restriction_target) + (dst_positive_scale_restriction_target)) + ((dst_positive_scale_restriction_target) + (dst_positive_scale_restriction_target))) + (((dst_negative_code_restriction_target) + (dst_negative_scale_restriction_target)) * S ((dst_negative_code_restriction_target) + (dst_negative_scale_restriction_target)) + ((dst_negative_scale_restriction_target) + (dst_negative_scale_restriction_target)))) + ((((dst_negative_code_restriction_target) + (dst_negative_scale_restriction_target)) * S ((dst_negative_code_restriction_target) + (dst_negative_scale_restriction_target)) + ((dst_negative_scale_restriction_target) + (dst_negative_scale_restriction_target))) + (((dst_negative_code_restriction_target) + (dst_negative_scale_restriction_target)) * S ((dst_negative_code_restriction_target) + (dst_negative_scale_restriction_target)) + ((dst_negative_scale_restriction_target) + (dst_negative_scale_restriction_target)))))) /\ (forall dst_index_restriction_target. (exists pvs_le_gap_restriction_targetdomain. pvs_le_gap_restriction_targetdomain + (dst_index_restriction_target) = (K)) -> exists dst_positive_restriction_target dst_negative_restriction_target dst_value_restriction_target. ((((exists ff_h_pvs_restriction_targetentrypositive. ff_h_pvs_restriction_targetentrypositive + S (dst_positive_restriction_target) = S ((S (dst_index_restriction_target)) * dst_positive_scale_restriction_target)) /\ exists ff_q_pvs_restriction_targetentrypositive. dst_positive_code_restriction_target = ff_q_pvs_restriction_targetentrypositive * S ((S (dst_index_restriction_target)) * dst_positive_scale_restriction_target) + (dst_positive_restriction_target))) /\ (((((exists ff_h_pvs_restriction_targetentrynegative. ff_h_pvs_restriction_targetentrynegative + S (dst_negative_restriction_target) = S ((S (dst_index_restriction_target)) * dst_negative_scale_restriction_target)) /\ exists ff_q_pvs_restriction_targetentrynegative. dst_negative_code_restriction_target = ff_q_pvs_restriction_targetentrynegative * S ((S (dst_index_restriction_target)) * dst_negative_scale_restriction_target) + (dst_negative_restriction_target))) /\ (exists ge_balance_positive_restriction_targetentryvalue ge_balance_negative_restriction_targetentryvalue. (((((dst_value_restriction_target) = 2 * (ge_balance_positive_restriction_targetentryvalue) /\ (ge_balance_negative_restriction_targetentryvalue) = 0) \/ exists ge_signed_half_restriction_targetentryvaluedecode. (((dst_value_restriction_target) = 2 * ge_signed_half_restriction_targetentryvaluedecode + 1 /\ (ge_balance_positive_restriction_targetentryvalue) = 0) /\ (ge_balance_negative_restriction_targetentryvalue) = S ge_signed_half_restriction_targetentryvaluedecode))) /\ ((dst_positive_restriction_target) + ge_balance_negative_restriction_targetentryvalue = (dst_negative_restriction_target) + ge_balance_positive_restriction_targetentryvalue)))))))))

eq_decidable · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b. a = b \/ ~(a = b)
```
factor_nonzero_right · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n c d. ~(n = 0) -> n = c * d -> ~(d = 0)
```
le_eq_or_lt · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b. (exists k. k + a = b) -> a = b \/ exists k. k + S a = b
```
le_of_succ_le_succ · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b. (exists k. k + S a = S b) -> exists r. r + a = b
```
le_refl · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. n <= n
```
le_trans · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n m k. n <= m -> m <= k -> n <= k
```
le_zero · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n. n <= 0 -> n = 0
```
lt_not_le · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b. (exists k. k + S a = b) -> ~ (exists k. k + b = a)
```
mul_comm · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall n m. n * m = m * n
```
mul_left_cancel_nonzero · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b c. ~(a = 0) -> a * b = a * c -> b = c
```
multiple_decidable_nonzero · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall d n. ~(d = 0) -> (exists q. n = d * q) \/ ~(exists q. n = d * q)
```

positive_divisor_involution_exists · checked inherited prerequisite

Exact statement in the checked dependency cone

forall n. ~(n=0) -> exists b c. (forall dvi_index_involution_prefix. (exists pvs_gap_involution_prefixdomain. pvs_gap_involution_prefixdomain + S (dvi_index_involution_prefix) = (S n)) -> exists dvi_value_involution_prefix. ((((exists ff_h_pvs_involution_prefixentry. ff_h_pvs_involution_prefixentry + S (dvi_value_involution_prefix) = S ((S (dvi_index_involution_prefix)) * c)) /\ exists ff_q_pvs_involution_prefixentry. b = ff_q_pvs_involution_prefixentry * S ((S (dvi_index_involution_prefix)) * c) + (dvi_value_involution_prefix))) /\ ((((~((dvi_index_involution_prefix)=0)) /\ ((n)=(dvi_index_involution_prefix)*(dvi_value_involution_prefix)))) \/ ((((dvi_index_involution_prefix)=0 \/ ~(exists pvs_factor_involution_prefixgraphnondivisor. (n) = (dvi_index_involution_prefix) * pvs_factor_involution_prefixgraphnondivisor)) /\ ((dvi_value_involution_prefix)=(dvi_index_involution_prefix))))))) /\ (((forall pfp_i_involution_permutationbounded. (exists pfp_gap_involution_permutationboundedindex. pfp_gap_involution_permutationboundedindex + S (pfp_i_involution_permutationbounded) = (S n)) -> exists pfp_a_involution_permutationbounded. (((exists ff_h_pfp_involution_permutationboundedentry. ff_h_pfp_involution_permutationboundedentry + S (pfp_a_involution_permutationbounded) = S ((S (pfp_i_involution_permutationbounded)) * c)) /\ exists ff_q_pfp_involution_permutationboundedentry. b = ff_q_pfp_involution_permutationboundedentry * S ((S (pfp_i_involution_permutationbounded)) * c) + (pfp_a_involution_permutationbounded))) /\ (exists pfp_gap_involution_permutationboundedvalue. pfp_gap_involution_permutationboundedvalue + S (pfp_a_involution_permutationbounded) = (S n))) /\ (((forall pfp_i_involution_permutationinjective pfp_j_involution_permutationinjective pfp_a_involution_permutationinjective. (exists pfp_gap_involution_permutationinjectivefirst. pfp_gap_involution_permutationinjectivefirst + S (pfp_i_involution_permutationinjective) = (S n)) -> (exists pfp_gap_involution_permutationinjectivesecond. pfp_gap_involution_permutationinjectivesecond + S (pfp_j_involution_permutationinjective) = (S n)) -> (((exists ff_h_pfp_involution_permutationinjectiveleft. ff_h_pfp_involution_permutationinjectiveleft + S (pfp_a_involution_permutationinjective) = S ((S (pfp_i_involution_permutationinjective)) * c)) /\ exists ff_q_pfp_involution_permutationinjectiveleft. b = ff_q_pfp_involution_permutationinjectiveleft * S ((S (pfp_i_involution_permutationinjective)) * c) + (pfp_a_involution_permutationinjective))) -> (((exists ff_h_pfp_involution_permutationinjectiveright. ff_h_pfp_involution_permutationinjectiveright + S (pfp_a_involution_permutationinjective) = S ((S (pfp_j_involution_permutationinjective)) * c)) /\ exists ff_q_pfp_involution_permutationinjectiveright. b = ff_q_pfp_involution_permutationinjectiveright * S ((S (pfp_j_involution_permutationinjective)) * c) + (pfp_a_involution_permutationinjective))) -> pfp_i_involution_permutationinjective = pfp_j_involution_permutationinjective) /\ (forall pfp_a_involution_permutationsurjective. (exists pfp_gap_involution_permutationsurjectivevalue. pfp_gap_involution_permutationsurjectivevalue + S (pfp_a_involution_permutationsurjective) = (S n)) -> exists pfp_i_involution_permutationsurjective. (exists pfp_gap_involution_permutationsurjectiveindex. pfp_gap_involution_permutationsurjectiveindex + S (pfp_i_involution_permutationsurjective) = (S n)) /\ (((exists ff_h_pfp_involution_permutationsurjectiveentry. ff_h_pfp_involution_permutationsurjectiveentry + S (pfp_a_involution_permutationsurjective) = S ((S (pfp_i_involution_permutationsurjective)) * c)) /\ exists ff_q_pfp_involution_permutationsurjectiveentry. b = ff_q_pfp_involution_permutationsurjectiveentry * S ((S (pfp_i_involution_permutationsurjective)) * c) + (pfp_a_involution_permutationsurjective))))))))

signed_mul_commutative · checked inherited prerequisite

Exact statement in the checked dependency cone

forall left right output. (exists sm_lp_comm_forward sm_ln_comm_forward sm_rp_comm_forward sm_rn_comm_forward sm_op_comm_forward sm_on_comm_forward. (((left = 2 * sm_lp_comm_forward /\ sm_ln_comm_forward = 0) \/ exists sd_half_comm_forward_left. ((left = 2 * sd_half_comm_forward_left + 1 /\ sm_lp_comm_forward = 0) /\ sm_ln_comm_forward = S sd_half_comm_forward_left)) /\ (((right = 2 * sm_rp_comm_forward /\ sm_rn_comm_forward = 0) \/ exists sd_half_comm_forward_right. ((right = 2 * sd_half_comm_forward_right + 1 /\ sm_rp_comm_forward = 0) /\ sm_rn_comm_forward = S sd_half_comm_forward_right)) /\ (((output = 2 * sm_op_comm_forward /\ sm_on_comm_forward = 0) \/ exists sd_half_comm_forward_output. ((output = 2 * sd_half_comm_forward_output + 1 /\ sm_op_comm_forward = 0) /\ sm_on_comm_forward = S sd_half_comm_forward_output)) /\ (sm_lp_comm_forward * sm_rp_comm_forward + sm_ln_comm_forward * sm_rn_comm_forward) + sm_on_comm_forward = (sm_lp_comm_forward * sm_rn_comm_forward + sm_ln_comm_forward * sm_rp_comm_forward) + sm_op_comm_forward)))) -> (exists sm_lp_comm_reverse sm_ln_comm_reverse sm_rp_comm_reverse sm_rn_comm_reverse sm_op_comm_reverse sm_on_comm_reverse. (((right = 2 * sm_lp_comm_reverse /\ sm_ln_comm_reverse = 0) \/ exists sd_half_comm_reverse_left. ((right = 2 * sd_half_comm_reverse_left + 1 /\ sm_lp_comm_reverse = 0) /\ sm_ln_comm_reverse = S sd_half_comm_reverse_left)) /\ (((left = 2 * sm_rp_comm_reverse /\ sm_rn_comm_reverse = 0) \/ exists sd_half_comm_reverse_right. ((left = 2 * sd_half_comm_reverse_right + 1 /\ sm_rp_comm_reverse = 0) /\ sm_rn_comm_reverse = S sd_half_comm_reverse_right)) /\ (((output = 2 * sm_op_comm_reverse /\ sm_on_comm_reverse = 0) \/ exists sd_half_comm_reverse_output. ((output = 2 * sd_half_comm_reverse_output + 1 /\ sm_op_comm_reverse = 0) /\ sm_on_comm_reverse = S sd_half_comm_reverse_output)) /\ (sm_lp_comm_reverse * sm_rp_comm_reverse + sm_ln_comm_reverse * sm_rn_comm_reverse) + sm_on_comm_reverse = (sm_lp_comm_reverse * sm_rn_comm_reverse + sm_ln_comm_reverse * sm_rp_comm_reverse) + sm_op_comm_reverse))))

signed_mul_functional · checked inherited prerequisite

Exact statement in the checked dependency cone

forall left right output1 output2. (exists sm_lp_functional_left sm_ln_functional_left sm_rp_functional_left sm_rn_functional_left sm_op_functional_left sm_on_functional_left. (((left = 2 * sm_lp_functional_left /\ sm_ln_functional_left = 0) \/ exists sd_half_functional_left_left. ((left = 2 * sd_half_functional_left_left + 1 /\ sm_lp_functional_left = 0) /\ sm_ln_functional_left = S sd_half_functional_left_left)) /\ (((right = 2 * sm_rp_functional_left /\ sm_rn_functional_left = 0) \/ exists sd_half_functional_left_right. ((right = 2 * sd_half_functional_left_right + 1 /\ sm_rp_functional_left = 0) /\ sm_rn_functional_left = S sd_half_functional_left_right)) /\ (((output1 = 2 * sm_op_functional_left /\ sm_on_functional_left = 0) \/ exists sd_half_functional_left_output. ((output1 = 2 * sd_half_functional_left_output + 1 /\ sm_op_functional_left = 0) /\ sm_on_functional_left = S sd_half_functional_left_output)) /\ (sm_lp_functional_left * sm_rp_functional_left + sm_ln_functional_left * sm_rn_functional_left) + sm_on_functional_left = (sm_lp_functional_left * sm_rn_functional_left + sm_ln_functional_left * sm_rp_functional_left) + sm_op_functional_left)))) -> (exists sm_lp_functional_right sm_ln_functional_right sm_rp_functional_right sm_rn_functional_right sm_op_functional_right sm_on_functional_right. (((left = 2 * sm_lp_functional_right /\ sm_ln_functional_right = 0) \/ exists sd_half_functional_right_left. ((left = 2 * sd_half_functional_right_left + 1 /\ sm_lp_functional_right = 0) /\ sm_ln_functional_right = S sd_half_functional_right_left)) /\ (((right = 2 * sm_rp_functional_right /\ sm_rn_functional_right = 0) \/ exists sd_half_functional_right_right. ((right = 2 * sd_half_functional_right_right + 1 /\ sm_rp_functional_right = 0) /\ sm_rn_functional_right = S sd_half_functional_right_right)) /\ (((output2 = 2 * sm_op_functional_right /\ sm_on_functional_right = 0) \/ exists sd_half_functional_right_output. ((output2 = 2 * sd_half_functional_right_output + 1 /\ sm_op_functional_right = 0) /\ sm_on_functional_right = S sd_half_functional_right_output)) /\ (sm_lp_functional_right * sm_rp_functional_right + sm_ln_functional_right * sm_rn_functional_right) + sm_on_functional_right = (sm_lp_functional_right * sm_rn_functional_right + sm_ln_functional_right * sm_rp_functional_right) + sm_op_functional_right)))) -> output1 = output2

signed_mul_total · checked inherited prerequisite

Exact statement in the checked dependency cone

forall left right. exists output. (exists sm_lp_total sm_ln_total sm_rp_total sm_rn_total sm_op_total sm_on_total. (((left = 2 * sm_lp_total /\ sm_ln_total = 0) \/ exists sd_half_total_left. ((left = 2 * sd_half_total_left + 1 /\ sm_lp_total = 0) /\ sm_ln_total = S sd_half_total_left)) /\ (((right = 2 * sm_rp_total /\ sm_rn_total = 0) \/ exists sd_half_total_right. ((right = 2 * sd_half_total_right + 1 /\ sm_rp_total = 0) /\ sm_rn_total = S sd_half_total_right)) /\ (((output = 2 * sm_op_total /\ sm_on_total = 0) \/ exists sd_half_total_output. ((output = 2 * sd_half_total_output + 1 /\ sm_op_total = 0) /\ sm_on_total = S sd_half_total_output)) /\ (sm_lp_total * sm_rp_total + sm_ln_total * sm_rn_total) + sm_on_total = (sm_lp_total * sm_rn_total + sm_ln_total * sm_rp_total) + sm_op_total))))

signed_prefix_sum_zero_tail · checked inherited prerequisite

Exact statement in the checked dependency cone

forall F k l a b. (exists pvs_le_gap_tail_order. pvs_le_gap_tail_order + (k) = (l)) -> (forall sfs_index_tail_window sfs_value_tail_window. (exists pvs_le_gap_tail_windowlower. pvs_le_gap_tail_windowlower + (k) = (sfs_index_tail_window)) -> (exists pvs_gap_tail_windowupper. pvs_gap_tail_windowupper + S (sfs_index_tail_window) = (l)) -> (exists dst_positive_code_tail_windowentry dst_positive_scale_tail_windowentry dst_negative_code_tail_windowentry dst_negative_scale_tail_windowentry dst_positive_tail_windowentry dst_negative_tail_windowentry. (((F) = (((((dst_positive_code_tail_windowentry) + (dst_positive_scale_tail_windowentry)) * S ((dst_positive_code_tail_windowentry) + (dst_positive_scale_tail_windowentry)) + ((dst_positive_scale_tail_windowentry) + (dst_positive_scale_tail_windowentry))) + (((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) * S ((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) + ((dst_negative_scale_tail_windowentry) + (dst_negative_scale_tail_windowentry)))) * S ((((dst_positive_code_tail_windowentry) + (dst_positive_scale_tail_windowentry)) * S ((dst_positive_code_tail_windowentry) + (dst_positive_scale_tail_windowentry)) + ((dst_positive_scale_tail_windowentry) + (dst_positive_scale_tail_windowentry))) + (((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) * S ((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) + ((dst_negative_scale_tail_windowentry) + (dst_negative_scale_tail_windowentry)))) + ((((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) * S ((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) + ((dst_negative_scale_tail_windowentry) + (dst_negative_scale_tail_windowentry))) + (((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) * S ((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) + ((dst_negative_scale_tail_windowentry) + (dst_negative_scale_tail_windowentry)))))) /\ (((((exists ff_h_pvs_tail_windowentrypositive. ff_h_pvs_tail_windowentrypositive + S (dst_positive_tail_windowentry) = S ((S (sfs_index_tail_window)) * dst_positive_scale_tail_windowentry)) /\ exists ff_q_pvs_tail_windowentrypositive. dst_positive_code_tail_windowentry = ff_q_pvs_tail_windowentrypositive * S ((S (sfs_index_tail_window)) * dst_positive_scale_tail_windowentry) + (dst_positive_tail_windowentry))) /\ (((((exists ff_h_pvs_tail_windowentrynegative. ff_h_pvs_tail_windowentrynegative + S (dst_negative_tail_windowentry) = S ((S (sfs_index_tail_window)) * dst_negative_scale_tail_windowentry)) /\ exists ff_q_pvs_tail_windowentrynegative. dst_negative_code_tail_windowentry = ff_q_pvs_tail_windowentrynegative * S ((S (sfs_index_tail_window)) * dst_negative_scale_tail_windowentry) + (dst_negative_tail_windowentry))) /\ (exists ge_balance_positive_tail_windowentryvalue ge_balance_negative_tail_windowentryvalue. (((((sfs_value_tail_window) = 2 * (ge_balance_positive_tail_windowentryvalue) /\ (ge_balance_negative_tail_windowentryvalue) = 0) \/ exists ge_signed_half_tail_windowentryvaluedecode. (((sfs_value_tail_window) = 2 * ge_signed_half_tail_windowentryvaluedecode + 1 /\ (ge_balance_positive_tail_windowentryvalue) = 0) /\ (ge_balance_negative_tail_windowentryvalue) = S ge_signed_half_tail_windowentryvaluedecode))) /\ ((dst_positive_tail_windowentry) + ge_balance_negative_tail_windowentryvalue = (dst_negative_tail_windowentry) + ge_balance_positive_tail_windowentryvalue))))))))) -> sfs_value_tail_window=0) -> (exists dst_positive_code_tail_short dst_positive_scale_tail_short dst_negative_code_tail_short dst_negative_scale_tail_short dst_positive_sum_tail_short dst_negative_sum_tail_short. (((F) = (((((dst_positive_code_tail_short) + (dst_positive_scale_tail_short)) * S ((dst_positive_code_tail_short) + (dst_positive_scale_tail_short)) + ((dst_positive_scale_tail_short) + (dst_positive_scale_tail_short))) + (((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) * S ((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) + ((dst_negative_scale_tail_short) + (dst_negative_scale_tail_short)))) * S ((((dst_positive_code_tail_short) + (dst_positive_scale_tail_short)) * S ((dst_positive_code_tail_short) + (dst_positive_scale_tail_short)) + ((dst_positive_scale_tail_short) + (dst_positive_scale_tail_short))) + (((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) * S ((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) + ((dst_negative_scale_tail_short) + (dst_negative_scale_tail_short)))) + ((((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) * S ((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) + ((dst_negative_scale_tail_short) + (dst_negative_scale_tail_short))) + (((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) * S ((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) + ((dst_negative_scale_tail_short) + (dst_negative_scale_tail_short)))))) /\ (((exists fs_u_dst_tail_shortpositive fs_v_dst_tail_shortpositive. ((((exists fs_h_dst_tail_shortpositive_body_start. fs_h_dst_tail_shortpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_tail_shortpositive)) /\ exists fs_q_dst_tail_shortpositive_body_start. fs_u_dst_tail_shortpositive = fs_q_dst_tail_shortpositive_body_start * S ((S (0)) * fs_v_dst_tail_shortpositive) + (0))) /\ ((((exists fs_h_dst_tail_shortpositive_body_terminal. fs_h_dst_tail_shortpositive_body_terminal + S (dst_positive_sum_tail_short) = S ((S (k)) * fs_v_dst_tail_shortpositive)) /\ exists fs_q_dst_tail_shortpositive_body_terminal. fs_u_dst_tail_shortpositive = fs_q_dst_tail_shortpositive_body_terminal * S ((S (k)) * fs_v_dst_tail_shortpositive) + (dst_positive_sum_tail_short))) /\ forall fs_i_dst_tail_shortpositive_body_steps. (exists fs_lt_dst_tail_shortpositive_body_steps_bound. fs_lt_dst_tail_shortpositive_body_steps_bound + S fs_i_dst_tail_shortpositive_body_steps = k) -> exists fs_a_dst_tail_shortpositive_body_steps fs_r_dst_tail_shortpositive_body_steps fs_s_dst_tail_shortpositive_body_steps. ((((exists fs_h_dst_tail_shortpositive_body_steps_summand. fs_h_dst_tail_shortpositive_body_steps_summand + S (fs_a_dst_tail_shortpositive_body_steps) = S ((S (fs_i_dst_tail_shortpositive_body_steps)) * dst_positive_scale_tail_short)) /\ exists fs_q_dst_tail_shortpositive_body_steps_summand. dst_positive_code_tail_short = fs_q_dst_tail_shortpositive_body_steps_summand * S ((S (fs_i_dst_tail_shortpositive_body_steps)) * dst_positive_scale_tail_short) + (fs_a_dst_tail_shortpositive_body_steps))) /\ ((((exists fs_h_dst_tail_shortpositive_body_steps_partial. fs_h_dst_tail_shortpositive_body_steps_partial + S (fs_r_dst_tail_shortpositive_body_steps) = S ((S (fs_i_dst_tail_shortpositive_body_steps)) * fs_v_dst_tail_shortpositive)) /\ exists fs_q_dst_tail_shortpositive_body_steps_partial. fs_u_dst_tail_shortpositive = fs_q_dst_tail_shortpositive_body_steps_partial * S ((S (fs_i_dst_tail_shortpositive_body_steps)) * fs_v_dst_tail_shortpositive) + (fs_r_dst_tail_shortpositive_body_steps))) /\ ((((exists fs_h_dst_tail_shortpositive_body_steps_successor. fs_h_dst_tail_shortpositive_body_steps_successor + S (fs_s_dst_tail_shortpositive_body_steps) = S ((S (S fs_i_dst_tail_shortpositive_body_steps)) * fs_v_dst_tail_shortpositive)) /\ exists fs_q_dst_tail_shortpositive_body_steps_successor. fs_u_dst_tail_shortpositive = fs_q_dst_tail_shortpositive_body_steps_successor * S ((S (S fs_i_dst_tail_shortpositive_body_steps)) * fs_v_dst_tail_shortpositive) + (fs_s_dst_tail_shortpositive_body_steps))) /\ fs_s_dst_tail_shortpositive_body_steps = fs_r_dst_tail_shortpositive_body_steps + fs_a_dst_tail_shortpositive_body_steps)))))) /\ (((exists fs_u_dst_tail_shortnegative fs_v_dst_tail_shortnegative. ((((exists fs_h_dst_tail_shortnegative_body_start. fs_h_dst_tail_shortnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_tail_shortnegative)) /\ exists fs_q_dst_tail_shortnegative_body_start. fs_u_dst_tail_shortnegative = fs_q_dst_tail_shortnegative_body_start * S ((S (0)) * fs_v_dst_tail_shortnegative) + (0))) /\ ((((exists fs_h_dst_tail_shortnegative_body_terminal. fs_h_dst_tail_shortnegative_body_terminal + S (dst_negative_sum_tail_short) = S ((S (k)) * fs_v_dst_tail_shortnegative)) /\ exists fs_q_dst_tail_shortnegative_body_terminal. fs_u_dst_tail_shortnegative = fs_q_dst_tail_shortnegative_body_terminal * S ((S (k)) * fs_v_dst_tail_shortnegative) + (dst_negative_sum_tail_short))) /\ forall fs_i_dst_tail_shortnegative_body_steps. (exists fs_lt_dst_tail_shortnegative_body_steps_bound. fs_lt_dst_tail_shortnegative_body_steps_bound + S fs_i_dst_tail_shortnegative_body_steps = k) -> exists fs_a_dst_tail_shortnegative_body_steps fs_r_dst_tail_shortnegative_body_steps fs_s_dst_tail_shortnegative_body_steps. ((((exists fs_h_dst_tail_shortnegative_body_steps_summand. fs_h_dst_tail_shortnegative_body_steps_summand + S (fs_a_dst_tail_shortnegative_body_steps) = S ((S (fs_i_dst_tail_shortnegative_body_steps)) * dst_negative_scale_tail_short)) /\ exists fs_q_dst_tail_shortnegative_body_steps_summand. dst_negative_code_tail_short = fs_q_dst_tail_shortnegative_body_steps_summand * S ((S (fs_i_dst_tail_shortnegative_body_steps)) * dst_negative_scale_tail_short) + (fs_a_dst_tail_shortnegative_body_steps))) /\ ((((exists fs_h_dst_tail_shortnegative_body_steps_partial. fs_h_dst_tail_shortnegative_body_steps_partial + S (fs_r_dst_tail_shortnegative_body_steps) = S ((S (fs_i_dst_tail_shortnegative_body_steps)) * fs_v_dst_tail_shortnegative)) /\ exists fs_q_dst_tail_shortnegative_body_steps_partial. fs_u_dst_tail_shortnegative = fs_q_dst_tail_shortnegative_body_steps_partial * S ((S (fs_i_dst_tail_shortnegative_body_steps)) * fs_v_dst_tail_shortnegative) + (fs_r_dst_tail_shortnegative_body_steps))) /\ ((((exists fs_h_dst_tail_shortnegative_body_steps_successor. fs_h_dst_tail_shortnegative_body_steps_successor + S (fs_s_dst_tail_shortnegative_body_steps) = S ((S (S fs_i_dst_tail_shortnegative_body_steps)) * fs_v_dst_tail_shortnegative)) /\ exists fs_q_dst_tail_shortnegative_body_steps_successor. fs_u_dst_tail_shortnegative = fs_q_dst_tail_shortnegative_body_steps_successor * S ((S (S fs_i_dst_tail_shortnegative_body_steps)) * fs_v_dst_tail_shortnegative) + (fs_s_dst_tail_shortnegative_body_steps))) /\ fs_s_dst_tail_shortnegative_body_steps = fs_r_dst_tail_shortnegative_body_steps + fs_a_dst_tail_shortnegative_body_steps)))))) /\ (exists ge_balance_positive_tail_shortresult ge_balance_negative_tail_shortresult. (((((a) = 2 * (ge_balance_positive_tail_shortresult) /\ (ge_balance_negative_tail_shortresult) = 0) \/ exists ge_signed_half_tail_shortresultdecode. (((a) = 2 * ge_signed_half_tail_shortresultdecode + 1 /\ (ge_balance_positive_tail_shortresult) = 0) /\ (ge_balance_negative_tail_shortresult) = S ge_signed_half_tail_shortresultdecode))) /\ ((dst_positive_sum_tail_short) + ge_balance_negative_tail_shortresult = (dst_negative_sum_tail_short) + ge_balance_positive_tail_shortresult))))))))) -> (exists dst_positive_code_tail_long dst_positive_scale_tail_long dst_negative_code_tail_long dst_negative_scale_tail_long dst_positive_sum_tail_long dst_negative_sum_tail_long. (((F) = (((((dst_positive_code_tail_long) + (dst_positive_scale_tail_long)) * S ((dst_positive_code_tail_long) + (dst_positive_scale_tail_long)) + ((dst_positive_scale_tail_long) + (dst_positive_scale_tail_long))) + (((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) * S ((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) + ((dst_negative_scale_tail_long) + (dst_negative_scale_tail_long)))) * S ((((dst_positive_code_tail_long) + (dst_positive_scale_tail_long)) * S ((dst_positive_code_tail_long) + (dst_positive_scale_tail_long)) + ((dst_positive_scale_tail_long) + (dst_positive_scale_tail_long))) + (((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) * S ((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) + ((dst_negative_scale_tail_long) + (dst_negative_scale_tail_long)))) + ((((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) * S ((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) + ((dst_negative_scale_tail_long) + (dst_negative_scale_tail_long))) + (((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) * S ((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) + ((dst_negative_scale_tail_long) + (dst_negative_scale_tail_long)))))) /\ (((exists fs_u_dst_tail_longpositive fs_v_dst_tail_longpositive. ((((exists fs_h_dst_tail_longpositive_body_start. fs_h_dst_tail_longpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_tail_longpositive)) /\ exists fs_q_dst_tail_longpositive_body_start. fs_u_dst_tail_longpositive = fs_q_dst_tail_longpositive_body_start * S ((S (0)) * fs_v_dst_tail_longpositive) + (0))) /\ ((((exists fs_h_dst_tail_longpositive_body_terminal. fs_h_dst_tail_longpositive_body_terminal + S (dst_positive_sum_tail_long) = S ((S (l)) * fs_v_dst_tail_longpositive)) /\ exists fs_q_dst_tail_longpositive_body_terminal. fs_u_dst_tail_longpositive = fs_q_dst_tail_longpositive_body_terminal * S ((S (l)) * fs_v_dst_tail_longpositive) + (dst_positive_sum_tail_long))) /\ forall fs_i_dst_tail_longpositive_body_steps. (exists fs_lt_dst_tail_longpositive_body_steps_bound. fs_lt_dst_tail_longpositive_body_steps_bound + S fs_i_dst_tail_longpositive_body_steps = l) -> exists fs_a_dst_tail_longpositive_body_steps fs_r_dst_tail_longpositive_body_steps fs_s_dst_tail_longpositive_body_steps. ((((exists fs_h_dst_tail_longpositive_body_steps_summand. fs_h_dst_tail_longpositive_body_steps_summand + S (fs_a_dst_tail_longpositive_body_steps) = S ((S (fs_i_dst_tail_longpositive_body_steps)) * dst_positive_scale_tail_long)) /\ exists fs_q_dst_tail_longpositive_body_steps_summand. dst_positive_code_tail_long = fs_q_dst_tail_longpositive_body_steps_summand * S ((S (fs_i_dst_tail_longpositive_body_steps)) * dst_positive_scale_tail_long) + (fs_a_dst_tail_longpositive_body_steps))) /\ ((((exists fs_h_dst_tail_longpositive_body_steps_partial. fs_h_dst_tail_longpositive_body_steps_partial + S (fs_r_dst_tail_longpositive_body_steps) = S ((S (fs_i_dst_tail_longpositive_body_steps)) * fs_v_dst_tail_longpositive)) /\ exists fs_q_dst_tail_longpositive_body_steps_partial. fs_u_dst_tail_longpositive = fs_q_dst_tail_longpositive_body_steps_partial * S ((S (fs_i_dst_tail_longpositive_body_steps)) * fs_v_dst_tail_longpositive) + (fs_r_dst_tail_longpositive_body_steps))) /\ ((((exists fs_h_dst_tail_longpositive_body_steps_successor. fs_h_dst_tail_longpositive_body_steps_successor + S (fs_s_dst_tail_longpositive_body_steps) = S ((S (S fs_i_dst_tail_longpositive_body_steps)) * fs_v_dst_tail_longpositive)) /\ exists fs_q_dst_tail_longpositive_body_steps_successor. fs_u_dst_tail_longpositive = fs_q_dst_tail_longpositive_body_steps_successor * S ((S (S fs_i_dst_tail_longpositive_body_steps)) * fs_v_dst_tail_longpositive) + (fs_s_dst_tail_longpositive_body_steps))) /\ fs_s_dst_tail_longpositive_body_steps = fs_r_dst_tail_longpositive_body_steps + fs_a_dst_tail_longpositive_body_steps)))))) /\ (((exists fs_u_dst_tail_longnegative fs_v_dst_tail_longnegative. ((((exists fs_h_dst_tail_longnegative_body_start. fs_h_dst_tail_longnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_tail_longnegative)) /\ exists fs_q_dst_tail_longnegative_body_start. fs_u_dst_tail_longnegative = fs_q_dst_tail_longnegative_body_start * S ((S (0)) * fs_v_dst_tail_longnegative) + (0))) /\ ((((exists fs_h_dst_tail_longnegative_body_terminal. fs_h_dst_tail_longnegative_body_terminal + S (dst_negative_sum_tail_long) = S ((S (l)) * fs_v_dst_tail_longnegative)) /\ exists fs_q_dst_tail_longnegative_body_terminal. fs_u_dst_tail_longnegative = fs_q_dst_tail_longnegative_body_terminal * S ((S (l)) * fs_v_dst_tail_longnegative) + (dst_negative_sum_tail_long))) /\ forall fs_i_dst_tail_longnegative_body_steps. (exists fs_lt_dst_tail_longnegative_body_steps_bound. fs_lt_dst_tail_longnegative_body_steps_bound + S fs_i_dst_tail_longnegative_body_steps = l) -> exists fs_a_dst_tail_longnegative_body_steps fs_r_dst_tail_longnegative_body_steps fs_s_dst_tail_longnegative_body_steps. ((((exists fs_h_dst_tail_longnegative_body_steps_summand. fs_h_dst_tail_longnegative_body_steps_summand + S (fs_a_dst_tail_longnegative_body_steps) = S ((S (fs_i_dst_tail_longnegative_body_steps)) * dst_negative_scale_tail_long)) /\ exists fs_q_dst_tail_longnegative_body_steps_summand. dst_negative_code_tail_long = fs_q_dst_tail_longnegative_body_steps_summand * S ((S (fs_i_dst_tail_longnegative_body_steps)) * dst_negative_scale_tail_long) + (fs_a_dst_tail_longnegative_body_steps))) /\ ((((exists fs_h_dst_tail_longnegative_body_steps_partial. fs_h_dst_tail_longnegative_body_steps_partial + S (fs_r_dst_tail_longnegative_body_steps) = S ((S (fs_i_dst_tail_longnegative_body_steps)) * fs_v_dst_tail_longnegative)) /\ exists fs_q_dst_tail_longnegative_body_steps_partial. fs_u_dst_tail_longnegative = fs_q_dst_tail_longnegative_body_steps_partial * S ((S (fs_i_dst_tail_longnegative_body_steps)) * fs_v_dst_tail_longnegative) + (fs_r_dst_tail_longnegative_body_steps))) /\ ((((exists fs_h_dst_tail_longnegative_body_steps_successor. fs_h_dst_tail_longnegative_body_steps_successor + S (fs_s_dst_tail_longnegative_body_steps) = S ((S (S fs_i_dst_tail_longnegative_body_steps)) * fs_v_dst_tail_longnegative)) /\ exists fs_q_dst_tail_longnegative_body_steps_successor. fs_u_dst_tail_longnegative = fs_q_dst_tail_longnegative_body_steps_successor * S ((S (S fs_i_dst_tail_longnegative_body_steps)) * fs_v_dst_tail_longnegative) + (fs_s_dst_tail_longnegative_body_steps))) /\ fs_s_dst_tail_longnegative_body_steps = fs_r_dst_tail_longnegative_body_steps + fs_a_dst_tail_longnegative_body_steps)))))) /\ (exists ge_balance_positive_tail_longresult ge_balance_negative_tail_longresult. (((((b) = 2 * (ge_balance_positive_tail_longresult) /\ (ge_balance_negative_tail_longresult) = 0) \/ exists ge_signed_half_tail_longresultdecode. (((b) = 2 * ge_signed_half_tail_longresultdecode + 1 /\ (ge_balance_positive_tail_longresult) = 0) /\ (ge_balance_negative_tail_longresult) = S ge_signed_half_tail_longresultdecode))) /\ ((dst_positive_sum_tail_long) + ge_balance_negative_tail_longresult = (dst_negative_sum_tail_long) + ge_balance_positive_tail_longresult))))))))) -> a=b

signed_table_domain_resize · checked inherited prerequisite

Exact statement in the checked dependency cone

forall N M F. (exists dst_positive_code_resize_input dst_positive_scale_resize_input dst_negative_code_resize_input dst_negative_scale_resize_input. (((F) = (((((dst_positive_code_resize_input) + (dst_positive_scale_resize_input)) * S ((dst_positive_code_resize_input) + (dst_positive_scale_resize_input)) + ((dst_positive_scale_resize_input) + (dst_positive_scale_resize_input))) + (((dst_negative_code_resize_input) + (dst_negative_scale_resize_input)) * S ((dst_negative_code_resize_input) + (dst_negative_scale_resize_input)) + ((dst_negative_scale_resize_input) + (dst_negative_scale_resize_input)))) * S ((((dst_positive_code_resize_input) + (dst_positive_scale_resize_input)) * S ((dst_positive_code_resize_input) + (dst_positive_scale_resize_input)) + ((dst_positive_scale_resize_input) + (dst_positive_scale_resize_input))) + (((dst_negative_code_resize_input) + (dst_negative_scale_resize_input)) * S ((dst_negative_code_resize_input) + (dst_negative_scale_resize_input)) + ((dst_negative_scale_resize_input) + (dst_negative_scale_resize_input)))) + ((((dst_negative_code_resize_input) + (dst_negative_scale_resize_input)) * S ((dst_negative_code_resize_input) + (dst_negative_scale_resize_input)) + ((dst_negative_scale_resize_input) + (dst_negative_scale_resize_input))) + (((dst_negative_code_resize_input) + (dst_negative_scale_resize_input)) * S ((dst_negative_code_resize_input) + (dst_negative_scale_resize_input)) + ((dst_negative_scale_resize_input) + (dst_negative_scale_resize_input)))))) /\ (forall dst_index_resize_input. (exists pvs_le_gap_resize_inputdomain. pvs_le_gap_resize_inputdomain + (dst_index_resize_input) = (N)) -> exists dst_positive_resize_input dst_negative_resize_input dst_value_resize_input. ((((exists ff_h_pvs_resize_inputentrypositive. ff_h_pvs_resize_inputentrypositive + S (dst_positive_resize_input) = S ((S (dst_index_resize_input)) * dst_positive_scale_resize_input)) /\ exists ff_q_pvs_resize_inputentrypositive. dst_positive_code_resize_input = ff_q_pvs_resize_inputentrypositive * S ((S (dst_index_resize_input)) * dst_positive_scale_resize_input) + (dst_positive_resize_input))) /\ (((((exists ff_h_pvs_resize_inputentrynegative. ff_h_pvs_resize_inputentrynegative + S (dst_negative_resize_input) = S ((S (dst_index_resize_input)) * dst_negative_scale_resize_input)) /\ exists ff_q_pvs_resize_inputentrynegative. dst_negative_code_resize_input = ff_q_pvs_resize_inputentrynegative * S ((S (dst_index_resize_input)) * dst_negative_scale_resize_input) + (dst_negative_resize_input))) /\ (exists ge_balance_positive_resize_inputentryvalue ge_balance_negative_resize_inputentryvalue. (((((dst_value_resize_input) = 2 * (ge_balance_positive_resize_inputentryvalue) /\ (ge_balance_negative_resize_inputentryvalue) = 0) \/ exists ge_signed_half_resize_inputentryvaluedecode. (((dst_value_resize_input) = 2 * ge_signed_half_resize_inputentryvaluedecode + 1 /\ (ge_balance_positive_resize_inputentryvalue) = 0) /\ (ge_balance_negative_resize_inputentryvalue) = S ge_signed_half_resize_inputentryvaluedecode))) /\ ((dst_positive_resize_input) + ge_balance_negative_resize_inputentryvalue = (dst_negative_resize_input) + ge_balance_positive_resize_inputentryvalue))))))))) -> (exists dst_positive_code_resize_output dst_positive_scale_resize_output dst_negative_code_resize_output dst_negative_scale_resize_output. (((F) = (((((dst_positive_code_resize_output) + (dst_positive_scale_resize_output)) * S ((dst_positive_code_resize_output) + (dst_positive_scale_resize_output)) + ((dst_positive_scale_resize_output) + (dst_positive_scale_resize_output))) + (((dst_negative_code_resize_output) + (dst_negative_scale_resize_output)) * S ((dst_negative_code_resize_output) + (dst_negative_scale_resize_output)) + ((dst_negative_scale_resize_output) + (dst_negative_scale_resize_output)))) * S ((((dst_positive_code_resize_output) + (dst_positive_scale_resize_output)) * S ((dst_positive_code_resize_output) + (dst_positive_scale_resize_output)) + ((dst_positive_scale_resize_output) + (dst_positive_scale_resize_output))) + (((dst_negative_code_resize_output) + (dst_negative_scale_resize_output)) * S ((dst_negative_code_resize_output) + (dst_negative_scale_resize_output)) + ((dst_negative_scale_resize_output) + (dst_negative_scale_resize_output)))) + ((((dst_negative_code_resize_output) + (dst_negative_scale_resize_output)) * S ((dst_negative_code_resize_output) + (dst_negative_scale_resize_output)) + ((dst_negative_scale_resize_output) + (dst_negative_scale_resize_output))) + (((dst_negative_code_resize_output) + (dst_negative_scale_resize_output)) * S ((dst_negative_code_resize_output) + (dst_negative_scale_resize_output)) + ((dst_negative_scale_resize_output) + (dst_negative_scale_resize_output)))))) /\ (forall dst_index_resize_output. (exists pvs_le_gap_resize_outputdomain. pvs_le_gap_resize_outputdomain + (dst_index_resize_output) = (M)) -> exists dst_positive_resize_output dst_negative_resize_output dst_value_resize_output. ((((exists ff_h_pvs_resize_outputentrypositive. ff_h_pvs_resize_outputentrypositive + S (dst_positive_resize_output) = S ((S (dst_index_resize_output)) * dst_positive_scale_resize_output)) /\ exists ff_q_pvs_resize_outputentrypositive. dst_positive_code_resize_output = ff_q_pvs_resize_outputentrypositive * S ((S (dst_index_resize_output)) * dst_positive_scale_resize_output) + (dst_positive_resize_output))) /\ (((((exists ff_h_pvs_resize_outputentrynegative. ff_h_pvs_resize_outputentrynegative + S (dst_negative_resize_output) = S ((S (dst_index_resize_output)) * dst_negative_scale_resize_output)) /\ exists ff_q_pvs_resize_outputentrynegative. dst_negative_code_resize_output = ff_q_pvs_resize_outputentrynegative * S ((S (dst_index_resize_output)) * dst_negative_scale_resize_output) + (dst_negative_resize_output))) /\ (exists ge_balance_positive_resize_outputentryvalue ge_balance_negative_resize_outputentryvalue. (((((dst_value_resize_output) = 2 * (ge_balance_positive_resize_outputentryvalue) /\ (ge_balance_negative_resize_outputentryvalue) = 0) \/ exists ge_signed_half_resize_outputentryvaluedecode. (((dst_value_resize_output) = 2 * ge_signed_half_resize_outputentryvaluedecode + 1 /\ (ge_balance_positive_resize_outputentryvalue) = 0) /\ (ge_balance_negative_resize_outputentryvalue) = S ge_signed_half_resize_outputentryvaluedecode))) /\ ((dst_positive_resize_output) + ge_balance_negative_resize_outputentryvalue = (dst_negative_resize_output) + ge_balance_positive_resize_outputentryvalue)))))))))

signed_table_lookup_any · checked inherited prerequisite

Exact statement in the checked dependency cone

forall N F i. (exists dst_positive_code_any_lookup_table dst_positive_scale_any_lookup_table dst_negative_code_any_lookup_table dst_negative_scale_any_lookup_table. (((F) = (((((dst_positive_code_any_lookup_table) + (dst_positive_scale_any_lookup_table)) * S ((dst_positive_code_any_lookup_table) + (dst_positive_scale_any_lookup_table)) + ((dst_positive_scale_any_lookup_table) + (dst_positive_scale_any_lookup_table))) + (((dst_negative_code_any_lookup_table) + (dst_negative_scale_any_lookup_table)) * S ((dst_negative_code_any_lookup_table) + (dst_negative_scale_any_lookup_table)) + ((dst_negative_scale_any_lookup_table) + (dst_negative_scale_any_lookup_table)))) * S ((((dst_positive_code_any_lookup_table) + (dst_positive_scale_any_lookup_table)) * S ((dst_positive_code_any_lookup_table) + (dst_positive_scale_any_lookup_table)) + ((dst_positive_scale_any_lookup_table) + (dst_positive_scale_any_lookup_table))) + (((dst_negative_code_any_lookup_table) + (dst_negative_scale_any_lookup_table)) * S ((dst_negative_code_any_lookup_table) + (dst_negative_scale_any_lookup_table)) + ((dst_negative_scale_any_lookup_table) + (dst_negative_scale_any_lookup_table)))) + ((((dst_negative_code_any_lookup_table) + (dst_negative_scale_any_lookup_table)) * S ((dst_negative_code_any_lookup_table) + (dst_negative_scale_any_lookup_table)) + ((dst_negative_scale_any_lookup_table) + (dst_negative_scale_any_lookup_table))) + (((dst_negative_code_any_lookup_table) + (dst_negative_scale_any_lookup_table)) * S ((dst_negative_code_any_lookup_table) + (dst_negative_scale_any_lookup_table)) + ((dst_negative_scale_any_lookup_table) + (dst_negative_scale_any_lookup_table)))))) /\ (forall dst_index_any_lookup_table. (exists pvs_le_gap_any_lookup_tabledomain. pvs_le_gap_any_lookup_tabledomain + (dst_index_any_lookup_table) = (N)) -> exists dst_positive_any_lookup_table dst_negative_any_lookup_table dst_value_any_lookup_table. ((((exists ff_h_pvs_any_lookup_tableentrypositive. ff_h_pvs_any_lookup_tableentrypositive + S (dst_positive_any_lookup_table) = S ((S (dst_index_any_lookup_table)) * dst_positive_scale_any_lookup_table)) /\ exists ff_q_pvs_any_lookup_tableentrypositive. dst_positive_code_any_lookup_table = ff_q_pvs_any_lookup_tableentrypositive * S ((S (dst_index_any_lookup_table)) * dst_positive_scale_any_lookup_table) + (dst_positive_any_lookup_table))) /\ (((((exists ff_h_pvs_any_lookup_tableentrynegative. ff_h_pvs_any_lookup_tableentrynegative + S (dst_negative_any_lookup_table) = S ((S (dst_index_any_lookup_table)) * dst_negative_scale_any_lookup_table)) /\ exists ff_q_pvs_any_lookup_tableentrynegative. dst_negative_code_any_lookup_table = ff_q_pvs_any_lookup_tableentrynegative * S ((S (dst_index_any_lookup_table)) * dst_negative_scale_any_lookup_table) + (dst_negative_any_lookup_table))) /\ (exists ge_balance_positive_any_lookup_tableentryvalue ge_balance_negative_any_lookup_tableentryvalue. (((((dst_value_any_lookup_table) = 2 * (ge_balance_positive_any_lookup_tableentryvalue) /\ (ge_balance_negative_any_lookup_tableentryvalue) = 0) \/ exists ge_signed_half_any_lookup_tableentryvaluedecode. (((dst_value_any_lookup_table) = 2 * ge_signed_half_any_lookup_tableentryvaluedecode + 1 /\ (ge_balance_positive_any_lookup_tableentryvalue) = 0) /\ (ge_balance_negative_any_lookup_tableentryvalue) = S ge_signed_half_any_lookup_tableentryvaluedecode))) /\ ((dst_positive_any_lookup_table) + ge_balance_negative_any_lookup_tableentryvalue = (dst_negative_any_lookup_table) + ge_balance_positive_any_lookup_tableentryvalue))))))))) -> exists z. (exists dst_positive_code_any_lookup_result dst_positive_scale_any_lookup_result dst_negative_code_any_lookup_result dst_negative_scale_any_lookup_result dst_positive_any_lookup_result dst_negative_any_lookup_result. (((F) = (((((dst_positive_code_any_lookup_result) + (dst_positive_scale_any_lookup_result)) * S ((dst_positive_code_any_lookup_result) + (dst_positive_scale_any_lookup_result)) + ((dst_positive_scale_any_lookup_result) + (dst_positive_scale_any_lookup_result))) + (((dst_negative_code_any_lookup_result) + (dst_negative_scale_any_lookup_result)) * S ((dst_negative_code_any_lookup_result) + (dst_negative_scale_any_lookup_result)) + ((dst_negative_scale_any_lookup_result) + (dst_negative_scale_any_lookup_result)))) * S ((((dst_positive_code_any_lookup_result) + (dst_positive_scale_any_lookup_result)) * S ((dst_positive_code_any_lookup_result) + (dst_positive_scale_any_lookup_result)) + ((dst_positive_scale_any_lookup_result) + (dst_positive_scale_any_lookup_result))) + (((dst_negative_code_any_lookup_result) + (dst_negative_scale_any_lookup_result)) * S ((dst_negative_code_any_lookup_result) + (dst_negative_scale_any_lookup_result)) + ((dst_negative_scale_any_lookup_result) + (dst_negative_scale_any_lookup_result)))) + ((((dst_negative_code_any_lookup_result) + (dst_negative_scale_any_lookup_result)) * S ((dst_negative_code_any_lookup_result) + (dst_negative_scale_any_lookup_result)) + ((dst_negative_scale_any_lookup_result) + (dst_negative_scale_any_lookup_result))) + (((dst_negative_code_any_lookup_result) + (dst_negative_scale_any_lookup_result)) * S ((dst_negative_code_any_lookup_result) + (dst_negative_scale_any_lookup_result)) + ((dst_negative_scale_any_lookup_result) + (dst_negative_scale_any_lookup_result)))))) /\ (((((exists ff_h_pvs_any_lookup_resultpositive. ff_h_pvs_any_lookup_resultpositive + S (dst_positive_any_lookup_result) = S ((S (i)) * dst_positive_scale_any_lookup_result)) /\ exists ff_q_pvs_any_lookup_resultpositive. dst_positive_code_any_lookup_result = ff_q_pvs_any_lookup_resultpositive * S ((S (i)) * dst_positive_scale_any_lookup_result) + (dst_positive_any_lookup_result))) /\ (((((exists ff_h_pvs_any_lookup_resultnegative. ff_h_pvs_any_lookup_resultnegative + S (dst_negative_any_lookup_result) = S ((S (i)) * dst_negative_scale_any_lookup_result)) /\ exists ff_q_pvs_any_lookup_resultnegative. dst_negative_code_any_lookup_result = ff_q_pvs_any_lookup_resultnegative * S ((S (i)) * dst_negative_scale_any_lookup_result) + (dst_negative_any_lookup_result))) /\ (exists ge_balance_positive_any_lookup_resultvalue ge_balance_negative_any_lookup_resultvalue. (((((z) = 2 * (ge_balance_positive_any_lookup_resultvalue) /\ (ge_balance_negative_any_lookup_resultvalue) = 0) \/ exists ge_signed_half_any_lookup_resultvaluedecode. (((z) = 2 * ge_signed_half_any_lookup_resultvaluedecode + 1 /\ (ge_balance_positive_any_lookup_resultvalue) = 0) /\ (ge_balance_negative_any_lookup_resultvalue) = S ge_signed_half_any_lookup_resultvaluedecode))) /\ ((dst_positive_any_lookup_result) + ge_balance_negative_any_lookup_resultvalue = (dst_negative_any_lookup_result) + ge_balance_positive_any_lookup_resultvalue)))))))))

succ_le_succ · checked inherited prerequisite
Exact statement in the checked dependency cone
```
forall a b. (exists k. k + a = b) -> exists r. r + S a = S b
```