Daniel Gaffé
email: daniel.gaffe@inria.fr

Annie Ressouche
email: annie.ressouche@inria.fr

Algebras and Synchronous Language Semantics

Keywords: synchronous languages, synchrony paradigm, Boolean algebra, multi-valued algebras langages synchrones, hypothèse synchrone, algèbre de Boole, algèbre multi-valuées

In this report, we study different multi-valued algebras allowing to formally specify synchronous language semantics.

concurrent and deterministic applications. Synchronous program semantics build formal models and the definition of the theoretical framework used to express them is an important challenge according to the targeted goals (verification, compilation, etc..).

Fundamentals of Synchrony

Synchronous languages rely on the synchronous hypothesis which assumes a discrete logic time scale, made of instants corresponding to reactions of the system. All the events concerned by a reaction are simultaneous : input events as well as the triggered output events. As a consequence, a reaction is instantaneous (we consider that a reaction takes no time), there are no concurrent partial reactions and so determinism can be ensured.

Part of synchronous languages have an imperative syntax and are more dedicated to the design of safety-critical embedded applications where control management is the main concern. The most popular imperative synchronous language is surely Esterel [START_REF] Berry | The Foundations of Esterel[END_REF]. On the other hand, some synchronous languages are declarative ( [START_REF] Lagnier | Programming and verifying critical systems by means of the synchronous data-flow programming language lustre[END_REF][START_REF] Benveniste | Synchronous programming with events and relations : the signal language and its semantics[END_REF]) and are more dedicated to signal processing like applications. All these languages have a parallel operator (implicit or explicit) and the only communication and synchronization means between sub programs are signals 1 . Thus, each program has a finite set of input and output signals completed with local signals devoted to internal communication between concurrent sub programs.

Synchronous Languages Semantics

As synchronous programming main concern is the design of critical embedded applications, the need for semantics mathematically founded allowing formal verification and exhaustive testing appeared very early. A fundamental concept of the synchronous paradigm is the notion of reaction. Indeed, synchronous programs react to input events by emitting output events and reach a new state. A program can be viewed as a possibly infinite sequence of reactions.

Basically, events are signals in a current environment (external and internal) which have a status (present or absent), and semantics formally compute an output environment according to an input one for each reaction. Let

Each transition P

O -→ I δ (P) is structurally computed from the body instruction of the program according to rewriting rules defined for each construct of the language. These rules allow the computation of output environment from input ones. All the synchronous languages have an operator emit or some variant, to change the environment. Indeed, it allows to change the status of signal in environment from absent to present. A logical coherence law helps to assign status to signals. This law says that: " a signal S is present in a reaction if and only if an emit S statement is executed" ( [START_REF] Edwards | Compiling Esterel[END_REF]). Then rewriting rules for operators formalize this signal coherence laws.

Algebras as Mathematical Framework

An elegant means to express these rewriting rules aforementioned is to use the S.O.S style defined by G. Plotkin ([33]). S.O.S rules are deduction rules of the shape:

Premiss(1) Premiss(2) ... Premiss(n) Conclusion

meaning that:

i=n i=1
Premiss(i) ⇒ Conclusion. As said before, synchronous languages supply a parallelism operator ( ). We express the rule for parallel operator of Esterel language, as an example:

p 1 O 1 -→ I p ′ 1 , p 2 O 2 -→ I p ′ 2 p 1 p 2 O 1 O 2 ----→ I p ′ 1 p ′ 2
This example is representative of synchronous language parallel rules. We can see that we need to perform a specific operation of union of environments (O 1 O 2 ) which "unify" the information concerning the status of signals in respective O 1 and O 2 output environments. If the status of S in O 1 is 0 (absent) and is 1 in O 2 (present), in O 1 O 2 , the status of S should be 1, in a Boolean consideration of signal status. Hence, to formally define semantics rules, we need to give an algebraic framework to represent both signal status and operations on them and on environments. The natural first approach considers a Boolean algebra with ∧, ∨ and ¬ operators. Then, starting from the fact that all signals (except input signals present in the reaction) have status 0 in the initial environment, the O 1 O 2 operation turns out to be the ∨ operation on respective signal status in O 1 and O 2 .

According to synchrony paradigm, correct programs should be both reactive and deterministic. Reactivity means that a synchronous program must always react to any input event sequence, possibly in doing nothing. Determinism means that computations are reproducible and then a program yields always the same output event sequence in reaction to an input sequence. Such programs are called logically correct (see [START_REF] Berry | The Constructive Semantics of Pure Esterel[END_REF]). On another hand, a challenging phenomenon synchronous language semantics have to deal with is the notion of causality. Causality means that for each event generated in a reaction, there is a causal chain of events leading to this generation. No causal loop may occur.

To take into account these two aspects of synchrony paradigm, G. Berry [START_REF] Berry | The Constructive Semantics of Pure Esterel[END_REF] introduced constructive semantics for the Esterel language. But, in these semantics the mathematical framework is no more a Boolean algebra but a ternary algebra. Finally, 4-valued algebras have been considered to check causality with fixpoint iterative techniques ( [START_REF] Schneider | Causality analysis of synchronous programs with delayed actions[END_REF]) or to get separated compilation means relying on semantics definition ( [START_REF] Ressouche | Modular Compilation of a Synchronous Language[END_REF]).

The aim of this report, is to answer the question: what algebra to define synchronous language semantics allowing both to deduce compilation means and to build formal models for verification.

This report is organized as follows: next section (section 2) introduces 3-valued and 4-valued algebras and studies their respective properties with respect to our concern. We particularly highlight a specific 4-valued algebra (Algebra5) which offers to define a semantics we can rely on both to perform a separated compilation and to get verification ability. In section 3, we show that bilattice structure of algebras allows to deduce a nice encoding of 4-valued algebras into Boolean pairs, in order to implement semantics rules as compilation technique. Section 4 concludes. This report contains a huge appendix gathering all the demonstrations concerning bilattice properties and algebra properties of Algebra5.

RR n°8138

2 Synchronous Languages'multi-valued Algebras A behavioral semantics was first defined for Esterel. It is specified using S.O.S rules and considers a Boolean algebra to represent signal status. It defines globally each reaction. The values of output environment and derivative are solutions of fixpoint equations resulting from signal coherence law application and instantaneous information exchange between concurrent statements. But, the equations involve non monotonic operators (the negative one essential to define local signal rules). Thus existence and computation of fixpoints cannot be ensured. As a consequence, it is ineffective. Moreover, it cannot characterize logically correct programs. It just give a formal definition of program behaviors. In complement, an operational semantics is needed to compile programs and equivalence between the two semantics has to be established.

Then, constructive semantics characterize logically correct programs and solve the causality checking problem. Their purpose is to replace "the idea of checking assumptions about signal status by the idea of propagating facts about signal status" 2 . A constructive version of behavioral semantics has been defined and also a constructive circuit semantics that translates each program into constructive circuits. In this constructive approach, a 3-valued algebra has been used to represent signal status. On another hand, declarative synchronous language as Signal( [START_REF] Benveniste | Synchronous programming with events and relations : the signal language and its semantics[END_REF]) also considers a ternary algebra to represent signal status.

3-valued Algebras

The general multi-valued algebra are introduced by Emil Post in 1921 [START_REF] Post | Introduction to a general theory of elementary propositions[END_REF][START_REF] Davis | Solvability, provability, definability : the collected works of Emil L Post[END_REF]. Concerning the synchronous languages,one has proposed to extend first the present (1) and absent (0) status of each signal with bottom (⊥). Intuitively, ⊥ represents the unknown status. Thus, a 3-valued algebra {⊥, 0, 1} is considered to represent signal status. More generally, 3-valued algebras has been introduced several decades ago to reasoning with uncertain knowledge. In these approaches, an ordering gives them a lattice structure. As they are mainly logic models, they have ∧, ∨ ,¬ and → operators.

3-valued Algebras as Lattices

3-valued Algebras Candidates

Lots of authors are well-known to develop a 3-valued algebra. Let's begin with Lukasiewicz [START_REF] Łukasiewicz | O logice tròjwartościowej[END_REF][START_REF] Łukasiewicz | Selected Writings[END_REF], and later Kleene [START_REF] Cole | Introduction to metamathematics[END_REF], Goëdel [START_REF] Gödel | Zum intuitionistischen Aussagenkalkül[END_REF][START_REF] Gödel | Collected Works : Publications 1929-1936[END_REF], [START_REF] Markov | A contructive logic[END_REF][START_REF] Vakarelov | Notes on n-lattices and constructive logic with strong negation[END_REF] (classicaly called Nelson), Jaskowski [START_REF] Jaskowski | Propositional calculus for contradictory deductive systems[END_REF][START_REF] Karpenko | Jaskowski's criterion and three-valued paraconsustent logics[END_REF] and Heyting [START_REF] Heyting | Logic and foundations of mathematics. Wolters-Noordhoff series of monographs and textbooks on pure and applied mathematics[END_REF]:

1 0 ⊥ 1 1 1 1 0 1 0 ⊥ ⊥ 1 ⊥ ⊥ 1 0 ⊥ 1 1 0 ⊥ 0 0 0 0 ⊥ ⊥ 0 ⊥ ¬ 1 0 0 1 ⊥ ⊥
∨, ∧ and ¬ are common to the five algebras. The difference concerns the imply operator. In fact, recent works have showed the link between semi-Heyting algebras and Gödel algebra's family [START_REF] Abad | Semi-heyting algebras termequivalent to gà ¶del algebras[END_REF]. Moreover Nelson-Markov'imply can be deduced from Lukasiewicz'imply or the opposite [START_REF] Ciucci | Logiques tri-valuées de l'information incomplète et logique épistémique[END_REF]:

x → L y = (x → N y) ∧ (¬y → N ¬x) x → N y = x → L (x → L y) 2 G.Berry in [7] RR n°8138 → 1 0 ⊥ 1 1 0 ⊥ 0 1 1 1 ⊥ 1 ⊥ 1 → 1 0 ⊥ 1 1 0 ⊥ 0 1 1 1 ⊥ 1 ⊥ ⊥ → 1 0 ⊥ 1 1 0 ⊥ 0 1 1 1 ⊥ 1 0 1 → 1 0 ⊥ 1 1 0 ⊥ 0 1 1 1 ⊥ 1 0 1 Lukasiewicz (L3) Kleene (K3) Gödel (G3) Heyting (He3) → 1 0 ⊥ 1 1 0 ⊥ 0 1 1 1 ⊥ 1 1 1 → 1 0 ⊥ 1 1 0 ⊥ 0 1 1 1 ⊥ 1 0 ⊥ Nelson (N3) Jaskowski (J3)
Ciucci and Dubois [START_REF] Ciucci | Three-valued logics for incomplete information and epistemic logic[END_REF] explain the implication operator (binary connector) can be defined by three rules:

• if x ≤ y then y → z ≤ x → z • if x ≤ y then z → x ≤ z → y • 0 → 0 = 1 and 1 → 1 = 1 and 1 → 0 = 0
With this definition, authors explain that 14 definitions of the imply'operator are finally possible.

Besides only Kleene'imply x → y can be defined as ¬x y.

In Lukasiewicz, ⊥ is encoding by the value "2". So the order 0 ≤ 1 ≤ ⊥ is implicit. According to Moisil [START_REF] Gr | The Algebraic Theory of Switching Circuits[END_REF], Lukasiewicz " " and " " are defined with this encoding by an arithmetic equation where "+" and "." are the classical arithmetic operators:

• x y = 2.x 2 .y 2 + x.y.(x + y + 1) + x + y • x y = x 2 .y 2 + 2.x.y.(x + y + 1)
But, concerning ¬x and x → y, Moisil says nothing. Following Moisel, in 3-valued algebras, operators can be expressed as polynomials with weights in Z/3Z (integer field modulo 3). Then, a binary operators can be characterized by a polynomial of the shape: α.x 2 .y 2 + β .x 2 .y + δ .x 2 + ε.x.y 2 + φ .x.y + γ.x + λ .y 2 + µ.y + ν; a unary one by a polynomial of the shape: δ .x 2 + γ.x + ν. To determine polynomials for ¬x and x → y, we compute which weights are solutions of the equations:

δ .x 2 + γ.x + ν = ¬x (mod3) α.x 2 .y 2 + β .x 2 .y + δ .x 2 + ε.x.y 2 + φ .x.y + γ.x + λ .y 2 + µ.y + ν = x → y (mod3)
where the weight of each product are equal to 0, 1 or 2. Solutions are:

¬x = 2.x + 1 x → y = x 2 .y 2 + 2.x 2 .y + 2.x.y 2 + 2.x.y + 2x + 1 = x 2 .y 2 + 2.x.y.(x + y + 1) + 2.x + 1
The proof is detailed in the appendix B.

RR n°8138

Differently Gödel algebra has an equational view too. Here ⊥ is considered less than 1 and greater than 0:

• x y = max(x, y)

• x y = min(x, y)

• x → y = 1 if x ≤ y, = y otherwise
Also we can cite Bochvar [START_REF] Bochvar | On a three-valued logical calculus and its applications to the analysis of the paradoxes of the classical extended functional calculus (in russian)[END_REF] (B3) (sometimes called weak Kleene):

1 0 ⊥ 1 1 1 ⊥ 0 1 0 ⊥ ⊥ ⊥ ⊥ ⊥ 1 0 ⊥ 1 1 0 ⊥ 0 0 0 ⊥ ⊥ ⊥ ⊥ ⊥ ¬ 1 0 0 1 ⊥ ⊥ → 1 0 ⊥ 1 1 0 ⊥ 0 1 1 ⊥ ⊥ ⊥ ⊥ ⊥
We can cite Sobocinski [START_REF] Sobocinski | Axiomatization of a partial system of three-valued calculus of propositions[END_REF] (S3):

1 0 ⊥ 1 1 1 1 0 1 0 0 ⊥ 1 0 ⊥ 1 0 ⊥ 1 1 0 1 0 0 0 0 ⊥ 1 0 ⊥ ¬ 1 0 0 1 ⊥ ⊥ → 1 0 ⊥ 1 1 0 0 0 1 1 1 ⊥ 1 0 ⊥
And finally, we can cite Sette [START_REF] Sette | On propositional calculus p1[END_REF][START_REF] Alexej | Algebraic study of sette's maximal paraconsistent logic[END_REF] (Se3). This logic has five operators: → and ¬ are primitive. The others can be deduced:

1 0 ⊥ 1 1 1 1 0 1 0 1 ⊥ 1 1 1 1 0 ⊥ 1 1 0 1 0 0 0 0 ⊥ 1 0 1 ¬ 1 0 0 1 ⊥ 1 ¬ ′ 1 0 0 1 ⊥ 0 → 1 0 ⊥ 1 1 0 1 0 1 1 1 ⊥ 1 0 1
In all these algebras (except Lukasiewicz algebra) , ⊥ the undefined symbol, is considered implicitly or explicitly as "1/2". So 0 ≤ ⊥ ≤ 1. We will called this order: "Boolean order ≤ B " in the following of this article.

To summarize, we have to understand the 3-valued logic or fuzzy logic domain is very wide and it is a specific branch of Computer Science research with its workshops and journals. We will never exhaustive, but fortunately many authors try to give a global view of this domains [START_REF] Ciucci | Three-valued logics for incomplete information and epistemic logic[END_REF][START_REF] Krassimir | On Intuitionistic Fuzzy Sets Theory[END_REF][START_REF] Bergmann | An introduction to many-valued and fuzzy logic. Semantics, algebras, and derivation systems[END_REF] or make a state of arts around famous authors. We can cite [START_REF] Łukasiewicz | Selected Writings[END_REF] about Lukasiewicz or [START_REF] Melvin | Fitting. Kleene's three-valued logics and their children[END_REF] about Kleene, in this way.

On another hand, these algebras are complete distributive lattices according to the following definition: Definition 1. A lattice is a partially ordered set (L,≤) in which each pair a, b has a least upper bound (a ∨ b) and a greatest lower bound (a ∧ b). L is complete if any subset X ⊆ L has a least upper bound and a greatest lower bound. L is distributive if it satisfies the distributive law

: x ∨ (y ∧ z) = (x ∨ y) ∧ (x ∨ z) or the inverse equivalent law.
The elements a ∨ b and a ∧ b are usually called the meet and join of a and b. This characterization as lattices allows to consider 3-valued algebras as models for 3-valued logic. For instance, Lukasiewicz algebra is a model for propositional calculus and it as been proved ( [START_REF] Iturrioz | An axion system for three-valued lukasiewicz propositional calculus[END_REF]) that any formula derivable in the propositional calculus is valid in 3-valued Lukasiewicz algebra. Applications of these 3-valued algebras are many in non classical logic domain as synchronous language semantics. RR n°8138

Signal language

Signal [START_REF] Benveniste | Synchronous programming with events and relations : the signal language and its semantics[END_REF] considers a 3-valued algebra to compute signal status: present, absent and ⊥. Signal language has no global clock, contrary to others synchronous languages. Hence, signal status have a specific interpretation: ⊥ means that the signal has no clock i.e is not defined. Present and absent have the usual meaning for signal having clock. Status computing is performed in Z/3Z with +1, -1 and 0 respectively encoding present, absent and ⊥. With this encoding, each operator of the language has a ternary equation representation:

¬a : -a a b : ab(ab -a -b -1) a b : ab(1 -a -b -ab) when b : -b -b 2 a when b : a(-b -b 2 ) a de f ault b : a + (1 -a 2 )b a$1initx0 : a 2 x with x ′ (xnext) = a + (1 -a 2 )x
The associated algebra has particular properties:

a + a = -a a + a + a = 0 a 2n = a 2 a 2n+1 = a a.(1 -a 2 ) = 0 ( f (a 2 )) n = f (a 2 ) (1 -a 2 ) 2 = 1 -a 2
These properties are used to compute the clock dependencies and deduce a possible clock order. From , and ¬ algebraic definition, we can deduce their truth table. With the previous encoding, we have:

1 0 ⊥ 1 1 1 ⊥ 0 1 0 ⊥ ⊥ ⊥ ⊥ ⊥ 1 0 ⊥ 1 1 0 ⊥ 0 0 0 ⊥ ⊥ ⊥ ⊥ ⊥ ¬ 1 0 0 1 ⊥ ⊥
It turns out that it is Bochvar algebra.

3-valued Algebras as CPOs

But totally ordered algebras and lattice structure do not always fit synchronous language semantics requirements, particularly concerning fixpoint computations. Mainly because the ≤ B order does not reflect how the information about variable computation increases. In constructive semantics, a program is translated into a Boolean equation system and output environment is its least fixpoint solution. 3-valued algebra approach allows to characterize the operational semantics of the synchronous compiler: its goal is to transform and stabilize all ⊥ status of internal and output signals to 0 or 1. Thus, a 3-valued algebra more appropriate to formalize program computations has been considered.

3-valued Algebras Candidates

As a matter of fact, we have to wait Scott [START_REF] Scott | Logic and programming languages[END_REF] to reconsider the order relation by defining ≤ as:

RR n°8138

x ≤ y iff either x = ⊥ or x = y true false Scott called this order relation x ≤ y by "x contained in y". In our view ( also following multi-valued logic community), we call ≤ K this order relation because it characterizes the degree of knowledge. We can note that 0 and 1 are incomparable in this relation because they have the same weight of knowledge.

Indeed, Scott Domain theory was devoted to partial algebraic data representation, where knowledge about the elements is ordered. The goal is to interpret the elements of such domains as pieces of information or (partial) results of a computation, where elements that are higher in the order extend the information of the elements below them in a consistent way.

Formally, a non-empty partially ordered set (D, ≤) is called a Scott domain if the following hold3 :

• D is directed complete, i.e. all directed subsets of D have a supremum;

• D is bounded complete, i.e. all subsets of D that have some upper bound have a supremum;

• D is algebraic, i.e. every element of D can be obtained as the supremum of a directed set of compact elements of An important result is the Kleene fixpoint theorem: If f is a continuous function on a poset D then it has a least fixed point, given as the least upper bound of all finite iterations of f on the least element ⊥: ∀n ∈ N f n (⊥).

Historically, Scott domain theory has been introduced to define the denotational semantics of programming languages. The denotational semantics defines a semantic domain for each syntactic category of the language, and a valuation function for each syntactic category which assigns a denotation in the appropriate semantic domain to each program. It turns out that representing semantic domains as Scott domains allows to compute program meaning as the limit of a sequence of approximations and Kleene fixpoint theorem gives an effective means to compute this limit.

A simple special case of Scott domain is known as flat domain. This consists of a set of incomparable elements, such as the integers, along with a single "bottom" element considered smaller than all other elements. A particular flat domain B ⊥ (see figure 2.3.1), has been used to define synchronous language semantics, particularly Esterel semantics.

Esterel language

As already mentioned, the constructive semantics of Esterel language [START_REF] Berry | The Constructive Semantics of Pure Esterel[END_REF] relies on B ⊥ Scott domain to compile programs. But ⊥ has not the same interpretation as for Signal language. Esterel has a global clock and at each instant of its clock, signal must be stabilized as present or absent. ⊥ has been introduced to allow the definition of an operational semantics based on Scott domain B ⊥ , in which the computation of signal status converge for all signals. Given an initial signal environment where unknown signals have status ⊥, the constructive semantics computes for each statement two predicates must and cannot. must sets the status of signal instantaneously emitted in the statement to 1 while cannot sets the status of signal that are not emitted in the statement to 0. Indeed a statement is composed of sub statements, and the status of signal S is set to 1 if it exists one emit S sub statement; but it is set to 0 if there is no emit S in all the sub statements.

This computation of absence of signals at each instant does not allow to rely on constructive semantics to get a separated compilation. Effectively, in a separated compilation, only a partial set of sub statements is considered and so the status of all signals cannot be determined. Because for those having ⊥ as status it could exist an emit for them in a sub program not considered. We propose a solution ( [START_REF] Ressouche | Modular Compilation of a Synchronous Language[END_REF]) based on 4-valued algebra to represent signal status. As a matter of fact, we need a semantics which keeps ⊥ status for unknown signals in the environment of a sub statement. Then we must unify all these sub environments and so we can get incompatible status (⊤) for some signals. Then, we need to represent signal status in a 4-valued algebra.

4-valued algebra

3-valued algebras are neither able to characterize status conflict between sub programs nor to allow a separated compilation. Thus we propose a new extension for status'signals: error (⊤) and then we are lead to consider 4-valued algebra.

