AF0017

factor_permutation_matching_unswap

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

Undo a target-list swap by swapping the two corresponding actual source-map entries. Entry alignment follows at the two moved positions and everywhere else by map injectivity.

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.

Exact expanded first-order arithmetic statement

forall b c d e D E u v U V l i j p q. (exists pfp_gap_unswap_source. pfp_gap_unswap_source + S (i) = (l)) -> (exists pfp_gap_unswap_target. pfp_gap_unswap_target + S (j) = (l)) -> (((forall pfp_i_unswap_permutationbounded. (exists pfp_gap_unswap_permutationboundedindex. pfp_gap_unswap_permutationboundedindex + S (pfp_i_unswap_permutationbounded) = (S l)) -> exists pfp_a_unswap_permutationbounded. (((exists ff_h_pfp_unswap_permutationboundedentry. ff_h_pfp_unswap_permutationboundedentry + S (pfp_a_unswap_permutationbounded) = S ((S (pfp_i_unswap_permutationbounded)) * v)) /\ exists ff_q_pfp_unswap_permutationboundedentry. u = ff_q_pfp_unswap_permutationboundedentry * S ((S (pfp_i_unswap_permutationbounded)) * v) + (pfp_a_unswap_permutationbounded))) /\ (exists pfp_gap_unswap_permutationboundedvalue. pfp_gap_unswap_permutationboundedvalue + S (pfp_a_unswap_permutationbounded) = (S l))) /\ (((forall pfp_i_unswap_permutationinjective pfp_j_unswap_permutationinjective pfp_a_unswap_permutationinjective. (exists pfp_gap_unswap_permutationinjectivefirst. pfp_gap_unswap_permutationinjectivefirst + S (pfp_i_unswap_permutationinjective) = (S l)) -> (exists pfp_gap_unswap_permutationinjectivesecond. pfp_gap_unswap_permutationinjectivesecond + S (pfp_j_unswap_permutationinjective) = (S l)) -> (((exists ff_h_pfp_unswap_permutationinjectiveleft. ff_h_pfp_unswap_permutationinjectiveleft + S (pfp_a_unswap_permutationinjective) = S ((S (pfp_i_unswap_permutationinjective)) * v)) /\ exists ff_q_pfp_unswap_permutationinjectiveleft. u = ff_q_pfp_unswap_permutationinjectiveleft * S ((S (pfp_i_unswap_permutationinjective)) * v) + (pfp_a_unswap_permutationinjective))) -> (((exists ff_h_pfp_unswap_permutationinjectiveright. ff_h_pfp_unswap_permutationinjectiveright + S (pfp_a_unswap_permutationinjective) = S ((S (pfp_j_unswap_permutationinjective)) * v)) /\ exists ff_q_pfp_unswap_permutationinjectiveright. u = ff_q_pfp_unswap_permutationinjectiveright * S ((S (pfp_j_unswap_permutationinjective)) * v) + (pfp_a_unswap_permutationinjective))) -> pfp_i_unswap_permutationinjective = pfp_j_unswap_permutationinjective) /\ (forall pfp_a_unswap_permutationsurjective. (exists pfp_gap_unswap_permutationsurjectivevalue. pfp_gap_unswap_permutationsurjectivevalue + S (pfp_a_unswap_permutationsurjective) = (S l)) -> exists pfp_i_unswap_permutationsurjective. (exists pfp_gap_unswap_permutationsurjectiveindex. pfp_gap_unswap_permutationsurjectiveindex + S (pfp_i_unswap_permutationsurjective) = (S l)) /\ (((exists ff_h_pfp_unswap_permutationsurjectiveentry. ff_h_pfp_unswap_permutationsurjectiveentry + S (pfp_a_unswap_permutationsurjective) = S ((S (pfp_i_unswap_permutationsurjective)) * v)) /\ exists ff_q_pfp_unswap_permutationsurjectiveentry. u = ff_q_pfp_unswap_permutationsurjectiveentry * S ((S (pfp_i_unswap_permutationsurjective)) * v) + (pfp_a_unswap_permutationsurjective)))))))) -> (forall pfp_i_unswap_matching pfp_j_unswap_matching pfp_a_unswap_matching. (exists pfp_gap_unswap_matchingbound. pfp_gap_unswap_matchingbound + S (pfp_i_unswap_matching) = (S l)) -> (((exists ff_h_pfp_unswap_matchingmap. ff_h_pfp_unswap_matchingmap + S (pfp_j_unswap_matching) = S ((S (pfp_i_unswap_matching)) * v)) /\ exists ff_q_pfp_unswap_matchingmap. u = ff_q_pfp_unswap_matchingmap * S ((S (pfp_i_unswap_matching)) * v) + (pfp_j_unswap_matching))) -> (((exists ff_h_pfp_unswap_matchingsource. ff_h_pfp_unswap_matchingsource + S (pfp_a_unswap_matching) = S ((S (pfp_i_unswap_matching)) * c)) /\ exists ff_q_pfp_unswap_matchingsource. b = ff_q_pfp_unswap_matchingsource * S ((S (pfp_i_unswap_matching)) * c) + (pfp_a_unswap_matching))) -> (((exists ff_h_pfp_unswap_matchingtarget. ff_h_pfp_unswap_matchingtarget + S (pfp_a_unswap_matching) = S ((S (pfp_j_unswap_matching)) * E)) /\ exists ff_q_pfp_unswap_matchingtarget. D = ff_q_pfp_unswap_matchingtarget * S ((S (pfp_j_unswap_matching)) * E) + (pfp_a_unswap_matching)))) -> (((((exists ff_h_pfp_target_swapoldi. ff_h_pfp_target_swapoldi + S (p) = S ((S (j)) * e)) /\ exists ff_q_pfp_target_swapoldi. d = ff_q_pfp_target_swapoldi * S ((S (j)) * e) + (p))) /\ (((((exists ff_h_pfp_target_swapoldlast. ff_h_pfp_target_swapoldlast + S (q) = S ((S (l)) * e)) /\ exists ff_q_pfp_target_swapoldlast. d = ff_q_pfp_target_swapoldlast * S ((S (l)) * e) + (q))) /\ (((((exists ff_h_pfp_target_swapnewi. ff_h_pfp_target_swapnewi + S (q) = S ((S (j)) * E)) /\ exists ff_q_pfp_target_swapnewi. D = ff_q_pfp_target_swapnewi * S ((S (j)) * E) + (q))) /\ (((((exists ff_h_pfp_target_swapnewlast. ff_h_pfp_target_swapnewlast + S (p) = S ((S (l)) * E)) /\ exists ff_q_pfp_target_swapnewlast. D = ff_q_pfp_target_swapnewlast * S ((S (l)) * E) + (p))) /\ (forall pfp_j_target_swap pfp_a_target_swap. (exists pfp_gap_target_swapbound. pfp_gap_target_swapbound + S (pfp_j_target_swap) = (S (l))) -> ~(pfp_j_target_swap = j) -> ~(pfp_j_target_swap = l) -> (((exists ff_h_pfp_target_swapold. ff_h_pfp_target_swapold + S (pfp_a_target_swap) = S ((S (pfp_j_target_swap)) * e)) /\ exists ff_q_pfp_target_swapold. d = ff_q_pfp_target_swapold * S ((S (pfp_j_target_swap)) * e) + (pfp_a_target_swap))) -> (((exists ff_h_pfp_target_swapnew. ff_h_pfp_target_swapnew + S (pfp_a_target_swap) = S ((S (pfp_j_target_swap)) * E)) /\ exists ff_q_pfp_target_swapnew. D = ff_q_pfp_target_swapnew * S ((S (pfp_j_target_swap)) * E) + (pfp_a_target_swap)))))))))))) -> (((((exists ff_h_pfp_map_swapoldi. ff_h_pfp_map_swapoldi + S (j) = S ((S (i)) * v)) /\ exists ff_q_pfp_map_swapoldi. u = ff_q_pfp_map_swapoldi * S ((S (i)) * v) + (j))) /\ (((((exists ff_h_pfp_map_swapoldlast. ff_h_pfp_map_swapoldlast + S (l) = S ((S (l)) * v)) /\ exists ff_q_pfp_map_swapoldlast. u = ff_q_pfp_map_swapoldlast * S ((S (l)) * v) + (l))) /\ (((((exists ff_h_pfp_map_swapnewi. ff_h_pfp_map_swapnewi + S (l) = S ((S (i)) * V)) /\ exists ff_q_pfp_map_swapnewi. U = ff_q_pfp_map_swapnewi * S ((S (i)) * V) + (l))) /\ (((((exists ff_h_pfp_map_swapnewlast. ff_h_pfp_map_swapnewlast + S (j) = S ((S (l)) * V)) /\ exists ff_q_pfp_map_swapnewlast. U = ff_q_pfp_map_swapnewlast * S ((S (l)) * V) + (j))) /\ (forall pfp_j_map_swap pfp_a_map_swap. (exists pfp_gap_map_swapbound. pfp_gap_map_swapbound + S (pfp_j_map_swap) = (S (l))) -> ~(pfp_j_map_swap = i) -> ~(pfp_j_map_swap = l) -> (((exists ff_h_pfp_map_swapold. ff_h_pfp_map_swapold + S (pfp_a_map_swap) = S ((S (pfp_j_map_swap)) * v)) /\ exists ff_q_pfp_map_swapold. u = ff_q_pfp_map_swapold * S ((S (pfp_j_map_swap)) * v) + (pfp_a_map_swap))) -> (((exists ff_h_pfp_map_swapnew. ff_h_pfp_map_swapnew + S (pfp_a_map_swap) = S ((S (pfp_j_map_swap)) * V)) /\ exists ff_q_pfp_map_swapnew. U = ff_q_pfp_map_swapnew * S ((S (pfp_j_map_swap)) * V) + (pfp_a_map_swap)))))))))))) -> (forall pfp_i_unswap_result pfp_j_unswap_result pfp_a_unswap_result. (exists pfp_gap_unswap_resultbound. pfp_gap_unswap_resultbound + S (pfp_i_unswap_result) = (S l)) -> (((exists ff_h_pfp_unswap_resultmap. ff_h_pfp_unswap_resultmap + S (pfp_j_unswap_result) = S ((S (pfp_i_unswap_result)) * V)) /\ exists ff_q_pfp_unswap_resultmap. U = ff_q_pfp_unswap_resultmap * S ((S (pfp_i_unswap_result)) * V) + (pfp_j_unswap_result))) -> (((exists ff_h_pfp_unswap_resultsource. ff_h_pfp_unswap_resultsource + S (pfp_a_unswap_result) = S ((S (pfp_i_unswap_result)) * c)) /\ exists ff_q_pfp_unswap_resultsource. b = ff_q_pfp_unswap_resultsource * S ((S (pfp_i_unswap_result)) * c) + (pfp_a_unswap_result))) -> (((exists ff_h_pfp_unswap_resulttarget. ff_h_pfp_unswap_resulttarget + S (pfp_a_unswap_result) = S ((S (pfp_j_unswap_result)) * e)) /\ exists ff_q_pfp_unswap_resulttarget. d = ff_q_pfp_unswap_resulttarget * S ((S (pfp_j_unswap_result)) * e) + (pfp_a_unswap_result))))

