jordan_crt_component_recovery

Exact expanded first-order arithmetic statement

forall n b c d e f g h s k. (forall jt_index_recoverleft. (exists jt_gap_recoverleftindex. jt_gap_recoverleftindex+S (jt_index_recoverleft)=(k)) -> exists jt_value_recoverleft. ((((exists fs_h_jt_recoverleftat. fs_h_jt_recoverleftat + S (jt_value_recoverleft) = S ((S (jt_index_recoverleft)) * c)) /\ exists fs_q_jt_recoverleftat. b = fs_q_jt_recoverleftat * S ((S (jt_index_recoverleft)) * c) + (jt_value_recoverleft))) /\ (exists jt_gap_recoverleftvalue. jt_gap_recoverleftvalue+S (jt_value_recoverleft)=(n)))) -> (forall jt_index_recoverright. (exists jt_gap_recoverrightindex. jt_gap_recoverrightindex+S (jt_index_recoverright)=(k)) -> exists jt_value_recoverright. ((((exists fs_h_jt_recoverrightat. fs_h_jt_recoverrightat + S (jt_value_recoverright) = S ((S (jt_index_recoverright)) * e)) /\ exists fs_q_jt_recoverrightat. d = fs_q_jt_recoverrightat * S ((S (jt_index_recoverright)) * e) + (jt_value_recoverright))) /\ (exists jt_gap_recoverrightvalue. jt_gap_recoverrightvalue+S (jt_value_recoverright)=(n)))) -> (forall jt_index_recoverfirst jt_left_recoverfirst jt_right_recoverfirst. (exists jt_gap_recoverfirstindex. jt_gap_recoverfirstindex+S (jt_index_recoverfirst)=(k)) -> (((exists fs_h_jt_recoverfirstleft. fs_h_jt_recoverfirstleft + S (jt_left_recoverfirst) = S ((S (jt_index_recoverfirst)) * g)) /\ exists fs_q_jt_recoverfirstleft. f = fs_q_jt_recoverfirstleft * S ((S (jt_index_recoverfirst)) * g) + (jt_left_recoverfirst))) -> (((exists fs_h_jt_recoverfirstright. fs_h_jt_recoverfirstright + S (jt_right_recoverfirst) = S ((S (jt_index_recoverfirst)) * c)) /\ exists fs_q_jt_recoverfirstright. b = fs_q_jt_recoverfirstright * S ((S (jt_index_recoverfirst)) * c) + (jt_right_recoverfirst))) -> (exists jt_left_recoverfirstmod jt_right_recoverfirstmod. (jt_left_recoverfirst)+(n)*jt_left_recoverfirstmod=(jt_right_recoverfirst)+(n)*jt_right_recoverfirstmod)) -> (forall jt_index_recoversecond jt_left_recoversecond jt_right_recoversecond. (exists jt_gap_recoversecondindex. jt_gap_recoversecondindex+S (jt_index_recoversecond)=(k)) -> (((exists fs_h_jt_recoversecondleft. fs_h_jt_recoversecondleft + S (jt_left_recoversecond) = S ((S (jt_index_recoversecond)) * s)) /\ exists fs_q_jt_recoversecondleft. h = fs_q_jt_recoversecondleft * S ((S (jt_index_recoversecond)) * s) + (jt_left_recoversecond))) -> (((exists fs_h_jt_recoversecondright. fs_h_jt_recoversecondright + S (jt_right_recoversecond) = S ((S (jt_index_recoversecond)) * e)) /\ exists fs_q_jt_recoversecondright. d = fs_q_jt_recoversecondright * S ((S (jt_index_recoversecond)) * e) + (jt_right_recoversecond))) -> (exists jt_left_recoversecondmod jt_right_recoversecondmod. (jt_left_recoversecond)+(n)*jt_left_recoversecondmod=(jt_right_recoversecond)+(n)*jt_right_recoversecondmod)) -> (forall jt_index_recoveroutput jt_left_recoveroutput jt_right_recoveroutput. (exists jt_gap_recoveroutputindex. jt_gap_recoveroutputindex+S (jt_index_recoveroutput)=(k)) -> (((exists fs_h_jt_recoveroutputleft. fs_h_jt_recoveroutputleft + S (jt_left_recoveroutput) = S ((S (jt_index_recoveroutput)) * g)) /\ exists fs_q_jt_recoveroutputleft. f = fs_q_jt_recoveroutputleft * S ((S (jt_index_recoveroutput)) * g) + (jt_left_recoveroutput))) -> (((exists fs_h_jt_recoveroutputright. fs_h_jt_recoveroutputright + S (jt_right_recoveroutput) = S ((S (jt_index_recoveroutput)) * s)) /\ exists fs_q_jt_recoveroutputright. h = fs_q_jt_recoveroutputright * S ((S (jt_index_recoveroutput)) * s) + (jt_right_recoveroutput))) -> jt_left_recoveroutput=jt_right_recoveroutput) -> (forall jt_index_recoverinputs jt_left_recoverinputs jt_right_recoverinputs. (exists jt_gap_recoverinputsindex. jt_gap_recoverinputsindex+S (jt_index_recoverinputs)=(k)) -> (((exists fs_h_jt_recoverinputsleft. fs_h_jt_recoverinputsleft + S (jt_left_recoverinputs) = S ((S (jt_index_recoverinputs)) * c)) /\ exists fs_q_jt_recoverinputsleft. b = fs_q_jt_recoverinputsleft * S ((S (jt_index_recoverinputs)) * c) + (jt_left_recoverinputs))) -> (((exists fs_h_jt_recoverinputsright. fs_h_jt_recoverinputsright + S (jt_right_recoverinputs) = S ((S (jt_index_recoverinputs)) * e)) /\ exists fs_q_jt_recoverinputsright. d = fs_q_jt_recoverinputsright * S ((S (jt_index_recoverinputs)) * e) + (jt_right_recoverinputs))) -> jt_left_recoverinputs=jt_right_recoverinputs)