4-valued logic have been first considered by Belnap [START_REF] Belnap | A useful four-valued logic[END_REF] to represent the knowledge in AI systems. In such deductive systems, the information need to fall in true, false, uncertain or conflicting truth values. Thus, 4-valued logic have four truth values: ⊥, 0, 1 and ⊤. In section 2.1, we saw that constructive semantics have the ability to deal with causality. Nevertheless, causality checking remains a global process applied at program level and prevents to benefit from the structural rules of the semantics to separately compile programs.

The semantics we propose to rely on for both verification and compilation purposes, associates a 4valued algebra equation system (E ) to each program instead of a Boolean one as traditional constructive semantics do. In each reaction, the equation system E helps us to compute an output environment from an input one: E : E = F(E). E is built according to semantics rules defined for each operator of the language. This means that at least the algebra must have usual logical operators: ¬, ⊞ , ⊡ which should have a Boolean like definition to be able to express the status of output and local signals from input and local signal status. Moreover, for the parallel operator (P 1 P 2 ) for instance, let E 1 and E 2 be the respective equation systems of P 1 and P 2 , then the overall equation system is the "unification" of E 1 and E 2 . This operation, we call Unify (⊔), performs the unification of signal status in the resulting equation system. For instance, assume that signal S has an equation S 1 = f 1 ( -→ v ) in E 1 to compute its status in P 1 , and an equation S 2 = f 2 ( -→ w ) in E 2 . Then the equation system for P 1 P 2 will have an equation

S = f 1 ( - → v ) ⊔ f 2 ( - → w ).
Intuitively, this operation must perform the union of the information concerning S status respectively in P 1 and P 2 . Then, the semantics computes the unique least fixpoint E = F(E) in the 4-valued algebra considered. To ensure that least fixpoints exist and can be computed, we need a 4-valued algebra with operators making F monotonic. To this aim, we also consider the symmetric operator of ⊔ , called ⊓ .

On another hand, one of the motivation for introducing this 4-valued framework is to rely on mathematical semantics to compile synchronous programs. The goal we would reach is to get a separated way to perform compilation. We know that we cannot totally rely on any semantics because synchronous language semantics cannot be both modular and causal [START_REF] Huizing | Semantics of reactive systems in abstract time[END_REF]. Since Esterel circuit semantics, causality is checked by sorting the Boolean equation system. Any causal program has a cycle free circuit. But, causality can be only check on the overall program, because two cycle free equation systems corresponding to 2 sub programs can yield a cyclic global equation system. This strong drawback is mainly due to the fact that this circuit semantics computes total orders on Boolean equation systems, i.e equation systems in RR n°8138 which ⊥ status (undetermined) has been changed to 0 (absent) to sort equation systems. Indeed variable dependencies in an equation system are only partial orders. In [START_REF] Ressouche | Modular Compilation of a Synchronous Language[END_REF][START_REF] Ressouche | Compilation Modulaire d'un Langage Synchrone[END_REF], we propose a technique to sort 4-valued equation systems with respect to their partial orders allowing to merge two equation systems and deduce the overall ordering from the previously computed ordering for each system. Doing that, the compilation mechanism falls in two phases: first, a phase where sorted equation systems are computed in a modular way (applying the semantics rules). During this phase we generate sorted 4-valued algebra equation systems because we want to have the ability to unify equation systems to get a global one. So, we don't decide that ⊥ becomes 0 at this level 4 . On another hand, if a signal has status 0 in an equation system and status 1 in another, the unification must compute ⊤ (error) as resulting status. Thus, a second phase is needed to generate final output code. This phase ensures that as soon as a variable that can be ⊤ appears, the compilation fails. Otherwise, ⊥ status are changed to 0 and the values are propagated as usual in a Boolean equation system. Phase 2 is the very last stage of compilation and is not done at each reaction. After this phase, there is no return possible and we are no more modular. To achieve phase 2, we need an operator called finalization (FL for short) not defined for ⊤ and which transform ⊥ into 0:

x FL(x) 1 1 0 0 ⊤ - ⊥ 0

4-valued Algebras Candidates

Several algebras are possible to handle the 4-valued signals: we present and compare here 5 versions whose aims differ. ⊔ and ⊓ are common. Perhaps ⊓ is useless to compilation concern, but it is the dual operator of ⊔ operator and is useful to prove distributive properties of algebras.

Common

⊔ 1 0 ⊤ ⊥ 1 1 ⊤ ⊤ 1 0 ⊤ 0 ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ 1 0 ⊤ ⊥ ⊓ 1 0 ⊤ ⊥ 1 1 ⊥ 1 ⊥ 0 ⊥ 0 0 ⊥ ⊤ 1 0 ⊤ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥
4 because an undefined status can increase either to present or to absent in the unification operation

RR n°8138 LE2008 ⊞ 1 0 ⊤ ⊥ 1 1 ⊤ ⊤ 1 0 ⊤ 0 ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ 1 0 ⊤ ⊥ ⊡ 1 0 ⊤ ⊥ 1 1 ⊥ 1 ⊥ 0 ⊥ 0 0 ⊥ ⊤ 1 0 ⊤ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ x ¬ x 1 0 0 1 ⊤ ⊥ ⊥ ⊤ Algebra2 ⊞ 1 0 ⊤ ⊥ 1 1 1 ⊤ ⊥ 0 1 0 ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ ⊥ ⊥ ⊤ ⊥ ⊡ 1 0 ⊤ ⊥ 1 1 0 ⊤ ⊥ 0 0 0 ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ ⊥ ⊥ ⊤ ⊥ x ¬ x 1 0 0 1 ⊤ ⊤ ⊥ ⊥ Algebra3 ⊞ 1 0 ⊤ ⊥ 1 1 1 ⊤ 1 0 1 0 ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ 1 ⊥ ⊤ ⊥ ⊡ 1 0 ⊤ ⊥ 1 1 0 ⊤ ⊥ 0 0 0 ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ ⊥ 0 ⊤ ⊥ x ¬ x 1 0 0 1 ⊤ ⊤ ⊥ ⊥ Algebra4 ⊞ 1 0 ⊤ ⊥ 1 1 1 1 1 0 1 0 ⊤ ⊥ ⊤ 1 ⊤ ⊤ ⊤ ⊥ 1 ⊥ ⊤ ⊥ ⊡ 1 0 ⊤ ⊥ 1 1 0 ⊤ ⊥ 0 0 0 0 0 ⊤ ⊤ 0 ⊤ ⊤ ⊥ ⊥ 0 ⊤ ⊥ x ¬ x 1 0 0 1 ⊤ ⊤ ⊥ ⊥ Algebra5 ⊞ 1 0 ⊤ ⊥ 1 1 1 1 1 0 1 0 ⊤ ⊥ ⊤ 1 ⊤ ⊤ 1 ⊥ 1 ⊥ 1 ⊥ ⊡ 1 0 ⊤ ⊥ 1 1 0 ⊤ ⊥ 0 0 0 0 0 ⊤ ⊤ 0 ⊤ 0 ⊥ ⊥ 0 0 ⊥ x ¬ x 1 0 0 1 ⊤ ⊤ ⊥ ⊥
• LE2008 algebra has been presented in [START_REF] Ressouche | Modular Compilation of a Synchronous Language[END_REF] and [START_REF] Ressouche | Modular Compilation of a Synchronous Language[END_REF]. We defined an imperative synchronous language (Light Esterel, LE for short) whose compiler applies the rules of a LE2008 algebra based semantics. This algebra does not make difference between the Unification ( ⊔ ) and Plus ( ⊞ ) operators on signals. But, LE2008 algebra cannot ensure that the function representing the LE2008 equation system associated to a program is monotonic since the operator ¬ is not.

• Algebra2 is a possible first generalization of classical Boolean properties between 0 and 1. This algebra propagates the error status (⊤).

• Algebra3 differs from the previous algebra by the behavior of ⊥: in our view ⊥ can become 0 or 1. So we must have 1 ⊞ ⊥ = 1 (because if ⊥ becomes 1 or 0, we want the sum results in 1). But, it is not the case for 0 ⊞ ⊥ which must have the possibility to become 1 if ⊥ becomes 1 too. Thus 0 ⊞ ⊥ = ⊥.

• In algebra4, each binary operator has a specific absorbing element (⊤ for ⊔ , ⊥ for ⊓ , 1 for ⊞ and 0 for ⊡ ). This algebra no more propagates error status.

• Algebra5: A variant of Algebra4 where ⊤ ⊞ ⊥ equals 1 and ⊤ ⊡ ⊥ equals 0. These strange modifications a priory, will have an explanation in section 2.4.2 where we will see that they offer the ability to provide Algebra5 with a bilattice structure.

Table 1 summarizes the logical properties of the algebras defined in section 2.4.1. Concerning Alge-bra5, all properties are demonstrated in appendix A.2.

Properties

Alg.LE2008 Alg.2 Alg.3 Alg.4 Alg.5

⊥ ⊔ x = x YES YES YES YES YES ⊥ ⊓ x = ⊥ - YES YES YES YES 1 ⊞ x = 1 (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) YES YES YES YES YES (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) YES YES YES YES YES (x ⊞ y) ⊞ z = x ⊞ (y ⊞ z) YES YES YES YES YES (x ⊡ y) ⊡ z = x ⊡ (y ⊡ z) YES YES YES YES YES (x ⊞ y) ⊡ z = (x ⊡ z) ⊞ (y ⊡ z) YES YES YES no YES (x ⊡ y) ⊞ z = (x ⊞ z) ⊡ (y ⊞ z) YES YES YES no YES (x ⊔ y) ⊓ z = (x ⊓ z) ⊔ (y ⊓ z) - YES YES YES YES (x ⊓ y) ⊔ z = (x ⊔ z) ⊓ (y ⊔ z) - YES YES YES YES (x ⊔ y) ⊞ z = (x ⊞ z) ⊔ (y ⊞ z) YES YES YES YES YES ¬(x ⊞ y) = ¬x ⊡ ¬y YES YES YES YES YES ¬(x ⊔ y) = ¬(x) ⊔ ¬(y) YES YES YES YES YES ¬(x ⊓ y) = ¬(x) ⊓ ¬(y) - YES YES YES YES

Bilattice Property of 4-valued Algebra

Indeed, we are interesting in algebras provided with a bilattice structure. Mainly because this framework considers two orderings: a Boolean ordering and a knowledge ordering which fit our concern.

Bilattice Theory

Bilattices were introduced by Ginsberg [START_REF] Ginsberg | Multivalued logics: A uniform approach to inference in artificial intelligence[END_REF] as the underlying framework for AI 5 inference systems. Bilattices are mathematical structures with two distinct orders usually denoted ≤ B and ≤ K . ≤ B expresses level of truth and is useful for truth evaluation, ≤ K represents the level of information or knowledge.

Definition 2. (Ginsberg [START_REF] Ginsberg | Multivalued logics: A uniform approach to inference in artificial intelligence[END_REF]) A bilattice is a structure (B, ≤ B ≤ K , ¬) consisting of a non empty set B, partial orderings ≤ B and ≤ K and a mapping ¬ : B → B such that:

1. (B, ≤ B ) and (B, ≤ K ) are complete lattices 2. x ≤ B y ⇒ ¬y ≤ B ¬x, ∀x, y ∈ B 3. x ≤ K y ⇒ ¬x ≤ K ¬y, ∀x, y ∈ B 4. ¬¬x = x, ∀x ∈ B
If ≤ B is a lattice ordering, let 0 (resp. 1) denotes the least(resp. upper) element. x ⊞ y (resp, x ⊡ y) is the join (resp. meet) of x and y. Similarly , if ≤ K is a lattice ordering, we denotes ⊥ (resp. ⊤) the least (resp. upper) element. x ⊔ y ( resp. x ⊓ y) is the join (resp. meet) of x and y.

A bilattice satisfies the interlacing conditions if:

1. x ≤ B y ⇒ x ⊔ z ≤ B y ⊔ z and x ⊓ z ≤ B y ⊓ z 2. x ≤ K y ⇒ x ⊞ z ≤ K x ⊞ z and x ⊡ z ≤ K x ⊡ z
In other words, a bilattice is interlaced if the lattice operations of one ordering are monotonic with respect to the other ordering and vice versa.

A bilattice is distributive if all twelve distributivity laws associated with the 4 operations ⊞ , ⊡ , ⊔ and ⊓ hold. All distributive bilattice are interlaced. Bilattice structure is a framework well suited to our concern, since it allows to separate two orderings (Boolean and knowledge) and then to be able to compute equation systems solutions. According to bilattice formalism, we introduce the following orders and we study their properties (see table 2) in the different algebras we have considered. LE2008 algebra, historically, has only the ≤ B ordering.

Application to 4-valued Algebras

x ≤ K (x ⊔ y) - YES YES YES YES x ≤ K y => (x ⊔ z) ≤ K (y ⊔ z) - YES YES YES YES x ≤ K y => (x ⊓ z) ≤ K (y ⊓ z) - YES YES YES YES ⊥ ≤ K (x ⊔ y) ≤ K ⊤ - YES YES YES YES ⊥ ≤ K (x ⊓ y) ≤ K ⊤ - YES YES YES YES x ≤ K y => ¬x ≤ K ¬y - YES YES YES YES x ≤ B (x ⊞ y) no no no YES YES (x ⊡ y) ≤ B x no no no YES YES x ≤ B y => (x ⊞ z) ≤ B (y ⊞ z) YES no no YES YES x ≤ B y => (x ⊡ z) ≤ B (y ⊡ z) YES no no YES YES 0 ≤ B (x ⊞ y) ≤ B 1 YES YES YES YES YES 0 ≤ B (x ⊡ y) ≤ B 1 YES YES YES YES YES x ≤ B y => ¬y ≤ B ¬x YES YES YES YES YES x ≤ B y and z ≤ B t => x ⊔ z ≤ B y ⊔ t YES YES YES YES YES x ≤ B y and z ≤ B t => x ⊓ z ≤ B y ⊓ t - YES YES YES YES x ≤ K y and z ≤ K t => x ⊞ z ≤ K y ⊞ t - YES YES no YES x ≤ K y and z ≤ K t => x ⊡ z ≤ K y ⊡ t - YES YES no YES
⊥ ≤ K 0 ≤ K ⊤ ⊥ ≤ K 1 ≤ K ⊤ 0 ≤ B ⊥ ≤ B 1 0 ≤ B ⊤ ≤ B 1
Let us denote ξ = {⊥, 0, 1, ⊤}. Algebra(4,5) can be seen as the bilattices (ξ , ≤ B , ≤ K , ¬) according to the previous definition of ≤ B and ≤ K orderings. But Algebra(2,3) cannot. Indeed, (ξ , ≤ B ) is a complete lattice with 0 and 1 as extremums and so is (ξ , ≤ K ) with ⊥ and ⊤ as extremums for Algebra [START_REF] Pigozzi | Multi-valued logic programming semantics: An algebraic approach[END_REF][START_REF] Benveniste | Synchronous programming with events and relations : the signal language and its semantics[END_REF]. But, looking at table 2, we can see that (ξ , ≤ B ) is not a lattice for Algebra [START_REF] André | Synccharts: un modèle graphique synchrone pour système réactifs complexes[END_REF][START_REF] Krassimir | On Intuitionistic Fuzzy Sets Theory[END_REF]. According to definition of ¬ operator (see section 2.4.1), for Algebra(4,5) we have: x ≤ B y ⇒ ¬y ≤ B ¬x, since only 0 and 1 are comparable with respect to ≤ B ordering; x ≤ K y ⇒ ¬x ≤ K ¬y, since only ⊥ and ⊤ are comparable with respect to ≤ K ordering; ¬¬x = x. Thus, Algebra(4,5) are bilattices.

In Algebra(4,5), the negation preserves the ≤ K order. This is this expression that ≤ K helps us to characterize the different degrees in the knowledge about element of the algebra. Hence, while it is expected that negation invert the notion of truth from a Boolean point of view, the role of negation with respect to ≤ K is somewhat transparent, we know no more and no less about x than about ¬x. As a consequence, Algebra(4,5) with this bilattice structure suits well our concern. We want to find out the appropriate mathematical framework such that algebra equation system solutions can be computed with a fixpoint. In particular, the separation between Boolean consideration and knowledge one is fundamental to make our approach works. Fixpoint computation refines the status of signal from ⊥ to ⊤ according to ≤ K ordering, so we are interested by monotony only with respect to knowledge order. Nevertheless, the ≤ B order is also mandatory to be able to compute Boolean like ( ⊡ , ⊞ ) operations on signal status which can appear in equations.

Distributivity is an important property in bilattice theory in general, but it our case, it is really significant because we can apply these laws to solve 4-valued algebra equation systems. The only algebra where the twelve distributive laws hold is Algebra5 (see table 1). So, we can consider that Algebra5 is a distributive bilattice and is the only one. We will see in section 3 the importance of distributive bilattice structure for our algebra.

5-valued algebra

All the previous algebras have the problem to not distinguish ¬⊥ and ⊥. But in the Boolean algebra we would like that x + ¬x = 1 ∀x ∈ {0, 1}. In the no-error case, ⊥ will be derived in 0 or 1 during the compilation. So the idea to characterize ¬⊥ as a specific possible status ∆ is perhaps interesting. The operators are extended around two new properties:

⊥ ⊞ ∆ = ∆ ⊞ ⊥ = 1 and ⊥ ⊡ ∆ = ∆ ⊡ ⊥ = 0. ⊥ and ∆ have the same weight too.
The operators have these definitions:

x ¬ x 1 0 0 1 ⊤ ⊤ ⊥ ∆ ∆ ⊥ ⊔ 1 0 ⊤ ⊥ ∆ 1 1 ⊤ ⊤ 1 1 0 ⊤ 0 ⊤ 0 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ 1 0 ⊤ ⊥ ?? ∆ 1 0 ⊤ ?? ∆ ⊓ 1 0 ⊤ ⊥ ∆ 1 1 ⊥ 1 ⊥ ⊥ 0 ⊥ 0 0 ⊥ ⊥ ⊤ 1 0 ⊤ ⊥ ∆ ⊥ ⊥ ⊥ ⊥ ⊥ ?? ∆ ⊥ ⊥ ∆ ?? ∆ ⊞ 1 0 ⊤ ⊥ ∆ 1 1 1 1 1 1 0 1 0 ⊤ ⊥ ∆ ⊤ 1 ⊤ ⊤ 1 1 ⊥ 1 ⊥ 1 ⊥ 1 ∆ 1 ∆ 1 1 ∆ ⊡ 1 0 ⊤ ⊥ ∆ 1 1 0 ⊤ ⊥ ∆ 0 0 0 0 0 0 ⊤ ⊤ 0 ⊤ 0 0 ⊥ ⊥ 0 0 ⊥ 0 ∆ ⊥ 0 0 0 ∆ It is very difficult to interpret: ∆ ⊔ ⊥.
Adding a new symbol gives more problems that it solves! In conclusion of this section, we will choose 4-valued algebras with bilattice structure. We are now interesting in encoding these rules to built effective synchronous languages compilers.

Encoding Bilattice in Boolean Algebra Product

From a practical point of view, we are interesting to represent element of ξ by Boolean pairs. RR n°8138

Encoding

We define encoding functions e : ξ → B × B: x ∈ ξ , e(x) = (x h , x l ). Several solutions are possible and affect the encoding of each operator especially. We sum up 3 possible encoding in the following • Coding 2 has the advantage to give a simple operation of finalization, it leads to forget x h component.

• Coding 3 explains the growing of the knowledge: (0, 0) unknown, (0, 1) or (1, 0) good knowledge and (1, 1) over-knowledge.

Table 3 shows the effect of each encoding on Algebra5 operators.

From table 3, we conclude that the third encoding has the simpler decomposition into pair of Boolean values for Algebra5. Then, we show in table 4 the encoding with respect to Coding 3 of the other 4-valued algebras we have studied in this report. This latter only details the ⊞, ⊡ and ¬ operators since ⊔ and ⊓ are identical for the 5 algebras and have been given in table 3.

Table 3 and table 4 analysis shows that Algebra5 is the best candidate for our purpose. Indeed, Algebra5 offers nice algebraic properties we will study in the next section.

Distributive Bilattice Properties Applied to Algebra5

If we consider Algebra5 and the third encoding (Coding 3), we can apply popular results from bilattice theory: Definition 3. Let (L, ≤) be a complete lattice. The structure L L = (L × L, ≤ B , ≤ K , ¬) is defined as follows:

• (x 1 , x 2 ) ≤ B (y 1 , y 2 ) iff x 1 ≤ x 2 and y 2 ≤ x 2 • (x 1 , x 2 ) ≤ K (y 1 , y 2 ) iff x 1 ≤ x 2 and x 2 ≤ y 2 • ¬(x 1 , x 2 ) = (x 2 , x 1 )
Lemma 1. (Ginsberg [START_REF] Ginsberg | Multivalued logics: A uniform approach to inference in artificial intelligence[END_REF]) Let (L, ≤) be a complete lattice. Then L L is an interlaced bilattice. If L is distributive, then so is L L.

Given the structure L L, it is easy to verify ( [START_REF] Pigozzi | Multi-valued logic programming semantics: An algebraic approach[END_REF]) that the basic bilattice operations are defined as follows 6 :

(c 1 , d 1 ) ⊔ (c 2 , d 2 ) = (c 1 + c 2 , d 1 + d 2 ) (c 1 , d 1 ) ⊓ (c 2 , d 2 ) = (c 1 .c 2 , d 1 .d 2 ) (c 1 , d 1 ) ⊞ (c 2 , d 2 ) = (c 1 + c 2 , d 1 .d 2 ) (c 1 , d 1 ) ⊡ (c 2 , d 2 ) = (c 1 .c 2 , d 1 + d 2 )
operation offers a means to built distributive bilattice. We will see that we can construct the algebra we want following this method. Let us consider the usual Boolean set (B). (B, ≤) is a complete lattice for 0 ≤ 1 ordering: Algebra ⊞ encoding Proof. We recall that Algebra5 is the bilattice (ξ , ≤ K ≤ B , ¬) defined in section 2.4.1. Let us consider the encoding e 3 : ξ → B × B defines as follows: ⊥ → (0, 0);0 → (0, 1);1 → (1, 0);⊤ → (1, 1). e 3 is an isomorphism from Algebra5 to B B:

