MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sad Unicode version

Definition df-sad 12689
Description: Define the addition of two bit sequences, using df-had 1371 and df-cad 1372 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
StepHypRef Expression
1 csad 12658 . 2  class sadd
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cn0 10012 . . . 4  class  NN0
54cpw 3659 . . 3  class  ~P NN0
6 vk . . . . . 6  set  k
76, 2wel 1702 . . . . 5  wff  k  e.  x
86, 3wel 1702 . . . . 5  wff  k  e.  y
9 c0 3489 . . . . . 6  class  (/)
106cv 1632 . . . . . . 7  class  k
11 vc . . . . . . . . 9  set  c
12 vm . . . . . . . . 9  set  m
13 c2o 6515 . . . . . . . . 9  class  2o
1412, 2wel 1702 . . . . . . . . . . 11  wff  m  e.  x
1512, 3wel 1702 . . . . . . . . . . 11  wff  m  e.  y
1611cv 1632 . . . . . . . . . . . 12  class  c
179, 16wcel 1701 . . . . . . . . . . 11  wff  (/)  e.  c
1814, 15, 17wcad 1370 . . . . . . . . . 10  wff cadd ( m  e.  x ,  m  e.  y ,  (/)  e.  c )
19 c1o 6514 . . . . . . . . . 10  class  1o
2018, 19, 9cif 3599 . . . . . . . . 9  class  if (cadd ( m  e.  x ,  m  e.  y ,  (/)  e.  c ) ,  1o ,  (/) )
2111, 12, 13, 4, 20cmpt2 5902 . . . . . . . 8  class  ( c  e.  2o ,  m  e.  NN0  |->  if (cadd ( m  e.  x ,  m  e.  y ,  (/)  e.  c ) ,  1o ,  (/) ) )
22 vn . . . . . . . . 9  set  n
2322cv 1632 . . . . . . . . . . 11  class  n
24 cc0 8782 . . . . . . . . . . 11  class  0
2523, 24wceq 1633 . . . . . . . . . 10  wff  n  =  0
26 c1 8783 . . . . . . . . . . 11  class  1
27 cmin 9082 . . . . . . . . . . 11  class  -
2823, 26, 27co 5900 . . . . . . . . . 10  class  ( n  -  1 )
2925, 9, 28cif 3599 . . . . . . . . 9  class  if ( n  =  0 ,  (/) ,  ( n  - 
1 ) )
3022, 4, 29cmpt 4114 . . . . . . . 8  class  ( n  e.  NN0  |->  if ( n  =  0 ,  (/) ,  ( n  - 
1 ) ) )
3121, 30, 24cseq 11093 . . . . . . 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 ) ) ) )
3210, 31cfv 5292 . . . . . 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 )
339, 32wcel 1701 . . . . 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 )
347, 8, 33whad 1369 . . . 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 ) )
3534, 6, 4crab 2581 . . 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 ) ) }
362, 3, 5, 5, 35cmpt2 5902 . 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 ) ) } )
371, 36wceq 1633 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 ) ) } )
Colors of variables: wff set class
This definition is referenced by:  sadfval  12690
  Copyright terms: Public domain W3C validator