Elementary linear algebriac formula for MUX operations.

Preface:

This document is devoted to derive the filter gates applied on the select lines of a multiplexer before entering the main AND circuit to produce the proper truth table. The document starts first by introducing the preliminaries using a miniaturized model, the 4-to-1 Multiplexer Model, the prototypical model of a MUX circuitry.

English:

For a 4-to-1 Multiplexer case. Let, $γ$ and $φ$ be symbols designating the select lines of the multiplexer And, $i$ be the symbols designating the input lines to the multiplexer, and $q$ designate the single output line from the MUX.

Lemma.01:

$$ \begin{bmatrix} γ_0 \\ γ_1 \\ γ_2 \\ γ_3 \\ \end{bmatrix} \land \begin{bmatrix} φ_0 \\ φ_1 \\ φ_2 \\ φ_3 \\ \end{bmatrix} = \begin{bmatrix} i_0 \\ i_1 \\ i_2 \\ i_3 \\ \end{bmatrix} $$

Lemma.02:

$$ \begin{bmatrix} i_0 \\ \end{bmatrix} \vee \begin{bmatrix} i_1 \\ \end{bmatrix} \vee \begin{bmatrix} i_2 \\ \end{bmatrix} \vee \begin{bmatrix} i_3 \\ \end{bmatrix} = q $$

Then,

For the first input, in case $q = i_0$:

$γ_0 = \neg{γ_0}$
$φ_0 = \neg{φ_0}$

For the second input, in case $q = i_1$:

$γ_1 = \neg{γ_1}$
$φ_1 = φ_1$

For the third input, in case $q = i_2$:

$γ_2 = γ_2$
$φ_2 = \neg{φ_2}$

For the forth input, in case $q = i_3$:

$γ_3 = γ_3$
$φ_3 = φ_3$

Generalized Formal first order logic:

First Assertion function: $a_0(n_i, n_s):\ n_i, n_s \rightarrow\ n_2 = log_2(n_i)$
Second Assertion function: $a_1(n_f, n_i):\ n_f, n_i \rightarrow\ n_f = n_i * n_s$

; where $n_i$ is the number of the input lines, $n_s$ is the number of select lines, and $n_f$ is the total number of the filter lines applied to the select lines for each input line.
Quantification formula:

$\forall{[i_{n_i},\ i_{n_i} \in I]}\ \forall{[s_{n_s},\ s_{n_s} \in S]}\ \exists{[f(s)_{n_s},\ f(s)_{n_s} \in F]};$ $[(f(s_{n_0})_{n_0} \land f(s_{n_1})_{n_1} \land ... \land f(s_{n_s})_{n_s}) \land i_{n_0}] \vee [(f(s_{n_0})_{n_0} \land f(s_{n_1})_{n_1} \land ... \land f(s_{n_s})_{n_s}) \land i_{n_1}] \vee ... \iff{i_{n_i}} \land a_0(n_i, n_s) \land a_1(n_f, n_i)$

; where $i_{n_i}$ is the input line at $n_i$, $s_{n_s}$ is the select line at $n_s$, and $f(s)_{n_s}$ is the filter function applied on the select line $s_{n_s}$ at $n_s$.

The quantification formula only holds when the assertion functions hold, and the circuitry selects an input line as an output.

Generalized Linear formula for the MUX:

$$ Circuit_{I} = \begin{bmatrix} f_{00}(s_0)_{i_0} \\ f_{10}(s_0)_{i_1} \\ . \\ . \\ . \\ \end{bmatrix} \land \begin{bmatrix} f_{01}(s_1)_{i_0} \\ f_{11}(s_1)_{i_1} \\ . \\ . \\ . \\ \end{bmatrix} \land ... \land \begin{bmatrix} f_{0{s}}(s_{s})_{i_0} \\ f_{(1)({s + 1})}(s_{s + 1})_{i_1} \\ . \\ . \\ f_{{n_i}{n_s}}(s_{n_s})_{i_{n_i}} \\ \end{bmatrix} \land \begin{bmatrix} i_0 \\ i_1 \\ i_2 \\ i_3 \\ . \\ . \\ . \\ i_{n_i} \end{bmatrix} $$

$$ Circuit_{II} = Circuit_I \vee \begin{bmatrix} Circuit_I - Circuit_I[i_0] \\ Circuit_I - Circuit_I[i_1] \\ Circuit_I - Circuit_I[i_2] \\ Circuit_I - Circuit_I[i_3] \\ . \\ . \\ . \\ Circuit_I - Circuit_I[n_i] \end{bmatrix} = \begin{bmatrix} i_0 \\ i_1 \\ i_2 \\ i_3 \\ . \\ . \\ . \\ i_{n_i} \end{bmatrix} = q_{output} $$