⊔ Coding 1 (x ⊔ y) h = x h + y h (x ⊔ y) l = x h .x l .y h .y l + x l .y h .y l + y l .x h .x l + x h .y h .y l Coding 2 (x ⊔ y) h = x h .y h .y l + x h .x l .y h + x h .x l .y l + x h .x l .y h .y l (x ⊔ y) l = x l + y l Coding 3 (x ⊔ y) h = x h + y h (x ⊔ y) l = x l + y l ⊓ Coding 1 (x ⊓ y) h = x h .y h (x ⊓ y) l = x h .x l + y h .y l + x h .x l .y h .y l + x h .y h .y l Coding 2 (x ⊓ y) h = x h .y h .y l + x h .x l .y h + x h .x l .y l + x h .x l .y h .y l (x ⊓ y) l = x l .y l Coding 3 (x ⊓ y) h = x h .y h (x ⊓ y) l = x l .y l ⊞ Coding 1 (x ⊞ y) h = x h .y h (x ⊞ y) l = y h .y l + x h .x l + x h .x l .y h + x l .y l Coding 2 (x ⊞ y) h = x h .y h .y l + x h .x l .y h + x h .x l .y l + x h .x l .y h .y l = (x ⊔ y) h (by definition) (x ⊞ y) l = x l + y l = (x ⊔ y) l (by definition) Coding 3 (x ⊞ y) h = x h + y h (x ⊞ y) l = x l .y l ⊡ Coding 1 (x ⊡ y) h = x h + y h (x ⊡ y) l = x h + y h .y l + x l .y l Coding 2 (x ⊡ y) h = x h .y h .y l + x h .x l .y h + x h .x l .y l + x h .x l .y h .y l = (x ⊓ y) (by definition) (x ⊡ y) l = x l .y l = (x ⊓ y) l (by definition) Coding 3 (x ⊡ y) h = x h .y h (x ⊡ y) l = x l + y l ¬ Coding 1 (¬x) h = x h ⊕ x l (¬x) l = x l Coding 2 (¬x) h = x h (¬x) l = x l Coding 3 (¬x) h = x l (¬x) l = x h
⊡ encoding LE2008 (x ⊞ y) h = x h + y h (x ⊡ y) h = x h .y h (x ⊞ y) l = x l + y l (x ⊡ y) l = x l .y l 2 (x ⊞ y) h = x h .x l + y h .y l + x l .y h + x h .y l (x ⊡ y) h = x h .x l + y h .y l + +x h .y h (x ⊞ y) l = x h .x l + y h .y l + x l .y l (x ⊡ y) l = x h .x l + y h .y l + x h .y l + x l .y h 3 (x ⊞ y) h = x h + y h (x ⊡ y) h = x h .x l + y h .y l + x h .y h (x ⊞ y) l = x h .x l + y h .y l + x l .y l (x ⊡ y) l = x l + y l 4 (x ⊞ y) h = y h + x h .x l + x h .y l (x ⊡ y) h = x h .y h + x h .x l .y l + y h .y l .x l (x ⊞ y) l = x l .y l + x h .x l .y h + y h .y l .x h (x ⊡ y) l = x l + y l 5 (x ⊞ y) h = x h + y h (x ⊡ y) h = x h .y h (x ⊞ y) l = x l .y l (x ⊡ y) l = x l + y l Algebra ¬ encoding LE2008 ¬x h = x h ¬x l = x l Algebra(2,3,4,5) ¬x h = x l ¬x l = x h
1. e 3 (x ⊔ y) = e 3 (x) ⊔ e 3 (y): 2. e 3 (x ⊓ y) = e 3 (x) ⊓ e 3 (y): the reasoning is similar to case 1. 4. e 3 (x ⊡ y) = e 3 (x) ⊡ e 3 (y): the proof is similar to the previous case.

Finally, e 3 (¬x) = ¬(e 3 (x)): if x = ⊥ or x = ⊤ the result is immediate since the ¬ operator does not change these value. So, we have e 3 (x) = (x h , x l ) with

x h = x l hence (x h , x l ) = (x l , x h ). ¬0 = 1 hence e 3 (¬0) = (1, 0) = ¬(0, 1) = ¬(e 3 (0)). The proof for x = 1 is symmetric.
Moreover, e 3 is clearly a bijection.

As a consequence, each Algebra5 equation system is equivalent to a Boolean equation system where each equation

x = f ( - → v ) is expanded in two equations: x h = f ( - → v ) h and x l = f ( - → v ) l such that ( f ( - → v ) h , f ( - → v ) l ) = e 3 ( f ( - → v )).

Conclusion

Synchronous languages have formal semantics computing models of programs either for verification purpose or for compilation. All along the three last decades, several version of semantics have been provided. They have all in common to compute the status of signals in an execution of a program. We need a mathematical framework to represent and compute signal status according to semantics rules. This paper is a review of some adopted solutions and points out another framework which has the ability to provide us with verification and separated compilation. It studies classical approaches with 3-valuated algebras. In these algebras, a ⊥ element turns out to be useful to have the ability to apply constructive rules. But to go further and get a separated compilation means relying on semantics, 4-valued algebras are required. We study five different 4-valued algebras and show that Algebra5 is a distributive bilattice. Then, we have the ability to consider two orders: a Boolean order and a knowledge order which allows us to get stabilization rules to compute signal status. The Boolean order is useful to compute the current environment of signals and the knowledge order is essential to merge environments after a separated compilation of statements. Nevertheless, Algebra3 is also an appealing framework because error is propagated which is not the case for Algebra5. But as soon as ⊤ becomes an absorptive element, the bilattice structure cannot exits and this property is really inescapable. The motivation for this work is the definition of a new method to compile synchronous languages in a separated way. Algebra5 provides us with well-suited properties allowing to define a constructive and efficient semantics as 4-valued constraints. It is also important to specify a behavioral semantics. It gives a meaning to programs and generates models for verification purpose. The chosen framework allows to get both and the equivalence between these two semantics holds and is immediate. Moreover, the isomorphism between Algebra5 and B B and the chosen encoding allow us to compute solutions as Boolean equation system solutions. Our previous work considered LE2008 algebra as the foundation of the semantics. The advantage was the simplicity of finalization process. The drawback was the ¬ operator interpretation incompatible with classical Boolean interpretation. Thanks to bilattice structure, we get the appropriate generalization of Boolean algebra in synchronous world.

A Demonstrations

A.1 Bilattice operators

Here, we study the projection of Algebra5 4-valued algebra into pair of Boolean values. For each element x of Algebra5, we will call (x pos ,x neg ) the pair of Boolean values associated to x with respect to a given encoding. We will rely on Algebra5 to define a mathematical semantics for imperative synchronous languages. We choose this notation, because property 1 allows us to consider that x pos (resp. x neg )represents the degree of presence (resp. absence) of the signal whose status is x.

A.1.1 ⊔ Unify operator:

Corresponding with the chosen encoding: signal status encoding ⊥ 00 0 01 1 10 ⊤ 11

Associated Truth Table after encoding:

x pos x neg y pos y neg S pos S neg

0 0 0 0 0 0 0 0 0 1 0 1 0 0 1 0 1 0 0 0 1 1 1 1 0 1 0 0 0 1 0 1 0 1 0 1 0 1 1 0 1 1 0 1 1 1 1 1 1 0 0 0 1 0 1 0 0 1 1 1 1 0 1 0 1 0 1 0 1 1 1 1 1 1 0 0 1 1 1 1 0 1 1 1 1 1 1 0 1 1 1 1 1 1 1 1
Simplification:

RR n°8138 Equations:

S pos = x pos + y pos S neg = x neg + y neg A.1.2 ⊓ Co-unify operator ⊓ 1 0 ⊤ ⊥ 1 1 ⊥ 1 ⊥ 0 ⊥ 0 0 ⊥ ⊤ 1 0 ⊤ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥
This operator is not actually used in the synchronous language compilers. In fact, it is essential to the bilattice theory introduced by Benhalp and Ginberg.

As the Unify operator, the co-unify operator has the special property to be its own dual operator by the morgan lows too:

¬(x ⊓ y) = ¬(x) ⊓ ¬(y)

Associated Truth Table after encoding:

RR n°8138

x pos x neg y pos y neg S pos S neg

0 0 0 0 0 0 0 0 0 1 0 0 0 0 1 0 0 0 0 0 1 1 0 0 0 1 0 0 0 0 0 1 0 1 0 1 0 1 1 0 0 0 0 1 1 1 0 1 1 0 0 0 0 0 1 0 0 1 0 0 1 0 1 0 1 0 1 0 1 1 1 0 1 1 0 0 0 0 1 1 0 1 0 1 1 1 1 0 1 0 1 1 1 1 1 1
Simplification:

⊞ 1 0 ⊤ ⊥ 1 1 1 1 1 0 1 0 ⊤ ⊥ ⊤ 1 ⊤ ⊤ 1 ⊥ 1 ⊥ 1 ⊥ RR n°8138
Associated Truth Table after encoding:

x pos x neg y pos y neg S pos S neg

0 0 0 0 0 0 0 0 0 1 0 0 0 0 1 0 1 0 0 0 1 1 1 0 0 1 0 0 0 0 0 1 0 1 0 1 0 1 1 0 1 0 0 1 1 1 1 1 1 0 0 0 1 0 1 0 0 1 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1 1 0 0 1 0 1 1 0 1 1 1 1 1 1 0 1 0 1 1 1 1 1 1
Simplification:

⊡ 1 0 ⊤ ⊥ 1 1 0 ⊤ ⊥ 0 0 0 0 0 ⊤ ⊤ 0 ⊤ 0 ⊥ ⊥ 0 0 ⊥ RR n°8138
Associated Truth Table after encoding:

x pos x neg y pos y neg S pos S neg

0 0 0 0 0 0 0 0 0 1 0 1 0 0 1 0 0 0 0 0 1 1 0 1 0 1 0 0 0 1 0 1 0 1 0 1 0 1 1 0 0 1 0 1 1 1 0 1 1 0 0 0 0 0 1 0 0 1 0 1 1 0 1 0 1 0 1 0 1 1 1 1 1 1 0 0 0 1 1 1 0 1 0 1 1 1 1 0 1 1 1 1 1 1 1 1
Simplification: Equations:

S pos = x pos .y pos S neg = x neg + y neg S pos and S neg equations for ⊔,⊓,⊞ and ⊡ can also been deduced from the isomorphism between Algebra5 and B B showed in property 1.

A.1.5 ¬ Neg operator:

x ¬ x ⊥ ⊥ 0 1 1 0 ⊤ ⊤

Associated Truth Table after encoding:

x pos x neg S pos S neg

0 0 0 0 0 1 1 0 1 0 0 1 1 1 1 1
Directly:

S pos = x neg S neg = x pos
This operation can be seen as a swap of variables according to the Belnap'theory.

A.1.6 Finalisation operator

x FL(x) ⊥ 0 0 0 1 1 ⊤ / 0 / 0 is the don't care value.

Associated Truth Table after encoding:

x pos x neg S pos S neg 0 0 0

1 0 1 0 1 1 0 1 0 1 1 / 0 / 0
Directly:

S pos = x pos S neg = x pos RR n°8138

A.2 Algebra properties

This section is devoted to the demonstrations of Algebra5 algebraic properties described in table 1. According to property 1 we can represent each element x of Algebra5 as a pair of Boolean value (x pos , x neg ). Hence each law of Algebra5 can be proved either by computing truth tables or by relying on this decomposition to deduce the law from Boolean algebra laws.

For each law, we propose both approaches. To ease the expression of proofs, we will use a matrix to represent the Boolean decomposition of elements of Algebra5:

x = x pos x neg A.2.1 Absorption Laws ¬(¬x) = x
Proof. we detail both approaches:

1. Truth table approach:

x ¬x ¬(¬x) ⊥ ⊥ ⊥ 0 1 0 1 0 1 ⊤ ⊤ ⊤ 2. Algebraic approach: ¬x = x neg x pos =⇒ ¬(¬x) = x pos x neg = x ⊥ ⊔ x = x
Proof. we detail both approaches:

1. Truth table approach x ⊥ ⊔ x ⊥ ⊥ 0 0 1 1 ⊤ ⊤ 2.
Algebraic approach: to establish the proof we rely on the decomposition of Algebra5 operators described in table 3 and proved in the previous section of this appendix.

⊥ ⊔ x = 0 + x pos 0 + x neg = x pos x neg = x
We recall that ⊥ = 0 0 .

RR n°8138

⊥ ⊓ x = ⊥ Proof. we detail both approaches:

1. Truth table approach x ⊥ ⊓ x ⊥ ⊥ 0 ⊥ 1 ⊥ ⊤ ⊥
2. Algebraic approach: to establish the proof we rely on the decomposition of Algebra5 operators described in table 3 and proved in the previous section of this appendix.

⊥ ⊓ x = 0 . x pos 0 . x neg = 0 0 = 0. 1 ⊞ x = 1
Proof. we detail both approaches:

1. Truth table approach:

x 1 ⊞ x ⊥ 1 0 1 1 1 ⊤ 1
2. Algebraic approach:

1 ⊞ x = 1 + x pos 0.x neg = 1 0 = 1
Because in Boolean algebra: 1 + x = 1 and 0.x = 0.

0 ⊞ x = x
Proof. we consider both approaches:

1. Truth table approach:

x 0 ⊞ x ⊥ ⊥ 0 0 1 1 ⊤ ⊤ RR n°8138
2. Algebraic approach:

0 ⊞ x = 0 + x pos 1.x neg = x pos x neg = x
Because 0 + x = x and 1.x = x in Boolean algebra.

⊥ ⊞ x = x
Proof. we consider both approaches:

1. Truth table approach:

x ⊥ ⊞ x ⊥ ⊥ 0 ⊥ 1 1 ⊤ 1
2. Algebraic approach:

0 0 ⊞ x pos x neg = 0 + x pos 0.x neg = x pos 0 = x pos x neg ⊥ ⊡ x = ⊥
Proof. we consider both approaches:

1. Truth table approach:

x ⊥ ⊡ x ⊥ ⊥ 0 0 1 ⊥ ⊤ 0 2. Algebraic approach: 0 0 ⊡ x pos x neg = 0 . x pos 0 + x neg = 0 x neg = 0 0 RR n°8138 0 ⊡ x = 0
Proof. we consider both approaches:

1. Truth table:

x 0 ⊡ x ⊥ 0 0 0 1 0 ⊤ 0 2. Algebraic approach: 0 1 ⊡ x pos x neg = 0 . x pos 1 + x neg = 0 1 1 ⊡ x = x
Proof. we consider both approaches:

1. Truth table:

x 1 ⊡ x ⊥ ⊥ 0 0 1 1 ⊤ ⊤ 2. Algebraic approach: 1 0 ⊡ x pos x neg = 1 . x pos 0 + x neg = x pos x neg ⊤ ⊔ x = ⊤
Proof. We consider both approaches.

1. Truth table approach:

x ⊤ ⊔ x ⊥ ⊤ 0 ⊤ 1 ⊤ ⊤ ⊤ 2. Algebraic approach: 1 1 ⊔ x pos x neg = 1 + x pos 1 + x neg = 1 1 RR n°8138 ⊤ ⊞ x = ⊤
Proof. We consider both approaches.

1. Truth table approach:

x ⊤ ⊞ x ⊥ 1 0 ⊤ 1 1 ⊤ ⊤ 2. Algebraic approach: 1 1 ⊔ x pos x neg = 1 + x pos 1 + x neg = 1 1 ⊤ ⊡ x = ⊤
Proof. We consider both approaches.

1. Truth table approach:

x ⊤ ⊡ x ⊥ 0 0 0 1 ⊤ ⊤ ⊤
2. Algebraic approach:

1 1 ⊞ x pos x neg = 1 + x pos 1 . x neg = 1 x neg = 1 1 RR n°8138 A.2.2 Associativity Laws (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)
Proof. We consider both approaches. 1. Truth table approach:

x y z x ⊔ y (x ⊔ y) ⊔ z y ⊔ z x ⊔ (y ⊔ z) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ 0 0 0 ⊥ ⊥ 1 ⊥ 1 1 1 ⊥ ⊥ ⊤ ⊥ ⊤ ⊤ ⊤ ⊥ 0 ⊥ 0 0 0 0 ⊥ 0 0 0 0 0 0 ⊥ 0 1 0 ⊤ ⊤ ⊤ ⊥ 0 ⊤ 0 ⊤ ⊤ ⊤ ⊥ 1 ⊥ 1 1 1 1 ⊥ 1 0 1 ⊤ ⊤ ⊤ ⊥ 1 1 1 1 1 1 ⊥ 1 ⊤ 1 ⊤ ⊤ ⊤ ⊥ ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ ⊥ ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊥ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ ⊥ ⊤ ⊤ ⊥ ⊤ ⊤ ⊥ 0 ⊤ ⊤ 0 ⊤ ⊤ ⊥ 1 ⊤ ⊤ 1 ⊤ ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 0 ⊥ ⊤ ⊤ 0 ⊤ ⊤ 0 0 ⊤ ⊤ 0 ⊤ ⊤ 0 1 ⊤ ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 1 ⊥ ⊤ ⊤ 1 ⊤ ⊤ 1 0 ⊤ ⊤ ⊤ ⊤ ⊤ 1 1 ⊤ ⊤ 1 ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ x y z x ⊔ y (x ⊔ y) ⊔ z y ⊔ z x ⊔ (y ⊔ z) 0 ⊥ ⊥ 0 0 ⊥ 0 0 ⊥ 0 0 0 0 0 0 ⊥ 1 0 ⊤ 1 ⊤ 0 ⊥ ⊤ 0 ⊤ ⊤ ⊤ 0 0 ⊥ 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 ⊤ ⊤ ⊤ 0 0 ⊤ 0 ⊤ ⊤ ⊤ 0 1 ⊥ ⊤ ⊤ 1 ⊤ 0 1 0 ⊤ ⊤ ⊤ ⊤ 0 1 1 ⊤ ⊤ 1 ⊤ 0 1 ⊤ ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ 0 ⊤ 0 ⊤ ⊤ ⊤ ⊤ 0 ⊤ 1 ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 1 ⊥ ⊥ 1 1 ⊥ 1 1 ⊥ 0 1 ⊤ 0 ⊤ 1 ⊥ 1 1 1 1 1 1 ⊥ ⊤ 1 ⊤ ⊤ ⊤ 1 0 ⊥ ⊤ ⊤ 0 ⊤ 1 0 0 ⊤ ⊤ 0 ⊤ 1 0 1 ⊤ ⊤ ⊤ ⊤ 1 0 ⊤ ⊤ ⊤ ⊤ ⊤ 1 1 ⊥ 1 1 1 1 1 1 0 1 ⊤ ⊤ ⊤ 1 1 1 1 1 1 1 1 1 ⊤ 1 ⊤ ⊤ ⊤ 1 ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ 1 ⊤ 0 ⊤ ⊤ ⊤ ⊤ 1 ⊤ 1 ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 2.
(x ⊞ y) ⊞ z = x ⊞ (y ⊞ z)
Proof. We consider both approaches.

1. Truth table approach:

x y z x ⊞ y (x ⊞ y) ⊞ z y ⊞ z x ⊞ (y ⊞ z) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 1 ⊥ 1 1 1 ⊥ ⊥ ⊤ ⊥ 1 1 1 ⊥ 0 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 0 ⊥ ⊥ ⊥ ⊥ ⊥ 0 1 ⊥ 1 1 1 ⊥ 0 ⊤ ⊥ 1 ⊤ 1 ⊥ 1 ⊥ 1 1 1 1 ⊥ 1 0 1 1 1 1 ⊥ 1 1 1 1 1 1 ⊥ 1 ⊤ 1 1 1 1 ⊥ ⊤ ⊥ 1 1 1 1 ⊥ ⊤ 0 1 1 ⊤ 1 ⊥ ⊤ 1 1 1 1 1 ⊥ ⊤ ⊤ 1 1 ⊤ 1 ⊤ ⊥ ⊥ 1 1 ⊥ 1 ⊤ ⊥ 0 1 1 ⊥ 1 ⊤ ⊥ 1 1 1 1 1 ⊤ ⊥ ⊤ 1 1 1 1 ⊤ 0 ⊥ ⊤ 1 ⊥ 1 ⊤ 0 0 ⊤ ⊤ 0 ⊤ ⊤ 0 1 ⊤ 1 1 1 ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 1 ⊥ 1 1 1 1 ⊤ 1 0 1 1 1 1 ⊤ 1 1 1 1 1 1 ⊤ 1 ⊤ 1 1 1 1 ⊤ ⊤ ⊥ ⊤ 1 1 1 ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 1 ⊤ 1 1 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ x y z x ⊞ y (x ⊞ y) ⊞ z y ⊞ z x ⊞ (y ⊞ z) 0 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ 0 ⊥ ⊥ ⊥ ⊥ 0 ⊥ 1 ⊥ 1 1 1 0 ⊥ ⊤ ⊥ 1 1 1 0 0 ⊥ 0 ⊥ ⊥ ⊥ 0 0 0 0 0 0 0 0 0 1 0 1 1 1 0 0 ⊤ 0 ⊤ ⊤ ⊤ 0 1 ⊥ 1 1 1 1 0 1 0 1 1 1 1 0 1 1 1 1 1 1 0 1 ⊤ 1 1 1 1 0 ⊤ ⊥ ⊤ 1 1 1 0 ⊤ 0 ⊤ ⊤ ⊤ ⊤ 0 ⊤ 1 ⊤ 1 1 1 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 1 ⊥ ⊥ 1 1 ⊥ 1 1 ⊥ 0 2.
(x ⊡ y) ⊡ z = x ⊡ (y ⊡ z)
Proof. We consider both approaches. 1. Truth table approach:

