JT0027

jordan_tuple_scan_exists

Construct the duplicate-free finite scan by HA induction and three genuine finite decisions.

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

95 new Alpha admissions come from 96 source lemmas: tuple equality reflexivity reuses an already-admitted theorem and is not counted twice. All counts use actual finite beta-coded enumerations. G008 multiplicativity is proved; the general prime-power count and distinct-prime product formula are further goals. General prime-power fields (G091) remain open. Stable is unchanged.

Exact theorem in conservative defined notation

∀ k. ∀ n. ∀ c. ¬n = 0 → ∀ x. ∃ y. ∃ z. ∃ m. ∃ i. ∃ j. JordanTupleScan(k,n,c,x,y,z,m,i,j)

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 2JordanPrimitiveTuple(n,b,c,k) · 2JordanTupleListed(b,c,k,B,C,D,E,j) · 2JordanTupleScan(k,n,c,limit,B,C,D,E,j) · 2

Actual proof prerequisites

jordan_tuple_scan_emptymatrix_rank_bounded_prefix_decidable · checked external prerequisitejordan_primitive_tuple_decidablejordan_tuple_listed_decidablejordan_tuple_scan_skipjordan_tuple_scan_append
Original expanded first-order statement 
forall k n c. ~(n=0) -> forall t. exists B C D E j. ((forall jt_i_scanexists. (exists jt_gap_scanexistssoundindex. jt_gap_scanexistssoundindex+S (jt_i_scanexists)=(j)) -> exists jt_b_scanexists jt_e_scanexists. ((((((exists fs_h_jt_scanexistssoundcode. fs_h_jt_scanexistssoundcode + S (jt_b_scanexists) = S ((S (jt_i_scanexists)) * C)) /\ exists fs_q_jt_scanexistssoundcode. B = fs_q_jt_scanexistssoundcode * S ((S (jt_i_scanexists)) * C) + (jt_b_scanexists))) /\ (((exists fs_h_jt_scanexistssoundscale. fs_h_jt_scanexistssoundscale + S (jt_e_scanexists) = S ((S (jt_i_scanexists)) * E)) /\ exists fs_q_jt_scanexistssoundscale. D = fs_q_jt_scanexistssoundscale * S ((S (jt_i_scanexists)) * E) + (jt_e_scanexists))))) /\ (((forall jt_index_scanexistsbound. (exists jt_gap_scanexistsboundindex. jt_gap_scanexistsboundindex+S (jt_index_scanexistsbound)=(k)) -> exists jt_value_scanexistsbound. ((((exists fs_h_jt_scanexistsboundat. fs_h_jt_scanexistsboundat + S (jt_value_scanexistsbound) = S ((S (jt_index_scanexistsbound)) * jt_e_scanexists)) /\ exists fs_q_jt_scanexistsboundat. jt_b_scanexists = fs_q_jt_scanexistsboundat * S ((S (jt_index_scanexistsbound)) * jt_e_scanexists) + (jt_value_scanexistsbound))) /\ (exists jt_gap_scanexistsboundvalue. jt_gap_scanexistsboundvalue+S (jt_value_scanexistsbound)=(n)))) /\ (forall jt_divisor_scanexistsprimitive. (exists jt_factor_scanexistsprimitivemodulus. (n)=(jt_divisor_scanexistsprimitive)*jt_factor_scanexistsprimitivemodulus) -> (forall jt_index_scanexistsprimitivecoordinates jt_value_scanexistsprimitivecoordinates. (exists jt_gap_scanexistsprimitivecoordinatesindex. jt_gap_scanexistsprimitivecoordinatesindex+S (jt_index_scanexistsprimitivecoordinates)=(k)) -> (((exists fs_h_jt_scanexistsprimitivecoordinatesat. fs_h_jt_scanexistsprimitivecoordinatesat + S (jt_value_scanexistsprimitivecoordinates) = S ((S (jt_index_scanexistsprimitivecoordinates)) * jt_e_scanexists)) /\ exists fs_q_jt_scanexistsprimitivecoordinatesat. jt_b_scanexists = fs_q_jt_scanexistsprimitivecoordinatesat * S ((S (jt_index_scanexistsprimitivecoordinates)) * jt_e_scanexists) + (jt_value_scanexistsprimitivecoordinates))) -> (exists jt_factor_scanexistsprimitivecoordinatesdivides. (jt_value_scanexistsprimitivecoordinates)=(jt_divisor_scanexistsprimitive)*jt_factor_scanexistsprimitivecoordinatesdivides)) -> jt_divisor_scanexistsprimitive=1))))) /\ (((forall jt_i_scanexists jt_h_scanexists jt_b_scanexists jt_e_scanexists jt_d_scanexists jt_f_scanexists. (exists jt_gap_scanexistsfirstindex. jt_gap_scanexistsfirstindex+S (jt_i_scanexists)=(j)) -> (exists jt_gap_scanexistssecondindex. jt_gap_scanexistssecondindex+S (jt_h_scanexists)=(j)) -> (((((exists fs_h_jt_scanexistsfirstcode. fs_h_jt_scanexistsfirstcode + S (jt_b_scanexists) = S ((S (jt_i_scanexists)) * C)) /\ exists fs_q_jt_scanexistsfirstcode. B = fs_q_jt_scanexistsfirstcode * S ((S (jt_i_scanexists)) * C) + (jt_b_scanexists))) /\ (((exists fs_h_jt_scanexistsfirstscale. fs_h_jt_scanexistsfirstscale + S (jt_e_scanexists) = S ((S (jt_i_scanexists)) * E)) /\ exists fs_q_jt_scanexistsfirstscale. D = fs_q_jt_scanexistsfirstscale * S ((S (jt_i_scanexists)) * E) + (jt_e_scanexists))))) -> (((((exists fs_h_jt_scanexistssecondcode. fs_h_jt_scanexistssecondcode + S (jt_d_scanexists) = S ((S (jt_h_scanexists)) * C)) /\ exists fs_q_jt_scanexistssecondcode. B = fs_q_jt_scanexistssecondcode * S ((S (jt_h_scanexists)) * C) + (jt_d_scanexists))) /\ (((exists fs_h_jt_scanexistssecondscale. fs_h_jt_scanexistssecondscale + S (jt_f_scanexists) = S ((S (jt_h_scanexists)) * E)) /\ exists fs_q_jt_scanexistssecondscale. D = fs_q_jt_scanexistssecondscale * S ((S (jt_h_scanexists)) * E) + (jt_f_scanexists))))) -> (forall jt_index_scanexistssame jt_left_scanexistssame jt_right_scanexistssame. (exists jt_gap_scanexistssameindex. jt_gap_scanexistssameindex+S (jt_index_scanexistssame)=(k)) -> (((exists fs_h_jt_scanexistssameleft. fs_h_jt_scanexistssameleft + S (jt_left_scanexistssame) = S ((S (jt_index_scanexistssame)) * jt_e_scanexists)) /\ exists fs_q_jt_scanexistssameleft. jt_b_scanexists = fs_q_jt_scanexistssameleft * S ((S (jt_index_scanexistssame)) * jt_e_scanexists) + (jt_left_scanexistssame))) -> (((exists fs_h_jt_scanexistssameright. fs_h_jt_scanexistssameright + S (jt_right_scanexistssame) = S ((S (jt_index_scanexistssame)) * jt_f_scanexists)) /\ exists fs_q_jt_scanexistssameright. jt_d_scanexists = fs_q_jt_scanexistssameright * S ((S (jt_index_scanexistssame)) * jt_f_scanexists) + (jt_right_scanexistssame))) -> jt_left_scanexistssame=jt_right_scanexistssame) -> jt_i_scanexists=jt_h_scanexists) /\ (forall jt_z_scanexists. (exists jt_gap_scanexistscodeindex. jt_gap_scanexistscodeindex+S (jt_z_scanexists)=(t)) -> (forall jt_index_scanexistsinputbound. (exists jt_gap_scanexistsinputboundindex. jt_gap_scanexistsinputboundindex+S (jt_index_scanexistsinputbound)=(k)) -> exists jt_value_scanexistsinputbound. ((((exists fs_h_jt_scanexistsinputboundat. fs_h_jt_scanexistsinputboundat + S (jt_value_scanexistsinputbound) = S ((S (jt_index_scanexistsinputbound)) * c)) /\ exists fs_q_jt_scanexistsinputboundat. jt_z_scanexists = fs_q_jt_scanexistsinputboundat * S ((S (jt_index_scanexistsinputbound)) * c) + (jt_value_scanexistsinputbound))) /\ (exists jt_gap_scanexistsinputboundvalue. jt_gap_scanexistsinputboundvalue+S (jt_value_scanexistsinputbound)=(n)))) -> (forall jt_divisor_scanexistsinputprimitive. (exists jt_factor_scanexistsinputprimitivemodulus. (n)=(jt_divisor_scanexistsinputprimitive)*jt_factor_scanexistsinputprimitivemodulus) -> (forall jt_index_scanexistsinputprimitivecoordinates jt_value_scanexistsinputprimitivecoordinates. (exists jt_gap_scanexistsinputprimitivecoordinatesindex. jt_gap_scanexistsinputprimitivecoordinatesindex+S (jt_index_scanexistsinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_scanexistsinputprimitivecoordinatesat. fs_h_jt_scanexistsinputprimitivecoordinatesat + S (jt_value_scanexistsinputprimitivecoordinates) = S ((S (jt_index_scanexistsinputprimitivecoordinates)) * c)) /\ exists fs_q_jt_scanexistsinputprimitivecoordinatesat. jt_z_scanexists = fs_q_jt_scanexistsinputprimitivecoordinatesat * S ((S (jt_index_scanexistsinputprimitivecoordinates)) * c) + (jt_value_scanexistsinputprimitivecoordinates))) -> (exists jt_factor_scanexistsinputprimitivecoordinatesdivides. (jt_value_scanexistsinputprimitivecoordinates)=(jt_divisor_scanexistsinputprimitive)*jt_factor_scanexistsinputprimitivecoordinatesdivides)) -> jt_divisor_scanexistsinputprimitive=1) -> (exists jt_index_scanexistslisted jt_code_scanexistslisted jt_scale_scanexistslisted. ((exists jt_gap_scanexistslistedindex. jt_gap_scanexistslistedindex+S (jt_index_scanexistslisted)=(j)) /\ (((((((exists fs_h_jt_scanexistslistedcode. fs_h_jt_scanexistslistedcode + S (jt_code_scanexistslisted) = S ((S (jt_index_scanexistslisted)) * C)) /\ exists fs_q_jt_scanexistslistedcode. B = fs_q_jt_scanexistslistedcode * S ((S (jt_index_scanexistslisted)) * C) + (jt_code_scanexistslisted))) /\ (((exists fs_h_jt_scanexistslistedscale. fs_h_jt_scanexistslistedscale + S (jt_scale_scanexistslisted) = S ((S (jt_index_scanexistslisted)) * E)) /\ exists fs_q_jt_scanexistslistedscale. D = fs_q_jt_scanexistslistedscale * S ((S (jt_index_scanexistslisted)) * E) + (jt_scale_scanexistslisted))))) /\ (forall jt_index_scanexistslistedequal jt_left_scanexistslistedequal jt_right_scanexistslistedequal. (exists jt_gap_scanexistslistedequalindex. jt_gap_scanexistslistedequalindex+S (jt_index_scanexistslistedequal)=(k)) -> (((exists fs_h_jt_scanexistslistedequalleft. fs_h_jt_scanexistslistedequalleft + S (jt_left_scanexistslistedequal) = S ((S (jt_index_scanexistslistedequal)) * c)) /\ exists fs_q_jt_scanexistslistedequalleft. jt_z_scanexists = fs_q_jt_scanexistslistedequalleft * S ((S (jt_index_scanexistslistedequal)) * c) + (jt_left_scanexistslistedequal))) -> (((exists fs_h_jt_scanexistslistedequalright. fs_h_jt_scanexistslistedequalright + S (jt_right_scanexistslistedequal) = S ((S (jt_index_scanexistslistedequal)) * jt_scale_scanexistslisted)) /\ exists fs_q_jt_scanexistslistedequalright. jt_code_scanexistslisted = fs_q_jt_scanexistslistedequalright * S ((S (jt_index_scanexistslistedequal)) * jt_scale_scanexistslisted) + (jt_right_scanexistslistedequal))) -> jt_left_scanexistslistedequal=jt_right_scanexistslistedequal)))))))))

