swrdccat - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > swrdccat		Unicode version

Theorem swrdccat 11365

Description: The subword of a concatenation of two words as concatenation of subwords of the two concatenated words. (Contributed by Alexander van der Vekens, 29-May-2018.)

**Hypothesis**
Ref	Expression
swrdccatin2.l	♯

**Assertion**
Ref	Expression
swrdccat	Word $/\$ Word $/\$ ♯ ++ substr substr ++ substr

**Proof of Theorem swrdccat**
Step	Hyp	Ref	Expression
1		swrdccatin2.l	. . . . 5 ♯
2	1	pfxccat3 11364	. . . 4 Word $/\$ Word $/\$ ♯ ++ substr substr substr substr ++ prefix
3	2	imp 124	. . 3 Word $/\$ Word $/\$ $/\$ ♯ ++ substr substr substr substr ++ prefix
4		lencl 11166	. . . . . 6 Word ♯
5	4	adantr 276	. . . . 5 Word $/\$ Word ♯
6	1	eqcomi 2235	. . . . . . 7 ♯
7	6	eleq1i 2297	. . . . . 6 ♯
8		elfz2nn0 10392	. . . . . . . . 9 $/\$ $/\$
9		iftrue 3614	. . . . . . . . . . . . . . . . . 18
10	9	adantl 277	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
11	10	opeq2d 3874	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
12	11	oveq2d 6044	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr substr
13		0z 9534	. . . . . . . . . . . . . . . . 17
14		simprll 539	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$
15	14	adantr 276	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
16	15	nn0zd 9644	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
17		simplrr 538	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
18	17	nn0zd 9644	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
19	16, 18	zsubcld 9651	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
20		zdcle 9600	. . . . . . . . . . . . . . . . 17 $/\$ DECID
21	13, 19, 20	sylancr 414	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ DECID
22		exmiddc 844	. . . . . . . . . . . . . . . . 17 DECID $\/$
23		iftrue 3614	. . . . . . . . . . . . . . . . . . . . . . 23
24	23	opeq1d 3873	. . . . . . . . . . . . . . . . . . . . . 22
25	24	oveq2d 6044	. . . . . . . . . . . . . . . . . . . . 21 substr substr
26	25	adantr 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr substr
27		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word Word
28		nn0z 9543	. . . . . . . . . . . . . . . . . . . . . . . . 25
29		nn0z 9543	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
30	29	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
31		zsubcl 9564	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
32	30, 31	sylan 283	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
33		nn0z 9543	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
34	33	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
35		zsubcl 9564	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
36	34, 35	sylan 283	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
37	32, 36	jca 306	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
38	28, 37	sylan2 286	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
39	27, 38	anim12i 338	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
40		3anass 1009	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ $/\$ Word $/\$ $/\$
41	39, 40	sylibr 134	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
42	41	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . 21 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word $/\$ $/\$
43		nn0re 9453	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
44		nn0re 9453	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
45	43, 44	anim12i 338	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
46		nn0re 9453	. . . . . . . . . . . . . . . . . . . . . . . . . 26
47		subge0 8697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
48	47	adantlr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
49		simplr 529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
50		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
51		simpll 527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
52		letr 8304	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
53	49, 50, 51, 52	syl3anc 1274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
54	53	expcomd 1487	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
55	48, 54	sylbid 150	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
56	55	com23 78	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
57	45, 46, 56	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
58	57	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$
59	58	imp 124	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
60	59	impcom 125	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
61	44	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
62	61	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
63	43	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
64	63	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
65	46	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
66	62, 64, 65	3jca 1204	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
67	66	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
68	67	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69		lesub1 8678	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
70	68, 69	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
71	60, 70	mpbid 147	. . . . . . . . . . . . . . . . . . . . 21 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
72		swrdlend 11288	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ $/\$ substr
73	42, 71, 72	sylc 62	. . . . . . . . . . . . . . . . . . . 20 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
74	26, 73	eqtrd 2264	. . . . . . . . . . . . . . . . . . 19 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
75	74	ex 115	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
76		iffalse 3617	. . . . . . . . . . . . . . . . . . . . . 22
77	76	opeq1d 3873	. . . . . . . . . . . . . . . . . . . . 21
78	77	oveq2d 6044	. . . . . . . . . . . . . . . . . . . 20 substr substr
79		simplr 529	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ Word
80	79	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word
81		0zd 9535	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
82	34, 28, 35	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
83	82	adantl 277	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$
84	83	adantr 276	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
85	80, 81, 84	3jca 1204	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word $/\$ $/\$
86	61, 46	anim12i 338	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
87	86	adantl 277	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
88		suble0 8698	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
89	87, 88	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$
90	89	biimpar 297	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
91		swrdlend 11288	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ $/\$ substr
92	85, 90, 91	sylc 62	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
93	78, 92	sylan9eq 2284	. . . . . . . . . . . . . . . . . . 19 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
94	93	ex 115	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
95	75, 94	jaoi 724	. . . . . . . . . . . . . . . . 17 $\/$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
96	22, 95	syl 14	. . . . . . . . . . . . . . . 16 DECID Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
97	21, 96	mpcom 36	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
98	12, 97	oveq12d 6046	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr ++ substr substr ++
99		simpll 527	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ Word
100	14	nn0zd 9644	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$
101	34	ad2antrl 490	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$
102		swrdclg 11280	. . . . . . . . . . . . . . . . 17 Word $/\$ $/\$ substr Word
103	99, 100, 101, 102	syl3anc 1274	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ substr Word
104		ccatrid 11233	. . . . . . . . . . . . . . . 16 substr Word substr ++ substr
105	103, 104	syl 14	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ substr ++ substr
106	105	adantr 276	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr ++ substr
107	98, 106	eqtrd 2264	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr ++ substr substr
108		iffalse 3617	. . . . . . . . . . . . . . . . . . 19
109	108	3ad2ant2 1046	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
110	109	opeq2d 3874	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
111	110	oveq2d 6044	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
112		simpl 109	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word Word
113	112, 30, 28	3anim123i 1211	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
114	113	3expb 1231	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
115		swrdlend 11288	. . . . . . . . . . . . . . . . . . 19 Word $/\$ $/\$ substr
116	114, 115	syl 14	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ substr
117	116	imp 124	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
118	117	3adant2 1043	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr
119	111, 118	eqtrd 2264	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr
120	63, 46, 47	syl2an 289	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
121	120	biimprd 158	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
122	121	adantl 277	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$
123	122	imp 124	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
124	123	3adant2 1043	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
125	124, 24	syl 14	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
126	125	oveq2d 6044	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
127	119, 126	oveq12d 6046	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr ++ substr ++ substr
128		swrdclg 11280	. . . . . . . . . . . . . . . 16 Word $/\$ $/\$ substr Word
129		ccatlid 11232	. . . . . . . . . . . . . . . 16 substr Word ++ substr substr
130	41, 128, 129	3syl 17	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ ++ substr substr
131	130	3ad2ant1 1045	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ++ substr substr
132	127, 131	eqtrd 2264	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr ++ substr substr
133	108	3ad2ant2 1046	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
134	133	opeq2d 3874	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
135	134	oveq2d 6044	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
136	43, 46, 47	syl2an 289	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
137	136	adantlr 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
138	137	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$
139	138	biimpd 144	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$
140	139	con3dimp 640	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
141	140	3adant2 1043	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
142	141, 76	syl 14	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
143	142	opeq1d 3873	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
144	143	oveq2d 6044	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
145	79	3ad2ant1 1045	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ Word
146		simplrr 538	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
147		simprlr 540	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$
148	147	adantr 276	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
149		zltnle 9569	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
150	28, 34, 149	syl2anr 290	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
151		ltle 8309	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
152	46, 61, 151	syl2anr 290	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
153	150, 152	sylbird 170	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
154	153	adantl 277	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$
155	154	imp 124	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
156		nn0sub2 9597	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
157	146, 148, 155, 156	syl3anc 1274	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
158	157	3adant3 1044	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
159		pfxval 11304	. . . . . . . . . . . . . . . 16 Word $/\$ prefix substr
160	145, 158, 159	syl2anc 411	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ prefix substr
161	144, 160	eqtr4d 2267	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr prefix
162	135, 161	oveq12d 6046	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr ++ substr substr ++ prefix
163	28	ad2antll 491	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$
164		zdcle 9600	. . . . . . . . . . . . . 14 $/\$ DECID
165	101, 163, 164	syl2anc 411	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ DECID
166	146	nn0zd 9644	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
167	100	adantr 276	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
168		zdcle 9600	. . . . . . . . . . . . . 14 $/\$ DECID
169	166, 167, 168	syl2anc 411	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ DECID
170	107, 132, 162, 165, 169	2if2dc 3649	. . . . . . . . . . . 12 Word $/\$ Word $/\$ $/\$ $/\$ substr ++ substr substr substr substr ++ prefix
171	170	exp32 365	. . . . . . . . . . 11 Word $/\$ Word $/\$ substr ++ substr substr substr substr ++ prefix
172	171	com12 30	. . . . . . . . . 10 $/\$ Word $/\$ Word substr ++ substr substr substr substr ++ prefix
173	172	3adant3 1044	. . . . . . . . 9 $/\$ $/\$ Word $/\$ Word substr ++ substr substr substr substr ++ prefix
174	8, 173	sylbi 121	. . . . . . . 8 Word $/\$ Word substr ++ substr substr substr substr ++ prefix
175	174	adantr 276	. . . . . . 7 $/\$ ♯ Word $/\$ Word substr ++ substr substr substr substr ++ prefix
176	175	com13 80	. . . . . 6 Word $/\$ Word $/\$ ♯ substr ++ substr substr substr substr ++ prefix
177	7, 176	sylbi 121	. . . . 5 ♯ Word $/\$ Word $/\$ ♯ substr ++ substr substr substr substr ++ prefix
178	5, 177	mpcom 36	. . . 4 Word $/\$ Word $/\$ ♯ substr ++ substr substr substr substr ++ prefix
179	178	imp 124	. . 3 Word $/\$ Word $/\$ $/\$ ♯ substr ++ substr substr substr substr ++ prefix
180	3, 179	eqtr4d 2267	. 2 Word $/\$ Word $/\$ $/\$ ♯ ++ substr substr ++ substr
181	180	ex 115	1 Word $/\$ Word $/\$ ♯ ++ substr substr ++ substr

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 716 DECID wdc 842 $/\$ w3a 1005