x y z x ⊡ y (x ⊡ y) ⊡ z y ⊡ z x ⊡ (y ⊡ z) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ 0 0 0 ⊥ ⊥ 1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊤ ⊥ 0 0 0 ⊥ 0 ⊥ 0 0 0 0 ⊥ 0 0 0 0 0 0 ⊥ 0 1 0 0 0 0 ⊥ 0 ⊤ 0 0 0 0 ⊥ 1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 1 0 ⊥ 0 0 ⊥ ⊥ 1 1 ⊥ ⊥ 1 1 ⊥ 1 ⊤ ⊥ 0 ⊤ 0 ⊥ ⊤ ⊥ 0 0 0 0 ⊥ ⊤ 0 0 0 0 0 ⊥ ⊤ 1 0 0 ⊤ 0 ⊥ ⊤ ⊤ 0 0 ⊤ 0 ⊤ ⊥ ⊥ 0 0 ⊥ 0 ⊤ ⊥ 0 0 0 0 0 ⊤ ⊥ 1 0 0 ⊥ 0 ⊤ ⊥ ⊤ 0 0 0 0 ⊤ 0 ⊥ 0 0 0 0 ⊤ 0 0 0 0 0 0 ⊤ 0 1 0 0 0 0 ⊤ 0 ⊤ 0 0 0 0 ⊤ 1 ⊥ ⊤ 0 ⊥ 0 ⊤ 1 0 ⊤ 0 0 0 ⊤ 1 1 ⊤ ⊤ 1 ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ ⊤ 0 0 0 ⊤ ⊤ 0 ⊤ 0 0 0 ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ x y z x ⊡ y (x ⊡ y) ⊡ z y ⊡ z x ⊡ (y ⊡ z) 0 ⊥ ⊥ 0 0 ⊥ 0 0 ⊥ 0 0 0 0 0 0 ⊥ 1 0 0 ⊥ 0 0 ⊥ ⊤ 0 0 0 0 0 0 ⊥ 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 ⊤ 0 0 0 0 0 1 ⊥ 0 0 ⊥ 0 0 1 0 0 0 0 0 0 1 1 0 0 1 0 0 1 ⊤ 0 0 ⊤ 0 0 ⊤ ⊥ 0 0 0 0 0 ⊤ 0 0 0 0 0 0 ⊤ 1 0 0 ⊤ 0 0 ⊤ ⊤ 0 0 ⊤ 0 1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 1 ⊥ 0 ⊥ 0 0 0 1 ⊥ 1 ⊥ ⊥ ⊥ ⊥ 1 ⊥ ⊤ ⊥ 0 0 0 1 0 ⊥ 0 0 0 0 1 0 0 0 0 0 0 1 0 1 0 0 0 0 1 0 ⊤ 0 0 0 0 1 1 ⊥ 1 ⊥ ⊥ ⊥ 1 1 0 1 0 0 0 1 1 1 1 1 1 1 1 1 ⊤ 1 ⊤ ⊤ ⊤ 1 ⊤ ⊥ ⊤ 0 0 0 1 ⊤ 0 ⊤ 0 0 0 1 ⊤ 1 ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 2.

A.2.3 Distributivity Laws

All the algebraic proofs of this section relies on the distributive laws of Boolean algebra.

(x ⊞ y) ⊡ z = (x ⊡ z) ⊞ (y ⊡ z)
Proof. we consider both approaches:

1. Truth table approach:

x y z x ⊞ y (x ⊞ y) ⊡ z x ⊞ z y ⊡ z (x ⊡ z) ⊞ (y ⊡ z) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ 0 0 0 0 ⊥ ⊥ 1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊤ ⊥ 0 0 0 0 ⊥ 0 ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ 0 0 ⊥ 0 0 0 0 ⊥ 0 1 ⊥ ⊥ ⊥ 0 ⊥ ⊥ 0 ⊤ ⊥ 0 0 0 0 ⊥ 1 ⊥ 1 ⊥ ⊥ ⊥ ⊥ ⊥ 1 0 1 0 0 0 0 ⊥ 1 1 1 1 ⊥ 1 1 ⊥ 1 ⊤ 1 ⊤ 0 ⊤ ⊤ ⊥ ⊤ ⊥ 1 ⊥ ⊥ 0 ⊥ ⊥ ⊤ 0 1 0 0 0 0 ⊥ ⊤ 1 1 1 ⊥ ⊤ 1 ⊥ ⊤ ⊤ 1 ⊤ 0 ⊤ ⊤ 0 ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ 0 ⊥ 0 ⊥ 0 0 0 0 0 ⊥ 1 ⊥ ⊥ 0 ⊥ ⊥ 0 ⊥ ⊤ ⊥ 0 0 0 0 0 0 ⊥ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 ⊤ 0 0 0 0 0 0 1 ⊥ 1 ⊥ 0 ⊥ ⊥ 0 1 0 1 0 0 0 0 0 1 1 1 1 0 1 1 0 1 ⊤ 1 ⊤ 0 ⊤ ⊤ 0 ⊤ ⊥ ⊤ 0 0 0 0 0 ⊤ 0 ⊤ 0 0 0 0 0 ⊤ 1 ⊤ ⊤ 0 ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊤ RR n°8138 x y z x ⊞ y (x ⊞ y) ⊡ z x ⊞ z y ⊡ z (x ⊡ z) ⊞ (y ⊡ z) 1 ⊥ ⊥ 1 ⊥ ⊥ ⊥ ⊥ 1 ⊥ 0 1 0 0 0 0 1 ⊥ 1 1 1 1 ⊥ 1 1 ⊥ ⊤ 1 ⊤ ⊤ 0 ⊤ 1 0 ⊥ 1 ⊥ ⊥ 0 ⊥ 1 0 0 1 0 0 0 0 1 0 1 1 1 1 0 1 1 0 ⊤ 1 ⊤ ⊤ 0 ⊤ 1 1 ⊥ 1 ⊥ ⊥ ⊥ ⊥ 1 1 0 1 0 0 0 0 1 1 1 1 1 1 1 1 1 1 ⊤ 1 ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊥ 1 ⊥ ⊥ 0 ⊥ 1 ⊤ 0 1 0 0 0 0 1 ⊤ 1 1 1 1 ⊤ 1 1 ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ ⊥ 1 ⊥ 0 ⊥ ⊥ ⊤ ⊥ 0 1 0 0 0 0 ⊤ ⊥ 1 1 1 ⊤ ⊥ 1 ⊤ ⊥ ⊤ 1 ⊤ ⊤ 0 ⊤ ⊤ 0 ⊥ ⊤ 0 0 0 0 ⊤ 0 0 ⊤ 0 0 0 0 ⊤ 0 1 ⊤ ⊤ ⊤ 0 ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊤ 1 ⊥ 1 ⊥ 0 ⊥ ⊥ ⊤ 1 0 1 0 0 0 0 ⊤ 1 1 1 1 ⊤ 1 1 ⊤ 1 ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ ⊤ 0 0 0 0 ⊤ ⊤ 0 ⊤ 0 0 0 0 ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤
2. Algebraic approach:

(x ⊞ y) ⊡ z = (x pos + y pos ).z pos (x neg .y neg ) + z neg = (x pos .z pos ) + (y pos .z pos ) (x neg + z neg ).(y neg + z neg = (x ⊡ z) ⊞ (y ⊡ z) RR n°8138 (x ⊡ y) ⊞ z = (x ⊞ z) ⊡ (y ⊞ z)
Proof. we consider both approaches:

1. Truth table approach:

x y z x ⊡ y (x ⊡ y) ⊞ z x ⊞ z y ⊞ z (x ⊞ z) ⊡ (y ⊞ z) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 1 ⊥ 1 1 1 1 ⊥ ⊥ ⊤ ⊥ 1 1 1 1 ⊥ 0 ⊥ 0 ⊥ ⊥ ⊥ ⊥ ⊥ 0 0 0 0 ⊥ 0 0 ⊥ 0 1 0 1 1 1 1 ⊥ 0 ⊤ 0 ⊤ 1 ⊤ ⊤ ⊥ 1 ⊥ ⊥ ⊥ ⊥ 1 ⊥ ⊥ 1 0 ⊥ ⊥ ⊥ 1 ⊥ ⊥ 1 1 ⊥ 1 1 1 1 ⊥ 1 ⊤ ⊥ 1 1 1 1 ⊥ ⊤ ⊥ 0 ⊥ ⊥ 1 ⊥ ⊥ ⊤ 0 0 0 ⊥ ⊤ 0 ⊥ ⊤ 1 0 1 1 1 1 ⊥ ⊤ ⊤ 0 ⊤ 1 ⊤ ⊤ 0 ⊥ ⊥ 0 ⊥ ⊥ ⊥ ⊥ 0 ⊥ 0 0 0 0 ⊥ 0 0 ⊥ 1 0 1 1 1 1 0 ⊥ ⊤ 0 ⊤ ⊤ 1 ⊤ 0 0 ⊥ 0 ⊥ ⊥ ⊥ ⊥ 0 0 0 0 0 0 0 0 0 0 1 0 1 1 1 1 0 0 ⊤ 0 ⊤ ⊤ ⊤ ⊤ 0 1 ⊥ 0 ⊥ ⊥ 1 ⊥ 0 1 0 0 0 0 1 0 0 1 1 0 1 1 1 1 0 1 ⊤ 0 ⊤ ⊤ 1 ⊤ 0 ⊤ ⊥ 0 ⊥ ⊥ 1 ⊥ 0 ⊤ 0 0 0 0 ⊤ 0 0 ⊤ 1 0 1 1 1 1 0 ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ RR n°8138 x y z x ⊡ y (x ⊡ y) ⊞ z x ⊞ z y ⊞ z (x ⊞ z) ⊡ (y ⊞ z) 1 ⊥ ⊥ ⊥ ⊥ 1 ⊥ ⊥ 1 ⊥ 0 ⊥ ⊥ 1 ⊥ ⊥ 1 ⊥ 1 ⊥ 1 1 1 1 1 ⊥ ⊤ ⊥ 1 1 1 1 1 0 ⊥ 0 ⊥ 1 ⊥ ⊥ 1 0 0 0 0 1 0 0 1 0 1 0 1 1 1 1 1 0 ⊤ 0 ⊤ 1 ⊤ ⊤ 1 1 ⊥ 1 1 1 1 1 1 1 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 ⊤ 1 1 1 1 1 1 ⊤ ⊥ ⊤ 1 1 1 1 1 ⊤ 0 ⊤ ⊤ 1 ⊤ ⊤ 1 ⊤ 1 ⊤ 1 1 1 1 1 ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊥ ⊥ 0 ⊥ 1 ⊥ ⊥ ⊤ ⊥ 0 0 0 ⊤ ⊥ 0 ⊤ ⊥ 1 0 1 1 1 1 ⊤ ⊥ ⊤ 0 ⊤ ⊤ 1 ⊤ ⊤ 0 ⊥ 0 ⊥ 1 ⊥ ⊥ ⊤ 0 0 0 0 ⊤ 0 0 ⊤ 0 1 0 1 1 1 1 ⊤ 0 ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ 1 ⊥ ⊤ 1 1 1 1 ⊤ 1 0 ⊤ ⊤ ⊤ 1 ⊤ ⊤ 1 1 ⊤ 1 1 1 1 ⊤ 1 ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊥ ⊤ 1 1 1 1 ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 1 ⊤ 1 1 1 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤
2. Algebraic approach:

(x ⊡ y) ⊞ z = (x pos .y pos ) + z pos (x neg + y neg ).z neg = (x pos + z pos ).(y pos + z pos ) (x neg .z neg ) + (y neg .z neg ) = (x ⊞ z) ⊡ (y ⊞ z) RR n°8138 (x ⊔ y) ⊓ z = (x ⊓ z) ⊔ (y ⊓ z)
Proof. we consider both approaches:

1. Truth table approach:

x y z x ⊔ y (x ⊔ y) ⊓ z x ⊓ z y ⊓ z (x ⊓ z) ⊔ (y ⊓ z) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊤ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ 0 ⊥ ⊥ ⊥ ⊥ ⊥ 0 0 0 0 ⊥ 0 0 ⊥ 0 1 0 ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊤ 0 0 ⊥ 0 0 ⊥ 1 ⊥ 1 ⊥ ⊥ ⊥ ⊥ ⊥ 1 0 1 ⊥ ⊥ ⊥ ⊥ ⊥ 1 1 1 1 ⊥ 1 1 ⊥ 1 ⊤ 1 1 ⊥ 1 1 ⊥ ⊤ ⊥ ⊤ ⊥ ⊥ ⊥ ⊥ ⊥ ⊤ 0 ⊤ 0 ⊥ 0 0 ⊥ ⊤ 1 ⊤ 1 ⊥ 1 1 ⊥ ⊤ ⊤ ⊤ ⊤ ⊥ ⊤ ⊤ 0 ⊥ ⊥ 0 ⊥ ⊥ ⊥ ⊥ 0 ⊥ 0 0 0 0 ⊥ 0 0 ⊥ 1 0 ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊤ 0 0 0 ⊥ 0 0 0 ⊥ 0 ⊥ ⊥ ⊥ ⊥ 0 0 0 0 0 0 0 0 0 0 1 0 ⊥ ⊥ ⊥ ⊥ 0 0 ⊤ 0 0 0 0 0 0 1 ⊥ ⊤ ⊥ ⊥ ⊥ ⊥ 0 1 0 ⊤ 0 0 ⊥ 0 0 1 1 ⊤ 1 ⊥ 1 1 0 1 ⊤ ⊤ ⊤ 0 1 ⊤ 0 ⊤ ⊥ ⊤ ⊥ ⊥ ⊥ ⊥ 0 ⊤ 0 ⊤ 0 0 0 0 0 ⊤ 1 ⊤ 1 ⊥ 1 1 0 ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊤ RR n°8138 x y z x ⊔ y (x ⊔ y) ⊓ z x ⊓ z y ⊓ z (x ⊓ z) ⊔ (y ⊓ z) 1 ⊥ ⊥ 1 ⊥ ⊥ ⊥ ⊥ 1 ⊥ 0 1 ⊥ ⊥ ⊥ ⊥ 1 ⊥ 1 1 1 1 ⊥ 1 1 ⊥ ⊤ 1 1 1 ⊥ 1 1 0 ⊥ ⊤ ⊥ ⊥ ⊥ ⊥ 1 0 0 ⊤ 0 ⊥ 0 0 1 0 1 ⊤ 1 1 ⊥ 1 1 0 ⊤ ⊤ ⊤ 1 0 ⊤ 1 1 ⊥ 1 ⊥ ⊥ ⊥ ⊥ 1 1 0 1 ⊥ ⊥ ⊥ ⊥ 1 1 1 1 1 1 1 1 1 1 ⊤ 1 1 1 1 1 1 ⊤ ⊥ ⊤ ⊥ ⊥ ⊥ ⊥ 1 ⊤ 0 ⊤ 0 ⊥ 0 0 1 ⊤ 1 ⊤ 1 1 1 1 1 ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊥ ⊥ ⊤ ⊥ ⊥ ⊥ ⊥ ⊤ ⊥ 0 ⊤ 0 0 ⊥ 0 ⊤ ⊥ 1 ⊤ 1 1 ⊥ 1 ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ ⊥ ⊤ ⊤ 0 ⊥ ⊤ ⊥ ⊥ ⊥ ⊥ ⊤ 0 0 ⊤ 0 0 0 0 ⊤ 0 1 ⊤ 1 1 ⊥ 1 ⊤ 0 ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊤ 1 ⊥ ⊤ ⊥ ⊥ ⊥ ⊥ ⊤ 1 0 ⊤ 0 0 ⊥ 0 ⊤ 1 1 ⊤ 1 1 1 1 ⊤ 1 ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊥ ⊤ ⊥ ⊥ ⊥ ⊥ ⊤ ⊤ 0 ⊤ 0 0 0 0 ⊤ ⊤ 1 ⊤ 1 1 1 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤
2. Algebraic approach:

(x ⊔ y) ⊓ z = (x pos + y pos ).z pos (x neg + y neg ).z neg = (x pos .z pos ) + (y pos .z pos ) (x neg .z neg ) + (y neg .z neg ) = (x ⊓ z) ⊔ (y ⊓ z) RR n°8138 (x ⊓ y) ⊔ z = (x ⊔ z) ⊓ (y ⊔ z)
Proof. we consider both approaches:

1. Truth table approach:

x y z x ⊓ y (x ⊓ y) ⊔ z x ⊔ z y ⊔ z (x ⊔ z) ⊓ (y ⊔ z) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ 0 0 0 0 ⊥ ⊥ 1 ⊥ 1 1 1 1 ⊥ ⊥ ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ ⊥ 0 ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ 0 0 ⊥ 0 0 0 0 ⊥ 0 1 ⊥ 1 1 ⊤ 1 ⊥ 0 ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ ⊥ 1 ⊥ ⊥ ⊥ ⊥ 1 ⊥ ⊥ 1 0 ⊥ 0 0 ⊤ 0 ⊥ 1 1 ⊥ 1 1 1 1 ⊥ 1 ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ ⊥ ⊤ ⊥ ⊥ ⊥ ⊥ ⊤ ⊥ ⊥ ⊤ 0 ⊥ 0 0 ⊤ 0 ⊥ ⊤ 1 ⊥ 1 1 ⊤ 1 ⊥ ⊤ ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ 0 ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ 0 ⊥ 0 ⊥ 0 0 0 0 0 ⊥ 1 ⊥ 1 ⊤ 1 1 0 ⊥ ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ 0 0 ⊥ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 ⊤ ⊤ ⊤ ⊤ 0 0 ⊤ 0 ⊤ ⊤ ⊤ ⊤ 0 1 ⊥ ⊥ ⊥ 0 1 ⊥ 0 1 0 ⊥ 0 0 ⊤ 0 0 1 1 ⊥ 1 ⊤ 1 1 0 1 ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊥ 0 0 0 ⊤ 0 0 ⊤ 0 0 0 0 ⊤ 0 0 ⊤ 1 0 ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ RR n°8138 x y z x ⊓ y (x ⊓ y) ⊔ z x ⊔ z y ⊔ z (x ⊔ z) ⊓ (y ⊔ z) 1 ⊥ ⊥ ⊥ ⊥ 1 ⊥ ⊥ 1 ⊥ 0 ⊥ 0 ⊤ 0 0 1 ⊥ 1 ⊥ 1 1 1 1 1 ⊥ ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ 1 0 ⊥ ⊥ ⊥ 1 0 ⊥ 1 0 0 ⊥ 0 ⊤ 0 0 1 0 1 ⊥ 1 1 ⊤ 1 1 0 ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ 1 1 ⊥ 1 1 1 1 1 1 1 0 1 ⊤ ⊤ ⊤ ⊤ 1 1 1 1 1 1 1 1 1 1 ⊤ 1 ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊥ 1 1 1 ⊤ 1 1 ⊤ 0 1 ⊤ ⊤ ⊤ ⊤ 1 ⊤ 1 1 1 1 ⊤ 1 1 ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ ⊥ ⊥ ⊥ ⊤ ⊥ ⊥ ⊤ ⊥ 0 ⊥ 0 ⊤ 0 0 ⊤ ⊥ 1 ⊥ 1 ⊤ 1 1 ⊤ ⊥ ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ ⊤ 0 ⊥ 0 0 ⊤ 0 0 ⊤ 0 0 0 0 ⊤ 0 0 ⊤ 0 1 0 ⊤ ⊤ ⊤ ⊤ ⊤ 0 ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ 1 ⊥ 1 1 ⊤ 1 1 ⊤ 1 0 1 ⊤ ⊤ ⊤ ⊤ ⊤ 1 1 1 1 ⊤ 1 1 ⊤ 1 ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤
2. Algebraic approach:

(x ⊓ y) ⊔ z = (x pos .y pos ) + z pos (x neg .y neg ) + z neg = (x pos + z pos ).(y pos + z pos ) (x neg + z neg ).(y neg + z neg ) = (x ⊔ z) ⊓ (y ⊔ z) (x ⊔ y) ⊞ z = (x ⊞ z) ⊔ (y ⊞ z)
Proof. we consider both approaches:

1. Truth table approach:

x y z x ⊔ y (x ⊔ y) ⊞ z x ⊞ z y ⊞ z (x ⊞ z) ⊔ (y ⊞ z) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 1 ⊥ 1 1 1 1 ⊥ ⊥ ⊤ ⊥ 1 1 1 1 ⊥ 0 ⊥ 0 ⊥ ⊥ ⊥ ⊥ ⊥ 0 0 0 0 ⊥ 0 0 ⊥ 0 1 0 1 1 1 1 ⊥ 0 ⊤ 0 ⊤ 1 ⊤ ⊤ ⊥ 1 ⊥ 1 1 ⊥ 1 1 ⊥ 1 0 1 1 ⊥ 1 1 ⊥ 1 1 1 1 1 1 1 ⊥ 1 ⊤ 1 1 1 1 1 ⊥ ⊤ ⊥ ⊤ 1 ⊥ 1 1 ⊥ ⊤ 0 ⊤ ⊤ ⊥ ⊤ ⊤ ⊥ ⊤ 1 ⊤ 1 1 1 1 ⊥ ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊤ 0 ⊥ ⊥ 0 ⊥ ⊥ ⊥ ⊥ 0 ⊥ 0 0 0 0 ⊥ 0 0 ⊥ 1 0 1 1 1 1 0 ⊥ ⊤ 0 ⊤ ⊤ 1 ⊤ 0 0 ⊥ 0 ⊥ ⊥ ⊥ ⊥ 0 0 0 0 0 0 0 0 0 0 1 0 1 1 1 1 0 0 ⊤ 0 ⊤ ⊤ ⊤ ⊤ 0 1 ⊥ ⊤ 1 ⊥ 1 1 0 1 0 ⊤ ⊤ 0 1 ⊤ 0 1 1 ⊤ 1 1 1 1 0 1 ⊤ ⊤ ⊤ ⊤ 1 ⊤ 0 ⊤ ⊥ ⊤ 1 ⊥ 1 1 0 ⊤ 0 ⊤ ⊤ 0 ⊤ ⊤ 0 ⊤ 1 ⊤ 1 1 1 1 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ RR n°8138 x y z x ⊔ y (x ⊔ y) ⊞ z x ⊞ z y ⊞ z (x ⊞ z) ⊔ (y ⊞ z) 1 ⊥ ⊥ 1 1 1 ⊥ 1 1 ⊥ 0 1 1 1 ⊥ 1 1 ⊥ 1 1 1 1 1 1 1 ⊥ ⊤ 1 1 1 1 1 1 0 ⊥ ⊤ 1 1 ⊥ 1 1 0 0 ⊤ ⊤ 1 0 ⊤ 1 0 1 ⊤ 1 1 1 1 1 0 ⊤ ⊤ ⊤ 1 ⊤ ⊤ 1 1 ⊥ 1 1 1 1 1 1 1 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 ⊤ 1 1 1 1 1 1 ⊤ ⊥ ⊤ 1 1 1 1 1 ⊤ 0 ⊤ ⊤ 1 ⊤ ⊤ 1 ⊤ 1 ⊤ 1 1 1 1 1 ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊥ ⊥ ⊤ 1 1 ⊥ 1 ⊤ ⊥ 0 ⊤ ⊤ ⊤ ⊥ ⊤ ⊤ ⊥ 1 ⊤ 1 1 1 1 ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊤ 0 ⊥ ⊤ 1 1 ⊥ 1 ⊤ 0 0 ⊤ ⊤ ⊤ 0 ⊤ ⊤ 0 1 ⊤ 1 1 1 1 ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 1 ⊥ ⊤ 1 1 1 1 ⊤ 1 0 ⊤ ⊤ ⊤ 1 ⊤ ⊤ 1 1 ⊤ 1 1 1 1 ⊤ 1 ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊥ ⊤ 1 1 1 1 ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 1 ⊤ 1 1 1 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤
2. Algebraic approach:

(x ⊔ y) ⊞ z = (x pos + y pos ) + z pos (x neg + y neg ).z neg = (x pos + z pos ) + (y pos + z pos ) (x neg .z neg ) + (y neg .z neg ) = (x ⊞ z) ⊔ (y ⊞ z) RR n°8138 (x ⊔ y) ⊡ z = (x ⊡ z) ⊔ (y ⊡ z)
Proof. we consider both approaches:

1. Truth table approach:

x y z x ⊔ y (x ⊔ y) ⊡ z x ⊡ z y ⊡ z (x ⊡ z) ⊔ (y ⊡ z) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ 0 0 0 0 ⊥ ⊥ 1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊤ ⊥ 0 0 0 0 ⊥ 0 ⊥ 0 0 ⊥ 0 0 ⊥ 0 0 0 0 0 0 0 ⊥ 0 1 0 0 ⊥ 0 0 ⊥ 0 ⊤ 0 0 0 0 0 ⊥ 1 ⊥ 1 ⊥ ⊥ ⊥ ⊥ ⊥ 1 0 1 0 0 0 0 ⊥ 1 1 1 1 ⊥ 1 1 ⊥ 1 ⊤ 1 ⊤ 0 ⊤ ⊤ ⊥ ⊤ ⊥ ⊤ 0 ⊥ 0 0 ⊥ ⊤ 0 ⊤ 0 0 0 0 ⊥ ⊤ 1 ⊤ ⊤ ⊥ ⊤ ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊤ 0 ⊥ ⊥ 0 0 0 ⊥ 0 0 ⊥ 0 0 0 0 0 0 0 ⊥ 1 0 0 0 ⊥ 0 0 ⊥ ⊤ 0 0 0 0 0 0 0 ⊥ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 ⊤ 0 0 0 0 0 0 1 ⊥ ⊤ 0 0 ⊥ 0 0 1 0 ⊤ 0 0 0 0 0 1 1 ⊤ ⊤ 0 1 ⊤ 0 1 ⊤ ⊤ ⊤ 0 ⊤ ⊤ 0 ⊤ ⊥ ⊤ 0 0 0 0 0 ⊤ 0 ⊤ 0 0 0 0 0 ⊤ 1 ⊤ ⊤ 0 ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊤ RR n°8138 x y z x ⊔ y (x ⊔ y) ⊡ z x ⊡ z y ⊡ z (x ⊡ z) ⊔ (y ⊡ z) 1 ⊥ ⊥ 1 ⊥ ⊥ ⊥ ⊥ 1 ⊥ 0 1 0 0 0 0 1 ⊥ 1 1 1 1 ⊥ 1 1 ⊥ ⊤ 1 ⊤ ⊤ 0 ⊤ 1 0 ⊥ ⊤ 0 ⊥ 0 0 1 0 0 ⊤ 0 0 0 0 1 0 1 ⊤ ⊤ 1 0 ⊤ 1 0 ⊤ ⊤ ⊤ ⊤ 0 ⊤ 1 1 ⊥ 1 ⊥ ⊥ ⊥ ⊥ 1 1 0 1 0 0 0 0 1 1 1 1 1 1 1 1 1 1 ⊤ 1 ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊥ ⊤ 0 ⊥ 0 0 1 ⊤ 0 ⊤ 0 0 0 0 1 ⊤ 1 ⊤ ⊤ 1 ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ ⊥ ⊤ 0 0 ⊥ 0 ⊤ ⊥ 0 ⊤ 0 0 0 0 ⊤ ⊥ 1 ⊤ ⊤ ⊤ ⊥ ⊤ ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊤ 0 ⊥ ⊤ 0 0 0 0 ⊤ 0 0 ⊤ 0 0 0 0 ⊤ 0 1 ⊤ ⊤ ⊤ 0 ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊤ 1 ⊥ ⊤ 0 0 ⊥ 0 ⊤ 1 0 ⊤ 0 0 0 0 ⊤ 1 1 ⊤ ⊤ ⊤ 1 ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ ⊤ 0 0 0 0 ⊤ ⊤ 0 ⊤ 0 0 0 0 ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤
2. Algebraic approach:

(x ⊔ y) ⊡ z = (x pos + y pos ).z pos (x neg + y neg ) + z neg = (x pos .z pos ) + (y pos ).z pos ) (x neg + z neg ) + (y neg + z neg ) = (x ⊡ z) ⊔ (y ⊡ z)
Here also we apply the x + x = x Boolean law.

