jordan_tuple_equal_drop_last

Exact expanded first-order arithmetic statement

forall b c d e k. (forall jt_index_eqdropsource jt_left_eqdropsource jt_right_eqdropsource. (exists jt_gap_eqdropsourceindex. jt_gap_eqdropsourceindex+S (jt_index_eqdropsource)=(S k)) -> (((exists fs_h_jt_eqdropsourceleft. fs_h_jt_eqdropsourceleft + S (jt_left_eqdropsource) = S ((S (jt_index_eqdropsource)) * c)) /\ exists fs_q_jt_eqdropsourceleft. b = fs_q_jt_eqdropsourceleft * S ((S (jt_index_eqdropsource)) * c) + (jt_left_eqdropsource))) -> (((exists fs_h_jt_eqdropsourceright. fs_h_jt_eqdropsourceright + S (jt_right_eqdropsource) = S ((S (jt_index_eqdropsource)) * e)) /\ exists fs_q_jt_eqdropsourceright. d = fs_q_jt_eqdropsourceright * S ((S (jt_index_eqdropsource)) * e) + (jt_right_eqdropsource))) -> jt_left_eqdropsource=jt_right_eqdropsource) -> (forall jt_index_eqdroptarget jt_left_eqdroptarget jt_right_eqdroptarget. (exists jt_gap_eqdroptargetindex. jt_gap_eqdroptargetindex+S (jt_index_eqdroptarget)=(k)) -> (((exists fs_h_jt_eqdroptargetleft. fs_h_jt_eqdroptargetleft + S (jt_left_eqdroptarget) = S ((S (jt_index_eqdroptarget)) * c)) /\ exists fs_q_jt_eqdroptargetleft. b = fs_q_jt_eqdroptargetleft * S ((S (jt_index_eqdroptarget)) * c) + (jt_left_eqdroptarget))) -> (((exists fs_h_jt_eqdroptargetright. fs_h_jt_eqdroptargetright + S (jt_right_eqdroptarget) = S ((S (jt_index_eqdroptarget)) * e)) /\ exists fs_q_jt_eqdroptargetright. d = fs_q_jt_eqdroptargetright * S ((S (jt_index_eqdroptarget)) * e) + (jt_right_eqdroptarget))) -> jt_left_eqdroptarget=jt_right_eqdroptarget)