GC0009

crt_merge_compatible_prefix_solution_exists

Every arbitrary finite list, including non-coprime and zero moduli, has a genuine simultaneous solution whenever each exact predecessor-LCM merge is gcd-compatible.

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

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 original first-admission records.

Historical partial components only: this chapter proves canonical solutions under successive-merge compatibility and in the pairwise-compatible dominating-last case. G011 is now closed in the separate Alpha-v27 generalized-crt branch for arbitrary pairwise-compatible finite lists, including noncoprime moduli. Full G011 proof · Alpha v27

Exact theorem in conservative defined notation

∀ r. ∀ s. ∀ b. ∀ c. ∀ l. CRTMergeCompatiblePrefix(r,s,b,c,l) → ∃ x. CRTPrefixSolution(r,s,b,c,l,x)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

CRTPrefixSolution(r,s,b,c,l,x) · 1CRTMergeCompatiblePrefix(r,s,b,c,l) · 1

Actual proof prerequisites

crt_prefix_solution_empty · checked external prerequisitecrt_merge_compatible_prefix_drop_lastcrt_prefix_lcm_exists_unique · checked external prerequisitebeta_at_exists · checked external prerequisitegcd_exists_relational · checked external prerequisitele_refl · checked external prerequisitegeneralized_binary_crt_merge_stepcrt_prefix_solution_transport_common_multiple · checked external prerequisitecrt_prefix_solution_successor_intro · checked external prerequisite
Original expanded first-order statement 
forall r s b c l. (forall gcomp_merge_index_fold_hypothesis gcomp_merge_solution_fold_hypothesis gcomp_merge_lcm_fold_hypothesis gcomp_merge_residue_fold_hypothesis gcomp_merge_modulus_fold_hypothesis gcomp_merge_gcd_fold_hypothesis. (exists ff_lt_gcrt_fold_hypothesis_bound. ff_lt_gcrt_fold_hypothesis_bound + S gcomp_merge_index_fold_hypothesis = l) -> (((forall gcrt_common_index_fold_hypothesis_lcm_own gcrt_common_modulus_fold_hypothesis_lcm_own. (exists ff_lt_gcrt_fold_hypothesis_lcm_own_bound. ff_lt_gcrt_fold_hypothesis_lcm_own_bound + S gcrt_common_index_fold_hypothesis_lcm_own = gcomp_merge_index_fold_hypothesis) -> (((exists ff_h_gcrt_fold_hypothesis_lcm_own_entry. ff_h_gcrt_fold_hypothesis_lcm_own_entry + S (gcrt_common_modulus_fold_hypothesis_lcm_own) = S ((S (gcrt_common_index_fold_hypothesis_lcm_own)) * c)) /\ exists ff_q_gcrt_fold_hypothesis_lcm_own_entry. b = ff_q_gcrt_fold_hypothesis_lcm_own_entry * S ((S (gcrt_common_index_fold_hypothesis_lcm_own)) * c) + (gcrt_common_modulus_fold_hypothesis_lcm_own))) -> exists gcrt_common_quotient_fold_hypothesis_lcm_own. gcomp_merge_lcm_fold_hypothesis = gcrt_common_modulus_fold_hypothesis_lcm_own * gcrt_common_quotient_fold_hypothesis_lcm_own) /\ forall gcrt_lcm_common_fold_hypothesis_lcm. (forall gcrt_common_index_fold_hypothesis_lcm_other gcrt_common_modulus_fold_hypothesis_lcm_other. (exists ff_lt_gcrt_fold_hypothesis_lcm_other_bound. ff_lt_gcrt_fold_hypothesis_lcm_other_bound + S gcrt_common_index_fold_hypothesis_lcm_other = gcomp_merge_index_fold_hypothesis) -> (((exists ff_h_gcrt_fold_hypothesis_lcm_other_entry. ff_h_gcrt_fold_hypothesis_lcm_other_entry + S (gcrt_common_modulus_fold_hypothesis_lcm_other) = S ((S (gcrt_common_index_fold_hypothesis_lcm_other)) * c)) /\ exists ff_q_gcrt_fold_hypothesis_lcm_other_entry. b = ff_q_gcrt_fold_hypothesis_lcm_other_entry * S ((S (gcrt_common_index_fold_hypothesis_lcm_other)) * c) + (gcrt_common_modulus_fold_hypothesis_lcm_other))) -> exists gcrt_common_quotient_fold_hypothesis_lcm_other. gcrt_lcm_common_fold_hypothesis_lcm = gcrt_common_modulus_fold_hypothesis_lcm_other * gcrt_common_quotient_fold_hypothesis_lcm_other) -> exists gcrt_lcm_quotient_fold_hypothesis_lcm. gcrt_lcm_common_fold_hypothesis_lcm = gcomp_merge_lcm_fold_hypothesis * gcrt_lcm_quotient_fold_hypothesis_lcm)) -> (forall gcrt_solution_index_fold_hypothesis_solution gcrt_solution_residue_fold_hypothesis_solution gcrt_solution_modulus_fold_hypothesis_solution. (exists ff_lt_gcrt_fold_hypothesis_solution_bound. ff_lt_gcrt_fold_hypothesis_solution_bound + S gcrt_solution_index_fold_hypothesis_solution = gcomp_merge_index_fold_hypothesis) -> (((exists ff_h_gcrt_fold_hypothesis_solution_residue. ff_h_gcrt_fold_hypothesis_solution_residue + S (gcrt_solution_residue_fold_hypothesis_solution) = S ((S (gcrt_solution_index_fold_hypothesis_solution)) * s)) /\ exists ff_q_gcrt_fold_hypothesis_solution_residue. r = ff_q_gcrt_fold_hypothesis_solution_residue * S ((S (gcrt_solution_index_fold_hypothesis_solution)) * s) + (gcrt_solution_residue_fold_hypothesis_solution))) -> (((exists ff_h_gcrt_fold_hypothesis_solution_modulus. ff_h_gcrt_fold_hypothesis_solution_modulus + S (gcrt_solution_modulus_fold_hypothesis_solution) = S ((S (gcrt_solution_index_fold_hypothesis_solution)) * c)) /\ exists ff_q_gcrt_fold_hypothesis_solution_modulus. b = ff_q_gcrt_fold_hypothesis_solution_modulus * S ((S (gcrt_solution_index_fold_hypothesis_solution)) * c) + (gcrt_solution_modulus_fold_hypothesis_solution))) -> (exists hgcrt_mod_left_gcrt_fold_hypothesis_solution_congruence hgcrt_mod_right_gcrt_fold_hypothesis_solution_congruence. gcomp_merge_solution_fold_hypothesis + gcrt_solution_modulus_fold_hypothesis_solution * hgcrt_mod_left_gcrt_fold_hypothesis_solution_congruence = gcrt_solution_residue_fold_hypothesis_solution + gcrt_solution_modulus_fold_hypothesis_solution * hgcrt_mod_right_gcrt_fold_hypothesis_solution_congruence)) -> (((exists ff_h_gcrt_fold_hypothesis_residue. ff_h_gcrt_fold_hypothesis_residue + S (gcomp_merge_residue_fold_hypothesis) = S ((S (gcomp_merge_index_fold_hypothesis)) * s)) /\ exists ff_q_gcrt_fold_hypothesis_residue. r = ff_q_gcrt_fold_hypothesis_residue * S ((S (gcomp_merge_index_fold_hypothesis)) * s) + (gcomp_merge_residue_fold_hypothesis))) -> (((exists ff_h_gcrt_fold_hypothesis_modulus. ff_h_gcrt_fold_hypothesis_modulus + S (gcomp_merge_modulus_fold_hypothesis) = S ((S (gcomp_merge_index_fold_hypothesis)) * c)) /\ exists ff_q_gcrt_fold_hypothesis_modulus. b = ff_q_gcrt_fold_hypothesis_modulus * S ((S (gcomp_merge_index_fold_hypothesis)) * c) + (gcomp_merge_modulus_fold_hypothesis))) -> ((((exists hag_left_factor_gcomp_fold_hypothesis_gcd. gcomp_merge_lcm_fold_hypothesis = gcomp_merge_gcd_fold_hypothesis * hag_left_factor_gcomp_fold_hypothesis_gcd) /\ (exists hag_right_factor_gcomp_fold_hypothesis_gcd. gcomp_merge_modulus_fold_hypothesis = gcomp_merge_gcd_fold_hypothesis * hag_right_factor_gcomp_fold_hypothesis_gcd)) /\ forall hag_divisor_gcomp_fold_hypothesis_gcd. (exists hag_common_left_gcomp_fold_hypothesis_gcd. gcomp_merge_lcm_fold_hypothesis = hag_divisor_gcomp_fold_hypothesis_gcd * hag_common_left_gcomp_fold_hypothesis_gcd) -> (exists hag_common_right_gcomp_fold_hypothesis_gcd. gcomp_merge_modulus_fold_hypothesis = hag_divisor_gcomp_fold_hypothesis_gcd * hag_common_right_gcomp_fold_hypothesis_gcd) -> exists hag_greatest_factor_gcomp_fold_hypothesis_gcd. gcomp_merge_gcd_fold_hypothesis = hag_divisor_gcomp_fold_hypothesis_gcd * hag_greatest_factor_gcomp_fold_hypothesis_gcd)) -> (exists hgcrt_mod_left_gcrt_fold_hypothesis_result hgcrt_mod_right_gcrt_fold_hypothesis_result. gcomp_merge_solution_fold_hypothesis + gcomp_merge_gcd_fold_hypothesis * hgcrt_mod_left_gcrt_fold_hypothesis_result = gcomp_merge_residue_fold_hypothesis + gcomp_merge_gcd_fold_hypothesis * hgcrt_mod_right_gcrt_fold_hypothesis_result)) -> exists x. (forall gcrt_solution_index_gcomp_fold_result gcrt_solution_residue_gcomp_fold_result gcrt_solution_modulus_gcomp_fold_result. (exists ff_lt_gcrt_gcomp_fold_result_bound. ff_lt_gcrt_gcomp_fold_result_bound + S gcrt_solution_index_gcomp_fold_result = l) -> (((exists ff_h_gcrt_gcomp_fold_result_residue. ff_h_gcrt_gcomp_fold_result_residue + S (gcrt_solution_residue_gcomp_fold_result) = S ((S (gcrt_solution_index_gcomp_fold_result)) * s)) /\ exists ff_q_gcrt_gcomp_fold_result_residue. r = ff_q_gcrt_gcomp_fold_result_residue * S ((S (gcrt_solution_index_gcomp_fold_result)) * s) + (gcrt_solution_residue_gcomp_fold_result))) -> (((exists ff_h_gcrt_gcomp_fold_result_modulus. ff_h_gcrt_gcomp_fold_result_modulus + S (gcrt_solution_modulus_gcomp_fold_result) = S ((S (gcrt_solution_index_gcomp_fold_result)) * c)) /\ exists ff_q_gcrt_gcomp_fold_result_modulus. b = ff_q_gcrt_gcomp_fold_result_modulus * S ((S (gcrt_solution_index_gcomp_fold_result)) * c) + (gcrt_solution_modulus_gcomp_fold_result))) -> (exists hgcrt_mod_left_gcrt_gcomp_fold_result_congruence hgcrt_mod_right_gcrt_gcomp_fold_result_congruence. x + gcrt_solution_modulus_gcomp_fold_result * hgcrt_mod_left_gcrt_gcomp_fold_result_congruence = gcrt_solution_residue_gcomp_fold_result + gcrt_solution_modulus_gcomp_fold_result * hgcrt_mod_right_gcrt_gcomp_fold_result_congruence))