(x ⊓ y) ⊞ z = (x ⊞ z) ⊓ (y ⊞ z)
Proof. we consider both approaches:

1. Truth table approach:

x y z x ⊓ y (x ⊓ y) ⊞ z x ⊞ z y ⊞ z (x ⊞ z) ⊓ (y ⊞ z) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 1 ⊥ 1 1 1 1 ⊥ ⊥ ⊤ ⊥ 1 1 1 1 ⊥ 0 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 0 ⊥ ⊥ ⊥ 0 ⊥ ⊥ 0 1 ⊥ 1 1 1 1 ⊥ 0 ⊤ ⊥ 1 1 ⊤ 1 ⊥ 1 ⊥ ⊥ ⊥ ⊥ 1 ⊥ ⊥ 1 0 ⊥ ⊥ ⊥ 1 ⊥ ⊥ 1 1 ⊥ 1 1 1 1 ⊥ 1 ⊤ ⊥ 1 1 1 1 ⊥ ⊤ ⊥ ⊥ ⊥ ⊥ 1 ⊥ ⊥ ⊤ 0 ⊥ ⊥ ⊥ ⊤ ⊥ ⊥ ⊤ 1 ⊥ 1 1 1 1 ⊥ ⊤ ⊤ ⊥ 1 1 ⊤ 1 0 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ 0 ⊥ ⊥ 0 ⊥ ⊥ 0 ⊥ 1 ⊥ 1 1 1 1 0 ⊥ ⊤ ⊥ 1 ⊤ 1 1 0 0 ⊥ 0 ⊥ ⊥ ⊥ ⊥ 0 0 0 0 0 0 0 0 0 0 1 0 1 1 1 1 0 0 ⊤ 0 ⊤ ⊤ ⊤ ⊤ 0 1 ⊥ ⊥ ⊥ ⊥ 1 ⊥ 0 1 0 ⊥ ⊥ 0 1 ⊥ 0 1 1 ⊥ 1 1 1 1 0 1 ⊤ ⊥ 1 ⊤ 1 1 0 ⊤ ⊥ 0 ⊥ ⊥ 1 ⊥ 0 ⊤ 0 0 0 0 ⊤ 0 0 ⊤ 1 0 1 1 1 1 0 ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ RR n°8138 x y z x ⊓ y (x ⊓ y) ⊞ z x ⊞ z y ⊞ z (x ⊞ z) ⊓ (y ⊞ z) 1 ⊥ ⊥ ⊥ ⊥ 1 ⊥ ⊥ 1 ⊥ 0 ⊥ ⊥ 1 ⊥ ⊥ 1 ⊥ 1 ⊥ 1 1 1 1 1 ⊥ ⊤ ⊥ 1 1 1 1 1 0 ⊥ ⊥ ⊥ 1 ⊥ ⊥ 1 0 0 ⊥ ⊥ 1 0 ⊥ 1 0 1 ⊥ 1 1 1 1 1 0 ⊤ ⊥ 1 1 ⊤ 1 1 1 ⊥ 1 1 1 1 1 1 1 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 ⊤ 1 1 1 1 1 1 ⊤ ⊥ 1 1 1 1 1 1 ⊤ 0 1 1 1 ⊤ 1 1 ⊤ 1 1 1 1 1 1 1 ⊤ ⊤ 1 1 1 ⊤ 1 ⊤ ⊥ ⊥ ⊥ ⊥ 1 ⊥ ⊥ ⊤ ⊥ 0 ⊥ ⊥ ⊤ ⊥ ⊥ ⊤ ⊥ 1 ⊥ 1 1 1 1 ⊤ ⊥ ⊤ ⊥ 1 ⊤ 1 1 ⊤ 0 ⊥ 0 ⊥ 1 ⊥ ⊥ ⊤ 0 0 0 0 ⊤ 0 0 ⊤ 0 1 0 1 1 1 1 ⊤ 0 ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ 1 ⊥ 1 1 1 1 1 ⊤ 1 0 1 1 ⊤ 1 1 ⊤ 1 1 1 1 1 1 1 ⊤ 1 ⊤ 1 1 ⊤ 1 1 ⊤ ⊤ ⊥ ⊤ 1 1 1 1 ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 1 ⊤ 1 1 1 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤
2. Algebraic approach:

(x ⊓ y) ⊞ z = (x pos .y pos ) + z pos (x neg .y neg ).z neg = (x pos + z pos ).(y pos + z pos ) (x neg .z neg ).(y neg .z neg ) = (x ⊞ z) ⊓ (y ⊞ z)
Symmetrically to previous law, we apply the x.x = x Boolean law.

(x ⊓ y) ⊡ z = (x ⊡ z) ⊓ (y ⊡ z)
Proof. we consider both approaches:

1. Truth table approach:

x y z x ⊓ y (x ⊓ y) ⊡ z x ⊡ z y ⊡ z (x ⊡ z) ⊓ (y ⊡ z) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ 0 0 0 0 ⊥ ⊥ 1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊤ ⊥ 0 0 0 0 ⊥ 0 ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ 0 0 ⊥ 0 0 0 0 ⊥ 0 1 ⊥ ⊥ ⊥ 0 ⊥ ⊥ 0 ⊤ ⊥ 0 0 0 0 ⊥ 1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 1 0 ⊥ 0 0 0 0 ⊥ 1 1 ⊥ ⊥ ⊥ 1 ⊥ ⊥ 1 ⊤ ⊥ 0 0 ⊤ 0 ⊥ ⊤ ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ ⊤ 0 ⊥ 0 0 0 0 ⊥ ⊤ 1 ⊥ ⊥ ⊥ ⊤ ⊥ ⊥ ⊤ ⊤ ⊥ 0 0 ⊤ 0 0 ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ 0 ⊥ 0 ⊥ 0 0 0 0 0 ⊥ 1 ⊥ ⊥ 0 ⊥ ⊥ 0 ⊥ ⊤ ⊥ 0 0 0 0 0 0 ⊥ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 ⊤ 0 0 0 0 0 0 1 ⊥ ⊥ ⊥ 0 ⊥ ⊥ 0 1 0 ⊥ 0 0 0 0 0 1 1 ⊥ ⊥ 0 1 ⊥ 0 1 ⊤ ⊥ 0 0 ⊤ 0 0 ⊤ ⊥ 0 0 0 0 0 0 ⊤ 0 0 0 0 0 0 0 ⊤ 1 0 0 0 ⊤ 0 0 ⊤ ⊤ 0 0 0 ⊤ 0 RR n°8138 x y z x ⊓ y (x ⊓ y) ⊡ z x ⊡ z y ⊡ z (x ⊡ z) ⊓ (y ⊡ z) 1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 1 ⊥ 0 ⊥ 0 0 0 0 1 ⊥ 1 ⊥ ⊥ 1 ⊥ ⊥ 1 ⊥ ⊤ ⊥ 0 ⊤ 0 0 1 0 ⊥ ⊥ ⊥ ⊥ 0 ⊥ 1 0 0 ⊥ 0 0 0 0 1 0 1 ⊥ ⊥ 1 0 ⊥ 1 0 ⊤ ⊥ 0 ⊤ 0 0 1 1 ⊥ 1 ⊥ ⊥ ⊥ ⊥ 1 1 0 1 0 0 0 0 1 1 1 1 1 1 1 1 1 1 ⊤ 1 ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊥ 1 ⊥ ⊥ 0 ⊥ 1 ⊤ 0 1 0 0 0 0 1 ⊤ 1 1 1 1 ⊤ 1 1 ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ ⊤ ⊥ 0 ⊥ 0 0 0 0 ⊤ ⊥ 1 ⊥ ⊥ ⊤ ⊥ ⊥ ⊤ ⊥ ⊤ ⊥ 0 ⊤ 0 0 ⊤ 0 ⊥ 0 0 0 0 0 ⊤ 0 0 0 0 0 0 0 ⊤ 0 1 0 0 ⊤ 0 0 ⊤ 0 ⊤ 0 0 ⊤ 0 0 ⊤ 1 ⊥ 1 ⊥ 0 ⊥ ⊥ ⊤ 1 0 1 0 0 0 0 ⊤ 1 1 1 1 ⊤ 1 1 ⊤ 1 ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ ⊤ 0 0 0 0 ⊤ ⊤ 0 ⊤ 0 0 0 0 ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤
2. Algebraic approach:

(x ⊓ y) ⊡ z = (x pos .y pos ).z pos (x neg .y neg ) + z neg = (x pos .z pos ).(y pos .z pos ) (x neg + z neg ).(y neg + z neg ) = (x ⊡ z) ⊓ (y ⊡ z) RR n°8138 (x ⊞ y) ⊔ z = (x ⊔ z) ⊞ (y ⊔ z)
Proof. we consider both approaches:

1. Truth table approach:

x y z x ⊞ y (x ⊞ y) ⊔ z x ⊔ z y ⊔ z (x ⊔ z) ⊞ (y ⊔ z) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ 0 0 0 0 ⊥ ⊥ 1 ⊥ 1 1 1 1 ⊥ ⊥ ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ ⊥ 0 ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ 0 0 ⊥ 0 0 0 0 ⊥ 0 1 ⊥ 1 1 ⊤ 1 ⊥ 0 ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ ⊥ 1 ⊥ 1 1 ⊥ 1 1 ⊥ 1 0 1 ⊤ 0 ⊤ ⊤ ⊥ 1 1 1 1 1 1 1 ⊥ 1 ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊥ ⊤ ⊥ 1 1 ⊥ ⊤ 1 ⊥ ⊤ 0 1 ⊤ 0 ⊤ ⊤ ⊥ ⊤ 1 1 1 1 ⊤ 1 ⊥ ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ 0 ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ 0 ⊥ 0 ⊥ 0 0 0 0 0 ⊥ 1 ⊥ 1 ⊤ 1 1 0 ⊥ ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ 0 0 ⊥ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 ⊤ ⊤ ⊤ ⊤ 0 0 ⊤ 0 ⊤ ⊤ ⊤ ⊤ 0 1 ⊥ 1 1 0 1 1 0 1 0 1 ⊤ 0 ⊤ ⊤ 0 1 1 1 1 ⊤ 1 1 0 1 ⊤ 1 ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊥ ⊤ ⊤ 0 ⊤ ⊤ 0 ⊤ 0 ⊤ ⊤ 0 ⊤ ⊤ 0 ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ RR n°8138 x y z x ⊞ y (x ⊞ y) ⊔ z x ⊔ z y ⊔ z (x ⊔ z) ⊞ (y ⊔ z) 1 ⊥ ⊥ 1 1 1 ⊥ 1 1 ⊥ 0 1 ⊤ ⊤ 0 ⊤ 1 ⊥ 1 1 1 1 1 1 1 ⊥ ⊤ 1 ⊤ ⊤ ⊤ ⊤ 1 0 ⊥ 1 1 1 0 1 1 0 0 1 ⊤ ⊤ 0 ⊤ 1 0 1 1 1 1 ⊤ 1 1 0 ⊤ 1 ⊤ ⊤ ⊤ ⊤ 1 1 ⊥ 1 1 1 1 1 1 1 0 1 ⊤ ⊤ ⊤ ⊤ 1 1 1 1 1 1 1 1 1 1 ⊤ 1 ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊥ 1 1 1 ⊤ 1 1 ⊤ 0 1 ⊤ ⊤ ⊤ ⊤ 1 ⊤ 1 1 1 1 ⊤ 1 1 ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ ⊥ 1 1 ⊤ ⊥ 1 ⊤ ⊥ 0 1 ⊤ ⊤ 0 ⊤ ⊤ ⊥ 1 1 1 ⊤ 1 1 ⊤ ⊥ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ 0 ⊥ ⊤ ⊤ ⊤ 0 ⊤ ⊤ 0 0 ⊤ ⊤ ⊤ 0 ⊤ ⊤ 0 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 1 ⊥ 1 1 ⊤ 1 1 ⊤ 1 0 1 ⊤ ⊤ ⊤ ⊤ ⊤ 1 1 1 1 ⊤ 1 1 ⊤ 1 ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤
2. Algebraic approach:

(x ⊞ y) ⊔ z = (x pos + y pos ) + z pos (x neg .y neg ) + z neg = (x pos + z pos ) + (y pos + z pos ) (x neg + z neg ).(y neg + z neg ) = (x ⊔ z) ⊞ (y ⊔ z) RR n°8138 (x ⊞ y) ⊓ z = (x ⊓ z) ⊞ (y ⊓ z)
Proof. we consider both approaches:

1. Truth table approach:

x y z x ⊞ y (x ⊞ y) ⊓ z x ⊓ z y ⊓ z (x ⊓ z) ⊞ (y ⊓ z) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊤ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 0 ⊥ ⊥ ⊥ 0 ⊥ ⊥ 0 1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊤ ⊥ ⊥ ⊥ 0 ⊥ ⊥ 1 ⊥ 1 ⊥ ⊥ ⊥ ⊥ ⊥ 1 0 1 ⊥ ⊥ ⊥ ⊥ ⊥ 1 1 1 1 ⊥ 1 1 ⊥ 1 ⊤ 1 1 ⊥ 1 1 ⊥ ⊤ ⊥ 1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊤ 0 1 ⊥ ⊥ 0 ⊥ ⊥ ⊤ 1 1 1 ⊥ 1 1 ⊥ ⊤ ⊤ 1 1 ⊥ ⊤ 1 0 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ 0 ⊥ ⊥ 0 ⊥ ⊥ 0 ⊥ 1 ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊤ ⊥ ⊥ 0 ⊥ ⊥ 0 0 ⊥ 0 ⊥ ⊥ ⊥ ⊥ 0 0 0 0 0 0 0 0 0 0 1 0 ⊥ ⊥ ⊥ ⊥ 0 0 ⊤ 0 0 0 0 0 0 1 ⊥ 1 ⊥ ⊥ ⊥ ⊥ 0 1 0 1 ⊥ 0 ⊥ ⊥ 0 1 1 1 1 ⊥ 1 1 0 1 ⊤ 1 1 0 1 1 0 ⊤ ⊥ ⊤ ⊥ ⊥ ⊥ ⊥ 0 ⊤ 0 ⊤ 0 0 0 0 0 ⊤ 1 ⊤ 1 ⊥ 1 1 0 ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊤ RR n°8138 x y z x ⊞ y (x ⊞ y) ⊓ z x ⊓ z y ⊓ z (x ⊓ z) ⊞ (y ⊓ z) 1 ⊥ ⊥ 1 ⊥ ⊥ ⊥ ⊥ 1 ⊥ 0 1 ⊥ ⊥ ⊥ ⊥ 1 ⊥ 1 1 1 1 ⊥ 1 1 ⊥ ⊤ 1 1 1 ⊥ 1 1 0 ⊥ 1 ⊥ ⊥ ⊥ ⊥ 1 0 0 1 ⊥ ⊥ 0 ⊥ 1 0 1 1 1 1 ⊥ 1 1 0 ⊤ 1 1 1 0 1 1 1 ⊥ 1 ⊥ ⊥ ⊥ ⊥ 1 1 0 1 ⊥ ⊥ ⊥ ⊥ 1 1 1 1 1 1 1 1 1 1 ⊤ 1 1 1 1 1 1 ⊤ ⊥ 1 ⊥ ⊥ ⊥ ⊥ 1 ⊤ 0 1 ⊥ ⊥ 0 ⊥ 1 ⊤ 1 1 1 1 1 1 1 ⊤ ⊤ 1 1 1 ⊤ 1 ⊤ ⊥ ⊥ 1 ⊥ ⊥ ⊥ ⊥ ⊤ ⊥ 0 1 ⊥ 0 ⊥ ⊥ ⊤ ⊥ 1 1 1 1 ⊥ 1 ⊤ ⊥ ⊤ 1 1 ⊤ ⊥ 1 ⊤ 0 ⊥ ⊤ ⊥ ⊥ ⊥ ⊥ ⊤ 0 0 ⊤ 0 0 0 0 ⊤ 0 1 ⊤ 1 1 ⊥ 1 ⊤ 0 ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊤ 1 ⊥ 1 ⊥ ⊥ ⊥ ⊥ ⊤ 1 0 1 ⊥ 0 ⊥ ⊥ ⊤ 1 1 1 1 1 1 1 ⊤ 1 ⊤ 1 1 ⊤ 1 1 ⊤ ⊤ ⊥ ⊤ ⊥ ⊥ ⊥ ⊥ ⊤ ⊤ 0 ⊤ 0 0 0 0 ⊤ ⊤ 1 ⊤ 1 1 1 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤
2. Algebraic approach:

(x ⊞ y) ⊓ z = (x pos + y pos ).z pos (x neg .y neg ).z neg = (x pos .z pos ) + (y pos .z pos ) (x neg .z neg ).(y neg .z neg ) = (x ⊓ z) ⊞ (y ⊓ z) RR n°8138 (x ⊡ y) ⊔ z = (x ⊔ z) ⊡ (y ⊔ z)
Proof. we consider both approaches:

1. Truth table approach:

