Exact expanded PA statement
forall p q i rb rc h sh. sh = S h -> (forall eri_column_fubini_row_restrict_source. (exists eri_gap_fubini_row_restrict_source_bound. eri_gap_fubini_row_restrict_source_bound + S (eri_column_fubini_row_restrict_source) = sh) -> exists eri_bit_fubini_row_restrict_source. ((((exists ff_h_eri_fubini_row_restrict_source_decoded. ff_h_eri_fubini_row_restrict_source_decoded + S (eri_bit_fubini_row_restrict_source) = S ((S (eri_column_fubini_row_restrict_source)) * rc)) /\ exists ff_q_eri_fubini_row_restrict_source_decoded. rb = ff_q_eri_fubini_row_restrict_source_decoded * S ((S (eri_column_fubini_row_restrict_source)) * rc) + (eri_bit_fubini_row_restrict_source))) /\ (((eri_bit_fubini_row_restrict_source = 0 /\ ((exists eri_gap_fubini_row_restrict_source_choice_left. eri_gap_fubini_row_restrict_source_choice_left + S (q * S i) = p * S eri_column_fubini_row_restrict_source) /\ ~(exists eri_gap_fubini_row_restrict_source_choice_right. eri_gap_fubini_row_restrict_source_choice_right + S (p * S eri_column_fubini_row_restrict_source) = q * S i))) \/ (eri_bit_fubini_row_restrict_source = 1 /\ ((exists eri_gap_fubini_row_restrict_source_choice_right. eri_gap_fubini_row_restrict_source_choice_right + S (p * S eri_column_fubini_row_restrict_source) = q * S i) /\ ~(exists eri_gap_fubini_row_restrict_source_choice_left. eri_gap_fubini_row_restrict_source_choice_left + S (q * S i) = p * S eri_column_fubini_row_restrict_source))))))) -> (forall eri_column_fubini_row_restrict_target. (exists eri_gap_fubini_row_restrict_target_bound. eri_gap_fubini_row_restrict_target_bound + S (eri_column_fubini_row_restrict_target) = h) -> exists eri_bit_fubini_row_restrict_target. ((((exists ff_h_eri_fubini_row_restrict_target_decoded. ff_h_eri_fubini_row_restrict_target_decoded + S (eri_bit_fubini_row_restrict_target) = S ((S (eri_column_fubini_row_restrict_target)) * rc)) /\ exists ff_q_eri_fubini_row_restrict_target_decoded. rb = ff_q_eri_fubini_row_restrict_target_decoded * S ((S (eri_column_fubini_row_restrict_target)) * rc) + (eri_bit_fubini_row_restrict_target))) /\ (((eri_bit_fubini_row_restrict_target = 0 /\ ((exists eri_gap_fubini_row_restrict_target_choice_left. eri_gap_fubini_row_restrict_target_choice_left + S (q * S i) = p * S eri_column_fubini_row_restrict_target) /\ ~(exists eri_gap_fubini_row_restrict_target_choice_right. eri_gap_fubini_row_restrict_target_choice_right + S (p * S eri_column_fubini_row_restrict_target) = q * S i))) \/ (eri_bit_fubini_row_restrict_target = 1 /\ ((exists eri_gap_fubini_row_restrict_target_choice_right. eri_gap_fubini_row_restrict_target_choice_right + S (p * S eri_column_fubini_row_restrict_target) = q * S i) /\ ~(exists eri_gap_fubini_row_restrict_target_choice_left. eri_gap_fubini_row_restrict_target_choice_left + S (q * S i) = p * S eri_column_fubini_row_restrict_target)))))))Structural proof guide
Generated structural guide
A successor indicator row restricts to the same code's predecessor prefix.
Use the direct prerequisites le_succ as previously established PA formulas.
The proof proceeds by equality transport (1).
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.