Complete tactic proof in conservative notation

All 135 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

135 script commands · 33 reading checkpoints · 4 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 (5)
jordan tuple scan emptyjordan primitive tuple decidablejordan tuple listed decidablejordan tuple scan skipjordan tuple scan append
01Fix variables and assumptionsL1–4

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

  1. L1
    intro k
  2. L2
    intro n
  3. L3
    intro c
  4. L4
    intro hn
02Induction on tL5–5

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

  1. L5
    induction t
03Construct an explicit witnessL6–10

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

  1. L6
    exists 0
  2. L7
    exists 0
  3. L8
    exists 0
  4. L9
    exists 0
  5. L10
    exists 0
04Use earlier factsL11–18

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

  1. L11
    specialize jordan_tuple_scan_empty (k)
  2. L12
    specialize jordan_tuple_scan_empty (n)
  3. L13
    specialize jordan_tuple_scan_empty (c)
  4. L14
    specialize jordan_tuple_scan_empty (0)
  5. L15
    specialize jordan_tuple_scan_empty (0)
  6. L16
    specialize jordan_tuple_scan_empty (0)
  7. L17
    specialize jordan_tuple_scan_empty (0)
  8. L18
    apply jordan_tuple_scan_empty
05Separate the logical casesL19–23

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

  1. L19
    cases IH
  2. L20
    cases IH_witness
  3. L21
    cases IH_witness_witness
  4. L22
    cases IH_witness_witness_witness
  5. L23
    cases IH_witness_witness_witness_witness