x y z x ⊡ y (x ⊡ y) ⊔ z x ⊔ z y ⊔ z (x ⊔ z) ⊡ (y ⊔ z) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ 0 0 0 0 ⊥ ⊥ 1 ⊥ 1 1 1 1 ⊥ ⊥ ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ ⊥ 0 ⊥ 0 0 ⊥ 0 0 ⊥ 0 0 0 0 0 0 0 ⊥ 0 1 0 ⊤ 1 ⊤ ⊤ ⊥ 0 ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊥ 1 ⊥ ⊥ ⊥ ⊥ 1 ⊥ ⊥ 1 0 ⊥ 0 0 ⊤ 0 ⊥ 1 1 ⊥ 1 1 1 1 ⊥ 1 ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ ⊥ ⊤ ⊥ 0 0 ⊥ ⊤ 0 ⊥ ⊤ 0 0 0 0 ⊤ 0 ⊥ ⊤ 1 0 ⊤ 1 ⊤ ⊤ ⊥ ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ 0 ⊥ ⊥ 0 0 0 ⊥ 0 0 ⊥ 0 0 0 0 0 0 0 ⊥ 1 0 ⊤ ⊤ 1 ⊤ 0 ⊥ ⊤ 0 ⊤ ⊤ ⊤ ⊤ 0 0 ⊥ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 ⊤ ⊤ ⊤ ⊤ 0 0 ⊤ 0 ⊤ ⊤ ⊤ ⊤ 0 1 ⊥ 0 0 0 1 0 0 1 0 0 0 0 ⊤ 0 0 1 1 0 ⊤ ⊤ 1 ⊤ 0 1 ⊤ 0 ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊥ 0 0 0 ⊤ 0 0 ⊤ 0 0 0 0 ⊤ 0 0 ⊤ 1 0 ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ RR n°8138 x y z x ⊡ y (x ⊡ y) ⊔ z x ⊔ z y ⊔ z (x ⊔ z) ⊡ (y ⊔ z) 1 ⊥ ⊥ ⊥ ⊥ 1 ⊥ ⊥ 1 ⊥ 0 ⊥ 0 ⊤ 0 0 1 ⊥ 1 ⊥ 1 1 1 1 1 ⊥ ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ 1 0 ⊥ 0 0 1 0 0 1 0 0 0 0 ⊤ 0 0 1 0 1 0 ⊤ 1 ⊤ ⊤ 1 0 ⊤ 0 ⊤ ⊤ ⊤ ⊤ 1 1 ⊥ 1 1 1 1 1 1 1 0 1 ⊤ ⊤ ⊤ ⊤ 1 1 1 1 1 1 1 1 1 1 ⊤ 1 ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊥ ⊤ ⊤ 1 ⊤ ⊤ 1 ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ 1 ⊤ 1 ⊤ ⊤ 1 ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ ⊥ 0 0 ⊤ ⊥ 0 ⊤ ⊥ 0 0 0 ⊤ 0 0 ⊤ ⊥ 1 0 ⊤ ⊤ 1 ⊤ ⊤ ⊥ ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ 0 ⊥ 0 0 ⊤ 0 0 ⊤ 0 0 0 0 ⊤ 0 0 ⊤ 0 1 0 ⊤ ⊤ ⊤ ⊤ ⊤ 0 ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ 1 ⊥ ⊤ ⊤ ⊤ 1 ⊤ ⊤ 1 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 1 1 ⊤ ⊤ ⊤ 1 ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊥ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤
2. Algebraic approach:

(x ⊡ y) ⊔ z = (x pos .y pos ) + z pos (x neg + y neg ) + z neg = (x pos + z pos ).(y pos + z pos ) (x neg + z neg ) + (y neg + z neg ) = (x ⊔ z) ⊡ (y ⊔ z) RR n°8138 (x ⊡ y) ⊓ z = (x ⊓ z) ⊡ (y ⊓ z)
Proof. we consider both approaches:

1. Truth table approach:

x y z x ⊡ y (x ⊡ y) ⊓ z x ⊓ z y ⊓ z (x ⊓ z) ⊡ (y ⊓ z) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊤ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ 0 ⊥ ⊥ ⊥ ⊥ ⊥ 0 0 0 0 ⊥ 0 0 ⊥ 0 1 0 ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊤ 0 0 ⊥ 0 0 ⊥ 1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 1 0 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 1 1 ⊥ ⊥ ⊥ 1 ⊥ ⊥ 1 ⊤ ⊥ ⊥ ⊥ 1 ⊥ ⊥ ⊤ ⊥ 0 ⊥ ⊥ ⊥ ⊥ ⊥ ⊤ 0 0 0 ⊥ 0 0 ⊥ ⊤ 1 0 ⊥ ⊥ 1 ⊥ ⊥ ⊤ ⊤ 0 0 ⊥ ⊤ 0 0 ⊥ ⊥ 0 ⊥ ⊥ ⊥ ⊥ 0 ⊥ 0 0 0 0 ⊥ 0 0 ⊥ 1 0 ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊤ 0 0 0 ⊥ 0 0 0 ⊥ 0 ⊥ ⊥ ⊥ ⊥ 0 0 0 0 0 0 0 0 0 0 1 0 ⊥ ⊥ ⊥ ⊥ 0 0 ⊤ 0 0 0 0 0 0 1 ⊥ 0 ⊥ ⊥ ⊥ ⊥ 0 1 0 0 0 0 ⊥ 0 0 1 1 0 ⊥ ⊥ 1 ⊥ 0 1 ⊤ 0 0 0 1 0 0 ⊤ ⊥ 0 ⊥ ⊥ ⊥ ⊥ 0 ⊤ 0 0 0 0 0 0 0 ⊤ 1 0 ⊥ ⊥ 1 ⊥ 0 ⊤ ⊤ 0 0 0 ⊤ 0 RR n°8138 x y z x ⊡ y (x ⊡ y) ⊓ z x ⊓ z y ⊓ z (x ⊓ z) ⊡ (y ⊓ z) 1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 1 ⊥ 0 ⊥ ⊥ ⊥ ⊥ ⊥ 1 ⊥ 1 ⊥ ⊥ 1 ⊥ ⊥ 1 ⊥ ⊤ ⊥ ⊥ 1 ⊥ ⊥ 1 0 ⊥ 0 ⊥ ⊥ ⊥ ⊥ 1 0 0 0 0 ⊥ 0 0 1 0 1 0 ⊥ 1 ⊥ ⊥ 1 0 ⊤ 0 0 1 0 0 1 1 ⊥ 1 ⊥ ⊥ ⊥ ⊥ 1 1 0 1 ⊥ ⊥ ⊥ ⊥ 1 1 1 1 1 1 1 1 1 1 ⊤ 1 1 1 1 1 1 ⊤ ⊥ ⊤ ⊥ ⊥ ⊥ ⊥ 1 ⊤ 0 ⊤ 0 ⊥ 0 0 1 ⊤ 1 ⊤ 1 1 1 1 1 ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊥ ⊥ 0 ⊥ ⊥ ⊥ ⊥ ⊤ ⊥ 0 0 0 0 ⊥ 0 ⊤ ⊥ 1 0 ⊥ 1 ⊥ ⊥ ⊤ ⊥ ⊤ 0 0 ⊤ ⊥ 0 ⊤ 0 ⊥ 0 ⊥ ⊥ ⊥ ⊥ ⊤ 0 0 0 0 0 0 0 ⊤ 0 1 0 ⊥ 1 ⊥ ⊥ ⊤ 0 ⊤ 0 0 ⊤ 0 0 ⊤ 1 ⊥ ⊤ ⊥ ⊥ ⊥ ⊥ ⊤ 1 0 ⊤ 0 0 ⊥ 0 ⊤ 1 1 ⊤ 1 1 1 1 ⊤ 1 ⊤ ⊤ ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊥ ⊤ ⊥ ⊥ ⊥ ⊥ ⊤ ⊤ 0 ⊤ 0 0 0 0 ⊤ ⊤ 1 ⊤ 1 1 1 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤
2. Algebraic approach:

(x ⊡ y) ⊓ z = (x pos .y pos ).z pos (x neg + y neg ).z neg = (x pos .z pos ).(y pos .z pos ) (x neg .z neg ) + y neg .z neg ) = (x ⊓ z) ⊡ (y ⊓ z)

RR n°8138 A.2.4 Indempotence Laws x ⊔ x = x ⊓ x = x ⊞ x = x ⊡ x = x
Proof. We consider both approaches.

1. Truth table approach: x ⊡ (y ⊞ x) = x Proof. We consider both approaches.

x x ⊔ x x ⊓ x x ⊞ x x ⊡ x ⊥ ⊥ ⊥ ⊥ ⊥ 0 0 0 0 0 1 1 1 1 1 ⊤ ⊤ ⊤ ⊤ ⊤ 2.
1. Truth table approach:

x y y ⊞ x x ⊡ (y ⊞ x) ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ ⊥ 1 1 ⊥ ⊥ ⊤ 1 ⊥ 0 ⊥ ⊥ 0 0 0 0 0 0 1 1 0 0 ⊤ ⊤ 0 1 ⊥ 1 1 1 0 1 1 1 1 1 1 1 ⊤ 1 1 ⊤ ⊥ 1 ⊤ ⊤ 0 ⊤ ⊤ ⊤ 1 1 ⊤ ⊤ ⊤ ⊤ ⊤
2. Algebraic approach:

x

(x ⊞ y) ⊡ x = x
Proof. We consider both approaches.

1. Truth table approach:

x y x ⊞ y (x ⊞ y) ⊡ x ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ ⊥ 1 1 ⊥ ⊥ ⊤ 1 ⊥ 0 ⊥ ⊥ 0 0 0 0 0 0 1 1 0 0 ⊤ ⊤ 0 1 ⊥ 1 1 1 0 1 1 1 1 1 1 1 ⊤ 1 1 ⊤ ⊥ 1 ⊤ ⊤ 0 ⊤ ⊤ ⊤ 1 1 ⊤ ⊤ ⊤ ⊤ ⊤ 2.
(x ⊔ y) ⊓ x = x
Proof. We consider both approaches.

1. Truth table approach: ¬(x ⊡ y) = ¬(x) ⊞ ¬(y)

x y x ⊔ y (x ⊔ y) ⊓ x ⊥ ⊥ ⊥ ⊥ ⊥ 0 0 ⊥ ⊥ 1 1 ⊥ ⊥ ⊤ ⊤ ⊥ 0 ⊥ 0 0 0 0 0 0 0 1 ⊤ 0 0 ⊤ ⊤ 0 1 ⊥ 1 1 1 0 ⊤ 1 1 1 1 1 1 ⊤ ⊤ 1 ⊤ ⊥ ⊤ ⊤ ⊤ 0 ⊤ ⊤ ⊤ 1 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 2.
x y x ⊓ y (x ⊓ y) ⊔ x ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ ⊥ 1 ⊥ ⊥ ⊥ ⊤ ⊥ ⊥ 0 ⊥ ⊥ 0 0 0 0 0 0 1 ⊥ 0 0 ⊤ 0 0 1 ⊥ ⊥ 1 1 0 ⊥ 1 1 1 1 1 1 ⊤ 1 1 ⊤ ⊥ ⊥ ⊤ ⊤ 0 0 ⊤ ⊤ 1 1 ⊤ ⊤ ⊤ ⊤ ⊤ 2.
Proof. We consider both approaches.

1. Truth table approach: ¬(x ⊞ y) = ¬(x) ⊡ ¬(y)

x y x ⊡ y ¬(x ⊡ y) ¬(x) ¬(y) ¬(x) ⊞ ¬(y) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 0 1 ⊥ 1 1 ⊥ 1 ⊥ ⊥ ⊥ 0 ⊥ ⊥ ⊤ 0 1 ⊥ ⊤ 1 0 ⊥ 0 1 1 ⊥ 1 0 0 0 1 1 1 1 0 1 0 1 1 0 1 0 ⊤ 0 1 1 ⊤ 1 1 ⊥ ⊥ ⊥ 0 ⊥ ⊥ 1 0 0 1 0 1 1 1 1 1 0 0 0 0 1 ⊤ ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊥ 0 1 ⊤ ⊥ 1 ⊤ 0 0 1 ⊤ 1 ⊤ ⊤ 1 ⊤ ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 2.
Proof. We consider both approaches.

1. Truth table approach: ¬(x ⊔ y) = ¬(x) ⊔ ¬(y)

x y x ⊡ y ¬(x ⊡ y) ¬(x) ¬(y) ¬(x) ⊞ ¬(y) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ ⊥ 1 ⊥ ⊥ 1 1 0 ⊥ 0 0 ⊥ ⊤ 1 0 ⊥ ⊤ 0 0 ⊥ ⊥ ⊥ 1 ⊥ ⊥ 0 0 0 1 1 1 1 0 1 1 0 1 0 0 0 ⊤ ⊤ ⊤ 1 ⊤ ⊤ 1 ⊥ 1 0 0 ⊥ 0 1 0 1 0 0 1 0 1 1 1 0 0 0 0 1 ⊤ 1 0 0 ⊤ 0 ⊤ ⊥ 1 0p ⊤ ⊥ ⊤ ⊤ 0 ⊤ ⊤ ⊤ 1 ⊤ ⊤ 1 1 0 ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 2.
Proof. We consider both approaches.

1. Truth table approach: ¬(x ⊓ y) = ¬(x) ⊓ ¬(y)

x y x ⊔ y ¬(x ⊔ y) ¬(x) ¬(y) ¬(x) ⊔ ¬(y) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 0 1 ⊥ 1 1 ⊥ 1 1 0 ⊥ 0 0 ⊥ ⊤ ⊤ ⊤ ⊥ ⊤ ⊤ 0 ⊥ 0 1 1 ⊥ 1 0 0 0 1 1 1 1 0 1 ⊤ ⊤ 1 0 ⊤ 0 ⊤ ⊤ ⊤ 1 ⊤ ⊤ 1 ⊥ 1 0 0 ⊥ 0 1 0 ⊤ ⊤ 0 1 ⊤ 1 1 1 0 0 0 0 1 ⊤ ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊥ ⊤ ⊤ ⊤ ⊥ ⊤ ⊤ 0 ⊤ ⊤ ⊤ 1 ⊤ ⊤ 1 ⊤ ⊤ ⊤ 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 2.
Proof. We consider both approaches.

1. Truth table approach:

x y x ⊓ y ¬(x ⊓ y) ¬(x) ¬(y) ¬(x) ⊓ ¬(y) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ 0 ⊥ ⊥ ⊥ 1 ⊥ ⊥ 1 ⊥ ⊥ ⊥ 0 ⊥ ⊥ ⊤ ⊥ ⊥ ⊥ ⊤ ⊥ 0 ⊥ ⊥ ⊥ 1 ⊥ ⊥ 0 0 0 1 1 1 1 0 1 ⊥ ⊥ 1 0 ⊥ 0 ⊤ 0 1 1 ⊤ 1 1 ⊥ ⊥ ⊥ 0 ⊥ ⊥ 1 0 ⊥ ⊥ 0 1 ⊥ 1 1 1 0 0 0 0 1 ⊤ 1 0 0 ⊤ 0 ⊤ ⊥ ⊥ ⊥ ⊤ ⊥ bot ⊤ 0 0 1 ⊤ 1 1 ⊤ 1 1 0 ⊤ 0 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 2.

A.3 Bilattice properties

In this section, we prove properties concerning bilattice orders. Similarly to section A.2, we can prove these properties using both truth tables and algebraic decomposition in Boolean pairs of elements of the bilattice. For the algebraic concern, we rely on the isomorphism : Algebra5 → B B (see property 1). Hence, we recall the definitions of ≤ K and ≤ B orders in B B:

(x 1 , x 2 ) ≤ K (y 1 , y 2 ) iff x 1 ≤ y 1 and x 2 ≤ y 2 in B. (x 1 , x 2 ) ≤ B (y 1 , y 2 ) iff x 1 ≤ y 1 and y 2 ≤ x 2 in B.
x ≤ K (x ⊔ y)

Proof using truth table:

x y x ⊔ y x ≤ K (x ⊔ y) ⊥ ⊥ ⊥ Yes ⊥ 0 0 Yes ⊥ 1 1 Yes ⊥ ⊤ ⊤ Yes 0 ⊥ 0 Yes 0 0 0 Yes 0 1 ⊤ Yes 0 ⊤ ⊤ Yes 1 ⊥ 1 Yes 1 0 ⊤ Yes 1 1 1 Yes 1 ⊤ ⊤ Yes ⊤ ⊥ ⊤ Yes ⊤ 0 ⊤ Yes ⊤ 1 ⊤ Yes ⊤ ⊤ ⊤ Yes
Algebraic approach:

Let us consider x = x pos x neg and y = y pos y neg . In B, x pos ≤ x pos + y pos and x neg ≤ x neg + y neg , then x pos x neg ≤ K

x pos + y pos x neg + y neg . According to ⊔ projection in B B, we can deduce that x ≤ K x ⊔ y.

(x ⊓ y) ≤ K x RR n°8138
Proof using truth table:

x y x ⊓ y (x ⊓ y) ≤ K x ⊥ ⊥ ⊥ Yes ⊥ 0 ⊥ Yes ⊥ 1 ⊥ Yes ⊥ ⊤ ⊥ Yes 0 ⊥ ⊥ Yes 0 0 0 Yes 0 1 ⊥ Yes 0 ⊤ 0 Yes 1 ⊥ ⊥ Yes 1 0 ⊥ Yes 1 1 1 Yes 1 ⊤ 1 Yes ⊤ ⊥ ⊥ Yes ⊤ 0 0 Yes ⊤ 1 1 Yes ⊤ ⊤ ⊤ Yes
Algebraic approach:

Let us consider x = x pos x neg and y = y pos y neg . In B, x pos .y pos ≤ x pos and

x neg .y neg ≤ x neg , then x pos .y pos x neg .y neg ≤ K

x pos x neg . So, according to ⊓ projection in B B, (x ⊓ y) ≤ K x.

x ≤ B (x ⊞ y)

Proof using truth table: (x ⊡ y) ≤ B x Proof using truth table: x ≤ K y => (x ⊔ z) ≤ K (y ⊔ z)

x y x ⊞ y x ≤ B (x ⊞ y) ⊥ ⊥ ⊥ Yes ⊥ 0 ⊥ Yes ⊥ 1 1 Yes ⊥ ⊤ 1 Yes 0 ⊥ ⊥ Yes 0 0 0 Yes 0 1 1 Yes 0 ⊤ ⊤ Yes 1 ⊥ 1 Yes 1 0 1 Yes 1 1 1 Yes 1 ⊤ 1 Yes ⊤ ⊥ 1 Yes ⊤ 0 ⊤ Yes ⊤ 1
x y x ⊡ y (x ⊡ y) ≤ B x ⊥ ⊥ ⊥ Yes ⊥ 0 0 Yes ⊥ 1 ⊥ Yes ⊥ ⊤ 0 Yes 0 ⊥ 0 Yes 0 0 0 Yes 0 1 0 Yes 0 ⊤ 0 Yes 1 ⊥ ⊥ Yes 1 0 0 Yes 1 1 1 Yes 1 ⊤ ⊤ Yes ⊤ ⊥ 0 Yes ⊤ 0 0 Yes ⊤ 1 ⊤ Yes ⊤ ⊤ ⊤
• Truth table approach:

x y z x ⊔ z y ⊔ z x ≤ K y => (x ⊔ z) ≤ K (y ⊔ z) ⊥ ⊥ ⊥ ⊥ ⊥ Yes ⊥ ⊥ 0 0 0 Yes ⊥ ⊥ 1 1 1 Yes ⊥ ⊥ ⊤ ⊤ ⊤ Yes ⊥ 0 ⊥ ⊥ 0 Yes ⊥ 0 0 0 0 Yes ⊥ 0 1 1 ⊤ Yes ⊥ 0 ⊤ ⊤ ⊤ Yes ⊥ 1 ⊥ ⊥ 1 Yes ⊥ 1 0 0 ⊤ Yes ⊥ 1 1 1 1 Yes ⊥ 1 ⊤ ⊤ ⊤ Yes ⊥ ⊤ ⊥ ⊥ ⊤ Yes ⊥ ⊤ 0 0 ⊤ Yes ⊥ ⊤ 1 1 ⊤ Yes ⊥ ⊤ ⊤ ⊤ ⊤ Yes 0 0 ⊥ 0 0 Yes 0 0 0 0 0 Yes 0 0 1 ⊤ ⊤ Yes 0 0 ⊤ ⊤ ⊤ Yes 0 ⊤ ⊥ 0 ⊤ Yes 0 ⊤ 0 0 ⊤ Yes 0 ⊤ 1 ⊤ ⊤ Yes 0 ⊤ ⊤ ⊤ ⊤ Yes 1 1 ⊥ 1 1 Yes 1 1 0 ⊤ ⊤ Yes 1 1 1 1 1 Yes 1 1 ⊤ ⊤ ⊤ Yes 1 ⊤ ⊥ 1 ⊤ Yes 1 ⊤ 0 ⊤ ⊤ Yes 1 ⊤ 1 1 ⊤ Yes 1 ⊤ ⊤ ⊤ ⊤ Yes ⊤ ⊤ ⊥ ⊤ ⊤ Yes ⊤ ⊤ 0 ⊤ ⊤ Yes ⊤ ⊤ 1 ⊤ ⊤ Yes ⊤ ⊤ ⊤ ⊤ ⊤ Yes RR n°8138
• Algebraic apprach:

Let us consider x = x pos x neg and y = y pos y neg and z = z pos z neg . x ≤ K y =⇒

x pos ≤ y pos and x neg ≤ y neg . Thus x pos + z pos ≤ y pos + z pos and x neg + z neg ≤ y neg + z neg . So, x ⊔ z ≤ K y ⊔ z.

