FORMALIZED MATHEMATICS Volume 10, Number 1, 2002 University of Białystok

Fan Homeomorphisms in the Plane

Yatsuka Nakamura Shinshu University Nagano

Summary. We will introduce four homeomorphisms (Fan morphisms) which give spoke-like distortion to the plane. They do not change the norms of vectors and preserve halfplanes invariant. These morphisms are used to regulate placement of points on the circle.

MML Identifier: JGRAPH 4.

The articles [14], [18], [5], [7], [1], [2], [11], [12], [10], [3], [13], [4], [9], [19], [16], [17], [15], [8], and [6] provide the notation and terminology for this paper.

1. Preliminaries

In this paper x, a denote real numbers and p, q denote points of E_{T}^{2}. The following propositions are true:

(1) If |x| < a, then − a < x and x < a.

(2) If a 0 and (x − a) · (x + a) < 0, then − a < x and x < a.

(3) For every real number s_{1} such that − 1 < s_{1} and s_{1} < 1 holds 1 + s_{1} > 0 and 1 − s_{1} > 0.

(4) For every real number a such that a^{2} 1 holds − 1 a and a 1.

(5) For every real number a such that a^{2} < 1 holds − 1 < a and a < 1.

(6) Let X be a non empty topological structure, g be a map from X into ℝ^{1}, B be a subset of X, and a be a real number. If g is continuous and B = {p; p ranges over points of X: π_{p}g > a}, then B is open.

(7) Let X be a non empty topological structure, g be a map from X into ℝ^{1}, B be a subset of X, and a be a real number. If g is continuous and B = {p; p ranges over points of X: π_{p}g < a}, then B is open.

(8) Let f be a map from E_{T}^{2} into E_{T}^{2}. Suppose that

(i) f is continuous and one-to-one, (ii) rngf = Ω_{E_{T}^{2}}, and (iii) for every point p_{2} of E_{T}^{2} there exists a non empty compact subset K

of E_{T}^{2} such that K = f^{∘}K and there exists a subset V_{2} of E_{T}^{2} such that p_{2} ∈ V_{2} and V_{2} is open and V_{2} ⊆ K and f(p_{2}) ∈ V_{2}. Then f is a homeomorphism.

(9) Let X be a non empty topological space, f_{1}, f_{2} be maps from X into ℝ^{1}, and a, b be real numbers. Suppose f_{1} is continuous and f_{2} is continuous and b ≠ 0 and for every point q of X holds f_{2}(q) ≠ 0. Then there exists a map g from X into ℝ^{1} such that

(i) for every point p of X and for all real numbers r_{1}, r_{2} such that f_{1}(p) = r_{1}

and f_{2}(p) = r_{2} holds g(p) = ^{\frac{\frac{r_{1}}{r_{2}} −a}{b}} , and (ii) g is continuous.

(10) Let X be a non empty topological space, f_{1}, f_{2} be maps from X into ℝ^{1}, and a, b be real numbers. Suppose f_{1} is continuous and f_{2} is continuous and b ≠ 0 and for every point q of X holds f_{2}(q) ≠ 0. Then there exists a map g from X into ℝ^{1} such that

(i) for every point p of X and for all real numbers r_{1}, r_{2} such that f_{1}(p) = r_{1}

and f_{2}(p) = r_{2} holds g(p) = r_{2} · ^{\frac{\frac{r_{1}}{r_{2}} −a}{b}} , and (ii) g is continuous.

(11) Let X be a non empty topological space and f_{1} be a map from X into ℝ^{1}. Suppose f_{1} is continuous. Then there exists a map g from X into ℝ^{1} such that for every point p of X and for every real number r_{1} such that f_{1}(p) = r_{1} holds g(p) = r_{1}^{2} and g is continuous.

(12) Let X be a non empty topological space and f_{1} be a map from X into ℝ^{1}. Suppose f_{1} is continuous. Then there exists a map g from X into ℝ^{1} such that for every point p of X and for every real number r_{1} such that f_{1}(p) = r_{1} holds g(p) = |r_{1}| and g is continuous.

(13) Let X be a non empty topological space and f_{1} be a map from X into ℝ^{1}. Suppose f_{1} is continuous. Then there exists a map g from X into ℝ^{1} such that for every point p of X and for every real number r_{1} such that f_{1}(p) = r_{1} holds g(p) = − r_{1} and g is continuous.

(14) Let X be a non empty topological space, f_{1}, f_{2} be maps from X into ℝ^{1}, and a, b be real numbers. Suppose f_{1} is continuous and f_{2} is continuous and b ≠ 0 and for every point q of X holds f_{2}(q) ≠ 0. Then there exists a map g from X into ℝ^{1} such that

(i) for every point p of X and for all real numbers r_{1}, r_{2} such that f_{1}(p) = r_{1}

and f_{2}(p) = r_{2} holds g(p) = r_{2} · − \sqrt{|1 − (^{\frac{\frac{r_{1}}{r_{2}} −a}{b}} )^{2}|} , and (ii) g is continuous.

(15) Let X be a non empty topological space, f_{1}, f_{2} be maps from X into ℝ^{1}, and a, b be real numbers. Suppose f_{1} is continuous and f_{2} is continuous and b ≠ 0 and for every point q of X holds f_{2}(q) ≠ 0. Then there exists a map g from X into ℝ^{1} such that

(i) for every point p of X and for all real numbers r_{1}, r_{2} such that f_{1}(p) = r_{1}

and f_{2}(p) = r_{2} holds g(p) = r_{2} · \sqrt{|1 − (^{\frac{\frac{r_{1}}{r_{2}} −a}{b}} )^{2}|} , and (ii) g is continuous. Let n be a natural number. The functor n NormF yields a function from the

carrier of E_{T}^{n} into the carrier of ℝ^{1} and is defined by: (Def. 1) For every point q of E_{T}^{n} holds n NormF(q) = |q|.

Next we state several propositions:

(16) For every natural number n holds dom(n NormF) = the carrier of E_{T}^{n} and dom(n NormF) = R^{n}.

(18)^{1} For every natural number n and for all points p, q of E_{T}^{n} holds ||p|−|q||

|p − q|.

(19) For every natural number n and for every map f from E_{T}^{n} into ℝ^{1} such that f = n NormF holds f is continuous.

(20) Let n be a natural number, K_{0} be a subset of E_{T}^{n}, and f be a map from (E_{T}^{n})↾K_{0} into ℝ^{1}. If for every point p of (E_{T}^{n})↾K_{0} holds f(p) = n NormF(p), then f is continuous.

(21) Let n be a natural number, p be a point of E^{n}, r be a real number, and B be a subset of E_{T}^{n}. If B = \overline{Ball}(p, r), then B is Bounded and closed.

(22) For every point p of E^{2} and for every real number r and for every subset B of E_{T}^{2} such that B = \overline{Ball}(p, r) holds B is compact.

2. Fan Morphism for West

Let s be a real number and let q be a point of E_{T}^{2}. The functor FanW(s, q) yields a point of E_{T}^{2} and is defined as follows:

