PQ000D

prime_field_polynomial_subtract_exists

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

Construct the entire actual canonical coefficient output by ordinary induction and beta-prefix extension; no output table 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 l. (~((p) = 1) /\ forall pfa_factor_left_subtract_exists_prime pfa_factor_right_subtract_exists_prime. (p) = pfa_factor_left_subtract_exists_prime * pfa_factor_right_subtract_exists_prime -> pfa_factor_left_subtract_exists_prime = 1 \/ pfa_factor_right_subtract_exists_prime = 1) -> (forall fom_index_pfp_subtract_exists_ab. (exists fom_gap_pfp_subtract_exists_ab_index_bound. fom_gap_pfp_subtract_exists_ab_index_bound + S (fom_index_pfp_subtract_exists_ab) = l) -> exists fom_value_pfp_subtract_exists_ab. ((((exists fom_beta_height_pfp_subtract_exists_ab_entry. fom_beta_height_pfp_subtract_exists_ab_entry + S (fom_value_pfp_subtract_exists_ab) = S ((S (fom_index_pfp_subtract_exists_ab)) * ac)) /\ exists fom_beta_quotient_pfp_subtract_exists_ab_entry. ab = fom_beta_quotient_pfp_subtract_exists_ab_entry * S ((S (fom_index_pfp_subtract_exists_ab)) * ac) + (fom_value_pfp_subtract_exists_ab))) /\ (exists fom_gap_pfp_subtract_exists_ab_value_bound. fom_gap_pfp_subtract_exists_ab_value_bound + S (fom_value_pfp_subtract_exists_ab) = p))) -> (forall fom_index_pfp_subtract_exists_bb. (exists fom_gap_pfp_subtract_exists_bb_index_bound. fom_gap_pfp_subtract_exists_bb_index_bound + S (fom_index_pfp_subtract_exists_bb) = l) -> exists fom_value_pfp_subtract_exists_bb. ((((exists fom_beta_height_pfp_subtract_exists_bb_entry. fom_beta_height_pfp_subtract_exists_bb_entry + S (fom_value_pfp_subtract_exists_bb) = S ((S (fom_index_pfp_subtract_exists_bb)) * bc)) /\ exists fom_beta_quotient_pfp_subtract_exists_bb_entry. bb = fom_beta_quotient_pfp_subtract_exists_bb_entry * S ((S (fom_index_pfp_subtract_exists_bb)) * bc) + (fom_value_pfp_subtract_exists_bb))) /\ (exists fom_gap_pfp_subtract_exists_bb_value_bound. fom_gap_pfp_subtract_exists_bb_value_bound + S (fom_value_pfp_subtract_exists_bb) = p))) -> exists rb rc. (forall pfs_index_subtract_exists_result. (exists pfa_gap_subtract_exists_resultindex. pfa_gap_subtract_exists_resultindex + S (pfs_index_subtract_exists_result) = (l)) -> exists pfs_left_subtract_exists_result pfs_right_subtract_exists_result pfs_result_subtract_exists_result. ((((exists ff_h_pfp_subtract_exists_resultleft. ff_h_pfp_subtract_exists_resultleft + S (pfs_left_subtract_exists_result) = S ((S (pfs_index_subtract_exists_result)) * ac)) /\ exists ff_q_pfp_subtract_exists_resultleft. ab = ff_q_pfp_subtract_exists_resultleft * S ((S (pfs_index_subtract_exists_result)) * ac) + (pfs_left_subtract_exists_result))) /\ (((((exists ff_h_pfp_subtract_exists_resultright. ff_h_pfp_subtract_exists_resultright + S (pfs_right_subtract_exists_result) = S ((S (pfs_index_subtract_exists_result)) * bc)) /\ exists ff_q_pfp_subtract_exists_resultright. bb = ff_q_pfp_subtract_exists_resultright * S ((S (pfs_index_subtract_exists_result)) * bc) + (pfs_right_subtract_exists_result))) /\ (((((exists ff_h_pfp_subtract_exists_resultresult. ff_h_pfp_subtract_exists_resultresult + S (pfs_result_subtract_exists_result) = S ((S (pfs_index_subtract_exists_result)) * rc)) /\ exists ff_q_pfp_subtract_exists_resultresult. rb = ff_q_pfp_subtract_exists_resultresult * S ((S (pfs_index_subtract_exists_result)) * rc) + (pfs_result_subtract_exists_result))) /\ ((((exists pfa_gap_subtract_exists_resultoperationleft. pfa_gap_subtract_exists_resultoperationleft + S (pfs_right_subtract_exists_result) = (p)) /\ (((exists pfa_gap_subtract_exists_resultoperationright. pfa_gap_subtract_exists_resultoperationright + S (pfs_result_subtract_exists_result) = (p)) /\ ((((exists pfa_gap_subtract_exists_resultoperationresultbound. pfa_gap_subtract_exists_resultoperationresultbound + S (pfs_left_subtract_exists_result) = (p)) /\ ((exists pfa_offset_left_subtract_exists_resultoperationresultcongruence pfa_offset_right_subtract_exists_resultoperationresultcongruence. ((pfs_right_subtract_exists_result) + (pfs_result_subtract_exists_result)) + (p) * pfa_offset_left_subtract_exists_resultoperationresultcongruence = (pfs_left_subtract_exists_result) + (p) * pfa_offset_right_subtract_exists_resultoperationresultcongruence))))))))))))))))

