Metamath Proof Explorer


Definition df-cad

Description: Definition of the "carry" output of the full adder. It is true when at least two arguments are true, so it is equal to the "majority" function on three variables. See cador and cadan for alternate definitions. (Contributed by Mario Carneiro, 4-Sep-2016)

Ref Expression
Assertion df-cad
|- ( cadd ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( ch /\ ( ph \/_ ps ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 wph
 |-  ph
1 wps
 |-  ps
2 wch
 |-  ch
3 0 1 2 wcad
 |-  cadd ( ph , ps , ch )
4 0 1 wa
 |-  ( ph /\ ps )
5 0 1 wxo
 |-  ( ph \/_ ps )
6 2 5 wa
 |-  ( ch /\ ( ph \/_ ps ) )
7 4 6 wo
 |-  ( ( ph /\ ps ) \/ ( ch /\ ( ph \/_ ps ) ) )
8 3 7 wb
 |-  ( cadd ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( ch /\ ( ph \/_ ps ) ) ) )