PX0076

prime_field_polynomial_subtract_equivalent_congruent

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Pairwise formal-equivalent inputs give formal-equivalent actual subtract outputs at either ordering of the two aligned lengths, including empty prefixes; no output equivalence or raw-code equality is assumed.

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 p ab ac bb bc cb cc L AB AC BB BC CB CC K. (~((p) = 1) /\ forall pfa_factor_left_subtract_congruent_prime pfa_factor_right_subtract_congruent_prime. (p) = pfa_factor_left_subtract_congruent_prime * pfa_factor_right_subtract_congruent_prime -> pfa_factor_left_subtract_congruent_prime = 1 \/ pfa_factor_right_subtract_congruent_prime = 1) -> (forall pfrep_power_subtract_congruent_first pfrep_left_subtract_congruent_first pfrep_right_subtract_congruent_first. ((exists pfrep_position_subtract_congruent_firstfirst. ((pfrep_position_subtract_congruent_firstfirst+S (pfrep_power_subtract_congruent_first)=(L)) /\ ((((exists ff_h_pfp_subtract_congruent_firstfirstentry. ff_h_pfp_subtract_congruent_firstfirstentry + S (pfrep_left_subtract_congruent_first) = S ((S (pfrep_position_subtract_congruent_firstfirst)) * ac)) /\ exists ff_q_pfp_subtract_congruent_firstfirstentry. ab = ff_q_pfp_subtract_congruent_firstfirstentry * S ((S (pfrep_position_subtract_congruent_firstfirst)) * ac) + (pfrep_left_subtract_congruent_first)))))) \/ (((exists pfrep_gap_subtract_congruent_firstfirstoutside. pfrep_gap_subtract_congruent_firstfirstoutside+(L)=(pfrep_power_subtract_congruent_first)) /\ (((pfrep_left_subtract_congruent_first)=0))))) -> ((exists pfrep_position_subtract_congruent_firstsecond. ((pfrep_position_subtract_congruent_firstsecond+S (pfrep_power_subtract_congruent_first)=(K)) /\ ((((exists ff_h_pfp_subtract_congruent_firstsecondentry. ff_h_pfp_subtract_congruent_firstsecondentry + S (pfrep_right_subtract_congruent_first) = S ((S (pfrep_position_subtract_congruent_firstsecond)) * AC)) /\ exists ff_q_pfp_subtract_congruent_firstsecondentry. AB = ff_q_pfp_subtract_congruent_firstsecondentry * S ((S (pfrep_position_subtract_congruent_firstsecond)) * AC) + (pfrep_right_subtract_congruent_first)))))) \/ (((exists pfrep_gap_subtract_congruent_firstsecondoutside. pfrep_gap_subtract_congruent_firstsecondoutside+(K)=(pfrep_power_subtract_congruent_first)) /\ (((pfrep_right_subtract_congruent_first)=0))))) -> pfrep_left_subtract_congruent_first=pfrep_right_subtract_congruent_first) -> (forall pfrep_power_subtract_congruent_second pfrep_left_subtract_congruent_second pfrep_right_subtract_congruent_second. ((exists pfrep_position_subtract_congruent_secondfirst. ((pfrep_position_subtract_congruent_secondfirst+S (pfrep_power_subtract_congruent_second)=(L)) /\ ((((exists ff_h_pfp_subtract_congruent_secondfirstentry. ff_h_pfp_subtract_congruent_secondfirstentry + S (pfrep_left_subtract_congruent_second) = S ((S (pfrep_position_subtract_congruent_secondfirst)) * bc)) /\ exists ff_q_pfp_subtract_congruent_secondfirstentry. bb = ff_q_pfp_subtract_congruent_secondfirstentry * S ((S (pfrep_position_subtract_congruent_secondfirst)) * bc) + (pfrep_left_subtract_congruent_second)))))) \/ (((exists pfrep_gap_subtract_congruent_secondfirstoutside. pfrep_gap_subtract_congruent_secondfirstoutside+(L)=(pfrep_power_subtract_congruent_second)) /\ (((pfrep_left_subtract_congruent_second)=0))))) -> ((exists pfrep_position_subtract_congruent_secondsecond. ((pfrep_position_subtract_congruent_secondsecond+S (pfrep_power_subtract_congruent_second)=(K)) /\ ((((exists ff_h_pfp_subtract_congruent_secondsecondentry. ff_h_pfp_subtract_congruent_secondsecondentry + S (pfrep_right_subtract_congruent_second) = S ((S (pfrep_position_subtract_congruent_secondsecond)) * BC)) /\ exists ff_q_pfp_subtract_congruent_secondsecondentry. BB = ff_q_pfp_subtract_congruent_secondsecondentry * S ((S (pfrep_position_subtract_congruent_secondsecond)) * BC) + (pfrep_right_subtract_congruent_second)))))) \/ (((exists pfrep_gap_subtract_congruent_secondsecondoutside. pfrep_gap_subtract_congruent_secondsecondoutside+(K)=(pfrep_power_subtract_congruent_second)) /\ (((pfrep_right_subtract_congruent_second)=0))))) -> pfrep_left_subtract_congruent_second=pfrep_right_subtract_congruent_second) -> (forall pfs_index_subtract_congruent_original. (exists pfa_gap_subtract_congruent_originalindex. pfa_gap_subtract_congruent_originalindex + S (pfs_index_subtract_congruent_original) = (L)) -> exists pfs_left_subtract_congruent_original pfs_right_subtract_congruent_original pfs_result_subtract_congruent_original. ((((exists ff_h_pfp_subtract_congruent_originalleft. ff_h_pfp_subtract_congruent_originalleft + S (pfs_left_subtract_congruent_original) = S ((S (pfs_index_subtract_congruent_original)) * ac)) /\ exists ff_q_pfp_subtract_congruent_originalleft. ab = ff_q_pfp_subtract_congruent_originalleft * S ((S (pfs_index_subtract_congruent_original)) * ac) + (pfs_left_subtract_congruent_original))) /\ (((((exists ff_h_pfp_subtract_congruent_originalright. ff_h_pfp_subtract_congruent_originalright + S (pfs_right_subtract_congruent_original) = S ((S (pfs_index_subtract_congruent_original)) * bc)) /\ exists ff_q_pfp_subtract_congruent_originalright. bb = ff_q_pfp_subtract_congruent_originalright * S ((S (pfs_index_subtract_congruent_original)) * bc) + (pfs_right_subtract_congruent_original))) /\ (((((exists ff_h_pfp_subtract_congruent_originalresult. ff_h_pfp_subtract_congruent_originalresult + S (pfs_result_subtract_congruent_original) = S ((S (pfs_index_subtract_congruent_original)) * cc)) /\ exists ff_q_pfp_subtract_congruent_originalresult. cb = ff_q_pfp_subtract_congruent_originalresult * S ((S (pfs_index_subtract_congruent_original)) * cc) + (pfs_result_subtract_congruent_original))) /\ ((((exists pfa_gap_subtract_congruent_originaloperationleft. pfa_gap_subtract_congruent_originaloperationleft + S (pfs_right_subtract_congruent_original) = (p)) /\ (((exists pfa_gap_subtract_congruent_originaloperationright. pfa_gap_subtract_congruent_originaloperationright + S (pfs_result_subtract_congruent_original) = (p)) /\ ((((exists pfa_gap_subtract_congruent_originaloperationresultbound. pfa_gap_subtract_congruent_originaloperationresultbound + S (pfs_left_subtract_congruent_original) = (p)) /\ ((exists pfa_offset_left_subtract_congruent_originaloperationresultcongruence pfa_offset_right_subtract_congruent_originaloperationresultcongruence. ((pfs_right_subtract_congruent_original) + (pfs_result_subtract_congruent_original)) + (p) * pfa_offset_left_subtract_congruent_originaloperationresultcongruence = (pfs_left_subtract_congruent_original) + (p) * pfa_offset_right_subtract_congruent_originaloperationresultcongruence)))))))))))))))) -> (forall pfs_index_subtract_congruent_other. (exists pfa_gap_subtract_congruent_otherindex. pfa_gap_subtract_congruent_otherindex + S (pfs_index_subtract_congruent_other) = (K)) -> exists pfs_left_subtract_congruent_other pfs_right_subtract_congruent_other pfs_result_subtract_congruent_other. ((((exists ff_h_pfp_subtract_congruent_otherleft. ff_h_pfp_subtract_congruent_otherleft + S (pfs_left_subtract_congruent_other) = S ((S (pfs_index_subtract_congruent_other)) * AC)) /\ exists ff_q_pfp_subtract_congruent_otherleft. AB = ff_q_pfp_subtract_congruent_otherleft * S ((S (pfs_index_subtract_congruent_other)) * AC) + (pfs_left_subtract_congruent_other))) /\ (((((exists ff_h_pfp_subtract_congruent_otherright. ff_h_pfp_subtract_congruent_otherright + S (pfs_right_subtract_congruent_other) = S ((S (pfs_index_subtract_congruent_other)) * BC)) /\ exists ff_q_pfp_subtract_congruent_otherright. BB = ff_q_pfp_subtract_congruent_otherright * S ((S (pfs_index_subtract_congruent_other)) * BC) + (pfs_right_subtract_congruent_other))) /\ (((((exists ff_h_pfp_subtract_congruent_otherresult. ff_h_pfp_subtract_congruent_otherresult + S (pfs_result_subtract_congruent_other) = S ((S (pfs_index_subtract_congruent_other)) * CC)) /\ exists ff_q_pfp_subtract_congruent_otherresult. CB = ff_q_pfp_subtract_congruent_otherresult * S ((S (pfs_index_subtract_congruent_other)) * CC) + (pfs_result_subtract_congruent_other))) /\ ((((exists pfa_gap_subtract_congruent_otheroperationleft. pfa_gap_subtract_congruent_otheroperationleft + S (pfs_right_subtract_congruent_other) = (p)) /\ (((exists pfa_gap_subtract_congruent_otheroperationright. pfa_gap_subtract_congruent_otheroperationright + S (pfs_result_subtract_congruent_other) = (p)) /\ ((((exists pfa_gap_subtract_congruent_otheroperationresultbound. pfa_gap_subtract_congruent_otheroperationresultbound + S (pfs_left_subtract_congruent_other) = (p)) /\ ((exists pfa_offset_left_subtract_congruent_otheroperationresultcongruence pfa_offset_right_subtract_congruent_otheroperationresultcongruence. ((pfs_right_subtract_congruent_other) + (pfs_result_subtract_congruent_other)) + (p) * pfa_offset_left_subtract_congruent_otheroperationresultcongruence = (pfs_left_subtract_congruent_other) + (p) * pfa_offset_right_subtract_congruent_otheroperationresultcongruence)))))))))))))))) -> (forall pfrep_power_subtract_congruent_result pfrep_left_subtract_congruent_result pfrep_right_subtract_congruent_result. ((exists pfrep_position_subtract_congruent_resultfirst. ((pfrep_position_subtract_congruent_resultfirst+S (pfrep_power_subtract_congruent_result)=(L)) /\ ((((exists ff_h_pfp_subtract_congruent_resultfirstentry. ff_h_pfp_subtract_congruent_resultfirstentry + S (pfrep_left_subtract_congruent_result) = S ((S (pfrep_position_subtract_congruent_resultfirst)) * cc)) /\ exists ff_q_pfp_subtract_congruent_resultfirstentry. cb = ff_q_pfp_subtract_congruent_resultfirstentry * S ((S (pfrep_position_subtract_congruent_resultfirst)) * cc) + (pfrep_left_subtract_congruent_result)))))) \/ (((exists pfrep_gap_subtract_congruent_resultfirstoutside. pfrep_gap_subtract_congruent_resultfirstoutside+(L)=(pfrep_power_subtract_congruent_result)) /\ (((pfrep_left_subtract_congruent_result)=0))))) -> ((exists pfrep_position_subtract_congruent_resultsecond. ((pfrep_position_subtract_congruent_resultsecond+S (pfrep_power_subtract_congruent_result)=(K)) /\ ((((exists ff_h_pfp_subtract_congruent_resultsecondentry. ff_h_pfp_subtract_congruent_resultsecondentry + S (pfrep_right_subtract_congruent_result) = S ((S (pfrep_position_subtract_congruent_resultsecond)) * CC)) /\ exists ff_q_pfp_subtract_congruent_resultsecondentry. CB = ff_q_pfp_subtract_congruent_resultsecondentry * S ((S (pfrep_position_subtract_congruent_resultsecond)) * CC) + (pfrep_right_subtract_congruent_result)))))) \/ (((exists pfrep_gap_subtract_congruent_resultsecondoutside. pfrep_gap_subtract_congruent_resultsecondoutside+(K)=(pfrep_power_subtract_congruent_result)) /\ (((pfrep_right_subtract_congruent_result)=0))))) -> pfrep_left_subtract_congruent_result=pfrep_right_subtract_congruent_result)