Constructive proof overview

Generated structural guide

Construct the entire actual canonical coefficient output by ordinary induction and beta-prefix extension; no output table is assumed.

The unchanged tactic script uses 6 declared prerequisites and contains 124 exact native proof lines.

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

Proof neighborhood

Direct dependencies

PQ000C prime_field_polynomial_subtract_empty le_succ Stable theorem; checked-use authorized zero_add Stable theorem; checked-use authorized PQ0001 prime_field_subtract_exists beta_prefix_extend Stable theorem; checked-use authorized finite_lt_succ_eq_or_lt Stable theorem; checked-use authorized

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

124 script commands · 44 reading checkpoints · 7 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 (2)
prime field polynomial subtract emptyprime field subtract exists

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–7

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 l
  7. L7
    intro hp
02Induction on lL8–10

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L8
    induction l
  2. L9
    intro ha
  3. L10
    intro hb
03Construct an explicit witnessL11–12

Supply the displayed value, then prove that it has the required property.

  1. L11
    exists 0
  2. L12
    exists 0
04Use earlier factsL13–20

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

  1. L13
    specialize prime_field_polynomial_subtract_empty (p)
  2. L14
    specialize prime_field_polynomial_subtract_empty (ab)
  3. L15
    specialize prime_field_polynomial_subtract_empty (ac)
  4. L16
    specialize prime_field_polynomial_subtract_empty (bb)
  5. L17
    specialize prime_field_polynomial_subtract_empty (bc)
  6. L18
    specialize prime_field_polynomial_subtract_empty (0)
  7. L19
    specialize prime_field_polynomial_subtract_empty (0)
  8. L20
    apply prime_field_polynomial_subtract_empty
05Fix variables and assumptionsL21–22

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

  1. L21
    intro ha
  2. L22
    intro hb
06Establish holdL23–32

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

  1. L23
    have hold : ∃ rb. ∃ rc. FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,l)Definitions: FpCoefficientSubtraction
  2. L24
    apply IH
  3. L25
    intro j
  4. L26
    intro hj
  5. L27
    specialize ha (j)
  6. L28
    apply ha
  7. L29
    specialize le_succ (S j)
  8. L30
    specialize le_succ (l)
  9. L31
    apply le_succ
  10. L32
    exact hj
07Fix variables and assumptionsL33–34

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

  1. L33
    intro j
  2. L34
    intro hj
08Use earlier factsL35–40

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

  1. L35
    specialize hb (j)
  2. L36
    apply hb
  3. L37
    specialize le_succ (S j)
  4. L38
    specialize le_succ (l)
  5. L39
    apply le_succ
  6. L40
    exact hj
