PX002E

prime_field_polynomial_quotient_prefix_exists

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

Construct every quotient coefficient with actual sum, subtraction, inverse-scaling and beta-extension witnesses, by ordinary finite induction.

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 k ab ac bb bc M N. (~((p) = 1) /\ forall pfa_factor_left_division_exists_prime pfa_factor_right_division_exists_prime. (p) = pfa_factor_left_division_exists_prime * pfa_factor_right_division_exists_prime -> pfa_factor_left_division_exists_prime = 1 \/ pfa_factor_right_division_exists_prime = 1) -> (exists pfa_gap_division_exists_scalar. pfa_gap_division_exists_scalar + S (k) = (p)) -> (forall fom_index_pfp_division_exists_source. (exists fom_gap_pfp_division_exists_source_index_bound. fom_gap_pfp_division_exists_source_index_bound + S (fom_index_pfp_division_exists_source) = N) -> exists fom_value_pfp_division_exists_source. ((((exists fom_beta_height_pfp_division_exists_source_entry. fom_beta_height_pfp_division_exists_source_entry + S (fom_value_pfp_division_exists_source) = S ((S (fom_index_pfp_division_exists_source)) * ac)) /\ exists fom_beta_quotient_pfp_division_exists_source_entry. ab = fom_beta_quotient_pfp_division_exists_source_entry * S ((S (fom_index_pfp_division_exists_source)) * ac) + (fom_value_pfp_division_exists_source))) /\ (exists fom_gap_pfp_division_exists_source_value_bound. fom_gap_pfp_division_exists_source_value_bound + S (fom_value_pfp_division_exists_source) = p))) -> exists qb qc. (forall pfd_index_division_exists_result. (exists pfa_gap_division_exists_resultbound. pfa_gap_division_exists_resultbound + S (pfd_index_division_exists_result) = (N)) -> exists pfd_value_division_exists_result. ((((exists ff_h_pfp_division_exists_resultentry. ff_h_pfp_division_exists_resultentry + S (pfd_value_division_exists_result) = S ((S (pfd_index_division_exists_result)) * qc)) /\ exists ff_q_pfp_division_exists_resultentry. qb = ff_q_pfp_division_exists_resultentry * S ((S (pfd_index_division_exists_result)) * qc) + (pfd_value_division_exists_result))) /\ ((exists pfd_input_division_exists_resultstep pfd_previous_division_exists_resultstep pfd_difference_division_exists_resultstep. ((((exists ff_h_pfp_division_exists_resultstepinput. ff_h_pfp_division_exists_resultstepinput + S (pfd_input_division_exists_resultstep) = S ((S (pfd_index_division_exists_result)) * ac)) /\ exists ff_q_pfp_division_exists_resultstepinput. ab = ff_q_pfp_division_exists_resultstepinput * S ((S (pfd_index_division_exists_result)) * ac) + (pfd_input_division_exists_resultstep))) /\ (((exists pfc_terms_code_division_exists_resultstepprevious pfc_terms_scale_division_exists_resultstepprevious pfc_natural_sum_division_exists_resultstepprevious. ((forall pfc_index_division_exists_resultsteppreviousdiagonal. (exists pfa_gap_division_exists_resultsteppreviousdiagonalbound. pfa_gap_division_exists_resultsteppreviousdiagonalbound + S (pfc_index_division_exists_resultsteppreviousdiagonal) = (S (pfd_index_division_exists_result))) -> exists pfc_value_division_exists_resultsteppreviousdiagonal. ((((exists ff_h_pfp_division_exists_resultsteppreviousdiagonalentry. ff_h_pfp_division_exists_resultsteppreviousdiagonalentry + S (pfc_value_division_exists_resultsteppreviousdiagonal) = S ((S (pfc_index_division_exists_resultsteppreviousdiagonal)) * pfc_terms_scale_division_exists_resultstepprevious)) /\ exists ff_q_pfp_division_exists_resultsteppreviousdiagonalentry. pfc_terms_code_division_exists_resultstepprevious = ff_q_pfp_division_exists_resultsteppreviousdiagonalentry * S ((S (pfc_index_division_exists_resultsteppreviousdiagonal)) * pfc_terms_scale_division_exists_resultstepprevious) + (pfc_value_division_exists_resultsteppreviousdiagonal))) /\ ((exists pfc_complement_division_exists_resultsteppreviousdiagonalterm pfc_left_division_exists_resultsteppreviousdiagonalterm pfc_right_division_exists_resultsteppreviousdiagonalterm. (((pfc_index_division_exists_resultsteppreviousdiagonal)+pfc_complement_division_exists_resultsteppreviousdiagonalterm=(pfd_index_division_exists_result)) /\ ((((((exists pfa_gap_division_exists_resultsteppreviousdiagonaltermleftinside. pfa_gap_division_exists_resultsteppreviousdiagonaltermleftinside + S (pfc_index_division_exists_resultsteppreviousdiagonal) = (pfd_index_division_exists_result)) /\ ((((exists ff_h_pfp_division_exists_resultsteppreviousdiagonaltermleftentry. ff_h_pfp_division_exists_resultsteppreviousdiagonaltermleftentry + S (pfc_left_division_exists_resultsteppreviousdiagonalterm) = S ((S (pfc_index_division_exists_resultsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_exists_resultsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_exists_resultsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_exists_resultsteppreviousdiagonal)) * qc) + (pfc_left_division_exists_resultsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_exists_resultsteppreviousdiagonaltermleftoutside. pfc_gap_division_exists_resultsteppreviousdiagonaltermleftoutside+(pfd_index_division_exists_result)=(pfc_index_division_exists_resultsteppreviousdiagonal)) /\ (((pfc_left_division_exists_resultsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_exists_resultsteppreviousdiagonaltermrightinside. pfa_gap_division_exists_resultsteppreviousdiagonaltermrightinside + S (pfc_complement_division_exists_resultsteppreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_division_exists_resultsteppreviousdiagonaltermrightentry. ff_h_pfp_division_exists_resultsteppreviousdiagonaltermrightentry + S (pfc_right_division_exists_resultsteppreviousdiagonalterm) = S ((S (pfc_complement_division_exists_resultsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_exists_resultsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_exists_resultsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_exists_resultsteppreviousdiagonalterm)) * bc) + (pfc_right_division_exists_resultsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_exists_resultsteppreviousdiagonaltermrightoutside. pfc_gap_division_exists_resultsteppreviousdiagonaltermrightoutside+(M)=(pfc_complement_division_exists_resultsteppreviousdiagonalterm)) /\ (((pfc_right_division_exists_resultsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_exists_resultsteppreviousdiagonal)=pfc_left_division_exists_resultsteppreviousdiagonalterm*pfc_right_division_exists_resultsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_exists_resultstepprevioussum fs_v_pfc_division_exists_resultstepprevioussum. ((((exists fs_h_pfc_division_exists_resultstepprevioussum_body_start. fs_h_pfc_division_exists_resultstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_exists_resultstepprevioussum)) /\ exists fs_q_pfc_division_exists_resultstepprevioussum_body_start. fs_u_pfc_division_exists_resultstepprevioussum = fs_q_pfc_division_exists_resultstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_exists_resultstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_exists_resultstepprevioussum_body_terminal. fs_h_pfc_division_exists_resultstepprevioussum_body_terminal + S (pfc_natural_sum_division_exists_resultstepprevious) = S ((S (S (pfd_index_division_exists_result))) * fs_v_pfc_division_exists_resultstepprevioussum)) /\ exists fs_q_pfc_division_exists_resultstepprevioussum_body_terminal. fs_u_pfc_division_exists_resultstepprevioussum = fs_q_pfc_division_exists_resultstepprevioussum_body_terminal * S ((S (S (pfd_index_division_exists_result))) * fs_v_pfc_division_exists_resultstepprevioussum) + (pfc_natural_sum_division_exists_resultstepprevious))) /\ forall fs_i_pfc_division_exists_resultstepprevioussum_body_steps. (exists fs_lt_pfc_division_exists_resultstepprevioussum_body_steps_bound. fs_lt_pfc_division_exists_resultstepprevioussum_body_steps_bound + S fs_i_pfc_division_exists_resultstepprevioussum_body_steps = S (pfd_index_division_exists_result)) -> exists fs_a_pfc_division_exists_resultstepprevioussum_body_steps fs_r_pfc_division_exists_resultstepprevioussum_body_steps fs_s_pfc_division_exists_resultstepprevioussum_body_steps. ((((exists fs_h_pfc_division_exists_resultstepprevioussum_body_steps_summand. fs_h_pfc_division_exists_resultstepprevioussum_body_steps_summand + S (fs_a_pfc_division_exists_resultstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_exists_resultstepprevioussum_body_steps)) * pfc_terms_scale_division_exists_resultstepprevious)) /\ exists fs_q_pfc_division_exists_resultstepprevioussum_body_steps_summand. pfc_terms_code_division_exists_resultstepprevious = fs_q_pfc_division_exists_resultstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_exists_resultstepprevioussum_body_steps)) * pfc_terms_scale_division_exists_resultstepprevious) + (fs_a_pfc_division_exists_resultstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_exists_resultstepprevioussum_body_steps_partial. fs_h_pfc_division_exists_resultstepprevioussum_body_steps_partial + S (fs_r_pfc_division_exists_resultstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_exists_resultstepprevioussum_body_steps)) * fs_v_pfc_division_exists_resultstepprevioussum)) /\ exists fs_q_pfc_division_exists_resultstepprevioussum_body_steps_partial. fs_u_pfc_division_exists_resultstepprevioussum = fs_q_pfc_division_exists_resultstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_exists_resultstepprevioussum_body_steps)) * fs_v_pfc_division_exists_resultstepprevioussum) + (fs_r_pfc_division_exists_resultstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_exists_resultstepprevioussum_body_steps_successor. fs_h_pfc_division_exists_resultstepprevioussum_body_steps_successor + S (fs_s_pfc_division_exists_resultstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_exists_resultstepprevioussum_body_steps)) * fs_v_pfc_division_exists_resultstepprevioussum)) /\ exists fs_q_pfc_division_exists_resultstepprevioussum_body_steps_successor. fs_u_pfc_division_exists_resultstepprevioussum = fs_q_pfc_division_exists_resultstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_exists_resultstepprevioussum_body_steps)) * fs_v_pfc_division_exists_resultstepprevioussum) + (fs_s_pfc_division_exists_resultstepprevioussum_body_steps))) /\ fs_s_pfc_division_exists_resultstepprevioussum_body_steps = fs_r_pfc_division_exists_resultstepprevioussum_body_steps + fs_a_pfc_division_exists_resultstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_exists_resultsteppreviousresiduebound. pfa_gap_division_exists_resultsteppreviousresiduebound + S (pfd_previous_division_exists_resultstep) = (p)) /\ ((exists pfa_offset_left_division_exists_resultsteppreviousresiduecongruence pfa_offset_right_division_exists_resultsteppreviousresiduecongruence. (pfc_natural_sum_division_exists_resultstepprevious) + (p) * pfa_offset_left_division_exists_resultsteppreviousresiduecongruence = (pfd_previous_division_exists_resultstep) + (p) * pfa_offset_right_division_exists_resultsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_exists_resultstepsubtractleft. pfa_gap_division_exists_resultstepsubtractleft + S (pfd_previous_division_exists_resultstep) = (p)) /\ (((exists pfa_gap_division_exists_resultstepsubtractright. pfa_gap_division_exists_resultstepsubtractright + S (pfd_difference_division_exists_resultstep) = (p)) /\ ((((exists pfa_gap_division_exists_resultstepsubtractresultbound. pfa_gap_division_exists_resultstepsubtractresultbound + S (pfd_input_division_exists_resultstep) = (p)) /\ ((exists pfa_offset_left_division_exists_resultstepsubtractresultcongruence pfa_offset_right_division_exists_resultstepsubtractresultcongruence. ((pfd_previous_division_exists_resultstep) + (pfd_difference_division_exists_resultstep)) + (p) * pfa_offset_left_division_exists_resultstepsubtractresultcongruence = (pfd_input_division_exists_resultstep) + (p) * pfa_offset_right_division_exists_resultstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_exists_resultstepmultiplyleft. pfa_gap_division_exists_resultstepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_exists_resultstepmultiplyright. pfa_gap_division_exists_resultstepmultiplyright + S (pfd_difference_division_exists_resultstep) = (p)) /\ ((((exists pfa_gap_division_exists_resultstepmultiplyresultbound. pfa_gap_division_exists_resultstepmultiplyresultbound + S (pfd_value_division_exists_result) = (p)) /\ ((exists pfa_offset_left_division_exists_resultstepmultiplyresultcongruence pfa_offset_right_division_exists_resultstepmultiplyresultcongruence. ((k) * (pfd_difference_division_exists_resultstep)) + (p) * pfa_offset_left_division_exists_resultstepmultiplyresultcongruence = (pfd_value_division_exists_result) + (p) * pfa_offset_right_division_exists_resultstepmultiplyresultcongruence)))))))))))))))))))

Constructive proof overview

Generated structural guide

Construct every quotient coefficient with actual sum, subtraction, inverse-scaling and beta-extension witnesses, by ordinary finite induction.

The unchanged tactic script uses 10 declared prerequisites and contains 128 exact native proof lines.

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

Proof neighborhood

Direct dependencies

PX0029 prime_field_polynomial_quotient_prefix_empty le_succ Alpha theorem; checked-use authorized le_refl Alpha theorem; checked-use authorized prime_field_convolution_coefficient_exists Alpha theorem; checked-use authorized prime_nonzero Alpha theorem; checked-use authorized prime_field_subtract_exists Alpha theorem; checked-use authorized prime_field_convolution_coefficient_bounded Alpha theorem; checked-use authorized prime_field_multiply_exists Alpha theorem; checked-use authorized beta_prefix_extend Alpha theorem; checked-use authorized PX002D prime_field_polynomial_quotient_prefix_append

Direct dependents

PX0037 prime_field_polynomial_division_quotient_data_exists

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

128 script commands · 32 reading checkpoints · 6 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 quotient prefix emptyprime field polynomial quotient prefix append

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 k
  3. L3
    intro ab
  4. L4
    intro ac
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro M
  8. L8
    intro N
  9. L9
    intro hp
  10. L10
    intro hk
02Induction on NL11–12

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

  1. L11
    induction N
  2. L12
    intro ha
03Construct an explicit witnessL13–14

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

  1. L13
    exists 0
  2. L14
    exists 0
04Use earlier factsL15–24

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

  1. L15
    specialize prime_field_polynomial_quotient_prefix_empty (p)
  2. L16
    specialize prime_field_polynomial_quotient_prefix_empty (k)
  3. L17
    specialize prime_field_polynomial_quotient_prefix_empty (ab)
  4. L18
    specialize prime_field_polynomial_quotient_prefix_empty (ac)
  5. L19
    specialize prime_field_polynomial_quotient_prefix_empty (bb)
  6. L20
    specialize prime_field_polynomial_quotient_prefix_empty (bc)
  7. L21
    specialize prime_field_polynomial_quotient_prefix_empty (M)
  8. L22
    specialize prime_field_polynomial_quotient_prefix_empty (0)
  9. L23
    specialize prime_field_polynomial_quotient_prefix_empty (0)
  10. L24
    apply prime_field_polynomial_quotient_prefix_empty
05Fix variables and assumptionsL25–25

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

  1. L25
    intro ha
06Establish holdL26–35

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

  1. L26
    have hold : ∃ qb. ∃ qc. FpPolynomialQuotientPrefix(p,k,ab,ac,bb,bc,M,qb,qc,N)Definitions: FpPolynomialQuotientPrefix
  2. L27
    apply IH
  3. L28
    intro i
  4. L29
    intro hi
  5. L30
    specialize ha (i)
  6. L31
    apply ha
  7. L32
    specialize le_succ (S i)
  8. L33
    specialize le_succ (N)
  9. L34
    apply le_succ
  10. L35
    exact hi
07Separate the logical casesL36–37

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

  1. L36
    cases hold
  2. L37
    cases hold_witness
08Establish hinputL38–42

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

  1. L38
    have hinput : exists a. ((((exists ff_h_pfp_division_exists_input. ff_h_pfp_division_exists_input + S (a) = S ((S (N)) * ac)) /\ exists ff_q_pfp_division_exists_input. ab = ff_q_pfp_division_exists_input * S ((S (N)) * ac) + (a))) /\ ((exists pfa_gap_division_exists_input_bound. pfa_gap_division_exists_input_bound + S (a) = (p))))
  2. L39
    specialize ha (N)
  3. L40
    apply ha
  4. L41
    specialize le_refl (S N)
  5. L42
    apply le_refl
09Separate the logical casesL43–44

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

  1. L43
    cases hinput
  2. L44
    cases hinput_witness
10Establish hcL45–54

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

  1. L45
    have hc : ∃ c. FpConvolutionCoefficient(p,x,x1,N,bb,bc,M,N,c)Definitions: FpConvolutionCoefficient
  2. L46
    specialize prime_field_convolution_coefficient_exists (p)
  3. L47
    specialize prime_field_convolution_coefficient_exists (x)
  4. L48
    specialize prime_field_convolution_coefficient_exists (x1)
  5. L49
    specialize prime_field_convolution_coefficient_exists (N)
  6. L50
    specialize prime_field_convolution_coefficient_exists (bb)
  7. L51
    specialize prime_field_convolution_coefficient_exists (bc)
  8. L52
    specialize prime_field_convolution_coefficient_exists (M)
  9. L53
    specialize prime_field_convolution_coefficient_exists (N)
  10. L54
    apply prime_field_convolution_coefficient_exists
11Fix variables and assumptionsL55–55

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

  1. L55
    intro hz
12Use earlier factsL56–59

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

  1. L56
    specialize prime_nonzero (p)
  2. L57
    apply prime_nonzero
  3. L58
    exact hp
  4. L59
    exact hz
13Separate the logical casesL60–60

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

  1. L60
    cases hc
14Establish hsL61–70

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

  1. L61
    have hs : ∃ s. FpAdd(p,x3,s,x2)Definitions: FpAdd
  2. L62
    specialize prime_field_subtract_exists (p)
  3. L63
    specialize prime_field_subtract_exists (x2)
  4. L64
    specialize prime_field_subtract_exists (x3)
  5. L65
    apply prime_field_subtract_exists
  6. L66
    exact hp
  7. L67
    exact hinput_witness_right
  8. L68
    specialize prime_field_convolution_coefficient_bounded (p)
  9. L69
    specialize prime_field_convolution_coefficient_bounded (x)
  10. L70
    specialize prime_field_convolution_coefficient_bounded (x1)
15Use earlier factsL71–78

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

  1. L71
    specialize prime_field_convolution_coefficient_bounded (N)
  2. L72
    specialize prime_field_convolution_coefficient_bounded (bb)
  3. L73
    specialize prime_field_convolution_coefficient_bounded (bc)
  4. L74
    specialize prime_field_convolution_coefficient_bounded (M)
  5. L75
    specialize prime_field_convolution_coefficient_bounded (N)
  6. L76
    specialize prime_field_convolution_coefficient_bounded (x3)
  7. L77
    apply prime_field_convolution_coefficient_bounded
  8. L78
    exact hc_witness
16Separate the logical casesL79–79

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

  1. L79
    cases hs
17Establish hqL80–86

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

  1. L80
    have hq : ∃ q. FpMul(p,k,x4,q)Definitions: FpMul
  2. L81
    specialize prime_field_multiply_exists (p)
  3. L82
    specialize prime_field_multiply_exists (k)
  4. L83
    specialize prime_field_multiply_exists (x4)
  5. L84
    apply prime_field_multiply_exists
  6. L85
    exact hp
  7. L86
    exact hk
18Separate the logical casesL87–88

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

  1. L87
    cases hs_witness
  2. L88
    cases hs_witness_right
19Use earlier factsL89–89

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

  1. L89
    exact hs_witness_right_left
20Separate the logical casesL90–90

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

  1. L90
    cases hq
21Establish hnewL91–96

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

  1. L91
    have hnew : ∃ QB. ∃ QC. BetaAt(QB,QC,N,x5) ∧ BetaPrefixEqual(x,x1,QB,QC,N)Definitions: BetaPrefixEqualBetaAt
  2. L92
    specialize beta_prefix_extend (N)
  3. L93
    specialize beta_prefix_extend (x)
  4. L94
    specialize beta_prefix_extend (x1)
  5. L95
    specialize beta_prefix_extend (x5)
  6. L96
    apply beta_prefix_extend
22Separate the logical casesL97–99

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

  1. L97
    cases hnew
  2. L98
    cases hnew_witness
  3. L99
    cases hnew_witness_witness
23Construct an explicit witnessL100–101

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

  1. L100
    exists x6
  2. L101
    exists x7
24Use earlier factsL102–111

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

  1. L102
    specialize prime_field_polynomial_quotient_prefix_append (p)
  2. L103
    specialize prime_field_polynomial_quotient_prefix_append (k)
  3. L104
    specialize prime_field_polynomial_quotient_prefix_append (ab)
  4. L105
    specialize prime_field_polynomial_quotient_prefix_append (ac)
  5. L106
    specialize prime_field_polynomial_quotient_prefix_append (bb)
  6. L107
    specialize prime_field_polynomial_quotient_prefix_append (bc)
  7. L108
    specialize prime_field_polynomial_quotient_prefix_append (M)
  8. L109
    specialize prime_field_polynomial_quotient_prefix_append (x)
  9. L110
    specialize prime_field_polynomial_quotient_prefix_append (x1)
  10. L111
    specialize prime_field_polynomial_quotient_prefix_append (x6)
25Use earlier factsL112–118

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

  1. L112
    specialize prime_field_polynomial_quotient_prefix_append (x7)
  2. L113
    specialize prime_field_polynomial_quotient_prefix_append (N)
  3. L114
    specialize prime_field_polynomial_quotient_prefix_append (x5)
  4. L115
    apply prime_field_polynomial_quotient_prefix_append
  5. L116
    exact hold_witness_witness
  6. L117
    exact hnew_witness_witness_right
  7. L118
    exact hnew_witness_witness_left
26Construct an explicit witnessL119–121

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

  1. L119
    exists x2
  2. L120
    exists x3
  3. L121
    exists x4
27Separate the logical casesL122–122

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

  1. L122
    split
28Use earlier factsL123–123

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

  1. L123
    exact hinput_witness_left
29Separate the logical casesL124–124

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

  1. L124
    split
30Use earlier factsL125–125

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

  1. L125
    exact hc_witness
31Separate the logical casesL126–126

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

  1. L126
    split
32Use earlier factsL127–128

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

  1. L127
    exact hs_witness
  2. L128
    exact hq_witness

Library-wide reading audit

Original exact command ledger · 128 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro ab
  4. 0004intro ac
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro M
  8. 0008intro N
  9. 0009intro hp
  10. 0010intro hk
  11. 0011induction N
  12. 0012intro ha
  13. 0013exists 0
  14. 0014exists 0
  15. 0015specialize prime_field_polynomial_quotient_prefix_empty (p)
  16. 0016specialize prime_field_polynomial_quotient_prefix_empty (k)
  17. 0017specialize prime_field_polynomial_quotient_prefix_empty (ab)
  18. 0018specialize prime_field_polynomial_quotient_prefix_empty (ac)
  19. 0019specialize prime_field_polynomial_quotient_prefix_empty (bb)
  20. 0020specialize prime_field_polynomial_quotient_prefix_empty (bc)
  21. 0021specialize prime_field_polynomial_quotient_prefix_empty (M)
  22. 0022specialize prime_field_polynomial_quotient_prefix_empty (0)
  23. 0023specialize prime_field_polynomial_quotient_prefix_empty (0)
  24. 0024apply prime_field_polynomial_quotient_prefix_empty
  25. 0025intro ha
  26. 0026have hold : exists qb qc. (forall pfd_index_division_exists_old. (exists pfa_gap_division_exists_oldbound. pfa_gap_division_exists_oldbound + S (pfd_index_division_exists_old) = (N)) -> exists pfd_value_division_exists_old. ((((exists ff_h_pfp_division_exists_oldentry. ff_h_pfp_division_exists_oldentry + S (pfd_value_division_exists_old) = S ((S (pfd_index_division_exists_old)) * qc)) /\ exists ff_q_pfp_division_exists_oldentry. qb = ff_q_pfp_division_exists_oldentry * S ((S (pfd_index_division_exists_old)) * qc) + (pfd_value_division_exists_old))) /\ ((exists pfd_input_division_exists_oldstep pfd_previous_division_exists_oldstep pfd_difference_division_exists_oldstep. ((((exists ff_h_pfp_division_exists_oldstepinput. ff_h_pfp_division_exists_oldstepinput + S (pfd_input_division_exists_oldstep) = S ((S (pfd_index_division_exists_old)) * ac)) /\ exists ff_q_pfp_division_exists_oldstepinput. ab = ff_q_pfp_division_exists_oldstepinput * S ((S (pfd_index_division_exists_old)) * ac) + (pfd_input_division_exists_oldstep))) /\ (((exists pfc_terms_code_division_exists_oldstepprevious pfc_terms_scale_division_exists_oldstepprevious pfc_natural_sum_division_exists_oldstepprevious. ((forall pfc_index_division_exists_oldsteppreviousdiagonal. (exists pfa_gap_division_exists_oldsteppreviousdiagonalbound. pfa_gap_division_exists_oldsteppreviousdiagonalbound + S (pfc_index_division_exists_oldsteppreviousdiagonal) = (S (pfd_index_division_exists_old))) -> exists pfc_value_division_exists_oldsteppreviousdiagonal. ((((exists ff_h_pfp_division_exists_oldsteppreviousdiagonalentry. ff_h_pfp_division_exists_oldsteppreviousdiagonalentry + S (pfc_value_division_exists_oldsteppreviousdiagonal) = S ((S (pfc_index_division_exists_oldsteppreviousdiagonal)) * pfc_terms_scale_division_exists_oldstepprevious)) /\ exists ff_q_pfp_division_exists_oldsteppreviousdiagonalentry. pfc_terms_code_division_exists_oldstepprevious = ff_q_pfp_division_exists_oldsteppreviousdiagonalentry * S ((S (pfc_index_division_exists_oldsteppreviousdiagonal)) * pfc_terms_scale_division_exists_oldstepprevious) + (pfc_value_division_exists_oldsteppreviousdiagonal))) /\ ((exists pfc_complement_division_exists_oldsteppreviousdiagonalterm pfc_left_division_exists_oldsteppreviousdiagonalterm pfc_right_division_exists_oldsteppreviousdiagonalterm. (((pfc_index_division_exists_oldsteppreviousdiagonal)+pfc_complement_division_exists_oldsteppreviousdiagonalterm=(pfd_index_division_exists_old)) /\ ((((((exists pfa_gap_division_exists_oldsteppreviousdiagonaltermleftinside. pfa_gap_division_exists_oldsteppreviousdiagonaltermleftinside + S (pfc_index_division_exists_oldsteppreviousdiagonal) = (pfd_index_division_exists_old)) /\ ((((exists ff_h_pfp_division_exists_oldsteppreviousdiagonaltermleftentry. ff_h_pfp_division_exists_oldsteppreviousdiagonaltermleftentry + S (pfc_left_division_exists_oldsteppreviousdiagonalterm) = S ((S (pfc_index_division_exists_oldsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_exists_oldsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_exists_oldsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_exists_oldsteppreviousdiagonal)) * qc) + (pfc_left_division_exists_oldsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_exists_oldsteppreviousdiagonaltermleftoutside. pfc_gap_division_exists_oldsteppreviousdiagonaltermleftoutside+(pfd_index_division_exists_old)=(pfc_index_division_exists_oldsteppreviousdiagonal)) /\ (((pfc_left_division_exists_oldsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_exists_oldsteppreviousdiagonaltermrightinside. pfa_gap_division_exists_oldsteppreviousdiagonaltermrightinside + S (pfc_complement_division_exists_oldsteppreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_division_exists_oldsteppreviousdiagonaltermrightentry. ff_h_pfp_division_exists_oldsteppreviousdiagonaltermrightentry + S (pfc_right_division_exists_oldsteppreviousdiagonalterm) = S ((S (pfc_complement_division_exists_oldsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_exists_oldsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_exists_oldsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_exists_oldsteppreviousdiagonalterm)) * bc) + (pfc_right_division_exists_oldsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_exists_oldsteppreviousdiagonaltermrightoutside. pfc_gap_division_exists_oldsteppreviousdiagonaltermrightoutside+(M)=(pfc_complement_division_exists_oldsteppreviousdiagonalterm)) /\ (((pfc_right_division_exists_oldsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_exists_oldsteppreviousdiagonal)=pfc_left_division_exists_oldsteppreviousdiagonalterm*pfc_right_division_exists_oldsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_exists_oldstepprevioussum fs_v_pfc_division_exists_oldstepprevioussum. ((((exists fs_h_pfc_division_exists_oldstepprevioussum_body_start. fs_h_pfc_division_exists_oldstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_exists_oldstepprevioussum)) /\ exists fs_q_pfc_division_exists_oldstepprevioussum_body_start. fs_u_pfc_division_exists_oldstepprevioussum = fs_q_pfc_division_exists_oldstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_exists_oldstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_exists_oldstepprevioussum_body_terminal. fs_h_pfc_division_exists_oldstepprevioussum_body_terminal + S (pfc_natural_sum_division_exists_oldstepprevious) = S ((S (S (pfd_index_division_exists_old))) * fs_v_pfc_division_exists_oldstepprevioussum)) /\ exists fs_q_pfc_division_exists_oldstepprevioussum_body_terminal. fs_u_pfc_division_exists_oldstepprevioussum = fs_q_pfc_division_exists_oldstepprevioussum_body_terminal * S ((S (S (pfd_index_division_exists_old))) * fs_v_pfc_division_exists_oldstepprevioussum) + (pfc_natural_sum_division_exists_oldstepprevious))) /\ forall fs_i_pfc_division_exists_oldstepprevioussum_body_steps. (exists fs_lt_pfc_division_exists_oldstepprevioussum_body_steps_bound. fs_lt_pfc_division_exists_oldstepprevioussum_body_steps_bound + S fs_i_pfc_division_exists_oldstepprevioussum_body_steps = S (pfd_index_division_exists_old)) -> exists fs_a_pfc_division_exists_oldstepprevioussum_body_steps fs_r_pfc_division_exists_oldstepprevioussum_body_steps fs_s_pfc_division_exists_oldstepprevioussum_body_steps. ((((exists fs_h_pfc_division_exists_oldstepprevioussum_body_steps_summand. fs_h_pfc_division_exists_oldstepprevioussum_body_steps_summand + S (fs_a_pfc_division_exists_oldstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_exists_oldstepprevioussum_body_steps)) * pfc_terms_scale_division_exists_oldstepprevious)) /\ exists fs_q_pfc_division_exists_oldstepprevioussum_body_steps_summand. pfc_terms_code_division_exists_oldstepprevious = fs_q_pfc_division_exists_oldstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_exists_oldstepprevioussum_body_steps)) * pfc_terms_scale_division_exists_oldstepprevious) + (fs_a_pfc_division_exists_oldstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_exists_oldstepprevioussum_body_steps_partial. fs_h_pfc_division_exists_oldstepprevioussum_body_steps_partial + S (fs_r_pfc_division_exists_oldstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_exists_oldstepprevioussum_body_steps)) * fs_v_pfc_division_exists_oldstepprevioussum)) /\ exists fs_q_pfc_division_exists_oldstepprevioussum_body_steps_partial. fs_u_pfc_division_exists_oldstepprevioussum = fs_q_pfc_division_exists_oldstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_exists_oldstepprevioussum_body_steps)) * fs_v_pfc_division_exists_oldstepprevioussum) + (fs_r_pfc_division_exists_oldstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_exists_oldstepprevioussum_body_steps_successor. fs_h_pfc_division_exists_oldstepprevioussum_body_steps_successor + S (fs_s_pfc_division_exists_oldstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_exists_oldstepprevioussum_body_steps)) * fs_v_pfc_division_exists_oldstepprevioussum)) /\ exists fs_q_pfc_division_exists_oldstepprevioussum_body_steps_successor. fs_u_pfc_division_exists_oldstepprevioussum = fs_q_pfc_division_exists_oldstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_exists_oldstepprevioussum_body_steps)) * fs_v_pfc_division_exists_oldstepprevioussum) + (fs_s_pfc_division_exists_oldstepprevioussum_body_steps))) /\ fs_s_pfc_division_exists_oldstepprevioussum_body_steps = fs_r_pfc_division_exists_oldstepprevioussum_body_steps + fs_a_pfc_division_exists_oldstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_exists_oldsteppreviousresiduebound. pfa_gap_division_exists_oldsteppreviousresiduebound + S (pfd_previous_division_exists_oldstep) = (p)) /\ ((exists pfa_offset_left_division_exists_oldsteppreviousresiduecongruence pfa_offset_right_division_exists_oldsteppreviousresiduecongruence. (pfc_natural_sum_division_exists_oldstepprevious) + (p) * pfa_offset_left_division_exists_oldsteppreviousresiduecongruence = (pfd_previous_division_exists_oldstep) + (p) * pfa_offset_right_division_exists_oldsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_exists_oldstepsubtractleft. pfa_gap_division_exists_oldstepsubtractleft + S (pfd_previous_division_exists_oldstep) = (p)) /\ (((exists pfa_gap_division_exists_oldstepsubtractright. pfa_gap_division_exists_oldstepsubtractright + S (pfd_difference_division_exists_oldstep) = (p)) /\ ((((exists pfa_gap_division_exists_oldstepsubtractresultbound. pfa_gap_division_exists_oldstepsubtractresultbound + S (pfd_input_division_exists_oldstep) = (p)) /\ ((exists pfa_offset_left_division_exists_oldstepsubtractresultcongruence pfa_offset_right_division_exists_oldstepsubtractresultcongruence. ((pfd_previous_division_exists_oldstep) + (pfd_difference_division_exists_oldstep)) + (p) * pfa_offset_left_division_exists_oldstepsubtractresultcongruence = (pfd_input_division_exists_oldstep) + (p) * pfa_offset_right_division_exists_oldstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_exists_oldstepmultiplyleft. pfa_gap_division_exists_oldstepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_exists_oldstepmultiplyright. pfa_gap_division_exists_oldstepmultiplyright + S (pfd_difference_division_exists_oldstep) = (p)) /\ ((((exists pfa_gap_division_exists_oldstepmultiplyresultbound. pfa_gap_division_exists_oldstepmultiplyresultbound + S (pfd_value_division_exists_old) = (p)) /\ ((exists pfa_offset_left_division_exists_oldstepmultiplyresultcongruence pfa_offset_right_division_exists_oldstepmultiplyresultcongruence. ((k) * (pfd_difference_division_exists_oldstep)) + (p) * pfa_offset_left_division_exists_oldstepmultiplyresultcongruence = (pfd_value_division_exists_old) + (p) * pfa_offset_right_division_exists_oldstepmultiplyresultcongruence)))))))))))))))))))
  27. 0027apply IH
  28. 0028intro i
  29. 0029intro hi
  30. 0030specialize ha (i)
  31. 0031apply ha
  32. 0032specialize le_succ (S i)
  33. 0033specialize le_succ (N)
  34. 0034apply le_succ
  35. 0035exact hi
  36. 0036cases hold
  37. 0037cases hold_witness
  38. 0038have hinput : exists a. ((((exists ff_h_pfp_division_exists_input. ff_h_pfp_division_exists_input + S (a) = S ((S (N)) * ac)) /\ exists ff_q_pfp_division_exists_input. ab = ff_q_pfp_division_exists_input * S ((S (N)) * ac) + (a))) /\ ((exists pfa_gap_division_exists_input_bound. pfa_gap_division_exists_input_bound + S (a) = (p))))
  39. 0039specialize ha (N)
  40. 0040apply ha
  41. 0041specialize le_refl (S N)
  42. 0042apply le_refl
  43. 0043cases hinput
  44. 0044cases hinput_witness
  45. 0045have hc : exists c. (exists pfc_terms_code_division_exists_previous pfc_terms_scale_division_exists_previous pfc_natural_sum_division_exists_previous. ((forall pfc_index_division_exists_previousdiagonal. (exists pfa_gap_division_exists_previousdiagonalbound. pfa_gap_division_exists_previousdiagonalbound + S (pfc_index_division_exists_previousdiagonal) = (S (N))) -> exists pfc_value_division_exists_previousdiagonal. ((((exists ff_h_pfp_division_exists_previousdiagonalentry. ff_h_pfp_division_exists_previousdiagonalentry + S (pfc_value_division_exists_previousdiagonal) = S ((S (pfc_index_division_exists_previousdiagonal)) * pfc_terms_scale_division_exists_previous)) /\ exists ff_q_pfp_division_exists_previousdiagonalentry. pfc_terms_code_division_exists_previous = ff_q_pfp_division_exists_previousdiagonalentry * S ((S (pfc_index_division_exists_previousdiagonal)) * pfc_terms_scale_division_exists_previous) + (pfc_value_division_exists_previousdiagonal))) /\ ((exists pfc_complement_division_exists_previousdiagonalterm pfc_left_division_exists_previousdiagonalterm pfc_right_division_exists_previousdiagonalterm. (((pfc_index_division_exists_previousdiagonal)+pfc_complement_division_exists_previousdiagonalterm=(N)) /\ ((((((exists pfa_gap_division_exists_previousdiagonaltermleftinside. pfa_gap_division_exists_previousdiagonaltermleftinside + S (pfc_index_division_exists_previousdiagonal) = (N)) /\ ((((exists ff_h_pfp_division_exists_previousdiagonaltermleftentry. ff_h_pfp_division_exists_previousdiagonaltermleftentry + S (pfc_left_division_exists_previousdiagonalterm) = S ((S (pfc_index_division_exists_previousdiagonal)) * x1)) /\ exists ff_q_pfp_division_exists_previousdiagonaltermleftentry. x = ff_q_pfp_division_exists_previousdiagonaltermleftentry * S ((S (pfc_index_division_exists_previousdiagonal)) * x1) + (pfc_left_division_exists_previousdiagonalterm)))))) \/ (((exists pfc_gap_division_exists_previousdiagonaltermleftoutside. pfc_gap_division_exists_previousdiagonaltermleftoutside+(N)=(pfc_index_division_exists_previousdiagonal)) /\ (((pfc_left_division_exists_previousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_exists_previousdiagonaltermrightinside. pfa_gap_division_exists_previousdiagonaltermrightinside + S (pfc_complement_division_exists_previousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_division_exists_previousdiagonaltermrightentry. ff_h_pfp_division_exists_previousdiagonaltermrightentry + S (pfc_right_division_exists_previousdiagonalterm) = S ((S (pfc_complement_division_exists_previousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_exists_previousdiagonaltermrightentry. bb = ff_q_pfp_division_exists_previousdiagonaltermrightentry * S ((S (pfc_complement_division_exists_previousdiagonalterm)) * bc) + (pfc_right_division_exists_previousdiagonalterm)))))) \/ (((exists pfc_gap_division_exists_previousdiagonaltermrightoutside. pfc_gap_division_exists_previousdiagonaltermrightoutside+(M)=(pfc_complement_division_exists_previousdiagonalterm)) /\ (((pfc_right_division_exists_previousdiagonalterm)=0))))) /\ (((pfc_value_division_exists_previousdiagonal)=pfc_left_division_exists_previousdiagonalterm*pfc_right_division_exists_previousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_exists_previoussum fs_v_pfc_division_exists_previoussum. ((((exists fs_h_pfc_division_exists_previoussum_body_start. fs_h_pfc_division_exists_previoussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_exists_previoussum)) /\ exists fs_q_pfc_division_exists_previoussum_body_start. fs_u_pfc_division_exists_previoussum = fs_q_pfc_division_exists_previoussum_body_start * S ((S (0)) * fs_v_pfc_division_exists_previoussum) + (0))) /\ ((((exists fs_h_pfc_division_exists_previoussum_body_terminal. fs_h_pfc_division_exists_previoussum_body_terminal + S (pfc_natural_sum_division_exists_previous) = S ((S (S (N))) * fs_v_pfc_division_exists_previoussum)) /\ exists fs_q_pfc_division_exists_previoussum_body_terminal. fs_u_pfc_division_exists_previoussum = fs_q_pfc_division_exists_previoussum_body_terminal * S ((S (S (N))) * fs_v_pfc_division_exists_previoussum) + (pfc_natural_sum_division_exists_previous))) /\ forall fs_i_pfc_division_exists_previoussum_body_steps. (exists fs_lt_pfc_division_exists_previoussum_body_steps_bound. fs_lt_pfc_division_exists_previoussum_body_steps_bound + S fs_i_pfc_division_exists_previoussum_body_steps = S (N)) -> exists fs_a_pfc_division_exists_previoussum_body_steps fs_r_pfc_division_exists_previoussum_body_steps fs_s_pfc_division_exists_previoussum_body_steps. ((((exists fs_h_pfc_division_exists_previoussum_body_steps_summand. fs_h_pfc_division_exists_previoussum_body_steps_summand + S (fs_a_pfc_division_exists_previoussum_body_steps) = S ((S (fs_i_pfc_division_exists_previoussum_body_steps)) * pfc_terms_scale_division_exists_previous)) /\ exists fs_q_pfc_division_exists_previoussum_body_steps_summand. pfc_terms_code_division_exists_previous = fs_q_pfc_division_exists_previoussum_body_steps_summand * S ((S (fs_i_pfc_division_exists_previoussum_body_steps)) * pfc_terms_scale_division_exists_previous) + (fs_a_pfc_division_exists_previoussum_body_steps))) /\ ((((exists fs_h_pfc_division_exists_previoussum_body_steps_partial. fs_h_pfc_division_exists_previoussum_body_steps_partial + S (fs_r_pfc_division_exists_previoussum_body_steps) = S ((S (fs_i_pfc_division_exists_previoussum_body_steps)) * fs_v_pfc_division_exists_previoussum)) /\ exists fs_q_pfc_division_exists_previoussum_body_steps_partial. fs_u_pfc_division_exists_previoussum = fs_q_pfc_division_exists_previoussum_body_steps_partial * S ((S (fs_i_pfc_division_exists_previoussum_body_steps)) * fs_v_pfc_division_exists_previoussum) + (fs_r_pfc_division_exists_previoussum_body_steps))) /\ ((((exists fs_h_pfc_division_exists_previoussum_body_steps_successor. fs_h_pfc_division_exists_previoussum_body_steps_successor + S (fs_s_pfc_division_exists_previoussum_body_steps) = S ((S (S fs_i_pfc_division_exists_previoussum_body_steps)) * fs_v_pfc_division_exists_previoussum)) /\ exists fs_q_pfc_division_exists_previoussum_body_steps_successor. fs_u_pfc_division_exists_previoussum = fs_q_pfc_division_exists_previoussum_body_steps_successor * S ((S (S fs_i_pfc_division_exists_previoussum_body_steps)) * fs_v_pfc_division_exists_previoussum) + (fs_s_pfc_division_exists_previoussum_body_steps))) /\ fs_s_pfc_division_exists_previoussum_body_steps = fs_r_pfc_division_exists_previoussum_body_steps + fs_a_pfc_division_exists_previoussum_body_steps)))))) /\ ((((exists pfa_gap_division_exists_previousresiduebound. pfa_gap_division_exists_previousresiduebound + S (c) = (p)) /\ ((exists pfa_offset_left_division_exists_previousresiduecongruence pfa_offset_right_division_exists_previousresiduecongruence. (pfc_natural_sum_division_exists_previous) + (p) * pfa_offset_left_division_exists_previousresiduecongruence = (c) + (p) * pfa_offset_right_division_exists_previousresiduecongruence)))))))))
  46. 0046specialize prime_field_convolution_coefficient_exists (p)
  47. 0047specialize prime_field_convolution_coefficient_exists (x)
  48. 0048specialize prime_field_convolution_coefficient_exists (x1)
  49. 0049specialize prime_field_convolution_coefficient_exists (N)
  50. 0050specialize prime_field_convolution_coefficient_exists (bb)
  51. 0051specialize prime_field_convolution_coefficient_exists (bc)
  52. 0052specialize prime_field_convolution_coefficient_exists (M)
  53. 0053specialize prime_field_convolution_coefficient_exists (N)
  54. 0054apply prime_field_convolution_coefficient_exists
  55. 0055intro hz
  56. 0056specialize prime_nonzero (p)
  57. 0057apply prime_nonzero
  58. 0058exact hp
  59. 0059exact hz
  60. 0060cases hc
  61. 0061have hs : exists s. (((exists pfa_gap_division_exists_differenceleft. pfa_gap_division_exists_differenceleft + S (x3) = (p)) /\ (((exists pfa_gap_division_exists_differenceright. pfa_gap_division_exists_differenceright + S (s) = (p)) /\ ((((exists pfa_gap_division_exists_differenceresultbound. pfa_gap_division_exists_differenceresultbound + S (x2) = (p)) /\ ((exists pfa_offset_left_division_exists_differenceresultcongruence pfa_offset_right_division_exists_differenceresultcongruence. ((x3) + (s)) + (p) * pfa_offset_left_division_exists_differenceresultcongruence = (x2) + (p) * pfa_offset_right_division_exists_differenceresultcongruence)))))))))
  62. 0062specialize prime_field_subtract_exists (p)
  63. 0063specialize prime_field_subtract_exists (x2)
  64. 0064specialize prime_field_subtract_exists (x3)
  65. 0065apply prime_field_subtract_exists
  66. 0066exact hp
  67. 0067exact hinput_witness_right
  68. 0068specialize prime_field_convolution_coefficient_bounded (p)
  69. 0069specialize prime_field_convolution_coefficient_bounded (x)
  70. 0070specialize prime_field_convolution_coefficient_bounded (x1)
  71. 0071specialize prime_field_convolution_coefficient_bounded (N)
  72. 0072specialize prime_field_convolution_coefficient_bounded (bb)
  73. 0073specialize prime_field_convolution_coefficient_bounded (bc)
  74. 0074specialize prime_field_convolution_coefficient_bounded (M)
  75. 0075specialize prime_field_convolution_coefficient_bounded (N)
  76. 0076specialize prime_field_convolution_coefficient_bounded (x3)
  77. 0077apply prime_field_convolution_coefficient_bounded
  78. 0078exact hc_witness
  79. 0079cases hs
  80. 0080have hq : exists q. (((exists pfa_gap_division_exists_quotientleft. pfa_gap_division_exists_quotientleft + S (k) = (p)) /\ (((exists pfa_gap_division_exists_quotientright. pfa_gap_division_exists_quotientright + S (x4) = (p)) /\ ((((exists pfa_gap_division_exists_quotientresultbound. pfa_gap_division_exists_quotientresultbound + S (q) = (p)) /\ ((exists pfa_offset_left_division_exists_quotientresultcongruence pfa_offset_right_division_exists_quotientresultcongruence. ((k) * (x4)) + (p) * pfa_offset_left_division_exists_quotientresultcongruence = (q) + (p) * pfa_offset_right_division_exists_quotientresultcongruence)))))))))
  81. 0081specialize prime_field_multiply_exists (p)
  82. 0082specialize prime_field_multiply_exists (k)
  83. 0083specialize prime_field_multiply_exists (x4)
  84. 0084apply prime_field_multiply_exists
  85. 0085exact hp
  86. 0086exact hk
  87. 0087cases hs_witness
  88. 0088cases hs_witness_right
  89. 0089exact hs_witness_right_left
  90. 0090cases hq
  91. 0091have hnew : exists QB QC. ((((exists ff_h_pfp_division_exists_new_entry. ff_h_pfp_division_exists_new_entry + S (x5) = S ((S (N)) * QC)) /\ exists ff_q_pfp_division_exists_new_entry. QB = ff_q_pfp_division_exists_new_entry * S ((S (N)) * QC) + (x5))) /\ ((forall mdr_i_pfp_division_exists_preservation mdr_a_pfp_division_exists_preservation. (exists mdr_gap_pfp_division_exists_preservationb. mdr_gap_pfp_division_exists_preservationb + S (mdr_i_pfp_division_exists_preservation) = (N)) -> (((exists ff_h_mdr_pfp_division_exists_preservationo. ff_h_mdr_pfp_division_exists_preservationo + S (mdr_a_pfp_division_exists_preservation) = S ((S (mdr_i_pfp_division_exists_preservation)) * x1)) /\ exists ff_q_mdr_pfp_division_exists_preservationo. x = ff_q_mdr_pfp_division_exists_preservationo * S ((S (mdr_i_pfp_division_exists_preservation)) * x1) + (mdr_a_pfp_division_exists_preservation))) -> (((exists ff_h_mdr_pfp_division_exists_preservationn. ff_h_mdr_pfp_division_exists_preservationn + S (mdr_a_pfp_division_exists_preservation) = S ((S (mdr_i_pfp_division_exists_preservation)) * QC)) /\ exists ff_q_mdr_pfp_division_exists_preservationn. QB = ff_q_mdr_pfp_division_exists_preservationn * S ((S (mdr_i_pfp_division_exists_preservation)) * QC) + (mdr_a_pfp_division_exists_preservation))))))
  92. 0092specialize beta_prefix_extend (N)
  93. 0093specialize beta_prefix_extend (x)
  94. 0094specialize beta_prefix_extend (x1)
  95. 0095specialize beta_prefix_extend (x5)
  96. 0096apply beta_prefix_extend
  97. 0097cases hnew
  98. 0098cases hnew_witness
  99. 0099cases hnew_witness_witness
  100. 0100exists x6
  101. 0101exists x7
  102. 0102specialize prime_field_polynomial_quotient_prefix_append (p)
  103. 0103specialize prime_field_polynomial_quotient_prefix_append (k)
  104. 0104specialize prime_field_polynomial_quotient_prefix_append (ab)
  105. 0105specialize prime_field_polynomial_quotient_prefix_append (ac)
  106. 0106specialize prime_field_polynomial_quotient_prefix_append (bb)
  107. 0107specialize prime_field_polynomial_quotient_prefix_append (bc)
  108. 0108specialize prime_field_polynomial_quotient_prefix_append (M)
  109. 0109specialize prime_field_polynomial_quotient_prefix_append (x)
  110. 0110specialize prime_field_polynomial_quotient_prefix_append (x1)
  111. 0111specialize prime_field_polynomial_quotient_prefix_append (x6)
  112. 0112specialize prime_field_polynomial_quotient_prefix_append (x7)
  113. 0113specialize prime_field_polynomial_quotient_prefix_append (N)
  114. 0114specialize prime_field_polynomial_quotient_prefix_append (x5)
  115. 0115apply prime_field_polynomial_quotient_prefix_append
  116. 0116exact hold_witness_witness
  117. 0117exact hnew_witness_witness_right
  118. 0118exact hnew_witness_witness_left
  119. 0119exists x2
  120. 0120exists x3
  121. 0121exists x4
  122. 0122split
  123. 0123exact hinput_witness_left
  124. 0124split
  125. 0125exact hc_witness
  126. 0126split
  127. 0127exact hs_witness
  128. 0128exact hq_witness