|
(--) ∧ (--) |
<(<<>> ⊕ u)(<<>> ⊕ u)> |
u |
(x+) |
|
(++) ∧ (--) |
<(<> ⊕ <u>)(<<>> ⊕ u)> |
u |
(x+) |
|
(-+) ∧ (--) |
<(<<>> ⊕ <u>)(<<>> ⊕ u)> |
<<>> |
(+x) |
|
(+-) ∧ (--) |
<(<> ⊕ u)(<<>> ⊕ u)> |
<> ⊕ <u> |
(--) |
|
(-x) ∧ (--) |
<(<<>>)(<<>> ⊕ u)> |
<> ⊕ <u> |
(--) |
|
(x-) ∧ (--) |
<(u)(<<>> ⊕ u)> |
<<>> |
(+x) |
|
(x+) ∧ (--) |
<(<u>)(<<>> ⊕ u)> |
<> ⊕ <u> |
(--) |
|
(+x) ∧ (--) |
<(<>)(<<>> ⊕ u)> |
<<>> |
(+x) |
|
|
|
|
|
|
(--) ∧ (++) |
<(<<>> ⊕ u)(<> ⊕ <u>)> |
u |
(x+) |
|
(++) ∧ (++) |
<(<> ⊕ <u>)(<> ⊕ <u>)> |
<> |
(-x) |
|
(-+) ∧ (++) |
<(<<>> ⊕ <u>)(<> ⊕ <u>)> |
<> ⊕ u |
(-+) |
|
(+-) ∧ (++) |
<(<> ⊕ u)(<> ⊕ <u>)> |
0 ⊕ u•0 |
(xx) |
|
(-x) ∧ (++) |
<(<<>>)(<> ⊕ <u>)> |
<<>> ⊕ u |
(++) |
|
(x-) ∧ (++) |
<(u)(<> ⊕ <u>)> |
<u> |
(x-) |
|
(x+) ∧ (++) |
<(<u>)(<> ⊕ <u>)> |
<> ⊕ <u> |
(--) |
|
(+x) ∧ (++) |
<(<>)(<> ⊕ <u>)> |
<<>> |
(+x) |
|
|
|
|
|
|
(--) ∧ (-+) |
<(<<>> ⊕ u)(<<>> ⊕ <u>)> |
<<>> |
(+x) |
|
(++) ∧ (-+) |
<(<> ⊕ <u>)(<<>> ⊕ <u>)> |
<> ⊕ u |
(-+) |
|
(-+) ∧ (-+) |
<(<<>> ⊕ <u>)(<<>> ⊕ <u>)> |
<u> |
(x-) |
|
(+-) ∧ (-+) |
<(<> ⊕ u)(<<>> ⊕ <u>)> |
<u> |
(x-) |
|
(-x) ∧ (-+) |
<(<<>>)(<<>> ⊕ <u>)> |
<> ⊕ u |
(-+) |
|
(x-) ∧ (-+) |
<(u)(<<>> ⊕ <u>)> |
<> ⊕ u |
(-+) |
|
(x+) ∧ (-+) |
<(<u>)(<<>> ⊕ <u>)> |
<<>> |
(+x) |
|
(+x) ∧ (-+) |
<(<>)(<<>> ⊕ <u>)> |
<<>> |
(+x) |
|
|
|
|
|
|
(--) ∧ (+-) |
<(<<>> ⊕ u)(<> ⊕ u)> |
<> ⊕ <u> |
(--) |
|
(++) ∧ (+-) |
<(<> ⊕ <u>)(<> ⊕ u)> |
0 ⊕ u•0 |
(xx) |
|
(-+) ∧ (+-) |
<(<<>> ⊕ <u>)(<> ⊕ u)> |
<u> |
(x-) |
|
(+-) ∧ (+-) |
<(<> ⊕ u)(<> ⊕ u)> |
<> |
(-x) |
|
(-x) ∧ (+-) |
<(<<>>)(<> ⊕ u)> |
<<>> ⊕ <u> |
(+-) |
|
(x-) ∧ (+-) |
<(u)(<> ⊕ u)> |
<> ⊕ u |
(-+) |
|
(x+) ∧ (+-) |
<(<u>)(<> ⊕ u)> |
u |
(x+) |
|
(+x) ∧ (+-) |
<(<>)(<> ⊕ u)> |
<<>> |
(+x) |
|
|
|
|
|
|
(--) ∧ (-x) |
<(<<>> ⊕ u)(<<>>)> |
<> ⊕ <u> |
(--) |
|
(++) ∧ (-x) |
<(<> ⊕ <u>)(<<>>)> |
<<>> ⊕ u |
(++) |
|
(-+) ∧ (-x) |
<(<<>> ⊕ <u>)(<<>>)> |
<> ⊕ u |
(-+) |
|
(+-) ∧ (-x) |
<(<> ⊕ u)(<<>>)> |
<<>> ⊕ <u> |
(+-) |
|
(-x) ∧ (-x) |
<(<<>>)(<<>>)> |
<> |
(-x) |
|
(x-) ∧ (-x) |
<(u)(<<>>)> |
<u> |
(x-) |
|
(x+) ∧ (-x) |
<(<u>)(<<>>)> |
u |
(x+) |
|
(+x) ∧ (-x) |
<(<>)(<<>>)> |
<<>> |
(+x) |
|
|
|
|
|
|
(--) ∧ (x-) |
<(<<>> ⊕ u)(u)> |
<<>> |
(+x) |
|
(++) ∧ (x-) |
<(<> ⊕ <u>)(u)> |
<u> |
(x-) |
|
(-+) ∧ (x-) |
<(<<>> ⊕ <u>)(u)> |
<> ⊕ u |
(-+) |
|
(+-) ∧ (x-) |
<(<> ⊕ u)(u)> |
<> ⊕ u |
(-+) |
|
(-x) ∧ (x-) |
<(<<>>)(u)> |
<u> |
(x-) |
|
(x-) ∧ (x-) |
<(u)(u)> |
<u> |
(x-) |
|
(x+) ∧ (x-) |
<(<u>)(u)> |
<<>> |
(+x) |
|
(+x) ∧ (x-) |
<(<>)(u)> |
<<>> |
(+x) |
|
|
|
|
|
|
(--) ∧ (x+) |
<(<<>> ⊕ u)(<u>)> |
<> ⊕ <u> |
(--) |
|
(++) ∧ (x+) |
<(<> ⊕ <u>)(<u>)> |
<> ⊕ <u> |
(--) |
|
(-+) ∧ (x+) |
<(<<>> ⊕ <u>)(<u>)> |
<<>> |
(+x) |
|
(+-) ∧ (x+) |
<(<> ⊕ u)(<u>)> |
u |
(x+) |
|
(-x) ∧ (x+) |
<(<<>>)(<u>)> |
u |
(x+) |
|
(x-) ∧ (x+) |
<(u)(<u>)> |
<<>> |
(+x) |
|
(x+) ∧ (x+) |
<(<u>)( <u>)> |
u |
(x+) |
|
(+x) ∧ (x+) |
<(<>)(<u>)> |
<<>> |
(+x) |
|
|
|
|
|
|
(--) ∧ (+x) |
<(<<>> ⊕ u)(<>)> |
<<>> |
(+x) |
|
(++) ∧ (+x) |
<(<> ⊕ <u>)(<>)> |
<<>> |
(+x) |
|
(-+) ∧ (+x) |
<(<<>> ⊕ <u>)(<>)> |
<<>> |
(+x) |
|
(+-) ∧ (+x) |
<(<> ⊕ u)(<>)> |
<<>> |
(+x) |
|
(-x) ∧ (+x) |
<(<<>>)(<>)> |
<<>> |
(+x) |
|
(x-) ∧ (+x) |
<(u)(<>)> |
<<>> |
(+x) |
|
(x+) ∧ (+x) |
<(<u>)(<>)> |
<<>> |
(+x) |
|
(+x) ∧ (+x) |
<(<>)(<>)> |
<<>> |
(+x) |
We stellen vast dat de conjunctie van enkelvoudige dubbelbits altijd commutatief is. Dit is een gevolg van het feit dat nevenschikking tussen welgevormde uitdrukkingen onafhankelijk is van de gebruikte volgorde.
Verder stellen we vast dat we uitsluitend (xx) bekomen voor het geval (+-) ∧ (++). De inbedding hiervan, namelijk (-+) ∧ (--), is echter niet (xx). De inbedding zien we dan verschijnen in de disjunctie hetgeen er duidelijk op wijst dat beide in feite deel uitmaken van een en dezelfde bewerkingsvorm.
Dit betekent ook dat er alleen nullen in de bitstring kunnen ontstaan van een conjunctie van gecollapste haakuitdrukkingen en nooit als gevolg van een conjunctie tussen welgevormde haakelementen.