x ≤ K y => (x ⊓ z) ≤ K (y ⊓ z

• Truth table approach:

x y z x ⊓ z y ⊓ z x ≤ K y => (x ⊓ z) ≤ K (y ⊓ z) ⊥ ⊥ ⊥ ⊥ ⊥ Yes ⊥ ⊥ 0 ⊥ ⊥ Yes ⊥ ⊥ 1 ⊥ ⊥ Yes ⊥ ⊥ ⊤ ⊥ ⊥ Yes ⊥ 0 ⊥ ⊥ ⊥ Yes ⊥ 0 0 ⊥ 0 Yes ⊥ 0 1 ⊥ ⊥ Yes ⊥ 0 ⊤ ⊥ 0 Yes ⊥ 1 ⊥ ⊥ ⊥ Yes ⊥ 1 0 ⊥ ⊥ Yes ⊥ 1 1 ⊥ 1 Yes ⊥ 1 ⊤ ⊥ 1 Yes ⊥ ⊤ ⊥ ⊥ ⊥ Yes ⊥ ⊤ 0 ⊥ 0 Yes ⊥ ⊤ 1 ⊥ 1 Yes ⊥ ⊤ ⊤ ⊥ ⊤ Yes 0 0 ⊥ ⊥ ⊥ Yes 0 0 0 0 0 Yes 0 0 1 ⊥ ⊥ Yes 0 0 ⊤ 0 0 Yes 0 ⊤ ⊥ ⊥ ⊥ Yes 0 ⊤ 0 0 0 Yes 0 ⊤ 1 ⊥ 1 Yes 0 ⊤ ⊤ 0 ⊤ Yes 1 1 ⊥ ⊥ ⊥ Yes 1 1 0 ⊥ ⊥ Yes 1 1 1 1 1 Yes 1 1 ⊤ 1 1 Yes 1 ⊤ ⊥ ⊥ ⊥ Yes 1 ⊤ 0 ⊥ 0 Yes 1 ⊤ 1 1 1 Yes 1 ⊤ ⊤ 1 ⊤ Yes ⊤ ⊤ ⊥ ⊥ ⊥ Yes ⊤ ⊤ 0 0 0 Yes ⊤ ⊤ 1 1 1 Yes ⊤ ⊤ ⊤ ⊤ ⊤ Yes RR n°8138
• Algebraic approach:

Let us consider x = x pos x neg and y = y pos y neg and z = z pos z neg . x ≤ K y =⇒

x pos ≤ y pos and x neg ≤ y neg . Thus x pos .z pos ≤ y pos .z pos and x neg .z neg ≤ y neg .z neg . So, x ⊓ z ≤ K y ⊓ z.

x ≤ B y => (x ⊞ z) ≤ B (y ⊞ z)

• Truth table approach:

x y z x ⊞ z y ⊞ z x ≤ B y => (x ⊞ z) ≤ B (y ⊞ z) ⊥ ⊥ ⊥ ⊥ ⊥ Yes ⊥ ⊥ 0 ⊥ ⊥ Yes ⊥ ⊥ 1 1 1 Yes ⊥ ⊥ ⊤ 1 1 Yes ⊥ 1 ⊥ ⊥ 1 Yes ⊥ 1 0 ⊥ 1 Yes ⊥ 1 1 1 1 Yes ⊥ 1 ⊤ 1 1 Yes 0 ⊥ ⊥ ⊥ ⊥ Yes 0 ⊥ 0 0 ⊥ Yes 0 ⊥ 1 1 1 Yes 0 ⊥ ⊤ ⊤ 1 Yes 0 0 ⊥ ⊥ ⊥ Yes 0 0 0 0 0 Yes 0 0 1 1 1 Yes 0 0 ⊤ ⊤ ⊤ Yes 0 1 ⊥ ⊥ 1 Yes 0 1 0 0 1 Yes 0 1 1 1 1 Yes 0 1 ⊤ ⊤ 1 Yes 0 ⊤ ⊥ ⊥ 1 Yes 0 ⊤ 0 0 ⊤ Yes 0 ⊤ 1 1 1 Yes 0 ⊤ ⊤ ⊤ ⊤ Yes 1 1 ⊥ 1 1 Yes 1 1 0 1 1 Yes 1 1 1 1 1 Yes 1 1 ⊤ 1 1 Yes ⊤ 1 ⊥ 1 1 Yes ⊤ 1 0 ⊤ 1 Yes ⊤ 1 1 1 1 Yes ⊤ 1 ⊤ ⊤ 1 Yes ⊤ ⊤ ⊥ 1 1 Yes ⊤ ⊤ 0 ⊤ ⊤ Yes ⊤ ⊤ 1 1 1 Yes ⊤ ⊤ ⊤ ⊤ ⊤ Yes RR n°8138
• Algebraic approach:

Let us consider x = x pos x neg and y = y pos y neg and z = z pos z neg . x ≤ B y =⇒

x pos ≤ y pos and y neg ≤ x neg . Thus x pos + z pos ≤ y pos + z pos and y neg .z neg ≤ x neg .z neg . So, x ⊞ z ≤ B y ⊞ z.

x ≤ B y => (x ⊡ z) ≤ B (y ⊡ z

• Truth table approach:

x y z x ⊡ z y ⊡ z x ≤ B y => (x ⊡ z) ≤ B (y ⊡ z) ⊥ ⊥ ⊥ ⊥ ⊥ Yes ⊥ ⊥ 0 0 0 Yes ⊥ ⊥ 1 ⊥ ⊥ Yes ⊥ ⊥ ⊤ 0 0 Yes ⊥ 1 ⊥ ⊥ ⊥ Yes ⊥ 1 0 0 0 Yes ⊥ 1 1 ⊥ 1 Yes ⊥ 1 ⊤ 0 ⊤ Yes 0 ⊥ ⊥ 0 ⊥ Yes 0 ⊥ 0 0 0 Yes 0 ⊥ 1 0 ⊥ Yes 0 ⊥ ⊤ 0 0 Yes 0 0 ⊥ 0 0 Yes 0 0 0 0 0 Yes 0 0 1 0 0 Yes 0 0 ⊤ 0 0 Yes 0 1 ⊥ 0 ⊥ Yes 0 1 0 0 0 Yes 0 1 1 0 1 Yes 0 1 ⊤ 0 ⊤ Yes 0 ⊤ ⊥ 0 0 Yes 0 ⊤ 0 0 0 Yes 0 ⊤ 1 0 ⊤ Yes 0 ⊤ ⊤ ⊤ ⊤ Yes 1 1 ⊥ ⊥ ⊥ Yes 1 1 0 0 0 Yes 1 1 1 1 1 Yes 1 1 ⊤ ⊤ ⊤ Yes ⊤ 1 ⊥ 0 ⊥ Yes ⊤ 1 0 0 0 Yes ⊤ 1 1 ⊤ 1 Yes ⊤ 1 ⊤ ⊤ ⊤ Yes ⊤ ⊤ ⊥ 0 0 Yes ⊤ ⊤ 0 0 0 Yes ⊤ ⊤ 1 ⊤ ⊤ Yes ⊤ ⊤ ⊤ ⊤ ⊤
≤ x neg + z neg . So, x ⊡ z ≤ B y ⊡ z. ⊥ ≤ K (x ⊔ y) ≤ K ⊤ • Truth table approach: x y x ⊔ y ⊥ ≤ K (x ⊔ y) ≤ K ⊤ ⊥ ⊥ ⊥ Yes ⊥ 0 0 Yes ⊥ 1 1 Yes ⊥ ⊤ ⊤ Yes 0 ⊥ 0 Yes 0 0 0 Yes 0 1 ⊤ Yes 0 ⊤ ⊤ Yes 1 ⊥ 1 Yes 1 0 ⊤ Yes 1 1 1 Yes 1 ⊤ ⊤ Yes ⊤ ⊥ ⊤ Yes ⊤ 0 ⊤ Yes ⊤ 1 ⊤ Yes ⊤ ⊤ ⊤ Yes
• Algebraic approach:

Let us consider x = x pos x neg and y = y pos y neg . In B, 0 ≤ x pos + y pos ≤ 1 and 0 ≤

x neg + y neg ≤ 1. So, 0 0 ≤ K x pos + y pos x neg + y neg ≤ K 1 1 . Hence, ⊥ ≤ K x ⊔ y ≤ K ⊤. ⊥ ≤ K (x ⊓ y) ≤ K ⊤ • Truth table approach: RR n°8138 x y x ⊓ y ⊥ ≤ K (x ⊓ y) ≤ K ⊤ ⊥ ⊥ ⊥ Yes ⊥ 0 ⊥ Yes ⊥ 1 ⊥ Yes ⊥ ⊤ ⊥ Yes 0 ⊥ ⊥ Yes 0 0 0 Yes 0 1 ⊥ Yes 0 ⊤ 0 Yes 1 ⊥ ⊥ Yes 1 0 ⊥ Yes 1 1 1 Yes 1 ⊤ 1 Yes ⊤ ⊥ ⊥ Yes ⊤ 0 0 Yes ⊤ 1 1 Yes ⊤ ⊤ ⊤ Yes
• Algebraic approach:

Let us consider x = x pos x neg and y = y pos y neg . In B, 0 ≤ x pos + y pos ≤ 1 and 0 ≤

x neg + y neg ≤ 1. So, 0 0 ≤ K x pos .y pos x neg .y neg ≤ K 1 1 . Hence, ⊥ ≤ K x ⊓ y ≤ K ⊤. 0 ≤ B (x ⊞ y) ≤ B 1 • Truth table approach: x y x ⊞ y 0 ≤ B (x ⊞ y) ≤ B 1 ⊥ ⊥ ⊥ Yes ⊥ 0 ⊥ Yes ⊥ 1 1 Yes ⊥ ⊤ 1 Yes 0 ⊥ ⊥ Yes 0 0 0 Yes 0 1 1 Yes 0 ⊤ ⊤ Yes 1 ⊥ 1 Yes 1 0 1 Yes 1 1 1 Yes 1 ⊤ 1 Yes ⊤ ⊥ 1 Yes ⊤ 0 ⊤ Yes ⊤ 1 1 Yes ⊤ ⊤ ⊤ Yes RR n°8138
• Algebraic approach:

Let us consider x = x pos x neg and y = y pos y neg . In B, 0 ≤ x pos + y pos ≤ 1 and 0 ≤

x neg .y neg ≤ 1. So, 0 1 ≤ B x pos + y pos x neg .y neg ≤ K 1 0 . Hence, 0 ≤ B x ⊞ y ≤ K 1. 0 ≤ B (x ⊡ y) ≤ B 1
• Truth table approach:

x y x ⊡ y 0 ≤ B (x ⊡ y) ≤ B 1 ⊥ ⊥ ⊥ Yes ⊥ 0 0 Yes ⊥ 1 ⊥ Yes ⊥ ⊤ 0 Yes 0 ⊥ 0 Yes 0 0 0 Yes 0 1 0 Yes 0 ⊤ 0 Yes 1 ⊥ ⊥ Yes 1 0 0 Yes 1 1 1 Yes 1 ⊤ ⊤ Yes ⊤ ⊥ 0 Yes ⊤ 0 0 Yes ⊤ 1 ⊤ Yes ⊤ ⊤ ⊤ Yes
• Algebraic approach:

Let us consider x = x pos x neg and y = y pos y neg . In B, 0 ≤ x pos .y pos ≤ 1 and 0 ≤

x neg + y neg ≤ 1. So, 0 1 ≤ B x pos + y pos x neg .y neg ≤ K 1 0 . Hence, 0 ≤ B x ⊡ y ≤ K 1.

RR n°8138

x ≤ K y => ¬x ≤ K ¬y

• Truth table approach:

x y ¬x ¬y x ≤ K y => ¬x ≤ K ¬y ⊥ ⊥ ⊥ ⊥ Yes ⊥ 0 ⊥ 1 Yes ⊥ 1 ⊥ 0 Yes ⊥ ⊤ ⊥ ⊤ Yes 0 0 1 1 Yes 0 ⊤ 1 ⊤ Yes 1 1 0 0 Yes 1 ⊤ 0 ⊤ Yes ⊤ ⊤ ⊤ ⊤ Yes • Algebraic approach:
Let us consider x = x pos x neg and y = y pos y neg . x ≤ K y =⇒ x pos ≤ y pos and x neg ≤ y neg . Thus, x neg x pos ≤ K y neg y pos . So, ¬x ≤ K ¬y.

x ≤ B y => ¬y ≤ B ¬x

• Truth table approach:

x y ¬x ¬y x ≤ B y => ¬y ≤ B ¬x ⊥ ⊥ ⊥ ⊥ Yes ⊥ 1 ⊥ 0 Yes 0 ⊥ 1 ⊥ Yes 0 0 1 1 Yes 0 1 1 0 Yes 0 ⊤ 1 ⊤ Yes 1 1 0 0 Yes ⊤ 1 ⊤ 0 Yes ⊤ ⊤ ⊤ ⊤ Yes • Algebraic approach:
Let us consider x = x pos x neg and y = y pos y neg . x ≤ B y =⇒ x pos ≤ y pos and y neg ≤

x neg . Thus, y neg y pos ≤ B x neg x pos . So, ¬y ≤ B ¬x.

RR n°8138

x ≤ B y and z ≤ B t => (x ⊔ z) ≤ B (y ⊔ t)

• Truth table approach:

x y z t x ⊔ z y ⊔ t (x ⊔ z) ≤ B (y ⊔ t) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ Yes ⊥ ⊥ ⊥ 1 ⊥ 1 Yes ⊥ ⊥ 0 ⊥ 0 ⊥ Yes ⊥ ⊥ 0 0 0 0 Yes ⊥ ⊥ 0 1 0 1 Yes ⊥ ⊥ 0 ⊤ 0 ⊤ Yes ⊥ ⊥ 1 1 1 1 Yes ⊥ ⊥ ⊤ 1 ⊤ 1 Yes ⊥ ⊥ ⊤ ⊤ ⊤ ⊤ Yes ⊥ 1 ⊥ ⊥ ⊥ 1 Yes ⊥ 1 ⊥ 1 ⊥ 1 Yes ⊥ 1 0 ⊥ 0 1 Yes ⊥ 1 0 0 0 ⊤ Yes ⊥ 1 0 1 0 1 Yes ⊥ 1 0 ⊤ 0 ⊤ Yes ⊥ 1 1 1 1 1 Yes ⊥ 1 ⊤ 1 ⊤ 1 Yes ⊥ 1 ⊤ ⊤ ⊤ ⊤ Yes 0 ⊥ ⊥ ⊥ 0 ⊥ Yes 0 ⊥ ⊥ 1 0 1 Yes 0 ⊥ 0 ⊥ 0 ⊥ Yes 0 ⊥ 0 0 0 0 Yes 0 ⊥ 0 1 0 1 Yes 0 ⊥ 0 ⊤ 0 ⊤ Yes 0 ⊥ 1 1 ⊤ 1 Yes 0 ⊥ ⊤ 1 ⊤ 1 Yes 0 ⊥ ⊤ ⊤ ⊤ ⊤ Yes 0 0 ⊥ ⊥ 0 0 Yes 0 0 ⊥ 1 0 ⊤ Yes 0 0 0 ⊥ 0 0 Yes 0 0 0 0 0 0 Yes 0 0 0 1 0 ⊤ Yes 0 0 0 ⊤ 0 ⊤ Yes 0 0 1 1 ⊤ ⊤ Yes 0 0 ⊤ 1 ⊤ ⊤ Yes 0 0 ⊤ ⊤ ⊤ ⊤ Yes x y z t x ⊔ z y ⊔ t (x ⊔ z) ≤ B (y ⊔ t) 0 1 ⊥ ⊥ 0 1 Yes 0 1 ⊥ 1 0 1 Yes 0 1 0 ⊥ 0 1 Yes 0 1 0 0 0 ⊤ Yes 0 1 0 1 0 1 Yes 0 1 0 ⊤ 0 ⊤ Yes 0 1 1 1 ⊤ 1 Yes 0 1 ⊤ 1 ⊤ 1 Yes 0 1 ⊤ ⊤ ⊤ ⊤ Yes 0 ⊤ ⊥ ⊥ 0 ⊤ Yes 0 ⊤ ⊥ 1 0 ⊤ Yes 0 ⊤ 0 ⊥ 0 ⊤ Yes 0 ⊤ 0 0 0 ⊤ Yes 0 ⊤ 0 1 0 ⊤ Yes 0 ⊤ 0 ⊤ 0 ⊤ Yes 0 ⊤ 1 1 ⊤ ⊤ Yes 0 ⊤ ⊤ 1 ⊤ ⊤ Yes 0 ⊤ ⊤ ⊤ ⊤ ⊤ Yes 1 1 ⊥ ⊥ 1 1 Yes 1 1 ⊥ 1 1 1 Yes 1 1 0 ⊥ ⊤ 1 Yes 1 1 0 0 ⊤ ⊤ Yes 1 1 0 1 ⊤ 1 Yes 1 1 0 ⊤ ⊤ ⊤ Yes 1 1 1 1 1 1 Yes 1 1 ⊤ 1 ⊤ 1 Yes 1 1 ⊤ ⊤ ⊤ ⊤ Yes ⊤ 1 ⊥ ⊥ ⊤ 1 Yes ⊤ 1 ⊥ 1 ⊤ 1 Yes ⊤ 1 0 ⊥ ⊤ 1 Yes ⊤ 1 0 0 ⊤ ⊤ Yes ⊤ 1 0 1 ⊤ 1 Yes ⊤ 1 0 ⊤ ⊤ ⊤ Yes ⊤ 1 1 1 ⊤ 1 Yes ⊤ 1 ⊤ 1 ⊤ 1 Yes ⊤ 1 ⊤ ⊤ ⊤ ⊤ Yes ⊤ ⊤ ⊥ ⊥ ⊤ ⊤ Yes ⊤ ⊤ ⊥ 1 ⊤ ⊤ Yes ⊤ ⊤ 0 ⊥ ⊤ ⊤ Yes ⊤ ⊤ 0 0 ⊤ ⊤ Yes ⊤ ⊤ 0 1 ⊤ ⊤ Yes ⊤ ⊤ 0 ⊤ ⊤ ⊤ Yes ⊤ ⊤ 1 1 ⊤ ⊤ Yes ⊤ ⊤ ⊤ 1 ⊤ ⊤ Yes ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ Yes
• Algebraic approach:

x (y ⊔ t).

x ≤ B y and z ≤ B t => (x ⊓ z) ≤ B (y ⊓ t)

• Truth Table approach:

x y z t x ⊓ z y ⊓ t (x ⊓ z) ≤ B (y ⊓ t) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ Yes ⊥ ⊥ ⊥ 1 ⊥ ⊥ Yes ⊥ ⊥ 0 ⊥ ⊥ ⊥ Yes ⊥ ⊥ 0 0 ⊥ ⊥ Yes ⊥ ⊥ 0 1 ⊥ ⊥ Yes ⊥ ⊥ 0 ⊤ ⊥ ⊥ Yes ⊥ ⊥ 1 1 ⊥ ⊥ Yes ⊥ ⊥ ⊤ 1 ⊥ ⊥ Yes ⊥ ⊥ ⊤ ⊤ ⊥ ⊥ Yes ⊥ 1 ⊥ ⊥ ⊥ ⊥ Yes ⊥ 1 ⊥ 1 ⊥ 1 Yes ⊥ 1 0 ⊥ ⊥ ⊥ Yes ⊥ 1 0 0 ⊥ ⊥ Yes ⊥ 1 0 1 ⊥ 1 Yes ⊥ 1 0 ⊤ ⊥ 1 Yes ⊥ 1 1 1 ⊥ 1 Yes ⊥ 1 ⊤ 1 ⊥ 1 Yes ⊥ 1 ⊤ ⊤ ⊥ 1 Yes 0 ⊥ ⊥ ⊥ ⊥ ⊥ Yes 0 ⊥ ⊥ 1 ⊥ ⊥ Yes 0 ⊥ 0 ⊥ 0 ⊥ Yes 0 ⊥ 0 0 0 ⊥ Yes 0 ⊥ 0 1 0 ⊥ Yes 0 ⊥ 0 ⊤ 0 ⊥ Yes 0 ⊥ 1 1 ⊥ ⊥ Yes 0 ⊥ ⊤ 1 0 ⊥ Yes 0 ⊥ ⊤ ⊤ 0 ⊥ Yes 0 0 ⊥ ⊥ ⊥ ⊥ Yes 0 0 ⊥ 1 ⊥ ⊥ Yes 0 0 0 ⊥ 0 ⊥ Yes 0 0 0 0 0 0 Yes 0 0 0 1 0 ⊥ Yes 0 0 0 ⊤ 0 0 Yes 0 0 1 1 ⊥ ⊥ Yes 0 0 ⊤ 1 0 ⊥ Yes 0 0 ⊤ ⊤ 0 0 Yes RR n°8138 x y z t x ⊓ z y ⊓ t (x ⊓ z) ≤ B (y ⊓ t) 0 1 ⊥ ⊥ ⊥ ⊥ Yes 0 1 ⊥ 1 ⊥ 1 Yes 0 1 0 ⊥ 0 ⊥ Yes 0 1 0 0 0 ⊥ Yes 0 1 0 1 0 1 Yes 0 1 0 ⊤ 0 1 Yes 0 1 1 1 ⊥ 1 Yes 0 1 ⊤ 1 0 1 Yes 0 1 ⊤ ⊤ 0 1 Yes 0 ⊤ ⊥ ⊥ ⊥ ⊥ Yes 0 ⊤ ⊥ 1 ⊥ 1 Yes 0 ⊤ 0 ⊥ 0 ⊥ Yes 0 ⊤ 0 0 0 0 Yes 0 ⊤ 0 1 0 1 Yes 0 ⊤ 0 ⊤ 0 ⊤ Yes 0 ⊤ 1 1 ⊥ 1 Yes 0 ⊤ ⊤ 1 0 1 Yes 0 ⊤ ⊤ ⊤ 0 ⊤ Yes 1 1 ⊥ ⊥ ⊥ ⊥ Yes 1 1 ⊥ 1 ⊥ 1 Yes 1 1 0 ⊥ ⊥ ⊥ Yes 1 1 0 0 ⊥ ⊥ Yes 1 1 0 1 ⊥ 1 Yes 1 1 0 ⊤ ⊥ 1 Yes 1 1 1 1 1 1 Yes 1 1 ⊤ 1 1 1 Yes 1 1 ⊤ ⊤ 1 1 Yes ⊤ 1 ⊥ ⊥ ⊥ ⊥ Yes ⊤ 1 ⊥ 1 ⊥ 1 Yes ⊤ 1 0 ⊥ 0 ⊥ Yes ⊤ 1 0 0 0 ⊥ Yes ⊤ 1 0 1 0 1 Yes ⊤ 1 0 ⊤ 0 1 Yes ⊤ 1 1 1 1 1 Yes ⊤ 1 ⊤ 1 ⊤ 1 Yes ⊤ 1 ⊤ ⊤ ⊤ 1 Yes ⊤ ⊤ ⊥ ⊥ ⊥ ⊥ Yes ⊤ ⊤ ⊥ 1 ⊥ 1 Yes ⊤ ⊤ 0 ⊥ 0 ⊥ Yes ⊤ ⊤ 0 0 0 0 Yes ⊤ ⊤ 0 1 0 1 Yes ⊤ ⊤ 0 ⊤ 0 ⊤ Yes ⊤ ⊤ 1 1 1 1 Yes ⊤ ⊤ ⊤ 1 ⊤ 1 Yes ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ Yes
• Algebraic approach:

x

RR n°8138

x ≤ K y and z ≤ K t => (x ⊞ z) ≤ K (y ⊞ t)

• Truth table approach:

x y z t x ⊞ z y ⊞ t (x ⊞ z) ≤ K (y ⊞ t) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ Yes ⊥ ⊥ ⊥ 0 ⊥ ⊥ Yes ⊥ ⊥ ⊥ 1 ⊥ 1 Yes ⊥ ⊥ ⊥ ⊤ ⊥ 1 Yes ⊥ ⊥ 0 0 ⊥ ⊥ Yes ⊥ ⊥ 0 ⊤ ⊥ 1 Yes ⊥ ⊥ 1 1 1 1 Yes ⊥ ⊥ 1 ⊤ 1 1 Yes ⊥ ⊥ ⊤ ⊤ 1 1 Yes ⊥ 0 ⊥ ⊥ ⊥ ⊥ Yes ⊥ 0 ⊥ 0 ⊥ 0 Yes ⊥ 0 ⊥ 1 ⊥ 1 Yes ⊥ 0 ⊥ ⊤ ⊥ ⊤ Yes ⊥ 0 0 0 ⊥ 0 Yes ⊥ 0 0 ⊤ ⊥ ⊤ Yes ⊥ 0 1 1 1 1 Yes ⊥ 0 1 ⊤ 1 ⊤ Yes ⊥ 0 ⊤ ⊤ 1 ⊤ Yes ⊥ 1 ⊥ ⊥ ⊥ 1 Yes ⊥ 1 ⊥ 0 ⊥ 1 Yes ⊥ 1 ⊥ 1 ⊥ 1 Yes ⊥ 1 ⊥ ⊤ ⊥ 1 Yes ⊥ 1 0 0 ⊥ 1 Yes ⊥ 1 0 ⊤ ⊥ 1 Yes ⊥ 1 1 1 1 1 Yes ⊥ 1 1 ⊤ 1 1 Yes ⊥ 1 ⊤ ⊤ 1 1 Yes ⊥ ⊤ ⊥ ⊥ ⊥ 1 Yes ⊥ ⊤ ⊥ 0 ⊥ ⊤ Yes ⊥ ⊤ ⊥ 1 ⊥ 1 Yes ⊥ ⊤ ⊥ ⊤ ⊥ ⊤ Yes ⊥ ⊤ 0 0 ⊥ ⊤ Yes ⊥ ⊤ 0 ⊤ ⊥ ⊤ Yes ⊥ ⊤ 1 1 1 1 Yes ⊥ ⊤ 1 ⊤ 1 ⊤ Yes ⊥ ⊤ ⊤ ⊤ 1 ⊤ Yes x y z t x ⊞ z y ⊞ t (x ⊞ z) ≤ K (y ⊞ t) 0 0 ⊥ ⊥ ⊥ ⊥ Yes 0 0 ⊥ 0 ⊥ 0 Yes 0 0 ⊥ 1 ⊥ 1 Yes 0 0 ⊥ ⊤ ⊥ ⊤ Yes 0 0 0 0 0 0 Yes 0 0 0 ⊤ 0 ⊤ Yes 0 0 1 1 1 1 Yes 0 0 1 ⊤ 1 ⊤ Yes 0 0 ⊤ ⊤ ⊤ ⊤ Yes 0 ⊤ ⊥ ⊥ ⊥ 1 Yes 0 ⊤ ⊥ 0 ⊥ ⊤ Yes 0 ⊤ ⊥ 1 ⊥ 1 Yes 0 ⊤ ⊥ ⊤ ⊥ ⊤ Yes 0 ⊤ 0 0 0 ⊤ Yes 0 ⊤ 0 ⊤ 0 ⊤ Yes 0 ⊤ 1 1 1 1 Yes 0 ⊤ 1 ⊤ 1 ⊤ Yes 0 ⊤ ⊤ ⊤ ⊤ ⊤ Yes 1 1 ⊥ ⊥ 1 1 Yes 1 1 ⊥ 0 1 1 Yes 1 1 ⊥ 1 1 1 Yes 1 1 ⊥ ⊤ 1 1 Yes 1 1 0 0 1 1 Yes 1 1 0 ⊤ 1 1 Yes 1 1 1 1 1 1 Yes 1 1 1 ⊤ 1 1 Yes 1 1 ⊤ ⊤ 1 1 Yes 1 ⊤ ⊥ ⊥ 1 1 Yes 1 ⊤ ⊥ 0 1 ⊤ Yes 1 ⊤ ⊥ 1 1 1 Yes 1 ⊤ ⊥ ⊤ 1 ⊤ Yes 1 ⊤ 0 0 1 ⊤ Yes 1 ⊤ 0 ⊤ 1 ⊤ Yes 1 ⊤ 1 1 1 1 Yes 1 ⊤ 1 ⊤ 1 ⊤ Yes 1 ⊤ ⊤ ⊤ 1 ⊤ Yes ⊤ ⊤ ⊥ ⊥ 1 1 Yes ⊤ ⊤ ⊥ 0 1 ⊤ Yes ⊤ ⊤ ⊥ 1 1 1 Yes ⊤ ⊤ ⊥ ⊤ 1 ⊤ Yes ⊤ ⊤ 0 0 ⊤ ⊤ Yes ⊤ ⊤ 0 ⊤ ⊤ ⊤ Yes ⊤ ⊤ 1 1 1 1 Yes ⊤ ⊤ 1 ⊤ 1 ⊤ Yes ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ Yes
• Algebraic approach:

x x ≤ K y and z ≤ K t => (x ⊡ z) ≤ K (y ⊡ t)

• Truth table approach:

x y z t x ⊡ z y ⊡ t (x ⊡ z) ≤ K (y ⊡ t) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ Yes ⊥ ⊥ ⊥ 0 ⊥ 0 Yes ⊥ ⊥ ⊥ 1 ⊥ ⊥ Yes ⊥ ⊥ ⊥ ⊤ ⊥ 0 Yes ⊥ ⊥ 0 0 0 0 Yes ⊥ ⊥ 0 ⊤ 0 0 Yes ⊥ ⊥ 1 1 ⊥ ⊥ Yes ⊥ ⊥ 1 ⊤ ⊥ 0 Yes ⊥ ⊥ ⊤ ⊤ 0 0 Yes ⊥ 0 ⊥ ⊥ ⊥ 0 Yes ⊥ 0 ⊥ 0 ⊥ 0 Yes ⊥ 0 ⊥ 1 ⊥ 0 Yes ⊥ 0 ⊥ ⊤ ⊥ 0 Yes ⊥ 0 0 0 0 0 Yes ⊥ 0 0 ⊤ 0 0 Yes ⊥ 0 1 1 ⊥ 0 Yes ⊥ 0 1 ⊤ ⊥ 0 Yes ⊥ 0 ⊤ ⊤ 0 0 Yes ⊥ 1 ⊥ ⊥ ⊥ ⊥ Yes ⊥ 1 ⊥ 0 ⊥ 0 Yes ⊥ 1 ⊥ 1 ⊥ 1 Yes ⊥ 1 ⊥ ⊤ ⊥ ⊤ Yes ⊥ 1 0 0 0 0 Yes ⊥ 1 0 ⊤ 0 ⊤ Yes ⊥ 1 1 1 ⊥ 1 Yes ⊥ 1 1 ⊤ ⊥ ⊤ Yes ⊥ 1 ⊤ ⊤ 0 ⊤ Yes ⊥ ⊤ ⊥ ⊥ ⊥ 0 Yes ⊥ ⊤ ⊥ 0 ⊥ 0 Yes ⊥ ⊤ ⊥ 1 ⊥ ⊤ Yes ⊥ ⊤ ⊥ ⊤ ⊥ ⊤ Yes ⊥ ⊤ 0 0 0 0 Yes ⊥ ⊤ 0 ⊤ 0 ⊤ Yes ⊥ ⊤ 1 1 ⊥ ⊤ Yes ⊥ ⊤ 1 ⊤ ⊥ ⊤ Yes ⊥ ⊤ ⊤ ⊤ 0 ⊤ Yes RR n°8138
⊤ 0 ⊤ 0 ⊤ Yes 0 ⊤ 1 1 0 ⊤ Yes 0 ⊤ 1 ⊤ 0 ⊤ Yes 0 ⊤ ⊤ ⊤ 0 ⊤ Yes 1 1 ⊥ ⊥ ⊥ ⊥ Yes 1 1 ⊥ 0 ⊥ 0 Yes 1 1 ⊥ 1 ⊥ 1 Yes 1 1 ⊥ ⊤ ⊥ ⊤ Yes 1 1 0 0 0 0 Yes 1 1 0 ⊤ 0 ⊤ Yes 1 1 1 1 1 1 Yes 1 1 1 ⊤ 1 ⊤ Yes 1 1 ⊤ ⊤ ⊤ ⊤ Yes 1 ⊤ ⊥ ⊥ ⊥ 0 Yes 1 ⊤ ⊥ 0 ⊥ 0 Yes 1 ⊤ ⊥ 1 ⊥ ⊤ Yes 1 ⊤ ⊥ ⊤ ⊥ ⊤ Yes 1 ⊤ 0 0 0 0 Yes 1 ⊤ 0 ⊤ 0 ⊤ Yes 1 ⊤ 1 1 1 ⊤ Yes 1 ⊤ 1 ⊤ 1 ⊤ Yes 1 ⊤ ⊤ ⊤ ⊤ ⊤ Yes ⊤ ⊤ ⊥ ⊥ 0 0 Yes ⊤ ⊤ ⊥ 0 0 0 Yes ⊤ ⊤ ⊥ 1 0 ⊤ Yes ⊤ ⊤ ⊥ ⊤ 0 ⊤ Yes ⊤ ⊤ 0 0 0 0 Yes ⊤ ⊤ 0 ⊤ 0 ⊤ Yes ⊤ ⊤ 1 1 ⊤ ⊤ Yes ⊤ ⊤ 1 ⊤ ⊤ ⊤ Yes ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ Yes
• Algebraic approach:

x

  us consider S a set of signals, an environment E is a function who defines a Boolean status (0 means absent, 1 means present) for each signal: E: S → B. Then, semantics defines transition of the form P O -→ I δ (P) where P is a synchronous program, I an input environment and O the resulting output environment, δ (P) is the derivative of P, i.e the new program that will react to the next input environment. The reaction O 1 ,O 2 ,...,O n ,... to an input environment sequence I 1 ,I 2 ,...,I n ,... results from the sequence of transitions:

Figure 1 :

 1 Figure 1: Scott order for B ⊥ .

Figure 2 : 4 -

 24 Figure 2: 4-valued algebras ≤ B and ≤ K orders

  (a) x = ⊥: ∀y ∈ ξ , x ⊔ y = y. On the other hand e 3 (x) = (0, 0) then ∀z ∈ B × B, e 3 (x) ≤ K z and then e 3 (x) ⊔ z = z and in particular for e 3 (y). (b) x = 0: the proof falls in two: (1) y = ⊥ or y = 0 , 0 ⊔ y = 0 and e 3 (0 ⊔ y) = (0, 1), on the other hand, e 3 (0) = (0, 1) and e 3 (⊥) = (0, 0) so if y = ⊥ or y = 0, e 3 (0) ⊔ e 3 (y) = (0, 1); (2) y = 1 or y = ⊤ , 0 ⊔ y = ⊤ and e 3 (0 ⊔ y) = (1, 1), on the other hand, e 3 (1) = (1, 0) and e 3 (⊤) = (1, 1) so e 3 (0) ⊔ e 3 (y) = (1, 1). (c) x = 1 the proof is similar to the previous case (d) x = ⊤, ∀y ∈ ξ , x ⊔ y = x. On the other hand, e 3 (x) = (1, 1) then ∀z ∈ B × B, z ≤ K e 3 (x)z and in particular e 3 (y) so e 3 (x) ⊔ e 3 (y) = e 3 (x).

3. e 3

 3 (x ⊞ y) = e 3 (x) ⊞ e 3 (y): (a) x = ⊥: the proof falls in two: (1) y = ⊥ or y = 0, ⊥ ⊞ y = ⊥ and so e 3 (⊥ ⊔ y) = (0, 0), on the other hand, e 3 (⊥) = (0, 0) and e 3 (0) = (0, 1) and then e 3 (y) ≤ B e 3 (⊥), hence e 3 (⊥) ⊞ e 3 (y) = e 3 (⊥) = (0, 0); (2) y = 1 or y = ⊤, x ⊞ y = 1 and e 3 (x ⊞ y) = (1, 0). On the other hand, e 3 (1) = (1, 0) and e 3 (⊤) = (1, 1), so e 3 (⊥) ⊞ (0, 1) = (0, 1) and e 3 (⊥) ⊞ (1, 1) = (0, 1). (b) x = 0: 0 ⊞ y = y in Algebra5, on the other hand in B B, we have the ordering: (0, 1) ≤ B (0, 0) ≤ B (1, 0) and (0, 1) ≤ B (1, 1) ≤ B (1, 0) thus e 3 (0) ⊞ e 3 (y) = e 3 (y). RR n°8138 (c) x = 1: 1 ⊞ y = 1 in Algebra5. On the other hand, (1, 0) is the upper element of B B, thus (1, 0) ⊞ z = (1, 0), hence the equality holds. (d) x = ⊤: the proof is symmetric to case (a).

Figure 3 :

 3 Figure 3: The Karnaughs table for ⊔ .

Figure 4 :A. 1 . 3 ⊞

 413 Figure 4: The Karnaughs table of ⊓ operator.

Figure 5 :A. 1 . 4 ⊡

 514 Figure 5: The Karnaughs table for ⊞ operator.

Figure 6 :

 6 Figure 6: The Karnaughs table for ⊡ operator.

  y ⊡ t (x ⊡ z) ≤ K (y ⊡ t)

Table 1 :

 1 Logical properties of the considered algebras

	RR n°8138

Table 2 :

 2 ≤ B and ≤

K properties in LE2008 and Algebra

[START_REF] André | Synccharts: un modèle graphique synchrone pour système réactifs complexes[END_REF][START_REF] Krassimir | On Intuitionistic Fuzzy Sets Theory[END_REF][START_REF] Pigozzi | Multi-valued logic programming semantics: An algebraic approach[END_REF][START_REF] Benveniste | Synchronous programming with events and relations : the signal language and its semantics[END_REF]

. For Algebra5, properties are proved in appendix A.3.

  table. Any other encoding can be looked by permutation and gives equivalent solutions:

	Symbol coding 1 coding 2 coding 3
	⊥	00	00	00
	0	11	10	01
	1	01	11	10
	⊤	10	01	11

Table 3 :

 3 Encoding rules for Algebra5 operators

	RR n°8138

Table 4 :

 4

Boolean encoding of LE2008 and Algebra(2,3,4,5) with respect to Coding3 Property 1. Algebra5 and B B are isomorphic.

  Algebraic approach:

	(	x pos x neg	⊞	y pos y neg	)⊞	z pos z neg	=	x pos + y pos x neg . y neg	⊞	z pos z neg	=	(x pos + y pos ) + z pos (x neg . y neg ) . z neg	=
	x pos + (y pos + z pos ) x neg . (y neg . z neg )	=	x pos x neg	⊞	y pos + z pos y neg . z neg	=	x pos x neg	⊞(	y pos y neg	⊞	z pos z neg	)
	RR n°8138

  Algebraic approach:

	x pos x neg	⊔	x pos x neg	=	x pos + x pos x neg + x neg	=	x pos x neg
	x pos x neg	⊓	x pos x neg	=	x pos . x pos x neg . x neg	=	x pos x neg
	x pos x neg	⊞	x pos x neg	=	x pos + x pos x neg . x neg	=	x pos x neg
	x pos x neg	⊡	x pos x neg	=	x pos . x pos x neg + x neg	=	x pos x neg

  pos + y pos ) . x pos (x neg + y neg ) . x neg =x pos . x pos + y pos . x pos x neg . x neg + y neg . x neg == x pos + y pos . x pos x neg + y neg . x neg

	(x ⊓ y) ⊔ x = x
	Proof. We consider both approaches.
	1. Truth table approach:
	Algebraic approach:
	(	x pos x neg	⊔	y pos y neg	)⊓	x pos x neg	=	x pos + y pos x neg + y neg	⊓	x pos x neg	=	(x =	x pos x neg

  neg . y pos ) + x pos (x pos + y neg ) . x neg = x neg . y pos + x pos x pos . x neg + y neg . x neg = x pos + y pos x neg . y neg Wrong case example:x=⊥, y=1 from truth table. neg + y pos ) . x pos (x pos . y neg ) + x neg = x neg . x pos + y pos . x pos x pos . y neg + x neg = x pos . y pos x neg + y neg Wrong case example:x=⊥, y=0 from truth table. . y pos + y pos . z pos + x neg . z pos (x neg + y neg ) . (y neg + z neg ) . (x pos + z neg ) x pos . y pos + x neg . z pos (x neg + y neg ) . (x pos + z neg ) Wrong case example:x=⊥,y=1, z=1 from truth table.(x ⊞ y) ⊡ (y ⊞ z) ⊡ (¬x ⊞ z) = (x ⊞ y) ⊡ (¬x ⊞ z) pos + y pos) . (y pos + z pos ) . (x neg + z pos ) (x neg . y neg ) + (y neg . z neg ) + (x pos . z neg ) pos + y pos ) . (x neg + z pos ) (x neg . y neg ) + (x pos . z neg )

				Wrong case example:x=⊥, y=0, from truth table.
	¬x ⊡ y ⊞ x = x ⊞ y x pos x neg ⊡ y pos y neg	⊞ ¬	x pos x neg	⊡	z pos z neg	=	x pos . y pos x neg + y neg		⊞	x neg . z pos x pos + z neg	=
	Proof. Algebraic approach:
	¬	x pos x neg	⊡	y pos y neg	⊞	x pos x neg	=	x neg x pos	⊡	y pos y neg	⊞	x pos x neg		=	x neg . y pos x pos + y neg	⊞	x pos x neg	=
	(x (¬x ⊞ y) ⊡ x = x ⊡ y
	Proof. Algebraic approach:
	Proof. Algebraic approach:
	¬	x pos x neg (	⊞ x pos x neg	y pos y neg ⊞	⊡ y pos y neg	x pos x neg ) ⊡ (	= y pos x neg x pos y neg ⊞	⊞ z pos y pos y neg z neg ) ⊡ (¬ ⊡	x pos x neg x pos x neg	= ⊞	x neg + y pos x pos . y neg z pos z neg ) =	⊡	x pos x neg	=
	Algebraic approach: ( x pos x neg x pos + y pos x neg . y neg ⊡ y pos + z pos ⊓ y neg . z neg (x At the other hand: y pos y neg ) ⊔ x pos x neg = x pos . y pos x neg . y neg (x pos . y pos ) + x pos (x neg . y neg ) + x neg = x pos x neg ⊡ x neg + z pos x pos . z neg = (x Proof. Algebraic approach: x pos x neg ⊞ y pos y neg ⊡ ¬ x pos x neg ⊞ z pos z neg = x pos + y pos x neg . y neg		⊔ ⊡	x pos x neg x neg + z pos = x pos . z neg	=
	(x ⊡ y) ⊔ x = x Proof. Algebraic approach: x pos x neg ⊡ y pos y neg ) ⊔ x pos x neg x pos x neg ⊡ y pos y neg x pos . y pos x neg + y neg ⊞ y pos . z pos y neg + z neg x At the other hand: = x pos . y pos x neg + y neg ⊔ x pos x neg ⊞ y pos y neg ⊡ z pos z neg ⊞ ¬ ⊞ x neg . z pos x pos + z neg = (x Wrong case example:x=⊥,y=0, z=0 = x pos x neg	(x pos . y pos ) + x pos (x neg + y neg ) + x neg ⊡ z pos z neg =	=
								x pos x neg + y neg		=	x pos x neg
	RR n°8138 RR n°8138 RR n°8138

x ⊡ y ⊞ y ⊡ z + ¬x ⊡ z = x ⊡ y ⊞ ¬x ⊡ z pos

  =⇒x pos ≤ y pos and y neg ≤ x neg . Thus x pos .z pos ≤ y pos .z pos and y neg + z neg

	Let us consider x =	x pos x neg	and y =	y pos y neg	and z =	z pos z neg	. x ≤ B y
					Yes
	• Algebraic approach:
	RR n°8138

  pos ≤ t pos and t neg ≤ z neg . Then, we have in B, x pos + z pos ≤ y pos + t pos and RR n°8138 y neg + t neg ≤ x neg + z neg . Thus, x pos + z pos x neg + z neg ≤ B y pos + t pos y neg + t neg . So, (x ⊔ z) ≤ B

	pos x neg	≤ B	y pos y neg	=⇒ x pos ≤ y pos and y neg ≤ x neg . Similarly,	z pos z neg	≤ B	t pos t neg	=⇒

z

  pos ≤ t pos and t neg ≤ z neg . Then, we have in B, x pos .z pos ≤ y pos .t pos and y neg .t neg ≤ RR n°8138 x neg .z neg . Thus, x pos .z pos x neg .z neg ≤ B y pos .t pos y neg .t neg . So, (x ⊓ z) ≤ B (y ⊓ t).

	pos x neg	≤ B	y pos y neg	=⇒ x pos ≤ y pos and y neg ≤ x neg . Similarly,	z pos z neg	≤ B	t pos t neg	=⇒

z

  =⇒ z pos ≤ t pos and z neg ≤ t neg . Then, we have in B, x pos +z pos ≤ y pos +t pos and x neg .z neg ≤ y neg .t neg . Thus. x pos + z pos x neg .z neg ≤ K y pos + t pos y neg .t neg . So, x⊞z ≤ K y⊞t.

	t pos
	t neg
	pos x neg	≤ K	y pos y neg	=⇒ x pos ≤ y pos and x neg ≤ y neg . Similarly,	z pos z neg	≤ K
	RR n°8138

  =⇒ z pos ≤ t pos and z neg ≤ t neg . Then, we have in B, x pos .z pos ≤ y pos .t pos and x neg + z neg ≤ y neg + t neg . Thus.x pos .z pos x neg + z neg ≤ K y pos .t pos y neg + t neg .So, x ⊡ z ≤ K y⊡ t.

	t pos
	t neg
	pos x neg	≤ K	y pos y neg	=⇒ x pos ≤ y pos and x neg ≤ y neg . Similarly,	z pos z neg	≤ K
	RR n°8138

RR n°8138

in Lustre declarative language they are called flows RR n°8138

this definition is from Wikipedia.RR n°8138

RR n°8138

we denote the meet and join operations with respect to ≤ B order by ⊡ and ⊞ ; the meet and join operations with respect to ≤ K order by ⊔ and ⊓ and the meet and join operation in the underlying lattice L by + and .RR n°8138

A.2.5 Finalization Laws FL(x ⊞ y) = FL(x) + FL(y) Proof. We consider both approaches.

Truth table approach:

x y x ⊞ y FL(x ⊞ y) FL(x) FL(y) FL(x) + FL(y)

Note: / 0 means don't care. FL(x ⊞ y) and FL(x) + FL(y) are compatible about (⊤, ⊥) or (⊥, ⊤). FL(x ⊡ y) = FL(x).FL(y)

Algebraic approach

Proof. We consider both approaches.

Truth table approach:

x y x ⊡ y FL(x ⊡ y) FL(x) FL(y) FL(x).FL(y) All the next equations are modulo 3. To keep a light writing, this property will be understanding and we write

About the imply operator →, each (x, y) of the truth table fixes a specific valuation of this equation:

The final equation takes the form:

x → y = x 2 .y 2 + 2.x 2 .y + 2.x.y 2 + 2.x.y + 2.x + 1 (mod.3) ∀x ∈ {0, 1, 2}, ∀y ∈ {0, 1, 2} About the neg operator ¬, each x value of the truth table fixes a specific evaluation of this equation. y has no effect (unary operator), so:

The final equation takes the form: