Displaying similar documents to “Basic Properties and Concept of Selected Subsequence of Zero Based Finite Sequences”

Model Checking. Part II

Kazuhisa Ishida (2008)

Formalized Mathematics

Similarity:

This article provides the definition of linear temporal logic (LTL) and its properties relevant to model checking based on [9]. Mizar formalization of LTL language and satisfiability is based on [2, 3].

Double Sequences and Limits

Noboru Endou, Hiroyuki Okazaki, Yasunari Shidama (2013)

Formalized Mathematics

Similarity:

Double sequences are important extension of the ordinary notion of a sequence. In this article we formalized three types of limits of double sequences and the theory of these limits.

The Sum and Product of Finite Sequences of Complex Numbers

Keiichi Miyajima, Takahiro Kato (2010)

Formalized Mathematics

Similarity:

This article extends the [10]. We define the sum and the product of the sequence of complex numbers, and formalize these theorems. Our method refers to the [11].

Stability of n -Bit Generalized Full Adder Circuits (GFAs). Part II

Katsumi Wasaki (2008)

Formalized Mathematics

Similarity:

We continue to formalize the concept of the Generalized Full Addition and Subtraction circuits (GFAs), define the structures of calculation units for the Redundant Signed Digit (RSD) operations, then prove its stability of the calculations. Generally, one-bit binary full adder assumes positive weights to all of its three binary inputs and two outputs. We define the circuit structure of two-types n-bit GFAs using the recursive construction to use the RSD arithmetic logical units that...

Formalization of Integral Linear Space

Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama (2011)

Formalized Mathematics

Similarity:

In this article, we formalize integral linear spaces, that is a linear space with integer coefficients. Integral linear spaces are necessary for lattice problems, LLL (Lenstra-Lenstra-Lovász) base reduction algorithm that outputs short lattice base and cryptographic systems with lattice [8].

Arithmetical transfinite induction and hierarchies of functions

Z. Ratajczyk (1992)

Fundamenta Mathematicae

Similarity:

We generalize to the case of arithmetical transfinite induction the following three theorems for PA: the Wainer Theorem, the Paris-Harrington Theorem, and a version of the Solovay-Ketonen Theorem. We give uniform proofs using combinatorial constructions.

Bertrand’s Ballot Theorem

Karol Pąk (2014)

Formalized Mathematics

Similarity:

In this article we formalize the Bertrand’s Ballot Theorem based on [17]. Suppose that in an election we have two candidates: A that receives n votes and B that receives k votes, and additionally n ≥ k. Then this theorem states that the probability of the situation where A maintains more votes than B throughout the counting of the ballots is equal to (n − k)/(n + k). This theorem is item #30 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/. ...

Riemann Integral of Functions from ℝ into Real Banach Space

Keiko Narita, Noboru Endou, Yasunari Shidama (2013)

Formalized Mathematics

Similarity:

In this article we deal with the Riemann integral of functions from R into a real Banach space. The last theorem establishes the integrability of continuous functions on the closed interval of reals. To prove the integrability we defined uniform continuity for functions from R into a real normed space, and proved related theorems. We also stated some properties of finite sequences of elements of a real normed space and finite sequences of real numbers. In addition we proved some theorems...

Semantics of MML Query

Grzegorz Bancerek (2012)

Formalized Mathematics

Similarity:

In the paper the semantics of MML Query queries is given. The formalization is done according to [4]

On a problem of Steve Kalikow

Saharon Shelah (2000)

Fundamenta Mathematicae

Similarity:

The Kalikow problem for a pair (λ,κ) of cardinal numbers,λ > κ (in particular κ = 2) is whether we can map the family of ω-sequences from λ to the family of ω-sequences from κ in a very continuous manner. Namely, we demand that for η,ν ∈ ω we have: η, ν are almost equal if and only if their images are. We show consistency of the negative answer, e.g., for ω but we prove it for smaller cardinals. We indicate a close connection with the free subset property and its variants. ...