Complete unchanged native tactic proof

All 106 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

106 script commands · 27 reading checkpoints · 9 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
crt merge compatible prefix drop lastgeneralized binary crt merge step

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

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

  1. L1
    intro r
  2. L2
    intro s
  3. L3
    intro b
  4. L4
    intro c
02Induction on lL5–6

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

  1. L5
    induction l
  2. L6
    intro hmerge
03Construct an explicit witnessL7–7

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

  1. L7
    exists 0
04Use earlier factsL8–14

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

  1. L8
    specialize crt_prefix_solution_empty r
  2. L9
    specialize crt_prefix_solution_empty s
  3. L10
    specialize crt_prefix_solution_empty b
  4. L11
    specialize crt_prefix_solution_empty c
  5. L12
    specialize crt_prefix_solution_empty 0
  6. L13
    specialize crt_prefix_solution_empty 0
  7. L14
    apply crt_prefix_solution_empty
05Calculate and transport equalitiesL15–15

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

  1. L15
    refl
06Fix variables and assumptionsL16–16

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

  1. L16
    intro hmerge
07Establish hrestrictedL17–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply crt merge compatible prefix drop last.

  1. L17
    have hrestricted : CRTMergeCompatiblePrefix(r,s,b,c,l)Definitions: CRTMergeCompatiblePrefixOriginal native command in the exact edition
  2. L18
    specialize crt_merge_compatible_prefix_drop_last r
  3. L19
    specialize crt_merge_compatible_prefix_drop_last s
  4. L20
    specialize crt_merge_compatible_prefix_drop_last b
  5. L21
    specialize crt_merge_compatible_prefix_drop_last c
  6. L22
    specialize crt_merge_compatible_prefix_drop_last l
  7. L23
    apply crt_merge_compatible_prefix_drop_last
  8. L24
    exact hmerge
