Definition df-sad 15173

Description: Define the addition of two bit sequences, using df-had 1533 and df-cad 1546 bit operations. (Contributed by Mario Carneiro, 5-Sep-2016.)

Assertion

Ref	Expression
df-sad	|- sadd = ( x e. ~P NN0 , y e. ~P NN0 |-> { k e. NN0 | hadd ( k e. x , k e. y , (/) e. ( seq 0 ( ( c e. 2o , m e. NN0 |-> if (cadd ( m e. x , m e. y , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) ) } )

Distinct variable group:   k, c, m, n, x, y

Detailed syntax breakdown of Definition df-sad

Step	Hyp	Ref	Expression
1		csad 15142	. 2 class sadd
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cn0 11292	. . . 4 class NN0
5	4	cpw 4158	. . 3 class ~P NN0
6		vk	. . . . . 6 setvar k
7	6, 2	wel 1991	. . . . 5 wff k e. x
8	6, 3	wel 1991	. . . . 5 wff k e. y
9		c0 3915	. . . . . 6 class (/)
10	6	cv 1482	. . . . . . 7 class k
11		vc	. . . . . . . . 9 setvar c
12		vm	. . . . . . . . 9 setvar m
13		c2o 7554	. . . . . . . . 9 class 2o
14	12, 2	wel 1991	. . . . . . . . . . 11 wff m e. x
15	12, 3	wel 1991	. . . . . . . . . . 11 wff m e. y
16	11	cv 1482	. . . . . . . . . . . 12 class c
17	9, 16	wcel 1990	. . . . . . . . . . 11 wff (/) e. c
18	14, 15, 17	wcad 1545	. . . . . . . . . 10 wff cadd ( m e. x , m e. y , (/) e. c )
19		c1o 7553	. . . . . . . . . 10 class 1o
20	18, 19, 9	cif 4086	. . . . . . . . 9 class if (cadd ( m e. x , m e. y , (/) e. c ) , 1o , (/) )
21	11, 12, 13, 4, 20	cmpt2 6652	. . . . . . . 8 class ( c e. 2o , m e. NN0 |-> if (cadd ( m e. x , m e. y , (/) e. c ) , 1o , (/) ) )
22		vn	. . . . . . . . 9 setvar n
23	22	cv 1482	. . . . . . . . . . 11 class n
24		cc0 9936	. . . . . . . . . . 11 class 0
25	23, 24	wceq 1483	. . . . . . . . . 10 wff n = 0
26		c1 9937	. . . . . . . . . . 11 class 1
27		cmin 10266	. . . . . . . . . . 11 class -
28	23, 26, 27	co 6650	. . . . . . . . . 10 class ( n - 1 )
29	25, 9, 28	cif 4086	. . . . . . . . 9 class if ( n = 0 , (/) , ( n - 1 ) )
30	22, 4, 29	cmpt 4729	. . . . . . . 8 class ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) )
31	21, 30, 24	cseq 12801	. . . . . . 7 class seq 0 ( ( c e. 2o , m e. NN0 |-> if (cadd ( m e. x , m e. y , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
32	10, 31	cfv 5888	. . . . . 6 class ( seq 0 ( ( c e. 2o , m e. NN0 |-> if (cadd ( m e. x , m e. y , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k )
33	9, 32	wcel 1990	. . . . 5 wff (/) e. ( seq 0 ( ( c e. 2o , m e. NN0 |-> if (cadd ( m e. x , m e. y , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k )
34	7, 8, 33	whad 1532	. . . 4 wff hadd ( k e. x , k e. y , (/) e. ( seq 0 ( ( c e. 2o , m e. NN0 |-> if (cadd ( m e. x , m e. y , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) )
35	34, 6, 4	crab 2916	. . 3 class { k e. NN0 | hadd ( k e. x , k e. y , (/) e. ( seq 0 ( ( c e. 2o , m e. NN0 |-> if (cadd ( m e. x , m e. y , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) ) }
36	2, 3, 5, 5, 35	cmpt2 6652	. 2 class ( x e. ~P NN0 , y e. ~P NN0 |-> { k e. NN0 | hadd ( k e. x , k e. y , (/) e. ( seq 0 ( ( c e. 2o , m e. NN0 |-> if (cadd ( m e. x , m e. y , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) ) } )
37	1, 36	wceq 1483	1 wff sadd = ( x e. ~P NN0 , y e. ~P NN0 |-> { k e. NN0 | hadd ( k e. x , k e. y , (/) e. ( seq 0 ( ( c e. 2o , m e. NN0 |-> if (cadd ( m e. x , m e. y , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` k ) ) } )

This definition is referenced by:  sadfval  15174