Constructive proof overview

Generated structural guide

Pairwise formal-equivalent inputs give formal-equivalent actual subtract outputs at either ordering of the two aligned lengths, including empty prefixes; no output equivalence or raw-code equality is assumed.

The unchanged tactic script uses 5 declared prerequisites and contains 154 exact native proof lines.

Alpha v34 checked-use · first admitted v33 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

le_total Alpha theorem; checked-use authorized PX0072 prime_field_polynomial_equivalent_implies_left_pad PX0074 prime_field_polynomial_subtract_left_pad_output PX001B prime_field_polynomial_left_pad_equivalent PX000F prime_field_polynomial_equivalent_symmetric

Direct dependents

none

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

154 script commands · 20 reading checkpoints · 5 local claims

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.

Named ingredients (4)
prime field polynomial equivalent implies left padprime field polynomial subtract left pad outputprime field polynomial left pad equivalentprime field polynomial equivalent symmetric

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro ab
  3. L3
    intro ac
  4. L4
    intro bb
  5. L5
    intro bc
  6. L6
    intro cb
  7. L7
    intro cc
  8. L8
    intro L
  9. L9
    intro AB
  10. L10
    intro AC
02Fix variables and assumptionsL11–20

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro BB
  2. L12
    intro BC
  3. L13
    intro CB
  4. L14
    intro CC
  5. L15
    intro K
  6. L16
    intro hp
  7. L17
    intro hA
  8. L18
    intro hB
  9. L19
    intro ho
  10. L20
    intro hn