(Def. 2) FanW(s, q) = \{ \begin{matrix}|q| · [− \sqrt{1 − (^{\frac{\frac{q_{2}}{|q|} −s}{1−s}} )^{2}} , ^{\frac{\frac{q_{2}}{|q|} −s}{1−s}} ], if \frac{q_{2}}{|q|} s and q_{1} < 0, \\ |q| · [− \sqrt{1 − (^{\frac{\frac{q_{2}}{|q|} −s}{1+s}} )^{2}} , ^{\frac{\frac{q_{2}}{|q|} −s}{1+s}} ], if \frac{q_{2}}{|q|} < s and q_{1} < 0, \\ q, otherwise. \end{matrix}

Let s be a real number. The functor s -FanMorphW yields a function from the carrier of E_{T}^{2} into the carrier of E_{T}^{2} and is defined by:

1The proposition (17) has been removed.

(Def. 3) For every point q of E_{T}^{2} holds s -FanMorphW(q) = FanW(s, q).

Next we state a number of propositions:

(23) Let s_{1} be a real number. Then

(i) if \frac{q_{2}}{|q|} s_{1} and q_{1} < 0, then s_{1} -FanMorphW(q) = [|q|·− \sqrt{1 − (^{\frac{\frac{q_{2}}{|q|} −s_{1}}{1−s_{1}}} )^{2}} ,

|q| · ^{\frac{\frac{q_{2}}{|q|} −s_{1}}{1−s_{1}}} ], and (ii) if q_{1} 0, then s_{1} -FanMorphW(q) = q.

(24) For every real number s_{1} such that \frac{q_{2}}{|q|} s_{1} and q_{1} < 0 holds

s_{1} -FanMorphW(q) = [|q| · − \sqrt{1 − (^{\frac{\frac{q_{2}}{|q|} −s_{1}}{1+s_{1}}} )^{2}} , |q| · ^{\frac{\frac{q_{2}}{|q|} −s_{1}}{1+s_{1}}} ].

(25) Let s_{1} be a real number such that − 1 < s_{1} and s_{1} < 1. Then (i) if \frac{q_{2}}{|q|} s_{1} and q_{1} 0 and q ≠ 0_{E_{T}^{2}}, then s_{1} -FanMorphW(q) = [|q| ·

− \sqrt{1 − (^{\frac{\frac{q_{2}}{|q|} −s_{1}}{1−s_{1}}} )^{2}} , |q| · ^{\frac{\frac{q_{2}}{|q|} −s_{1}}{1−s_{1}}} ], and (ii) if \frac{q_{2}}{|q|} s_{1} and q_{1} 0 and q ≠ 0_{E_{T}^{2}}, then s_{1} -FanMorphW(q) = [|q| ·

− \sqrt{1 − (^{\frac{\frac{q_{2}}{|q|} −s_{1}}{1+s_{1}}} )^{2}} , |q| · ^{\frac{\frac{q_{2}}{|q|} −s_{1}}{1+s_{1}}} ].

(26) Let s_{1} be a real number, K_{1} be a non empty subset of E_{T}^{2}, and f be a

map from (E_{T}^{2})↾K_{1} into ℝ^{1}. Suppose that

(i) − 1 < s_{1}, (ii) s_{1} < 1, (iii) for every point p of E_{T}^{2} such that p ∈ the carrier of (E_{T}^{2})↾K_{1} holds

f(p) = |p| · ^{\frac{\frac{p_{2}}{|p|} −s_{1}}{1−s_{1}}} , and (iv) for every point q of E_{T}^{2} such that q ∈ the carrier of (E_{T}^{2})↾K_{1} holds q_{1} 0

and q ≠ 0_{E_{T}^{2}}. Then f is continuous.

(27) Let s_{1} be a real number, K_{1} be a non empty subset of E_{T}^{2}, and f be a

map from (E_{T}^{2})↾K_{1} into ℝ^{1}. Suppose that

(i) − 1 < s_{1}, (ii) s_{1} < 1, (iii) for every point p of E_{T}^{2} such that p ∈ the carrier of (E_{T}^{2})↾K_{1} holds

f(p) = |p| · ^{\frac{\frac{p_{2}}{|p|} −s_{1}}{1+s_{1}}} , and (iv) for every point q of E_{T}^{2} such that q ∈ the carrier of (E_{T}^{2})↾K_{1} holds q_{1} 0

and q ≠ 0_{E_{T}^{2}}. Then f is continuous.

(28) Let s_{1} be a real number, K_{1} be a non empty subset of E_{T}^{2}, and f be a

map from (E_{T}^{2})↾K_{1} into ℝ^{1}. Suppose that

(i) − 1 < s_{1}, (ii) s_{1} < 1, (iii) for every point p of E_{T}^{2} such that p ∈ the carrier of (E_{T}^{2})↾K_{1} holds

f(p) = |p| · − \sqrt{1 − (^{\frac{\frac{p_{2}}{|p|} −s_{1}}{1−s_{1}}} )^{2}} , and

(iv) for every point q of E_{T}^{2} such that q ∈ the carrier of (E_{T}^{2})↾K_{1} holds q_{1} 0 and \frac{q_{2}}{|q|} s_{1} and q ≠ 0_{E_{T}^{2}}. Then f is continuous.

(29) Let s_{1} be a real number, K_{1} be a non empty subset of E_{T}^{2}, and f be a

map from (E_{T}^{2})↾K_{1} into ℝ^{1}. Suppose that

(i) − 1 < s_{1}, (ii) s_{1} < 1, (iii) for every point p of E_{T}^{2} such that p ∈ the carrier of (E_{T}^{2})↾K_{1} holds

f(p) = |p| · − \sqrt{1 − (^{\frac{\frac{p_{2}}{|p|} −s_{1}}{1+s_{1}}} )^{2}} , and

(iv) for every point q of E_{T}^{2} such that q ∈ the carrier of (E_{T}^{2})↾K_{1} holds q_{1} 0 and \frac{q_{2}}{|q|} s_{1} and q ≠ 0_{E_{T}^{2}}. Then f is continuous.

(30) Let s_{1} be a real number, K_{0}, B_{0} be subsets of E_{T}^{2}, and f be a map from (E_{T}^{2})↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < s_{1} and s_{1} < 1 and f = s_{1} -FanMorphW↾K_{0} and B_{0} = {q; q ranges over points of E_{T}^{2}: q_{1} 0 ∧ q ≠ 0_{E_{T}^{2}}\} and K_{0} = \{p : \frac{p_{2}}{|p|} s_{1} ∧ p_{1} 0 ∧ p ≠ 0_{E_{T}^{2}}\}. Then f is continuous.

(31) Let s_{1} be a real number, K_{0}, B_{0} be subsets of E_{T}^{2}, and f be a map from (E_{T}^{2})↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < s_{1} and s_{1} < 1 and f = s_{1} -FanMorphW↾K_{0} and B_{0} = {q; q ranges over points of E_{T}^{2}: q_{1} 0 ∧ q ≠ 0_{E_{T}^{2}}\} and K_{0} = \{p : \frac{p_{2}}{|p|} s_{1} ∧ p_{1} 0 ∧ p ≠ 0_{E_{T}^{2}}\}. Then f is continuous.

(32) For every real number s_{1} and for every subset K_{3} of E_{T}^{2} such that K_{3} = {p : p_{2} s_{1} · |p| ∧ p_{1} 0} holds K_{3} is closed.

(33) For every real number s_{1} and for every subset K_{3} of E_{T}^{2} such that K_{3} = {p : p_{2} s_{1} · |p| ∧ p_{1} 0} holds K_{3} is closed.

(34) Let s_{1} be a real number, K_{0}, B_{0} be subsets of E_{T}^{2}, and f be a map from (E_{T}^{2})↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < s_{1} and s_{1} < 1 and f = s_{1} -FanMorphW↾K_{0} and B_{0} = (the carrier of E_{T}^{2}) \ {0_{E_{T}^{2}}} and K_{0} = {p : p_{1} 0 ∧ p ≠ 0_{E_{T}^{2}}}. Then f is continuous.

(35) Let s_{1} be a real number, K_{0}, B_{0} be subsets of E_{T}^{2}, and f be a map from (E_{T}^{2})↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < s_{1} and s_{1} < 1 and f = s_{1} -FanMorphW↾K_{0} and B_{0} = (the carrier of E_{T}^{2}) \ {0_{E_{T}^{2}}} and K_{0} = {p : p_{1} 0 ∧ p ≠ 0_{E_{T}^{2}}}. Then f is continuous.

(36) Let B_{0} be a subset of E_{T}^{2} and K_{0} be a subset of (E_{T}^{2})↾B_{0}. Suppose B_{0} = (the carrier of E_{T}^{2}) \ {0_{E_{T}^{2}}} and K_{0} = {p : p_{1} 0 ∧ p ≠ 0_{E_{T}^{2}}}. Then K_{0} is

closed.

(37) Let s_{1} be a real number, B_{0} be a subset of E_{T}^{2}, K_{0} be a subset of (E_{T}^{2})↾B_{0}, and f be a map from (E_{T}^{2})↾B_{0}↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < s_{1} and s_{1} < 1 and f = s_{1} -FanMorphW↾K_{0} and B_{0} = (the carrier of E_{T}^{2}) \ {0_{E_{T}^{2}}} and K_{0} = {p : p_{1} 0 ∧ p ≠ 0_{E_{T}^{2}}}. Then f is continuous.

(38) Let B_{0} be a subset of E_{T}^{2} and K_{0} be a subset of (E_{T}^{2})↾B_{0}. Suppose B_{0} = (the carrier of E_{T}^{2}) \ {0_{E_{T}^{2}}} and K_{0} = {p : p_{1} 0 ∧ p ≠ 0_{E_{T}^{2}}}. Then K_{0} is closed.

(39) Let s_{1} be a real number, B_{0} be a subset of E_{T}^{2}, K_{0} be a subset of (E_{T}^{2})↾B_{0}, and f be a map from (E_{T}^{2})↾B_{0}↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < s_{1} and s_{1} < 1 and f = s_{1} -FanMorphW↾K_{0} and B_{0} = (the carrier of E_{T}^{2}) \ {0_{E_{T}^{2}}} and K_{0} = {p : p_{1} 0 ∧ p ≠ 0_{E_{T}^{2}}}. Then f is continuous.

(40) For every real number s_{1} and for every point p of E_{T}^{2} holds |s_{1} -FanMorphW(p)| = |p|.

(41) For every real number s_{1} and for all sets x, K_{0} such that − 1 < s_{1} and s_{1} < 1 and x ∈ K_{0} and K_{0} = {p : p_{1} 0 ∧ p ≠ 0_{E_{T}^{2}}} holds s_{1} -FanMorphW(x) ∈ K_{0}.

(42) For every real number s_{1} and for all sets x, K_{0} such that − 1 < s_{1} and s_{1} < 1 and x ∈ K_{0} and K_{0} = {p : p_{1} 0 ∧ p ≠ 0_{E_{T}^{2}}} holds s_{1} -FanMorphW(x) ∈ K_{0}.

(43) Let s_{1} be a real number and D be a non empty subset of E_{T}^{2}. Suppose − 1 < s_{1} and s_{1} < 1 and D^{c} = {0_{E_{T}^{2}}}. Then there exists a map h from (E_{T}^{2})↾D into (E_{T}^{2})↾D such that h = s_{1} -FanMorphW↾D and h is continuous.

(44) Let s_{1} be a real number. Suppose − 1 < s_{1} and s_{1} < 1. Then there exists a map h from E_{T}^{2} into E_{T}^{2} such that h = s_{1} -FanMorphW and h is continuous.

(45) For every real number s_{1} such that − 1 < s_{1} and s_{1} < 1 holds s_{1} -FanMorphW is one-to-one.

(46) For every real number s_{1} such that − 1 < s_{1} and s_{1} < 1 holds s_{1} -FanMorphW is a map from E_{T}^{2} into E_{T}^{2} and rng(s_{1} -FanMorphW) = the carrier of E_{T}^{2}.

(47) Let s_{1} be a real number and p_{2} be a point of E_{T}^{2}. Suppose − 1 < s_{1} and s_{1} < 1. Then there exists a non empty compact subset K of E_{T}^{2} such that K = s_{1} -FanMorphW^{∘} K and there exists a subset V_{2} of E_{T}^{2} such that p_{2} ∈ V_{2} and V_{2} is open and V_{2} ⊆ K and s_{1} -FanMorphW(p_{2}) ∈ V_{2}.

(48) Let s_{1} be a real number. Suppose − 1 < s_{1} and s_{1} < 1. Then there exists a map f from E_{T}^{2} into E_{T}^{2} such that f = s_{1} -FanMorphW and f is a homeomorphism.

(49) Let s_{1} be a real number and q be a point of E_{T}^{2}. Suppose − 1 < s_{1} and s_{1} < 1 and q_{1} < 0 and \frac{q_{2}}{|q|} s_{1}. Let p be a point of E_{T}^{2}. If p = s_{1} -FanMorphW(q), then p_{1} < 0 and p_{2} 0.

(50) Let s_{1} be a real number and q be a point of E_{T}^{2}. Suppose − 1 < s_{1} and s_{1} < 1 and q_{1} < 0 and \frac{q_{2}}{|q|} < s_{1}. Let p be a point of E_{T}^{2}. If p = s_{1} -FanMorphW(q), then p_{1} < 0 and p_{2} < 0.

(51) Let s_{1} be a real number and q_{1}, q_{2} be points of E_{T}^{2}. Suppose − 1 < s_{1} and s_{1} < 1 and (q_{1})_{1} < 0 and \frac{(q_{1})_{2}}{|q_{1}|} s_{1} and (q_{2})_{1} < 0 and \frac{(q_{2})_{2}}{|q_{2}|} s_{1} and

\frac{(q_{1})_{2}}{|q_{1}|} < \frac{(q_{2})_{2}}{|q_{2}|} . Let p_{1}, p_{2} be points of E_{T}^{2}. If p_{1} = s_{1} -FanMorphW(q_{1}) and

p_{2} = s_{1} -FanMorphW(q_{2}), then \frac{(p_{1})_{2}}{|p_{1}|} < \frac{(p_{2})_{2}}{|p_{2}|} .

(52) Let s_{1} be a real number and q_{1}, q_{2} be points of E_{T}^{2}. Suppose − 1 < s_{1} and s_{1} < 1 and (q_{1})_{1} < 0 and \frac{(q_{1})_{2}}{|q_{1}|} < s_{1} and (q_{2})_{1} < 0 and \frac{(q_{2})_{2}}{|q_{2}|} < s_{1} and

\frac{(q_{1})_{2}}{|q_{1}|} < \frac{(q_{2})_{2}}{|q_{2}|} . Let p_{1}, p_{2} be points of E_{T}^{2}. If p_{1} = s_{1} -FanMorphW(q_{1}) and

p_{2} = s_{1} -FanMorphW(q_{2}), then \frac{(p_{1})_{2}}{|p_{1}|} < \frac{(p_{2})_{2}}{|p_{2}|} .

(53) Let s_{1} be a real number and q_{1}, q_{2} be points of E_{T}^{2}. Suppose − 1 < s_{1} and s_{1} < 1 and (q_{1})_{1} < 0 and (q_{2})_{1} < 0 and \frac{(q_{1})_{2}}{|q_{1}|} < \frac{(q_{2})_{2}}{|q_{2}|} . Let p_{1}, p_{2} be points of E_{T}^{2}. If p_{1} = s_{1} -FanMorphW(q_{1}) and p_{2} = s_{1} -FanMorphW(q_{2}), then \frac{(p_{1})_{2}}{|p_{1}|} < \frac{(p_{2})_{2}}{|p_{2}|} .

(54) Let s_{1} be a real number and q be a point of E_{T}^{2}. Suppose − 1 < s_{1} and s_{1} < 1 and q_{1} < 0 and \frac{q_{2}}{|q|} = s_{1}. Let p be a point of E_{T}^{2}. If p = s_{1} -FanMorphW(q), then p_{1} < 0 and p_{2} = 0.

(55) For every real number s_{1} holds 0_{E_{T}^{2}} = s_{1} -FanMorphW(0_{E_{T}^{2}}).

3. Fan Morphism for North

Let s be a real number and let q be a point of E_{T}^{2}. The functor FanN(s, q) yields a point of E_{T}^{2} and is defined by:

(Def. 4) FanN(s, q) = \{ \begin{matrix}|q| · [^{\frac{\frac{q_{1}}{|q|} −s}{1−s}} , \sqrt{1 − (^{\frac{\frac{q_{1}}{|q|} −s}{1−s}} )^{2}} ], if \frac{q_{1}}{|q|} s and q_{2} > 0, \\ |q| · [^{\frac{\frac{q_{1}}{|q|} −s}{1+s}} , \sqrt{1 − (^{\frac{\frac{q_{1}}{|q|} −s}{1+s}} )^{2}} ], if \frac{q_{1}}{|q|} < s and q_{2} > 0, \\ q, otherwise. \end{matrix}

Let c be a real number. The functor c -FanMorphN yielding a function from the carrier of E_{T}^{2} into the carrier of E_{T}^{2} is defined as follows:

(Def. 5) For every point q of E_{T}^{2} holds c -FanMorphN(q) = FanN(c, q).

One can prove the following propositions:

(56) Let c_{1} be a real number. Then (i) if \frac{q_{1}}{|q|} c_{1} and q_{2} > 0, then c_{1} -FanMorphN(q) = [|q| · ^{\frac{\frac{q_{1}}{|q|} −c_{1}}{1−c_{1}}} , |q| ·

\sqrt{1 − (^{\frac{\frac{q_{1}}{|q|} −c_{1}}{1−c_{1}}} )^{2}} ], and (ii) if q_{2} 0, then c_{1} -FanMorphN(q) = q.

(57) For every real number c_{1} such that \frac{q_{1}}{|q|} c_{1} and q_{2} > 0 holds

c_{1} -FanMorphN(q) = [|q| · ^{\frac{\frac{q_{1}}{|q|} −c_{1}}{1+c_{1}}} , |q| · \sqrt{1 − (^{\frac{\frac{q_{1}}{|q|} −c_{1}}{1+c_{1}}} )^{2}} ].

(58) Let c_{1} be a real number such that − 1 < c_{1} and c_{1} < 1. Then

(i) if \frac{q_{1}}{|q|} c_{1} and q_{2} 0 and q ≠ 0_{E_{T}^{2}}, then c_{1} -FanMorphN(q) = [|q|· ^{\frac{\frac{q_{1}}{|q|} −c_{1}}{1−c_{1}}} ,

|q| · \sqrt{1 − (^{\frac{\frac{q_{1}}{|q|} −c_{1}}{1−c_{1}}} )^{2}} ], and

(ii) if \frac{q_{1}}{|q|} c_{1} and q_{2} 0 and q ≠ 0_{E_{T}^{2}}, then c_{1} -FanMorphN(q) = [|q|· ^{\frac{\frac{q_{1}}{|q|} −c_{1}}{1+c_{1}}} ,

|q| · \sqrt{1 − (^{\frac{\frac{q_{1}}{|q|} −c_{1}}{1+c_{1}}} )^{2}} ].

(59) Let c_{1} be a real number, K_{1} be a non empty subset of E_{T}^{2}, and f be a

map from (E_{T}^{2})↾K_{1} into ℝ^{1}. Suppose that

(i) − 1 < c_{1}, (ii) c_{1} < 1, (iii) for every point p of E_{T}^{2} such that p ∈ the carrier of (E_{T}^{2})↾K_{1} holds

f(p) = |p| · ^{\frac{\frac{p_{1}}{|p|} −c_{1}}{1−c_{1}}} , and (iv) for every point q of E_{T}^{2} such that q ∈ the carrier of (E_{T}^{2})↾K_{1} holds q_{2} 0

and q ≠ 0_{E_{T}^{2}}. Then f is continuous.

(60) Let c_{1} be a real number, K_{1} be a non empty subset of E_{T}^{2}, and f be a

map from (E_{T}^{2})↾K_{1} into ℝ^{1}. Suppose that

(i) − 1 < c_{1}, (ii) c_{1} < 1, (iii) for every point p of E_{T}^{2} such that p ∈ the carrier of (E_{T}^{2})↾K_{1} holds

f(p) = |p| · ^{\frac{\frac{p_{1}}{|p|} −c_{1}}{1+c_{1}}} , and (iv) for every point q of E_{T}^{2} such that q ∈ the carrier of (E_{T}^{2})↾K_{1} holds q_{2} 0

and q ≠ 0_{E_{T}^{2}}. Then f is continuous.

(61) Let c_{1} be a real number, K_{1} be a non empty subset of E_{T}^{2}, and f be a

map from (E_{T}^{2})↾K_{1} into ℝ^{1}. Suppose that

(i) − 1 < c_{1}, (ii) c_{1} < 1, (iii) for every point p of E_{T}^{2} such that p ∈ the carrier of (E_{T}^{2})↾K_{1} holds

f(p) = |p| · \sqrt{1 − (^{\frac{\frac{p_{1}}{|p|} −c_{1}}{1−c_{1}}} )^{2}} , and (iv) for every point q of E_{T}^{2} such that q ∈ the carrier of (E_{T}^{2})↾K_{1} holds q_{2} 0

and \frac{q_{1}}{|q|} c_{1} and q ≠ 0_{E_{T}^{2}}. Then f is continuous.

(62) Let c_{1} be a real number, K_{1} be a non empty subset of E_{T}^{2}, and f be a

map from (E_{T}^{2})↾K_{1} into ℝ^{1}. Suppose that

(i) − 1 < c_{1}, (ii) c_{1} < 1, (iii) for every point p of E_{T}^{2} such that p ∈ the carrier of (E_{T}^{2})↾K_{1} holds

f(p) = |p| · \sqrt{1 − (^{\frac{\frac{p_{1}}{|p|} −c_{1}}{1+c_{1}}} )^{2}} , and

(iv) for every point q of E_{T}^{2} such that q ∈ the carrier of (E_{T}^{2})↾K_{1} holds q_{2} 0 and \frac{q_{1}}{|q|} c_{1} and q ≠ 0_{E_{T}^{2}}. Then f is continuous.

(63) Let c_{1} be a real number, K_{0}, B_{0} be subsets of E_{T}^{2}, and f be a map from (E_{T}^{2})↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < c_{1} and c_{1} < 1 and f = c_{1} -FanMorphN↾K_{0} and B_{0} = {q; q ranges over points of E_{T}^{2}: q_{2} 0 ∧ q ≠ 0_{E_{T}^{2}}\} and K_{0} = \{p : \frac{p_{1}}{|p|} c_{1} ∧ p_{2} 0 ∧ p ≠ 0_{E_{T}^{2}}\}. Then f is continuous.

(64) Let c_{1} be a real number, K_{0}, B_{0} be subsets of E_{T}^{2}, and f be a map from (E_{T}^{2})↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < c_{1} and c_{1} < 1 and f = c_{1} -FanMorphN↾K_{0} and B_{0} = {q; q ranges over points of E_{T}^{2}: q_{2} 0 ∧ q ≠ 0_{E_{T}^{2}}\} and K_{0} = \{p : \frac{p_{1}}{|p|} c_{1} ∧ p_{2} 0 ∧ p ≠ 0_{E_{T}^{2}}\}. Then f is continuous.

(65) For every real number c_{1} and for every subset K_{3} of E_{T}^{2} such that K_{3} = {p : p_{1} c_{1} · |p| ∧ p_{2} 0} holds K_{3} is closed.

(66) For every real number c_{1} and for every subset K_{3} of E_{T}^{2} such that K_{3} = {p : p_{1} c_{1} · |p| ∧ p_{2} 0} holds K_{3} is closed.

(67) Let c_{1} be a real number, K_{0}, B_{0} be subsets of E_{T}^{2}, and f be a map from (E_{T}^{2})↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < c_{1} and c_{1} < 1 and f = c_{1} -FanMorphN↾K_{0} and B_{0} = (the carrier of E_{T}^{2}) \ {0_{E_{T}^{2}}} and K_{0} = {p : p_{2} 0 ∧ p ≠ 0_{E_{T}^{2}}}. Then f is continuous.

(68) Let c_{1} be a real number, K_{0}, B_{0} be subsets of E_{T}^{2}, and f be a map from (E_{T}^{2})↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < c_{1} and c_{1} < 1 and f = c_{1} -FanMorphN↾K_{0} and B_{0} = (the carrier of E_{T}^{2}) \ {0_{E_{T}^{2}}} and K_{0} = {p : p_{2} 0 ∧ p ≠ 0_{E_{T}^{2}}}. Then f is continuous.

(69) Let B_{0} be a subset of E_{T}^{2} and K_{0} be a subset of (E_{T}^{2})↾B_{0}. Suppose B_{0} = (the carrier of E_{T}^{2}) \ {0_{E_{T}^{2}}} and K_{0} = {p : p_{2} 0 ∧ p ≠ 0_{E_{T}^{2}}}. Then K_{0} is closed.

(70) Let B_{0} be a subset of E_{T}^{2} and K_{0} be a subset of (E_{T}^{2})↾B_{0}. Suppose B_{0} = (the carrier of E_{T}^{2}) \ {0_{E_{T}^{2}}} and K_{0} = {p : p_{2} 0 ∧ p ≠ 0_{E_{T}^{2}}}. Then K_{0} is

closed.

(71) Let c_{1} be a real number, B_{0} be a subset of E_{T}^{2}, K_{0} be a subset of (E_{T}^{2})↾B_{0}, and f be a map from (E_{T}^{2})↾B_{0}↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < c_{1} and c_{1} < 1 and f = c_{1} -FanMorphN↾K_{0} and B_{0} = (the carrier of E_{T}^{2}) \ {0_{E_{T}^{2}}} and K_{0} = {p : p_{2} 0 ∧ p ≠ 0_{E_{T}^{2}}}. Then f is continuous.

(72) Let c_{1} be a real number, B_{0} be a subset of E_{T}^{2}, K_{0} be a subset of (E_{T}^{2})↾B_{0}, and f be a map from (E_{T}^{2})↾B_{0}↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < c_{1} and c_{1} < 1 and f = c_{1} -FanMorphN↾K_{0} and B_{0} = (the carrier of E_{T}^{2}) \ {0_{E_{T}^{2}}} and K_{0} = {p : p_{2} 0 ∧ p ≠ 0_{E_{T}^{2}}}. Then f is continuous.

(73) For every real number c_{1} and for every point p of E_{T}^{2} holds |c_{1} -FanMorphN(p)| = |p|.

(74) For every real number c_{1} and for all sets x, K_{0} such that − 1 < c_{1} and c_{1} < 1 and x ∈ K_{0} and K_{0} = {p : p_{2} 0 ∧ p ≠ 0_{E_{T}^{2}}} holds c_{1} -FanMorphN(x) ∈ K_{0}.

(75) For every real number c_{1} and for all sets x, K_{0} such that − 1 < c_{1} and c_{1} < 1 and x ∈ K_{0} and K_{0} = {p : p_{2} 0 ∧ p ≠ 0_{E_{T}^{2}}} holds c_{1} -FanMorphN(x) ∈ K_{0}.

(76) Let c_{1} be a real number and D be a non empty subset of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and D^{c} = {0_{E_{T}^{2}}}. Then there exists a map h from (E_{T}^{2})↾D into (E_{T}^{2})↾D such that h = c_{1} -FanMorphN↾D and h is continuous.

(77) Let c_{1} be a real number. Suppose − 1 < c_{1} and c_{1} < 1. Then there exists a map h from E_{T}^{2} into E_{T}^{2} such that h = c_{1} -FanMorphN and h is continuous.

(78) For every real number c_{1} such that − 1 < c_{1} and c_{1} < 1 holds c_{1} -FanMorphN is one-to-one.

(79) For every real number c_{1} such that − 1 < c_{1} and c_{1} < 1 holds c_{1} -FanMorphN is a map from E_{T}^{2} into E_{T}^{2} and rng(c_{1} -FanMorphN) = the carrier of E_{T}^{2}.

(80) Let c_{1} be a real number and p_{2} be a point of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1. Then there exists a non empty compact subset K of E_{T}^{2} such that K = c_{1} -FanMorphN^{∘} K and there exists a subset V_{2} of E_{T}^{2} such that p_{2} ∈ V_{2} and V_{2} is open and V_{2} ⊆ K and c_{1} -FanMorphN(p_{2}) ∈ V_{2}.

(81) Let c_{1} be a real number. Suppose − 1 < c_{1} and c_{1} < 1. Then there exists a map f from E_{T}^{2} into E_{T}^{2} such that f = c_{1} -FanMorphN and f is a homeomorphism.

(82) Let c_{1} be a real number and q be a point of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and q_{2} > 0 and \frac{q_{1}}{|q|} c_{1}. Let p be a point of E_{T}^{2}. If p = c_{1} -FanMorphN(q), then p_{2} > 0 and p_{1} 0.

(83) Let c_{1} be a real number and q be a point of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and q_{2} > 0 and \frac{q_{1}}{|q|} < c_{1}. Let p be a point of E_{T}^{2}. If p = c_{1} -FanMorphN(q), then p_{2} > 0 and p_{1} < 0.

(84) Let c_{1} be a real number and q_{1}, q_{2} be points of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and (q_{1})_{2} > 0 and \frac{(q_{1})_{1}}{|q_{1}|} c_{1} and (q_{2})_{2} > 0 and \frac{(q_{2})_{1}}{|q_{2}|} c_{1} and

\frac{(q_{1})_{1}}{|q_{1}|} < \frac{(q_{2})_{1}}{|q_{2}|} . Let p_{1}, p_{2} be points of E_{T}^{2}. If p_{1} = c_{1} -FanMorphN(q_{1}) and

p_{2} = c_{1} -FanMorphN(q_{2}), then \frac{(p_{1})_{1}}{|p_{1}|} < \frac{(p_{2})_{1}}{|p_{2}|} .

(85) Let c_{1} be a real number and q_{1}, q_{2} be points of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and (q_{1})_{2} > 0 and \frac{(q_{1})_{1}}{|q_{1}|} < c_{1} and (q_{2})_{2} > 0 and \frac{(q_{2})_{1}}{|q_{2}|} < c_{1} and

\frac{(q_{1})_{1}}{|q_{1}|} < \frac{(q_{2})_{1}}{|q_{2}|} . Let p_{1}, p_{2} be points of E_{T}^{2}. If p_{1} = c_{1} -FanMorphN(q_{1}) and

p_{2} = c_{1} -FanMorphN(q_{2}), then \frac{(p_{1})_{1}}{|p_{1}|} < \frac{(p_{2})_{1}}{|p_{2}|} .

(86) Let c_{1} be a real number and q_{1}, q_{2} be points of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and (q_{1})_{2} > 0 and (q_{2})_{2} > 0 and \frac{(q_{1})_{1}}{|q_{1}|} < \frac{(q_{2})_{1}}{|q_{2}|} . Let p_{1}, p_{2} be points of E_{T}^{2}. If p_{1} = c_{1} -FanMorphN(q_{1}) and p_{2} = c_{1} -FanMorphN(q_{2}), then \frac{(p_{1})_{1}}{|p_{1}|} < \frac{(p_{2})_{1}}{|p_{2}|} .

(87) Let c_{1} be a real number and q be a point of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and q_{2} > 0 and \frac{q_{1}}{|q|} = c_{1}. Let p be a point of E_{T}^{2}. If p = c_{1} -FanMorphN(q), then p_{2} > 0 and p_{1} = 0.

(88) For every real number c_{1} holds 0_{E_{T}^{2}} = c_{1} -FanMorphN(0_{E_{T}^{2}}).

4. Fan Morphism for East

Let s be a real number and let q be a point of E_{T}^{2}. The functor FanE(s, q) yields a point of E_{T}^{2} and is defined as follows:

(Def. 6) FanE(s, q) = \{ \begin{matrix}|q| · [\sqrt{1 − (^{\frac{\frac{q_{2}}{|q|} −s}{1−s}} )^{2}} , ^{\frac{\frac{q_{2}}{|q|} −s}{1−s}} ], if \frac{q_{2}}{|q|} s and q_{1} > 0, \\ |q| · [\sqrt{1 − (^{\frac{\frac{q_{2}}{|q|} −s}{1+s}} )^{2}} , ^{\frac{\frac{q_{2}}{|q|} −s}{1+s}} ], if \frac{q_{2}}{|q|} < s and q_{1} > 0, \\ q, otherwise. \end{matrix}

Let s be a real number. The functor s -FanMorphE yielding a function from the carrier of E_{T}^{2} into the carrier of E_{T}^{2} is defined as follows:

(Def. 7) For every point q of E_{T}^{2} holds s -FanMorphE(q) = FanE(s, q).

Next we state a number of propositions:

(89) Let s_{1} be a real number. Then

(i) if \frac{q_{2}}{|q|} s_{1} and q_{1} > 0, then s_{1} -FanMorphE(q) = [|q| · \sqrt{1 − (^{\frac{\frac{q_{2}}{|q|} −s_{1}}{1−s_{1}}} )^{2}} ,

|q| · ^{\frac{\frac{q_{2}}{|q|} −s_{1}}{1−s_{1}}} ], and (ii) if q_{1} 0, then s_{1} -FanMorphE(q) = q.

(90) For every real number s_{1} such that \frac{q_{2}}{|q|} s_{1} and q_{1} > 0 holds

s_{1} -FanMorphE(q) = [|q| · \sqrt{1 − (^{\frac{\frac{q_{2}}{|q|} −s_{1}}{1+s_{1}}} )^{2}} , |q| · ^{\frac{\frac{q_{2}}{|q|} −s_{1}}{1+s_{1}}} ].

(91) Let s_{1} be a real number such that − 1 < s_{1} and s_{1} < 1. Then (i) if \frac{q_{2}}{|q|} s_{1} and q_{1} 0 and q ≠ 0_{E_{T}^{2}}, then s_{1} -FanMorphE(q) = [|q| ·

\sqrt{1 − (^{\frac{\frac{q_{2}}{|q|} −s_{1}}{1−s_{1}}} )^{2}} , |q| · ^{\frac{\frac{q_{2}}{|q|} −s_{1}}{1−s_{1}}} ], and (ii) if \frac{q_{2}}{|q|} s_{1} and q_{1} 0 and q ≠ 0_{E_{T}^{2}}, then s_{1} -FanMorphE(q) = [|q| ·

\sqrt{1 − (^{\frac{\frac{q_{2}}{|q|} −s_{1}}{1+s_{1}}} )^{2}} , |q| · ^{\frac{\frac{q_{2}}{|q|} −s_{1}}{1+s_{1}}} ].

(92) Let s_{1} be a real number, K_{1} be a non empty subset of E_{T}^{2}, and f be a

map from (E_{T}^{2})↾K_{1} into ℝ^{1}. Suppose that

(i) − 1 < s_{1}, (ii) s_{1} < 1, (iii) for every point p of E_{T}^{2} such that p ∈ the carrier of (E_{T}^{2})↾K_{1} holds

f(p) = |p| · ^{\frac{\frac{p_{2}}{|p|} −s_{1}}{1−s_{1}}} , and (iv) for every point q of E_{T}^{2} such that q ∈ the carrier of (E_{T}^{2})↾K_{1} holds q_{1} 0

and q ≠ 0_{E_{T}^{2}}. Then f is continuous.

(93) Let s_{1} be a real number, K_{1} be a non empty subset of E_{T}^{2}, and f be a

map from (E_{T}^{2})↾K_{1} into ℝ^{1}. Suppose that

(i) − 1 < s_{1}, (ii) s_{1} < 1, (iii) for every point p of E_{T}^{2} such that p ∈ the carrier of (E_{T}^{2})↾K_{1} holds

f(p) = |p| · ^{\frac{\frac{p_{2}}{|p|} −s_{1}}{1+s_{1}}} , and (iv) for every point q of E_{T}^{2} such that q ∈ the carrier of (E_{T}^{2})↾K_{1} holds q_{1} 0

and q ≠ 0_{E_{T}^{2}}. Then f is continuous.

(94) Let s_{1} be a real number, K_{1} be a non empty subset of E_{T}^{2}, and f be a

map from (E_{T}^{2})↾K_{1} into ℝ^{1}. Suppose that

(i) − 1 < s_{1}, (ii) s_{1} < 1, (iii) for every point p of E_{T}^{2} such that p ∈ the carrier of (E_{T}^{2})↾K_{1} holds

f(p) = |p| · \sqrt{1 − (^{\frac{\frac{p_{2}}{|p|} −s_{1}}{1−s_{1}}} )^{2}} , and (iv) for every point q of E_{T}^{2} such that q ∈ the carrier of (E_{T}^{2})↾K_{1} holds q_{1} 0

and \frac{q_{2}}{|q|} s_{1} and q ≠ 0_{E_{T}^{2}}. Then f is continuous.

(95) Let s_{1} be a real number, K_{1} be a non empty subset of E_{T}^{2}, and f be a map from (E_{T}^{2})↾K_{1} into ℝ^{1}. Suppose that (i) − 1 < s_{1}, (ii) s_{1} < 1, (iii) for every point p of E_{T}^{2} such that p ∈ the carrier of (E_{T}^{2})↾K_{1} holds

f(p) = |p| · \sqrt{1 − (^{\frac{\frac{p_{2}}{|p|} −s_{1}}{1+s_{1}}} )^{2}} , and

(iv) for every point q of E_{T}^{2} such that q ∈ the carrier of (E_{T}^{2})↾K_{1} holds q_{1} 0 and \frac{q_{2}}{|q|} s_{1} and q ≠ 0_{E_{T}^{2}}. Then f is continuous.

(96) Let s_{1} be a real number, K_{0}, B_{0} be subsets of E_{T}^{2}, and f be a map from (E_{T}^{2})↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < s_{1} and s_{1} < 1 and f = s_{1} -FanMorphE↾K_{0} and B_{0} = {q; q ranges over points of E_{T}^{2}: q_{1} 0 ∧ q ≠ 0_{E_{T}^{2}}\} and K_{0} = \{p : \frac{p_{2}}{|p|} s_{1} ∧ p_{1} 0 ∧ p ≠ 0_{E_{T}^{2}}\}. Then f is continuous.

(97) Let s_{1} be a real number, K_{0}, B_{0} be subsets of E_{T}^{2}, and f be a map from (E_{T}^{2})↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < s_{1} and s_{1} < 1 and f = s_{1} -FanMorphE↾K_{0} and B_{0} = {q; q ranges over points of E_{T}^{2}: q_{1} 0 ∧ q ≠ 0_{E_{T}^{2}}\} and K_{0} = \{p : \frac{p_{2}}{|p|} s_{1} ∧ p_{1} 0 ∧ p ≠ 0_{E_{T}^{2}}\}. Then f is continuous.

(98) For every real number s_{1} and for every subset K_{3} of E_{T}^{2} such that K_{3} = {p : p_{2} s_{1} · |p| ∧ p_{1} 0} holds K_{3} is closed.

(99) For every real number s_{1} and for every subset K_{3} of E_{T}^{2} such that K_{3} = {p : p_{2} s_{1} · |p| ∧ p_{1} 0} holds K_{3} is closed.

(100) Let s_{1} be a real number, K_{0}, B_{0} be subsets of E_{T}^{2}, and f be a map from (E_{T}^{2})↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < s_{1} and s_{1} < 1 and f = s_{1} -FanMorphE↾K_{0} and B_{0} = (the carrier of E_{T}^{2}) \ {0_{E_{T}^{2}}} and K_{0} = {p : p_{1} 0 ∧ p ≠ 0_{E_{T}^{2}}}. Then f is continuous.

(101) Let s_{1} be a real number, K_{0}, B_{0} be subsets of E_{T}^{2}, and f be a map from (E_{T}^{2})↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < s_{1} and s_{1} < 1 and f = s_{1} -FanMorphE↾K_{0} and B_{0} = (the carrier of E_{T}^{2}) \ {0_{E_{T}^{2}}} and K_{0} = {p : p_{1} 0 ∧ p ≠ 0_{E_{T}^{2}}}. Then f is continuous.

(102) Let s_{1} be a real number, B_{0} be a subset of E_{T}^{2}, K_{0} be a subset of (E_{T}^{2})↾B_{0}, and f be a map from (E_{T}^{2})↾B_{0}↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < s_{1} and s_{1} < 1 and f = s_{1} -FanMorphE↾K_{0} and B_{0} = (the carrier of E_{T}^{2}) \ {0_{E_{T}^{2}}} and K_{0} = {p : p_{1} 0 ∧ p ≠ 0_{E_{T}^{2}}}. Then f is continuous.

(103) Let s_{1} be a real number, B_{0} be a subset of E_{T}^{2}, K_{0} be a subset of (E_{T}^{2})↾B_{0}, and f be a map from (E_{T}^{2})↾B_{0}↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < s_{1} and s_{1} < 1 and f = s_{1} -FanMorphE↾K_{0} and B_{0} = (the carrier of E_{T}^{2}) \ {0_{E_{T}^{2}}} and K_{0} = {p : p_{1} 0 ∧ p ≠ 0_{E_{T}^{2}}}. Then f is continuous.

(104) For every real number s_{1} and for every point p of E_{T}^{2} holds |s_{1} -FanMorphE(p)| = |p|.

(105) For every real number s_{1} and for all sets x, K_{0} such that − 1 < s_{1} and s_{1} < 1 and x ∈ K_{0} and K_{0} = {p : p_{1} 0 ∧ p ≠ 0_{E_{T}^{2}}} holds s_{1} -FanMorphE(x) ∈ K_{0}.

(106) For every real number s_{1} and for all sets x, K_{0} such that − 1 < s_{1} and s_{1} < 1 and x ∈ K_{0} and K_{0} = {p : p_{1} 0 ∧ p ≠ 0_{E_{T}^{2}}} holds s_{1} -FanMorphE(x) ∈ K_{0}.

(107) Let s_{1} be a real number and D be a non empty subset of E_{T}^{2}. Suppose − 1 < s_{1} and s_{1} < 1 and D^{c} = {0_{E_{T}^{2}}}. Then there exists a map h from (E_{T}^{2})↾D into (E_{T}^{2})↾D such that h = s_{1} -FanMorphE↾D and h is continuous.

(108) Let s_{1} be a real number. Suppose − 1 < s_{1} and s_{1} < 1. Then there exists a map h from E_{T}^{2} into E_{T}^{2} such that h = s_{1} -FanMorphE and h is continuous.

(109) For every real number s_{1} such that − 1 < s_{1} and s_{1} < 1 holds s_{1} -FanMorphE is one-to-one.

(110) For every real number s_{1} such that − 1 < s_{1} and s_{1} < 1 holds s_{1} -FanMorphE is a map from E_{T}^{2} into E_{T}^{2} and rng(s_{1} -FanMorphE) = the carrier of E_{T}^{2}.

(111) Let s_{1} be a real number and p_{2} be a point of E_{T}^{2}. Suppose − 1 < s_{1} and s_{1} < 1. Then there exists a non empty compact subset K of E_{T}^{2} such that K = s_{1} -FanMorphE^{∘} K and there exists a subset V_{2} of E_{T}^{2} such that p_{2} ∈ V_{2} and V_{2} is open and V_{2} ⊆ K and s_{1} -FanMorphE(p_{2}) ∈ V_{2}.

(112) Let s_{1} be a real number. Suppose − 1 < s_{1} and s_{1} < 1. Then there exists a map f from E_{T}^{2} into E_{T}^{2} such that f = s_{1} -FanMorphE and f is a homeomorphism.

(113) Let s_{1} be a real number and q be a point of E_{T}^{2}. Suppose − 1 < s_{1} and s_{1} < 1 and q_{1} > 0 and \frac{q_{2}}{|q|} s_{1}. Let p be a point of E_{T}^{2}. If p = s_{1} -FanMorphE(q), then p_{1} > 0 and p_{2} 0.

(114) Let s_{1} be a real number and q be a point of E_{T}^{2}. Suppose − 1 < s_{1} and s_{1} < 1 and q_{1} > 0 and \frac{q_{2}}{|q|} < s_{1}. Let p be a point of E_{T}^{2}. If p = s_{1} -FanMorphE(q), then p_{1} > 0 and p_{2} < 0.

(115) Let s_{1} be a real number and q_{1}, q_{2} be points of E_{T}^{2}. Suppose − 1 < s_{1} and s_{1} < 1 and (q_{1})_{1} > 0 and \frac{(q_{1})_{2}}{|q_{1}|} s_{1} and (q_{2})_{1} > 0 and \frac{(q_{2})_{2}}{|q_{2}|} s_{1} and

\frac{(q_{1})_{2}}{|q_{1}|} < \frac{(q_{2})_{2}}{|q_{2}|} . Let p_{1}, p_{2} be points of E_{T}^{2}. If p_{1} = s_{1} -FanMorphE(q_{1}) and

p_{2} = s_{1} -FanMorphE(q_{2}), then \frac{(p_{1})_{2}}{|p_{1}|} < \frac{(p_{2})_{2}}{|p_{2}|} .

(116) Let s_{1} be a real number and q_{1}, q_{2} be points of E_{T}^{2}. Suppose − 1 < s_{1} and s_{1} < 1 and (q_{1})_{1} > 0 and \frac{(q_{1})_{2}}{|q_{1}|} < s_{1} and (q_{2})_{1} > 0 and \frac{(q_{2})_{2}}{|q_{2}|} < s_{1} and

\frac{(q_{1})_{2}}{|q_{1}|} < \frac{(q_{2})_{2}}{|q_{2}|} . Let p_{1}, p_{2} be points of E_{T}^{2}. If p_{1} = s_{1} -FanMorphE(q_{1}) and

p_{2} = s_{1} -FanMorphE(q_{2}), then \frac{(p_{1})_{2}}{|p_{1}|} < \frac{(p_{2})_{2}}{|p_{2}|} .

(117) Let s_{1} be a real number and q_{1}, q_{2} be points of E_{T}^{2}. Suppose − 1 < s_{1} and s_{1} < 1 and (q_{1})_{1} > 0 and (q_{2})_{1} > 0 and \frac{(q_{1})_{2}}{|q_{1}|} < \frac{(q_{2})_{2}}{|q_{2}|} . Let p_{1}, p_{2} be points of E_{T}^{2}. If p_{1} = s_{1} -FanMorphE(q_{1}) and p_{2} = s_{1} -FanMorphE(q_{2}), then \frac{(p_{1})_{2}}{|p_{1}|} < \frac{(p_{2})_{2}}{|p_{2}|} .

(118) Let s_{1} be a real number and q be a point of E_{T}^{2}. Suppose − 1 < s_{1} and s_{1} < 1 and q_{1} > 0 and \frac{q_{2}}{|q|} = s_{1}. Let p be a point of E_{T}^{2}. If p = s_{1} -FanMorphE(q), then p_{1} > 0 and p_{2} = 0.

(119) For every real number s_{1} holds 0_{E_{T}^{2}} = s_{1} -FanMorphE(0_{E_{T}^{2}}).

5. Fan Morphism for South

Let s be a real number and let q be a point of E_{T}^{2}. The functor FanS(s, q) yields a point of E_{T}^{2} and is defined by:

(Def. 8) FanS(s, q) = \{ \begin{matrix}|q| · [^{\frac{\frac{q_{1}}{|q|} −s}{1−s}} , − \sqrt{1 − (^{\frac{\frac{q_{1}}{|q|} −s}{1−s}} )^{2}} ], if \frac{q_{1}}{|q|} s and q_{2} < 0, \\ |q| · [^{\frac{\frac{q_{1}}{|q|} −s}{1+s}} , − \sqrt{1 − (^{\frac{\frac{q_{1}}{|q|} −s}{1+s}} )^{2}} ], if \frac{q_{1}}{|q|} < s and q_{2} < 0, \\ q, otherwise. \end{matrix}

Let c be a real number. The functor c -FanMorphS yielding a function from the carrier of E_{T}^{2} into the carrier of E_{T}^{2} is defined by:

(Def. 9) For every point q of E_{T}^{2} holds c -FanMorphS(q) = FanS(c, q).

One can prove the following propositions:

(120) Let c_{1} be a real number. Then (i) if \frac{q_{1}}{|q|} c_{1} and q_{2} < 0, then c_{1} -FanMorphS(q) = [|q| · ^{\frac{\frac{q_{1}}{|q|} −c_{1}}{1−c_{1}}} ,

|q| · − \sqrt{1 − (^{\frac{\frac{q_{1}}{|q|} −c_{1}}{1−c_{1}}} )^{2}} ], and (ii) if q_{2} 0, then c_{1} -FanMorphS(q) = q.

(121) For every real number c_{1} such that \frac{q_{1}}{|q|} c_{1} and q_{2} < 0 holds

c_{1} -FanMorphS(q) = [|q| · ^{\frac{\frac{q_{1}}{|q|} −c_{1}}{1+c_{1}}} , |q| · − \sqrt{1 − (^{\frac{\frac{q_{1}}{|q|} −c_{1}}{1+c_{1}}} )^{2}} ].

(122) Let c_{1} be a real number such that − 1 < c_{1} and c_{1} < 1. Then (i) if \frac{q_{1}}{|q|} c_{1} and q_{2} 0 and q ≠ 0_{E_{T}^{2}}, then c_{1} -FanMorphS(q) = [|q|· ^{\frac{\frac{q_{1}}{|q|} −c_{1}}{1−c_{1}}} ,

|q| · − \sqrt{1 − (^{\frac{\frac{q_{1}}{|q|} −c_{1}}{1−c_{1}}} )^{2}} ], and

(ii) if \frac{q_{1}}{|q|} c_{1} and q_{2} 0 and q ≠ 0_{E_{T}^{2}}, then c_{1} -FanMorphS(q) = [|q|· ^{\frac{\frac{q_{1}}{|q|} −c_{1}}{1+c_{1}}} ,

|q| · − \sqrt{1 − (^{\frac{\frac{q_{1}}{|q|} −c_{1}}{1+c_{1}}} )^{2}} ].

(123) Let c_{1} be a real number, K_{1} be a non empty subset of E_{T}^{2}, and f be a

map from (E_{T}^{2})↾K_{1} into ℝ^{1}. Suppose that

(i) − 1 < c_{1}, (ii) c_{1} < 1, (iii) for every point p of E_{T}^{2} such that p ∈ the carrier of (E_{T}^{2})↾K_{1} holds

f(p) = |p| · ^{\frac{\frac{p_{1}}{|p|} −c_{1}}{1−c_{1}}} , and (iv) for every point q of E_{T}^{2} such that q ∈ the carrier of (E_{T}^{2})↾K_{1} holds q_{2} 0

and q ≠ 0_{E_{T}^{2}}. Then f is continuous.

(124) Let c_{1} be a real number, K_{1} be a non empty subset of E_{T}^{2}, and f be a

map from (E_{T}^{2})↾K_{1} into ℝ^{1}. Suppose that

(i) − 1 < c_{1}, (ii) c_{1} < 1, (iii) for every point p of E_{T}^{2} such that p ∈ the carrier of (E_{T}^{2})↾K_{1} holds

f(p) = |p| · ^{\frac{\frac{p_{1}}{|p|} −c_{1}}{1+c_{1}}} , and (iv) for every point q of E_{T}^{2} such that q ∈ the carrier of (E_{T}^{2})↾K_{1} holds q_{2} 0

and q ≠ 0_{E_{T}^{2}}. Then f is continuous.

(125) Let c_{1} be a real number, K_{1} be a non empty subset of E_{T}^{2}, and f be a

map from (E_{T}^{2})↾K_{1} into ℝ^{1}. Suppose that

(i) − 1 < c_{1}, (ii) c_{1} < 1, (iii) for every point p of E_{T}^{2} such that p ∈ the carrier of (E_{T}^{2})↾K_{1} holds

f(p) = |p| · − \sqrt{1 − (^{\frac{\frac{p_{1}}{|p|} −c_{1}}{1−c_{1}}} )^{2}} , and (iv) for every point q of E_{T}^{2} such that q ∈ the carrier of (E_{T}^{2})↾K_{1} holds q_{2} 0

and \frac{q_{1}}{|q|} c_{1} and q ≠ 0_{E_{T}^{2}}. Then f is continuous.

(126) Let c_{1} be a real number, K_{1} be a non empty subset of E_{T}^{2}, and f be a

map from (E_{T}^{2})↾K_{1} into ℝ^{1}. Suppose that

(i) − 1 < c_{1}, (ii) c_{1} < 1, (iii) for every point p of E_{T}^{2} such that p ∈ the carrier of (E_{T}^{2})↾K_{1} holds

f(p) = |p| · − \sqrt{1 − (^{\frac{\frac{p_{1}}{|p|} −c_{1}}{1+c_{1}}} )^{2}} , and (iv) for every point q of E_{T}^{2} such that q ∈ the carrier of (E_{T}^{2})↾K_{1} holds q_{2} 0

and \frac{q_{1}}{|q|} c_{1} and q ≠ 0_{E_{T}^{2}}. Then f is continuous.

(127) Let c_{1} be a real number, K_{0}, B_{0} be subsets of E_{T}^{2}, and f be a map from (E_{T}^{2})↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < c_{1} and c_{1} < 1 and f = c_{1} -FanMorphS↾K_{0} and B_{0} = {q; q ranges over points of E_{T}^{2}: q_{2} 0 ∧ q ≠ 0_{E_{T}^{2}}\} and K_{0} = \{p : \frac{p_{1}}{|p|} c_{1} ∧ p_{2} 0 ∧ p ≠ 0_{E_{T}^{2}}\}. Then f is continuous.

(128) Let c_{1} be a real number, K_{0}, B_{0} be subsets of E_{T}^{2}, and f be a map from (E_{T}^{2})↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < c_{1} and c_{1} < 1 and f = c_{1} -FanMorphS↾K_{0} and B_{0} = {q; q ranges over points of E_{T}^{2}: q_{2} 0 ∧ q ≠ 0_{E_{T}^{2}}\} and K_{0} = \{p : \frac{p_{1}}{|p|} c_{1} ∧ p_{2} 0 ∧ p ≠ 0_{E_{T}^{2}}\}. Then f is continuous.

(129) For every real number c_{1} and for every subset K_{3} of E_{T}^{2} such that K_{3} = {p : p_{1} c_{1} · |p| ∧ p_{2} 0} holds K_{3} is closed.

(130) For every real number c_{1} and for every subset K_{3} of E_{T}^{2} such that K_{3} = {p : p_{1} c_{1} · |p| ∧ p_{2} 0} holds K_{3} is closed.

(131) Let c_{1} be a real number, K_{0}, B_{0} be subsets of E_{T}^{2}, and f be a map from (E_{T}^{2})↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < c_{1} and c_{1} < 1 and f = c_{1} -FanMorphS↾K_{0} and B_{0} = (the carrier of E_{T}^{2}) \ {0_{E_{T}^{2}}} and K_{0} = {p : p_{2} 0 ∧ p ≠ 0_{E_{T}^{2}}}. Then f is continuous.

(132) Let c_{1} be a real number, K_{0}, B_{0} be subsets of E_{T}^{2}, and f be a map from (E_{T}^{2})↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < c_{1} and c_{1} < 1 and f = c_{1} -FanMorphS↾K_{0} and B_{0} = (the carrier of E_{T}^{2}) \ {0_{E_{T}^{2}}} and K_{0} = {p : p_{2} 0 ∧ p ≠ 0_{E_{T}^{2}}}. Then f is continuous.

(133) Let c_{1} be a real number, B_{0} be a subset of E_{T}^{2}, K_{0} be a subset of (E_{T}^{2})↾B_{0}, and f be a map from (E_{T}^{2})↾B_{0}↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < c_{1} and c_{1} < 1 and f = c_{1} -FanMorphS↾K_{0} and B_{0} = (the carrier of E_{T}^{2}) \ {0_{E_{T}^{2}}} and K_{0} = {p : p_{2} 0 ∧ p ≠ 0_{E_{T}^{2}}}. Then f is continuous.

(134) Let c_{1} be a real number, B_{0} be a subset of E_{T}^{2}, K_{0} be a subset of (E_{T}^{2})↾B_{0}, and f be a map from (E_{T}^{2})↾B_{0}↾K_{0} into (E_{T}^{2})↾B_{0}. Suppose − 1 < c_{1} and c_{1} < 1 and f = c_{1} -FanMorphS↾K_{0} and B_{0} = (the carrier of E_{T}^{2}) \ {0_{E_{T}^{2}}} and K_{0} = {p : p_{2} 0 ∧ p ≠ 0_{E_{T}^{2}}}. Then f is continuous.

(135) For every real number c_{1} and for every point p of E_{T}^{2} holds |c_{1} -FanMorphS(p)| = |p|.

(136) For every real number c_{1} and for all sets x, K_{0} such that − 1 < c_{1} and c_{1} < 1 and x ∈ K_{0} and K_{0} = {p : p_{2} 0 ∧ p ≠ 0_{E_{T}^{2}}} holds c_{1} -FanMorphS(x) ∈ K_{0}.

(137) For every real number c_{1} and for all sets x, K_{0} such that − 1 < c_{1} and c_{1} < 1 and x ∈ K_{0} and K_{0} = {p : p_{2} 0 ∧ p ≠ 0_{E_{T}^{2}}} holds c_{1} -FanMorphS(x) ∈ K_{0}.

(138) Let c_{1} be a real number and D be a non empty subset of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and D^{c} = {0_{E_{T}^{2}}}. Then there exists a map h from (E_{T}^{2})↾D into (E_{T}^{2})↾D such that h = c_{1} -FanMorphS↾D and h is continuous.

(139) Let c_{1} be a real number. Suppose − 1 < c_{1} and c_{1} < 1. Then there exists a map h from E_{T}^{2} into E_{T}^{2} such that h = c_{1} -FanMorphS and h is continuous.

(140) For every real number c_{1} such that − 1 < c_{1} and c_{1} < 1 holds c_{1} -FanMorphS is one-to-one.

(141) For every real number c_{1} such that − 1 < c_{1} and c_{1} < 1 holds c_{1} -FanMorphS is a map from E_{T}^{2} into E_{T}^{2} and rng(c_{1} -FanMorphS) = the carrier of E_{T}^{2}.

(142) Let c_{1} be a real number and p_{2} be a point of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1. Then there exists a non empty compact subset K of E_{T}^{2} such that K = c_{1} -FanMorphS^{∘} K and there exists a subset V_{2} of E_{T}^{2} such that p_{2} ∈ V_{2} and V_{2} is open and V_{2} ⊆ K and c_{1} -FanMorphS(p_{2}) ∈ V_{2}.

(143) Let c_{1} be a real number. Suppose − 1 < c_{1} and c_{1} < 1. Then there exists a map f from E_{T}^{2} into E_{T}^{2} such that f = c_{1} -FanMorphS and f is a homeomorphism.

(144) Let c_{1} be a real number and q be a point of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and q_{2} < 0 and \frac{q_{1}}{|q|} c_{1}. Let p be a point of E_{T}^{2}. If p = c_{1} -FanMorphS(q), then p_{2} < 0 and p_{1} 0.

(145) Let c_{1} be a real number and q be a point of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and q_{2} < 0 and \frac{q_{1}}{|q|} < c_{1}. Let p be a point of E_{T}^{2}. If p = c_{1} -FanMorphS(q), then p_{2} < 0 and p_{1} < 0.

(146) Let c_{1} be a real number and q_{1}, q_{2} be points of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and (q_{1})_{2} < 0 and \frac{(q_{1})_{1}}{|q_{1}|} c_{1} and (q_{2})_{2} < 0 and \frac{(q_{2})_{1}}{|q_{2}|} c_{1} and

\frac{(q_{1})_{1}}{|q_{1}|} < \frac{(q_{2})_{1}}{|q_{2}|} . Let p_{1}, p_{2} be points of E_{T}^{2}. If p_{1} = c_{1} -FanMorphS(q_{1}) and

p_{2} = c_{1} -FanMorphS(q_{2}), then \frac{(p_{1})_{1}}{|p_{1}|} < \frac{(p_{2})_{1}}{|p_{2}|} .

(147) Let c_{1} be a real number and q_{1}, q_{2} be points of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and (q_{1})_{2} < 0 and \frac{(q_{1})_{1}}{|q_{1}|} < c_{1} and (q_{2})_{2} < 0 and \frac{(q_{2})_{1}}{|q_{2}|} < c_{1} and

\frac{(q_{1})_{1}}{|q_{1}|} < \frac{(q_{2})_{1}}{|q_{2}|} . Let p_{1}, p_{2} be points of E_{T}^{2}. If p_{1} = c_{1} -FanMorphS(q_{1}) and

p_{2} = c_{1} -FanMorphS(q_{2}), then \frac{(p_{1})_{1}}{|p_{1}|} < \frac{(p_{2})_{1}}{|p_{2}|} .

(148) Let c_{1} be a real number and q_{1}, q_{2} be points of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and (q_{1})_{2} < 0 and (q_{2})_{2} < 0 and \frac{(q_{1})_{1}}{|q_{1}|} < \frac{(q_{2})_{1}}{|q_{2}|} . Let p_{1}, p_{2} be points of E_{T}^{2}. If p_{1} = c_{1} -FanMorphS(q_{1}) and p_{2} = c_{1} -FanMorphS(q_{2}), then \frac{(p_{1})_{1}}{|p_{1}|} < \frac{(p_{2})_{1}}{|p_{2}|} .

(149) Let c_{1} be a real number and q be a point of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and q_{2} < 0 and \frac{q_{1}}{|q|} = c_{1}. Let p be a point of E_{T}^{2}. If p = c_{1} -FanMorphS(q), then p_{2} < 0 and p_{1} = 0.

(150) For every real number c_{1} holds 0_{E_{T}^{2}} = c_{1} -FanMorphS(0_{E_{T}^{2}}).

References

[1] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

fan homeomorphisms in the plane 19

[2] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[3] Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357–367, 1990.

[4] Czesław Byliński and Piotr Rudnicki. Bounding boxes for compact sets in E^{2}. Formalized Mathematics, 6(3):427–440, 1997.

[5] Agata Darmochwał. Compact spaces. Formalized Mathematics, 1(2):383–386, 1990.

[6] Agata Darmochwał. Families of subsets, subspaces and mappings in topological spaces. Formalized Mathematics, 1(2):257–261, 1990.

[7] Agata Darmochwał. The Euclidean space. Formalized Mathematics, 2(4):599–603, 1991.

[8] Agata Darmochwał and Yatsuka Nakamura. Metric spaces as topological spaces - fundamental concepts. Formalized Mathematics, 2(4):605–608, 1991.

[9] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[10] Stanisława Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Formalized Mathematics, 1(3):607–610, 1990.

[11] Yatsuka Nakamura. Graph theoretical properties of arcs in the plane and Fashoda Meet Theorem. Formalized Mathematics, 7(2):193–201, 1998.

[12] Yatsuka Nakamura, Andrzej Trybulec, and Czesław Byliński. Bounded domains and unbounded domains. Formalized Mathematics, 8(1):1–13, 1999.

[13] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990.

[14] Jan Popiołek. Some properties of functions modul and signum. Formalized Mathematics, 1(2):263–264, 1990.

[15] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[16] Andrzej Trybulec and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445–449, 1990.

[17] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[18] Zinaida Trybulec and Halina Święczkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

[19] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.

Received January 8, 2002

Half Open Intervals in Real Numbers

Yatsuka Nakamura Shinshu University Nagano

Summary. Left and right half open intervals in the real line are defined. Their properties are investigated. A class of all finite union of such intervals are, in a sense, closed by operations of union, intersection and the difference of sets.

MML Identifier: RCOMP 2.

The terminology and notation used here are introduced in the following articles: [5], [1], [3], [4], and [2].

In this paper s, g, h, r, p, p_{1}, p_{2}, q, q_{1}, q_{2}, x, y, z denote real numbers. The following two propositions are true:

(1) x < y and x < z iff x < min(y, z).

(2) y < x and z < x iff max(y, z) < x. Let g, s be real numbers. The functor [g, s[ yielding a subset of ℝ is defined

as follows: (Def. 1) [g, s[= {r; r ranges over real numbers: g r ∧ r < s}.

The functor ]g, s] yields a subset of ℝ and is defined as follows: (Def. 2) ]g, s] = {r; r ranges over real numbers: g < r ∧ r s}.

Next we state a number of propositions:

(3) r ∈ [p, q[ iff p r and r < q.

(4) r ∈ ]p, q] iff p < r and r q.

(5) For all g, s such that g < s holds [g, s[= ]g, s[ ∪ {g}.

(6) For all g, s such that g < s holds ]g, s] = ]g, s[ ∪ {s}.

(7) [g, g[= ∅.

(8) ]g, g] = ∅.

(9) If p g, then [g, p[= ∅.

(10) If p g, then ]g, p] = ∅.

(11) If g p and p h, then [g, p[∪[p, h[= [g, h[.

(12) If g p and p h, then ]g, p] ∪]p, h] = ]g, h].

(13) If g p_{1} and g p_{2} and p_{1} h and p_{2} h, then [g, h] = [g, p_{1}[∪[p_{1}, p_{2}]∪ ]p_{2}, h].

(14) If g < p_{1} and g < p_{2} and p_{1} < h and p_{2} < h, then ]g, h[ = ]g, p_{1}] ∪ ]p_{1}, p_{2}[ ∪ [p_{2}, h[.

(15) [q_{1}, q_{2}[∩[p_{1}, p_{2}[= [max(q_{1}, p_{1}), min(q_{2}, p_{2})[.

(16) ]q_{1}, q_{2}] ∩]p_{1}, p_{2}] = ]max(q_{1}, p_{1}), min(q_{2}, p_{2})].

(17) ]p, q[ ⊆ [p, q[ and ]p, q[ ⊆ ]p, q] and [p, q[⊆ [p, q] and ]p, q] ⊆ [p, q].

(18) If r ∈ [p, g[ and s ∈ [p, g[, then [r, s] ⊆ [p, g[.

(19) If r ∈ ]p, g] and s ∈ ]p, g], then [r, s] ⊆ ]p, g].

(20) If p q and q r, then [p, q] ∪]q, r] = [p, r].

(21) If p q and q r, then [p, q[∪[q, r] = [p, r].

(22) If [q_{1}, q_{2}[ meets [p_{1}, p_{2}[, then q_{2} p_{1}.

(23) If ]q_{1}, q_{2}] meets ]p_{1}, p_{2}], then q_{2} p_{1}.

(24) If [q_{1}, q_{2}[ meets [p_{1}, p_{2}[, then [q_{1}, q_{2}[∪[p_{1}, p_{2}[= [min(q_{1}, p_{1}), max(q_{2}, p_{2})[.

(25) If ]q_{1}, q_{2}] meets ]p_{1}, p_{2}], then ]q_{1}, q_{2}] ∪]p_{1}, p_{2}] = ]min(q_{1}, p_{1}), max(q_{2}, p_{2})].

(26) If [p_{1}, p_{2}[ meets [q_{1}, q_{2}[, then [p_{1}, p_{2}[\[q_{1}, q_{2}[= [p_{1}, q_{1}[∪[q_{2}, p_{2}[.

(27) If ]p_{1}, p_{2}] meets ]q_{1}, q_{2}], then ]p_{1}, p_{2}] \]q_{1}, q_{2}] = ]p_{1}, q_{1}] ∪]q_{2}, p_{2}].

References

[1] Konrad Raczkowski and Paweł Sadowski. Topological properties of subsets in real numbers. Formalized Mathematics, 1(4):777–780, 1990.

[2] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[3] Andrzej Trybulec and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445–449, 1990.

[4] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[5] Zinaida Trybulec and Halina Święczkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

Received February 1, 2002

Some Remarks on Clockwise Oriented Sequences on Go-boards^{1}

Adam Naumowicz^{2} University of Białystok

Robert Milewski University of Białystok

Summary. The main goal of this paper is to present alternative characterizations of clockwise oriented sequences on Go-boards.

MML Identifier: JORDAN1I.

The articles [8], [21], [9], [2], [3], [26], [24], [4], [16], [18], [23], [14], [20], [19], [5], [7], [13], [1], [6], [12], [28], [15], [17], [25], [27], [22], [10], and [11] provide the terminology and notation for this paper.

1. Preliminaries

In this paper i, j, k, n denote natural numbers. Next we state several propositions:

(1) For all subsets A, B of E_{T}^{n} such that A is Bounded or B is Bounded holds A ∩ B is Bounded.

(2) For all subsets A, B of E_{T}^{n} such that A is not Bounded and B is Bounded holds A \ B is not Bounded.

(3) For every compact connected non vertical non horizontal subset C of E_{T}^{2} holds (W-min L̃(Cage(C, n))) ↫ Cage(C, n) > 1.

(4) For every compact connected non vertical non horizontal subset C of E_{T}^{2} holds (E-max L̃(Cage(C, n))) ↫ Cage(C, n) > 1.

(5) For every compact connected non vertical non horizontal subset C of E_{T}^{2} holds (S-max L̃(Cage(C, n))) ↫ Cage(C, n) > 1.

1This work has been partially supported by CALCULEMUS grant HPRN-CT-2000-00102.

2This work was completed during the authors’s visit to Shinshu University.

2. On Bounding Points of Circular Sequences

Next we state several propositions:

(6) Let f be a non constant standard special circular sequence and p be a point of E_{T}^{2}. If p ∈ rngf, then leftcell(f, p ↫ f) = leftcell(f_{⟲}^{p}, 1).

(7) Let f be a non constant standard special circular sequence and p be a point of E_{T}^{2}. If p ∈ rngf, then rightcell(f, p ↫ f) = rightcell(f_{⟲}^{p}, 1).

(8) For every compact connected non vertical non horizontal non empty subset C of E_{T}^{2} holds W-minC ∈ rightcell((Cage(C, n))_{⟲}^{W-min L̃(Cage(C,n))}, 1).

(9) For every compact connected non vertical non horizontal non empty subset C of E_{T}^{2} holds E-maxC ∈ rightcell((Cage(C, n))_{⟲}^{E-max L̃(Cage(C,n))}, 1).

(10) For every compact connected non vertical non horizontal non empty subset C of E_{T}^{2} holds S-maxC ∈ rightcell((Cage(C, n))_{⟲}^{S-max L̃(Cage(C,n))}, 1).

3. On Clockwise Oriented Sequences

One can prove the following propositions:

(11) Let f be a clockwise oriented non constant standard special circular sequence and p be a point of E_{T}^{2}. If p_{1} < W-bound L̃(f), then p ∈ LeftComp(f).

(12) Let f be a clockwise oriented non constant standard special circular sequence and p be a point of E_{T}^{2}. If p_{1} > E-bound L̃(f), then p ∈ LeftComp(f).

(13) Let f be a clockwise oriented non constant standard special circular sequence and p be a point of E_{T}^{2}. If p_{2} < S-bound L̃(f), then p ∈ LeftComp(f).

(14) Let f be a clockwise oriented non constant standard special circular sequence and p be a point of E_{T}^{2}. If p_{2} > N-bound L̃(f), then p ∈ LeftComp(f).

(15) Let f be a clockwise oriented non constant standard special circular sequence and G be a Go-board. Suppose f is a sequence which elements belong to G. Let i, j, k be natural numbers. Suppose 1 k and k + 1 lenf and ⟨⟨i, j⟩⟩ ∈ the indices of G and ⟨⟨i + 1, j⟩⟩ ∈ the indices of G and f_{k} = G ∘ (i + 1, j) and f_{k+1} = G ∘ (i, j). Then j < widthG.

(16) Let f be a clockwise oriented non constant standard special circular sequence and G be a Go-board. Suppose f is a sequence which elements belong to G. Let i, j, k be natural numbers. Suppose 1 k and k + 1 lenf and ⟨⟨i, j⟩⟩ ∈ the indices of G and ⟨⟨i, j + 1⟩⟩ ∈ the indices of G and f_{k} = G ∘ (i, j) and f_{k+1} = G ∘ (i, j + 1). Then i < lenG.

(17) Let f be a clockwise oriented non constant standard special circular sequence and G be a Go-board. Suppose f is a sequence which elements belong to G. Let i, j, k be natural numbers. Suppose 1 k and k + 1 lenf and ⟨⟨i, j⟩⟩ ∈ the indices of G and ⟨⟨i + 1, j⟩⟩ ∈ the indices of G and f_{k} = G ∘ (i, j) and f_{k+1} = G ∘ (i + 1, j). Then j > 1.

(18) Let f be a clockwise oriented non constant standard special circular sequence and G be a Go-board. Suppose f is a sequence which elements belong to G. Let i, j, k be natural numbers. Suppose 1 k and k + 1 lenf and ⟨⟨i, j⟩⟩ ∈ the indices of G and ⟨⟨i, j + 1⟩⟩ ∈ the indices of G and f_{k} = G ∘ (i, j + 1) and f_{k+1} = G ∘ (i, j). Then i > 1.

(19) Let f be a clockwise oriented non constant standard special circular sequence and G be a Go-board. Suppose f is a sequence which elements belong to G. Let i, j, k be natural numbers. Suppose 1 k and k + 1 lenf and ⟨⟨i, j⟩⟩ ∈ the indices of G and ⟨⟨i + 1, j⟩⟩ ∈ the indices of G and f_{k} = G ∘ (i + 1, j) and f_{k+1} = G ∘ (i, j). Then (f_{k})_{2} ≠ N-bound L̃(f).

(20) Let f be a clockwise oriented non constant standard special circular sequence and G be a Go-board. Suppose f is a sequence which elements belong to G. Let i, j, k be natural numbers. Suppose 1 k and k + 1 lenf and ⟨⟨i, j⟩⟩ ∈ the indices of G and ⟨⟨i, j + 1⟩⟩ ∈ the indices of G and f_{k} = G ∘ (i, j) and f_{k+1} = G ∘ (i, j + 1). Then (f_{k})_{1} ≠ E-bound L̃(f).

(21) Let f be a clockwise oriented non constant standard special circular sequence and G be a Go-board. Suppose f is a sequence which elements belong to G. Let i, j, k be natural numbers. Suppose 1 k and k + 1 lenf and ⟨⟨i, j⟩⟩ ∈ the indices of G and ⟨⟨i + 1, j⟩⟩ ∈ the indices of G and f_{k} = G ∘ (i, j) and f_{k+1} = G ∘ (i + 1, j). Then (f_{k})_{2} ≠ S-bound L̃(f).

(22) Let f be a clockwise oriented non constant standard special circular sequence and G be a Go-board. Suppose f is a sequence which elements belong to G. Let i, j, k be natural numbers. Suppose 1 k and k + 1 lenf and ⟨⟨i, j⟩⟩ ∈ the indices of G and ⟨⟨i, j + 1⟩⟩ ∈ the indices of G and f_{k} = G ∘ (i, j + 1) and f_{k+1} = G ∘ (i, j). Then (f_{k})_{1} ≠ W-bound L̃(f).

(23) Let f be a clockwise oriented non constant standard special circular sequence, G be a Go-board, and k be a natural number. Suppose f is a sequence which elements belong to G and 1 k and k + 1 lenf and f_{k} = W-min L̃(f). Then there exist natural numbers i, j such that ⟨⟨i, j⟩⟩∈ the indices of G and ⟨⟨i, j + 1⟩⟩∈ the indices of G and f_{k} = G ∘ (i, j) and f_{k+1} = G ∘ (i, j + 1).

(24) Let f be a clockwise oriented non constant standard special circular sequence, G be a Go-board, and k be a natural number. Suppose f is a sequence which elements belong to G and 1 k and k + 1 lenf and f_{k} = N-min L̃(f). Then there exist natural numbers i, j such that ⟨⟨i, j⟩⟩∈ the indices of G and ⟨⟨i + 1, j⟩⟩∈ the indices of G and f_{k} = G ∘ (i, j) and f_{k+1} = G ∘ (i + 1, j).

(25) Let f be a clockwise oriented non constant standard special circular sequence, G be a Go-board, and k be a natural number. Suppose f is a sequence which elements belong to G and 1 k and k + 1 lenf and f_{k} = E-max L̃(f). Then there exist natural numbers i, j such that ⟨⟨i, j +1⟩⟩∈ the indices of G and ⟨⟨i, j⟩⟩∈ the indices of G and f_{k} = G∘(i, j +1) and f_{k+1} = G ∘ (i, j).

(26) Let f be a clockwise oriented non constant standard special circular sequence, G be a Go-board, and k be a natural number. Suppose f is a sequence which elements belong to G and 1 k and k + 1 lenf and f_{k} = S-max L̃(f). Then there exist natural numbers i, j such that ⟨⟨i + 1, j⟩⟩∈ the indices of G and ⟨⟨i, j⟩⟩∈ the indices of G and f_{k} = G ∘ (i + 1, j) and f_{k+1} = G ∘ (i, j).

(27) Let f be a non constant standard special circular sequence. Then f is clockwise oriented if and only if (f_{⟲}^{W-min L̃(f)})_{2} ∈ W-most L̃(f).

(28) Let f be a non constant standard special circular sequence. Then f is clockwise oriented if and only if (f_{⟲}^{E-max L̃(f)})_{2} ∈ E-most L̃(f).

(29) Let f be a non constant standard special circular sequence. Then f is clockwise oriented if and only if (f_{⟲}^{S-max L̃(f)})_{2} ∈ S-most L̃(f).

(30) Let C be a compact non vertical non horizontal non empty subset of E_{T}^{2} satisfying conditions of simple closed curve and p be a point of E_{T}^{2}. Suppose p_{1} = \frac{W-bound C+E-bound C}{2} and i > 0 and 1 k and k widthGauge(C, i) and Gauge(C, i) ∘ (CenterGauge(C, i), k) ∈ UpperArc L̃(Cage(C, i)) and p_{2} = sup(proj2^{∘}(L(Gauge(C, 1) ∘ (CenterGauge(C, 1), 1), Gauge(C, i) ∘ (CenterGauge(C, i), k)) ∩ LowerArc L̃(Cage(C, i)))). Then there exists j such that 1 j and j lenGauge(C, i) and p = Gauge(C, i) ∘ (CenterGauge(C, i), j).

References

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[2] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

[3] Czesław Byliński. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529–536, 1990.

[4] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[5] Czesław Byliński. Gauges. Formalized Mathematics, 8(1):25–27, 1999.

[6] Czesław Byliński and Piotr Rudnicki. Bounding boxes for compact sets in E^{2}. Formalized Mathematics, 6(3):427–440, 1997.

[7] Czesław Byliński and Mariusz Żynel. Cages - the external approximation of Jordan’s curve. Formalized Mathematics, 9(1):19–24, 2001.

[8] Agata Darmochwał. Compact spaces. Formalized Mathematics, 1(2):383–386, 1990.

[9] Agata Darmochwał. The Euclidean space. Formalized Mathematics, 2(4):599–603, 1991.

[10] Agata Darmochwał and Yatsuka Nakamura. The topological space E_{T}^{2}. Arcs, line segments and special polygonal arcs. Formalized Mathematics, 2(5):617–621, 1991.

[11] Agata Darmochwał and Yatsuka Nakamura. The topological space E_{T}^{2}. Simple closed curves. Formalized Mathematics, 2(5):663–664, 1991.

some remarks on clockwise oriented sequences … 27

[12] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[13] Katarzyna Jankowska. Matrices. Abelian group of matrices. Formalized Mathematics, 2(4):475–480, 1991.

[14] Artur Korniłowicz, Robert Milewski, Adam Naumowicz, and Andrzej Trybulec. Gauges and cages. Part I. Formalized Mathematics, 9(3):501–509, 2001.

[15] Jarosław Kotowicz. Monotone real sequences. Subsequences. Formalized Mathematics, 1(3):471–475, 1990.

[16] Jarosław Kotowicz and Yatsuka Nakamura. Introduction to Go-board - part I. Formalized Mathematics, 3(1):107–115, 1992.

[17] Yatsuka Nakamura and Czesław Byliński. Extremal properties of vertices on special polygons. Part I. Formalized Mathematics, 5(1):97–102, 1996.

[18] Yatsuka Nakamura and Andrzej Trybulec. Decomposing a Go-board into cells. Formalized Mathematics, 5(3):323–328, 1996.

[19] Yatsuka Nakamura and Andrzej Trybulec. A decomposition of a simple closed curves and the order of their points. Formalized Mathematics, 6(4):563–572, 1997.

[20] Yatsuka Nakamura, Andrzej Trybulec, and Czesław Byliński. Bounded domains and unbounded domains. Formalized Mathematics, 8(1):1–13, 1999.

[21] Beata Padlewska. Connected spaces. Formalized Mathematics, 1(1):239–244, 1990.

[22] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[23] Andrzej Trybulec. Left and right component of the complement of a special closed curve. Formalized Mathematics, 5(4):465–468, 1996.

[24] Andrzej Trybulec. On the decomposition of finite sequences. Formalized Mathematics, 5(3):317–322, 1996.

[25] Andrzej Trybulec and Yatsuka Nakamura. On the order on a special polygon. Formalized Mathematics, 6(4):541–548, 1997.

[26] Wojciech A. Trybulec. Pigeon hole principle. Formalized Mathematics, 1(3):575–579, 1990.

[27] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[28] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.

Dickson’s Lemma

Gilbert Lee University of Alberta Edmonton

Piotr Rudnicki University of Alberta Edmonton

Summary. We present a Mizar formalization of the proof of Dickson’s lemma following [6], chapters 4.2 and 4.3.

MML Identifier: DICKSON.

The papers [19], [29], [1], [7], [13], [21], [12], [8], [9], [2], [20], [26], [27], [24], [17], [18], [30], [32], [31], [28], [23], [4], [11], [5], [14], [22], [3], [15], [16], [25], and [10] provide the terminology and notation for this paper.

1. Preliminaries

One can prove the following two propositions:

(1) For every function g and for every set x such that domg = {x} holds g = x⟼→ . g(x).

(2) For every natural number n holds n ⊆ n + 1.

The scheme FinSegRng2 deals with natural numbers A, B, a unary functor F yielding a set, and a unary predicate P, and states that:

{F(i); i ranges over natural numbers: A < i ∧ i B ∧ P[i]} is finite

for all values of the parameters.

The following proposition is true

(3) For every infinite set X holds there exists a function from ℕ into X which is one-to-one.

Let R be a relational structure and let f be a sequence of R. We say that f is ascending if and only if:

(Def. 1) For every natural number n holds f(n+1) ≠ f(n) and ⟨⟨f(n), f(n+1)⟩⟩∈

the internal relation of R. Let R be a relational structure and let f be a sequence of R. We say that f

is weakly ascending if and only if: (Def. 2) For every natural number n holds ⟨⟨f(n), f(n+1)⟩⟩∈ the internal relation

of R. The following propositions are true:

(4) Let R be a non empty transitive relational structure and f be a sequence of R. Suppose f is weakly ascending. Let i, j be natural numbers. If i < j, then f(i) f(j).

(5) Let R be a non empty relational structure. Then R is connected if and only if the internal relation of R is strongly connected in the carrier of R.

(6) Let R be a binary relation and X be a set. Then R is reflexive in X and connected in X if and only if R is strongly connected in X.

(7) Let L be a relational structure, Y be a set, and a be an element of L. Then (the internal relation of L)-Seg(a) misses Y and a ∈ Y if and only if a is minimal w.r.t. Y, the internal relation of L.

(8) Let L be a non empty transitive antisymmetric relational structure, a, x be elements of L, and N be a set. Suppose a is minimal w.r.t. (the internal relation of L)-Seg(x) ∩ N, the internal relation of L. Then a is minimal w.r.t. N, the internal relation of L.

2. More on Ordering Relations

Let R be a relational structure. We say that R is quasi ordered if and only if:

(Def. 3) R is reflexive and transitive.

Let R be a relational structure. Let us assume that R is quasi ordered. The functor EqRel(R) yielding an equivalence relation of the carrier of R is defined as follows:

(Def. 4) EqRel(R) = (the internal relation of R) ∩ (the internal relation of R)^{⌣}. The following proposition is true

(9) Let R be a relational structure and x, y be elements of the carrier of R. If R is quasi ordered, then x ∈ [y]_{EqRel(R)} iff x y and y x.

Let R be a relational structure. The functor _{E}R yielding a binary relation on ClassesEqRel(R) is defined as follows:

(Def. 5) For all sets A, B holds ⟨⟨A, B⟩⟩∈ _{E}R iff there exist elements a, b of R

such that A = [a]_{EqRel(R)} and B = [b]_{EqRel(R)} and a b. We now state two propositions:

(10) For every relational structure R such that R is quasi ordered holds _{E}R partially orders ClassesEqRel(R).

(11) Let R be a non empty relational structure. If R is quasi ordered and

connected, then _{E}R linearly orders ClassesEqRel(R). Let R be a binary relation. The functor R\^{⌣} yields a binary relation and is

defined by: (Def. 6) R\^{⌣} = R \ R^{⌣}.

Let R be a binary relation. Note that R\^{⌣} is asymmetric. Let X be a set and let R be a binary relation on X. Then R\^{⌣} is a binary

relation on X.

Let R be a relational structure. The functor R\^{⌣} yielding a strict relational structure is defined as follows:

(Def. 7) R\^{⌣} = ⟨the carrier of R, the internal relation of R\^{⌣}⟩.

Let R be a non empty relational structure. One can check that R\^{⌣} is non empty.

Let R be a transitive relational structure. One can check that R\^{⌣} is transitive.

Let R be a relational structure. One can check that R\^{⌣} is antisymmetric. We now state several propositions:

(12) For every non empty poset R and for every element x of the carrier of R holds [x]_{EqRel(R)} = {x}.

(13) For every binary relation R holds R = R\^{⌣} iff R is asymmetric.

(14) For every binary relation R such that R is transitive holds R\^{⌣} is transitive.

(15) Let R be a binary relation and a, b be sets. If R is antisymmetric, then ⟨⟨a, b⟩⟩∈ R\^{⌣} iff ⟨⟨a, b⟩⟩∈ R and a ≠ b.

(16) For every relational structure R such that R is well founded holds R\^{⌣} is well founded.

(17) For every relational structure R such that R\^{⌣} is well founded and R is antisymmetric holds R is well founded.

3. Foundedness Properties

The following two propositions are true:

(18) Let L be a relational structure, N be a set, and x be an element of L\^{⌣}. Then x is minimal w.r.t. N, the internal relation of L\^{⌣} if and only if x ∈ N and for every element y of L such that y ∈ N and ⟨⟨y, x⟩⟩ ∈ the internal relation of L holds ⟨⟨x, y⟩⟩∈ the internal relation of L.

(19) Let R, S be non empty relational structures and m be a map from R

into S. Suppose that

(i) R is quasi ordered, (ii) S is antisymmetric, (iii) S\^{⌣} is well founded, and (iv) for all elements a, b of R holds if a b, then m(a) m(b) and if

m(a) = m(b), then ⟨⟨a, b⟩⟩∈ EqRel(R). Then R\^{⌣} is well founded.

Let R be a non empty relational structure and let N be a subset of the carrier of R. The functor MinClassesN yields a family of subsets of the carrier of R and is defined by the condition (Def. 8).

(Def. 8) Let x be a set. Then x ∈ MinClassesN if and only if there exists an element y of R\^{⌣} such that y is minimal w.r.t. N, the internal relation of R\^{⌣} and x = [y]_{EqRel(R)} ∩ N.

Next we state several propositions:

(20) Let R be a non empty relational structure, N be a subset of the carrier of R, and x be a set. Suppose R is quasi ordered and x ∈ MinClassesN. Let y be an element of R\^{⌣}. If y ∈ x, then y is minimal w.r.t. N, the internal relation of R\^{⌣}.

(21) Let R be a non empty relational structure. Then R\^{⌣} is well founded if and only if for every subset N of the carrier of R such that N ≠ ∅ there exists a set x such that x ∈ MinClassesN.

(22) Let R be a non empty relational structure, N be a subset of the carrier of R, and y be an element of R\^{⌣}. If y is minimal w.r.t. N, the internal relation of R\^{⌣}, then MinClassesN is non empty.

(23) Let R be a non empty relational structure, N be a subset of the carrier of R, and x be a set. If R is quasi ordered and x ∈ MinClassesN, then x is non empty.

(24) Let R be a non empty relational structure. Suppose R is quasi ordered. Then R is connected and R\^{⌣} is well founded if and only if for every non empty subset N of the carrier of R holds \overline{\overline{MinClassesN}} = 1.

(25) Let R be a non empty poset. Then the following statements are equiva-

lent

(i) the internal relation of R well orders the carrier of R, (ii) for every non empty subset N of the carrier of R holds \overline{\overline{MinClassesN}} =

1. Let R be a relational structure, let N be a subset of the carrier of R, and

let B be a set. We say that B is Dickson basis of N, R if and only if: (Def. 9) B ⊆ N and for every element a of R such that a ∈ N there exists an

element b of R such that b ∈ B and b a.

The following two propositions are true:

(26) For every relational structure R holds ∅ is Dickson basis of ∅_{the carrier of R}, R.

(27) Let R be a non empty relational structure, N be a non empty subset of the carrier of R, and B be a set. If B is Dickson basis of N, R, then B is non empty.

Let R be a relational structure. We say that R is Dickson if and only if: (Def. 10) For every subset N of the carrier of R holds there exists a set which is

Dickson basis of N, R and finite. The following two propositions are true:

(28) For every non empty relational structure R such that R\^{⌣} is well founded and R is connected holds R is Dickson.

(29) Let R, S be relational structures. Suppose that (i) the internal relation of R ⊆ the internal relation of S, (ii) R is Dickson, and (iii) the carrier of R = the carrier of S.

Then S is Dickson. Let f be a function and let b be a set. Let us assume that domf = ℕ and

b ∈ rngf. The functor f mindexb yielding a natural number is defined by: (Def. 11) f(f mindexb) = b and for every natural number i such that f(i) = b

holds f mindexb i. Let R be a non empty 1-sorted structure, let f be a sequence of R, let b be

a set, and let m be a natural number. Let us assume that there exists a natural number j such that m < j and f(j) = b. The functor f mindex(b, m) yielding a natural number is defined as follows:

(Def. 12) f(f mindex(b, m)) = b and m < f mindex(b, m) and for every natural

number i such that m < i and f(i) = b holds f mindex(b, m) i. Next we state several propositions:

(30) Let R be a non empty relational structure. Suppose R is quasi ordered and Dickson. Let f be a sequence of R. Then there exist natural numbers i, j such that i < j and f(i) f(j).

(31) Let R be a relational structure, N be a subset of the carrier of R, and x be an element of R\^{⌣}. Suppose R is quasi ordered and x ∈ N and (the internal relation of R)-Seg(x) ∩ N ⊆ [x]_{EqRel(R)}. Then x is minimal w.r.t. N, the internal relation of R\^{⌣}.

(32) Let R be a non empty relational structure. Suppose R is quasi ordered and for every sequence f of R there exist natural numbers i, j such that i < j and f(i) f(j). Let N be a non empty subset of the carrier of R. Then MinClassesN is finite and MinClassesN is non empty.

(33) Let R be a non empty relational structure. Suppose R is quasi ordered and for every non empty subset N of the carrier of R holds MinClassesN is finite and MinClassesN is non empty. Then R is Dickson.

(34) For every non empty relational structure R such that R is quasi ordered and Dickson holds R\^{⌣} is well founded.

(35) Let R be a non empty poset and N be a non empty subset of the carrier of R. Suppose R is Dickson. Then there exists a set B such that B is Dickson basis of N, R and for every set C such that C is Dickson basis of N, R holds B ⊆ C.

Let R be a non empty relational structure and let N be a subset of the carrier of R. Let us assume that R is Dickson. The functor Dickson-Bases(N, R) yields a non empty family of subsets of the carrier of R and is defined as follows:

(Def. 13) For every set B holds B ∈ Dickson-Bases(N, R) iff B is Dickson basis of

N, R. We now state several propositions:

(36) Let R be a non empty relational structure and s be a sequence of R. If R is Dickson, then there exists a sequence of R which is a subsequence of s and weakly ascending.

(37) For every relational structure R such that R is empty holds R is Dickson.

(38) Let M, N be relational structures. Suppose M is Dickson and N is Dickson and M is quasi ordered and N is quasi ordered. Then [: M, N :] is quasi ordered and [: M, N :] is Dickson.

(39) Let R, S be relational structures. Suppose R and S are isomorphic and R is Dickson and quasi ordered. Then S is quasi ordered and Dickson.

(40) Let p be a relational structure yielding many sorted set indexed by 1

and z be an element of 1. Then p(z) and ∏ p are isomorphic. Let X be a set, let p be a relational structure yielding many sorted set

indexed by X, and let Y be a subset of X. Note that p↾Y is relational structure yielding.

Next we state three propositions:

(41) Let n be a non empty natural number and p be a relational structure yielding many sorted set indexed by n. Then ∏ p is non empty if and only if p is nonempty.

(42) Let n be a non empty natural number, p be a relational structure yielding many sorted set indexed by n + 1, n_{1} be a subset of n + 1, and n_{2} be an element of n + 1. If n_{1} = n and n_{2} = n, then [: ∏(p↾n_{1}), p(n_{2}) :] and ∏ p are isomorphic.

(43) Let n be a non empty natural number and p be a relational structure yielding many sorted set indexed by n. Suppose that for every element i of n holds p(i) is Dickson and p(i) is quasi ordered. Then ∏ p is quasi ordered and ∏ p is Dickson.

Let p be a relational structure yielding many sorted set indexed by ∅. One can check the following observations:

∗ ∏ p is non empty,

∗ ∏ p is antisymmetric,

∗ ∏ p is quasi ordered, and

∗ ∏ p is Dickson. The binary relation NATOrd on ℕ is defined by:

(Def. 14) NATOrd = {⟨⟨x, y⟩⟩; x ranges over elements of ℕ, y ranges over elements

of ℕ: x y}. We now state four propositions:

(44) NATOrd is reflexive in ℕ.

(45) NATOrd is antisymmetric in ℕ.

(46) NATOrd is strongly connected in ℕ.

(47) NATOrd is transitive in ℕ.

The non empty relational structure OrderedNAT is defined as follows: (Def. 15) OrderedNAT = ⟨ℕ, NATOrd⟩.

One can verify the following observations:

∗ OrderedNAT is connected,

∗ OrderedNAT is Dickson,

∗ OrderedNAT is quasi ordered,

∗ OrderedNAT is antisymmetric,

∗ OrderedNAT is transitive, and

∗ OrderedNAT is well founded. Let n be a natural number. One can check the following observations:

∗ ∏(n ⟼→ OrderedNAT) is non empty,

∗ ∏(n ⟼→ OrderedNAT) is Dickson,

∗ ∏(n ⟼→ OrderedNAT) is quasi ordered, and

∗ ∏(n ⟼→ OrderedNAT) is antisymmetric. We now state three propositions:

(48) Let M be a relational structure. Suppose M is Dickson and quasi ordered. Then [: M, OrderedNAT:] is quasi ordered and [: M, OrderedNAT:] is Dickson.

(49) Let R, S be non empty relational structures. Suppose that (i) R is Dickson and quasi ordered, (ii) S is quasi ordered, (iii) the internal relation of R ⊆ the internal relation of S, and 36 gilbert lee and piotr rudnicki

(iv) the carrier of R = the carrier of S. Then S\^{⌣} is well founded.

(50) Let R be a non empty relational structure. Suppose R is quasi ordered. Then R is Dickson if and only if for every non empty relational structure S such that S is quasi ordered and the internal relation of R ⊆ the internal relation of S and the carrier of R = the carrier of S holds S\^{⌣} is well founded.

References

[1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990.

[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[3] Grzegorz Bancerek. The well ordering relations. Formalized Mathematics, 1(1):123–129, 1990.

[4] Grzegorz Bancerek. Directed sets, nets, ideals, filters, and maps. Formalized Mathematics, 6(1):93–107, 1997.

[5] Grzegorz Bancerek. The “way-below” relation. Formalized Mathematics, 6(1):169–176, 1997.

[6] Thomas Becker and Volker Weispfenning. Gröbner bases: A Computational Approach to Commutative Algebra. Springer-Verlag, New York, Berlin, 1993.

[7] Czesław Byliński. A classical first order language. Formalized Mathematics, 1(4):669–676, 1990.

[8] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

[9] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[10] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.

[11] Czesław Byliński. Galois connections. Formalized Mathematics, 6(1):131–143, 1997.

[12] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990.

[13] Agata Darmochwał and Andrzej Trybulec. Similarity of formulae. Formalized Mathematics, 2(5):635–642, 1991.

[14] Adam Grabowski. Auxiliary and approximating relations. Formalized Mathematics, 6(2):179–188, 1997.

[15] Adam Grabowski and Robert Milewski. Boolean posets, posets under inclusion and products of relational structures. Formalized Mathematics, 6(1):117–121, 1997.

[16] Artur Korniłowicz. Cartesian products of relations and relational structures. Formalized Mathematics, 6(1):145–152, 1997.

[17] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, I. Formalized Mathematics, 5(2):167–172, 1996.

[18] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990.

[19] Jan Popiołek. Introduction to Banach and Hilbert spaces - part III. Formalized Mathematics, 2(4):523–526, 1991.

[20] Jan Popiołek. Real normed space. Formalized Mathematics, 2(1):111–115, 1991.

[21] Konrad Raczkowski and Paweł Sadowski. Equivalence relations and classes of abstraction. Formalized Mathematics, 1(3):441–444, 1990.

[22] Piotr Rudnicki and Andrzej Trybulec. On same equivalents of well-foundedness. Formalized Mathematics, 6(3):339–343, 1997.

[23] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[24] Andrzej Trybulec. Many-sorted sets. Formalized Mathematics, 4(1):15–22, 1993.

[25] Andrzej Trybulec. Moore-Smith convergence. Formalized Mathematics, 6(2):213–225, 1997.

[26] Wojciech A. Trybulec. Partially ordered sets. Formalized Mathematics, 1(2):313–319,

dickson’s lemma 37

[27] Wojciech A. Trybulec and Grzegorz Bancerek. Kuratowski - Zorn lemma. Formalized Mathematics, 1(2):387–393, 1990.

[28] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[29] Zinaida Trybulec and Halina Święczkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

[30] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.

[31] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990.

[32] Edmund Woronowicz and Anna Zalewska. Properties of binary relations. Formalized Mathematics, 1(1):85–89, 1990.

On Ordering of Bags

Gilbert Lee University of Alberta Edmonton

Piotr Rudnicki University of Alberta Edmonton

Summary. We present a Mizar formalization of chapter 4.4 of [6] devoted to special orderings in additive monoids to be used for ordering terms in multivariate polynomials. We have extended the treatment to the case of infinite number of variables. It turns out that in such case admissible orderings are not necessarily well orderings.

MML Identifier: BAGORDER.

The notation and terminology used here are introduced in the following papers: [21], [33], [18], [26], [7], [5], [11], [29], [8], [9], [1], [22], [30], [31], [2], [28], [24], [25], [20], [14], [34], [36], [35], [17], [16], [32], [27], [19], [4], [12], [23], [3], [15], [13], and [10].

1. Preliminaries

The following propositions are true:

(1) For all sets x, y, z such that z ∈ x and z ∈ y holds x \ {z} = y \ {z} iff x = y.

(2) For all natural numbers n, k holds k ∈ Segn iff k −1 is a natural number and k − 1 < n.

Let f be a natural-yielding function and let X be a set. One can verify that f↾X is natural-yielding.

Let f be a finite-support function and let X be a set. One can check that f↾X is finite-support.

Next we state three propositions:

(3) For every function f and for every set x such that x ∈ domf holds f · ⟨x⟩ = ⟨f(x)⟩.

(4) Let f, g, h be functions. Suppose domf = domg and rngf ⊆ domh and rngg ⊆ domh and f and g are fiberwise equipotent. Then h · f and h · g are fiberwise equipotent.

(5) For every finite sequence f_{1} of elements of ℕ holds ∑ f_{1} = 0 iff f_{1} = lenf_{1} ↦ 0.

Let n, i, j be natural numbers and let b be a many sorted set indexed by n. The functor ⟨b(i), …, b(j)⟩ yields a many sorted set indexed by j − ′i and is defined by:

(Def. 1) For every natural number k such that k ∈ j− ′i holds ⟨b(i), …, b(j)⟩(k) =

b(i + k). Let n, i, j be natural numbers and let b be a natural-yielding many sorted

set indexed by n. One can verify that ⟨b(i), …, b(j)⟩ is natural-yielding.

Let n, i, j be natural numbers and let b be a finite-support many sorted set indexed by n. Note that ⟨b(i), …, b(j)⟩ is finite-support.

One can prove the following proposition

(6) Let n, i be natural numbers and a, b be many sorted sets indexed by n. Then a = b if and only if the following conditions are satisfied:

(i) ⟨a(0), …, a(i + 1)⟩ = ⟨b(0), …, b(i + 1)⟩, and (ii) ⟨a(i + 1), …, a(n)⟩ = ⟨b(i + 1), …, b(n)⟩. Let x be a non empty set and let n be a non empty natural number. The

functor Fin(x, n) is defined as follows: (Def. 2) Fin(x, n) = {y; y ranges over elements of 2^{x}: y is finite ∧ y is non

empty ∧ \overline{\overline{y}} n\}. Let x be a non empty set and let n be a non empty natural number. Observe

that Fin(x, n) is non empty.

One can prove the following propositions:

(7) Let R be an antisymmetric transitive non empty relational structure and X be a finite subset of the carrier of R. Suppose X ≠ ∅. Then there exists an element x of R such that x ∈ X and x is maximal w.r.t. X, the internal relation of R.

(8) Let R be an antisymmetric transitive non empty relational structure and X be a finite subset of the carrier of R. Suppose X ≠ ∅. Then there exists an element x of R such that x ∈ X and x is minimal w.r.t. X, the internal relation of R.

(9) Let R be a non empty antisymmetric transitive relational structure and f be a sequence of R. Suppose f is descending. Let j, i be natural numbers. If i < j, then f(i) ≠ f(j) and ⟨⟨f(j), f(i)⟩⟩∈ the internal relation of R.

Let R be a non empty relational structure and let s be a sequence of R. We say that s is non-increasing if and only if:

(Def. 3) For every natural number i holds ⟨⟨s(i + 1), s(i)⟩⟩∈ the internal relation

of R. We now state three propositions:

(10) Let R be a non empty transitive relational structure and f be a sequence of R. Suppose f is non-increasing. Let j, i be natural numbers. If i < j, then ⟨⟨f(j), f(i)⟩⟩∈ the internal relation of R.

(11) Let R be a non empty transitive relational structure and s be a sequence of R. Suppose R is well founded and s is non-increasing. Then there exists a natural number p such that for every natural number r if p r, then s(p) = s(r).

(12) Let X be a set, a be an element of X, A be a finite subset of X, and R be an order in X. If A = {a} and R linearly orders A, then SgmX(R, A) = ⟨a⟩.

2. More About Bags

Let n be an ordinal number and let b be a bag of n. The functor TotDegreeb yielding a natural number is defined by:

(Def. 4) There exists a finite sequence f of elements of ℕ such that TotDegreeb =

∑ f and f = b · SgmX(^{⊆} _{n}, supportb). The following propositions are true:

(13) Let n be an ordinal number, b be a bag of n, s be a finite subset of n, and f, g be finite sequences of elements of ℕ. If f = b · SgmX(^{⊆} _{n}, supportb) and g = b · SgmX(^{⊆} _{n}, supportb ∪ s), then ∑ f = ∑ g.

(14) For every ordinal number n and for all bags a, b of n holds TotDegree(a+ b) = TotDegreea + TotDegreeb.

(15) For every ordinal number n and for all bags a, b of n such that b | a holds TotDegree(a − ′b) = TotDegreea − TotDegreeb.

(16) For every ordinal number n and for every bag b of n holds TotDegreeb = 0 iff b = EmptyBagn.

(17) For all natural numbers i, j, n holds ⟨(EmptyBagn)(i), …, (EmptyBagn) (j)⟩ = EmptyBag(j − ′i).

(18) For all natural numbers i, j, n and for all bags a, b of n holds ⟨(a + b)(i), …, (a + b)(j)⟩ = ⟨a(i), …, a(j)⟩ + ⟨b(i), …, b(j)⟩.

(19) For every set X holds supportEmptyBagX = ∅.

(20) For every set X and for every bag b of X such that supportb = ∅ holds b = EmptyBagX.

(21) For all ordinal numbers n, m and for every bag b of n such that m ∈ n holds b↾m is a bag of m.

(22) For every ordinal number n and for all bags a, b of n such that b | a holds supportb ⊆ supporta.

3. Some Special Orders

Let n be an ordinal number and let o be an order in Bagsn. We say that o is admissible if and only if the conditions (Def. 5) are satisfied.

(Def. 5)(i) o is strongly connected in Bagsn, (ii) for every bag a of n holds ⟨⟨EmptyBagn, a⟩⟩∈ o, and (iii) for all bags a, b, c of n such that ⟨⟨a, b⟩⟩∈ o holds ⟨⟨a + c, b + c⟩⟩∈ o. Let n be an ordinal number. We introduce LexOrdern as a synonym of

BagOrdern.

One can prove the following propositions:

(23) For every ordinal number n holds LexOrdern is admissible.

(24) For every infinite ordinal number o holds LexOrdero is non well-ordering. Let n be an ordinal number. The functor InvLexOrdern yields an order in

Bagsn and is defined by the condition (Def. 6). (Def. 6) Let p, q be bags of n. Then ⟨⟨p, q⟩⟩∈ InvLexOrdern if and only if one of

the following conditions is satisfied:

(i) p = q, or (ii) there exists an ordinal number i such that i ∈ n and p(i) < q(i) and

for every ordinal number k such that i ∈ k and k ∈ n holds p(k) = q(k). The following propositions are true:

(25) For every ordinal number n holds InvLexOrdern is admissible.

(26) For every ordinal number o holds InvLexOrdero is well-ordering. Let n be an ordinal number and let o be an order in Bagsn. Let us assume

that for all bags a, b, c of n such that ⟨⟨a, b⟩⟩ ∈ o holds ⟨⟨a + c, b + c⟩⟩ ∈ o. The functor Gradedo yields an order in Bagsn and is defined by:

(Def. 7) For all bags a, b of n holds ⟨⟨a, b⟩⟩ ∈ Gradedo iff TotDegreea <

TotDegreeb or TotDegreea = TotDegreeb and ⟨⟨a, b⟩⟩∈ o. The following proposition is true

(27) Let n be an ordinal number and o be an order in Bagsn. Suppose for all bags a, b, c of n such that ⟨⟨a, b⟩⟩ ∈ o holds ⟨⟨a + c, b + c⟩⟩ ∈ o and o is strongly connected in Bagsn. Then Gradedo is admissible.

Let n be an ordinal number. The functor GrLexOrdern yielding an order in Bagsn is defined as follows:

(Def. 8) GrLexOrdern = GradedLexOrdern.

The functor GrInvLexOrdern yielding an order in Bagsn is defined by: (Def. 9) GrInvLexOrdern = GradedInvLexOrdern.

Next we state four propositions:

(28) For every ordinal number n holds GrLexOrdern is admissible.

(29) For every infinite ordinal number o holds GrLexOrdero is non wellordering.

(30) For every ordinal number n holds GrInvLexOrdern is admissible.

(31) For every ordinal number o holds GrInvLexOrdero is well-ordering. Let i, n be natural numbers, let o_{1} be an order in Bags(i + 1), and let o_{2} be

an order in Bags(n − ′(i + 1)). The functor BlockOrder(i, n, o_{1}, o_{2}) yielding an order in Bagsn is defined by the condition (Def. 10).

(Def. 10) Let p, q be bags of n. Then ⟨⟨p, q⟩⟩ ∈ BlockOrder(i, n, o_{1}, o_{2}) if and only

if one of the following conditions is satisfied:

(i) ⟨p(0), …, p(i + 1)⟩ ≠ ⟨q(0), …, q(i + 1)⟩ and ⟨⟨⟨p(0), …, p(i + 1)⟩, ⟨q(0), …, q(i + 1)⟩⟩⟩∈ o_{1}, or

(ii) ⟨p(0), …, p(i+1)⟩ = ⟨q(0), …, q(i+1)⟩ and ⟨⟨⟨p(i+1), …, p(n)⟩, ⟨q(i+

1), …, q(n)⟩⟩⟩∈ o_{2}. The following proposition is true

(32) Let i, n be natural numbers, o_{1} be an order in Bags(i + 1), and o_{2} be an order in Bags(n − ′(i + 1)). If o_{1} is admissible and o_{2} is admissible, then BlockOrder(i, n, o_{1}, o_{2}) is admissible.

Let n be a natural number. The functor NaivelyOrderedBagsn yielding a strict relational structure is defined by the conditions (Def. 11).

(Def. 11)(i) The carrier of NaivelyOrderedBagsn = Bagsn, and

(ii) for all bags x, y of n holds ⟨⟨x, y⟩⟩ ∈ the internal relation of

NaivelyOrderedBagsn iff x | y. The following propositions are true:

(33) For every natural number n holds the carrier of ∏(n ⟼→ OrderedNAT) = Bagsn.

(34) For every natural number n holds NaivelyOrderedBagsn = ∏(n ⟼→ OrderedNAT).

(35) Let n be a natural number and o be an order in Bagsn. Suppose o is admissible. Then the internal relation of NaivelyOrderedBagsn ⊆ o and o is well-ordering.

4. Ordering of Finite Subsets

Let R be a connected non empty poset and let X be an element of Fin(the carrier of R). Let us assume that X is non empty. The functor PosetMinX yielding an element of R is defined as follows:

(Def. 12) PosetMinX ∈ X and PosetMinX is minimal w.r.t. X, the internal re-

lation of R. The functor PosetMaxX yields an element of R and is defined as follows:

(Def. 13) PosetMaxX ∈ X and PosetMaxX is maximal w.r.t. X, the internal

relation of R. Let R be a connected non empty poset. The functor FinOrd-ApproxR yiel-

ding a function from ℕ into 2^{[: Fin (the carrier of R), Fin (the carrier of R) :]} is defined by the conditions (Def. 14).

(Def. 14)(i) domFinOrd-ApproxR = ℕ,

(ii) (FinOrd-ApproxR)(0) = {⟨⟨x, y⟩⟩; x ranges over elements of Fin(the carrier of R), y ranges over elements of Fin(the carrier of R): x = ∅ ∨ x ≠ ∅ ∧ y ≠ ∅ ∧ PosetMaxx ≠ PosetMaxy ∧ ⟨⟨PosetMaxx, PosetMaxy⟩⟩∈ the internal relation of R}, and

(iii) for every element n of ℕ holds (FinOrd-ApproxR)(n + 1) = {⟨⟨x, y⟩⟩; x ranges over elements of Fin(the carrier of R), y ranges over elements of Fin(the carrier of R): x ≠ ∅ ∧ y ≠ ∅ ∧ PosetMaxx = PosetMaxy ∧ ⟨⟨x \ {PosetMaxx}, y \ {PosetMaxy}⟩⟩∈ (FinOrd-ApproxR)(n)}.

One can prove the following propositions:

(36) Let R be a connected non empty poset and x, y be elements of Fin(the carrier of R). Then ⟨⟨x, y⟩⟩∈ ⋃ rngFinOrd-ApproxR if and only if one of the following conditions is satisfied:

(i) x = ∅, or (ii) x ≠ ∅ and y ≠ ∅ and PosetMaxx ≠ PosetMaxy and ⟨⟨PosetMaxx,

PosetMaxy⟩⟩∈ the internal relation of R, or (iii) x ≠ ∅ and y ≠ ∅ and PosetMaxx = PosetMaxy and ⟨⟨x\{PosetMaxx},

y \ {PosetMaxy}⟩⟩∈ ⋃ rngFinOrd-ApproxR.

(37) For every connected non empty poset R and for every element x of Fin(the carrier of R) such that x ≠ ∅ holds ⟨⟨x, ∅⟩⟩ ∉ ⋃ rngFinOrd-ApproxR.

(38) Let R be a connected non empty poset and a be an element of Fin(the carrier of R). Then a \ {PosetMaxa} is an element of Fin(the carrier of R).

(39) For every connected non empty poset R holds ⋃ rngFinOrd-ApproxR

is an order in Fin(the carrier of R). Let R be a connected non empty poset. The functor FinOrdR yields an

order in Fin(the carrier of R) and is defined as follows: (Def. 15) FinOrdR = ⋃ rngFinOrd-ApproxR.

Let R be a connected non empty poset. The functor FinPosetR yields a poset and is defined by:

(Def. 16) FinPosetR = ⟨Fin(the carrier of R), FinOrdR⟩.

Let R be a connected non empty poset. One can check that FinPosetR is non empty.

The following proposition is true

(40) Let R be a connected non empty poset and a, b be elements of FinPosetR. Then ⟨⟨a, b⟩⟩ ∈ the internal relation of FinPosetR if and only if there exist elements x, y of Fin(the carrier of R) such that a = x but b = y but x = ∅ or x ≠ ∅ and y ≠ ∅ and PosetMaxx ≠ PosetMaxy and ⟨⟨PosetMaxx, PosetMaxy⟩⟩ ∈ the internal relation of R or x ≠ ∅ and y ≠ ∅ and PosetMaxx = PosetMaxy and ⟨⟨x \ {PosetMaxx}, y \ {PosetMaxy}⟩⟩∈ FinOrdR.

Let R be a connected non empty poset. One can verify that FinPosetR is connected.

Let R be a connected non empty relational structure and let C be a non empty set. Let us assume that R is well founded and C ⊆ the carrier of R. The functor MinElement(C, R) yields an element of R and is defined by:

(Def. 17) MinElement(C, R) ∈ C and MinElement(C, R) is minimal w.r.t. C, the

internal relation of R. Let R be a non empty relational structure, let s be a sequence of R, and let

j be a natural number. The functor SeqShift(s, j) yields a sequence of R and is defined by:

(Def. 18) For every natural number i holds (SeqShift(s, j))(i) = s(i + j).

One can prove the following propositions:

(41) Let R be a non empty relational structure, s be a sequence of R, and j be a natural number. If s is descending, then SeqShift(s, j) is descending.

(42) For every connected non empty poset R such that R is well founded holds FinPosetR is well founded.

References

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[2] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990.

[3] Grzegorz Bancerek. The well ordering relations. Formalized Mathematics, 1(1):123–129, 1990.

[4] Grzegorz Bancerek. Directed sets, nets, ideals, filters, and maps. Formalized Mathematics, 6(1):93–107, 1997.

[5] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

[6] Thomas Becker and Volker Weispfenning. Gröbner bases: A Computational Approach to Commutative Algebra. Springer-Verlag, New York, Berlin, 1993.

[7] Czesław Byliński. Binary operations applied to finite sequences. Formalized Mathematics, 1(4):643–649, 1990.

[8] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

[9] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164,

46 gilbert lee and piotr rudnicki

[10] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.

[11] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990.

[12] Adam Grabowski. Auxiliary and approximating relations. Formalized Mathematics, 6(2):179–188, 1997.

[13] Adam Grabowski and Robert Milewski. Boolean posets, posets under inclusion and products of relational structures. Formalized Mathematics, 6(1):117–121, 1997.

[14] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[15] Andrzej Kondracki. The Chinese Remainder Theorem. Formalized Mathematics, 6(4):573–577, 1997.

[16] Jarosław Kotowicz. Monotone real sequences. Subsequences. Formalized Mathematics, 1(3):471–475, 1990.

[17] Jarosław Kotowicz. Functions and finite sequences of real numbers. Formalized Mathematics, 3(2):275–278, 1992.

[18] Gilbert Lee and Piotr Rudnicki. Dickson’s lemma. Formalized Mathematics, 10(1):29–37, 2002.

[19] Beata Madras. On the concept of the triangulation. Formalized Mathematics, 5(3):457– 462, 1996.

[20] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, I. Formalized Mathematics, 5(2):167–172, 1996.

[21] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Formalized Mathematics, 4(1):83–86, 1993.

[22] Jan Popiołek. Real normed space. Formalized Mathematics, 2(1):111–115, 1991.

[23] Piotr Rudnicki and Andrzej Trybulec. On same equivalents of well-foundedness. Formalized Mathematics, 6(3):339–343, 1997.

[24] Piotr Rudnicki and Andrzej Trybulec. Multivariate polynomials with arbitrary number of variables. Formalized Mathematics, 9(1):95–110, 2001.

[25] Christoph Schwarzweller and Andrzej Trybulec. The evaluation of multivariate polynomials. Formalized Mathematics, 9(2):331–338, 2001.

[26] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 1990.

[27] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[28] Andrzej Trybulec. Many-sorted sets. Formalized Mathematics, 4(1):15–22, 1993.

[29] Andrzej Trybulec and Agata Darmochwał. Boolean domains. Formalized Mathematics, 1(1):187–190, 1990.

[30] Wojciech A. Trybulec. Partially ordered sets. Formalized Mathematics, 1(2):313–319, 1990.

[31] Wojciech A. Trybulec and Grzegorz Bancerek. Kuratowski - Zorn lemma. Formalized Mathematics, 1(2):387–393, 1990.

[32] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[33] Zinaida Trybulec and Halina Święczkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

[34] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.

[35] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990.

[36] Edmund Woronowicz and Anna Zalewska. Properties of binary relations. Formalized Mathematics, 1(1):85–89, 1990.

Combining of Multi Cell Circuits

Grzegorz Bancerek Białystok Technical University Shin’nosuke Yamaguchi Shinshu University Nagano

Yasunari Shidama Shinshu University Nagano

Summary. In this article we continue the investigations from [11] and [3] of verification of a circuit design. We concentrate on the combination of multi cell circuits from given cells (circuit modules). Namely, we formalize a design of

the form 0  1  2  n

and prove its stability. The formalization proposed consists in a series of schemes which allow to define multi cells circuits and prove their properties. Our goal is to achive mathematical formalization which will allow to verify designs of real circuits.

MML Identifier: CIRCCMB2.

The articles [18], [2], [11], [12], [13], [3], [4], [9], [5], [6], [7], [10], [14], [16], [1], [8], [19], [20], [17], and [15] provide the terminology and notation for this paper.

1. One Gate Circuits

Let n be a natural number, let f be a function from Boolean^{n} into Boolean, and let p be a finite sequence with length n. One can verify that 1GateCircuit(p, f) is Boolean.

The following four propositions are true:

(1) Let X be a finite non empty set, n be a natural number, p be a finite sequence with length n, f be a function from X^{n} into X, o be an operation symbol of 1GateCircStr(p, f), and s be a state of 1GateCircuit(p, f). Then o depends-on-ins = s · p.

(2) Let X be a finite non empty set, n be a natural number, p be a finite sequence with length n, f be a function from X^{n} into X, and s be a state of 1GateCircuit(p, f). Then Following(s) is stable.

(3) Let S be a non void circuit-like non empty many sorted signature, A be a non-empty circuit of S, and s be a state of A. If s is stable, then for every natural number n holds Following(s, n) = s.

(4) Let S be a non void circuit-like non empty many sorted signature, A be a non-empty circuit of S, s be a state of A, and n_{1}, n_{2} be natural numbers. If Following(s, n_{1}) is stable and n_{1} n_{2}, then Following(s, n_{2}) = Following(s, n_{1}).

2. Defining Multi Cell Circuit Structures

In this article we present several logical schemes. The scheme CIRCCMB2’sch 1 deals with a non empty many sorted signature A, a set B, a ternary functor F yielding a non empty many sorted signature, and a binary functor G yielding a set, and states that:

There exist many sorted sets f, h indexed by ℕ such that

(i) f(0) = A, (ii) h(0) = B, and (iii) for every natural number n and for every non empty many sorted signature S and for every set x such that S = f(n) and x = h(n) holds f(n + 1) = F(S, x, n) and h(n + 1) = G(x, n)

for all values of the parameters.

The scheme CIRCCMB2’sch 2 deals with a ternary functor F yielding a non empty many sorted signature, a binary functor G yielding a set, many sorted sets A, B indexed by ℕ, and a ternary predicate P, and states that:

For every natural number n there exists a non empty many sorted signature S such that S = A(n) and P[S, B(n), n]

provided the parameters meet the following requirements:

• There exists a non empty many sorted signature S and there exists a set x such that S = A(0) and x = B(0) and P[S, x, 0],

• Let n be a natural number, S be a non empty many sorted signature, and x be a set. If S = A(n) and x = B(n), then A(n + 1) = F(S, x, n) and B(n + 1) = G(x, n), and

• Let n be a natural number, S be a non empty many sorted signature, and x be a set. If S = A(n) and x = B(n) and P[S, x, n], then P[F(S, x, n), G(x, n), n + 1].

The scheme CIRCCMB2’sch 3 deals with a non empty many sorted signature A, a ternary functor F yielding a non empty many sorted signature, a binary functor G yielding a set, and many sorted sets B, C indexed by ℕ, and states that:

For every natural number n and for every set x such that x = C(n) holds C(n + 1) = G(x, n)

provided the following requirements are met:

• B(0) = A, and

• Let n be a natural number, S be a non empty many sorted signature, and x be a set. If S = B(n) and x = C(n), then B(n + 1) = F(S, x, n) and C(n + 1) = G(x, n).

The scheme CIRCCMB2’sch 4 deals with a non empty many sorted signature A, a set B, a ternary functor F yielding a non empty many sorted signature, a binary functor G yielding a set, and a natural number C, and states that:

There exists a non empty many sorted signature S and there exist many sorted sets f, h indexed by ℕ such that

(i) S = f(C), (ii) f(0) = A, (iii) h(0) = B, and (iv) for every natural number n and for every non empty many sorted signature S and for every set x such that S = f(n) and x = h(n) holds f(n + 1) = F(S, x, n) and h(n + 1) = G(x, n)

for all values of the parameters.

The scheme CIRCCMB2’sch 5 deals with a non empty many sorted signature A, a set B, a ternary functor F yielding a non empty many sorted signature, a binary functor G yielding a set, and a natural number C, and states that:

Let S_{1}, S_{2} be non empty many sorted signatures. Suppose that

(i) there exist many sorted sets f, h indexed by ℕ such that S_{1} = f(C) and f(0) = A and h(0) = B and for every natural number n and for every non empty many sorted signature S and for every set x such that S = f(n) and x = h(n) holds f(n + 1) = F(S, x, n) and h(n + 1) = G(x, n), and (ii) there exist many sorted sets f, h indexed by ℕ such that S_{2} = f(C) and f(0) = A and h(0) = B and for every natural number n and for every non empty many sorted signature S and for every set x such that S = f(n) and x = h(n) holds f(n + 1) = F(S, x, n) and h(n + 1) = G(x, n).

Then S_{1} = S_{2}

for all values of the parameters.

The scheme CIRCCMB2’sch 6 deals with a non empty many sorted signature A, a set B, a ternary functor F yielding a non empty many sorted signature, a binary functor G yielding a set, and a natural number C, and states that:

(i) There exists a non empty many sorted signature S and there exist many sorted sets f, h indexed by ℕ such that S = f(C) and f(0) = A and h(0) = B and for every natural number n and for every non empty many sorted signature S and for every set x such that S = f(n) and x = h(n) holds f(n + 1) = F(S, x, n) and h(n + 1) = G(x, n), and (ii) for all non empty many sorted signatures S_{1}, S_{2} such that there exist many sorted sets f, h indexed by ℕ such that S_{1} = f(C) and f(0) = A and h(0) = B and for every natural number n and for every non empty many sorted signature S and for every set x such that S = f(n) and x = h(n) holds f(n + 1) = F(S, x, n) and h(n + 1) = G(x, n) and there exist many sorted sets f, h indexed by ℕ such that S_{2} = f(C) and f(0) = A and h(0) = B and for every natural number n and for every non empty many sorted signature S and for every set x such that S = f(n) and x = h(n) holds f(n + 1) = F(S, x, n) and h(n + 1) = G(x, n) holds S_{1} = S_{2}

for all values of the parameters.

The scheme CIRCCMB2’sch 7 deals with a non empty many sorted signature A, a ternary functor F yielding a non empty many sorted signature, a set B, a binary functor G yielding a set, and a natural number C, and states that:

There exists an unsplit non void non empty non empty strict many sorted signature S with arity held in gates and Boolean denotation held in gates and there exist many sorted sets f, h indexed by ℕ such that

(i) S = f(C), (ii) f(0) = A, (iii) h(0) = B, and (iv) for every natural number n and for every non empty many sorted signature S and for every set x such that S = f(n) and x = h(n) holds f(n + 1) = F(S, x, n) and h(n + 1) = G(x, n)

provided the parameters meet the following requirements:

• A is unsplit, non void, non empty, and strict and has arity held in gates and Boolean denotation held in gates, and • Let S be an unsplit non void strict non empty many sorted si-

gnature with arity held in gates and Boolean denotation held in gates, x be a set, and n be a natural number. Then F(S, x, n) is unsplit, non void, non empty, and strict and has arity held in gates and Boolean denotation held in gates.

The scheme CIRCCMB2’sch 8 deals with a non empty many sorted signature A, a binary functor F yielding an unsplit non void non empty many sorted signature with arity held in gates and Boolean denotation held in gates, a set B, a binary functor G yielding a set, and a natural number C, and states that:

There exists an unsplit non void non empty non empty strict many sorted signature S with arity held in gates and Boolean denotation held in gates and there exist many sorted sets f, h indexed by ℕ such that

(i) S = f(C), (ii) f(0) = A, (iii) h(0) = B, and (iv) for every natural number n and for every non empty many sorted signature S and for every set x such that S = f(n) and x = h(n) holds f(n + 1) = S+·F(x, n) and h(n + 1) = G(x, n)

provided the parameters meet the following requirement:

• A is unsplit, non void, non empty, and strict and has arity held in gates and Boolean denotation held in gates.

The scheme CIRCCMB2’sch 9 deals with a non empty many sorted signature A, a set B, a ternary functor F yielding a non empty many sorted signature, a binary functor G yielding a set, and a natural number C, and states that:

Let S_{1}, S_{2} be unsplit non void non empty strict non empty many sorted signatures with arity held in gates and Boolean denotation held in gates. Suppose that

(i) there exist many sorted sets f, h indexed by ℕ such that S_{1} = f(C) and f(0) = A and h(0) = B and for every natural number n and for every non empty many sorted signature S and for every set x such that S = f(n) and x = h(n) holds f(n + 1) = F(S, x, n) and h(n + 1) = G(x, n), and (ii) there exist many sorted sets f, h indexed by ℕ such that S_{2} = f(C) and f(0) = A and h(0) = B and for every natural number n and for every non empty many sorted signature S and for every set x such that S = f(n) and x = h(n) holds f(n + 1) = F(S, x, n) and h(n + 1) = G(x, n).

Then S_{1} = S_{2}

for all values of the parameters.

3. Input of Multi Cell Circuit

We now state several propositions:

(5) For all functions f, g such that f ≈ g holds rng(f+·g) = rngf ∪ rngg.

(6) For all non empty many sorted signatures S_{1}, S_{2} such that S_{1} ≈ S_{2} holds InputVertices(S_{1}+·S_{2}) = (InputVertices(S_{1}) \ InnerVertices(S_{2})) ∪ (InputVertices(S_{2}) \ InnerVertices(S_{1})).

(7) For every set X with no pairs and for every binary relation Y holds X \ Y = X.

(8) For every binary relation X and for all sets Y, Z such that Z ⊆ Y and Y \ Z has no pairs holds X \ Y = X \ Z.

(9) For all sets X, Z and for every binary relation Y such that Z ⊆ Y and X \ Z has no pairs holds X \ Y = X \ Z.

Now we present two schemes. The scheme CIRCCMB2’sch 10 deals with an unsplit non void non empty many sorted signature A with arity held in gates and Boolean denotation held in gates, a unary functor F yielding a set, a many sorted set B indexed by ℕ, a binary functor G yielding an unsplit non void non empty many sorted signature with arity held in gates and Boolean denotation held in gates, and a binary functor H yielding a set, and states that:

Let n be a natural number. Then there exist unsplit non void non empty many sorted signatures S_{1}, S_{2} with arity held in gates and Boolean denotation held in gates such that S_{1} = F(n) and S_{2} = F(n + 1) and InputVertices(S_{2}) = InputVertices(S_{1}) ∪ (InputVertices(G(B(n), n)) \ {B(n)}) and InnerVertices(S_{1}) is a binary relation and InputVertices(S_{1}) has no pairs

provided the following requirements are met:

• InnerVertices(A) is a binary relation,

• InputVertices(A) has no pairs,

• F(0) = A and B(0) ∈ InnerVertices(A),

• For every natural number n and for every set x holds InnerVertices(G(x, n)) is a binary relation,

• For every natural number n and for every set x such that x = B(n) holds InputVertices(G(x, n)) \ {x} has no pairs, and

• Let n be a natural number, S be a non empty many sorted signature, and x be a set. Suppose S = F(n) and x = B(n). Then F(n + 1) = S+·G(x, n) and B(n + 1) = H(x, n) and x ∈ InputVertices(G(x, n)) and H(x, n) ∈ InnerVertices(G(x, n)).

The scheme CIRCCMB2’sch 11 deals with a unary functor F yielding an unsplit non void non empty many sorted signature with arity held in gates and Boolean denotation held in gates, a many sorted set A indexed by ℕ, a binary functor G yielding an unsplit non void non empty many sorted signature with arity held in gates and Boolean denotation held in gates, and a binary functor H yielding a set, and states that:

For every natural number n holds InputVertices(F(n + 1)) = InputVertices(F(n)) ∪ (InputVertices(G(A(n), n)) \ {A(n)}) and InnerVertices(F(n)) is a binary relation and InputVertices(F(n)) has no pairs

provided the parameters meet the following requirements:

• InnerVertices(F(0)) is a binary relation,

• InputVertices(F(0)) has no pairs,

• A(0) ∈ InnerVertices(F(0)),

• For every natural number n and for every set x holds InnerVertices(G(x, n)) is a binary relation,

• For every natural number n and for every set x such that x = A(n) holds InputVertices(G(x, n)) \ {x} has no pairs, and

• Let n be a natural number, S be a non empty many sorted signature, and x be a set. Suppose S = F(n) and x = A(n). Then F(n + 1) = S+·G(x, n) and A(n + 1) = H(x, n) and x ∈ InputVertices(G(x, n)) and H(x, n) ∈ InnerVertices(G(x, n)).

4. Defining Multi Cell Circuits

Now we present several schemes. The scheme CIRCCMB2’sch 12 deals with a non empty many sorted signature A, a non-empty algebra B over A, a set C, a ternary functor F yielding a non empty many sorted signature, a 4-ary functor G yielding a set, and a binary functor H yielding a set, and states that:

There exist many sorted sets f, g, h indexed by ℕ such that

(i) f(0) = A, (ii) g(0) = B, (iii) h(0) = C, and (iv) for every natural number n and for every non empty many sorted signature S and for every non-empty algebra A over S and for every set x such that S = f(n) and A = g(n) and x = h(n) holds f(n + 1) = F(S, x, n) and g(n + 1) = G(S, A, x, n) and h(n + 1) = H(x, n)

for all values of the parameters.

The scheme CIRCCMB2’sch 13 deals with a ternary functor F yielding a non empty many sorted signature, a 4-ary functor G yielding a set, a binary functor H yielding a set, many sorted sets A, B, C indexed by ℕ, and a 4-ary predicate P, and states that:

Let n be a natural number. Then there exists a non empty many sorted signature S and there exists a non-empty algebra A over S such that S = A(n) and A = B(n) and P[S, A, C(n), n] provided the following conditions are satisfied:

• There exists a non empty many sorted signature S and there exists a non-empty algebra A over S and there exists a set x such that S = A(0) and A = B(0) and x = C(0) and P[S, A, x, 0],

• Let n be a natural number, S be a non empty many sorted signature, A be a non-empty algebra over S, and x be a set. Suppose S = A(n) and A = B(n) and x = C(n). Then A(n + 1) = F(S, x, n) and B(n + 1) = G(S, A, x, n) and C(n + 1) = H(x, n),

• Let n be a natural number, S be a non empty many sorted signature, A be a non-empty algebra over S, and x be a set. If S = A(n) and A = B(n) and x = C(n) and P[S, A, x, n], then P[F(S, x, n), G(S, A, x, n), H(x, n), n + 1], and

• Let S be a non empty many sorted signature, A be a non-empty algebra over S, x be a set, and n be a natural number. Then G(S, A, x, n) is a non-empty algebra over F(S, x, n).

The scheme CIRCCMB2’sch 14 deals with a ternary functor F yielding a non empty many sorted signature, a 4-ary functor G yielding a set, a binary functor H yielding a set, and many sorted sets A, B, C, D, E, F indexed by ℕ, and states that:

A = B and C = D and E = F provided the parameters meet the following conditions:

• There exists a non empty many sorted signature S and there exists a non-empty algebra A over S such that S = A(0) and A = C(0),

• A(0) = B(0) and C(0) = D(0) and E(0) = F(0),

• Let n be a natural number, S be a non empty many sorted signature, A be a non-empty algebra over S, and x be a set. Suppose S = A(n) and A = C(n) and x = E(n). Then A(n+1) = F(S, x, n) and C(n + 1) = G(S, A, x, n) and E(n + 1) = H(x, n),

• Let n be a natural number, S be a non empty many sorted signature, A be a non-empty algebra over S, and x be a set. Suppose S = B(n) and A = D(n) and x = F(n). Then B(n + 1) = F(S, x, n) and D(n + 1) = G(S, A, x, n) and F(n + 1) = H(x, n), and

• Let S be a non empty many sorted signature, A be a non-empty algebra over S, x be a set, and n be a natural number. Then G(S, A, x, n) is a non-empty algebra over F(S, x, n).

The scheme CIRCCMB2’sch 15 deals with a non empty many sorted signature A, a non-empty algebra B over A, a ternary functor F yielding a non empty many sorted signature, a 4-ary functor G yielding a set, a binary functor H yielding a set, and many sorted sets C, D, E indexed by ℕ, and states that:

Let n be a natural number, S be a non empty many sorted signature, and x be a set. If S = C(n) and x = E(n), then

C(n + 1) = F(S, x, n) and E(n + 1) = H(x, n) provided the parameters meet the following conditions:

• C(0) = A and D(0) = B,

• Let n be a natural number, S be a non empty many sorted signature, A be a non-empty algebra over S, and x be a set. Suppose S = C(n) and A = D(n) and x = E(n). Then C(n+1) = F(S, x, n) and D(n + 1) = G(S, A, x, n) and E(n + 1) = H(x, n), and

• Let S be a non empty many sorted signature, A be a non-empty algebra over S, x be a set, and n be a natural number. Then G(S, A, x, n) is a non-empty algebra over F(S, x, n).

The scheme CIRCCMB2’sch 16 deals with a non empty many sorted signature A, a non-empty algebra B over A, a set C, a ternary functor F yielding a non empty many sorted signature, a 4-ary functor G yielding a set, a binary functor H yielding a set, and a natural number D, and states that:

There exists a non empty many sorted signature S and there exists a non-empty algebra A over S and there exist many sorted sets f, g, h indexed by ℕ such that

(i) S = f(D), (ii) A = g(D), (iii) f(0) = A, (iv) g(0) = B,

(v) h(0) = C, and (vi) for every natural number n and for every non empty many sorted signature S and for every non-empty algebra A over S and for every set x such that S = f(n) and A = g(n) and x = h(n) holds f(n + 1) = F(S, x, n) and g(n + 1) = G(S, A, x, n) and h(n + 1) = H(x, n)

provided the following condition is satisfied:

• Let S be a non empty many sorted signature, A be a non-empty algebra over S, x be a set, and n be a natural number. Then G(S, A, x, n) is a non-empty algebra over F(S, x, n).

The scheme CIRCCMB2’sch 17 deals with non empty many sorted signatures A, B, a non-empty algebra C over A, a set D, a ternary functor F yielding a non empty many sorted signature, a 4-ary functor G yielding a set, a binary functor H yielding a set, and a natural number E, and states that:

There exists a non-empty algebra A over B and there exist many sorted sets f, g, h indexed by ℕ such that

(i) B = f(E), (ii) A = g(E), (iii) f(0) = A, (iv) g(0) = C,

(v) h(0) = D, and (vi) for every natural number n and for every non empty many sorted signature S and for every non-empty algebra A over S and for every set x such that S = f(n) and A = g(n) and x = h(n) holds f(n + 1) = F(S, x, n) and g(n + 1) = G(S, A, x, n) and h(n + 1) = H(x, n)

provided the parameters meet the following requirements:

• There exist many sorted sets f, h indexed by ℕ such that (i) B = f(E), (ii) f(0) = A, (iii) h(0) = D, and (iv) for every natural number n and for every non empty many sorted signature S and for every set x such that S = f(n) and x = h(n) holds f(n + 1) = F(S, x, n) and h(n + 1) = H(x, n),

and

• Let S be a non empty many sorted signature, A be a non-empty algebra over S, x be a set, and n be a natural number. Then G(S, A, x, n) is a non-empty algebra over F(S, x, n).

The scheme CIRCCMB2’sch 18 deals with non empty many sorted signatures A, B, a non-empty algebra C over A, a set D, a ternary functor F yielding a non empty many sorted signature, a 4-ary functor G yielding a set, a binary functor H yielding a set, and a natural number E, and states that:

Let A_{1}, A_{2} be non-empty algebras over B. Suppose that

(i) there exist many sorted sets f, g, h indexed by ℕ such that B = f(E) and A_{1} = g(E) and f(0) = A and g(0) = C and h(0) = D and for every natural number n and for every non empty many sorted signature S and for every non-empty algebra A over S and for every set x such that S = f(n) and A = g(n) and x = h(n) holds f(n + 1) = F(S, x, n) and g(n + 1) = G(S, A, x, n) and h(n + 1) = H(x, n), and (ii) there exist many sorted sets f, g, h indexed by ℕ such that B = f(E) and A_{2} = g(E) and f(0) = A and g(0) = C and h(0) = D and for every natural number n and for every non empty many sorted signature S and for every non-empty algebra A over S and for every set x such that S = f(n) and A = g(n) and x = h(n) holds f(n + 1) = F(S, x, n) and g(n + 1) = G(S, A, x, n) and h(n + 1) = H(x, n).

Then A_{1} = A_{2}

provided the parameters meet the following condition:

• Let S be a non empty many sorted signature, A be a non-empty algebra over S, x be a set, and n be a natural number. Then G(S, A, x, n) is a non-empty algebra over F(S, x, n).

The scheme CIRCCMB2’sch 19 deals with unsplit non void strict non empty many sorted signatures A, B with arity held in gates and Boolean denotation held in gates, a Boolean strict circuit C of A with denotation held in gates, a ternary functor F yielding a non empty many sorted signature, a 4-ary functor G yielding a set, a set D, a binary functor H yielding a set, and a natural number E, and states that:

There exists a Boolean strict circuit A of B with denotation held in gates and there exist many sorted sets f, g, h indexed by ℕ such that

(i) B = f(E), (ii) A = g(E), (iii) f(0) = A, (iv) g(0) = C,

(v) h(0) = D, and (vi) for every natural number n and for every non empty many sorted signature S and for every non-empty algebra A over S and for every set x such that S = f(n) and A = g(n) and x = h(n) holds f(n + 1) = F(S, x, n) and g(n + 1) = G(S, A, x, n) and h(n + 1) = H(x, n)

provided the following conditions are satisfied:

• Let S be an unsplit non void strict non empty many sorted signature with arity held in gates and Boolean denotation held in gates, x be a set, and n be a natural number. Then F(S, x, n) is unsplit, non void, and strict and has arity held in gates and Boolean denotation held in gates,

• There exist many sorted sets f, h indexed by ℕ such that (i) B = f(E), (ii) f(0) = A, (iii) h(0) = D, and (iv) for every natural number n and for every non empty many sorted signature S and for every set x such that S = f(n) and x = h(n) holds f(n + 1) = F(S, x, n) and h(n + 1) = H(x, n),

• Let S be a non empty many sorted signature, A be a non-empty algebra over S, x be a set, and n be a natural number. Then G(S, A, x, n) is a non-empty algebra over F(S, x, n), and

• Let S, S_{1} be unsplit non void strict non empty many sorted signatures with arity held in gates and Boolean denotation held in gates, A be a Boolean strict circuit of S with denotation held in gates, x be a set, and n be a natural number. Suppose S_{1} = F(S, x, n). Then G(S, A, x, n) is a Boolean strict circuit of S_{1} with denotation held in gates.

Let S be a non empty many sorted signature and let A be a set. Let us assume that A is a non-empty algebra over S. The functor MSAlg(A, S) yielding

a non-empty algebra over S is defined as follows:

(Def. 1) MSAlg(A, S) = A.

Now we present two schemes. The scheme CIRCCMB2’sch 20 deals with unsplit non void strict non empty many sorted signatures A, B with arity held in gates and Boolean denotation held in gates, a Boolean strict circuit C of A with denotation held in gates, a binary functor F yielding an unsplit non void non empty many sorted signature with arity held in gates and Boolean denotation held in gates, a binary functor G yielding a set, a set D, a binary functor H yielding a set, and a natural number E, and states that:

There exists a Boolean strict circuit A of B with denotation held in gates and there exist many sorted sets f, g, h indexed by ℕ such that

(i) B = f(E), (ii) A = g(E), (iii) f(0) = A, (iv) g(0) = C,

(v) h(0) = D, and (vi) for every natural number n and for every non empty many sorted signature S and for every non-empty algebra A_{1} over S and for every set x and for every non-empty algebra A_{2} over F(x, n) such that S = f(n) and A_{1} = g(n) and x = h(n) and A_{2} = G(x, n) holds f(n+1) = S+·F(x, n) and g(n+1) = A_{1}+·A_{2} and h(n + 1) = H(x, n)

provided the parameters meet the following requirements:

• There exist many sorted sets f, h indexed by ℕ such that (i) B = f(E), (ii) f(0) = A, (iii) h(0) = D, and (iv) for every natural number n and for every non empty many sorted signature S and for every set x such that S = f(n) and x = h(n) holds f(n + 1) = S+·F(x, n) and h(n + 1) = H(x, n),

and

• Let x be a set and n be a natural number. Then G(x, n) is a Boolean strict circuit of F(x, n) with denotation held in gates.

The scheme CIRCCMB2’sch 21 deals with a non empty many sorted signature A, an unsplit non void strict non empty many sorted signature B with arity held in gates and Boolean denotation held in gates, a non-empty algebra C over A, a set D, a ternary functor F yielding a non empty many sorted signature, a 4-ary functor G yielding a set, a binary functor H yielding a set, and a natural number E, and states that:

Let A_{1}, A_{2} be Boolean strict circuits of B with denotation held in gates. Suppose that

(i) there exist many sorted sets f, g, h indexed by ℕ such that B = f(E) and A_{1} = g(E) and f(0) = A and g(0) = C and h(0) = D and for every natural number n and for every non empty many sorted signature S and for every non-empty algebra A over S and for every set x such that S = f(n) and A = g(n) and x = h(n) holds f(n + 1) = F(S, x, n) and g(n + 1) = G(S, A, x, n) and h(n + 1) = H(x, n), and (ii) there exist many sorted sets f, g, h indexed by ℕ such that B = f(E) and A_{2} = g(E) and f(0) = A and g(0) = C and h(0) = D and for every natural number n and for every non empty many sorted signature S and for every non-empty algebra A over S and for every set x such that S = f(n) and A = g(n) and x = h(n) holds f(n + 1) = F(S, x, n) and g(n + 1) = G(S, A, x, n) and h(n + 1) = H(x, n).

Then A_{1} = A_{2}

provided the parameters have the following property:

• Let S be a non empty many sorted signature, A be a non-empty algebra over S, x be a set, and n be a natural number. Then G(S, A, x, n) is a non-empty algebra over F(S, x, n).

5. Stability of Multi Cell Circuit

One can prove the following propositions:

(10) Let S_{1}, S_{2}, S be non void circuit-like non empty many sorted signatures. Suppose InnerVertices(S_{1}) misses InputVertices(S_{2}) and S = S_{1}+·S_{2}. Let C_{1} be a non-empty circuit of S_{1}, C_{2} be a non-empty circuit of S_{2}, and C be a non-empty circuit of S. Suppose C_{1} ≈ C_{2} and C = C_{1}+·C_{2}. Let s_{2} be a state of C_{2} and s be a state of C. If s_{2} = s↾the carrier of S_{2}, then Following(s_{2}) = Following(s)↾the carrier of S_{2}.

(11) Let S_{1}, S_{2}, S be non void circuit-like non empty many sorted signatures. Suppose InputVertices(S_{1}) misses InnerVertices(S_{2}) and S = S_{1}+·S_{2}. Let C_{1} be a non-empty circuit of S_{1}, C_{2} be a non-empty circuit of S_{2}, and C be a non-empty circuit of S. Suppose C_{1} ≈ C_{2} and C = C_{1}+·C_{2}. Let s_{1} be a state of C_{1} and s be a state of C. If s_{1} = s↾the carrier of S_{1}, then Following(s_{1}) = Following(s)↾the carrier of S_{1}.

(12) Let S_{1}, S_{2}, S be non void circuit-like non empty many sorted signatures. Suppose S_{1} ≈ S_{2} and InnerVertices(S_{1}) misses InputVertices(S_{2}) and S = S_{1}+·S_{2}. Let C_{1} be a non-empty circuit of S_{1}, C_{2} be a non-empty circuit of S_{2}, and C be a non-empty circuit of S. Suppose C_{1} ≈ C_{2} and C = C_{1}+·C_{2}.

Let s_{1} be a state of C_{1}, s_{2} be a state of C_{2}, and s be a state of C. Suppose s_{1} = s↾the carrier of S_{1} and s_{2} = s↾the carrier of S_{2} and s_{1} is stable and s_{2} is stable. Then s is stable.

(13) Let S_{1}, S_{2}, S be non void circuit-like non empty many sorted signatures. Suppose S_{1} ≈ S_{2} and InputVertices(S_{1}) misses InnerVertices(S_{2}) and S = S_{1}+·S_{2}. Let C_{1} be a non-empty circuit of S_{1}, C_{2} be a non-empty circuit of S_{2}, and C be a non-empty circuit of S. Suppose C_{1} ≈ C_{2} and C = C_{1}+·C_{2}. Let s_{1} be a state of C_{1}, s_{2} be a state of C_{2}, and s be a state of C. Suppose s_{1} = s↾the carrier of S_{1} and s_{2} = s↾the carrier of S_{2} and s_{1} is stable and s_{2} is stable. Then s is stable.

(14) Let S_{1}, S_{2}, S be non void circuit-like non empty many sorted signatures. Suppose InputVertices(S_{1}) misses InnerVertices(S_{2}) and S = S_{1}+·S_{2}. Let A_{1} be a non-empty circuit of S_{1}, A_{2} be a non-empty circuit of S_{2}, and A be a non-empty circuit of S. Suppose A_{1} ≈ A_{2} and A = A_{1}+·A_{2}. Let s be a state of A and s_{1} be a state of A_{1}. Suppose s_{1} = s↾the carrier of S_{1}. Let n be a natural number. Then Following(s, n)↾the carrier of S_{1} = Following(s_{1}, n).

(15) Let S_{1}, S_{2}, S be non void circuit-like non empty many sorted signatures. Suppose InputVertices(S_{2}) misses InnerVertices(S_{1}) and S = S_{1}+·S_{2}. Let A_{1} be a non-empty circuit of S_{1}, A_{2} be a non-empty circuit of S_{2}, and A be a non-empty circuit of S. Suppose A_{1} ≈ A_{2} and A = A_{1}+·A_{2}. Let s be a state of A and s_{2} be a state of A_{2}. Suppose s_{2} = s↾the carrier of S_{2}. Let n be a natural number. Then Following(s, n)↾the carrier of S_{2} = Following(s_{2}, n).

(16) Let S_{1}, S_{2}, S be non void circuit-like non empty many sorted signatures. Suppose InputVertices(S_{1}) misses InnerVertices(S_{2}) and S = S_{1}+·S_{2}. Let A_{1} be a non-empty circuit of S_{1}, A_{2} be a non-empty circuit of S_{2}, and A be a non-empty circuit of S. Suppose A_{1} ≈ A_{2} and A = A_{1}+·A_{2}. Let s be a state of A and s_{1} be a state of A_{1}. Suppose s_{1} = s↾the carrier of S_{1} and s_{1} is stable. Let s_{2} be a state of A_{2}. If s_{2} = s↾the carrier of S_{2}, then Following(s)↾the carrier of S_{2} = Following(s_{2}).

(17) Let S_{1}, S_{2}, S be non void circuit-like non empty many sorted signatures. Suppose S = S_{1}+·S_{2}. Let A_{1} be a non-empty circuit of S_{1}, A_{2} be a nonempty circuit of S_{2}, and A be a non-empty circuit of S. Suppose A_{1} ≈ A_{2} and A = A_{1}+·A_{2}. Let s be a state of A and s_{1} be a state of A_{1}. Suppose s_{1} = s↾the carrier of S_{1} and s_{1} is stable. Let s_{2} be a state of A_{2}. If s_{2} = s↾the carrier of S_{2} and s_{2} is stable, then s is stable.

(18) Let S_{1}, S_{2}, S be non void circuit-like non empty many sorted signatures. Suppose S = S_{1}+·S_{2}. Let A_{1} be a non-empty circuit of S_{1}, A_{2} be a nonempty circuit of S_{2}, and A be a non-empty circuit of S. Suppose A_{1} ≈ A_{2} and A = A_{1}+·A_{2}. Let s be a state of A. Suppose s is stable. Then (i) for every state s_{1} of A_{1} such that s_{1} = s↾the carrier of S_{1} holds s_{1} is

stable, and (ii) for every state s_{2} of A_{2} such that s_{2} = s↾the carrier of S_{2} holds s_{2} is

stable.

(19) Let S_{1}, S_{2}, S be non void circuit-like non empty many sorted signatures. Suppose InputVertices(S_{1}) misses InnerVertices(S_{2}) and S = S_{1}+·S_{2}. Let A_{1} be a non-empty circuit of S_{1}, A_{2} be a non-empty circuit of S_{2}, and A be a non-empty circuit of S. Suppose A_{1} ≈ A_{2} and A = A_{1}+·A_{2}. Let s_{1} be a state of A_{1}, s_{2} be a state of A_{2}, and s be a state of A. Suppose s_{1} = s↾the carrier of S_{1} and s_{2} = s↾the carrier of S_{2} and s_{1} is stable. Let n be a natural number. Then Following(s, n)↾the carrier of S_{2} = Following(s_{2}, n).

(20) Let S_{1}, S_{2}, S be non void circuit-like non empty many sorted signatures. Suppose InputVertices(S_{1}) misses InnerVertices(S_{2}) and S = S_{1}+·S_{2}. Let A_{1} be a non-empty circuit of S_{1}, A_{2} be a non-empty circuit of S_{2}, and A be a non-empty circuit of S. Suppose A_{1} ≈ A_{2} and A = A_{1}+·A_{2}. Let n_{1}, n_{2} be natural numbers, s be a state of A, s_{1} be a state of A_{1}, and s_{2} be a state of A_{2}. Suppose s_{1} = s↾the carrier of S_{1} and Following(s_{1}, n_{1}) is stable and s_{2} = Following(s, n_{1})↾the carrier of S_{2} and Following(s_{2}, n_{2}) is stable. Then Following(s, n_{1} + n_{2}) is stable.

(21) Let S_{1}, S_{2}, S be non void circuit-like non empty many sorted signatures. Suppose InputVertices(S_{1}) misses InnerVertices(S_{2}) and S = S_{1}+·S_{2}. Let A_{1} be a non-empty circuit of S_{1}, A_{2} be a non-empty circuit of S_{2}, and A be a non-empty circuit of S. Suppose A_{1} ≈ A_{2} and A = A_{1}+·A_{2}. Let n_{1}, n_{2} be natural numbers. Suppose for every state s of A_{1} holds Following(s, n_{1}) is stable and for every state s of A_{2} holds Following(s, n_{2}) is stable. Let s be a state of A. Then Following(s, n_{1} + n_{2}) is stable.

(22) Let S_{1}, S_{2}, S be non void circuit-like non empty many sorted signatures. Suppose InputVertices(S_{1}) misses InnerVertices(S_{2}) and InputVertices(S_{2}) misses InnerVertices(S_{1}) and S = S_{1}+·S_{2}. Let A_{1} be a non-empty circuit of S_{1}, A_{2} be a non-empty circuit of S_{2}, and A be a non-empty circuit of S. Suppose A_{1} ≈ A_{2} and A = A_{1}+·A_{2}. Let s be a state of A and s_{1} be a state of A_{1}. Suppose s_{1} = s↾the carrier of S_{1}. Let s_{2} be a state of A_{2}. Suppose s_{2} = s↾the carrier of S_{2}. Let n be a natural number. Then Following(s, n) = Following(s_{1}, n)+·Following(s_{2}, n).

(23) Let S_{1}, S_{2}, S be non void circuit-like non empty many sorted signatures. Suppose InputVertices(S_{1}) misses InnerVertices(S_{2}) and InputVertices(S_{2}) misses InnerVertices(S_{1}) and S = S_{1}+·S_{2}. Let A_{1} be a non-empty circuit of S_{1}, A_{2} be a non-empty circuit of S_{2}, and A be a non-empty circuit of S. Suppose A_{1} ≈ A_{2} and A = A_{1}+·A_{2}. Let n_{1}, n_{2} be natural numbers, s be a state of A, and s_{1} be a state of A_{1}. Suppose s_{1} = s↾the carrier of S_{1}. Let s_{2} be a state of A_{2}. Suppose s_{2} = s↾the carrier of S_{2} and Following(s_{1}, n_{1}) is stable and Following(s_{2}, n_{2}) is stable. Then Following(s, max(n_{1}, n_{2})) is stable.

(24) Let S_{1}, S_{2}, S be non void circuit-like non empty many sorted signatures. Suppose InputVertices(S_{1}) misses InnerVertices(S_{2}) and InputVertices(S_{2}) misses InnerVertices(S_{1}) and S = S_{1}+·S_{2}. Let A_{1} be a non-empty circuit of S_{1}, A_{2} be a non-empty circuit of S_{2}, and A be a nonempty circuit of S. Suppose A_{1} ≈ A_{2} and A = A_{1}+·A_{2}. Let n be a natural number, s be a state of A, and s_{1} be a state of A_{1}. Suppose s_{1} = s↾the carrier of S_{1}. Let s_{2} be a state of A_{2}. Suppose s_{2} = s↾the carrier of S_{2} but Following(s_{1}, n) is not stable or Following(s_{2}, n) is not stable. Then Following(s, n) is not stable.

(25) Let S_{1}, S_{2}, S be non void circuit-like non empty many sorted signatures. Suppose InputVertices(S_{1}) misses InnerVertices(S_{2}) and InputVertices(S_{2}) misses InnerVertices(S_{1}) and S = S_{1}+·S_{2}. Let A_{1} be a non-empty circuit of S_{1}, A_{2} be a non-empty circuit of S_{2}, and A be a non-empty circuit of S. Suppose A_{1} ≈ A_{2} and A = A_{1}+·A_{2}. Let n_{1}, n_{2} be natural numbers. Suppose for every state s of A_{1} holds Following(s, n_{1}) is stable and for every state s of A_{2} holds Following(s, n_{2}) is stable. Let s be a state of A. Then Following(s, max(n_{1}, n_{2})) is stable.

The scheme CIRCCMB2’sch 22 deals with unsplit non void strict non empty many sorted signatures A, B with arity held in gates and Boolean denotation held in gates, a Boolean strict circuit C of A with denotation held in gates, a Boolean strict circuit D of B with denotation held in gates, a binary functor F yielding an unsplit non void strict non empty many sorted signature with arity held in gates and Boolean denotation held in gates, a binary functor G yielding a set, a many sorted set E indexed by ℕ, a set F, a binary functor H yielding a set, and a unary functor I yielding a natural number, and states that:

For every state s of D holds Following(s, I(0) + I(2) · I(1)) is stable

provided the following conditions are satisfied:

• Let x be a set and n be a natural number. Then G(x, n) is a Boolean strict circuit of F(x, n) with denotation held in gates,

• For every state s of C holds Following(s, I(0)) is stable,

• Let n be a natural number, x be a set, and A be a non-empty circuit of F(x, n). If x = E(n) and A = G(x, n), then for every state s of A holds Following(s, I(1)) is stable,

• There exist many sorted sets f, g indexed by ℕ such that (i) B = f(I(2)), (ii) D = g(I(2)), (iii) f(0) = A, (iv) g(0) = C,

combining of multi cell circuits 63

(v) E(0) = F, and (vi) for every natural number n and for every non empty many sorted signature S and for every non-empty algebra A_{1} over S and for every set x and for every non-empty algebra A_{2} over F(x, n) such that S = f(n) and A_{1} = g(n) and x = E(n) and A_{2} = G(x, n) holds f(n+1) = S+·F(x, n) and g(n+1) = A_{1}+·A_{2} and E(n + 1) = H(x, n),

• InnerVertices(A) is a binary relation and InputVertices(A) has no pairs,

• E(0) = F and F ∈ InnerVertices(A),

• For every natural number n and for every set x holds InnerVertices(F(x, n)) is a binary relation,

• For every natural number n and for every set x such that x = E(n) holds InputVertices(F(x, n)) \ {x} has no pairs, and

• For every natural number n and for every set x such that x = E(n) holds E(n + 1) = H(x, n) and x ∈ InputVertices(F(x, n)) and H(x, n) ∈ InnerVertices(F(x, n)).

References

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[2] Grzegorz Bancerek. König’s theorem. Formalized Mathematics, 1(3):589–593, 1990.

[3] Grzegorz Bancerek and Yatsuka Nakamura. Full adder circuit. Part I. Formalized Mathematics, 5(3):367–380, 1996.

[4] Czesław Byliński. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529–536, 1990.

[5] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

[6] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[7] Czesław Byliński. The modification of a function by a function and the iteration of the composition of a function. Formalized Mathematics, 1(3):521–527, 1990.

[8] Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357–367, 1990.

[9] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990.

[10] Jarosław Kotowicz. The limit of a real function at infinity. Formalized Mathematics, 2(1):17–28, 1991.

[11] Yatsuka Nakamura and Grzegorz Bancerek. Combining of circuits. Formalized Mathematics, 5(2):283–295, 1996.

[12] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Introduction to circuits, I. Formalized Mathematics, 5(2):227–232, 1996.

[13] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Introduction to circuits, II. Formalized Mathematics, 5(2):273–278, 1996.

[14] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, II. Formalized Mathematics, 5(2):215–220, 1996.

[15] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[16] Andrzej Trybulec. Many sorted algebras. Formalized Mathematics, 5(1):37–42, 1996.

[17] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[18] Zinaida Trybulec and Halina Święczkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

64 grzegorz bancerek et al.

[19] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.

[20] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990.

Full Adder Circuit. Part II

Grzegorz Bancerek Białystok Technical University Shin’nosuke Yamaguchi Shinshu University Nagano

Katsumi Wasaki Shinshu University Nagano

Summary. In this article we continue the investigations from [6] of verification of a design of adder circuit. We define it as a combination of 1-bit adders using schemes from [7]. n-bit adder circuit has the following structure

1st bit adder x_{1} y_{1}  x_{2} y_{2} r_{1}  r_{2}2nd bit adder  n-th bit adder x_{n} y_{n} r_{n}

As the main result we prove the stability of the circuit. Further works will consist of the proof of full correctness of the circuit.

MML Identifier: FACIRC 2.

The articles [13], [20], [1], [4], [10], [11], [14], [6], [5], [8], [9], [2], [21], [16], [12], [18], [3], [17], [22], [19], and [15] provide the notation and terminology for this paper.

The following three propositions are true:

(1) For all sets x, y, z such that x ≠ z and y ≠ z holds {x, y} \ {z} = {x, y}.

(2) For all non empty sets X, Y and for all natural numbers n, m such that n ≠ m holds X^{n} ≠ Y^{m}.

(3) For all sets x, y, z holds x ≠ ⟨⟨⟨x, y⟩, z⟩⟩ and y ≠ ⟨⟨⟨x, y⟩, z⟩⟩. Let us note that every many sorted signature which is void is also unsplit

and has arity held in gates and Boolean denotation held in gates.

One can check that there exists a many sorted signature which is strict and void.

Let x be a set. The functor SingleMSSx yielding a strict void many sorted signature is defined as follows:

(Def. 1) The carrier of SingleMSSx = {x}.

Let x be a set. Note that SingleMSSx is non empty. Let x be a set.

(Def. 2) SingleMSAx is a Boolean strict algebra over SingleMSSx. We now state three propositions:

(4) For every set x and for every many sorted signature S holds SingleMSSx ≈ S.

(5) Let x be a set and S be a non empty many sorted signature. Suppose x ∈ the carrier of S. Then SingleMSSx+·S = the many sorted signature of S.

(6) Let x be a set, S be a non empty strict many sorted signature, and A be a Boolean algebra over S. If x ∈ the carrier of S, then SingleMSAx+·A = the algebra of A.

∅ is a finite sequence with length 0. We introduce ε as a synonym of ∅. Let n be a natural number and let x, y be finite sequences. The functor

n-BitAdderStr(x, y) yields an unsplit non void strict non empty many sorted signature with arity held in gates and Boolean denotation held in gates and is defined by the condition (Def. 3).

(Def. 3) There exist many sorted sets f, g indexed by ℕ such that (i) n-BitAdderStr(x, y) = f(n), (ii) f(0) = 1GateCircStr(ε, Boolean^{0} ⟼→ false), (iii) g(0) = ⟨⟨ε, Boolean^{0} ⟼→ false⟩⟩, and (iv) for every natural number n and for every non empty many sorted

signature S and for every set z such that S = f(n) and z = g(n) holds f(n + 1) = S+·BitAdderWithOverflowStr(x(n + 1), y(n + 1), z) and g(n + 1) = MajorityOutput(x(n + 1), y(n + 1), z).

Let n be a natural number and let x, y be finite sequences. The functor n-BitAdderCirc(x, y) yields a Boolean strict circuit of n-BitAdderStr(x, y) with denotation held in gates and is defined by the condition (Def. 4).

(Def. 4) There exist many sorted sets f, g, h indexed by ℕ such that (i) n-BitAdderStr(x, y) = f(n), (ii) n-BitAdderCirc(x, y) = g(n), (iii) f(0) = 1GateCircStr(ε, Boolean^{0} ⟼→ false), (iv) g(0) = 1GateCircuit(ε, Boolean^{0} ⟼→ false),

(v) h(0) = ⟨⟨ε, Boolean^{0} ⟼→ false⟩⟩, and (vi) for every natural number n and for every non empty many sor-

ted signature S and for every non-empty algebra A over S and for every set z such that S = f(n) and A = g(n) and z = h(n) holds f(n + 1) = S+·BitAdderWithOverflowStr(x(n + 1), y(n + 1), z) and g(n + 1) = A+·BitAdderWithOverflowCirc(x(n + 1), y(n + 1), z) and h(n + 1) = MajorityOutput(x(n + 1), y(n + 1), z).

Let n be a natural number and let x, y be finite sequences. The functor n-BitMajorityOutput(x, y) yielding an element of InnerVertices(n-BitAdderStr

(x, y)) is defined by the condition (Def. 5). (Def. 5) There exists a many sorted set h indexed by ℕ such that

(i) n-BitMajorityOutput(x, y) = h(n), (ii) h(0) = ⟨⟨ε, Boolean^{0} ⟼→ false⟩⟩, and (iii) for every natural number n and for every set z such that z = h(n) holds

h(n + 1) = MajorityOutput(x(n + 1), y(n + 1), z). We now state several propositions:

(7) Let x, y be finite sequences and f, g, h be many sorted sets indexed by ℕ. Suppose that

(i) f(0) = 1GateCircStr(ε, Boolean^{0} ⟼→ false), (ii) g(0) = 1GateCircuit(ε, Boolean^{0} ⟼→ false), (iii) h(0) = ⟨⟨ε, Boolean^{0} ⟼→ false⟩⟩, and (iv) for every natural number n and for every non empty many sor-

ted signature S and for every non-empty algebra A over S and for every set z such that S = f(n) and A = g(n) and z = h(n) holds f(n + 1) = S+·BitAdderWithOverflowStr(x(n + 1), y(n + 1), z) and g(n + 1) = A+·BitAdderWithOverflowCirc(x(n + 1), y(n + 1), z) and h(n + 1) = MajorityOutput(x(n + 1), y(n + 1), z). Let n be a natural number. Then n-BitAdderStr(x, y) = f(n) and n-BitAdderCirc(x, y) = g(n) and n-BitMajorityOutput(x, y) = h(n).

(8) For all finite sequences a, b holds 0-BitAdderStr(a, b) = 1GateCircStr(ε, Boolean^{0} ⟼→ false) and 0-BitAdderCirc(a, b) = 1GateCircuit(ε, Boolean^{0} ⟼→ false) and 0-BitMajorityOutput(a, b) = ⟨⟨ε, Boolean^{0} ⟼→ false⟩⟩.

(9) Let a, b be finite sequences and c be a set. Suppose c = ⟨⟨ε, Boolean^{0} ⟼→ false⟩⟩. Then 1-BitAdderStr(a, b) = 1GateCircStr(ε, Boolean^{0} ⟼→ false)+·BitAdderWithOverflowStr(a(1), b(1), c) and 1-BitAdderCirc(a, b) = 1GateCircuit(ε, Boolean^{0} ⟼→ false)+·BitAdderWithOverflowCirc(a(1),

b(1), c) and 1-BitMajorityOutput(a, b) = MajorityOutput(a(1), b(1), c).

(10) For all sets a, b, c such that c = ⟨⟨ε, Boolean^{0} ⟼→ false⟩⟩ holds 1-BitAdderStr(⟨a⟩, ⟨b⟩) = 1GateCircStr(ε, Boolean^{0} ⟼→ false) +·BitAdderWithOverflowStr(a, b, c) and 1-BitAdderCirc(⟨a⟩, ⟨b⟩) = 1GateCircuit(ε, Boolean^{0} ⟼→ false)+·BitAdderWithOverflowCirc(a, b, c) and 1-BitMajorityOutput(⟨a⟩, ⟨b⟩) = MajorityOutput(a, b, c).

(11) Let n be a natural number, p, q be finite sequences with length n, and p_{1}, p_{2}, q_{1}, q_{2} be finite sequences. Then n-BitAdderStr(p ^{⌢} p_{1}, q ^{⌢} q_{1}) = n-BitAdderStr(p^{⌢} p_{2}, q ^{⌢} q_{2}) and n-BitAdderCirc(p^{⌢} p_{1}, q ^{⌢} q_{1}) = n-BitAdderCirc(p^{⌢} p_{2}, q ^{⌢} q_{2}) and n-BitMajorityOutput(p^{⌢} p_{1}, q ^{⌢} q_{1}) = n-BitMajorityOutput(p^{⌢} p_{2}, q^{⌢} q_{2}).

(12) Let n be a natural number, x, y be finite sequences with length n, and a, b be sets. Then (n + 1)-BitAdderStr(x ^{⌢} ⟨a⟩, y ^{⌢} ⟨b⟩) = (n-BitAdderStr(x, y))+·BitAdderWithOverflowStr(a, b, n-BitMajorityOutput(x, y)) and (n + 1)-BitAdderCirc(x^{⌢} ⟨a⟩, y ^{⌢} ⟨b⟩) = (n-BitAdderCirc(x, y))+·BitAdderWithOverflowCirc (a, b, n-BitMajorityOutput(x, y)) and (n + 1)-BitMajorityOutput(x ^{⌢} ⟨a⟩, y^{⌢} ⟨b⟩) = MajorityOutput(a, b, n-BitMajorityOutput(x, y)).

(13) Let n be a natural number and x, y be finite sequences. Then (n + 1)-BitAdderStr(x, y) = (n-BitAdderStr(x, y))+·BitAdderWithOverflowStr (x(n+1), y(n+1), n-BitMajorityOutput(x, y)) and (n+1)-BitAdderCirc(x, y) = (n-BitAdderCirc(x, y))+·BitAdderWithOverflowCirc(x(n+1), y(n+1), n-BitMajorityOutput(x, y)) and (n + 1)-BitMajorityOutput(x, y) = MajorityOutput(x(n + 1), y(n + 1), n-BitMajorityOutput(x, y)).

(14) For all natural numbers n, m such that n m and for all finite sequences x, y holds InnerVertices(n-BitAdderStr(x, y)) ⊆ InnerVertices(m-BitAdderStr(x, y)).

(15) For every natural number n and for all finite sequences x, y holds InnerVertices((n+1)-BitAdderStr(x, y)) = InnerVertices(n-BitAdderStr(x, y)) ∪ InnerVertices(BitAdderWithOverflowStr(x(n + 1), y(n + 1), n-BitMajorityOutput(x, y))).

Let k, n be natural numbers. Let us assume that k 1 and k n. Let x, y be finite sequences. The functor (k, n)-BitAdderOutput(x, y) yielding an element of InnerVertices(n-BitAdderStr(x, y)) is defined by:

(Def. 6) There exists a natural number i such that k = i + 1 and (k, n)-BitAdderOutput(x, y) = BitAdderOutput(x(k), y(k), i-BitMajorityOutput(x, y)).

Next we state several propositions:

(16) For all natural numbers n, k such that k < n and for all finite sequences x, y holds (k + 1, n)-BitAdderOutput(x, y) = BitAdderOutput(x(k +

1), y(k + 1), k-BitMajorityOutput(x, y)).

(17) For every natural number n and for all finite sequences x, y holds InnerVertices(n-BitAdderStr(x, y)) is a binary relation.

(18) For all sets x, y, c holds InnerVertices(MajorityIStr(x, y, c)) = {⟨⟨⟨x, y⟩, &⟩⟩, ⟨⟨⟨y, c⟩, &⟩⟩, ⟨⟨⟨c, x⟩, &⟩⟩}.

(19) For all sets x, y, c such that x ≠ ⟨⟨⟨y, c⟩, &⟩⟩ and y ≠ ⟨⟨⟨c, x⟩, &⟩⟩ and c ≠ ⟨⟨⟨x, y⟩, &⟩⟩ holds InputVertices(MajorityIStr(x, y, c)) = {x, y, c}.

(20) For all sets x, y, c holds InnerVertices(MajorityStr(x, y, c)) = {⟨⟨⟨x, y⟩, &⟩⟩, ⟨⟨⟨y, c⟩, &⟩⟩, ⟨⟨⟨c, x⟩, &⟩⟩} ∪ {MajorityOutput(x, y, c)}.

(21) For all sets x, y, c such that x ≠ ⟨⟨⟨y, c⟩, &⟩⟩ and y ≠ ⟨⟨⟨c, x⟩, &⟩⟩ and c ≠ ⟨⟨⟨x, y⟩, &⟩⟩ holds InputVertices(MajorityStr(x, y, c)) = {x, y, c}.

(22) For all non empty many sorted signatures S_{1}, S_{2} such that S_{1} ≈ S_{2} and InputVertices(S_{1}) = InputVertices(S_{2}) holds InputVertices(S_{1}+·S_{2}) = InputVertices(S_{1}).

(23) For all sets x, y, c such that x ≠ ⟨⟨⟨y, c⟩, &⟩⟩ and y ≠ ⟨⟨⟨c, x⟩, &⟩⟩ and c ≠ ⟨⟨⟨x, y⟩, &⟩⟩ and c ≠ ⟨⟨⟨x, y⟩, xor ⟩⟩ holds InputVertices(BitAdderWithOverflowStr(x, y, c)) = {x, y, c}.

(24) For all sets x, y, c holds InnerVertices(BitAdderWithOverflowStr(x, y, c)) = {⟨⟨⟨x, y⟩, xor ⟩⟩, 2GatesCircOutput(x, y, c, xor)}∪{⟨⟨⟨x, y⟩, &⟩⟩, ⟨⟨⟨y, c⟩, &⟩⟩, ⟨⟨⟨c, x⟩, &⟩⟩} ∪ {MajorityOutput(x, y, c)}.

Let us mention that every set which is empty is also non pair. Observe that ∅ is nonpair yielding. Let f be a nonpair yielding function and

let x be a set. Observe that f(x) is non pair.

Let n be a natural number and let x, y be finite sequences. Note that n-BitMajorityOutput(x, y) is pair.

The following propositions are true:

(25) Let x, y be finite sequences and n be a natural number. Then (n-BitMajorityOutput(x, y))_{1} = ε and (n-BitMajorityOutput(x, y))_{2} = Boolean^{0} ⟼→ false and π_{1}((n-BitMajorityOutput(x, y))_{2}) = Boolean^{0} or \overline{\overline{(n-BitMajorityOutput(x, y))_{1}}} = 3 and (n-BitMajorityOutput(x, y))_{2} = or_{3} and π_{1}((n-BitMajorityOutput(x, y))_{2}) = Boolean^{3} .

(26) For every natural number n and for all finite sequences x, y and for every set p holds n-BitMajorityOutput(x, y) ≠ ⟨⟨p, &⟩⟩ and n-BitMajorityOutput(x, y) ≠ ⟨⟨p, xor ⟩⟩.

(27) Let f, g be nonpair yielding finite sequences and n be a natural number. Then InputVertices((n + 1)-BitAdderStr(f, g)) = InputVertices(n-BitAdderStr(f, g)) ∪ (InputVertices (BitAdderWithOverflowStr(f(n+1), g(n+1), n-BitMajorityOutput(f, g)))\ {n-BitMajorityOutput(f, g)}) and InnerVertices(n-BitAdderStr(f, g)) is a binary relation and InputVertices(n-BitAdderStr(f, g)) has no pairs.

70 grzegorz bancerek et al.

(28) For every natural number n and for all nonpair yielding finite sequences x, y with length n holds InputVertices(n-BitAdderStr(x, y)) = rngx ∪ rngy.

(29) Let x, y, c be sets, s be a state of MajorityCirc(x, y, c), and a_{1}, a_{2}, a_{3} be elements of Boolean. If a_{1} = s(⟨⟨⟨x, y⟩, &⟩⟩) and a_{2} = s(⟨⟨⟨y, c⟩, &⟩⟩) and a_{3} = s(⟨⟨⟨c, x⟩, &⟩⟩), then (Following(s))(MajorityOutput(x, y, c)) = a_{1} ∨ a_{2} ∨ a_{3}.

(30) Let x, y, c be sets. Suppose x ≠ ⟨⟨⟨y, c⟩, &⟩⟩ and y ≠ ⟨⟨⟨c, x⟩, &⟩⟩ and c ≠ ⟨⟨⟨x, y⟩, &⟩⟩ and c ≠ ⟨⟨⟨x, y⟩, xor ⟩⟩. Let s be a state of MajorityCirc(x, y, c). Then Following(s, 2) is stable.

(31) Let x, y, c be sets. Suppose x ≠ ⟨⟨⟨y, c⟩, &⟩⟩ and y ≠ ⟨⟨⟨c, x⟩, &⟩⟩ and c ≠ ⟨⟨⟨x, y⟩, &⟩⟩ and c ≠ ⟨⟨⟨x, y⟩, xor ⟩⟩. Let s be a state of BitAdderWithOverflowCirc(x, y, c) and a_{1}, a_{2}, a_{3} be elements of Boolean. Suppose a_{1} = s(x) and a_{2} = s(y) and a_{3} = s(c). Then (Following(s, 2))(BitAdderOutput(x, y, c)) = a_{1} ⊕ a_{2} ⊕ a_{3} and (Following(s, 2))(MajorityOutput(x, y, c)) = a_{1} ∧ a_{2} ∨ a_{2} ∧ a_{3} ∨ a_{3} ∧ a_{1}.

(32) Let x, y, c be sets. Suppose x ≠ ⟨⟨⟨y, c⟩, &⟩⟩ and y ≠ ⟨⟨⟨c, x⟩, &⟩⟩ and c ≠ ⟨⟨⟨x, y⟩, &⟩⟩ and c ≠ ⟨⟨⟨x, y⟩, xor ⟩⟩. Let s be a state of BitAdderWithOverflowCirc(x, y, c). Then Following(s, 2) is stable.

(33) Let n be a natural number, x, y be nonpair yielding finite sequences with length n, and s be a state of n-BitAdderCirc(x, y). Then Following(s, 1 + 2 · n) is stable.

References

[1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990.

[2] Grzegorz Bancerek. Curried and uncurried functions. Formalized Mathematics, 1(3):537– 541, 1990.

[3] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[4] Grzegorz Bancerek. König’s theorem. Formalized Mathematics, 1(3):589–593, 1990.

[5] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

[6] Grzegorz Bancerek and Yatsuka Nakamura. Full adder circuit. Part I. Formalized Mathematics, 5(3):367–380, 1996.

[7] Grzegorz Bancerek, Shin’nosuke Yamaguchi, and Yasunari Shidama. Combining of multi cell circuits. Formalized Mathematics, 10(1):47–64, 2002.

[8] Czesław Byliński. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529–536, 1990.

[9] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

[10] Yatsuka Nakamura and Grzegorz Bancerek. Combining of circuits. Formalized Mathematics, 5(2):283–295, 1996.

[11] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Introduction to circuits, II. Formalized Mathematics, 5(2):273–278, 1996.

[12] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, II. Formalized Mathematics, 5(2):215–220, 1996.

full adder circuit. part ii 71

[13] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Formalized Mathematics, 4(1):83–86, 1993.

[14] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25–34, 1990.

[15] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[16] Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97–105, 1990.

[17] Andrzej Trybulec. Many-sorted sets. Formalized Mathematics, 4(1):15–22, 1993.

[18] Andrzej Trybulec. Many sorted algebras. Formalized Mathematics, 5(1):37–42, 1996.

[19] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[20] Zinaida Trybulec and Halina Święczkowska. Boolean properties of sets. Formalized Mathematics, 1(1):17–23, 1990.

[21] Edmund Woronowicz. Many–argument relations. Formalized Mathematics, 1(4):733–737, 1990.

[22] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.

Contents Formaliz. Math. 10 (1)

Fan Homeomorphisms in the Plane

By Yatsuka Nakamura  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

Half Open Intervals in Real Numbers

By Yatsuka Nakamura  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

Some Remarks on Clockwise Oriented Sequences on Go-boards

By Adam Naumowicz and Robert Milewski  . . . . . . . . . . . . . . . 23

Dickson’s Lemma

By Gilbert Lee and Piotr Rudnicki  . . . . . . . . . . . . . . . . . . . . . . . 29

On Ordering of Bags

By Gilbert Lee and Piotr Rudnicki  . . . . . . . . . . . . . . . . . . . . . . . 39

Combining of Multi Cell Circuits

By Grzegorz Bancerek et al.  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47

Full Adder Circuit. Part II

By Grzegorz Bancerek et al.  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65

Continued on inside back cover