06Establish hbL24–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix rank bounded prefix decidable.

  1. L24
    have hb : BetaPrefixInto(t,c,k,n) ∨ ¬BetaPrefixInto(t,c,k,n)Definitions: BetaPrefixInto(t,c,k,n)Original native command in the exact edition
  2. L25
    specialize matrix_rank_bounded_prefix_decidable (t)
  3. L26
    specialize matrix_rank_bounded_prefix_decidable (c)
  4. L27
    specialize matrix_rank_bounded_prefix_decidable (k)
  5. L28
    specialize matrix_rank_bounded_prefix_decidable (n)
  6. L29
    apply matrix_rank_bounded_prefix_decidable
07Separate the logical casesL30–30

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

  1. L30
    cases hb
08Establish hpL31–37

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply jordan primitive tuple decidable.

  1. L31
    have hp : JordanPrimitiveTuple(n,t,c,k) ∨ ¬JordanPrimitiveTuple(n,t,c,k)Definitions: JordanPrimitiveTuple(n,t,c,k)Original native command in the exact edition
  2. L32
    specialize jordan_primitive_tuple_decidable (n)
  3. L33
    specialize jordan_primitive_tuple_decidable (t)
  4. L34
    specialize jordan_primitive_tuple_decidable (c)
  5. L35
    specialize jordan_primitive_tuple_decidable (k)
  6. L36
    apply jordan_primitive_tuple_decidable
  7. L37
    exact hn
09Separate the logical casesL38–38

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

  1. L38
    cases hp
10Establish hlL39–48

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply jordan tuple listed decidable.

  1. L39
    have hl : JordanTupleListed(t,c,k,x,x1,x2,x3,x4) ∨ ¬JordanTupleListed(t,c,k,x,x1,x2,x3,x4)Definitions: JordanTupleListed(t,c,k,x,x1,x2,x3,x4)Original native command in the exact edition
  2. L40
    specialize jordan_tuple_listed_decidable (t)
  3. L41
    specialize jordan_tuple_listed_decidable (c)
  4. L42
    specialize jordan_tuple_listed_decidable (k)
  5. L43
    specialize jordan_tuple_listed_decidable (x)
  6. L44
    specialize jordan_tuple_listed_decidable (x1)
  7. L45
    specialize jordan_tuple_listed_decidable (x2)
  8. L46
    specialize jordan_tuple_listed_decidable (x3)
  9. L47
    specialize jordan_tuple_listed_decidable (x4)
  10. L48
    apply jordan_tuple_listed_decidable
11Separate the logical casesL49–49

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

  1. L49
    cases hl
12Construct an explicit witnessL50–54

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

  1. L50
    exists x
  2. L51
    exists x1
  3. L52
    exists x2
  4. L53
    exists x3
  5. L54
    exists x4