03Establish horderL21–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le total.

  1. L21
    have horder : L<=K \/ K<=L
  2. L22
    specialize le_total (L)
  3. L23
    specialize le_total (K)
  4. L24
    apply le_total
04Separate the logical casesL25–26

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L25
    cases horder
  2. L26
    cases horder_left
05Calculate and transport equalitiesL27–33

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L27
    rewrite <- horder_left_witness at hA
  2. L28
    rewrite <- horder_left_witness at hA
  3. L29
    rewrite <- horder_left_witness at hB
  4. L30
    rewrite <- horder_left_witness at hB
  5. L31
    rewrite <- horder_left_witness at hn
  6. L32
    rewrite <- horder_left_witness
  7. L33
    rewrite <- horder_left_witness
06Establish hpadAL34–42

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial equivalent implies left pad.

  1. L34
    have hpadA : PolynomialLeftPad(ab,ac,L,x,AB,AC)Definitions: PolynomialLeftPad
  2. L35
    specialize prime_field_polynomial_equivalent_implies_left_pad (ab)
  3. L36
    specialize prime_field_polynomial_equivalent_implies_left_pad (ac)
  4. L37
    specialize prime_field_polynomial_equivalent_implies_left_pad (L)
  5. L38
    specialize prime_field_polynomial_equivalent_implies_left_pad (x)
  6. L39
    specialize prime_field_polynomial_equivalent_implies_left_pad (AB)
  7. L40
    specialize prime_field_polynomial_equivalent_implies_left_pad (AC)
  8. L41
    apply prime_field_polynomial_equivalent_implies_left_pad
  9. L42
    exact hA
07Establish hpadBL43–52

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial equivalent implies left pad.

  1. L43
    have hpadB : PolynomialLeftPad(bb,bc,L,x,BB,BC)Definitions: PolynomialLeftPad
  2. L44
    specialize prime_field_polynomial_equivalent_implies_left_pad (bb)
  3. L45
    specialize prime_field_polynomial_equivalent_implies_left_pad (bc)
  4. L46
    specialize prime_field_polynomial_equivalent_implies_left_pad (L)
  5. L47
    specialize prime_field_polynomial_equivalent_implies_left_pad (x)
  6. L48
    specialize prime_field_polynomial_equivalent_implies_left_pad (BB)
  7. L49
    specialize prime_field_polynomial_equivalent_implies_left_pad (BC)
  8. L50
    apply prime_field_polynomial_equivalent_implies_left_pad
  9. L51
    exact hB
  10. L52
    specialize prime_field_polynomial_left_pad_equivalent (cb)
