Metamath Proof Explorer

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 
|- 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 ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csad 
 |-  sadd
1 vx 
 |-  x
2 cn0 
 |-  NN0
3 2 cpw 
 |-  ~P NN0
4 vy 
 |-  y
5 vk 
 |-  k
6 5 cv 
 |-  k
7 1 cv 
 |-  x
8 6 7 wcel 
 |-  k e. x
9 4 cv 
 |-  y
10 6 9 wcel 
 |-  k e. y
11 c0 
 |-  (/)
12 cc0 
 |-  0
13 vc 
 |-  c
14 c2o 
 |-  2o
15 vm 
 |-  m
16 15 cv 
 |-  m
17 16 7 wcel 
 |-  m e. x
18 16 9 wcel 
 |-  m e. y
19 13 cv 
 |-  c
20 11 19 wcel 
 |-  (/) e. c
21 17 18 20 wcad 
 |-  cadd ( m e. x , m e. y , (/) e. c )
22 c1o 
 |-  1o
23 21 22 11 cif 
 |-  if ( cadd ( m e. x , m e. y , (/) e. c ) , 1o , (/) )
24 13 15 14 2 23 cmpo 
 |-  ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. x , m e. y , (/) e. c ) , 1o , (/) ) )
25 vn 
 |-  n
26 25 cv 
 |-  n
27 26 12 wceq 
 |-  n = 0
28 cmin 
 |-  -
29 c1 
 |-  1
30 26 29 28 co 
 |-  ( n - 1 )
31 27 11 30 cif 
 |-  if ( n = 0 , (/) , ( n - 1 ) )
32 25 2 31 cmpt 
 |-  ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) )
33 24 32 12 cseq 
 |-  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 ) ) ) )
34 6 33 cfv 
 |-  ( 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 11 34 wcel 
 |-  (/) 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 8 10 35 whad 
 |-  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 36 5 2 crab 
 |-  { 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 ) ) }
38 1 4 3 3 37 cmpo 
 |-  ( 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 ) ) } )
39 0 38 wceq 
 |-  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 ) ) } )