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

Preliminaries to Automatic Generation of Mizar Documentation for Circuits

Grzegorz Bancerek^{1} Białystok Technical University

Adam Naumowicz^{2} University of Białystok

Summary. In this paper we introduce technical notions used by a system which automatically generates Mizar documentation for specified circuits. They provide a ready for use elements needed to justify correctness of circuits’ construction. We concentrate on the concept of stabilization and analyze one-gate circuits and their combinations.

MML Identifier: CIRCCMB3.

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

1. Stabilizing Circuits

The following proposition is true

(1) 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 x be a set. If x ∈ InputVertices(S), then for every natural number n holds (Following(s, n))(x) = s(x).

Let S be a non void circuit-like non empty many sorted signature, let A be a non-empty circuit of S, and let s be a state of A. We say that s is stabilizing if and only if:

1This paper was written when the first author visited Shinshu University as a two-year JSPS Fellow.

2The paper was prepared during the author’s cooperative research at Shinshu University ’Verification of circuit designs with the aid of the Mizar system’.

(Def. 1) There exists a natural number n such that Following(s, n) is stable.

Let S be a non void circuit-like non empty many sorted signature and let A be a non-empty circuit of S. We say that A is stabilizing if and only if:

(Def. 2) Every state of A is stabilizing.

We say that A has a stabilization limit if and only if: (Def. 3) There exists a natural number n such that for every state s of A holds

Following(s, n) is stable. Let S be a non void circuit-like non empty many sorted signature. Note that

every non-empty circuit of S which has a stabilization limit is also stabilizing.

Let S be a non void circuit-like non empty many sorted signature, let A be a non-empty circuit of S, and let s be a state of A. Let us assume that s is stabilizing. The functor Result(s) yields a state of A and is defined as follows:

(Def. 4) Result(s) is stable and there exists a natural number n such that

Result(s) = Following(s, n). Let S be a non void circuit-like non empty many sorted signature, let A be

a non-empty circuit of S, and let s be a state of A. Let us assume that s is stabilizing. The stabilization time of s is a natural number and is defined by the conditions (Def. 5).

(Def. 5)(i) Following(s, the stabilization time of s) is stable, and

(ii) for every natural number n such that n < the stabilization time of s

holds Following(s, n) is not stable. The following propositions are true:

(2) 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 stabilizing, then Result(s) = Following(s, the stabilization time of s).

(3) 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 be a natural number. If Following(s, n) is stable, then the stabilization time of s n.

(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 be a natural number. If Following(s, n) is stable, then Result(s) = Following(s, n).

(5) 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 be a natural number. Suppose s is stabilizing and n the stabilization time of s. Then Result(s) = Following(s, n).

(6) 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 stabilizing, then for every set x such that x ∈ InputVertices(S) holds (Result(s))(x) = s(x).

(7) Let S_{1}, S be non void circuit-like non empty many sorted signatures, A_{1} be a non-empty circuit of S_{1}, A be a non-empty circuit of S, s be a state of A, and s_{1} be a state of A_{1}. If s_{1} = s↾the carrier of S_{1}, then for every vertex v_{1} of S_{1} holds s_{1}(v_{1}) = s(v_{1}).

(8) Let S_{1}, S_{2} 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}). Let S be a non void circuitlike non empty many sorted signature. Suppose S = S_{1}+·S_{2}. Let A_{1} be a non-empty circuit of S_{1} and A_{2} be a non-empty circuit of S_{2}. Suppose A_{1} ≈ A_{2}. Let A be a non-empty circuit of S. Suppose A = A_{1}+·A_{2}. Let 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 s_{2} = s↾the carrier of S_{2} and s_{1} is stabilizing and s_{2} is stabilizing. Then s is stabilizing.

(9) Let S_{1}, S_{2} 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}). Let S be a non void circuitlike non empty many sorted signature. Suppose S = S_{1}+·S_{2}. Let A_{1} be a non-empty circuit of S_{1} and A_{2} be a non-empty circuit of S_{2}. Suppose A_{1} ≈ A_{2}. Let A be a non-empty circuit of S. Suppose 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 stabilizing. Let s_{2} be a state of A_{2}. Suppose s_{2} = s↾the carrier of S_{2} and s_{2} is stabilizing. Then the stabilization time of s = max(the stabilization time of s_{1}, the stabilization time of s_{2}).

(10) Let S_{1}, S_{2} be non void circuit-like non empty many sorted signatures. Suppose InputVertices(S_{1}) misses InnerVertices(S_{2}). Let S be a non void circuit-like non empty many sorted signature. Suppose S = S_{1}+·S_{2}. Let A_{1} be a non-empty circuit of S_{1} and A_{2} be a non-empty circuit of S_{2}. Suppose A_{1} ≈ A_{2}. Let A be a non-empty circuit of S. Suppose 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 stabilizing. Let s_{2} be a state of A_{2}. Suppose s_{2} = Following(s, the stabilization time of s_{1})↾the carrier of S_{2} and s_{2} is stabilizing. Then s is stabilizing.

(11) Let S_{1}, S_{2} be non void circuit-like non empty many sorted signatures. Suppose InputVertices(S_{1}) misses InnerVertices(S_{2}). Let S be a non void circuit-like non empty many sorted signature. Suppose S = S_{1}+·S_{2}. Let A_{1} be a non-empty circuit of S_{1} and A_{2} be a non-empty circuit of S_{2}. Suppose A_{1} ≈ A_{2}. Let A be a non-empty circuit of S. Suppose 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 stabilizing. Let s_{2} be a state of A_{2}. Suppose s_{2} = Following(s, the stabilization time of s_{1})↾the carrier of S_{2} and s_{2} is stabilizing. Then the stabilization time of s = (the stabilization time of s_{1}) + (the stabilization time of s_{2}).

(12) 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 stabilizing. Let s_{2} be a state of A_{2}. Suppose s_{2} = Following(s, the stabilization time of s_{1})↾the carrier of S_{2} and s_{2} is stabilizing. Then Result(s)↾the carrier of S_{1} = Result(s_{1}).

2. One-gate Circuits

We now state three propositions:

(13) Let x be a set, X be a non empty finite set, n be a natural number, p be a finite sequence with length n, g be a function from X^{n} into X, and s be a state of 1GateCircuit(p, g). Then s · p is an element of X^{n}.

(14) For all sets x_{1}, x_{2}, x_{3}, x_{4} holds rng⟨x_{1}, x_{2}, x_{3}, x_{4}⟩ = {x_{1}, x_{2}, x_{3}, x_{4}}.

(15) For all sets x_{1}, x_{2}, x_{3}, x_{4}, x_{5} holds rng⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩ =

{x_{1}, x_{2}, x_{3}, x_{4}, x_{5}}. Let x_{1}, x_{2}, x_{3}, x_{4} be sets. Then ⟨x_{1}, x_{2}, x_{3}, x_{4}⟩ is a finite sequence with length

4. Let x_{5} be a set. Then ⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩ is a finite sequence with length 5. Let S be a many sorted signature. We say that S is one-gate if and only if

the condition (Def. 6) is satisfied. (Def. 6) There exists a non empty finite set X and there exists a natural number

n and there exists a finite sequence p with length n and there exists a function f from X^{n} into X such that S = 1GateCircStr(p, f).

Let S be a non empty many sorted signature and let A be an algebra over S. We say that A is one-gate if and only if the condition (Def. 7) is satisfied.

(Def. 7) There exists a non empty finite set X and there exists a natural number n and there exists a finite sequence p with length n and there exists a function f from X^{n} into X such that S = 1GateCircStr(p, f) and A = 1GateCircuit(p, f).

Let p be a finite sequence and let x be a set. Observe that 1GateCircStr(p, x) is finite.

Let us note that every many sorted signature which is one-gate is also strict, non void, non empty, unsplit, and finite and has arity held in gates.

One can check that every non empty many sorted signature which is one-gate has also denotation held in gates.

Let X be a non empty finite set, let n be a natural number, let p be a finite sequence with length n, and let f be a function from X^{n} into X. Note that 1GateCircStr(p, f) is one-gate.

One can check that there exists a many sorted signature which is one-gate.

Let S be an one-gate many sorted signature. Observe that every circuit of S which is one-gate is also strict and non-empty.

Let X be a non empty finite set, let n be a natural number, let p be a finite sequence with length n, and let f be a function from X^{n} into X. One can check that 1GateCircuit(p, f) is one-gate.

Let S be an one-gate many sorted signature. Observe that there exists a circuit of S which is one-gate and non-empty.

Let S be an one-gate many sorted signature. The functor OutputS yields a vertex of S and is defined as follows:

(Def. 8) OutputS = ⋃ (the operation symbols of S). Let S be an one-gate many sorted signature. Observe that OutputS is pair. Next we state several propositions:

(16) Let S be an one-gate many sorted signature, p be a finite sequence, and x be a set. If S = 1GateCircStr(p, x), then OutputS = ⟨⟨p, x⟩⟩.

(17) For every one-gate many sorted signature S holds InnerVertices(S) = {OutputS}.

(18) Let S be an one-gate many sorted signature, A be an one-gate circuit of S, n be a natural number, X be a finite non empty set, f be a function from X^{n} into X, and p be a finite sequence with length n. If A = 1GateCircuit(p, f), then S = 1GateCircStr(p, f).

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

(20) Let S be an one-gate many sorted signature, A be an one-gate circuit of

S, and s be a state of A. Then Following(s) is stable. Let S be a non void circuit-like non empty many sorted signature. Observe

that every non-empty circuit of S which is one-gate has also a stabilization limit.

We now state two propositions:

(21) Let S be an one-gate many sorted signature, A be an one-gate circuit of S, and s be a state of A. Then Result(s) = Following(s).

(22) Let S be an one-gate many sorted signature, A be an one-gate circuit of

S, and s be a state of A. Then the stabilization time of s 1. In this article we present several logical schemes. The scheme OneGate1Ex

deals with a set A, a non empty finite set B, and a unary functor F yielding an element of B, and states that:

There exists an one-gate many sorted signature S and there exists an one-gate circuit A of S such that InputVertices(S) = {A} and for every state s of A holds (Result(s))(OutputS) = F(s(A))

for all values of the parameters.

The scheme OneGate2Ex deals with sets A, B, a non empty finite set C, and a binary functor F yielding an element of C, and states that:

There exists an one-gate many sorted signature S and there exists an one-gate circuit A of S such that InputVertices(S) = {A, B} and for every state s of A holds (Result(s))(OutputS) = F(s(A), s(B))

for all values of the parameters.

The scheme OneGate3Ex deals with sets A, B, C, a non empty finite set D, and a ternary functor F yielding an element of D, and states that:

There exists an one-gate many sorted signature S and there exists an one-gate circuit A of S such that InputVertices(S) = {A, B, C} and for every state s of A holds (Result(s))(OutputS)

= F(s(A), s(B), s(C))

for all values of the parameters.

The scheme OneGate4Ex deals with sets A, B, C, D, a non empty finite set E, and a 4-ary functor F yielding an element of E, and states that:

There exists an one-gate many sorted signature S and there exists an one-gate circuit A of S such that InputVertices(S) = {A, B, C, D} and for every state s of A holds (Result(s))(OutputS)

= F(s(A), s(B), s(C), s(D))

for all values of the parameters.

The scheme OneGate5Ex deals with sets A, B, C, D, E, a non empty finite set F, and a 5-ary functor F yielding an element of F, and states that:

There exists an one-gate many sorted signature S and there exists an one-gate circuit A of S such that InputVertices(S) = {A, B, C, D, E} and for every state s of A holds (Result(s))(OutputS)

= F(s(A), s(B), s(C), s(D), s(E))

for all values of the parameters.

3. Mono-sorted Circuits

One can prove the following propositions:

(23) For every constant function f holds f = domf ⟼→ the value of f.

(24) For all non empty sets X, Y and for all natural numbers n, m such that n ≠ 0 and X^{n} = Y^{m} holds X = Y and n = m.

(25) For all non empty many sorted signatures S_{1}, S_{2} holds every vertex of S_{1} is a vertex of S_{1}+·S_{2}.

(26) For all non empty many sorted signatures S_{1}, S_{2} holds every vertex of

S_{2} is a vertex of S_{1}+·S_{2}. Let X be a non empty finite set. A non void non empty unsplit many sorted

signature with arity held in gates with denotation held in gates is said to be a signature over X if it satisfies the condition (Def. 9).

(Def. 9) There exists a circuit A of it such that the sorts of A are constant and

the value of the sorts of A = X and A has denotation held in gates. Next we state the proposition

(27) Let n be a natural number, X be a non empty finite set, f be a function from X^{n} into X, and p be a finite sequence with length n. Then 1GateCircStr(p, f) is a signature over X.

Let X be a non empty finite set. Observe that there exists a signature over X which is strict and one-gate.

Let n be a natural number, let X be a non empty finite set, let f be a function from X^{n} into X, and let p be a finite sequence with length n. Then 1GateCircStr(p, f) is a strict signature over X.

Let X be a non empty finite set and let S be a signature over X. A circuit of S is called a circuit over X and S if:

(Def. 10) It has denotation held in gates and the sorts of it are constant and the

value of the sorts of it = X. Let X be a non empty finite set and let S be a signature over X. One can

check that every circuit over X and S is non-empty and has denotation held in gates.

Next we state the proposition

(28) Let n be a natural number, X be a non empty finite set, f be a function from X^{n} into X, and p be a finite sequence with length n. Then 1GateCircuit(p, f) is a circuit over X and 1GateCircStr(p, f).

Let X be a non empty finite set and let S be an one-gate signature over X. One can check that there exists a circuit over X and S which is strict and one-gate.

Let X be a non empty finite set and let S be a signature over X. One can check that there exists a circuit over X and S which is strict.

Let n be a natural number, let X be a non empty finite set, let f be a function from X^{n} into X, and let p be a finite sequence with length n. Then 1GateCircuit(p, f) is a strict circuit over X and 1GateCircStr(p, f).

One can prove the following propositions:

(29) For every non empty finite set X and for all signatures S_{1}, S_{2} over X holds S_{1} ≈ S_{2}.

(30) Let X be a non empty finite set, S_{1}, S_{2} be signatures over X, A_{1} be a circuit over X and S_{1}, and A_{2} be a circuit over X and S_{2}. Then A_{1} ≈ A_{2}.

(31) Let X be a non empty finite set, S_{1}, S_{2} be signatures over X, A_{1} be a circuit over X and S_{1}, and A_{2} be a circuit over X and S_{2}. Then A_{1}+·A_{2} is a circuit of S_{1}+·S_{2}.

(32) Let X be a non empty finite set, S_{1}, S_{2} be signatures over X, A_{1} be a circuit over X and S_{1}, and A_{2} be a circuit over X and S_{2}. Then A_{1}+·A_{2}

has denotation held in gates.

(33) Let X be a non empty finite set, S_{1}, S_{2} be signatures over X, A_{1} be a circuit over X and S_{1}, and A_{2} be a circuit over X and S_{2}. Then the sorts of A_{1}+·A_{2} are constant and the value of the sorts of A_{1}+·A_{2} = X.

Let S_{1}, S_{2} be finite non empty many sorted signatures. Note that S_{1}+·S_{2} is finite.

Let X be a non empty finite set and let S_{1}, S_{2} be signatures over X. One can verify that S_{1}+·S_{2} has denotation held in gates.

Let X be a non empty finite set and let S_{1}, S_{2} be signatures over X. Then S_{1}+·S_{2} is a strict signature over X.

Let X be a non empty finite set, let S_{1}, S_{2} be signatures over X, let A_{1} be a circuit over X and S_{1}, and let A_{2} be a circuit over X and S_{2}. Then A_{1}+·A_{2} is a strict circuit over X and S_{1}+·S_{2}.

One can prove the following two propositions:

(34) For all sets x, y holds rk(x) ∈ rk(⟨⟨x, y⟩⟩) and rk(y) ∈ rk(⟨⟨x, y⟩⟩).

(35) Let S be a finite non void non empty unsplit many sorted signature with arity held in gates with denotation held in gates and A be a nonempty circuit of S such that A has denotation held in gates. Then A has a stabilization limit.

Let X be a non empty finite set and let S be a finite signature over X. One can verify that every circuit over X and S has a stabilization limit.

Now we present three schemes. The scheme 1AryDef deals with a non empty set A and a unary functor F yielding an element of A, and states that:

(i) There exists a function f from A^{1} into A such that for every element x of A holds f(⟨x⟩) = F(x), and (ii) for all functions f_{1}, f_{2} from A^{1} into A such that for every element x of A holds f_{1}(⟨x⟩) = F(x) and for every element x of A holds f_{2}(⟨x⟩) = F(x) holds f_{1} = f_{2}

for all values of the parameters.

The scheme 2AryDef deals with a non empty set A and a binary functor F yielding an element of A, and states that:

(i) There exists a function f from A^{2} into A such that for all elements x, y of A holds f(⟨x, y⟩) = F(x, y), and (ii) for all functions f_{1}, f_{2} from A^{2} into A such that for all elements x, y of A holds f_{1}(⟨x, y⟩) = F(x, y) and for all elements x, y of A holds f_{2}(⟨x, y⟩) = F(x, y) holds f_{1} = f_{2}

for all values of the parameters.

The scheme 3AryDef deals with a non empty set A and a ternary functor F yielding an element of A, and states that:

(i) There exists a function f from A^{3} into A such that for all elements x, y, z of A holds f(⟨x, y, z⟩) = F(x, y, z), and (ii) for all functions f_{1}, f_{2} from A^{3} into A such that for all elements x, y, z of A holds f_{1}(⟨x, y, z⟩) = F(x, y, z) and for all elements x, y, z of A holds f_{2}(⟨x, y, z⟩) = F(x, y, z) holds f_{1} = f_{2}

for all values of the parameters.

We now state three propositions:

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

(37) Let f be a function and x_{1}, x_{2}, x_{3}, x_{4} be sets. If x_{1} ∈ domf and x_{2} ∈ domf and x_{3} ∈ domf and x_{4} ∈ domf, then f · ⟨x_{1}, x_{2}, x_{3}, x_{4}⟩ = ⟨f(x_{1}), f(x_{2}), f(x_{3}), f(x_{4})⟩.

(38) Let f be a function and x_{1}, x_{2}, x_{3}, x_{4}, x_{5} be sets. Suppose x_{1} ∈ domf and x_{2} ∈ domf and x_{3} ∈ domf and x_{4} ∈ domf and x_{5} ∈ domf. Then f · ⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩ = ⟨f(x_{1}), f(x_{2}), f(x_{3}), f(x_{4}), f(x_{5})⟩.

Now we present several schemes. The scheme OneGate1Result deals with a set A, a non empty finite set B, a unary functor F yielding an element of B, and a function C from B^{1} into B, and states that:

For every state s of 1GateCircuit(⟨A⟩, C) and for every element a_{1} of B such that a_{1} = s(A) holds (Result(s))(Output1GateCircStr(⟨A⟩, C)) = F(a_{1})

provided the following requirement is met:

• For every function g from B^{1} into B holds g = C iff for every element a_{1} of B holds g(⟨a_{1}⟩) = F(a_{1}).

The scheme OneGate2Result deals with sets A, B, a non empty finite set C, a binary functor F yielding an element of C, and a function D from C^{2} into C, and states that:

For every state s of 1GateCircuit(⟨A, B⟩, D) and for all elements a_{1}, a_{2} of C such that a_{1} = s(A) and a_{2} = s(B) holds (Result(s))(Output1GateCircStr(⟨A, B⟩, D)) = F(a_{1}, a_{2})

provided the parameters satisfy the following condition:

• For every function g from C^{2} into C holds g = D iff for all elements a_{1}, a_{2} of C holds g(⟨a_{1}, a_{2}⟩) = F(a_{1}, a_{2}).

The scheme OneGate3Result deals with sets A, B, C, a non empty finite set D, a ternary functor F yielding an element of D, and a function E from D^{3} into D, and states that:

Let s be a state of 1GateCircuit(⟨A, B, C⟩, E) and a_{1}, a_{2}, a_{3} be elements of D. If a_{1} = s(A) and a_{2} = s(B) and a_{3} = s(C), then (Result(s))(Output1GateCircStr(⟨A, B, C⟩, E)) = F(a_{1}, a_{2}, a_{3})

provided the following requirement is met:

• For every function g from D^{3} into D holds g = E iff for all elements a_{1}, a_{2}, a_{3} of D holds g(⟨a_{1}, a_{2}, a_{3}⟩) = F(a_{1}, a_{2}, a_{3}).

The scheme OneGate4Result deals with sets A, B, C, D, a non empty finite set E, a 4-ary functor F yielding an element of E, and a function F from E^{4} into E, and states that:

Let s be a state of 1GateCircuit(⟨A, B, C, D⟩, F) and a_{1}, a_{2}, a_{3}, a_{4} be elements of E. If a_{1} = s(A) and a_{2} = s(B) and a_{3} = s(C) and a_{4} = s(D), then (Result(s))(Output1GateCircStr(⟨A, B, C, D⟩, F)) = F(a_{1}, a_{2}, a_{3}, a_{4})

provided the following condition is met:

• Let g be a function from E^{4} into E. Then g = F if and only if for all elements a_{1}, a_{2}, a_{3}, a_{4} of E holds g(⟨a_{1}, a_{2}, a_{3}, a_{4}⟩) = F(a_{1}, a_{2}, a_{3}, a_{4}).

The scheme OneGate5Result deals with sets A, B, C, D, E, a non empty finite set F, a 5-ary functor F yielding an element of F, and a function G from F^{5} into F, and states that:

Let s be a state of 1GateCircuit(⟨A, B, C, D, E⟩, G) and a_{1}, a_{2}, a_{3}, a_{4}, a_{5} be elements of F. Suppose a_{1} = s(A) and a_{2} = s(B) and a_{3} = s(C) and a_{4} = s(D) and a_{5} = s(E). Then (Result(s))(Output1GateCircStr(⟨A, B, C, D, E⟩, G)) = F(a_{1}, a_{2}, a_{3}, a_{4}, a_{5})

provided the following requirement is met:

• Let g be a function from F^{5} into F. Then g = G if and only if for all elements a_{1}, a_{2}, a_{3}, a_{4}, a_{5} of F holds g(⟨a_{1}, a_{2}, a_{3}, a_{4}, a_{5}⟩) = F(a_{1}, a_{2}, a_{3}, a_{4}, a_{5}).

4. Input of a Compound Circuit

We now state a number of propositions:

(39) Let n be a natural number, X be a non empty finite set, f be a function from X^{n} into X, p be a finite sequence with length n, and S be a signature over X. If rngp ⊆ the carrier of S and Output1GateCircStr(p, f) ∉ InputVertices(S), then InputVertices(S+·1GateCircStr(p, f)) = InputVertices(S).

(40) Let X_{1}, X_{2} be sets, X be a non empty finite set, n be a natural number, f be a function from X^{n} into X, p be a finite sequence with length n, and S be a signature over X. Suppose rngp = X_{1} ∪ X_{2} and X_{1} ⊆ the carrier of S and X_{2} misses InnerVertices(S) and Output1GateCircStr(p, f) ∉ InputVertices(S). Then InputVertices(S+·1GateCircStr(p, f)) = InputVertices(S) ∪ X_{2}.

(41) Let x_{1} be a set, X be a non empty finite set, f be a function from X^{1} into X, and S be a signature over X. If x_{1} ∈ the carrier of S and Output1GateCircStr(⟨x_{1}⟩, f) ∉ InputVertices(S), then InputVertices(S+·1GateCircStr(⟨x_{1}⟩, f)) = InputVertices(S).

(42) Let x_{1}, x_{2} be sets, X be a non empty finite set, f be a function from X^{2} into X, and S be a signature over X. Suppose x_{1} ∈ the carrier of S and x_{2} ∉ InnerVertices(S) and Output1GateCircStr(⟨x_{1}, x_{2}⟩, f) ∉ InputVertices(S). Then InputVertices(S+·1GateCircStr(⟨x_{1}, x_{2}⟩, f)) = InputVertices(S) ∪ {x_{2}}.

(43) Let x_{1}, x_{2} be sets, X be a non empty finite set, f be a function from X^{2} into X, and S be a signature over X. Suppose x_{2} ∈ the carrier of S and x_{1} ∉ InnerVertices(S) and Output1GateCircStr(⟨x_{1}, x_{2}⟩, f) ∉ InputVertices(S). Then InputVertices(S+·1GateCircStr(⟨x_{1}, x_{2}⟩, f)) = InputVertices(S) ∪ {x_{1}}.

(44) Let x_{1}, x_{2} be sets, X be a non empty finite set, f be a function from X^{2} into X, and S be a signature over X. Suppose x_{1} ∈ the carrier of S and x_{2} ∈ the carrier of S and Output1GateCircStr(⟨x_{1}, x_{2}⟩, f) ∉ InputVertices(S). Then InputVertices(S+·1GateCircStr(⟨x_{1}, x_{2}⟩, f)) = InputVertices(S).

(45) Let x_{1}, x_{2}, x_{3} be sets, X be a non empty finite set, f be a function from X^{3} into X, and S be a signature over X. Suppose x_{1} ∈ the carrier of S and x_{2} ∉ InnerVertices(S) and x_{3} ∉ InnerVertices(S) and Output1GateCircStr(⟨x_{1}, x_{2}, x_{3}⟩, f) ∉ InputVertices(S). Then InputVertices(S+·1GateCircStr(⟨x_{1}, x_{2}, x_{3}⟩, f)) = InputVertices(S) ∪ {x_{2}, x_{3}}.

(46) Let x_{1}, x_{2}, x_{3} be sets, X be a non empty finite set, f be a function from X^{3} into X, and S be a signature over X. Suppose x_{2} ∈ the carrier of S and x_{1} ∉ InnerVertices(S) and x_{3} ∉ InnerVertices(S) and Output1GateCircStr(⟨x_{1}, x_{2}, x_{3}⟩, f) ∉ InputVertices(S). Then InputVertices(S+·1GateCircStr(⟨x_{1}, x_{2}, x_{3}⟩, f)) = InputVertices(S) ∪ {x_{1}, x_{3}}.

(47) Let x_{1}, x_{2}, x_{3} be sets, X be a non empty finite set, f be a function from X^{3} into X, and S be a signature over X. Suppose x_{3} ∈ the carrier of S and x_{1} ∉ InnerVertices(S) and x_{2} ∉ InnerVertices(S) and Output1GateCircStr(⟨x_{1}, x_{2}, x_{3}⟩, f) ∉ InputVertices(S). Then InputVertices(S+·1GateCircStr(⟨x_{1}, x_{2}, x_{3}⟩, f)) = InputVertices(S) ∪ {x_{1}, x_{2}}.

(48) Let x_{1}, x_{2}, x_{3} be sets, X be a non empty finite set, f be a function from X^{3} into X, and S be a signature over X. Suppose x_{1} ∈ the carrier of S and x_{2} ∈ the carrier of S and x_{3} ∉ InnerVertices(S) and Output1GateCircStr(⟨x_{1}, x_{2}, x_{3}⟩, f) ∉ InputVertices(S). Then InputVertices(S+·1GateCircStr(⟨x_{1}, x_{2}, x_{3}⟩, f)) = InputVertices(S) ∪ {x_{3}}.

(49) Let x_{1}, x_{2}, x_{3} be sets, X be a non empty finite set, f be a function from X^{3} into X, and S be a signature over X. Suppose x_{1} ∈ the carrier of S and x_{3} ∈ the carrier of S and x_{2} ∉ InnerVertices(S) and Output1GateCircStr(⟨x_{1}, x_{2}, x_{3}⟩, f) ∉ InputVertices(S). Then InputVertices(S+·1GateCircStr(⟨x_{1}, x_{2}, x_{3}⟩, f)) = InputVertices(S) ∪ {x_{2}}.

(50) Let x_{1}, x_{2}, x_{3} be sets, X be a non empty finite set, f be a function from X^{3} into X, and S be a signature over X. Suppose x_{2} ∈ the carrier of S and x_{3} ∈ the carrier of S and x_{1} ∉ InnerVertices(S) and Output1GateCircStr(⟨x_{1}, x_{2}, x_{3}⟩, f) ∉ InputVertices(S). Then InputVertices(S+·1GateCircStr(⟨x_{1}, x_{2}, x_{3}⟩, f)) = InputVertices(S) ∪ {x_{1}}.

(51) Let x_{1}, x_{2}, x_{3} be sets, X be a non empty finite set, f be a function from X^{3} into X, and S be a signature over X. Suppose x_{1} ∈ the carrier of S and x_{2} ∈ the carrier of S and x_{3} ∈ the carrier of S and Output1GateCircStr(⟨x_{1}, x_{2}, x_{3}⟩, f) ∉ InputVertices(S). Then InputVertices(S+·1GateCircStr(⟨x_{1}, x_{2}, x_{3}⟩, f)) = InputVertices(S).

5. Result of a Compound Circuit

Next we state the proposition

(52) Let X be a non empty finite set, S be a finite signature over X, A be a circuit over X and S, n be a natural number, f be a function from X^{n} into X, and p be a finite sequence with length n. Suppose Output1GateCircStr(p, f) ∉ InputVertices(S). Let s be a state of A+·1GateCircuit(p, f) and s′ be a state of A. Suppose s′= s↾the carrier of S. Then the stabilization time of s 1 + the stabilization time of s′.

