jordan_tuple_listed_lift

Exact expanded first-order arithmetic statement

forall b c k B C D E j. (exists jt_index_listedliftold jt_code_listedliftold jt_scale_listedliftold. ((exists jt_gap_listedliftoldindex. jt_gap_listedliftoldindex+S (jt_index_listedliftold)=(j)) /\ (((((((exists fs_h_jt_listedliftoldcode. fs_h_jt_listedliftoldcode + S (jt_code_listedliftold) = S ((S (jt_index_listedliftold)) * C)) /\ exists fs_q_jt_listedliftoldcode. B = fs_q_jt_listedliftoldcode * S ((S (jt_index_listedliftold)) * C) + (jt_code_listedliftold))) /\ (((exists fs_h_jt_listedliftoldscale. fs_h_jt_listedliftoldscale + S (jt_scale_listedliftold) = S ((S (jt_index_listedliftold)) * E)) /\ exists fs_q_jt_listedliftoldscale. D = fs_q_jt_listedliftoldscale * S ((S (jt_index_listedliftold)) * E) + (jt_scale_listedliftold))))) /\ (forall jt_index_listedliftoldequal jt_left_listedliftoldequal jt_right_listedliftoldequal. (exists jt_gap_listedliftoldequalindex. jt_gap_listedliftoldequalindex+S (jt_index_listedliftoldequal)=(k)) -> (((exists fs_h_jt_listedliftoldequalleft. fs_h_jt_listedliftoldequalleft + S (jt_left_listedliftoldequal) = S ((S (jt_index_listedliftoldequal)) * c)) /\ exists fs_q_jt_listedliftoldequalleft. b = fs_q_jt_listedliftoldequalleft * S ((S (jt_index_listedliftoldequal)) * c) + (jt_left_listedliftoldequal))) -> (((exists fs_h_jt_listedliftoldequalright. fs_h_jt_listedliftoldequalright + S (jt_right_listedliftoldequal) = S ((S (jt_index_listedliftoldequal)) * jt_scale_listedliftold)) /\ exists fs_q_jt_listedliftoldequalright. jt_code_listedliftold = fs_q_jt_listedliftoldequalright * S ((S (jt_index_listedliftoldequal)) * jt_scale_listedliftold) + (jt_right_listedliftoldequal))) -> jt_left_listedliftoldequal=jt_right_listedliftoldequal))))) -> (exists jt_index_listedliftnew jt_code_listedliftnew jt_scale_listedliftnew. ((exists jt_gap_listedliftnewindex. jt_gap_listedliftnewindex+S (jt_index_listedliftnew)=(S j)) /\ (((((((exists fs_h_jt_listedliftnewcode. fs_h_jt_listedliftnewcode + S (jt_code_listedliftnew) = S ((S (jt_index_listedliftnew)) * C)) /\ exists fs_q_jt_listedliftnewcode. B = fs_q_jt_listedliftnewcode * S ((S (jt_index_listedliftnew)) * C) + (jt_code_listedliftnew))) /\ (((exists fs_h_jt_listedliftnewscale. fs_h_jt_listedliftnewscale + S (jt_scale_listedliftnew) = S ((S (jt_index_listedliftnew)) * E)) /\ exists fs_q_jt_listedliftnewscale. D = fs_q_jt_listedliftnewscale * S ((S (jt_index_listedliftnew)) * E) + (jt_scale_listedliftnew))))) /\ (forall jt_index_listedliftnewequal jt_left_listedliftnewequal jt_right_listedliftnewequal. (exists jt_gap_listedliftnewequalindex. jt_gap_listedliftnewequalindex+S (jt_index_listedliftnewequal)=(k)) -> (((exists fs_h_jt_listedliftnewequalleft. fs_h_jt_listedliftnewequalleft + S (jt_left_listedliftnewequal) = S ((S (jt_index_listedliftnewequal)) * c)) /\ exists fs_q_jt_listedliftnewequalleft. b = fs_q_jt_listedliftnewequalleft * S ((S (jt_index_listedliftnewequal)) * c) + (jt_left_listedliftnewequal))) -> (((exists fs_h_jt_listedliftnewequalright. fs_h_jt_listedliftnewequalright + S (jt_right_listedliftnewequal) = S ((S (jt_index_listedliftnewequal)) * jt_scale_listedliftnew)) /\ exists fs_q_jt_listedliftnewequalright. jt_code_listedliftnew = fs_q_jt_listedliftnewequalright * S ((S (jt_index_listedliftnewequal)) * jt_scale_listedliftnew) + (jt_right_listedliftnewequal))) -> jt_left_listedliftnewequal=jt_right_listedliftnewequal)))))