08Use earlier factsL53–62

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L53
    specialize prime_field_polynomial_left_pad_equivalent (cc)
  2. L54
    specialize prime_field_polynomial_left_pad_equivalent (L)
  3. L55
    specialize prime_field_polynomial_left_pad_equivalent (x)
  4. L56
    specialize prime_field_polynomial_left_pad_equivalent (CB)
  5. L57
    specialize prime_field_polynomial_left_pad_equivalent (CC)
  6. L58
    apply prime_field_polynomial_left_pad_equivalent
  7. L59
    specialize prime_field_polynomial_subtract_left_pad_output (p)
  8. L60
    specialize prime_field_polynomial_subtract_left_pad_output (ab)
  9. L61
    specialize prime_field_polynomial_subtract_left_pad_output (ac)
  10. L62
    specialize prime_field_polynomial_subtract_left_pad_output (bb)
09Use earlier factsL63–72

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L63
    specialize prime_field_polynomial_subtract_left_pad_output (bc)
  2. L64
    specialize prime_field_polynomial_subtract_left_pad_output (cb)
  3. L65
    specialize prime_field_polynomial_subtract_left_pad_output (cc)
  4. L66
    specialize prime_field_polynomial_subtract_left_pad_output (L)
  5. L67
    specialize prime_field_polynomial_subtract_left_pad_output (x)
  6. L68
    specialize prime_field_polynomial_subtract_left_pad_output (AB)
  7. L69
    specialize prime_field_polynomial_subtract_left_pad_output (AC)
  8. L70
    specialize prime_field_polynomial_subtract_left_pad_output (BB)
  9. L71
    specialize prime_field_polynomial_subtract_left_pad_output (BC)
  10. L72
    specialize prime_field_polynomial_subtract_left_pad_output (CB)
10Use earlier factsL73–79

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L73
    specialize prime_field_polynomial_subtract_left_pad_output (CC)
  2. L74
    apply prime_field_polynomial_subtract_left_pad_output
  3. L75
    exact hp
  4. L76
    exact ho
  5. L77
    exact hpadA
  6. L78
    exact hpadB
  7. L79
    exact hn
11Separate the logical casesL80–80

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L80
    cases horder_right
12Calculate and transport equalitiesL81–87

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L81
    rewrite <- horder_right_witness at hA
  2. L82
    rewrite <- horder_right_witness at hA
  3. L83
    rewrite <- horder_right_witness at hB
  4. L84
    rewrite <- horder_right_witness at hB
  5. L85
    rewrite <- horder_right_witness at ho
  6. L86
    rewrite <- horder_right_witness
  7. L87
    rewrite <- horder_right_witness
13Establish hpadAL88–97

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial equivalent implies left pad.

  1. L88
    have hpadA : PolynomialLeftPad(AB,AC,K,x,ab,ac)Definitions: PolynomialLeftPad
  2. L89
    specialize prime_field_polynomial_equivalent_implies_left_pad (AB)
  3. L90
    specialize prime_field_polynomial_equivalent_implies_left_pad (AC)
  4. L91
    specialize prime_field_polynomial_equivalent_implies_left_pad (K)
  5. L92
    specialize prime_field_polynomial_equivalent_implies_left_pad (x)
  6. L93
    specialize prime_field_polynomial_equivalent_implies_left_pad (ab)
  7. L94
    specialize prime_field_polynomial_equivalent_implies_left_pad (ac)
  8. L95
    apply prime_field_polynomial_equivalent_implies_left_pad
  9. L96
    specialize prime_field_polynomial_equivalent_symmetric (ab)
  10. L97
    specialize prime_field_polynomial_equivalent_symmetric (ac)
14Use earlier factsL98–103

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L98
    specialize prime_field_polynomial_equivalent_symmetric (x+K)
  2. L99
    specialize prime_field_polynomial_equivalent_symmetric (AB)
  3. L100
    specialize prime_field_polynomial_equivalent_symmetric (AC)
  4. L101
    specialize prime_field_polynomial_equivalent_symmetric (K)
  5. L102
    apply prime_field_polynomial_equivalent_symmetric
  6. L103
    exact hA
15Establish hpadBL104–113

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial equivalent implies left pad.

  1. L104
    have hpadB : PolynomialLeftPad(BB,BC,K,x,bb,bc)Definitions: PolynomialLeftPad
  2. L105
    specialize prime_field_polynomial_equivalent_implies_left_pad (BB)
  3. L106
    specialize prime_field_polynomial_equivalent_implies_left_pad (BC)
  4. L107
    specialize prime_field_polynomial_equivalent_implies_left_pad (K)
  5. L108
    specialize prime_field_polynomial_equivalent_implies_left_pad (x)
  6. L109
    specialize prime_field_polynomial_equivalent_implies_left_pad (bb)
  7. L110
    specialize prime_field_polynomial_equivalent_implies_left_pad (bc)
  8. L111
    apply prime_field_polynomial_equivalent_implies_left_pad
  9. L112
    specialize prime_field_polynomial_equivalent_symmetric (bb)
  10. L113
    specialize prime_field_polynomial_equivalent_symmetric (bc)
16Use earlier factsL114–123

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L114
    specialize prime_field_polynomial_equivalent_symmetric (x+K)
  2. L115
    specialize prime_field_polynomial_equivalent_symmetric (BB)
  3. L116
    specialize prime_field_polynomial_equivalent_symmetric (BC)
  4. L117
    specialize prime_field_polynomial_equivalent_symmetric (K)
  5. L118
    apply prime_field_polynomial_equivalent_symmetric
  6. L119
    exact hB
  7. L120
    specialize prime_field_polynomial_equivalent_symmetric (CB)
  8. L121
    specialize prime_field_polynomial_equivalent_symmetric (CC)
  9. L122
    specialize prime_field_polynomial_equivalent_symmetric (K)
  10. L123
    specialize prime_field_polynomial_equivalent_symmetric (cb)
