jordan_tuple_congruence_symm

Exact expanded first-order arithmetic statement

forall n b c d e k. (forall jt_index_msource jt_left_msource jt_right_msource. (exists jt_gap_msourceindex. jt_gap_msourceindex+S (jt_index_msource)=(k)) -> (((exists fs_h_jt_msourceleft. fs_h_jt_msourceleft + S (jt_left_msource) = S ((S (jt_index_msource)) * c)) /\ exists fs_q_jt_msourceleft. b = fs_q_jt_msourceleft * S ((S (jt_index_msource)) * c) + (jt_left_msource))) -> (((exists fs_h_jt_msourceright. fs_h_jt_msourceright + S (jt_right_msource) = S ((S (jt_index_msource)) * e)) /\ exists fs_q_jt_msourceright. d = fs_q_jt_msourceright * S ((S (jt_index_msource)) * e) + (jt_right_msource))) -> (exists jt_left_msourcemod jt_right_msourcemod. (jt_left_msource)+(n)*jt_left_msourcemod=(jt_right_msource)+(n)*jt_right_msourcemod)) -> (forall jt_index_mtarget jt_left_mtarget jt_right_mtarget. (exists jt_gap_mtargetindex. jt_gap_mtargetindex+S (jt_index_mtarget)=(k)) -> (((exists fs_h_jt_mtargetleft. fs_h_jt_mtargetleft + S (jt_left_mtarget) = S ((S (jt_index_mtarget)) * e)) /\ exists fs_q_jt_mtargetleft. d = fs_q_jt_mtargetleft * S ((S (jt_index_mtarget)) * e) + (jt_left_mtarget))) -> (((exists fs_h_jt_mtargetright. fs_h_jt_mtargetright + S (jt_right_mtarget) = S ((S (jt_index_mtarget)) * c)) /\ exists fs_q_jt_mtargetright. b = fs_q_jt_mtargetright * S ((S (jt_index_mtarget)) * c) + (jt_right_mtarget))) -> (exists jt_left_mtargetmod jt_right_mtargetmod. (jt_left_mtarget)+(n)*jt_left_mtargetmod=(jt_right_mtarget)+(n)*jt_right_mtargetmod))