Now we present several schemes. The scheme Comb1CircResult deals with a set A, a non empty finite set B, a unary functor F yielding an element of B, a finite signature C over B, a circuit D over B and C, and a function E from B^{1} into B, and states that:

Let s be a state of D+·1GateCircuit(⟨A⟩, E) and s′ be a state of D. Suppose s′ = s↾the carrier of C. Let a_{1} be an element of B. Suppose if A ∈ InnerVertices(C), then a_{1} = (Result(s′))(A) and if A ∉ InnerVertices(C), then a_{1} = s(A). Then (Result(s))(Output1GateCircStr(⟨A⟩, E)) = F(a_{1})

provided the parameters meet the following conditions:

• For every function g from B^{1} into B holds g = E iff for every element a_{1} of B holds g(⟨a_{1}⟩) = F(a_{1}), and

• Output1GateCircStr(⟨A⟩, E) ∉ InputVertices(C). The scheme Comb2CircResult deals with sets A, B, a non empty finite set

C, a binary functor F yielding an element of C, a finite signature D over C, a circuit E over C and D, and a function F from C^{2} into C, and states that:

Let s be a state of E+·1GateCircuit(⟨A, B⟩, F) and s′ be a state of E. Suppose s′ = s↾the carrier of D. Let a_{1}, a_{2} be elements of C. Suppose if A ∈ InnerVertices(D), then a_{1} = (Result(s′))(A) and if A ∉ InnerVertices(D), then a_{1} = s(A) and if B ∈ InnerVertices(D), then a_{2} = (Result(s′))(B) and if B ∉ InnerVertices(D), then a_{2} = s(B). Then (Result(s))(Output1GateCircStr(⟨A, B⟩, F)) = F(a_{1}, a_{2})

provided the parameters meet the following requirements:

• For every function g from C^{2} into C holds g = F iff for all elements a_{1}, a_{2} of C holds g(⟨a_{1}, a_{2}⟩) = F(a_{1}, a_{2}), and

• Output1GateCircStr(⟨A, B⟩, F) ∉ InputVertices(D). The scheme Comb3CircResult deals with sets A, B, C, a non empty finite set

D, a ternary functor F yielding an element of D, a finite signature E over D, a circuit F over D and E, and a function G from D^{3} into D, and states that:

Let s be a state of F+·1GateCircuit(⟨A, B, C⟩, G) and s′be a state of F. Suppose s′= s↾the carrier of E. Let a_{1}, a_{2}, a_{3} be elements of D. Suppose that

(i) if A ∈ InnerVertices(E), then a_{1} = (Result(s′))(A), (ii) if A ∉ InnerVertices(E), then a_{1} = s(A), (iii) if B ∈ InnerVertices(E), then a_{2} = (Result(s′))(B), (iv) if B ∉ InnerVertices(E), then a_{2} = s(B),

(v) if C ∈ InnerVertices(E), then a_{3} = (Result(s′))(C), and (vi) if C ∉ InnerVertices(E), then a_{3} = s(C).

Then (Result(s))(Output1GateCircStr(⟨A, B, C⟩, G)) = F(a_{1}, a_{2}, a_{3})

provided the parameters meet the following requirements:

• For every function g from D^{3} into D holds g = G iff for all elements a_{1}, a_{2}, a_{3} of D holds g(⟨a_{1}, a_{2}, a_{3}⟩) = F(a_{1}, a_{2}, a_{3}), and

• Output1GateCircStr(⟨A, B, C⟩, G) ∉ InputVertices(E). The scheme Comb4CircResult deals with sets A, B, C, D, a non empty finite

set E, a 4-ary functor F yielding an element of E, a finite signature F over E, a circuit G over E and F, and a function H from E^{4} into E, and states that:

Let s be a state of G+·1GateCircuit(⟨A, B, C, D⟩, H) and s′ be a state of G. Suppose s′ = s↾the carrier of F. Let a_{1}, a_{2}, a_{3}, a_{4} be elements of E. Suppose that if A ∈ InnerVertices(F), then a_{1} = (Result(s′))(A) and if A ∉ InnerVertices(F), then a_{1} = s(A) and if B ∈ InnerVertices(F), then a_{2} = (Result(s′))(B) and if B ∉ InnerVertices(F), then a_{2} = s(B) and if C ∈ InnerVertices(F), then a_{3} = (Result(s′))(C) and if C ∉ InnerVertices(F), then a_{3} = s(C) and if D ∈ InnerVertices(F), then a_{4} = (Result(s′))(D) and if D ∉ InnerVertices(F), then a_{4} = s(D). Then (Result(s))(Output1GateCircStr(⟨A, B, C, D⟩, H)) = F(a_{1}, a_{2}, a_{3}, a_{4}) provided the parameters satisfy the following conditions:

• Let g be a function from E^{4} into E. Then g = H if and only if for all elements a_{1}, a_{2}, a_{3}, a_{4} of E holds g(⟨a_{1}, a_{2}, a_{3}, a_{4}⟩) = F(a_{1}, a_{2}, a_{3}, a_{4}), and

• Output1GateCircStr(⟨A, B, C, D⟩, H) ∉ InputVertices(F). The scheme Comb5CircResult deals with sets A, B, C, D, E, a non empty

finite set F, a 5-ary functor F yielding an element of F, a finite signature G over F, a circuit H over F and G, and a function I from F^{5} into F, and states that:

Let s be a state of H+·1GateCircuit(⟨A, B, C, D, E⟩, I) and s′ be a state of H. Suppose s′ = s↾the carrier of G. Let a_{1}, a_{2}, a_{3}, a_{4}, a_{5} be elements of F. Suppose that if A ∈ InnerVertices(G), then a_{1} = (Result(s′))(A) and if A ∉ InnerVertices(G), then a_{1} = s(A) and if B ∈ InnerVertices(G), then a_{2} = (Result(s′))(B) and if B ∉ InnerVertices(G), then a_{2} = s(B) and if C ∈ InnerVertices(G), then a_{3} = (Result(s′))(C) and if C ∉ InnerVertices(G), then a_{3} = s(C) and if D ∈ InnerVertices(G), then a_{4} = (Result(s′))(D) and if D ∉ InnerVertices(G), then a_{4} = s(D) and if E ∈ InnerVertices(G), then a_{5} = (Result(s′))(E) and if E ∉ InnerVertices(G), then a_{5} = s(E). Then (Result(s))(Output1GateCircStr(⟨A, B, C, D, E⟩, I)) = F(a_{1}, a_{2}, a_{3}, a_{4}, a_{5})

provided the parameters meet the following conditions:

• Let g be a function from F^{5} into F. Then g = I if and only if for all elements a_{1}, a_{2}, a_{3}, a_{4}, a_{5} of F holds g(⟨a_{1}, a_{2}, a_{3}, a_{4}, a_{5}⟩) = F(a_{1}, a_{2}, a_{3}, a_{4}, a_{5}), and

• Output1GateCircStr(⟨A, B, C, D, E⟩, I) ∉ InputVertices(G).

6. Inputs Without Pairs

Let S be a non empty many sorted signature. We say that S has nonpair inputs if and only if:

(Def. 11) InputVertices(S) has no pairs.

Note that ℕ has no pairs. Let X be a set with no pairs. Note that every subset of X has no pairs.

Let us observe that every function which is natural-yielding is also nonpair yielding.

Let us note that every finite sequence of elements of ℕ is natural-yielding. Let us observe that there exists a finite sequence which is one-to-one and

natural-yielding.

Let n be a natural number. Observe that there exists a finite sequence with length n which is one-to-one and natural-yielding.

Let p be a nonpair yielding finite sequence and let f be a set. Observe that 1GateCircStr(p, f) has nonpair inputs.

One can verify that there exists an one-gate many sorted signature which has nonpair inputs. Let X be a non empty finite set. One can verify that there exists an one-gate signature over X which has nonpair inputs.

Let S be a non empty many sorted signature with nonpair inputs. One can check that InputVertices(S) has no pairs.

The following proposition is true

(53) Let S be a non empty many sorted signature with nonpair inputs and x

be a vertex of S. If x is pair, then x ∈ InnerVertices(S). Let S be an unsplit non empty many sorted signature with arity held in

gates. One can verify that InnerVertices(S) is relation-like.

Let S be an unsplit non empty non void many sorted signature with denotation held in gates. Note that InnerVertices(S) is relation-like.

Let S_{1}, S_{2} be unsplit non empty many sorted signatures with arity held in gates with nonpair inputs. One can verify that S_{1}+·S_{2} has nonpair inputs.

One can prove the following propositions:

(54) For every non pair set x and for every binary relation R holds x ∉ R.

(55) Let x_{1} be a set, X be a non empty finite set, f be a function from X^{1} into X, and S be a signature over X with nonpair inputs. If x_{1} ∈ the carrier of S or x_{1} is non pair, then S+·1GateCircStr(⟨x_{1}⟩, f) has nonpair inputs.

Let X be a non empty finite set, let S be a signature over X with nonpair inputs, let x_{1} be a vertex of S, and let f be a function from X^{1} into X. One can verify that S+·1GateCircStr(⟨x_{1}⟩, f) has nonpair inputs.

Let X be a non empty finite set, let S be a signature over X with nonpair inputs, let x_{1} be a non pair set, and let f be a function from X^{1} into X. One can verify that S+·1GateCircStr(⟨x_{1}⟩, f) has nonpair inputs.

We now state the proposition

(56) Let x_{1}, x_{2} be sets, X be a non empty finite set, f be a function from X^{2} into X, and S be a signature over X with nonpair inputs. Suppose x_{1} ∈ the carrier of S or x_{1} is non pair but x_{2} ∈ the carrier of S or x_{2} is non pair. Then S+·1GateCircStr(⟨x_{1}, x_{2}⟩, f) has nonpair inputs.

Let X be a non empty finite set, let S be a signature over X with nonpair inputs, let x_{1} be a vertex of S, let n_{2} be a non pair set, and let f be a function from X^{2} into X. Observe that S+·1GateCircStr(⟨x_{1}, n_{2}⟩, f) has nonpair inputs and S+·1GateCircStr(⟨n_{2}, x_{1}⟩, f) has nonpair inputs.

Let X be a non empty finite set, let S be a signature over X with nonpair inputs, let x_{1}, x_{2} be vertices of S, and let f be a function from X^{2} into X. One can verify that S+·1GateCircStr(⟨x_{1}, x_{2}⟩, f) has nonpair inputs.

One can prove the following proposition 132 grzegorz bancerek and adam naumowicz

(57) Let x_{1}, x_{2}, x_{3} be sets, X be a non empty finite set, f be a function from X^{3} into X, and S be a signature over X with nonpair inputs. Suppose that

(i) x_{1} ∈ the carrier of S or x_{1} is non pair, (ii) x_{2} ∈ the carrier of S or x_{2} is non pair, and (iii) x_{3} ∈ the carrier of S or x_{3} is non pair.

Then S+·1GateCircStr(⟨x_{1}, x_{2}, x_{3}⟩, f) has nonpair inputs. Let X be a non empty finite set, let S be a signature over X with nonpair

inputs, let x_{1}, x_{2} be vertices of S, let n be a non pair set, and let f be a function from X^{3} into X. One can verify the following observations:

∗ S+·1GateCircStr(⟨x_{1}, x_{2}, n⟩, f) has nonpair inputs,

∗ S+·1GateCircStr(⟨x_{1}, n, x_{2}⟩, f) has nonpair inputs, and

∗ S+·1GateCircStr(⟨n, x_{1}, x_{2}⟩, f) has nonpair inputs. Let X be a non empty finite set, let S be a signature over X with nonpair

inputs, let x be a vertex of S, let n_{1}, n_{2} be non pair sets, and let f be a function from X^{3} into X. One can check the following observations:

∗ S+·1GateCircStr(⟨x, n_{1}, n_{2}⟩, f) has nonpair inputs,

∗ S+·1GateCircStr(⟨n_{1}, x, n_{2}⟩, f) has nonpair inputs, and

∗ S+·1GateCircStr(⟨n_{1}, n_{2}, x⟩, f) has nonpair inputs. Let X be a non empty finite set, let S be a signature over X with nonpair

inputs, let x_{1}, x_{2}, x_{3} be vertices of S, and let f be a function from X^{3} into X. Observe that S+·1GateCircStr(⟨x_{1}, x_{2}, x_{3}⟩, f) has nonpair inputs.

References

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

[2] Grzegorz Bancerek. Sequences of ordinal numbers. Formalized Mathematics, 1(2):281– 290, 1990.

[3] Grzegorz Bancerek. Tarski’s classes and ranks. Formalized Mathematics, 1(3):563–567, 1990.

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

[5] Grzegorz Bancerek and Yatsuka Nakamura. Full adder circuit. Part I. Formalized Mathematics, 5(3):367–380, 1996.

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

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

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

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

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

[11] Jing-Chao Chen. A small computer model with push-down stack. Formalized Mathematics, 8(1):175–182, 1999.

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

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

preliminaries to automatic generation … 133

[14] Jarosław Kotowicz. The limit of a real function at infinity. Formalized Mathematics, 2(1):17–28, 1991.

[15] Yatsuka Nakamura and Grzegorz Bancerek. Combining of circuits. Formalized Mathematics, 5(2):283–295, 1996.

[16] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Introduction to circuits, II. Formalized Mathematics, 5(2):273–278, 1996.

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

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

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

[20] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25–34, 1990.

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

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

[23] Andrzej Trybulec. Many sorted algebras. Formalized Mathematics, 5(1):37–42, 1996.

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

[25] Wojciech A. Trybulec. Groups. Formalized Mathematics, 1(5):821–827, 1990.

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

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

Received July 26, 2002

Properties of the Upper and Lower Sequence on the Cage^{1}

Robert Milewski University of Białystok

MML Identifier: JORDAN15.

The terminology and notation used here are introduced in the following articles: [24], [27], [1], [3], [4], [2], [14], [12], [25], [22], [23], [11], [21], [8], [9], [6], [26], [15], [10], [18], [17], [5], [20], [19], [7], [13], and [16].

In this paper n is a natural number. We now state a number of propositions:

(1) For all subsets A, B of E_{T}^{2} such that A meets B holds proj1^{∘} A meets proj1^{∘} B.

(2) Let A, B be subsets of E_{T}^{2} and s be a real number. If A misses B and A ⊆ HorizontalLines and B ⊆ HorizontalLines, then proj1^{∘} A misses proj1^{∘} B.

(3) For every closed subset S of E_{T}^{2} such that S is Bounded holds proj1^{∘} S is closed.

(4) For every compact subset S of E_{T}^{2} holds proj1^{∘} S is compact.

(5) Let p, q, p_{1}, q_{1} be points of E_{T}^{2}. Suppose L(p, q) is vertical and L(p_{1}, q_{1}) is vertical and p_{1} = (p_{1})_{1} and p_{2} (p_{1})_{2} and (p_{1})_{2} (q_{1})_{2} and (q_{1})_{2} q_{2}. Then L(p_{1}, q_{1}) ⊆ L(p, q).

(6) Let p, q, p_{1}, q_{1} be points of E_{T}^{2}. Suppose L(p, q) is horizontal and L(p_{1}, q_{1}) is horizontal and p_{2} = (p_{1})_{2} and p_{1} (p_{1})_{1} and (p_{1})_{1} (q_{1})_{1} and (q_{1})_{1} q_{1}. Then L(p_{1}, q_{1}) ⊆ L(p, q).

(7) Let G be a Go-board and i, j, k, j_{1}, k_{1} be natural numbers. Suppose 1 i and i lenG and 1 j and j j_{1} and j_{1} k_{1} and k_{1} k and k widthG. Then L(G ∘ (i, j_{1}), G ∘ (i, k_{1})) ⊆ L(G ∘ (i, j), G ∘ (i, k)).

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

(8) Let G be a Go-board and i, j, k, j_{1}, k_{1} be natural numbers. Suppose 1 i and i widthG and 1 j and j j_{1} and j_{1} k_{1} and k_{1} k and k lenG. Then L(G ∘ (j_{1}, i), G ∘ (k_{1}, i)) ⊆ L(G ∘ (j, i), G ∘ (k, i)).

(9) Let G be a Go-board and j, k, j_{1}, k_{1} be natural numbers. Suppose 1 j and j j_{1} and j_{1} k_{1} and k_{1} k and k widthG. Then L(G ∘ (CenterG, j_{1}), G∘(CenterG, k_{1})) ⊆ L(G∘(CenterG, j), G∘(CenterG, k)).

(10) Let G be a Go-board. Suppose lenG = widthG. Let j, k, j_{1}, k_{1} be natural numbers. Suppose 1 j and j j_{1} and j_{1} k_{1} and k_{1} k and k lenG. Then L(G ∘ (j_{1}, CenterG), G ∘ (k_{1}, CenterG)) ⊆ L(G ∘ (j, CenterG), G ∘ (k, CenterG)).

(11) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2} and i, j, k be natural numbers. Suppose 1 i and i lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and Gauge(C, n) ∘ (i, j) ∈ L̃(LowerSeq(C, n)). Then there exists a natural number j_{1} such that j j_{1} and j_{1} k and L(Gauge(C, n) ∘ (i, j_{1}), Gauge(C, n) ∘ (i, k)) ∩ L̃(LowerSeq(C, n)) = {Gauge(C, n) ∘ (i, j_{1})}.

(12) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2} and i, j, k be natural numbers. Suppose 1 i and i lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and Gauge(C, n) ∘ (i, k) ∈ L̃(UpperSeq(C, n)). Then there exists a natural number k_{1} such that j k_{1} and k_{1} k and L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k_{1})) ∩ L̃(UpperSeq(C, n)) = {Gauge(C, n) ∘ (i, k_{1})}.

(13) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2} and i, j, k be natural numbers. Suppose 1 i and i lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and Gauge(C, n)∘(i, j) ∈ L̃(LowerSeq(C, n)) and Gauge(C, n) ∘ (i, k) ∈ L̃(UpperSeq(C, n)). Then there exist natural numbers j_{1}, k_{1} such that j j_{1} and j_{1} k_{1} and k_{1} k and L(Gauge(C, n) ∘ (i, j_{1}), Gauge(C, n) ∘ (i, k_{1})) ∩ L̃(LowerSeq(C, n)) = {Gauge(C, n) ∘ (i, j_{1})} and L(Gauge(C, n) ∘ (i, j_{1}), Gauge(C, n) ∘ (i, k_{1})) ∩ L̃(UpperSeq(C, n)) = {Gauge(C, n) ∘ (i, k_{1})}.

(14) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2} and i, j, k be natural numbers. Suppose 1 j and j k and k lenGauge(C, n) and 1 i and i widthGauge(C, n) and Gauge(C, n) ∘ (j, i) ∈ L̃(LowerSeq(C, n)). Then there exists a natural number j_{1} such that j j_{1} and j_{1} k and L(Gauge(C, n) ∘ (j_{1}, i), Gauge(C, n) ∘ (k, i)) ∩ L̃(LowerSeq(C, n)) = {Gauge(C, n) ∘ (j_{1}, i)}.

(15) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2} and i, j, k be natural numbers. Suppose 1 j and j k and k lenGauge(C, n) and 1 i and i widthGauge(C, n) and Gauge(C, n) ∘ (k, i) ∈ L̃(UpperSeq(C, n)). Then there exists a natural number k_{1} such that j k_{1} and k_{1} k and L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k_{1}, i)) ∩

L̃(UpperSeq(C, n)) = {Gauge(C, n) ∘ (k_{1}, i)}.

(16) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2} and i, j, k be natural numbers. Suppose 1 j and j k and k lenGauge(C, n) and 1 i and i widthGauge(C, n) and Gauge(C, n) ∘ (j, i) ∈ L̃(LowerSeq(C, n)) and Gauge(C, n) ∘ (k, i) ∈ L̃(UpperSeq(C, n)). Then there exist natural numbers j_{1}, k_{1} such that j j_{1} and j_{1} k_{1} and k_{1} k and L(Gauge(C, n) ∘ (j_{1}, i), Gauge(C, n) ∘ (k_{1}, i))∩L̃(LowerSeq(C, n)) = {Gauge(C, n)∘(j_{1}, i)} and L(Gauge(C, n)∘ (j_{1}, i), Gauge(C, n)∘(k_{1}, i))∩L̃(UpperSeq(C, n)) = {Gauge(C, n)∘(k_{1}, i)}.

(17) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2} and i, j, k be natural numbers. Suppose 1 i and i lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and Gauge(C, n) ∘ (i, j) ∈ L̃(UpperSeq(C, n)). Then there exists a natural number j_{1} such that j j_{1} and j_{1} k and L(Gauge(C, n) ∘ (i, j_{1}), Gauge(C, n) ∘ (i, k)) ∩ L̃(UpperSeq(C, n)) = {Gauge(C, n) ∘ (i, j_{1})}.

(18) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2} and i, j, k be natural numbers. Suppose 1 i and i lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and Gauge(C, n) ∘ (i, k) ∈ L̃(LowerSeq(C, n)). Then there exists a natural number k_{1} such that j k_{1} and k_{1} k and L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k_{1})) ∩ L̃(LowerSeq(C, n)) = {Gauge(C, n) ∘ (i, k_{1})}.

(19) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2} and i, j, k be natural numbers. Suppose 1 i and i lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and Gauge(C, n)∘(i, j) ∈ L̃(UpperSeq(C, n)) and Gauge(C, n) ∘ (i, k) ∈ L̃(LowerSeq(C, n)). Then there exist natural numbers j_{1}, k_{1} such that j j_{1} and j_{1} k_{1} and k_{1} k and L(Gauge(C, n) ∘ (i, j_{1}), Gauge(C, n) ∘ (i, k_{1})) ∩ L̃(UpperSeq(C, n)) = {Gauge(C, n) ∘ (i, j_{1})} and L(Gauge(C, n) ∘ (i, j_{1}), Gauge(C, n) ∘ (i, k_{1})) ∩ L̃(LowerSeq(C, n)) = {Gauge(C, n) ∘ (i, k_{1})}.

(20) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2} and i, j, k be natural numbers. Suppose 1 j and j k and k lenGauge(C, n) and 1 i and i widthGauge(C, n) and Gauge(C, n) ∘ (j, i) ∈ L̃(UpperSeq(C, n)). Then there exists a natural number j_{1} such that j j_{1} and j_{1} k and L(Gauge(C, n) ∘ (j_{1}, i), Gauge(C, n) ∘ (k, i)) ∩ L̃(UpperSeq(C, n)) = {Gauge(C, n) ∘ (j_{1}, i)}.

(21) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2} and i, j, k be natural numbers. Suppose 1 j and j k and k lenGauge(C, n) and 1 i and i widthGauge(C, n) and Gauge(C, n) ∘ (k, i) ∈ L̃(LowerSeq(C, n)). Then there exists a natural number k_{1} such that j k_{1} and k_{1} k and L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k_{1}, i)) ∩ L̃(LowerSeq(C, n)) = {Gauge(C, n) ∘ (k_{1}, i)}.

(22) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2} and i, j, k be natural numbers. Suppose 1 j and j k and k lenGauge(C, n) and 1 i and i widthGauge(C, n) and Gauge(C, n) ∘ (j, i) ∈ L̃(UpperSeq(C, n)) and Gauge(C, n) ∘ (k, i) ∈ L̃(LowerSeq(C, n)). Then there exist natural numbers j_{1}, k_{1} such that j j_{1} and j_{1} k_{1} and k_{1} k and L(Gauge(C, n) ∘ (j_{1}, i), Gauge(C, n) ∘ (k_{1}, i))∩L̃(UpperSeq(C, n)) = {Gauge(C, n)∘(j_{1}, i)} and L(Gauge(C, n)∘ (j_{1}, i), Gauge(C, n)∘(k_{1}, i))∩L̃(LowerSeq(C, n)) = {Gauge(C, n)∘(k_{1}, i)}.

(23) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < i and i < lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and Gauge(C, n) ∘ (i, k) ∈ L̃(UpperSeq(C, n)) and Gauge(C, n) ∘ (i, j) ∈ L̃(LowerSeq(C, n)). Then L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) meets LowerArcC.

(24) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < i and i < lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and Gauge(C, n) ∘ (i, k) ∈ L̃(UpperSeq(C, n)) and Gauge(C, n) ∘ (i, j) ∈ L̃(LowerSeq(C, n)). Then L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) meets UpperArcC.

(25) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < i and i < lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and n > 0 and Gauge(C, n) ∘ (i, k) ∈ UpperArc L̃(Cage(C, n)) and Gauge(C, n) ∘ (i, j) ∈ LowerArc L̃(Cage(C, n)). Then L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) meets LowerArcC.

(26) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < i and i < lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and n > 0 and Gauge(C, n) ∘ (i, k) ∈ UpperArc L̃(Cage(C, n)) and Gauge(C, n) ∘ (i, j) ∈ LowerArc L̃(Cage(C, n)). Then L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) meets UpperArcC.

(27) Let C be a simple closed curve and j, k be natural numbers. Suppose 1 j and j k and k widthGauge(C, n + 1) and Gauge(C, n + 1) ∘ (CenterGauge(C, n + 1), k) ∈ UpperArc L̃(Cage(C, n + 1)) and Gauge(C, n+1)∘(CenterGauge(C, n+1), j) ∈ LowerArc L̃(Cage(C, n+1)). Then L(Gauge(C, n + 1) ∘ (CenterGauge(C, n + 1), j), Gauge(C, n + 1) ∘ (CenterGauge(C, n + 1), k)) meets LowerArcC.

(28) Let C be a simple closed curve and j, k be natural numbers. Suppose 1 j and j k and k widthGauge(C, n + 1) and Gauge(C, n + 1) ∘ (CenterGauge(C, n + 1), k) ∈ UpperArc L̃(Cage(C, n + 1)) and Gauge(C, n+1)∘(CenterGauge(C, n+1), j) ∈ LowerArc L̃(Cage(C, n+1)). Then L(Gauge(C, n + 1) ∘ (CenterGauge(C, n + 1), j), Gauge(C, n + 1) ∘

(CenterGauge(C, n + 1), k)) meets UpperArcC.

(29) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2} and i, j, k be natural numbers. Suppose 1 < j and k < lenGauge(C, n) and 1 i and i widthGauge(C, n) and Gauge(C, n) ∘ (k, i) ∈ L̃(UpperSeq(C, n)) and Gauge(C, n) ∘ (j, i) ∈ L̃(LowerSeq(C, n)). Then j ≠ k.

(30) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < j and j k and k < lenGauge(C, n) and 1 i and i widthGauge(C, n) and L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k, i)) ∩ L̃(UpperSeq(C, n)) = {Gauge(C, n) ∘ (k, i)} and L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k, i)) ∩ L̃(LowerSeq(C, n)) = {Gauge(C, n) ∘ (j, i)}. Then L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k, i)) meets LowerArcC.

(31) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < j and j k and k < lenGauge(C, n) and 1 i and i widthGauge(C, n) and L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k, i)) ∩ L̃(UpperSeq(C, n)) = {Gauge(C, n) ∘ (k, i)} and L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k, i)) ∩ L̃(LowerSeq(C, n)) = {Gauge(C, n) ∘ (j, i)}. Then L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k, i)) meets UpperArcC.

(32) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < j and j k and k < lenGauge(C, n) and 1 i and i widthGauge(C, n) and Gauge(C, n) ∘ (k, i) ∈ L̃(UpperSeq(C, n)) and Gauge(C, n) ∘ (j, i) ∈ L̃(LowerSeq(C, n)). Then L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k, i)) meets LowerArcC.

(33) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < j and j k and k < lenGauge(C, n) and 1 i and i widthGauge(C, n) and Gauge(C, n) ∘ (k, i) ∈ L̃(UpperSeq(C, n)) and Gauge(C, n) ∘ (j, i) ∈ L̃(LowerSeq(C, n)). Then L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k, i)) meets UpperArcC.

(34) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < j and j k and k < lenGauge(C, n) and 1 i and i widthGauge(C, n) and n > 0 and Gauge(C, n) ∘ (k, i) ∈ UpperArc L̃(Cage(C, n)) and Gauge(C, n) ∘ (j, i) ∈ LowerArc L̃(Cage(C, n)). Then L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k, i)) meets LowerArcC.

(35) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < j and j k and k < lenGauge(C, n) and 1 i and i widthGauge(C, n) and n > 0 and Gauge(C, n) ∘ (k, i) ∈ UpperArc L̃(Cage(C, n)) and Gauge(C, n) ∘ (j, i) ∈ LowerArc L̃(Cage(C, n)). Then L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k, i)) meets UpperArcC.

(36) Let C be a simple closed curve and j, k be natural numbers. Suppose 1 < j and j k and k < lenGauge(C, n + 1) and Gauge(C, n + 1) ∘ (k, CenterGauge(C, n + 1)) ∈ UpperArc L̃(Cage(C, n + 1)) and Gauge(C, n+1)∘(j, CenterGauge(C, n+1)) ∈ LowerArc L̃(Cage(C, n+1)). Then L(Gauge(C, n + 1) ∘ (j, CenterGauge(C, n + 1)), Gauge(C, n + 1) ∘ (k, CenterGauge(C, n + 1))) meets LowerArcC.

(37) Let C be a simple closed curve and j, k be natural numbers. Suppose 1 < j and j k and k < lenGauge(C, n + 1) and Gauge(C, n + 1) ∘ (k, CenterGauge(C, n + 1)) ∈ UpperArc L̃(Cage(C, n + 1)) and Gauge(C, n+1)∘(j, CenterGauge(C, n+1)) ∈ LowerArc L̃(Cage(C, n+1)). Then L(Gauge(C, n + 1) ∘ (j, CenterGauge(C, n + 1)), Gauge(C, n + 1) ∘ (k, CenterGauge(C, n + 1))) meets UpperArcC.

