Fatou's Lemma and the Lebesgue's Convergence Theorem
In this article we prove the Fatou's Lemma and Lebesgue's Convergence Theorem [10].MML identifier: MESFUN10, version: 7.9.01 4.101.1015
Fermat’s Little Theorem via Divisibility of Newton’s Binomial
Solving equations in integers is an important part of the number theory [29]. In many cases it can be conducted by the factorization of equation’s elements, such as the Newton’s binomial. The article introduces several simple formulas, which may facilitate this process. Some of them are taken from relevant books [28], [14]. In the second section of the article, Fermat’s Little Theorem is proved in a classical way, on the basis of divisibility of Newton’s binomial. Although slightly redundant in...
Finite Product of Semiring of Sets
We formalize that the image of a semiring of sets [17] by an injective function is a semiring of sets.We offer a non-trivial example of a semiring of sets in a topological space [21]. Finally, we show that the finite product of a semiring of sets is also a semiring of sets [21] and that the finite product of a classical semiring of sets [8] is a classical semiring of sets. In this case, we use here the notation from the book of Aliprantis and Border [1].
First Order Languages: Further Syntax and Semantics
Third of a series of articles laying down the bases for classical first order model theory. Interpretation of a language in a universe set. Evaluation of a term in a universe. Truth evaluation of an atomic formula. Reassigning the value of a symbol in a given interpretation. Syntax and semantics of a non atomic formula are then defined concurrently (this point is explained in [16], 4.2.1). As a consequence, the evaluation of any w.f.f. string and the relation of logical implication are introduced....
Formalization of Generalized Almost Distributive Lattices
Almost Distributive Lattices (ADL) are structures defined by Swamy and Rao [14] as a common abstraction of some generalizations of the Boolean algebra. In our paper, we deal with a certain further generalization of ADLs, namely the Generalized Almost Distributive Lattices (GADL). Our main aim was to give the formal counterpart of this structure and we succeeded formalizing all items from the Section 3 of Rao et al.’s paper [13]. Essentially among GADLs we can find structures which are neither V-commutative...
Formalization of the Advanced Encryption Standard. Part I
In this article, we formalize the Advanced Encryption Standard (AES). AES, which is the most widely used symmetric cryptosystem in the world, is a block cipher that was selected by the National Institute of Standards and Technology (NIST) as an official Federal Information Processing Standard for the United States in 2001 [12]. AES is the successor to DES [13], which was formerly the most widely used symmetric cryptosystem in the world. We formalize the AES algorithm according to [12]. We then verify...
Formulation of Cell Petri Nets
Based on the Petri net definitions and theorems already formalized in the Mizar article [13], in this article we were able to formalize the definition of cell Petri nets. It is based on [12]. Colored Petri net has already been defined in [11]. In addition, the conditions of the firing rule and the colored set to this definition, that defines the cell Petri nets are further extended to CPNT.i further. The synthesis of two Petri nets was introduced in [11] and in this work the definition is extended...
Free Interpretation, Quotient Interpretation and Substitution of a Letter with a Term for First Order Languages
Fourth of a series of articles laying down the bases for classical first order model theory. This paper supplies a toolkit of constructions to work with languages and interpretations, and results relating them. The free interpretation of a language, having as a universe the set of terms of the language itself, is defined.The quotient of an interpreteation with respect to an equivalence relation is built, and shown to remain an interpretation when the relation respects it. Both the concepts of quotient...
From Foundations to Science: Justifying and Unwinding Proofs