efgredleme

Description: Lemma for efgred . (Contributed by Mario Carneiro, 1-Oct-2015) (Proof shortened by AV, 15-Oct-2022)

	Ref	Expression
Hypotheses	efgval.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
	efgval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
	efgval2.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
	efgval2.t	$⊢ T = (v \in W ⟼ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩))$
	efgred.d	$⊢ D = W ∖ ⋃_{x \in W} ran T (x)$
	efgred.s	$⊢ S = (m \in \{t \in (Word W ∖ \{\emptyset\}) \| (t (0) \in D \land \forall k \in (1 ..^\|t\|) t (k) \in ran T (t (k - 1)))\} ⟼ m (\|m\| - 1))$
	efgredlem.1	$⊢ φ \to \forall a \in dom S \forall b \in dom S (\|S (a)\| < \|S (A)\| \to (S (a) = S (b) \to a (0) = b (0)))$
	efgredlem.2	$⊢ φ \to A \in dom S$
	efgredlem.3	$⊢ φ \to B \in dom S$
	efgredlem.4	$⊢ φ \to S (A) = S (B)$
	efgredlem.5	$⊢ φ \to \neg A (0) = B (0)$
	efgredlemb.k	$⊢ K = \|A\| - 1 - 1$
	efgredlemb.l	$⊢ L = \|B\| - 1 - 1$
	efgredlemb.p	$⊢ φ \to P \in (0 \dots \|A (K)\|)$
	efgredlemb.q	$⊢ φ \to Q \in (0 \dots \|B (L)\|)$
	efgredlemb.u	$⊢ φ \to U \in (I \times 2_{𝑜})$
	efgredlemb.v	$⊢ φ \to V \in (I \times 2_{𝑜})$
	efgredlemb.6	$⊢ φ \to S (A) = P T (A (K)) U$
	efgredlemb.7	$⊢ φ \to S (B) = Q T (B (L)) V$
	efgredlemb.8	$⊢ φ \to \neg A (K) = B (L)$
	efgredlemd.9	$⊢ φ \to P \in ℤ_{\geq (Q + 2)}$
	efgredlemd.c	$⊢ φ \to C \in dom S$
	efgredlemd.sc	$⊢ φ \to S (C) = (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩)$
Assertion	efgredleme	$⊢ φ \to (A (K) \in ran T (S (C)) \land B (L) \in ran T (S (C)))$

Proof

