:: Formal Languages -- Concatenation and Closure
:: by Micha{\l} Trybulec
::
:: Received March 9, 2007
:: Copyright (c) 2007-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, AFINSQ_1, NAT_1, ORDINAL4, XBOOLE_0, TARSKI,
RELAT_1, FUNCT_1, ZFMISC_1, XXREAL_0, ARYTM_3, CARD_1, FINSEQ_1,
PRE_POLY, NEWTON, SETFAM_1, FLANG_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, FUNCT_1,
RELSET_1, FUNCT_2, SETFAM_1, XXREAL_0, NAT_1, AFINSQ_1, CATALAN2;
constructors XREAL_0, NAT_1, CATALAN2, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, XXREAL_0, XREAL_0, NAT_1,
AFINSQ_1, CATALAN2, FUNCT_1, FINSET_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
expansions TARSKI;
theorems AFINSQ_1, NAT_1, ORDINAL1, SUBSET_1, TARSKI, XBOOLE_0, XBOOLE_1,
XREAL_1, ZFMISC_1, XXREAL_0, FUNCT_2, RELAT_1;
schemes CARD_FIL, DOMAIN_1, NAT_1, RECDEF_1, SUBSET_1;
begin
reserve E, x, y, X 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; :: redefines ^ (AFINSQ_1, redefinition) → ^ (ORDINAL4, definition)
coherence by AFINSQ_1:def 7;
end;
definition
let E;
redefine func <%>E -> Element of E^omega; :: redefines <%> (AFINSQ_1, definition)
coherence by AFINSQ_1:def 7;
end;
definition
let E be non empty set;
let e be Element of E;
redefine func <%e%> -> Element of E^omega; :: redefines <% (AFINSQ_1, definition)
coherence by AFINSQ_1:def 7;
end;
definition
let E, a;
redefine func {a} -> Subset of E^omega; :: redefines { (TARSKI, definition)
coherence by SUBSET_1:33;
end;
definition
let E;
let f be sequence of bool E;
let n;
redefine func f.n -> Subset of E; :: redefines . (FUNCT_1, definition)
coherence
proof
n is Element of NAT by ORDINAL1:def 12;
then f.n in rng f by FUNCT_2:112;
hence thesis;
end;
end;
:: Preliminaries - Numbers:
theorem Th1:
n1 > n or n2 > n implies n1 + n2 > n
proof
A1: n1 > n & n2 >= 0 implies n1 + n2 > n + 0 by XREAL_1:8;
A2: n1 >= 0 & n2 > n implies n1 + n2 > n + 0 by XREAL_1:8;
assume n1 > n or n2 > n;
hence thesis by A1,A2;
end;
theorem Th2:
n1 + n <= n2 + 1 & n > 0 implies n1 <= n2
proof
assume that
A1: n1 + n <= n2 + 1 and
A2: n > 0;
1 + 0 <= n by A2,NAT_1:13;
hence thesis by A1,XREAL_1:8;
end;
theorem Th3:
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
A1: n1 + n2 = 1;
now
A2: n1 = 0 & n2 = 0 implies contradiction by A1;
assume
A3: n1 <= 1 & n2 <= 1;
n1 = 1 & n2 = 1 implies contradiction by A1;
hence thesis by A3,A2,NAT_1:25;
end;
hence thesis by A1,Th1;
end;
thus thesis;
end;
:: Preliminaries - Sequences:
theorem Th4:
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
A1: a ^ b = <%x%>;
then len (a ^ b) = 1 by AFINSQ_1:34;
then len a + len b = 1 by AFINSQ_1:17;
then len a = 1 & b = <%>E or a = <%>E & len b = 1 by Th3;
hence thesis by A1;
end;
assume a = <%>E & b = <%x%> or b = <%>E & a = <%x%>;
hence thesis;
end;
theorem Th5:
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:31;
hence thesis by AFINSQ_1:def 7;
end;
theorem Th6:
for x being object holds <%x%> is Element of E^omega implies x in E
proof let x be object;
assume <%x%> is Element of E^omega;
then rng <%x%> c= E by RELAT_1:def 19;
then {x} c= E by AFINSQ_1:33;
hence thesis by ZFMISC_1:31;
end;
theorem Th7:
len b = n + 1 implies ex c, e st len c = n & b = c ^ <%e%>
proof
assume
A1: len b = n + 1;
then b <> {};
then consider c9 being XFinSequence, x being object such that
A2: b = c9 ^ <%x%> by AFINSQ_1:40;
<%x%> is Element of E^omega by A2,Th5;
then reconsider e = x as Element of E by Th6;
reconsider c = c9 as Element of E^omega by A2,Th5;
take c, e;
n + 1 = len c + len <%x%> by A1,A2,AFINSQ_1:17
.= len c + 1 by AFINSQ_1:34;
hence thesis by A2;
end;
theorem Th8:
for p being XFinSequence st p <> {}
ex q being XFinSequence, x being object st p = <%x%> ^ q
proof
let p be XFinSequence;
defpred P[Nat] means for p being XFinSequence st len p = $1 & p <> {} ex q
being XFinSequence, x being object st p = <%x%> ^ q;
A1: now
let n;
assume
A2: P[n];
thus P[n + 1]
proof
let p be XFinSequence such that
A3: len p = n + 1 and
A4: p <> {};
consider q being XFinSequence, x being object such that
A5: p = q ^ <%x%> by A4,AFINSQ_1:40;
A6: n + 1 = len q + len <%x%> by A3,A5,AFINSQ_1:17
.= len q + 1 by AFINSQ_1:34;
per cases;
suppose
q = {};
then p = {}^<%x%> by A5
.= <%x%> ^ {};
hence thesis;
end;
suppose
q <> {};
then consider r being XFinSequence, y being object such that
A7: q = <%y%> ^ r by A2,A6;
p = <%y%> ^ (r ^ <%x%>) by A5,A7,AFINSQ_1:27;
hence thesis;
end;
end;
end;
A8: P[0];
A9: for n holds P[n] from NAT_1:sch 2(A8, A1);
A10: len p = len p;
assume p <> {};
hence thesis by A9,A10;
end;
theorem
len b = n + 1 implies ex c, e st len c = n & b = <%e%> ^ c
proof
assume
A1: len b = n + 1;
then b <> {};
then consider c9 being XFinSequence, x being object such that
A2: b = <%x%> ^ c9 by Th8;
<%x%> is Element of E^omega by A2,Th5;
then reconsider e = x as Element of E by Th6;
reconsider c = c9 as Element of E^omega by A2,Th5;
take c, e;
n + 1 = len c + len <%x%> by A1,A2,AFINSQ_1:17
.= len c + 1 by AFINSQ_1:34;
hence thesis by A2;
end;
Lm1:
for p being XFinSequence st len p = i + j ex q1, q2 being
XFinSequence st len q1 = i & len q2 = j & p = q1 ^ q2 by AFINSQ_1:61;
theorem
len b = n + m implies ex c1, c2 st len c1 = n & len c2 = m & b = c1 ^ c2
proof
assume len b = n + m;
then consider c19, c29 being XFinSequence such that
A1: len c19 = n & len c29 = m and
A2: b = c19 ^ c29 by Lm1;
reconsider c2 = c29 as Element of E^omega by A2,Th5;
reconsider c1 = c19 as Element of E^omega by A2,Th5;
take c1, c2;
thus thesis by A1,A2;
end;
theorem Th11:
a ^ a = a implies a = {}
proof
assume a ^ a = a;
then len a + len a = len a by AFINSQ_1:17;
hence thesis;
end;
begin
:: Concatenation of Languages
:: Definition of ^^
definition
let E, A, B;
func A ^^ B -> Subset of E^omega means
:Def1:
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
A1: x in C iff x in E^omega & P[x] from SUBSET_1:sch 1;
take C;
thus thesis by A1;
end;
uniqueness
proof
let C1, C2 be Subset of E^omega such that
A2: x in C1 iff ex a, b st a in A & b in B & x = a ^ b and
A3: x in C2 iff ex a, b st a in A & b in B & x = a ^ b;
now
let x be object;
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 A2;
hence thesis by A3;
end;
assume x in C2;
then ex a, b st a in A & b in B & x = a ^ b by A3;
hence x in C1 by A2;
end;
hence thesis by TARSKI:2;
end;
end;
:: Concatenation of Languages
:: Properties of ^^
theorem Th12:
A ^^ B = {} iff A = {} or B = {}
proof
thus A ^^ B = {} implies A = {} or B = {}
proof
assume that
A1: A ^^ B = {} and
A2: A <> {} and
A3: B <> {};
consider a such that
A4: a in A by A2,SUBSET_1:4;
consider b such that
A5: b in B by A3,SUBSET_1:4;
a ^ b in A ^^ B by A4,A5,Def1;
hence contradiction by A1;
end;
assume
A6: A = {} or B = {};
not ex x being object st x in A ^^ B
proof
given x being object such that
A7: x in A ^^ B;
ex a, b st a in A & b in B & x = a ^ b by A7,Def1;
hence contradiction by A6;
end;
hence thesis by XBOOLE_0:def 1;
end;
theorem Th13:
A ^^ {<%>E} = A & {<%>E} ^^ A = A
proof
A1: for x being object holds x in A ^^ {<%>E} implies x in A
proof let x be object;
assume x in A ^^ {<%>E};
then consider a, d such that
A2: a in A and
A3: d in {<%>E} & x = a ^ d by Def1;
x = a ^ {} by A3,TARSKI:def 1;
hence thesis by A2;
end;
A4: for x being object holds x in A implies x in {<%>E} ^^ A
proof let x be object;
assume
A5: x in A;
ex d, a st d in {<%>E} & a in A & x = d ^ a
proof
reconsider a = x as Element of E^omega by A5;
consider d such that
A6: d = <%>E;
take d, a;
thus thesis by A5,A6,TARSKI:def 1;
end;
hence thesis by Def1;
end;
A7: for x being object holds x in A implies x in A ^^ {<%>E}
proof let x be object;
assume
A8: x in A;
ex a, d st a in A & d in {<%>E} & x = a ^ d
proof
reconsider a = x as Element of E^omega by A8;
set d = <%>E;
take a, d;
thus thesis by A8,TARSKI:def 1;
end;
hence thesis by Def1;
end;
for x being object holds x in {<%>E} ^^ A implies x in A
proof let x be object;
assume x in {<%>E} ^^ A;
then consider d, a such that
A9: d in {<%>E} and
A10: a in A and
A11: x = d ^ a by Def1;
x = {} ^ a by A9,A11,TARSKI:def 1;
hence thesis by A10;
end;
hence thesis by A1,A4,A7,TARSKI:2;
end;
theorem Th14:
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 and
A4: b in B and
<%>E = a ^ b by Def1;
A5: now
let x;
assume that
A6: x in A or x in B and
A7: x <> <%>E;
A8: now
assume
A9: x in B;
then reconsider xb = x as Element of E^omega;
A10: a ^ xb <> <%>E by A7,AFINSQ_1:30;
a ^ xb in A ^^ B by A3,A9,Def1;
hence contradiction by A1,A10,TARSKI:def 1;
end;
now
assume
A11: x in A;
then reconsider xa = x as Element of E^omega;
A12: xa ^ b <> <%>E by A7,AFINSQ_1:30;
xa ^ b in A ^^ B by A4,A11,Def1;
hence contradiction by A1,A12,TARSKI:def 1;
end;
hence contradiction by A6,A8;
end;
then
A13: for x being object holds x in B iff x = <%>E by A4;
for x being object holds x in A iff x = <%>E by A3,A5;
hence contradiction by A2,A13,TARSKI:def 1;
end;
assume A = {<%>E} & B = {<%>E};
hence thesis by Th13;
end;
theorem Th15:
<%>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 ex a, b st a in A & b in B & a ^ b = <%>E by Def1;
hence thesis by AFINSQ_1:30;
end;
assume <%>E in A & <%>E in B;
then {} ^ <%>E in A ^^ B by Def1;
hence thesis;
end;
theorem Th16:
<%>E in B implies A c= A ^^ B & A c= B ^^ A
proof
assume
A1: <%>E in B;
thus A c= A ^^ B
proof
let x be object;
assume
A2: x in A;
then reconsider xa = x as Element of E^omega;
xa ^ {} in A ^^ B by A1,A2,Def1;
hence thesis;
end;
thus A c= B ^^ A
proof
let x be object;
assume
A3: x in A;
then reconsider xa = x as Element of E^omega;
{} ^ xa in B ^^ A by A1,A3,Def1;
hence thesis;
end;
end;
theorem Th17:
A c= C & B c= D implies A ^^ B c= C ^^ D
proof
assume
A1: A c= C & B c= D;
thus thesis
proof
let x be object;
assume x in A ^^ B;
then ex a, b st a in A & b in B & x = a ^ b by Def1;
hence thesis by A1,Def1;
end;
end;
theorem Th18:
(A ^^ B) ^^ C = A ^^ (B ^^ C)
proof
now
let x be object;
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) and
A2: c in C & x = ab ^ c by Def1;
consider a, b such that
A3: a in A and
A4: b in B & ab = a ^ b by A1,Def1;
x = a ^ (b ^ c) & b ^ c in B ^^ C by A2,A4,Def1,AFINSQ_1:27;
hence thesis by A3,Def1;
end;
assume x in A ^^ (B ^^ C);
then consider a, bc such that
A5: a in A and
A6: bc in (B ^^ C) and
A7: x = a ^ bc by Def1;
consider b, c such that
A8: b in B and
A9: c in C and
A10: bc = b ^ c by A6,Def1;
x = (a ^ b) ^ c & a ^ b in A ^^ B by A5,A7,A8,A10,Def1,AFINSQ_1:27;
hence x in (A ^^ B) ^^ C by A9,Def1;
end;
hence thesis by TARSKI:2;
end;
theorem Th19:
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 be object;
assume x in A ^^ (B /\ C);
then consider a, bc such that
A1: a in A and
A2: bc in B /\ C and
A3: x = a ^ bc by Def1;
bc in C by A2,XBOOLE_0:def 4;
then
A4: x in A ^^ C by A1,A3,Def1;
bc in B by A2,XBOOLE_0:def 4;
then x in A ^^ B by A1,A3,Def1;
hence thesis by A4,XBOOLE_0:def 4;
end;
thus (B /\ C) ^^ A c= (B ^^ A) /\ (C ^^ A)
proof
let x be object;
assume x in (B /\ C) ^^ A;
then consider bc, a such that
A5: bc in B /\ C and
A6: a in A & x = bc ^ a by Def1;
bc in C by A5,XBOOLE_0:def 4;
then
A7: x in C ^^ A by A6,Def1;
bc in B by A5,XBOOLE_0:def 4;
then x in B ^^ A by A6,Def1;
hence thesis by A7,XBOOLE_0:def 4;
end;
end;
theorem Th20:
A ^^ B \/ A ^^ C = A ^^ (B \/ C) & B ^^ A \/ C ^^ A = (B \/ C) ^^ A
proof
A1: A ^^ (B \/ C) c= (A ^^ B) \/ (A ^^ C)
proof
let x be object;
assume x in A ^^ (B \/ C);
then consider a, bc such that
A2: a in A and
A3: bc in B \/ C and
A4: x = a ^ bc by Def1;
bc in B or bc in C by A3,XBOOLE_0:def 3;
then x in A ^^ B or x in A ^^ C by A2,A4,Def1;
hence thesis by XBOOLE_0:def 3;
end;
A5: (B \/ C) ^^ A c= (B ^^ A) \/ (C ^^ A)
proof
let x be object;
assume x in (B \/ C) ^^ A;
then consider bc, a such that
A6: bc in B \/ C and
A7: a in A & x = bc ^ a by Def1;
bc in B or bc in C by A6,XBOOLE_0:def 3;
then x in B ^^ A or x in C ^^ A by A7,Def1;
hence thesis by XBOOLE_0:def 3;
end;
C c= B \/ C by XBOOLE_1:7;
then
A8: C ^^ A c= (B \/ C) ^^ A by Th17;
B c= B \/ C by XBOOLE_1:7;
then B ^^ A c= (B \/ C) ^^ A by Th17;
then
A9: (B ^^ A) \/ (C ^^ A) c= (B \/ C) ^^ A by A8,XBOOLE_1:8;
C c= B \/ C by XBOOLE_1:7;
then
A10: A ^^ C c= A ^^ (B \/ C) by Th17;
B c= B \/ C by XBOOLE_1:7;
then A ^^ B c= A ^^ (B \/ C) by Th17;
then (A ^^ B) \/ (A ^^ C) c= A ^^ (B \/ C) by A10,XBOOLE_1:8;
hence thesis by A1,A5,A9,XBOOLE_0:def 10;
end;
theorem Th21:
(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 be object;
assume
A1: x in (A ^^ B) \ (A ^^ C);
then x in A ^^ B by XBOOLE_0:def 5;
then consider a, b such that
A2: a in A and
A3: b in B and
A4: x = a ^ b by Def1;
A5: now
assume not b in C;
then b in B \ C by A3,XBOOLE_0:def 5;
hence thesis by A2,A4,Def1;
end;
not x in A ^^ C by A1,XBOOLE_0:def 5;
hence thesis by A2,A4,A5,Def1;
end;
thus (B ^^ A) \ (C ^^ A) c= (B \ C) ^^ A
proof
let x be object;
assume
A6: x in (B ^^ A) \ (C ^^ A);
then x in B ^^ A by XBOOLE_0:def 5;
then consider b, a such that
A7: b in B and
A8: a in A & x = b ^ a by Def1;
A9: now
assume not b in C;
then b in B \ C by A7,XBOOLE_0:def 5;
hence thesis by A8,Def1;
end;
not x in C ^^ A by A6,XBOOLE_0:def 5;
hence thesis by A8,A9,Def1;
end;
end;
theorem
(A ^^ B) \+\ (A ^^ C) c= A ^^ (B \+\ C) & (B ^^ A) \+\ (C ^^ A) c= (B
\+\ C) ^^ A
proof
(A ^^ B) \+\ (A ^^ C) = ((A ^^ B) \/ (A ^^ C)) \ ((A ^^ B) /\ (A ^^ C))
by XBOOLE_1:101
.= (A ^^ (B \/ C)) \ ((A ^^ B) /\ (A ^^ C)) by Th20;
then
A1: (A ^^ B) \+\ (A ^^ C) c= (A ^^ (B \/ C)) \ (A ^^ (B /\ C)) by Th19,
XBOOLE_1:34;
(B ^^ A) \+\ (C ^^ A) = ((B ^^ A) \/ (C ^^ A)) \ ((B ^^ A) /\ (C ^^ A))
by XBOOLE_1:101
.= ((B \/ C) ^^ A) \ ((B ^^ A) /\ (C ^^ A)) by Th20;
then
A2: (B ^^ A) \+\ (C ^^ A) c= ((B \/ C) ^^ A) \ ((B /\ C) ^^ A) by Th19,
XBOOLE_1:34;
((B \/ C) ^^ A) \ ((B /\ C) ^^ A) c= ((B \/ C) \ (B /\ C)) ^^ A by Th21;
then
A3: (B ^^ A) \+\ (C ^^ A) c= ((B \/ C) \ (B /\ C)) ^^ A by A2;
(A ^^ (B \/ C)) \ (A ^^ (B /\ C)) c= A ^^ ((B \/ C) \ (B /\ C)) by Th21;
then (A ^^ B) \+\ (A ^^ C) c= A ^^ ((B \/ C) \ (B /\ C)) by A1;
hence thesis by A3,XBOOLE_1:101;
end;
begin
:: Concatenation of a Language with Itself
:: Definition of |^
definition
let E, A, n;
func A |^ n -> Subset of E^omega means
:Def2:
ex concat being sequence of
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;
A1: for i being 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 Nat;
let x be Element of bool (E^omega);
take x ^^ A;
thus thesis;
end;
consider f being sequence of bool (E^omega) such that
A2: f.0 = {<%>E} & for i being Nat holds P[i, f.i, f.(i + 1
)] from RECDEF_1:sch 2(A1);
consider C being Subset of E^omega such that
A3: C = f.n;
take C;
now
let i;
reconsider j = i as Element of NAT by ORDINAL1:def 12;
ex B, C st C = f.(j + 1) & B = f.j & C = B ^^ A by A2;
hence f.(i + 1) = f.i ^^ A;
end;
hence thesis by A2,A3;
end;
uniqueness
proof
let C1, C2 be Subset of E^omega;
given f1 being sequence of bool (E^omega) such that
A4: C1 = f1.n and
A5: f1.0 = {<%>E} and
A6: for i holds f1.(i + 1) = f1.i ^^ A;
given f2 being sequence of bool (E^omega) such that
A7: C2 = f2.n and
A8: f2.0 = {<%>E} and
A9: for i holds f2.(i + 1) = f2.i ^^ A;
defpred P[Nat] means f1.$1 = f2.$1;
A10: now
let k;
assume
A11: P[k];
f2.(k + 1) = f2.k ^^ A by A9;
hence P[k + 1] by A6,A11;
end;
A12: P[0] by A5,A8;
for k holds P[k] from NAT_1:sch 2(A12, A10);
hence thesis by A4,A7;
end;
end;
:: Concatenation of a Language with Itself
:: Properties of |^
theorem Th23:
A |^ (n + 1) = (A |^ n) ^^ A
proof
consider concat being sequence of bool (E^omega) such that
A1: A |^ n = concat.n and
A2: concat.0 = {<%>E} and
A3: for i holds concat.(i + 1) = concat.i ^^ A by Def2;
concat.(n + 1) = (A |^ n) ^^ A by A1,A3;
hence thesis by A2,A3,Def2;
end;
theorem Th24:
A |^ 0 = {<%>E}
proof
ex concat being sequence of bool (E^omega) st A |^ 0 = concat.0 &
concat.0 = {<%>E} & for i holds concat.(i + 1) = concat.i ^^ A by Def2;
hence thesis;
end;
theorem Th25:
A |^ 1 = A
proof
consider concat being sequence of bool (E^omega) such that
A1: A |^ 1 = concat.1 and
A2: concat.0 = {<%>E} & for i holds concat.(i + 1) = concat.i ^^ A by Def2;
thus A |^ 1 = concat.(0 + 1) by A1
.= {<%>E} ^^ A by A2
.= A by Th13;
end;
theorem Th26:
A |^ 2 = A ^^ A
proof
thus A |^ 2 = A |^ (1 + 1) .= (A |^ 1) ^^ A by Th23
.= A ^^ A by Th25;
end;
theorem Th27:
A |^ n = {} iff n > 0 & A = {}
proof
defpred P[Nat] means A |^ $1 = {};
thus A |^ n = {} implies n > 0 & A = {}
proof
assume that
A1: A |^ n = {} and
A2: n <= 0 or A <> {};
A3: now
defpred P[Nat] means A |^ $1 <> {};
assume
A4: A <> {};
A5: now
let n;
assume P[n];
then consider a1 such that
A6: a1 in A |^ n by SUBSET_1:4;
consider a2 such that
A7: a2 in A by A4,SUBSET_1:4;
a1 ^ a2 in A |^ n ^^ A by A6,A7,Def1;
hence P[n + 1] by Th23;
end;
A |^ 0 = {<%>E} by Th24;
then
A8: P[0];
for n holds P[n] from NAT_1:sch 2(A8, A5);
hence contradiction by A1;
end;
now
assume n <= 0;
then n = 0;
then A |^ n = {<%>E} by Th24;
hence contradiction by A1;
end;
hence thesis by A2,A3;
end;
assume that
A9: n > 0 and
A10: A = {};
A11: now
let m be Nat;
assume that
1 <= m and
P[m];
{}(E^omega) |^ (m + 1) = {}(E^omega) |^ m ^^ {}(E^omega) by Th23
.= {} by Th12;
hence P[m + 1] by A10;
end;
A12: P[1] by A10,Th25;
A13: for m being Nat st m >= 1 holds P[m] from NAT_1:sch 8(A12, A11);
n >= 0 + 1 by A9,NAT_1:13;
hence thesis by A13;
end;
theorem Th28:
{<%>E} |^ n = {<%>E}
proof
defpred P[Nat] means {<%>E} |^ $1 = {<%>E};
A1: now
let n;
assume
A2: P[n];
{<%>E} |^ (n + 1) = ({<%>E} |^ n) ^^ {<%>E} by Th23
.= {<%>E} by A2,Th13;
hence P[n + 1];
end;
A3: P[0] by Th24;
for n holds P[n] from NAT_1:sch 2(A3, A1);
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
A1: A |^ n = {<%>E};
now
assume n > 0;
then consider m such that
A2: m + 1 = n by NAT_1:6;
A |^ n = (A |^ m) ^^ A by A2,Th23;
hence A = {<%>E} by A1,Th14;
end;
hence thesis;
end;
assume n = 0 or A = {<%>E};
hence thesis by Th24,Th28;
end;
theorem Th30:
<%>E in A implies <%>E in A |^ n
proof
defpred P[Nat] means <%>E in A |^ $1;
assume
A1: <%>E in A;
A2: now
let n;
assume P[n];
then <%>E in (A |^ n) ^^ A by A1,Th15;
hence P[n + 1] by Th23;
end;
A |^ 0 = {<%>E} by Th24;
then
A3: P[0] by TARSKI:def 1;
for n holds P[n] from NAT_1:sch 2(A3, A2);
hence thesis;
end;
theorem
<%>E in A |^ n & n > 0 implies <%>E in A
proof
assume that
A1: <%>E in A |^ n and
A2: n > 0;
consider m such that
A3: m + 1 = n by A2,NAT_1:6;
A |^ n = (A |^ m) ^^ A by A3,Th23;
then ex a1, a2 st a1 in A |^ m & a2 in A & a1 ^ a2 = <%>E by A1,Def1;
hence thesis by AFINSQ_1:30;
end;
theorem Th32:
(A |^ n) ^^ A = A ^^ (A |^ n)
proof
defpred P[Nat] means (A |^ $1) ^^ A = A ^^ (A |^ $1);
A1: now
let n;
assume
A2: P[n];
(A |^ (n + 1)) ^^ A = ((A |^ n) ^^ A) ^^ A by Th23
.= A ^^ ((A |^ n) ^^ A) by A2,Th18
.= A ^^ (A |^ (n + 1)) by Th23;
hence P[n + 1];
end;
(A |^ 0) ^^ A = {<%>E} ^^ A by Th24
.= A by Th13
.= A ^^ {<%>E} by Th13
.= A ^^ (A |^ 0) by Th24;
then
A3: P[0];
for n holds P[n] from NAT_1:sch 2(A3, A1);
hence thesis;
end;
theorem Th33:
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);
A1: now
let l;
assume
A2: P[l];
now
let m, n be Nat;
A3: now
assume m + n < l + 1;
then m + n <= l by NAT_1:13;
hence A |^ (m + n) = (A |^ m) ^^ (A |^ n) by A2;
end;
A4: now
assume
A5: m + n = l + 1;
A6: now
assume
A7: n = 0;
thus A |^ (m + n) = (A |^ (l + 1)) ^^ {<%>E} by A5,Th13
.= (A |^ m) ^^ (A |^ n) by A5,A7,Th24;
end;
A8: now
assume that
A9: m > 0 and
A10: n > 0;
consider k such that
A11: k + 1 = m by A9,NAT_1:6;
A |^ (m + n) = A |^ (k + n + 1) by A11
.= (A |^ (k + n)) ^^ A by Th23
.= A ^^ (A |^ (k + n)) by Th32
.= A ^^ ((A |^ k) ^^ (A |^ n)) by A2,A5,A11
.= (A ^^ (A |^ k)) ^^ (A |^ n) by Th18
.= ((A |^ k) ^^ A) ^^ (A |^ n) by Th32
.= ((A |^ k) ^^ (A |^ 1)) ^^ (A |^ n) by Th25
.= (A |^ m) ^^ (A |^ n) by A2,A5,A10,A11,Th2;
hence A |^ (m + n) = (A |^ m) ^^ (A |^ n);
end;
now
assume
A12: m = 0;
thus A |^ (m + n) = {<%>E} ^^ (A |^ (l + 1)) by A5,Th13
.= (A |^ m) ^^ (A |^ n) by A5,A12,Th24;
end;
hence A |^ (m + n) = (A |^ m) ^^ (A |^ n) by A6,A8;
end;
assume m + n <= l + 1;
hence A |^ (m + n) = (A |^ m) ^^ (A |^ n) by A4,A3,XXREAL_0:1;
end;
hence P[l + 1];
end;
A13: P[0]
proof
let m, n;
assume
A14: m + n <= 0;
then
A15: m = 0;
A16: m + n = 0 by A14;
hence A |^ (m + n) = (A |^ 0) ^^ {<%>E} by Th13
.= (A |^ m) ^^ (A |^ n) by A16,A15,Th24;
end;
for l holds P[l] from NAT_1:sch 2(A13, A1);
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);
A1: now
let l;
assume
A2: P[l];
now
let m, n;
A3: now
assume m + n < l + 1;
then m + n <= l by NAT_1:13;
hence (A |^ m) |^ n = A |^ (m * n) by A2;
end;
A4: now
assume
A5: m + n = l + 1;
A6: now
assume that
m > 0 and
A7: n > 0;
consider k such that
A8: k + 1 = n by A7,NAT_1:6;
A9: m + k <= l by A5,A8;
(A |^ m) |^ n = ((A |^ m) |^ k) ^^ (A |^ m) by A8,Th23
.= (A |^ (m * k)) ^^ (A |^ m) by A2,A9
.= A |^ (m * k + m) by Th33
.= A |^ (m * n) by A8;
hence (A |^ m) |^ n = A |^ (m * n);
end;
A10: now
assume
A11: n = 0;
hence (A |^ m) |^ n = {<%>E} by Th24
.= A |^ (m * n) by A11,Th24;
end;
now
assume
A12: m = 0;
hence (A |^ m) |^ n = {<%>E} |^ n by Th24
.= {<%>E} by Th28
.= A |^ (m * n) by A12,Th24;
end;
hence (A |^ m) |^ n = A |^ (m * n) by A10,A6;
end;
assume m + n <= l + 1;
hence (A |^ m) |^ n = A |^ (m * n) by A4,A3,XXREAL_0:1;
end;
hence P[l + 1];
end;
A13: P[0]
proof
let m, n;
assume
A14: m + n <= 0;
then
A15: m = 0;
n = 0 by A14;
hence (A |^ m) |^ n = {<%>E} by Th24
.= A |^ (m * n) by A15,Th24;
end;
A16: for l holds P[l] from NAT_1:sch 2(A13, A1);
now
let m, n;
reconsider l = m + n as Nat;
m + n <= l;
hence (A |^ m) |^ n = A |^ (m * n) by A16;
end;
hence thesis;
end;
theorem Th35:
<%>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
A3: m + 1 = n by A2,NAT_1:6;
<%>E in A |^ m by A1,Th30;
then A c= A |^ m ^^ A by Th16;
hence thesis by A3,Th23;
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
A3: n + k = m by A2,NAT_1:10;
<%>E in A |^ k by A1,Th30;
then A |^ n c= A |^ k ^^ A |^ n by Th16;
hence thesis by A3,Th33;
end;
theorem Th37:
A c= B implies A |^ n c= B |^ n
proof
defpred P[Nat] means A |^ $1 c= B |^ $1;
assume
A1: A c= B;
A2: now
let n;
assume
A3: P[n];
(A |^ n) ^^ A = A |^ (n + 1) & (B |^ n) ^^ B = B |^ (n + 1) by Th23;
hence P[n + 1] by A1,A3,Th17;
end;
A |^ 0 = {<%>E} by Th24;
then
A4: P[0] by Th24;
for n holds P[n] from NAT_1:sch 2(A4, A2);
hence thesis;
end;
theorem
(A |^ n) \/ (B |^ n) c= (A \/ B) |^ n
proof
A |^ n c= (A \/ B) |^ n & B |^ n c= (A \/ B) |^ n by Th37,XBOOLE_1:7;
hence thesis by XBOOLE_1:8;
end;
theorem
(A /\ B) |^ n c= (A |^ n) /\ (B |^ n)
proof
(A /\ B) |^ n c= A |^ n & (A /\ B) |^ n c= B |^ n by Th37,XBOOLE_1:17;
hence thesis by XBOOLE_1:19;
end;
theorem Th40:
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 Def1;
hence thesis by Th33;
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 Th41:
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
defpred P[set] means ex k st $1 = A |^ k;
assume x in A*;
then consider X such that
A1: x in X and
A2: X in { B : ex k st B = A |^ k } by TARSKI:def 4;
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
A4: x in A |^ n;
defpred P[set] means ex k st $1 = A |^ k;
consider B such that
A5: x in B and
A6: P[B] by A4;
reconsider A = { C : P[C] } as Subset-Family of E^omega from DOMAIN_1:sch 7;
B in A by A6;
hence thesis by A5,TARSKI:def 4;
end;
theorem Th42:
A |^ n c= A*
proof
(A |^ n) in { B : ex k st B = A |^ k };
hence thesis by ZFMISC_1:74;
end;
theorem Th43:
A c= A*
proof
A = A |^ 1 by Th25;
hence thesis by Th42;
end;
theorem
A ^^ A c= A*
proof
A ^^ A = A |^ 2 by Th26;
hence thesis by Th42;
end;
theorem Th45:
a in C* & b in C* implies a ^ b in C*
proof
assume that
A1: a in C* and
A2: b in C*;
consider k such that
A3: a in C |^ k by A1,Th41;
consider l such that
A4: b in C |^ l by A2,Th41;
a ^ b in C |^ (k + l) by A3,A4,Th40;
hence thesis by Th41;
end;
theorem Th46:
A c= C* & B c= C* implies A ^^ B c= C*
proof
assume
A1: A c= C* & B c= C*;
thus thesis
proof
let x be object;
assume x in A ^^ B;
then ex a, b st a in A & b in B & x = a ^ b by Def1;
hence thesis by A1,Th45;
end;
end;
theorem
A* = {<%>E} iff A = {} or A = {<%>E}
proof
thus A* = {<%>E} implies A = {} or A = {<%>E}
proof
A1: A c= A* by Th43;
assume that
A2: A* = {<%>E} and
A3: A <> {} & A <> {<%>E};
ex x being object st x in A & x <> <%>E by A3,ZFMISC_1:35;
hence contradiction by A2,A1,TARSKI:def 1;
end;
A4: now
assume
A5: A = {};
A6: now
let x be object;
assume x in A*;
then consider n such that
A7: x in A |^ n by Th41;
n = 0 implies x in {<%>E} by A7,Th24;
hence x in {<%>E} by A5,A7,Th27;
end;
now
let x be object;
assume x in {<%>E};
then x in A |^ 0 by Th24;
hence x in A* by Th41;
end;
hence A* = {<%>E} by A6,TARSKI:2;
end;
now
assume
A8: A = {<%>E};
A9: A* c= {<%>E}
proof
let x be object;
assume x in A*;
then ex n st x in A |^ n by Th41;
hence thesis by A8,Th28;
end;
{<%>E} c= A*
proof
let x be object;
assume x in {<%>E};
then x in A |^ 0 by Th24;
hence thesis by Th41;
end;
hence A* = {<%>E} by A9,XBOOLE_0:def 10;
end;
hence thesis by A4;
end;
theorem Th48:
<%>E in A*
proof
{<%>E} = A |^ 0 by Th24;
then <%>E in A |^ 0 by TARSKI:def 1;
hence thesis by Th41;
end;
theorem
A* = {x} implies x = <%>E
proof
assume that
A1: A* = {x} and
A2: x <> <%>E;
reconsider a = x as Element of E^omega by A1,ZFMISC_1:31;
x in A* by A1,ZFMISC_1:31;
then
A3: a ^ a in A* by Th45;
a ^ a <> x by A2,Th11;
hence thesis by A1,A3,TARSKI:def 1;
end;
theorem Th50:
x in A |^ (m + 1) implies x in (A*) ^^ A & x in A ^^ (A*)
proof
assume x in A |^ (m + 1);
then
A1: x in (A |^ m) ^^ A by Th23;
then consider a, b such that
A2: a in A |^ m and
A3: b in A & x = a ^ b by Def1;
a in A* by A2,Th41;
hence x in (A*) ^^ A by A3,Def1;
x in A ^^ (A |^ m) by A1,Th32;
then consider a, b such that
A4: a in A and
A5: b in A |^ m and
A6: x = a ^ b by Def1;
b in A* by A5,Th41;
hence thesis by A4,A6,Def1;
end;
theorem
A |^ (m + 1) c= (A*) ^^ A & A |^ (m + 1) c= A ^^ (A*)
by Th50;
theorem Th52:
x in (A*) ^^ A or x in A ^^ (A*) implies x in A*
proof
A1: now
let x;
assume x in A ^^ (A*);
then consider a, b such that
A2: a in A and
A3: b in A* and
A4: x = a ^ b by Def1;
consider n such that
A5: b in A |^ n by A3,Th41;
a in A |^ 1 by A2,Th25;
then a ^ b in A |^ (n + 1) by A5,Th40;
hence x in A* by A4,Th41;
end;
now
let x;
assume x in (A*) ^^ A;
then consider a, b such that
A6: a in A* and
A7: b in A and
A8: x = a ^ b by Def1;
consider n such that
A9: a in A |^ n by A6,Th41;
b in A |^ 1 by A7,Th25;
then a ^ b in A |^ (n + 1) by A9,Th40;
hence x in A* by A8,Th41;
end;
hence thesis by A1;
end;
theorem
(A*) ^^ A c= A* & A ^^ (A*) c= A*
by Th52;
theorem Th54:
<%>E in A implies A* = (A*) ^^ A & A* = A ^^ (A*)
proof
assume
A1: <%>E in A;
A2: <%>E in A* by Th48;
A3: now
let x;
assume x in A*;
then consider n such that
A4: x in A |^ n by Th41;
A5: now
assume n = 0;
then x in {<%>E} by A4,Th24;
then x = <%>E by TARSKI:def 1;
hence x in (A*) ^^ A & x in A ^^ (A*) by A1,A2,Th15;
end;
A6: now
assume n > 0;
then ex m st m + 1 = n by NAT_1:6;
hence x in A ^^ (A*) by A4,Th50;
end;
now
assume n > 0;
then ex m st m + 1 = n by NAT_1:6;
hence x in (A*) ^^ A by A4,Th50;
end;
hence x in (A*) ^^ A & x in A ^^ (A*) by A5,A6;
end;
then
A7: for x being object holds x in A* implies x in (A*) ^^ A;
A8: for x being object holds x in A* implies x in A ^^ (A*) by A3;
for x being object
holds (x in (A*) ^^ A implies x in A*) & (x in A ^^ (A*) implies x
in A*) by Th52;
hence thesis by A7,A8,TARSKI:2;
end;
theorem
<%>E in A implies A* = (A*) ^^ (A |^ n) & A* = (A |^ n) ^^ (A*)
proof
defpred P[Nat] means A* = (A*) ^^ (A |^ $1) & A* = (A |^ $1) ^^ (A*);
A1: (A |^ 0) ^^ (A*) = {<%>E} ^^ (A*) by Th24
.= A* by Th13;
assume
A2: <%>E in A;
A3: now
let n;
assume
A4: P[n];
A5: (A*) ^^ (A |^ (n + 1)) = (A*) ^^ ((A |^ n) ^^ A) by Th23
.= (A*) ^^ A by A4,Th18
.= A* by A2,Th54;
(A |^ (n + 1)) ^^ (A*) = ((A |^ n) ^^ A) ^^ (A*) by Th23
.= (A ^^ (A |^ n)) ^^ (A*) by Th32
.= A ^^ (A*) by A4,Th18
.= A* by A2,Th54;
hence P[n + 1] by A5;
end;
(A*) ^^ (A |^ 0) = (A*) ^^ {<%>E} by Th24
.= A* by Th13;
then
A6: P[0] by A1;
for n holds P[n] from NAT_1:sch 2(A6, A3);
hence thesis;
end;
theorem Th56:
A* = {<%>E} \/ A ^^ (A*) & A* = {<%>E} \/ (A*) ^^ A
proof
A1: now
let x be object;
assume x in {<%>E} \/ (A*) ^^ A;
then x in {<%>E} or x in (A*) ^^ A by XBOOLE_0:def 3;
then x = <%>E or x in A* by Th52,TARSKI:def 1;
hence x in A* by Th48;
end;
A2: now
let x be object;
assume x in A*;
then consider n such that
A3: x in A |^ n by Th41;
A4: now
assume n > 0;
then ex m st m + 1 = n by NAT_1:6;
hence x in (A*) ^^ A by A3,Th50;
end;
n = 0 implies x in {<%>E} by A3,Th24;
hence x in {<%>E} \/ (A*) ^^ A by A4,XBOOLE_0:def 3;
end;
A5: now
let x be object;
assume x in A*;
then consider n such that
A6: x in A |^ n by Th41;
A7: now
assume n > 0;
then ex m st m + 1 = n by NAT_1:6;
hence x in A ^^ (A*) by A6,Th50;
end;
n = 0 implies x in {<%>E} by A6,Th24;
hence x in {<%>E} \/ A ^^ (A*) by A7,XBOOLE_0:def 3;
end;
now
let x be object;
assume x in {<%>E} \/ A ^^ (A*);
then x in {<%>E} or x in A ^^ (A*) by XBOOLE_0:def 3;
then x = <%>E or x in A* by Th52,TARSKI:def 1;
hence x in A* by Th48;
end;
hence thesis by A2,A5,A1,TARSKI:2;
end;
theorem Th57:
A ^^ (A*) = (A*) ^^ A
proof
A1: A* = {<%>E} \/ A ^^ (A*) & A* = {<%>E} \/ (A*) ^^ A by Th56;
now
per cases;
suppose
A2: <%>E in A;
then A* = A ^^ (A*) by Th54;
hence thesis by A2,Th54;
end;
suppose
A3: not <%>E in A;
then not <%>E in (A*) ^^ A by Th15;
then
A4: {<%>E} misses (A*) ^^ A by ZFMISC_1:50;
not <%>E in A ^^ (A*) by A3,Th15;
then {<%>E} misses A ^^ (A*) by ZFMISC_1:50;
hence thesis by A1,A4,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);
A1: now
let n;
assume
A2: P[n];
(A |^ (n + 1)) ^^ (A*) = (A |^ n ^^ A) ^^ (A*) by Th23
.= A |^ n ^^ (A ^^ (A*)) by Th18
.= A |^ n ^^ ((A*) ^^ A) by Th57
.= ((A*) ^^ A |^ n) ^^ A by A2,Th18
.= (A*) ^^ (A |^ n ^^ A) by Th18
.= (A*) ^^ A |^ (n + 1) by Th23;
hence P[n + 1];
end;
(A |^ 0) ^^ (A*) = {<%>E} ^^ (A*) by Th24
.= A* by Th13
.= (A*) ^^ {<%>E} by Th13
.= (A*) ^^ (A |^ 0) by Th24;
then
A3: P[0];
for n holds P[n] from NAT_1:sch 2(A3, A1);
hence thesis;
end;
theorem Th59:
A c= B* implies A |^ n c= B*
proof
defpred P[Nat] means A |^ $1 c= B*;
assume
A1: A c= B*;
A2: now
let n;
assume P[n];
then (A |^ n) ^^ A c= B* by A1,Th46;
hence P[n + 1] by Th23;
end;
<%>E in B* by Th48;
then {<%>E} c= B* by ZFMISC_1:31;
then
A3: P[0] by Th24;
for n holds P[n] from NAT_1:sch 2(A3, A2);
hence thesis;
end;
theorem Th60:
A c= B* implies A* c= B*
proof
assume
A1: A c= B*;
thus thesis
proof
let x be object;
assume x in A*;
then consider n such that
A2: x in A |^ n by Th41;
A |^ n c= B* by A1,Th59;
hence thesis by A2;
end;
end;
theorem Th61:
A c= B implies A* c= B*
proof
assume
A1: A c= B;
B c= B* by Th43;
then A c= B* by A1;
hence thesis by Th60;
end;
theorem Th62:
(A*)* = A*
proof
(A*)* c= A* & A* c= (A*)* by Th43,Th60;
hence thesis by XBOOLE_0:def 10;
end;
theorem
(A*) ^^ (A*) = A*
proof
<%>E in A* by Th48;
then
A1: A* c= (A*) ^^ (A*) by Th16;
(A*) ^^ (A*) c= A* by Th46;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem
(A |^ n)* c= A* by Th42,Th60;
theorem Th65:
(A*) |^ n c= A*
proof
(A*) |^ n c= (A*)* by Th42;
hence thesis by Th62;
end;
theorem
n > 0 implies (A*) |^ n = A*
proof
<%>E in A* by Th48;
then
A1: n > 0 implies A* c= (A*) |^ n by Th35;
(A*) |^ n c= A* by Th65;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem Th67:
A c= B* implies B* = (B \/ A)*
proof
defpred P[Nat] means (B \/ A) |^ $1 c= B*;
assume
A1: A c= B*;
A2: now
let n;
assume
A3: P[n];
B c= B* by Th43;
then
A4: B \/ A c= B* by A1,XBOOLE_1:8;
(B \/ A) |^ (n + 1) = (B \/ A) |^ n ^^ (B \/ A) by Th23;
hence P[n + 1] by A3,A4,Th46;
end;
(B \/ A) |^ 0 = {<%>E} & <%>E in B* by Th24,Th48;
then
A5: P[0] by ZFMISC_1:31;
A6: for n holds P[n] from NAT_1:sch 2(A5, A2);
A7: (B \/ A)* c= B*
proof
let x be object;
assume x in (B \/ A)*;
then consider n such that
A8: x in (B \/ A) |^ n by Th41;
(B \/ A) |^ n c= B* by A6;
hence thesis by A8;
end;
B* c= (B \/ A)* by Th61,XBOOLE_1:7;
hence thesis by A7,XBOOLE_0:def 10;
end;
theorem Th68:
a in A* implies A* = (A \/ {a})*
by ZFMISC_1:31,Th67;
theorem
A* = (A \ {<%>E})*
proof
thus (A \ {<%>E})* = ((A \ {<%>E}) \/ {<%>E})* by Th48,Th68
.= (A \/ {<%>E})* by XBOOLE_1:39
.= A* by Th48,Th68;
end;
theorem
(A*) \/ (B*) c= (A \/ B)*
proof
A* c= (A \/ B)* & B* c= (A \/ B)* by Th61,XBOOLE_1:7;
hence thesis by XBOOLE_1:8;
end;
theorem
(A /\ B)* c= (A*) /\ (B*)
proof
(A /\ B)* c= A* & (A /\ B)* c= B* by Th61,XBOOLE_1:17;
hence thesis by XBOOLE_1:19;
end;
theorem Th72:
<%x%> in A* iff <%x%> in A
proof
thus <%x%> in A* implies <%x%> in A
proof
defpred P[Nat] means <%x%> in A |^ $1;
assume that
A1: <%x%> in A* and
A2: not <%x%> in A;
A3: ex i being Nat st P[i] by A1,Th41;
ex n1 being Nat st P[n1] & for n2 being Nat st P[n2] holds n1 <= n2
from NAT_1:sch 5(A3);
then consider n1 being Nat such that
A4: P[n1] and
A5: for n2 being Nat st P[n2] holds n1 <= n2;
A6: now
assume n1 = 0;
then <%x%> in {<%>E} by A4,Th24;
hence contradiction by TARSKI:def 1;
end;
A7: now
assume n1 > 1;
then consider n2 such that
A8: n2 + 1 = n1 by NAT_1:6;
<%x%> in (A |^ n2) ^^ A by A4,A8,Th23;
then consider a, b such that
A9: a in (A |^ n2) and
A10: b in A & <%x%> = a ^ b by Def1;
now
reconsider n2 as Element of NAT by ORDINAL1:def 12;
assume that
A11: a = <%x%> and
b = <%>E;
ex i being Element of NAT st P[i] & n1 > i
proof
take n2;
thus thesis by A8,A9,A11,NAT_1:13;
end;
hence contradiction by A5;
end;
hence <%x%> in A by A10,Th4;
end;
n1 = 1 implies <%x%> in A by A4,Th25;
hence contradiction by A2,A7,A6,NAT_1:25;
end;
assume <%x%> in A;
then <%x%> in A |^ 1 by Th25;
hence thesis by Th41;
end;
begin
:: Lexemes as a Subset of E^omega
:: Definition of Lex
definition
let E;
func Lex(E) -> Subset of E^omega means
:Def4:
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
A1: 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 A1;
given e such that
A2: e in E and
A3: x = <%e%>;
{e} c= E by A2,ZFMISC_1:31;
then rng <%e%> c= E by AFINSQ_1:33;
then <%e%> is XFinSequence of E by RELAT_1:def 19;
then <%e%> is Element of E^omega by AFINSQ_1:def 7;
hence thesis by A1,A2,A3;
end;
hence thesis;
end;
uniqueness
proof
let C1, C2 be Subset of E^omega such that
A4: x in C1 iff ex e st e in E & x = <%e%> and
A5: x in C2 iff ex e st e in E & x = <%e%>;
now
let x be object;
thus x in C1 implies x in C2
proof
assume x in C1;
then ex e st e in E & x = <%e%> by A4;
hence thesis by A5;
end;
assume x in C2;
then ex e st e in E & x = <%e%> by A5;
hence x in C1 by A4;
end;
hence thesis by TARSKI:2;
end;
end;
:: Lexemes as a Subset of E^omega
:: Properties of Lex
theorem Th73:
a in Lex(E) |^ len a
proof
defpred P[Nat] means for a holds len a = $1 implies a in Lex(E) |^ $1;
A1: now
let n;
assume
A2: P[n];
now
let b;
assume len b = n + 1;
then consider c, e such that
A3: len c = n and
A4: b = c ^ <%e%> by Th7;
<%e%> is Element of E^omega by A4,Th5;
then e in E by Th6;
then <%e%> in Lex(E) by Def4;
then
A5: <%e%> in Lex(E) |^ 1 by Th25;
c in Lex(E) |^ n by A2,A3;
hence b in Lex(E) |^ (n + 1) by A4,A5,Th40;
end;
hence P[n + 1];
end;
A6: P[0]
proof
let a;
assume len a = 0;
then a = <%>E;
then a in {<%>E} by TARSKI:def 1;
hence thesis by Th24;
end;
for n holds P[n] from NAT_1:sch 2(A6, A1);
hence thesis;
end;
theorem
Lex(E)* = E^omega
proof
A1: now
let x be object;
assume x in E^omega;
then reconsider a = x as Element of E^omega;
a in Lex(E) |^ len a by Th73;
hence x in Lex(E)* by Th41;
end;
for x being object st x in Lex(E)* holds x in E^omega;
hence thesis by A1,TARSKI:2;
end;
theorem
A* = E^omega implies Lex(E) c= A
proof
assume
A1: A* = E^omega;
thus thesis
proof
let x be object;
assume
A2: x in Lex(E);
then ex e st e in E & x = <%e%> by Def4;
hence thesis by A1,A2,Th72;
end;
end;