jordan_primitive_tuple_transport

Exact expanded first-order arithmetic statement

forall n b c d e k. (forall jt_index_pr_equal jt_left_pr_equal jt_right_pr_equal. (exists jt_gap_pr_equalindex. jt_gap_pr_equalindex+S (jt_index_pr_equal)=(k)) -> (((exists fs_h_jt_pr_equalleft. fs_h_jt_pr_equalleft + S (jt_left_pr_equal) = S ((S (jt_index_pr_equal)) * c)) /\ exists fs_q_jt_pr_equalleft. b = fs_q_jt_pr_equalleft * S ((S (jt_index_pr_equal)) * c) + (jt_left_pr_equal))) -> (((exists fs_h_jt_pr_equalright. fs_h_jt_pr_equalright + S (jt_right_pr_equal) = S ((S (jt_index_pr_equal)) * e)) /\ exists fs_q_jt_pr_equalright. d = fs_q_jt_pr_equalright * S ((S (jt_index_pr_equal)) * e) + (jt_right_pr_equal))) -> jt_left_pr_equal=jt_right_pr_equal) -> (forall jt_divisor_prsource. (exists jt_factor_prsourcemodulus. (n)=(jt_divisor_prsource)*jt_factor_prsourcemodulus) -> (forall jt_index_prsourcecoordinates jt_value_prsourcecoordinates. (exists jt_gap_prsourcecoordinatesindex. jt_gap_prsourcecoordinatesindex+S (jt_index_prsourcecoordinates)=(k)) -> (((exists fs_h_jt_prsourcecoordinatesat. fs_h_jt_prsourcecoordinatesat + S (jt_value_prsourcecoordinates) = S ((S (jt_index_prsourcecoordinates)) * c)) /\ exists fs_q_jt_prsourcecoordinatesat. b = fs_q_jt_prsourcecoordinatesat * S ((S (jt_index_prsourcecoordinates)) * c) + (jt_value_prsourcecoordinates))) -> (exists jt_factor_prsourcecoordinatesdivides. (jt_value_prsourcecoordinates)=(jt_divisor_prsource)*jt_factor_prsourcecoordinatesdivides)) -> jt_divisor_prsource=1) -> (forall jt_divisor_prtarget. (exists jt_factor_prtargetmodulus. (n)=(jt_divisor_prtarget)*jt_factor_prtargetmodulus) -> (forall jt_index_prtargetcoordinates jt_value_prtargetcoordinates. (exists jt_gap_prtargetcoordinatesindex. jt_gap_prtargetcoordinatesindex+S (jt_index_prtargetcoordinates)=(k)) -> (((exists fs_h_jt_prtargetcoordinatesat. fs_h_jt_prtargetcoordinatesat + S (jt_value_prtargetcoordinates) = S ((S (jt_index_prtargetcoordinates)) * e)) /\ exists fs_q_jt_prtargetcoordinatesat. d = fs_q_jt_prtargetcoordinatesat * S ((S (jt_index_prtargetcoordinates)) * e) + (jt_value_prtargetcoordinates))) -> (exists jt_factor_prtargetcoordinatesdivides. (jt_value_prtargetcoordinates)=(jt_divisor_prtarget)*jt_factor_prtargetcoordinatesdivides)) -> jt_divisor_prtarget=1)