AF0018

factor_permutation_matched_unswap_exists

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

Use the recursively constructed finite permutation's actual preimage, construct both extended and transposed map codes, and return a full matching bijection into the original unswapped target list.

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 l j p q. (exists pfp_gap_unswap_exists_index. pfp_gap_unswap_exists_index + S (j) = (l)) -> (((((forall pfp_i_unswap_exists_prefixpermutationbounded. (exists pfp_gap_unswap_exists_prefixpermutationboundedindex. pfp_gap_unswap_exists_prefixpermutationboundedindex + S (pfp_i_unswap_exists_prefixpermutationbounded) = (l)) -> exists pfp_a_unswap_exists_prefixpermutationbounded. (((exists ff_h_pfp_unswap_exists_prefixpermutationboundedentry. ff_h_pfp_unswap_exists_prefixpermutationboundedentry + S (pfp_a_unswap_exists_prefixpermutationbounded) = S ((S (pfp_i_unswap_exists_prefixpermutationbounded)) * v)) /\ exists ff_q_pfp_unswap_exists_prefixpermutationboundedentry. u = ff_q_pfp_unswap_exists_prefixpermutationboundedentry * S ((S (pfp_i_unswap_exists_prefixpermutationbounded)) * v) + (pfp_a_unswap_exists_prefixpermutationbounded))) /\ (exists pfp_gap_unswap_exists_prefixpermutationboundedvalue. pfp_gap_unswap_exists_prefixpermutationboundedvalue + S (pfp_a_unswap_exists_prefixpermutationbounded) = (l))) /\ (((forall pfp_i_unswap_exists_prefixpermutationinjective pfp_j_unswap_exists_prefixpermutationinjective pfp_a_unswap_exists_prefixpermutationinjective. (exists pfp_gap_unswap_exists_prefixpermutationinjectivefirst. pfp_gap_unswap_exists_prefixpermutationinjectivefirst + S (pfp_i_unswap_exists_prefixpermutationinjective) = (l)) -> (exists pfp_gap_unswap_exists_prefixpermutationinjectivesecond. pfp_gap_unswap_exists_prefixpermutationinjectivesecond + S (pfp_j_unswap_exists_prefixpermutationinjective) = (l)) -> (((exists ff_h_pfp_unswap_exists_prefixpermutationinjectiveleft. ff_h_pfp_unswap_exists_prefixpermutationinjectiveleft + S (pfp_a_unswap_exists_prefixpermutationinjective) = S ((S (pfp_i_unswap_exists_prefixpermutationinjective)) * v)) /\ exists ff_q_pfp_unswap_exists_prefixpermutationinjectiveleft. u = ff_q_pfp_unswap_exists_prefixpermutationinjectiveleft * S ((S (pfp_i_unswap_exists_prefixpermutationinjective)) * v) + (pfp_a_unswap_exists_prefixpermutationinjective))) -> (((exists ff_h_pfp_unswap_exists_prefixpermutationinjectiveright. ff_h_pfp_unswap_exists_prefixpermutationinjectiveright + S (pfp_a_unswap_exists_prefixpermutationinjective) = S ((S (pfp_j_unswap_exists_prefixpermutationinjective)) * v)) /\ exists ff_q_pfp_unswap_exists_prefixpermutationinjectiveright. u = ff_q_pfp_unswap_exists_prefixpermutationinjectiveright * S ((S (pfp_j_unswap_exists_prefixpermutationinjective)) * v) + (pfp_a_unswap_exists_prefixpermutationinjective))) -> pfp_i_unswap_exists_prefixpermutationinjective = pfp_j_unswap_exists_prefixpermutationinjective) /\ (forall pfp_a_unswap_exists_prefixpermutationsurjective. (exists pfp_gap_unswap_exists_prefixpermutationsurjectivevalue. pfp_gap_unswap_exists_prefixpermutationsurjectivevalue + S (pfp_a_unswap_exists_prefixpermutationsurjective) = (l)) -> exists pfp_i_unswap_exists_prefixpermutationsurjective. (exists pfp_gap_unswap_exists_prefixpermutationsurjectiveindex. pfp_gap_unswap_exists_prefixpermutationsurjectiveindex + S (pfp_i_unswap_exists_prefixpermutationsurjective) = (l)) /\ (((exists ff_h_pfp_unswap_exists_prefixpermutationsurjectiveentry. ff_h_pfp_unswap_exists_prefixpermutationsurjectiveentry + S (pfp_a_unswap_exists_prefixpermutationsurjective) = S ((S (pfp_i_unswap_exists_prefixpermutationsurjective)) * v)) /\ exists ff_q_pfp_unswap_exists_prefixpermutationsurjectiveentry. u = ff_q_pfp_unswap_exists_prefixpermutationsurjectiveentry * S ((S (pfp_i_unswap_exists_prefixpermutationsurjective)) * v) + (pfp_a_unswap_exists_prefixpermutationsurjective)))))))) /\ (forall pfp_i_unswap_exists_prefixmatching pfp_j_unswap_exists_prefixmatching pfp_a_unswap_exists_prefixmatching. (exists pfp_gap_unswap_exists_prefixmatchingbound. pfp_gap_unswap_exists_prefixmatchingbound + S (pfp_i_unswap_exists_prefixmatching) = (l)) -> (((exists ff_h_pfp_unswap_exists_prefixmatchingmap. ff_h_pfp_unswap_exists_prefixmatchingmap + S (pfp_j_unswap_exists_prefixmatching) = S ((S (pfp_i_unswap_exists_prefixmatching)) * v)) /\ exists ff_q_pfp_unswap_exists_prefixmatchingmap. u = ff_q_pfp_unswap_exists_prefixmatchingmap * S ((S (pfp_i_unswap_exists_prefixmatching)) * v) + (pfp_j_unswap_exists_prefixmatching))) -> (((exists ff_h_pfp_unswap_exists_prefixmatchingsource. ff_h_pfp_unswap_exists_prefixmatchingsource + S (pfp_a_unswap_exists_prefixmatching) = S ((S (pfp_i_unswap_exists_prefixmatching)) * c)) /\ exists ff_q_pfp_unswap_exists_prefixmatchingsource. b = ff_q_pfp_unswap_exists_prefixmatchingsource * S ((S (pfp_i_unswap_exists_prefixmatching)) * c) + (pfp_a_unswap_exists_prefixmatching))) -> (((exists ff_h_pfp_unswap_exists_prefixmatchingtarget. ff_h_pfp_unswap_exists_prefixmatchingtarget + S (pfp_a_unswap_exists_prefixmatching) = S ((S (pfp_j_unswap_exists_prefixmatching)) * E)) /\ exists ff_q_pfp_unswap_exists_prefixmatchingtarget. D = ff_q_pfp_unswap_exists_prefixmatchingtarget * S ((S (pfp_j_unswap_exists_prefixmatching)) * E) + (pfp_a_unswap_exists_prefixmatching)))))) -> (((exists ff_h_pfp_unswap_exists_last. ff_h_pfp_unswap_exists_last + S (p) = S ((S (l)) * c)) /\ exists ff_q_pfp_unswap_exists_last. b = ff_q_pfp_unswap_exists_last * S ((S (l)) * c) + (p))) -> (((((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 U V. (((((forall pfp_i_unswap_exists_resultpermutationbounded. (exists pfp_gap_unswap_exists_resultpermutationboundedindex. pfp_gap_unswap_exists_resultpermutationboundedindex + S (pfp_i_unswap_exists_resultpermutationbounded) = (S l)) -> exists pfp_a_unswap_exists_resultpermutationbounded. (((exists ff_h_pfp_unswap_exists_resultpermutationboundedentry. ff_h_pfp_unswap_exists_resultpermutationboundedentry + S (pfp_a_unswap_exists_resultpermutationbounded) = S ((S (pfp_i_unswap_exists_resultpermutationbounded)) * V)) /\ exists ff_q_pfp_unswap_exists_resultpermutationboundedentry. U = ff_q_pfp_unswap_exists_resultpermutationboundedentry * S ((S (pfp_i_unswap_exists_resultpermutationbounded)) * V) + (pfp_a_unswap_exists_resultpermutationbounded))) /\ (exists pfp_gap_unswap_exists_resultpermutationboundedvalue. pfp_gap_unswap_exists_resultpermutationboundedvalue + S (pfp_a_unswap_exists_resultpermutationbounded) = (S l))) /\ (((forall pfp_i_unswap_exists_resultpermutationinjective pfp_j_unswap_exists_resultpermutationinjective pfp_a_unswap_exists_resultpermutationinjective. (exists pfp_gap_unswap_exists_resultpermutationinjectivefirst. pfp_gap_unswap_exists_resultpermutationinjectivefirst + S (pfp_i_unswap_exists_resultpermutationinjective) = (S l)) -> (exists pfp_gap_unswap_exists_resultpermutationinjectivesecond. pfp_gap_unswap_exists_resultpermutationinjectivesecond + S (pfp_j_unswap_exists_resultpermutationinjective) = (S l)) -> (((exists ff_h_pfp_unswap_exists_resultpermutationinjectiveleft. ff_h_pfp_unswap_exists_resultpermutationinjectiveleft + S (pfp_a_unswap_exists_resultpermutationinjective) = S ((S (pfp_i_unswap_exists_resultpermutationinjective)) * V)) /\ exists ff_q_pfp_unswap_exists_resultpermutationinjectiveleft. U = ff_q_pfp_unswap_exists_resultpermutationinjectiveleft * S ((S (pfp_i_unswap_exists_resultpermutationinjective)) * V) + (pfp_a_unswap_exists_resultpermutationinjective))) -> (((exists ff_h_pfp_unswap_exists_resultpermutationinjectiveright. ff_h_pfp_unswap_exists_resultpermutationinjectiveright + S (pfp_a_unswap_exists_resultpermutationinjective) = S ((S (pfp_j_unswap_exists_resultpermutationinjective)) * V)) /\ exists ff_q_pfp_unswap_exists_resultpermutationinjectiveright. U = ff_q_pfp_unswap_exists_resultpermutationinjectiveright * S ((S (pfp_j_unswap_exists_resultpermutationinjective)) * V) + (pfp_a_unswap_exists_resultpermutationinjective))) -> pfp_i_unswap_exists_resultpermutationinjective = pfp_j_unswap_exists_resultpermutationinjective) /\ (forall pfp_a_unswap_exists_resultpermutationsurjective. (exists pfp_gap_unswap_exists_resultpermutationsurjectivevalue. pfp_gap_unswap_exists_resultpermutationsurjectivevalue + S (pfp_a_unswap_exists_resultpermutationsurjective) = (S l)) -> exists pfp_i_unswap_exists_resultpermutationsurjective. (exists pfp_gap_unswap_exists_resultpermutationsurjectiveindex. pfp_gap_unswap_exists_resultpermutationsurjectiveindex + S (pfp_i_unswap_exists_resultpermutationsurjective) = (S l)) /\ (((exists ff_h_pfp_unswap_exists_resultpermutationsurjectiveentry. ff_h_pfp_unswap_exists_resultpermutationsurjectiveentry + S (pfp_a_unswap_exists_resultpermutationsurjective) = S ((S (pfp_i_unswap_exists_resultpermutationsurjective)) * V)) /\ exists ff_q_pfp_unswap_exists_resultpermutationsurjectiveentry. U = ff_q_pfp_unswap_exists_resultpermutationsurjectiveentry * S ((S (pfp_i_unswap_exists_resultpermutationsurjective)) * V) + (pfp_a_unswap_exists_resultpermutationsurjective)))))))) /\ (forall pfp_i_unswap_exists_resultmatching pfp_j_unswap_exists_resultmatching pfp_a_unswap_exists_resultmatching. (exists pfp_gap_unswap_exists_resultmatchingbound. pfp_gap_unswap_exists_resultmatchingbound + S (pfp_i_unswap_exists_resultmatching) = (S l)) -> (((exists ff_h_pfp_unswap_exists_resultmatchingmap. ff_h_pfp_unswap_exists_resultmatchingmap + S (pfp_j_unswap_exists_resultmatching) = S ((S (pfp_i_unswap_exists_resultmatching)) * V)) /\ exists ff_q_pfp_unswap_exists_resultmatchingmap. U = ff_q_pfp_unswap_exists_resultmatchingmap * S ((S (pfp_i_unswap_exists_resultmatching)) * V) + (pfp_j_unswap_exists_resultmatching))) -> (((exists ff_h_pfp_unswap_exists_resultmatchingsource. ff_h_pfp_unswap_exists_resultmatchingsource + S (pfp_a_unswap_exists_resultmatching) = S ((S (pfp_i_unswap_exists_resultmatching)) * c)) /\ exists ff_q_pfp_unswap_exists_resultmatchingsource. b = ff_q_pfp_unswap_exists_resultmatchingsource * S ((S (pfp_i_unswap_exists_resultmatching)) * c) + (pfp_a_unswap_exists_resultmatching))) -> (((exists ff_h_pfp_unswap_exists_resultmatchingtarget. ff_h_pfp_unswap_exists_resultmatchingtarget + S (pfp_a_unswap_exists_resultmatching) = S ((S (pfp_j_unswap_exists_resultmatching)) * e)) /\ exists ff_q_pfp_unswap_exists_resultmatchingtarget. d = ff_q_pfp_unswap_exists_resultmatchingtarget * S ((S (pfp_j_unswap_exists_resultmatching)) * e) + (pfp_a_unswap_exists_resultmatching))))))

Constructive proof overview

Generated structural guide

Use the recursively constructed finite permutation's actual preimage, construct both extended and transposed map codes, and return a full matching bijection into the original unswapped target list.

The unchanged tactic script uses 4 declared prerequisites and contains 117 exact native proof lines.

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

Proof neighborhood

Direct dependencies

AF0010 factor_permutation_matched_append beta_prefix_swap_last_from_entries Stable theorem; checked-use authorized AF0013 factor_permutation_swap_bijection AF0017 factor_permutation_matching_unswap

Direct dependents

AF0019 prime_factor_lists_matching_by_length

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

117 script commands · 29 reading checkpoints · 6 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (3)
factor permutation matched appendfactor permutation swap bijectionfactor permutation matching unswap

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 l
  10. L10
    intro j
02Fix variables and assumptionsL11–16

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

  1. L11
    intro p
  2. L12
    intro q
  3. L13
    intro hj
  4. L14
    intro hm
  5. L15
    intro hleft
  6. L16
    intro hs
03Establish hrightL17–17

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

  1. L17
    have hright : ((exists ff_h_pfp_unswap_exists_target_last. ff_h_pfp_unswap_exists_target_last + S (p) = S ((S (l)) * E)) /\ exists ff_q_pfp_unswap_exists_target_last. D = ff_q_pfp_unswap_exists_target_last * S ((S (l)) * E) + (p))
04Separate the logical casesL18–21

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

  1. L18
    cases hs
  2. L19
    cases hs_right
  3. L20
    cases hs_right_right
  4. L21
    cases hs_right_right_right
05Use earlier factsL22–22

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

  1. L22
    exact hs_right_right_right_left
06Establish hfullL23–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor permutation matched append.

  1. L23
    have hfull : ∃ U. ∃ V. PermutationPrefix(U,V,S l) ∧ FactorListMatching(b,c,D,E,U,V,S l) ∧ (BetaAt(U,V,l,l) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(u,v,x,y) → BetaAt(U,V,x,y)))Definitions: PermutationPrefixFactorListMatchingLtBetaAt
  2. L24
    specialize factor_permutation_matched_append (b)
  3. L25
    specialize factor_permutation_matched_append (c)
  4. L26
    specialize factor_permutation_matched_append (D)
  5. L27
    specialize factor_permutation_matched_append (E)
  6. L28
    specialize factor_permutation_matched_append (u)
  7. L29
    specialize factor_permutation_matched_append (v)
  8. L30
    specialize factor_permutation_matched_append (l)
  9. L31
    specialize factor_permutation_matched_append (p)
  10. L32
    apply factor_permutation_matched_append
07Use earlier factsL33–35

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

  1. L33
    exact hm
  2. L34
    exact hleft
  3. L35
    exact hright
08Separate the logical casesL36–43

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

  1. L36
    cases hfull
  2. L37
    cases hfull_witness
  3. L38
    cases hfull_witness_witness
  4. L39
    cases hfull_witness_witness_left
  5. L40
    cases hfull_witness_witness_right
  6. L41
    cases hm
  7. L42
    cases hm_left
  8. L43
    cases hm_left_right
09Establish hpreimageL44–47

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

  1. L44
    have hpreimage : exists i. (exists pfp_gap_unswap_preimage_bound. pfp_gap_unswap_preimage_bound + S (i) = (l)) /\ (((exists ff_h_pfp_unswap_preimage_entry. ff_h_pfp_unswap_preimage_entry + S (j) = S ((S (i)) * v)) /\ exists ff_q_pfp_unswap_preimage_entry. u = ff_q_pfp_unswap_preimage_entry * S ((S (i)) * v) + (j)))
  2. L45
    specialize hm_left_right_right (j)
  3. L46
    apply hm_left_right_right
  4. L47
    exact hj
10Separate the logical casesL48–49

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

  1. L48
    cases hpreimage
  2. L49
    cases hpreimage_witness
11Establish hmapiL50–55

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

  1. L50
    have hmapi : ((exists ff_h_pfp_unswap_full_image. ff_h_pfp_unswap_full_image + S (j) = S ((S (x2)) * x1)) /\ exists ff_q_pfp_unswap_full_image. x = ff_q_pfp_unswap_full_image * S ((S (x2)) * x1) + (j))
  2. L51
    specialize hfull_witness_witness_right_right (x2)
  3. L52
    specialize hfull_witness_witness_right_right (j)
  4. L53
    apply hfull_witness_witness_right_right
  5. L54
    exact hpreimage_witness_left
  6. L55
    exact hpreimage_witness_right
12Establish hmapnewL56–65

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

  1. L56
    have hmapnew : ∃ U. ∃ V. BetaAt(U,V,x2,l) ∧ (BetaAt(U,V,l,j) ∧ (∀ y. ∀ z. Lt(y,S l) → ¬y = x2 → ¬y = l → BetaAt(x,x1,y,z) → BetaAt(U,V,y,z)))Definitions: LtBetaAt
  2. L57
    specialize beta_prefix_swap_last_from_entries (x)
  3. L58
    specialize beta_prefix_swap_last_from_entries (x1)
  4. L59
    specialize beta_prefix_swap_last_from_entries (l)
  5. L60
    specialize beta_prefix_swap_last_from_entries (x2)
  6. L61
    specialize beta_prefix_swap_last_from_entries (j)
  7. L62
    specialize beta_prefix_swap_last_from_entries (l)
  8. L63
    apply beta_prefix_swap_last_from_entries
  9. L64
    exact hpreimage_witness_left
  10. L65
    exact hmapi
13Use earlier factsL66–66

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

  1. L66
    exact hfull_witness_witness_right_left
14Separate the logical casesL67–70

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

  1. L67
    cases hmapnew
  2. L68
    cases hmapnew_witness
  3. L69
    cases hmapnew_witness_witness
  4. L70
    cases hmapnew_witness_witness_right
15Establish hmapswapL71–71

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

  1. L71
    have hmapswap : BetaAt(x,x1,x2,j) ∧ (BetaAt(x,x1,l,l) ∧ (BetaAt(x3,x4,x2,l) ∧ (BetaAt(x3,x4,l,j) ∧ (∀ y. ∀ z. Lt(y,S l) → ¬y = x2 → ¬y = l → BetaAt(x,x1,y,z) → BetaAt(x3,x4,y,z)))))Definitions: LtBetaAt
16Separate the logical casesL72–72

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

  1. L72
    split
17Use earlier factsL73–73

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

  1. L73
    exact hmapi
18Separate the logical casesL74–74

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

  1. L74
    split
19Use earlier factsL75–75

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

  1. L75
    exact hfull_witness_witness_right_left
20Separate the logical casesL76–76

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

  1. L76
    split
21Use earlier factsL77–77

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

  1. L77
    exact hmapnew_witness_witness_left
22Separate the logical casesL78–78

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

  1. L78
    split
23Use earlier factsL79–80

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

  1. L79
    exact hmapnew_witness_witness_right_left
  2. L80
    exact hmapnew_witness_witness_right_right
24Construct an explicit witnessL81–82

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

  1. L81
    exists x3
  2. L82
    exists x4
25Separate the logical casesL83–83

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

  1. L83
    split
26Use earlier factsL84–93

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

  1. L84
    specialize factor_permutation_swap_bijection (x)
  2. L85
    specialize factor_permutation_swap_bijection (x1)
  3. L86
    specialize factor_permutation_swap_bijection (x3)
  4. L87
    specialize factor_permutation_swap_bijection (x4)
  5. L88
    specialize factor_permutation_swap_bijection (l)
  6. L89
    specialize factor_permutation_swap_bijection (x2)
  7. L90
    specialize factor_permutation_swap_bijection (j)
  8. L91
    specialize factor_permutation_swap_bijection (l)
  9. L92
    apply factor_permutation_swap_bijection
  10. L93
    exact hpreimage_witness_left
27Use earlier factsL94–103

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

  1. L94
    exact hfull_witness_witness_left_left
  2. L95
    exact hmapswap
  3. L96
    specialize factor_permutation_matching_unswap (b)
  4. L97
    specialize factor_permutation_matching_unswap (c)
  5. L98
    specialize factor_permutation_matching_unswap (d)
  6. L99
    specialize factor_permutation_matching_unswap (e)
  7. L100
    specialize factor_permutation_matching_unswap (D)
  8. L101
    specialize factor_permutation_matching_unswap (E)
  9. L102
    specialize factor_permutation_matching_unswap (x)
  10. L103
    specialize factor_permutation_matching_unswap (x1)
28Use earlier factsL104–113

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

  1. L104
    specialize factor_permutation_matching_unswap (x3)
  2. L105
    specialize factor_permutation_matching_unswap (x4)
  3. L106
    specialize factor_permutation_matching_unswap (l)
  4. L107
    specialize factor_permutation_matching_unswap (x2)
  5. L108
    specialize factor_permutation_matching_unswap (j)
  6. L109
    specialize factor_permutation_matching_unswap (p)
  7. L110
    specialize factor_permutation_matching_unswap (q)
  8. L111
    apply factor_permutation_matching_unswap
  9. L112
    exact hpreimage_witness_left
  10. L113
    exact hj
29Use earlier factsL114–117

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

  1. L114
    exact hfull_witness_witness_left_left
  2. L115
    exact hfull_witness_witness_left_right
  3. L116
    exact hs
  4. L117
    exact hmapswap

Library-wide reading audit

Original exact command ledger · 117 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 l
  10. 0010intro j
  11. 0011intro p
  12. 0012intro q
  13. 0013intro hj
  14. 0014intro hm
  15. 0015intro hleft
  16. 0016intro hs
  17. 0017have hright : ((exists ff_h_pfp_unswap_exists_target_last. ff_h_pfp_unswap_exists_target_last + S (p) = S ((S (l)) * E)) /\ exists ff_q_pfp_unswap_exists_target_last. D = ff_q_pfp_unswap_exists_target_last * S ((S (l)) * E) + (p))
  18. 0018cases hs
  19. 0019cases hs_right
  20. 0020cases hs_right_right
  21. 0021cases hs_right_right_right
  22. 0022exact hs_right_right_right_left
  23. 0023have hfull : exists U V. ((((((forall pfp_i_unswap_full_matchingpermutationbounded. (exists pfp_gap_unswap_full_matchingpermutationboundedindex. pfp_gap_unswap_full_matchingpermutationboundedindex + S (pfp_i_unswap_full_matchingpermutationbounded) = (S l)) -> exists pfp_a_unswap_full_matchingpermutationbounded. (((exists ff_h_pfp_unswap_full_matchingpermutationboundedentry. ff_h_pfp_unswap_full_matchingpermutationboundedentry + S (pfp_a_unswap_full_matchingpermutationbounded) = S ((S (pfp_i_unswap_full_matchingpermutationbounded)) * V)) /\ exists ff_q_pfp_unswap_full_matchingpermutationboundedentry. U = ff_q_pfp_unswap_full_matchingpermutationboundedentry * S ((S (pfp_i_unswap_full_matchingpermutationbounded)) * V) + (pfp_a_unswap_full_matchingpermutationbounded))) /\ (exists pfp_gap_unswap_full_matchingpermutationboundedvalue. pfp_gap_unswap_full_matchingpermutationboundedvalue + S (pfp_a_unswap_full_matchingpermutationbounded) = (S l))) /\ (((forall pfp_i_unswap_full_matchingpermutationinjective pfp_j_unswap_full_matchingpermutationinjective pfp_a_unswap_full_matchingpermutationinjective. (exists pfp_gap_unswap_full_matchingpermutationinjectivefirst. pfp_gap_unswap_full_matchingpermutationinjectivefirst + S (pfp_i_unswap_full_matchingpermutationinjective) = (S l)) -> (exists pfp_gap_unswap_full_matchingpermutationinjectivesecond. pfp_gap_unswap_full_matchingpermutationinjectivesecond + S (pfp_j_unswap_full_matchingpermutationinjective) = (S l)) -> (((exists ff_h_pfp_unswap_full_matchingpermutationinjectiveleft. ff_h_pfp_unswap_full_matchingpermutationinjectiveleft + S (pfp_a_unswap_full_matchingpermutationinjective) = S ((S (pfp_i_unswap_full_matchingpermutationinjective)) * V)) /\ exists ff_q_pfp_unswap_full_matchingpermutationinjectiveleft. U = ff_q_pfp_unswap_full_matchingpermutationinjectiveleft * S ((S (pfp_i_unswap_full_matchingpermutationinjective)) * V) + (pfp_a_unswap_full_matchingpermutationinjective))) -> (((exists ff_h_pfp_unswap_full_matchingpermutationinjectiveright. ff_h_pfp_unswap_full_matchingpermutationinjectiveright + S (pfp_a_unswap_full_matchingpermutationinjective) = S ((S (pfp_j_unswap_full_matchingpermutationinjective)) * V)) /\ exists ff_q_pfp_unswap_full_matchingpermutationinjectiveright. U = ff_q_pfp_unswap_full_matchingpermutationinjectiveright * S ((S (pfp_j_unswap_full_matchingpermutationinjective)) * V) + (pfp_a_unswap_full_matchingpermutationinjective))) -> pfp_i_unswap_full_matchingpermutationinjective = pfp_j_unswap_full_matchingpermutationinjective) /\ (forall pfp_a_unswap_full_matchingpermutationsurjective. (exists pfp_gap_unswap_full_matchingpermutationsurjectivevalue. pfp_gap_unswap_full_matchingpermutationsurjectivevalue + S (pfp_a_unswap_full_matchingpermutationsurjective) = (S l)) -> exists pfp_i_unswap_full_matchingpermutationsurjective. (exists pfp_gap_unswap_full_matchingpermutationsurjectiveindex. pfp_gap_unswap_full_matchingpermutationsurjectiveindex + S (pfp_i_unswap_full_matchingpermutationsurjective) = (S l)) /\ (((exists ff_h_pfp_unswap_full_matchingpermutationsurjectiveentry. ff_h_pfp_unswap_full_matchingpermutationsurjectiveentry + S (pfp_a_unswap_full_matchingpermutationsurjective) = S ((S (pfp_i_unswap_full_matchingpermutationsurjective)) * V)) /\ exists ff_q_pfp_unswap_full_matchingpermutationsurjectiveentry. U = ff_q_pfp_unswap_full_matchingpermutationsurjectiveentry * S ((S (pfp_i_unswap_full_matchingpermutationsurjective)) * V) + (pfp_a_unswap_full_matchingpermutationsurjective)))))))) /\ (forall pfp_i_unswap_full_matchingmatching pfp_j_unswap_full_matchingmatching pfp_a_unswap_full_matchingmatching. (exists pfp_gap_unswap_full_matchingmatchingbound. pfp_gap_unswap_full_matchingmatchingbound + S (pfp_i_unswap_full_matchingmatching) = (S l)) -> (((exists ff_h_pfp_unswap_full_matchingmatchingmap. ff_h_pfp_unswap_full_matchingmatchingmap + S (pfp_j_unswap_full_matchingmatching) = S ((S (pfp_i_unswap_full_matchingmatching)) * V)) /\ exists ff_q_pfp_unswap_full_matchingmatchingmap. U = ff_q_pfp_unswap_full_matchingmatchingmap * S ((S (pfp_i_unswap_full_matchingmatching)) * V) + (pfp_j_unswap_full_matchingmatching))) -> (((exists ff_h_pfp_unswap_full_matchingmatchingsource. ff_h_pfp_unswap_full_matchingmatchingsource + S (pfp_a_unswap_full_matchingmatching) = S ((S (pfp_i_unswap_full_matchingmatching)) * c)) /\ exists ff_q_pfp_unswap_full_matchingmatchingsource. b = ff_q_pfp_unswap_full_matchingmatchingsource * S ((S (pfp_i_unswap_full_matchingmatching)) * c) + (pfp_a_unswap_full_matchingmatching))) -> (((exists ff_h_pfp_unswap_full_matchingmatchingtarget. ff_h_pfp_unswap_full_matchingmatchingtarget + S (pfp_a_unswap_full_matchingmatching) = S ((S (pfp_j_unswap_full_matchingmatching)) * E)) /\ exists ff_q_pfp_unswap_full_matchingmatchingtarget. D = ff_q_pfp_unswap_full_matchingmatchingtarget * S ((S (pfp_j_unswap_full_matchingmatching)) * E) + (pfp_a_unswap_full_matchingmatching)))))) /\ (((((exists ff_h_pfp_unswap_full_extensionlast. ff_h_pfp_unswap_full_extensionlast + S (l) = S ((S (l)) * V)) /\ exists ff_q_pfp_unswap_full_extensionlast. U = ff_q_pfp_unswap_full_extensionlast * S ((S (l)) * V) + (l))) /\ (forall pfp_i_unswap_full_extensionprefix pfp_a_unswap_full_extensionprefix. (exists pfp_gap_unswap_full_extensionprefixbound. pfp_gap_unswap_full_extensionprefixbound + S (pfp_i_unswap_full_extensionprefix) = (l)) -> (((exists ff_h_pfp_unswap_full_extensionprefixold. ff_h_pfp_unswap_full_extensionprefixold + S (pfp_a_unswap_full_extensionprefix) = S ((S (pfp_i_unswap_full_extensionprefix)) * v)) /\ exists ff_q_pfp_unswap_full_extensionprefixold. u = ff_q_pfp_unswap_full_extensionprefixold * S ((S (pfp_i_unswap_full_extensionprefix)) * v) + (pfp_a_unswap_full_extensionprefix))) -> (((exists ff_h_pfp_unswap_full_extensionprefixnew. ff_h_pfp_unswap_full_extensionprefixnew + S (pfp_a_unswap_full_extensionprefix) = S ((S (pfp_i_unswap_full_extensionprefix)) * V)) /\ exists ff_q_pfp_unswap_full_extensionprefixnew. U = ff_q_pfp_unswap_full_extensionprefixnew * S ((S (pfp_i_unswap_full_extensionprefix)) * V) + (pfp_a_unswap_full_extensionprefix)))))))
  24. 0024specialize factor_permutation_matched_append (b)
  25. 0025specialize factor_permutation_matched_append (c)
  26. 0026specialize factor_permutation_matched_append (D)
  27. 0027specialize factor_permutation_matched_append (E)
  28. 0028specialize factor_permutation_matched_append (u)
  29. 0029specialize factor_permutation_matched_append (v)
  30. 0030specialize factor_permutation_matched_append (l)
  31. 0031specialize factor_permutation_matched_append (p)
  32. 0032apply factor_permutation_matched_append
  33. 0033exact hm
  34. 0034exact hleft
  35. 0035exact hright
  36. 0036cases hfull
  37. 0037cases hfull_witness
  38. 0038cases hfull_witness_witness
  39. 0039cases hfull_witness_witness_left
  40. 0040cases hfull_witness_witness_right
  41. 0041cases hm
  42. 0042cases hm_left
  43. 0043cases hm_left_right
  44. 0044have hpreimage : exists i. (exists pfp_gap_unswap_preimage_bound. pfp_gap_unswap_preimage_bound + S (i) = (l)) /\ (((exists ff_h_pfp_unswap_preimage_entry. ff_h_pfp_unswap_preimage_entry + S (j) = S ((S (i)) * v)) /\ exists ff_q_pfp_unswap_preimage_entry. u = ff_q_pfp_unswap_preimage_entry * S ((S (i)) * v) + (j)))
  45. 0045specialize hm_left_right_right (j)
  46. 0046apply hm_left_right_right
  47. 0047exact hj
  48. 0048cases hpreimage
  49. 0049cases hpreimage_witness
  50. 0050have hmapi : ((exists ff_h_pfp_unswap_full_image. ff_h_pfp_unswap_full_image + S (j) = S ((S (x2)) * x1)) /\ exists ff_q_pfp_unswap_full_image. x = ff_q_pfp_unswap_full_image * S ((S (x2)) * x1) + (j))
  51. 0051specialize hfull_witness_witness_right_right (x2)
  52. 0052specialize hfull_witness_witness_right_right (j)
  53. 0053apply hfull_witness_witness_right_right
  54. 0054exact hpreimage_witness_left
  55. 0055exact hpreimage_witness_right
  56. 0056have hmapnew : exists U V. ((((exists ff_h_pfp_unswap_map_new_selected. ff_h_pfp_unswap_map_new_selected + S (l) = S ((S (x2)) * V)) /\ exists ff_q_pfp_unswap_map_new_selected. U = ff_q_pfp_unswap_map_new_selected * S ((S (x2)) * V) + (l))) /\ (((((exists ff_h_pfp_unswap_map_new_last. ff_h_pfp_unswap_map_new_last + S (j) = S ((S (l)) * V)) /\ exists ff_q_pfp_unswap_map_new_last. U = ff_q_pfp_unswap_map_new_last * S ((S (l)) * V) + (j))) /\ (forall k a. (exists pfp_gap_unswap_map_preserve_bound. pfp_gap_unswap_map_preserve_bound + S (k) = (S l)) -> ~(k = x2) -> ~(k = l) -> (((exists ff_h_pfp_unswap_map_preserve_old. ff_h_pfp_unswap_map_preserve_old + S (a) = S ((S (k)) * x1)) /\ exists ff_q_pfp_unswap_map_preserve_old. x = ff_q_pfp_unswap_map_preserve_old * S ((S (k)) * x1) + (a))) -> (((exists ff_h_pfp_unswap_map_preserve_new. ff_h_pfp_unswap_map_preserve_new + S (a) = S ((S (k)) * V)) /\ exists ff_q_pfp_unswap_map_preserve_new. U = ff_q_pfp_unswap_map_preserve_new * S ((S (k)) * V) + (a)))))))
  57. 0057specialize beta_prefix_swap_last_from_entries (x)
  58. 0058specialize beta_prefix_swap_last_from_entries (x1)
  59. 0059specialize beta_prefix_swap_last_from_entries (l)
  60. 0060specialize beta_prefix_swap_last_from_entries (x2)
  61. 0061specialize beta_prefix_swap_last_from_entries (j)
  62. 0062specialize beta_prefix_swap_last_from_entries (l)
  63. 0063apply beta_prefix_swap_last_from_entries
  64. 0064exact hpreimage_witness_left
  65. 0065exact hmapi
  66. 0066exact hfull_witness_witness_right_left
  67. 0067cases hmapnew
  68. 0068cases hmapnew_witness
  69. 0069cases hmapnew_witness_witness
  70. 0070cases hmapnew_witness_witness_right
  71. 0071have hmapswap : ((((exists ff_h_pfp_unswap_actual_mapoldi. ff_h_pfp_unswap_actual_mapoldi + S (j) = S ((S (x2)) * x1)) /\ exists ff_q_pfp_unswap_actual_mapoldi. x = ff_q_pfp_unswap_actual_mapoldi * S ((S (x2)) * x1) + (j))) /\ (((((exists ff_h_pfp_unswap_actual_mapoldlast. ff_h_pfp_unswap_actual_mapoldlast + S (l) = S ((S (l)) * x1)) /\ exists ff_q_pfp_unswap_actual_mapoldlast. x = ff_q_pfp_unswap_actual_mapoldlast * S ((S (l)) * x1) + (l))) /\ (((((exists ff_h_pfp_unswap_actual_mapnewi. ff_h_pfp_unswap_actual_mapnewi + S (l) = S ((S (x2)) * x4)) /\ exists ff_q_pfp_unswap_actual_mapnewi. x3 = ff_q_pfp_unswap_actual_mapnewi * S ((S (x2)) * x4) + (l))) /\ (((((exists ff_h_pfp_unswap_actual_mapnewlast. ff_h_pfp_unswap_actual_mapnewlast + S (j) = S ((S (l)) * x4)) /\ exists ff_q_pfp_unswap_actual_mapnewlast. x3 = ff_q_pfp_unswap_actual_mapnewlast * S ((S (l)) * x4) + (j))) /\ (forall pfp_j_unswap_actual_map pfp_a_unswap_actual_map. (exists pfp_gap_unswap_actual_mapbound. pfp_gap_unswap_actual_mapbound + S (pfp_j_unswap_actual_map) = (S (l))) -> ~(pfp_j_unswap_actual_map = x2) -> ~(pfp_j_unswap_actual_map = l) -> (((exists ff_h_pfp_unswap_actual_mapold. ff_h_pfp_unswap_actual_mapold + S (pfp_a_unswap_actual_map) = S ((S (pfp_j_unswap_actual_map)) * x1)) /\ exists ff_q_pfp_unswap_actual_mapold. x = ff_q_pfp_unswap_actual_mapold * S ((S (pfp_j_unswap_actual_map)) * x1) + (pfp_a_unswap_actual_map))) -> (((exists ff_h_pfp_unswap_actual_mapnew. ff_h_pfp_unswap_actual_mapnew + S (pfp_a_unswap_actual_map) = S ((S (pfp_j_unswap_actual_map)) * x4)) /\ exists ff_q_pfp_unswap_actual_mapnew. x3 = ff_q_pfp_unswap_actual_mapnew * S ((S (pfp_j_unswap_actual_map)) * x4) + (pfp_a_unswap_actual_map)))))))))))
  72. 0072split
  73. 0073exact hmapi
  74. 0074split
  75. 0075exact hfull_witness_witness_right_left
  76. 0076split
  77. 0077exact hmapnew_witness_witness_left
  78. 0078split
  79. 0079exact hmapnew_witness_witness_right_left
  80. 0080exact hmapnew_witness_witness_right_right
  81. 0081exists x3
  82. 0082exists x4
  83. 0083split
  84. 0084specialize factor_permutation_swap_bijection (x)
  85. 0085specialize factor_permutation_swap_bijection (x1)
  86. 0086specialize factor_permutation_swap_bijection (x3)
  87. 0087specialize factor_permutation_swap_bijection (x4)
  88. 0088specialize factor_permutation_swap_bijection (l)
  89. 0089specialize factor_permutation_swap_bijection (x2)
  90. 0090specialize factor_permutation_swap_bijection (j)
  91. 0091specialize factor_permutation_swap_bijection (l)
  92. 0092apply factor_permutation_swap_bijection
  93. 0093exact hpreimage_witness_left
  94. 0094exact hfull_witness_witness_left_left
  95. 0095exact hmapswap
  96. 0096specialize factor_permutation_matching_unswap (b)
  97. 0097specialize factor_permutation_matching_unswap (c)
  98. 0098specialize factor_permutation_matching_unswap (d)
  99. 0099specialize factor_permutation_matching_unswap (e)
  100. 0100specialize factor_permutation_matching_unswap (D)
  101. 0101specialize factor_permutation_matching_unswap (E)
  102. 0102specialize factor_permutation_matching_unswap (x)
  103. 0103specialize factor_permutation_matching_unswap (x1)
  104. 0104specialize factor_permutation_matching_unswap (x3)
  105. 0105specialize factor_permutation_matching_unswap (x4)
  106. 0106specialize factor_permutation_matching_unswap (l)
  107. 0107specialize factor_permutation_matching_unswap (x2)
  108. 0108specialize factor_permutation_matching_unswap (j)
  109. 0109specialize factor_permutation_matching_unswap (p)
  110. 0110specialize factor_permutation_matching_unswap (q)
  111. 0111apply factor_permutation_matching_unswap
  112. 0112exact hpreimage_witness_left
  113. 0113exact hj
  114. 0114exact hfull_witness_witness_left_left
  115. 0115exact hfull_witness_witness_left_right
  116. 0116exact hs
  117. 0117exact hmapswap