13Use earlier factsL55–64

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

  1. L55
    specialize jordan_tuple_scan_skip (k)
  2. L56
    specialize jordan_tuple_scan_skip (n)
  3. L57
    specialize jordan_tuple_scan_skip (c)
  4. L58
    specialize jordan_tuple_scan_skip (t)
  5. L59
    specialize jordan_tuple_scan_skip (x)
  6. L60
    specialize jordan_tuple_scan_skip (x1)
  7. L61
    specialize jordan_tuple_scan_skip (x2)
  8. L62
    specialize jordan_tuple_scan_skip (x3)
  9. L63
    specialize jordan_tuple_scan_skip (x4)
  10. L64
    apply jordan_tuple_scan_skip
14Use earlier factsL65–65

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

  1. L65
    exact IH_witness_witness_witness_witness_witness
15Fix variables and assumptionsL66–67

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

  1. L66
    intro hbound
  2. L67
    intro hprimitive
16Use earlier factsL68–68

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

  1. L68
    exact hl_left
17Establish hnewL69–78

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

  1. L69
    have hnew : ∃ U. ∃ V. ∃ W. ∃ X. JordanTupleScan(k,n,c,S t,U,V,W,X,S x4)Definitions: JordanTupleScan(k,n,c,S t,U,V,W,X,S x4)Original native command in the exact edition
  2. L70
    specialize jordan_tuple_scan_append (k)
  3. L71
    specialize jordan_tuple_scan_append (n)
  4. L72
    specialize jordan_tuple_scan_append (c)
  5. L73
    specialize jordan_tuple_scan_append (t)
  6. L74
    specialize jordan_tuple_scan_append (x)
  7. L75
    specialize jordan_tuple_scan_append (x1)
  8. L76
    specialize jordan_tuple_scan_append (x2)
  9. L77
    specialize jordan_tuple_scan_append (x3)
  10. L78
    specialize jordan_tuple_scan_append (x4)
18Use earlier factsL79–83

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

  1. L79
    apply jordan_tuple_scan_append
  2. L80
    exact IH_witness_witness_witness_witness_witness
  3. L81
    exact hb_left
  4. L82
    exact hp_left
  5. L83
    exact hl_right
19Separate the logical casesL84–87

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

  1. L84
    cases hnew
  2. L85
    cases hnew_witness
  3. L86
    cases hnew_witness_witness
  4. L87
    cases hnew_witness_witness_witness
20Construct an explicit witnessL88–92

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

  1. L88
    exists x5
  2. L89
    exists x6
  3. L90
    exists x7
  4. L91
    exists x8
  5. L92
    exists S x4
21Use earlier factsL93–93

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

  1. L93
    exact hnew_witness_witness_witness_witness
22Construct an explicit witnessL94–98

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

  1. L94
    exists x
  2. L95
    exists x1
  3. L96
    exists x2
  4. L97
    exists x3
  5. L98
    exists x4
23Use earlier factsL99–108

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

  1. L99
    specialize jordan_tuple_scan_skip (k)
  2. L100
    specialize jordan_tuple_scan_skip (n)
  3. L101
    specialize jordan_tuple_scan_skip (c)
  4. L102
    specialize jordan_tuple_scan_skip (t)
  5. L103
    specialize jordan_tuple_scan_skip (x)
  6. L104
    specialize jordan_tuple_scan_skip (x1)
  7. L105
    specialize jordan_tuple_scan_skip (x2)
  8. L106
    specialize jordan_tuple_scan_skip (x3)
  9. L107
    specialize jordan_tuple_scan_skip (x4)
  10. L108
    apply jordan_tuple_scan_skip
24Use earlier factsL109–109

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

  1. L109
    exact IH_witness_witness_witness_witness_witness
25Fix variables and assumptionsL110–111

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

  1. L110
    intro hbound
  2. L111
    intro hprimitive
26Separate the logical casesL112–112

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

  1. L112
    exfalso
27Use earlier factsL113–114

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

  1. L113
    apply hp_right
  2. L114
    exact hprimitive
28Construct an explicit witnessL115–119

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

  1. L115
    exists x
  2. L116
    exists x1
  3. L117
    exists x2
  4. L118
    exists x3
  5. L119
    exists x4