08Establish hprefixL25–27

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

  1. L25
    have hprefix : ∃ x. CRTPrefixSolution(r,s,b,c,l,x)Definitions: CRTPrefixSolutionOriginal native command in the exact edition
  2. L26
    apply IH
  3. L27
    exact hrestricted
09Separate the logical casesL28–28

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

  1. L28
    cases hprefix
10Establish hlcmL29–33

Establish this local claim before using it. It is not an additional assumption.

  1. L29
    have hlcm : ∃ P. CRTPrefixLCM(b,c,l,P) ∧ (∀ x. CRTPrefixLCM(b,c,l,x) → x = P)Definitions: CRTPrefixLCMOriginal native command in the exact edition
  2. L30
    specialize crt_prefix_lcm_exists_unique b
  3. L31
    specialize crt_prefix_lcm_exists_unique c
  4. L32
    specialize crt_prefix_lcm_exists_unique l
  5. L33
    exact crt_prefix_lcm_exists_unique
11Separate the logical casesL34–35

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

  1. L34
    cases hlcm
  2. L35
    cases hlcm_witness
12Establish hresidueL36–40

Establish this local claim before using it. It is not an additional assumption.

  1. L36
    have hresidue : exists a. (((exists ff_h_gcrt_gcomp_fold_actual_residue. ff_h_gcrt_gcomp_fold_actual_residue + S (a) = S ((S (l)) * s)) /\ exists ff_q_gcrt_gcomp_fold_actual_residue. r = ff_q_gcrt_gcomp_fold_actual_residue * S ((S (l)) * s) + (a)))
  2. L37
    specialize beta_at_exists r
  3. L38
    specialize beta_at_exists s
  4. L39
    specialize beta_at_exists l
  5. L40
    exact beta_at_exists
13Separate the logical casesL41–41

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

  1. L41
    cases hresidue
14Establish hmodulusL42–46

Establish this local claim before using it. It is not an additional assumption.

  1. L42
    have hmodulus : exists n. (((exists ff_h_gcrt_gcomp_fold_actual_modulus. ff_h_gcrt_gcomp_fold_actual_modulus + S (n) = S ((S (l)) * c)) /\ exists ff_q_gcrt_gcomp_fold_actual_modulus. b = ff_q_gcrt_gcomp_fold_actual_modulus * S ((S (l)) * c) + (n)))
  2. L43
    specialize beta_at_exists b
  3. L44
    specialize beta_at_exists c
  4. L45
    specialize beta_at_exists l
  5. L46
    exact beta_at_exists
15Separate the logical casesL47–47

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

  1. L47
    cases hmodulus
16Establish hgcdL48–51

Establish this local claim before using it. It is not an additional assumption.

  1. L48
    have hgcd : ∃ g. IsGCD(g,x1,x3)Definitions: IsGCDOriginal native command in the exact edition
  2. L49
    specialize gcd_exists_relational x1
  3. L50
    specialize gcd_exists_relational x3
  4. L51
    exact gcd_exists_relational
17Separate the logical casesL52–52

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

  1. L52
    cases hgcd
18Establish hcompatibleL53–62

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

  1. L53
    have hcompatible : exists hgcrt_mod_left_gcrt_gcomp_fold_actual_compatible hgcrt_mod_right_gcrt_gcomp_fold_actual_compatible. x + x4 * hgcrt_mod_left_gcrt_gcomp_fold_actual_compatible = x2 + x4 * hgcrt_mod_right_gcrt_gcomp_fold_actual_compatible
  2. L54
    specialize hmerge l
  3. L55
    specialize hmerge x
  4. L56
    specialize hmerge x1
  5. L57
    specialize hmerge x2
  6. L58
    specialize hmerge x3
  7. L59
    specialize hmerge x4
  8. L60
    apply hmerge
  9. L61
    specialize le_refl (S l)
  10. L62
    exact le_refl