Constructive proof overview

Generated structural guide

Undo a target-list swap by swapping the two corresponding actual source-map entries. Entry alignment follows at the two moved positions and everywhere else by map injectivity.

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

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

Proof neighborhood

Direct dependencies

eq_decidable Stable theorem; checked-use authorized beta_at_unique Stable theorem; checked-use authorized AF0012 factor_permutation_swap_reflect_unchanged finite_bounded_entry_lt Stable theorem; checked-use authorized le_succ Stable theorem; checked-use authorized le_refl Stable theorem; checked-use authorized

Direct dependents

AF0018 factor_permutation_matched_unswap_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

206 script commands · 40 reading checkpoints · 15 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 (1)
factor permutation swap reflect unchanged

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
  5. L5
    intro D
  6. L6
    intro E
  7. L7
    intro u
  8. L8
    intro v
  9. L9
    intro U
  10. L10
    intro V
02Fix variables and assumptionsL11–20

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

  1. L11
    intro l
  2. L12
    intro i
  3. L13
    intro j
  4. L14
    intro p
  5. L15
    intro q
  6. L16
    intro hi
  7. L17
    intro hj
  8. L18
    intro hp
  9. L19
    intro hm
  10. L20
    intro hs
03Fix variables and assumptionsL21–21

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

  1. L21
    intro ht
