Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Signed one is code 2. Positive-only table graphs preserve arbitrary zeroth values, including N=0. The unit and divisor-sum identities are proved, never embedded in definitions. The separate inverse family proves the general unit-at-one criterion; multiplicative-function closure remains open.
Exact theorem in conservative defined notation
∀ N. ∀ F. ∀ w. ArithTable(N,F) → ∃ x. ConstantOneTable(N,x) ∧ (ArithAt(x,0,w) ∧ (∀ y. ∀ z. ¬y = 0 → Le(y,N) → (DirichletSum(F,x,y,z) → DivisorSum(F,y,z)) ∧ (DivisorSum(F,y,z) → DirichletSum(F,x,y,z))))Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall N F w. (exists dst_positive_code_ones_exists_input dst_positive_scale_ones_exists_input dst_negative_code_ones_exists_input dst_negative_scale_ones_exists_input. (((F) = (((((dst_positive_code_ones_exists_input) + (dst_positive_scale_ones_exists_input)) * S ((dst_positive_code_ones_exists_input) + (dst_positive_scale_ones_exists_input)) + ((dst_positive_scale_ones_exists_input) + (dst_positive_scale_ones_exists_input))) + (((dst_negative_code_ones_exists_input) + (dst_negative_scale_ones_exists_input)) * S ((dst_negative_code_ones_exists_input) + (dst_negative_scale_ones_exists_input)) + ((dst_negative_scale_ones_exists_input) + (dst_negative_scale_ones_exists_input)))) * S ((((dst_positive_code_ones_exists_input) + (dst_positive_scale_ones_exists_input)) * S ((dst_positive_code_ones_exists_input) + (dst_positive_scale_ones_exists_input)) + ((dst_positive_scale_ones_exists_input) + (dst_positive_scale_ones_exists_input))) + (((dst_negative_code_ones_exists_input) + (dst_negative_scale_ones_exists_input)) * S ((dst_negative_code_ones_exists_input) + (dst_negative_scale_ones_exists_input)) + ((dst_negative_scale_ones_exists_input) + (dst_negative_scale_ones_exists_input)))) + ((((dst_negative_code_ones_exists_input) + (dst_negative_scale_ones_exists_input)) * S ((dst_negative_code_ones_exists_input) + (dst_negative_scale_ones_exists_input)) + ((dst_negative_scale_ones_exists_input) + (dst_negative_scale_ones_exists_input))) + (((dst_negative_code_ones_exists_input) + (dst_negative_scale_ones_exists_input)) * S ((dst_negative_code_ones_exists_input) + (dst_negative_scale_ones_exists_input)) + ((dst_negative_scale_ones_exists_input) + (dst_negative_scale_ones_exists_input)))))) /\ (forall dst_index_ones_exists_input. (exists pvs_le_gap_ones_exists_inputdomain. pvs_le_gap_ones_exists_inputdomain + (dst_index_ones_exists_input) = (N)) -> exists dst_positive_ones_exists_input dst_negative_ones_exists_input dst_value_ones_exists_input. ((((exists ff_h_pvs_ones_exists_inputentrypositive. ff_h_pvs_ones_exists_inputentrypositive + S (dst_positive_ones_exists_input) = S ((S (dst_index_ones_exists_input)) * dst_positive_scale_ones_exists_input)) /\ exists ff_q_pvs_ones_exists_inputentrypositive. dst_positive_code_ones_exists_input = ff_q_pvs_ones_exists_inputentrypositive * S ((S (dst_index_ones_exists_input)) * dst_positive_scale_ones_exists_input) + (dst_positive_ones_exists_input))) /\ (((((exists ff_h_pvs_ones_exists_inputentrynegative. ff_h_pvs_ones_exists_inputentrynegative + S (dst_negative_ones_exists_input) = S ((S (dst_index_ones_exists_input)) * dst_negative_scale_ones_exists_input)) /\ exists ff_q_pvs_ones_exists_inputentrynegative. dst_negative_code_ones_exists_input = ff_q_pvs_ones_exists_inputentrynegative * S ((S (dst_index_ones_exists_input)) * dst_negative_scale_ones_exists_input) + (dst_negative_ones_exists_input))) /\ (exists ge_balance_positive_ones_exists_inputentryvalue ge_balance_negative_ones_exists_inputentryvalue. (((((dst_value_ones_exists_input) = 2 * (ge_balance_positive_ones_exists_inputentryvalue) /\ (ge_balance_negative_ones_exists_inputentryvalue) = 0) \/ exists ge_signed_half_ones_exists_inputentryvaluedecode. (((dst_value_ones_exists_input) = 2 * ge_signed_half_ones_exists_inputentryvaluedecode + 1 /\ (ge_balance_positive_ones_exists_inputentryvalue) = 0) /\ (ge_balance_negative_ones_exists_inputentryvalue) = S ge_signed_half_ones_exists_inputentryvaluedecode))) /\ ((dst_positive_ones_exists_input) + ge_balance_negative_ones_exists_inputentryvalue = (dst_negative_ones_exists_input) + ge_balance_positive_ones_exists_inputentryvalue))))))))) -> exists U. ((((exists dst_positive_code_ones_exists_resulttable dst_positive_scale_ones_exists_resulttable dst_negative_code_ones_exists_resulttable dst_negative_scale_ones_exists_resulttable. (((U) = (((((dst_positive_code_ones_exists_resulttable) + (dst_positive_scale_ones_exists_resulttable)) * S ((dst_positive_code_ones_exists_resulttable) + (dst_positive_scale_ones_exists_resulttable)) + ((dst_positive_scale_ones_exists_resulttable) + (dst_positive_scale_ones_exists_resulttable))) + (((dst_negative_code_ones_exists_resulttable) + (dst_negative_scale_ones_exists_resulttable)) * S ((dst_negative_code_ones_exists_resulttable) + (dst_negative_scale_ones_exists_resulttable)) + ((dst_negative_scale_ones_exists_resulttable) + (dst_negative_scale_ones_exists_resulttable)))) * S ((((dst_positive_code_ones_exists_resulttable) + (dst_positive_scale_ones_exists_resulttable)) * S ((dst_positive_code_ones_exists_resulttable) + (dst_positive_scale_ones_exists_resulttable)) + ((dst_positive_scale_ones_exists_resulttable) + (dst_positive_scale_ones_exists_resulttable))) + (((dst_negative_code_ones_exists_resulttable) + (dst_negative_scale_ones_exists_resulttable)) * S ((dst_negative_code_ones_exists_resulttable) + (dst_negative_scale_ones_exists_resulttable)) + ((dst_negative_scale_ones_exists_resulttable) + (dst_negative_scale_ones_exists_resulttable)))) + ((((dst_negative_code_ones_exists_resulttable) + (dst_negative_scale_ones_exists_resulttable)) * S ((dst_negative_code_ones_exists_resulttable) + (dst_negative_scale_ones_exists_resulttable)) + ((dst_negative_scale_ones_exists_resulttable) + (dst_negative_scale_ones_exists_resulttable))) + (((dst_negative_code_ones_exists_resulttable) + (dst_negative_scale_ones_exists_resulttable)) * S ((dst_negative_code_ones_exists_resulttable) + (dst_negative_scale_ones_exists_resulttable)) + ((dst_negative_scale_ones_exists_resulttable) + (dst_negative_scale_ones_exists_resulttable)))))) /\ (forall dst_index_ones_exists_resulttable. (exists pvs_le_gap_ones_exists_resulttabledomain. pvs_le_gap_ones_exists_resulttabledomain + (dst_index_ones_exists_resulttable) = (N)) -> exists dst_positive_ones_exists_resulttable dst_negative_ones_exists_resulttable dst_value_ones_exists_resulttable. ((((exists ff_h_pvs_ones_exists_resulttableentrypositive. ff_h_pvs_ones_exists_resulttableentrypositive + S (dst_positive_ones_exists_resulttable) = S ((S (dst_index_ones_exists_resulttable)) * dst_positive_scale_ones_exists_resulttable)) /\ exists ff_q_pvs_ones_exists_resulttableentrypositive. dst_positive_code_ones_exists_resulttable = ff_q_pvs_ones_exists_resulttableentrypositive * S ((S (dst_index_ones_exists_resulttable)) * dst_positive_scale_ones_exists_resulttable) + (dst_positive_ones_exists_resulttable))) /\ (((((exists ff_h_pvs_ones_exists_resulttableentrynegative. ff_h_pvs_ones_exists_resulttableentrynegative + S (dst_negative_ones_exists_resulttable) = S ((S (dst_index_ones_exists_resulttable)) * dst_negative_scale_ones_exists_resulttable)) /\ exists ff_q_pvs_ones_exists_resulttableentrynegative. dst_negative_code_ones_exists_resulttable = ff_q_pvs_ones_exists_resulttableentrynegative * S ((S (dst_index_ones_exists_resulttable)) * dst_negative_scale_ones_exists_resulttable) + (dst_negative_ones_exists_resulttable))) /\ (exists ge_balance_positive_ones_exists_resulttableentryvalue ge_balance_negative_ones_exists_resulttableentryvalue. (((((dst_value_ones_exists_resulttable) = 2 * (ge_balance_positive_ones_exists_resulttableentryvalue) /\ (ge_balance_negative_ones_exists_resulttableentryvalue) = 0) \/ exists ge_signed_half_ones_exists_resulttableentryvaluedecode. (((dst_value_ones_exists_resulttable) = 2 * ge_signed_half_ones_exists_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_ones_exists_resulttableentryvalue) = 0) /\ (ge_balance_negative_ones_exists_resulttableentryvalue) = S ge_signed_half_ones_exists_resulttableentryvaluedecode))) /\ ((dst_positive_ones_exists_resulttable) + ge_balance_negative_ones_exists_resulttableentryvalue = (dst_negative_ones_exists_resulttable) + ge_balance_positive_ones_exists_resulttableentryvalue))))))))) /\ (forall du_index_ones_exists_result du_value_ones_exists_result. ~(du_index_ones_exists_result=0) -> (exists pvs_le_gap_ones_exists_resultbound. pvs_le_gap_ones_exists_resultbound + (du_index_ones_exists_result) = (N)) -> (exists dst_positive_code_ones_exists_resultentry dst_positive_scale_ones_exists_resultentry dst_negative_code_ones_exists_resultentry dst_negative_scale_ones_exists_resultentry dst_positive_ones_exists_resultentry dst_negative_ones_exists_resultentry. (((U) = (((((dst_positive_code_ones_exists_resultentry) + (dst_positive_scale_ones_exists_resultentry)) * S ((dst_positive_code_ones_exists_resultentry) + (dst_positive_scale_ones_exists_resultentry)) + ((dst_positive_scale_ones_exists_resultentry) + (dst_positive_scale_ones_exists_resultentry))) + (((dst_negative_code_ones_exists_resultentry) + (dst_negative_scale_ones_exists_resultentry)) * S ((dst_negative_code_ones_exists_resultentry) + (dst_negative_scale_ones_exists_resultentry)) + ((dst_negative_scale_ones_exists_resultentry) + (dst_negative_scale_ones_exists_resultentry)))) * S ((((dst_positive_code_ones_exists_resultentry) + (dst_positive_scale_ones_exists_resultentry)) * S ((dst_positive_code_ones_exists_resultentry) + (dst_positive_scale_ones_exists_resultentry)) + ((dst_positive_scale_ones_exists_resultentry) + (dst_positive_scale_ones_exists_resultentry))) + (((dst_negative_code_ones_exists_resultentry) + (dst_negative_scale_ones_exists_resultentry)) * S ((dst_negative_code_ones_exists_resultentry) + (dst_negative_scale_ones_exists_resultentry)) + ((dst_negative_scale_ones_exists_resultentry) + (dst_negative_scale_ones_exists_resultentry)))) + ((((dst_negative_code_ones_exists_resultentry) + (dst_negative_scale_ones_exists_resultentry)) * S ((dst_negative_code_ones_exists_resultentry) + (dst_negative_scale_ones_exists_resultentry)) + ((dst_negative_scale_ones_exists_resultentry) + (dst_negative_scale_ones_exists_resultentry))) + (((dst_negative_code_ones_exists_resultentry) + (dst_negative_scale_ones_exists_resultentry)) * S ((dst_negative_code_ones_exists_resultentry) + (dst_negative_scale_ones_exists_resultentry)) + ((dst_negative_scale_ones_exists_resultentry) + (dst_negative_scale_ones_exists_resultentry)))))) /\ (((((exists ff_h_pvs_ones_exists_resultentrypositive. ff_h_pvs_ones_exists_resultentrypositive + S (dst_positive_ones_exists_resultentry) = S ((S (du_index_ones_exists_result)) * dst_positive_scale_ones_exists_resultentry)) /\ exists ff_q_pvs_ones_exists_resultentrypositive. dst_positive_code_ones_exists_resultentry = ff_q_pvs_ones_exists_resultentrypositive * S ((S (du_index_ones_exists_result)) * dst_positive_scale_ones_exists_resultentry) + (dst_positive_ones_exists_resultentry))) /\ (((((exists ff_h_pvs_ones_exists_resultentrynegative. ff_h_pvs_ones_exists_resultentrynegative + S (dst_negative_ones_exists_resultentry) = S ((S (du_index_ones_exists_result)) * dst_negative_scale_ones_exists_resultentry)) /\ exists ff_q_pvs_ones_exists_resultentrynegative. dst_negative_code_ones_exists_resultentry = ff_q_pvs_ones_exists_resultentrynegative * S ((S (du_index_ones_exists_result)) * dst_negative_scale_ones_exists_resultentry) + (dst_negative_ones_exists_resultentry))) /\ (exists ge_balance_positive_ones_exists_resultentryvalue ge_balance_negative_ones_exists_resultentryvalue. (((((du_value_ones_exists_result) = 2 * (ge_balance_positive_ones_exists_resultentryvalue) /\ (ge_balance_negative_ones_exists_resultentryvalue) = 0) \/ exists ge_signed_half_ones_exists_resultentryvaluedecode. (((du_value_ones_exists_result) = 2 * ge_signed_half_ones_exists_resultentryvaluedecode + 1 /\ (ge_balance_positive_ones_exists_resultentryvalue) = 0) /\ (ge_balance_negative_ones_exists_resultentryvalue) = S ge_signed_half_ones_exists_resultentryvaluedecode))) /\ ((dst_positive_ones_exists_resultentry) + ge_balance_negative_ones_exists_resultentryvalue = (dst_negative_ones_exists_resultentry) + ge_balance_positive_ones_exists_resultentryvalue))))))))) -> du_value_ones_exists_result=2))) /\ (((exists dst_positive_code_ones_exists_prescribed_zero dst_positive_scale_ones_exists_prescribed_zero dst_negative_code_ones_exists_prescribed_zero dst_negative_scale_ones_exists_prescribed_zero dst_positive_ones_exists_prescribed_zero dst_negative_ones_exists_prescribed_zero. (((U) = (((((dst_positive_code_ones_exists_prescribed_zero) + (dst_positive_scale_ones_exists_prescribed_zero)) * S ((dst_positive_code_ones_exists_prescribed_zero) + (dst_positive_scale_ones_exists_prescribed_zero)) + ((dst_positive_scale_ones_exists_prescribed_zero) + (dst_positive_scale_ones_exists_prescribed_zero))) + (((dst_negative_code_ones_exists_prescribed_zero) + (dst_negative_scale_ones_exists_prescribed_zero)) * S ((dst_negative_code_ones_exists_prescribed_zero) + (dst_negative_scale_ones_exists_prescribed_zero)) + ((dst_negative_scale_ones_exists_prescribed_zero) + (dst_negative_scale_ones_exists_prescribed_zero)))) * S ((((dst_positive_code_ones_exists_prescribed_zero) + (dst_positive_scale_ones_exists_prescribed_zero)) * S ((dst_positive_code_ones_exists_prescribed_zero) + (dst_positive_scale_ones_exists_prescribed_zero)) + ((dst_positive_scale_ones_exists_prescribed_zero) + (dst_positive_scale_ones_exists_prescribed_zero))) + (((dst_negative_code_ones_exists_prescribed_zero) + (dst_negative_scale_ones_exists_prescribed_zero)) * S ((dst_negative_code_ones_exists_prescribed_zero) + (dst_negative_scale_ones_exists_prescribed_zero)) + ((dst_negative_scale_ones_exists_prescribed_zero) + (dst_negative_scale_ones_exists_prescribed_zero)))) + ((((dst_negative_code_ones_exists_prescribed_zero) + (dst_negative_scale_ones_exists_prescribed_zero)) * S ((dst_negative_code_ones_exists_prescribed_zero) + (dst_negative_scale_ones_exists_prescribed_zero)) + ((dst_negative_scale_ones_exists_prescribed_zero) + (dst_negative_scale_ones_exists_prescribed_zero))) + (((dst_negative_code_ones_exists_prescribed_zero) + (dst_negative_scale_ones_exists_prescribed_zero)) * S ((dst_negative_code_ones_exists_prescribed_zero) + (dst_negative_scale_ones_exists_prescribed_zero)) + ((dst_negative_scale_ones_exists_prescribed_zero) + (dst_negative_scale_ones_exists_prescribed_zero)))))) /\ (((((exists ff_h_pvs_ones_exists_prescribed_zeropositive. ff_h_pvs_ones_exists_prescribed_zeropositive + S (dst_positive_ones_exists_prescribed_zero) = S ((S (0)) * dst_positive_scale_ones_exists_prescribed_zero)) /\ exists ff_q_pvs_ones_exists_prescribed_zeropositive. dst_positive_code_ones_exists_prescribed_zero = ff_q_pvs_ones_exists_prescribed_zeropositive * S ((S (0)) * dst_positive_scale_ones_exists_prescribed_zero) + (dst_positive_ones_exists_prescribed_zero))) /\ (((((exists ff_h_pvs_ones_exists_prescribed_zeronegative. ff_h_pvs_ones_exists_prescribed_zeronegative + S (dst_negative_ones_exists_prescribed_zero) = S ((S (0)) * dst_negative_scale_ones_exists_prescribed_zero)) /\ exists ff_q_pvs_ones_exists_prescribed_zeronegative. dst_negative_code_ones_exists_prescribed_zero = ff_q_pvs_ones_exists_prescribed_zeronegative * S ((S (0)) * dst_negative_scale_ones_exists_prescribed_zero) + (dst_negative_ones_exists_prescribed_zero))) /\ (exists ge_balance_positive_ones_exists_prescribed_zerovalue ge_balance_negative_ones_exists_prescribed_zerovalue. (((((w) = 2 * (ge_balance_positive_ones_exists_prescribed_zerovalue) /\ (ge_balance_negative_ones_exists_prescribed_zerovalue) = 0) \/ exists ge_signed_half_ones_exists_prescribed_zerovaluedecode. (((w) = 2 * ge_signed_half_ones_exists_prescribed_zerovaluedecode + 1 /\ (ge_balance_positive_ones_exists_prescribed_zerovalue) = 0) /\ (ge_balance_negative_ones_exists_prescribed_zerovalue) = S ge_signed_half_ones_exists_prescribed_zerovaluedecode))) /\ ((dst_positive_ones_exists_prescribed_zero) + ge_balance_negative_ones_exists_prescribed_zerovalue = (dst_negative_ones_exists_prescribed_zero) + ge_balance_positive_ones_exists_prescribed_zerovalue))))))))) /\ (forall n z. ~(n=0) -> (exists pvs_le_gap_ones_exists_bound. pvs_le_gap_ones_exists_bound + (n) = (N)) -> ((((((~((n)=0)) /\ (exists dc_mask_ones_exists_lawconvolution. ((((exists dst_positive_code_ones_exists_lawconvolutionmasktable dst_positive_scale_ones_exists_lawconvolutionmasktable dst_negative_code_ones_exists_lawconvolutionmasktable dst_negative_scale_ones_exists_lawconvolutionmasktable. (((dc_mask_ones_exists_lawconvolution) = (((((dst_positive_code_ones_exists_lawconvolutionmasktable) + (dst_positive_scale_ones_exists_lawconvolutionmasktable)) * S ((dst_positive_code_ones_exists_lawconvolutionmasktable) + (dst_positive_scale_ones_exists_lawconvolutionmasktable)) + ((dst_positive_scale_ones_exists_lawconvolutionmasktable) + (dst_positive_scale_ones_exists_lawconvolutionmasktable))) + (((dst_negative_code_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)) * S ((dst_negative_code_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)) + ((dst_negative_scale_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)))) * S ((((dst_positive_code_ones_exists_lawconvolutionmasktable) + (dst_positive_scale_ones_exists_lawconvolutionmasktable)) * S ((dst_positive_code_ones_exists_lawconvolutionmasktable) + (dst_positive_scale_ones_exists_lawconvolutionmasktable)) + ((dst_positive_scale_ones_exists_lawconvolutionmasktable) + (dst_positive_scale_ones_exists_lawconvolutionmasktable))) + (((dst_negative_code_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)) * S ((dst_negative_code_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)) + ((dst_negative_scale_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)))) + ((((dst_negative_code_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)) * S ((dst_negative_code_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)) + ((dst_negative_scale_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable))) + (((dst_negative_code_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)) * S ((dst_negative_code_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)) + ((dst_negative_scale_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)))))) /\ (forall dst_index_ones_exists_lawconvolutionmasktable. (exists pvs_le_gap_ones_exists_lawconvolutionmasktabledomain. pvs_le_gap_ones_exists_lawconvolutionmasktabledomain + (dst_index_ones_exists_lawconvolutionmasktable) = (n)) -> exists dst_positive_ones_exists_lawconvolutionmasktable dst_negative_ones_exists_lawconvolutionmasktable dst_value_ones_exists_lawconvolutionmasktable. ((((exists ff_h_pvs_ones_exists_lawconvolutionmasktableentrypositive. ff_h_pvs_ones_exists_lawconvolutionmasktableentrypositive + S (dst_positive_ones_exists_lawconvolutionmasktable) = S ((S (dst_index_ones_exists_lawconvolutionmasktable)) * dst_positive_scale_ones_exists_lawconvolutionmasktable)) /\ exists ff_q_pvs_ones_exists_lawconvolutionmasktableentrypositive. dst_positive_code_ones_exists_lawconvolutionmasktable = ff_q_pvs_ones_exists_lawconvolutionmasktableentrypositive * S ((S (dst_index_ones_exists_lawconvolutionmasktable)) * dst_positive_scale_ones_exists_lawconvolutionmasktable) + (dst_positive_ones_exists_lawconvolutionmasktable))) /\ (((((exists ff_h_pvs_ones_exists_lawconvolutionmasktableentrynegative. ff_h_pvs_ones_exists_lawconvolutionmasktableentrynegative + S (dst_negative_ones_exists_lawconvolutionmasktable) = S ((S (dst_index_ones_exists_lawconvolutionmasktable)) * dst_negative_scale_ones_exists_lawconvolutionmasktable)) /\ exists ff_q_pvs_ones_exists_lawconvolutionmasktableentrynegative. dst_negative_code_ones_exists_lawconvolutionmasktable = ff_q_pvs_ones_exists_lawconvolutionmasktableentrynegative * S ((S (dst_index_ones_exists_lawconvolutionmasktable)) * dst_negative_scale_ones_exists_lawconvolutionmasktable) + (dst_negative_ones_exists_lawconvolutionmasktable))) /\ (exists ge_balance_positive_ones_exists_lawconvolutionmasktableentryvalue ge_balance_negative_ones_exists_lawconvolutionmasktableentryvalue. (((((dst_value_ones_exists_lawconvolutionmasktable) = 2 * (ge_balance_positive_ones_exists_lawconvolutionmasktableentryvalue) /\ (ge_balance_negative_ones_exists_lawconvolutionmasktableentryvalue) = 0) \/ exists ge_signed_half_ones_exists_lawconvolutionmasktableentryvaluedecode. (((dst_value_ones_exists_lawconvolutionmasktable) = 2 * ge_signed_half_ones_exists_lawconvolutionmasktableentryvaluedecode + 1 /\ (ge_balance_positive_ones_exists_lawconvolutionmasktableentryvalue) = 0) /\ (ge_balance_negative_ones_exists_lawconvolutionmasktableentryvalue) = S ge_signed_half_ones_exists_lawconvolutionmasktableentryvaluedecode))) /\ ((dst_positive_ones_exists_lawconvolutionmasktable) + ge_balance_negative_ones_exists_lawconvolutionmasktableentryvalue = (dst_negative_ones_exists_lawconvolutionmasktable) + ge_balance_positive_ones_exists_lawconvolutionmasktableentryvalue))))))))) /\ (forall dc_index_ones_exists_lawconvolutionmask dc_value_ones_exists_lawconvolutionmask. (exists pvs_le_gap_ones_exists_lawconvolutionmaskdomain. pvs_le_gap_ones_exists_lawconvolutionmaskdomain + (dc_index_ones_exists_lawconvolutionmask) = (n)) -> (exists dst_positive_code_ones_exists_lawconvolutionmasklookup dst_positive_scale_ones_exists_lawconvolutionmasklookup dst_negative_code_ones_exists_lawconvolutionmasklookup dst_negative_scale_ones_exists_lawconvolutionmasklookup dst_positive_ones_exists_lawconvolutionmasklookup dst_negative_ones_exists_lawconvolutionmasklookup. (((dc_mask_ones_exists_lawconvolution) = (((((dst_positive_code_ones_exists_lawconvolutionmasklookup) + (dst_positive_scale_ones_exists_lawconvolutionmasklookup)) * S ((dst_positive_code_ones_exists_lawconvolutionmasklookup) + (dst_positive_scale_ones_exists_lawconvolutionmasklookup)) + ((dst_positive_scale_ones_exists_lawconvolutionmasklookup) + (dst_positive_scale_ones_exists_lawconvolutionmasklookup))) + (((dst_negative_code_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)) * S ((dst_negative_code_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)) + ((dst_negative_scale_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)))) * S ((((dst_positive_code_ones_exists_lawconvolutionmasklookup) + (dst_positive_scale_ones_exists_lawconvolutionmasklookup)) * S ((dst_positive_code_ones_exists_lawconvolutionmasklookup) + (dst_positive_scale_ones_exists_lawconvolutionmasklookup)) + ((dst_positive_scale_ones_exists_lawconvolutionmasklookup) + (dst_positive_scale_ones_exists_lawconvolutionmasklookup))) + (((dst_negative_code_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)) * S ((dst_negative_code_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)) + ((dst_negative_scale_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)))) + ((((dst_negative_code_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)) * S ((dst_negative_code_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)) + ((dst_negative_scale_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup))) + (((dst_negative_code_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)) * S ((dst_negative_code_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)) + ((dst_negative_scale_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)))))) /\ (((((exists ff_h_pvs_ones_exists_lawconvolutionmasklookuppositive. ff_h_pvs_ones_exists_lawconvolutionmasklookuppositive + S (dst_positive_ones_exists_lawconvolutionmasklookup) = S ((S (dc_index_ones_exists_lawconvolutionmask)) * dst_positive_scale_ones_exists_lawconvolutionmasklookup)) /\ exists ff_q_pvs_ones_exists_lawconvolutionmasklookuppositive. dst_positive_code_ones_exists_lawconvolutionmasklookup = ff_q_pvs_ones_exists_lawconvolutionmasklookuppositive * S ((S (dc_index_ones_exists_lawconvolutionmask)) * dst_positive_scale_ones_exists_lawconvolutionmasklookup) + (dst_positive_ones_exists_lawconvolutionmasklookup))) /\ (((((exists ff_h_pvs_ones_exists_lawconvolutionmasklookupnegative. ff_h_pvs_ones_exists_lawconvolutionmasklookupnegative + S (dst_negative_ones_exists_lawconvolutionmasklookup) = S ((S (dc_index_ones_exists_lawconvolutionmask)) * dst_negative_scale_ones_exists_lawconvolutionmasklookup)) /\ exists ff_q_pvs_ones_exists_lawconvolutionmasklookupnegative. dst_negative_code_ones_exists_lawconvolutionmasklookup = ff_q_pvs_ones_exists_lawconvolutionmasklookupnegative * S ((S (dc_index_ones_exists_lawconvolutionmask)) * dst_negative_scale_ones_exists_lawconvolutionmasklookup) + (dst_negative_ones_exists_lawconvolutionmasklookup))) /\ (exists ge_balance_positive_ones_exists_lawconvolutionmasklookupvalue ge_balance_negative_ones_exists_lawconvolutionmasklookupvalue. (((((dc_value_ones_exists_lawconvolutionmask) = 2 * (ge_balance_positive_ones_exists_lawconvolutionmasklookupvalue) /\ (ge_balance_negative_ones_exists_lawconvolutionmasklookupvalue) = 0) \/ exists ge_signed_half_ones_exists_lawconvolutionmasklookupvaluedecode. (((dc_value_ones_exists_lawconvolutionmask) = 2 * ge_signed_half_ones_exists_lawconvolutionmasklookupvaluedecode + 1 /\ (ge_balance_positive_ones_exists_lawconvolutionmasklookupvalue) = 0) /\ (ge_balance_negative_ones_exists_lawconvolutionmasklookupvalue) = S ge_signed_half_ones_exists_lawconvolutionmasklookupvaluedecode))) /\ ((dst_positive_ones_exists_lawconvolutionmasklookup) + ge_balance_negative_ones_exists_lawconvolutionmasklookupvalue = (dst_negative_ones_exists_lawconvolutionmasklookup) + ge_balance_positive_ones_exists_lawconvolutionmasklookupvalue))))))))) -> ((((~((dc_index_ones_exists_lawconvolutionmask)=0)) /\ (exists dc_quotient_ones_exists_lawconvolutionmaskentry dc_left_ones_exists_lawconvolutionmaskentry dc_right_ones_exists_lawconvolutionmaskentry. (((n)=(dc_index_ones_exists_lawconvolutionmask)*dc_quotient_ones_exists_lawconvolutionmaskentry) /\ (((exists dst_positive_code_ones_exists_lawconvolutionmaskentryleft dst_positive_scale_ones_exists_lawconvolutionmaskentryleft dst_negative_code_ones_exists_lawconvolutionmaskentryleft dst_negative_scale_ones_exists_lawconvolutionmaskentryleft dst_positive_ones_exists_lawconvolutionmaskentryleft dst_negative_ones_exists_lawconvolutionmaskentryleft. (((F) = (((((dst_positive_code_ones_exists_lawconvolutionmaskentryleft) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryleft)) * S ((dst_positive_code_ones_exists_lawconvolutionmaskentryleft) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryleft)) + ((dst_positive_scale_ones_exists_lawconvolutionmaskentryleft) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryleft))) + (((dst_negative_code_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)) * S ((dst_negative_code_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)) + ((dst_negative_scale_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)))) * S ((((dst_positive_code_ones_exists_lawconvolutionmaskentryleft) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryleft)) * S ((dst_positive_code_ones_exists_lawconvolutionmaskentryleft) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryleft)) + ((dst_positive_scale_ones_exists_lawconvolutionmaskentryleft) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryleft))) + (((dst_negative_code_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)) * S ((dst_negative_code_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)) + ((dst_negative_scale_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)))) + ((((dst_negative_code_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)) * S ((dst_negative_code_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)) + ((dst_negative_scale_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft))) + (((dst_negative_code_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)) * S ((dst_negative_code_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)) + ((dst_negative_scale_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)))))) /\ (((((exists ff_h_pvs_ones_exists_lawconvolutionmaskentryleftpositive. ff_h_pvs_ones_exists_lawconvolutionmaskentryleftpositive + S (dst_positive_ones_exists_lawconvolutionmaskentryleft) = S ((S (dc_index_ones_exists_lawconvolutionmask)) * dst_positive_scale_ones_exists_lawconvolutionmaskentryleft)) /\ exists ff_q_pvs_ones_exists_lawconvolutionmaskentryleftpositive. dst_positive_code_ones_exists_lawconvolutionmaskentryleft = ff_q_pvs_ones_exists_lawconvolutionmaskentryleftpositive * S ((S (dc_index_ones_exists_lawconvolutionmask)) * dst_positive_scale_ones_exists_lawconvolutionmaskentryleft) + (dst_positive_ones_exists_lawconvolutionmaskentryleft))) /\ (((((exists ff_h_pvs_ones_exists_lawconvolutionmaskentryleftnegative. ff_h_pvs_ones_exists_lawconvolutionmaskentryleftnegative + S (dst_negative_ones_exists_lawconvolutionmaskentryleft) = S ((S (dc_index_ones_exists_lawconvolutionmask)) * dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)) /\ exists ff_q_pvs_ones_exists_lawconvolutionmaskentryleftnegative. dst_negative_code_ones_exists_lawconvolutionmaskentryleft = ff_q_pvs_ones_exists_lawconvolutionmaskentryleftnegative * S ((S (dc_index_ones_exists_lawconvolutionmask)) * dst_negative_scale_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_ones_exists_lawconvolutionmaskentryleft))) /\ (exists ge_balance_positive_ones_exists_lawconvolutionmaskentryleftvalue ge_balance_negative_ones_exists_lawconvolutionmaskentryleftvalue. (((((dc_left_ones_exists_lawconvolutionmaskentry) = 2 * (ge_balance_positive_ones_exists_lawconvolutionmaskentryleftvalue) /\ (ge_balance_negative_ones_exists_lawconvolutionmaskentryleftvalue) = 0) \/ exists ge_signed_half_ones_exists_lawconvolutionmaskentryleftvaluedecode. (((dc_left_ones_exists_lawconvolutionmaskentry) = 2 * ge_signed_half_ones_exists_lawconvolutionmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_ones_exists_lawconvolutionmaskentryleftvalue) = 0) /\ (ge_balance_negative_ones_exists_lawconvolutionmaskentryleftvalue) = S ge_signed_half_ones_exists_lawconvolutionmaskentryleftvaluedecode))) /\ ((dst_positive_ones_exists_lawconvolutionmaskentryleft) + ge_balance_negative_ones_exists_lawconvolutionmaskentryleftvalue = (dst_negative_ones_exists_lawconvolutionmaskentryleft) + ge_balance_positive_ones_exists_lawconvolutionmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_ones_exists_lawconvolutionmaskentryright dst_positive_scale_ones_exists_lawconvolutionmaskentryright dst_negative_code_ones_exists_lawconvolutionmaskentryright dst_negative_scale_ones_exists_lawconvolutionmaskentryright dst_positive_ones_exists_lawconvolutionmaskentryright dst_negative_ones_exists_lawconvolutionmaskentryright. (((U) = (((((dst_positive_code_ones_exists_lawconvolutionmaskentryright) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryright)) * S ((dst_positive_code_ones_exists_lawconvolutionmaskentryright) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryright)) + ((dst_positive_scale_ones_exists_lawconvolutionmaskentryright) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryright))) + (((dst_negative_code_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)) * S ((dst_negative_code_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)) + ((dst_negative_scale_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)))) * S ((((dst_positive_code_ones_exists_lawconvolutionmaskentryright) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryright)) * S ((dst_positive_code_ones_exists_lawconvolutionmaskentryright) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryright)) + ((dst_positive_scale_ones_exists_lawconvolutionmaskentryright) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryright))) + (((dst_negative_code_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)) * S ((dst_negative_code_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)) + ((dst_negative_scale_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)))) + ((((dst_negative_code_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)) * S ((dst_negative_code_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)) + ((dst_negative_scale_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright))) + (((dst_negative_code_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)) * S ((dst_negative_code_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)) + ((dst_negative_scale_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)))))) /\ (((((exists ff_h_pvs_ones_exists_lawconvolutionmaskentryrightpositive. ff_h_pvs_ones_exists_lawconvolutionmaskentryrightpositive + S (dst_positive_ones_exists_lawconvolutionmaskentryright) = S ((S (dc_quotient_ones_exists_lawconvolutionmaskentry)) * dst_positive_scale_ones_exists_lawconvolutionmaskentryright)) /\ exists ff_q_pvs_ones_exists_lawconvolutionmaskentryrightpositive. dst_positive_code_ones_exists_lawconvolutionmaskentryright = ff_q_pvs_ones_exists_lawconvolutionmaskentryrightpositive * S ((S (dc_quotient_ones_exists_lawconvolutionmaskentry)) * dst_positive_scale_ones_exists_lawconvolutionmaskentryright) + (dst_positive_ones_exists_lawconvolutionmaskentryright))) /\ (((((exists ff_h_pvs_ones_exists_lawconvolutionmaskentryrightnegative. ff_h_pvs_ones_exists_lawconvolutionmaskentryrightnegative + S (dst_negative_ones_exists_lawconvolutionmaskentryright) = S ((S (dc_quotient_ones_exists_lawconvolutionmaskentry)) * dst_negative_scale_ones_exists_lawconvolutionmaskentryright)) /\ exists ff_q_pvs_ones_exists_lawconvolutionmaskentryrightnegative. dst_negative_code_ones_exists_lawconvolutionmaskentryright = ff_q_pvs_ones_exists_lawconvolutionmaskentryrightnegative * S ((S (dc_quotient_ones_exists_lawconvolutionmaskentry)) * dst_negative_scale_ones_exists_lawconvolutionmaskentryright) + (dst_negative_ones_exists_lawconvolutionmaskentryright))) /\ (exists ge_balance_positive_ones_exists_lawconvolutionmaskentryrightvalue ge_balance_negative_ones_exists_lawconvolutionmaskentryrightvalue. (((((dc_right_ones_exists_lawconvolutionmaskentry) = 2 * (ge_balance_positive_ones_exists_lawconvolutionmaskentryrightvalue) /\ (ge_balance_negative_ones_exists_lawconvolutionmaskentryrightvalue) = 0) \/ exists ge_signed_half_ones_exists_lawconvolutionmaskentryrightvaluedecode. (((dc_right_ones_exists_lawconvolutionmaskentry) = 2 * ge_signed_half_ones_exists_lawconvolutionmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_ones_exists_lawconvolutionmaskentryrightvalue) = 0) /\ (ge_balance_negative_ones_exists_lawconvolutionmaskentryrightvalue) = S ge_signed_half_ones_exists_lawconvolutionmaskentryrightvaluedecode))) /\ ((dst_positive_ones_exists_lawconvolutionmaskentryright) + ge_balance_negative_ones_exists_lawconvolutionmaskentryrightvalue = (dst_negative_ones_exists_lawconvolutionmaskentryright) + ge_balance_positive_ones_exists_lawconvolutionmaskentryrightvalue))))))))) /\ (exists sto_ap_ones_exists_lawconvolutionmaskentryproduct sto_an_ones_exists_lawconvolutionmaskentryproduct sto_bp_ones_exists_lawconvolutionmaskentryproduct sto_bn_ones_exists_lawconvolutionmaskentryproduct sto_cp_ones_exists_lawconvolutionmaskentryproduct sto_cn_ones_exists_lawconvolutionmaskentryproduct. (((((dc_left_ones_exists_lawconvolutionmaskentry) = 2 * (sto_ap_ones_exists_lawconvolutionmaskentryproduct) /\ (sto_an_ones_exists_lawconvolutionmaskentryproduct) = 0) \/ exists ge_signed_half_ones_exists_lawconvolutionmaskentryproductleft. (((dc_left_ones_exists_lawconvolutionmaskentry) = 2 * ge_signed_half_ones_exists_lawconvolutionmaskentryproductleft + 1 /\ (sto_ap_ones_exists_lawconvolutionmaskentryproduct) = 0) /\ (sto_an_ones_exists_lawconvolutionmaskentryproduct) = S ge_signed_half_ones_exists_lawconvolutionmaskentryproductleft))) /\ ((((((dc_right_ones_exists_lawconvolutionmaskentry) = 2 * (sto_bp_ones_exists_lawconvolutionmaskentryproduct) /\ (sto_bn_ones_exists_lawconvolutionmaskentryproduct) = 0) \/ exists ge_signed_half_ones_exists_lawconvolutionmaskentryproductright. (((dc_right_ones_exists_lawconvolutionmaskentry) = 2 * ge_signed_half_ones_exists_lawconvolutionmaskentryproductright + 1 /\ (sto_bp_ones_exists_lawconvolutionmaskentryproduct) = 0) /\ (sto_bn_ones_exists_lawconvolutionmaskentryproduct) = S ge_signed_half_ones_exists_lawconvolutionmaskentryproductright))) /\ ((((((dc_value_ones_exists_lawconvolutionmask) = 2 * (sto_cp_ones_exists_lawconvolutionmaskentryproduct) /\ (sto_cn_ones_exists_lawconvolutionmaskentryproduct) = 0) \/ exists ge_signed_half_ones_exists_lawconvolutionmaskentryproductoutput. (((dc_value_ones_exists_lawconvolutionmask) = 2 * ge_signed_half_ones_exists_lawconvolutionmaskentryproductoutput + 1 /\ (sto_cp_ones_exists_lawconvolutionmaskentryproduct) = 0) /\ (sto_cn_ones_exists_lawconvolutionmaskentryproduct) = S ge_signed_half_ones_exists_lawconvolutionmaskentryproductoutput))) /\ ((sto_ap_ones_exists_lawconvolutionmaskentryproduct * sto_bp_ones_exists_lawconvolutionmaskentryproduct + sto_an_ones_exists_lawconvolutionmaskentryproduct * sto_bn_ones_exists_lawconvolutionmaskentryproduct) + sto_cn_ones_exists_lawconvolutionmaskentryproduct = (sto_ap_ones_exists_lawconvolutionmaskentryproduct * sto_bn_ones_exists_lawconvolutionmaskentryproduct + sto_an_ones_exists_lawconvolutionmaskentryproduct * sto_bp_ones_exists_lawconvolutionmaskentryproduct) + sto_cp_ones_exists_lawconvolutionmaskentryproduct))))))))))))))) \/ ((((dc_index_ones_exists_lawconvolutionmask)=0 \/ ~(exists pvs_factor_ones_exists_lawconvolutionmaskentrynondivisor. (n) = (dc_index_ones_exists_lawconvolutionmask) * pvs_factor_ones_exists_lawconvolutionmaskentrynondivisor)) /\ ((dc_value_ones_exists_lawconvolutionmask)=0))))))) /\ (exists dst_positive_code_ones_exists_lawconvolutionfold dst_positive_scale_ones_exists_lawconvolutionfold dst_negative_code_ones_exists_lawconvolutionfold dst_negative_scale_ones_exists_lawconvolutionfold dst_positive_sum_ones_exists_lawconvolutionfold dst_negative_sum_ones_exists_lawconvolutionfold. (((dc_mask_ones_exists_lawconvolution) = (((((dst_positive_code_ones_exists_lawconvolutionfold) + (dst_positive_scale_ones_exists_lawconvolutionfold)) * S ((dst_positive_code_ones_exists_lawconvolutionfold) + (dst_positive_scale_ones_exists_lawconvolutionfold)) + ((dst_positive_scale_ones_exists_lawconvolutionfold) + (dst_positive_scale_ones_exists_lawconvolutionfold))) + (((dst_negative_code_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)) * S ((dst_negative_code_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)) + ((dst_negative_scale_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)))) * S ((((dst_positive_code_ones_exists_lawconvolutionfold) + (dst_positive_scale_ones_exists_lawconvolutionfold)) * S ((dst_positive_code_ones_exists_lawconvolutionfold) + (dst_positive_scale_ones_exists_lawconvolutionfold)) + ((dst_positive_scale_ones_exists_lawconvolutionfold) + (dst_positive_scale_ones_exists_lawconvolutionfold))) + (((dst_negative_code_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)) * S ((dst_negative_code_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)) + ((dst_negative_scale_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)))) + ((((dst_negative_code_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)) * S ((dst_negative_code_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)) + ((dst_negative_scale_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold))) + (((dst_negative_code_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)) * S ((dst_negative_code_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)) + ((dst_negative_scale_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)))))) /\ (((exists fs_u_dst_ones_exists_lawconvolutionfoldpositive fs_v_dst_ones_exists_lawconvolutionfoldpositive. ((((exists fs_h_dst_ones_exists_lawconvolutionfoldpositive_body_start. fs_h_dst_ones_exists_lawconvolutionfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_ones_exists_lawconvolutionfoldpositive)) /\ exists fs_q_dst_ones_exists_lawconvolutionfoldpositive_body_start. fs_u_dst_ones_exists_lawconvolutionfoldpositive = fs_q_dst_ones_exists_lawconvolutionfoldpositive_body_start * S ((S (0)) * fs_v_dst_ones_exists_lawconvolutionfoldpositive) + (0))) /\ ((((exists fs_h_dst_ones_exists_lawconvolutionfoldpositive_body_terminal. fs_h_dst_ones_exists_lawconvolutionfoldpositive_body_terminal + S (dst_positive_sum_ones_exists_lawconvolutionfold) = S ((S (S (n))) * fs_v_dst_ones_exists_lawconvolutionfoldpositive)) /\ exists fs_q_dst_ones_exists_lawconvolutionfoldpositive_body_terminal. fs_u_dst_ones_exists_lawconvolutionfoldpositive = fs_q_dst_ones_exists_lawconvolutionfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_ones_exists_lawconvolutionfoldpositive) + (dst_positive_sum_ones_exists_lawconvolutionfold))) /\ forall fs_i_dst_ones_exists_lawconvolutionfoldpositive_body_steps. (exists fs_lt_dst_ones_exists_lawconvolutionfoldpositive_body_steps_bound. fs_lt_dst_ones_exists_lawconvolutionfoldpositive_body_steps_bound + S fs_i_dst_ones_exists_lawconvolutionfoldpositive_body_steps = S (n)) -> exists fs_a_dst_ones_exists_lawconvolutionfoldpositive_body_steps fs_r_dst_ones_exists_lawconvolutionfoldpositive_body_steps fs_s_dst_ones_exists_lawconvolutionfoldpositive_body_steps. ((((exists fs_h_dst_ones_exists_lawconvolutionfoldpositive_body_steps_summand. fs_h_dst_ones_exists_lawconvolutionfoldpositive_body_steps_summand + S (fs_a_dst_ones_exists_lawconvolutionfoldpositive_body_steps) = S ((S (fs_i_dst_ones_exists_lawconvolutionfoldpositive_body_steps)) * dst_positive_scale_ones_exists_lawconvolutionfold)) /\ exists fs_q_dst_ones_exists_lawconvolutionfoldpositive_body_steps_summand. dst_positive_code_ones_exists_lawconvolutionfold = fs_q_dst_ones_exists_lawconvolutionfoldpositive_body_steps_summand * S ((S (fs_i_dst_ones_exists_lawconvolutionfoldpositive_body_steps)) * dst_positive_scale_ones_exists_lawconvolutionfold) + (fs_a_dst_ones_exists_lawconvolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_ones_exists_lawconvolutionfoldpositive_body_steps_partial. fs_h_dst_ones_exists_lawconvolutionfoldpositive_body_steps_partial + S (fs_r_dst_ones_exists_lawconvolutionfoldpositive_body_steps) = S ((S (fs_i_dst_ones_exists_lawconvolutionfoldpositive_body_steps)) * fs_v_dst_ones_exists_lawconvolutionfoldpositive)) /\ exists fs_q_dst_ones_exists_lawconvolutionfoldpositive_body_steps_partial. fs_u_dst_ones_exists_lawconvolutionfoldpositive = fs_q_dst_ones_exists_lawconvolutionfoldpositive_body_steps_partial * S ((S (fs_i_dst_ones_exists_lawconvolutionfoldpositive_body_steps)) * fs_v_dst_ones_exists_lawconvolutionfoldpositive) + (fs_r_dst_ones_exists_lawconvolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_ones_exists_lawconvolutionfoldpositive_body_steps_successor. fs_h_dst_ones_exists_lawconvolutionfoldpositive_body_steps_successor + S (fs_s_dst_ones_exists_lawconvolutionfoldpositive_body_steps) = S ((S (S fs_i_dst_ones_exists_lawconvolutionfoldpositive_body_steps)) * fs_v_dst_ones_exists_lawconvolutionfoldpositive)) /\ exists fs_q_dst_ones_exists_lawconvolutionfoldpositive_body_steps_successor. fs_u_dst_ones_exists_lawconvolutionfoldpositive = fs_q_dst_ones_exists_lawconvolutionfoldpositive_body_steps_successor * S ((S (S fs_i_dst_ones_exists_lawconvolutionfoldpositive_body_steps)) * fs_v_dst_ones_exists_lawconvolutionfoldpositive) + (fs_s_dst_ones_exists_lawconvolutionfoldpositive_body_steps))) /\ fs_s_dst_ones_exists_lawconvolutionfoldpositive_body_steps = fs_r_dst_ones_exists_lawconvolutionfoldpositive_body_steps + fs_a_dst_ones_exists_lawconvolutionfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_ones_exists_lawconvolutionfoldnegative fs_v_dst_ones_exists_lawconvolutionfoldnegative. ((((exists fs_h_dst_ones_exists_lawconvolutionfoldnegative_body_start. fs_h_dst_ones_exists_lawconvolutionfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_ones_exists_lawconvolutionfoldnegative)) /\ exists fs_q_dst_ones_exists_lawconvolutionfoldnegative_body_start. fs_u_dst_ones_exists_lawconvolutionfoldnegative = fs_q_dst_ones_exists_lawconvolutionfoldnegative_body_start * S ((S (0)) * fs_v_dst_ones_exists_lawconvolutionfoldnegative) + (0))) /\ ((((exists fs_h_dst_ones_exists_lawconvolutionfoldnegative_body_terminal. fs_h_dst_ones_exists_lawconvolutionfoldnegative_body_terminal + S (dst_negative_sum_ones_exists_lawconvolutionfold) = S ((S (S (n))) * fs_v_dst_ones_exists_lawconvolutionfoldnegative)) /\ exists fs_q_dst_ones_exists_lawconvolutionfoldnegative_body_terminal. fs_u_dst_ones_exists_lawconvolutionfoldnegative = fs_q_dst_ones_exists_lawconvolutionfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_ones_exists_lawconvolutionfoldnegative) + (dst_negative_sum_ones_exists_lawconvolutionfold))) /\ forall fs_i_dst_ones_exists_lawconvolutionfoldnegative_body_steps. (exists fs_lt_dst_ones_exists_lawconvolutionfoldnegative_body_steps_bound. fs_lt_dst_ones_exists_lawconvolutionfoldnegative_body_steps_bound + S fs_i_dst_ones_exists_lawconvolutionfoldnegative_body_steps = S (n)) -> exists fs_a_dst_ones_exists_lawconvolutionfoldnegative_body_steps fs_r_dst_ones_exists_lawconvolutionfoldnegative_body_steps fs_s_dst_ones_exists_lawconvolutionfoldnegative_body_steps. ((((exists fs_h_dst_ones_exists_lawconvolutionfoldnegative_body_steps_summand. fs_h_dst_ones_exists_lawconvolutionfoldnegative_body_steps_summand + S (fs_a_dst_ones_exists_lawconvolutionfoldnegative_body_steps) = S ((S (fs_i_dst_ones_exists_lawconvolutionfoldnegative_body_steps)) * dst_negative_scale_ones_exists_lawconvolutionfold)) /\ exists fs_q_dst_ones_exists_lawconvolutionfoldnegative_body_steps_summand. dst_negative_code_ones_exists_lawconvolutionfold = fs_q_dst_ones_exists_lawconvolutionfoldnegative_body_steps_summand * S ((S (fs_i_dst_ones_exists_lawconvolutionfoldnegative_body_steps)) * dst_negative_scale_ones_exists_lawconvolutionfold) + (fs_a_dst_ones_exists_lawconvolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_ones_exists_lawconvolutionfoldnegative_body_steps_partial. fs_h_dst_ones_exists_lawconvolutionfoldnegative_body_steps_partial + S (fs_r_dst_ones_exists_lawconvolutionfoldnegative_body_steps) = S ((S (fs_i_dst_ones_exists_lawconvolutionfoldnegative_body_steps)) * fs_v_dst_ones_exists_lawconvolutionfoldnegative)) /\ exists fs_q_dst_ones_exists_lawconvolutionfoldnegative_body_steps_partial. fs_u_dst_ones_exists_lawconvolutionfoldnegative = fs_q_dst_ones_exists_lawconvolutionfoldnegative_body_steps_partial * S ((S (fs_i_dst_ones_exists_lawconvolutionfoldnegative_body_steps)) * fs_v_dst_ones_exists_lawconvolutionfoldnegative) + (fs_r_dst_ones_exists_lawconvolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_ones_exists_lawconvolutionfoldnegative_body_steps_successor. fs_h_dst_ones_exists_lawconvolutionfoldnegative_body_steps_successor + S (fs_s_dst_ones_exists_lawconvolutionfoldnegative_body_steps) = S ((S (S fs_i_dst_ones_exists_lawconvolutionfoldnegative_body_steps)) * fs_v_dst_ones_exists_lawconvolutionfoldnegative)) /\ exists fs_q_dst_ones_exists_lawconvolutionfoldnegative_body_steps_successor. fs_u_dst_ones_exists_lawconvolutionfoldnegative = fs_q_dst_ones_exists_lawconvolutionfoldnegative_body_steps_successor * S ((S (S fs_i_dst_ones_exists_lawconvolutionfoldnegative_body_steps)) * fs_v_dst_ones_exists_lawconvolutionfoldnegative) + (fs_s_dst_ones_exists_lawconvolutionfoldnegative_body_steps))) /\ fs_s_dst_ones_exists_lawconvolutionfoldnegative_body_steps = fs_r_dst_ones_exists_lawconvolutionfoldnegative_body_steps + fs_a_dst_ones_exists_lawconvolutionfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_ones_exists_lawconvolutionfoldresult ge_balance_negative_ones_exists_lawconvolutionfoldresult. (((((z) = 2 * (ge_balance_positive_ones_exists_lawconvolutionfoldresult) /\ (ge_balance_negative_ones_exists_lawconvolutionfoldresult) = 0) \/ exists ge_signed_half_ones_exists_lawconvolutionfoldresultdecode. (((z) = 2 * ge_signed_half_ones_exists_lawconvolutionfoldresultdecode + 1 /\ (ge_balance_positive_ones_exists_lawconvolutionfoldresult) = 0) /\ (ge_balance_negative_ones_exists_lawconvolutionfoldresult) = S ge_signed_half_ones_exists_lawconvolutionfoldresultdecode))) /\ ((dst_positive_sum_ones_exists_lawconvolutionfold) + ge_balance_negative_ones_exists_lawconvolutionfoldresult = (dst_negative_sum_ones_exists_lawconvolutionfold) + ge_balance_positive_ones_exists_lawconvolutionfoldresult))))))))))))) -> (((~((n)=0)) /\ (exists dm_mask_table_ones_exists_lawdivisor. ((((exists dst_positive_code_ones_exists_lawdivisormasktable dst_positive_scale_ones_exists_lawdivisormasktable dst_negative_code_ones_exists_lawdivisormasktable dst_negative_scale_ones_exists_lawdivisormasktable. (((dm_mask_table_ones_exists_lawdivisor) = (((((dst_positive_code_ones_exists_lawdivisormasktable) + (dst_positive_scale_ones_exists_lawdivisormasktable)) * S ((dst_positive_code_ones_exists_lawdivisormasktable) + (dst_positive_scale_ones_exists_lawdivisormasktable)) + ((dst_positive_scale_ones_exists_lawdivisormasktable) + (dst_positive_scale_ones_exists_lawdivisormasktable))) + (((dst_negative_code_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)) * S ((dst_negative_code_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)) + ((dst_negative_scale_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)))) * S ((((dst_positive_code_ones_exists_lawdivisormasktable) + (dst_positive_scale_ones_exists_lawdivisormasktable)) * S ((dst_positive_code_ones_exists_lawdivisormasktable) + (dst_positive_scale_ones_exists_lawdivisormasktable)) + ((dst_positive_scale_ones_exists_lawdivisormasktable) + (dst_positive_scale_ones_exists_lawdivisormasktable))) + (((dst_negative_code_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)) * S ((dst_negative_code_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)) + ((dst_negative_scale_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)))) + ((((dst_negative_code_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)) * S ((dst_negative_code_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)) + ((dst_negative_scale_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable))) + (((dst_negative_code_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)) * S ((dst_negative_code_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)) + ((dst_negative_scale_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)))))) /\ (forall dst_index_ones_exists_lawdivisormasktable. (exists pvs_le_gap_ones_exists_lawdivisormasktabledomain. pvs_le_gap_ones_exists_lawdivisormasktabledomain + (dst_index_ones_exists_lawdivisormasktable) = (n)) -> exists dst_positive_ones_exists_lawdivisormasktable dst_negative_ones_exists_lawdivisormasktable dst_value_ones_exists_lawdivisormasktable. ((((exists ff_h_pvs_ones_exists_lawdivisormasktableentrypositive. ff_h_pvs_ones_exists_lawdivisormasktableentrypositive + S (dst_positive_ones_exists_lawdivisormasktable) = S ((S (dst_index_ones_exists_lawdivisormasktable)) * dst_positive_scale_ones_exists_lawdivisormasktable)) /\ exists ff_q_pvs_ones_exists_lawdivisormasktableentrypositive. dst_positive_code_ones_exists_lawdivisormasktable = ff_q_pvs_ones_exists_lawdivisormasktableentrypositive * S ((S (dst_index_ones_exists_lawdivisormasktable)) * dst_positive_scale_ones_exists_lawdivisormasktable) + (dst_positive_ones_exists_lawdivisormasktable))) /\ (((((exists ff_h_pvs_ones_exists_lawdivisormasktableentrynegative. ff_h_pvs_ones_exists_lawdivisormasktableentrynegative + S (dst_negative_ones_exists_lawdivisormasktable) = S ((S (dst_index_ones_exists_lawdivisormasktable)) * dst_negative_scale_ones_exists_lawdivisormasktable)) /\ exists ff_q_pvs_ones_exists_lawdivisormasktableentrynegative. dst_negative_code_ones_exists_lawdivisormasktable = ff_q_pvs_ones_exists_lawdivisormasktableentrynegative * S ((S (dst_index_ones_exists_lawdivisormasktable)) * dst_negative_scale_ones_exists_lawdivisormasktable) + (dst_negative_ones_exists_lawdivisormasktable))) /\ (exists ge_balance_positive_ones_exists_lawdivisormasktableentryvalue ge_balance_negative_ones_exists_lawdivisormasktableentryvalue. (((((dst_value_ones_exists_lawdivisormasktable) = 2 * (ge_balance_positive_ones_exists_lawdivisormasktableentryvalue) /\ (ge_balance_negative_ones_exists_lawdivisormasktableentryvalue) = 0) \/ exists ge_signed_half_ones_exists_lawdivisormasktableentryvaluedecode. (((dst_value_ones_exists_lawdivisormasktable) = 2 * ge_signed_half_ones_exists_lawdivisormasktableentryvaluedecode + 1 /\ (ge_balance_positive_ones_exists_lawdivisormasktableentryvalue) = 0) /\ (ge_balance_negative_ones_exists_lawdivisormasktableentryvalue) = S ge_signed_half_ones_exists_lawdivisormasktableentryvaluedecode))) /\ ((dst_positive_ones_exists_lawdivisormasktable) + ge_balance_negative_ones_exists_lawdivisormasktableentryvalue = (dst_negative_ones_exists_lawdivisormasktable) + ge_balance_positive_ones_exists_lawdivisormasktableentryvalue))))))))) /\ (forall dm_index_ones_exists_lawdivisormask dm_value_ones_exists_lawdivisormask. (exists pvs_le_gap_ones_exists_lawdivisormaskdomain. pvs_le_gap_ones_exists_lawdivisormaskdomain + (dm_index_ones_exists_lawdivisormask) = (n)) -> (exists dst_positive_code_ones_exists_lawdivisormasklookup dst_positive_scale_ones_exists_lawdivisormasklookup dst_negative_code_ones_exists_lawdivisormasklookup dst_negative_scale_ones_exists_lawdivisormasklookup dst_positive_ones_exists_lawdivisormasklookup dst_negative_ones_exists_lawdivisormasklookup. (((dm_mask_table_ones_exists_lawdivisor) = (((((dst_positive_code_ones_exists_lawdivisormasklookup) + (dst_positive_scale_ones_exists_lawdivisormasklookup)) * S ((dst_positive_code_ones_exists_lawdivisormasklookup) + (dst_positive_scale_ones_exists_lawdivisormasklookup)) + ((dst_positive_scale_ones_exists_lawdivisormasklookup) + (dst_positive_scale_ones_exists_lawdivisormasklookup))) + (((dst_negative_code_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)) * S ((dst_negative_code_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)) + ((dst_negative_scale_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)))) * S ((((dst_positive_code_ones_exists_lawdivisormasklookup) + (dst_positive_scale_ones_exists_lawdivisormasklookup)) * S ((dst_positive_code_ones_exists_lawdivisormasklookup) + (dst_positive_scale_ones_exists_lawdivisormasklookup)) + ((dst_positive_scale_ones_exists_lawdivisormasklookup) + (dst_positive_scale_ones_exists_lawdivisormasklookup))) + (((dst_negative_code_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)) * S ((dst_negative_code_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)) + ((dst_negative_scale_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)))) + ((((dst_negative_code_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)) * S ((dst_negative_code_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)) + ((dst_negative_scale_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup))) + (((dst_negative_code_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)) * S ((dst_negative_code_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)) + ((dst_negative_scale_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)))))) /\ (((((exists ff_h_pvs_ones_exists_lawdivisormasklookuppositive. ff_h_pvs_ones_exists_lawdivisormasklookuppositive + S (dst_positive_ones_exists_lawdivisormasklookup) = S ((S (dm_index_ones_exists_lawdivisormask)) * dst_positive_scale_ones_exists_lawdivisormasklookup)) /\ exists ff_q_pvs_ones_exists_lawdivisormasklookuppositive. dst_positive_code_ones_exists_lawdivisormasklookup = ff_q_pvs_ones_exists_lawdivisormasklookuppositive * S ((S (dm_index_ones_exists_lawdivisormask)) * dst_positive_scale_ones_exists_lawdivisormasklookup) + (dst_positive_ones_exists_lawdivisormasklookup))) /\ (((((exists ff_h_pvs_ones_exists_lawdivisormasklookupnegative. ff_h_pvs_ones_exists_lawdivisormasklookupnegative + S (dst_negative_ones_exists_lawdivisormasklookup) = S ((S (dm_index_ones_exists_lawdivisormask)) * dst_negative_scale_ones_exists_lawdivisormasklookup)) /\ exists ff_q_pvs_ones_exists_lawdivisormasklookupnegative. dst_negative_code_ones_exists_lawdivisormasklookup = ff_q_pvs_ones_exists_lawdivisormasklookupnegative * S ((S (dm_index_ones_exists_lawdivisormask)) * dst_negative_scale_ones_exists_lawdivisormasklookup) + (dst_negative_ones_exists_lawdivisormasklookup))) /\ (exists ge_balance_positive_ones_exists_lawdivisormasklookupvalue ge_balance_negative_ones_exists_lawdivisormasklookupvalue. (((((dm_value_ones_exists_lawdivisormask) = 2 * (ge_balance_positive_ones_exists_lawdivisormasklookupvalue) /\ (ge_balance_negative_ones_exists_lawdivisormasklookupvalue) = 0) \/ exists ge_signed_half_ones_exists_lawdivisormasklookupvaluedecode. (((dm_value_ones_exists_lawdivisormask) = 2 * ge_signed_half_ones_exists_lawdivisormasklookupvaluedecode + 1 /\ (ge_balance_positive_ones_exists_lawdivisormasklookupvalue) = 0) /\ (ge_balance_negative_ones_exists_lawdivisormasklookupvalue) = S ge_signed_half_ones_exists_lawdivisormasklookupvaluedecode))) /\ ((dst_positive_ones_exists_lawdivisormasklookup) + ge_balance_negative_ones_exists_lawdivisormasklookupvalue = (dst_negative_ones_exists_lawdivisormasklookup) + ge_balance_positive_ones_exists_lawdivisormasklookupvalue))))))))) -> ((((~((dm_index_ones_exists_lawdivisormask)=0)) /\ (exists dm_quotient_ones_exists_lawdivisormaskentry. (((n)=(dm_index_ones_exists_lawdivisormask)*dm_quotient_ones_exists_lawdivisormaskentry) /\ (exists dst_positive_code_ones_exists_lawdivisormaskentryinput dst_positive_scale_ones_exists_lawdivisormaskentryinput dst_negative_code_ones_exists_lawdivisormaskentryinput dst_negative_scale_ones_exists_lawdivisormaskentryinput dst_positive_ones_exists_lawdivisormaskentryinput dst_negative_ones_exists_lawdivisormaskentryinput. (((F) = (((((dst_positive_code_ones_exists_lawdivisormaskentryinput) + (dst_positive_scale_ones_exists_lawdivisormaskentryinput)) * S ((dst_positive_code_ones_exists_lawdivisormaskentryinput) + (dst_positive_scale_ones_exists_lawdivisormaskentryinput)) + ((dst_positive_scale_ones_exists_lawdivisormaskentryinput) + (dst_positive_scale_ones_exists_lawdivisormaskentryinput))) + (((dst_negative_code_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)) * S ((dst_negative_code_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)) + ((dst_negative_scale_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)))) * S ((((dst_positive_code_ones_exists_lawdivisormaskentryinput) + (dst_positive_scale_ones_exists_lawdivisormaskentryinput)) * S ((dst_positive_code_ones_exists_lawdivisormaskentryinput) + (dst_positive_scale_ones_exists_lawdivisormaskentryinput)) + ((dst_positive_scale_ones_exists_lawdivisormaskentryinput) + (dst_positive_scale_ones_exists_lawdivisormaskentryinput))) + (((dst_negative_code_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)) * S ((dst_negative_code_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)) + ((dst_negative_scale_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)))) + ((((dst_negative_code_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)) * S ((dst_negative_code_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)) + ((dst_negative_scale_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput))) + (((dst_negative_code_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)) * S ((dst_negative_code_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)) + ((dst_negative_scale_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)))))) /\ (((((exists ff_h_pvs_ones_exists_lawdivisormaskentryinputpositive. ff_h_pvs_ones_exists_lawdivisormaskentryinputpositive + S (dst_positive_ones_exists_lawdivisormaskentryinput) = S ((S (dm_index_ones_exists_lawdivisormask)) * dst_positive_scale_ones_exists_lawdivisormaskentryinput)) /\ exists ff_q_pvs_ones_exists_lawdivisormaskentryinputpositive. dst_positive_code_ones_exists_lawdivisormaskentryinput = ff_q_pvs_ones_exists_lawdivisormaskentryinputpositive * S ((S (dm_index_ones_exists_lawdivisormask)) * dst_positive_scale_ones_exists_lawdivisormaskentryinput) + (dst_positive_ones_exists_lawdivisormaskentryinput))) /\ (((((exists ff_h_pvs_ones_exists_lawdivisormaskentryinputnegative. ff_h_pvs_ones_exists_lawdivisormaskentryinputnegative + S (dst_negative_ones_exists_lawdivisormaskentryinput) = S ((S (dm_index_ones_exists_lawdivisormask)) * dst_negative_scale_ones_exists_lawdivisormaskentryinput)) /\ exists ff_q_pvs_ones_exists_lawdivisormaskentryinputnegative. dst_negative_code_ones_exists_lawdivisormaskentryinput = ff_q_pvs_ones_exists_lawdivisormaskentryinputnegative * S ((S (dm_index_ones_exists_lawdivisormask)) * dst_negative_scale_ones_exists_lawdivisormaskentryinput) + (dst_negative_ones_exists_lawdivisormaskentryinput))) /\ (exists ge_balance_positive_ones_exists_lawdivisormaskentryinputvalue ge_balance_negative_ones_exists_lawdivisormaskentryinputvalue. (((((dm_value_ones_exists_lawdivisormask) = 2 * (ge_balance_positive_ones_exists_lawdivisormaskentryinputvalue) /\ (ge_balance_negative_ones_exists_lawdivisormaskentryinputvalue) = 0) \/ exists ge_signed_half_ones_exists_lawdivisormaskentryinputvaluedecode. (((dm_value_ones_exists_lawdivisormask) = 2 * ge_signed_half_ones_exists_lawdivisormaskentryinputvaluedecode + 1 /\ (ge_balance_positive_ones_exists_lawdivisormaskentryinputvalue) = 0) /\ (ge_balance_negative_ones_exists_lawdivisormaskentryinputvalue) = S ge_signed_half_ones_exists_lawdivisormaskentryinputvaluedecode))) /\ ((dst_positive_ones_exists_lawdivisormaskentryinput) + ge_balance_negative_ones_exists_lawdivisormaskentryinputvalue = (dst_negative_ones_exists_lawdivisormaskentryinput) + ge_balance_positive_ones_exists_lawdivisormaskentryinputvalue))))))))))))) \/ ((((dm_index_ones_exists_lawdivisormask)=0 \/ ~(exists pvs_factor_ones_exists_lawdivisormaskentrynondivisor. (n) = (dm_index_ones_exists_lawdivisormask) * pvs_factor_ones_exists_lawdivisormaskentrynondivisor)) /\ ((dm_value_ones_exists_lawdivisormask)=0))))))) /\ (exists dst_positive_code_ones_exists_lawdivisorfold dst_positive_scale_ones_exists_lawdivisorfold dst_negative_code_ones_exists_lawdivisorfold dst_negative_scale_ones_exists_lawdivisorfold dst_positive_sum_ones_exists_lawdivisorfold dst_negative_sum_ones_exists_lawdivisorfold. (((dm_mask_table_ones_exists_lawdivisor) = (((((dst_positive_code_ones_exists_lawdivisorfold) + (dst_positive_scale_ones_exists_lawdivisorfold)) * S ((dst_positive_code_ones_exists_lawdivisorfold) + (dst_positive_scale_ones_exists_lawdivisorfold)) + ((dst_positive_scale_ones_exists_lawdivisorfold) + (dst_positive_scale_ones_exists_lawdivisorfold))) + (((dst_negative_code_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)) * S ((dst_negative_code_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)) + ((dst_negative_scale_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)))) * S ((((dst_positive_code_ones_exists_lawdivisorfold) + (dst_positive_scale_ones_exists_lawdivisorfold)) * S ((dst_positive_code_ones_exists_lawdivisorfold) + (dst_positive_scale_ones_exists_lawdivisorfold)) + ((dst_positive_scale_ones_exists_lawdivisorfold) + (dst_positive_scale_ones_exists_lawdivisorfold))) + (((dst_negative_code_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)) * S ((dst_negative_code_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)) + ((dst_negative_scale_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)))) + ((((dst_negative_code_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)) * S ((dst_negative_code_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)) + ((dst_negative_scale_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold))) + (((dst_negative_code_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)) * S ((dst_negative_code_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)) + ((dst_negative_scale_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)))))) /\ (((exists fs_u_dst_ones_exists_lawdivisorfoldpositive fs_v_dst_ones_exists_lawdivisorfoldpositive. ((((exists fs_h_dst_ones_exists_lawdivisorfoldpositive_body_start. fs_h_dst_ones_exists_lawdivisorfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_ones_exists_lawdivisorfoldpositive)) /\ exists fs_q_dst_ones_exists_lawdivisorfoldpositive_body_start. fs_u_dst_ones_exists_lawdivisorfoldpositive = fs_q_dst_ones_exists_lawdivisorfoldpositive_body_start * S ((S (0)) * fs_v_dst_ones_exists_lawdivisorfoldpositive) + (0))) /\ ((((exists fs_h_dst_ones_exists_lawdivisorfoldpositive_body_terminal. fs_h_dst_ones_exists_lawdivisorfoldpositive_body_terminal + S (dst_positive_sum_ones_exists_lawdivisorfold) = S ((S (S (n))) * fs_v_dst_ones_exists_lawdivisorfoldpositive)) /\ exists fs_q_dst_ones_exists_lawdivisorfoldpositive_body_terminal. fs_u_dst_ones_exists_lawdivisorfoldpositive = fs_q_dst_ones_exists_lawdivisorfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_ones_exists_lawdivisorfoldpositive) + (dst_positive_sum_ones_exists_lawdivisorfold))) /\ forall fs_i_dst_ones_exists_lawdivisorfoldpositive_body_steps. (exists fs_lt_dst_ones_exists_lawdivisorfoldpositive_body_steps_bound. fs_lt_dst_ones_exists_lawdivisorfoldpositive_body_steps_bound + S fs_i_dst_ones_exists_lawdivisorfoldpositive_body_steps = S (n)) -> exists fs_a_dst_ones_exists_lawdivisorfoldpositive_body_steps fs_r_dst_ones_exists_lawdivisorfoldpositive_body_steps fs_s_dst_ones_exists_lawdivisorfoldpositive_body_steps. ((((exists fs_h_dst_ones_exists_lawdivisorfoldpositive_body_steps_summand. fs_h_dst_ones_exists_lawdivisorfoldpositive_body_steps_summand + S (fs_a_dst_ones_exists_lawdivisorfoldpositive_body_steps) = S ((S (fs_i_dst_ones_exists_lawdivisorfoldpositive_body_steps)) * dst_positive_scale_ones_exists_lawdivisorfold)) /\ exists fs_q_dst_ones_exists_lawdivisorfoldpositive_body_steps_summand. dst_positive_code_ones_exists_lawdivisorfold = fs_q_dst_ones_exists_lawdivisorfoldpositive_body_steps_summand * S ((S (fs_i_dst_ones_exists_lawdivisorfoldpositive_body_steps)) * dst_positive_scale_ones_exists_lawdivisorfold) + (fs_a_dst_ones_exists_lawdivisorfoldpositive_body_steps))) /\ ((((exists fs_h_dst_ones_exists_lawdivisorfoldpositive_body_steps_partial. fs_h_dst_ones_exists_lawdivisorfoldpositive_body_steps_partial + S (fs_r_dst_ones_exists_lawdivisorfoldpositive_body_steps) = S ((S (fs_i_dst_ones_exists_lawdivisorfoldpositive_body_steps)) * fs_v_dst_ones_exists_lawdivisorfoldpositive)) /\ exists fs_q_dst_ones_exists_lawdivisorfoldpositive_body_steps_partial. fs_u_dst_ones_exists_lawdivisorfoldpositive = fs_q_dst_ones_exists_lawdivisorfoldpositive_body_steps_partial * S ((S (fs_i_dst_ones_exists_lawdivisorfoldpositive_body_steps)) * fs_v_dst_ones_exists_lawdivisorfoldpositive) + (fs_r_dst_ones_exists_lawdivisorfoldpositive_body_steps))) /\ ((((exists fs_h_dst_ones_exists_lawdivisorfoldpositive_body_steps_successor. fs_h_dst_ones_exists_lawdivisorfoldpositive_body_steps_successor + S (fs_s_dst_ones_exists_lawdivisorfoldpositive_body_steps) = S ((S (S fs_i_dst_ones_exists_lawdivisorfoldpositive_body_steps)) * fs_v_dst_ones_exists_lawdivisorfoldpositive)) /\ exists fs_q_dst_ones_exists_lawdivisorfoldpositive_body_steps_successor. fs_u_dst_ones_exists_lawdivisorfoldpositive = fs_q_dst_ones_exists_lawdivisorfoldpositive_body_steps_successor * S ((S (S fs_i_dst_ones_exists_lawdivisorfoldpositive_body_steps)) * fs_v_dst_ones_exists_lawdivisorfoldpositive) + (fs_s_dst_ones_exists_lawdivisorfoldpositive_body_steps))) /\ fs_s_dst_ones_exists_lawdivisorfoldpositive_body_steps = fs_r_dst_ones_exists_lawdivisorfoldpositive_body_steps + fs_a_dst_ones_exists_lawdivisorfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_ones_exists_lawdivisorfoldnegative fs_v_dst_ones_exists_lawdivisorfoldnegative. ((((exists fs_h_dst_ones_exists_lawdivisorfoldnegative_body_start. fs_h_dst_ones_exists_lawdivisorfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_ones_exists_lawdivisorfoldnegative)) /\ exists fs_q_dst_ones_exists_lawdivisorfoldnegative_body_start. fs_u_dst_ones_exists_lawdivisorfoldnegative = fs_q_dst_ones_exists_lawdivisorfoldnegative_body_start * S ((S (0)) * fs_v_dst_ones_exists_lawdivisorfoldnegative) + (0))) /\ ((((exists fs_h_dst_ones_exists_lawdivisorfoldnegative_body_terminal. fs_h_dst_ones_exists_lawdivisorfoldnegative_body_terminal + S (dst_negative_sum_ones_exists_lawdivisorfold) = S ((S (S (n))) * fs_v_dst_ones_exists_lawdivisorfoldnegative)) /\ exists fs_q_dst_ones_exists_lawdivisorfoldnegative_body_terminal. fs_u_dst_ones_exists_lawdivisorfoldnegative = fs_q_dst_ones_exists_lawdivisorfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_ones_exists_lawdivisorfoldnegative) + (dst_negative_sum_ones_exists_lawdivisorfold))) /\ forall fs_i_dst_ones_exists_lawdivisorfoldnegative_body_steps. (exists fs_lt_dst_ones_exists_lawdivisorfoldnegative_body_steps_bound. fs_lt_dst_ones_exists_lawdivisorfoldnegative_body_steps_bound + S fs_i_dst_ones_exists_lawdivisorfoldnegative_body_steps = S (n)) -> exists fs_a_dst_ones_exists_lawdivisorfoldnegative_body_steps fs_r_dst_ones_exists_lawdivisorfoldnegative_body_steps fs_s_dst_ones_exists_lawdivisorfoldnegative_body_steps. ((((exists fs_h_dst_ones_exists_lawdivisorfoldnegative_body_steps_summand. fs_h_dst_ones_exists_lawdivisorfoldnegative_body_steps_summand + S (fs_a_dst_ones_exists_lawdivisorfoldnegative_body_steps) = S ((S (fs_i_dst_ones_exists_lawdivisorfoldnegative_body_steps)) * dst_negative_scale_ones_exists_lawdivisorfold)) /\ exists fs_q_dst_ones_exists_lawdivisorfoldnegative_body_steps_summand. dst_negative_code_ones_exists_lawdivisorfold = fs_q_dst_ones_exists_lawdivisorfoldnegative_body_steps_summand * S ((S (fs_i_dst_ones_exists_lawdivisorfoldnegative_body_steps)) * dst_negative_scale_ones_exists_lawdivisorfold) + (fs_a_dst_ones_exists_lawdivisorfoldnegative_body_steps))) /\ ((((exists fs_h_dst_ones_exists_lawdivisorfoldnegative_body_steps_partial. fs_h_dst_ones_exists_lawdivisorfoldnegative_body_steps_partial + S (fs_r_dst_ones_exists_lawdivisorfoldnegative_body_steps) = S ((S (fs_i_dst_ones_exists_lawdivisorfoldnegative_body_steps)) * fs_v_dst_ones_exists_lawdivisorfoldnegative)) /\ exists fs_q_dst_ones_exists_lawdivisorfoldnegative_body_steps_partial. fs_u_dst_ones_exists_lawdivisorfoldnegative = fs_q_dst_ones_exists_lawdivisorfoldnegative_body_steps_partial * S ((S (fs_i_dst_ones_exists_lawdivisorfoldnegative_body_steps)) * fs_v_dst_ones_exists_lawdivisorfoldnegative) + (fs_r_dst_ones_exists_lawdivisorfoldnegative_body_steps))) /\ ((((exists fs_h_dst_ones_exists_lawdivisorfoldnegative_body_steps_successor. fs_h_dst_ones_exists_lawdivisorfoldnegative_body_steps_successor + S (fs_s_dst_ones_exists_lawdivisorfoldnegative_body_steps) = S ((S (S fs_i_dst_ones_exists_lawdivisorfoldnegative_body_steps)) * fs_v_dst_ones_exists_lawdivisorfoldnegative)) /\ exists fs_q_dst_ones_exists_lawdivisorfoldnegative_body_steps_successor. fs_u_dst_ones_exists_lawdivisorfoldnegative = fs_q_dst_ones_exists_lawdivisorfoldnegative_body_steps_successor * S ((S (S fs_i_dst_ones_exists_lawdivisorfoldnegative_body_steps)) * fs_v_dst_ones_exists_lawdivisorfoldnegative) + (fs_s_dst_ones_exists_lawdivisorfoldnegative_body_steps))) /\ fs_s_dst_ones_exists_lawdivisorfoldnegative_body_steps = fs_r_dst_ones_exists_lawdivisorfoldnegative_body_steps + fs_a_dst_ones_exists_lawdivisorfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_ones_exists_lawdivisorfoldresult ge_balance_negative_ones_exists_lawdivisorfoldresult. (((((z) = 2 * (ge_balance_positive_ones_exists_lawdivisorfoldresult) /\ (ge_balance_negative_ones_exists_lawdivisorfoldresult) = 0) \/ exists ge_signed_half_ones_exists_lawdivisorfoldresultdecode. (((z) = 2 * ge_signed_half_ones_exists_lawdivisorfoldresultdecode + 1 /\ (ge_balance_positive_ones_exists_lawdivisorfoldresult) = 0) /\ (ge_balance_negative_ones_exists_lawdivisorfoldresult) = S ge_signed_half_ones_exists_lawdivisorfoldresultdecode))) /\ ((dst_positive_sum_ones_exists_lawdivisorfold) + ge_balance_negative_ones_exists_lawdivisorfoldresult = (dst_negative_sum_ones_exists_lawdivisorfold) + ge_balance_positive_ones_exists_lawdivisorfoldresult)))))))))))))) /\ ((((~((n)=0)) /\ (exists dm_mask_table_ones_exists_lawdivisor. ((((exists dst_positive_code_ones_exists_lawdivisormasktable dst_positive_scale_ones_exists_lawdivisormasktable dst_negative_code_ones_exists_lawdivisormasktable dst_negative_scale_ones_exists_lawdivisormasktable. (((dm_mask_table_ones_exists_lawdivisor) = (((((dst_positive_code_ones_exists_lawdivisormasktable) + (dst_positive_scale_ones_exists_lawdivisormasktable)) * S ((dst_positive_code_ones_exists_lawdivisormasktable) + (dst_positive_scale_ones_exists_lawdivisormasktable)) + ((dst_positive_scale_ones_exists_lawdivisormasktable) + (dst_positive_scale_ones_exists_lawdivisormasktable))) + (((dst_negative_code_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)) * S ((dst_negative_code_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)) + ((dst_negative_scale_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)))) * S ((((dst_positive_code_ones_exists_lawdivisormasktable) + (dst_positive_scale_ones_exists_lawdivisormasktable)) * S ((dst_positive_code_ones_exists_lawdivisormasktable) + (dst_positive_scale_ones_exists_lawdivisormasktable)) + ((dst_positive_scale_ones_exists_lawdivisormasktable) + (dst_positive_scale_ones_exists_lawdivisormasktable))) + (((dst_negative_code_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)) * S ((dst_negative_code_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)) + ((dst_negative_scale_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)))) + ((((dst_negative_code_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)) * S ((dst_negative_code_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)) + ((dst_negative_scale_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable))) + (((dst_negative_code_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)) * S ((dst_negative_code_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)) + ((dst_negative_scale_ones_exists_lawdivisormasktable) + (dst_negative_scale_ones_exists_lawdivisormasktable)))))) /\ (forall dst_index_ones_exists_lawdivisormasktable. (exists pvs_le_gap_ones_exists_lawdivisormasktabledomain. pvs_le_gap_ones_exists_lawdivisormasktabledomain + (dst_index_ones_exists_lawdivisormasktable) = (n)) -> exists dst_positive_ones_exists_lawdivisormasktable dst_negative_ones_exists_lawdivisormasktable dst_value_ones_exists_lawdivisormasktable. ((((exists ff_h_pvs_ones_exists_lawdivisormasktableentrypositive. ff_h_pvs_ones_exists_lawdivisormasktableentrypositive + S (dst_positive_ones_exists_lawdivisormasktable) = S ((S (dst_index_ones_exists_lawdivisormasktable)) * dst_positive_scale_ones_exists_lawdivisormasktable)) /\ exists ff_q_pvs_ones_exists_lawdivisormasktableentrypositive. dst_positive_code_ones_exists_lawdivisormasktable = ff_q_pvs_ones_exists_lawdivisormasktableentrypositive * S ((S (dst_index_ones_exists_lawdivisormasktable)) * dst_positive_scale_ones_exists_lawdivisormasktable) + (dst_positive_ones_exists_lawdivisormasktable))) /\ (((((exists ff_h_pvs_ones_exists_lawdivisormasktableentrynegative. ff_h_pvs_ones_exists_lawdivisormasktableentrynegative + S (dst_negative_ones_exists_lawdivisormasktable) = S ((S (dst_index_ones_exists_lawdivisormasktable)) * dst_negative_scale_ones_exists_lawdivisormasktable)) /\ exists ff_q_pvs_ones_exists_lawdivisormasktableentrynegative. dst_negative_code_ones_exists_lawdivisormasktable = ff_q_pvs_ones_exists_lawdivisormasktableentrynegative * S ((S (dst_index_ones_exists_lawdivisormasktable)) * dst_negative_scale_ones_exists_lawdivisormasktable) + (dst_negative_ones_exists_lawdivisormasktable))) /\ (exists ge_balance_positive_ones_exists_lawdivisormasktableentryvalue ge_balance_negative_ones_exists_lawdivisormasktableentryvalue. (((((dst_value_ones_exists_lawdivisormasktable) = 2 * (ge_balance_positive_ones_exists_lawdivisormasktableentryvalue) /\ (ge_balance_negative_ones_exists_lawdivisormasktableentryvalue) = 0) \/ exists ge_signed_half_ones_exists_lawdivisormasktableentryvaluedecode. (((dst_value_ones_exists_lawdivisormasktable) = 2 * ge_signed_half_ones_exists_lawdivisormasktableentryvaluedecode + 1 /\ (ge_balance_positive_ones_exists_lawdivisormasktableentryvalue) = 0) /\ (ge_balance_negative_ones_exists_lawdivisormasktableentryvalue) = S ge_signed_half_ones_exists_lawdivisormasktableentryvaluedecode))) /\ ((dst_positive_ones_exists_lawdivisormasktable) + ge_balance_negative_ones_exists_lawdivisormasktableentryvalue = (dst_negative_ones_exists_lawdivisormasktable) + ge_balance_positive_ones_exists_lawdivisormasktableentryvalue))))))))) /\ (forall dm_index_ones_exists_lawdivisormask dm_value_ones_exists_lawdivisormask. (exists pvs_le_gap_ones_exists_lawdivisormaskdomain. pvs_le_gap_ones_exists_lawdivisormaskdomain + (dm_index_ones_exists_lawdivisormask) = (n)) -> (exists dst_positive_code_ones_exists_lawdivisormasklookup dst_positive_scale_ones_exists_lawdivisormasklookup dst_negative_code_ones_exists_lawdivisormasklookup dst_negative_scale_ones_exists_lawdivisormasklookup dst_positive_ones_exists_lawdivisormasklookup dst_negative_ones_exists_lawdivisormasklookup. (((dm_mask_table_ones_exists_lawdivisor) = (((((dst_positive_code_ones_exists_lawdivisormasklookup) + (dst_positive_scale_ones_exists_lawdivisormasklookup)) * S ((dst_positive_code_ones_exists_lawdivisormasklookup) + (dst_positive_scale_ones_exists_lawdivisormasklookup)) + ((dst_positive_scale_ones_exists_lawdivisormasklookup) + (dst_positive_scale_ones_exists_lawdivisormasklookup))) + (((dst_negative_code_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)) * S ((dst_negative_code_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)) + ((dst_negative_scale_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)))) * S ((((dst_positive_code_ones_exists_lawdivisormasklookup) + (dst_positive_scale_ones_exists_lawdivisormasklookup)) * S ((dst_positive_code_ones_exists_lawdivisormasklookup) + (dst_positive_scale_ones_exists_lawdivisormasklookup)) + ((dst_positive_scale_ones_exists_lawdivisormasklookup) + (dst_positive_scale_ones_exists_lawdivisormasklookup))) + (((dst_negative_code_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)) * S ((dst_negative_code_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)) + ((dst_negative_scale_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)))) + ((((dst_negative_code_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)) * S ((dst_negative_code_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)) + ((dst_negative_scale_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup))) + (((dst_negative_code_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)) * S ((dst_negative_code_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)) + ((dst_negative_scale_ones_exists_lawdivisormasklookup) + (dst_negative_scale_ones_exists_lawdivisormasklookup)))))) /\ (((((exists ff_h_pvs_ones_exists_lawdivisormasklookuppositive. ff_h_pvs_ones_exists_lawdivisormasklookuppositive + S (dst_positive_ones_exists_lawdivisormasklookup) = S ((S (dm_index_ones_exists_lawdivisormask)) * dst_positive_scale_ones_exists_lawdivisormasklookup)) /\ exists ff_q_pvs_ones_exists_lawdivisormasklookuppositive. dst_positive_code_ones_exists_lawdivisormasklookup = ff_q_pvs_ones_exists_lawdivisormasklookuppositive * S ((S (dm_index_ones_exists_lawdivisormask)) * dst_positive_scale_ones_exists_lawdivisormasklookup) + (dst_positive_ones_exists_lawdivisormasklookup))) /\ (((((exists ff_h_pvs_ones_exists_lawdivisormasklookupnegative. ff_h_pvs_ones_exists_lawdivisormasklookupnegative + S (dst_negative_ones_exists_lawdivisormasklookup) = S ((S (dm_index_ones_exists_lawdivisormask)) * dst_negative_scale_ones_exists_lawdivisormasklookup)) /\ exists ff_q_pvs_ones_exists_lawdivisormasklookupnegative. dst_negative_code_ones_exists_lawdivisormasklookup = ff_q_pvs_ones_exists_lawdivisormasklookupnegative * S ((S (dm_index_ones_exists_lawdivisormask)) * dst_negative_scale_ones_exists_lawdivisormasklookup) + (dst_negative_ones_exists_lawdivisormasklookup))) /\ (exists ge_balance_positive_ones_exists_lawdivisormasklookupvalue ge_balance_negative_ones_exists_lawdivisormasklookupvalue. (((((dm_value_ones_exists_lawdivisormask) = 2 * (ge_balance_positive_ones_exists_lawdivisormasklookupvalue) /\ (ge_balance_negative_ones_exists_lawdivisormasklookupvalue) = 0) \/ exists ge_signed_half_ones_exists_lawdivisormasklookupvaluedecode. (((dm_value_ones_exists_lawdivisormask) = 2 * ge_signed_half_ones_exists_lawdivisormasklookupvaluedecode + 1 /\ (ge_balance_positive_ones_exists_lawdivisormasklookupvalue) = 0) /\ (ge_balance_negative_ones_exists_lawdivisormasklookupvalue) = S ge_signed_half_ones_exists_lawdivisormasklookupvaluedecode))) /\ ((dst_positive_ones_exists_lawdivisormasklookup) + ge_balance_negative_ones_exists_lawdivisormasklookupvalue = (dst_negative_ones_exists_lawdivisormasklookup) + ge_balance_positive_ones_exists_lawdivisormasklookupvalue))))))))) -> ((((~((dm_index_ones_exists_lawdivisormask)=0)) /\ (exists dm_quotient_ones_exists_lawdivisormaskentry. (((n)=(dm_index_ones_exists_lawdivisormask)*dm_quotient_ones_exists_lawdivisormaskentry) /\ (exists dst_positive_code_ones_exists_lawdivisormaskentryinput dst_positive_scale_ones_exists_lawdivisormaskentryinput dst_negative_code_ones_exists_lawdivisormaskentryinput dst_negative_scale_ones_exists_lawdivisormaskentryinput dst_positive_ones_exists_lawdivisormaskentryinput dst_negative_ones_exists_lawdivisormaskentryinput. (((F) = (((((dst_positive_code_ones_exists_lawdivisormaskentryinput) + (dst_positive_scale_ones_exists_lawdivisormaskentryinput)) * S ((dst_positive_code_ones_exists_lawdivisormaskentryinput) + (dst_positive_scale_ones_exists_lawdivisormaskentryinput)) + ((dst_positive_scale_ones_exists_lawdivisormaskentryinput) + (dst_positive_scale_ones_exists_lawdivisormaskentryinput))) + (((dst_negative_code_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)) * S ((dst_negative_code_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)) + ((dst_negative_scale_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)))) * S ((((dst_positive_code_ones_exists_lawdivisormaskentryinput) + (dst_positive_scale_ones_exists_lawdivisormaskentryinput)) * S ((dst_positive_code_ones_exists_lawdivisormaskentryinput) + (dst_positive_scale_ones_exists_lawdivisormaskentryinput)) + ((dst_positive_scale_ones_exists_lawdivisormaskentryinput) + (dst_positive_scale_ones_exists_lawdivisormaskentryinput))) + (((dst_negative_code_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)) * S ((dst_negative_code_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)) + ((dst_negative_scale_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)))) + ((((dst_negative_code_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)) * S ((dst_negative_code_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)) + ((dst_negative_scale_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput))) + (((dst_negative_code_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)) * S ((dst_negative_code_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)) + ((dst_negative_scale_ones_exists_lawdivisormaskentryinput) + (dst_negative_scale_ones_exists_lawdivisormaskentryinput)))))) /\ (((((exists ff_h_pvs_ones_exists_lawdivisormaskentryinputpositive. ff_h_pvs_ones_exists_lawdivisormaskentryinputpositive + S (dst_positive_ones_exists_lawdivisormaskentryinput) = S ((S (dm_index_ones_exists_lawdivisormask)) * dst_positive_scale_ones_exists_lawdivisormaskentryinput)) /\ exists ff_q_pvs_ones_exists_lawdivisormaskentryinputpositive. dst_positive_code_ones_exists_lawdivisormaskentryinput = ff_q_pvs_ones_exists_lawdivisormaskentryinputpositive * S ((S (dm_index_ones_exists_lawdivisormask)) * dst_positive_scale_ones_exists_lawdivisormaskentryinput) + (dst_positive_ones_exists_lawdivisormaskentryinput))) /\ (((((exists ff_h_pvs_ones_exists_lawdivisormaskentryinputnegative. ff_h_pvs_ones_exists_lawdivisormaskentryinputnegative + S (dst_negative_ones_exists_lawdivisormaskentryinput) = S ((S (dm_index_ones_exists_lawdivisormask)) * dst_negative_scale_ones_exists_lawdivisormaskentryinput)) /\ exists ff_q_pvs_ones_exists_lawdivisormaskentryinputnegative. dst_negative_code_ones_exists_lawdivisormaskentryinput = ff_q_pvs_ones_exists_lawdivisormaskentryinputnegative * S ((S (dm_index_ones_exists_lawdivisormask)) * dst_negative_scale_ones_exists_lawdivisormaskentryinput) + (dst_negative_ones_exists_lawdivisormaskentryinput))) /\ (exists ge_balance_positive_ones_exists_lawdivisormaskentryinputvalue ge_balance_negative_ones_exists_lawdivisormaskentryinputvalue. (((((dm_value_ones_exists_lawdivisormask) = 2 * (ge_balance_positive_ones_exists_lawdivisormaskentryinputvalue) /\ (ge_balance_negative_ones_exists_lawdivisormaskentryinputvalue) = 0) \/ exists ge_signed_half_ones_exists_lawdivisormaskentryinputvaluedecode. (((dm_value_ones_exists_lawdivisormask) = 2 * ge_signed_half_ones_exists_lawdivisormaskentryinputvaluedecode + 1 /\ (ge_balance_positive_ones_exists_lawdivisormaskentryinputvalue) = 0) /\ (ge_balance_negative_ones_exists_lawdivisormaskentryinputvalue) = S ge_signed_half_ones_exists_lawdivisormaskentryinputvaluedecode))) /\ ((dst_positive_ones_exists_lawdivisormaskentryinput) + ge_balance_negative_ones_exists_lawdivisormaskentryinputvalue = (dst_negative_ones_exists_lawdivisormaskentryinput) + ge_balance_positive_ones_exists_lawdivisormaskentryinputvalue))))))))))))) \/ ((((dm_index_ones_exists_lawdivisormask)=0 \/ ~(exists pvs_factor_ones_exists_lawdivisormaskentrynondivisor. (n) = (dm_index_ones_exists_lawdivisormask) * pvs_factor_ones_exists_lawdivisormaskentrynondivisor)) /\ ((dm_value_ones_exists_lawdivisormask)=0))))))) /\ (exists dst_positive_code_ones_exists_lawdivisorfold dst_positive_scale_ones_exists_lawdivisorfold dst_negative_code_ones_exists_lawdivisorfold dst_negative_scale_ones_exists_lawdivisorfold dst_positive_sum_ones_exists_lawdivisorfold dst_negative_sum_ones_exists_lawdivisorfold. (((dm_mask_table_ones_exists_lawdivisor) = (((((dst_positive_code_ones_exists_lawdivisorfold) + (dst_positive_scale_ones_exists_lawdivisorfold)) * S ((dst_positive_code_ones_exists_lawdivisorfold) + (dst_positive_scale_ones_exists_lawdivisorfold)) + ((dst_positive_scale_ones_exists_lawdivisorfold) + (dst_positive_scale_ones_exists_lawdivisorfold))) + (((dst_negative_code_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)) * S ((dst_negative_code_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)) + ((dst_negative_scale_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)))) * S ((((dst_positive_code_ones_exists_lawdivisorfold) + (dst_positive_scale_ones_exists_lawdivisorfold)) * S ((dst_positive_code_ones_exists_lawdivisorfold) + (dst_positive_scale_ones_exists_lawdivisorfold)) + ((dst_positive_scale_ones_exists_lawdivisorfold) + (dst_positive_scale_ones_exists_lawdivisorfold))) + (((dst_negative_code_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)) * S ((dst_negative_code_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)) + ((dst_negative_scale_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)))) + ((((dst_negative_code_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)) * S ((dst_negative_code_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)) + ((dst_negative_scale_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold))) + (((dst_negative_code_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)) * S ((dst_negative_code_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)) + ((dst_negative_scale_ones_exists_lawdivisorfold) + (dst_negative_scale_ones_exists_lawdivisorfold)))))) /\ (((exists fs_u_dst_ones_exists_lawdivisorfoldpositive fs_v_dst_ones_exists_lawdivisorfoldpositive. ((((exists fs_h_dst_ones_exists_lawdivisorfoldpositive_body_start. fs_h_dst_ones_exists_lawdivisorfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_ones_exists_lawdivisorfoldpositive)) /\ exists fs_q_dst_ones_exists_lawdivisorfoldpositive_body_start. fs_u_dst_ones_exists_lawdivisorfoldpositive = fs_q_dst_ones_exists_lawdivisorfoldpositive_body_start * S ((S (0)) * fs_v_dst_ones_exists_lawdivisorfoldpositive) + (0))) /\ ((((exists fs_h_dst_ones_exists_lawdivisorfoldpositive_body_terminal. fs_h_dst_ones_exists_lawdivisorfoldpositive_body_terminal + S (dst_positive_sum_ones_exists_lawdivisorfold) = S ((S (S (n))) * fs_v_dst_ones_exists_lawdivisorfoldpositive)) /\ exists fs_q_dst_ones_exists_lawdivisorfoldpositive_body_terminal. fs_u_dst_ones_exists_lawdivisorfoldpositive = fs_q_dst_ones_exists_lawdivisorfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_ones_exists_lawdivisorfoldpositive) + (dst_positive_sum_ones_exists_lawdivisorfold))) /\ forall fs_i_dst_ones_exists_lawdivisorfoldpositive_body_steps. (exists fs_lt_dst_ones_exists_lawdivisorfoldpositive_body_steps_bound. fs_lt_dst_ones_exists_lawdivisorfoldpositive_body_steps_bound + S fs_i_dst_ones_exists_lawdivisorfoldpositive_body_steps = S (n)) -> exists fs_a_dst_ones_exists_lawdivisorfoldpositive_body_steps fs_r_dst_ones_exists_lawdivisorfoldpositive_body_steps fs_s_dst_ones_exists_lawdivisorfoldpositive_body_steps. ((((exists fs_h_dst_ones_exists_lawdivisorfoldpositive_body_steps_summand. fs_h_dst_ones_exists_lawdivisorfoldpositive_body_steps_summand + S (fs_a_dst_ones_exists_lawdivisorfoldpositive_body_steps) = S ((S (fs_i_dst_ones_exists_lawdivisorfoldpositive_body_steps)) * dst_positive_scale_ones_exists_lawdivisorfold)) /\ exists fs_q_dst_ones_exists_lawdivisorfoldpositive_body_steps_summand. dst_positive_code_ones_exists_lawdivisorfold = fs_q_dst_ones_exists_lawdivisorfoldpositive_body_steps_summand * S ((S (fs_i_dst_ones_exists_lawdivisorfoldpositive_body_steps)) * dst_positive_scale_ones_exists_lawdivisorfold) + (fs_a_dst_ones_exists_lawdivisorfoldpositive_body_steps))) /\ ((((exists fs_h_dst_ones_exists_lawdivisorfoldpositive_body_steps_partial. fs_h_dst_ones_exists_lawdivisorfoldpositive_body_steps_partial + S (fs_r_dst_ones_exists_lawdivisorfoldpositive_body_steps) = S ((S (fs_i_dst_ones_exists_lawdivisorfoldpositive_body_steps)) * fs_v_dst_ones_exists_lawdivisorfoldpositive)) /\ exists fs_q_dst_ones_exists_lawdivisorfoldpositive_body_steps_partial. fs_u_dst_ones_exists_lawdivisorfoldpositive = fs_q_dst_ones_exists_lawdivisorfoldpositive_body_steps_partial * S ((S (fs_i_dst_ones_exists_lawdivisorfoldpositive_body_steps)) * fs_v_dst_ones_exists_lawdivisorfoldpositive) + (fs_r_dst_ones_exists_lawdivisorfoldpositive_body_steps))) /\ ((((exists fs_h_dst_ones_exists_lawdivisorfoldpositive_body_steps_successor. fs_h_dst_ones_exists_lawdivisorfoldpositive_body_steps_successor + S (fs_s_dst_ones_exists_lawdivisorfoldpositive_body_steps) = S ((S (S fs_i_dst_ones_exists_lawdivisorfoldpositive_body_steps)) * fs_v_dst_ones_exists_lawdivisorfoldpositive)) /\ exists fs_q_dst_ones_exists_lawdivisorfoldpositive_body_steps_successor. fs_u_dst_ones_exists_lawdivisorfoldpositive = fs_q_dst_ones_exists_lawdivisorfoldpositive_body_steps_successor * S ((S (S fs_i_dst_ones_exists_lawdivisorfoldpositive_body_steps)) * fs_v_dst_ones_exists_lawdivisorfoldpositive) + (fs_s_dst_ones_exists_lawdivisorfoldpositive_body_steps))) /\ fs_s_dst_ones_exists_lawdivisorfoldpositive_body_steps = fs_r_dst_ones_exists_lawdivisorfoldpositive_body_steps + fs_a_dst_ones_exists_lawdivisorfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_ones_exists_lawdivisorfoldnegative fs_v_dst_ones_exists_lawdivisorfoldnegative. ((((exists fs_h_dst_ones_exists_lawdivisorfoldnegative_body_start. fs_h_dst_ones_exists_lawdivisorfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_ones_exists_lawdivisorfoldnegative)) /\ exists fs_q_dst_ones_exists_lawdivisorfoldnegative_body_start. fs_u_dst_ones_exists_lawdivisorfoldnegative = fs_q_dst_ones_exists_lawdivisorfoldnegative_body_start * S ((S (0)) * fs_v_dst_ones_exists_lawdivisorfoldnegative) + (0))) /\ ((((exists fs_h_dst_ones_exists_lawdivisorfoldnegative_body_terminal. fs_h_dst_ones_exists_lawdivisorfoldnegative_body_terminal + S (dst_negative_sum_ones_exists_lawdivisorfold) = S ((S (S (n))) * fs_v_dst_ones_exists_lawdivisorfoldnegative)) /\ exists fs_q_dst_ones_exists_lawdivisorfoldnegative_body_terminal. fs_u_dst_ones_exists_lawdivisorfoldnegative = fs_q_dst_ones_exists_lawdivisorfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_ones_exists_lawdivisorfoldnegative) + (dst_negative_sum_ones_exists_lawdivisorfold))) /\ forall fs_i_dst_ones_exists_lawdivisorfoldnegative_body_steps. (exists fs_lt_dst_ones_exists_lawdivisorfoldnegative_body_steps_bound. fs_lt_dst_ones_exists_lawdivisorfoldnegative_body_steps_bound + S fs_i_dst_ones_exists_lawdivisorfoldnegative_body_steps = S (n)) -> exists fs_a_dst_ones_exists_lawdivisorfoldnegative_body_steps fs_r_dst_ones_exists_lawdivisorfoldnegative_body_steps fs_s_dst_ones_exists_lawdivisorfoldnegative_body_steps. ((((exists fs_h_dst_ones_exists_lawdivisorfoldnegative_body_steps_summand. fs_h_dst_ones_exists_lawdivisorfoldnegative_body_steps_summand + S (fs_a_dst_ones_exists_lawdivisorfoldnegative_body_steps) = S ((S (fs_i_dst_ones_exists_lawdivisorfoldnegative_body_steps)) * dst_negative_scale_ones_exists_lawdivisorfold)) /\ exists fs_q_dst_ones_exists_lawdivisorfoldnegative_body_steps_summand. dst_negative_code_ones_exists_lawdivisorfold = fs_q_dst_ones_exists_lawdivisorfoldnegative_body_steps_summand * S ((S (fs_i_dst_ones_exists_lawdivisorfoldnegative_body_steps)) * dst_negative_scale_ones_exists_lawdivisorfold) + (fs_a_dst_ones_exists_lawdivisorfoldnegative_body_steps))) /\ ((((exists fs_h_dst_ones_exists_lawdivisorfoldnegative_body_steps_partial. fs_h_dst_ones_exists_lawdivisorfoldnegative_body_steps_partial + S (fs_r_dst_ones_exists_lawdivisorfoldnegative_body_steps) = S ((S (fs_i_dst_ones_exists_lawdivisorfoldnegative_body_steps)) * fs_v_dst_ones_exists_lawdivisorfoldnegative)) /\ exists fs_q_dst_ones_exists_lawdivisorfoldnegative_body_steps_partial. fs_u_dst_ones_exists_lawdivisorfoldnegative = fs_q_dst_ones_exists_lawdivisorfoldnegative_body_steps_partial * S ((S (fs_i_dst_ones_exists_lawdivisorfoldnegative_body_steps)) * fs_v_dst_ones_exists_lawdivisorfoldnegative) + (fs_r_dst_ones_exists_lawdivisorfoldnegative_body_steps))) /\ ((((exists fs_h_dst_ones_exists_lawdivisorfoldnegative_body_steps_successor. fs_h_dst_ones_exists_lawdivisorfoldnegative_body_steps_successor + S (fs_s_dst_ones_exists_lawdivisorfoldnegative_body_steps) = S ((S (S fs_i_dst_ones_exists_lawdivisorfoldnegative_body_steps)) * fs_v_dst_ones_exists_lawdivisorfoldnegative)) /\ exists fs_q_dst_ones_exists_lawdivisorfoldnegative_body_steps_successor. fs_u_dst_ones_exists_lawdivisorfoldnegative = fs_q_dst_ones_exists_lawdivisorfoldnegative_body_steps_successor * S ((S (S fs_i_dst_ones_exists_lawdivisorfoldnegative_body_steps)) * fs_v_dst_ones_exists_lawdivisorfoldnegative) + (fs_s_dst_ones_exists_lawdivisorfoldnegative_body_steps))) /\ fs_s_dst_ones_exists_lawdivisorfoldnegative_body_steps = fs_r_dst_ones_exists_lawdivisorfoldnegative_body_steps + fs_a_dst_ones_exists_lawdivisorfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_ones_exists_lawdivisorfoldresult ge_balance_negative_ones_exists_lawdivisorfoldresult. (((((z) = 2 * (ge_balance_positive_ones_exists_lawdivisorfoldresult) /\ (ge_balance_negative_ones_exists_lawdivisorfoldresult) = 0) \/ exists ge_signed_half_ones_exists_lawdivisorfoldresultdecode. (((z) = 2 * ge_signed_half_ones_exists_lawdivisorfoldresultdecode + 1 /\ (ge_balance_positive_ones_exists_lawdivisorfoldresult) = 0) /\ (ge_balance_negative_ones_exists_lawdivisorfoldresult) = S ge_signed_half_ones_exists_lawdivisorfoldresultdecode))) /\ ((dst_positive_sum_ones_exists_lawdivisorfold) + ge_balance_negative_ones_exists_lawdivisorfoldresult = (dst_negative_sum_ones_exists_lawdivisorfold) + ge_balance_positive_ones_exists_lawdivisorfoldresult))))))))))))) -> (((~((n)=0)) /\ (exists dc_mask_ones_exists_lawconvolution. ((((exists dst_positive_code_ones_exists_lawconvolutionmasktable dst_positive_scale_ones_exists_lawconvolutionmasktable dst_negative_code_ones_exists_lawconvolutionmasktable dst_negative_scale_ones_exists_lawconvolutionmasktable. (((dc_mask_ones_exists_lawconvolution) = (((((dst_positive_code_ones_exists_lawconvolutionmasktable) + (dst_positive_scale_ones_exists_lawconvolutionmasktable)) * S ((dst_positive_code_ones_exists_lawconvolutionmasktable) + (dst_positive_scale_ones_exists_lawconvolutionmasktable)) + ((dst_positive_scale_ones_exists_lawconvolutionmasktable) + (dst_positive_scale_ones_exists_lawconvolutionmasktable))) + (((dst_negative_code_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)) * S ((dst_negative_code_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)) + ((dst_negative_scale_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)))) * S ((((dst_positive_code_ones_exists_lawconvolutionmasktable) + (dst_positive_scale_ones_exists_lawconvolutionmasktable)) * S ((dst_positive_code_ones_exists_lawconvolutionmasktable) + (dst_positive_scale_ones_exists_lawconvolutionmasktable)) + ((dst_positive_scale_ones_exists_lawconvolutionmasktable) + (dst_positive_scale_ones_exists_lawconvolutionmasktable))) + (((dst_negative_code_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)) * S ((dst_negative_code_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)) + ((dst_negative_scale_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)))) + ((((dst_negative_code_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)) * S ((dst_negative_code_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)) + ((dst_negative_scale_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable))) + (((dst_negative_code_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)) * S ((dst_negative_code_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)) + ((dst_negative_scale_ones_exists_lawconvolutionmasktable) + (dst_negative_scale_ones_exists_lawconvolutionmasktable)))))) /\ (forall dst_index_ones_exists_lawconvolutionmasktable. (exists pvs_le_gap_ones_exists_lawconvolutionmasktabledomain. pvs_le_gap_ones_exists_lawconvolutionmasktabledomain + (dst_index_ones_exists_lawconvolutionmasktable) = (n)) -> exists dst_positive_ones_exists_lawconvolutionmasktable dst_negative_ones_exists_lawconvolutionmasktable dst_value_ones_exists_lawconvolutionmasktable. ((((exists ff_h_pvs_ones_exists_lawconvolutionmasktableentrypositive. ff_h_pvs_ones_exists_lawconvolutionmasktableentrypositive + S (dst_positive_ones_exists_lawconvolutionmasktable) = S ((S (dst_index_ones_exists_lawconvolutionmasktable)) * dst_positive_scale_ones_exists_lawconvolutionmasktable)) /\ exists ff_q_pvs_ones_exists_lawconvolutionmasktableentrypositive. dst_positive_code_ones_exists_lawconvolutionmasktable = ff_q_pvs_ones_exists_lawconvolutionmasktableentrypositive * S ((S (dst_index_ones_exists_lawconvolutionmasktable)) * dst_positive_scale_ones_exists_lawconvolutionmasktable) + (dst_positive_ones_exists_lawconvolutionmasktable))) /\ (((((exists ff_h_pvs_ones_exists_lawconvolutionmasktableentrynegative. ff_h_pvs_ones_exists_lawconvolutionmasktableentrynegative + S (dst_negative_ones_exists_lawconvolutionmasktable) = S ((S (dst_index_ones_exists_lawconvolutionmasktable)) * dst_negative_scale_ones_exists_lawconvolutionmasktable)) /\ exists ff_q_pvs_ones_exists_lawconvolutionmasktableentrynegative. dst_negative_code_ones_exists_lawconvolutionmasktable = ff_q_pvs_ones_exists_lawconvolutionmasktableentrynegative * S ((S (dst_index_ones_exists_lawconvolutionmasktable)) * dst_negative_scale_ones_exists_lawconvolutionmasktable) + (dst_negative_ones_exists_lawconvolutionmasktable))) /\ (exists ge_balance_positive_ones_exists_lawconvolutionmasktableentryvalue ge_balance_negative_ones_exists_lawconvolutionmasktableentryvalue. (((((dst_value_ones_exists_lawconvolutionmasktable) = 2 * (ge_balance_positive_ones_exists_lawconvolutionmasktableentryvalue) /\ (ge_balance_negative_ones_exists_lawconvolutionmasktableentryvalue) = 0) \/ exists ge_signed_half_ones_exists_lawconvolutionmasktableentryvaluedecode. (((dst_value_ones_exists_lawconvolutionmasktable) = 2 * ge_signed_half_ones_exists_lawconvolutionmasktableentryvaluedecode + 1 /\ (ge_balance_positive_ones_exists_lawconvolutionmasktableentryvalue) = 0) /\ (ge_balance_negative_ones_exists_lawconvolutionmasktableentryvalue) = S ge_signed_half_ones_exists_lawconvolutionmasktableentryvaluedecode))) /\ ((dst_positive_ones_exists_lawconvolutionmasktable) + ge_balance_negative_ones_exists_lawconvolutionmasktableentryvalue = (dst_negative_ones_exists_lawconvolutionmasktable) + ge_balance_positive_ones_exists_lawconvolutionmasktableentryvalue))))))))) /\ (forall dc_index_ones_exists_lawconvolutionmask dc_value_ones_exists_lawconvolutionmask. (exists pvs_le_gap_ones_exists_lawconvolutionmaskdomain. pvs_le_gap_ones_exists_lawconvolutionmaskdomain + (dc_index_ones_exists_lawconvolutionmask) = (n)) -> (exists dst_positive_code_ones_exists_lawconvolutionmasklookup dst_positive_scale_ones_exists_lawconvolutionmasklookup dst_negative_code_ones_exists_lawconvolutionmasklookup dst_negative_scale_ones_exists_lawconvolutionmasklookup dst_positive_ones_exists_lawconvolutionmasklookup dst_negative_ones_exists_lawconvolutionmasklookup. (((dc_mask_ones_exists_lawconvolution) = (((((dst_positive_code_ones_exists_lawconvolutionmasklookup) + (dst_positive_scale_ones_exists_lawconvolutionmasklookup)) * S ((dst_positive_code_ones_exists_lawconvolutionmasklookup) + (dst_positive_scale_ones_exists_lawconvolutionmasklookup)) + ((dst_positive_scale_ones_exists_lawconvolutionmasklookup) + (dst_positive_scale_ones_exists_lawconvolutionmasklookup))) + (((dst_negative_code_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)) * S ((dst_negative_code_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)) + ((dst_negative_scale_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)))) * S ((((dst_positive_code_ones_exists_lawconvolutionmasklookup) + (dst_positive_scale_ones_exists_lawconvolutionmasklookup)) * S ((dst_positive_code_ones_exists_lawconvolutionmasklookup) + (dst_positive_scale_ones_exists_lawconvolutionmasklookup)) + ((dst_positive_scale_ones_exists_lawconvolutionmasklookup) + (dst_positive_scale_ones_exists_lawconvolutionmasklookup))) + (((dst_negative_code_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)) * S ((dst_negative_code_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)) + ((dst_negative_scale_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)))) + ((((dst_negative_code_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)) * S ((dst_negative_code_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)) + ((dst_negative_scale_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup))) + (((dst_negative_code_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)) * S ((dst_negative_code_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)) + ((dst_negative_scale_ones_exists_lawconvolutionmasklookup) + (dst_negative_scale_ones_exists_lawconvolutionmasklookup)))))) /\ (((((exists ff_h_pvs_ones_exists_lawconvolutionmasklookuppositive. ff_h_pvs_ones_exists_lawconvolutionmasklookuppositive + S (dst_positive_ones_exists_lawconvolutionmasklookup) = S ((S (dc_index_ones_exists_lawconvolutionmask)) * dst_positive_scale_ones_exists_lawconvolutionmasklookup)) /\ exists ff_q_pvs_ones_exists_lawconvolutionmasklookuppositive. dst_positive_code_ones_exists_lawconvolutionmasklookup = ff_q_pvs_ones_exists_lawconvolutionmasklookuppositive * S ((S (dc_index_ones_exists_lawconvolutionmask)) * dst_positive_scale_ones_exists_lawconvolutionmasklookup) + (dst_positive_ones_exists_lawconvolutionmasklookup))) /\ (((((exists ff_h_pvs_ones_exists_lawconvolutionmasklookupnegative. ff_h_pvs_ones_exists_lawconvolutionmasklookupnegative + S (dst_negative_ones_exists_lawconvolutionmasklookup) = S ((S (dc_index_ones_exists_lawconvolutionmask)) * dst_negative_scale_ones_exists_lawconvolutionmasklookup)) /\ exists ff_q_pvs_ones_exists_lawconvolutionmasklookupnegative. dst_negative_code_ones_exists_lawconvolutionmasklookup = ff_q_pvs_ones_exists_lawconvolutionmasklookupnegative * S ((S (dc_index_ones_exists_lawconvolutionmask)) * dst_negative_scale_ones_exists_lawconvolutionmasklookup) + (dst_negative_ones_exists_lawconvolutionmasklookup))) /\ (exists ge_balance_positive_ones_exists_lawconvolutionmasklookupvalue ge_balance_negative_ones_exists_lawconvolutionmasklookupvalue. (((((dc_value_ones_exists_lawconvolutionmask) = 2 * (ge_balance_positive_ones_exists_lawconvolutionmasklookupvalue) /\ (ge_balance_negative_ones_exists_lawconvolutionmasklookupvalue) = 0) \/ exists ge_signed_half_ones_exists_lawconvolutionmasklookupvaluedecode. (((dc_value_ones_exists_lawconvolutionmask) = 2 * ge_signed_half_ones_exists_lawconvolutionmasklookupvaluedecode + 1 /\ (ge_balance_positive_ones_exists_lawconvolutionmasklookupvalue) = 0) /\ (ge_balance_negative_ones_exists_lawconvolutionmasklookupvalue) = S ge_signed_half_ones_exists_lawconvolutionmasklookupvaluedecode))) /\ ((dst_positive_ones_exists_lawconvolutionmasklookup) + ge_balance_negative_ones_exists_lawconvolutionmasklookupvalue = (dst_negative_ones_exists_lawconvolutionmasklookup) + ge_balance_positive_ones_exists_lawconvolutionmasklookupvalue))))))))) -> ((((~((dc_index_ones_exists_lawconvolutionmask)=0)) /\ (exists dc_quotient_ones_exists_lawconvolutionmaskentry dc_left_ones_exists_lawconvolutionmaskentry dc_right_ones_exists_lawconvolutionmaskentry. (((n)=(dc_index_ones_exists_lawconvolutionmask)*dc_quotient_ones_exists_lawconvolutionmaskentry) /\ (((exists dst_positive_code_ones_exists_lawconvolutionmaskentryleft dst_positive_scale_ones_exists_lawconvolutionmaskentryleft dst_negative_code_ones_exists_lawconvolutionmaskentryleft dst_negative_scale_ones_exists_lawconvolutionmaskentryleft dst_positive_ones_exists_lawconvolutionmaskentryleft dst_negative_ones_exists_lawconvolutionmaskentryleft. (((F) = (((((dst_positive_code_ones_exists_lawconvolutionmaskentryleft) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryleft)) * S ((dst_positive_code_ones_exists_lawconvolutionmaskentryleft) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryleft)) + ((dst_positive_scale_ones_exists_lawconvolutionmaskentryleft) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryleft))) + (((dst_negative_code_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)) * S ((dst_negative_code_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)) + ((dst_negative_scale_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)))) * S ((((dst_positive_code_ones_exists_lawconvolutionmaskentryleft) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryleft)) * S ((dst_positive_code_ones_exists_lawconvolutionmaskentryleft) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryleft)) + ((dst_positive_scale_ones_exists_lawconvolutionmaskentryleft) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryleft))) + (((dst_negative_code_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)) * S ((dst_negative_code_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)) + ((dst_negative_scale_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)))) + ((((dst_negative_code_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)) * S ((dst_negative_code_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)) + ((dst_negative_scale_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft))) + (((dst_negative_code_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)) * S ((dst_negative_code_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)) + ((dst_negative_scale_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)))))) /\ (((((exists ff_h_pvs_ones_exists_lawconvolutionmaskentryleftpositive. ff_h_pvs_ones_exists_lawconvolutionmaskentryleftpositive + S (dst_positive_ones_exists_lawconvolutionmaskentryleft) = S ((S (dc_index_ones_exists_lawconvolutionmask)) * dst_positive_scale_ones_exists_lawconvolutionmaskentryleft)) /\ exists ff_q_pvs_ones_exists_lawconvolutionmaskentryleftpositive. dst_positive_code_ones_exists_lawconvolutionmaskentryleft = ff_q_pvs_ones_exists_lawconvolutionmaskentryleftpositive * S ((S (dc_index_ones_exists_lawconvolutionmask)) * dst_positive_scale_ones_exists_lawconvolutionmaskentryleft) + (dst_positive_ones_exists_lawconvolutionmaskentryleft))) /\ (((((exists ff_h_pvs_ones_exists_lawconvolutionmaskentryleftnegative. ff_h_pvs_ones_exists_lawconvolutionmaskentryleftnegative + S (dst_negative_ones_exists_lawconvolutionmaskentryleft) = S ((S (dc_index_ones_exists_lawconvolutionmask)) * dst_negative_scale_ones_exists_lawconvolutionmaskentryleft)) /\ exists ff_q_pvs_ones_exists_lawconvolutionmaskentryleftnegative. dst_negative_code_ones_exists_lawconvolutionmaskentryleft = ff_q_pvs_ones_exists_lawconvolutionmaskentryleftnegative * S ((S (dc_index_ones_exists_lawconvolutionmask)) * dst_negative_scale_ones_exists_lawconvolutionmaskentryleft) + (dst_negative_ones_exists_lawconvolutionmaskentryleft))) /\ (exists ge_balance_positive_ones_exists_lawconvolutionmaskentryleftvalue ge_balance_negative_ones_exists_lawconvolutionmaskentryleftvalue. (((((dc_left_ones_exists_lawconvolutionmaskentry) = 2 * (ge_balance_positive_ones_exists_lawconvolutionmaskentryleftvalue) /\ (ge_balance_negative_ones_exists_lawconvolutionmaskentryleftvalue) = 0) \/ exists ge_signed_half_ones_exists_lawconvolutionmaskentryleftvaluedecode. (((dc_left_ones_exists_lawconvolutionmaskentry) = 2 * ge_signed_half_ones_exists_lawconvolutionmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_ones_exists_lawconvolutionmaskentryleftvalue) = 0) /\ (ge_balance_negative_ones_exists_lawconvolutionmaskentryleftvalue) = S ge_signed_half_ones_exists_lawconvolutionmaskentryleftvaluedecode))) /\ ((dst_positive_ones_exists_lawconvolutionmaskentryleft) + ge_balance_negative_ones_exists_lawconvolutionmaskentryleftvalue = (dst_negative_ones_exists_lawconvolutionmaskentryleft) + ge_balance_positive_ones_exists_lawconvolutionmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_ones_exists_lawconvolutionmaskentryright dst_positive_scale_ones_exists_lawconvolutionmaskentryright dst_negative_code_ones_exists_lawconvolutionmaskentryright dst_negative_scale_ones_exists_lawconvolutionmaskentryright dst_positive_ones_exists_lawconvolutionmaskentryright dst_negative_ones_exists_lawconvolutionmaskentryright. (((U) = (((((dst_positive_code_ones_exists_lawconvolutionmaskentryright) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryright)) * S ((dst_positive_code_ones_exists_lawconvolutionmaskentryright) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryright)) + ((dst_positive_scale_ones_exists_lawconvolutionmaskentryright) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryright))) + (((dst_negative_code_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)) * S ((dst_negative_code_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)) + ((dst_negative_scale_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)))) * S ((((dst_positive_code_ones_exists_lawconvolutionmaskentryright) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryright)) * S ((dst_positive_code_ones_exists_lawconvolutionmaskentryright) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryright)) + ((dst_positive_scale_ones_exists_lawconvolutionmaskentryright) + (dst_positive_scale_ones_exists_lawconvolutionmaskentryright))) + (((dst_negative_code_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)) * S ((dst_negative_code_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)) + ((dst_negative_scale_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)))) + ((((dst_negative_code_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)) * S ((dst_negative_code_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)) + ((dst_negative_scale_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright))) + (((dst_negative_code_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)) * S ((dst_negative_code_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)) + ((dst_negative_scale_ones_exists_lawconvolutionmaskentryright) + (dst_negative_scale_ones_exists_lawconvolutionmaskentryright)))))) /\ (((((exists ff_h_pvs_ones_exists_lawconvolutionmaskentryrightpositive. ff_h_pvs_ones_exists_lawconvolutionmaskentryrightpositive + S (dst_positive_ones_exists_lawconvolutionmaskentryright) = S ((S (dc_quotient_ones_exists_lawconvolutionmaskentry)) * dst_positive_scale_ones_exists_lawconvolutionmaskentryright)) /\ exists ff_q_pvs_ones_exists_lawconvolutionmaskentryrightpositive. dst_positive_code_ones_exists_lawconvolutionmaskentryright = ff_q_pvs_ones_exists_lawconvolutionmaskentryrightpositive * S ((S (dc_quotient_ones_exists_lawconvolutionmaskentry)) * dst_positive_scale_ones_exists_lawconvolutionmaskentryright) + (dst_positive_ones_exists_lawconvolutionmaskentryright))) /\ (((((exists ff_h_pvs_ones_exists_lawconvolutionmaskentryrightnegative. ff_h_pvs_ones_exists_lawconvolutionmaskentryrightnegative + S (dst_negative_ones_exists_lawconvolutionmaskentryright) = S ((S (dc_quotient_ones_exists_lawconvolutionmaskentry)) * dst_negative_scale_ones_exists_lawconvolutionmaskentryright)) /\ exists ff_q_pvs_ones_exists_lawconvolutionmaskentryrightnegative. dst_negative_code_ones_exists_lawconvolutionmaskentryright = ff_q_pvs_ones_exists_lawconvolutionmaskentryrightnegative * S ((S (dc_quotient_ones_exists_lawconvolutionmaskentry)) * dst_negative_scale_ones_exists_lawconvolutionmaskentryright) + (dst_negative_ones_exists_lawconvolutionmaskentryright))) /\ (exists ge_balance_positive_ones_exists_lawconvolutionmaskentryrightvalue ge_balance_negative_ones_exists_lawconvolutionmaskentryrightvalue. (((((dc_right_ones_exists_lawconvolutionmaskentry) = 2 * (ge_balance_positive_ones_exists_lawconvolutionmaskentryrightvalue) /\ (ge_balance_negative_ones_exists_lawconvolutionmaskentryrightvalue) = 0) \/ exists ge_signed_half_ones_exists_lawconvolutionmaskentryrightvaluedecode. (((dc_right_ones_exists_lawconvolutionmaskentry) = 2 * ge_signed_half_ones_exists_lawconvolutionmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_ones_exists_lawconvolutionmaskentryrightvalue) = 0) /\ (ge_balance_negative_ones_exists_lawconvolutionmaskentryrightvalue) = S ge_signed_half_ones_exists_lawconvolutionmaskentryrightvaluedecode))) /\ ((dst_positive_ones_exists_lawconvolutionmaskentryright) + ge_balance_negative_ones_exists_lawconvolutionmaskentryrightvalue = (dst_negative_ones_exists_lawconvolutionmaskentryright) + ge_balance_positive_ones_exists_lawconvolutionmaskentryrightvalue))))))))) /\ (exists sto_ap_ones_exists_lawconvolutionmaskentryproduct sto_an_ones_exists_lawconvolutionmaskentryproduct sto_bp_ones_exists_lawconvolutionmaskentryproduct sto_bn_ones_exists_lawconvolutionmaskentryproduct sto_cp_ones_exists_lawconvolutionmaskentryproduct sto_cn_ones_exists_lawconvolutionmaskentryproduct. (((((dc_left_ones_exists_lawconvolutionmaskentry) = 2 * (sto_ap_ones_exists_lawconvolutionmaskentryproduct) /\ (sto_an_ones_exists_lawconvolutionmaskentryproduct) = 0) \/ exists ge_signed_half_ones_exists_lawconvolutionmaskentryproductleft. (((dc_left_ones_exists_lawconvolutionmaskentry) = 2 * ge_signed_half_ones_exists_lawconvolutionmaskentryproductleft + 1 /\ (sto_ap_ones_exists_lawconvolutionmaskentryproduct) = 0) /\ (sto_an_ones_exists_lawconvolutionmaskentryproduct) = S ge_signed_half_ones_exists_lawconvolutionmaskentryproductleft))) /\ ((((((dc_right_ones_exists_lawconvolutionmaskentry) = 2 * (sto_bp_ones_exists_lawconvolutionmaskentryproduct) /\ (sto_bn_ones_exists_lawconvolutionmaskentryproduct) = 0) \/ exists ge_signed_half_ones_exists_lawconvolutionmaskentryproductright. (((dc_right_ones_exists_lawconvolutionmaskentry) = 2 * ge_signed_half_ones_exists_lawconvolutionmaskentryproductright + 1 /\ (sto_bp_ones_exists_lawconvolutionmaskentryproduct) = 0) /\ (sto_bn_ones_exists_lawconvolutionmaskentryproduct) = S ge_signed_half_ones_exists_lawconvolutionmaskentryproductright))) /\ ((((((dc_value_ones_exists_lawconvolutionmask) = 2 * (sto_cp_ones_exists_lawconvolutionmaskentryproduct) /\ (sto_cn_ones_exists_lawconvolutionmaskentryproduct) = 0) \/ exists ge_signed_half_ones_exists_lawconvolutionmaskentryproductoutput. (((dc_value_ones_exists_lawconvolutionmask) = 2 * ge_signed_half_ones_exists_lawconvolutionmaskentryproductoutput + 1 /\ (sto_cp_ones_exists_lawconvolutionmaskentryproduct) = 0) /\ (sto_cn_ones_exists_lawconvolutionmaskentryproduct) = S ge_signed_half_ones_exists_lawconvolutionmaskentryproductoutput))) /\ ((sto_ap_ones_exists_lawconvolutionmaskentryproduct * sto_bp_ones_exists_lawconvolutionmaskentryproduct + sto_an_ones_exists_lawconvolutionmaskentryproduct * sto_bn_ones_exists_lawconvolutionmaskentryproduct) + sto_cn_ones_exists_lawconvolutionmaskentryproduct = (sto_ap_ones_exists_lawconvolutionmaskentryproduct * sto_bn_ones_exists_lawconvolutionmaskentryproduct + sto_an_ones_exists_lawconvolutionmaskentryproduct * sto_bp_ones_exists_lawconvolutionmaskentryproduct) + sto_cp_ones_exists_lawconvolutionmaskentryproduct))))))))))))))) \/ ((((dc_index_ones_exists_lawconvolutionmask)=0 \/ ~(exists pvs_factor_ones_exists_lawconvolutionmaskentrynondivisor. (n) = (dc_index_ones_exists_lawconvolutionmask) * pvs_factor_ones_exists_lawconvolutionmaskentrynondivisor)) /\ ((dc_value_ones_exists_lawconvolutionmask)=0))))))) /\ (exists dst_positive_code_ones_exists_lawconvolutionfold dst_positive_scale_ones_exists_lawconvolutionfold dst_negative_code_ones_exists_lawconvolutionfold dst_negative_scale_ones_exists_lawconvolutionfold dst_positive_sum_ones_exists_lawconvolutionfold dst_negative_sum_ones_exists_lawconvolutionfold. (((dc_mask_ones_exists_lawconvolution) = (((((dst_positive_code_ones_exists_lawconvolutionfold) + (dst_positive_scale_ones_exists_lawconvolutionfold)) * S ((dst_positive_code_ones_exists_lawconvolutionfold) + (dst_positive_scale_ones_exists_lawconvolutionfold)) + ((dst_positive_scale_ones_exists_lawconvolutionfold) + (dst_positive_scale_ones_exists_lawconvolutionfold))) + (((dst_negative_code_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)) * S ((dst_negative_code_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)) + ((dst_negative_scale_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)))) * S ((((dst_positive_code_ones_exists_lawconvolutionfold) + (dst_positive_scale_ones_exists_lawconvolutionfold)) * S ((dst_positive_code_ones_exists_lawconvolutionfold) + (dst_positive_scale_ones_exists_lawconvolutionfold)) + ((dst_positive_scale_ones_exists_lawconvolutionfold) + (dst_positive_scale_ones_exists_lawconvolutionfold))) + (((dst_negative_code_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)) * S ((dst_negative_code_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)) + ((dst_negative_scale_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)))) + ((((dst_negative_code_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)) * S ((dst_negative_code_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)) + ((dst_negative_scale_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold))) + (((dst_negative_code_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)) * S ((dst_negative_code_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)) + ((dst_negative_scale_ones_exists_lawconvolutionfold) + (dst_negative_scale_ones_exists_lawconvolutionfold)))))) /\ (((exists fs_u_dst_ones_exists_lawconvolutionfoldpositive fs_v_dst_ones_exists_lawconvolutionfoldpositive. ((((exists fs_h_dst_ones_exists_lawconvolutionfoldpositive_body_start. fs_h_dst_ones_exists_lawconvolutionfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_ones_exists_lawconvolutionfoldpositive)) /\ exists fs_q_dst_ones_exists_lawconvolutionfoldpositive_body_start. fs_u_dst_ones_exists_lawconvolutionfoldpositive = fs_q_dst_ones_exists_lawconvolutionfoldpositive_body_start * S ((S (0)) * fs_v_dst_ones_exists_lawconvolutionfoldpositive) + (0))) /\ ((((exists fs_h_dst_ones_exists_lawconvolutionfoldpositive_body_terminal. fs_h_dst_ones_exists_lawconvolutionfoldpositive_body_terminal + S (dst_positive_sum_ones_exists_lawconvolutionfold) = S ((S (S (n))) * fs_v_dst_ones_exists_lawconvolutionfoldpositive)) /\ exists fs_q_dst_ones_exists_lawconvolutionfoldpositive_body_terminal. fs_u_dst_ones_exists_lawconvolutionfoldpositive = fs_q_dst_ones_exists_lawconvolutionfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_ones_exists_lawconvolutionfoldpositive) + (dst_positive_sum_ones_exists_lawconvolutionfold))) /\ forall fs_i_dst_ones_exists_lawconvolutionfoldpositive_body_steps. (exists fs_lt_dst_ones_exists_lawconvolutionfoldpositive_body_steps_bound. fs_lt_dst_ones_exists_lawconvolutionfoldpositive_body_steps_bound + S fs_i_dst_ones_exists_lawconvolutionfoldpositive_body_steps = S (n)) -> exists fs_a_dst_ones_exists_lawconvolutionfoldpositive_body_steps fs_r_dst_ones_exists_lawconvolutionfoldpositive_body_steps fs_s_dst_ones_exists_lawconvolutionfoldpositive_body_steps. ((((exists fs_h_dst_ones_exists_lawconvolutionfoldpositive_body_steps_summand. fs_h_dst_ones_exists_lawconvolutionfoldpositive_body_steps_summand + S (fs_a_dst_ones_exists_lawconvolutionfoldpositive_body_steps) = S ((S (fs_i_dst_ones_exists_lawconvolutionfoldpositive_body_steps)) * dst_positive_scale_ones_exists_lawconvolutionfold)) /\ exists fs_q_dst_ones_exists_lawconvolutionfoldpositive_body_steps_summand. dst_positive_code_ones_exists_lawconvolutionfold = fs_q_dst_ones_exists_lawconvolutionfoldpositive_body_steps_summand * S ((S (fs_i_dst_ones_exists_lawconvolutionfoldpositive_body_steps)) * dst_positive_scale_ones_exists_lawconvolutionfold) + (fs_a_dst_ones_exists_lawconvolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_ones_exists_lawconvolutionfoldpositive_body_steps_partial. fs_h_dst_ones_exists_lawconvolutionfoldpositive_body_steps_partial + S (fs_r_dst_ones_exists_lawconvolutionfoldpositive_body_steps) = S ((S (fs_i_dst_ones_exists_lawconvolutionfoldpositive_body_steps)) * fs_v_dst_ones_exists_lawconvolutionfoldpositive)) /\ exists fs_q_dst_ones_exists_lawconvolutionfoldpositive_body_steps_partial. fs_u_dst_ones_exists_lawconvolutionfoldpositive = fs_q_dst_ones_exists_lawconvolutionfoldpositive_body_steps_partial * S ((S (fs_i_dst_ones_exists_lawconvolutionfoldpositive_body_steps)) * fs_v_dst_ones_exists_lawconvolutionfoldpositive) + (fs_r_dst_ones_exists_lawconvolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_ones_exists_lawconvolutionfoldpositive_body_steps_successor. fs_h_dst_ones_exists_lawconvolutionfoldpositive_body_steps_successor + S (fs_s_dst_ones_exists_lawconvolutionfoldpositive_body_steps) = S ((S (S fs_i_dst_ones_exists_lawconvolutionfoldpositive_body_steps)) * fs_v_dst_ones_exists_lawconvolutionfoldpositive)) /\ exists fs_q_dst_ones_exists_lawconvolutionfoldpositive_body_steps_successor. fs_u_dst_ones_exists_lawconvolutionfoldpositive = fs_q_dst_ones_exists_lawconvolutionfoldpositive_body_steps_successor * S ((S (S fs_i_dst_ones_exists_lawconvolutionfoldpositive_body_steps)) * fs_v_dst_ones_exists_lawconvolutionfoldpositive) + (fs_s_dst_ones_exists_lawconvolutionfoldpositive_body_steps))) /\ fs_s_dst_ones_exists_lawconvolutionfoldpositive_body_steps = fs_r_dst_ones_exists_lawconvolutionfoldpositive_body_steps + fs_a_dst_ones_exists_lawconvolutionfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_ones_exists_lawconvolutionfoldnegative fs_v_dst_ones_exists_lawconvolutionfoldnegative. ((((exists fs_h_dst_ones_exists_lawconvolutionfoldnegative_body_start. fs_h_dst_ones_exists_lawconvolutionfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_ones_exists_lawconvolutionfoldnegative)) /\ exists fs_q_dst_ones_exists_lawconvolutionfoldnegative_body_start. fs_u_dst_ones_exists_lawconvolutionfoldnegative = fs_q_dst_ones_exists_lawconvolutionfoldnegative_body_start * S ((S (0)) * fs_v_dst_ones_exists_lawconvolutionfoldnegative) + (0))) /\ ((((exists fs_h_dst_ones_exists_lawconvolutionfoldnegative_body_terminal. fs_h_dst_ones_exists_lawconvolutionfoldnegative_body_terminal + S (dst_negative_sum_ones_exists_lawconvolutionfold) = S ((S (S (n))) * fs_v_dst_ones_exists_lawconvolutionfoldnegative)) /\ exists fs_q_dst_ones_exists_lawconvolutionfoldnegative_body_terminal. fs_u_dst_ones_exists_lawconvolutionfoldnegative = fs_q_dst_ones_exists_lawconvolutionfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_ones_exists_lawconvolutionfoldnegative) + (dst_negative_sum_ones_exists_lawconvolutionfold))) /\ forall fs_i_dst_ones_exists_lawconvolutionfoldnegative_body_steps. (exists fs_lt_dst_ones_exists_lawconvolutionfoldnegative_body_steps_bound. fs_lt_dst_ones_exists_lawconvolutionfoldnegative_body_steps_bound + S fs_i_dst_ones_exists_lawconvolutionfoldnegative_body_steps = S (n)) -> exists fs_a_dst_ones_exists_lawconvolutionfoldnegative_body_steps fs_r_dst_ones_exists_lawconvolutionfoldnegative_body_steps fs_s_dst_ones_exists_lawconvolutionfoldnegative_body_steps. ((((exists fs_h_dst_ones_exists_lawconvolutionfoldnegative_body_steps_summand. fs_h_dst_ones_exists_lawconvolutionfoldnegative_body_steps_summand + S (fs_a_dst_ones_exists_lawconvolutionfoldnegative_body_steps) = S ((S (fs_i_dst_ones_exists_lawconvolutionfoldnegative_body_steps)) * dst_negative_scale_ones_exists_lawconvolutionfold)) /\ exists fs_q_dst_ones_exists_lawconvolutionfoldnegative_body_steps_summand. dst_negative_code_ones_exists_lawconvolutionfold = fs_q_dst_ones_exists_lawconvolutionfoldnegative_body_steps_summand * S ((S (fs_i_dst_ones_exists_lawconvolutionfoldnegative_body_steps)) * dst_negative_scale_ones_exists_lawconvolutionfold) + (fs_a_dst_ones_exists_lawconvolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_ones_exists_lawconvolutionfoldnegative_body_steps_partial. fs_h_dst_ones_exists_lawconvolutionfoldnegative_body_steps_partial + S (fs_r_dst_ones_exists_lawconvolutionfoldnegative_body_steps) = S ((S (fs_i_dst_ones_exists_lawconvolutionfoldnegative_body_steps)) * fs_v_dst_ones_exists_lawconvolutionfoldnegative)) /\ exists fs_q_dst_ones_exists_lawconvolutionfoldnegative_body_steps_partial. fs_u_dst_ones_exists_lawconvolutionfoldnegative = fs_q_dst_ones_exists_lawconvolutionfoldnegative_body_steps_partial * S ((S (fs_i_dst_ones_exists_lawconvolutionfoldnegative_body_steps)) * fs_v_dst_ones_exists_lawconvolutionfoldnegative) + (fs_r_dst_ones_exists_lawconvolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_ones_exists_lawconvolutionfoldnegative_body_steps_successor. fs_h_dst_ones_exists_lawconvolutionfoldnegative_body_steps_successor + S (fs_s_dst_ones_exists_lawconvolutionfoldnegative_body_steps) = S ((S (S fs_i_dst_ones_exists_lawconvolutionfoldnegative_body_steps)) * fs_v_dst_ones_exists_lawconvolutionfoldnegative)) /\ exists fs_q_dst_ones_exists_lawconvolutionfoldnegative_body_steps_successor. fs_u_dst_ones_exists_lawconvolutionfoldnegative = fs_q_dst_ones_exists_lawconvolutionfoldnegative_body_steps_successor * S ((S (S fs_i_dst_ones_exists_lawconvolutionfoldnegative_body_steps)) * fs_v_dst_ones_exists_lawconvolutionfoldnegative) + (fs_s_dst_ones_exists_lawconvolutionfoldnegative_body_steps))) /\ fs_s_dst_ones_exists_lawconvolutionfoldnegative_body_steps = fs_r_dst_ones_exists_lawconvolutionfoldnegative_body_steps + fs_a_dst_ones_exists_lawconvolutionfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_ones_exists_lawconvolutionfoldresult ge_balance_negative_ones_exists_lawconvolutionfoldresult. (((((z) = 2 * (ge_balance_positive_ones_exists_lawconvolutionfoldresult) /\ (ge_balance_negative_ones_exists_lawconvolutionfoldresult) = 0) \/ exists ge_signed_half_ones_exists_lawconvolutionfoldresultdecode. (((z) = 2 * ge_signed_half_ones_exists_lawconvolutionfoldresultdecode + 1 /\ (ge_balance_positive_ones_exists_lawconvolutionfoldresult) = 0) /\ (ge_balance_negative_ones_exists_lawconvolutionfoldresult) = S ge_signed_half_ones_exists_lawconvolutionfoldresultdecode))) /\ ((dst_positive_sum_ones_exists_lawconvolutionfold) + ge_balance_negative_ones_exists_lawconvolutionfoldresult = (dst_negative_sum_ones_exists_lawconvolutionfold) + ge_balance_positive_ones_exists_lawconvolutionfoldresult))))))))))))))))))))Complete tactic proof in conservative notation
All 29 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
29 script commands · 10 reading checkpoints · 1 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (2)
01Fix variables and assumptionsL1–4
02Establish huL5–8
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet constant one table exists.
- L5
have hu : ∃ U. ConstantOneTable(N,U) ∧ ArithAt(U,0,w)Definitions: ConstantOneTable(N,U)ArithAt(U,0,w)Original native command in the exact edition - L6
specialize dirichlet_constant_one_table_exists (N) - L7
specialize dirichlet_constant_one_table_exists (w) - L8
apply dirichlet_constant_one_table_exists
03Separate the logical casesL9–10
04Construct an explicit witnessL11–11
Supply the displayed value, then prove that it has the required property.
- L11
exists x
05Separate the logical casesL12–12
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L12
split
06Use earlier factsL13–13
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L13
exact hu_witness_left
07Separate the logical casesL14–14
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L14
split
08Use earlier factsL15–15
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L15
exact hu_witness_right
09Fix variables and assumptionsL16–19
10Use earlier factsL20–29
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L20
specialize dirichlet_constant_one_sum_iff (N) - L21
specialize dirichlet_constant_one_sum_iff (F) - L22
specialize dirichlet_constant_one_sum_iff (x) - L23
specialize dirichlet_constant_one_sum_iff (n) - L24
specialize dirichlet_constant_one_sum_iff (z) - L25
apply dirichlet_constant_one_sum_iff - L26
exact hf - L27
exact hu_witness_left - L28
exact hn - L29
exact hb
Original defined command ledger · 29 lines
- 0001
intro N - 0002
intro F - 0003
intro w - 0004
intro hf - 0005
have hu : ∃ U. ConstantOneTable(N,U) ∧ ArithAt(U,0,w) - 0006
specialize dirichlet_constant_one_table_exists (N) - 0007
specialize dirichlet_constant_one_table_exists (w) - 0008
apply dirichlet_constant_one_table_exists - 0009
cases hu - 0010
cases hu_witness - 0011
exists x - 0012
split - 0013
exact hu_witness_left - 0014
split - 0015
exact hu_witness_right - 0016
intro n - 0017
intro z - 0018
intro hn - 0019
intro hb - 0020
specialize dirichlet_constant_one_sum_iff (N) - 0021
specialize dirichlet_constant_one_sum_iff (F) - 0022
specialize dirichlet_constant_one_sum_iff (x) - 0023
specialize dirichlet_constant_one_sum_iff (n) - 0024
specialize dirichlet_constant_one_sum_iff (z) - 0025
apply dirichlet_constant_one_sum_iff - 0026
exact hf - 0027
exact hu_witness_left - 0028
exact hn - 0029
exact hb