19Use earlier factsL63–67

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

  1. L63
    exact hlcm_witness_left
  2. L64
    exact hprefix_witness
  3. L65
    exact hresidue_witness
  4. L66
    exact hmodulus_witness
  5. L67
    exact hgcd_witness
20Establish hmergedL68–76

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply generalized binary crt merge step.

  1. L68
    have hmerged : exists z. (((exists hgcrt_mod_left_gcrt_gcomp_fold_merged_old hgcrt_mod_right_gcrt_gcomp_fold_merged_old. z + x1 * hgcrt_mod_left_gcrt_gcomp_fold_merged_old = x + x1 * hgcrt_mod_right_gcrt_gcomp_fold_merged_old) /\ (exists hgcrt_mod_left_gcrt_gcomp_fold_merged_new hgcrt_mod_right_gcrt_gcomp_fold_merged_new. z + x3 * hgcrt_mod_left_gcrt_gcomp_fold_merged_new = x2 + x3 * hgcrt_mod_right_gcrt_gcomp_fold_merged_new)))
  2. L69
    specialize generalized_binary_crt_merge_step x1
  3. L70
    specialize generalized_binary_crt_merge_step x3
  4. L71
    specialize generalized_binary_crt_merge_step x
  5. L72
    specialize generalized_binary_crt_merge_step x2
  6. L73
    specialize generalized_binary_crt_merge_step x4
  7. L74
    apply generalized_binary_crt_merge_step
  8. L75
    exact hgcd_witness
  9. L76
    exact hcompatible
21Separate the logical casesL77–78

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

  1. L77
    cases hmerged
  2. L78
    cases hmerged_witness
22Establish htransportedL79–88

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply crt prefix solution transport common multiple.

  1. L79
    have htransported : CRTPrefixSolution(r,s,b,c,l,x5)Definitions: CRTPrefixSolutionOriginal native command in the exact edition
  2. L80
    specialize crt_prefix_solution_transport_common_multiple r
  3. L81
    specialize crt_prefix_solution_transport_common_multiple s
  4. L82
    specialize crt_prefix_solution_transport_common_multiple b
  5. L83
    specialize crt_prefix_solution_transport_common_multiple c
  6. L84
    specialize crt_prefix_solution_transport_common_multiple l
  7. L85
    specialize crt_prefix_solution_transport_common_multiple x1
  8. L86
    specialize crt_prefix_solution_transport_common_multiple x
  9. L87
    specialize crt_prefix_solution_transport_common_multiple x5
  10. L88
    apply crt_prefix_solution_transport_common_multiple
23Separate the logical casesL89–89

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

  1. L89
    cases hlcm_witness_left
24Use earlier factsL90–92

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

  1. L90
    exact hlcm_witness_left_left
  2. L91
    exact hprefix_witness
  3. L92
    exact hmerged_witness_left
25Construct an explicit witnessL93–93

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

  1. L93
    exists x5
26Use earlier factsL94–103

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

  1. L94
    specialize crt_prefix_solution_successor_intro r
  2. L95
    specialize crt_prefix_solution_successor_intro s
  3. L96
    specialize crt_prefix_solution_successor_intro b
  4. L97
    specialize crt_prefix_solution_successor_intro c
  5. L98
    specialize crt_prefix_solution_successor_intro l
  6. L99
    specialize crt_prefix_solution_successor_intro x5
  7. L100
    specialize crt_prefix_solution_successor_intro x2
  8. L101
    specialize crt_prefix_solution_successor_intro x3
  9. L102
    apply crt_prefix_solution_successor_intro
  10. L103
    exact htransported
27Use earlier factsL104–106

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

  1. L104
    exact hresidue_witness
  2. L105
    exact hmodulus_witness
  3. L106
    exact hmerged_witness_right

Library-wide reading audit