04Separate the logical casesL22–23

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

  1. L22
    cases hp
  2. L23
    cases hp_right
05Establish hscopyL24–25

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

  1. L24
    have hscopy : BetaAt(d,e,j,p) ∧ (BetaAt(d,e,l,q) ∧ (BetaAt(D,E,j,q) ∧ (BetaAt(D,E,l,p) ∧ (∀ x. ∀ y. Lt(x,S l) → ¬x = j → ¬x = l → BetaAt(d,e,x,y) → BetaAt(D,E,x,y)))))Definitions: LtBetaAt
  2. L25
    exact hs
06Separate the logical casesL26–29

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

  1. L26
    cases hscopy
  2. L27
    cases hscopy_right
  3. L28
    cases hscopy_right_right
  4. L29
    cases hscopy_right_right_right
07Establish htcopyL30–31

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

  1. L30
    have htcopy : BetaAt(u,v,i,j) ∧ (BetaAt(u,v,l,l) ∧ (BetaAt(U,V,i,l) ∧ (BetaAt(U,V,l,j) ∧ (∀ x. ∀ y. Lt(x,S l) → ¬x = i → ¬x = l → BetaAt(u,v,x,y) → BetaAt(U,V,x,y)))))Definitions: LtBetaAt
  2. L31
    exact ht
08Separate the logical casesL32–35

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

  1. L32
    cases htcopy
  2. L33
    cases htcopy_right
  3. L34
    cases htcopy_right_right
  4. L35
    cases htcopy_right_right_right
09Fix variables and assumptionsL36–41

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

  1. L36
    intro k
  2. L37
    intro z
  3. L38
    intro a
  4. L39
    intro hk
  5. L40
    intro hmap
  6. L41
    intro hsource
10Establish hcaseL42–45

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

  1. L42
    have hcase : k = i \/ ~(k = i)
  2. L43
    specialize eq_decidable (k)
  3. L44
    specialize eq_decidable (i)
  4. L45
    apply eq_decidable