wceq 1398

wcel 2202

c0 3496

cif 3607

cop 3676 class class class wbr 4093

cfv 5333 (class class class)co 6028

cr 8074

cc0 8075

caddc 8078

clt 8256

cle 8257

cmin 8392

cn0 9444

cz 9523

cfz 10288 ♯chash 11083 Word cword 11162 ++ cconcat 11216 substr csubstr 11275 prefix cpfx 11302

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4209 ax-sep 4212 ax-nul 4220 ax-pow 4270 ax-pr 4305 ax-un 4536 ax-setind 4641 ax-iinf 4692 ax-cnex 8166 ax-resscn 8167 ax-1cn 8168 ax-1re 8169 ax-icn 8170 ax-addcl 8171 ax-addrcl 8172 ax-mulcl 8173 ax-addcom 8175 ax-addass 8177 ax-distr 8179 ax-i2m1 8180 ax-0lt1 8181 ax-0id 8183 ax-rnegex 8184 ax-cnre 8186 ax-pre-ltirr 8187 ax-pre-ltwlin 8188 ax-pre-lttrn 8189 ax-pre-apti 8190 ax-pre-ltadd 8191

This theorem depends on definitions: df-bi 117 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2364 df-ne 2404 df-nel 2499 df-ral 2516 df-rex 2517 df-reu 2518 df-rab 2520 df-v 2805 df-sbc 3033 df-csb 3129 df-dif 3203 df-un 3205 df-in 3207 df-ss 3214 df-nul 3497 df-if 3608 df-pw 3658 df-sn 3679 df-pr 3680 df-op 3682 df-uni 3899 df-int 3934 df-iun 3977 df-br 4094 df-opab 4156 df-mpt 4157 df-tr 4193 df-id 4396 df-iord 4469 df-on 4471 df-ilim 4472 df-suc 4474 df-iom 4695 df-xp 4737 df-rel 4738 df-cnv 4739 df-co 4740 df-dm 4741 df-rn 4742 df-res 4743 df-ima 4744 df-iota 5293 df-fun 5335 df-fn 5336 df-f 5337 df-f1 5338 df-fo 5339 df-f1o 5340 df-fv 5341 df-riota 5981 df-ov 6031 df-oprab 6032 df-mpo 6033 df-1st 6312 df-2nd 6313 df-recs 6514 df-frec 6600 df-1o 6625 df-er 6745 df-en 6953 df-dom 6954 df-fin 6955 df-pnf 8258 df-mnf 8259 df-xr 8260 df-ltxr 8261 df-le 8262 df-sub 8394 df-neg 8395 df-inn 9186 df-n0 9445 df-z 9524 df-uz 9800 df-fz 10289 df-fzo 10423 df-ihash 11084 df-word 11163 df-concat 11217 df-substr 11276 df-pfx 11303

This theorem is referenced by: (None)

W3C validator