Formal languages are introduced as subsets of the set of all
0-based finite sequences over a given set (the alphabet). Concatenation,
the n-th power and closure (Kleene closure / star closure) are defined and their properties are shown.
Finally, it is shown that the closure of the alphabet
(understood here as the language of words of length 1)
equals to the set of all words over that alphabet,
and that the alphabet is the minimal set with this property.
Sections:
- Preliminaries
- Concatenation of Languages
- n-th Power of a Language
- Closure of a Language
- Alphabet as a Language
Bibliography:
- John E. Hopcroft, Jeffrey D. Ullman: "Introduction to Automata Theory, Languages, and Computation", Addison-Wesley Publishing Company, 1979
- William M. Waite, Gerhard Goos: "Compiler Construction", Springer-Verlag New York Inc., 1984
Mizar Mathematical Library identifier: FLANG_1.
Abstract in PDF: here.
Motorola Software Group, 2007.
Files:
:: Formal Languages -- Concatenation and Closure
:: by Micha{\l} Trybulec
::
:: Received March 9, 2007
:: Copyright (c) 2007 Association of Mizar Users
environ
vocabularies FUNCT_1, BOOLE, FINSEQ_1, RELAT_1, TARSKI, ALGSEQ_1, AFINSQ_1,
MEASURE6, GROUP_1, SETFAM_1, FLANG_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, NAT_1,
DOMAIN_1, FUNCT_1, RELSET_1, FUNCT_2, ORDINAL1, SETFAM_1, XXREAL_0,
AFINSQ_1, CATALAN2;
constructors XXREAL_0, NAT_1, XREAL_0, CATALAN2;
registrations SUBSET_1, RELSET_1, NAT_1, ORDINAL1, AFINSQ_1, XREAL_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin
reserve E, x, y, z, X, Y, Z for set;
reserve A, B, C, D for Subset of E^omega;
reserve a, a1, a2, b, c, c1, c2, d, ab, bc for Element of E^omega;
reserve e for Element of E;
reserve i, j, k, l, n, n1, n2, m for Nat;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries - Redefinitions
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, a, b;
redefine func a ^ b -> Element of E^omega;
end;
definition
let E;
redefine func <%>E -> Element of E^omega;
end;
definition
let E be non empty set;
let e be Element of E;
redefine func <%e%> -> Element of E^omega;
end;
definition
let E, a;
redefine func {a} -> Subset of E^omega;
end;
definition
let E;
let f be Function of NAT, bool E;
let n;
redefine func f.n -> Subset of E;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries - Numbers:
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: FLANG_1:1
n1 > n or n2 > n implies n1 + n2 > n;
theorem :: FLANG_1:2
n1 + n <= n2 + 1 & n > 0 implies n1 <= n2;
theorem :: FLANG_1:3
n1 + n2 = 1 iff (n1 = 1 & n2 = 0) or (n1 = 0 & n2 = 1);
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries - Sequences:
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: FLANG_1:4
a ^ b = <%x%> iff (a = <%>E & b = <%x%>) or (b = <%>E & a = <%x%>);
theorem :: FLANG_1:5
for p, q being XFinSequence holds
a = p ^ q implies
p is Element of E^omega &
q is Element of E^omega;
theorem :: FLANG_1:6
<%x%> is Element of E^omega implies x in E;
theorem :: FLANG_1:7
len b = n + 1 implies ex c, e st len c = n & b = c ^ <%e%>;
theorem :: FLANG_1:8
for p being XFinSequence st p <> {}
ex q being XFinSequence, x st p = <%x%> ^ q;
theorem :: FLANG_1:9
len b = n + 1 implies ex c, e st len c = n & b = <%e%> ^ c;
theorem :: FLANG_1:10
for p being XFinSequence st len p = i + j
ex q1, q2 being XFinSequence st len q1 = i & len q2 = j & p = q1 ^ q2;
theorem :: FLANG_1:11
len b = n + m implies ex c1, c2 st len c1 = n & len c2 = m & b = c1 ^ c2;
theorem :: FLANG_1:12
a ^ a = a implies a = {};
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Concatenation of Languages
:: Definition of ^^
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, A, B;
func A ^^ B -> Subset of E^omega means
:: FLANG_1:def 1
x in it iff ex a, b st a in A & b in B & x = a ^ b;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Concatenation of Languages
:: Properties of ^^
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: FLANG_1:13
A ^^ B = {} iff A = {} or B = {};
theorem :: FLANG_1:14
A ^^ {<%>E} = A & {<%>E} ^^ A = A;
theorem :: FLANG_1:15
A ^^ B = {<%>E} iff A = {<%>E} & B = {<%>E};
theorem :: FLANG_1:16
<%>E in A ^^ B iff <%>E in A & <%>E in B;
theorem :: FLANG_1:17
<%>E in B implies A c= A ^^ B & A c= B ^^ A;
theorem :: FLANG_1:18
A c= C & B c= D implies A ^^ B c= C ^^ D;
theorem :: FLANG_1:19
(A ^^ B) ^^ C = A ^^ (B ^^ C);
theorem :: FLANG_1:20
A ^^ (B /\ C) c= (A ^^ B) /\ (A ^^ C) &
(B /\ C) ^^ A c= (B ^^ A) /\ (C ^^ A);
theorem :: FLANG_1:21
A ^^ B \/ A ^^ C = A ^^ (B \/ C) &
B ^^ A \/ C ^^ A = (B \/ C) ^^ A;
theorem :: FLANG_1:22
(A ^^ B) \ (A ^^ C) c= A ^^ (B \ C) &
(B ^^ A) \ (C ^^ A) c= (B \ C) ^^ A;
theorem :: FLANG_1:23
(A ^^ B) \+\ (A ^^ C) c= A ^^ (B \+\ C) &
(B ^^ A) \+\ (C ^^ A) c= (B \+\ C) ^^ A;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Concatenation of a Language with Itself
:: Definition of |^
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, A, n;
func A |^ n -> Subset of E^omega means
:: FLANG_1:def 2
ex concat being Function of NAT, bool (E^omega) st
it = concat.n &
concat.0 = {<%>E} &
for i holds concat.(i + 1) = concat.i ^^ A;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Concatenation of a Language with Itself
:: Properties of |^
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: FLANG_1:24
A |^ (n + 1) = (A |^ n) ^^ A;
theorem :: FLANG_1:25
A |^ 0 = {<%>E};
theorem :: FLANG_1:26
A |^ 1 = A;
theorem :: FLANG_1:27
A |^ 2 = A ^^ A;
theorem :: FLANG_1:28
A |^ n = {} iff n > 0 & A = {};
theorem :: FLANG_1:29
{<%>E} |^ n = {<%>E};
theorem :: FLANG_1:30
A |^ n = {<%>E} iff n = 0 or A = {<%>E};
theorem :: FLANG_1:31
<%>E in A implies <%>E in A |^ n;
theorem :: FLANG_1:32
<%>E in A |^ n & n > 0 implies <%>E in A;
theorem :: FLANG_1:33
(A |^ n) ^^ A = A ^^ (A |^ n);
theorem :: FLANG_1:34
A |^ (m + n) = (A |^ m) ^^ (A |^ n);
theorem :: FLANG_1:35
(A |^ m) |^ n = A |^ (m * n);
theorem :: FLANG_1:36
<%>E in A & n > 0 implies A c= A |^ n;
theorem :: FLANG_1:37
<%>E in A & m > n implies A |^ n c= A |^ m;
theorem :: FLANG_1:38
A c= B implies A |^ n c= B |^ n;
theorem :: FLANG_1:39
(A |^ n) \/ (B |^ n) c= (A \/ B) |^ n;
theorem :: FLANG_1:40
(A /\ B) |^ n c= (A |^ n) /\ (B |^ n);
theorem :: FLANG_1:41
a in C |^ m & b in C |^ n implies a ^ b in C |^ (m + n);
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Kleene Closure
:: Definition of *
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, A;
func A* -> Subset of E^omega equals
:: FLANG_1:def 3
union { B : ex n st B = A |^ n };
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Kleene Closure
:: Properties of *
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: FLANG_1:42
x in A* iff ex n st x in A |^ n;
theorem :: FLANG_1:43
A |^ n c= A*;
theorem :: FLANG_1:44
A c= A*;
theorem :: FLANG_1:45
A ^^ A c= A*;
theorem :: FLANG_1:46
a in C* & b in C* implies a ^ b in C*;
theorem :: FLANG_1:47
A c= C* & B c= C* implies A ^^ B c= C*;
theorem :: FLANG_1:48
A* = {<%>E} iff A = {} or A = {<%>E};
theorem :: FLANG_1:49
<%>E in A*;
theorem :: FLANG_1:50
A* = {x} implies x = <%>E;
theorem :: FLANG_1:51
x in A |^ (m + 1) implies x in (A*) ^^ A & x in A ^^ (A*);
theorem :: FLANG_1:52
A |^ (m + 1) c= (A*) ^^ A & A |^ (m + 1) c= A ^^ (A*);
theorem :: FLANG_1:53
x in (A*) ^^ A or x in A ^^ (A*) implies x in A*;
theorem :: FLANG_1:54
(A*) ^^ A c= A* & A ^^ (A*) c= A*;
theorem :: FLANG_1:55
<%>E in A implies A* = (A*) ^^ A & A* = A ^^ (A*);
theorem :: FLANG_1:56
<%>E in A implies A* = (A*) ^^ (A |^ n) & A* = (A |^ n) ^^ (A*);
theorem :: FLANG_1:57
A* = {<%>E} \/ A ^^ (A*) & A* = {<%>E} \/ (A*) ^^ A;
theorem :: FLANG_1:58
A ^^ (A*) = (A*) ^^ A;
theorem :: FLANG_1:59
(A |^ n) ^^ (A*) = (A*) ^^ (A |^ n);
theorem :: FLANG_1:60
A c= B* implies A |^ n c= B*;
theorem :: FLANG_1:61
A c= B* implies A* c= B*;
theorem :: FLANG_1:62
A c= B implies A* c= B*;
theorem :: FLANG_1:63
(A*)* = A*;
theorem :: FLANG_1:64
(A*) ^^ (A*) = A*;
theorem :: FLANG_1:65
(A |^ n)* c= A*;
theorem :: FLANG_1:66
(A*) |^ n c= A*;
theorem :: FLANG_1:67
n > 0 implies (A*) |^ n = A*;
theorem :: FLANG_1:68
A c= B* implies B* = (B \/ A)*;
theorem :: FLANG_1:69
a in A* implies A* = (A \/ {a})*;
theorem :: FLANG_1:70
A* = (A \ {<%>E})*;
theorem :: FLANG_1:71
(A*) \/ (B*) c= (A \/ B)*;
theorem :: FLANG_1:72
(A /\ B)* c= (A*) /\ (B*);
theorem :: FLANG_1:73
<%x%> in A* iff <%x%> in A;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Lexemes as a Subset of E^omega
:: Definition of Lex
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E;
func Lex(E) -> Subset of E^omega means
:: FLANG_1:def 4
x in it iff ex e st e in E & x = <%e%>;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Lexemes as a Subset of E^omega
:: Properties of Lex
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: FLANG_1:74
a in Lex(E) |^ len a;
theorem :: FLANG_1:75
Lex(E)* = E^omega;
theorem :: FLANG_1:76
A* = E^omega implies Lex(E) c= A;
Top
:: Formal Languages -- Concatenation and Closure
:: by Micha{\l} Trybulec
::
:: Received March 9, 2007
:: Copyright (c) 2007 Association of Mizar Users
environ
vocabularies FUNCT_1, BOOLE, FINSEQ_1, RELAT_1, TARSKI, ALGSEQ_1, AFINSQ_1,
MEASURE6, GROUP_1, SETFAM_1, FLANG_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, NAT_1,
DOMAIN_1, FUNCT_1, RELSET_1, FUNCT_2, ORDINAL1, SETFAM_1, XXREAL_0,
AFINSQ_1, CATALAN2;
constructors XXREAL_0, NAT_1, XREAL_0, CATALAN2;
registrations SUBSET_1, RELSET_1, NAT_1, ORDINAL1, AFINSQ_1, XREAL_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
theorems AFINSQ_1, ISOCAT_2, NAT_1, ORDINAL1, REAL_1, SUBSET_1, TARSKI,
XBOOLE_0, XBOOLE_1, XREAL_1, ZFMISC_1;
schemes CARD_FIL, DOMAIN_1, NAT_1, RECDEF_1, SUBSET_1;
begin
reserve E, x, y, z, X, Y, Z for set;
reserve A, B, C, D for Subset of E^omega;
reserve a, a1, a2, b, c, c1, c2, d, ab, bc for Element of E^omega;
reserve e for Element of E;
reserve i, j, k, l, n, n1, n2, m for Nat;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries - Redefinitions
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, a, b;
redefine func a ^ b -> Element of E^omega;
coherence
proof
a ^ b is XFinSequence of E;
hence thesis by AFINSQ_1:def 8;
end;
end;
definition
let E;
redefine func <%>E -> Element of E^omega;
coherence by AFINSQ_1:def 8;
end;
definition
let E be non empty set;
let e be Element of E;
redefine func <%e%> -> Element of E^omega;
coherence
proof
{e} c= E;
then rng <%e%> c= E by AFINSQ_1:36;
hence thesis by AFINSQ_1:def 8;
end;
end;
definition
let E, a;
redefine func {a} -> Subset of E^omega;
coherence by SUBSET_1:55;
end;
definition
let E;
let f be Function of NAT, bool E;
let n;
redefine func f.n -> Subset of E;
coherence
proof
A: n is Element of NAT by ORDINAL1:def 13;
f.n in rng f by A, ISOCAT_2:4;
hence thesis;
end;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries - Numbers:
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem LmNum5:
n1 > n or n2 > n implies n1 + n2 > n
proof
assume
A: n1 > n or n2 > n;
A1:
n1 > n & n2 >= 0 implies n1 + n2 > n + 0 by XREAL_1:10;
A2:
n1 >= 0 & n2 > n implies n1 + n2 > n + 0 by XREAL_1:10;
thus thesis by A, A1, A2;
end;
theorem LmNum30:
n1 + n <= n2 + 1 & n > 0 implies n1 <= n2
proof
assume
A: n1 + n <= n2 + 1 & n > 0;
then 1 + 0 <= n by NAT_1:13;
hence thesis by A, XREAL_1:10;
end;
theorem LmNum40:
n1 + n2 = 1 iff (n1 = 1 & n2 = 0) or (n1 = 0 & n2 = 1)
proof
thus n1 + n2 = 1 implies (n1 = 1 & n2 = 0) or (n1 = 0 & n2 = 1)
proof
assume
A: n1 + n2 = 1;
now
assume
C1: n1 <= 1 & n2 <= 1;
C2: n1 = 1 & n2 = 1 implies contradiction by A;
n1 = 0 & n2 = 0 implies contradiction by A;
hence (n1 = 1 & n2 = 0) or (n1 = 0 & n2 = 1) by C1, NAT_1:26, C2;
end;
hence thesis by A, LmNum5;
end;
thus thesis;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries - Sequences:
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem LmSeq10:
a ^ b = <%x%> iff (a = <%>E & b = <%x%>) or (b = <%>E & a = <%x%>)
proof
thus a ^ b = <%x%> implies (a = <%>E & b = <%x%>) or (b = <%>E & a = <%x%>)
proof
assume
A: a ^ b = <%x%>;
then len (a ^ b) = 1 by AFINSQ_1:38;
then len a + len b = 1 by AFINSQ_1:20;
then (len a = 1 & len b = 0) or (len a = 0 & len b = 1) by LmNum40;
then (len a = 1 & b = <%>E) or (a = <%>E & len b = 1) by AFINSQ_1:18;
hence thesis by A, AFINSQ_1:32;
end;
assume (a = <%>E & b = <%x%>) or (b = <%>E & a = <%x%>);
hence thesis by AFINSQ_1:32;
end;
theorem LmSeq20:
for p, q being XFinSequence holds
a = p ^ q implies
p is Element of E^omega &
q is Element of E^omega
proof
let p, q be XFinSequence;
assume a = p ^ q;
then p is XFinSequence of E &
q is XFinSequence of E by AFINSQ_1:34;
hence thesis by AFINSQ_1:def 8;
end;
theorem LmSeq30:
<%x%> is Element of E^omega implies x in E
proof
assume <%x%> is Element of E^omega;
then rng <%x%> c= E by ORDINAL1:def 8;
then {x} c= E by AFINSQ_1:36;
hence thesis by ZFMISC_1:37;
end;
theorem LmSeq40:
len b = n + 1 implies ex c, e st len c = n & b = c ^ <%e%>
proof
assume
C0: len b = n + 1;
then
C1: b <> {} by AFINSQ_1:18;
consider c' being XFinSequence, x such that
C2: b = c' ^ <%x%> by C1, AFINSQ_1:44;
reconsider c = c' as Element of E^omega by C2, LmSeq20;
C3:
n + 1 = len c + len <%x%> by C0, C2, AFINSQ_1:20
.= len c + 1 by AFINSQ_1:37;
<%x%> is Element of E^omega by C2, LmSeq20;
then reconsider e = x as Element of E by LmSeq30;
take c, e;
thus thesis by C3, C2;
end;
theorem LmSeq41:
for p being XFinSequence st p <> {}
ex q being XFinSequence, x st p = <%x%> ^ q
proof
defpred P[Nat] means
for p being XFinSequence st len p = $1 & p <> {}
ex q being XFinSequence, x st p = <%x%> ^ q;
A:
P[0] by AFINSQ_1:18;
B:
now
let n;
assume
B1: P[n];
thus P[n + 1]
proof
let p be XFinSequence such that
B2: len p = n + 1 & p <> {};
consider q being XFinSequence, x such that
B3: p = q ^ <%x%> by B2, AFINSQ_1:44;
B4: n + 1 = len q + len <%x%> by B2, B3, AFINSQ_1:20
.= len q + 1 by AFINSQ_1:37;
per cases;
suppose
B4a: q = {};
then p = <%x%> by B3, AFINSQ_1:32
.= <%x%> ^ q by B4a, AFINSQ_1:32;
hence ex s being XFinSequence, z st p = <%z%> ^ s;
end;
suppose q <> {};
then consider r being XFinSequence, y such that
B5: q = <%y%> ^ r by B1, B4;
p = <%y%> ^ (r ^ <%x%>) by B3, B5, AFINSQ_1:30;
hence ex s being XFinSequence, z st p = <%z%> ^ s;
end;
end;
end;
C:
for n holds P[n] from NAT_1:sch 2(A, B);
let p be XFinSequence;
assume
D: p <> {};
len p = len p;
hence thesis by C, D;
end;
theorem
len b = n + 1 implies ex c, e st len c = n & b = <%e%> ^ c
proof
assume
C0: len b = n + 1;
then
C1: b <> {} by AFINSQ_1:18;
consider c' being XFinSequence, x such that
C2: b = <%x%> ^ c' by C1, LmSeq41;
reconsider c = c' as Element of E^omega by C2, LmSeq20;
C3:
n + 1 = len c + len <%x%> by C0, C2, AFINSQ_1:20
.= len c + 1 by AFINSQ_1:37;
<%x%> is Element of E^omega by C2, LmSeq20;
then reconsider e = x as Element of E by LmSeq30;
take c, e;
thus thesis by C3, C2;
end;
theorem LmSeq43:
for p being XFinSequence st len p = i + j
ex q1, q2 being XFinSequence st len q1 = i & len q2 = j & p = q1 ^ q2
proof
defpred P[Nat] means
for p being XFinSequence, i, j st len p = $1 & len p = i + j
ex q1, q2 being XFinSequence st len q1 = i & len q2 = j & p = q1 ^ q2;
A:
P[0]
proof
let p be XFinSequence;
let i, j;
assume
A1: len p = 0 & len p = i + j;
then
A2: i = 0 & j = 0 by NAT_1:7;
A3: p = {} by A1, AFINSQ_1:18;
A4: len {} = i & len {} = j by A2, AFINSQ_1:18;
p = {} ^ {} by A3, AFINSQ_1:32;
hence thesis by A4;
end;
B:
now
let n;
assume
B1: P[n];
thus P[n + 1]
proof
let p be XFinSequence;
let i, j;
assume
B2: len p = n + 1 & len p = i + j;
per cases;
suppose
B3: j = 0;
take q1 = p;
take q2 = {};
thus len q1 = i & len q2 = j & p = q1 ^ q2
by B2, B3, AFINSQ_1:18, AFINSQ_1:32;
end;
suppose j > 0;
then consider k such that
B4a: j = k + 1 by NAT_1:6;
B4b: n = i + k by B2, B4a;
p <> {} by B2, AFINSQ_1:18;
then consider q being XFinSequence, x such that
B3a: p = q ^ <%x%> by AFINSQ_1:44;
n + 1 = len q + len <%x%> by B2, B3a, AFINSQ_1:20
.= len q + 1 by AFINSQ_1:37;
then consider q1, q2 being XFinSequence such that
B3b: len q1 = i & len q2 = k & q = q1 ^ q2 by B1, B4b;
B3c: p = q1 ^ (q2 ^ <%x%>) by B3a, B3b, AFINSQ_1:30;
len (q2 ^ <%x%>) = len q2 + len <%x%> by AFINSQ_1:20
.= j by B3b, B4a, AFINSQ_1:37;
hence ex q1, q2 being XFinSequence st
len q1 = i & len q2 = j & p = q1 ^ q2 by B3b, B3c;
end;
end;
end;
for n holds P[n] from NAT_1:sch 2(A, B);
hence thesis;
end;
theorem
len b = n + m implies ex c1, c2 st len c1 = n & len c2 = m & b = c1 ^ c2
proof
assume
C0: len b = n + m;
consider c1', c2' being XFinSequence such that
C2: len c1' = n & len c2' = m & b = c1' ^ c2' by C0, LmSeq43;
reconsider c1 = c1' as Element of E^omega by C2, LmSeq20;
reconsider c2 = c2' as Element of E^omega by C2, LmSeq20;
take c1, c2;
thus thesis by C2;
end;
theorem LmSeq50:
a ^ a = a implies a = {}
proof
assume
A: a ^ a = a;
len a + len a = len a by A, AFINSQ_1:20;
hence thesis by AFINSQ_1:18;
end;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Concatenation of Languages
:: Definition of ^^
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, A, B;
func A ^^ B -> Subset of E^omega means :DefConcat:
x in it iff ex a, b st a in A & b in B & x = a ^ b;
existence
proof
defpred P[set] means ex a, b st a in A & b in B & $1 = a ^ b;
consider C such that
A: x in C iff x in E^omega & P[x] from SUBSET_1:sch 1;
take C;
thus thesis by A;
end;
uniqueness
proof
let C1, C2 be Subset of E^omega such that
A1: x in C1 iff ex a, b st a in A & b in B & x = a ^ b and
A2: x in C2 iff ex a, b st a in A & b in B & x = a ^ b;
now
let x;
thus x in C1 implies x in C2
proof
assume x in C1;
then ex a, b st a in A & b in B & x = a ^ b by A1;
hence x in C2 by A2;
end;
assume x in C2;
then ex a, b st a in A & b in B & x = a ^ b by A2;
hence x in C1 by A1;
end;
hence thesis by TARSKI:2;
end;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Concatenation of Languages
:: Properties of ^^
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem ThConcat70:
A ^^ B = {} iff A = {} or B = {}
proof
thus A ^^ B = {} implies A = {} or B = {}
proof
assume that
A1: A ^^ B = {} and
A2: A <> {} & B <> {};
consider a such that
A3: a in A by A2, SUBSET_1:10;
consider b such that
A4: b in B by A2, SUBSET_1:10;
a ^ b in A ^^ B by A3, A4, DefConcat;
hence contradiction by A1;
end;
assume
B: A = {} or B = {};
not ex x st x in A ^^ B
proof
given x such that
B1: x in A ^^ B;
ex a, b st a in A & b in B & x = a ^ b by B1, DefConcat;
hence contradiction by B;
end;
hence thesis by XBOOLE_0:def 1;
end;
theorem ThConcat80:
A ^^ {<%>E} = A & {<%>E} ^^ A = A
proof
A1:
x in {<%>E} ^^ A implies x in A
proof
assume x in {<%>E} ^^ A;
then consider d, a such that
B1: d in {<%>E} & a in A & x = d ^ a by DefConcat;
x = <%>E ^ a by B1, TARSKI:def 1;
hence thesis by B1, AFINSQ_1:32;
end;
A2:
x in A ^^ {<%>E} implies x in A
proof
assume x in A ^^ {<%>E};
then consider a, d such that
B2: a in A & d in {<%>E} & x = a ^ d by DefConcat;
x = a ^ <%>E by B2, TARSKI:def 1;
hence thesis by B2, AFINSQ_1:32;
end;
A3:
x in A implies x in {<%>E} ^^ A
proof
assume
B3: x in A;
ex d, a st d in {<%>E} & a in A & x = d ^ a
proof
consider d such that
C3: d = <%>E;
reconsider a = x as Element of E^omega by B3;
take d, a;
thus thesis by B3, C3, AFINSQ_1:32, TARSKI:def 1;
end;
hence thesis by DefConcat;
end;
A4:
x in A implies x in A ^^ {<%>E}
proof
assume
B4: x in A;
ex a, d st a in A & d in {<%>E} & x = a ^ d
proof
set d = <%>E;
reconsider a = x as Element of E^omega by B4;
take a, d;
thus thesis by B4, AFINSQ_1:32, TARSKI:def 1;
end;
hence thesis by DefConcat;
end;
thus thesis by A1, A2, A3, A4, TARSKI:2;
end;
theorem ThConcat90:
A ^^ B = {<%>E} iff A = {<%>E} & B = {<%>E}
proof
thus A ^^ B = {<%>E} implies A = {<%>E} & B = {<%>E}
proof
assume that
A1: A ^^ B = {<%>E} and
A2: (A <> {<%>E} or B <> {<%>E});
<%>E in A ^^ B by A1, TARSKI:def 1;
then consider a, b such that
A3: a in A & b in B & <%>E = a ^ b by DefConcat;
B: now
let x;
assume
B1: (x in A or x in B) & x <> <%>E;
B2: now
assume
B2a: x in A;
then reconsider xa = x as Element of E^omega;
B2b: xa ^ b in A ^^ B by A3, B2a, DefConcat;
xa ^ b <> <%>E by B1, AFINSQ_1:33;
hence contradiction by B2b, A1, TARSKI:def 1;
end;
B3: now
assume
B3a: x in B;
then reconsider xb = x as Element of E^omega;
B3b: a ^ xb in A ^^ B by A3, B3a, DefConcat;
a ^ xb <> <%>E by B1, AFINSQ_1:33;
hence contradiction by B3b, A1, TARSKI:def 1;
end;
thus contradiction by B1, B2, B3;
end;
(x in A iff x = <%>E) & (x in B iff x = <%>E) by A3, B;
hence contradiction by A2, TARSKI:def 1;
end;
assume A = {<%>E} & B = {<%>E};
hence thesis by ThConcat80;
end;
theorem ThConcat100:
<%>E in A ^^ B iff <%>E in A & <%>E in B
proof
thus <%>E in A ^^ B implies <%>E in A & <%>E in B
proof
assume <%>E in A ^^ B;
then consider a, b such that
A: a in A & b in B & a ^ b = <%>E by DefConcat;
thus thesis by A, AFINSQ_1:33;
end;
assume <%>E in A & <%>E in B;
then <%>E ^ <%>E in A ^^ B by DefConcat;
hence thesis by AFINSQ_1:32;
end;
theorem ThConcat110:
<%>E in B implies A c= A ^^ B & A c= B ^^ A
proof
assume
A: <%>E in B;
thus A c= A ^^ B
proof
let x;
assume
B1: x in A;
then reconsider xa = x as Element of E^omega;
xa ^ <%>E in A ^^ B by A, B1, DefConcat;
hence x in A ^^ B by AFINSQ_1:32;
end;
thus A c= B ^^ A
proof
let x;
assume
C1: x in A;
then reconsider xa = x as Element of E^omega;
<%>E ^ xa in B ^^ A by A, C1, DefConcat;
hence x in B ^^ A by AFINSQ_1:32;
end;
end;
theorem ThConcat10:
A c= C & B c= D implies A ^^ B c= C ^^ D
proof
assume
A: A c= C & B c= D;
thus thesis
proof
let x;
assume x in A ^^ B;
then consider a, b such that
B: a in A & b in B & x = a ^ b by DefConcat;
thus x in C ^^ D by A, B, DefConcat;
end;
end;
theorem ThConcat20:
(A ^^ B) ^^ C = A ^^ (B ^^ C)
proof
now
let x;
thus x in (A ^^ B) ^^ C implies x in A ^^ (B ^^ C)
proof
assume x in (A ^^ B) ^^ C;
then consider ab, c such that
A1: ab in (A ^^ B) & c in C & x = ab ^ c by DefConcat;
consider a, b such that
A2: a in A & b in B & ab = a ^ b by A1, DefConcat;
A3: x = a ^ (b ^ c) by A1, A2, AFINSQ_1:30;
b ^ c in B ^^ C by A1, A2, DefConcat;
hence thesis by A2, A3, DefConcat;
end;
assume x in A ^^ (B ^^ C);
then consider a, bc such that
A1: a in A & bc in (B ^^ C) & x = a ^ bc by DefConcat;
consider b, c such that
A2: b in B & c in C & bc = b ^ c by A1, DefConcat;
A3: x = (a ^ b) ^ c by A1, A2, AFINSQ_1:30;
a ^ b in A ^^ B by A1, A2, DefConcat;
hence x in (A ^^ B) ^^ C by A2, A3, DefConcat;
end;
hence thesis by TARSKI:2;
end;
theorem ThConcat30:
A ^^ (B /\ C) c= (A ^^ B) /\ (A ^^ C) &
(B /\ C) ^^ A c= (B ^^ A) /\ (C ^^ A)
proof
thus A ^^ (B /\ C) c= (A ^^ B) /\ (A ^^ C)
proof
let x;
assume x in A ^^ (B /\ C);
then consider a, bc such that
A1: a in A & bc in B /\ C & x = a ^ bc by DefConcat;
bc in B & bc in C by A1, XBOOLE_0:def 3;
then x in A ^^ B & x in A ^^ C by A1, DefConcat;
hence x in (A ^^ B) /\ (A ^^ C) by XBOOLE_0:def 3;
end;
thus (B /\ C) ^^ A c= (B ^^ A) /\ (C ^^ A)
proof
let x;
assume x in (B /\ C) ^^ A;
then consider bc, a such that
B1: bc in B /\ C & a in A & x = bc ^ a by DefConcat;
bc in B & bc in C by B1, XBOOLE_0:def 3;
then x in B ^^ A & x in C ^^ A by B1, DefConcat;
hence x in (B ^^ A) /\ (C ^^ A) by XBOOLE_0:def 3;
end;
end;
theorem ThConcat40:
A ^^ B \/ A ^^ C = A ^^ (B \/ C) &
B ^^ A \/ C ^^ A = (B \/ C) ^^ A
proof
A:
A ^^ (B \/ C) c= (A ^^ B) \/ (A ^^ C)
proof
let x;
assume x in A ^^ (B \/ C);
then consider a, bc such that
A1: a in A & bc in B \/ C & x = a ^ bc by DefConcat;
bc in B or bc in C by A1, XBOOLE_0:def 2;
then x in A ^^ B or x in A ^^ C by A1, DefConcat;
hence x in (A ^^ B) \/ (A ^^ C) by XBOOLE_0:def 2;
end;
B:
(B \/ C) ^^ A c= (B ^^ A) \/ (C ^^ A)
proof
let x;
assume x in (B \/ C) ^^ A;
then consider bc, a such that
B1: bc in B \/ C & a in A & x = bc ^ a by DefConcat;
bc in B or bc in C by B1, XBOOLE_0:def 2;
then x in B ^^ A or x in C ^^ A by B1, DefConcat;
hence x in (B ^^ A) \/ (C ^^ A) by XBOOLE_0:def 2;
end;
C:
now
B c= B \/ C & C c= B \/ C by XBOOLE_1:7;
then A ^^ B c= A ^^ (B \/ C) & A ^^ C c= A ^^ (B \/ C) by ThConcat10;
hence (A ^^ B) \/ (A ^^ C) c= A ^^ (B \/ C) by XBOOLE_1:8;
end;
D:
now
B c= B \/ C & C c= B \/ C by XBOOLE_1:7;
then B ^^ A c= (B \/ C) ^^ A & C ^^ A c= (B \/ C) ^^ A by ThConcat10;
hence (B ^^ A) \/ (C ^^ A) c= (B \/ C) ^^ A by XBOOLE_1:8;
end;
thus thesis by A, B, C, D, XBOOLE_0:def 10;
end;
theorem ThConcat50:
(A ^^ B) \ (A ^^ C) c= A ^^ (B \ C) &
(B ^^ A) \ (C ^^ A) c= (B \ C) ^^ A
proof
thus (A ^^ B) \ (A ^^ C) c= A ^^ (B \ C)
proof
let x;
assume x in (A ^^ B) \ (A ^^ C);
then
A1: x in A ^^ B & not x in A ^^ C by XBOOLE_0:def 4;
then consider a, b such that
A2: a in A & b in B & x = a ^ b by DefConcat;
A4: now
assume not b in C;
then b in B \ C by A2, XBOOLE_0:def 4;
hence x in A ^^ (B \ C) by A2, DefConcat;
end;
thus x in A ^^ (B \ C) by A1, A2, DefConcat, A4;
end;
thus (B ^^ A) \ (C ^^ A) c= (B \ C) ^^ A
proof
let x;
assume x in (B ^^ A) \ (C ^^ A);
then
B1: x in B ^^ A & not x in C ^^ A by XBOOLE_0:def 4;
then consider b, a such that
B2: b in B & a in A & x = b ^ a by DefConcat;
B4: now
assume not b in C;
then b in B \ C by B2, XBOOLE_0:def 4;
hence x in (B \ C) ^^ A by B2, DefConcat;
end;
thus x in (B \ C) ^^ A by B1, B2, DefConcat, B4;
end;
end;
theorem
(A ^^ B) \+\ (A ^^ C) c= A ^^ (B \+\ C) &
(B ^^ A) \+\ (C ^^ A) c= (B \+\ C) ^^ A
proof
A:
now
A1: A ^^ (B /\ C) c= (A ^^ B) /\ (A ^^ C) by ThConcat30;
A2: (A ^^ (B \/ C)) \ (A ^^ (B /\ C)) c=
A ^^ ((B \/ C) \ (B /\ C)) by ThConcat50;
(A ^^ B) \+\ (A ^^ C)
= ((A ^^ B) \/ (A ^^ C)) \ ((A ^^ B) /\ (A ^^ C)) by XBOOLE_1:101
.= (A ^^ (B \/ C)) \ ((A ^^ B) /\ (A ^^ C)) by ThConcat40;
then (A ^^ B) \+\ (A ^^ C) c=
(A ^^ (B \/ C)) \ (A ^^ (B /\ C)) by A1, XBOOLE_1:34;
then (A ^^ B) \+\ (A ^^ C) c= A ^^ ((B \/ C) \ (B /\ C)) by A2, XBOOLE_1:1;
hence (A ^^ B) \+\ (A ^^ C) c= A ^^ (B \+\ C) by XBOOLE_1:101;
end;
B:
now
B1: (B /\ C) ^^ A c= (B ^^ A) /\ (C ^^ A) by ThConcat30;
B2: ((B \/ C) ^^ A) \ ((B /\ C) ^^ A) c=
((B \/ C) \ (B /\ C)) ^^ A by ThConcat50;
(B ^^ A) \+\ (C ^^ A)
= ((B ^^ A) \/ (C ^^ A)) \ ((B ^^ A) /\ (C ^^ A)) by XBOOLE_1:101
.= ((B \/ C) ^^ A) \ ((B ^^ A) /\ (C ^^ A)) by ThConcat40;
then (B ^^ A) \+\ (C ^^ A) c=
((B \/ C) ^^ A) \ ((B /\ C) ^^ A) by B1, XBOOLE_1:34;
then (B ^^ A) \+\ (C ^^ A) c= ((B \/ C) \ (B /\ C)) ^^ A by B2, XBOOLE_1:1;
hence (B ^^ A) \+\ (C ^^ A) c= (B \+\ C) ^^ A by XBOOLE_1:101;
end;
thus thesis by A, B;
end;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Concatenation of a Language with Itself
:: Definition of |^
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, A, n;
func A |^ n -> Subset of E^omega means :DefPower:
ex concat being Function of NAT, bool (E^omega) st
it = concat.n &
concat.0 = {<%>E} &
for i holds concat.(i + 1) = concat.i ^^ A;
existence
proof
defpred P[set, set, set] means
ex B, C st C = $3 & B = $2 & C = B ^^ A;
A: for i being Element of NAT
for x being Element of bool (E^omega)
ex y being Element of bool (E^omega) st P[i, x, y]
proof
let i be Element of NAT;
let x be Element of bool (E^omega);
take x ^^ A;
thus thesis;
end;
consider f being Function of NAT, bool (E^omega) such that
B: f.0 = {<%>E} & for i being Element of NAT holds P[i, f.i, f.(i + 1)]
from RECDEF_1:sch 2(A);
consider C being Subset of E^omega such that
C: C = f.n;
take C;
C2: now
let i;
reconsider j = i as Element of NAT by ORDINAL1:def 13;
consider B, C such that
C2A: C = f.(j + 1) & B = f.j & C = B ^^ A by B;
thus f.(i + 1) = f.i ^^ A by C2A;
end;
thus thesis by B, C, C2;
end;
uniqueness
proof
let C1, C2 be Subset of E^omega;
given f1 being Function of NAT, bool (E^omega) such that
A1: C1 = f1.n &
f1.0 = {<%>E} &
for i holds f1.(i + 1) = f1.i ^^ A;
given f2 being Function of NAT, bool (E^omega) such that
A2: C2 = f2.n &
f2.0 = {<%>E} &
for i holds f2.(i + 1) = f2.i ^^ A;
defpred P[Nat] means f1.$1 = f2.$1;
B1: P[0] by A1, A2;
B2: now
let k;
assume
B2A: P[k];
f2.(k + 1) = f2.k ^^ A by A2;
hence P[k + 1] by B2A, A1;
end;
for k holds P[k] from NAT_1:sch 2(B1, B2);
hence thesis by A1, A2;
end;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Concatenation of a Language with Itself
:: Properties of |^
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem ThPower10:
A |^ (n + 1) = (A |^ n) ^^ A
proof
consider concat being Function of NAT, bool (E^omega) such that
A: A |^ n = concat.n &
concat.0 = {<%>E} &
for i holds concat.(i + 1) = concat.i ^^ A by DefPower;
concat.(n + 1) = (A |^ n) ^^ A by A;
hence thesis by DefPower, A;
end;
theorem ThPower20:
A |^ 0 = {<%>E}
proof
consider concat being Function of NAT, bool (E^omega) such that
A: A |^ 0 = concat.0 &
concat.0 = {<%>E} &
for i holds concat.(i + 1) = concat.i ^^ A by DefPower;
thus thesis by A;
end;
theorem ThPower30:
A |^ 1 = A
proof
consider concat being Function of NAT, bool (E^omega) such that
A: A |^ 1 = concat.1 &
concat.0 = {<%>E} &
for i holds concat.(i + 1) = concat.i ^^ A by DefPower;
thus A |^ 1 = concat.(0 + 1) by A
.= {<%>E} ^^ A by A
.= A by ThConcat80;
end;
theorem ThPower40:
A |^ 2 = A ^^ A
proof
thus A |^ 2 = A |^ (1 + 1)
.= (A |^ 1) ^^ A by ThPower10
.= A ^^ A by ThPower30;
end;
theorem ThPower50:
A |^ n = {} iff n > 0 & A = {}
proof
thus A |^ n = {} implies n > 0 & A = {}
proof
assume that
A1: A |^ n = {} and
A2: n <= 0 or A <> {};
B: now
assume
B1: A <> {};
defpred P[Nat] means A |^ $1 <> {};
C: P[0]
proof
A |^ 0 = {<%>E} by ThPower20;
hence thesis;
end;
D: now
let n;
assume
D1: P[n];
consider a1 such that
E1: a1 in A |^ n by D1, SUBSET_1:10;
consider a2 such that
E2: a2 in A by B1, SUBSET_1:10;
a1 ^ a2 in A |^ n ^^ A by E1, E2, DefConcat;
hence P[n + 1] by ThPower10;
end;
for n holds P[n] from NAT_1:sch 2(C, D);
hence contradiction by A1;
end;
now
assume n <= 0;
then n = 0;
then A |^ n = {<%>E} by ThPower20;
hence contradiction by A1;
end;
hence thesis by A2, B;
end;
assume
A1: n > 0 & A = {};
then
A2: n >= 0 + 1 by NAT_1:13;
defpred P[Nat] means A |^ $1 = {};
B:
P[1] by A1, ThPower30;
C:
now
let m be Element of NAT;
assume 1 <= m & P[m];
{}(E^omega) |^ (m + 1) = {}(E^omega) |^ m ^^ {}(E^omega) by ThPower10
.= {} by ThConcat70;
hence P[m + 1] by A1;
end;
D:
for m being Element of NAT st m >= 1 holds P[m] from NAT_1:sch 8(B, C);
for n st n >= 1 holds P[n]
proof
let n;
reconsider m = n as Element of NAT by ORDINAL1:def 13;
m >= 1 implies P[m] by D;
hence thesis;
end;
hence thesis by A2;
end;
theorem ThPower60:
{<%>E} |^ n = {<%>E}
proof
defpred P[Nat] means {<%>E} |^ $1 = {<%>E};
A:
P[0] by ThPower20;
B:
now
let n;
assume
B1: P[n];
{<%>E} |^ (n + 1) = ({<%>E} |^ n) ^^ {<%>E} by ThPower10
.= {<%>E} by B1, ThConcat80;
hence P[n + 1];
end;
for n holds P[n] from NAT_1:sch 2(A, B);
hence thesis;
end;
theorem
A |^ n = {<%>E} iff n = 0 or A = {<%>E}
proof
thus A |^ n = {<%>E} implies n = 0 or A = {<%>E}
proof
assume
A: A |^ n = {<%>E};
now
assume n > 0;
then consider m such that
B: m + 1 = n by NAT_1:6;
A |^ n = (A |^ m) ^^ A by B, ThPower10;
hence A = {<%>E} by A, ThConcat90;
end;
hence thesis;
end;
assume n = 0 or A = {<%>E};
hence thesis by ThPower20, ThPower60;
end;
theorem ThPower70:
<%>E in A implies <%>E in A |^ n
proof
assume
A: <%>E in A;
defpred P[Nat] means <%>E in A |^ $1;
B:
P[0]
proof
A |^ 0 = {<%>E} by ThPower20;
hence thesis by TARSKI:def 1;
end;
C:
now
let n;
assume P[n];
then <%>E in (A |^ n) ^^ A by A, ThConcat100;
hence P[n + 1] by ThPower10;
end;
for n holds P[n] from NAT_1:sch 2(B, C);
hence thesis;
end;
theorem
<%>E in A |^ n & n > 0 implies <%>E in A
proof
assume
A: <%>E in A |^ n & n > 0;
then consider m such that
B: m + 1 = n by NAT_1:6;
A |^ n = (A |^ m) ^^ A by B, ThPower10;
then consider a1, a2 such that
C: a1 in A |^ m & a2 in A & a1 ^ a2 = <%>E by A, DefConcat;
thus thesis by C, AFINSQ_1:33;
end;
theorem ThPower80:
(A |^ n) ^^ A = A ^^ (A |^ n)
proof
defpred P[Nat] means (A |^ $1) ^^ A = A ^^ (A |^ $1);
A:
P[0]
proof
thus (A |^ 0) ^^ A = {<%>E} ^^ A by ThPower20
.= A by ThConcat80
.= A ^^ {<%>E} by ThConcat80
.= A ^^ (A |^ 0) by ThPower20;
end;
B:
now
let n;
assume
B1: P[n];
(A |^ (n + 1)) ^^ A = ((A |^ n) ^^ A) ^^ A by ThPower10
.= A ^^ ((A |^ n) ^^ A) by B1, ThConcat20
.= A ^^ (A |^ (n + 1)) by ThPower10;
hence P[n + 1];
end;
for n holds P[n] from NAT_1:sch 2(A, B);
hence thesis;
end;
theorem ThPower90:
A |^ (m + n) = (A |^ m) ^^ (A |^ n)
proof
defpred P[Nat] means
for m, n st m + n <= $1 holds A |^ (m + n) = (A |^ m) ^^ (A |^ n);
A:
P[0]
proof
let m, n;
assume m + n <= 0;
then
A0: m + n = 0;
then
A1: m = 0 & n = 0 by NAT_1:7;
thus A |^ (m + n) = (A |^ 0) ^^ {<%>E} by A0, ThConcat80
.= (A |^ m) ^^ (A |^ n) by ThPower20, A1;
end;
B:
now
let l;
assume
B1: P[l];
now
let m, n be Nat;
assume
C1: m + n <= l + 1;
C2: now
assume
C2'1: m + n = l + 1;
C2'2: now
assume
C2'2A: m = 0;
thus A |^ (m + n) = {<%>E} ^^ (A |^ (l + 1)) by C2'1, ThConcat80
.= (A |^ m) ^^ (A |^ n) by ThPower20, C2'2A, C2'1;
end;
C2'3: now
assume
C2'3A: n = 0;
thus A |^ (m + n) = (A |^ (l + 1)) ^^ {<%>E} by C2'1, ThConcat80
.= (A |^ m) ^^ (A |^ n) by ThPower20, C2'3A, C2'1;
end;
C2'4: now
assume
C2'4A1: m > 0 & n > 0;
then consider k such that
C2'4A2: k + 1 = m by NAT_1:6;
C2'4C: k + 1 <= l by C2'4A1, C2'4A2, C2'1, LmNum30;
A |^ (m + n) = A |^ (k + n + 1) by C2'4A2
.= (A |^ (k + n)) ^^ A by ThPower10
.= A ^^ (A |^ (k + n)) by ThPower80
.= A ^^ ((A |^ k) ^^ (A |^ n)) by C2'4A2, C2'1, B1
.= (A ^^ (A |^ k)) ^^ (A |^ n) by ThConcat20
.= ((A |^ k) ^^ A) ^^ (A |^ n) by ThPower80
.= ((A |^ k) ^^ (A |^ 1)) ^^ (A |^ n) by ThPower30
.= (A |^ m) ^^ (A |^ n) by C2'4C, B1, C2'4A2;
hence A |^ (m + n) = (A |^ m) ^^ (A |^ n);
end;
thus A |^ (m + n) = (A |^ m) ^^ (A |^ n) by C2'2, C2'3, C2'4;
end;
C3: now
assume m + n < l + 1;
then m + n <= l by NAT_1:13;
hence A |^ (m + n) = (A |^ m) ^^ (A |^ n) by B1;
end;
thus A |^ (m + n) = (A |^ m) ^^ (A |^ n) by C1, REAL_1:def 5, C2, C3;
end;
hence P[l + 1];
end;
for l holds P[l] from NAT_1:sch 2(A, B);
hence thesis;
end;
theorem
(A |^ m) |^ n = A |^ (m * n)
proof
defpred P[Nat] means
for m, n st m + n <= $1 holds (A |^ m) |^ n = A |^ (m * n);
A:
P[0]
proof
let m, n;
assume m + n <= 0;
then m + n = 0;
then
A1: m = 0 & n = 0 by NAT_1:7;
hence (A |^ m) |^ n = {<%>E} by ThPower20
.= A |^ (m * n) by ThPower20, A1;
end;
B:
now
let l;
assume
B1: P[l];
now
let m, n;
assume
C1: m + n <= l + 1;
C2: now
assume
C2'1: m + n = l + 1;
C2'2: now
assume
C2'2A: m = 0;
thus (A |^ m) |^ n = {<%>E} |^ n by C2'2A, ThPower20
.= {<%>E} by ThPower60
.= A |^ (m * n) by ThPower20, C2'2A;
end;
C2'3: now
assume
C2'3A: n = 0;
hence (A |^ m) |^ n = {<%>E} by ThPower20
.= A |^ (m * n) by ThPower20, C2'3A;
end;
C2'4: now
assume m > 0 & n > 0;
then consider k such that
C2'4A2: k + 1 = n by NAT_1:6;
C2'4B: m + k <= l by C2'4A2, C2'1;
(A |^ m) |^ n = ((A |^ m) |^ k) ^^ (A |^ m) by C2'4A2, ThPower10
.= (A |^ (m * k)) ^^ (A |^ m) by C2'4B, B1
.= A |^ (m * k + m) by ThPower90
.= A |^ (m * n) by C2'4A2;
hence (A |^ m) |^ n = A |^ (m * n);
end;
thus (A |^ m) |^ n = A |^ (m * n) by C2'2, C2'3, C2'4;
end;
C3: now
assume m + n < l + 1;
then m + n <= l by NAT_1:13;
hence (A |^ m) |^ n = A |^ (m * n) by B1;
end;
thus (A |^ m) |^ n = A |^ (m * n) by C1, REAL_1:def 5, C2, C3;
end;
hence P[l + 1];
end;
D:
for l holds P[l] from NAT_1:sch 2(A, B);
now
let m, n;
reconsider l = m + n as Nat;
m + n <= l;
hence (A |^ m) |^ n = A |^ (m * n) by D;
end;
hence thesis;
end;
theorem ThPower120:
<%>E in A & n > 0 implies A c= A |^ n
proof
assume that
A1: <%>E in A and
A2: n > 0;
consider m such that
B: m + 1 = n by A2, NAT_1:6;
<%>E in A |^ m by A1, ThPower70;
then A c= A |^ m ^^ A by ThConcat110;
hence thesis by B, ThPower10;
end;
theorem
<%>E in A & m > n implies A |^ n c= A |^ m
proof
assume that
A1: <%>E in A and
A2: m > n;
consider k such that
B: n + k = m by A2, NAT_1:10;
<%>E in A |^ k by A1, ThPower70;
then A |^ n c= A |^ k ^^ A |^ n by ThConcat110;
hence thesis by B, ThPower90;
end;
theorem ThPower130:
A c= B implies A |^ n c= B |^ n
proof
assume
A: A c= B;
defpred P[Nat] means A |^ $1 c= B |^ $1;
B:
P[0]
proof
A |^ 0 = {<%>E} & B |^ 0 = {<%>E} by ThPower20;
hence thesis;
end;
C:
now
let n;
assume
C1: P[n];
(A |^ n) ^^ A = A |^ (n + 1) & (B |^ n) ^^ B = B |^ (n + 1) by ThPower10;
hence P[n + 1] by C1, A, ThConcat10;
end;
for n holds P[n] from NAT_1:sch 2(B, C);
hence thesis;
end;
theorem
(A |^ n) \/ (B |^ n) c= (A \/ B) |^ n
proof
A c= A \/ B & B c= A \/ B by XBOOLE_1:7;
then A |^ n c= (A \/ B) |^ n & B |^ n c= (A \/ B) |^ n by ThPower130;
hence thesis by XBOOLE_1:8;
end;
theorem
(A /\ B) |^ n c= (A |^ n) /\ (B |^ n)
proof
A /\ B c= A & A /\ B c= B by XBOOLE_1:17;
then (A /\ B) |^ n c= A |^ n & (A /\ B) |^ n c= B |^ n by ThPower130;
hence thesis by XBOOLE_1:19;
end;
theorem ThPower160:
a in C |^ m & b in C |^ n implies a ^ b in C |^ (m + n)
proof
assume a in C |^ m & b in C |^ n;
then a ^ b in (C |^ m) ^^ (C |^ n) by DefConcat;
hence thesis by ThPower90;
end;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Kleene Closure
:: Definition of *
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, A;
func A* -> Subset of E^omega equals
union { B : ex n st B = A |^ n };
coherence
proof
defpred P[set] means ex n st $1 = A |^ n;
reconsider M = { B : P[B] } as Subset-Family of E^omega
from DOMAIN_1:sch 7;
union M is Subset of E^omega;
hence thesis;
end;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Kleene Closure
:: Properties of *
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem ThClosure10:
x in A* iff ex n st x in A |^ n
proof
thus x in A* implies ex n st x in A |^ n
proof
assume
A: x in A*;
consider X such that
A1: x in X and
A2: X in { B : ex k st B = A |^ k } by A, TARSKI:def 4;
defpred P[set] means ex k st $1 = A |^ k;
A3: X in { B : P[B] } by A2;
P[X] from CARD_FIL:sch 1(A3);
hence thesis by A1;
end;
given n such that
B: x in A |^ n;
defpred P[set] means ex k st $1 = A |^ k;
consider B such that
D: x in B & P[B] by B;
reconsider A = { C : P[C] } as Subset-Family of E^omega from DOMAIN_1:sch 7;
B in A by D;
hence thesis by D, TARSKI:def 4;
end;
theorem ThClosure40:
A |^ n c= A*
proof
(A |^ n) in { B : ex k st B = A |^ k };
hence thesis by ZFMISC_1:92;
end;
theorem ThClosure50:
A c= A*
proof
A = A |^ 1 by ThPower30;
hence thesis by ThClosure40;
end;
theorem
A ^^ A c= A*
proof
A ^^ A = A |^ 2 by ThPower40;
hence thesis by ThClosure40;
end;
theorem ThClosure60:
a in C* & b in C* implies a ^ b in C*
proof
assume
A: a in C* & b in C*;
consider k such that
Ak: a in C |^ k by A, ThClosure10;
consider l such that
Al: b in C |^ l by A, ThClosure10;
a ^ b in C |^ (k + l) by Ak, Al, ThPower160;
hence thesis by ThClosure10;
end;
theorem ThClosure70:
A c= C* & B c= C* implies A ^^ B c= C*
proof
assume
A: A c= C* & B c= C*;
thus thesis
proof
let x;
assume x in A ^^ B;
then consider a, b such that
B: a in A & b in B & x = a ^ b by DefConcat;
thus x in C* by A, B, ThClosure60;
end;
end;
theorem
A* = {<%>E} iff A = {} or A = {<%>E}
proof
thus A* = {<%>E} implies A = {} or A = {<%>E}
proof
assume that
A1: A* = {<%>E} and
A2: A <> {} & A <> {<%>E};
consider x such that
A3: x in A & x <> <%>E by A2, ZFMISC_1:41;
reconsider a = x as Element of E^omega by A3;
A c= A* by ThClosure50;
hence contradiction by A1, TARSKI:def 1,A3;
end;
B:
now
assume
B0: A = {};
B1: now
let x;
assume x in A*;
then consider n such that
B2: x in A |^ n by ThClosure10;
B3: n = 0 implies x in {<%>E} by B2, ThPower20;
n > 0 implies contradiction by B0, B2, ThPower50;
hence x in {<%>E} by B3;
end;
now
let x;
assume x in {<%>E};
then x in A |^ 0 by ThPower20;
hence x in A* by ThClosure10;
end;
hence A* = {<%>E} by B1, TARSKI:2;
end;
now
assume
C1: A = {<%>E};
C2: A* c= {<%>E}
proof
let x;
assume x in A*;
then consider n such that
C3: x in A |^ n by ThClosure10;
thus x in {<%>E} by C1, C3, ThPower60;
end;
{<%>E} c= A*
proof
let x;
assume x in {<%>E};
then x in A |^ 0 by ThPower20;
hence x in A* by ThClosure10;
end;
hence A* = {<%>E} by C2, XBOOLE_0:def 10;
end;
hence thesis by B;
end;
theorem ThClosure30:
<%>E in A*
proof
{<%>E} = A |^ 0 by ThPower20;
then <%>E in A |^ 0 by TARSKI:def 1;
hence thesis by ThClosure10;
end;
theorem
A* = {x} implies x = <%>E
proof
assume
A: A* = {x} & x <> <%>E;
then
B: x in A* by ZFMISC_1:37;
reconsider a = x as Element of E^omega by A, ZFMISC_1:37;
C:
a ^ a in A* by B, ThClosure60;
a ^ a <> x by A, LmSeq50;
hence thesis by A, C, TARSKI:def 1;
end;
theorem ThClosure15:
x in A |^ (m + 1) implies x in (A*) ^^ A & x in A ^^ (A*)
proof
assume x in A |^ (m + 1);
then
A: x in (A |^ m) ^^ A by ThPower10;
then consider a, b such that
B: a in A |^ m & b in A & x = a ^ b by DefConcat;
a in A* & b in A by B, ThClosure10;
hence x in (A*) ^^ A by DefConcat, B;
x in A ^^ (A |^ m) by A, ThPower80;
then consider a, b such that
C: a in A & b in A |^ m & x = a ^ b by DefConcat;
a in A & b in A* by C, ThClosure10;
hence x in A ^^ (A*) by DefConcat, C;
end;
theorem
A |^ (m + 1) c= (A*) ^^ A & A |^ (m + 1) c= A ^^ (A*)
proof
thus A |^ (m + 1) c= (A*) ^^ A
proof
let x;
assume x in A |^ (m + 1);
hence x in (A*) ^^ A by ThClosure15;
end;
let x;
assume x in A |^ (m + 1);
hence x in A ^^ (A*) by ThClosure15;
end;
theorem ThClosure20:
x in (A*) ^^ A or x in A ^^ (A*) implies x in A*
proof
B:
now
let x;
assume x in (A*) ^^ A;
then consider a, b such that
B1: a in A* & b in A & x = a ^ b by DefConcat;
consider n such that
B2: a in A |^ n by B1, ThClosure10;
b in A |^ 1 by B1, ThPower30;
then a ^ b in A |^ (n + 1) by B2, ThPower160;
hence x in A* by ThClosure10, B1;
end;
C:
now
let x;
assume x in A ^^ (A*);
then consider a, b such that
C1: a in A & b in A* & x = a ^ b by DefConcat;
consider n such that
C2: b in A |^ n by C1, ThClosure10;
a in A |^ 1 by C1, ThPower30;
then a ^ b in A |^ (n + 1) by C2, ThPower160;
hence x in A* by ThClosure10, C1;
end;
thus thesis by B, C;
end;
theorem
(A*) ^^ A c= A* & A ^^ (A*) c= A*
proof
thus (A*) ^^ A c= A*
proof
let x;
assume x in (A*) ^^ A;
hence x in A* by ThClosure20;
end;
thus A ^^ (A*) c= A*
proof
let x;
assume x in A^^ (A*);
hence x in A* by ThClosure20;
end;
end;
theorem ThClosure38:
<%>E in A implies A* = (A*) ^^ A & A* = A ^^ (A*)
proof
assume
A1: <%>E in A;
A2:
<%>E in A* by ThClosure30;
B:
for x holds
(x in (A*) ^^ A implies x in A*) &
(x in A ^^ (A*) implies x in A*) by ThClosure20;
now
let x;
assume x in A*;
then consider n such that
D1: x in A |^ n by ThClosure10;
D2: now
assume n = 0;
then x in {<%>E} by D1, ThPower20;
then x = <%>E by TARSKI:def 1;
hence x in (A*) ^^ A & x in A ^^ (A*) by A1, A2, ThConcat100;
end;
E:
now
assume n > 0;
then consider m such that
E1: m + 1 = n by NAT_1:6;
thus x in (A*) ^^ A by D1, E1, ThClosure15;
end;
F:
now
assume n > 0;
then consider m such that
F1: m + 1 = n by NAT_1:6;
thus x in A ^^ (A*) by D1, F1, ThClosure15;
end;
thus x in (A*) ^^ A & x in A ^^ (A*) by D2, E, F;
end;
then (x in A* implies x in (A*) ^^ A) &
(x in A* implies x in A ^^ (A*));
hence thesis by B, TARSKI:2;
end;
theorem
<%>E in A implies A* = (A*) ^^ (A |^ n) & A* = (A |^ n) ^^ (A*)
proof
assume
A0: <%>E in A;
defpred P[Nat] means A* = (A*) ^^ (A |^ $1) & A* = (A |^ $1) ^^ (A*);
A:
P[0]
proof
thus (A*) ^^ (A |^ 0) = (A*) ^^ {<%>E} by ThPower20
.= A* by ThConcat80;
thus (A |^ 0) ^^ (A*) = {<%>E} ^^ (A*) by ThPower20
.= A* by ThConcat80;
end;
B:
now
let n;
assume
B1: P[n];
B2: (A*) ^^ (A |^ (n + 1)) = (A*) ^^ ((A |^ n) ^^ A) by ThPower10
.= (A*) ^^ A by ThConcat20, B1
.= A* by A0, ThClosure38;
B3: (A |^ (n + 1)) ^^ (A*) = ((A |^ n) ^^ A) ^^ (A*) by ThPower10
.= (A ^^ (A |^ n)) ^^ (A*) by ThPower80
.= A ^^ (A*) by ThConcat20, B1
.= A* by A0, ThClosure38;
thus P[n + 1] by B2, B3;
end;
for n holds P[n] from NAT_1:sch 2(A, B);
hence thesis;
end;
theorem ThClosure39:
A* = {<%>E} \/ A ^^ (A*) & A* = {<%>E} \/ (A*) ^^ A
proof
A:
now
let x;
assume x in A*;
then consider n such that
A1: x in A |^ n by ThClosure10;
A2: n = 0 implies x in {<%>E} by A1, ThPower20;
now
assume n > 0;
then consider m such that
A3: m + 1 = n by NAT_1:6;
thus x in (A*) ^^ A by A1, A3, ThClosure15;
end;
hence x in {<%>E} \/ (A*) ^^ A by A2, XBOOLE_0:def 2;
end;
B:
now
let x;
assume x in A*;
then consider n such that
B1: x in A |^ n by ThClosure10;
B2: n = 0 implies x in {<%>E} by B1, ThPower20;
now
assume n > 0;
then consider m such that
B3: m + 1 = n by NAT_1:6;
thus x in A ^^ (A*) by B1, B3, ThClosure15;
end;
hence x in {<%>E} \/ A ^^ (A*) by B2, XBOOLE_0:def 2;
end;
C:
now
let x;
assume x in {<%>E} \/ A ^^ (A*);
then x in {<%>E} or x in A ^^ (A*) by XBOOLE_0:def 2;
then x = <%>E or x in A* by TARSKI:def 1, ThClosure20;
hence x in A* by ThClosure30;
end;
D:
now
let x;
assume x in {<%>E} \/ (A*) ^^ A;
then x in {<%>E} or x in (A*) ^^ A by XBOOLE_0:def 2;
then x = <%>E or x in A* by TARSKI:def 1, ThClosure20;
hence x in A* by ThClosure30;
end;
thus thesis by A, B, C, D, TARSKI:2;
end;
theorem ThClosure105:
A ^^ (A*) = (A*) ^^ A
proof
A:
A* = {<%>E} \/ A ^^ (A*) & A* = {<%>E} \/ (A*) ^^ A by ThClosure39;
now per cases;
suppose <%>E in A;
then A* = A ^^ (A*) & A* = (A*) ^^ A by ThClosure38;
hence A ^^ (A*) = (A*) ^^ A;
end;
suppose not <%>E in A;
then not <%>E in A ^^ (A*) & not <%>E in (A*) ^^ A by ThConcat100;
then {<%>E} misses A ^^ (A*) & {<%>E} misses (A*) ^^ A by ZFMISC_1:56;
hence A ^^ (A*) = (A*) ^^ A by A, XBOOLE_1:71;
end;
end;
hence thesis;
end;
theorem
(A |^ n) ^^ (A*) = (A*) ^^ (A |^ n)
proof
defpred P[Nat] means (A |^ $1) ^^ (A*) = (A*) ^^ (A |^ $1);
A:
P[0]
proof
thus (A |^ 0) ^^ (A*) = {<%>E} ^^ (A*) by ThPower20
.= A* by ThConcat80
.= (A*) ^^ {<%>E} by ThConcat80
.= (A*) ^^ (A |^ 0) by ThPower20;
end;
B:
now
let n;
assume
B1: P[n];
(A |^ (n + 1)) ^^ (A*) = (A |^ n ^^ A) ^^ (A*) by ThPower10
.= A |^ n ^^ (A ^^ (A*)) by ThConcat20
.= A |^ n ^^ ((A*) ^^ A) by ThClosure105
.= ((A*) ^^ A |^ n) ^^ A by B1, ThConcat20
.= (A*) ^^ (A |^ n ^^ A) by ThConcat20
.= (A*) ^^ A |^ (n + 1) by ThPower10;
hence P[n + 1];
end;
for n holds P[n] from NAT_1:sch 2(A, B);
hence thesis;
end;
theorem ThClosure80:
A c= B* implies A |^ n c= B*
proof
assume
A: A c= B*;
defpred P[Nat] means A |^ $1 c= B*;
B:
P[0]
proof
<%>E in B* by ThClosure30;
then {<%>E} c= B* by ZFMISC_1:37;
hence thesis by ThPower20;
end;
C:
now
let n;
assume P[n];
then (A |^ n) ^^ A c= B* by A, ThClosure70;
hence P[n + 1] by ThPower10;
end;
for n holds P[n] from NAT_1:sch 2(B, C);
hence thesis;
end;
theorem ThClosure90:
A c= B* implies A* c= B*
proof
assume
A: A c= B*;
thus thesis
proof
let x;
assume
B1: x in A*;
consider n such that
B2: x in A |^ n by B1, ThClosure10;
A |^ n c= B* by A, ThClosure80;
hence x in B* by B2;
end;
end;
theorem ThClosure100:
A c= B implies A* c= B*
proof
assume
A: A c= B;
B c= B* by ThClosure50;
then A c= B* by A, XBOOLE_1:1;
hence thesis by ThClosure90;
end;
theorem ThClosure120:
(A*)* = A*
proof
B:
(A*)* c= A* by ThClosure90;
A* c= (A*)* by ThClosure50;
hence thesis by B, XBOOLE_0:def 10;
end;
theorem
(A*) ^^ (A*) = A*
proof
A:
(A*) ^^ (A*) c= A* by ThClosure70;
<%>E in A* by ThClosure30;
then A* c= (A*) ^^ (A*) by ThConcat110;
hence thesis by A, XBOOLE_0:def 10;
end;
theorem
(A |^ n)* c= A*
proof
A |^ n c= A* by ThClosure40;
hence thesis by ThClosure90;
end;
theorem ThClosure135:
(A*) |^ n c= A*
proof
(A*) |^ n c= (A*)* by ThClosure40;
hence thesis by ThClosure120;
end;
theorem
n > 0 implies (A*) |^ n = A*
proof
<%>E in A* by ThClosure30;
then
A: n > 0 implies A* c= (A*) |^ n by ThPower120;
(A*) |^ n c= A* by ThClosure135;
hence thesis by A, XBOOLE_0:def 10;
end;
theorem ThClosure145:
A c= B* implies B* = (B \/ A)*
proof
assume
A: A c= B*;
defpred P[Nat] means (B \/ A) |^ $1 c= B*;
B:
P[0]
proof
B1: (B \/ A) |^ 0 = {<%>E} by ThPower20;
<%>E in B* by ThClosure30;
hence thesis by B1, ZFMISC_1:37;
end;
C:
now
let n;
assume
C0: P[n];
C1: (B \/ A) |^ (n + 1) = (B \/ A) |^ n ^^ (B \/ A) by ThPower10;
B c= B* by ThClosure50;
then B \/ A c= B* by XBOOLE_1:8, A;
hence P[n + 1] by C0, C1, ThClosure70;
end;
D:
for n holds P[n] from NAT_1:sch 2(B, C);
E:
(B \/ A)* c= B*
proof
let x;
assume x in (B \/ A)*;
then consider n such that
E1: x in (B \/ A) |^ n by ThClosure10;
(B \/ A) |^ n c= B* by D;
hence x in B* by E1;
end;
B c= B \/ A by XBOOLE_1:7;
then B* c= (B \/ A)* by ThClosure100;
hence thesis by E, XBOOLE_0:def 10;
end;
theorem ThClosure150:
a in A* implies A* = (A \/ {a})*
proof
assume a in A*;
then {a} c= A* by ZFMISC_1:37;
hence thesis by ThClosure145;
end;
theorem
A* = (A \ {<%>E})*
proof
B:
<%>E in A* by ThClosure30;
<%>E in (A \ {<%>E})* by ThClosure30;
hence (A \ {<%>E})* = ((A \ {<%>E}) \/ {<%>E})* by ThClosure150
.= (A \/ {<%>E})* by XBOOLE_1:39
.= A* by B, ThClosure150;
end;
theorem
(A*) \/ (B*) c= (A \/ B)*
proof
A c= A \/ B & B c= A \/ B by XBOOLE_1:7;
then A* c= (A \/ B)* & B* c= (A \/ B)* by ThClosure100;
hence thesis by XBOOLE_1:8;
end;
theorem
(A /\ B)* c= (A*) /\ (B*)
proof
A /\ B c= A & A /\ B c= B by XBOOLE_1:17;
then (A /\ B)* c= A* & (A /\ B)* c= B* by ThClosure100;
hence thesis by XBOOLE_1:19;
end;
theorem ThClosure180:
<%x%> in A* iff <%x%> in A
proof
thus <%x%> in A* implies <%x%> in A
proof
assume
A: <%x%> in A* & not <%x%> in A;
defpred P[Nat] means <%x%> in A |^ $1;
consider n such that
B1: P[n] by A, ThClosure10;
reconsider m = n as Element of NAT by ORDINAL1:def 13;
B2: ex i being Element of NAT st P[i]
proof
take m;
thus thesis by B1;
end;
ex n1 being Element of NAT st
P[n1] &
for n2 being Element of NAT st P[n2] holds n1 <= n2 from NAT_1:sch 5(B2);
then consider n1 being Element of NAT such that
C1: P[n1] and
C2: for n2 being Element of NAT st P[n2] holds n1 <= n2;
reconsider n1 as Nat;
D: now
assume n1 > 1;
then consider n2 such that
D1: n2 + 1 = n1 by NAT_1:6;
<%x%> in (A |^ n2) ^^ A by C1, D1, ThPower10;
then consider a, b such that
E: a in (A |^ n2) & b in A & <%x%> = a ^ b by DefConcat;
now
assume
G: (a = <%x%> & b = <%>E);
reconsider n2 as Element of NAT by ORDINAL1:def 13;
ex i being Element of NAT st P[i] & n1 > i
proof
take n2;
thus thesis by D1, E, G, NAT_1:13;
end;
hence contradiction by C2;
end;
hence <%x%> in A by E, LmSeq10;
end;
H: n1 = 1 implies <%x%> in A by C1, ThPower30;
now
assume n1 = 0;
then <%x%> in {<%>E} by C1, ThPower20;
then <%x%> = <%>E by TARSKI:def 1;
then { [0, x] } = {} by AFINSQ_1:35;
hence contradiction;
end;
hence contradiction by A, D, H, NAT_1:26;
end;
assume <%x%> in A;
then <%x%> in A |^ 1 by ThPower30;
hence thesis by ThClosure10;
end;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Lexemes as a Subset of E^omega
:: Definition of Lex
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E;
func Lex(E) -> Subset of E^omega means :DefAlphabet:
x in it iff ex e st e in E & x = <%e%>;
existence
proof
defpred P[set] means ex e st e in E & $1 = <%e%>;
consider C such that
A: x in C iff x in E^omega & P[x] from SUBSET_1:sch 1;
take C;
x in C iff ex e st e in E & x = <%e%>
proof
thus x in C implies ex e st e in E & x = <%e%> by A;
given e such that
B: e in E & x = <%e%>;
{e} c= E by B, ZFMISC_1:37;
then rng <%e%> c= E by AFINSQ_1:36;
then <%e%> is XFinSequence of E by ORDINAL1:def 8;
then <%e%> is Element of E^omega by AFINSQ_1:def 8;
hence thesis by A, B;
end;
hence thesis;
end;
uniqueness
proof
let C1, C2 be Subset of E^omega such that
A1: x in C1 iff ex e st e in E & x = <%e%> and
A2: x in C2 iff ex e st e in E & x = <%e%>;
now
let x;
thus x in C1 implies x in C2
proof
assume x in C1;
then ex e st e in E & x = <%e%> by A1;
hence x in C2 by A2;
end;
assume x in C2;
then ex e st e in E & x = <%e%> by A2;
hence x in C1 by A1;
end;
hence thesis by TARSKI:2;
end;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Lexemes as a Subset of E^omega
:: Properties of Lex
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem ThAlphabet10:
a in Lex(E) |^ len a
proof
defpred P[Nat] means
for a holds len a = $1 implies a in Lex(E) |^ $1;
A:
P[0]
proof
let a;
assume len a = 0;
then a = <%>E by AFINSQ_1:18;
then a in {<%>E} by TARSKI:def 1;
hence thesis by ThPower20;
end;
B:
now
let n;
assume
B1: P[n];
now
let b;
assume len b = n + 1;
then consider c, e such that
C1: len c = n & b = c ^ <%e%> by LmSeq40;
C3: c in Lex(E) |^ n by C1, B1;
<%e%> is Element of E^omega by C1, LmSeq20;
then e in E by LmSeq30;
then <%e%> in Lex(E) by DefAlphabet;
then <%e%> in Lex(E) |^ 1 by ThPower30;
hence b in Lex(E) |^ (n + 1) by C1, C3, ThPower160;
end;
hence P[n + 1];
end;
for n holds P[n] from NAT_1:sch 2(A, B);
hence thesis;
end;
theorem
Lex(E)* = E^omega
proof
A:
now
let x;
assume x in E^omega;
then reconsider a = x as Element of E^omega;
a in Lex(E) |^ len a by ThAlphabet10;
hence x in Lex(E)* by ThClosure10;
end;
B:
for x st x in Lex(E)* holds x in E^omega;
thus thesis by A, B, TARSKI:2;
end;
theorem
A* = E^omega implies Lex(E) c= A
proof
assume
A: A* = E^omega;
thus thesis
proof
let x;
assume
B1: x in Lex(E);
then consider e such that
B2: e in E & x = <%e%> by DefAlphabet;
thus x in A by B1, B2, A, ThClosure180;
end;
end;
Top
|
Mizar
