jordan_tuples_bounded_one_equal

Exact expanded first-order arithmetic statement

forall b c d e k. (forall jt_index_unit_left. (exists jt_gap_unit_leftindex. jt_gap_unit_leftindex+S (jt_index_unit_left)=(k)) -> exists jt_value_unit_left. ((((exists fs_h_jt_unit_leftat. fs_h_jt_unit_leftat + S (jt_value_unit_left) = S ((S (jt_index_unit_left)) * c)) /\ exists fs_q_jt_unit_leftat. b = fs_q_jt_unit_leftat * S ((S (jt_index_unit_left)) * c) + (jt_value_unit_left))) /\ (exists jt_gap_unit_leftvalue. jt_gap_unit_leftvalue+S (jt_value_unit_left)=(1)))) -> (forall jt_index_unit_right. (exists jt_gap_unit_rightindex. jt_gap_unit_rightindex+S (jt_index_unit_right)=(k)) -> exists jt_value_unit_right. ((((exists fs_h_jt_unit_rightat. fs_h_jt_unit_rightat + S (jt_value_unit_right) = S ((S (jt_index_unit_right)) * e)) /\ exists fs_q_jt_unit_rightat. d = fs_q_jt_unit_rightat * S ((S (jt_index_unit_right)) * e) + (jt_value_unit_right))) /\ (exists jt_gap_unit_rightvalue. jt_gap_unit_rightvalue+S (jt_value_unit_right)=(1)))) -> (forall jt_index_unit_equal jt_left_unit_equal jt_right_unit_equal. (exists jt_gap_unit_equalindex. jt_gap_unit_equalindex+S (jt_index_unit_equal)=(k)) -> (((exists fs_h_jt_unit_equalleft. fs_h_jt_unit_equalleft + S (jt_left_unit_equal) = S ((S (jt_index_unit_equal)) * c)) /\ exists fs_q_jt_unit_equalleft. b = fs_q_jt_unit_equalleft * S ((S (jt_index_unit_equal)) * c) + (jt_left_unit_equal))) -> (((exists fs_h_jt_unit_equalright. fs_h_jt_unit_equalright + S (jt_right_unit_equal) = S ((S (jt_index_unit_equal)) * e)) /\ exists fs_q_jt_unit_equalright. d = fs_q_jt_unit_equalright * S ((S (jt_index_unit_equal)) * e) + (jt_right_unit_equal))) -> jt_left_unit_equal=jt_right_unit_equal)