(38) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < j and j k and k < lenGauge(C, n) and 1 i and i widthGauge(C, n) and L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k, i)) ∩ L̃(UpperSeq(C, n)) = {Gauge(C, n) ∘ (j, i)} and L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k, i)) ∩ L̃(LowerSeq(C, n)) = {Gauge(C, n) ∘ (k, i)}. Then L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k, i)) meets LowerArcC.

(39) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < j and j k and k < lenGauge(C, n) and 1 i and i widthGauge(C, n) and L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k, i)) ∩ L̃(UpperSeq(C, n)) = {Gauge(C, n) ∘ (j, i)} and L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k, i)) ∩ L̃(LowerSeq(C, n)) = {Gauge(C, n) ∘ (k, i)}. Then L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k, i)) meets UpperArcC.

(40) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < j and j k and k < lenGauge(C, n) and 1 i and i widthGauge(C, n) and Gauge(C, n) ∘ (j, i) ∈ L̃(UpperSeq(C, n)) and Gauge(C, n) ∘ (k, i) ∈ L̃(LowerSeq(C, n)). Then L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k, i)) meets LowerArcC.

(41) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < j and j k and k < lenGauge(C, n) and 1 i and i widthGauge(C, n) and Gauge(C, n) ∘ (j, i) ∈ L̃(UpperSeq(C, n)) and Gauge(C, n) ∘ (k, i) ∈ L̃(LowerSeq(C, n)). Then L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k, i)) meets UpperArcC.

(42) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < j and j k and k < lenGauge(C, n) and 1 i and i widthGauge(C, n) and n > 0 and Gauge(C, n) ∘ (j, i) ∈ UpperArc L̃(Cage(C, n)) and Gauge(C, n) ∘ (k, i) ∈ LowerArc L̃(Cage(C, n)). Then L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k, i)) meets LowerArcC.

(43) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < j and j k and k < lenGauge(C, n)

and 1  i and i  widthGauge(C, n) and n > 0 and

Gauge(C, n) ∘ (j, i) ∈ UpperArc L̃(Cage(C, n)) and Gauge(C, n) ∘ (k, i) ∈ LowerArc L̃(Cage(C, n)). Then L(Gauge(C, n) ∘ (j, i), Gauge(C, n) ∘ (k, i)) meets UpperArcC.

(44) Let C be a simple closed curve and j, k be natural numbers. Suppose 1 < j and j k and k < lenGauge(C, n + 1) and Gauge(C, n + 1) ∘ (j, CenterGauge(C, n + 1)) ∈ UpperArc L̃(Cage(C, n + 1)) and Gauge(C, n+1)∘(k, CenterGauge(C, n+1)) ∈ LowerArc L̃(Cage(C, n+1)). Then L(Gauge(C, n + 1) ∘ (j, CenterGauge(C, n + 1)), Gauge(C, n + 1) ∘ (k, CenterGauge(C, n + 1))) meets LowerArcC.

(45) Let C be a simple closed curve and j, k be natural numbers. Suppose 1 < j and j k and k < lenGauge(C, n + 1) and Gauge(C, n + 1) ∘ (j, CenterGauge(C, n + 1)) ∈ UpperArc L̃(Cage(C, n + 1)) and Gauge(C, n+1)∘(k, CenterGauge(C, n+1)) ∈ LowerArc L̃(Cage(C, n+1)). Then L(Gauge(C, n + 1) ∘ (j, CenterGauge(C, n + 1)), Gauge(C, n + 1) ∘ (k, CenterGauge(C, n + 1))) meets UpperArcC.

(46) Let C be a simple closed curve and i_{1}, i_{2}, j, k be natural numbers. Suppose that 1 < i_{1} and i_{1} i_{2} and i_{2} < lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and (L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n)∘(i_{2}, k)))∩L̃(UpperSeq(C, n)) = {Gauge(C, n)∘(i_{2}, k)} and (L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n)∘(i_{2}, k)))∩L̃(LowerSeq(C, n)) = {Gauge(C, n)∘(i_{1}, j)}. Then L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n) ∘ (i_{2}, k)) meets UpperArcC.

(47) Let C be a simple closed curve and i_{1}, i_{2}, j, k be natural numbers. Suppose that 1 < i_{1} and i_{1} i_{2} and i_{2} < lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and (L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n)∘(i_{2}, k)))∩L̃(UpperSeq(C, n)) = {Gauge(C, n)∘(i_{2}, k)} and (L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n)∘(i_{2}, k)))∩L̃(LowerSeq(C, n)) = {Gauge(C, n)∘(i_{1}, j)}. Then L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n) ∘ (i_{2}, k)) meets LowerArcC.

(48) Let C be a simple closed curve and i_{1}, i_{2}, j, k be natural numbers. Suppose that 1 < i_{2} and i_{2} i_{1} and i_{1} < lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and (L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n)∘(i_{2}, k)))∩L̃(UpperSeq(C, n)) = {Gauge(C, n)∘(i_{2}, k)} and (L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n)∘(i_{2}, k)))∩L̃(LowerSeq(C, n)) = {Gauge(C, n)∘(i_{1}, j)}.

Then L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n) ∘ (i_{2}, k)) meets UpperArcC.

(49) Let C be a simple closed curve and i_{1}, i_{2}, j, k be natural numbers. Suppose that 1 < i_{2} and i_{2} i_{1} and i_{1} < lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and (L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n)∘(i_{2}, k)))∩L̃(UpperSeq(C, n)) = {Gauge(C, n)∘(i_{2}, k)} and (L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n)∘(i_{2}, k)))∩L̃(LowerSeq(C, n)) = {Gauge(C, n)∘(i_{1}, j)}. Then L(Gauge(C, n) ∘ (i_{1}, j), Gauge(C, n) ∘ (i_{1}, k)) ∪ L(Gauge(C, n) ∘ (i_{1}, k), Gauge(C, n) ∘ (i_{2}, k)) meets LowerArcC.

(50) Let C be a simple closed curve and i_{1}, i_{2}, j, k be natural numbers. Suppose that 1 < i_{1} and i_{1} < lenGauge(C, n + 1) and 1 < i_{2} and i_{2} < lenGauge(C, n+1) and 1 j and j k and k widthGauge(C, n+1) and Gauge(C, n + 1) ∘ (i_{1}, k) ∈ UpperArc L̃(Cage(C, n + 1)) and Gauge(C, n + 1) ∘ (i_{2}, j) ∈ LowerArc L̃(Cage(C, n + 1)). Then L(Gauge(C, n + 1) ∘ (i_{2}, j), Gauge(C, n + 1) ∘ (i_{2}, k)) ∪ L(Gauge(C, n + 1) ∘ (i_{2}, k), Gauge(C, n + 1) ∘ (i_{1}, k)) meets UpperArcC.

(51) Let C be a simple closed curve and i_{1}, i_{2}, j, k be natural numbers. Suppose that 1 < i_{1} and i_{1} < lenGauge(C, n + 1) and 1 < i_{2} and i_{2} < lenGauge(C, n+1) and 1 j and j k and k widthGauge(C, n+1) and Gauge(C, n + 1) ∘ (i_{1}, k) ∈ UpperArc L̃(Cage(C, n + 1)) and Gauge(C, n + 1) ∘ (i_{2}, j) ∈ LowerArc L̃(Cage(C, n + 1)). Then L(Gauge(C, n + 1) ∘ (i_{2}, j), Gauge(C, n + 1) ∘ (i_{2}, k)) ∪ L(Gauge(C, n + 1) ∘ (i_{2}, k), Gauge(C, n + 1) ∘ (i_{1}, k)) meets LowerArcC.

(52) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < i and i < lenGauge(C, n + 1) and 1 j and j k and k widthGauge(C, n + 1) and Gauge(C, n + 1) ∘ (i, k) ∈ UpperArc L̃(Cage(C, n + 1)) and Gauge(C, n + 1) ∘ (CenterGauge(C, n + 1), j) ∈ LowerArc L̃(Cage(C, n + 1)). Then L(Gauge(C, n + 1) ∘ (CenterGauge(C, n+1), j), Gauge(C, n+1)∘(CenterGauge(C, n+1), k))∪ L(Gauge(C, n + 1) ∘ (CenterGauge(C, n + 1), k), Gauge(C, n + 1) ∘ (i, k)) meets UpperArcC.

(53) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < i and i < lenGauge(C, n + 1) and 1 j and j k and k widthGauge(C, n + 1) and Gauge(C, n + 1) ∘ (i, k) ∈ UpperArc L̃(Cage(C, n + 1)) and Gauge(C, n + 1) ∘ (CenterGauge(C, n + 1), j) ∈ LowerArc L̃(Cage(C, n + 1)). Then L(Gauge(C, n + 1) ∘ (CenterGauge(C, n+1), j), Gauge(C, n+1)∘(CenterGauge(C, n+1), k))∪ L(Gauge(C, n + 1) ∘ (CenterGauge(C, n + 1), k), Gauge(C, n + 1) ∘ (i, k)) meets LowerArcC. properties of the upper and lower sequence … 143

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. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 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.

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

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

[14] Jarosław Kotowicz. Convergent real sequences. Upper and lower bound of sets of real numbers. Formalized Mathematics, 1(3):477–481, 1990.

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

[16] Robert Milewski. Upper and lower sequence of a cage. Formalized Mathematics, 9(4):787– 790, 2001.

[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] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990.

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

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

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

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

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

On the Decompositions of Intervals and Simple Closed Curves^{1}

Adam Grabowski University of Białystok

Summary. The aim of the paper is to show that the only subcontinua of the Jordan curve are arcs, the whole curve, and singletons of its points. Additionally, it has been shown that the only subcontinua of the unit interval 𝕀 are closed intervals.

MML Identifier: BORSUK 4.

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

1. Preliminaries

Let us note that every simple closed curve is non trivial.

Let T be a non empty topological space. One can check that there exists a subset of T which is non empty, compact, and connected.

Let us observe that every element of the carrier of 𝕀 is real.

Next we state two propositions:

(1) Let X be a non empty set and A, B be non empty subsets of X. If A ⊂ B, then there exists an element p of X such that p ∈ B and A ⊆ B \ {p}.

(2) Let X be a non empty set and A be a non empty subset of X. Then A is trivial if and only if there exists an element x of X such that A = {x}.

1This work has been partially supported by the European Community TYPES grant IST-1999-29001 and CALCULEMUS grant HPRN-CT-2000-00102.

Let T be a non trivial 1-sorted structure. Observe that there exists a subset of the carrier of T which is non trivial.

The following proposition is true

(3) For every non trivial set X and for every set p there exists an element q of X such that q ≠ p.

Let X be a non trivial set. Observe that there exists a subset of X which is non trivial.

We now state a number of propositions:

(4) Let T be a non trivial set, X be a non trivial subset of T, and p be a set. Then there exists an element q of T such that q ∈ X and q ≠ p.

(5) Let f, g be functions and a be a set. Suppose f is one-to-one and g is one-to-one and domf ∩ domg = {a} and rngf ∩ rngg = {f(a)}. Then f+·g is one-to-one.

(6) Let f, g be functions and a be a set. Suppose f is one-to-one and g is one-to-one and domf ∩ domg = {a} and rngf ∩ rngg = {f(a)} and f(a) = g(a). Then (f+·g)^{−1} = f^{−1} +·g^{−1} .

(7) Let n be a natural number, A be a non empty subset of the carrier of E_{T}^{n}, and p, q be points of E_{T}^{n}. If A is an arc from p to q, then A \ {p} is non empty.

(8) For every natural number n and for all points a, b of E_{T}^{n} holds L(a, b) is n-convex.

(9) For all real numbers s_{1}, s_{3}, s_{4}, l such that s_{1} s_{3} and s_{1} < s_{4} and 0 l and l 1 holds s_{1} (1 − l) · s_{3} + l · s_{4}.

(10) For every set x and for all real numbers a, b such that a b and x ∈ [a, b] holds x ∈ ]a, b[ or x = a or x = b.

(11) For all real numbers a, b, c, d such that ]a, b[ meets [c, d] holds b > c.

(12) For all real numbers a, b, c, d such that b c holds [a, b] misses ]c, d[.

(13) For all real numbers a, b, c, d such that b c holds ]a, b[ misses [c, d].

(14) For all real numbers a, b, c, d such that a < b and [a, b] ⊆ [c, d] holds c a and b d.

(15) For all real numbers a, b, c, d such that a < b and ]a, b[ ⊆ [c, d] holds c a and b d.

(16) For all real numbers a, b, c, d such that a < b and ]a, b[ ⊆ [c, d] holds [a, b] ⊆ [c, d].

(17) Let A be a subset of the carrier of 𝕀 and a, b be real numbers. If a < b and A = ]a, b[, then [a, b] ⊆ the carrier of 𝕀.

(18) Let A be a subset of the carrier of 𝕀 and a, b be real numbers. If a < b and A = ]a, b], then [a, b] ⊆ the carrier of 𝕀.

(19) Let A be a subset of the carrier of 𝕀 and a, b be real numbers. If a < b and A = [a, b[, then [a, b] ⊆ the carrier of 𝕀.

(20) For all real numbers a, b such that a ≠ b holds \overline{]a, b]} = [a, b].

(21) For all real numbers a, b such that a ≠ b holds \overline{[a, b[} = [a, b].

(22) For every subset A of 𝕀 and for all real numbers a, b such that a < b and A = ]a, b[ holds \overline{A} = [a, b].

(23) For every subset A of the carrier of 𝕀 and for all real numbers a, b such that a < b and A = ]a, b] holds \overline{A} = [a, b].

(24) For every subset A of the carrier of 𝕀 and for all real numbers a, b such that a < b and A = [a, b[ holds \overline{A} = [a, b].

(25) For all real numbers a, b such that a < b holds [a, b] ≠ ]a, b].

(26) For all real numbers a, b holds [a, b[ misses {b} and ]a, b] misses {a}.

(27) For all real numbers a, b such that a b holds [a, b] \ {a} = ]a, b].