Original defined command ledger · 106 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005induction l
  6. 0006intro hmerge
  7. 0007exists 0
  8. 0008specialize crt_prefix_solution_empty r
  9. 0009specialize crt_prefix_solution_empty s
  10. 0010specialize crt_prefix_solution_empty b
  11. 0011specialize crt_prefix_solution_empty c
  12. 0012specialize crt_prefix_solution_empty 0
  13. 0013specialize crt_prefix_solution_empty 0
  14. 0014apply crt_prefix_solution_empty
  15. 0015refl
  16. 0016intro hmerge
  17. 0017have hrestricted : forall gcomp_merge_index_fold_restricted gcomp_merge_solution_fold_restricted gcomp_merge_lcm_fold_restricted gcomp_merge_residue_fold_restricted gcomp_merge_modulus_fold_restricted gcomp_merge_gcd_fold_restricted. (exists ff_lt_gcrt_fold_restricted_bound. ff_lt_gcrt_fold_restricted_bound + S gcomp_merge_index_fold_restricted = l) -> (((forall gcrt_common_index_fold_restricted_lcm_own gcrt_common_modulus_fold_restricted_lcm_own. (exists ff_lt_gcrt_fold_restricted_lcm_own_bound. ff_lt_gcrt_fold_restricted_lcm_own_bound + S gcrt_common_index_fold_restricted_lcm_own = gcomp_merge_index_fold_restricted) -> (((exists ff_h_gcrt_fold_restricted_lcm_own_entry. ff_h_gcrt_fold_restricted_lcm_own_entry + S (gcrt_common_modulus_fold_restricted_lcm_own) = S ((S (gcrt_common_index_fold_restricted_lcm_own)) * c)) /\ exists ff_q_gcrt_fold_restricted_lcm_own_entry. b = ff_q_gcrt_fold_restricted_lcm_own_entry * S ((S (gcrt_common_index_fold_restricted_lcm_own)) * c) + (gcrt_common_modulus_fold_restricted_lcm_own))) -> exists gcrt_common_quotient_fold_restricted_lcm_own. gcomp_merge_lcm_fold_restricted = gcrt_common_modulus_fold_restricted_lcm_own * gcrt_common_quotient_fold_restricted_lcm_own) /\ forall gcrt_lcm_common_fold_restricted_lcm. (forall gcrt_common_index_fold_restricted_lcm_other gcrt_common_modulus_fold_restricted_lcm_other. (exists ff_lt_gcrt_fold_restricted_lcm_other_bound. ff_lt_gcrt_fold_restricted_lcm_other_bound + S gcrt_common_index_fold_restricted_lcm_other = gcomp_merge_index_fold_restricted) -> (((exists ff_h_gcrt_fold_restricted_lcm_other_entry. ff_h_gcrt_fold_restricted_lcm_other_entry + S (gcrt_common_modulus_fold_restricted_lcm_other) = S ((S (gcrt_common_index_fold_restricted_lcm_other)) * c)) /\ exists ff_q_gcrt_fold_restricted_lcm_other_entry. b = ff_q_gcrt_fold_restricted_lcm_other_entry * S ((S (gcrt_common_index_fold_restricted_lcm_other)) * c) + (gcrt_common_modulus_fold_restricted_lcm_other))) -> exists gcrt_common_quotient_fold_restricted_lcm_other. gcrt_lcm_common_fold_restricted_lcm = gcrt_common_modulus_fold_restricted_lcm_other * gcrt_common_quotient_fold_restricted_lcm_other) -> exists gcrt_lcm_quotient_fold_restricted_lcm. gcrt_lcm_common_fold_restricted_lcm = gcomp_merge_lcm_fold_restricted * gcrt_lcm_quotient_fold_restricted_lcm)) -> (forall gcrt_solution_index_fold_restricted_solution gcrt_solution_residue_fold_restricted_solution gcrt_solution_modulus_fold_restricted_solution. (exists ff_lt_gcrt_fold_restricted_solution_bound. ff_lt_gcrt_fold_restricted_solution_bound + S gcrt_solution_index_fold_restricted_solution = gcomp_merge_index_fold_restricted) -> (((exists ff_h_gcrt_fold_restricted_solution_residue. ff_h_gcrt_fold_restricted_solution_residue + S (gcrt_solution_residue_fold_restricted_solution) = S ((S (gcrt_solution_index_fold_restricted_solution)) * s)) /\ exists ff_q_gcrt_fold_restricted_solution_residue. r = ff_q_gcrt_fold_restricted_solution_residue * S ((S (gcrt_solution_index_fold_restricted_solution)) * s) + (gcrt_solution_residue_fold_restricted_solution))) -> (((exists ff_h_gcrt_fold_restricted_solution_modulus. ff_h_gcrt_fold_restricted_solution_modulus + S (gcrt_solution_modulus_fold_restricted_solution) = S ((S (gcrt_solution_index_fold_restricted_solution)) * c)) /\ exists ff_q_gcrt_fold_restricted_solution_modulus. b = ff_q_gcrt_fold_restricted_solution_modulus * S ((S (gcrt_solution_index_fold_restricted_solution)) * c) + (gcrt_solution_modulus_fold_restricted_solution))) -> (exists hgcrt_mod_left_gcrt_fold_restricted_solution_congruence hgcrt_mod_right_gcrt_fold_restricted_solution_congruence. gcomp_merge_solution_fold_restricted + gcrt_solution_modulus_fold_restricted_solution * hgcrt_mod_left_gcrt_fold_restricted_solution_congruence = gcrt_solution_residue_fold_restricted_solution + gcrt_solution_modulus_fold_restricted_solution * hgcrt_mod_right_gcrt_fold_restricted_solution_congruence)) -> (((exists ff_h_gcrt_fold_restricted_residue. ff_h_gcrt_fold_restricted_residue + S (gcomp_merge_residue_fold_restricted) = S ((S (gcomp_merge_index_fold_restricted)) * s)) /\ exists ff_q_gcrt_fold_restricted_residue. r = ff_q_gcrt_fold_restricted_residue * S ((S (gcomp_merge_index_fold_restricted)) * s) + (gcomp_merge_residue_fold_restricted))) -> (((exists ff_h_gcrt_fold_restricted_modulus. ff_h_gcrt_fold_restricted_modulus + S (gcomp_merge_modulus_fold_restricted) = S ((S (gcomp_merge_index_fold_restricted)) * c)) /\ exists ff_q_gcrt_fold_restricted_modulus. b = ff_q_gcrt_fold_restricted_modulus * S ((S (gcomp_merge_index_fold_restricted)) * c) + (gcomp_merge_modulus_fold_restricted))) -> ((((exists hag_left_factor_gcomp_fold_restricted_gcd. gcomp_merge_lcm_fold_restricted = gcomp_merge_gcd_fold_restricted * hag_left_factor_gcomp_fold_restricted_gcd) /\ (exists hag_right_factor_gcomp_fold_restricted_gcd. gcomp_merge_modulus_fold_restricted = gcomp_merge_gcd_fold_restricted * hag_right_factor_gcomp_fold_restricted_gcd)) /\ forall hag_divisor_gcomp_fold_restricted_gcd. (exists hag_common_left_gcomp_fold_restricted_gcd. gcomp_merge_lcm_fold_restricted = hag_divisor_gcomp_fold_restricted_gcd * hag_common_left_gcomp_fold_restricted_gcd) -> (exists hag_common_right_gcomp_fold_restricted_gcd. gcomp_merge_modulus_fold_restricted = hag_divisor_gcomp_fold_restricted_gcd * hag_common_right_gcomp_fold_restricted_gcd) -> exists hag_greatest_factor_gcomp_fold_restricted_gcd. gcomp_merge_gcd_fold_restricted = hag_divisor_gcomp_fold_restricted_gcd * hag_greatest_factor_gcomp_fold_restricted_gcd)) -> (exists hgcrt_mod_left_gcrt_fold_restricted_result hgcrt_mod_right_gcrt_fold_restricted_result. gcomp_merge_solution_fold_restricted + gcomp_merge_gcd_fold_restricted * hgcrt_mod_left_gcrt_fold_restricted_result = gcomp_merge_residue_fold_restricted + gcomp_merge_gcd_fold_restricted * hgcrt_mod_right_gcrt_fold_restricted_result)
  18. 0018specialize crt_merge_compatible_prefix_drop_last r
  19. 0019specialize crt_merge_compatible_prefix_drop_last s
  20. 0020specialize crt_merge_compatible_prefix_drop_last b
  21. 0021specialize crt_merge_compatible_prefix_drop_last c
  22. 0022specialize crt_merge_compatible_prefix_drop_last l
  23. 0023apply crt_merge_compatible_prefix_drop_last
  24. 0024exact hmerge
  25. 0025have hprefix : exists x. (forall gcrt_solution_index_gcomp_fold_old_solution gcrt_solution_residue_gcomp_fold_old_solution gcrt_solution_modulus_gcomp_fold_old_solution. (exists ff_lt_gcrt_gcomp_fold_old_solution_bound. ff_lt_gcrt_gcomp_fold_old_solution_bound + S gcrt_solution_index_gcomp_fold_old_solution = l) -> (((exists ff_h_gcrt_gcomp_fold_old_solution_residue. ff_h_gcrt_gcomp_fold_old_solution_residue + S (gcrt_solution_residue_gcomp_fold_old_solution) = S ((S (gcrt_solution_index_gcomp_fold_old_solution)) * s)) /\ exists ff_q_gcrt_gcomp_fold_old_solution_residue. r = ff_q_gcrt_gcomp_fold_old_solution_residue * S ((S (gcrt_solution_index_gcomp_fold_old_solution)) * s) + (gcrt_solution_residue_gcomp_fold_old_solution))) -> (((exists ff_h_gcrt_gcomp_fold_old_solution_modulus. ff_h_gcrt_gcomp_fold_old_solution_modulus + S (gcrt_solution_modulus_gcomp_fold_old_solution) = S ((S (gcrt_solution_index_gcomp_fold_old_solution)) * c)) /\ exists ff_q_gcrt_gcomp_fold_old_solution_modulus. b = ff_q_gcrt_gcomp_fold_old_solution_modulus * S ((S (gcrt_solution_index_gcomp_fold_old_solution)) * c) + (gcrt_solution_modulus_gcomp_fold_old_solution))) -> (exists hgcrt_mod_left_gcrt_gcomp_fold_old_solution_congruence hgcrt_mod_right_gcrt_gcomp_fold_old_solution_congruence. x + gcrt_solution_modulus_gcomp_fold_old_solution * hgcrt_mod_left_gcrt_gcomp_fold_old_solution_congruence = gcrt_solution_residue_gcomp_fold_old_solution + gcrt_solution_modulus_gcomp_fold_old_solution * hgcrt_mod_right_gcrt_gcomp_fold_old_solution_congruence))
  26. 0026apply IH
  27. 0027exact hrestricted
  28. 0028cases hprefix
  29. 0029have hlcm : exists P. ((((forall gcrt_common_index_gcomp_fold_old_lcm_own gcrt_common_modulus_gcomp_fold_old_lcm_own. (exists ff_lt_gcrt_gcomp_fold_old_lcm_own_bound. ff_lt_gcrt_gcomp_fold_old_lcm_own_bound + S gcrt_common_index_gcomp_fold_old_lcm_own = l) -> (((exists ff_h_gcrt_gcomp_fold_old_lcm_own_entry. ff_h_gcrt_gcomp_fold_old_lcm_own_entry + S (gcrt_common_modulus_gcomp_fold_old_lcm_own) = S ((S (gcrt_common_index_gcomp_fold_old_lcm_own)) * c)) /\ exists ff_q_gcrt_gcomp_fold_old_lcm_own_entry. b = ff_q_gcrt_gcomp_fold_old_lcm_own_entry * S ((S (gcrt_common_index_gcomp_fold_old_lcm_own)) * c) + (gcrt_common_modulus_gcomp_fold_old_lcm_own))) -> exists gcrt_common_quotient_gcomp_fold_old_lcm_own. P = gcrt_common_modulus_gcomp_fold_old_lcm_own * gcrt_common_quotient_gcomp_fold_old_lcm_own) /\ forall gcrt_lcm_common_gcomp_fold_old_lcm. (forall gcrt_common_index_gcomp_fold_old_lcm_other gcrt_common_modulus_gcomp_fold_old_lcm_other. (exists ff_lt_gcrt_gcomp_fold_old_lcm_other_bound. ff_lt_gcrt_gcomp_fold_old_lcm_other_bound + S gcrt_common_index_gcomp_fold_old_lcm_other = l) -> (((exists ff_h_gcrt_gcomp_fold_old_lcm_other_entry. ff_h_gcrt_gcomp_fold_old_lcm_other_entry + S (gcrt_common_modulus_gcomp_fold_old_lcm_other) = S ((S (gcrt_common_index_gcomp_fold_old_lcm_other)) * c)) /\ exists ff_q_gcrt_gcomp_fold_old_lcm_other_entry. b = ff_q_gcrt_gcomp_fold_old_lcm_other_entry * S ((S (gcrt_common_index_gcomp_fold_old_lcm_other)) * c) + (gcrt_common_modulus_gcomp_fold_old_lcm_other))) -> exists gcrt_common_quotient_gcomp_fold_old_lcm_other. gcrt_lcm_common_gcomp_fold_old_lcm = gcrt_common_modulus_gcomp_fold_old_lcm_other * gcrt_common_quotient_gcomp_fold_old_lcm_other) -> exists gcrt_lcm_quotient_gcomp_fold_old_lcm. gcrt_lcm_common_gcomp_fold_old_lcm = P * gcrt_lcm_quotient_gcomp_fold_old_lcm)) /\ forall z. (((forall gcrt_common_index_gcomp_fold_old_lcm_unique_own gcrt_common_modulus_gcomp_fold_old_lcm_unique_own. (exists ff_lt_gcrt_gcomp_fold_old_lcm_unique_own_bound. ff_lt_gcrt_gcomp_fold_old_lcm_unique_own_bound + S gcrt_common_index_gcomp_fold_old_lcm_unique_own = l) -> (((exists ff_h_gcrt_gcomp_fold_old_lcm_unique_own_entry. ff_h_gcrt_gcomp_fold_old_lcm_unique_own_entry + S (gcrt_common_modulus_gcomp_fold_old_lcm_unique_own) = S ((S (gcrt_common_index_gcomp_fold_old_lcm_unique_own)) * c)) /\ exists ff_q_gcrt_gcomp_fold_old_lcm_unique_own_entry. b = ff_q_gcrt_gcomp_fold_old_lcm_unique_own_entry * S ((S (gcrt_common_index_gcomp_fold_old_lcm_unique_own)) * c) + (gcrt_common_modulus_gcomp_fold_old_lcm_unique_own))) -> exists gcrt_common_quotient_gcomp_fold_old_lcm_unique_own. z = gcrt_common_modulus_gcomp_fold_old_lcm_unique_own * gcrt_common_quotient_gcomp_fold_old_lcm_unique_own) /\ forall gcrt_lcm_common_gcomp_fold_old_lcm_unique. (forall gcrt_common_index_gcomp_fold_old_lcm_unique_other gcrt_common_modulus_gcomp_fold_old_lcm_unique_other. (exists ff_lt_gcrt_gcomp_fold_old_lcm_unique_other_bound. ff_lt_gcrt_gcomp_fold_old_lcm_unique_other_bound + S gcrt_common_index_gcomp_fold_old_lcm_unique_other = l) -> (((exists ff_h_gcrt_gcomp_fold_old_lcm_unique_other_entry. ff_h_gcrt_gcomp_fold_old_lcm_unique_other_entry + S (gcrt_common_modulus_gcomp_fold_old_lcm_unique_other) = S ((S (gcrt_common_index_gcomp_fold_old_lcm_unique_other)) * c)) /\ exists ff_q_gcrt_gcomp_fold_old_lcm_unique_other_entry. b = ff_q_gcrt_gcomp_fold_old_lcm_unique_other_entry * S ((S (gcrt_common_index_gcomp_fold_old_lcm_unique_other)) * c) + (gcrt_common_modulus_gcomp_fold_old_lcm_unique_other))) -> exists gcrt_common_quotient_gcomp_fold_old_lcm_unique_other. gcrt_lcm_common_gcomp_fold_old_lcm_unique = gcrt_common_modulus_gcomp_fold_old_lcm_unique_other * gcrt_common_quotient_gcomp_fold_old_lcm_unique_other) -> exists gcrt_lcm_quotient_gcomp_fold_old_lcm_unique. gcrt_lcm_common_gcomp_fold_old_lcm_unique = z * gcrt_lcm_quotient_gcomp_fold_old_lcm_unique)) -> z = P)
  30. 0030specialize crt_prefix_lcm_exists_unique b
  31. 0031specialize crt_prefix_lcm_exists_unique c
  32. 0032specialize crt_prefix_lcm_exists_unique l
  33. 0033exact crt_prefix_lcm_exists_unique
  34. 0034cases hlcm
  35. 0035cases hlcm_witness
  36. 0036have hresidue : exists a. (((exists ff_h_gcrt_gcomp_fold_actual_residue. ff_h_gcrt_gcomp_fold_actual_residue + S (a) = S ((S (l)) * s)) /\ exists ff_q_gcrt_gcomp_fold_actual_residue. r = ff_q_gcrt_gcomp_fold_actual_residue * S ((S (l)) * s) + (a)))
  37. 0037specialize beta_at_exists r
  38. 0038specialize beta_at_exists s
  39. 0039specialize beta_at_exists l
  40. 0040exact beta_at_exists
  41. 0041cases hresidue
  42. 0042have hmodulus : exists n. (((exists ff_h_gcrt_gcomp_fold_actual_modulus. ff_h_gcrt_gcomp_fold_actual_modulus + S (n) = S ((S (l)) * c)) /\ exists ff_q_gcrt_gcomp_fold_actual_modulus. b = ff_q_gcrt_gcomp_fold_actual_modulus * S ((S (l)) * c) + (n)))
  43. 0043specialize beta_at_exists b
  44. 0044specialize beta_at_exists c
  45. 0045specialize beta_at_exists l
  46. 0046exact beta_at_exists
  47. 0047cases hmodulus
  48. 0048have hgcd : exists g. ((((exists hag_left_factor_gcomp_fold_actual_gcd. x1 = g * hag_left_factor_gcomp_fold_actual_gcd) /\ (exists hag_right_factor_gcomp_fold_actual_gcd. x3 = g * hag_right_factor_gcomp_fold_actual_gcd)) /\ forall hag_divisor_gcomp_fold_actual_gcd. (exists hag_common_left_gcomp_fold_actual_gcd. x1 = hag_divisor_gcomp_fold_actual_gcd * hag_common_left_gcomp_fold_actual_gcd) -> (exists hag_common_right_gcomp_fold_actual_gcd. x3 = hag_divisor_gcomp_fold_actual_gcd * hag_common_right_gcomp_fold_actual_gcd) -> exists hag_greatest_factor_gcomp_fold_actual_gcd. g = hag_divisor_gcomp_fold_actual_gcd * hag_greatest_factor_gcomp_fold_actual_gcd))
  49. 0049specialize gcd_exists_relational x1
  50. 0050specialize gcd_exists_relational x3
  51. 0051exact gcd_exists_relational
  52. 0052cases hgcd
  53. 0053have hcompatible : exists hgcrt_mod_left_gcrt_gcomp_fold_actual_compatible hgcrt_mod_right_gcrt_gcomp_fold_actual_compatible. x + x4 * hgcrt_mod_left_gcrt_gcomp_fold_actual_compatible = x2 + x4 * hgcrt_mod_right_gcrt_gcomp_fold_actual_compatible
  54. 0054specialize hmerge l
  55. 0055specialize hmerge x
  56. 0056specialize hmerge x1
  57. 0057specialize hmerge x2
  58. 0058specialize hmerge x3
  59. 0059specialize hmerge x4
  60. 0060apply hmerge
  61. 0061specialize le_refl (S l)
  62. 0062exact le_refl
  63. 0063exact hlcm_witness_left
  64. 0064exact hprefix_witness
  65. 0065exact hresidue_witness
  66. 0066exact hmodulus_witness
  67. 0067exact hgcd_witness
  68. 0068have hmerged : exists z. (((exists hgcrt_mod_left_gcrt_gcomp_fold_merged_old hgcrt_mod_right_gcrt_gcomp_fold_merged_old. z + x1 * hgcrt_mod_left_gcrt_gcomp_fold_merged_old = x + x1 * hgcrt_mod_right_gcrt_gcomp_fold_merged_old) /\ (exists hgcrt_mod_left_gcrt_gcomp_fold_merged_new hgcrt_mod_right_gcrt_gcomp_fold_merged_new. z + x3 * hgcrt_mod_left_gcrt_gcomp_fold_merged_new = x2 + x3 * hgcrt_mod_right_gcrt_gcomp_fold_merged_new)))
  69. 0069specialize generalized_binary_crt_merge_step x1
  70. 0070specialize generalized_binary_crt_merge_step x3
  71. 0071specialize generalized_binary_crt_merge_step x
  72. 0072specialize generalized_binary_crt_merge_step x2
  73. 0073specialize generalized_binary_crt_merge_step x4
  74. 0074apply generalized_binary_crt_merge_step
  75. 0075exact hgcd_witness
  76. 0076exact hcompatible
  77. 0077cases hmerged
  78. 0078cases hmerged_witness
  79. 0079have htransported : forall gcrt_solution_index_gcomp_fold_transported gcrt_solution_residue_gcomp_fold_transported gcrt_solution_modulus_gcomp_fold_transported. (exists ff_lt_gcrt_gcomp_fold_transported_bound. ff_lt_gcrt_gcomp_fold_transported_bound + S gcrt_solution_index_gcomp_fold_transported = l) -> (((exists ff_h_gcrt_gcomp_fold_transported_residue. ff_h_gcrt_gcomp_fold_transported_residue + S (gcrt_solution_residue_gcomp_fold_transported) = S ((S (gcrt_solution_index_gcomp_fold_transported)) * s)) /\ exists ff_q_gcrt_gcomp_fold_transported_residue. r = ff_q_gcrt_gcomp_fold_transported_residue * S ((S (gcrt_solution_index_gcomp_fold_transported)) * s) + (gcrt_solution_residue_gcomp_fold_transported))) -> (((exists ff_h_gcrt_gcomp_fold_transported_modulus. ff_h_gcrt_gcomp_fold_transported_modulus + S (gcrt_solution_modulus_gcomp_fold_transported) = S ((S (gcrt_solution_index_gcomp_fold_transported)) * c)) /\ exists ff_q_gcrt_gcomp_fold_transported_modulus. b = ff_q_gcrt_gcomp_fold_transported_modulus * S ((S (gcrt_solution_index_gcomp_fold_transported)) * c) + (gcrt_solution_modulus_gcomp_fold_transported))) -> (exists hgcrt_mod_left_gcrt_gcomp_fold_transported_congruence hgcrt_mod_right_gcrt_gcomp_fold_transported_congruence. x5 + gcrt_solution_modulus_gcomp_fold_transported * hgcrt_mod_left_gcrt_gcomp_fold_transported_congruence = gcrt_solution_residue_gcomp_fold_transported + gcrt_solution_modulus_gcomp_fold_transported * hgcrt_mod_right_gcrt_gcomp_fold_transported_congruence)
  80. 0080specialize crt_prefix_solution_transport_common_multiple r
  81. 0081specialize crt_prefix_solution_transport_common_multiple s
  82. 0082specialize crt_prefix_solution_transport_common_multiple b
  83. 0083specialize crt_prefix_solution_transport_common_multiple c
  84. 0084specialize crt_prefix_solution_transport_common_multiple l
  85. 0085specialize crt_prefix_solution_transport_common_multiple x1
  86. 0086specialize crt_prefix_solution_transport_common_multiple x
  87. 0087specialize crt_prefix_solution_transport_common_multiple x5
  88. 0088apply crt_prefix_solution_transport_common_multiple
  89. 0089cases hlcm_witness_left
  90. 0090exact hlcm_witness_left_left
  91. 0091exact hprefix_witness
  92. 0092exact hmerged_witness_left
  93. 0093exists x5
  94. 0094specialize crt_prefix_solution_successor_intro r
  95. 0095specialize crt_prefix_solution_successor_intro s
  96. 0096specialize crt_prefix_solution_successor_intro b
  97. 0097specialize crt_prefix_solution_successor_intro c
  98. 0098specialize crt_prefix_solution_successor_intro l
  99. 0099specialize crt_prefix_solution_successor_intro x5
  100. 0100specialize crt_prefix_solution_successor_intro x2
  101. 0101specialize crt_prefix_solution_successor_intro x3
  102. 0102apply crt_prefix_solution_successor_intro
  103. 0103exact htransported
  104. 0104exact hresidue_witness
  105. 0105exact hmodulus_witness
  106. 0106exact hmerged_witness_right