Definition df-sad

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

	Ref	Expression
Assertion	df-sad	$$⊢\mathrm{sadd}=\left(x\in 𝒫{\mathbb{N}}_0,y\in 𝒫{\mathbb{N}}_0⟼\left\{k\in {\mathbb{N}}_0|hadd\left(k\in x,k\in y,\varnothing \in seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in x,m\in y,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(k\right)\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csad	$$class\mathrm{sadd}$$
1		vx	$$setvarx$$
2		cn0	$$class{\mathbb{N}}_0$$
3	2	cpw	$$class𝒫{\mathbb{N}}_0$$
4		vy	$$setvary$$
5		vk	$$setvark$$
6	5	cv	$$setvark$$
7	1	cv	$$setvarx$$
8	6 7	wcel	$$wffk\in x$$
9	4	cv	$$setvary$$
10	6 9	wcel	$$wffk\in y$$
11		c0	$$class\varnothing$$
12		cc0	$$class0$$
13		vc	$$setvarc$$
14		c2o	$$class{2}_{𝑜}$$
15		vm	$$setvarm$$
16	15	cv	$$setvarm$$
17	16 7	wcel	$$wffm\in x$$
18	16 9	wcel	$$wffm\in y$$
19	13	cv	$$setvarc$$
20	11 19	wcel	$$wff\varnothing \in c$$
21	17 18 20	wcad	$$wffcadd\left(m\in x,m\in y,\varnothing \in c\right)$$
22		c1o	$$class{1}_{𝑜}$$
23	21 22 11	cif	$$classif\left(cadd\left(m\in x,m\in y,\varnothing \in c\right),1_{𝑜},\varnothing \right)$$
24	13 15 14 2 23	cmpo	$$class\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in x,m\in y,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right)$$
25		vn	$$setvarn$$
26	25	cv	$$setvarn$$
27	26 12	wceq	$$wffn=0$$
28		cmin	$$class-$$
29		c1	$$class1$$
30	26 29 28	co	$$class\left(n-1\right)$$
31	27 11 30	cif	$$classif\left(n=0,\varnothing ,n-1\right)$$
32	25 2 31	cmpt	$$class\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)$$
33	24 32 12	cseq	$$classseq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in x,m\in y,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)$$
34	6 33	cfv	$$classseq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in x,m\in y,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(k\right)$$
35	11 34	wcel	$$wff\varnothing \in seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in x,m\in y,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(k\right)$$
36	8 10 35	whad	$$wffhadd\left(k\in x,k\in y,\varnothing \in seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in x,m\in y,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(k\right)\right)$$
37	36 5 2	crab	$$class\left\{k\in {\mathbb{N}}_0|hadd\left(k\in x,k\in y,\varnothing \in seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in x,m\in y,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(k\right)\right)\right\}$$
38	1 4 3 3 37	cmpo	$$class\left(x\in 𝒫{\mathbb{N}}_0,y\in 𝒫{\mathbb{N}}_0⟼\left\{k\in {\mathbb{N}}_0|hadd\left(k\in x,k\in y,\varnothing \in seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in x,m\in y,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(k\right)\right)\right\}\right)$$
39	0 38	wceq	$$wff\mathrm{sadd}=\left(x\in 𝒫{\mathbb{N}}_0,y\in 𝒫{\mathbb{N}}_0⟼\left\{k\in {\mathbb{N}}_0|hadd\left(k\in x,k\in y,\varnothing \in seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in x,m\in y,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(k\right)\right)\right\}\right)$$