jordan_tuple_scan_append

Exact expanded first-order arithmetic statement

forall k n c t B C D E j. (((forall jt_i_appendinvariant. (exists jt_gap_appendinvariantsoundindex. jt_gap_appendinvariantsoundindex+S (jt_i_appendinvariant)=(j)) -> exists jt_b_appendinvariant jt_e_appendinvariant. ((((((exists fs_h_jt_appendinvariantsoundcode. fs_h_jt_appendinvariantsoundcode + S (jt_b_appendinvariant) = S ((S (jt_i_appendinvariant)) * C)) /\ exists fs_q_jt_appendinvariantsoundcode. B = fs_q_jt_appendinvariantsoundcode * S ((S (jt_i_appendinvariant)) * C) + (jt_b_appendinvariant))) /\ (((exists fs_h_jt_appendinvariantsoundscale. fs_h_jt_appendinvariantsoundscale + S (jt_e_appendinvariant) = S ((S (jt_i_appendinvariant)) * E)) /\ exists fs_q_jt_appendinvariantsoundscale. D = fs_q_jt_appendinvariantsoundscale * S ((S (jt_i_appendinvariant)) * E) + (jt_e_appendinvariant))))) /\ (((forall jt_index_appendinvariantbound. (exists jt_gap_appendinvariantboundindex. jt_gap_appendinvariantboundindex+S (jt_index_appendinvariantbound)=(k)) -> exists jt_value_appendinvariantbound. ((((exists fs_h_jt_appendinvariantboundat. fs_h_jt_appendinvariantboundat + S (jt_value_appendinvariantbound) = S ((S (jt_index_appendinvariantbound)) * jt_e_appendinvariant)) /\ exists fs_q_jt_appendinvariantboundat. jt_b_appendinvariant = fs_q_jt_appendinvariantboundat * S ((S (jt_index_appendinvariantbound)) * jt_e_appendinvariant) + (jt_value_appendinvariantbound))) /\ (exists jt_gap_appendinvariantboundvalue. jt_gap_appendinvariantboundvalue+S (jt_value_appendinvariantbound)=(n)))) /\ (forall jt_divisor_appendinvariantprimitive. (exists jt_factor_appendinvariantprimitivemodulus. (n)=(jt_divisor_appendinvariantprimitive)*jt_factor_appendinvariantprimitivemodulus) -> (forall jt_index_appendinvariantprimitivecoordinates jt_value_appendinvariantprimitivecoordinates. (exists jt_gap_appendinvariantprimitivecoordinatesindex. jt_gap_appendinvariantprimitivecoordinatesindex+S (jt_index_appendinvariantprimitivecoordinates)=(k)) -> (((exists fs_h_jt_appendinvariantprimitivecoordinatesat. fs_h_jt_appendinvariantprimitivecoordinatesat + S (jt_value_appendinvariantprimitivecoordinates) = S ((S (jt_index_appendinvariantprimitivecoordinates)) * jt_e_appendinvariant)) /\ exists fs_q_jt_appendinvariantprimitivecoordinatesat. jt_b_appendinvariant = fs_q_jt_appendinvariantprimitivecoordinatesat * S ((S (jt_index_appendinvariantprimitivecoordinates)) * jt_e_appendinvariant) + (jt_value_appendinvariantprimitivecoordinates))) -> (exists jt_factor_appendinvariantprimitivecoordinatesdivides. (jt_value_appendinvariantprimitivecoordinates)=(jt_divisor_appendinvariantprimitive)*jt_factor_appendinvariantprimitivecoordinatesdivides)) -> jt_divisor_appendinvariantprimitive=1))))) /\ (((forall jt_i_appendinvariant jt_h_appendinvariant jt_b_appendinvariant jt_e_appendinvariant jt_d_appendinvariant jt_f_appendinvariant. (exists jt_gap_appendinvariantfirstindex. jt_gap_appendinvariantfirstindex+S (jt_i_appendinvariant)=(j)) -> (exists jt_gap_appendinvariantsecondindex. jt_gap_appendinvariantsecondindex+S (jt_h_appendinvariant)=(j)) -> (((((exists fs_h_jt_appendinvariantfirstcode. fs_h_jt_appendinvariantfirstcode + S (jt_b_appendinvariant) = S ((S (jt_i_appendinvariant)) * C)) /\ exists fs_q_jt_appendinvariantfirstcode. B = fs_q_jt_appendinvariantfirstcode * S ((S (jt_i_appendinvariant)) * C) + (jt_b_appendinvariant))) /\ (((exists fs_h_jt_appendinvariantfirstscale. fs_h_jt_appendinvariantfirstscale + S (jt_e_appendinvariant) = S ((S (jt_i_appendinvariant)) * E)) /\ exists fs_q_jt_appendinvariantfirstscale. D = fs_q_jt_appendinvariantfirstscale * S ((S (jt_i_appendinvariant)) * E) + (jt_e_appendinvariant))))) -> (((((exists fs_h_jt_appendinvariantsecondcode. fs_h_jt_appendinvariantsecondcode + S (jt_d_appendinvariant) = S ((S (jt_h_appendinvariant)) * C)) /\ exists fs_q_jt_appendinvariantsecondcode. B = fs_q_jt_appendinvariantsecondcode * S ((S (jt_h_appendinvariant)) * C) + (jt_d_appendinvariant))) /\ (((exists fs_h_jt_appendinvariantsecondscale. fs_h_jt_appendinvariantsecondscale + S (jt_f_appendinvariant) = S ((S (jt_h_appendinvariant)) * E)) /\ exists fs_q_jt_appendinvariantsecondscale. D = fs_q_jt_appendinvariantsecondscale * S ((S (jt_h_appendinvariant)) * E) + (jt_f_appendinvariant))))) -> (forall jt_index_appendinvariantsame jt_left_appendinvariantsame jt_right_appendinvariantsame. (exists jt_gap_appendinvariantsameindex. jt_gap_appendinvariantsameindex+S (jt_index_appendinvariantsame)=(k)) -> (((exists fs_h_jt_appendinvariantsameleft. fs_h_jt_appendinvariantsameleft + S (jt_left_appendinvariantsame) = S ((S (jt_index_appendinvariantsame)) * jt_e_appendinvariant)) /\ exists fs_q_jt_appendinvariantsameleft. jt_b_appendinvariant = fs_q_jt_appendinvariantsameleft * S ((S (jt_index_appendinvariantsame)) * jt_e_appendinvariant) + (jt_left_appendinvariantsame))) -> (((exists fs_h_jt_appendinvariantsameright. fs_h_jt_appendinvariantsameright + S (jt_right_appendinvariantsame) = S ((S (jt_index_appendinvariantsame)) * jt_f_appendinvariant)) /\ exists fs_q_jt_appendinvariantsameright. jt_d_appendinvariant = fs_q_jt_appendinvariantsameright * S ((S (jt_index_appendinvariantsame)) * jt_f_appendinvariant) + (jt_right_appendinvariantsame))) -> jt_left_appendinvariantsame=jt_right_appendinvariantsame) -> jt_i_appendinvariant=jt_h_appendinvariant) /\ (forall jt_z_appendinvariant. (exists jt_gap_appendinvariantcodeindex. jt_gap_appendinvariantcodeindex+S (jt_z_appendinvariant)=(t)) -> (forall jt_index_appendinvariantinputbound. (exists jt_gap_appendinvariantinputboundindex. jt_gap_appendinvariantinputboundindex+S (jt_index_appendinvariantinputbound)=(k)) -> exists jt_value_appendinvariantinputbound. ((((exists fs_h_jt_appendinvariantinputboundat. fs_h_jt_appendinvariantinputboundat + S (jt_value_appendinvariantinputbound) = S ((S (jt_index_appendinvariantinputbound)) * c)) /\ exists fs_q_jt_appendinvariantinputboundat. jt_z_appendinvariant = fs_q_jt_appendinvariantinputboundat * S ((S (jt_index_appendinvariantinputbound)) * c) + (jt_value_appendinvariantinputbound))) /\ (exists jt_gap_appendinvariantinputboundvalue. jt_gap_appendinvariantinputboundvalue+S (jt_value_appendinvariantinputbound)=(n)))) -> (forall jt_divisor_appendinvariantinputprimitive. (exists jt_factor_appendinvariantinputprimitivemodulus. (n)=(jt_divisor_appendinvariantinputprimitive)*jt_factor_appendinvariantinputprimitivemodulus) -> (forall jt_index_appendinvariantinputprimitivecoordinates jt_value_appendinvariantinputprimitivecoordinates. (exists jt_gap_appendinvariantinputprimitivecoordinatesindex. jt_gap_appendinvariantinputprimitivecoordinatesindex+S (jt_index_appendinvariantinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_appendinvariantinputprimitivecoordinatesat. fs_h_jt_appendinvariantinputprimitivecoordinatesat + S (jt_value_appendinvariantinputprimitivecoordinates) = S ((S (jt_index_appendinvariantinputprimitivecoordinates)) * c)) /\ exists fs_q_jt_appendinvariantinputprimitivecoordinatesat. jt_z_appendinvariant = fs_q_jt_appendinvariantinputprimitivecoordinatesat * S ((S (jt_index_appendinvariantinputprimitivecoordinates)) * c) + (jt_value_appendinvariantinputprimitivecoordinates))) -> (exists jt_factor_appendinvariantinputprimitivecoordinatesdivides. (jt_value_appendinvariantinputprimitivecoordinates)=(jt_divisor_appendinvariantinputprimitive)*jt_factor_appendinvariantinputprimitivecoordinatesdivides)) -> jt_divisor_appendinvariantinputprimitive=1) -> (exists jt_index_appendinvariantlisted jt_code_appendinvariantlisted jt_scale_appendinvariantlisted. ((exists jt_gap_appendinvariantlistedindex. jt_gap_appendinvariantlistedindex+S (jt_index_appendinvariantlisted)=(j)) /\ (((((((exists fs_h_jt_appendinvariantlistedcode. fs_h_jt_appendinvariantlistedcode + S (jt_code_appendinvariantlisted) = S ((S (jt_index_appendinvariantlisted)) * C)) /\ exists fs_q_jt_appendinvariantlistedcode. B = fs_q_jt_appendinvariantlistedcode * S ((S (jt_index_appendinvariantlisted)) * C) + (jt_code_appendinvariantlisted))) /\ (((exists fs_h_jt_appendinvariantlistedscale. fs_h_jt_appendinvariantlistedscale + S (jt_scale_appendinvariantlisted) = S ((S (jt_index_appendinvariantlisted)) * E)) /\ exists fs_q_jt_appendinvariantlistedscale. D = fs_q_jt_appendinvariantlistedscale * S ((S (jt_index_appendinvariantlisted)) * E) + (jt_scale_appendinvariantlisted))))) /\ (forall jt_index_appendinvariantlistedequal jt_left_appendinvariantlistedequal jt_right_appendinvariantlistedequal. (exists jt_gap_appendinvariantlistedequalindex. jt_gap_appendinvariantlistedequalindex+S (jt_index_appendinvariantlistedequal)=(k)) -> (((exists fs_h_jt_appendinvariantlistedequalleft. fs_h_jt_appendinvariantlistedequalleft + S (jt_left_appendinvariantlistedequal) = S ((S (jt_index_appendinvariantlistedequal)) * c)) /\ exists fs_q_jt_appendinvariantlistedequalleft. jt_z_appendinvariant = fs_q_jt_appendinvariantlistedequalleft * S ((S (jt_index_appendinvariantlistedequal)) * c) + (jt_left_appendinvariantlistedequal))) -> (((exists fs_h_jt_appendinvariantlistedequalright. fs_h_jt_appendinvariantlistedequalright + S (jt_right_appendinvariantlistedequal) = S ((S (jt_index_appendinvariantlistedequal)) * jt_scale_appendinvariantlisted)) /\ exists fs_q_jt_appendinvariantlistedequalright. jt_code_appendinvariantlisted = fs_q_jt_appendinvariantlistedequalright * S ((S (jt_index_appendinvariantlistedequal)) * jt_scale_appendinvariantlisted) + (jt_right_appendinvariantlistedequal))) -> jt_left_appendinvariantlistedequal=jt_right_appendinvariantlistedequal)))))))))) -> (forall jt_index_appendbound. (exists jt_gap_appendboundindex. jt_gap_appendboundindex+S (jt_index_appendbound)=(k)) -> exists jt_value_appendbound. ((((exists fs_h_jt_appendboundat. fs_h_jt_appendboundat + S (jt_value_appendbound) = S ((S (jt_index_appendbound)) * c)) /\ exists fs_q_jt_appendboundat. t = fs_q_jt_appendboundat * S ((S (jt_index_appendbound)) * c) + (jt_value_appendbound))) /\ (exists jt_gap_appendboundvalue. jt_gap_appendboundvalue+S (jt_value_appendbound)=(n)))) -> (forall jt_divisor_appendprimitive. (exists jt_factor_appendprimitivemodulus. (n)=(jt_divisor_appendprimitive)*jt_factor_appendprimitivemodulus) -> (forall jt_index_appendprimitivecoordinates jt_value_appendprimitivecoordinates. (exists jt_gap_appendprimitivecoordinatesindex. jt_gap_appendprimitivecoordinatesindex+S (jt_index_appendprimitivecoordinates)=(k)) -> (((exists fs_h_jt_appendprimitivecoordinatesat. fs_h_jt_appendprimitivecoordinatesat + S (jt_value_appendprimitivecoordinates) = S ((S (jt_index_appendprimitivecoordinates)) * c)) /\ exists fs_q_jt_appendprimitivecoordinatesat. t = fs_q_jt_appendprimitivecoordinatesat * S ((S (jt_index_appendprimitivecoordinates)) * c) + (jt_value_appendprimitivecoordinates))) -> (exists jt_factor_appendprimitivecoordinatesdivides. (jt_value_appendprimitivecoordinates)=(jt_divisor_appendprimitive)*jt_factor_appendprimitivecoordinatesdivides)) -> jt_divisor_appendprimitive=1) -> ~(exists jt_index_appendfresh jt_code_appendfresh jt_scale_appendfresh. ((exists jt_gap_appendfreshindex. jt_gap_appendfreshindex+S (jt_index_appendfresh)=(j)) /\ (((((((exists fs_h_jt_appendfreshcode. fs_h_jt_appendfreshcode + S (jt_code_appendfresh) = S ((S (jt_index_appendfresh)) * C)) /\ exists fs_q_jt_appendfreshcode. B = fs_q_jt_appendfreshcode * S ((S (jt_index_appendfresh)) * C) + (jt_code_appendfresh))) /\ (((exists fs_h_jt_appendfreshscale. fs_h_jt_appendfreshscale + S (jt_scale_appendfresh) = S ((S (jt_index_appendfresh)) * E)) /\ exists fs_q_jt_appendfreshscale. D = fs_q_jt_appendfreshscale * S ((S (jt_index_appendfresh)) * E) + (jt_scale_appendfresh))))) /\ (forall jt_index_appendfreshequal jt_left_appendfreshequal jt_right_appendfreshequal. (exists jt_gap_appendfreshequalindex. jt_gap_appendfreshequalindex+S (jt_index_appendfreshequal)=(k)) -> (((exists fs_h_jt_appendfreshequalleft. fs_h_jt_appendfreshequalleft + S (jt_left_appendfreshequal) = S ((S (jt_index_appendfreshequal)) * c)) /\ exists fs_q_jt_appendfreshequalleft. t = fs_q_jt_appendfreshequalleft * S ((S (jt_index_appendfreshequal)) * c) + (jt_left_appendfreshequal))) -> (((exists fs_h_jt_appendfreshequalright. fs_h_jt_appendfreshequalright + S (jt_right_appendfreshequal) = S ((S (jt_index_appendfreshequal)) * jt_scale_appendfresh)) /\ exists fs_q_jt_appendfreshequalright. jt_code_appendfresh = fs_q_jt_appendfreshequalright * S ((S (jt_index_appendfreshequal)) * jt_scale_appendfresh) + (jt_right_appendfreshequal))) -> jt_left_appendfreshequal=jt_right_appendfreshequal))))) -> exists U V W X. ((forall jt_i_appendresult. (exists jt_gap_appendresultsoundindex. jt_gap_appendresultsoundindex+S (jt_i_appendresult)=(S j)) -> exists jt_b_appendresult jt_e_appendresult. ((((((exists fs_h_jt_appendresultsoundcode. fs_h_jt_appendresultsoundcode + S (jt_b_appendresult) = S ((S (jt_i_appendresult)) * V)) /\ exists fs_q_jt_appendresultsoundcode. U = fs_q_jt_appendresultsoundcode * S ((S (jt_i_appendresult)) * V) + (jt_b_appendresult))) /\ (((exists fs_h_jt_appendresultsoundscale. fs_h_jt_appendresultsoundscale + S (jt_e_appendresult) = S ((S (jt_i_appendresult)) * X)) /\ exists fs_q_jt_appendresultsoundscale. W = fs_q_jt_appendresultsoundscale * S ((S (jt_i_appendresult)) * X) + (jt_e_appendresult))))) /\ (((forall jt_index_appendresultbound. (exists jt_gap_appendresultboundindex. jt_gap_appendresultboundindex+S (jt_index_appendresultbound)=(k)) -> exists jt_value_appendresultbound. ((((exists fs_h_jt_appendresultboundat. fs_h_jt_appendresultboundat + S (jt_value_appendresultbound) = S ((S (jt_index_appendresultbound)) * jt_e_appendresult)) /\ exists fs_q_jt_appendresultboundat. jt_b_appendresult = fs_q_jt_appendresultboundat * S ((S (jt_index_appendresultbound)) * jt_e_appendresult) + (jt_value_appendresultbound))) /\ (exists jt_gap_appendresultboundvalue. jt_gap_appendresultboundvalue+S (jt_value_appendresultbound)=(n)))) /\ (forall jt_divisor_appendresultprimitive. (exists jt_factor_appendresultprimitivemodulus. (n)=(jt_divisor_appendresultprimitive)*jt_factor_appendresultprimitivemodulus) -> (forall jt_index_appendresultprimitivecoordinates jt_value_appendresultprimitivecoordinates. (exists jt_gap_appendresultprimitivecoordinatesindex. jt_gap_appendresultprimitivecoordinatesindex+S (jt_index_appendresultprimitivecoordinates)=(k)) -> (((exists fs_h_jt_appendresultprimitivecoordinatesat. fs_h_jt_appendresultprimitivecoordinatesat + S (jt_value_appendresultprimitivecoordinates) = S ((S (jt_index_appendresultprimitivecoordinates)) * jt_e_appendresult)) /\ exists fs_q_jt_appendresultprimitivecoordinatesat. jt_b_appendresult = fs_q_jt_appendresultprimitivecoordinatesat * S ((S (jt_index_appendresultprimitivecoordinates)) * jt_e_appendresult) + (jt_value_appendresultprimitivecoordinates))) -> (exists jt_factor_appendresultprimitivecoordinatesdivides. (jt_value_appendresultprimitivecoordinates)=(jt_divisor_appendresultprimitive)*jt_factor_appendresultprimitivecoordinatesdivides)) -> jt_divisor_appendresultprimitive=1))))) /\ (((forall jt_i_appendresult jt_h_appendresult jt_b_appendresult jt_e_appendresult jt_d_appendresult jt_f_appendresult. (exists jt_gap_appendresultfirstindex. jt_gap_appendresultfirstindex+S (jt_i_appendresult)=(S j)) -> (exists jt_gap_appendresultsecondindex. jt_gap_appendresultsecondindex+S (jt_h_appendresult)=(S j)) -> (((((exists fs_h_jt_appendresultfirstcode. fs_h_jt_appendresultfirstcode + S (jt_b_appendresult) = S ((S (jt_i_appendresult)) * V)) /\ exists fs_q_jt_appendresultfirstcode. U = fs_q_jt_appendresultfirstcode * S ((S (jt_i_appendresult)) * V) + (jt_b_appendresult))) /\ (((exists fs_h_jt_appendresultfirstscale. fs_h_jt_appendresultfirstscale + S (jt_e_appendresult) = S ((S (jt_i_appendresult)) * X)) /\ exists fs_q_jt_appendresultfirstscale. W = fs_q_jt_appendresultfirstscale * S ((S (jt_i_appendresult)) * X) + (jt_e_appendresult))))) -> (((((exists fs_h_jt_appendresultsecondcode. fs_h_jt_appendresultsecondcode + S (jt_d_appendresult) = S ((S (jt_h_appendresult)) * V)) /\ exists fs_q_jt_appendresultsecondcode. U = fs_q_jt_appendresultsecondcode * S ((S (jt_h_appendresult)) * V) + (jt_d_appendresult))) /\ (((exists fs_h_jt_appendresultsecondscale. fs_h_jt_appendresultsecondscale + S (jt_f_appendresult) = S ((S (jt_h_appendresult)) * X)) /\ exists fs_q_jt_appendresultsecondscale. W = fs_q_jt_appendresultsecondscale * S ((S (jt_h_appendresult)) * X) + (jt_f_appendresult))))) -> (forall jt_index_appendresultsame jt_left_appendresultsame jt_right_appendresultsame. (exists jt_gap_appendresultsameindex. jt_gap_appendresultsameindex+S (jt_index_appendresultsame)=(k)) -> (((exists fs_h_jt_appendresultsameleft. fs_h_jt_appendresultsameleft + S (jt_left_appendresultsame) = S ((S (jt_index_appendresultsame)) * jt_e_appendresult)) /\ exists fs_q_jt_appendresultsameleft. jt_b_appendresult = fs_q_jt_appendresultsameleft * S ((S (jt_index_appendresultsame)) * jt_e_appendresult) + (jt_left_appendresultsame))) -> (((exists fs_h_jt_appendresultsameright. fs_h_jt_appendresultsameright + S (jt_right_appendresultsame) = S ((S (jt_index_appendresultsame)) * jt_f_appendresult)) /\ exists fs_q_jt_appendresultsameright. jt_d_appendresult = fs_q_jt_appendresultsameright * S ((S (jt_index_appendresultsame)) * jt_f_appendresult) + (jt_right_appendresultsame))) -> jt_left_appendresultsame=jt_right_appendresultsame) -> jt_i_appendresult=jt_h_appendresult) /\ (forall jt_z_appendresult. (exists jt_gap_appendresultcodeindex. jt_gap_appendresultcodeindex+S (jt_z_appendresult)=(S t)) -> (forall jt_index_appendresultinputbound. (exists jt_gap_appendresultinputboundindex. jt_gap_appendresultinputboundindex+S (jt_index_appendresultinputbound)=(k)) -> exists jt_value_appendresultinputbound. ((((exists fs_h_jt_appendresultinputboundat. fs_h_jt_appendresultinputboundat + S (jt_value_appendresultinputbound) = S ((S (jt_index_appendresultinputbound)) * c)) /\ exists fs_q_jt_appendresultinputboundat. jt_z_appendresult = fs_q_jt_appendresultinputboundat * S ((S (jt_index_appendresultinputbound)) * c) + (jt_value_appendresultinputbound))) /\ (exists jt_gap_appendresultinputboundvalue. jt_gap_appendresultinputboundvalue+S (jt_value_appendresultinputbound)=(n)))) -> (forall jt_divisor_appendresultinputprimitive. (exists jt_factor_appendresultinputprimitivemodulus. (n)=(jt_divisor_appendresultinputprimitive)*jt_factor_appendresultinputprimitivemodulus) -> (forall jt_index_appendresultinputprimitivecoordinates jt_value_appendresultinputprimitivecoordinates. (exists jt_gap_appendresultinputprimitivecoordinatesindex. jt_gap_appendresultinputprimitivecoordinatesindex+S (jt_index_appendresultinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_appendresultinputprimitivecoordinatesat. fs_h_jt_appendresultinputprimitivecoordinatesat + S (jt_value_appendresultinputprimitivecoordinates) = S ((S (jt_index_appendresultinputprimitivecoordinates)) * c)) /\ exists fs_q_jt_appendresultinputprimitivecoordinatesat. jt_z_appendresult = fs_q_jt_appendresultinputprimitivecoordinatesat * S ((S (jt_index_appendresultinputprimitivecoordinates)) * c) + (jt_value_appendresultinputprimitivecoordinates))) -> (exists jt_factor_appendresultinputprimitivecoordinatesdivides. (jt_value_appendresultinputprimitivecoordinates)=(jt_divisor_appendresultinputprimitive)*jt_factor_appendresultinputprimitivecoordinatesdivides)) -> jt_divisor_appendresultinputprimitive=1) -> (exists jt_index_appendresultlisted jt_code_appendresultlisted jt_scale_appendresultlisted. ((exists jt_gap_appendresultlistedindex. jt_gap_appendresultlistedindex+S (jt_index_appendresultlisted)=(S j)) /\ (((((((exists fs_h_jt_appendresultlistedcode. fs_h_jt_appendresultlistedcode + S (jt_code_appendresultlisted) = S ((S (jt_index_appendresultlisted)) * V)) /\ exists fs_q_jt_appendresultlistedcode. U = fs_q_jt_appendresultlistedcode * S ((S (jt_index_appendresultlisted)) * V) + (jt_code_appendresultlisted))) /\ (((exists fs_h_jt_appendresultlistedscale. fs_h_jt_appendresultlistedscale + S (jt_scale_appendresultlisted) = S ((S (jt_index_appendresultlisted)) * X)) /\ exists fs_q_jt_appendresultlistedscale. W = fs_q_jt_appendresultlistedscale * S ((S (jt_index_appendresultlisted)) * X) + (jt_scale_appendresultlisted))))) /\ (forall jt_index_appendresultlistedequal jt_left_appendresultlistedequal jt_right_appendresultlistedequal. (exists jt_gap_appendresultlistedequalindex. jt_gap_appendresultlistedequalindex+S (jt_index_appendresultlistedequal)=(k)) -> (((exists fs_h_jt_appendresultlistedequalleft. fs_h_jt_appendresultlistedequalleft + S (jt_left_appendresultlistedequal) = S ((S (jt_index_appendresultlistedequal)) * c)) /\ exists fs_q_jt_appendresultlistedequalleft. jt_z_appendresult = fs_q_jt_appendresultlistedequalleft * S ((S (jt_index_appendresultlistedequal)) * c) + (jt_left_appendresultlistedequal))) -> (((exists fs_h_jt_appendresultlistedequalright. fs_h_jt_appendresultlistedequalright + S (jt_right_appendresultlistedequal) = S ((S (jt_index_appendresultlistedequal)) * jt_scale_appendresultlisted)) /\ exists fs_q_jt_appendresultlistedequalright. jt_code_appendresultlisted = fs_q_jt_appendresultlistedequalright * S ((S (jt_index_appendresultlistedequal)) * jt_scale_appendresultlisted) + (jt_right_appendresultlistedequal))) -> jt_left_appendresultlistedequal=jt_right_appendresultlistedequal)))))))))