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	sseldi	$⊢ φ \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	sseldi	$⊢ φ \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		elfzelz	$⊢ Q \in (0 \dots \|B (L)\|) \to Q \in ℤ$
67	15 66	syl	$⊢ φ \to Q \in ℤ$
68	67	zcnd	$⊢ φ \to Q \in ℂ$
69	58	nn0cnd	$⊢ φ \to \|A (K)\| \in ℂ$
70		2z	$⊢ 2 \in ℤ$
71		zaddcl	$⊢ (Q \in ℤ \land 2 \in ℤ) \to Q + 2 \in ℤ$
72	67 70 71	sylancl	$⊢ φ \to Q + 2 \in ℤ$
73	72	zcnd	$⊢ φ \to Q + 2 \in ℂ$
74	68 69 73	addsubassd	$⊢ φ \to Q + \|A (K)\| - (Q + 2) = Q + \|A (K)\| - (Q + 2)$
75		2cn	$⊢ 2 \in ℂ$
76	75	a1i	$⊢ φ \to 2 \in ℂ$
77	68 69 76	pnpcand	$⊢ φ \to Q + \|A (K)\| - (Q + 2) = \|A (K)\| - 2$
78	65 74 77	3eqtr2d	$⊢ φ \to \|B (L) prefix Q\| + \|A (K) substr ⟨Q + 2, \|A (K)\|⟩\| = \|A (K)\| - 2$
79	32 45 78	3eqtrd	$⊢ φ \to \|S (C)\| = \|A (K)\| - 2$
80		elfzelz	$⊢ P \in (0 \dots \|A (K)\|) \to P \in ℤ$
81	14 80	syl	$⊢ φ \to P \in ℤ$
82		zsubcl	$⊢ (P \in ℤ \land 2 \in ℤ) \to P - 2 \in ℤ$
83	81 70 82	sylancl	$⊢ φ \to P - 2 \in ℤ$
84	70	a1i	$⊢ φ \to 2 \in ℤ$
85	81	zcnd	$⊢ φ \to P \in ℂ$
86		npcan	$⊢ (P \in ℂ \land 2 \in ℂ) \to P - 2 + 2 = P$
87	85 75 86	sylancl	$⊢ φ \to P - 2 + 2 = P$
88	87	fveq2d	$⊢ φ \to ℤ_{\geq (P - 2 + 2)} = ℤ_{\geq P}$
89	52 88	eleqtrrd	$⊢ φ \to \|A (K)\| \in ℤ_{\geq (P - 2 + 2)}$
90		eluzsub	$⊢ (P - 2 \in ℤ \land 2 \in ℤ \land \|A (K)\| \in ℤ_{\geq (P - 2 + 2)}) \to \|A (K)\| - 2 \in ℤ_{\geq (P - 2)}$
91	83 84 89 90	syl3anc	$⊢ φ \to \|A (K)\| - 2 \in ℤ_{\geq (P - 2)}$
92	79 91	eqeltrd	$⊢ φ \to \|S (C)\| \in ℤ_{\geq (P - 2)}$
93		eluzsub	$⊢ (Q \in ℤ \land 2 \in ℤ \land P \in ℤ_{\geq (Q + 2)}) \to P - 2 \in ℤ_{\geq Q}$
94	67 84 21 93	syl3anc	$⊢ φ \to P - 2 \in ℤ_{\geq Q}$
95		uztrn	$⊢ (\|S (C)\| \in ℤ_{\geq (P - 2)} \land P - 2 \in ℤ_{\geq Q}) \to \|S (C)\| \in ℤ_{\geq Q}$
96	92 94 95	syl2anc	$⊢ φ \to \|S (C)\| \in ℤ_{\geq Q}$
97		elfzuzb	$⊢ Q \in (0 \dots \|S (C)\|) \leftrightarrow (Q \in ℤ_{\geq 0} \land \|S (C)\| \in ℤ_{\geq Q})$
98	31 96 97	sylanbrc	$⊢ φ \to Q \in (0 \dots \|S (C)\|)$
99	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) ”⟩⟩$
100	29 98 17 99	syl3anc	$⊢ φ \to Q T (S (C)) V = S (C) splice ⟨Q, Q, ⟨“ V M (V) ”⟩⟩$
101		pfxcl	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to A (K) prefix Q \in Word (I \times 2_{𝑜})$
102	41 101	syl	$⊢ φ \to A (K) prefix Q \in Word (I \times 2_{𝑜})$
103		wrd0	$⊢ \emptyset \in Word (I \times 2_{𝑜})$
104	103	a1i	$⊢ φ \to \emptyset \in Word (I \times 2_{𝑜})$
105	3	efgmf	$⊢ M : I \times 2_{𝑜} ⟶ I \times 2_{𝑜}$
106	105	ffvelrni	$⊢ V \in (I \times 2_{𝑜}) \to M (V) \in (I \times 2_{𝑜})$
107	17 106	syl	$⊢ φ \to M (V) \in (I \times 2_{𝑜})$
108	17 107	s2cld	$⊢ φ \to ⟨“ V M (V) ”⟩ \in Word (I \times 2_{𝑜})$
109	67	zred	$⊢ φ \to Q \in ℝ$
110		nn0addge1	$⊢ (Q \in ℝ \land 2 \in ℕ_{0}) \to Q \leq Q + 2$
111	109 48 110	sylancl	$⊢ φ \to Q \leq Q + 2$
112		eluz2	$⊢ Q + 2 \in ℤ_{\geq Q} \leftrightarrow (Q \in ℤ \land Q + 2 \in ℤ \land Q \leq Q + 2)$
113	67 72 111 112	syl3anbrc	$⊢ φ \to Q + 2 \in ℤ_{\geq Q}$
114		uztrn	$⊢ (P \in ℤ_{\geq (Q + 2)} \land Q + 2 \in ℤ_{\geq Q}) \to P \in ℤ_{\geq Q}$
115	21 113 114	syl2anc	$⊢ φ \to P \in ℤ_{\geq Q}$
116		elfzuzb	$⊢ Q \in (0 \dots P) \leftrightarrow (Q \in ℤ_{\geq 0} \land P \in ℤ_{\geq Q})$
117	31 115 116	sylanbrc	$⊢ φ \to Q \in (0 \dots P)$
118		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$
119	41 117 14 118	syl3anc	$⊢ φ \to (A (K) prefix Q) ++ (A (K) substr ⟨Q, P⟩) = A (K) prefix P$
120	119	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)\|⟩))$
121		pfxcl	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to A (K) prefix P \in Word (I \times 2_{𝑜})$
122	41 121	syl	$⊢ φ \to A (K) prefix P \in Word (I \times 2_{𝑜})$
123	105	ffvelrni	$⊢ U \in (I \times 2_{𝑜}) \to M (U) \in (I \times 2_{𝑜})$
124	16 123	syl	$⊢ φ \to M (U) \in (I \times 2_{𝑜})$
125	16 124	s2cld	$⊢ φ \to ⟨“ U M (U) ”⟩ \in Word (I \times 2_{𝑜})$
126		swrdcl	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to A (K) substr ⟨P, \|A (K)\|⟩ \in Word (I \times 2_{𝑜})$
127	41 126	syl	$⊢ φ \to A (K) substr ⟨P, \|A (K)\|⟩ \in Word (I \times 2_{𝑜})$
128		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)\|⟩))$
129	122 125 127 128	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)\|⟩))$
130	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) ”⟩⟩$
131	40 14 16 130	syl3anc	$⊢ φ \to P T (A (K)) U = A (K) splice ⟨P, P, ⟨“ U M (U) ”⟩⟩$
132		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)\|⟩)$
133	40 14 14 125 132	syl13anc	$⊢ φ \to A (K) splice ⟨P, P, ⟨“ U M (U) ”⟩⟩ = ((A (K) prefix P) ++ ⟨“ U M (U) ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩)$
134	18 131 133	3eqtrd	$⊢ φ \to S (A) = ((A (K) prefix P) ++ ⟨“ U M (U) ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩)$
135	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) ”⟩⟩$
136	36 15 17 135	syl3anc	$⊢ φ \to Q T (B (L)) V = B (L) splice ⟨Q, Q, ⟨“ V M (V) ”⟩⟩$
137		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)\|⟩)$
138	36 15 15 108 137	syl13anc	$⊢ φ \to B (L) splice ⟨Q, Q, ⟨“ V M (V) ”⟩⟩ = ((B (L) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
139	19 136 138	3eqtrd	$⊢ φ \to S (B) = ((B (L) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
140	10 134 139	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)\|⟩)$
141	120 129 140	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)\|⟩)$
142		swrdcl	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to A (K) substr ⟨Q, P⟩ \in Word (I \times 2_{𝑜})$
143	41 142	syl	$⊢ φ \to A (K) substr ⟨Q, P⟩ \in Word (I \times 2_{𝑜})$
144		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_{𝑜})$
145	125 127 144	syl2anc	$⊢ φ \to ⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) \in Word (I \times 2_{𝑜})$
146		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)\|⟩)))$
147	102 143 145 146	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)\|⟩)))$
148		swrdcl	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to B (L) substr ⟨Q, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})$
149	37 148	syl	$⊢ φ \to B (L) substr ⟨Q, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})$
150		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)\|⟩))$
151	39 108 149 150	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)\|⟩))$
152	141 147 151	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)\|⟩))$
153		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_{𝑜})$
154	143 145 153	syl2anc	$⊢ φ \to (A (K) substr ⟨Q, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) \in Word (I \times 2_{𝑜})$
155		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_{𝑜})$
156	108 149 155	syl2anc	$⊢ φ \to ⟨“ V M (V) ”⟩ ++ (B (L) substr ⟨Q, \|B (L)\|⟩) \in Word (I \times 2_{𝑜})$
157		uztrn	$⊢ (\|A (K)\| \in ℤ_{\geq P} \land P \in ℤ_{\geq Q}) \to \|A (K)\| \in ℤ_{\geq Q}$
158	52 115 157	syl2anc	$⊢ φ \to \|A (K)\| \in ℤ_{\geq Q}$
159		elfzuzb	$⊢ Q \in (0 \dots \|A (K)\|) \leftrightarrow (Q \in ℤ_{\geq 0} \land \|A (K)\| \in ℤ_{\geq Q})$
160	31 158 159	sylanbrc	$⊢ φ \to Q \in (0 \dots \|A (K)\|)$
161		pfxlen	$⊢ (A (K) \in Word (I \times 2_{𝑜}) \land Q \in (0 \dots \|A (K)\|)) \to \|A (K) prefix Q\| = Q$
162	41 160 161	syl2anc	$⊢ φ \to \|A (K) prefix Q\| = Q$
163	162 47	eqtr4d	$⊢ φ \to \|A (K) prefix Q\| = \|B (L) prefix Q\|$
164		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)\|⟩)))$
165	102 154 39 156 163 164	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)\|⟩)))$
166	152 165	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)\|⟩))$
167	166	simpld	$⊢ φ \to A (K) prefix Q = B (L) prefix Q$
168	167	oveq1d	$⊢ φ \to (A (K) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩)$
169		ccatrid	$⊢ A (K) prefix Q \in Word (I \times 2_{𝑜}) \to (A (K) prefix Q) ++ \emptyset = A (K) prefix Q$
170	102 169	syl	$⊢ φ \to (A (K) prefix Q) ++ \emptyset = A (K) prefix Q$
171	170	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)\|⟩)$
172	168 171 23	3eqtr4rd	$⊢ φ \to S (C) = ((A (K) prefix Q) ++ \emptyset) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩)$
173	162	eqcomd	$⊢ φ \to Q = \|A (K) prefix Q\|$
174		hash0	$⊢ \|\emptyset\| = 0$
175	174	oveq2i	$⊢ Q + \|\emptyset\| = Q + 0$
176	68	addid1d	$⊢ φ \to Q + 0 = Q$
177	175 176	syl5req	$⊢ φ \to Q = Q + \|\emptyset\|$
178	102 104 43 108 172 173 177	splval2	$⊢ φ \to S (C) splice ⟨Q, Q, ⟨“ V M (V) ”⟩⟩ = ((A (K) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩)$
179		elfzuzb	$⊢ Q \in (0 \dots Q + 2) \leftrightarrow (Q \in ℤ_{\geq 0} \land Q + 2 \in ℤ_{\geq Q})$
180	31 113 179	sylanbrc	$⊢ φ \to Q \in (0 \dots Q + 2)$
181		elfzuzb	$⊢ Q + 2 \in (0 \dots P) \leftrightarrow (Q + 2 \in ℤ_{\geq 0} \land P \in ℤ_{\geq (Q + 2)})$
182	50 21 181	sylanbrc	$⊢ φ \to Q + 2 \in (0 \dots P)$
183		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⟩$
184	41 180 182 14 183	syl13anc	$⊢ φ \to (A (K) substr ⟨Q, Q + 2⟩) ++ (A (K) substr ⟨Q + 2, P⟩) = A (K) substr ⟨Q, P⟩$
185	184	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)\|⟩))$
186		swrdcl	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to A (K) substr ⟨Q, Q + 2⟩ \in Word (I \times 2_{𝑜})$
187	41 186	syl	$⊢ φ \to A (K) substr ⟨Q, Q + 2⟩ \in Word (I \times 2_{𝑜})$
188		swrdcl	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to A (K) substr ⟨Q + 2, P⟩ \in Word (I \times 2_{𝑜})$
189	41 188	syl	$⊢ φ \to A (K) substr ⟨Q + 2, P⟩ \in Word (I \times 2_{𝑜})$
190		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)\|⟩)))$
191	187 189 145 190	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)\|⟩)))$
192	166	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)\|⟩)$
193	185 191 192	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)\|⟩)$
194		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_{𝑜})$
195	189 145 194	syl2anc	$⊢ φ \to (A (K) substr ⟨Q + 2, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) \in Word (I \times 2_{𝑜})$
196		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$
197	41 180 56 196	syl3anc	$⊢ φ \to \|A (K) substr ⟨Q, Q + 2⟩\| = Q + 2 - Q$
198		pncan2	$⊢ (Q \in ℂ \land 2 \in ℂ) \to Q + 2 - Q = 2$
199	68 75 198	sylancl	$⊢ φ \to Q + 2 - Q = 2$
200	197 199	eqtrd	$⊢ φ \to \|A (K) substr ⟨Q, Q + 2⟩\| = 2$
201		s2len	$⊢ \|⟨“ V M (V) ”⟩\| = 2$
202	200 201	eqtr4di	$⊢ φ \to \|A (K) substr ⟨Q, Q + 2⟩\| = \|⟨“ V M (V) ”⟩\|$
203		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)\|⟩))$
204	187 195 108 149 202 203	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)\|⟩))$
205	193 204	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)\|⟩)$
206	205	simpld	$⊢ φ \to A (K) substr ⟨Q, Q + 2⟩ = ⟨“ V M (V) ”⟩$
207	206	oveq2d	$⊢ φ \to (A (K) prefix Q) ++ (A (K) substr ⟨Q, Q + 2⟩) = (A (K) prefix Q) ++ ⟨“ V M (V) ”⟩$
208		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)$
209	41 180 56 208	syl3anc	$⊢ φ \to (A (K) prefix Q) ++ (A (K) substr ⟨Q, Q + 2⟩) = A (K) prefix (Q + 2)$
210	207 209	eqtr3d	$⊢ φ \to (A (K) prefix Q) ++ ⟨“ V M (V) ”⟩ = A (K) prefix (Q + 2)$
211	210	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)\|⟩)$
212		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)\|$
213	41 56 62 212	syl3anc	$⊢ φ \to (A (K) prefix (Q + 2)) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = A (K) prefix \|A (K)\|$
214		pfxid	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to A (K) prefix \|A (K)\| = A (K)$
215	41 214	syl	$⊢ φ \to A (K) prefix \|A (K)\| = A (K)$
216	211 213 215	3eqtrd	$⊢ φ \to ((A (K) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = A (K)$
217	100 178 216	3eqtrd	$⊢ φ \to Q T (S (C)) V = A (K)$
218	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)$
219	29 218	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)$
220	219	simprd	$⊢ φ \to T (S (C)) : (0 \dots \|S (C)\|) \times (I \times 2_{𝑜}) ⟶ W$
221	220	ffnd	$⊢ φ \to T (S (C)) Fn ((0 \dots \|S (C)\|) \times (I \times 2_{𝑜}))$
222		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))$
223	221 98 17 222	syl3anc	$⊢ φ \to Q T (S (C)) V \in ran T (S (C))$
224	217 223	eqeltrrd	$⊢ φ \to A (K) \in ran T (S (C))$
225		uztrn	$⊢ (P - 2 \in ℤ_{\geq Q} \land Q \in ℤ_{\geq 0}) \to P - 2 \in ℤ_{\geq 0}$
226	94 31 225	syl2anc	$⊢ φ \to P - 2 \in ℤ_{\geq 0}$
227		elfzuzb	$⊢ P - 2 \in (0 \dots \|S (C)\|) \leftrightarrow (P - 2 \in ℤ_{\geq 0} \land \|S (C)\| \in ℤ_{\geq (P - 2)})$
228	226 92 227	sylanbrc	$⊢ φ \to P - 2 \in (0 \dots \|S (C)\|)$
229	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) ”⟩⟩$
230	29 228 16 229	syl3anc	$⊢ φ \to (P - 2) T (S (C)) U = S (C) splice ⟨P - 2, P - 2, ⟨“ U M (U) ”⟩⟩$
231		pfxcl	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to B (L) prefix (P - 2) \in Word (I \times 2_{𝑜})$
232	37 231	syl	$⊢ φ \to B (L) prefix (P - 2) \in Word (I \times 2_{𝑜})$
233		swrdcl	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to B (L) substr ⟨P, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})$
234	37 233	syl	$⊢ φ \to B (L) substr ⟨P, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})$
235		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)\|⟩$
236	41 182 14 62 235	syl13anc	$⊢ φ \to (A (K) substr ⟨Q + 2, P⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = A (K) substr ⟨Q + 2, \|A (K)\|⟩$
237	205	simprd	$⊢ φ \to (A (K) substr ⟨Q + 2, P⟩) ++ (⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = B (L) substr ⟨Q, \|B (L)\|⟩$
238		elfzuzb	$⊢ Q \in (0 \dots P - 2) \leftrightarrow (Q \in ℤ_{\geq 0} \land P - 2 \in ℤ_{\geq Q})$
239	31 94 238	sylanbrc	$⊢ φ \to Q \in (0 \dots P - 2)$
240	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)\|$
241	240 52	eqeltrrd	$⊢ φ \to \|B (L)\| \in ℤ_{\geq P}$
242		0le2	$⊢ 0 \leq 2$
243	242	a1i	$⊢ φ \to 0 \leq 2$
244	81	zred	$⊢ φ \to P \in ℝ$
245		2re	$⊢ 2 \in ℝ$
246		subge02	$⊢ (P \in ℝ \land 2 \in ℝ) \to (0 \leq 2 \leftrightarrow P - 2 \leq P)$
247	244 245 246	sylancl	$⊢ φ \to (0 \leq 2 \leftrightarrow P - 2 \leq P)$
248	243 247	mpbid	$⊢ φ \to P - 2 \leq P$
249		eluz2	$⊢ P \in ℤ_{\geq (P - 2)} \leftrightarrow (P - 2 \in ℤ \land P \in ℤ \land P - 2 \leq P)$
250	83 81 248 249	syl3anbrc	$⊢ φ \to P \in ℤ_{\geq (P - 2)}$
251		uztrn	$⊢ (\|B (L)\| \in ℤ_{\geq P} \land P \in ℤ_{\geq (P - 2)}) \to \|B (L)\| \in ℤ_{\geq (P - 2)}$
252	241 250 251	syl2anc	$⊢ φ \to \|B (L)\| \in ℤ_{\geq (P - 2)}$
253		elfzuzb	$⊢ P - 2 \in (0 \dots \|B (L)\|) \leftrightarrow (P - 2 \in ℤ_{\geq 0} \land \|B (L)\| \in ℤ_{\geq (P - 2)})$
254	226 252 253	sylanbrc	$⊢ φ \to P - 2 \in (0 \dots \|B (L)\|)$
255		lencl	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to \|B (L)\| \in ℕ_{0}$
256	37 255	syl	$⊢ φ \to \|B (L)\| \in ℕ_{0}$
257	256 59	eleqtrdi	$⊢ φ \to \|B (L)\| \in ℤ_{\geq 0}$
258		eluzfz2	$⊢ \|B (L)\| \in ℤ_{\geq 0} \to \|B (L)\| \in (0 \dots \|B (L)\|)$
259	257 258	syl	$⊢ φ \to \|B (L)\| \in (0 \dots \|B (L)\|)$
260		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)\|⟩$
261	37 239 254 259 260	syl13anc	$⊢ φ \to (B (L) substr ⟨Q, P - 2⟩) ++ (B (L) substr ⟨P - 2, \|B (L)\|⟩) = B (L) substr ⟨Q, \|B (L)\|⟩$
262	237 261	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)\|⟩)$
263		swrdcl	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to B (L) substr ⟨Q, P - 2⟩ \in Word (I \times 2_{𝑜})$
264	37 263	syl	$⊢ φ \to B (L) substr ⟨Q, P - 2⟩ \in Word (I \times 2_{𝑜})$
265		swrdcl	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to B (L) substr ⟨P - 2, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})$
266	37 265	syl	$⊢ φ \to B (L) substr ⟨P - 2, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})$
267		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)$
268	41 182 14 267	syl3anc	$⊢ φ \to \|A (K) substr ⟨Q + 2, P⟩\| = P - (Q + 2)$
269		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$
270	37 239 254 269	syl3anc	$⊢ φ \to \|B (L) substr ⟨Q, P - 2⟩\| = P - 2 - Q$
271	85 68 76	sub32d	$⊢ φ \to P - Q - 2 = P - 2 - Q$
272	85 68 76	subsub4d	$⊢ φ \to P - Q - 2 = P - (Q + 2)$
273	270 271 272	3eqtr2d	$⊢ φ \to \|B (L) substr ⟨Q, P - 2⟩\| = P - (Q + 2)$
274	268 273	eqtr4d	$⊢ φ \to \|A (K) substr ⟨Q + 2, P⟩\| = \|B (L) substr ⟨Q, P - 2⟩\|$
275		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)\|⟩))$
276	189 145 264 266 274 275	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)\|⟩))$
277	262 276	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)\|⟩)$
278	277	simpld	$⊢ φ \to A (K) substr ⟨Q + 2, P⟩ = B (L) substr ⟨Q, P - 2⟩$
279	277	simprd	$⊢ φ \to ⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) = B (L) substr ⟨P - 2, \|B (L)\|⟩$
280		elfzuzb	$⊢ P - 2 \in (0 \dots P) \leftrightarrow (P - 2 \in ℤ_{\geq 0} \land P \in ℤ_{\geq (P - 2)})$
281	226 250 280	sylanbrc	$⊢ φ \to P - 2 \in (0 \dots P)$
282		elfzuz	$⊢ P \in (0 \dots \|A (K)\|) \to P \in ℤ_{\geq 0}$
283	14 282	syl	$⊢ φ \to P \in ℤ_{\geq 0}$
284		elfzuzb	$⊢ P \in (0 \dots \|B (L)\|) \leftrightarrow (P \in ℤ_{\geq 0} \land \|B (L)\| \in ℤ_{\geq P})$
285	283 241 284	sylanbrc	$⊢ φ \to P \in (0 \dots \|B (L)\|)$
286		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)\|⟩$
287	37 281 285 259 286	syl13anc	$⊢ φ \to (B (L) substr ⟨P - 2, P⟩) ++ (B (L) substr ⟨P, \|B (L)\|⟩) = B (L) substr ⟨P - 2, \|B (L)\|⟩$
288	279 287	eqtr4d	$⊢ φ \to ⟨“ U M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) = (B (L) substr ⟨P - 2, P⟩) ++ (B (L) substr ⟨P, \|B (L)\|⟩)$
289		swrdcl	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to B (L) substr ⟨P - 2, P⟩ \in Word (I \times 2_{𝑜})$
290	37 289	syl	$⊢ φ \to B (L) substr ⟨P - 2, P⟩ \in Word (I \times 2_{𝑜})$
291		s2len	$⊢ \|⟨“ U M (U) ”⟩\| = 2$
292		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)$
293	37 281 285 292	syl3anc	$⊢ φ \to \|B (L) substr ⟨P - 2, P⟩\| = P - (P - 2)$
294		nncan	$⊢ (P \in ℂ \land 2 \in ℂ) \to P - (P - 2) = 2$
295	85 75 294	sylancl	$⊢ φ \to P - (P - 2) = 2$
296	293 295	eqtr2d	$⊢ φ \to 2 = \|B (L) substr ⟨P - 2, P⟩\|$
297	291 296	syl5eq	$⊢ φ \to \|⟨“ U M (U) ”⟩\| = \|B (L) substr ⟨P - 2, P⟩\|$
298		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)\|⟩))$
299	125 127 290 234 297 298	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)\|⟩))$
300	288 299	mpbid	$⊢ φ \to (⟨“ U M (U) ”⟩ = B (L) substr ⟨P - 2, P⟩ \land A (K) substr ⟨P, \|A (K)\|⟩ = B (L) substr ⟨P, \|B (L)\|⟩)$
301	300	simprd	$⊢ φ \to A (K) substr ⟨P, \|A (K)\|⟩ = B (L) substr ⟨P, \|B (L)\|⟩$
302	278 301	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)\|⟩)$
303	236 302	eqtr3d	$⊢ φ \to A (K) substr ⟨Q + 2, \|A (K)\|⟩ = (B (L) substr ⟨Q, P - 2⟩) ++ (B (L) substr ⟨P, \|B (L)\|⟩)$
304	303	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)\|⟩))$
305		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)\|⟩))$
306	39 264 234 305	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)\|⟩))$
307	304 306	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)\|⟩)$
308		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)$
309	37 239 254 308	syl3anc	$⊢ φ \to (B (L) prefix Q) ++ (B (L) substr ⟨Q, P - 2⟩) = B (L) prefix (P - 2)$
310	309	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)\|⟩)$
311	23 307 310	3eqtrd	$⊢ φ \to S (C) = (B (L) prefix (P - 2)) ++ (B (L) substr ⟨P, \|B (L)\|⟩)$
312		ccatrid	$⊢ B (L) prefix (P - 2) \in Word (I \times 2_{𝑜}) \to (B (L) prefix (P - 2)) ++ \emptyset = B (L) prefix (P - 2)$
313	232 312	syl	$⊢ φ \to (B (L) prefix (P - 2)) ++ \emptyset = B (L) prefix (P - 2)$
314	313	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)\|⟩)$
315	311 314	eqtr4d	$⊢ φ \to S (C) = ((B (L) prefix (P - 2)) ++ \emptyset) ++ (B (L) substr ⟨P, \|B (L)\|⟩)$
316		pfxlen	$⊢ (B (L) \in Word (I \times 2_{𝑜}) \land P - 2 \in (0 \dots \|B (L)\|)) \to \|B (L) prefix (P - 2)\| = P - 2$
317	37 254 316	syl2anc	$⊢ φ \to \|B (L) prefix (P - 2)\| = P - 2$
318	317	eqcomd	$⊢ φ \to P - 2 = \|B (L) prefix (P - 2)\|$
319	174	oveq2i	$⊢ P - 2 + \|\emptyset\| = P - 2 + 0$
320	83	zcnd	$⊢ φ \to P - 2 \in ℂ$
321	320	addid1d	$⊢ φ \to P - 2 + 0 = P - 2$
322	319 321	syl5req	$⊢ φ \to P - 2 = P - 2 + \|\emptyset\|$
323	232 104 234 125 315 318 322	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)\|⟩)$
324	300	simpld	$⊢ φ \to ⟨“ U M (U) ”⟩ = B (L) substr ⟨P - 2, P⟩$
325	324	oveq2d	$⊢ φ \to (B (L) prefix (P - 2)) ++ ⟨“ U M (U) ”⟩ = (B (L) prefix (P - 2)) ++ (B (L) substr ⟨P - 2, P⟩)$
326		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$
327	37 281 285 326	syl3anc	$⊢ φ \to (B (L) prefix (P - 2)) ++ (B (L) substr ⟨P - 2, P⟩) = B (L) prefix P$
328	325 327	eqtrd	$⊢ φ \to (B (L) prefix (P - 2)) ++ ⟨“ U M (U) ”⟩ = B (L) prefix P$
329	328	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)\|⟩)$
330		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)\|$
331	37 285 259 330	syl3anc	$⊢ φ \to (B (L) prefix P) ++ (B (L) substr ⟨P, \|B (L)\|⟩) = B (L) prefix \|B (L)\|$
332		pfxid	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to B (L) prefix \|B (L)\| = B (L)$
333	37 332	syl	$⊢ φ \to B (L) prefix \|B (L)\| = B (L)$
334	329 331 333	3eqtrd	$⊢ φ \to ((B (L) prefix (P - 2)) ++ ⟨“ U M (U) ”⟩) ++ (B (L) substr ⟨P, \|B (L)\|⟩) = B (L)$
335	230 323 334	3eqtrd	$⊢ φ \to (P - 2) T (S (C)) U = B (L)$
336		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))$
337	221 228 16 336	syl3anc	$⊢ φ \to (P - 2) T (S (C)) U \in ran T (S (C))$
338	335 337	eqeltrrd	$⊢ φ \to B (L) \in ran T (S (C))$
339	224 338	jca	$⊢ φ \to (A (K) \in ran T (S (C)) \land B (L) \in ran T (S (C)))$

Metamath Proof Explorer

Theorem efgredleme

Proof