jordan_tuple_bounded_congruence_equal

Exact expanded first-order arithmetic statement

forall n b c d e k. (forall jt_index_congboundleft. (exists jt_gap_congboundleftindex. jt_gap_congboundleftindex+S (jt_index_congboundleft)=(k)) -> exists jt_value_congboundleft. ((((exists fs_h_jt_congboundleftat. fs_h_jt_congboundleftat + S (jt_value_congboundleft) = S ((S (jt_index_congboundleft)) * c)) /\ exists fs_q_jt_congboundleftat. b = fs_q_jt_congboundleftat * S ((S (jt_index_congboundleft)) * c) + (jt_value_congboundleft))) /\ (exists jt_gap_congboundleftvalue. jt_gap_congboundleftvalue+S (jt_value_congboundleft)=(n)))) -> (forall jt_index_congboundright. (exists jt_gap_congboundrightindex. jt_gap_congboundrightindex+S (jt_index_congboundright)=(k)) -> exists jt_value_congboundright. ((((exists fs_h_jt_congboundrightat. fs_h_jt_congboundrightat + S (jt_value_congboundright) = S ((S (jt_index_congboundright)) * e)) /\ exists fs_q_jt_congboundrightat. d = fs_q_jt_congboundrightat * S ((S (jt_index_congboundright)) * e) + (jt_value_congboundright))) /\ (exists jt_gap_congboundrightvalue. jt_gap_congboundrightvalue+S (jt_value_congboundright)=(n)))) -> (forall jt_index_congboth jt_left_congboth jt_right_congboth. (exists jt_gap_congbothindex. jt_gap_congbothindex+S (jt_index_congboth)=(k)) -> (((exists fs_h_jt_congbothleft. fs_h_jt_congbothleft + S (jt_left_congboth) = S ((S (jt_index_congboth)) * c)) /\ exists fs_q_jt_congbothleft. b = fs_q_jt_congbothleft * S ((S (jt_index_congboth)) * c) + (jt_left_congboth))) -> (((exists fs_h_jt_congbothright. fs_h_jt_congbothright + S (jt_right_congboth) = S ((S (jt_index_congboth)) * e)) /\ exists fs_q_jt_congbothright. d = fs_q_jt_congbothright * S ((S (jt_index_congboth)) * e) + (jt_right_congboth))) -> (exists jt_left_congbothmod jt_right_congbothmod. (jt_left_congboth)+(n)*jt_left_congbothmod=(jt_right_congboth)+(n)*jt_right_congbothmod)) -> (forall jt_index_congequal jt_left_congequal jt_right_congequal. (exists jt_gap_congequalindex. jt_gap_congequalindex+S (jt_index_congequal)=(k)) -> (((exists fs_h_jt_congequalleft. fs_h_jt_congequalleft + S (jt_left_congequal) = S ((S (jt_index_congequal)) * c)) /\ exists fs_q_jt_congequalleft. b = fs_q_jt_congequalleft * S ((S (jt_index_congequal)) * c) + (jt_left_congequal))) -> (((exists fs_h_jt_congequalright. fs_h_jt_congequalright + S (jt_right_congequal) = S ((S (jt_index_congequal)) * e)) /\ exists fs_q_jt_congequalright. d = fs_q_jt_congequalright * S ((S (jt_index_congequal)) * e) + (jt_right_congequal))) -> jt_left_congequal=jt_right_congequal)