Step	Hyp	Ref	Expression
1		efgval.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
2		efgval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
3		efgval2.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
4		efgval2.t	$⊢ T = (v \in W ⟼ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩))$
5		efgred.d	$⊢ D = W ∖ ⋃_{x \in W} ran T (x)$
6		efgred.s	$⊢ S = (m \in \{t \in (Word W ∖ \{\emptyset\}) \| (t (0) \in D \land \forall k \in (1 ..^\|t\|) t (k) \in ran T (t (k - 1)))\} ⟼ m (\|m\| - 1))$
7		efgredlem.1	$⊢ φ \to \forall a \in dom S \forall b \in dom S (\|S (a)\| < \|S (A)\| \to (S (a) = S (b) \to a (0) = b (0)))$
8		efgredlem.2	$⊢ φ \to A \in dom S$
9		efgredlem.3	$⊢ φ \to B \in dom S$
10		efgredlem.4	$⊢ φ \to S (A) = S (B)$
11		efgredlem.5	$⊢ φ \to \neg A (0) = B (0)$
12		efgredlemb.k	$⊢ K = \|A\| - 1 - 1$
13		efgredlemb.l	$⊢ L = \|B\| - 1 - 1$
14		efgredlemb.p	$⊢ φ \to P \in (0 \dots \|A (K)\|)$
15		efgredlemb.q	$⊢ φ \to Q \in (0 \dots \|B (L)\|)$
16		efgredlemb.u	$⊢ φ \to U \in (I \times 2_{𝑜})$
17		efgredlemb.v	$⊢ φ \to V \in (I \times 2_{𝑜})$
18		efgredlemb.6	$⊢ φ \to S (A) = P T (A (K)) U$
19		efgredlemb.7	$⊢ φ \to S (B) = Q T (B (L)) V$
20		efgredlemb.8	$⊢ φ \to \neg A (K) = B (L)$
21		efgredlemd.9	$⊢ φ \to P \in ℤ_{\geq (Q + 2)}$
22		efgredlemd.c	$⊢ φ \to C \in dom S$
23		efgredlemd.sc	$⊢ φ \to S (C) = (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩)$
24	1 2 3 4 5 6	efgsf	$⊢ S : \{t \in (Word W ∖ \{\emptyset\}) \| (t (0) \in D \land \forall k \in (1 ..^\|t\|) t (k) \in ran T (t (k - 1)))\} ⟶ W$
25	24	fdmi	$⊢ dom S = \{t \in (Word W ∖ \{\emptyset\}) \| (t (0) \in D \land \forall k \in (1 ..^\|t\|) t (k) \in ran T (t (k - 1)))\}$
26	25	feq2i	$⊢ S : dom S ⟶ W \leftrightarrow S : \{t \in (Word W ∖ \{\emptyset\}) \| (t (0) \in D \land \forall k \in (1 ..^\|t\|) t (k) \in ran T (t (k - 1)))\} ⟶ W$
27	24 26	mpbir	$⊢ S : dom S ⟶ W$
28	27	ffvelrni	$⊢ C \in dom S \to S (C) \in W$
29	22 28	syl	$⊢ φ \to S (C) \in W$
30		elfzuz	$⊢ Q \in (0 \dots \|B (L)\|) \to Q \in ℤ_{\geq 0}$
31	15 30	syl	$⊢ φ \to Q \in ℤ_{\geq 0}$
32	23	fveq2d	$⊢ φ \to \|S (C)\| = \|(B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩)\|$
33		fviss	$⊢ I (Word (I \times 2_{𝑜})) \subseteq Word (I \times 2_{𝑜})$
34	1 33	eqsstri	$⊢ W \subseteq Word (I \times 2_{𝑜})$
35	1 2 3 4 5 6 7 8 9 10 11 12 13	efgredlemf	$⊢ φ \to (A (K) \in W \land B (L) \in W)$
36	35	simprd	$⊢ φ \to B (L) \in W$
37	34 36	sselid	$⊢ φ \to B (L) \in Word (I \times 2_{𝑜})$
38		pfxcl	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to B (L) prefix Q \in Word (I \times 2_{𝑜})$
39	37 38	syl	$⊢ φ \to B (L) prefix Q \in Word (I \times 2_{𝑜})$
40	35	simpld	$⊢ φ \to A (K) \in W$
41	34 40	sselid	$⊢ φ \to A (K) \in Word (I \times 2_{𝑜})$
42		swrdcl	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to A (K) substr ⟨Q + 2, \|A (K)\|⟩ \in Word (I \times 2_{𝑜})$
43	41 42	syl	$⊢ φ \to A (K) substr ⟨Q + 2, \|A (K)\|⟩ \in Word (I \times 2_{𝑜})$
44		ccatlen	$⊢ (B (L) prefix Q \in Word (I \times 2_{𝑜}) \land A (K) substr ⟨Q + 2, \|A (K)\|⟩ \in Word (I \times 2_{𝑜})) \to \|(B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩)\| = \|B (L) prefix Q\| + \|A (K) substr ⟨Q + 2, \|A (K)\|⟩\|$
45	39 43 44	syl2anc	$⊢ φ \to \|(B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩)\| = \|B (L) prefix Q\| + \|A (K) substr ⟨Q + 2, \|A (K)\|⟩\|$
46		pfxlen	$⊢ (B (L) \in Word (I \times 2_{𝑜}) \land Q \in (0 \dots \|B (L)\|)) \to \|B (L) prefix Q\| = Q$
47	37 15 46	syl2anc	$⊢ φ \to \|B (L) prefix Q\| = Q$
48		2nn0	$⊢ 2 \in ℕ_{0}$
49		uzaddcl	$⊢ (Q \in ℤ_{\geq 0} \land 2 \in ℕ_{0}) \to Q + 2 \in ℤ_{\geq 0}$
50	31 48 49	sylancl	$⊢ φ \to Q + 2 \in ℤ_{\geq 0}$
51		elfzuz3	$⊢ P \in (0 \dots \|A (K)\|) \to \|A (K)\| \in ℤ_{\geq P}$
52	14 51	syl	$⊢ φ \to \|A (K)\| \in ℤ_{\geq P}$
53		uztrn	$⊢ (\|A (K)\| \in ℤ_{\geq P} \land P \in ℤ_{\geq (Q + 2)}) \to \|A (K)\| \in ℤ_{\geq (Q + 2)}$
54	52 21 53	syl2anc	$⊢ φ \to \|A (K)\| \in ℤ_{\geq (Q + 2)}$
55		elfzuzb	$⊢ Q + 2 \in (0 \dots \|A (K)\|) \leftrightarrow (Q + 2 \in ℤ_{\geq 0} \land \|A (K)\| \in ℤ_{\geq (Q + 2)})$
56	50 54 55	sylanbrc	$⊢ φ \to Q + 2 \in (0 \dots \|A (K)\|)$
57		lencl	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to \|A (K)\| \in ℕ_{0}$
58	41 57	syl	$⊢ φ \to \|A (K)\| \in ℕ_{0}$
59		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
60	58 59	eleqtrdi	$⊢ φ \to \|A (K)\| \in ℤ_{\geq 0}$
61		eluzfz2	$⊢ \|A (K)\| \in ℤ_{\geq 0} \to \|A (K)\| \in (0 \dots \|A (K)\|)$
62	60 61	syl	$⊢ φ \to \|A (K)\| \in (0 \dots \|A (K)\|)$
63		swrdlen	$⊢ (A (K) \in Word (I \times 2_{𝑜}) \land Q + 2 \in (0 \dots \|A (K)\|) \land \|A (K)\| \in (0 \dots \|A (K)\|)) \to \|A (K) substr ⟨Q + 2, \|A (K)\|⟩\| = \|A (K)\| - (Q + 2)$
64	41 56 62 63	syl3anc	$⊢ φ \to \|A (K) substr ⟨Q + 2, \|A (K)\|⟩\| = \|A (K)\| - (Q + 2)$
65	47 64	oveq12d	$⊢ φ \to \|B (L) prefix Q\| + \|A (K) substr ⟨Q + 2, \|A (K)\|⟩\| = Q + \|A (K)\| - (Q + 2)$
66	15	elfzelzd	$⊢ φ \to Q \in ℤ$
67	66	zcnd	$⊢ φ \to Q \in ℂ$
68	58	nn0cnd	$⊢ φ \to \|A (K)\| \in ℂ$
69		2z	$⊢ 2 \in ℤ$
70		zaddcl	$⊢ (Q \in ℤ \land 2 \in ℤ) \to Q + 2 \in ℤ$
71	66 69 70	sylancl	$⊢ φ \to Q + 2 \in ℤ$
72	71	zcnd	$⊢ φ \to Q + 2 \in ℂ$
73	67 68 72	addsubassd	$⊢ φ \to Q + \|A (K)\| - (Q + 2) = Q + \|A (K)\| - (Q + 2)$
74		2cn	$⊢ 2 \in ℂ$
75	74	a1i	$⊢ φ \to 2 \in ℂ$
76	67 68 75	pnpcand	$⊢ φ \to Q + \|A (K)\| - (Q + 2) = \|A (K)\| - 2$
77	65 73 76	3eqtr2d	$⊢ φ \to \|B (L) prefix Q\| + \|A (K) substr ⟨Q + 2, \|A (K)\|⟩\| = \|A (K)\| - 2$
78	32 45 77	3eqtrd	$⊢ φ \to \|S (C)\| = \|A (K)\| - 2$
79	14	elfzelzd	$⊢ φ \to P \in ℤ$
80		zsubcl	$⊢ (P \in ℤ \land 2 \in ℤ) \to P - 2 \in ℤ$
81	79 69 80	sylancl	$⊢ φ \to P - 2 \in ℤ$
82	69	a1i	$⊢ φ \to 2 \in ℤ$
83	79	zcnd	$⊢ φ \to P \in ℂ$
84		npcan	$⊢ (P \in ℂ \land 2 \in ℂ) \to P - 2 + 2 = P$
85	83 74 84	sylancl	$⊢ φ \to P - 2 + 2 = P$
86	85	fveq2d	$⊢ φ \to ℤ_{\geq (P - 2 + 2)} = ℤ_{\geq P}$
87	52 86	eleqtrrd	$⊢ φ \to \|A (K)\| \in ℤ_{\geq (P - 2 + 2)}$
88		eluzsub	$⊢ (P - 2 \in ℤ \land 2 \in ℤ \land \|A (K)\| \in ℤ_{\geq (P - 2 + 2)}) \to \|A (K)\| - 2 \in ℤ_{\geq (P - 2)}$
89	81 82 87 88	syl3anc	$⊢ φ \to \|A (K)\| - 2 \in ℤ_{\geq (P - 2)}$
90	78 89	eqeltrd	$⊢ φ \to \|S (C)\| \in ℤ_{\geq (P - 2)}$
91		eluzsub	$⊢ (Q \in ℤ \land 2 \in ℤ \land P \in ℤ_{\geq (Q + 2)}) \to P - 2 \in ℤ_{\geq Q}$
92	66 82 21 91	syl3anc	$⊢ φ \to P - 2 \in ℤ_{\geq Q}$
93		uztrn	$⊢ (\|S (C)\| \in ℤ_{\geq (P - 2)} \land P - 2 \in ℤ_{\geq Q}) \to \|S (C)\| \in ℤ_{\geq Q}$
94	90 92 93	syl2anc	$⊢ φ \to \|S (C)\| \in ℤ_{\geq Q}$
95		elfzuzb	$⊢ Q \in (0 \dots \|S (C)\|) \leftrightarrow (Q \in ℤ_{\geq 0} \land \|S (C)\| \in ℤ_{\geq Q})$
96	31 94 95	sylanbrc	$⊢ φ \to Q \in (0 \dots \|S (C)\|)$
97	1 2 3 4	efgtval	$⊢ (S (C) \in W \land Q \in (0 \dots \|S (C)\|) \land V \in (I \times 2_{𝑜})) \to Q T (S (C)) V = S (C) splice ⟨Q, Q, ⟨“ V M (V) ”⟩⟩$
98	29 96 17 97	syl3anc	$⊢ φ \to Q T (S (C)) V = S (C) splice ⟨Q, Q, ⟨“ V M (V) ”⟩⟩$
99		pfxcl	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to A (K) prefix Q \in Word (I \times 2_{𝑜})$
100	41 99	syl	$⊢ φ \to A (K) prefix Q \in Word (I \times 2_{𝑜})$
101		wrd0	$⊢ \emptyset \in Word (I \times 2_{𝑜})$
102	101	a1i	$⊢ φ \to \emptyset \in Word (I \times 2_{𝑜})$
103	3	efgmf	$⊢ M : I \times 2_{𝑜} ⟶ I \times 2_{𝑜}$
104	103	ffvelrni	$⊢ V \in (I \times 2_{𝑜}) \to M (V) \in (I \times 2_{𝑜})$
105	17 104	syl	$⊢ φ \to M (V) \in (I \times 2_{𝑜})$
106	17 105	s2cld	$⊢ φ \to ⟨“ V M (V) ”⟩ \in Word (I \times 2_{𝑜})$
107	66	zred	$⊢ φ \to Q \in ℝ$
108		nn0addge1	$⊢ (Q \in ℝ \land 2 \in ℕ_{0}) \to Q \leq Q + 2$
109	107 48 108	sylancl	$⊢ φ \to Q \leq Q + 2$
110		eluz2	$⊢ Q + 2 \in ℤ_{\geq Q} \leftrightarrow (Q \in ℤ \land Q + 2 \in ℤ \land Q \leq Q + 2)$
111	66 71 109 110	syl3anbrc	$⊢ φ \to Q + 2 \in ℤ_{\geq Q}$
112		uztrn	$⊢ (P \in ℤ_{\geq (Q + 2)} \land Q + 2 \in ℤ_{\geq Q}) \to P \in ℤ_{\geq Q}$
113	21 111 112	syl2anc	$⊢ φ \to P \in ℤ_{\geq Q}$
114		elfzuzb	$⊢ Q \in (0 \dots P) \leftrightarrow (Q \in ℤ_{\geq 0} \land P \in ℤ_{\geq Q})$
115	31 113 114	sylanbrc	$⊢ φ \to Q \in (0 \dots P)$
116		ccatpfx	$⊢ (A (K) \in Word (I \times 2_{𝑜}) \land Q \in (0 \dots P) \land P \in (0 \dots \|A (K)\|)) \to (A (K) prefix Q) ++ (A (K) substr ⟨Q, P⟩) = A (K) prefix P$
117	41 115 14 116	syl3anc	$⊢ φ \to (A (K) prefix Q) ++ (A (K) substr ⟨Q, P⟩) = A (K) prefix P$
118	117	oveq1d	$⊢ φ \to ((A (K) prefix Q) ++ (A (K) substr ⟨Q, P⟩)) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = (A (K) prefix P) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩))$
119		pfxcl	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to A (K) prefix P \in Word (I \times 2_{𝑜})$
120	41 119	syl	$⊢ φ \to A (K) prefix P \in Word (I \times 2_{𝑜})$
121	103	ffvelrni	$⊢ U \in (I \times 2_{𝑜}) \to M (U) \in (I \times 2_{𝑜})$
122	16 121	syl	$⊢ φ \to M (U) \in (I \times 2_{𝑜})$
123	16 122	s2cld	$⊢ φ \to ⟨“ U M (U) ”⟩ \in Word (I \times 2_{𝑜})$
124		swrdcl	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to A (K) substr ⟨P, \|A (K)\|⟩ \in Word (I \times 2_{𝑜})$
125	41 124	syl	$⊢ φ \to A (K) substr ⟨P, \|A (K)\|⟩ \in Word (I \times 2_{𝑜})$
126		ccatass	$⊢ (A (K) prefix P \in Word (I \times 2_{𝑜}) \land ⟨“ U M (U) ”⟩ \in Word (I \times 2_{𝑜}) \land A (K) substr ⟨P, \|A (K)\|⟩ \in Word (I \times 2_{𝑜})) \to ((A (K) prefix P) ++ ⟨“ U M (U) ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = (A (K) prefix P) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩))$
127	120 123 125 126	syl3anc	$⊢ φ \to ((A (K) prefix P) ++ ⟨“ U M (U) ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = (A (K) prefix P) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩))$
128	1 2 3 4	efgtval	$⊢ (A (K) \in W \land P \in (0 \dots \|A (K)\|) \land U \in (I \times 2_{𝑜})) \to P T (A (K)) U = A (K) splice ⟨P, P, ⟨“ U M (U) ”⟩⟩$
129	40 14 16 128	syl3anc	$⊢ φ \to P T (A (K)) U = A (K) splice ⟨P, P, ⟨“ U M (U) ”⟩⟩$
130		splval	$⊢ (A (K) \in W \land (P \in (0 \dots \|A (K)\|) \land P \in (0 \dots \|A (K)\|) \land ⟨“ U M (U) ”⟩ \in Word (I \times 2_{𝑜}))) \to A (K) splice ⟨P, P, ⟨“ U M (U) ”⟩⟩ = ((A (K) prefix P) ++ ⟨“ U M (U) ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩)$
131	40 14 14 123 130	syl13anc	$⊢ φ \to A (K) splice ⟨P, P, ⟨“ U M (U) ”⟩⟩ = ((A (K) prefix P) ++ ⟨“ U M (U) ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩)$
132	18 129 131	3eqtrd	$⊢ φ \to S (A) = ((A (K) prefix P) ++ ⟨“ U M (U) ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩)$
133	1 2 3 4	efgtval	$⊢ (B (L) \in W \land Q \in (0 \dots \|B (L)\|) \land V \in (I \times 2_{𝑜})) \to Q T (B (L)) V = B (L) splice ⟨Q, Q, ⟨“ V M (V) ”⟩⟩$
134	36 15 17 133	syl3anc	$⊢ φ \to Q T (B (L)) V = B (L) splice ⟨Q, Q, ⟨“ V M (V) ”⟩⟩$
135		splval	$⊢ (B (L) \in W \land (Q \in (0 \dots \|B (L)\|) \land Q \in (0 \dots \|B (L)\|) \land ⟨“ V M (V) ”⟩ \in Word (I \times 2_{𝑜}))) \to B (L) splice ⟨Q, Q, ⟨“ V M (V) ”⟩⟩ = ((B (L) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
136	36 15 15 106 135	syl13anc	$⊢ φ \to B (L) splice ⟨Q, Q, ⟨“ V M (V) ”⟩⟩ = ((B (L) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
137	19 134 136	3eqtrd	$⊢ φ \to S (B) = ((B (L) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
138	10 132 137	3eqtr3d	$⊢ φ \to ((A (K) prefix P) ++ ⟨“ U M (U) ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = ((B (L) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
139	118 127 138	3eqtr2d	$⊢ φ \to ((A (K) prefix Q) ++ (A (K) substr ⟨Q, P⟩)) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = ((B (L) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
140		swrdcl	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to A (K) substr ⟨Q, P⟩ \in Word (I \times 2_{𝑜})$
141	41 140	syl	$⊢ φ \to A (K) substr ⟨Q, P⟩ \in Word (I \times 2_{𝑜})$
142		ccatcl	$⊢ (⟨“ U M (U) ”⟩ \in Word (I \times 2_{𝑜}) \land A (K) substr ⟨P, \|A (K)\|⟩ \in Word (I \times 2_{𝑜})) \to ⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) \in Word (I \times 2_{𝑜})$
143	123 125 142	syl2anc	$⊢ φ \to ⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) \in Word (I \times 2_{𝑜})$
144		ccatass	$⊢ (A (K) prefix Q \in Word (I \times 2_{𝑜}) \land A (K) substr ⟨Q, P⟩ \in Word (I \times 2_{𝑜}) \land ⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) \in Word (I \times 2_{𝑜})) \to ((A (K) prefix Q) ++ (A (K) substr ⟨Q, P⟩)) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = (A (K) prefix Q) ++ ((A (K) substr ⟨Q, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)))$
145	100 141 143 144	syl3anc	$⊢ φ \to ((A (K) prefix Q) ++ (A (K) substr ⟨Q, P⟩)) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = (A (K) prefix Q) ++ ((A (K) substr ⟨Q, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)))$
146		swrdcl	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to B (L) substr ⟨Q, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})$
147	37 146	syl	$⊢ φ \to B (L) substr ⟨Q, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})$
148		ccatass	$⊢ (B (L) prefix Q \in Word (I \times 2_{𝑜}) \land ⟨“ V M (V) ”⟩ \in Word (I \times 2_{𝑜}) \land B (L) substr ⟨Q, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})) \to ((B (L) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩) = (B (L) prefix Q) ++ (⟨“ V M (V) ”⟩ ++ (B (L) substr ⟨Q, \|B (L)\|⟩))$
149	39 106 147 148	syl3anc	$⊢ φ \to ((B (L) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩) = (B (L) prefix Q) ++ (⟨“ V M (V) ”⟩ ++ (B (L) substr ⟨Q, \|B (L)\|⟩))$
150	139 145 149	3eqtr3d	$⊢ φ \to (A (K) prefix Q) ++ ((A (K) substr ⟨Q, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩))) = (B (L) prefix Q) ++ (⟨“ V M (V) ”⟩ ++ (B (L) substr ⟨Q, \|B (L)\|⟩))$
151		ccatcl	$⊢ (A (K) substr ⟨Q, P⟩ \in Word (I \times 2_{𝑜}) \land ⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) \in Word (I \times 2_{𝑜})) \to (A (K) substr ⟨Q, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) \in Word (I \times 2_{𝑜})$
152	141 143 151	syl2anc	$⊢ φ \to (A (K) substr ⟨Q, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) \in Word (I \times 2_{𝑜})$
153		ccatcl	$⊢ (⟨“ V M (V) ”⟩ \in Word (I \times 2_{𝑜}) \land B (L) substr ⟨Q, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})) \to ⟨“ V M (V) ”⟩ ++ (B (L) substr ⟨Q, \|B (L)\|⟩) \in Word (I \times 2_{𝑜})$
154	106 147 153	syl2anc	$⊢ φ \to ⟨“ V M (V) ”⟩ ++ (B (L) substr ⟨Q, \|B (L)\|⟩) \in Word (I \times 2_{𝑜})$
155		uztrn	$⊢ (\|A (K)\| \in ℤ_{\geq P} \land P \in ℤ_{\geq Q}) \to \|A (K)\| \in ℤ_{\geq Q}$
156	52 113 155	syl2anc	$⊢ φ \to \|A (K)\| \in ℤ_{\geq Q}$
157		elfzuzb	$⊢ Q \in (0 \dots \|A (K)\|) \leftrightarrow (Q \in ℤ_{\geq 0} \land \|A (K)\| \in ℤ_{\geq Q})$
158	31 156 157	sylanbrc	$⊢ φ \to Q \in (0 \dots \|A (K)\|)$
159		pfxlen	$⊢ (A (K) \in Word (I \times 2_{𝑜}) \land Q \in (0 \dots \|A (K)\|)) \to \|A (K) prefix Q\| = Q$
160	41 158 159	syl2anc	$⊢ φ \to \|A (K) prefix Q\| = Q$
161	160 47	eqtr4d	$⊢ φ \to \|A (K) prefix Q\| = \|B (L) prefix Q\|$
162		ccatopth	$⊢ ((A (K) prefix Q \in Word (I \times 2_{𝑜}) \land (A (K) substr ⟨Q, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) \in Word (I \times 2_{𝑜})) \land (B (L) prefix Q \in Word (I \times 2_{𝑜}) \land ⟨“ V M (V) ”⟩ ++ (B (L) substr ⟨Q, \|B (L)\|⟩) \in Word (I \times 2_{𝑜})) \land \|A (K) prefix Q\| = \|B (L) prefix Q\|) \to ((A (K) prefix Q) ++ ((A (K) substr ⟨Q, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩))) = (B (L) prefix Q) ++ (⟨“ V M (V) ”⟩ ++ (B (L) substr ⟨Q, \|B (L)\|⟩)) \leftrightarrow (A (K) prefix Q = B (L) prefix Q \land (A (K) substr ⟨Q, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = ⟨“ V M (V) ”⟩ ++ (B (L) substr ⟨Q, \|B (L)\|⟩)))$
163	100 152 39 154 161 162	syl221anc	$⊢ φ \to ((A (K) prefix Q) ++ ((A (K) substr ⟨Q, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩))) = (B (L) prefix Q) ++ (⟨“ V M (V) ”⟩ ++ (B (L) substr ⟨Q, \|B (L)\|⟩)) \leftrightarrow (A (K) prefix Q = B (L) prefix Q \land (A (K) substr ⟨Q, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = ⟨“ V M (V) ”⟩ ++ (B (L) substr ⟨Q, \|B (L)\|⟩)))$
164	150 163	mpbid	$⊢ φ \to (A (K) prefix Q = B (L) prefix Q \land (A (K) substr ⟨Q, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = ⟨“ V M (V) ”⟩ ++ (B (L) substr ⟨Q, \|B (L)\|⟩))$
165	164	simpld	$⊢ φ \to A (K) prefix Q = B (L) prefix Q$
166	165	oveq1d	$⊢ φ \to (A (K) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩)$
167		ccatrid	$⊢ A (K) prefix Q \in Word (I \times 2_{𝑜}) \to (A (K) prefix Q) ++ \emptyset = A (K) prefix Q$
168	100 167	syl	$⊢ φ \to (A (K) prefix Q) ++ \emptyset = A (K) prefix Q$
169	168	oveq1d	$⊢ φ \to ((A (K) prefix Q) ++ \emptyset) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = (A (K) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩)$
170	166 169 23	3eqtr4rd	$⊢ φ \to S (C) = ((A (K) prefix Q) ++ \emptyset) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩)$
171	160	eqcomd	$⊢ φ \to Q = \|A (K) prefix Q\|$
172		hash0	$⊢ \|\emptyset\| = 0$
173	172	oveq2i	$⊢ Q + \|\emptyset\| = Q + 0$
174	67	addid1d	$⊢ φ \to Q + 0 = Q$
175	173 174	eqtr2id	$⊢ φ \to Q = Q + \|\emptyset\|$
176	100 102 43 106 170 171 175	splval2	$⊢ φ \to S (C) splice ⟨Q, Q, ⟨“ V M (V) ”⟩⟩ = ((A (K) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩)$
177		elfzuzb	$⊢ Q \in (0 \dots Q + 2) \leftrightarrow (Q \in ℤ_{\geq 0} \land Q + 2 \in ℤ_{\geq Q})$
178	31 111 177	sylanbrc	$⊢ φ \to Q \in (0 \dots Q + 2)$
179		elfzuzb	$⊢ Q + 2 \in (0 \dots P) \leftrightarrow (Q + 2 \in ℤ_{\geq 0} \land P \in ℤ_{\geq (Q + 2)})$
180	50 21 179	sylanbrc	$⊢ φ \to Q + 2 \in (0 \dots P)$
181		ccatswrd	$⊢ (A (K) \in Word (I \times 2_{𝑜}) \land (Q \in (0 \dots Q + 2) \land Q + 2 \in (0 \dots P) \land P \in (0 \dots \|A (K)\|))) \to (A (K) substr ⟨Q, Q + 2⟩) ++ (A (K) substr ⟨Q + 2, P⟩) = A (K) substr ⟨Q, P⟩$
182	41 178 180 14 181	syl13anc	$⊢ φ \to (A (K) substr ⟨Q, Q + 2⟩) ++ (A (K) substr ⟨Q + 2, P⟩) = A (K) substr ⟨Q, P⟩$
183	182	oveq1d	$⊢ φ \to ((A (K) substr ⟨Q, Q + 2⟩) ++ (A (K) substr ⟨Q + 2, P⟩)) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = (A (K) substr ⟨Q, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩))$
184		swrdcl	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to A (K) substr ⟨Q, Q + 2⟩ \in Word (I \times 2_{𝑜})$
185	41 184	syl	$⊢ φ \to A (K) substr ⟨Q, Q + 2⟩ \in Word (I \times 2_{𝑜})$
186		swrdcl	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to A (K) substr ⟨Q + 2, P⟩ \in Word (I \times 2_{𝑜})$
187	41 186	syl	$⊢ φ \to A (K) substr ⟨Q + 2, P⟩ \in Word (I \times 2_{𝑜})$
188		ccatass	$⊢ (A (K) substr ⟨Q, Q + 2⟩ \in Word (I \times 2_{𝑜}) \land A (K) substr ⟨Q + 2, P⟩ \in Word (I \times 2_{𝑜}) \land ⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) \in Word (I \times 2_{𝑜})) \to ((A (K) substr ⟨Q, Q + 2⟩) ++ (A (K) substr ⟨Q + 2, P⟩)) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = (A (K) substr ⟨Q, Q + 2⟩) ++ ((A (K) substr ⟨Q + 2, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)))$
189	185 187 143 188	syl3anc	$⊢ φ \to ((A (K) substr ⟨Q, Q + 2⟩) ++ (A (K) substr ⟨Q + 2, P⟩)) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = (A (K) substr ⟨Q, Q + 2⟩) ++ ((A (K) substr ⟨Q + 2, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)))$
190	164	simprd	$⊢ φ \to (A (K) substr ⟨Q, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = ⟨“ V M (V) ”⟩ ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
191	183 189 190	3eqtr3d	$⊢ φ \to (A (K) substr ⟨Q, Q + 2⟩) ++ ((A (K) substr ⟨Q + 2, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩))) = ⟨“ V M (V) ”⟩ ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
192		ccatcl	$⊢ (A (K) substr ⟨Q + 2, P⟩ \in Word (I \times 2_{𝑜}) \land ⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) \in Word (I \times 2_{𝑜})) \to (A (K) substr ⟨Q + 2, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) \in Word (I \times 2_{𝑜})$
193	187 143 192	syl2anc	$⊢ φ \to (A (K) substr ⟨Q + 2, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) \in Word (I \times 2_{𝑜})$
194		swrdlen	$⊢ (A (K) \in Word (I \times 2_{𝑜}) \land Q \in (0 \dots Q + 2) \land Q + 2 \in (0 \dots \|A (K)\|)) \to \|A (K) substr ⟨Q, Q + 2⟩\| = Q + 2 - Q$
195	41 178 56 194	syl3anc	$⊢ φ \to \|A (K) substr ⟨Q, Q + 2⟩\| = Q + 2 - Q$
196		pncan2	$⊢ (Q \in ℂ \land 2 \in ℂ) \to Q + 2 - Q = 2$
197	67 74 196	sylancl	$⊢ φ \to Q + 2 - Q = 2$
198	195 197	eqtrd	$⊢ φ \to \|A (K) substr ⟨Q, Q + 2⟩\| = 2$
199		s2len	$⊢ \|⟨“ V M (V) ”⟩\| = 2$
200	198 199	eqtr4di	$⊢ φ \to \|A (K) substr ⟨Q, Q + 2⟩\| = \|⟨“ V M (V) ”⟩\|$
201		ccatopth	$⊢ ((A (K) substr ⟨Q, Q + 2⟩ \in Word (I \times 2_{𝑜}) \land (A (K) substr ⟨Q + 2, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) \in Word (I \times 2_{𝑜})) \land (⟨“ V M (V) ”⟩ \in Word (I \times 2_{𝑜}) \land B (L) substr ⟨Q, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})) \land \|A (K) substr ⟨Q, Q + 2⟩\| = \|⟨“ V M (V) ”⟩\|) \to ((A (K) substr ⟨Q, Q + 2⟩) ++ ((A (K) substr ⟨Q + 2, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩))) = ⟨“ V M (V) ”⟩ ++ (B (L) substr ⟨Q, \|B (L)\|⟩) \leftrightarrow (A (K) substr ⟨Q, Q + 2⟩ = ⟨“ V M (V) ”⟩ \land (A (K) substr ⟨Q + 2, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = B (L) substr ⟨Q, \|B (L)\|⟩))$
202	185 193 106 147 200 201	syl221anc	$⊢ φ \to ((A (K) substr ⟨Q, Q + 2⟩) ++ ((A (K) substr ⟨Q + 2, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩))) = ⟨“ V M (V) ”⟩ ++ (B (L) substr ⟨Q, \|B (L)\|⟩) \leftrightarrow (A (K) substr ⟨Q, Q + 2⟩ = ⟨“ V M (V) ”⟩ \land (A (K) substr ⟨Q + 2, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = B (L) substr ⟨Q, \|B (L)\|⟩))$
203	191 202	mpbid	$⊢ φ \to (A (K) substr ⟨Q, Q + 2⟩ = ⟨“ V M (V) ”⟩ \land (A (K) substr ⟨Q + 2, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = B (L) substr ⟨Q, \|B (L)\|⟩)$
204	203	simpld	$⊢ φ \to A (K) substr ⟨Q, Q + 2⟩ = ⟨“ V M (V) ”⟩$
205	204	oveq2d	$⊢ φ \to (A (K) prefix Q) ++ (A (K) substr ⟨Q, Q + 2⟩) = (A (K) prefix Q) ++ ⟨“ V M (V) ”⟩$
206		ccatpfx	$⊢ (A (K) \in Word (I \times 2_{𝑜}) \land Q \in (0 \dots Q + 2) \land Q + 2 \in (0 \dots \|A (K)\|)) \to (A (K) prefix Q) ++ (A (K) substr ⟨Q, Q + 2⟩) = A (K) prefix (Q + 2)$
207	41 178 56 206	syl3anc	$⊢ φ \to (A (K) prefix Q) ++ (A (K) substr ⟨Q, Q + 2⟩) = A (K) prefix (Q + 2)$
208	205 207	eqtr3d	$⊢ φ \to (A (K) prefix Q) ++ ⟨“ V M (V) ”⟩ = A (K) prefix (Q + 2)$
209	208	oveq1d	$⊢ φ \to ((A (K) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = (A (K) prefix (Q + 2)) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩)$
210		ccatpfx	$⊢ (A (K) \in Word (I \times 2_{𝑜}) \land Q + 2 \in (0 \dots \|A (K)\|) \land \|A (K)\| \in (0 \dots \|A (K)\|)) \to (A (K) prefix (Q + 2)) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = A (K) prefix \|A (K)\|$
211	41 56 62 210	syl3anc	$⊢ φ \to (A (K) prefix (Q + 2)) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = A (K) prefix \|A (K)\|$
212		pfxid	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to A (K) prefix \|A (K)\| = A (K)$
213	41 212	syl	$⊢ φ \to A (K) prefix \|A (K)\| = A (K)$
214	209 211 213	3eqtrd	$⊢ φ \to ((A (K) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = A (K)$
215	98 176 214	3eqtrd	$⊢ φ \to Q T (S (C)) V = A (K)$
216	1 2 3 4	efgtf	$⊢ S (C) \in W \to (T (S (C)) = (a \in (0 \dots \|S (C)\|), i \in (I \times 2_{𝑜}) ⟼ S (C) splice ⟨a, a, ⟨“ i M (i) ”⟩⟩) \land T (S (C)) : (0 \dots \|S (C)\|) \times (I \times 2_{𝑜}) ⟶ W)$
217	29 216	syl	$⊢ φ \to (T (S (C)) = (a \in (0 \dots \|S (C)\|), i \in (I \times 2_{𝑜}) ⟼ S (C) splice ⟨a, a, ⟨“ i M (i) ”⟩⟩) \land T (S (C)) : (0 \dots \|S (C)\|) \times (I \times 2_{𝑜}) ⟶ W)$
218	217	simprd	$⊢ φ \to T (S (C)) : (0 \dots \|S (C)\|) \times (I \times 2_{𝑜}) ⟶ W$
219	218	ffnd	$⊢ φ \to T (S (C)) Fn ((0 \dots \|S (C)\|) \times (I \times 2_{𝑜}))$
220		fnovrn	$⊢ (T (S (C)) Fn ((0 \dots \|S (C)\|) \times (I \times 2_{𝑜})) \land Q \in (0 \dots \|S (C)\|) \land V \in (I \times 2_{𝑜})) \to Q T (S (C)) V \in ran T (S (C))$
221	219 96 17 220	syl3anc	$⊢ φ \to Q T (S (C)) V \in ran T (S (C))$
222	215 221	eqeltrrd	$⊢ φ \to A (K) \in ran T (S (C))$
223		uztrn	$⊢ (P - 2 \in ℤ_{\geq Q} \land Q \in ℤ_{\geq 0}) \to P - 2 \in ℤ_{\geq 0}$
224	92 31 223	syl2anc	$⊢ φ \to P - 2 \in ℤ_{\geq 0}$
225		elfzuzb	$⊢ P - 2 \in (0 \dots \|S (C)\|) \leftrightarrow (P - 2 \in ℤ_{\geq 0} \land \|S (C)\| \in ℤ_{\geq (P - 2)})$
226	224 90 225	sylanbrc	$⊢ φ \to P - 2 \in (0 \dots \|S (C)\|)$
227	1 2 3 4	efgtval	$⊢ (S (C) \in W \land P - 2 \in (0 \dots \|S (C)\|) \land U \in (I \times 2_{𝑜})) \to (P - 2) T (S (C)) U = S (C) splice ⟨P - 2, P - 2, ⟨“ U M (U) ”⟩⟩$
228	29 226 16 227	syl3anc	$⊢ φ \to (P - 2) T (S (C)) U = S (C) splice ⟨P - 2, P - 2, ⟨“ U M (U) ”⟩⟩$
229		pfxcl	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to B (L) prefix (P - 2) \in Word (I \times 2_{𝑜})$
230	37 229	syl	$⊢ φ \to B (L) prefix (P - 2) \in Word (I \times 2_{𝑜})$
231		swrdcl	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to B (L) substr ⟨P, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})$
232	37 231	syl	$⊢ φ \to B (L) substr ⟨P, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})$
233		ccatswrd	$⊢ (A (K) \in Word (I \times 2_{𝑜}) \land (Q + 2 \in (0 \dots P) \land P \in (0 \dots \|A (K)\|) \land \|A (K)\| \in (0 \dots \|A (K)\|))) \to (A (K) substr ⟨Q + 2, P⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = A (K) substr ⟨Q + 2, \|A (K)\|⟩$
234	41 180 14 62 233	syl13anc	$⊢ φ \to (A (K) substr ⟨Q + 2, P⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = A (K) substr ⟨Q + 2, \|A (K)\|⟩$
235	203	simprd	$⊢ φ \to (A (K) substr ⟨Q + 2, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = B (L) substr ⟨Q, \|B (L)\|⟩$
236		elfzuzb	$⊢ Q \in (0 \dots P - 2) \leftrightarrow (Q \in ℤ_{\geq 0} \land P - 2 \in ℤ_{\geq Q})$
237	31 92 236	sylanbrc	$⊢ φ \to Q \in (0 \dots P - 2)$
238	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	efgredlemg	$⊢ φ \to \|A (K)\| = \|B (L)\|$
239	238 52	eqeltrrd	$⊢ φ \to \|B (L)\| \in ℤ_{\geq P}$
240		0le2	$⊢ 0 \leq 2$
241	240	a1i	$⊢ φ \to 0 \leq 2$
242	79	zred	$⊢ φ \to P \in ℝ$
243		2re	$⊢ 2 \in ℝ$
244		subge02	$⊢ (P \in ℝ \land 2 \in ℝ) \to (0 \leq 2 \leftrightarrow P - 2 \leq P)$
245	242 243 244	sylancl	$⊢ φ \to (0 \leq 2 \leftrightarrow P - 2 \leq P)$
246	241 245	mpbid	$⊢ φ \to P - 2 \leq P$
247		eluz2	$⊢ P \in ℤ_{\geq (P - 2)} \leftrightarrow (P - 2 \in ℤ \land P \in ℤ \land P - 2 \leq P)$
248	81 79 246 247	syl3anbrc	$⊢ φ \to P \in ℤ_{\geq (P - 2)}$
249		uztrn	$⊢ (\|B (L)\| \in ℤ_{\geq P} \land P \in ℤ_{\geq (P - 2)}) \to \|B (L)\| \in ℤ_{\geq (P - 2)}$
250	239 248 249	syl2anc	$⊢ φ \to \|B (L)\| \in ℤ_{\geq (P - 2)}$
251		elfzuzb	$⊢ P - 2 \in (0 \dots \|B (L)\|) \leftrightarrow (P - 2 \in ℤ_{\geq 0} \land \|B (L)\| \in ℤ_{\geq (P - 2)})$
252	224 250 251	sylanbrc	$⊢ φ \to P - 2 \in (0 \dots \|B (L)\|)$
253		lencl	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to \|B (L)\| \in ℕ_{0}$
254	37 253	syl	$⊢ φ \to \|B (L)\| \in ℕ_{0}$
255	254 59	eleqtrdi	$⊢ φ \to \|B (L)\| \in ℤ_{\geq 0}$
256		eluzfz2	$⊢ \|B (L)\| \in ℤ_{\geq 0} \to \|B (L)\| \in (0 \dots \|B (L)\|)$
257	255 256	syl	$⊢ φ \to \|B (L)\| \in (0 \dots \|B (L)\|)$
258		ccatswrd	$⊢ (B (L) \in Word (I \times 2_{𝑜}) \land (Q \in (0 \dots P - 2) \land P - 2 \in (0 \dots \|B (L)\|) \land \|B (L)\| \in (0 \dots \|B (L)\|))) \to (B (L) substr ⟨Q, P - 2⟩) ++ (B (L) substr ⟨P - 2, \|B (L)\|⟩) = B (L) substr ⟨Q, \|B (L)\|⟩$
259	37 237 252 257 258	syl13anc	$⊢ φ \to (B (L) substr ⟨Q, P - 2⟩) ++ (B (L) substr ⟨P - 2, \|B (L)\|⟩) = B (L) substr ⟨Q, \|B (L)\|⟩$
260	235 259	eqtr4d	$⊢ φ \to (A (K) substr ⟨Q + 2, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = (B (L) substr ⟨Q, P - 2⟩) ++ (B (L) substr ⟨P - 2, \|B (L)\|⟩)$
261		swrdcl	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to B (L) substr ⟨Q, P - 2⟩ \in Word (I \times 2_{𝑜})$
262	37 261	syl	$⊢ φ \to B (L) substr ⟨Q, P - 2⟩ \in Word (I \times 2_{𝑜})$
263		swrdcl	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to B (L) substr ⟨P - 2, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})$
264	37 263	syl	$⊢ φ \to B (L) substr ⟨P - 2, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})$
265		swrdlen	$⊢ (A (K) \in Word (I \times 2_{𝑜}) \land Q + 2 \in (0 \dots P) \land P \in (0 \dots \|A (K)\|)) \to \|A (K) substr ⟨Q + 2, P⟩\| = P - (Q + 2)$
266	41 180 14 265	syl3anc	$⊢ φ \to \|A (K) substr ⟨Q + 2, P⟩\| = P - (Q + 2)$
267		swrdlen	$⊢ (B (L) \in Word (I \times 2_{𝑜}) \land Q \in (0 \dots P - 2) \land P - 2 \in (0 \dots \|B (L)\|)) \to \|B (L) substr ⟨Q, P - 2⟩\| = P - 2 - Q$
268	37 237 252 267	syl3anc	$⊢ φ \to \|B (L) substr ⟨Q, P - 2⟩\| = P - 2 - Q$
269	83 67 75	sub32d	$⊢ φ \to P - Q - 2 = P - 2 - Q$
270	83 67 75	subsub4d	$⊢ φ \to P - Q - 2 = P - (Q + 2)$
271	268 269 270	3eqtr2d	$⊢ φ \to \|B (L) substr ⟨Q, P - 2⟩\| = P - (Q + 2)$
272	266 271	eqtr4d	$⊢ φ \to \|A (K) substr ⟨Q + 2, P⟩\| = \|B (L) substr ⟨Q, P - 2⟩\|$
273		ccatopth	$⊢ ((A (K) substr ⟨Q + 2, P⟩ \in Word (I \times 2_{𝑜}) \land ⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) \in Word (I \times 2_{𝑜})) \land (B (L) substr ⟨Q, P - 2⟩ \in Word (I \times 2_{𝑜}) \land B (L) substr ⟨P - 2, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})) \land \|A (K) substr ⟨Q + 2, P⟩\| = \|B (L) substr ⟨Q, P - 2⟩\|) \to ((A (K) substr ⟨Q + 2, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = (B (L) substr ⟨Q, P - 2⟩) ++ (B (L) substr ⟨P - 2, \|B (L)\|⟩) \leftrightarrow (A (K) substr ⟨Q + 2, P⟩ = B (L) substr ⟨Q, P - 2⟩ \land ⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) = B (L) substr ⟨P - 2, \|B (L)\|⟩))$
274	187 143 262 264 272 273	syl221anc	$⊢ φ \to ((A (K) substr ⟨Q + 2, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = (B (L) substr ⟨Q, P - 2⟩) ++ (B (L) substr ⟨P - 2, \|B (L)\|⟩) \leftrightarrow (A (K) substr ⟨Q + 2, P⟩ = B (L) substr ⟨Q, P - 2⟩ \land ⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) = B (L) substr ⟨P - 2, \|B (L)\|⟩))$
275	260 274	mpbid	$⊢ φ \to (A (K) substr ⟨Q + 2, P⟩ = B (L) substr ⟨Q, P - 2⟩ \land ⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) = B (L) substr ⟨P - 2, \|B (L)\|⟩)$
276	275	simpld	$⊢ φ \to A (K) substr ⟨Q + 2, P⟩ = B (L) substr ⟨Q, P - 2⟩$
277	275	simprd	$⊢ φ \to ⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) = B (L) substr ⟨P - 2, \|B (L)\|⟩$
278		elfzuzb	$⊢ P - 2 \in (0 \dots P) \leftrightarrow (P - 2 \in ℤ_{\geq 0} \land P \in ℤ_{\geq (P - 2)})$
279	224 248 278	sylanbrc	$⊢ φ \to P - 2 \in (0 \dots P)$
280		elfzuz	$⊢ P \in (0 \dots \|A (K)\|) \to P \in ℤ_{\geq 0}$
281	14 280	syl	$⊢ φ \to P \in ℤ_{\geq 0}$
282		elfzuzb	$⊢ P \in (0 \dots \|B (L)\|) \leftrightarrow (P \in ℤ_{\geq 0} \land \|B (L)\| \in ℤ_{\geq P})$
283	281 239 282	sylanbrc	$⊢ φ \to P \in (0 \dots \|B (L)\|)$
284		ccatswrd	$⊢ (B (L) \in Word (I \times 2_{𝑜}) \land (P - 2 \in (0 \dots P) \land P \in (0 \dots \|B (L)\|) \land \|B (L)\| \in (0 \dots \|B (L)\|))) \to (B (L) substr ⟨P - 2, P⟩) ++ (B (L) substr ⟨P, \|B (L)\|⟩) = B (L) substr ⟨P - 2, \|B (L)\|⟩$
285	37 279 283 257 284	syl13anc	$⊢ φ \to (B (L) substr ⟨P - 2, P⟩) ++ (B (L) substr ⟨P, \|B (L)\|⟩) = B (L) substr ⟨P - 2, \|B (L)\|⟩$
286	277 285	eqtr4d	$⊢ φ \to ⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) = (B (L) substr ⟨P - 2, P⟩) ++ (B (L) substr ⟨P, \|B (L)\|⟩)$
287		swrdcl	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to B (L) substr ⟨P - 2, P⟩ \in Word (I \times 2_{𝑜})$
288	37 287	syl	$⊢ φ \to B (L) substr ⟨P - 2, P⟩ \in Word (I \times 2_{𝑜})$
289		s2len	$⊢ \|⟨“ U M (U) ”⟩\| = 2$
290		swrdlen	$⊢ (B (L) \in Word (I \times 2_{𝑜}) \land P - 2 \in (0 \dots P) \land P \in (0 \dots \|B (L)\|)) \to \|B (L) substr ⟨P - 2, P⟩\| = P - (P - 2)$
291	37 279 283 290	syl3anc	$⊢ φ \to \|B (L) substr ⟨P - 2, P⟩\| = P - (P - 2)$
292		nncan	$⊢ (P \in ℂ \land 2 \in ℂ) \to P - (P - 2) = 2$
293	83 74 292	sylancl	$⊢ φ \to P - (P - 2) = 2$
294	291 293	eqtr2d	$⊢ φ \to 2 = \|B (L) substr ⟨P - 2, P⟩\|$
295	289 294	eqtrid	$⊢ φ \to \|⟨“ U M (U) ”⟩\| = \|B (L) substr ⟨P - 2, P⟩\|$
296		ccatopth	$⊢ ((⟨“ U M (U) ”⟩ \in Word (I \times 2_{𝑜}) \land A (K) substr ⟨P, \|A (K)\|⟩ \in Word (I \times 2_{𝑜})) \land (B (L) substr ⟨P - 2, P⟩ \in Word (I \times 2_{𝑜}) \land B (L) substr ⟨P, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})) \land \|⟨“ U M (U) ”⟩\| = \|B (L) substr ⟨P - 2, P⟩\|) \to (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) = (B (L) substr ⟨P - 2, P⟩) ++ (B (L) substr ⟨P, \|B (L)\|⟩) \leftrightarrow (⟨“ U M (U) ”⟩ = B (L) substr ⟨P - 2, P⟩ \land A (K) substr ⟨P, \|A (K)\|⟩ = B (L) substr ⟨P, \|B (L)\|⟩))$
297	123 125 288 232 295 296	syl221anc	$⊢ φ \to (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) = (B (L) substr ⟨P - 2, P⟩) ++ (B (L) substr ⟨P, \|B (L)\|⟩) \leftrightarrow (⟨“ U M (U) ”⟩ = B (L) substr ⟨P - 2, P⟩ \land A (K) substr ⟨P, \|A (K)\|⟩ = B (L) substr ⟨P, \|B (L)\|⟩))$
298	286 297	mpbid	$⊢ φ \to (⟨“ U M (U) ”⟩ = B (L) substr ⟨P - 2, P⟩ \land A (K) substr ⟨P, \|A (K)\|⟩ = B (L) substr ⟨P, \|B (L)\|⟩)$
299	298	simprd	$⊢ φ \to A (K) substr ⟨P, \|A (K)\|⟩ = B (L) substr ⟨P, \|B (L)\|⟩$
300	276 299	oveq12d	$⊢ φ \to (A (K) substr ⟨Q + 2, P⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = (B (L) substr ⟨Q, P - 2⟩) ++ (B (L) substr ⟨P, \|B (L)\|⟩)$
301	234 300	eqtr3d	$⊢ φ \to A (K) substr ⟨Q + 2, \|A (K)\|⟩ = (B (L) substr ⟨Q, P - 2⟩) ++ (B (L) substr ⟨P, \|B (L)\|⟩)$
302	301	oveq2d	$⊢ φ \to (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = (B (L) prefix Q) ++ ((B (L) substr ⟨Q, P - 2⟩) ++ (B (L) substr ⟨P, \|B (L)\|⟩))$
303		ccatass	$⊢ (B (L) prefix Q \in Word (I \times 2_{𝑜}) \land B (L) substr ⟨Q, P - 2⟩ \in Word (I \times 2_{𝑜}) \land B (L) substr ⟨P, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})) \to ((B (L) prefix Q) ++ (B (L) substr ⟨Q, P - 2⟩)) ++ (B (L) substr ⟨P, \|B (L)\|⟩) = (B (L) prefix Q) ++ ((B (L) substr ⟨Q, P - 2⟩) ++ (B (L) substr ⟨P, \|B (L)\|⟩))$
304	39 262 232 303	syl3anc	$⊢ φ \to ((B (L) prefix Q) ++ (B (L) substr ⟨Q, P - 2⟩)) ++ (B (L) substr ⟨P, \|B (L)\|⟩) = (B (L) prefix Q) ++ ((B (L) substr ⟨Q, P - 2⟩) ++ (B (L) substr ⟨P, \|B (L)\|⟩))$
305	302 304	eqtr4d	$⊢ φ \to (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = ((B (L) prefix Q) ++ (B (L) substr ⟨Q, P - 2⟩)) ++ (B (L) substr ⟨P, \|B (L)\|⟩)$
306		ccatpfx	$⊢ (B (L) \in Word (I \times 2_{𝑜}) \land Q \in (0 \dots P - 2) \land P - 2 \in (0 \dots \|B (L)\|)) \to (B (L) prefix Q) ++ (B (L) substr ⟨Q, P - 2⟩) = B (L) prefix (P - 2)$
307	37 237 252 306	syl3anc	$⊢ φ \to (B (L) prefix Q) ++ (B (L) substr ⟨Q, P - 2⟩) = B (L) prefix (P - 2)$
308	307	oveq1d	$⊢ φ \to ((B (L) prefix Q) ++ (B (L) substr ⟨Q, P - 2⟩)) ++ (B (L) substr ⟨P, \|B (L)\|⟩) = (B (L) prefix (P - 2)) ++ (B (L) substr ⟨P, \|B (L)\|⟩)$
309	23 305 308	3eqtrd	$⊢ φ \to S (C) = (B (L) prefix (P - 2)) ++ (B (L) substr ⟨P, \|B (L)\|⟩)$
310		ccatrid	$⊢ B (L) prefix (P - 2) \in Word (I \times 2_{𝑜}) \to (B (L) prefix (P - 2)) ++ \emptyset = B (L) prefix (P - 2)$
311	230 310	syl	$⊢ φ \to (B (L) prefix (P - 2)) ++ \emptyset = B (L) prefix (P - 2)$
312	311	oveq1d	$⊢ φ \to ((B (L) prefix (P - 2)) ++ \emptyset) ++ (B (L) substr ⟨P, \|B (L)\|⟩) = (B (L) prefix (P - 2)) ++ (B (L) substr ⟨P, \|B (L)\|⟩)$
313	309 312	eqtr4d	$⊢ φ \to S (C) = ((B (L) prefix (P - 2)) ++ \emptyset) ++ (B (L) substr ⟨P, \|B (L)\|⟩)$
314		pfxlen	$⊢ (B (L) \in Word (I \times 2_{𝑜}) \land P - 2 \in (0 \dots \|B (L)\|)) \to \|B (L) prefix (P - 2)\| = P - 2$
315	37 252 314	syl2anc	$⊢ φ \to \|B (L) prefix (P - 2)\| = P - 2$
316	315	eqcomd	$⊢ φ \to P - 2 = \|B (L) prefix (P - 2)\|$
317	172	oveq2i	$⊢ P - 2 + \|\emptyset\| = P - 2 + 0$
318	81	zcnd	$⊢ φ \to P - 2 \in ℂ$
319	318	addid1d	$⊢ φ \to P - 2 + 0 = P - 2$
320	317 319	eqtr2id	$⊢ φ \to P - 2 = P - 2 + \|\emptyset\|$
321	230 102 232 123 313 316 320	splval2	$⊢ φ \to S (C) splice ⟨P - 2, P - 2, ⟨“ U M (U) ”⟩⟩ = ((B (L) prefix (P - 2)) ++ ⟨“ U M (U) ”⟩) ++ (B (L) substr ⟨P, \|B (L)\|⟩)$
322	298	simpld	$⊢ φ \to ⟨“ U M (U) ”⟩ = B (L) substr ⟨P - 2, P⟩$
323	322	oveq2d	$⊢ φ \to (B (L) prefix (P - 2)) ++ ⟨“ U M (U) ”⟩ = (B (L) prefix (P - 2)) ++ (B (L) substr ⟨P - 2, P⟩)$
324		ccatpfx	$⊢ (B (L) \in Word (I \times 2_{𝑜}) \land P - 2 \in (0 \dots P) \land P \in (0 \dots \|B (L)\|)) \to (B (L) prefix (P - 2)) ++ (B (L) substr ⟨P - 2, P⟩) = B (L) prefix P$
325	37 279 283 324	syl3anc	$⊢ φ \to (B (L) prefix (P - 2)) ++ (B (L) substr ⟨P - 2, P⟩) = B (L) prefix P$
326	323 325	eqtrd	$⊢ φ \to (B (L) prefix (P - 2)) ++ ⟨“ U M (U) ”⟩ = B (L) prefix P$
327	326	oveq1d	$⊢ φ \to ((B (L) prefix (P - 2)) ++ ⟨“ U M (U) ”⟩) ++ (B (L) substr ⟨P, \|B (L)\|⟩) = (B (L) prefix P) ++ (B (L) substr ⟨P, \|B (L)\|⟩)$
328		ccatpfx	$⊢ (B (L) \in Word (I \times 2_{𝑜}) \land P \in (0 \dots \|B (L)\|) \land \|B (L)\| \in (0 \dots \|B (L)\|)) \to (B (L) prefix P) ++ (B (L) substr ⟨P, \|B (L)\|⟩) = B (L) prefix \|B (L)\|$
329	37 283 257 328	syl3anc	$⊢ φ \to (B (L) prefix P) ++ (B (L) substr ⟨P, \|B (L)\|⟩) = B (L) prefix \|B (L)\|$
330		pfxid	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to B (L) prefix \|B (L)\| = B (L)$
331	37 330	syl	$⊢ φ \to B (L) prefix \|B (L)\| = B (L)$
332	327 329 331	3eqtrd	$⊢ φ \to ((B (L) prefix (P - 2)) ++ ⟨“ U M (U) ”⟩) ++ (B (L) substr ⟨P, \|B (L)\|⟩) = B (L)$
333	228 321 332	3eqtrd	$⊢ φ \to (P - 2) T (S (C)) U = B (L)$
334		fnovrn	$⊢ (T (S (C)) Fn ((0 \dots \|S (C)\|) \times (I \times 2_{𝑜})) \land P - 2 \in (0 \dots \|S (C)\|) \land U \in (I \times 2_{𝑜})) \to (P - 2) T (S (C)) U \in ran T (S (C))$
335	219 226 16 334	syl3anc	$⊢ φ \to (P - 2) T (S (C)) U \in ran T (S (C))$
336	333 335	eqeltrrd	$⊢ φ \to B (L) \in ran T (S (C))$
337	222 336	jca	$⊢ φ \to (A (K) \in ran T (S (C)) \land B (L) \in ran T (S (C)))$

Metamath Proof Explorer

Theorem efgredleme

Proof