09Separate the logical casesL41–42

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

  1. L41
    cases hold
  2. L42
    cases hold_witness
10Establish hsource0L43–45

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

  1. L43
    have hsource0 : exists a. ((((exists ff_h_pfp_subtract_last_source0. ff_h_pfp_subtract_last_source0 + S (a) = S ((S (l)) * ac)) /\ exists ff_q_pfp_subtract_last_source0. ab = ff_q_pfp_subtract_last_source0 * S ((S (l)) * ac) + (a))) /\ ((exists pfa_gap_subtract_last_bound0. pfa_gap_subtract_last_bound0 + S (a) = (p))))
  2. L44
    specialize ha (l)
  3. L45
    apply ha
11Construct an explicit witnessL46–46

Supply the displayed value, then prove that it has the required property.

  1. L46
    exists 0
12Use earlier factsL47–47

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

  1. L47
    apply zero_add
13Separate the logical casesL48–49

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

  1. L48
    cases hsource0
  2. L49
    cases hsource0_witness
14Establish hsource1L50–52

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

  1. L50
    have hsource1 : exists a. ((((exists ff_h_pfp_subtract_last_source1. ff_h_pfp_subtract_last_source1 + S (a) = S ((S (l)) * bc)) /\ exists ff_q_pfp_subtract_last_source1. bb = ff_q_pfp_subtract_last_source1 * S ((S (l)) * bc) + (a))) /\ ((exists pfa_gap_subtract_last_bound1. pfa_gap_subtract_last_bound1 + S (a) = (p))))
  2. L51
    specialize hb (l)
  3. L52
    apply hb
15Construct an explicit witnessL53–53

Supply the displayed value, then prove that it has the required property.

  1. L53
    exists 0
16Use earlier factsL54–54

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

  1. L54
    apply zero_add
17Separate the logical casesL55–56

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

  1. L55
    cases hsource1
  2. L56
    cases hsource1_witness
18Establish hvalueL57–64

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field subtract exists.

  1. L57
    have hvalue : exists r. (((exists pfa_gap_subtract_last_valueleft. pfa_gap_subtract_last_valueleft + S (x3) = (p)) /\ (((exists pfa_gap_subtract_last_valueright. pfa_gap_subtract_last_valueright + S (r) = (p)) /\ ((((exists pfa_gap_subtract_last_valueresultbound. pfa_gap_subtract_last_valueresultbound + S (x2) = (p)) /\ ((exists pfa_offset_left_subtract_last_valueresultcongruence pfa_offset_right_subtract_last_valueresultcongruence. ((x3) + (r)) + (p) * pfa_offset_left_subtract_last_valueresultcongruence = (x2) + (p) * pfa_offset_right_subtract_last_valueresultcongruence)))))))))
  2. L58
    specialize prime_field_subtract_exists (p)
  3. L59
    specialize prime_field_subtract_exists (x2)
  4. L60
    specialize prime_field_subtract_exists (x3)
  5. L61
    apply prime_field_subtract_exists
  6. L62
    exact hp
  7. L63
    exact hsource0_witness_right
  8. L64
    exact hsource1_witness_right
19Separate the logical casesL65–65

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

  1. L65
    cases hvalue
20Establish hnewL66–71

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta prefix extend.

  1. L66
    have hnew : ∃ db. ∃ dc. BetaAt(db,dc,l,x4) ∧ (∀ y. ∀ z. Lt(y,l) → BetaAt(x,x1,y,z) → BetaAt(db,dc,y,z))Definitions: LtBetaAt
  2. L67
    specialize beta_prefix_extend (l)
  3. L68
    specialize beta_prefix_extend (x)
  4. L69
    specialize beta_prefix_extend (x1)
  5. L70
    specialize beta_prefix_extend (x4)
  6. L71
    apply beta_prefix_extend
21Separate the logical casesL72–74

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

  1. L72
    cases hnew
  2. L73
    cases hnew_witness
  3. L74
    cases hnew_witness_witness
