Description: For sequences that correspond to valid integers, the adder sequence function produces the sequence for the sum. This is effectively a proof of the correctness of the ripple carry adder, implemented with logic gates corresponding to df-had and df-cad .
It is interesting to consider in what sense the sadd function can be said to be "adding" things outside the range of the bits function, that is, when adding sequences that are not eventually constant and so do not denote any integer. The correct interpretation is that the sequences are representations of 2-adic integers, which have a natural ring structure. (Contributed by Mario Carneiro, 9-Sep-2016)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sadadd | |- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( bits ` A ) sadd ( bits ` B ) ) = ( bits ` ( A + B ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bitsss | |- ( bits ` A ) C_ NN0 |
|
| 2 | bitsss | |- ( bits ` B ) C_ NN0 |
|
| 3 | sadcl | |- ( ( ( bits ` A ) C_ NN0 /\ ( bits ` B ) C_ NN0 ) -> ( ( bits ` A ) sadd ( bits ` B ) ) C_ NN0 ) |
|
| 4 | 1 2 3 | mp2an | |- ( ( bits ` A ) sadd ( bits ` B ) ) C_ NN0 |
| 5 | 4 | sseli | |- ( k e. ( ( bits ` A ) sadd ( bits ` B ) ) -> k e. NN0 ) |
| 6 | 5 | a1i | |- ( ( A e. ZZ /\ B e. ZZ ) -> ( k e. ( ( bits ` A ) sadd ( bits ` B ) ) -> k e. NN0 ) ) |
| 7 | bitsss | |- ( bits ` ( A + B ) ) C_ NN0 |
|
| 8 | 7 | sseli | |- ( k e. ( bits ` ( A + B ) ) -> k e. NN0 ) |
| 9 | 8 | a1i | |- ( ( A e. ZZ /\ B e. ZZ ) -> ( k e. ( bits ` ( A + B ) ) -> k e. NN0 ) ) |
| 10 | eqid | |- seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. ( bits ` A ) , m e. ( bits ` B ) , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) = seq 0 ( ( c e. 2o , m e. NN0 |-> if ( cadd ( m e. ( bits ` A ) , m e. ( bits ` B ) , (/) e. c ) , 1o , (/) ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) |
|
| 11 | eqid | |- `' ( bits |` NN0 ) = `' ( bits |` NN0 ) |
|
| 12 | simpll | |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ k e. NN0 ) -> A e. ZZ ) |
|
| 13 | simplr | |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ k e. NN0 ) -> B e. ZZ ) |
|
| 14 | simpr | |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ k e. NN0 ) -> k e. NN0 ) |
|
| 15 | 1nn0 | |- 1 e. NN0 |
|
| 16 | 15 | a1i | |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ k e. NN0 ) -> 1 e. NN0 ) |
| 17 | 14 16 | nn0addcld | |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ k e. NN0 ) -> ( k + 1 ) e. NN0 ) |
| 18 | 10 11 12 13 17 | sadaddlem | |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ k e. NN0 ) -> ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ ( k + 1 ) ) ) = ( bits ` ( ( A + B ) mod ( 2 ^ ( k + 1 ) ) ) ) ) |
| 19 | 12 13 | zaddcld | |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ k e. NN0 ) -> ( A + B ) e. ZZ ) |
| 20 | bitsmod | |- ( ( ( A + B ) e. ZZ /\ ( k + 1 ) e. NN0 ) -> ( bits ` ( ( A + B ) mod ( 2 ^ ( k + 1 ) ) ) ) = ( ( bits ` ( A + B ) ) i^i ( 0 ..^ ( k + 1 ) ) ) ) |
|
| 21 | 19 17 20 | syl2anc | |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ k e. NN0 ) -> ( bits ` ( ( A + B ) mod ( 2 ^ ( k + 1 ) ) ) ) = ( ( bits ` ( A + B ) ) i^i ( 0 ..^ ( k + 1 ) ) ) ) |
| 22 | 18 21 | eqtrd | |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ k e. NN0 ) -> ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ ( k + 1 ) ) ) = ( ( bits ` ( A + B ) ) i^i ( 0 ..^ ( k + 1 ) ) ) ) |
| 23 | 22 | eleq2d | |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ k e. NN0 ) -> ( k e. ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ ( k + 1 ) ) ) <-> k e. ( ( bits ` ( A + B ) ) i^i ( 0 ..^ ( k + 1 ) ) ) ) ) |
| 24 | elin | |- ( k e. ( ( ( bits ` A ) sadd ( bits ` B ) ) i^i ( 0 ..^ ( k + 1 ) ) ) <-> ( k e. ( ( bits ` A ) sadd ( bits ` B ) ) /\ k e. ( 0 ..^ ( k + 1 ) ) ) ) |
|
| 25 | elin | |- ( k e. ( ( bits ` ( A + B ) ) i^i ( 0 ..^ ( k + 1 ) ) ) <-> ( k e. ( bits ` ( A + B ) ) /\ k e. ( 0 ..^ ( k + 1 ) ) ) ) |
|
| 26 | 23 24 25 | 3bitr3g | |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ k e. NN0 ) -> ( ( k e. ( ( bits ` A ) sadd ( bits ` B ) ) /\ k e. ( 0 ..^ ( k + 1 ) ) ) <-> ( k e. ( bits ` ( A + B ) ) /\ k e. ( 0 ..^ ( k + 1 ) ) ) ) ) |
| 27 | nn0uz | |- NN0 = ( ZZ>= ` 0 ) |
|
| 28 | 14 27 | eleqtrdi | |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ k e. NN0 ) -> k e. ( ZZ>= ` 0 ) ) |
| 29 | eluzfz2 | |- ( k e. ( ZZ>= ` 0 ) -> k e. ( 0 ... k ) ) |
|
| 30 | 28 29 | syl | |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ k e. NN0 ) -> k e. ( 0 ... k ) ) |
| 31 | 14 | nn0zd | |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ k e. NN0 ) -> k e. ZZ ) |
| 32 | fzval3 | |- ( k e. ZZ -> ( 0 ... k ) = ( 0 ..^ ( k + 1 ) ) ) |
|
| 33 | 31 32 | syl | |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ k e. NN0 ) -> ( 0 ... k ) = ( 0 ..^ ( k + 1 ) ) ) |
| 34 | 30 33 | eleqtrd | |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ k e. NN0 ) -> k e. ( 0 ..^ ( k + 1 ) ) ) |
| 35 | 34 | biantrud | |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ k e. NN0 ) -> ( k e. ( ( bits ` A ) sadd ( bits ` B ) ) <-> ( k e. ( ( bits ` A ) sadd ( bits ` B ) ) /\ k e. ( 0 ..^ ( k + 1 ) ) ) ) ) |
| 36 | 34 | biantrud | |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ k e. NN0 ) -> ( k e. ( bits ` ( A + B ) ) <-> ( k e. ( bits ` ( A + B ) ) /\ k e. ( 0 ..^ ( k + 1 ) ) ) ) ) |
| 37 | 26 35 36 | 3bitr4d | |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ k e. NN0 ) -> ( k e. ( ( bits ` A ) sadd ( bits ` B ) ) <-> k e. ( bits ` ( A + B ) ) ) ) |
| 38 | 37 | ex | |- ( ( A e. ZZ /\ B e. ZZ ) -> ( k e. NN0 -> ( k e. ( ( bits ` A ) sadd ( bits ` B ) ) <-> k e. ( bits ` ( A + B ) ) ) ) ) |
| 39 | 6 9 38 | pm5.21ndd | |- ( ( A e. ZZ /\ B e. ZZ ) -> ( k e. ( ( bits ` A ) sadd ( bits ` B ) ) <-> k e. ( bits ` ( A + B ) ) ) ) |
| 40 | 39 | eqrdv | |- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( bits ` A ) sadd ( bits ` B ) ) = ( bits ` ( A + B ) ) ) |