Description: Definition of the "sum" output of the full adder (triple exclusive disjunction, or XOR3, or testing whether an odd number of parameters are true). (Contributed by Mario Carneiro, 4-Sep-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | df-had | |- ( hadd ( ph , ps , ch ) <-> ( ( ph \/_ ps ) \/_ ch ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | wph | |- ph |
|
1 | wps | |- ps |
|
2 | wch | |- ch |
|
3 | 0 1 2 | whad | |- hadd ( ph , ps , ch ) |
4 | 0 1 | wxo | |- ( ph \/_ ps ) |
5 | 4 2 | wxo | |- ( ( ph \/_ ps ) \/_ ch ) |
6 | 3 5 | wb | |- ( hadd ( ph , ps , ch ) <-> ( ( ph \/_ ps ) \/_ ch ) ) |