22Construct an explicit witnessL75–76

Supply the displayed value, then prove that it has the required property.

  1. L75
    exists x5
  2. L76
    exists x6
23Fix variables and assumptionsL77–78

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

  1. L77
    intro j
  2. L78
    intro hj
24Establish hcaseL79–83

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L79
    have hcase : j=l \/ (exists pfa_gap_subtract_index_case. pfa_gap_subtract_index_case + S (j) = (l))
  2. L80
    specialize finite_lt_succ_eq_or_lt (l)
  3. L81
    specialize finite_lt_succ_eq_or_lt (j)
  4. L82
    apply finite_lt_succ_eq_or_lt
  5. L83
    exact hj
25Separate the logical casesL84–84

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

  1. L84
    cases hcase
26Construct an explicit witnessL85–87

Supply the displayed value, then prove that it has the required property.

  1. L85
    exists x2
  2. L86
    exists x3
  3. L87
    exists x4
27Separate the logical casesL88–88

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

  1. L88
    split
28Calculate and transport equalitiesL89–90

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

  1. L89
    rewrite hcase_left
  2. L90
    rewrite hcase_left
29Use earlier factsL91–91

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

  1. L91
    exact hsource0_witness_left
30Separate the logical casesL92–92

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

  1. L92
    split
31Calculate and transport equalitiesL93–94

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

  1. L93
    rewrite hcase_left
  2. L94
    rewrite hcase_left
32Use earlier factsL95–95

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

  1. L95
    exact hsource1_witness_left
33Separate the logical casesL96–96

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

  1. L96
    split
34Calculate and transport equalitiesL97–98

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

  1. L97
    rewrite hcase_left
  2. L98
    rewrite hcase_left
35Use earlier factsL99–100

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

  1. L99
    exact hnew_witness_witness_left
  2. L100
    exact hvalue_witness
36Establish hpreviousL101–104

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

  1. L101
    have hprevious : ∃ v0. ∃ v1. ∃ v2. BetaAt(ab,ac,j,v0) ∧ (BetaAt(bb,bc,j,v1) ∧ (BetaAt(x,x1,j,v2) ∧ FpAdd(p,v1,v2,v0)))Definitions: FpAddBetaAt
  2. L102
    specialize hold_witness_witness (j)
  3. L103
    apply hold_witness_witness
  4. L104
    exact hcase_right
37Separate the logical casesL105–110

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

  1. L105
    cases hprevious
  2. L106
    cases hprevious_witness
  3. L107
    cases hprevious_witness_witness
  4. L108
    cases hprevious_witness_witness_witness
  5. L109
    cases hprevious_witness_witness_witness_right
  6. L110
    cases hprevious_witness_witness_witness_right_right
38Construct an explicit witnessL111–113

Supply the displayed value, then prove that it has the required property.

  1. L111
    exists x7
  2. L112
    exists x8
  3. L113
    exists x9
39Separate the logical casesL114–114

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

  1. L114
    split
40Use earlier factsL115–115

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

  1. L115
    exact hprevious_witness_witness_witness_left
41Separate the logical casesL116–116

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

  1. L116
    split
42Use earlier factsL117–117

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

  1. L117
    exact hprevious_witness_witness_witness_right_left
43Separate the logical casesL118–118

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

  1. L118
    split
44Use earlier factsL119–124

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

  1. L119
    specialize hnew_witness_witness_right (j)
  2. L120
    specialize hnew_witness_witness_right (x9)
  3. L121
    apply hnew_witness_witness_right
  4. L122
    exact hcase_right
  5. L123
    exact hprevious_witness_witness_witness_right_right_left
  6. L124
    exact hprevious_witness_witness_witness_right_right_right

Library-wide reading audit