11Separate the logical casesL46–46

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

  1. L46
    cases hcase
12Establish hzL47–56

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

  1. L47
    have hz : z = l
  2. L48
    specialize beta_at_unique (U)
  3. L49
    specialize beta_at_unique (V)
  4. L50
    specialize beta_at_unique (i)
  5. L51
    specialize beta_at_unique (z)
  6. L52
    specialize beta_at_unique (l)
  7. L53
    apply beta_at_unique
  8. L54
    rewrite hcase_left at hmap
  9. L55
    rewrite hcase_left at hmap
  10. L56
    exact hmap
13Use earlier factsL57–57

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

  1. L57
    exact htcopy_right_right_left
14Establish hvalueL58–67

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

  1. L58
    have hvalue : ((exists ff_h_pfp_unswap_selected_target. ff_h_pfp_unswap_selected_target + S (a) = S ((S (j)) * E)) /\ exists ff_q_pfp_unswap_selected_target. D = ff_q_pfp_unswap_selected_target * S ((S (j)) * E) + (a))
  2. L59
    specialize hm (i)
  3. L60
    specialize hm (j)
  4. L61
    specialize hm (a)
  5. L62
    apply hm
  6. L63
    specialize le_succ (S i)
  7. L64
    specialize le_succ (l)
  8. L65
    apply le_succ
  9. L66
    exact hi
  10. L67
    exact htcopy_left
15Calculate and transport equalitiesL68–69

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

  1. L68
    rewrite hcase_left at hsource
  2. L69
    rewrite hcase_left at hsource
16Use earlier factsL70–70

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

  1. L70
    exact hsource
17Establish haL71–80

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

  1. L71
    have ha : a = q
  2. L72
    specialize beta_at_unique (D)
  3. L73
    specialize beta_at_unique (E)
  4. L74
    specialize beta_at_unique (j)
  5. L75
    specialize beta_at_unique (a)
  6. L76
    specialize beta_at_unique (q)
  7. L77
    apply beta_at_unique
  8. L78
    exact hvalue
  9. L79
    exact hscopy_right_right_left
  10. L80
    rewrite hz
18Calculate and transport equalitiesL81–83

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

  1. L81
    rewrite hz
  2. L82
    rewrite ha
  3. L83
    rewrite ha
19Use earlier factsL84–84

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

  1. L84
    exact hscopy_right_left
20Establish hlastL85–88

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

  1. L85
    have hlast : k = l \/ ~(k = l)
  2. L86
    specialize eq_decidable (k)
  3. L87
    specialize eq_decidable (l)
  4. L88
    apply eq_decidable
21Separate the logical casesL89–89

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

  1. L89
    cases hlast
22Establish hzL90–99

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

  1. L90
    have hz : z = j
  2. L91
    specialize beta_at_unique (U)
  3. L92
    specialize beta_at_unique (V)
  4. L93
    specialize beta_at_unique (l)
  5. L94
    specialize beta_at_unique (z)
  6. L95
    specialize beta_at_unique (j)
  7. L96
    apply beta_at_unique
  8. L97
    rewrite hlast_left at hmap
  9. L98
    rewrite hlast_left at hmap
  10. L99
    exact hmap
23Use earlier factsL100–100

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

  1. L100
    exact htcopy_right_right_right_left
24Establish hvalueL101–110

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

  1. L101
    have hvalue : ((exists ff_h_pfp_unswap_last_target. ff_h_pfp_unswap_last_target + S (a) = S ((S (l)) * E)) /\ exists ff_q_pfp_unswap_last_target. D = ff_q_pfp_unswap_last_target * S ((S (l)) * E) + (a))
  2. L102
    specialize hm (l)
  3. L103
    specialize hm (l)
  4. L104
    specialize hm (a)
  5. L105
    apply hm
  6. L106
    specialize le_refl (S l)
  7. L107
    apply le_refl
  8. L108
    exact htcopy_right_left
  9. L109
    rewrite hlast_left at hsource
  10. L110
    rewrite hlast_left at hsource
25Use earlier factsL111–111

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

  1. L111
    exact hsource
26Establish haL112–121

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

  1. L112
    have ha : a = p
  2. L113
    specialize beta_at_unique (D)
  3. L114
    specialize beta_at_unique (E)
  4. L115
    specialize beta_at_unique (l)
  5. L116
    specialize beta_at_unique (a)
  6. L117
    specialize beta_at_unique (p)
  7. L118
    apply beta_at_unique
  8. L119
    exact hvalue
  9. L120
    exact hscopy_right_right_right_left
  10. L121
    rewrite hz
27Calculate and transport equalitiesL122–124

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

  1. L122
    rewrite hz
  2. L123
    rewrite ha
  3. L124
    rewrite ha
28Use earlier factsL125–125

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

  1. L125
    exact hscopy_left
