jordan_canonical_crt_tuple_unique

Exact expanded first-order arithmetic statement

forall m n b c d e f g h s k. (forall jt_divisor_uniquecrtcop. (exists jt_factor_uniquecrtcopa. (m)=(jt_divisor_uniquecrtcop)*jt_factor_uniquecrtcopa) -> (exists jt_factor_uniquecrtcopb. (n)=(jt_divisor_uniquecrtcop)*jt_factor_uniquecrtcopb) -> jt_divisor_uniquecrtcop=1) -> (((forall jt_index_uniquecrtfirstbound. (exists jt_gap_uniquecrtfirstboundindex. jt_gap_uniquecrtfirstboundindex+S (jt_index_uniquecrtfirstbound)=(k)) -> exists jt_value_uniquecrtfirstbound. ((((exists fs_h_jt_uniquecrtfirstboundat. fs_h_jt_uniquecrtfirstboundat + S (jt_value_uniquecrtfirstbound) = S ((S (jt_index_uniquecrtfirstbound)) * g)) /\ exists fs_q_jt_uniquecrtfirstboundat. f = fs_q_jt_uniquecrtfirstboundat * S ((S (jt_index_uniquecrtfirstbound)) * g) + (jt_value_uniquecrtfirstbound))) /\ (exists jt_gap_uniquecrtfirstboundvalue. jt_gap_uniquecrtfirstboundvalue+S (jt_value_uniquecrtfirstbound)=(m*n)))) /\ (((forall jt_index_uniquecrtfirstleft jt_left_uniquecrtfirstleft jt_right_uniquecrtfirstleft. (exists jt_gap_uniquecrtfirstleftindex. jt_gap_uniquecrtfirstleftindex+S (jt_index_uniquecrtfirstleft)=(k)) -> (((exists fs_h_jt_uniquecrtfirstleftleft. fs_h_jt_uniquecrtfirstleftleft + S (jt_left_uniquecrtfirstleft) = S ((S (jt_index_uniquecrtfirstleft)) * g)) /\ exists fs_q_jt_uniquecrtfirstleftleft. f = fs_q_jt_uniquecrtfirstleftleft * S ((S (jt_index_uniquecrtfirstleft)) * g) + (jt_left_uniquecrtfirstleft))) -> (((exists fs_h_jt_uniquecrtfirstleftright. fs_h_jt_uniquecrtfirstleftright + S (jt_right_uniquecrtfirstleft) = S ((S (jt_index_uniquecrtfirstleft)) * c)) /\ exists fs_q_jt_uniquecrtfirstleftright. b = fs_q_jt_uniquecrtfirstleftright * S ((S (jt_index_uniquecrtfirstleft)) * c) + (jt_right_uniquecrtfirstleft))) -> (exists jt_left_uniquecrtfirstleftmod jt_right_uniquecrtfirstleftmod. (jt_left_uniquecrtfirstleft)+(m)*jt_left_uniquecrtfirstleftmod=(jt_right_uniquecrtfirstleft)+(m)*jt_right_uniquecrtfirstleftmod)) /\ (forall jt_index_uniquecrtfirstright jt_left_uniquecrtfirstright jt_right_uniquecrtfirstright. (exists jt_gap_uniquecrtfirstrightindex. jt_gap_uniquecrtfirstrightindex+S (jt_index_uniquecrtfirstright)=(k)) -> (((exists fs_h_jt_uniquecrtfirstrightleft. fs_h_jt_uniquecrtfirstrightleft + S (jt_left_uniquecrtfirstright) = S ((S (jt_index_uniquecrtfirstright)) * g)) /\ exists fs_q_jt_uniquecrtfirstrightleft. f = fs_q_jt_uniquecrtfirstrightleft * S ((S (jt_index_uniquecrtfirstright)) * g) + (jt_left_uniquecrtfirstright))) -> (((exists fs_h_jt_uniquecrtfirstrightright. fs_h_jt_uniquecrtfirstrightright + S (jt_right_uniquecrtfirstright) = S ((S (jt_index_uniquecrtfirstright)) * e)) /\ exists fs_q_jt_uniquecrtfirstrightright. d = fs_q_jt_uniquecrtfirstrightright * S ((S (jt_index_uniquecrtfirstright)) * e) + (jt_right_uniquecrtfirstright))) -> (exists jt_left_uniquecrtfirstrightmod jt_right_uniquecrtfirstrightmod. (jt_left_uniquecrtfirstright)+(n)*jt_left_uniquecrtfirstrightmod=(jt_right_uniquecrtfirstright)+(n)*jt_right_uniquecrtfirstrightmod)))))) -> (((forall jt_index_uniquecrtsecondbound. (exists jt_gap_uniquecrtsecondboundindex. jt_gap_uniquecrtsecondboundindex+S (jt_index_uniquecrtsecondbound)=(k)) -> exists jt_value_uniquecrtsecondbound. ((((exists fs_h_jt_uniquecrtsecondboundat. fs_h_jt_uniquecrtsecondboundat + S (jt_value_uniquecrtsecondbound) = S ((S (jt_index_uniquecrtsecondbound)) * s)) /\ exists fs_q_jt_uniquecrtsecondboundat. h = fs_q_jt_uniquecrtsecondboundat * S ((S (jt_index_uniquecrtsecondbound)) * s) + (jt_value_uniquecrtsecondbound))) /\ (exists jt_gap_uniquecrtsecondboundvalue. jt_gap_uniquecrtsecondboundvalue+S (jt_value_uniquecrtsecondbound)=(m*n)))) /\ (((forall jt_index_uniquecrtsecondleft jt_left_uniquecrtsecondleft jt_right_uniquecrtsecondleft. (exists jt_gap_uniquecrtsecondleftindex. jt_gap_uniquecrtsecondleftindex+S (jt_index_uniquecrtsecondleft)=(k)) -> (((exists fs_h_jt_uniquecrtsecondleftleft. fs_h_jt_uniquecrtsecondleftleft + S (jt_left_uniquecrtsecondleft) = S ((S (jt_index_uniquecrtsecondleft)) * s)) /\ exists fs_q_jt_uniquecrtsecondleftleft. h = fs_q_jt_uniquecrtsecondleftleft * S ((S (jt_index_uniquecrtsecondleft)) * s) + (jt_left_uniquecrtsecondleft))) -> (((exists fs_h_jt_uniquecrtsecondleftright. fs_h_jt_uniquecrtsecondleftright + S (jt_right_uniquecrtsecondleft) = S ((S (jt_index_uniquecrtsecondleft)) * c)) /\ exists fs_q_jt_uniquecrtsecondleftright. b = fs_q_jt_uniquecrtsecondleftright * S ((S (jt_index_uniquecrtsecondleft)) * c) + (jt_right_uniquecrtsecondleft))) -> (exists jt_left_uniquecrtsecondleftmod jt_right_uniquecrtsecondleftmod. (jt_left_uniquecrtsecondleft)+(m)*jt_left_uniquecrtsecondleftmod=(jt_right_uniquecrtsecondleft)+(m)*jt_right_uniquecrtsecondleftmod)) /\ (forall jt_index_uniquecrtsecondright jt_left_uniquecrtsecondright jt_right_uniquecrtsecondright. (exists jt_gap_uniquecrtsecondrightindex. jt_gap_uniquecrtsecondrightindex+S (jt_index_uniquecrtsecondright)=(k)) -> (((exists fs_h_jt_uniquecrtsecondrightleft. fs_h_jt_uniquecrtsecondrightleft + S (jt_left_uniquecrtsecondright) = S ((S (jt_index_uniquecrtsecondright)) * s)) /\ exists fs_q_jt_uniquecrtsecondrightleft. h = fs_q_jt_uniquecrtsecondrightleft * S ((S (jt_index_uniquecrtsecondright)) * s) + (jt_left_uniquecrtsecondright))) -> (((exists fs_h_jt_uniquecrtsecondrightright. fs_h_jt_uniquecrtsecondrightright + S (jt_right_uniquecrtsecondright) = S ((S (jt_index_uniquecrtsecondright)) * e)) /\ exists fs_q_jt_uniquecrtsecondrightright. d = fs_q_jt_uniquecrtsecondrightright * S ((S (jt_index_uniquecrtsecondright)) * e) + (jt_right_uniquecrtsecondright))) -> (exists jt_left_uniquecrtsecondrightmod jt_right_uniquecrtsecondrightmod. (jt_left_uniquecrtsecondright)+(n)*jt_left_uniquecrtsecondrightmod=(jt_right_uniquecrtsecondright)+(n)*jt_right_uniquecrtsecondrightmod)))))) -> (forall jt_index_uniquecrtoutputs jt_left_uniquecrtoutputs jt_right_uniquecrtoutputs. (exists jt_gap_uniquecrtoutputsindex. jt_gap_uniquecrtoutputsindex+S (jt_index_uniquecrtoutputs)=(k)) -> (((exists fs_h_jt_uniquecrtoutputsleft. fs_h_jt_uniquecrtoutputsleft + S (jt_left_uniquecrtoutputs) = S ((S (jt_index_uniquecrtoutputs)) * g)) /\ exists fs_q_jt_uniquecrtoutputsleft. f = fs_q_jt_uniquecrtoutputsleft * S ((S (jt_index_uniquecrtoutputs)) * g) + (jt_left_uniquecrtoutputs))) -> (((exists fs_h_jt_uniquecrtoutputsright. fs_h_jt_uniquecrtoutputsright + S (jt_right_uniquecrtoutputs) = S ((S (jt_index_uniquecrtoutputs)) * s)) /\ exists fs_q_jt_uniquecrtoutputsright. h = fs_q_jt_uniquecrtoutputsright * S ((S (jt_index_uniquecrtoutputs)) * s) + (jt_right_uniquecrtoutputs))) -> jt_left_uniquecrtoutputs=jt_right_uniquecrtoutputs)