(28) For all real numbers a, b such that a b holds [a, b] \ {b} = [a, b[.

(29) For all real numbers a, b, c such that a < b and b < c holds ]a, b] ∩ [b, c[= {b}.

(30) For all real numbers a, b, c holds [a, b[ misses [b, c] and [a, b] misses ]b, c].

(31) For all real numbers a, b, c such that a b and b c holds [a, c] \ {b} = [a, b[∪]b, c].

(32) Let A be a subset of the carrier of 𝕀 and a, b be real numbers. If a b and A = [a, b], then 0 a and b 1.

(33) Let A, B be subsets of 𝕀 and a, b, c be real numbers. If a < b and b < c and A = [a, b[ and B = ]b, c], then A and B are separated.

(34) For all real numbers a, b such that a b holds [a, b] = [a, b[∪{b}.

(35) For all real numbers a, b such that a b holds [a, b] = {a} ∪]a, b].

(36) For all real numbers a, b, c, d such that a b and b < c and c d holds [a, d] = [a, b] ∪]b, c[ ∪ [c, d].

(37) For all real numbers a, b, c, d such that a b and b < c and c d holds [a, d] \ ([a, b] ∪ [c, d]) = ]b, c[.

(38) For all real numbers a, b, c such that a < b and b < c holds ]a, b]∪]b, c[ = ]a, c[.

(39) For all real numbers a, b, c such that a < b and b < c holds [b, c[⊆ ]a, c[.

(40) For all real numbers a, b, c such that a < b and b < c holds ]a, b] ∪ [b, c[= ]a, c[.

(41) For all real numbers a, b, c such that a < b and b < c holds ]a, c[\]a, b] = ]b, c[.

(42) For all real numbers a, b, c such that a < b and b < c holds ]a, c[ \ [b, c[= ]a, b[.

(43) For all points p_{1}, p_{2} of 𝕀 holds [p_{1}, p_{2}] is a subset of 𝕀.

(44) For all points a, b of 𝕀 holds ]a, b[ is a subset of 𝕀.

2. Decompositions of Intervals

The following propositions are true:

(45) For every real number p holds {p} is a closed-interval subset of ℝ.

(46) Let A be a non empty connected subset of 𝕀 and a, b, c be points of 𝕀. If a b and b c and a ∈ A and c ∈ A, then b ∈ A.

(47) For every non empty connected subset A of 𝕀 and for all real numbers a, b such that a ∈ A and b ∈ A holds [a, b] ⊆ A.

(48) For all real numbers a, b and for every subset A of 𝕀 such that a b and A = [a, b] holds A is closed.

(49) For all points p_{1}, p_{2} of 𝕀 such that p_{1} p_{2} holds [p_{1}, p_{2}] is a non empty compact connected subset of 𝕀.

(50) Let X be a subset of the carrier of 𝕀 and X′be a subset of ℝ. If X′= X, then X′ is upper bounded and lower bounded.

(51) Let X be a subset of the carrier of 𝕀, X′ be a subset of ℝ, and x be a real number. If x ∈ X′ and X′= X, then inf X′ x and x supX′.

(52) For every subset A of ℝ and for every subset B of 𝕀 such that A = B holds A is closed iff B is closed.

(53) For every closed-interval subset C of ℝ holds inf C supC.

(54) Let C be a non empty compact connected subset of 𝕀 and C′be a subset of ℝ. If C = C′ and [inf C′, supC′] ⊆ C′, then [inf C′, supC′] = C′.

(55) Every non empty compact connected subset of 𝕀 is a closed-interval subset of ℝ.

(56) For every non empty compact connected subset C of 𝕀 there exist points p_{1}, p_{2} of 𝕀 such that p_{1} p_{2} and C = [p_{1}, p_{2}].

3. Decompositions of Simple Closed Curves

The strict non empty subspace I(01) of 𝕀 is defined as follows: (Def. 1) The carrier of I(01) = ]0, 1[.

One can prove the following propositions:

(57) For every subset A of 𝕀 such that A = the carrier of I(01) holds I(01) = 𝕀↾A.

(58) The carrier of I(01) = (the carrier of 𝕀) \ {0, 1}.

(59) I(01) is an open subspace of 𝕀.

(60) For every real number r holds r ∈ the carrier of I(01) iff 0 < r and r < 1.

(61) For all points a, b of 𝕀 such that a < b and b ≠ 1 holds ]a, b] is a non empty subset of I(01).

(62) For all points a, b of 𝕀 such that a < b and a ≠ 0 holds [a, b[ is a non empty subset of I(01).

(63) For every simple closed curve D holds (E_{T}^{2})↾□_{E^{2}} and (E_{T}^{2})↾D are homeomorphic.

(64) Let D be a non empty subset of E_{T}^{2} and p_{1}, p_{2} be points of E_{T}^{2}. If D is an arc from p_{1} to p_{2}, then I(01) and (E_{T}^{2})↾(D \ {p_{1}, p_{2}}) are homeomorphic.

(65) Let D be a subset of the carrier of E_{T}^{2} and p_{1}, p_{2} be points of E_{T}^{2}. If D is an arc from p_{1} to p_{2}, then 𝕀 and (E_{T}^{2})↾D are homeomorphic.

(66) For all points p_{1}, p_{2} of E_{T}^{2} such that p_{1} ≠ p_{2} holds 𝕀 and (E_{T}^{2})↾L(p_{1}, p_{2}) are homeomorphic.

(67) Let E be a subset of I(01). Given points p_{1}, p_{2} of 𝕀 such that p_{1} < p_{2} and E = [p_{1}, p_{2}]. Then 𝕀 and I(01)↾E are homeomorphic.

(68) Let A be a non empty subset of the carrier of E_{T}^{2}, p, q be points of E_{T}^{2}, and a, b be points of 𝕀. Suppose A is an arc from p to q and a < b. Then there exists a non empty subset E of 𝕀 and there exists a map f from 𝕀↾E into (E_{T}^{2})↾A such that E = [a, b] and f is a homeomorphism and f(a) = p and f(b) = q.

(69) Let A be a topological space, B be a non empty topological space, f be a map from A into B, C be a topological space, and X be a subset of A. Suppose f is continuous and C is a subspace of B. Let h be a map from A↾X into C. If h = f↾X, then h is continuous.

(70) For every subset X of 𝕀 and for all points a, b of 𝕀 such that a b and X = ]a, b[ holds X is open.

(71) For every subset X of I(01) and for all points a, b of 𝕀 such that a b and X = ]a, b[ holds X is open.

(72) For every non empty subset X of I(01) and for every point a of 𝕀 such that 0 < a and X = ]0, a] holds X is closed.

(73) For every non empty subset X of I(01) and for every point a of 𝕀 such that X = [a, 1[ holds X is closed.

(74) Let A be a non empty subset of the carrier of E_{T}^{2}, p, q be points of E_{T}^{2}, and a, b be points of 𝕀. Suppose A is an arc from p to q and a < b and b ≠ 1. Then there exists a non empty subset E of I(01) and there exists a map f from I(01)↾E into (E_{T}^{2})↾(A \ {p}) such that E = ]a, b] and f is a homeomorphism and f(b) = q.

(75) Let A be a non empty subset of the carrier of E_{T}^{2}, p, q be points of E_{T}^{2}, and a, b be points of 𝕀. Suppose A is an arc from p to q and a < b and a ≠ 0. Then there exists a non empty subset E of I(01) and there exists 150 adam grabowski

a map f from I(01)↾E into (E_{T}^{2})↾(A \ {q}) such that E = [a, b[ and f is a homeomorphism and f(a) = p.

(76) Let A, B be non empty subsets of the carrier of E_{T}^{2} and p, q be points of E_{T}^{2}. Suppose A is an arc from p to q and B is an arc from q to p and A ∩ B = {p, q} and p ≠ q. Then I(01) and (E_{T}^{2})↾((A \ {p}) ∪ (B \ {p})) are homeomorphic.

(77) For every simple closed curve D and for every point p of E_{T}^{2} such that p ∈ D holds (E_{T}^{2})↾(D \ {p}) and I(01) are homeomorphic.

(78) Let D be a simple closed curve and p, q be points of E_{T}^{2}. If p ∈ D and q ∈ D, then (E_{T}^{2})↾(D \ {p}) and (E_{T}^{2})↾(D \ {q}) are homeomorphic.

(79) Let C be a non empty subset of E_{T}^{2} and E be a subset of I(01). Suppose there exist points p_{1}, p_{2} of 𝕀 such that p_{1} < p_{2} and E = [p_{1}, p_{2}] and I(01)↾E and (E_{T}^{2})↾C are homeomorphic. Then there exist points s_{1}, s_{2} of E_{T}^{2} such that C is an arc from s_{1} to s_{2}.

(80) Let D_{1} be a non empty subset of E_{T}^{2}, f be a map from (E_{T}^{2})↾D_{1} into I(01), and C be a non empty subset of E_{T}^{2}. Suppose f is a homeomorphism and C ⊆ D_{1} and there exist points p_{1}, p_{2} of 𝕀 such that p_{1} < p_{2} and f^{∘}C = [p_{1}, p_{2}]. Then there exist points s_{1}, s_{2} of E_{T}^{2} such that C is an arc from s_{1} to s_{2}.

(81) Let D be a simple closed curve and C be a non empty compact connected subset of E_{T}^{2}. Suppose C ⊆ D. Then C = D or there exist points p_{1}, p_{2} of E_{T}^{2} such that C is an arc from p_{1} to p_{2} or there exists a point p of E_{T}^{2} such that C = {p}.

References

[1] Józef Białas. Group and field definitions. Formalized Mathematics, 1(3):433–439, 1990.

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

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

[4] 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.

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

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

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

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

[9] Agata Darmochwał and Yatsuka Nakamura. Metric spaces as topological spaces - fundamental concepts. Formalized Mathematics, 2(4):605–608, 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.

[12] Noboru Endou and Artur Korniłowicz. The definition of the Riemann definite integral and some related lemmas. Formalized Mathematics, 8(1):93–102, 1999.

on the decompositions of intervals … 151

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

[14] Zbigniew Karno. Separated and weakly separated subspaces of topological spaces. Formalized Mathematics, 2(5):665–674, 1991.

[15] Jarosław Kotowicz. Convergent real sequences. Upper and lower bound of sets of real numbers. Formalized Mathematics, 1(3):477–481, 1990.

[16] Yatsuka Nakamura. Half open intervals in real numbers. Formalized Mathematics, 10(1):21–22, 2002.

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

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

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

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

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

[22] Andrzej Trybulec. A Borsuk theorem on homotopy types. Formalized Mathematics, 2(4):535–545, 1991.

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

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

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

[26] Mariusz Żynel and Adam Guzowski. T_{0} topological spaces. Formalized Mathematics, 5(1):75–77, 1996.

On the Minimal Distance Between Sets in Euclidean Space^{1}

Andrzej Trybulec University of Białystok

Summary. The concept of the minimal distance between two sets in a Euclidean space is introduced and some useful lemmas are proved.

MML Identifier: JORDAN1K.

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

1. Preliminaries

In this paper X is a set and Y is a non empty set. We now state several propositions:

(1) Let f be a function from X into Y. Suppose f is onto. Let y be an element of Y. Then there exists a set x such that x ∈ X and y = f(x).

(2) Let f be a function from X into Y. Suppose f is onto. Let y be an element of Y. Then there exists an element x of X such that y = f(x).

(3) For every function f from X into Y and for every subset A of X such that f is onto holds (f^{∘}A)^{c} ⊆ f^{∘}A^{c}.

(4) For every function f from X into Y and for every subset A of X such that f is one-to-one holds f^{∘}A^{c} ⊆ (f^{∘}A)^{c}.

(5) For every function f from X into Y and for every subset A of X such that f is bijective holds (f^{∘}A)^{c} = f^{∘}A^{c}.

1This work has been partially supported by the European Community TYPES grant IST-1999-29001 and CALCULEMUS grant HPRN-CT-2000-00102. The work was completed while the author visited Shinhsu University (Nagano).

2. Topological and Metrizable Spaces

One can prove the following two propositions:

(6) For every topological space T and for every subset A of T holds A is a component of ∅_{T} iff A is empty.

(7) Let T be a non empty topological space and A, B, C be subsets of T. If A ⊆ B and A is a component of C and B is a component of C, then A = B.

In the sequel n denotes a natural number.

We now state the proposition

(8) If n 1, then for every subset P of E^{n} such that P is bounded holds − P is not bounded.

In the sequel r is a real number and M is a non empty metric space.

Next we state a number of propositions:

(9) For every non empty subset C of M_{top} and for every point p of M_{top} holds (dist_{min}(C))(p) 0.

(10) Let C be a non empty subset of M_{top} and p be a point of M. If for every point q of M such that q ∈ C holds ρ(p, q) r, then (dist_{min}(C))(p) r.

(11) For all non empty subsets A, B of M_{top} holds dist_{min}^{min}(A, B) 0.

(12) For all compact subsets A, B of M_{top} such that A meets B holds dist_{min}^{min}(A, B) = 0.

(13) Let A, B be non empty subsets of M_{top}. Suppose that for all points p, q of M such that p ∈ A and q ∈ B holds ρ(p, q) r. Then dist_{min}^{min}(A, B) r.

(14) Let P, Q be subsets of E_{T}^{n}. Suppose P is a component of Q^{c}. Then P is inside component of Q or P is outside component of Q.

(15) If n 1, then BDD∅_{E_{T}^{n}} = ∅_{E_{T}^{n}}.

(16) BDDΩ_{E_{T}^{n}} = ∅_{E_{T}^{n}}.

(17) If n 1, then UBD∅_{E_{T}^{n}} = Ω_{E_{T}^{n}}.

(18) UBDΩ_{E_{T}^{n}} = ∅_{E_{T}^{n}}.

(19) For every connected subset P of E_{T}^{n} and for every subset Q of E_{T}^{n} such that P misses Q holds P ⊆ UBDQ or P ⊆ BDDQ.

3. Euclid Plane

For simplicity, we adopt the following rules: C, D are simple closed curves, n is a natural number, p, q, q_{1}, q_{2} are points of E_{T}^{2}, r, s_{1}, s_{2}, t_{1}, t_{2} are real numbers, and x, y are points of E^{2}.

Next we state a number of propositions:

(20) ρ([0, 0], r · q) = |r| · ρ([0, 0], q).

(21) ρ(q_{1} + q, q_{2} + q) = ρ(q_{1}, q_{2}).

(22) If p ≠ q, then ρ(p, q) > 0.

(23) ρ(q_{1} − q, q_{2} − q) = ρ(q_{1}, q_{2}).

(24) ρ(p, q) = ρ(− p, − q).

(25) ρ(q − q_{1}, q − q_{2}) = ρ(q_{1}, q_{2}).

(26) ρ(r · p, r · q) = |r| · ρ(p, q).

(27) If r 1, then ρ(p, r · p + (1 − r) · q) = (1 − r) · ρ(p, q).

(28) If 0 r, then ρ(q, r · p + (1 − r) · q) = r · ρ(p, q).

(29) If p ∈ L(q_{1}, q_{2}), then ρ(q_{1}, p) + ρ(p, q_{2}) = ρ(q_{1}, q_{2}).

(30) If q_{1} ∈ L(q_{2}, p) and q_{1} ≠ q_{2}, then ρ(q_{1}, p) < ρ(q_{2}, p).

(31) If y = [0, 0], then Ball(y, r) = {q : |q| < r}.

4. Affine Maps

Next we state several propositions:

(32) (AffineMap(r, s_{1}, r, s_{2}))(p) = r · p + [s_{1}, s_{2}].

(33) (AffineMap(r, q_{1}, r, q_{2}))(p) = r · p + q.

(34) If s_{1} > 0 and s_{2} > 0, then AffineMap(s_{1}, t_{1}, s_{2}, t_{2}) · AffineMap(\frac{1}{s_{1}} , − \frac{t_{1}}{s_{1}} , \frac{1}{s_{2}} , − \frac{t_{2}}{s_{2}} ) = id_{R^{2}} .

(35) If y = [0, 0] and x = q and r > 0, then (AffineMap(r, q_{1}, r, q_{2}))^{∘} Ball(y, 1) = Ball(x, r).

(36) For all real numbers A, B, C, D such that A > 0 and C > 0 holds AffineMap(A, B, C, D) is onto.

(37) Ball(x, r)^{c} is a connected subset of E_{T}^{2}.

5. Minimal Distance Between Subsets

Let us consider n and let A, B be subsets of the carrier of E_{T}^{n}. The functor dist_{min}(A, B) yielding a real number is defined by:

(Def. 1) There exist subsets A′, B′ of (E^{n})_{top} such that A = A′ and B = B′ and

dist_{min}(A, B) = dist_{min}^{min}(A′, B′). Let M be a non empty metric space and let P, Q be non empty compact

subsets of M_{top}. Let us note that the functor dist_{min}^{min}(P, Q) is commutative. Let us observe that the functor dist_{max}^{max}(P, Q) is commutative.

Let us consider n and let A, B be non empty compact subsets of E_{T}^{n}. Let us observe that the functor dist_{min}(A, B) is commutative.

Next we state several propositions:

(38) For all non empty subsets A, B of E_{T}^{n} holds dist_{min}(A, B) 0.

(39) For all compact subsets A, B of E_{T}^{n} such that A meets B holds dist_{min}(A, B) = 0.

(40) Let A, B be non empty subsets of E_{T}^{n}. Suppose that for all points p, q of E_{T}^{n} such that p ∈ A and q ∈ B holds ρ(p, q) r. Then dist_{min}(A, B) r.

(41) Let D be a subset of the carrier of E_{T}^{n} and A, C be non empty subsets of the carrier of E_{T}^{n}. If C ⊆ D, then dist_{min}(A, D) dist_{min}(A, C).

(42) For all non empty compact subsets A, B of E_{T}^{n} there exist points p, q of E_{T}^{n} such that p ∈ A and q ∈ B and dist_{min}(A, B) = ρ(p, q).

(43) For all points p, q of E_{T}^{n} holds dist_{min}({p}, {q}) = ρ(p, q).

Let us consider n, let p be a point of E_{T}^{n}, and let B be a subset of the carrier of E_{T}^{n}. The functor ρ(p, B) yielding a real number is defined as follows:

(Def. 2) ρ(p, B) = dist_{min}({p}, B).

Next we state several propositions:

(44) For every non empty subset A of E_{T}^{n} and for every point p of E_{T}^{n} holds ρ(p, A) 0.

(45) For every compact subset A of E_{T}^{n} and for every point p of E_{T}^{n} such that p ∈ A holds ρ(p, A) = 0.

(46) Let A be a non empty compact subset of E_{T}^{n} and p be a point of E_{T}^{n}. Then there exists a point q of E_{T}^{n} such that q ∈ A and ρ(p, A) = ρ(p, q).

(47) Let C be a non empty subset of the carrier of E_{T}^{n} and D be a subset of the carrier of E_{T}^{n}. If C ⊆ D, then for every point q of E_{T}^{n} holds ρ(q, D) ρ(q, C).

(48) Let A be a non empty subset of E_{T}^{n} and p be a point of E_{T}^{n}. If for every point q of E_{T}^{n} such that q ∈ A holds ρ(p, q) r, then ρ(p, A) r.

(49) For all points p, q of E_{T}^{n} holds ρ(p, {q}) = ρ(p, q).

(50) For every non empty subset A of E_{T}^{n} and for all points p, q of E_{T}^{n} such that q ∈ A holds ρ(p, A) ρ(p, q).

(51) Let A be a compact non empty subset of E_{T}^{2} and B be an open subset of E_{T}^{2}. If A ⊆ B, then for every point p of E_{T}^{2} such that p ∉ B holds ρ(p, B) < ρ(p, A).

6. BDD and UBD

The following two propositions are true:

(52) UBDC meets UBDD.

(53) If q ∈ UBDC and p ∈ BDDC, then ρ(q, C) < ρ(q, p).

Let us consider C. Observe that BDDC is non empty.

One can prove the following three propositions:

(54) If p ∉ BDDC, then ρ(p, C) ρ(p, BDDC).

on the minimal distance between sets … 157

(55) C ⊈ BDDD or D ⊈ BDDC.

(56) If C ⊆ BDDD, then D ⊆ UBDC.

7. Main Definitions

We now state the proposition

(57) L̃(Cage(C, n)) ⊆ UBDC.

Let us consider C. The functor LowerMiddlePointC yielding a point of E_{T}^{2} is defined by:

(Def. 3) LowerMiddlePointC =

FPoint(LowerArcC, W-minC, E-maxC, VerticalLine \frac{W-bound C+E-bound C}{2} ). The functor UpperMiddlePointC yielding a point of E_{T}^{2} is defined by:

(Def. 4) UpperMiddlePointC =

FPoint(UpperArcC, W-minC, E-maxC, VerticalLine \frac{W-bound C+E-bound C}{2} ). We now state several propositions:

(58) LowerArcC meets VerticalLine \frac{W-bound C+E-bound C}{2} .

(59) UpperArcC meets VerticalLine \frac{W-bound C+E-bound C}{2} .

(60) (LowerMiddlePointC)_{1} = \frac{W-bound C+E-bound C}{2} .

(61) (UpperMiddlePointC)_{1} = \frac{W-bound C+E-bound C}{2} .

(62) LowerMiddlePointC ∈ LowerArcC.

(63) UpperMiddlePointC ∈ UpperArcC.

References

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

[2] Józef Białas and Yatsuka Nakamura. The theorem of Weierstrass. Formalized Mathematics, 5(3):353–359, 1996.

[3] Leszek Borys. Paracompact and metrizable spaces. Formalized Mathematics, 2(4):481– 485, 1991.

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

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

[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.

[12] Adam Grabowski and Yatsuka Nakamura. The ordering of points on a curve. Part II. Formalized Mathematics, 6(4):467–473, 1997.

158 andrzej trybulec

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

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

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

[16] Artur Korniłowicz. Properties of left and right components. Formalized Mathematics, 8(1):163–168, 1999.

[17] Jarosław Kotowicz. Convergent real sequences. Upper and lower bound of sets of real numbers. Formalized Mathematics, 1(3):477–481, 1990.

[18] Yatsuka Nakamura. On Outside Fashoda Meet Theorem. Formalized Mathematics, 9(4):697–704, 2001.

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

[20] 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.

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

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

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

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

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

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

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

Sequences of Metric Spaces and an Abstract Intermediate Value Theorem^{1}

Yatsuka Nakamura Shinshu University Nagano

Andrzej Trybulec University of Białystok

Summary. Relations of convergence of real sequences and convergence of metric spaces are investigated. An abstract intermediate value theorem for two closed sets in the range is presented. At the end, it is proven that an arc connecting the west minimal point and the east maximal point in a simple closed curve must be identical to the upper arc or lower arc of the closed curve.

MML Identifier: TOPMETR3.

The notation and terminology used here are introduced in the following papers: [21], [22], [23], [3], [4], [2], [12], [18], [6], [1], [20], [7], [5], [8], [16], [14], [13], [15], [11], [19], [17], [9], and [10].

The following propositions are true:

(1) Let R be a non empty subset of ℝ and r_{0} be a real number. If for every real number r such that r ∈ R holds r r_{0}, then supR r_{0}.

(2) Let X be a non empty metric space, S be a sequence of X, and F be a subset of X_{top}. Suppose S is convergent and for every natural number n holds S(n) ∈ F and F is closed. Then limS ∈ F.

(3) Let X, Y be non empty metric spaces, f be a map from X_{top} into Y_{top}, and S be a sequence of X. Then f · S is a sequence of Y.

(4) Let X, Y be non empty metric spaces, f be a map from X_{top} into Y_{top}, S be a sequence of X, and T be a sequence of Y. If S is convergent and T = f · S and f is continuous, then T is convergent.

1This work has been partially supported by the European Community TYPES grant IST-1999-29001 and CALCULEMUS grant HPRN-CT-2000-00102.

(5) For every non empty metric space X holds every function from ℕ into the carrier of X is a sequence of X.

(6) Let s be a sequence of real numbers and S be a sequence of the metric space of real numbers such that s = S. Then

(i) s is convergent iff S is convergent, and (ii) if s is convergent, then lims = limS.

(7) Let a, b be real numbers and s be a sequence of real numbers. If rngs ⊆ [a, b], then s is a sequence of [a, b]_{M}.

(8) Let a, b be real numbers and S be a sequence of [a, b]_{M}. Suppose a b. Then S is a sequence of the metric space of real numbers.

(9) Let a, b be real numbers, S_{1} be a sequence of [a, b]_{M}, and S be a sequence of the metric space of real numbers such that S = S_{1} and a b. Then

(i) S is convergent iff S_{1} is convergent, and (ii) if S is convergent, then limS = limS_{1}.

(10) Let a, b be real numbers, s be a sequence of real numbers, and S be a sequence of [a, b]_{M}. If S = s and a b and s is convergent, then S is convergent and lims = limS.

(11) Let a, b be real numbers, s be a sequence of real numbers, and S be a sequence of [a, b]_{M}. If S = s and a b and s is non-decreasing, then S is convergent.

(12) Let a, b be real numbers, s be a sequence of real numbers, and S be a sequence of [a, b]_{M}. If S = s and a b and s is non-increasing, then S is convergent.

(13) Let s be a sequence of real numbers and r_{0} be a real number. Suppose for every natural number n holds s(n) r_{0} and s is convergent. Then lims r_{0}.

(14) Let s be a sequence of real numbers and r_{0} be a real number. Suppose for every natural number n holds s(n) r_{0} and s is convergent. Then lims r_{0}.

(15) Let R be a non empty subset of ℝ. Suppose R is upper bounded. Then there exists a sequence s of real numbers such that s is non-decreasing and rngs ⊆ R and lims = supR.

(16) Let R be a non empty subset of ℝ. Suppose R is lower bounded. Then there exists a sequence s of real numbers such that s is non-increasing and rngs ⊆ R and lims = inf R.

(17) Let X be a non empty metric space, f be a map from 𝕀 into X_{top}, F_{1}, F_{2} be subsets of X_{top}, and r_{1}, r_{2} be real numbers. Suppose that 0 r_{1} and r_{2} 1 and r_{1} r_{2} and f(r_{1}) ∈ F_{1} and f(r_{2}) ∈ F_{2} and F_{1} is closed and F_{2} is closed and f is continuous and F_{1} ∪ F_{2} = the carrier of X. Then there exists a real number r such that r_{1} r and r r_{2} and f(r) ∈ F_{1} ∩ F_{2}.

sequences of metric spaces and … 161

(18) Let n be a natural number, p_{1}, p_{2} be points of E_{T}^{n}, and P, P_{1} be non empty subsets of the carrier of E_{T}^{n}. If P is an arc from p_{1} to p_{2} and P_{1} is an arc from p_{2} to p_{1} and P_{1} ⊆ P, then P_{1} = P.

(19) Let P, P_{1} be compact non empty subsets of E_{T}^{2}. Suppose P is a simple closed curve and P_{1} is an arc from W-minP to E-maxP and P_{1} ⊆ P. Then P_{1} = UpperArcP or P_{1} = LowerArcP.

References

[1] Leszek Borys. Paracompact and metrizable spaces. Formalized Mathematics, 2(4):481– 485, 1991.

[2] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.

[3] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 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 and Piotr Rudnicki. Bounding boxes for compact sets in E^{2}. Formalized Mathematics, 6(3):427–440, 1997.

[6] Agata Darmochwał. Compact spaces. Formalized Mathematics, 1(2):383–386, 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] 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.

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

[11] Alicia de la Cruz. Totally bounded metric spaces. Formalized Mathematics, 2(4):559–562, 1991.

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

[13] Jarosław Kotowicz. Convergent real sequences. Upper and lower bound of sets of real numbers. Formalized Mathematics, 1(3):477–481, 1990.

[14] Jarosław Kotowicz. Convergent sequences and the limit of sequences. Formalized Mathematics, 1(2):273–275, 1990.

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

[16] Jarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269–272, 1990.

[17] 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.

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

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

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

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

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

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

On the Decomposition of a Simple Closed Curve into Two Arcs

Andrzej Trybulec^{1} University of Białystok Yatsuka Nakamura Shinshu University Nagano

Summary. The purpose of the paper is to prove lemmas needed for the Jordan curve theorem. The main result is that the decomposition of a simple closed curve into two arcs with the ends p_{1}, p_{2} is unique in the sense that every arc on the curve with the same ends must be equal to one of them.

MML Identifier: JORDAN16.

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

One can prove the following proposition

(1) Let S_{1} be a finite non empty subset of ℝ and e be a real number. If for every real number r such that r ∈ S_{1} holds r < e, then maxS_{1} < e.

For simplicity, we use the following convention: C is a simple closed curve, A, A_{1}, A_{2} are subsets of E_{T}^{2}, p, p_{1}, p_{2}, q, q_{1}, q_{2} are points of E_{T}^{2}, and n is a natural number.

Let us consider n. Note that there exists a subset of E_{T}^{n} which is trivial.

We now state a number of propositions:

(2) For all sets a, b, c, X such that a ∈ X and b ∈ X and c ∈ X holds {a, b, c} ⊆ X.

(3) ∅_{E_{T}^{n}} is Bounded.

(4) LowerArcC ≠ UpperArcC.

(5) Segment(A, p_{1}, p_{2}, q_{1}, q_{2}) ⊆ A.

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

The work has been done while the author visited Shinshu University.

(6) Let T be a non empty topological space and A, B be subsets of the carrier of T. If A ⊆ B, then T ↾A is a subspace of T ↾B.

(7) If A is an arc from p_{1} to p_{2} and q ∈ A, then q ∈ LSegment(A, p_{1}, p_{2}, q).

(8) If A is an arc from p_{1} to p_{2} and q ∈ A, then q ∈ RSegment(A, p_{1}, p_{2}, q).

(9) If A is an arc from p_{1} to p_{2} and LE q_{1}, q_{2}, A, p_{1}, p_{2}, then q_{1} ∈ Segment(A, p_{1}, p_{2}, q_{1}, q_{2}) and q_{2} ∈ Segment(A, p_{1}, p_{2}, q_{1}, q_{2}).

(10) Segment(p, q, C) ⊆ C.

(11) If p ∈ C and q ∈ C, then LE(p, q, C) or LE(q, p, C).

(12) Let X, Y be non empty topological spaces, Y_{0} be a non empty subspace of Y, f be a map from X into Y, and g be a map from X into Y_{0}. If f = g and f is continuous, then g is continuous.

(13) Let S, T be non empty topological spaces, S_{0} be a non empty subspace of S, T_{0} be a non empty subspace of T, and f be a map from S into T. Suppose f is a homeomorphism. Let g be a map from S_{0} into T_{0}. If g = f↾S_{0} and g is onto, then g is a homeomorphism.

(14) Let P_{1}, P_{2}, P_{3} be subsets of E_{T}^{2} and p_{1}, p_{2} be points of E_{T}^{2}. Suppose P_{1} is an arc from p_{1} to p_{2} and P_{2} is an arc from p_{1} to p_{2} and P_{3} is an arc from p_{1} to p_{2} and P_{2} ∩ P_{3} = {p_{1}, p_{2}} and P_{1} ⊆ P_{2} ∪ P_{3}. Then P_{1} = P_{2} or P_{1} = P_{3}.

(15) Let C be a simple closed curve, A_{1}, A_{2} be subsets of E_{T}^{2}, and p_{1}, p_{2} be points of E_{T}^{2}. Suppose A_{1} is an arc from p_{1} to p_{2} and A_{2} is an arc from p_{1} to p_{2} and A_{1} ⊆ C and A_{2} ⊆ C and A_{1} ≠ A_{2}. Then A_{1} ∪ A_{2} = C and A_{1} ∩ A_{2} = {p_{1}, p_{2}}.

(16) Let A_{1}, A_{2} be subsets of E_{T}^{2} and p_{1}, p_{2}, q_{1}, q_{2} be points of E_{T}^{2}. If A_{1} is an arc from p_{1} to p_{2} and A_{1} ∩ A_{2} = {q_{1}, q_{2}}, then A_{1} ≠ A_{2}.

(17) Let C be a simple closed curve, A_{1}, A_{2} be subsets of E_{T}^{2}, and p_{1}, p_{2} be points of E_{T}^{2}. Suppose A_{1} is an arc from p_{1} to p_{2} and A_{2} is an arc from p_{1} to p_{2} and A_{1} ⊆ C and A_{2} ⊆ C and A_{1} ∩ A_{2} = {p_{1}, p_{2}}. Then A_{1} ∪ A_{2} = C.

(18) Suppose A_{1} ⊆ C and A_{2} ⊆ C and A_{1} ≠ A_{2} and A_{1} is an arc from p_{1} to p_{2} and A_{2} is an arc from p_{1} to p_{2}. Let given A. If A is an arc from p_{1} to p_{2} and A ⊆ C, then A = A_{1} or A = A_{2}.

(19) Let C be a simple closed curve and A be a non empty subset of E_{T}^{2}. If A is an arc from W-minC to E-maxC and A ⊆ C, then A = LowerArcC or A = UpperArcC.

(20) Suppose A is an arc from p_{1} to p_{2} and LE q_{1}, q_{2}, A, p_{1}, p_{2}. Then there exists a map g from 𝕀 into (E_{T}^{2})↾A and there exist real numbers s_{1}, s_{2} such that g is a homeomorphism and g(0) = p_{1} and g(1) = p_{2} and g(s_{1}) = q_{1} and g(s_{2}) = q_{2} and 0 s_{1} and s_{1} s_{2} and s_{2} 1.

(21) Suppose A is an arc from p_{1} to p_{2} and LE q_{1}, q_{2}, A, p_{1}, p_{2} and q_{1} ≠ q_{2}. Then there exists a map g from 𝕀 into (E_{T}^{2})↾A and there exist real numbers s_{1}, s_{2} such that g is a homeomorphism and g(0) = p_{1} and g(1) = p_{2} and g(s_{1}) = q_{1} and g(s_{2}) = q_{2} and 0 s_{1} and s_{1} < s_{2} and s_{2} 1.

(22) If A is an arc from p_{1} to p_{2} and LE q_{1}, q_{2}, A, p_{1}, p_{2}, then Segment(A, p_{1}, p_{2}, q_{1}, q_{2}) is non empty.

(23) If p ∈ C, then p ∈ Segment(p, W-minC, C) and W-minC ∈

Segment(p, W-minC, C). Let f be a partial function from ℝ to ℝ. We say that f is continuous if and

only if: (Def. 1) f is continuous on domf.

Let f be a function from ℝ into ℝ. Let us observe that f is continuous if and only if:

(Def. 2) f is continuous on ℝ.

Let a, b be real numbers. The functor AffineMap(a, b) yielding a function from ℝ into ℝ is defined by:

(Def. 3) For every real number x holds (AffineMap(a, b))(x) = a · x + b. Let a, b be real numbers. Observe that AffineMap(a, b) is continuous. Let us mention that there exists a function from ℝ into ℝ which is continuous. We now state a number of propositions:

(24) Let f, g be continuous partial functions from ℝ to ℝ. Then g · f is a continuous partial function from ℝ to ℝ.

(25) For all real numbers a, b holds (AffineMap(a, b))(0) = b.

(26) For all real numbers a, b holds (AffineMap(a, b))(1) = a + b.

(27) For all real numbers a, b such that a ≠ 0 holds AffineMap(a, b) is oneto-one.

(28) For all real numbers a, b, x, y such that a > 0 and x < y holds (AffineMap(a, b))(x) < (AffineMap(a, b))(y).

(29) For all real numbers a, b, x, y such that a < 0 and x < y holds (AffineMap(a, b))(x) > (AffineMap(a, b))(y).

(30) For all real numbers a, b, x, y such that a 0 and x y holds (AffineMap(a, b))(x) (AffineMap(a, b))(y).

(31) For all real numbers a, b, x, y such that a 0 and x y holds (AffineMap(a, b))(x) (AffineMap(a, b))(y).

(32) For all real numbers a, b such that a ≠ 0 holds rngAffineMap(a, b) = ℝ.

(33) For all real numbers a, b such that a ≠ 0 holds (AffineMap(a, b))^{−1} = AffineMap(a^{−1} , − \frac{b}{a}).

(34) For all real numbers a, b such that a > 0 holds (AffineMap(a, b))^{∘}[0, 1] = [b, a + b].

(35) For every map f from ℝ^{1} into ℝ^{1} and for all real numbers a, b such that a ≠ 0 and f = AffineMap(a, b) holds f is a homeomorphism.

166 andrzej trybulec and yatsuka nakamura

(36) If A is an arc from p_{1} to p_{2} and LE q_{1}, q_{2}, A, p_{1}, p_{2} and q_{1} ≠ q_{2}, then Segment(A, p_{1}, p_{2}, q_{1}, q_{2}) is an arc from q_{1} to q_{2}.

(37) Let p_{1}, p_{2} be points of E_{T}^{2} and P be a subset of E_{T}^{2}. Suppose P ⊆ C and P is an arc from p_{1} to p_{2} and W-minC ∈ P and E-maxC ∈ P. Then UpperArcC ⊆ P or LowerArcC ⊆ P.

References

[1] Leszek Borys. Paracompact and metrizable spaces. Formalized Mathematics, 2(4):481– 485, 1991.

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

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

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

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

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

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

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

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

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

[11] 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.

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

[13] Adam Grabowski and Yatsuka Nakamura. The ordering of points on a curve. Part II. Formalized Mathematics, 6(4):467–473, 1997.

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

[15] Zbigniew Karno. Continuity of mappings over the union of subspaces. Formalized Mathematics, 3(1):1–16, 1992.

[16] Yatsuka Nakamura. On the dividing function of the simple closed curve into segments. Formalized Mathematics, 7(1):135–138, 1998.

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

[18] 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.

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

[20] Beata Padlewska. Locally connected spaces. Formalized Mathematics, 2(1):93–96, 1991.

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

[22] Konrad Raczkowski and Paweł Sadowski. Real function continuity. Formalized Mathematics, 1(4):787–791, 1990.

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

[24] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25–34, 1990.

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

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

on the decomposition of a simple closed … 167

[27] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics,

1(1):73–83, 1990.

Received September 16, 2002

The Ordering of Points on a Curve. Part III^{1}

Artur Korniłowicz University of Białystok

MML Identifier: JORDAN17.

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

We follow the rules: C, P denote simple closed curves and a, b, c, d, e denote points of E_{T}^{2}.

We now state several propositions:

(1) Let n be a natural number, a, p_{1}, p_{2} be points of E_{T}^{n}, and P be a subset of the carrier of E_{T}^{n}. Suppose a ∈ P and P is an arc from p_{1} to p_{2}. Then there exists a map f from 𝕀 into (E_{T}^{n})↾P and there exists a real number r such that f is a homeomorphism and f(0) = p_{1} and f(1) = p_{2} and 0 r and r 1 and f(r) = a.

(2) LE(W-minP, E-maxP, P).

(3) If LE(a, E-maxP, P), then a ∈ UpperArcP.

(4) If LE(E-maxP, a, P), then a ∈ LowerArcP.

(5) If LE(a, W-minP, P), then a ∈ LowerArcP.

(6) Let P be a subset of the carrier of E_{T}^{2}. Suppose a ≠ b and P is an arc from c to d and LE a, b, P, c, d. Then there exists e such that a ≠ e and b ≠ e and LE a, e, P, c, d and LE e, b, P, c, d.

(7) If a ∈ P, then there exists e such that a ≠ e and LE(a, e, P).

(8) If a ≠ b and LE(a, b, P), then there exists c such that c ≠ a and c ≠ b and LE(a, c, P) and LE(c, b, P).

Let P be a compact non empty subset of E_{T}^{2} and let a, b, c, d be points of E_{T}^{2}. We say that a, b, c, d are in this order on P if and only if:

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

(Def. 1) LE(a, b, P) and LE(b, c, P) and LE(c, d, P) or LE(b, c, P) and LE(c, d, P) and LE(d, a, P) or LE(c, d, P) and LE(d, a, P) and LE(a, b, P) or LE(d, a, P) and LE(a, b, P) and LE(b, c, P).

The following propositions are true:

(9) If a ∈ P, then a, a, a, a are in this order on P.

(10) If a, b, c, d are in this order on P, then b, c, d, a are in this order on P.

(11) If a, b, c, d are in this order on P, then c, d, a, b are in this order on P.

(12) If a, b, c, d are in this order on P, then d, a, b, c are in this order on P.

(13) Suppose a ≠ b and a, b, c, d are in this order on P. Then there exists e such that e ≠ a and e ≠ b and a, e, b, c are in this order on P.

(14) Suppose a ≠ b and a, b, c, d are in this order on P. Then there exists e such that e ≠ a and e ≠ b and a, e, b, d are in this order on P.

(15) Suppose b ≠ c and a, b, c, d are in this order on P. Then there exists e such that e ≠ b and e ≠ c and a, b, e, c are in this order on P.

(16) Suppose b ≠ c and a, b, c, d are in this order on P. Then there exists e such that e ≠ b and e ≠ c and b, e, c, d are in this order on P.

(17) Suppose c ≠ d and a, b, c, d are in this order on P. Then there exists e such that e ≠ c and e ≠ d and a, c, e, d are in this order on P.

(18) Suppose c ≠ d and a, b, c, d are in this order on P. Then there exists e such that e ≠ c and e ≠ d and b, c, e, d are in this order on P.

(19) Suppose d ≠ a and a, b, c, d are in this order on P. Then there exists e such that e ≠ d and e ≠ a and a, b, d, e are in this order on P.

(20) Suppose d ≠ a and a, b, c, d are in this order on P. Then there exists e such that e ≠ d and e ≠ a and a, c, d, e are in this order on P.

(21) Suppose a ≠ c and a ≠ d and b ≠ d and a, b, c, d are in this order on P and b, a, c, d are in this order on P. Then a = b.

(22) Suppose a ≠ b and b ≠ c and c ≠ d and a, b, c, d are in this order on P and c, b, a, d are in this order on P. Then a = c.

(23) Suppose a ≠ b and a ≠ c and b ≠ d and a, b, c, d are in this order on P and d, b, c, a are in this order on P. Then a = d.

(24) Suppose a ≠ c and a ≠ d and b ≠ d and a, b, c, d are in this order on P and a, c, b, d are in this order on P. Then b = c.

(25) Suppose a ≠ b and b ≠ c and c ≠ d and a, b, c, d are in this order on P and a, d, c, b are in this order on P. Then b = d.

(26) Suppose a ≠ b and a ≠ c and b ≠ d and a, b, c, d are in this order on P and a, b, d, c are in this order on P. Then c = d.

(27) Suppose a ∈ C and b ∈ C and c ∈ C and d ∈ C. Then (i) a, b, c, d are in this order on C, or (ii) a, b, d, c are in this order on C, or

the ordering of points on a curve. … 171

(iii) a, c, b, d are in this order on C, or (iv) a, c, d, b are in this order on C, or

(v) a, d, b, c are in this order on C, or (vi) a, d, c, b are in this order on C.

References

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

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

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

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

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

[6] 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.

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

[8] Adam Grabowski and Yatsuka Nakamura. The ordering of points on a curve. Part II. Formalized Mathematics, 6(4):467–473, 1997.

[9] 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.

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

[11] Andrzej Trybulec. A Borsuk theorem on homotopy types. Formalized Mathematics, 2(4):535–545, 1991.

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

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

The Ordering of Points on a Curve. Part IV^{1}

Artur Korniłowicz University of Białystok

MML Identifier: JORDAN18.

The notation and terminology used in this paper are introduced in the following articles: [19], [21], [22], [2], [3], [10], [20], [13], [14], [18], [6], [17], [5], [11], [1], [7], [8], [4], [9], [16], [12], and [15].

1. Preliminaries

For simplicity, we adopt the following rules: n denotes an element of ℕ, V denotes a subset of the carrier of E_{T}^{n}, s, s_{1}, s_{2}, t, t_{1}, t_{2} denote points of E_{T}^{n}, C denotes a simple closed curve, P denotes a subset of the carrier of E_{T}^{2}, and a, p, p_{1}, p_{2}, q, q_{1}, q_{2} denote points of E_{T}^{2}.

Next we state several propositions:

(1) For all real numbers a, b holds (a − b)^{2} = (b − a)^{2}.

(2) Let S, T be non empty topological spaces, f be a map from S into T, and A be a subset of T. If f is a homeomorphism and A is connected, then f^{−1} (A) is connected.

(3) Let S, T be non empty topological structures, f be a map from S into T, and A be a subset of T. If f is a homeomorphism and A is compact, then f^{−1} (A) is compact.

(4) proj2^{∘} NorthHalflinea is lower bounded.

(5) proj2^{∘} SouthHalflinea is upper bounded.

(6) proj1^{∘} WestHalflinea is upper bounded.

(7) proj1^{∘} EastHalflinea is lower bounded.

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

Let us consider a. One can verify the following observations:

∗ proj2^{∘} NorthHalflinea is non empty,

∗ proj2^{∘} SouthHalflinea is non empty,

∗ proj1^{∘} WestHalflinea is non empty, and

∗ proj1^{∘} EastHalflinea is non empty.

Next we state four propositions:

(8) inf(proj2^{∘} NorthHalflinea) = a_{2}.

(9) sup(proj2^{∘} SouthHalflinea) = a_{2}.

(10) sup(proj1^{∘} WestHalflinea) = a_{1}.

(11) inf(proj1^{∘} EastHalflinea) = a_{1}.

Let us consider a. One can verify the following observations:

∗ NorthHalflinea is closed,

∗ SouthHalflinea is closed,

∗ EastHalflinea is closed, and

∗ WestHalflinea is closed.

One can prove the following propositions:

(12) If a ∈ BDDP, then NorthHalflinea ⊈ UBDP.

(13) If a ∈ BDDP, then SouthHalflinea ⊈ UBDP.

(14) If a ∈ BDDP, then EastHalflinea ⊈ UBDP.

(15) If a ∈ BDDP, then WestHalflinea ⊈ UBDP.

(16) Let P be a subset of the carrier of E_{T}^{2} and p_{1}, p_{2}, q be points of E_{T}^{2}. If P is an arc from p_{1} to p_{2} and q ≠ p_{2}, then p_{2} ∉ LSegment(P, p_{1}, p_{2}, q).

(17) Let P be a subset of the carrier of E_{T}^{2} and p_{1}, p_{2}, q be points of E_{T}^{2}. If P is an arc from p_{1} to p_{2} and q ≠ p_{1}, then p_{1} ∉ RSegment(P, p_{1}, p_{2}, q).

(18) Let C be a simple closed curve, P be a subset of the carrier of E_{T}^{2}, and p_{1}, p_{2} be points of E_{T}^{2}. Suppose P is an arc from p_{1} to p_{2} and P ⊆ C. Then there exists a non empty subset R of E_{T}^{2} such that R is an arc from p_{1} to p_{2} and P ∪ R = C and P ∩ R = {p_{1}, p_{2}}.

(19) Let P be a subset of the carrier of E_{T}^{2} and p_{1}, p_{2}, q_{1}, q_{2} be points of E_{T}^{2}. Suppose P is an arc from p_{1} to p_{2} and q_{1} ∈ P and q_{2} ∈ P and q_{1} ≠ p_{1} and q_{1} ≠ p_{2} and q_{2} ≠ p_{1} and q_{2} ≠ p_{2} and q_{1} ≠ q_{2}. Then there exists a non empty subset Q of E_{T}^{2} such that Q is an arc from q_{1} to q_{2} and Q ⊆ P and Q misses {p_{1}, p_{2}}.

2. Two Special Points on a Simple Closed Curve

Let us consider p, P. The functor North-Bound(p, P) yields a point of E_{T}^{2} and is defined by:

(Def. 1) North-Bound(p, P) = [p_{1}, inf(proj2^{∘}(P ∩ NorthHalflinep))].

The functor South-Bound(p, P) yields a point of E_{T}^{2} and is defined by: (Def. 2) South-Bound(p, P) = [p_{1}, sup(proj2^{∘}(P ∩ SouthHalflinep))].

One can prove the following propositions:

(20) (North-Bound(p, P))_{1} = p_{1} and (South-Bound(p, P))_{1} = p_{1}.

(21) (North-Bound(p, P))_{2} = inf(proj2^{∘}(P ∩ NorthHalflinep)) and (South-Bound(p, P))_{2} = sup(proj2^{∘}(P ∩ SouthHalflinep)).

(22) For every compact subset C of E_{T}^{2} such that p ∈ BDDC holds North-Bound(p, C) ∈ C and North-Bound(p, C) ∈ NorthHalflinep and South-Bound(p, C) ∈ C and South-Bound(p, C) ∈ SouthHalflinep.

(23) For every compact subset C of E_{T}^{2} such that p ∈ BDDC holds (South-Bound(p, C))_{2} < p_{2} and p_{2} < (North-Bound(p, C))_{2}.

(24) For every compact subset C of E_{T}^{2} such that p ∈ BDDC holds inf(proj2^{∘}(C ∩ NorthHalflinep)) > sup(proj2^{∘}(C ∩ SouthHalflinep)).

(25) For every compact subset C of E_{T}^{2} such that p ∈ BDDC holds South-Bound(p, C) ≠ North-Bound(p, C).

(26) For every subset C of the carrier of E_{T}^{2} holds L(North-Bound(p, C), South-Bound(p, C)) is vertical.

(27) For every compact subset C of E_{T}^{2} such that p ∈ BDDC holds L(North-Bound(p, C), South-Bound(p, C)) ∩ C = {North-Bound(p, C), South-Bound(p, C)}.

(28) Let C be a compact subset of E_{T}^{2}. Suppose p ∈ BDDC and q ∈ BDDC and p_{1} ≠ q_{1}. Then North-Bound(p, C), South-Bound(q, C), North-Bound(q, C), South-Bound(p, C) are mutually different.

3. An Order of Points on a Simple Closed Curve

Let us consider n, V, s_{1}, s_{2}, t_{1}, t_{2}. We say that s_{1}, s_{2} separate t_{1}, t_{2} on V if and only if:

(Def. 3) For every subset A of the carrier of E_{T}^{n} such that A is an arc from s_{1} to

s_{2} and A ⊆ V holds A meets {t_{1}, t_{2}}. We introduce s_{1}, s_{2} are neighbours wrt t_{1}, t_{2} on V as an antonym of s_{1}, s_{2} separate t_{1}, t_{2} on V.

We now state a number of propositions:

(29) t, t separate s_{1}, s_{2} on V.

(30) If s_{1}, s_{2} separate t_{1}, t_{2} on V, then s_{2}, s_{1} separate t_{1}, t_{2} on V.

(31) If s_{1}, s_{2} separate t_{1}, t_{2} on V, then s_{1}, s_{2} separate t_{2}, t_{1} on V.

(32) s, t_{1} separate s, t_{2} on V.

(33) t_{1}, s separate t_{2}, s on V.

176 artur korniłowicz

(34) t_{1}, s separate s, t_{2} on V.

(35) s, t_{1} separate t_{2}, s on V.

(36) Let p_{1}, p_{2}, q be points of E_{T}^{2}. Suppose q ∈ C and p_{1} ∈ C and p_{2} ∈ C and p_{1} ≠ p_{2} and p_{1} ≠ q and p_{2} ≠ q. Then p_{1}, p_{2} are neighbours wrt q, q on C.

(37) If p_{1} ≠ p_{2} and p_{1} ∈ C and p_{2} ∈ C, then if p_{1}, p_{2} separate q_{1}, q_{2} on C, then q_{1}, q_{2} separate p_{1}, p_{2} on C.

(38) Suppose p_{1} ∈ C and p_{2} ∈ C and q_{1} ∈ C and p_{1} ≠ p_{2} and q_{1} ≠ p_{1} and q_{1} ≠ p_{2} and q_{2} ≠ p_{1} and q_{2} ≠ p_{2}. Then p_{1}, p_{2} are neighbours wrt q_{1}, q_{2} on C or p_{1}, q_{1} are neighbours wrt p_{2}, q_{2} on C.

References

[1] Leszek Borys. Paracompact and metrizable spaces. Formalized Mathematics, 2(4):481– 485, 1991.

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

[3] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 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. The topological space E_{T}^{2}. Arcs, line segments and special polygonal arcs. Formalized Mathematics, 2(5):617–621, 1991.

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

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

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

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

[13] Jarosław Kotowicz. Convergent real sequences. Upper and lower bound of sets of real numbers. Formalized Mathematics, 1(3):477–481, 1990.

[14] Wojciech Leończuk and Krzysztof Prażmowski. Incidence projective spaces. Formalized Mathematics, 2(2):225–232, 1991.

[15] 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.

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

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

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

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

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

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

the ordering of points on a curve. … 177

[22] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics,

1(1):73–83, 1990.

Received September 16, 2002

Order Sorted Algebras^{1}

Josef Urban Charles University Praha

Summary. Initial notions for order sorted algebras.

MML Identifier: OSALG 1.

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

1. Preliminaries

In this paper i is a set.

Let I be a set, let f be a many sorted set indexed by I, and let p be a finite sequence of elements of I. One can check that f · p is finite sequence-like.

Let S be a non empty many sorted signature. A sort symbol of S is an element of S.

Let S be a non empty many sorted signature. (Def. 1) An element of the operation symbols of S is said to be an operation

symbol of S. Let S be a non void non empty many sorted signature and let o be an

operation symbol of S. Then the result sort of o is an element of S.

Let X be a set. Then △_{X} is an order in X. We introduce △_{X}^{o} as a synonym of △_{X}.

Let X be a set. Then △_{X} is an equivalence relation of X. We introduce △_{X}^{r} as a synonym of △_{X}.

1This work was done during author’s research visit in Bialystok, funded by the CALCU-LEMUS grant HPRN-CT-2000-00102.

We introduce overloaded many sorted signatures which are extensions of many sorted signature and are systems

⟨ a carrier, operation symbols, an overloading, an arity, a result sort ⟩, where the carrier is a set, the operation symbols constitute a set, the overloading is an equivalence relation of the operation symbols, the arity is a function from the operation symbols into the carrier^{∗}, and the result sort is a function from the operation symbols into the carrier.

We introduce relation sorted signatures which are extensions of many sorted signature and relational structure and are systems

⟨ a carrier, an internal relation, operation symbols, an arity, a result sort ⟩, where the carrier is a set, the internal relation is a binary relation on the carrier, the operation symbols constitute a set, the arity is a function from the operation symbols into the carrier^{∗}, and the result sort is a function from the operation symbols into the carrier.

We consider overloaded relation sorted signatures as extensions of overloaded many sorted signature and relation sorted signature as systems

⟨ a carrier, an internal relation, operation symbols, an overloading, an arity, a result sort ⟩, where the carrier is a set, the internal relation is a binary relation on the carrier, the operation symbols constitute a set, the overloading is an equivalence relation of the operation symbols, the arity is a function from the operation symbols into the carrier^{∗}, and the result sort is a function from the operation symbols into the carrier.

For simplicity, we use the following convention: A, O are non empty sets, R is an order in A, O_{1} is an equivalence relation of O, f is a function from O into A^{∗}, and g is a function from O into A.

One can prove the following proposition

(1) ⟨A, R, O, O_{1}, f, g⟩ is non empty, non void, reflexive, transitive, and antisymmetric.

Let us consider A, R, O, O_{1}, f, g. One can verify that ⟨A, R, O, O_{1}, f, g⟩ is strict, non empty, reflexive, transitive, and antisymmetric.

2. The Notions: Order-Sorted, Discernable, Op-Discrete

In the sequel S is an overloaded relation sorted signature.

Let us consider S. We say that S is order-sorted if and only if: (Def. 2) S is reflexive, transitive, and antisymmetric.

Let us note that every overloaded relation sorted signature which is ordersorted is also reflexive, transitive, and antisymmetric and there exists an overloaded relation sorted signature which is strict, non empty, non void, and ordersorted.

Let us observe that there exists an overloaded many sorted signature which is non empty and non void.

Let S be a non empty non void overloaded many sorted signature and let x, y be operation symbols of S. The predicate x ≅ y is defined by:

(Def. 3) ⟨⟨x, y⟩⟩∈ the overloading of S.

Let us notice that the predicate x ≅ y is reflexive and symmetric.

One can prove the following proposition

(2) Let S be a non empty non void overloaded many sorted signature and o, o_{1}, o_{2} be operation symbols of S. If o ≅ o_{1} and o_{1} ≅ o_{2}, then o ≅ o_{2}.

Let S be a non empty non void overloaded many sorted signature. We say that S is discernable if and only if the condition (Def. 4) is satisfied.

(Def. 4) Let x, y be operation symbols of S. Suppose x ≅ y and Arity(x) =

Arity(y) and the result sort of x = the result sort of y. Then x = y. We say that S is op-discrete if and only if:

(Def. 5) The overloading of S = △_{the operation symbols of S}^{r}.

The following two propositions are true:

(3) Let S be a non empty non void overloaded many sorted signature. Then S is op-discrete if and only if for all operation symbols x, y of S such that x ≅ y holds x = y.

(4) For every non empty non void overloaded many sorted signature S such that S is op-discrete holds S is discernable.

3. Order Sorted Signature

In the sequel S_{0} is a non empty non void many sorted signature. Let us consider S_{0}. The functor OSSignS_{0} yields a strict non empty non

void order-sorted overloaded relation sorted signature and is defined by the conditions (Def. 6).

(Def. 6)(i) The carrier of S_{0} = the carrier of OSSignS_{0}, (ii) △_{the carrier of S_{0}} = the internal relation of OSSignS_{0}, (iii) the operation symbols of S_{0} = the operation symbols of OSSignS_{0}, (iv) △_{the operation symbols of S_{0}} = the overloading of OSSignS_{0},

(v) the arity of S_{0} = the arity of OSSignS_{0}, and (vi) the result sort of S_{0} = the result sort of OSSignS_{0}. Next we state the proposition

(5) OSSignS_{0} is discrete and op-discrete. Let us mention that there exists a strict non empty non void order-sorted

overloaded relation sorted signature which is discrete, op-discrete, and discernable.

Let us observe that every non empty non void overloaded relation sorted signature which is op-discrete is also discernable.

Let us consider S_{0}. Observe that OSSignS_{0} is discrete and op-discrete. An order sorted signature is a discernable non empty non void order-sorted

overloaded relation sorted signature.

We use the following convention: S is a non empty poset, s_{1}, s_{2} are elements of S, and w_{1}, w_{2} are elements of (the carrier of S)^{∗}.

Let us consider S and let w_{1}, w_{2} be elements of (the carrier of S)^{∗}. The predicate w_{1} w_{2} is defined as follows:

(Def. 7) lenw_{1} = lenw_{2} and for every set i such that i ∈ domw_{1} and for all s_{1},

s_{2} such that s_{1} = w_{1}(i) and s_{2} = w_{2}(i) holds s_{1} s_{2}. Let us note that the predicate w_{1} w_{2} is reflexive.

We now state two propositions:

(6) For all elements w_{1}, w_{2} of (the carrier of S)^{∗} such that w_{1} w_{2} and w_{2} w_{1} holds w_{1} = w_{2}.

(7) If S is discrete and w_{1} w_{2}, then w_{1} = w_{2}. We follow the rules: S is an order sorted signature, o, o_{1}, o_{2} are operation

symbols of S, and w_{1} is an element of (the carrier of S)^{∗}. One can prove the following proposition

(8) If S is discrete and o_{1} ≅ o_{2} and Arity(o_{1}) Arity(o_{2}) and the result sort of o_{1} the result sort of o_{2}, then o_{1} = o_{2}.

Let us consider S and let us consider o. We say that o is monotone if and only if:

(Def. 8) For every o_{2} such that o ≅ o_{2} and Arity(o) Arity(o_{2}) holds the result

sort of o the result sort of o_{2}. Let us consider S. We say that S is monotone if and only if:

(Def. 9) Every operation symbol of S is monotone.

The following proposition is true

(9) If S is op-discrete, then S is monotone. Let us observe that there exists an order sorted signature which is monotone. Let S be a monotone order sorted signature. Observe that there exists an

operation symbol of S which is monotone.

Let S be a monotone order sorted signature. One can check that every operation symbol of S is monotone.

One can check that every order sorted signature which is op-discrete is also monotone.

We now state the proposition

(10) If S is monotone and Arity(o_{1}) = ∅ and o_{1} ≅ o_{2} and Arity(o_{2}) = ∅, then o_{1} = o_{2}.

Let us consider S, o, o_{1}, w_{1}. We say that o_{1} has least args for o, w_{1} if and only if:

(Def. 10) o ≅ o_{1} and w_{1} Arity(o_{1}) and for every o_{2} such that o ≅ o_{2} and

w_{1} Arity(o_{2}) holds Arity(o_{1}) Arity(o_{2}). We say that o_{1} has least sort for o, w_{1} if and only if:

(Def. 11) o ≅ o_{1} and w_{1} Arity(o_{1}) and for every o_{2} such that o ≅ o_{2} and

w_{1} Arity(o_{2}) holds the result sort of o_{1} the result sort of o_{2}. Let us consider S, o, o_{1}, w_{1}. We say that o_{1} has least rank for o, w_{1} if and

only if: (Def. 12) o_{1} has least args for o, w_{1} and least sort for o, w_{1}.

Let us consider S, o. We say that o is regular if and only if: (Def. 13) o is monotone and for every w_{1} such that w_{1} Arity(o) holds there

exists o_{1} which has least args for o, w_{1}. Let S_{1} be a monotone order sorted signature. We say that S_{1} is regular if

and only if: (Def. 14) Every operation symbol of S_{1} is regular.

In the sequel S_{1} is a monotone order sorted signature, o, o_{1} are operation symbols of S_{1}, and w_{1} is an element of (the carrier of S_{1})^{∗}.

We now state two propositions:

(11) S_{1} is regular iff for all o, w_{1} such that w_{1} Arity(o) holds there exists o_{1} which has least rank for o, w_{1}.

(12) For every monotone order sorted signature S_{1} such that S_{1} is op-discrete

holds S_{1} is regular. One can verify that there exists a monotone order sorted signature which is

regular.

Let us mention that every monotone order sorted signature which is opdiscrete is also regular.

Let S_{2} be a regular monotone order sorted signature. One can verify that every operation symbol of S_{2} is regular.

We adopt the following rules: S_{2} is a regular monotone order sorted signature, o, o_{3}, o_{4} are operation symbols of S_{2}, and w_{1} is an element of (the carrier of S_{2})^{∗}.

One can prove the following proposition

(13) If w_{1} Arity(o) and o_{3} has least args for o, w_{1} and o_{4} has least args for

o, w_{1}, then o_{3} = o_{4}. Let us consider S_{2}, o, w_{1}. Let us assume that w_{1} Arity(o). The functor

LBound(o, w_{1}) yields an operation symbol of S_{2} and is defined as follows: (Def. 15) LBound(o, w_{1}) has least args for o, w_{1}.

One can prove the following proposition (14) For every w_{1} such that w_{1} Arity(o) holds LBound(o, w_{1}) has least

rank for o, w_{1}. In the sequel R denotes a non empty poset and z denotes a non empty set. Let us consider R, z. The functor ConstOSSet(R, z) yielding a many sorted

set indexed by the carrier of R is defined by: (Def. 16) ConstOSSet(R, z) = (the carrier of R) ⟼→ z.

The following proposition is true

(15) ConstOSSet(R, z) is non-empty and for all elements s_{1}, s_{2} of R such that

s_{1} s_{2} holds (ConstOSSet(R, z))(s_{1}) ⊆ (ConstOSSet(R, z))(s_{2}). Let C be a 1-sorted structure.

(Def. 17) A many sorted set indexed by the carrier of C is said to be a many sorted

set indexed by C. Let us consider R, z. Then ConstOSSet(R, z) is a many sorted set indexed

by R.

Let us consider R and let M be a many sorted set indexed by R. We say that M is order-sorted if and only if:

(Def. 18) For all elements s_{1}, s_{2} of R such that s_{1} s_{2} holds M(s_{1}) ⊆ M(s_{2}).

Next we state the proposition

(16) ConstOSSet(R, z) is order-sorted.

Let us consider R. Observe that there exists a many sorted set indexed by R which is order-sorted.

Let us consider R, z. Then ConstOSSet(R, z) is an order-sorted many sorted set indexed by R.

Let R be a non empty poset. An order sorted set of R is an order-sorted many sorted set indexed by R.

Let R be a non empty poset. Observe that there exists an order sorted set of R which is non-empty.

We adopt the following convention: s_{1}, s_{2} denote sort symbols of S, o, o_{1}, o_{2}, o_{3} denote operation symbols of S, and w_{1}, w_{2} denote elements of (the carrier of S)^{∗}.

Let us consider S and let M be an algebra over S. We say that M is ordersorted if and only if:

(Def. 19) For all s_{1}, s_{2} such that s_{1} s_{2} holds (the sorts of M)(s_{1}) ⊆ (the sorts

of M)(s_{2}). The following proposition is true

(17) For every algebra M over S holds M is order-sorted iff the sorts of M

are an order sorted set of S. In the sequel C_{1} denotes a many sorted function from (ConstOSSet(S, z))^{#} ·

the arity of S into ConstOSSet(S, z) · the result sort of S.

Let us consider S, z, C_{1}. The functor ConstOSA(S, z, C_{1}) yielding a strict non-empty algebra over S is defined by:

(Def. 20) The sorts of ConstOSA(S, z, C_{1}) = ConstOSSet(S, z) and the characte-

ristics of ConstOSA(S, z, C_{1}) = C_{1}. One can prove the following proposition

(18) ConstOSA(S, z, C_{1}) is order-sorted.

Let us consider S. One can check that there exists an algebra over S which is strict, non-empty, and order-sorted.

Let us consider S, z, C_{1}. One can verify that ConstOSA(S, z, C_{1}) is ordersorted.

Let us consider S. An order sorted algebra of S is an order-sorted algebra over S.

Next we state the proposition

(19) For every discrete order sorted signature S holds every algebra over S is

order-sorted. Let S be a discrete order sorted signature. Observe that every algebra over

S is order-sorted.

In the sequel A denotes an order sorted algebra of S. We now state the proposition

(20) If w_{1} w_{2}, then (the sorts of A)^{#}(w_{1}) ⊆ (the sorts of A)^{#}(w_{2}). In the sequel M is an algebra over S_{0}. Let us consider S_{0}, M. The functor OSAlgM yielding a strict order sorted

algebra of OSSignS_{0} is defined as follows: (Def. 21) The sorts of OSAlgM = the sorts of M and the characteristics of

OSAlgM = the characteristics of M. In the sequel A denotes an order sorted algebra of S. We now state the proposition

(21) For all elements w_{1}, w_{2}, w_{3} of (the carrier of S)^{∗} such that w_{1} w_{2} and

w_{2} w_{3} holds w_{1} w_{3}. Let us consider S, o_{1}, o_{2}. The predicate o_{1} o_{2} is defined as follows:

(Def. 22) o_{1} ≅ o_{2} and Arity(o_{1}) Arity(o_{2}) and the result sort of o_{1} the result

sort of o_{2}. Let us note that the predicate o_{1} o_{2} is reflexive.

We now state several propositions:

(22) If o_{1} o_{2} and o_{2} o_{1}, then o_{1} = o_{2}.

(23) If o_{1} o_{2} and o_{2} o_{3}, then o_{1} o_{3}.

(24) If the result sort of o_{1} the result sort of o_{2}, then Result(o_{1}, A) ⊆ Result(o_{2}, A).

(25) If Arity(o_{1}) Arity(o_{2}), then Args(o_{1}, A) ⊆ Args(o_{2}, A).

(26) If o_{1} o_{2}, then Args(o_{1}, A) ⊆ Args(o_{2}, A) and Result(o_{1}, A) ⊆

Result(o_{2}, A). Let us consider S, A. We say that A is monotone if and only if:

(Def. 23) For all o_{1}, o_{2} such that o_{1} o_{2} holds Den(o_{2}, A)↾ Args(o_{1}, A) = Den(o_{1},

A). We now state two propositions:

(27) Let A be a non-empty order sorted algebra of S. Then A is monotone if and only if for all o_{1}, o_{2} such that o_{1} o_{2} holds Den(o_{1}, A) ⊆ Den(o_{2}, A).

(28) If S is discrete and op-discrete, then A is monotone.

Let us consider S, z and let z_{1} be an element of z. The functor TrivialOSA(S, z, z_{1}) yielding a strict order sorted algebra of S is defined by:

(Def. 24) The sorts of TrivialOSA(S, z, z_{1}) = ConstOSSet(S, z) and for every o

holds Den(o, TrivialOSA(S, z, z_{1})) = Args(o, TrivialOSA(S, z, z_{1})) ⟼→ z_{1}. Next we state the proposition

(29) For every element z_{1} of z holds TrivialOSA(S, z, z_{1}) is non-empty and

TrivialOSA(S, z, z_{1}) is monotone. Let us consider S. Note that there exists an order sorted algebra of S which

is monotone, strict, and non-empty.

Let us consider S, z and let z_{1} be an element of z. One can check that TrivialOSA(S, z, z_{1}) is monotone and non-empty.

In the sequel o_{5}, o_{6} are operation symbols of S. Let us consider S. The functor OperNamesS yields a non empty family of

subsets of the operation symbols of S and is defined as follows: (Def. 25) OperNamesS = Classes(the overloading of S).

Let us consider S. One can check that every element of OperNamesS is non empty.

Let us consider S. An OperName of S is an element of OperNamesS. Let us consider S, o_{5}. The functor Nameo_{5} yields an OperName of S and is

defined by: (Def. 26) Nameo_{5} = [o_{5}]_{the overloading of S}.

Next we state three propositions:

(30) o_{5} ≅ o_{6} iff o_{6} ∈ [o_{5}]_{the overloading of S}.

(31) o_{5} ≅ o_{6} iff Nameo_{5} = Nameo_{6}.

(32) For every set X holds X is an OperName of S iff there exists o_{5} such

that X = Nameo_{5}. Let us consider S and let o be an OperName of S. We see that the element

of o is an operation symbol of S.

Next we state two propositions:

order sorted algebras 187

(33) For every OperName o_{8} of S and for every operation symbol o_{7} of S holds o_{7} is an element of o_{8} iff Nameo_{7} = o_{8}.

(34) Let S_{2} be a regular monotone order sorted signature, o_{5}, o_{6} be operation symbols of S_{2}, and w be an element of (the carrier of S_{2})^{∗}. If o_{5} ≅ o_{6} and lenArity(o_{5}) = lenArity(o_{6}) and w Arity(o_{5}) and w Arity(o_{6}), then LBound(o_{5}, w) = LBound(o_{6}, w).

Let S_{2} be a regular monotone order sorted signature, let o_{8} be an OperName of S_{2}, and let w be an element of (the carrier of S_{2})^{∗}. Let us assume that there exists an element o_{7} of o_{8} such that w Arity(o_{7}). The functor LBound(o_{8}, w) yields an element of o_{8} and is defined as follows:

(Def. 27) For every element o_{7} of o_{8} such that w Arity(o_{7}) holds

LBound(o_{8}, w) = LBound(o_{7}, w). Next we state the proposition

(35) Let S be a regular monotone order sorted signature, o be an operation symbol of S, and w_{1} be an element of (the carrier of S)^{∗}. If w_{1} Arity(o), then LBound(o, w_{1}) o.

Acknowledgments

Thanks to Joseph Goguen, for providing me with his articles on osas, and Andrzej Trybulec, for suggesting and funding this work in Bialystok.

References

[1] Grzegorz Bancerek. König’s theorem. Formalized Mathematics, 1(3):589–593, 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 and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

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

[6] Adam Grabowski. On the category of posets. Formalized Mathematics, 5(4):501–505, 1996.

[7] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147–152, 1990.

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

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

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

[11] Andrzej Trybulec. Many sorted algebras. Formalized Mathematics, 5(1):37–42, 1996.

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

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

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

188 josef urban

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

1990.

Received September 19, 2002

Subalgebras of an Order Sorted Algebra. Lattice of Subalgebras^{1}

Josef Urban Charles University Praha

MML Identifier: OSALG 2.

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

1. Auxiliary Facts about Order Sorted Sets

In this paper x denotes a set and R denotes a non empty poset.

Next we state two propositions:

(1) For all order sorted sets X, Y of R holds X ∩ Y is an order sorted set of R.

(2) For all order sorted sets X, Y of R holds X ∪ Y is an order sorted set of R.

Let R be a non empty poset and let M be an order sorted set of R. A many sorted subset indexed by M is said to be an order sorted subset of M if:

(Def. 1) It is an order sorted set of R.

Let R be a non empty poset and let M be a non-empty order sorted set of R. Note that there exists an order sorted subset of M which is non-empty.

1This work was done during author’s research visit in Bialystok, funded by the CALCU-LEMUS grant HPRN-CT-2000-00102.

2. Constants of an Order Sorted Algebra

Let S be an order sorted signature and let U_{0} be an order sorted algebra of S. A many sorted subset indexed by the sorts of U_{0} is said to be an OSSubset of U_{0} if:

(Def. 2) It is an order sorted set of S.

Let S be an order sorted signature. Note that there exists an order sorted algebra of S which is monotone, strict, and non-empty.

Let S be an order sorted signature and let U_{0} be a non-empty order sorted algebra of S. One can verify that there exists an OSSubset of U_{0} which is nonempty.

Next we state the proposition

(3) For every non void strict non empty many sorted signature S_{0} with constant operations holds OSSignS_{0} has constant operations.

Let us note that there exists an order sorted signature which is strict and has constant operations.

3. Subalgebras of an Order Sorted Algebra

The following proposition is true

(4) Let S be an order sorted signature and U_{0} be an order sorted algebra of S. Then ⟨the sorts of U_{0}, the characteristics of U_{0}⟩ is order-sorted.

Let S be an order sorted signature and let U_{0} be an order sorted algebra of S. One can verify that there exists a subalgebra of U_{0} which is order-sorted.

Let S be an order sorted signature and let U_{0} be an order sorted algebra of S. An OSSubAlgebra of U_{0} is an order-sorted subalgebra of U_{0}.

Let S be an order sorted signature and let U_{0} be an order sorted algebra of S. One can verify that there exists an OSSubAlgebra of U_{0} which is strict.

Let S be an order sorted signature and let U_{0} be a non-empty order sorted algebra of S. Observe that there exists an OSSubAlgebra of U_{0} which is nonempty and strict.

One can prove the following proposition

(5) Let S be an order sorted signature, U_{0} be an order sorted algebra of S, and U_{1} be an algebra over S. Then U_{1} is an OSSubAlgebra of U_{0} if and only if the following conditions are satisfied:

(i) the sorts of U_{1} are an OSSubset of U_{0}, and (ii) for every OSSubset B of U_{0} such that B = the sorts of U_{1} holds B is

operations closed and the characteristics of U_{1} = Opers(U_{0}, B). In the sequel S_{1} is an order sorted signature and O_{0}, O_{1}, O_{2} are order sorted

algebras of S_{1}.

The following propositions are true:

(6) O_{1} is an OSSubAlgebra of O_{1}.

(7) If O_{0} is an OSSubAlgebra of O_{1} and O_{1} is an OSSubAlgebra of O_{2}, then O_{0} is an OSSubAlgebra of O_{2}.

(8) If O_{1} is a strict OSSubAlgebra of O_{2} and O_{2} is a strict OSSubAlgebra of O_{1}, then O_{1} = O_{2}.

(9) For all OSSubAlgebras O_{1}, O_{2} of O_{0} such that the sorts of O_{1} ⊆ the sorts of O_{2} holds O_{1} is an OSSubAlgebra of O_{2}.

(10) For all strict OSSubAlgebras O_{1}, O_{2} of O_{0} such that the sorts of O_{1} = the

sorts of O_{2} holds O_{1} = O_{2}. In the sequel s, s_{1}, s_{2} are sort symbols of S_{1}. Let us consider S_{1}, O_{0}, s. The functor OSConstants(O_{0}, s) yields a subset

of (the sorts of O_{0})(s) and is defined by: (Def. 3) OSConstants(O_{0}, s) = ⋃{Constants(O_{0}, s_{2}) : s_{2} s}.

One can prove the following proposition

(11) Constants(O_{0}, s) ⊆ OSConstants(O_{0}, s).

Let us consider S_{1} and let M be a many sorted set indexed by the carrier of S_{1}. The functor OSClM yields an order sorted set of S_{1} and is defined by:

(Def. 4) For every sort symbol s of S_{1} holds (OSClM)(s) = ⋃{M(s_{1}) : s_{1} s}.

Next we state three propositions:

(12) For every many sorted set M indexed by the carrier of S_{1} holds M ⊆ OSClM.

(13) Let M be a many sorted set indexed by the carrier of S_{1} and A be an order sorted set of S_{1}. If M ⊆ A, then OSClM ⊆ A.

(14) For every order sorted signature S and for every order sorted set X of

S holds OSClX = X. Let us consider S_{1}, O_{0}. The functor OSConstantsO_{0} yields an OSSubset of

O_{0} and is defined by: (Def. 5) For every sort symbol s of S_{1} holds (OSConstantsO_{0})(s) =

OSConstants(O_{0}, s). One can prove the following propositions:

(15) Constants(O_{0}) ⊆ OSConstantsO_{0}.

(16) For every OSSubset A of O_{0} such that Constants(O_{0}) ⊆ A holds OSConstantsO_{0} ⊆ A.

(17) For every OSSubset A of O_{0} holds OSConstantsO_{0} = OSClConstants(O_{0}).

(18) For every OSSubAlgebra O_{1} of O_{0} holds OSConstantsO_{0} is an OSSubset of O_{1}.

(19) Let S be an order sorted signature with constant operations, O_{0} be a nonempty order sorted algebra of S, and O_{1} be a non-empty OSSubAlgebra of O_{0}. Then OSConstantsO_{0} is a non-empty OSSubset of O_{1}.

4. Order Sorted Subsets of an Order Sorted Algebra

Next we state the proposition

(20) Let I be a set, M be a many sorted set indexed by I, and x be a set.

Then x is a many sorted subset indexed by M if and only if x ∈ ∏(2^{M}). Let R be a non empty poset and let M be an order sorted set of R. The

functor OSboolM yielding a set is defined by: (Def. 6) For every set x holds x ∈ OSboolM iff x is an order sorted subset of M.

Let S be an order sorted signature, let U_{0} be an order sorted algebra of S, and let A be an OSSubset of U_{0}. The functor OSSubSortA yields a set and is defined as follows:

(Def. 7) OSSubSortA = {x; x ranges over elements of SubSorts(A): x is an order

sorted set of S}. We now state two propositions:

(21) For every OSSubset A of O_{0} holds OSSubSortA ⊆ SubSorts(A).

(22) For every OSSubset A of O_{0} holds the sorts of O_{0} ∈ OSSubSortA. Let us consider S_{1}, O_{0} and let A be an OSSubset of O_{0}. One can check that

OSSubSortA is non empty.

Let us consider S_{1}, O_{0}. The functor OSSubSortO_{0} yielding a set is defined by:

(Def. 8) OSSubSortO_{0} = {x; x ranges over elements of SubSorts(O_{0}):

x is an order sorted set of S_{1}}. The following proposition is true

(23) For every OSSubset A of O_{0} holds OSSubSortA ⊆ OSSubSortO_{0}. Let us consider S_{1}, O_{0}. One can check that OSSubSortO_{0} is non empty. Let us consider S_{1}, O_{0} and let e be an element of OSSubSortO_{0}. The functor

@e yielding an OSSubset of O_{0} is defined by: (Def. 9) ^{@}e = e.

Next we state two propositions:

(24) For all OSSubsets A, B of O_{0} holds B ∈ OSSubSortA iff B is operations closed and OSConstantsO_{0} ⊆ B and A ⊆ B.

(25) For every OSSubset B of O_{0} holds B ∈ OSSubSortO_{0} iff B is operations

closed. Let us consider S_{1}, O_{0}, let A be an OSSubset of O_{0}, and let s be an element

of the carrier of S_{1}. The functor OSSubSort(A, s) yields a set and is defined by: (Def. 10) For every set x holds x ∈ OSSubSort(A, s) iff there exists an OSSubset

B of O_{0} such that B ∈ OSSubSortA and x = B(s). We now state three propositions:

(26) For every OSSubset A of O_{0} and for all sort symbols s_{1}, s_{2} of S_{1} such that s_{1} s_{2} holds OSSubSort(A, s_{2}) is coarser than OSSubSort(A, s_{1}).

(27) For every OSSubset A of O_{0} and for every sort symbol s of S_{1} holds OSSubSort(A, s) ⊆ SubSort(A, s).

(28) For every OSSubset A of O_{0} and for every sort symbol s of S_{1} holds (the

sorts of O_{0})(s) ∈ OSSubSort(A, s). Let us consider S_{1}, O_{0}, let A be an OSSubset of O_{0}, and let s be a sort

symbol of S_{1}. Note that OSSubSort(A, s) is non empty.

Let us consider S_{1}, O_{0} and let A be an OSSubset of O_{0}. The functor OSMSubSortA yields an OSSubset of O_{0} and is defined by:

(Def. 11) For every sort symbol s of S_{1} holds (OSMSubSortA)(s) =

⋂ OSSubSort(A, s). Let us consider S_{1}, O_{0} and let A be an OSSubset of O_{0}. We say that A is

os-opers closed if and only if: (Def. 12) A is operations closed.

Let us consider S_{1}, O_{0}. One can verify that there exists an OSSubset of O_{0} which is os-opers closed.

Next we state several propositions:

(29) For every OSSubset A of O_{0} holds OSConstantsO_{0} ∪ A ⊆ OSMSubSortA.

(30) For every OSSubset A of O_{0} such that OSConstantsO_{0} ∪A is non-empty holds OSMSubSortA is non-empty.

(31) Let o be an operation symbol of S_{1}, A be an OSSubset of O_{0}, and B be an OSSubset of O_{0}. If B ∈ OSSubSortA, then ((OSMSubSortA)^{#} · the arity of S_{1})(o) ⊆ (B^{#} · the arity of S_{1})(o).

(32) Let o be an operation symbol of S_{1}, A be an OSSubset of O_{0}, and B be an OSSubset of O_{0}. Suppose B ∈ OSSubSortA. Then rng(Den(o, O_{0})↾((OSMSubSortA)^{#}·the arity of S_{1})(o)) ⊆ (B·the result sort of S_{1})(o).

(33) Let o be an operation symbol of S_{1} and A be an OSSubset of O_{0}. Then rng(Den(o, O_{0})↾((OSMSubSortA)^{#} · the arity of S_{1})(o)) ⊆ (OSMSubSortA · the result sort of S_{1})(o).

(34) For every OSSubset A of O_{0} holds OSMSubSortA is operations closed

and A ⊆ OSMSubSortA. Let us consider S_{1}, O_{0} and let A be an OSSubset of O_{0}. Note that

OSMSubSortA is os-opers closed.

5. Operations on Subalgebras of an Order Sorted Algebra

Let us consider S_{1}, O_{0} and let A be an os-opers closed OSSubset of O_{0}. Note that O_{0}↾A is order-sorted.

Let us consider S_{1}, O_{0} and let O_{1}, O_{2} be OSSubAlgebras of O_{0}. One can check that O_{1} ∩ O_{2} is order-sorted.

Let us consider S_{1}, O_{0} and let A be an OSSubset of O_{0}. The functor OSGenA yields a strict OSSubAlgebra of O_{0} and is defined by the conditions (Def. 13).

(Def. 13)(i) A is an OSSubset of OSGenA, and

(ii) for every OSSubAlgebra O_{1} of O_{0} such that A is an OSSubset of O_{1}

holds OSGenA is an OSSubAlgebra of O_{1}. We now state several propositions:

(35) For every OSSubset A of O_{0} holds OSGenA = O_{0}↾ OSMSubSortA and the sorts of OSGenA = OSMSubSortA.

(36) Let S be a non void non empty many sorted signature, U_{0} be an algebra over S, and A be a subset of U_{0}. Then Gen(A) = U_{0}↾ MSSubSort(A) and the sorts of Gen(A) = MSSubSort(A).

(37) For every OSSubset A of O_{0} holds the sorts of Gen(A) ⊆ the sorts of OSGenA.

(38) For every OSSubset A of O_{0} holds Gen(A) is a subalgebra of OSGenA.

(39) Let O_{0} be a strict order sorted algebra of S_{1} and B be an OSSubset of O_{0}. If B = the sorts of O_{0}, then OSGenB = O_{0}.

(40) For every strict OSSubAlgebra O_{1} of O_{0} and for every OSSubset B of O_{0} such that B = the sorts of O_{1} holds OSGenB = O_{1}.

(41) For every non-empty order sorted algebra U_{0} of S_{1} and for every OSSubAlgebra U_{1} of U_{0} holds OSGenOSConstantsU_{0} ∩ U_{1} = OSGenOSConstantsU_{0}.

Let us consider S_{1}, let U_{0} be a non-empty order sorted algebra of S_{1}, and let U_{1}, U_{2} be OSSubAlgebras of U_{0}. The functor U_{1} ⊔_{os} U_{2} yielding a strict OSSubAlgebra of U_{0} is defined by:

(Def. 14) For every OSSubset A of U_{0} such that A = (the sorts of U_{1}) ∪ (the sorts

of U_{2}) holds U_{1} ⊔_{os} U_{2} = OSGenA. One can prove the following propositions:

(42) Let U_{0} be a non-empty order sorted algebra of S_{1}, U_{1} be an OSSubAlgebra of U_{0}, and A, B be OSSubsets of U_{0}. If B = A ∪ the sorts of U_{1}, then OSGenA ⊔_{os} U_{1} = OSGenB.

(43) Let U_{0} be a non-empty order sorted algebra of S_{1}, U_{1} be an OSSubAlgebra of U_{0}, and B be an OSSubset of U_{0}. If B = the sorts of U_{0}, then OSGenB ⊔_{os} U_{1} = OSGenB.

(44) For every non-empty order sorted algebra U_{0} of S_{1} and for all OSSubAlgebras U_{1}, U_{2} of U_{0} holds U_{1} ⊔_{os} U_{2} = U_{2} ⊔_{os} U_{1}.

(45) For every non-empty order sorted algebra U_{0} of S_{1} and for all strict OSSubAlgebras U_{1}, U_{2} of U_{0} holds U_{1} ∩ (U_{1} ⊔_{os} U_{2}) = U_{1}.

(46) For every non-empty order sorted algebra U_{0} of S_{1} and for all strict OSSubAlgebras U_{1}, U_{2} of U_{0} holds U_{1} ∩ U_{2} ⊔_{os} U_{2} = U_{2}.

6. The Lattice of Subalgebras of an Order Sorted Algebra

Let us consider S_{1}, O_{0}. The functor OSSubO_{0} yields a set and is defined by: (Def. 15) For every x holds x ∈ OSSubO_{0} iff x is a strict OSSubAlgebra of O_{0}.

We now state the proposition

(47) OSSubO_{0} ⊆ Subalgebras(O_{0}).

Let S be an order sorted signature and let U_{0} be an order sorted algebra of S. Note that OSSubU_{0} is non empty.

Let us consider S_{1}, O_{0}. Then OSSubO_{0} is a subset of Subalgebras(O_{0}). Let us consider S_{1} and let U_{0} be a non-empty order sorted algebra of S_{1}.

The functor OSAlgJoinU_{0} yields a binary operation on OSSubU_{0} and is defined as follows:

(Def. 16) For all elements x, y of OSSubU_{0} and for all strict OSSubAlgebras U_{1}, U_{2}

of U_{0} such that x = U_{1} and y = U_{2} holds (OSAlgJoinU_{0})(x, y) = U_{1}⊔_{os}U_{2}. Let us consider S_{1} and let U_{0} be a non-empty order sorted algebra of S_{1}. The

functor OSAlgMeetU_{0} yields a binary operation on OSSubU_{0} and is defined as follows:

(Def. 17) For all elements x, y of OSSubU_{0} and for all strict OSSubAlgebras U_{1}, U_{2}

of U_{0} such that x = U_{1} and y = U_{2} holds (OSAlgMeetU_{0})(x, y) = U_{1} ∩U_{2}. The following proposition is true

(48) For every non-empty order sorted algebra U_{0} of S_{1} and for all elements

x, y of OSSubU_{0} holds (OSAlgMeetU_{0})(x, y) = (MSAlgMeet(U_{0}))(x, y). In the sequel U_{0} denotes a non-empty order sorted algebra of S_{1}. We now state four propositions:

(49) OSAlgJoinU_{0} is commutative.

(50) OSAlgJoinU_{0} is associative.

(51) OSAlgMeetU_{0} is commutative.

(52) OSAlgMeetU_{0} is associative.

Let us consider S_{1} and let U_{0} be a non-empty order sorted algebra of S_{1}. The functor OSSubAlLatticeU_{0} yielding a strict lattice is defined by:

(Def. 18) OSSubAlLatticeU_{0} = ⟨OSSubU_{0}, OSAlgJoinU_{0}, OSAlgMeetU_{0}⟩.

Next we state the proposition

(53) For every non-empty order sorted algebra U_{0} of S_{1} holds OSSubAlLatticeU_{0} is bounded.

196 josef urban

Let us consider S_{1} and let U_{0} be a non-empty order sorted algebra of S_{1}. Note that OSSubAlLatticeU_{0} is bounded.

The following propositions are true:

(54) For every non-empty order sorted algebra U_{0} of S_{1} holds ⊥_{OSSubAlLattice U_{0}} = OSGenOSConstantsU_{0}.

(55) Let U_{0} be a non-empty order sorted algebra of S_{1} and B be an OSSubset of U_{0}. If B = the sorts of U_{0}, then ⊤_{OSSubAlLattice U_{0}} = OSGenB.

(56) For every strict non-empty order sorted algebra U_{0} of S_{1} holds ⊤_{OSSubAlLattice U_{0}} = U_{0}.

Acknowledgments

Thanks to Joseph Goguen, for providing me with his articles on osas, and Andrzej Trybulec, for suggesting and funding this work in Bialystok.

References

[1] Grzegorz Bancerek. König’s theorem. Formalized Mathematics, 1(3):589–593, 1990.

[2] Ewa Burakowska. Subalgebras of many sorted algebra. Lattice of subalgebras. Formalized Mathematics, 5(1):47–54, 1996.

[3] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.

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

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

[6] Artur Korniłowicz. Definitions and basic properties of boolean & union of many sorted sets. Formalized Mathematics, 5(2):279–281, 1996.

[7] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147–152, 1990.

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

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

[10] Andrzej Trybulec. Many sorted algebras. Formalized Mathematics, 5(1):37–42, 1996.

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

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

[13] Josef Urban. Order sorted algebras. Formalized Mathematics, 10(3):179–188, 2002.

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

[15] Stanisław Żukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215– 222, 1990.

Homomorphisms of Order Sorted Algebras^{1}

Josef Urban Charles University Praha

MML Identifier: OSALG 3.

The notation and terminology used in this paper have been introduced in the following articles: [8], [12], [14], [15], [4], [5], [2], [1], [9], [11], [7], [10], [3], [13], and [6].

In this paper R denotes a non empty poset and S_{1} denotes an order sorted signature.

Let us consider R and let F be a many sorted function indexed by the carrier of R. We say that F is order-sorted if and only if:

(Def. 1) For all elements s_{1}, s_{2} of R such that s_{1} s_{2} and for every set a_{1} such

that a_{1} ∈ domF (s_{1}) holds a_{1} ∈ domF (s_{2}) and F (s_{1})(a_{1}) = F (s_{2})(a_{1}). Next we state several propositions:

(1) For every set I and for every many sorted set A indexed by I holds id_{A} is “1-1”.

(2) Let F be a many sorted function indexed by the carrier of R. Suppose F is order-sorted. Let s_{1}, s_{2} be elements of R. If s_{1} s_{2}, then domF (s_{1}) ⊆ domF (s_{2}) and F (s_{1}) ⊆ F (s_{2}).

(3) Let A be an order sorted set of R, B be a non-empty order sorted set of R, and F be a many sorted function from A into B. Then F is order-sorted if and only if for all elements s_{1}, s_{2} of R such that s_{1} s_{2} and for every set a_{1} such that a_{1} ∈ A(s_{1}) holds F (s_{1})(a_{1}) = F (s_{2})(a_{1}).

(4) Let F be a many sorted function indexed by the carrier of R. Suppose F is order-sorted. Let w_{1}, w_{2} be elements of (the carrier of R)^{∗}. If w_{1} w_{2}, then F^{#}(w_{1}) ⊆ F^{#}(w_{2}).

1This work was done during author’s research visit in Bialystok, funded by the CALCU-LEMUS grant HPRN-CT-2000-00102.

(5) For every order sorted set A of R holds id_{A} is order-sorted.

(6) Let A be an order sorted set of R, B, C be non-empty order sorted sets of R, F be a many sorted function from A into B, and G be a many sorted function from B into C. If F is order-sorted and G is order-sorted, then G ∘ F is order-sorted.

(7) Let A, B be order sorted sets of R and F be a many sorted function from A into B. If F is “1-1”, onto, and order-sorted, then F^{−1} is order-sorted.

(8) Let A be an order sorted set of R and F be a many sorted function indexed by the carrier of R. If F is order-sorted, then F ^{∘} A is an order sorted set of R.

Let us consider S_{1} and let U_{1}, U_{2} be order sorted algebras of S_{1}. We say that U_{1} and U_{2} are os-isomorphic if and only if:

(Def. 2) There exists a many sorted function from U_{1} into U_{2} which is an isomor-

phism of U_{1} and U_{2} and order-sorted. The following propositions are true:

(9) For every order sorted algebra U_{1} of S_{1} holds U_{1} and U_{1} are osisomorphic.

(10) Let U_{1}, U_{2} be non-empty order sorted algebras of S_{1}. If U_{1} and U_{2} are

os-isomorphic, then U_{2} and U_{1} are os-isomorphic. Let us consider S_{1} and let U_{1}, U_{2} be order sorted algebras of S_{1}. Let us note

that the predicate U_{1} and U_{2} are os-isomorphic is reflexive.

One can prove the following propositions:

(11) Let U_{1}, U_{2}, U_{3} be non-empty order sorted algebras of S_{1}. Suppose U_{1} and U_{2} are os-isomorphic and U_{2} and U_{3} are os-isomorphic. Then U_{1} and U_{3} are os-isomorphic.

(12) Let U_{1}, U_{2} be non-empty order sorted algebras of S_{1} and F be a many sorted function from U_{1} into U_{2}. Suppose F is order-sorted and a homomorphism of U_{1} into U_{2}. Then ImF is order-sorted.

(13) Let U_{1}, U_{2} be non-empty order sorted algebras of S_{1} and F be a many sorted function from U_{1} into U_{2}. Suppose F is order-sorted. Let o_{1}, o_{2} be operation symbols of S_{1}. Suppose o_{1} o_{2}. Let x be an element of Args(o_{1}, U_{1}) and x_{1} be an element of Args(o_{2}, U_{1}). If x = x_{1}, then F #x = F #x_{1}.

(14) Let U_{1} be a monotone non-empty order sorted algebra of S_{1}, U_{2} be a non-empty order sorted algebra of S_{1}, and F be a many sorted function from U_{1} into U_{2}. Suppose F is order-sorted and a homomorphism of U_{1} into U_{2}. Then ImF is order-sorted and ImF is a monotone order sorted algebra of S_{1}.

(15) For every monotone order sorted algebra U_{1} of S_{1} holds every OSSubAlgebra of U_{1} is monotone.

Let us consider S_{1} and let U_{1} be a monotone order sorted algebra of S_{1}. One can check that there exists an OSSubAlgebra of U_{1} which is monotone.

Let us consider S_{1} and let U_{1} be a monotone order sorted algebra of S_{1}. One can verify that every OSSubAlgebra of U_{1} is monotone.

The following propositions are true:

(16) Let U_{1}, U_{2} be non-empty order sorted algebras of S_{1} and F be a many sorted function from U_{1} into U_{2}. Suppose F is a homomorphism of U_{1} into U_{2} and order-sorted. Then there exists a many sorted function G from U_{1} into ImF such that F = G and G is order-sorted and an epimorphism of U_{1} onto ImF.

(17) Let U_{1}, U_{2} be non-empty order sorted algebras of S_{1} and F be a many sorted function from U_{1} into U_{2}. Suppose F is a homomorphism of U_{1} into U_{2} and order-sorted. Then there exists a many sorted function F_{1} from U_{1} into ImF and there exists a many sorted function F_{2} from ImF into U_{2} such that

(i) F_{1} is an epimorphism of U_{1} onto ImF, (ii) F_{2} is a monomorphism of ImF into U_{2}, (iii) F = F_{2} ∘ F_{1}, (iv) F_{1} is order-sorted, and

(v) F_{2} is order-sorted. Let us consider S_{1} and let U_{1} be an order sorted algebra of S_{1}. Note that

⟨the sorts of U_{1}, the characteristics of U_{1}⟩ is order-sorted.

One can prove the following propositions:

(18) Let U_{1} be an order sorted algebra of S_{1}. Then U_{1} is monotone if and only if ⟨the sorts of U_{1}, the characteristics of U_{1}⟩ is monotone.

(19) Let U_{1}, U_{2} be strict non-empty order sorted algebras of S_{1}. Suppose U_{1} and U_{2} are os-isomorphic. Then U_{1} is monotone if and only if U_{2} is monotone.

Acknowledgments

Thanks to Joseph Goguen, for providing me with his articles on osas, and Andrzej Trybulec, for suggesting and funding this work in Bialystok.

References

[1] Grzegorz Bancerek. König’s theorem. Formalized Mathematics, 1(3):589–593, 1990.

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

[3] Ewa Burakowska. Subalgebras of many sorted algebra. Lattice of subalgebras. Formalized Mathematics, 5(1):47–54, 1996.

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

[5] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, [6] Małgorzata Korolkiewicz. Homomorphisms of many sorted algebras. Formalized Mathe-

matics, 5(1):61–65, 1996.

[7] Beata Madras. Product of family of universal algebras. Formalized Mathematics, 4(1):103– 108, 1993.

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

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

[10] Andrzej Trybulec. Many sorted algebras. Formalized Mathematics, 5(1):37–42, 1996.

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

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

[13] Josef Urban. Order sorted algebras. Formalized Mathematics, 10(3):179–188, 2002.

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

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

Order Sorted Quotient Algebra^{1}

Josef Urban Charles University Praha

MML Identifier: OSALG 4.

The terminology and notation used in this paper are introduced in the following papers: [7], [16], [21], [24], [4], [25], [6], [15], [9], [19], [8], [14], [5], [3], [1], [20], [17], [2], [12], [18], [10], [13], [23], [22], and [11].

1. Preliminaries

Let R be a non empty poset. One can verify that there exists an order sorted set of R which is binary relation yielding.

Let R be a non empty poset, let A, B be many sorted sets indexed by the carrier of R, and let I_{1} be a many sorted relation between A and B. We say that I_{1} is os-compatible if and only if the condition (Def. 1) is satisfied.

(Def. 1) Let s_{1}, s_{2} be elements of the carrier of R. Suppose s_{1} s_{2}. Let x, y be

sets. If x ∈ A(s_{1}) and y ∈ B(s_{1}), then ⟨⟨x, y⟩⟩∈ I_{1}(s_{1}) iff ⟨⟨x, y⟩⟩∈ I_{1}(s_{2}). Let R be a non empty poset and let A, B be many sorted sets indexed by

the carrier of R. A many sorted relation between A and B is said to be an order sorted relation of A, B if:

(Def. 2) It is os-compatible.

The following proposition is true

(1) Let R be a non empty poset, A, B be many sorted sets indexed by the carrier of R, and O_{1} be a many sorted relation between A and B. If O_{1} is os-compatible, then O_{1} is an order sorted set of R.

1This work was done during author’s research visit in Bialystok, funded by the CALCU-LEMUS grant HPRN-CT-2000-00102.

Let R be a non empty poset and let A be a many sorted set indexed by the carrier of R. An order sorted relation of A is an order sorted relation of A, A.

Let S be an order sorted signature and let U_{1} be an order sorted algebra of S. A many sorted relation indexed by U_{1} is said to be an order sorted relation of U_{1} if:

(Def. 3) It is os-compatible.

Let S be an order sorted signature and let U_{1} be an order sorted algebra of S. One can check that there exists an order sorted relation of U_{1} which is equivalence.

Let S be an order sorted signature and let U_{1} be a non-empty order sorted algebra of S. Note that there exists an equivalence order sorted relation of U_{1} which is MSCongruence-like.

Let S be an order sorted signature and let U_{1} be a non-empty order sorted algebra of S. An order sorted congruence of U_{1} is a MSCongruence-like equivalence order sorted relation of U_{1}.

Let R be a non empty poset. The functor PathRelR yields an equivalence relation of the carrier of R and is defined by the condition (Def. 4).

(Def. 4) Let x, y be sets. Then ⟨⟨x, y⟩⟩ ∈ PathRelR if and only if the following

conditions are satisfied:

(i) x ∈ the carrier of R, (ii) y ∈ the carrier of R, and (iii) there exists a finite sequence p of elements of the carrier of R such that

1 < lenp and p(1) = x and p(lenp) = y and for every natural number n such that 2 n and n lenp holds ⟨⟨p(n), p(n − 1)⟩⟩ ∈ the internal relation of R or ⟨⟨p(n − 1), p(n)⟩⟩∈ the internal relation of R.

One can prove the following proposition

(2) For every non empty poset R and for all elements s_{1}, s_{2} of the carrier of R such that s_{1} s_{2} holds ⟨⟨s_{1}, s_{2}⟩⟩∈ PathRelR.

Let R be a non empty poset and let s_{1}, s_{2} be elements of the carrier of R. The predicate s_{1} ≅ s_{2} is defined as follows:

(Def. 5) ⟨⟨s_{1}, s_{2}⟩⟩∈ PathRelR.

Let us notice that the predicate s_{1} ≅ s_{2} is reflexive and symmetric. One can prove the following proposition

(3) For every non empty poset R and for all elements s_{1}, s_{2}, s_{3} of the carrier of R such that s_{1} ≅ s_{2} and s_{2} ≅ s_{3} holds s_{1} ≅ s_{3}.

Let R be a non empty poset. The functor ComponentsR yields a non empty family of subsets of the carrier of R and is defined by:

(Def. 6) ComponentsR = ClassesPathRelR.

Let R be a non empty poset. Note that every element of ComponentsR is non empty.

Let R be a non empty poset. A subset of R is called a component of R if: (Def. 7) It ∈ ComponentsR.

Let R be a non empty poset and let s_{1} be an element of the carrier of R. The functor ·_{CSp} s_{1} yielding a component of R is defined by:

(Def. 8) ·_{CSp} s_{1} = [s_{1}]_{PathRel R}.

The following two propositions are true:

(4) For every non empty poset R and for every element s_{1} of the carrier of R holds s_{1} ∈ ·_{CSp} s_{1}.

(5) For every non empty poset R and for all elements s_{1}, s_{2} of the carrier of R such that s_{1} s_{2} holds ·_{CSp} s_{1} = ·_{CSp} s_{2}.

Let R be a non empty poset, let A be a many sorted set indexed by the carrier of R, and let C be a component of R. A-carrier of C is defined as follows:

(Def. 9) A-carrier of C = ⋃{A(s); s ranges over elements of the carrier of R:

s ∈ C}. We now state the proposition

(6) Let R be a non empty poset, A be a many sorted set indexed by the carrier of R, s be an element of the carrier of R, and x be a set. If x ∈ A(s), then x ∈ A-carrier of ·_{CSp} s.

Let R be a non empty poset. We say that R is locally directed if and only if:

(Def. 10) Every component of R is directed. The following three propositions are true:

(7) For every discrete non empty poset R and for all elements x, y of the carrier of R such that ⟨⟨x, y⟩⟩∈ PathRelR holds x = y.

(8) Let R be a discrete non empty poset and C be a component of R. Then there exists an element x of the carrier of R such that C = {x}.

(9) Every discrete non empty poset is locally directed. Let us observe that there exists a non empty poset which is locally directed. One can verify that there exists an order sorted signature which is locally

directed.

Let us observe that every non empty poset which is discrete is also locally directed.

Let S be a locally directed non empty poset. Note that every component of S is directed.

One can prove the following proposition

(10) ∅ is an equivalence relation of ∅. Let S be a locally directed order sorted signature, let A be an order sorted

algebra of S, let E be an equivalence order sorted relation of A, and let C be a component of S. The functor CompClass(E, C) yielding an equivalence relation of (the sorts of A)-carrier of C is defined as follows:

(Def. 11) For all sets x, y holds ⟨⟨x, y⟩⟩ ∈ CompClass(E, C) iff there exists an

element s_{1} of the carrier of S such that s_{1} ∈ C and ⟨⟨x, y⟩⟩∈ E(s_{1}). Let S be a locally directed order sorted signature, let A be an order sorted

algebra of S, let E be an equivalence order sorted relation of A, and let s_{1} be an element of the carrier of S. The functor OSClass(E, s_{1}) yielding a subset of ClassesCompClass(E, ·_{CSp} s_{1}) is defined by:

(Def. 12) For every set z holds z ∈ OSClass(E, s_{1}) iff there exists a set x such that

x ∈ (the sorts of A)(s_{1}) and z = [x]_{CompClass (E,·_{CSp} s_{1})}. Let S be a locally directed order sorted signature, let A be a non-empty

order sorted algebra of S, let E be an equivalence order sorted relation of A, and let s_{1} be an element of the carrier of S. One can verify that OSClass(E, s_{1}) is non empty.

The following proposition is true

(11) Let S be a locally directed order sorted signature, A be an order sorted algebra of S, E be an equivalence order sorted relation of A, and s_{1}, s_{2} be elements of the carrier of S. If s_{1} s_{2}, then OSClass(E, s_{1}) ⊆ OSClass(E, s_{2}).

Let S be a locally directed order sorted signature, let A be an order sorted algebra of S, and let E be an equivalence order sorted relation of A. The functor OSClassE yields an order sorted set of S and is defined as follows:

(Def. 13) For every element s_{1} of the carrier of S holds (OSClassE)(s_{1}) =

OSClass(E, s_{1}). Let S be a locally directed order sorted signature, let A be a non-empty

order sorted algebra of S, and let E be an equivalence order sorted relation of A. One can check that OSClassE is non-empty.

Let S be a locally directed order sorted signature, let U_{1} be a non-empty order sorted algebra of S, let E be an equivalence order sorted relation of U_{1}, let s be an element of the carrier of S, and let x be an element of (the sorts of U_{1})(s). The functor OSClass(E, x) yields an element of OSClass(E, s) and is defined by:

(Def. 14) OSClass(E, x) = [x]_{CompClass (E,·_{CSp} s)}.

One can prove the following three propositions:

(12) Let R be a locally directed non empty poset and x, y be elements of the carrier of R. Given an element z of the carrier of R such that z x and z y. Then there exists an element u of R such that x u and y u.

(13) Let S be a locally directed order sorted signature, U_{1} be a non-empty order sorted algebra of S, E be an equivalence order sorted relation of U_{1}, s be an element of the carrier of S, and x, y be elements of (the sorts of U_{1})(s). Then OSClass(E, x) = OSClass(E, y) if and only if ⟨⟨x, y⟩⟩∈ E(s).

(14) Let S be a locally directed order sorted signature, U_{1} be a non-empty order sorted algebra of S, E be an equivalence order sorted relation of U_{1}, s_{1}, s_{2} be elements of the carrier of S, and x be an element of (the sorts of U_{1})(s_{1}). Suppose s_{1} s_{2}. Let y be an element of (the sorts of U_{1})(s_{2}). If y = x, then OSClass(E, x) = OSClass(E, y).

2. Order Sorted Quotient Algebra

In the sequel S denotes a locally directed order sorted signature and o denotes an element of the operation symbols of S.

Let us consider S, o, let A be a non-empty order sorted algebra of S, let R be an order sorted congruence of A, and let x be an element of Args(o, A). The functor Rosx yields an element of ∏(OSClassR ·Arity(o)) and is defined by the condition (Def. 15).

(Def. 15) Let n be a natural number. Suppose n ∈ domArity(o). Then there exists an element y of (the sorts of A)(Arity(o)_{n}) such that y = x(n) and (Rosx)(n) = OSClass(R, y).

Let us consider S, o, let A be a non-empty order sorted algebra of S, and let R be an order sorted congruence of A. The functor OSQuotRes(R, o) yielding a function from ((the sorts of A) · (the result sort of S))(o) into (OSClassR · the result sort of S)(o) is defined as follows:

(Def. 16) For every element x of (the sorts of A)(the result sort of o) holds

(OSQuotRes(R, o))(x) = OSClass(R, x). The functor OSQuotArgs(R, o) yielding a function from ((the sorts of A)^{#} · the arity of S)(o) into ((OSClassR)^{#} · the arity of S)(o) is defined by:

(Def. 17) For every element x of Args(o, A) holds (OSQuotArgs(R, o))(x) = Rosx.

Let us consider S, let A be a non-empty order sorted algebra of S, and let R be an order sorted congruence of A. The functor OSQuotResR yields a many sorted function from (the sorts of A) · (the result sort of S) into OSClassR · the result sort of S and is defined by:

(Def. 18) For every operation symbol o of S holds (OSQuotResR)(o) =

OSQuotRes(R, o). The functor OSQuotArgsR yields a many sorted function from (the sorts of A)^{#} · the arity of S into (OSClassR)^{#} · the arity of S and is defined as follows:

(Def. 19) For every operation symbol o of S holds (OSQuotArgsR)(o) =

OSQuotArgs(R, o). One can prove the following proposition (15) Let A be a non-empty order sorted algebra of S, R be an order sorted

congruence of A, and x be a set. Suppose x ∈ ((OSClassR)^{#} · the arity of S)(o). Then there exists an element a of Args(o, A) such that x = Rosa.

Let us consider S, o, let A be a non-empty order sorted algebra of S, and let R be an order sorted congruence of A. The functor OSQuotCharact(R, o) yielding a function from ((OSClassR)^{#} · the arity of S)(o) into (OSClassR · the result sort of S)(o) is defined as follows:

(Def. 20) For every element a of Args(o, A) such that Rosa ∈ ((OSClassR)^{#} · the arity of S)(o) holds (OSQuotCharact(R, o))(Rosa) = (OSQuotRes(R, o) · Den(o, A))(a).

Let us consider S, let A be a non-empty order sorted algebra of S, and let R be an order sorted congruence of A. The functor OSQuotCharactR yielding a many sorted function from (OSClassR)^{#} · the arity of S into OSClassR · the result sort of S is defined as follows:

(Def. 21) For every operation symbol o of S holds (OSQuotCharactR)(o) =

OSQuotCharact(R, o). Let us consider S, let U_{1} be a non-empty order sorted algebra of S, and let

R be an order sorted congruence of U_{1}. The functor QuotOSAlg(U_{1}, R) yields an order sorted algebra of S and is defined by:

(Def. 22) QuotOSAlg(U_{1}, R) = ⟨OSClassR, OSQuotCharactR⟩.

Let us consider S, let U_{1} be a non-empty order sorted algebra of S, and let R be an order sorted congruence of U_{1}. One can check that QuotOSAlg(U_{1}, R) is strict and non-empty.

Let us consider S, let U_{1} be a non-empty order sorted algebra of S, let R be an order sorted congruence of U_{1}, and let s be an element of the carrier of S. The functor OSNatHom(U_{1}, R, s) yielding a function from (the sorts of U_{1})(s) into OSClass(R, s) is defined by:

(Def. 23) For every element x of (the sorts of U_{1})(s) holds (OSNatHom(U_{1}, R, s))(x) =

OSClass(R, x). Let us consider S, let U_{1} be a non-empty order sorted algebra of S, and let

R be an order sorted congruence of U_{1}. The functor OSNatHom(U_{1}, R) yielding a many sorted function from U_{1} into QuotOSAlg(U_{1}, R) is defined as follows:

(Def. 24) For every element s of the carrier of S holds (OSNatHom(U_{1}, R))(s) =

OSNatHom(U_{1}, R, s). Next we state two propositions:

(16) Let U_{1} be a non-empty order sorted algebra of S and R be an order sorted congruence of U_{1}. Then OSNatHom(U_{1}, R) is an epimorphism of U_{1} onto QuotOSAlg(U_{1}, R) and OSNatHom(U_{1}, R) is order-sorted.

(17) Let U_{1}, U_{2} be non-empty order sorted algebras of S and F be a many sorted function from U_{1} into U_{2}. Suppose F is a homomorphism of U_{1} into U_{2} and order-sorted. Then Congruence(F) is an order sorted congruence of U_{1}.

Let us consider S, let U_{1}, U_{2} be non-empty order sorted algebras of S, and let F be a many sorted function from U_{1} into U_{2}. Let us assume that F is a homomorphism of U_{1} into U_{2} and order-sorted. The functor OSCngF yielding an order sorted congruence of U_{1} is defined as follows:

(Def. 25) OSCngF = Congruence(F).

Let us consider S, let U_{1}, U_{2} be non-empty order sorted algebras of S, let F be a many sorted function from U_{1} into U_{2}, and let s be an element of the carrier of S. Let us assume that F is a homomorphism of U_{1} into U_{2} and order-sorted. The functor OSHomQuot(F, s) yields a function from (the sorts of QuotOSAlg(U_{1}, OSCngF))(s) into (the sorts of U_{2})(s) and is defined as follows:

(Def. 26) For every element x of (the sorts of U_{1})(s) holds

(OSHomQuot(F, s))(OSClass(OSCngF, x)) = F (s)(x). Let us consider S, let U_{1}, U_{2} be non-empty order sorted algebras of S, and

let F be a many sorted function from U_{1} into U_{2}. The functor OSHomQuotF yields a many sorted function from QuotOSAlg(U_{1}, OSCngF) into U_{2} and is defined by:

(Def. 27) For every element s of the carrier of S holds (OSHomQuotF)(s) =

OSHomQuot(F, s). The following three propositions are true:

(18) Let U_{1}, U_{2} be non-empty order sorted algebras of S and F be a many sorted function from U_{1} into U_{2}. Suppose F is a homomorphism of U_{1} into U_{2} and order-sorted. Then OSHomQuotF is a monomorphism of QuotOSAlg(U_{1}, OSCngF) into U_{2} and OSHomQuotF is order-sorted.

(19) Let U_{1}, U_{2} be non-empty order sorted algebras of S and F be a many sorted function from U_{1} into U_{2}. Suppose F is an epimorphism of U_{1} onto U_{2} and order-sorted. Then OSHomQuotF is an isomorphism of QuotOSAlg(U_{1}, OSCngF) and U_{2}.

(20) Let U_{1}, U_{2} be non-empty order sorted algebras of S and F be a many sorted function from U_{1} into U_{2}. Suppose F is an epimorphism of U_{1} onto U_{2} and order-sorted. Then QuotOSAlg(U_{1}, OSCngF) and U_{2} are isomorphic.

Let S be an order sorted signature, let U_{1} be a non-empty order sorted algebra of S, and let R be an equivalence order sorted relation of U_{1}. We say that R is monotone if and only if the condition (Def. 28) is satisfied.

(Def. 28) Let o_{1}, o_{2} be operation symbols of S. Suppose o_{1} o_{2}. Let x_{1} be an element of Args(o_{1}, U_{1}) and x_{2} be an element of Args(o_{2}, U_{1}). Suppose that for every natural number y such that y ∈ domx_{1} holds ⟨⟨x_{1}(y), x_{2}(y)⟩⟩ ∈ R(Arity(o_{2})_{y}). Then ⟨⟨(Den(o_{1}, U_{1}))(x_{1}), (Den(o_{2}, U_{1}))(x_{2})⟩⟩ ∈ R(the result sort of o_{2}).

One can prove the following two propositions:

(21) Let S be an order sorted signature and U_{1} be a non-empty order sorted algebra of S. Then [[the sorts of U_{1}, the sorts of U_{1}]] is an order sorted congruence of U_{1}.

(22) Let S be an order sorted signature, U_{1} be a non-empty order sorted algebra of S, and R be an order sorted congruence of U_{1}. If R = [[the sorts of U_{1}, the sorts of U_{1}]], then R is monotone.

Let S be an order sorted signature and let U_{1} be a non-empty order sorted algebra of S. One can verify that there exists an order sorted congruence of U_{1} which is monotone.

Let S be an order sorted signature and let U_{1} be a non-empty order sorted algebra of S. Note that there exists an equivalence order sorted relation of U_{1} which is monotone.

The following proposition is true

(23) Let S be an order sorted signature and U_{1} be a non-empty order sorted algebra of S. Then every monotone equivalence order sorted relation of U_{1} is MSCongruence-like.

Let S be an order sorted signature and let U_{1} be a non-empty order sorted algebra of S. Observe that every equivalence order sorted relation of U_{1} which is monotone is also MSCongruence-like.

We now state the proposition

(24) Let S be an order sorted signature and U_{1} be a monotone non-empty order sorted algebra of S. Then every order sorted congruence of U_{1} is monotone.

Let S be an order sorted signature and let U_{1} be a monotone non-empty order sorted algebra of S. Observe that every order sorted congruence of U_{1} is monotone.

Let us consider S, let U_{1} be a non-empty order sorted algebra of S, and let R be a monotone order sorted congruence of U_{1}. Note that QuotOSAlg(U_{1}, R) is monotone.

We now state two propositions:

(25) Let given S, U_{1} be a non-empty order sorted algebra of S, and R be a monotone order sorted congruence of U_{1}. Then QuotOSAlg(U_{1}, R) is a monotone order sorted algebra of S.

(26) Let U_{1} be a non-empty order sorted algebra of S, U_{2} be a monotone nonempty order sorted algebra of S, and F be a many sorted function from U_{1} into U_{2}. Suppose F is a homomorphism of U_{1} into U_{2} and order-sorted. Then OSCngF is monotone.

Let us consider S, let U_{1}, U_{2} be non-empty order sorted algebras of S, let F be a many sorted function from U_{1} into U_{2}, let R be an order sorted congruence of U_{1}, and let s be an element of the carrier of S. Let us assume that F is a homomorphism of U_{1} into U_{2} and order-sorted and R ⊆ OSCngF. The functor OSHomQuot(F, R, s) yields a function from (the sorts of QuotOSAlg(U_{1}, R))(s) into (the sorts of U_{2})(s) and is defined as follows:

(Def. 29) For every element x of (the sorts of U_{1})(s) holds

(OSHomQuot(F, R, s))(OSClass(R, x)) = F (s)(x). Let us consider S, let U_{1}, U_{2} be non-empty order sorted algebras of S,

let F be a many sorted function from U_{1} into U_{2}, and let R be an order sorted congruence of U_{1}. The functor OSHomQuot(F, R) yields a many sorted function from QuotOSAlg(U_{1}, R) into U_{2} and is defined as follows:

(Def. 30) For every element s of the carrier of S holds (OSHomQuot(F, R))(s) =

OSHomQuot(F, R, s). Next we state the proposition

(27) Let U_{1}, U_{2} be non-empty order sorted algebras of S, F be a many sorted function from U_{1} into U_{2}, and R be an order sorted congruence of U_{1}. Suppose F is a homomorphism of U_{1} into U_{2} and order-sorted and R ⊆ OSCngF. Then OSHomQuot(F, R) is a homomorphism of QuotOSAlg(U_{1}, R) into U_{2} and OSHomQuot(F, R) is order-sorted.

Acknowledgments

Thanks to Joseph Goguen, for providing me with his articles on osas, and Andrzej Trybulec, for suggesting and funding this work in Bialystok.

References

[1] Grzegorz Bancerek. König’s theorem. Formalized Mathematics, 1(3):589–593, 1990.

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

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

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

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

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

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

[8] Adam Grabowski. On the category of posets. Formalized Mathematics, 5(4):501–505, 1996.

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

[10] Małgorzata Korolkiewicz. Homomorphisms of many sorted algebras. Formalized Mathematics, 5(1):61–65, 1996.

[11] Małgorzata Korolkiewicz. Many sorted quotient algebra. Formalized Mathematics, 5(1):79–84, 1996.

[12] Beata Madras. Product of family of universal algebras. Formalized Mathematics, 4(1):103– 108, 1993.

[13] Beata Madras. Products of many sorted algebras. Formalized Mathematics, 5(1):55–60, 1996.

[14] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147–152, 1990.

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

[16] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 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] Wojciech A. Trybulec. Partially ordered sets. Formalized Mathematics, 1(2):313–319, 1990.

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

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

[22] Josef Urban. Homomorphisms of order sorted algebras. Formalized Mathematics, 10(3):197–200, 2002.

[23] Josef Urban. Order sorted algebras. Formalized Mathematics, 10(3):179–188, 2002.

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

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

Free Order Sorted Universal Algebra^{1}

Josef Urban Charles University Praha

Summary. Free Order Sorted Universal Algebra — the general construction for any locally directed signatures.

MML Identifier: OSAFREE.

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

1. Preliminaries

In this paper S is an order sorted signature.

Let S be an order sorted signature and let U_{0} be an order sorted algebra of S. A subset of U_{0} is called an order sorted generator set of U_{0} if:

(Def. 1) For every OSSubset O of U_{0} such that O = OSClit holds the sorts of

OSGenO = the sorts of U_{0}. The following proposition is true

(1) Let S be an order sorted signature, U_{0} be a strict non-empty order sorted algebra of S, and A be a subset of U_{0}. Then A is an order sorted generator set of U_{0} if and only if for every OSSubset O of U_{0} such that O = OSClA holds OSGenO = U_{0}.

Let us consider S, let U_{0} be a monotone order sorted algebra of S, and let I_{1} be an order sorted generator set of U_{0}. We say that I_{1} is osfree if and only if the condition (Def. 2) is satisfied.

1This work was done during author’s research visit in Bialystok, funded by the CALCU-LEMUS grant HPRN-CT-2000-00102.

(Def. 2) Let U_{1} be a monotone non-empty order sorted algebra of S and f be a many sorted function from I_{1} into the sorts of U_{1}. Then there exists a many sorted function h from U_{0} into U_{1} such that h is a homomorphism of U_{0} into U_{1} and order-sorted and h ↾ I_{1} = f.

Let S be an order sorted signature and let I_{1} be a monotone order sorted algebra of S. We say that I_{1} is osfree if and only if:

(Def. 3) There exists an order sorted generator set of I_{1} which is osfree.

2. Construction of Free Order Sorted Algebras for Given Signature

Let S be an order sorted signature and let X be a many sorted set indexed by S. The functor OSRELX yields a relation between [: the operation symbols of S, {the carrier of S}:] ∪ ⋃ coprod(X) and ([: the operation symbols of S, {the carrier of S}:] ∪ ⋃ coprod(X))^{∗} and is defined by the condition (Def. 4).

(Def. 4) Let a be an element of [: the operation symbols of S, {the carrier of S}:] ∪ ⋃ coprod(X) and b be an element of ([: the operation symbols of S, {the carrier of S}:] ∪ ⋃ coprod(X))^{∗}. Then ⟨⟨a, b⟩⟩∈ OSRELX if and only if the following conditions are satisfied:

(i) a ∈ [: the operation symbols of S, {the carrier of S}:], and (ii) for every operation symbol o of S such that ⟨⟨o, the carrier of S⟩⟩ = a

holds lenb = lenArity(o) and for every set x such that x ∈ domb holds if b(x) ∈ [: the operation symbols of S, {the carrier of S}:], then for every operation symbol o_{1} of S such that ⟨⟨o_{1}, the carrier of S⟩⟩ = b(x) holds the result sort of o_{1} Arity(o)_{x} and if b(x) ∈ ⋃ coprod(X), then there exists an element i of the carrier of S such that i Arity(o)_{x} and b(x) ∈ coprod(i, X).

In the sequel S is an order sorted signature, X is a many sorted set indexed by S, o is an operation symbol of S, and b is an element of ([: the operation symbols of S, {the carrier of S}:] ∪ ⋃ coprod(X))^{∗}.

One can prove the following proposition

(2) ⟨⟨⟨⟨o, the carrier of S⟩⟩, b⟩⟩∈ OSRELX if and only if the following conditions are satisfied:

(i) lenb = lenArity(o), and (ii) for every set x such that x ∈ domb holds if b(x) ∈ [: the operation

symbols of S, {the carrier of S}:], then for every operation symbol o_{1} of S such that ⟨⟨o_{1}, the carrier of S⟩⟩ = b(x) holds the result sort of o_{1} Arity(o)_{x} and if b(x) ∈ ⋃ coprod(X), then there exists an element i of the carrier of S such that i Arity(o)_{x} and b(x) ∈ coprod(i, X).

Let S be an order sorted signature and let X be a many sorted set indexed by S. The functor DTConOSAX yielding a tree construction structure is defined by:

(Def. 5) DTConOSAX = ⟨[: the operation symbols of S, {the carrier of S}:] ∪

⋃ coprod(X), OSRELX⟩. Let S be an order sorted signature and let X be a many sorted set indexed

by S. Note that DTConOSAX is strict and non empty.

The following proposition is true

(3) Let S be an order sorted signature and X be a non-empty many sorted set indexed by S. Then the nonterminals of DTConOSAX = [: the operation symbols of S, {the carrier of S}:] and the terminals of DTConOSAX = ⋃ coprod(X).

Let S be an order sorted signature and let X be a non-empty many sorted set indexed by S. Note that DTConOSAX has terminals, nonterminals, and useful nonterminals.

The following proposition is true

(4) Let S be an order sorted signature, X be a non-empty many sorted set indexed by S, and t be a set. Then t ∈ the terminals of DTConOSAX if and only if there exists an element s of the carrier of S and there exists a set x such that x ∈ X(s) and t = ⟨⟨x, s⟩⟩.

Let S be an order sorted signature, let X be a non-empty many sorted set indexed by S, and let o be an operation symbol of S. The functor OSSym(o, X) yielding a symbol of DTConOSAX is defined as follows:

(Def. 6) OSSym(o, X) = ⟨⟨o, the carrier of S⟩⟩.

Let S be an order sorted signature, let X be a non-empty many sorted set indexed by S, and let s be an element of the carrier of S. The functor ParsedTerms(X, s) yielding a subset of TS(DTConOSAX) is defined by the condition (Def. 7).

(Def. 7) ParsedTerms(X, s) = {a; a ranges over elements of TS(DTConOSAX): ⋁_{s_{1} : element of the carrier of S} ⋁_{x: set} (s_{1} s ∧ x ∈ X(s_{1}) ∧ a = the root tree of ⟨⟨x, s_{1}⟩⟩) ∨ ⋁_{o: operation symbol of S} (⟨⟨o, the carrier of S⟩⟩ = a(∅) ∧ the result sort of o s)}.

Let S be an order sorted signature, let X be a non-empty many sorted set indexed by S, and let s be an element of the carrier of S. Note that ParsedTerms(X, s) is non empty.

Let S be an order sorted signature and let X be a non-empty many sorted set indexed by S. The functor ParsedTermsX yields an order sorted set of S and is defined by:

(Def. 8) For every element s of the carrier of S holds (ParsedTermsX)(s) = ParsedTerms(X, s).

Let S be an order sorted signature and let X be a non-empty many sorted set indexed by S. One can verify that ParsedTermsX is non-empty.

The following four propositions are true:

(5) Let S be an order sorted signature, X be a non-empty many sorted set indexed by S, o be an operation symbol of S, and x be a set. Suppose x ∈ ((ParsedTermsX)^{#} · the arity of S)(o). Then x is a finite sequence of elements of TS(DTConOSAX).

(6) Let S be an order sorted signature, X be a non-empty many sorted set indexed by S, o be an operation symbol of S, and p be a finite sequence of elements of TS(DTConOSAX). Then p ∈ ((ParsedTermsX)^{#} · the arity of S)(o) if and only if domp = domArity(o) and for every natural number n such that n ∈ domp holds p(n) ∈ ParsedTerms(X, Arity(o)_{n}).

(7) Let S be an order sorted signature, X be a non-empty many sorted set indexed by S, o be an operation symbol of S, and p be a finite sequence of elements of TS(DTConOSAX). Then OSSym(o, X) ⇒ the roots of p if and only if p ∈ ((ParsedTermsX)^{#} · the arity of S)(o).

(8) For every order sorted signature S and for every non-empty many sorted set X indexed by S holds ⋃ rngParsedTermsX = TS(DTConOSAX).

Let S be an order sorted signature, let X be a non-empty many sorted set indexed by S, and let o be an operation symbol of S. The functor PTDenOp(o, X) yields a function from ((ParsedTermsX)^{#} · the arity of S)(o) into (ParsedTermsX · the result sort of S)(o) and is defined as follows:

(Def. 9) For every finite sequence p of elements of TS(DTConOSAX) such that OSSym(o, X) ⇒ the roots of p holds (PTDenOp(o, X))(p) = OSSym(o, X)-tree(p).

Let S be an order sorted signature and let X be a non-empty many sorted set indexed by S. The functor PTOperX yields a many sorted function from (ParsedTermsX)^{#} · the arity of S into ParsedTermsX · the result sort of S and is defined by:

(Def. 10) For every operation symbol o of S holds (PTOperX)(o) =

PTDenOp(o, X). Let S be an order sorted signature and let X be a non-empty many sorted set

indexed by S. The functor ParsedTermsOSAX yielding an order sorted algebra of S is defined as follows:

(Def. 11) ParsedTermsOSAX = ⟨ParsedTermsX, PTOperX⟩.

Let S be an order sorted signature and let X be a non-empty many sorted set indexed by S. One can check that ParsedTermsOSAX is strict and non-empty.

Let S be an order sorted signature, let X be a non-empty many sorted set indexed by S, and let o be an operation symbol of S. Then OSSym(o, X) is a nonterminal of DTConOSAX.

Next we state several propositions:

(9) Let S be an order sorted signature, X be a non-empty many sorted set indexed by S, and s be an element of the carrier of S. Then (the sorts of ParsedTermsOSAX)(s) = {a; a ranges over elements of TS(DTConOSAX): ⋁_{s_{1} : element of the carrier of S} ⋁_{x: set} (s_{1} s ∧ x ∈ X(s_{1}) ∧ a = the root tree of ⟨⟨x, s_{1}⟩⟩) ∨ ⋁_{o: operation symbol of S} (⟨⟨o, the carrier of S⟩⟩= a(∅) ∧ the result sort of o s)}.

(10) Let S be an order sorted signature, X be a non-empty many sorted set indexed by S, s, s_{1} be elements of the carrier of S, and x be a set. Suppose x ∈ X(s). Then

(i) the root tree of ⟨⟨x, s⟩⟩ is an element of TS(DTConOSAX), (ii) for every set z holds ⟨⟨z, the carrier of S⟩⟩ ≠ (the root tree of ⟨⟨x, s⟩⟩)(∅),

and (iii) the root tree of ⟨⟨x, s⟩⟩∈ (the sorts of ParsedTermsOSAX)(s_{1}) iff s s_{1}.

(11) Let S be an order sorted signature, X be a non-empty many sorted set indexed by S, t be an element of TS(DTConOSAX), and o be an operation symbol of S. Suppose t(∅) = ⟨⟨o, the carrier of S⟩⟩. Then

(i) there exists a subtree sequence p joinable by OSSym(o, X) such that t = OSSym(o, X)-tree(p) and OSSym(o, X) ⇒ the roots of p and p ∈ Args(o, ParsedTermsOSAX) and t = (Den(o, ParsedTermsOSAX))(p),

(ii) for every element s_{2} of the carrier of S and for every set x holds t ≠ the

root tree of ⟨⟨x, s_{2}⟩⟩, and (iii) for every element s_{1} of the carrier of S holds t ∈ (the sorts of

ParsedTermsOSAX)(s_{1}) iff the result sort of o s_{1}.

(12) Let S be an order sorted signature, X be a non-empty many sorted set indexed by S, n_{1} be a symbol of DTConOSAX, and t_{1} be a finite sequence of elements of TS(DTConOSAX). Suppose n_{1} ⇒ the roots of t_{1}. Then

(i) n_{1} ∈ the nonterminals of DTConOSAX, (ii) n_{1}-tree(t_{1}) ∈ TS(DTConOSAX), and (iii) there exists an operation symbol o of S such that n_{1} = ⟨⟨o, the carrier

of S⟩⟩ and t_{1} ∈ Args(o, ParsedTermsOSAX) and n_{1}-tree(t_{1}) = (Den(o, ParsedTermsOSAX))(t_{1}) and for every element s_{1} of the carrier of S holds n_{1}-tree(t_{1}) ∈ (the sorts of ParsedTermsOSAX)(s_{1}) iff the result sort of o s_{1}.

(13) Let S be an order sorted signature, X be a non-empty many sorted set indexed by S, o be an operation symbol of S, and x be a finite sequence. Then x ∈ Args(o, ParsedTermsOSAX) if and only if the following conditions are satisfied:

(i) x is a finite sequence of elements of TS(DTConOSAX), and (ii) OSSym(o, X) ⇒ the roots of x.

(14) Let S be an order sorted signature, X be a non-empty many sorted set indexed by S, and t be an element of TS(DTConOSAX). Then there exists a sort symbol s of S such that t ∈ (the sorts of ParsedTermsOSAX)(s) and for every element s_{1} of the carrier of S such that t ∈ (the sorts of ParsedTermsOSAX)(s_{1}) holds s s_{1}.

Let S be an order sorted signature, let X be a non-empty many sorted set indexed by S, and let t be an element of TS(DTConOSAX). The functor LeastSortt yields a sort symbol of S and is defined by the conditions (Def. 12).

(Def. 12)(i) t ∈ (the sorts of ParsedTermsOSAX)(LeastSortt), and

(ii) for every element s_{1} of the carrier of S such that t ∈ (the sorts of

ParsedTermsOSAX)(s_{1}) holds LeastSortt s_{1}. Let S be a non empty non void many sorted signature and let A be a non-

empty algebra over S. (Def. 13) An element of ⋃ (the sorts of A) is said to be an element of A.

We now state four propositions:

(15) Let S be an order sorted signature, X be a non-empty many sorted set indexed by S, and x be a set. Then x is an element of ParsedTermsOSAX if and only if x is an element of TS(DTConOSAX).

(16) Let S be an order sorted signature, X be a non-empty many sorted set indexed by S, s be an element of the carrier of S, and x be a set. If x ∈ (the sorts of ParsedTermsOSAX)(s), then x is an element of TS(DTConOSAX).

(17) Let S be an order sorted signature, X be a non-empty many sorted set indexed by S, s be an element of the carrier of S, and x be a set. Suppose x ∈ X(s). Let t be an element of TS(DTConOSAX). If t = the root tree of ⟨⟨x, s⟩⟩, then LeastSortt = s.

(18) Let S be an order sorted signature, X be a non-empty many sorted set indexed by S, o be an operation symbol of S, x be an element of Args(o, ParsedTermsOSAX), and t be an element of TS(DTConOSAX). If t = (Den(o, ParsedTermsOSAX))(x), then LeastSortt = the result sort of o.

Let S be an order sorted signature, let X be a non-empty many sorted set indexed by S, and let o_{2} be an operation symbol of S. Note that Args(o_{2}, ParsedTermsOSAX) is non empty.

Let S be a locally directed order sorted signature, let X be a nonempty many sorted set indexed by S, and let x be a finite sequence of elements of TS(DTConOSAX). The functor LeastSortsx yielding an element of (the carrier of S)^{∗} is defined as follows:

(Def. 14) domLeastSortsx = domx and for every natural number y such that y ∈ domx there exists an element t of TS(DTConOSAX) such that t = x(y) and (LeastSortsx)(y) = LeastSortt.

We now state the proposition

(19) Let S be a locally directed order sorted signature, X be a non-empty many sorted set indexed by S, o be an operation symbol of S, and x be a finite sequence of elements of TS(DTConOSAX). Then LeastSortsx Arity(o) if and only if x ∈ Args(o, ParsedTermsOSAX).

Let us note that there exists a monotone order sorted signature which is locally directed and regular.

Let S be a locally directed regular monotone order sorted signature, let X be a non-empty many sorted set indexed by S, let o be an operation symbol of S, and let x be a finite sequence of elements of TS(DTConOSAX). Let us assume that OSSym(LBound(o, LeastSortsx), X) ⇒ the roots of x. The functor π_{x}o yields an element of TS(DTConOSAX) and is defined by:

(Def. 15) π_{x}o = OSSym(LBound(o, LeastSortsx), X)-tree(x).

Let S be a locally directed order sorted signature, let X be a non-empty many sorted set indexed by S, and let t be a symbol of DTConOSAX. Let us assume that there exists a finite sequence p such that t ⇒ p. The functor ^{@}(X, t) yields an operation symbol of S and is defined by:

(Def. 16) ⟨⟨^{@}(X, t), the carrier of S⟩⟩= t.

Let S be an order sorted signature, let X be a non-empty many sorted set indexed by S, and let t be a symbol of DTConOSAX. Let us assume that t ∈ the terminals of DTConOSAX. The functor ∏ t yielding an element of TS(DTConOSAX) is defined by:

(Def. 17) ∏ t = the root tree of t.

Let S be a locally directed order sorted signature and let X be a non-empty many sorted set indexed by S. The functor LCongruenceX yielding a monotone order sorted congruence of ParsedTermsOSAX is defined by:

(Def. 18) For every monotone order sorted congruence R of ParsedTermsOSAX

holds LCongruenceX ⊆ R. Let S be a locally directed order sorted signature and let X be a non-empty

many sorted set indexed by S. The functor FreeOSAX yielding a strict nonempty monotone order sorted algebra of S is defined by:

(Def. 19) FreeOSAX = QuotOSAlg(ParsedTermsOSAX, LCongruenceX).

Let S be an order sorted signature, let X be a non-empty many sorted set indexed by S, and let t be a symbol of DTConOSAX. The functor ^{@}t yields a subset of [: TS(DTConOSAX), the carrier of S:] and is defined by the condition (Def. 20).

(Def. 20) ^{@}t = {⟨⟨the root tree of t, s_{1}⟩⟩; s_{1} ranges over elements of the carrier of

S: ⋁_{s: element of the carrier of S} ⋁_{x: set} (x ∈ X(s) ∧ t = ⟨⟨x, s⟩⟩ ∧ s s_{1})}. Let S be an order sorted signature, let X be a non-empty many sorted set

indexed by S, let n_{1} be a symbol of DTConOSAX, and let x be a finite sequence of elements of 2^{[: TS(DTConOSA X), the carrier of S:]}. The functor ^{@}(n_{1}, x) yielding a subset of [: TS(DTConOSAX), the carrier of S:] is defined by the condition (Def. 21).

(Def. 21) ^{@}(n_{1}, x) = {⟨⟨(Den(o_{2}, ParsedTermsOSAX))(x_{2}), s_{3}⟩⟩; o_{2} ranges over operation symbols of S, x_{2} ranges over elements of Args(o_{2}, ParsedTermsOSAX), s_{3} ranges over elements of the carrier of S: ⋁_{o_{1} : operation symbol of S} (n_{1} = ⟨⟨o_{1}, the carrier of S⟩⟩ ∧ o_{1} ≅ o_{2} ∧ lenArity(o_{1}) = lenArity(o_{2}) ∧ the result sort of o_{1} s_{3} ∧ the result sort of o_{2} s_{3}) ∧ ⋁_{w_{3} : element of (the carrier of S)^{∗}} (domw_{3} = domx ∧ ⋀_{y: natural number} (y ∈ domx ⇒ ⟨⟨x_{2}(y), (w_{3})_{y}⟩⟩∈ x(y)))}.

Let S be a locally directed order sorted signature and let X be a non-empty many sorted set indexed by S. The functor PTClassesX yielding a function from TS(DTConOSAX) into 2^{[: TS(DTConOSA X), the carrier of S:]} is defined by the conditions (Def. 22).

(Def. 22)(i) For every symbol t of DTConOSAX such that t ∈ the terminals of

DTConOSAX holds (PTClassesX)(the root tree of t) = ^{@}t, and (ii) for every symbol n_{1} of DTConOSAX and for every finite sequence t_{1}

of elements of TS(DTConOSAX) and for every finite sequence r_{1} such that r_{1} = the roots of t_{1} and n_{1} ⇒ r_{1} and for every finite sequence x of elements of 2^{[: TS(DTConOSA X), the carrier of S:]} such that x = PTClassesX ·t_{1} holds (PTClassesX)(n_{1}-tree(t_{1})) = ^{@}(n_{1}, x).

One can prove the following four propositions:

(20) Let S be a locally directed order sorted signature, X be a non-empty many sorted set indexed by S, and t be an element of TS(DTConOSAX). Then

(i) for every element s of the carrier of S holds t ∈ (the sorts of ParsedTermsOSAX)(s) iff ⟨⟨t, s⟩⟩∈ (PTClassesX)(t), and

(ii) for every element s of the carrier of S and for every element y of TS(DTConOSAX) such that ⟨⟨y, s⟩⟩ ∈ (PTClassesX)(t) holds ⟨⟨t, s⟩⟩ ∈ (PTClassesX)(y).

(21) Let S be a locally directed order sorted signature, X be a non-empty many sorted set indexed by S, t be an element of TS(DTConOSAX), and s be an element of the carrier of S. If there exists an element y of TS(DTConOSAX) such that ⟨⟨y, s⟩⟩ ∈ (PTClassesX)(t), then ⟨⟨t, s⟩⟩ ∈ (PTClassesX)(t).

(22) Let S be a locally directed order sorted signature, X be a non-empty many sorted set indexed by S, x, y be elements of TS(DTConOSAX), and s_{1}, s_{2} be elements of the carrier of S. Suppose s_{1} s_{2} and x ∈ (the sorts of ParsedTermsOSAX)(s_{1}) and y ∈ (the sorts of ParsedTermsOSAX)(s_{1}). Then ⟨⟨y, s_{1}⟩⟩ ∈ (PTClassesX)(x) if and only if ⟨⟨y, s_{2}⟩⟩∈ (PTClassesX)(x).

(23) Let S be a locally directed order sorted signature, X be a non-empty many sorted set indexed by S, x, y, z be elements of TS(DTConOSAX), and s be an element of the carrier of S. If ⟨⟨y, s⟩⟩∈ (PTClassesX)(x) and ⟨⟨z, s⟩⟩∈ (PTClassesX)(y), then ⟨⟨x, s⟩⟩∈ (PTClassesX)(z).

Let S be a locally directed order sorted signature and let X be a nonempty many sorted set indexed by S. The functor PTCongruenceX yielding an equivalence order sorted relation of ParsedTermsOSAX is defined by the condition (Def. 23).

(Def. 23) Let i be a set. Suppose i ∈ the carrier of S. Then (PTCongruenceX)(i) = {⟨⟨x, y⟩⟩; x ranges over elements of TS(DTConOSAX), y ranges over elements of TS(DTConOSAX): ⟨⟨x, i⟩⟩∈ (PTClassesX)(y)}.

One can prove the following propositions:

(24) Let S be a locally directed order sorted signature, X be a nonempty many sorted set indexed by S, and x, y, s be sets. If ⟨⟨x, s⟩⟩ ∈ (PTClassesX)(y), then x ∈ TS(DTConOSAX) and y ∈ TS(DTConOSAX) and s ∈ the carrier of S.

(25) Let S be a locally directed order sorted signature, X be a non-empty many sorted set indexed by S, C be a component of S, and x, y be sets. Then ⟨⟨x, y⟩⟩ ∈ CompClass(PTCongruenceX, C) if and only if there exists an element s_{1} of the carrier of S such that s_{1} ∈ C and ⟨⟨x, s_{1}⟩⟩ ∈ (PTClassesX)(y).

(26) Let S be a locally directed order sorted signature, X be a non-empty many sorted set indexed by S, s be an element of the carrier of S, and x be an element of (the sorts of ParsedTermsOSAX)(s). Then OSClass(PTCongruenceX, x) = π_{1}((PTClassesX)(x)).

(27) Let S be a locally directed order sorted signature, X be a non-empty many sorted set indexed by S, and R be a many sorted relation indexed by ParsedTermsOSAX. Then R = PTCongruenceX if and only if the following conditions are satisfied:

(i) for all elements s_{1}, s_{2} of the carrier of S and for every set x such that x ∈ X(s_{1}) holds if s_{1} s_{2}, then ⟨⟨the root tree of ⟨⟨x, s_{1}⟩⟩, the root tree of ⟨⟨x, s_{1}⟩⟩⟩⟩ ∈ R(s_{2}) and for every set y such that ⟨⟨the root tree of ⟨⟨x, s_{1}⟩⟩, y⟩⟩∈ R(s_{2}) or ⟨⟨y, the root tree of ⟨⟨x, s_{1}⟩⟩⟩⟩∈ R(s_{2}) holds s_{1} s_{2} and y = the root tree of ⟨⟨x, s_{1}⟩⟩, and

(ii) for all operation symbols o_{1}, o_{2} of S and for every element x_{1} of Args(o_{1}, ParsedTermsOSAX) and for every element x_{2} of Args(o_{2}, ParsedTermsOSAX) and for every element s_{3} of the carrier of S holds ⟨⟨(Den(o_{1}, ParsedTermsOSAX))(x_{1}), (Den(o_{2}, ParsedTermsOSAX))(x_{2})⟩⟩ ∈ R(s_{3}) iff o_{1} ≅ o_{2} and lenArity(o_{1}) = lenArity(o_{2}) and the result sort of o_{1} s_{3} and the result sort of o_{2} s_{3} and there exists an element w_{3} of (the carrier of S)^{∗} such that domw_{3} = domx_{1} and for every natural number y such that y ∈ domw_{3} holds ⟨⟨x_{1}(y), x_{2}(y)⟩⟩∈ R((w_{3})_{y}).

(28) Let S be a locally directed order sorted signature and X be a non-empty

many sorted set indexed by S. Then PTCongruenceX is monotone. Let S be a locally directed order sorted signature and let X be a non-empty

many sorted set indexed by S. Observe that PTCongruenceX is monotone.

Let S be a locally directed order sorted signature, let X be a non-empty many sorted set indexed by S, and let s be an element of the carrier of S. The functor PTVars(s, X) yields a subset of (the sorts of ParsedTermsOSAX)(s) and is defined by:

(Def. 24) For every set x holds x ∈ PTVars(s, X) iff there exists a set a such that

a ∈ X(s) and x = the root tree of ⟨⟨a, s⟩⟩. Let S be a locally directed order sorted signature, let X be a non-empty

many sorted set indexed by S, and let s be an element of the carrier of S. One can check that PTVars(s, X) is non empty.

We now state the proposition

(29) Let S be a locally directed order sorted signature, X be a non-empty many sorted set indexed by S, and s be an element of the carrier of S. Then PTVars(s, X) = {the root tree of t; t ranges over symbols of DTConOSAX : t ∈ the terminals of DTConOSAX ∧ t_{2} = s}.

Let S be a locally directed order sorted signature and let X be a nonempty many sorted set indexed by S. The functor PTVarsX yielding a subset of ParsedTermsOSAX is defined by:

(Def. 25) For every element s of the carrier of S holds (PTVarsX)(s) =

PTVars(s, X). The following proposition is true

(30) Let S be a locally directed order sorted signature and X be a non-empty

many sorted set indexed by S. Then PTVarsX is non-empty. Let S be a locally directed order sorted signature, let X be a non-empty

many sorted set indexed by S, and let s be an element of the carrier of S. The functor OSFreeGen(s, X) yields a subset of (the sorts of FreeOSAX)(s) and is defined by:

(Def. 26) For every set x holds x ∈ OSFreeGen(s, X) iff there exists a set a such that a ∈ X(s) and x = (OSNatHom(ParsedTermsOSAX, LCongruenceX)) (s)(the root tree of ⟨⟨a, s⟩⟩).

Let S be a locally directed order sorted signature, let X be a non-empty many sorted set indexed by S, and let s be an element of the carrier of S. Note that OSFreeGen(s, X) is non empty.

We now state the proposition (31) Let S be a locally directed order sorted signature, X be a non-empty

many sorted set indexed by S, and s be an element of the carrier of S. Then OSFreeGen(s, X) = {(OSNatHom(ParsedTermsOSAX, LCongruenceX)) (s)(the root tree of t); t ranges over symbols of DTConOSAX : t ∈ the terminals of DTConOSAX ∧ t_{2} = s}.

Let S be a locally directed order sorted signature and let X be a non-empty many sorted set indexed by S. The functor OSFreeGenX yielding an order sorted generator set of FreeOSAX is defined by:

(Def. 27) For every element s of the carrier of S holds (OSFreeGenX)(s) =

OSFreeGen(s, X). The following proposition is true

(32) Let S be a locally directed order sorted signature and X be a non-empty

many sorted set indexed by S. Then OSFreeGenX is non-empty. Let S be a locally directed order sorted signature and let X be a non-empty

many sorted set indexed by S. Observe that OSFreeGenX is non-empty.

Let S be a locally directed order sorted signature, let X be a nonempty many sorted set indexed by S, let R be an order sorted congruence of ParsedTermsOSAX, and let t be an element of TS(DTConOSAX). The functor OSClass(R, t) yielding an element of OSClass(R, LeastSortt) is defined by the condition (Def. 28).

(Def. 28) Let s be an element of the carrier of S and x be an element of (the sorts

of ParsedTermsOSAX)(s). If t = x, then OSClass(R, t) = OSClass(R, x). We now state several propositions:

(33) Let S be a locally directed order sorted signature, X be a non-empty many sorted set indexed by S, R be an order sorted congruence of ParsedTermsOSAX, and t be an element of TS(DTConOSAX). Then t ∈ OSClass(R, t).

(34) Let S be a locally directed order sorted signature, X be a non-empty many sorted set indexed by S, s be an element of the carrier of S, t be an element of TS(DTConOSAX), and x, x_{1} be sets. Suppose x ∈ X(s) and t = the root tree of ⟨⟨x, s⟩⟩. Then x_{1} ∈ OSClass(PTCongruenceX, t) if and only if x_{1} = t.

(35) Let S be a locally directed order sorted signature, X be a non-empty many sorted set indexed by S, R be an order sorted congruence of ParsedTermsOSAX, and t_{2}, t_{3} be elements of TS(DTConOSAX). Then t_{3} ∈ OSClass(R, t_{2}) if and only if OSClass(R, t_{2}) = OSClass(R, t_{3}).

(36) Let S be a locally directed order sorted signature, X be a non-empty many sorted set indexed by S, R_{1}, R_{2} be order sorted congruences of ParsedTermsOSAX, and t be an element of TS(DTConOSAX). If R_{1} ⊆ R_{2}, then OSClass(R_{1}, t) ⊆ OSClass(R_{2}, t).

(37) Let S be a locally directed order sorted signature, X be a non-empty many sorted set indexed by S, s be an element of the carrier of S, t be an element of TS(DTConOSAX), and x, x_{1} be sets. Suppose x ∈ X(s) and t = the root tree of ⟨⟨x, s⟩⟩. Then x_{1} ∈ OSClass(LCongruenceX, t) if and only if x_{1} = t.

Let S be a locally directed order sorted signature, let X be a non-empty many sorted set indexed by S, let A be a non-empty many sorted set indexed by the carrier of S, let F be a many sorted function from PTVarsX into A, and let t be a symbol of DTConOSAX. Let us assume that t ∈ the terminals of DTConOSAX. The functor π(F, A, t) yields an element of ⋃ A and is defined as follows:

(Def. 29) For every function f such that f = F (t_{2}) holds π(F, A, t) = f(the root

tree of t). Next we state the proposition

(38) Let S be a locally directed order sorted signature, X be a non-empty many sorted set indexed by S, U_{1} be a monotone non-empty order sorted algebra of S, and f be a many sorted function from PTVarsX into the sorts of U_{1}. Then there exists a many sorted function h from ParsedTermsOSAX into U_{1} such that h is a homomorphism of ParsedTermsOSAX into U_{1} and order-sorted and h ↾ PTVarsX = f.

Let S be a locally directed order sorted signature, let X be a non-empty many sorted set indexed by S, and let s be an element of the carrier of S. The functor NHReverse(s, X) yields a function from OSFreeGen(s, X) into PTVars(s, X) and is defined by the condition (Def. 30).

(Def. 30) Let t be a symbol of DTConOSAX.

Suppose (OSNatHom(ParsedTermsOSAX, LCongruenceX))(s)(the root tree of t) ∈ OSFreeGen(s, X). Then (NHReverse(s, X))((OSNatHom (ParsedTermsOSAX, LCongruenceX))(s)(the root tree of t)) = the root tree of t.

Let S be a locally directed order sorted signature and let X be a non-empty many sorted set indexed by S. The functor NHReverseX yielding a many sorted function from OSFreeGenX into PTVarsX is defined as follows:

(Def. 31) For every element s of the carrier of S holds (NHReverseX)(s) =

NHReverse(s, X). Next we state two propositions:

(39) Let S be a locally directed order sorted signature and X be a non-empty many sorted set indexed by S. Then OSFreeGenX is osfree.

(40) Let S be a locally directed order sorted signature and X be a non-empty many sorted set indexed by S. Then FreeOSAX is osfree.

Let S be a locally directed order sorted signature. Note that there exists a non-empty monotone order sorted algebra of S which is osfree and strict.

3. Minimal Terms

Let S be a locally directed regular monotone order sorted signature and let X be a non-empty many sorted set indexed by S. The functor PTMinX yields a function from TS(DTConOSAX) into TS(DTConOSAX) and is defined by the conditions (Def. 32).

(Def. 32)(i) For every symbol t of DTConOSAX such that t ∈ the terminals of

DTConOSAX holds (PTMinX)(the root tree of t) = ∏ t, and (ii) for every symbol n_{1} of DTConOSAX and for every finite sequence t_{1}

of elements of TS(DTConOSAX) and for every finite sequence r_{1} such that r_{1} = the roots of t_{1} and n_{1} ⇒ r_{1} and for every finite sequence x of elements of TS(DTConOSAX) such that x = PTMinX · t_{1} holds (PTMinX)(n_{1}-tree(t_{1})) = π_{x}(^{@}(X, n_{1})).

Next we state several propositions:

(41) Let S be a locally directed regular monotone order sorted signature, X be a non-empty many sorted set indexed by S, and t be an element of TS(DTConOSAX). Then

(i) (PTMinX)(t) ∈ OSClass(PTCongruenceX, t), (ii) LeastSort(PTMinX)(t) LeastSortt, (iii) for every element s of the carrier of S and for every set x such that

x ∈ X(s) and t = the root tree of ⟨⟨x, s⟩⟩ holds (PTMinX)(t) = t, and (iv) for every operation symbol o of S and for every finite sequence t_{1}

of elements of TS(DTConOSAX) such that OSSym(o, X) ⇒ the roots of t_{1} and t = OSSym(o, X)-tree(t_{1}) holds LeastSortsPTMinX · t_{1} Arity(o) and OSSym(o, X) ⇒ the roots of PTMinX · t_{1} and OSSym(LBound(o, LeastSortsPTMinX ·t_{1}), X) ⇒ the roots of PTMinX · t_{1} and (PTMinX)(t) = OSSym(LBound(o, LeastSortsPTMinX · t_{1}), X)-tree(PTMinX · t_{1}).

(42) Let S be a locally directed regular monotone order sorted signature, X be a non-empty many sorted set indexed by S, and t, t_{2} be elements of TS(DTConOSAX). If t_{2} ∈ OSClass(PTCongruenceX, t), then (PTMinX)(t_{2}) = (PTMinX)(t).

(43) Let S be a locally directed regular monotone order sorted signature, X be a non-empty many sorted set indexed by S, and t_{2}, t_{3} be elements of TS(DTConOSAX). Then t_{3} ∈ OSClass(PTCongruenceX, t_{2}) if and only if (PTMinX)(t_{3}) = (PTMinX)(t_{2}).

(44) Let S be a locally directed regular monotone order sorted signature, X be a non-empty many sorted set indexed by S, and t_{2} be an element of TS(DTConOSAX). Then (PTMinX)((PTMinX)(t_{2})) = (PTMinX)(t_{2}).

(45) Let S be a locally directed regular monotone order sorted signature, X be a non-empty many sorted set indexed by S, R be a monotone equivalence order sorted relation of ParsedTermsOSAX, and t be an element of TS(DTConOSAX). Then ⟨⟨t, (PTMinX)(t)⟩⟩∈ R(LeastSortt).

(46) Let S be a locally directed regular monotone order sorted signature, X be a non-empty many sorted set indexed by S, and R be a monotone equivalence order sorted relation of ParsedTermsOSAX. Then PTCongruenceX ⊆ R.

(47) Let S be a locally directed regular monotone order sorted signature and X be a non-empty many sorted set indexed by S. Then LCongruenceX = PTCongruenceX.

Let S be a locally directed regular monotone order sorted signature and let X be a non-empty many sorted set indexed by S. An element of TS(DTConOSAX) is called a minimal term of S, X if:

(Def. 33) (PTMinX)(it) = it.

Let S be a locally directed regular monotone order sorted signature and let X be a non-empty many sorted set indexed by S. The functor MinTermsX yields a subset of TS(DTConOSAX) and is defined by:

(Def. 34) MinTermsX = rngPTMinX.

The following proposition is true

(48) Let S be a locally directed regular monotone order sorted signature, X be a non-empty many sorted set indexed by S, and x be a set. Then x is a minimal term of S, X if and only if x ∈ MinTermsX.

Acknowledgments

Thanks to Joseph Goguen, for providing me with his articles on osas, and Andrzej Trybulec, for suggesting and funding this work in Bialystok.

References

[1] Grzegorz Bancerek. Curried and uncurried functions. Formalized Mathematics, 1(3):537– 541, 1990.

[2] Grzegorz Bancerek. König’s theorem. Formalized Mathematics, 1(3):589–593, 1990.

[3] Grzegorz Bancerek. Cartesian product of functions. Formalized Mathematics, 2(4):547– 552, 1991.

[4] Grzegorz Bancerek. König’s lemma. Formalized Mathematics, 2(3):397–402, 1991.

[5] Grzegorz Bancerek. Sets and functions of trees and joining operations of trees. Formalized Mathematics, 3(2):195–204, 1992.

[6] Grzegorz Bancerek. Joining of decorated trees. Formalized Mathematics, 4(1):77–82, 1993.

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

free order sorted universal algebra 225

[8] Grzegorz Bancerek and Piotr Rudnicki. On defining functions on trees. Formalized Mathematics, 4(1):91–101, 1993.

[9] Ewa Burakowska. Subalgebras of many sorted algebra. Lattice of subalgebras. Formalized Mathematics, 5(1):47–54, 1996.

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

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

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

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

[14] Patricia L. Carlson and Grzegorz Bancerek. Context-free grammar - part 1. Formalized Mathematics, 2(5):683–687, 1991.

[15] Małgorzata Korolkiewicz. Homomorphisms of many sorted algebras. Formalized Mathematics, 5(1):61–65, 1996.

[16] Małgorzata Korolkiewicz. Many sorted quotient algebra. Formalized Mathematics, 5(1):79–84, 1996.

[17] Beata Madras. Product of family of universal algebras. Formalized Mathematics, 4(1):103– 108, 1993.

[18] Andrzej Nędzusiak. σ-fields and probability. Formalized Mathematics, 1(2):401–407, 1990.

[19] Beata Perkowska. Free many sorted universal algebra. Formalized Mathematics, 5(1):67– 74, 1996.

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

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

[22] Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97–105, 1990.

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

[24] Andrzej Trybulec. Many sorted algebras. Formalized Mathematics, 5(1):37–42, 1996.

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

[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] Josef Urban. Homomorphisms of order sorted algebras. Formalized Mathematics, 10(3):197–200, 2002.

[29] Josef Urban. Order sorted algebras. Formalized Mathematics, 10(3):179–188, 2002.

[30] Josef Urban. Order sorted quotient algebra. Formalized Mathematics, 10(3):201–210, 2002.

[31] Josef Urban. Subalgebras of an order sorted algebra. Lattice of subalgebras. Formalized Mathematics, 10(3):189–196, 2002.

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

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

Contents Formaliz. Math. 10 (3)

Preliminaries to Automatic Generation of Mizar Documentation

for Circuits

By Grzegorz Bancerek and Adam Naumowicz  . . . . . . . . . . . 117

Properties of the Upper and Lower Sequence on the Cage

By Robert Milewski  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 135

On the Decompositions of Intervals and Simple Closed Curves

By Adam Grabowski . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145

On the Minimal Distance Between Sets in Euclidean Space

By Andrzej Trybulec  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153

Sequences of Metric Spaces and an Abstract Intermediate Value

Theorem

By Yatsuka Nakamura and Andrzej Trybulec  . . . . . . . . . . . 159

On the Decomposition of a Simple Closed Curve into Two Arcs

By Andrzej Trybulec and Yatsuka Nakamura  . . . . . . . . . . . 163

The Ordering of Points on a Curve. Part III

By Artur Korniłowicz  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169

The Ordering of Points on a Curve. Part IV

By Artur Korniłowicz  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 173

Order Sorted Algebras

By Josef Urban  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 179

Subalgebras of an Order Sorted Algebra. Lattice of Subalgebras

By Josef Urban  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 189

Homomorphisms of Order Sorted Algebras

By Josef Urban  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 197

Continued on inside back cover

Order Sorted Quotient Algebra

By Josef Urban  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 201

Free Order Sorted Universal Algebra

By Josef Urban  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 211