jordan_tuple_listed_equal_transport

Exact expanded first-order arithmetic statement

forall b c d e k B C D E j. (forall jt_index_listedtransport jt_left_listedtransport jt_right_listedtransport. (exists jt_gap_listedtransportindex. jt_gap_listedtransportindex+S (jt_index_listedtransport)=(k)) -> (((exists fs_h_jt_listedtransportleft. fs_h_jt_listedtransportleft + S (jt_left_listedtransport) = S ((S (jt_index_listedtransport)) * c)) /\ exists fs_q_jt_listedtransportleft. b = fs_q_jt_listedtransportleft * S ((S (jt_index_listedtransport)) * c) + (jt_left_listedtransport))) -> (((exists fs_h_jt_listedtransportright. fs_h_jt_listedtransportright + S (jt_right_listedtransport) = S ((S (jt_index_listedtransport)) * e)) /\ exists fs_q_jt_listedtransportright. d = fs_q_jt_listedtransportright * S ((S (jt_index_listedtransport)) * e) + (jt_right_listedtransport))) -> jt_left_listedtransport=jt_right_listedtransport) -> (exists jt_index_listedsource jt_code_listedsource jt_scale_listedsource. ((exists jt_gap_listedsourceindex. jt_gap_listedsourceindex+S (jt_index_listedsource)=(j)) /\ (((((((exists fs_h_jt_listedsourcecode. fs_h_jt_listedsourcecode + S (jt_code_listedsource) = S ((S (jt_index_listedsource)) * C)) /\ exists fs_q_jt_listedsourcecode. B = fs_q_jt_listedsourcecode * S ((S (jt_index_listedsource)) * C) + (jt_code_listedsource))) /\ (((exists fs_h_jt_listedsourcescale. fs_h_jt_listedsourcescale + S (jt_scale_listedsource) = S ((S (jt_index_listedsource)) * E)) /\ exists fs_q_jt_listedsourcescale. D = fs_q_jt_listedsourcescale * S ((S (jt_index_listedsource)) * E) + (jt_scale_listedsource))))) /\ (forall jt_index_listedsourceequal jt_left_listedsourceequal jt_right_listedsourceequal. (exists jt_gap_listedsourceequalindex. jt_gap_listedsourceequalindex+S (jt_index_listedsourceequal)=(k)) -> (((exists fs_h_jt_listedsourceequalleft. fs_h_jt_listedsourceequalleft + S (jt_left_listedsourceequal) = S ((S (jt_index_listedsourceequal)) * e)) /\ exists fs_q_jt_listedsourceequalleft. d = fs_q_jt_listedsourceequalleft * S ((S (jt_index_listedsourceequal)) * e) + (jt_left_listedsourceequal))) -> (((exists fs_h_jt_listedsourceequalright. fs_h_jt_listedsourceequalright + S (jt_right_listedsourceequal) = S ((S (jt_index_listedsourceequal)) * jt_scale_listedsource)) /\ exists fs_q_jt_listedsourceequalright. jt_code_listedsource = fs_q_jt_listedsourceequalright * S ((S (jt_index_listedsourceequal)) * jt_scale_listedsource) + (jt_right_listedsourceequal))) -> jt_left_listedsourceequal=jt_right_listedsourceequal))))) -> (exists jt_index_listedtarget jt_code_listedtarget jt_scale_listedtarget. ((exists jt_gap_listedtargetindex. jt_gap_listedtargetindex+S (jt_index_listedtarget)=(j)) /\ (((((((exists fs_h_jt_listedtargetcode. fs_h_jt_listedtargetcode + S (jt_code_listedtarget) = S ((S (jt_index_listedtarget)) * C)) /\ exists fs_q_jt_listedtargetcode. B = fs_q_jt_listedtargetcode * S ((S (jt_index_listedtarget)) * C) + (jt_code_listedtarget))) /\ (((exists fs_h_jt_listedtargetscale. fs_h_jt_listedtargetscale + S (jt_scale_listedtarget) = S ((S (jt_index_listedtarget)) * E)) /\ exists fs_q_jt_listedtargetscale. D = fs_q_jt_listedtargetscale * S ((S (jt_index_listedtarget)) * E) + (jt_scale_listedtarget))))) /\ (forall jt_index_listedtargetequal jt_left_listedtargetequal jt_right_listedtargetequal. (exists jt_gap_listedtargetequalindex. jt_gap_listedtargetequalindex+S (jt_index_listedtargetequal)=(k)) -> (((exists fs_h_jt_listedtargetequalleft. fs_h_jt_listedtargetequalleft + S (jt_left_listedtargetequal) = S ((S (jt_index_listedtargetequal)) * c)) /\ exists fs_q_jt_listedtargetequalleft. b = fs_q_jt_listedtargetequalleft * S ((S (jt_index_listedtargetequal)) * c) + (jt_left_listedtargetequal))) -> (((exists fs_h_jt_listedtargetequalright. fs_h_jt_listedtargetequalright + S (jt_right_listedtargetequal) = S ((S (jt_index_listedtargetequal)) * jt_scale_listedtarget)) /\ exists fs_q_jt_listedtargetequalright. jt_code_listedtarget = fs_q_jt_listedtargetequalright * S ((S (jt_index_listedtargetequal)) * jt_scale_listedtarget) + (jt_right_listedtargetequal))) -> jt_left_listedtargetequal=jt_right_listedtargetequal)))))