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

Definition df-sad 12642
Description: Define the addition of two bit sequences, using df-had 1370 and df-cad 1371 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 12611 . 2  class sadd
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cn0 9965 . . . 4  class  NN0
54cpw 3625 . . 3  class  ~P NN0
6 vk . . . . . 6  set  k
76, 2wel 1685 . . . . 5  wff  k  e.  x
86, 3wel 1685 . . . . 5  wff  k  e.  y
9 c0 3455 . . . . . 6  class  (/)
106cv 1622 . . . . . . 7  class  k
11 vc . . . . . . . . 9  set  c
12 vm . . . . . . . . 9  set  m
13 c2o 6473 . . . . . . . . 9  class  2o
1412, 2wel 1685 . . . . . . . . . . 11  wff  m  e.  x
1512, 3wel 1685 . . . . . . . . . . 11  wff  m  e.  y
1611cv 1622 . . . . . . . . . . . 12  class  c
179, 16wcel 1684 . . . . . . . . . . 11  wff  (/)  e.  c
1814, 15, 17wcad 1369 . . . . . . . . . 10  wff cadd ( m  e.  x ,  m  e.  y ,  (/)  e.  c )
19 c1o 6472 . . . . . . . . . 10  class  1o
2018, 19, 9cif 3565 . . . . . . . . 9  class  if (cadd ( m  e.  x ,  m  e.  y ,  (/)  e.  c ) ,  1o ,  (/) )
2111, 12, 13, 4, 20cmpt2 5860 . . . . . . . 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 1622 . . . . . . . . . . 11  class  n
24 cc0 8737 . . . . . . . . . . 11  class  0
2523, 24wceq 1623 . . . . . . . . . 10  wff  n  =  0
26 c1 8738 . . . . . . . . . . 11  class  1
27 cmin 9037 . . . . . . . . . . 11  class  -
2823, 26, 27co 5858 . . . . . . . . . 10  class  ( n  -  1 )
2925, 9, 28cif 3565 . . . . . . . . 9  class  if ( n  =  0 ,  (/) ,  ( n  - 
1 ) )
3022, 4, 29cmpt 4077 . . . . . . . 8  class  ( n  e.  NN0  |->  if ( n  =  0 ,  (/) ,  ( n  - 
1 ) ) )
3121, 30, 24cseq 11046 . . . . . . 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 5255 . . . . . 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 1684 . . . . 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 1368 . . . 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 2547 . . 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 5860 . 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 1623 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  12643
  Copyright terms: Public domain W3C validator