Metamath Proof Explorer

Theorem pfxlsw2ccat

Description: Reconstruct a word from its prefix and its last two symbols. (Contributed by Thierry Arnoux, 26-Sep-2023)

Ref Expression
Hypothesis pfxlsw2ccat.n ⊢ 𝑁 = ( ♯ ‘ 𝑊 )
Assertion pfxlsw2ccat ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → 𝑊 = ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ⟨“ ( 𝑊 ‘ ( 𝑁 − 2 ) ) ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ ) )

Proof

Step Hyp Ref Expression
1 pfxlsw2ccat.n ⊢ 𝑁 = ( ♯ ‘ 𝑊 )
2 simpl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → 𝑊 ∈ Word 𝑉 )
3 simpr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → 2 ≤ 𝑁 )
4 3 1 breqtrdi ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → 2 ≤ ( ♯ ‘ 𝑊 ) )
5 wrdlenge2n0 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 𝑊 ≠ ∅ )
6 2 4 5 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → 𝑊 ≠ ∅ )
7 pfxlswccat ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑊 ) ”⟩ ) = 𝑊 )
8 2 6 7 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑊 ) ”⟩ ) = 𝑊 )
9 lsw ⊢ ( 𝑊 ∈ Word 𝑉 → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
10 1 oveq1i ⊢ ( 𝑁 − 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 )
11 10 fveq2i ⊢ ( 𝑊 ‘ ( 𝑁 − 1 ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) )
12 9 11 eqtr4di ⊢ ( 𝑊 ∈ Word 𝑉 → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( 𝑁 − 1 ) ) )
13 2 12 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( 𝑁 − 1 ) ) )
14 13 s1eqd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ⟨“ ( lastS ‘ 𝑊 ) ”⟩ = ⟨“ ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ )
15 14 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑊 ) ”⟩ ) = ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ++ ⟨“ ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ ) )
16 8 15 eqtr3d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → 𝑊 = ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ++ ⟨“ ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ ) )
17 pfxcl ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ Word 𝑉 )
18 2 17 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ Word 𝑉 )
19 lencl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
20 2 19 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
21 1 20 eqeltrid ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → 𝑁 ∈ ℕ0 )
22 nn0ge2m1nn ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁 ) → ( 𝑁 − 1 ) ∈ ℕ )
23 21 3 22 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( 𝑁 − 1 ) ∈ ℕ )
24 10 23 eqeltrrid ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ )
25 20 nn0red ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ♯ ‘ 𝑊 ) ∈ ℝ )
26 25 lem1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ≤ ( ♯ ‘ 𝑊 ) )
27 pfxn0 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ≠ ∅ )
28 2 24 26 27 syl3anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ≠ ∅ )
29 pfxlswccat ⊢ ( ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∈ Word 𝑉 ∧ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ≠ ∅ ) → ( ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) prefix ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) ++ ⟨“ ( lastS ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) ”⟩ ) = ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
30 18 28 29 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) prefix ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) ++ ⟨“ ( lastS ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) ”⟩ ) = ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
31 ige2m1fz ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
32 20 4 31 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
33 pfxlen ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
34 2 32 33 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
35 34 oveq1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) = ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) )
36 0zd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → 0 ∈ ℤ )
37 nn0ge2m1nn0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁 ) → ( 𝑁 − 1 ) ∈ ℕ0 )
38 21 3 37 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( 𝑁 − 1 ) ∈ ℕ0 )
39 10 38 eqeltrrid ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℕ0 )
40 39 nn0zd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℤ )
41 1zzd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → 1 ∈ ℤ )
42 40 41 zsubcld ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ∈ ℤ )
43 2nn0 ⊢ 2 ∈ ℕ0
44 43 a1i ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → 2 ∈ ℕ0 )
45 nn0sub ⊢ ( ( 2 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 2 ≤ 𝑁 ↔ ( 𝑁 − 2 ) ∈ ℕ0 ) )
46 45 biimpa ⊢ ( ( ( 2 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 2 ≤ 𝑁 ) → ( 𝑁 − 2 ) ∈ ℕ0 )
47 44 21 3 46 syl21anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( 𝑁 − 2 ) ∈ ℕ0 )
48 47 nn0ge0d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → 0 ≤ ( 𝑁 − 2 ) )
49 21 nn0cnd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → 𝑁 ∈ ℂ )
50 sub1m1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) − 1 ) = ( 𝑁 − 2 ) )
51 49 50 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( 𝑁 − 1 ) − 1 ) = ( 𝑁 − 2 ) )
52 48 51 breqtrrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → 0 ≤ ( ( 𝑁 − 1 ) − 1 ) )
53 10 oveq1i ⊢ ( ( 𝑁 − 1 ) − 1 ) = ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 )
54 52 53 breqtrdi ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → 0 ≤ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) )
55 24 nnred ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℝ )
56 55 lem1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ≤ ( ( ♯ ‘ 𝑊 ) − 1 ) )
57 36 40 42 54 56 elfzd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 1 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
58 35 57 eqeltrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
59 pfxpfx ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) prefix ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) = ( 𝑊 prefix ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) )
60 2 32 58 59 syl3anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) prefix ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) = ( 𝑊 prefix ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) )
61 34 10 eqtr4di ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ( 𝑁 − 1 ) )
62 61 oveq1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) = ( ( 𝑁 − 1 ) − 1 ) )
63 62 51 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) = ( 𝑁 − 2 ) )
64 63 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( 𝑊 prefix ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) = ( 𝑊 prefix ( 𝑁 − 2 ) ) )
65 60 64 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) prefix ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) = ( 𝑊 prefix ( 𝑁 − 2 ) ) )
66 pfxtrcfvl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( lastS ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) )
67 2 4 66 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( lastS ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) )
68 1 a1i ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → 𝑁 = ( ♯ ‘ 𝑊 ) )
69 68 fvoveq1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 2 ) ) )
70 67 69 eqtr4d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( lastS ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ( 𝑊 ‘ ( 𝑁 − 2 ) ) )
71 70 s1eqd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ⟨“ ( lastS ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) ”⟩ = ⟨“ ( 𝑊 ‘ ( 𝑁 − 2 ) ) ”⟩ )
72 65 71 oveq12d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) prefix ( ( ♯ ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) − 1 ) ) ++ ⟨“ ( lastS ‘ ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) ”⟩ ) = ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ⟨“ ( 𝑊 ‘ ( 𝑁 − 2 ) ) ”⟩ ) )
73 30 72 eqtr3d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ⟨“ ( 𝑊 ‘ ( 𝑁 − 2 ) ) ”⟩ ) )
74 73 oveq1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ++ ⟨“ ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ ) = ( ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ⟨“ ( 𝑊 ‘ ( 𝑁 − 2 ) ) ”⟩ ) ++ ⟨“ ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ ) )
75 pfxcl ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix ( 𝑁 − 2 ) ) ∈ Word 𝑉 )
76 2 75 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( 𝑊 prefix ( 𝑁 − 2 ) ) ∈ Word 𝑉 )
77 ccatw2s1ccatws2 ⊢ ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ∈ Word 𝑉 → ( ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ⟨“ ( 𝑊 ‘ ( 𝑁 − 2 ) ) ”⟩ ) ++ ⟨“ ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ ) = ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ⟨“ ( 𝑊 ‘ ( 𝑁 − 2 ) ) ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ ) )
78 76 77 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → ( ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ⟨“ ( 𝑊 ‘ ( 𝑁 − 2 ) ) ”⟩ ) ++ ⟨“ ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ ) = ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ⟨“ ( 𝑊 ‘ ( 𝑁 − 2 ) ) ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ ) )
79 16 74 78 3eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → 𝑊 = ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ⟨“ ( 𝑊 ‘ ( 𝑁 − 2 ) ) ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ ) )