29Use earlier factsL120–129

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

  1. L120
    specialize jordan_tuple_scan_skip (k)
  2. L121
    specialize jordan_tuple_scan_skip (n)
  3. L122
    specialize jordan_tuple_scan_skip (c)
  4. L123
    specialize jordan_tuple_scan_skip (t)
  5. L124
    specialize jordan_tuple_scan_skip (x)
  6. L125
    specialize jordan_tuple_scan_skip (x1)
  7. L126
    specialize jordan_tuple_scan_skip (x2)
  8. L127
    specialize jordan_tuple_scan_skip (x3)
  9. L128
    specialize jordan_tuple_scan_skip (x4)
  10. L129
    apply jordan_tuple_scan_skip
30Use earlier factsL130–130

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

  1. L130
    exact IH_witness_witness_witness_witness_witness
31Fix variables and assumptionsL131–132

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

  1. L131
    intro hbound
  2. L132
    intro hprimitive
32Separate the logical casesL133–133

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

  1. L133
    exfalso
33Use earlier factsL134–135

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

  1. L134
    apply hb_right
  2. L135
    exact hbound

Library-wide reading audit

Original defined command ledger · 135 lines
  1. 0001intro k
  2. 0002intro n
  3. 0003intro c
  4. 0004intro hn
  5. 0005induction t
  6. 0006exists 0
  7. 0007exists 0
  8. 0008exists 0
  9. 0009exists 0
  10. 0010exists 0
  11. 0011specialize jordan_tuple_scan_empty (k)
  12. 0012specialize jordan_tuple_scan_empty (n)
  13. 0013specialize jordan_tuple_scan_empty (c)
  14. 0014specialize jordan_tuple_scan_empty (0)
  15. 0015specialize jordan_tuple_scan_empty (0)
  16. 0016specialize jordan_tuple_scan_empty (0)
  17. 0017specialize jordan_tuple_scan_empty (0)
  18. 0018apply jordan_tuple_scan_empty
  19. 0019cases IH
  20. 0020cases IH_witness
  21. 0021cases IH_witness_witness
  22. 0022cases IH_witness_witness_witness
  23. 0023cases IH_witness_witness_witness_witness
  24. 0024have hb : BetaPrefixInto(t,c,k,n) ∨ ¬BetaPrefixInto(t,c,k,n)
  25. 0025specialize matrix_rank_bounded_prefix_decidable (t)
  26. 0026specialize matrix_rank_bounded_prefix_decidable (c)
  27. 0027specialize matrix_rank_bounded_prefix_decidable (k)
  28. 0028specialize matrix_rank_bounded_prefix_decidable (n)
  29. 0029apply matrix_rank_bounded_prefix_decidable
  30. 0030cases hb
  31. 0031have hp : JordanPrimitiveTuple(n,t,c,k) ∨ ¬JordanPrimitiveTuple(n,t,c,k)
  32. 0032specialize jordan_primitive_tuple_decidable (n)
  33. 0033specialize jordan_primitive_tuple_decidable (t)
  34. 0034specialize jordan_primitive_tuple_decidable (c)
  35. 0035specialize jordan_primitive_tuple_decidable (k)
  36. 0036apply jordan_primitive_tuple_decidable
  37. 0037exact hn
  38. 0038cases hp
  39. 0039have hl : JordanTupleListed(t,c,k,x,x1,x2,x3,x4) ∨ ¬JordanTupleListed(t,c,k,x,x1,x2,x3,x4)
  40. 0040specialize jordan_tuple_listed_decidable (t)
  41. 0041specialize jordan_tuple_listed_decidable (c)
  42. 0042specialize jordan_tuple_listed_decidable (k)
  43. 0043specialize jordan_tuple_listed_decidable (x)
  44. 0044specialize jordan_tuple_listed_decidable (x1)
  45. 0045specialize jordan_tuple_listed_decidable (x2)
  46. 0046specialize jordan_tuple_listed_decidable (x3)
  47. 0047specialize jordan_tuple_listed_decidable (x4)
  48. 0048apply jordan_tuple_listed_decidable
  49. 0049cases hl
  50. 0050exists x
  51. 0051exists x1
  52. 0052exists x2
  53. 0053exists x3
  54. 0054exists x4
  55. 0055specialize jordan_tuple_scan_skip (k)
  56. 0056specialize jordan_tuple_scan_skip (n)
  57. 0057specialize jordan_tuple_scan_skip (c)
  58. 0058specialize jordan_tuple_scan_skip (t)
  59. 0059specialize jordan_tuple_scan_skip (x)
  60. 0060specialize jordan_tuple_scan_skip (x1)
  61. 0061specialize jordan_tuple_scan_skip (x2)
  62. 0062specialize jordan_tuple_scan_skip (x3)
  63. 0063specialize jordan_tuple_scan_skip (x4)
  64. 0064apply jordan_tuple_scan_skip
  65. 0065exact IH_witness_witness_witness_witness_witness
  66. 0066intro hbound
  67. 0067intro hprimitive
  68. 0068exact hl_left
  69. 0069have hnew : ∃ U. ∃ V. ∃ W. ∃ X. JordanTupleScan(k,n,c,S t,U,V,W,X,S x4)
  70. 0070specialize jordan_tuple_scan_append (k)
  71. 0071specialize jordan_tuple_scan_append (n)
  72. 0072specialize jordan_tuple_scan_append (c)
  73. 0073specialize jordan_tuple_scan_append (t)
  74. 0074specialize jordan_tuple_scan_append (x)
  75. 0075specialize jordan_tuple_scan_append (x1)
  76. 0076specialize jordan_tuple_scan_append (x2)
  77. 0077specialize jordan_tuple_scan_append (x3)
  78. 0078specialize jordan_tuple_scan_append (x4)
  79. 0079apply jordan_tuple_scan_append
  80. 0080exact IH_witness_witness_witness_witness_witness
  81. 0081exact hb_left
  82. 0082exact hp_left
  83. 0083exact hl_right
  84. 0084cases hnew
  85. 0085cases hnew_witness
  86. 0086cases hnew_witness_witness
  87. 0087cases hnew_witness_witness_witness
  88. 0088exists x5
  89. 0089exists x6
  90. 0090exists x7
  91. 0091exists x8
  92. 0092exists S x4
  93. 0093exact hnew_witness_witness_witness_witness
  94. 0094exists x
  95. 0095exists x1
  96. 0096exists x2
  97. 0097exists x3
  98. 0098exists x4
  99. 0099specialize jordan_tuple_scan_skip (k)
  100. 0100specialize jordan_tuple_scan_skip (n)
  101. 0101specialize jordan_tuple_scan_skip (c)
  102. 0102specialize jordan_tuple_scan_skip (t)
  103. 0103specialize jordan_tuple_scan_skip (x)
  104. 0104specialize jordan_tuple_scan_skip (x1)
  105. 0105specialize jordan_tuple_scan_skip (x2)
  106. 0106specialize jordan_tuple_scan_skip (x3)
  107. 0107specialize jordan_tuple_scan_skip (x4)
  108. 0108apply jordan_tuple_scan_skip
  109. 0109exact IH_witness_witness_witness_witness_witness
  110. 0110intro hbound
  111. 0111intro hprimitive
  112. 0112exfalso
  113. 0113apply hp_right
  114. 0114exact hprimitive
  115. 0115exists x
  116. 0116exists x1
  117. 0117exists x2
  118. 0118exists x3
  119. 0119exists x4
  120. 0120specialize jordan_tuple_scan_skip (k)
  121. 0121specialize jordan_tuple_scan_skip (n)
  122. 0122specialize jordan_tuple_scan_skip (c)
  123. 0123specialize jordan_tuple_scan_skip (t)
  124. 0124specialize jordan_tuple_scan_skip (x)
  125. 0125specialize jordan_tuple_scan_skip (x1)
  126. 0126specialize jordan_tuple_scan_skip (x2)
  127. 0127specialize jordan_tuple_scan_skip (x3)
  128. 0128specialize jordan_tuple_scan_skip (x4)
  129. 0129apply jordan_tuple_scan_skip
  130. 0130exact IH_witness_witness_witness_witness_witness
  131. 0131intro hbound
  132. 0132intro hprimitive
  133. 0133exfalso
  134. 0134apply hb_right
  135. 0135exact hbound