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

 Description: Define the addition of two bit sequences, using df-had 1386 and df-cad 1387 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 10177 . . . 4
54cpw 3759 . . 3
6 vk . . . . . 6
76, 2wel 1722 . . . . 5
86, 3wel 1722 . . . . 5
9 c0 3588 . . . . . 6
106cv 1648 . . . . . . 7
11 vc . . . . . . . . 9
12 vm . . . . . . . . 9
13 c2o 6677 . . . . . . . . 9
1412, 2wel 1722 . . . . . . . . . . 11
1512, 3wel 1722 . . . . . . . . . . 11
1611cv 1648 . . . . . . . . . . . 12
179, 16wcel 1721 . . . . . . . . . . 11
1814, 15, 17wcad 1385 . . . . . . . . . 10 cadd
19 c1o 6676 . . . . . . . . . 10
2018, 19, 9cif 3699 . . . . . . . . 9 cadd
2111, 12, 13, 4, 20cmpt2 6042 . . . . . . . 8 cadd
22 vn . . . . . . . . 9
2322cv 1648 . . . . . . . . . . 11
24 cc0 8946 . . . . . . . . . . 11
2523, 24wceq 1649 . . . . . . . . . 10
26 c1 8947 . . . . . . . . . . 11
27 cmin 9247 . . . . . . . . . . 11
2823, 26, 27co 6040 . . . . . . . . . 10
2925, 9, 28cif 3699 . . . . . . . . 9
3022, 4, 29cmpt 4226 . . . . . . . 8
3121, 30, 24cseq 11278 . . . . . . 7 cadd
3210, 31cfv 5413 . . . . . 6 cadd
339, 32wcel 1721 . . . . 5 cadd