Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Exact expanded first-order arithmetic statement
forall ab ac L bb bc M ub uc vb vc K. (((forall pfrep_power_common_symmetric_old_left pfrep_left_common_symmetric_old_left pfrep_right_common_symmetric_old_left. ((exists pfrep_position_common_symmetric_old_leftfirst. ((pfrep_position_common_symmetric_old_leftfirst+S (pfrep_power_common_symmetric_old_left)=(L)) /\ ((((exists ff_h_pfp_common_symmetric_old_leftfirstentry. ff_h_pfp_common_symmetric_old_leftfirstentry + S (pfrep_left_common_symmetric_old_left) = S ((S (pfrep_position_common_symmetric_old_leftfirst)) * ac)) /\ exists ff_q_pfp_common_symmetric_old_leftfirstentry. ab = ff_q_pfp_common_symmetric_old_leftfirstentry * S ((S (pfrep_position_common_symmetric_old_leftfirst)) * ac) + (pfrep_left_common_symmetric_old_left)))))) \/ (((exists pfrep_gap_common_symmetric_old_leftfirstoutside. pfrep_gap_common_symmetric_old_leftfirstoutside+(L)=(pfrep_power_common_symmetric_old_left)) /\ (((pfrep_left_common_symmetric_old_left)=0))))) -> ((exists pfrep_position_common_symmetric_old_leftsecond. ((pfrep_position_common_symmetric_old_leftsecond+S (pfrep_power_common_symmetric_old_left)=(K)) /\ ((((exists ff_h_pfp_common_symmetric_old_leftsecondentry. ff_h_pfp_common_symmetric_old_leftsecondentry + S (pfrep_right_common_symmetric_old_left) = S ((S (pfrep_position_common_symmetric_old_leftsecond)) * uc)) /\ exists ff_q_pfp_common_symmetric_old_leftsecondentry. ub = ff_q_pfp_common_symmetric_old_leftsecondentry * S ((S (pfrep_position_common_symmetric_old_leftsecond)) * uc) + (pfrep_right_common_symmetric_old_left)))))) \/ (((exists pfrep_gap_common_symmetric_old_leftsecondoutside. pfrep_gap_common_symmetric_old_leftsecondoutside+(K)=(pfrep_power_common_symmetric_old_left)) /\ (((pfrep_right_common_symmetric_old_left)=0))))) -> pfrep_left_common_symmetric_old_left=pfrep_right_common_symmetric_old_left) /\ ((forall pfrep_power_common_symmetric_old_right pfrep_left_common_symmetric_old_right pfrep_right_common_symmetric_old_right. ((exists pfrep_position_common_symmetric_old_rightfirst. ((pfrep_position_common_symmetric_old_rightfirst+S (pfrep_power_common_symmetric_old_right)=(M)) /\ ((((exists ff_h_pfp_common_symmetric_old_rightfirstentry. ff_h_pfp_common_symmetric_old_rightfirstentry + S (pfrep_left_common_symmetric_old_right) = S ((S (pfrep_position_common_symmetric_old_rightfirst)) * bc)) /\ exists ff_q_pfp_common_symmetric_old_rightfirstentry. bb = ff_q_pfp_common_symmetric_old_rightfirstentry * S ((S (pfrep_position_common_symmetric_old_rightfirst)) * bc) + (pfrep_left_common_symmetric_old_right)))))) \/ (((exists pfrep_gap_common_symmetric_old_rightfirstoutside. pfrep_gap_common_symmetric_old_rightfirstoutside+(M)=(pfrep_power_common_symmetric_old_right)) /\ (((pfrep_left_common_symmetric_old_right)=0))))) -> ((exists pfrep_position_common_symmetric_old_rightsecond. ((pfrep_position_common_symmetric_old_rightsecond+S (pfrep_power_common_symmetric_old_right)=(K)) /\ ((((exists ff_h_pfp_common_symmetric_old_rightsecondentry. ff_h_pfp_common_symmetric_old_rightsecondentry + S (pfrep_right_common_symmetric_old_right) = S ((S (pfrep_position_common_symmetric_old_rightsecond)) * vc)) /\ exists ff_q_pfp_common_symmetric_old_rightsecondentry. vb = ff_q_pfp_common_symmetric_old_rightsecondentry * S ((S (pfrep_position_common_symmetric_old_rightsecond)) * vc) + (pfrep_right_common_symmetric_old_right)))))) \/ (((exists pfrep_gap_common_symmetric_old_rightsecondoutside. pfrep_gap_common_symmetric_old_rightsecondoutside+(K)=(pfrep_power_common_symmetric_old_right)) /\ (((pfrep_right_common_symmetric_old_right)=0))))) -> pfrep_left_common_symmetric_old_right=pfrep_right_common_symmetric_old_right)))) -> (((forall pfrep_power_common_symmetric_new_left pfrep_left_common_symmetric_new_left pfrep_right_common_symmetric_new_left. ((exists pfrep_position_common_symmetric_new_leftfirst. ((pfrep_position_common_symmetric_new_leftfirst+S (pfrep_power_common_symmetric_new_left)=(M)) /\ ((((exists ff_h_pfp_common_symmetric_new_leftfirstentry. ff_h_pfp_common_symmetric_new_leftfirstentry + S (pfrep_left_common_symmetric_new_left) = S ((S (pfrep_position_common_symmetric_new_leftfirst)) * bc)) /\ exists ff_q_pfp_common_symmetric_new_leftfirstentry. bb = ff_q_pfp_common_symmetric_new_leftfirstentry * S ((S (pfrep_position_common_symmetric_new_leftfirst)) * bc) + (pfrep_left_common_symmetric_new_left)))))) \/ (((exists pfrep_gap_common_symmetric_new_leftfirstoutside. pfrep_gap_common_symmetric_new_leftfirstoutside+(M)=(pfrep_power_common_symmetric_new_left)) /\ (((pfrep_left_common_symmetric_new_left)=0))))) -> ((exists pfrep_position_common_symmetric_new_leftsecond. ((pfrep_position_common_symmetric_new_leftsecond+S (pfrep_power_common_symmetric_new_left)=(K)) /\ ((((exists ff_h_pfp_common_symmetric_new_leftsecondentry. ff_h_pfp_common_symmetric_new_leftsecondentry + S (pfrep_right_common_symmetric_new_left) = S ((S (pfrep_position_common_symmetric_new_leftsecond)) * vc)) /\ exists ff_q_pfp_common_symmetric_new_leftsecondentry. vb = ff_q_pfp_common_symmetric_new_leftsecondentry * S ((S (pfrep_position_common_symmetric_new_leftsecond)) * vc) + (pfrep_right_common_symmetric_new_left)))))) \/ (((exists pfrep_gap_common_symmetric_new_leftsecondoutside. pfrep_gap_common_symmetric_new_leftsecondoutside+(K)=(pfrep_power_common_symmetric_new_left)) /\ (((pfrep_right_common_symmetric_new_left)=0))))) -> pfrep_left_common_symmetric_new_left=pfrep_right_common_symmetric_new_left) /\ ((forall pfrep_power_common_symmetric_new_right pfrep_left_common_symmetric_new_right pfrep_right_common_symmetric_new_right. ((exists pfrep_position_common_symmetric_new_rightfirst. ((pfrep_position_common_symmetric_new_rightfirst+S (pfrep_power_common_symmetric_new_right)=(L)) /\ ((((exists ff_h_pfp_common_symmetric_new_rightfirstentry. ff_h_pfp_common_symmetric_new_rightfirstentry + S (pfrep_left_common_symmetric_new_right) = S ((S (pfrep_position_common_symmetric_new_rightfirst)) * ac)) /\ exists ff_q_pfp_common_symmetric_new_rightfirstentry. ab = ff_q_pfp_common_symmetric_new_rightfirstentry * S ((S (pfrep_position_common_symmetric_new_rightfirst)) * ac) + (pfrep_left_common_symmetric_new_right)))))) \/ (((exists pfrep_gap_common_symmetric_new_rightfirstoutside. pfrep_gap_common_symmetric_new_rightfirstoutside+(L)=(pfrep_power_common_symmetric_new_right)) /\ (((pfrep_left_common_symmetric_new_right)=0))))) -> ((exists pfrep_position_common_symmetric_new_rightsecond. ((pfrep_position_common_symmetric_new_rightsecond+S (pfrep_power_common_symmetric_new_right)=(K)) /\ ((((exists ff_h_pfp_common_symmetric_new_rightsecondentry. ff_h_pfp_common_symmetric_new_rightsecondentry + S (pfrep_right_common_symmetric_new_right) = S ((S (pfrep_position_common_symmetric_new_rightsecond)) * uc)) /\ exists ff_q_pfp_common_symmetric_new_rightsecondentry. ub = ff_q_pfp_common_symmetric_new_rightsecondentry * S ((S (pfrep_position_common_symmetric_new_rightsecond)) * uc) + (pfrep_right_common_symmetric_new_right)))))) \/ (((exists pfrep_gap_common_symmetric_new_rightsecondoutside. pfrep_gap_common_symmetric_new_rightsecondoutside+(K)=(pfrep_power_common_symmetric_new_right)) /\ (((pfrep_right_common_symmetric_new_right)=0))))) -> pfrep_left_common_symmetric_new_right=pfrep_right_common_symmetric_new_right))))Constructive proof overview
Generated structural guide
Swapping the two original inputs and their actual representatives preserves the common-representation graph.
The unchanged tactic script uses 0 declared prerequisites and contains 16 exact native proof lines.
Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
none
Direct dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.