JT0027

jordan_tuple_scan_exists

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

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

Exact expanded first-order arithmetic 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)))))))))

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

JT001D jordan_tuple_scan_empty matrix_rank_bounded_prefix_decidable Alpha theorem; checked-use authorized JT0015 jordan_primitive_tuple_decidable JT001C jordan_tuple_listed_decidable JT0023 jordan_tuple_scan_skip JT0026 jordan_tuple_scan_append

Direct dependents

JT0029 jordan_totient_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

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.

Named ingredients (5)
jordan tuple scan emptyjordan primitive tuple decidablejordan tuple listed decidablejordan tuple scan skipjordan tuple scan 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–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
  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
  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
  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
  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 exact 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 : (forall jt_index_scantotalyes. (exists jt_gap_scantotalyesindex. jt_gap_scantotalyesindex+S (jt_index_scantotalyes)=(k)) -> exists jt_value_scantotalyes. ((((exists fs_h_jt_scantotalyesat. fs_h_jt_scantotalyesat + S (jt_value_scantotalyes) = S ((S (jt_index_scantotalyes)) * c)) /\ exists fs_q_jt_scantotalyesat. t = fs_q_jt_scantotalyesat * S ((S (jt_index_scantotalyes)) * c) + (jt_value_scantotalyes))) /\ (exists jt_gap_scantotalyesvalue. jt_gap_scantotalyesvalue+S (jt_value_scantotalyes)=(n)))) \/ ~(forall jt_index_scantotalno. (exists jt_gap_scantotalnoindex. jt_gap_scantotalnoindex+S (jt_index_scantotalno)=(k)) -> exists jt_value_scantotalno. ((((exists fs_h_jt_scantotalnoat. fs_h_jt_scantotalnoat + S (jt_value_scantotalno) = S ((S (jt_index_scantotalno)) * c)) /\ exists fs_q_jt_scantotalnoat. t = fs_q_jt_scantotalnoat * S ((S (jt_index_scantotalno)) * c) + (jt_value_scantotalno))) /\ (exists jt_gap_scantotalnovalue. jt_gap_scantotalnovalue+S (jt_value_scantotalno)=(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 : (forall jt_divisor_scanprimyes. (exists jt_factor_scanprimyesmodulus. (n)=(jt_divisor_scanprimyes)*jt_factor_scanprimyesmodulus) -> (forall jt_index_scanprimyescoordinates jt_value_scanprimyescoordinates. (exists jt_gap_scanprimyescoordinatesindex. jt_gap_scanprimyescoordinatesindex+S (jt_index_scanprimyescoordinates)=(k)) -> (((exists fs_h_jt_scanprimyescoordinatesat. fs_h_jt_scanprimyescoordinatesat + S (jt_value_scanprimyescoordinates) = S ((S (jt_index_scanprimyescoordinates)) * c)) /\ exists fs_q_jt_scanprimyescoordinatesat. t = fs_q_jt_scanprimyescoordinatesat * S ((S (jt_index_scanprimyescoordinates)) * c) + (jt_value_scanprimyescoordinates))) -> (exists jt_factor_scanprimyescoordinatesdivides. (jt_value_scanprimyescoordinates)=(jt_divisor_scanprimyes)*jt_factor_scanprimyescoordinatesdivides)) -> jt_divisor_scanprimyes=1) \/ ~(forall jt_divisor_scanprimno. (exists jt_factor_scanprimnomodulus. (n)=(jt_divisor_scanprimno)*jt_factor_scanprimnomodulus) -> (forall jt_index_scanprimnocoordinates jt_value_scanprimnocoordinates. (exists jt_gap_scanprimnocoordinatesindex. jt_gap_scanprimnocoordinatesindex+S (jt_index_scanprimnocoordinates)=(k)) -> (((exists fs_h_jt_scanprimnocoordinatesat. fs_h_jt_scanprimnocoordinatesat + S (jt_value_scanprimnocoordinates) = S ((S (jt_index_scanprimnocoordinates)) * c)) /\ exists fs_q_jt_scanprimnocoordinatesat. t = fs_q_jt_scanprimnocoordinatesat * S ((S (jt_index_scanprimnocoordinates)) * c) + (jt_value_scanprimnocoordinates))) -> (exists jt_factor_scanprimnocoordinatesdivides. (jt_value_scanprimnocoordinates)=(jt_divisor_scanprimno)*jt_factor_scanprimnocoordinatesdivides)) -> jt_divisor_scanprimno=1)
  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 : (exists jt_index_scanlistedyes jt_code_scanlistedyes jt_scale_scanlistedyes. ((exists jt_gap_scanlistedyesindex. jt_gap_scanlistedyesindex+S (jt_index_scanlistedyes)=(x4)) /\ (((((((exists fs_h_jt_scanlistedyescode. fs_h_jt_scanlistedyescode + S (jt_code_scanlistedyes) = S ((S (jt_index_scanlistedyes)) * x1)) /\ exists fs_q_jt_scanlistedyescode. x = fs_q_jt_scanlistedyescode * S ((S (jt_index_scanlistedyes)) * x1) + (jt_code_scanlistedyes))) /\ (((exists fs_h_jt_scanlistedyesscale. fs_h_jt_scanlistedyesscale + S (jt_scale_scanlistedyes) = S ((S (jt_index_scanlistedyes)) * x3)) /\ exists fs_q_jt_scanlistedyesscale. x2 = fs_q_jt_scanlistedyesscale * S ((S (jt_index_scanlistedyes)) * x3) + (jt_scale_scanlistedyes))))) /\ (forall jt_index_scanlistedyesequal jt_left_scanlistedyesequal jt_right_scanlistedyesequal. (exists jt_gap_scanlistedyesequalindex. jt_gap_scanlistedyesequalindex+S (jt_index_scanlistedyesequal)=(k)) -> (((exists fs_h_jt_scanlistedyesequalleft. fs_h_jt_scanlistedyesequalleft + S (jt_left_scanlistedyesequal) = S ((S (jt_index_scanlistedyesequal)) * c)) /\ exists fs_q_jt_scanlistedyesequalleft. t = fs_q_jt_scanlistedyesequalleft * S ((S (jt_index_scanlistedyesequal)) * c) + (jt_left_scanlistedyesequal))) -> (((exists fs_h_jt_scanlistedyesequalright. fs_h_jt_scanlistedyesequalright + S (jt_right_scanlistedyesequal) = S ((S (jt_index_scanlistedyesequal)) * jt_scale_scanlistedyes)) /\ exists fs_q_jt_scanlistedyesequalright. jt_code_scanlistedyes = fs_q_jt_scanlistedyesequalright * S ((S (jt_index_scanlistedyesequal)) * jt_scale_scanlistedyes) + (jt_right_scanlistedyesequal))) -> jt_left_scanlistedyesequal=jt_right_scanlistedyesequal))))) \/ ~(exists jt_index_scanlistedno jt_code_scanlistedno jt_scale_scanlistedno. ((exists jt_gap_scanlistednoindex. jt_gap_scanlistednoindex+S (jt_index_scanlistedno)=(x4)) /\ (((((((exists fs_h_jt_scanlistednocode. fs_h_jt_scanlistednocode + S (jt_code_scanlistedno) = S ((S (jt_index_scanlistedno)) * x1)) /\ exists fs_q_jt_scanlistednocode. x = fs_q_jt_scanlistednocode * S ((S (jt_index_scanlistedno)) * x1) + (jt_code_scanlistedno))) /\ (((exists fs_h_jt_scanlistednoscale. fs_h_jt_scanlistednoscale + S (jt_scale_scanlistedno) = S ((S (jt_index_scanlistedno)) * x3)) /\ exists fs_q_jt_scanlistednoscale. x2 = fs_q_jt_scanlistednoscale * S ((S (jt_index_scanlistedno)) * x3) + (jt_scale_scanlistedno))))) /\ (forall jt_index_scanlistednoequal jt_left_scanlistednoequal jt_right_scanlistednoequal. (exists jt_gap_scanlistednoequalindex. jt_gap_scanlistednoequalindex+S (jt_index_scanlistednoequal)=(k)) -> (((exists fs_h_jt_scanlistednoequalleft. fs_h_jt_scanlistednoequalleft + S (jt_left_scanlistednoequal) = S ((S (jt_index_scanlistednoequal)) * c)) /\ exists fs_q_jt_scanlistednoequalleft. t = fs_q_jt_scanlistednoequalleft * S ((S (jt_index_scanlistednoequal)) * c) + (jt_left_scanlistednoequal))) -> (((exists fs_h_jt_scanlistednoequalright. fs_h_jt_scanlistednoequalright + S (jt_right_scanlistednoequal) = S ((S (jt_index_scanlistednoequal)) * jt_scale_scanlistedno)) /\ exists fs_q_jt_scanlistednoequalright. jt_code_scanlistedno = fs_q_jt_scanlistednoequalright * S ((S (jt_index_scanlistednoequal)) * jt_scale_scanlistedno) + (jt_right_scanlistednoequal))) -> jt_left_scanlistednoequal=jt_right_scanlistednoequal)))))
  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 : exists U V W X. ((forall jt_i_scantotalnew. (exists jt_gap_scantotalnewsoundindex. jt_gap_scantotalnewsoundindex+S (jt_i_scantotalnew)=(S x4)) -> exists jt_b_scantotalnew jt_e_scantotalnew. ((((((exists fs_h_jt_scantotalnewsoundcode. fs_h_jt_scantotalnewsoundcode + S (jt_b_scantotalnew) = S ((S (jt_i_scantotalnew)) * V)) /\ exists fs_q_jt_scantotalnewsoundcode. U = fs_q_jt_scantotalnewsoundcode * S ((S (jt_i_scantotalnew)) * V) + (jt_b_scantotalnew))) /\ (((exists fs_h_jt_scantotalnewsoundscale. fs_h_jt_scantotalnewsoundscale + S (jt_e_scantotalnew) = S ((S (jt_i_scantotalnew)) * X)) /\ exists fs_q_jt_scantotalnewsoundscale. W = fs_q_jt_scantotalnewsoundscale * S ((S (jt_i_scantotalnew)) * X) + (jt_e_scantotalnew))))) /\ (((forall jt_index_scantotalnewbound. (exists jt_gap_scantotalnewboundindex. jt_gap_scantotalnewboundindex+S (jt_index_scantotalnewbound)=(k)) -> exists jt_value_scantotalnewbound. ((((exists fs_h_jt_scantotalnewboundat. fs_h_jt_scantotalnewboundat + S (jt_value_scantotalnewbound) = S ((S (jt_index_scantotalnewbound)) * jt_e_scantotalnew)) /\ exists fs_q_jt_scantotalnewboundat. jt_b_scantotalnew = fs_q_jt_scantotalnewboundat * S ((S (jt_index_scantotalnewbound)) * jt_e_scantotalnew) + (jt_value_scantotalnewbound))) /\ (exists jt_gap_scantotalnewboundvalue. jt_gap_scantotalnewboundvalue+S (jt_value_scantotalnewbound)=(n)))) /\ (forall jt_divisor_scantotalnewprimitive. (exists jt_factor_scantotalnewprimitivemodulus. (n)=(jt_divisor_scantotalnewprimitive)*jt_factor_scantotalnewprimitivemodulus) -> (forall jt_index_scantotalnewprimitivecoordinates jt_value_scantotalnewprimitivecoordinates. (exists jt_gap_scantotalnewprimitivecoordinatesindex. jt_gap_scantotalnewprimitivecoordinatesindex+S (jt_index_scantotalnewprimitivecoordinates)=(k)) -> (((exists fs_h_jt_scantotalnewprimitivecoordinatesat. fs_h_jt_scantotalnewprimitivecoordinatesat + S (jt_value_scantotalnewprimitivecoordinates) = S ((S (jt_index_scantotalnewprimitivecoordinates)) * jt_e_scantotalnew)) /\ exists fs_q_jt_scantotalnewprimitivecoordinatesat. jt_b_scantotalnew = fs_q_jt_scantotalnewprimitivecoordinatesat * S ((S (jt_index_scantotalnewprimitivecoordinates)) * jt_e_scantotalnew) + (jt_value_scantotalnewprimitivecoordinates))) -> (exists jt_factor_scantotalnewprimitivecoordinatesdivides. (jt_value_scantotalnewprimitivecoordinates)=(jt_divisor_scantotalnewprimitive)*jt_factor_scantotalnewprimitivecoordinatesdivides)) -> jt_divisor_scantotalnewprimitive=1))))) /\ (((forall jt_i_scantotalnew jt_h_scantotalnew jt_b_scantotalnew jt_e_scantotalnew jt_d_scantotalnew jt_f_scantotalnew. (exists jt_gap_scantotalnewfirstindex. jt_gap_scantotalnewfirstindex+S (jt_i_scantotalnew)=(S x4)) -> (exists jt_gap_scantotalnewsecondindex. jt_gap_scantotalnewsecondindex+S (jt_h_scantotalnew)=(S x4)) -> (((((exists fs_h_jt_scantotalnewfirstcode. fs_h_jt_scantotalnewfirstcode + S (jt_b_scantotalnew) = S ((S (jt_i_scantotalnew)) * V)) /\ exists fs_q_jt_scantotalnewfirstcode. U = fs_q_jt_scantotalnewfirstcode * S ((S (jt_i_scantotalnew)) * V) + (jt_b_scantotalnew))) /\ (((exists fs_h_jt_scantotalnewfirstscale. fs_h_jt_scantotalnewfirstscale + S (jt_e_scantotalnew) = S ((S (jt_i_scantotalnew)) * X)) /\ exists fs_q_jt_scantotalnewfirstscale. W = fs_q_jt_scantotalnewfirstscale * S ((S (jt_i_scantotalnew)) * X) + (jt_e_scantotalnew))))) -> (((((exists fs_h_jt_scantotalnewsecondcode. fs_h_jt_scantotalnewsecondcode + S (jt_d_scantotalnew) = S ((S (jt_h_scantotalnew)) * V)) /\ exists fs_q_jt_scantotalnewsecondcode. U = fs_q_jt_scantotalnewsecondcode * S ((S (jt_h_scantotalnew)) * V) + (jt_d_scantotalnew))) /\ (((exists fs_h_jt_scantotalnewsecondscale. fs_h_jt_scantotalnewsecondscale + S (jt_f_scantotalnew) = S ((S (jt_h_scantotalnew)) * X)) /\ exists fs_q_jt_scantotalnewsecondscale. W = fs_q_jt_scantotalnewsecondscale * S ((S (jt_h_scantotalnew)) * X) + (jt_f_scantotalnew))))) -> (forall jt_index_scantotalnewsame jt_left_scantotalnewsame jt_right_scantotalnewsame. (exists jt_gap_scantotalnewsameindex. jt_gap_scantotalnewsameindex+S (jt_index_scantotalnewsame)=(k)) -> (((exists fs_h_jt_scantotalnewsameleft. fs_h_jt_scantotalnewsameleft + S (jt_left_scantotalnewsame) = S ((S (jt_index_scantotalnewsame)) * jt_e_scantotalnew)) /\ exists fs_q_jt_scantotalnewsameleft. jt_b_scantotalnew = fs_q_jt_scantotalnewsameleft * S ((S (jt_index_scantotalnewsame)) * jt_e_scantotalnew) + (jt_left_scantotalnewsame))) -> (((exists fs_h_jt_scantotalnewsameright. fs_h_jt_scantotalnewsameright + S (jt_right_scantotalnewsame) = S ((S (jt_index_scantotalnewsame)) * jt_f_scantotalnew)) /\ exists fs_q_jt_scantotalnewsameright. jt_d_scantotalnew = fs_q_jt_scantotalnewsameright * S ((S (jt_index_scantotalnewsame)) * jt_f_scantotalnew) + (jt_right_scantotalnewsame))) -> jt_left_scantotalnewsame=jt_right_scantotalnewsame) -> jt_i_scantotalnew=jt_h_scantotalnew) /\ (forall jt_z_scantotalnew. (exists jt_gap_scantotalnewcodeindex. jt_gap_scantotalnewcodeindex+S (jt_z_scantotalnew)=(S t)) -> (forall jt_index_scantotalnewinputbound. (exists jt_gap_scantotalnewinputboundindex. jt_gap_scantotalnewinputboundindex+S (jt_index_scantotalnewinputbound)=(k)) -> exists jt_value_scantotalnewinputbound. ((((exists fs_h_jt_scantotalnewinputboundat. fs_h_jt_scantotalnewinputboundat + S (jt_value_scantotalnewinputbound) = S ((S (jt_index_scantotalnewinputbound)) * c)) /\ exists fs_q_jt_scantotalnewinputboundat. jt_z_scantotalnew = fs_q_jt_scantotalnewinputboundat * S ((S (jt_index_scantotalnewinputbound)) * c) + (jt_value_scantotalnewinputbound))) /\ (exists jt_gap_scantotalnewinputboundvalue. jt_gap_scantotalnewinputboundvalue+S (jt_value_scantotalnewinputbound)=(n)))) -> (forall jt_divisor_scantotalnewinputprimitive. (exists jt_factor_scantotalnewinputprimitivemodulus. (n)=(jt_divisor_scantotalnewinputprimitive)*jt_factor_scantotalnewinputprimitivemodulus) -> (forall jt_index_scantotalnewinputprimitivecoordinates jt_value_scantotalnewinputprimitivecoordinates. (exists jt_gap_scantotalnewinputprimitivecoordinatesindex. jt_gap_scantotalnewinputprimitivecoordinatesindex+S (jt_index_scantotalnewinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_scantotalnewinputprimitivecoordinatesat. fs_h_jt_scantotalnewinputprimitivecoordinatesat + S (jt_value_scantotalnewinputprimitivecoordinates) = S ((S (jt_index_scantotalnewinputprimitivecoordinates)) * c)) /\ exists fs_q_jt_scantotalnewinputprimitivecoordinatesat. jt_z_scantotalnew = fs_q_jt_scantotalnewinputprimitivecoordinatesat * S ((S (jt_index_scantotalnewinputprimitivecoordinates)) * c) + (jt_value_scantotalnewinputprimitivecoordinates))) -> (exists jt_factor_scantotalnewinputprimitivecoordinatesdivides. (jt_value_scantotalnewinputprimitivecoordinates)=(jt_divisor_scantotalnewinputprimitive)*jt_factor_scantotalnewinputprimitivecoordinatesdivides)) -> jt_divisor_scantotalnewinputprimitive=1) -> (exists jt_index_scantotalnewlisted jt_code_scantotalnewlisted jt_scale_scantotalnewlisted. ((exists jt_gap_scantotalnewlistedindex. jt_gap_scantotalnewlistedindex+S (jt_index_scantotalnewlisted)=(S x4)) /\ (((((((exists fs_h_jt_scantotalnewlistedcode. fs_h_jt_scantotalnewlistedcode + S (jt_code_scantotalnewlisted) = S ((S (jt_index_scantotalnewlisted)) * V)) /\ exists fs_q_jt_scantotalnewlistedcode. U = fs_q_jt_scantotalnewlistedcode * S ((S (jt_index_scantotalnewlisted)) * V) + (jt_code_scantotalnewlisted))) /\ (((exists fs_h_jt_scantotalnewlistedscale. fs_h_jt_scantotalnewlistedscale + S (jt_scale_scantotalnewlisted) = S ((S (jt_index_scantotalnewlisted)) * X)) /\ exists fs_q_jt_scantotalnewlistedscale. W = fs_q_jt_scantotalnewlistedscale * S ((S (jt_index_scantotalnewlisted)) * X) + (jt_scale_scantotalnewlisted))))) /\ (forall jt_index_scantotalnewlistedequal jt_left_scantotalnewlistedequal jt_right_scantotalnewlistedequal. (exists jt_gap_scantotalnewlistedequalindex. jt_gap_scantotalnewlistedequalindex+S (jt_index_scantotalnewlistedequal)=(k)) -> (((exists fs_h_jt_scantotalnewlistedequalleft. fs_h_jt_scantotalnewlistedequalleft + S (jt_left_scantotalnewlistedequal) = S ((S (jt_index_scantotalnewlistedequal)) * c)) /\ exists fs_q_jt_scantotalnewlistedequalleft. jt_z_scantotalnew = fs_q_jt_scantotalnewlistedequalleft * S ((S (jt_index_scantotalnewlistedequal)) * c) + (jt_left_scantotalnewlistedequal))) -> (((exists fs_h_jt_scantotalnewlistedequalright. fs_h_jt_scantotalnewlistedequalright + S (jt_right_scantotalnewlistedequal) = S ((S (jt_index_scantotalnewlistedequal)) * jt_scale_scantotalnewlisted)) /\ exists fs_q_jt_scantotalnewlistedequalright. jt_code_scantotalnewlisted = fs_q_jt_scantotalnewlistedequalright * S ((S (jt_index_scantotalnewlistedequal)) * jt_scale_scantotalnewlisted) + (jt_right_scantotalnewlistedequal))) -> jt_left_scantotalnewlistedequal=jt_right_scantotalnewlistedequal)))))))))
  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