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

 Description: Define the addition of two bit sequences, using df-had 1389 and df-cad 1390 bit operations. (Contributed by Mario Carneiro, 5-Sep-2016.)
Assertion
Ref Expression
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-sad
StepHypRef Expression
2 vx . . 3
3 vy . . 3
4 cn0 10221 . . . 4
54cpw 3799 . . 3
6 vk . . . . . 6
76, 2wel 1726 . . . . 5
86, 3wel 1726 . . . . 5
9 c0 3628 . . . . . 6
106cv 1651 . . . . . . 7
11 vc . . . . . . . . 9
12 vm . . . . . . . . 9
13 c2o 6718 . . . . . . . . 9
1412, 2wel 1726 . . . . . . . . . . 11
1512, 3wel 1726 . . . . . . . . . . 11
1611cv 1651 . . . . . . . . . . . 12
179, 16wcel 1725 . . . . . . . . . . 11
1814, 15, 17wcad 1388 . . . . . . . . . 10 cadd
19 c1o 6717 . . . . . . . . . 10
2018, 19, 9cif 3739 . . . . . . . . 9 cadd
2111, 12, 13, 4, 20cmpt2 6083 . . . . . . . 8 cadd
22 vn . . . . . . . . 9
2322cv 1651 . . . . . . . . . . 11
24 cc0 8990 . . . . . . . . . . 11
2523, 24wceq 1652 . . . . . . . . . 10
26 c1 8991 . . . . . . . . . . 11
27 cmin 9291 . . . . . . . . . . 11
2823, 26, 27co 6081 . . . . . . . . . 10
2925, 9, 28cif 3739 . . . . . . . . 9
3022, 4, 29cmpt 4266 . . . . . . . 8
3121, 30, 24cseq 11323 . . . . . . 7 cadd
3210, 31cfv 5454 . . . . . 6 cadd
339, 32wcel 1725 . . . . 5 cadd