17Use earlier factsL124–133

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L124
    specialize prime_field_polynomial_equivalent_symmetric (cc)
  2. L125
    specialize prime_field_polynomial_equivalent_symmetric (x+K)
  3. L126
    apply prime_field_polynomial_equivalent_symmetric
  4. L127
    specialize prime_field_polynomial_left_pad_equivalent (CB)
  5. L128
    specialize prime_field_polynomial_left_pad_equivalent (CC)
  6. L129
    specialize prime_field_polynomial_left_pad_equivalent (K)
  7. L130
    specialize prime_field_polynomial_left_pad_equivalent (x)
  8. L131
    specialize prime_field_polynomial_left_pad_equivalent (cb)
  9. L132
    specialize prime_field_polynomial_left_pad_equivalent (cc)
  10. L133
    apply prime_field_polynomial_left_pad_equivalent
18Use earlier factsL134–143

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L134
    specialize prime_field_polynomial_subtract_left_pad_output (p)
  2. L135
    specialize prime_field_polynomial_subtract_left_pad_output (AB)
  3. L136
    specialize prime_field_polynomial_subtract_left_pad_output (AC)
  4. L137
    specialize prime_field_polynomial_subtract_left_pad_output (BB)
  5. L138
    specialize prime_field_polynomial_subtract_left_pad_output (BC)
  6. L139
    specialize prime_field_polynomial_subtract_left_pad_output (CB)
  7. L140
    specialize prime_field_polynomial_subtract_left_pad_output (CC)
  8. L141
    specialize prime_field_polynomial_subtract_left_pad_output (K)
  9. L142
    specialize prime_field_polynomial_subtract_left_pad_output (x)
  10. L143
    specialize prime_field_polynomial_subtract_left_pad_output (ab)
19Use earlier factsL144–153

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L144
    specialize prime_field_polynomial_subtract_left_pad_output (ac)
  2. L145
    specialize prime_field_polynomial_subtract_left_pad_output (bb)
  3. L146
    specialize prime_field_polynomial_subtract_left_pad_output (bc)
  4. L147
    specialize prime_field_polynomial_subtract_left_pad_output (cb)
  5. L148
    specialize prime_field_polynomial_subtract_left_pad_output (cc)
  6. L149
    apply prime_field_polynomial_subtract_left_pad_output
  7. L150
    exact hp
  8. L151
    exact hn
  9. L152
    exact hpadA
  10. L153
    exact hpadB
20Use earlier factsL154–154

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L154
    exact ho

Library-wide reading audit

