Exact expanded PA statement
forall p a n b c l i. ~(exists qr_x_esipe_fixed_nonresidue. exists qr_u_esipe_fixed_nonresidue qr_v_esipe_fixed_nonresidue. qr_x_esipe_fixed_nonresidue * qr_x_esipe_fixed_nonresidue + p * qr_u_esipe_fixed_nonresidue = a + p * qr_v_esipe_fixed_nonresidue) -> (forall esip_index_fixed_prefix. (exists esip_gap_fixed_prefix_prefix_bound. esip_gap_fixed_prefix_prefix_bound + S (esip_index_fixed_prefix) = l) -> exists esip_mate_fixed_prefix. ((((exists ff_h_esip_fixed_prefix_entry. ff_h_esip_fixed_prefix_entry + S (esip_mate_fixed_prefix) = S ((S (esip_index_fixed_prefix)) * c)) /\ exists ff_q_esip_fixed_prefix_entry. b = ff_q_esip_fixed_prefix_entry * S ((S (esip_index_fixed_prefix)) * c) + (esip_mate_fixed_prefix))) /\ ((exists esip_gap_fixed_prefix_relation_index_bound. esip_gap_fixed_prefix_relation_index_bound + S (esip_index_fixed_prefix) = n) /\ ((((~((S esip_index_fixed_prefix) = 0) /\ (exists esip_gap_fixed_prefix_relation_scaled_left_bound. esip_gap_fixed_prefix_relation_scaled_left_bound + S (S esip_index_fixed_prefix) = p))) /\ (((~(esip_mate_fixed_prefix = 0) /\ (exists esip_gap_fixed_prefix_relation_scaled_right_bound. esip_gap_fixed_prefix_relation_scaled_right_bound + S (esip_mate_fixed_prefix) = p))) /\ (exists esi_mod_left_fixed_prefix_relation_scaled_mod esi_mod_right_fixed_prefix_relation_scaled_mod. ((S esip_index_fixed_prefix) * esip_mate_fixed_prefix) + p * esi_mod_left_fixed_prefix_relation_scaled_mod = (a) + p * esi_mod_right_fixed_prefix_relation_scaled_mod))))))) -> (exists esip_gap_fixed_bound. esip_gap_fixed_bound + S (i) = l) -> ~(((exists ff_h_esipe_fixed_at. ff_h_esipe_fixed_at + S (S i) = S ((S (i)) * c)) /\ exists ff_q_esipe_fixed_at. b = ff_q_esipe_fixed_at * S ((S (i)) * c) + (S i)))Structural proof guide
Generated structural guide
A nonresidue scaled-inverse prefix has no decoded fixed point.
Use the direct prerequisites scaled_inverse_prefix_entry_sound, scaled_inverse_no_fixed_of_not_qres as previously established PA formulas.
The proof proceeds by case analysis (1), intermediate claims (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.
- 0001
intro p - 0002
intro a - 0003
intro n - 0004
intro b - 0005
intro c - 0006
intro l - 0007
intro i - 0008
intro hnotqres - 0009
intro hprefix - 0010
intro hi - 0011
intro hfixed - 0012
have hrelation : (exists esip_gap_fixed_relation_index_bound. esip_gap_fixed_relation_index_bound + S (i) = n) /\ ((((~((S i) = 0) /\ (exists esip_gap_fixed_relation_scaled_left_bound. esip_gap_fixed_relation_scaled_left_bound + S (S i) = p))) /\ (((~(S i = 0) /\ (exists esip_gap_fixed_relation_scaled_right_bound. esip_gap_fixed_relation_scaled_right_bound + S (S i) = p))) /\ (exists esi_mod_left_fixed_relation_scaled_mod esi_mod_right_fixed_relation_scaled_mod. ((S i) * S i) + p * esi_mod_left_fixed_relation_scaled_mod = (a) + p * esi_mod_right_fixed_relation_scaled_mod)))) - 0013
specialize scaled_inverse_prefix_entry_sound p - 0014
specialize scaled_inverse_prefix_entry_sound a - 0015
specialize scaled_inverse_prefix_entry_sound n - 0016
specialize scaled_inverse_prefix_entry_sound b - 0017
specialize scaled_inverse_prefix_entry_sound c - 0018
specialize scaled_inverse_prefix_entry_sound l - 0019
specialize scaled_inverse_prefix_entry_sound i - 0020
specialize scaled_inverse_prefix_entry_sound (S i) - 0021
apply scaled_inverse_prefix_entry_sound - 0022
exact hprefix - 0023
exact hi - 0024
exact hfixed - 0025
cases hrelation - 0026
specialize scaled_inverse_no_fixed_of_not_qres p - 0027
specialize scaled_inverse_no_fixed_of_not_qres a - 0028
specialize scaled_inverse_no_fixed_of_not_qres (S i) - 0029
apply scaled_inverse_no_fixed_of_not_qres - 0030
exact hnotqres - 0031
exact hrelation_right