29Establish holdL126–135

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

  1. L126
    have hold : ((exists ff_h_pfp_unswap_unchanged_map. ff_h_pfp_unswap_unchanged_map + S (z) = S ((S (k)) * v)) /\ exists ff_q_pfp_unswap_unchanged_map. u = ff_q_pfp_unswap_unchanged_map * S ((S (k)) * v) + (z))
  2. L127
    specialize factor_permutation_swap_reflect_unchanged (u)
  3. L128
    specialize factor_permutation_swap_reflect_unchanged (v)
  4. L129
    specialize factor_permutation_swap_reflect_unchanged (U)
  5. L130
    specialize factor_permutation_swap_reflect_unchanged (V)
  6. L131
    specialize factor_permutation_swap_reflect_unchanged (l)
  7. L132
    specialize factor_permutation_swap_reflect_unchanged (i)
  8. L133
    specialize factor_permutation_swap_reflect_unchanged (j)
  9. L134
    specialize factor_permutation_swap_reflect_unchanged (l)
  10. L135
    specialize factor_permutation_swap_reflect_unchanged (k)
30Use earlier factsL136–142

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

  1. L136
    specialize factor_permutation_swap_reflect_unchanged (z)
  2. L137
    apply factor_permutation_swap_reflect_unchanged
  3. L138
    exact ht
  4. L139
    exact hk
  5. L140
    exact hcase_right
  6. L141
    exact hlast_right
  7. L142
    exact hmap
31Establish hvalueL143–150

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

  1. L143
    have hvalue : ((exists ff_h_pfp_unswap_unchanged_target. ff_h_pfp_unswap_unchanged_target + S (a) = S ((S (z)) * E)) /\ exists ff_q_pfp_unswap_unchanged_target. D = ff_q_pfp_unswap_unchanged_target * S ((S (z)) * E) + (a))
  2. L144
    specialize hm (k)
  3. L145
    specialize hm (z)
  4. L146
    specialize hm (a)
  5. L147
    apply hm
  6. L148
    exact hk
  7. L149
    exact hold
  8. L150
    exact hsource
32Establish hzboundL151–160

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

  1. L151
    have hzbound : exists pfp_gap_unswap_image_bound. pfp_gap_unswap_image_bound + S (z) = (S l)
  2. L152
    specialize finite_bounded_entry_lt (u)
  3. L153
    specialize finite_bounded_entry_lt (v)
  4. L154
    specialize finite_bounded_entry_lt (S l)
  5. L155
    specialize finite_bounded_entry_lt (k)
  6. L156
    specialize finite_bounded_entry_lt (z)
  7. L157
    apply finite_bounded_entry_lt
  8. L158
    exact hp_left
  9. L159
    exact hk
  10. L160
    exact hold
33Establish hzjL161–170

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

  1. L161
    have hzj : ~(z = j)
  2. L162
    intro heq
  3. L163
    apply hcase_right
  4. L164
    specialize hp_right_left (k)
  5. L165
    specialize hp_right_left (i)
  6. L166
    specialize hp_right_left (j)
  7. L167
    apply hp_right_left
  8. L168
    exact hk
  9. L169
    specialize le_succ (S i)
  10. L170
    specialize le_succ (l)
34Use earlier factsL171–172

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

  1. L171
    apply le_succ
  2. L172
    exact hi
35Calculate and transport equalitiesL173–174

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

  1. L173
    rewrite heq at hold
  2. L174
    rewrite heq at hold
36Use earlier factsL175–176

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

  1. L175
    exact hold
  2. L176
    exact htcopy_left
37Establish hzlL177–186

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

  1. L177
    have hzl : ~(z = l)
  2. L178
    intro heq
  3. L179
    apply hlast_right
  4. L180
    specialize hp_right_left (k)
  5. L181
    specialize hp_right_left (l)
  6. L182
    specialize hp_right_left (l)
  7. L183
    apply hp_right_left
  8. L184
    exact hk
  9. L185
    specialize le_refl (S l)
  10. L186
    apply le_refl
38Calculate and transport equalitiesL187–188

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

  1. L187
    rewrite heq at hold
  2. L188
    rewrite heq at hold
39Use earlier factsL189–198

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

  1. L189
    exact hold
  2. L190
    exact htcopy_right_left
  3. L191
    specialize factor_permutation_swap_reflect_unchanged (d)
  4. L192
    specialize factor_permutation_swap_reflect_unchanged (e)
  5. L193
    specialize factor_permutation_swap_reflect_unchanged (D)
  6. L194
    specialize factor_permutation_swap_reflect_unchanged (E)
  7. L195
    specialize factor_permutation_swap_reflect_unchanged (l)
  8. L196
    specialize factor_permutation_swap_reflect_unchanged (j)
  9. L197
    specialize factor_permutation_swap_reflect_unchanged (p)
  10. L198
    specialize factor_permutation_swap_reflect_unchanged (q)
