jordan_tuple_prefix_equal

Exact expanded first-order arithmetic statement

forall b c d e k. (forall jt_index_prefixsource jt_value_prefixsource. (exists jt_gap_prefixsourceindex. jt_gap_prefixsourceindex+S (jt_index_prefixsource)=(k)) -> (((exists fs_h_jt_prefixsourceold. fs_h_jt_prefixsourceold + S (jt_value_prefixsource) = S ((S (jt_index_prefixsource)) * c)) /\ exists fs_q_jt_prefixsourceold. b = fs_q_jt_prefixsourceold * S ((S (jt_index_prefixsource)) * c) + (jt_value_prefixsource))) -> (((exists fs_h_jt_prefixsourcenew. fs_h_jt_prefixsourcenew + S (jt_value_prefixsource) = S ((S (jt_index_prefixsource)) * e)) /\ exists fs_q_jt_prefixsourcenew. d = fs_q_jt_prefixsourcenew * S ((S (jt_index_prefixsource)) * e) + (jt_value_prefixsource)))) -> (forall jt_index_prefixtarget jt_left_prefixtarget jt_right_prefixtarget. (exists jt_gap_prefixtargetindex. jt_gap_prefixtargetindex+S (jt_index_prefixtarget)=(k)) -> (((exists fs_h_jt_prefixtargetleft. fs_h_jt_prefixtargetleft + S (jt_left_prefixtarget) = S ((S (jt_index_prefixtarget)) * c)) /\ exists fs_q_jt_prefixtargetleft. b = fs_q_jt_prefixtargetleft * S ((S (jt_index_prefixtarget)) * c) + (jt_left_prefixtarget))) -> (((exists fs_h_jt_prefixtargetright. fs_h_jt_prefixtargetright + S (jt_right_prefixtarget) = S ((S (jt_index_prefixtarget)) * e)) /\ exists fs_q_jt_prefixtargetright. d = fs_q_jt_prefixtargetright * S ((S (jt_index_prefixtarget)) * e) + (jt_right_prefixtarget))) -> jt_left_prefixtarget=jt_right_prefixtarget)