Original exact command ledger · 124 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro l
  7. 0007intro hp
  8. 0008induction l
  9. 0009intro ha
  10. 0010intro hb
  11. 0011exists 0
  12. 0012exists 0
  13. 0013specialize prime_field_polynomial_subtract_empty (p)
  14. 0014specialize prime_field_polynomial_subtract_empty (ab)
  15. 0015specialize prime_field_polynomial_subtract_empty (ac)
  16. 0016specialize prime_field_polynomial_subtract_empty (bb)
  17. 0017specialize prime_field_polynomial_subtract_empty (bc)
  18. 0018specialize prime_field_polynomial_subtract_empty (0)
  19. 0019specialize prime_field_polynomial_subtract_empty (0)
  20. 0020apply prime_field_polynomial_subtract_empty
  21. 0021intro ha
  22. 0022intro hb
  23. 0023have hold : exists rb rc. (forall pfs_index_subtract_old. (exists pfa_gap_subtract_oldindex. pfa_gap_subtract_oldindex + S (pfs_index_subtract_old) = (l)) -> exists pfs_left_subtract_old pfs_right_subtract_old pfs_result_subtract_old. ((((exists ff_h_pfp_subtract_oldleft. ff_h_pfp_subtract_oldleft + S (pfs_left_subtract_old) = S ((S (pfs_index_subtract_old)) * ac)) /\ exists ff_q_pfp_subtract_oldleft. ab = ff_q_pfp_subtract_oldleft * S ((S (pfs_index_subtract_old)) * ac) + (pfs_left_subtract_old))) /\ (((((exists ff_h_pfp_subtract_oldright. ff_h_pfp_subtract_oldright + S (pfs_right_subtract_old) = S ((S (pfs_index_subtract_old)) * bc)) /\ exists ff_q_pfp_subtract_oldright. bb = ff_q_pfp_subtract_oldright * S ((S (pfs_index_subtract_old)) * bc) + (pfs_right_subtract_old))) /\ (((((exists ff_h_pfp_subtract_oldresult. ff_h_pfp_subtract_oldresult + S (pfs_result_subtract_old) = S ((S (pfs_index_subtract_old)) * rc)) /\ exists ff_q_pfp_subtract_oldresult. rb = ff_q_pfp_subtract_oldresult * S ((S (pfs_index_subtract_old)) * rc) + (pfs_result_subtract_old))) /\ ((((exists pfa_gap_subtract_oldoperationleft. pfa_gap_subtract_oldoperationleft + S (pfs_right_subtract_old) = (p)) /\ (((exists pfa_gap_subtract_oldoperationright. pfa_gap_subtract_oldoperationright + S (pfs_result_subtract_old) = (p)) /\ ((((exists pfa_gap_subtract_oldoperationresultbound. pfa_gap_subtract_oldoperationresultbound + S (pfs_left_subtract_old) = (p)) /\ ((exists pfa_offset_left_subtract_oldoperationresultcongruence pfa_offset_right_subtract_oldoperationresultcongruence. ((pfs_right_subtract_old) + (pfs_result_subtract_old)) + (p) * pfa_offset_left_subtract_oldoperationresultcongruence = (pfs_left_subtract_old) + (p) * pfa_offset_right_subtract_oldoperationresultcongruence))))))))))))))))
  24. 0024apply IH
  25. 0025intro j
  26. 0026intro hj
  27. 0027specialize ha (j)
  28. 0028apply ha
  29. 0029specialize le_succ (S j)
  30. 0030specialize le_succ (l)
  31. 0031apply le_succ
  32. 0032exact hj
  33. 0033intro j
  34. 0034intro hj
  35. 0035specialize hb (j)
  36. 0036apply hb
  37. 0037specialize le_succ (S j)
  38. 0038specialize le_succ (l)
  39. 0039apply le_succ
  40. 0040exact hj
  41. 0041cases hold
  42. 0042cases hold_witness
  43. 0043have hsource0 : exists a. ((((exists ff_h_pfp_subtract_last_source0. ff_h_pfp_subtract_last_source0 + S (a) = S ((S (l)) * ac)) /\ exists ff_q_pfp_subtract_last_source0. ab = ff_q_pfp_subtract_last_source0 * S ((S (l)) * ac) + (a))) /\ ((exists pfa_gap_subtract_last_bound0. pfa_gap_subtract_last_bound0 + S (a) = (p))))
  44. 0044specialize ha (l)
  45. 0045apply ha
  46. 0046exists 0
  47. 0047apply zero_add
  48. 0048cases hsource0
  49. 0049cases hsource0_witness
  50. 0050have hsource1 : exists a. ((((exists ff_h_pfp_subtract_last_source1. ff_h_pfp_subtract_last_source1 + S (a) = S ((S (l)) * bc)) /\ exists ff_q_pfp_subtract_last_source1. bb = ff_q_pfp_subtract_last_source1 * S ((S (l)) * bc) + (a))) /\ ((exists pfa_gap_subtract_last_bound1. pfa_gap_subtract_last_bound1 + S (a) = (p))))
  51. 0051specialize hb (l)
  52. 0052apply hb
  53. 0053exists 0
  54. 0054apply zero_add
  55. 0055cases hsource1
  56. 0056cases hsource1_witness
  57. 0057have hvalue : exists r. (((exists pfa_gap_subtract_last_valueleft. pfa_gap_subtract_last_valueleft + S (x3) = (p)) /\ (((exists pfa_gap_subtract_last_valueright. pfa_gap_subtract_last_valueright + S (r) = (p)) /\ ((((exists pfa_gap_subtract_last_valueresultbound. pfa_gap_subtract_last_valueresultbound + S (x2) = (p)) /\ ((exists pfa_offset_left_subtract_last_valueresultcongruence pfa_offset_right_subtract_last_valueresultcongruence. ((x3) + (r)) + (p) * pfa_offset_left_subtract_last_valueresultcongruence = (x2) + (p) * pfa_offset_right_subtract_last_valueresultcongruence)))))))))
  58. 0058specialize prime_field_subtract_exists (p)
  59. 0059specialize prime_field_subtract_exists (x2)
  60. 0060specialize prime_field_subtract_exists (x3)
  61. 0061apply prime_field_subtract_exists
  62. 0062exact hp
  63. 0063exact hsource0_witness_right
  64. 0064exact hsource1_witness_right
  65. 0065cases hvalue
  66. 0066have hnew : exists db dc. (((((exists ff_h_pfp_subtract_append. ff_h_pfp_subtract_append + S (x4) = S ((S (l)) * dc)) /\ exists ff_q_pfp_subtract_append. db = ff_q_pfp_subtract_append * S ((S (l)) * dc) + (x4))) /\ ((forall mdr_i_pfp_subtract_preserve mdr_a_pfp_subtract_preserve. (exists mdr_gap_pfp_subtract_preserveb. mdr_gap_pfp_subtract_preserveb + S (mdr_i_pfp_subtract_preserve) = (l)) -> (((exists ff_h_mdr_pfp_subtract_preserveo. ff_h_mdr_pfp_subtract_preserveo + S (mdr_a_pfp_subtract_preserve) = S ((S (mdr_i_pfp_subtract_preserve)) * x1)) /\ exists ff_q_mdr_pfp_subtract_preserveo. x = ff_q_mdr_pfp_subtract_preserveo * S ((S (mdr_i_pfp_subtract_preserve)) * x1) + (mdr_a_pfp_subtract_preserve))) -> (((exists ff_h_mdr_pfp_subtract_preserven. ff_h_mdr_pfp_subtract_preserven + S (mdr_a_pfp_subtract_preserve) = S ((S (mdr_i_pfp_subtract_preserve)) * dc)) /\ exists ff_q_mdr_pfp_subtract_preserven. db = ff_q_mdr_pfp_subtract_preserven * S ((S (mdr_i_pfp_subtract_preserve)) * dc) + (mdr_a_pfp_subtract_preserve)))))))
  67. 0067specialize beta_prefix_extend (l)
  68. 0068specialize beta_prefix_extend (x)
  69. 0069specialize beta_prefix_extend (x1)
  70. 0070specialize beta_prefix_extend (x4)
  71. 0071apply beta_prefix_extend
  72. 0072cases hnew
  73. 0073cases hnew_witness
  74. 0074cases hnew_witness_witness
  75. 0075exists x5
  76. 0076exists x6
  77. 0077intro j
  78. 0078intro hj
  79. 0079have hcase : j=l \/ (exists pfa_gap_subtract_index_case. pfa_gap_subtract_index_case + S (j) = (l))
  80. 0080specialize finite_lt_succ_eq_or_lt (l)
  81. 0081specialize finite_lt_succ_eq_or_lt (j)
  82. 0082apply finite_lt_succ_eq_or_lt
  83. 0083exact hj
  84. 0084cases hcase
  85. 0085exists x2
  86. 0086exists x3
  87. 0087exists x4
  88. 0088split
  89. 0089rewrite hcase_left
  90. 0090rewrite hcase_left
  91. 0091exact hsource0_witness_left
  92. 0092split
  93. 0093rewrite hcase_left
  94. 0094rewrite hcase_left
  95. 0095exact hsource1_witness_left
  96. 0096split
  97. 0097rewrite hcase_left
  98. 0098rewrite hcase_left
  99. 0099exact hnew_witness_witness_left
  100. 0100exact hvalue_witness
  101. 0101have hprevious : exists v0 v1 v2. (((((exists ff_h_pfp_subtract_previous0. ff_h_pfp_subtract_previous0 + S (v0) = S ((S (j)) * ac)) /\ exists ff_q_pfp_subtract_previous0. ab = ff_q_pfp_subtract_previous0 * S ((S (j)) * ac) + (v0))) /\ (((((exists ff_h_pfp_subtract_previous1. ff_h_pfp_subtract_previous1 + S (v1) = S ((S (j)) * bc)) /\ exists ff_q_pfp_subtract_previous1. bb = ff_q_pfp_subtract_previous1 * S ((S (j)) * bc) + (v1))) /\ (((((exists ff_h_pfp_subtract_previous2. ff_h_pfp_subtract_previous2 + S (v2) = S ((S (j)) * x1)) /\ exists ff_q_pfp_subtract_previous2. x = ff_q_pfp_subtract_previous2 * S ((S (j)) * x1) + (v2))) /\ ((((exists pfa_gap_subtract_previousoperationleft. pfa_gap_subtract_previousoperationleft + S (v1) = (p)) /\ (((exists pfa_gap_subtract_previousoperationright. pfa_gap_subtract_previousoperationright + S (v2) = (p)) /\ ((((exists pfa_gap_subtract_previousoperationresultbound. pfa_gap_subtract_previousoperationresultbound + S (v0) = (p)) /\ ((exists pfa_offset_left_subtract_previousoperationresultcongruence pfa_offset_right_subtract_previousoperationresultcongruence. ((v1) + (v2)) + (p) * pfa_offset_left_subtract_previousoperationresultcongruence = (v0) + (p) * pfa_offset_right_subtract_previousoperationresultcongruence))))))))))))))))
  102. 0102specialize hold_witness_witness (j)
  103. 0103apply hold_witness_witness
  104. 0104exact hcase_right
  105. 0105cases hprevious
  106. 0106cases hprevious_witness
  107. 0107cases hprevious_witness_witness
  108. 0108cases hprevious_witness_witness_witness
  109. 0109cases hprevious_witness_witness_witness_right
  110. 0110cases hprevious_witness_witness_witness_right_right
  111. 0111exists x7
  112. 0112exists x8
  113. 0113exists x9
  114. 0114split
  115. 0115exact hprevious_witness_witness_witness_left
  116. 0116split
  117. 0117exact hprevious_witness_witness_witness_right_left
  118. 0118split
  119. 0119specialize hnew_witness_witness_right (j)
  120. 0120specialize hnew_witness_witness_right (x9)
  121. 0121apply hnew_witness_witness_right
  122. 0122exact hcase_right
  123. 0123exact hprevious_witness_witness_witness_right_right_left
  124. 0124exact hprevious_witness_witness_witness_right_right_right