40Use earlier factsL199–206

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

  1. L199
    specialize factor_permutation_swap_reflect_unchanged (z)
  2. L200
    specialize factor_permutation_swap_reflect_unchanged (a)
  3. L201
    apply factor_permutation_swap_reflect_unchanged
  4. L202
    exact hs
  5. L203
    exact hzbound
  6. L204
    exact hzj
  7. L205
    exact hzl
  8. L206
    exact hvalue

Library-wide reading audit

Original exact command ledger · 206 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro D
  6. 0006intro E
  7. 0007intro u
  8. 0008intro v
  9. 0009intro U
  10. 0010intro V
  11. 0011intro l
  12. 0012intro i
  13. 0013intro j
  14. 0014intro p
  15. 0015intro q
  16. 0016intro hi
  17. 0017intro hj
  18. 0018intro hp
  19. 0019intro hm
  20. 0020intro hs
  21. 0021intro ht
  22. 0022cases hp
  23. 0023cases hp_right
  24. 0024have hscopy : ((((exists ff_h_pfp_target_swapoldi. ff_h_pfp_target_swapoldi + S (p) = S ((S (j)) * e)) /\ exists ff_q_pfp_target_swapoldi. d = ff_q_pfp_target_swapoldi * S ((S (j)) * e) + (p))) /\ (((((exists ff_h_pfp_target_swapoldlast. ff_h_pfp_target_swapoldlast + S (q) = S ((S (l)) * e)) /\ exists ff_q_pfp_target_swapoldlast. d = ff_q_pfp_target_swapoldlast * S ((S (l)) * e) + (q))) /\ (((((exists ff_h_pfp_target_swapnewi. ff_h_pfp_target_swapnewi + S (q) = S ((S (j)) * E)) /\ exists ff_q_pfp_target_swapnewi. D = ff_q_pfp_target_swapnewi * S ((S (j)) * E) + (q))) /\ (((((exists ff_h_pfp_target_swapnewlast. ff_h_pfp_target_swapnewlast + S (p) = S ((S (l)) * E)) /\ exists ff_q_pfp_target_swapnewlast. D = ff_q_pfp_target_swapnewlast * S ((S (l)) * E) + (p))) /\ (forall pfp_j_target_swap pfp_a_target_swap. (exists pfp_gap_target_swapbound. pfp_gap_target_swapbound + S (pfp_j_target_swap) = (S (l))) -> ~(pfp_j_target_swap = j) -> ~(pfp_j_target_swap = l) -> (((exists ff_h_pfp_target_swapold. ff_h_pfp_target_swapold + S (pfp_a_target_swap) = S ((S (pfp_j_target_swap)) * e)) /\ exists ff_q_pfp_target_swapold. d = ff_q_pfp_target_swapold * S ((S (pfp_j_target_swap)) * e) + (pfp_a_target_swap))) -> (((exists ff_h_pfp_target_swapnew. ff_h_pfp_target_swapnew + S (pfp_a_target_swap) = S ((S (pfp_j_target_swap)) * E)) /\ exists ff_q_pfp_target_swapnew. D = ff_q_pfp_target_swapnew * S ((S (pfp_j_target_swap)) * E) + (pfp_a_target_swap)))))))))))
  25. 0025exact hs
  26. 0026cases hscopy
  27. 0027cases hscopy_right
  28. 0028cases hscopy_right_right
  29. 0029cases hscopy_right_right_right
  30. 0030have htcopy : ((((exists ff_h_pfp_map_swapoldi. ff_h_pfp_map_swapoldi + S (j) = S ((S (i)) * v)) /\ exists ff_q_pfp_map_swapoldi. u = ff_q_pfp_map_swapoldi * S ((S (i)) * v) + (j))) /\ (((((exists ff_h_pfp_map_swapoldlast. ff_h_pfp_map_swapoldlast + S (l) = S ((S (l)) * v)) /\ exists ff_q_pfp_map_swapoldlast. u = ff_q_pfp_map_swapoldlast * S ((S (l)) * v) + (l))) /\ (((((exists ff_h_pfp_map_swapnewi. ff_h_pfp_map_swapnewi + S (l) = S ((S (i)) * V)) /\ exists ff_q_pfp_map_swapnewi. U = ff_q_pfp_map_swapnewi * S ((S (i)) * V) + (l))) /\ (((((exists ff_h_pfp_map_swapnewlast. ff_h_pfp_map_swapnewlast + S (j) = S ((S (l)) * V)) /\ exists ff_q_pfp_map_swapnewlast. U = ff_q_pfp_map_swapnewlast * S ((S (l)) * V) + (j))) /\ (forall pfp_j_map_swap pfp_a_map_swap. (exists pfp_gap_map_swapbound. pfp_gap_map_swapbound + S (pfp_j_map_swap) = (S (l))) -> ~(pfp_j_map_swap = i) -> ~(pfp_j_map_swap = l) -> (((exists ff_h_pfp_map_swapold. ff_h_pfp_map_swapold + S (pfp_a_map_swap) = S ((S (pfp_j_map_swap)) * v)) /\ exists ff_q_pfp_map_swapold. u = ff_q_pfp_map_swapold * S ((S (pfp_j_map_swap)) * v) + (pfp_a_map_swap))) -> (((exists ff_h_pfp_map_swapnew. ff_h_pfp_map_swapnew + S (pfp_a_map_swap) = S ((S (pfp_j_map_swap)) * V)) /\ exists ff_q_pfp_map_swapnew. U = ff_q_pfp_map_swapnew * S ((S (pfp_j_map_swap)) * V) + (pfp_a_map_swap)))))))))))
  31. 0031exact ht
  32. 0032cases htcopy
  33. 0033cases htcopy_right
  34. 0034cases htcopy_right_right
  35. 0035cases htcopy_right_right_right
  36. 0036intro k
  37. 0037intro z
  38. 0038intro a
  39. 0039intro hk
  40. 0040intro hmap
  41. 0041intro hsource
  42. 0042have hcase : k = i \/ ~(k = i)
  43. 0043specialize eq_decidable (k)
  44. 0044specialize eq_decidable (i)
  45. 0045apply eq_decidable
  46. 0046cases hcase
  47. 0047have hz : z = l
  48. 0048specialize beta_at_unique (U)
  49. 0049specialize beta_at_unique (V)
  50. 0050specialize beta_at_unique (i)
  51. 0051specialize beta_at_unique (z)
  52. 0052specialize beta_at_unique (l)
  53. 0053apply beta_at_unique
  54. 0054rewrite hcase_left at hmap
  55. 0055rewrite hcase_left at hmap
  56. 0056exact hmap
  57. 0057exact htcopy_right_right_left
  58. 0058have hvalue : ((exists ff_h_pfp_unswap_selected_target. ff_h_pfp_unswap_selected_target + S (a) = S ((S (j)) * E)) /\ exists ff_q_pfp_unswap_selected_target. D = ff_q_pfp_unswap_selected_target * S ((S (j)) * E) + (a))
  59. 0059specialize hm (i)
  60. 0060specialize hm (j)
  61. 0061specialize hm (a)
  62. 0062apply hm
  63. 0063specialize le_succ (S i)
  64. 0064specialize le_succ (l)
  65. 0065apply le_succ
  66. 0066exact hi
  67. 0067exact htcopy_left
  68. 0068rewrite hcase_left at hsource
  69. 0069rewrite hcase_left at hsource
  70. 0070exact hsource
  71. 0071have ha : a = q
  72. 0072specialize beta_at_unique (D)
  73. 0073specialize beta_at_unique (E)
  74. 0074specialize beta_at_unique (j)
  75. 0075specialize beta_at_unique (a)
  76. 0076specialize beta_at_unique (q)
  77. 0077apply beta_at_unique
  78. 0078exact hvalue
  79. 0079exact hscopy_right_right_left
  80. 0080rewrite hz
  81. 0081rewrite hz
  82. 0082rewrite ha
  83. 0083rewrite ha
  84. 0084exact hscopy_right_left
  85. 0085have hlast : k = l \/ ~(k = l)
  86. 0086specialize eq_decidable (k)
  87. 0087specialize eq_decidable (l)
  88. 0088apply eq_decidable
  89. 0089cases hlast
  90. 0090have hz : z = j
  91. 0091specialize beta_at_unique (U)
  92. 0092specialize beta_at_unique (V)
  93. 0093specialize beta_at_unique (l)
  94. 0094specialize beta_at_unique (z)
  95. 0095specialize beta_at_unique (j)
  96. 0096apply beta_at_unique
  97. 0097rewrite hlast_left at hmap
  98. 0098rewrite hlast_left at hmap
  99. 0099exact hmap
  100. 0100exact htcopy_right_right_right_left
  101. 0101have hvalue : ((exists ff_h_pfp_unswap_last_target. ff_h_pfp_unswap_last_target + S (a) = S ((S (l)) * E)) /\ exists ff_q_pfp_unswap_last_target. D = ff_q_pfp_unswap_last_target * S ((S (l)) * E) + (a))
  102. 0102specialize hm (l)
  103. 0103specialize hm (l)
  104. 0104specialize hm (a)
  105. 0105apply hm
  106. 0106specialize le_refl (S l)
  107. 0107apply le_refl
  108. 0108exact htcopy_right_left
  109. 0109rewrite hlast_left at hsource
  110. 0110rewrite hlast_left at hsource
  111. 0111exact hsource
  112. 0112have ha : a = p
  113. 0113specialize beta_at_unique (D)
  114. 0114specialize beta_at_unique (E)
  115. 0115specialize beta_at_unique (l)
  116. 0116specialize beta_at_unique (a)
  117. 0117specialize beta_at_unique (p)
  118. 0118apply beta_at_unique
  119. 0119exact hvalue
  120. 0120exact hscopy_right_right_right_left
  121. 0121rewrite hz
  122. 0122rewrite hz
  123. 0123rewrite ha
  124. 0124rewrite ha
  125. 0125exact hscopy_left
  126. 0126have hold : ((exists ff_h_pfp_unswap_unchanged_map. ff_h_pfp_unswap_unchanged_map + S (z) = S ((S (k)) * v)) /\ exists ff_q_pfp_unswap_unchanged_map. u = ff_q_pfp_unswap_unchanged_map * S ((S (k)) * v) + (z))
  127. 0127specialize factor_permutation_swap_reflect_unchanged (u)
  128. 0128specialize factor_permutation_swap_reflect_unchanged (v)
  129. 0129specialize factor_permutation_swap_reflect_unchanged (U)
  130. 0130specialize factor_permutation_swap_reflect_unchanged (V)
  131. 0131specialize factor_permutation_swap_reflect_unchanged (l)
  132. 0132specialize factor_permutation_swap_reflect_unchanged (i)
  133. 0133specialize factor_permutation_swap_reflect_unchanged (j)
  134. 0134specialize factor_permutation_swap_reflect_unchanged (l)
  135. 0135specialize factor_permutation_swap_reflect_unchanged (k)
  136. 0136specialize factor_permutation_swap_reflect_unchanged (z)
  137. 0137apply factor_permutation_swap_reflect_unchanged
  138. 0138exact ht
  139. 0139exact hk
  140. 0140exact hcase_right
  141. 0141exact hlast_right
  142. 0142exact hmap
  143. 0143have hvalue : ((exists ff_h_pfp_unswap_unchanged_target. ff_h_pfp_unswap_unchanged_target + S (a) = S ((S (z)) * E)) /\ exists ff_q_pfp_unswap_unchanged_target. D = ff_q_pfp_unswap_unchanged_target * S ((S (z)) * E) + (a))
  144. 0144specialize hm (k)
  145. 0145specialize hm (z)
  146. 0146specialize hm (a)
  147. 0147apply hm
  148. 0148exact hk
  149. 0149exact hold
  150. 0150exact hsource
  151. 0151have hzbound : exists pfp_gap_unswap_image_bound. pfp_gap_unswap_image_bound + S (z) = (S l)
  152. 0152specialize finite_bounded_entry_lt (u)
  153. 0153specialize finite_bounded_entry_lt (v)
  154. 0154specialize finite_bounded_entry_lt (S l)
  155. 0155specialize finite_bounded_entry_lt (k)
  156. 0156specialize finite_bounded_entry_lt (z)
  157. 0157apply finite_bounded_entry_lt
  158. 0158exact hp_left
  159. 0159exact hk
  160. 0160exact hold
  161. 0161have hzj : ~(z = j)
  162. 0162intro heq
  163. 0163apply hcase_right
  164. 0164specialize hp_right_left (k)
  165. 0165specialize hp_right_left (i)
  166. 0166specialize hp_right_left (j)
  167. 0167apply hp_right_left
  168. 0168exact hk
  169. 0169specialize le_succ (S i)
  170. 0170specialize le_succ (l)
  171. 0171apply le_succ
  172. 0172exact hi
  173. 0173rewrite heq at hold
  174. 0174rewrite heq at hold
  175. 0175exact hold
  176. 0176exact htcopy_left
  177. 0177have hzl : ~(z = l)
  178. 0178intro heq
  179. 0179apply hlast_right
  180. 0180specialize hp_right_left (k)
  181. 0181specialize hp_right_left (l)
  182. 0182specialize hp_right_left (l)
  183. 0183apply hp_right_left
  184. 0184exact hk
  185. 0185specialize le_refl (S l)
  186. 0186apply le_refl
  187. 0187rewrite heq at hold
  188. 0188rewrite heq at hold
  189. 0189exact hold
  190. 0190exact htcopy_right_left
  191. 0191specialize factor_permutation_swap_reflect_unchanged (d)
  192. 0192specialize factor_permutation_swap_reflect_unchanged (e)
  193. 0193specialize factor_permutation_swap_reflect_unchanged (D)
  194. 0194specialize factor_permutation_swap_reflect_unchanged (E)
  195. 0195specialize factor_permutation_swap_reflect_unchanged (l)
  196. 0196specialize factor_permutation_swap_reflect_unchanged (j)
  197. 0197specialize factor_permutation_swap_reflect_unchanged (p)
  198. 0198specialize factor_permutation_swap_reflect_unchanged (q)
  199. 0199specialize factor_permutation_swap_reflect_unchanged (z)
  200. 0200specialize factor_permutation_swap_reflect_unchanged (a)
  201. 0201apply factor_permutation_swap_reflect_unchanged
  202. 0202exact hs
  203. 0203exact hzbound
  204. 0204exact hzj
  205. 0205exact hzl
  206. 0206exact hvalue