Definition df-seq0 6535

Description: Define a recursive sequence builder operation that starts at index 0. This is a frequently-used variation of the seq1 operation (see df-seq1 6309), which starts at index 1. See seq00 6551 and seq0p1 6552 for its initial and successor values. See dfseq0 6564 for an alternate definition.

Assertion

Ref	Expression
df-seq0	|- seq0 = {<.<.f, g>., h>. | h = (((f seq1 (g shift 1)) shift -u1) |` NN0)}

Distinct variable group:   f,g,h

Detailed syntax breakdown of Definition df-seq0

Step	Hyp	Ref	Expression
1		cseq0 6533	. 2 class seq0
2		vh	. . . . 5 set h
3	2	cv 957	. . . 4 class h
4		vf	. . . . . . . 8 set f
5	4	cv 957	. . . . . . 7 class f
6		vg	. . . . . . . . 9 set g
7	6	cv 957	. . . . . . . 8 class g
8		c1 5247	. . . . . . . 8 class 1
9		cshi 6341	. . . . . . . 8 class shift
10	7, 8, 9	co 3969	. . . . . . 7 class (g shift 1)
11		cseq1 6308	. . . . . . 7 class seq1
12	5, 10, 11	co 3969	. . . . . 6 class (f seq1 (g shift 1))
13	8	cneg 5305	. . . . . 6 class -u1
14	12, 13, 9	co 3969	. . . . 5 class ((f seq1 (g shift 1)) shift -u1)
15		cn0 5309	. . . . 5 class NN0
16	14, 15	cres 3178	. . . 4 class (((f seq1 (g shift 1)) shift -u1) |` NN0)
17	3, 16	wceq 958	. . 3 wff h = (((f seq1 (g shift 1)) shift -u1) |` NN0)
18	17, 4, 6, 2	copab2 3970	. 2 class {<.<.f, g>., h>. | h = (((f seq1 (g shift 1)) shift -u1) |` NN0)}
19	1, 18	wceq 958	1 wff seq0 = {<.<.f, g>., h>. | h = (((f seq1 (g shift 1)) shift -u1) |` NN0)}

This definition is referenced by:  seq0fval 6536  dfseq0 6564

Copyright terms: Public domain