Original exact command ledger · 154 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro cb
  7. 0007intro cc
  8. 0008intro L
  9. 0009intro AB
  10. 0010intro AC
  11. 0011intro BB
  12. 0012intro BC
  13. 0013intro CB
  14. 0014intro CC
  15. 0015intro K
  16. 0016intro hp
  17. 0017intro hA
  18. 0018intro hB
  19. 0019intro ho
  20. 0020intro hn
  21. 0021have horder : L<=K \/ K<=L
  22. 0022specialize le_total (L)
  23. 0023specialize le_total (K)
  24. 0024apply le_total
  25. 0025cases horder
  26. 0026cases horder_left
  27. 0027rewrite <- horder_left_witness at hA
  28. 0028rewrite <- horder_left_witness at hA
  29. 0029rewrite <- horder_left_witness at hB
  30. 0030rewrite <- horder_left_witness at hB
  31. 0031rewrite <- horder_left_witness at hn
  32. 0032rewrite <- horder_left_witness
  33. 0033rewrite <- horder_left_witness
  34. 0034have hpadA : ((forall pfp_repeat_index_subtract_congruent_forward_hpadAzeros. (exists pfa_gap_subtract_congruent_forward_hpadAzerosindex. pfa_gap_subtract_congruent_forward_hpadAzerosindex + S (pfp_repeat_index_subtract_congruent_forward_hpadAzeros) = (x)) -> (((exists ff_h_pfp_subtract_congruent_forward_hpadAzerosentry. ff_h_pfp_subtract_congruent_forward_hpadAzerosentry + S (0) = S ((S (pfp_repeat_index_subtract_congruent_forward_hpadAzeros)) * AC)) /\ exists ff_q_pfp_subtract_congruent_forward_hpadAzerosentry. AB = ff_q_pfp_subtract_congruent_forward_hpadAzerosentry * S ((S (pfp_repeat_index_subtract_congruent_forward_hpadAzeros)) * AC) + (0)))) /\ ((forall pfrep_index_subtract_congruent_forward_hpadA pfrep_value_subtract_congruent_forward_hpadA. (exists pfa_gap_subtract_congruent_forward_hpadAbound. pfa_gap_subtract_congruent_forward_hpadAbound + S (pfrep_index_subtract_congruent_forward_hpadA) = (L)) -> (((exists ff_h_pfp_subtract_congruent_forward_hpadAinput. ff_h_pfp_subtract_congruent_forward_hpadAinput + S (pfrep_value_subtract_congruent_forward_hpadA) = S ((S (pfrep_index_subtract_congruent_forward_hpadA)) * ac)) /\ exists ff_q_pfp_subtract_congruent_forward_hpadAinput. ab = ff_q_pfp_subtract_congruent_forward_hpadAinput * S ((S (pfrep_index_subtract_congruent_forward_hpadA)) * ac) + (pfrep_value_subtract_congruent_forward_hpadA))) -> (((exists ff_h_pfp_subtract_congruent_forward_hpadAoutput. ff_h_pfp_subtract_congruent_forward_hpadAoutput + S (pfrep_value_subtract_congruent_forward_hpadA) = S ((S ((x)+pfrep_index_subtract_congruent_forward_hpadA)) * AC)) /\ exists ff_q_pfp_subtract_congruent_forward_hpadAoutput. AB = ff_q_pfp_subtract_congruent_forward_hpadAoutput * S ((S ((x)+pfrep_index_subtract_congruent_forward_hpadA)) * AC) + (pfrep_value_subtract_congruent_forward_hpadA))))))
  35. 0035specialize prime_field_polynomial_equivalent_implies_left_pad (ab)
  36. 0036specialize prime_field_polynomial_equivalent_implies_left_pad (ac)
  37. 0037specialize prime_field_polynomial_equivalent_implies_left_pad (L)
  38. 0038specialize prime_field_polynomial_equivalent_implies_left_pad (x)
  39. 0039specialize prime_field_polynomial_equivalent_implies_left_pad (AB)
  40. 0040specialize prime_field_polynomial_equivalent_implies_left_pad (AC)
  41. 0041apply prime_field_polynomial_equivalent_implies_left_pad
  42. 0042exact hA
  43. 0043have hpadB : ((forall pfp_repeat_index_subtract_congruent_forward_hpadBzeros. (exists pfa_gap_subtract_congruent_forward_hpadBzerosindex. pfa_gap_subtract_congruent_forward_hpadBzerosindex + S (pfp_repeat_index_subtract_congruent_forward_hpadBzeros) = (x)) -> (((exists ff_h_pfp_subtract_congruent_forward_hpadBzerosentry. ff_h_pfp_subtract_congruent_forward_hpadBzerosentry + S (0) = S ((S (pfp_repeat_index_subtract_congruent_forward_hpadBzeros)) * BC)) /\ exists ff_q_pfp_subtract_congruent_forward_hpadBzerosentry. BB = ff_q_pfp_subtract_congruent_forward_hpadBzerosentry * S ((S (pfp_repeat_index_subtract_congruent_forward_hpadBzeros)) * BC) + (0)))) /\ ((forall pfrep_index_subtract_congruent_forward_hpadB pfrep_value_subtract_congruent_forward_hpadB. (exists pfa_gap_subtract_congruent_forward_hpadBbound. pfa_gap_subtract_congruent_forward_hpadBbound + S (pfrep_index_subtract_congruent_forward_hpadB) = (L)) -> (((exists ff_h_pfp_subtract_congruent_forward_hpadBinput. ff_h_pfp_subtract_congruent_forward_hpadBinput + S (pfrep_value_subtract_congruent_forward_hpadB) = S ((S (pfrep_index_subtract_congruent_forward_hpadB)) * bc)) /\ exists ff_q_pfp_subtract_congruent_forward_hpadBinput. bb = ff_q_pfp_subtract_congruent_forward_hpadBinput * S ((S (pfrep_index_subtract_congruent_forward_hpadB)) * bc) + (pfrep_value_subtract_congruent_forward_hpadB))) -> (((exists ff_h_pfp_subtract_congruent_forward_hpadBoutput. ff_h_pfp_subtract_congruent_forward_hpadBoutput + S (pfrep_value_subtract_congruent_forward_hpadB) = S ((S ((x)+pfrep_index_subtract_congruent_forward_hpadB)) * BC)) /\ exists ff_q_pfp_subtract_congruent_forward_hpadBoutput. BB = ff_q_pfp_subtract_congruent_forward_hpadBoutput * S ((S ((x)+pfrep_index_subtract_congruent_forward_hpadB)) * BC) + (pfrep_value_subtract_congruent_forward_hpadB))))))
  44. 0044specialize prime_field_polynomial_equivalent_implies_left_pad (bb)
  45. 0045specialize prime_field_polynomial_equivalent_implies_left_pad (bc)
  46. 0046specialize prime_field_polynomial_equivalent_implies_left_pad (L)
  47. 0047specialize prime_field_polynomial_equivalent_implies_left_pad (x)
  48. 0048specialize prime_field_polynomial_equivalent_implies_left_pad (BB)
  49. 0049specialize prime_field_polynomial_equivalent_implies_left_pad (BC)
  50. 0050apply prime_field_polynomial_equivalent_implies_left_pad
  51. 0051exact hB
  52. 0052specialize prime_field_polynomial_left_pad_equivalent (cb)
  53. 0053specialize prime_field_polynomial_left_pad_equivalent (cc)
  54. 0054specialize prime_field_polynomial_left_pad_equivalent (L)
  55. 0055specialize prime_field_polynomial_left_pad_equivalent (x)
  56. 0056specialize prime_field_polynomial_left_pad_equivalent (CB)
  57. 0057specialize prime_field_polynomial_left_pad_equivalent (CC)
  58. 0058apply prime_field_polynomial_left_pad_equivalent
  59. 0059specialize prime_field_polynomial_subtract_left_pad_output (p)
  60. 0060specialize prime_field_polynomial_subtract_left_pad_output (ab)
  61. 0061specialize prime_field_polynomial_subtract_left_pad_output (ac)
  62. 0062specialize prime_field_polynomial_subtract_left_pad_output (bb)
  63. 0063specialize prime_field_polynomial_subtract_left_pad_output (bc)
  64. 0064specialize prime_field_polynomial_subtract_left_pad_output (cb)
  65. 0065specialize prime_field_polynomial_subtract_left_pad_output (cc)
  66. 0066specialize prime_field_polynomial_subtract_left_pad_output (L)
  67. 0067specialize prime_field_polynomial_subtract_left_pad_output (x)
  68. 0068specialize prime_field_polynomial_subtract_left_pad_output (AB)
  69. 0069specialize prime_field_polynomial_subtract_left_pad_output (AC)
  70. 0070specialize prime_field_polynomial_subtract_left_pad_output (BB)
  71. 0071specialize prime_field_polynomial_subtract_left_pad_output (BC)
  72. 0072specialize prime_field_polynomial_subtract_left_pad_output (CB)
  73. 0073specialize prime_field_polynomial_subtract_left_pad_output (CC)
  74. 0074apply prime_field_polynomial_subtract_left_pad_output
  75. 0075exact hp
  76. 0076exact ho
  77. 0077exact hpadA
  78. 0078exact hpadB
  79. 0079exact hn
  80. 0080cases horder_right
  81. 0081rewrite <- horder_right_witness at hA
  82. 0082rewrite <- horder_right_witness at hA
  83. 0083rewrite <- horder_right_witness at hB
  84. 0084rewrite <- horder_right_witness at hB
  85. 0085rewrite <- horder_right_witness at ho
  86. 0086rewrite <- horder_right_witness
  87. 0087rewrite <- horder_right_witness
  88. 0088have hpadA : ((forall pfp_repeat_index_subtract_congruent_reverse_hpadAzeros. (exists pfa_gap_subtract_congruent_reverse_hpadAzerosindex. pfa_gap_subtract_congruent_reverse_hpadAzerosindex + S (pfp_repeat_index_subtract_congruent_reverse_hpadAzeros) = (x)) -> (((exists ff_h_pfp_subtract_congruent_reverse_hpadAzerosentry. ff_h_pfp_subtract_congruent_reverse_hpadAzerosentry + S (0) = S ((S (pfp_repeat_index_subtract_congruent_reverse_hpadAzeros)) * ac)) /\ exists ff_q_pfp_subtract_congruent_reverse_hpadAzerosentry. ab = ff_q_pfp_subtract_congruent_reverse_hpadAzerosentry * S ((S (pfp_repeat_index_subtract_congruent_reverse_hpadAzeros)) * ac) + (0)))) /\ ((forall pfrep_index_subtract_congruent_reverse_hpadA pfrep_value_subtract_congruent_reverse_hpadA. (exists pfa_gap_subtract_congruent_reverse_hpadAbound. pfa_gap_subtract_congruent_reverse_hpadAbound + S (pfrep_index_subtract_congruent_reverse_hpadA) = (K)) -> (((exists ff_h_pfp_subtract_congruent_reverse_hpadAinput. ff_h_pfp_subtract_congruent_reverse_hpadAinput + S (pfrep_value_subtract_congruent_reverse_hpadA) = S ((S (pfrep_index_subtract_congruent_reverse_hpadA)) * AC)) /\ exists ff_q_pfp_subtract_congruent_reverse_hpadAinput. AB = ff_q_pfp_subtract_congruent_reverse_hpadAinput * S ((S (pfrep_index_subtract_congruent_reverse_hpadA)) * AC) + (pfrep_value_subtract_congruent_reverse_hpadA))) -> (((exists ff_h_pfp_subtract_congruent_reverse_hpadAoutput. ff_h_pfp_subtract_congruent_reverse_hpadAoutput + S (pfrep_value_subtract_congruent_reverse_hpadA) = S ((S ((x)+pfrep_index_subtract_congruent_reverse_hpadA)) * ac)) /\ exists ff_q_pfp_subtract_congruent_reverse_hpadAoutput. ab = ff_q_pfp_subtract_congruent_reverse_hpadAoutput * S ((S ((x)+pfrep_index_subtract_congruent_reverse_hpadA)) * ac) + (pfrep_value_subtract_congruent_reverse_hpadA))))))
  89. 0089specialize prime_field_polynomial_equivalent_implies_left_pad (AB)
  90. 0090specialize prime_field_polynomial_equivalent_implies_left_pad (AC)
  91. 0091specialize prime_field_polynomial_equivalent_implies_left_pad (K)
  92. 0092specialize prime_field_polynomial_equivalent_implies_left_pad (x)
  93. 0093specialize prime_field_polynomial_equivalent_implies_left_pad (ab)
  94. 0094specialize prime_field_polynomial_equivalent_implies_left_pad (ac)
  95. 0095apply prime_field_polynomial_equivalent_implies_left_pad
  96. 0096specialize prime_field_polynomial_equivalent_symmetric (ab)
  97. 0097specialize prime_field_polynomial_equivalent_symmetric (ac)
  98. 0098specialize prime_field_polynomial_equivalent_symmetric (x+K)
  99. 0099specialize prime_field_polynomial_equivalent_symmetric (AB)
  100. 0100specialize prime_field_polynomial_equivalent_symmetric (AC)
  101. 0101specialize prime_field_polynomial_equivalent_symmetric (K)
  102. 0102apply prime_field_polynomial_equivalent_symmetric
  103. 0103exact hA
  104. 0104have hpadB : ((forall pfp_repeat_index_subtract_congruent_reverse_hpadBzeros. (exists pfa_gap_subtract_congruent_reverse_hpadBzerosindex. pfa_gap_subtract_congruent_reverse_hpadBzerosindex + S (pfp_repeat_index_subtract_congruent_reverse_hpadBzeros) = (x)) -> (((exists ff_h_pfp_subtract_congruent_reverse_hpadBzerosentry. ff_h_pfp_subtract_congruent_reverse_hpadBzerosentry + S (0) = S ((S (pfp_repeat_index_subtract_congruent_reverse_hpadBzeros)) * bc)) /\ exists ff_q_pfp_subtract_congruent_reverse_hpadBzerosentry. bb = ff_q_pfp_subtract_congruent_reverse_hpadBzerosentry * S ((S (pfp_repeat_index_subtract_congruent_reverse_hpadBzeros)) * bc) + (0)))) /\ ((forall pfrep_index_subtract_congruent_reverse_hpadB pfrep_value_subtract_congruent_reverse_hpadB. (exists pfa_gap_subtract_congruent_reverse_hpadBbound. pfa_gap_subtract_congruent_reverse_hpadBbound + S (pfrep_index_subtract_congruent_reverse_hpadB) = (K)) -> (((exists ff_h_pfp_subtract_congruent_reverse_hpadBinput. ff_h_pfp_subtract_congruent_reverse_hpadBinput + S (pfrep_value_subtract_congruent_reverse_hpadB) = S ((S (pfrep_index_subtract_congruent_reverse_hpadB)) * BC)) /\ exists ff_q_pfp_subtract_congruent_reverse_hpadBinput. BB = ff_q_pfp_subtract_congruent_reverse_hpadBinput * S ((S (pfrep_index_subtract_congruent_reverse_hpadB)) * BC) + (pfrep_value_subtract_congruent_reverse_hpadB))) -> (((exists ff_h_pfp_subtract_congruent_reverse_hpadBoutput. ff_h_pfp_subtract_congruent_reverse_hpadBoutput + S (pfrep_value_subtract_congruent_reverse_hpadB) = S ((S ((x)+pfrep_index_subtract_congruent_reverse_hpadB)) * bc)) /\ exists ff_q_pfp_subtract_congruent_reverse_hpadBoutput. bb = ff_q_pfp_subtract_congruent_reverse_hpadBoutput * S ((S ((x)+pfrep_index_subtract_congruent_reverse_hpadB)) * bc) + (pfrep_value_subtract_congruent_reverse_hpadB))))))
  105. 0105specialize prime_field_polynomial_equivalent_implies_left_pad (BB)
  106. 0106specialize prime_field_polynomial_equivalent_implies_left_pad (BC)
  107. 0107specialize prime_field_polynomial_equivalent_implies_left_pad (K)
  108. 0108specialize prime_field_polynomial_equivalent_implies_left_pad (x)
  109. 0109specialize prime_field_polynomial_equivalent_implies_left_pad (bb)
  110. 0110specialize prime_field_polynomial_equivalent_implies_left_pad (bc)
  111. 0111apply prime_field_polynomial_equivalent_implies_left_pad
  112. 0112specialize prime_field_polynomial_equivalent_symmetric (bb)
  113. 0113specialize prime_field_polynomial_equivalent_symmetric (bc)
  114. 0114specialize prime_field_polynomial_equivalent_symmetric (x+K)
  115. 0115specialize prime_field_polynomial_equivalent_symmetric (BB)
  116. 0116specialize prime_field_polynomial_equivalent_symmetric (BC)
  117. 0117specialize prime_field_polynomial_equivalent_symmetric (K)
  118. 0118apply prime_field_polynomial_equivalent_symmetric
  119. 0119exact hB
  120. 0120specialize prime_field_polynomial_equivalent_symmetric (CB)
  121. 0121specialize prime_field_polynomial_equivalent_symmetric (CC)
  122. 0122specialize prime_field_polynomial_equivalent_symmetric (K)
  123. 0123specialize prime_field_polynomial_equivalent_symmetric (cb)
  124. 0124specialize prime_field_polynomial_equivalent_symmetric (cc)
  125. 0125specialize prime_field_polynomial_equivalent_symmetric (x+K)
  126. 0126apply prime_field_polynomial_equivalent_symmetric
  127. 0127specialize prime_field_polynomial_left_pad_equivalent (CB)
  128. 0128specialize prime_field_polynomial_left_pad_equivalent (CC)
  129. 0129specialize prime_field_polynomial_left_pad_equivalent (K)
  130. 0130specialize prime_field_polynomial_left_pad_equivalent (x)
  131. 0131specialize prime_field_polynomial_left_pad_equivalent (cb)
  132. 0132specialize prime_field_polynomial_left_pad_equivalent (cc)
  133. 0133apply prime_field_polynomial_left_pad_equivalent
  134. 0134specialize prime_field_polynomial_subtract_left_pad_output (p)
  135. 0135specialize prime_field_polynomial_subtract_left_pad_output (AB)
  136. 0136specialize prime_field_polynomial_subtract_left_pad_output (AC)
  137. 0137specialize prime_field_polynomial_subtract_left_pad_output (BB)
  138. 0138specialize prime_field_polynomial_subtract_left_pad_output (BC)
  139. 0139specialize prime_field_polynomial_subtract_left_pad_output (CB)
  140. 0140specialize prime_field_polynomial_subtract_left_pad_output (CC)
  141. 0141specialize prime_field_polynomial_subtract_left_pad_output (K)
  142. 0142specialize prime_field_polynomial_subtract_left_pad_output (x)
  143. 0143specialize prime_field_polynomial_subtract_left_pad_output (ab)
  144. 0144specialize prime_field_polynomial_subtract_left_pad_output (ac)
  145. 0145specialize prime_field_polynomial_subtract_left_pad_output (bb)
  146. 0146specialize prime_field_polynomial_subtract_left_pad_output (bc)
  147. 0147specialize prime_field_polynomial_subtract_left_pad_output (cb)
  148. 0148specialize prime_field_polynomial_subtract_left_pad_output (cc)
  149. 0149apply prime_field_polynomial_subtract_left_pad_output
  150. 0150exact hp
  151. 0151exact hn
  152. 0152exact hpadA
  153. 0153exact hpadB
  154. 0154exact ho