This article includes proofs of several facts
that are supplemental to the theorems proved in [1].
Next, it builds upon that theory to extend the framework
for proving facts about formal languages in general
and regular expression operators in particular.
In this article, two quantifiers are defined and their properties are shown:
m to n occurrences (or the union of a range of powers)
and optional occurrence. Although optional occurrence
is a special case of the previous operator (0 to 1 occurrences),
it is often defined in regex applications as a separate
operator - hence its explicit definition and properties in the article.
Notation and terminology were taken from [2].
Sections:
- Preliminaries
- Addenda to FLANG_1
- Union of a Range of Powers
- Optional Occurrence
Bibliography:
Mizar Mathematical Library identifier: FLANG_2.
Abstract in PDF: here.
Motorola Software Group, 2007.
Files:
:: Regular Expression Quantifiers -- $m$ to $n$ Occurrences
:: by Micha{\l} Trybulec
::
:: Received June 6, 2007
:: Copyright (c) 2007 Association of Mizar Users
environ
vocabularies BOOLE, FINSEQ_1, TARSKI, ALGSEQ_1, ARYTM_1, AFINSQ_1, MEASURE6,
GROUP_1, ARYTM, SETFAM_1, MODAL_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, XREAL_0,
XXREAL_0, AFINSQ_1, CATALAN2, FLANG_1;
constructors XXREAL_0, NAT_1, XREAL_0, CATALAN2, FLANG_1;
registrations SUBSET_1, RELSET_1, NAT_1, ORDINAL1, AFINSQ_1, XREAL_0,
XBOOLE_0, RELAT_1, FUNCT_1, ARYTM_3, XXREAL_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
theorems AFINSQ_1, NAT_1, REAL_1, SUBSET_1, TARSKI, XBOOLE_0, XBOOLE_1,
XREAL_1, ZFMISC_1, FLANG_1, XXREAL_0;
schemes CARD_FIL, DOMAIN_1, NAT_1;
begin
reserve E, x, y, X, Y, Z for set;
reserve A, B, C, D for Subset of E^omega;
reserve a, a1, a2, b, c, d for Element of E^omega;
reserve e for Element of E;
reserve i, j, k, l, kl, m, n, mn, n1, n2 for Nat;
reserve p, q, r, r1, r2 for real number;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries - Numbers:
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: FLANG_2:1
m + k <= i & i <= n + k implies
ex mn st mn + k = i & m <= mn & mn <= n;
theorem :: FLANG_2:2
m <= n & k <= l & m + k <= i & i <= n + l implies
ex mn, kl st mn + kl = i & m <= mn & mn <= n & k <= kl & kl <= l;
theorem :: FLANG_2:3
m < n implies ex k st m + k = n & k > 0;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries - Sequences:
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: FLANG_2:4
a ^ b = a or b ^ a = a implies b = {};
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Addenda - FLANG_1:
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: FLANG_2:5
(x in A or x in B) & x <> <%>E implies A ^^ B <> {<%>E};
theorem :: FLANG_2:6
<%x%> in A ^^ B iff <%>E in A & <%x%> in B or <%x%> in A & <%>E in B;
theorem :: FLANG_2:7
x in A & x <> <%>E & n > 0 implies A |^ n <> {<%>E};
theorem :: FLANG_2:8
<%>E in A |^ n iff n = 0 or <%>E in A;
theorem :: FLANG_2:9
<%x%> in A |^ n iff <%x%> in A & ((<%>E in A & n > 1) or n = 1);
theorem :: FLANG_2:10
m <> n & A |^ m = {x} & A |^ n = {x} implies x = <%>E;
theorem :: FLANG_2:11
(A |^ m) |^ n = (A |^ n) |^ m;
theorem :: FLANG_2:12
(A |^ m) ^^ (A |^ n) = (A |^ n) ^^ (A |^ m);
theorem :: FLANG_2:13
<%>E in B implies A c= A ^^ (B |^ l) & A c= (B |^ l) ^^ A;
theorem :: FLANG_2:14
A c= C |^ k & B c= C |^ l implies A ^^ B c= C |^ (k + l);
theorem :: FLANG_2:15
x in A & x <> <%>E implies A* <> {<%>E};
theorem :: FLANG_2:16
<%>E in A & n > 0 implies (A |^ n)* = A*;
theorem :: FLANG_2:17
<%>E in A implies (A |^ n)* = (A*) |^ n;
theorem :: FLANG_2:18
A c= A ^^ (B*) & A c= (B*) ^^ A;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Union of a Range of Powers
:: Definition of |^ (n, m)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, A;
let m, n;
func A |^ (m, n) -> Subset of E^omega equals
:: FLANG_2:def 1
union { B: ex k st m <= k & k <= n & B = A |^ k };
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Union of a Range of Powers
:: Properties of |^ (n, m)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: FLANG_2:19
x in A |^ (m, n) iff ex k st m <= k & k <= n & x in A |^ k;
theorem :: FLANG_2:20
m <= k & k <= n implies A |^ k c= A |^ (m, n);
theorem :: FLANG_2:21
A |^ (m, n) = {} iff m > n or (m > 0 & A = {});
theorem :: FLANG_2:22
A |^ (m, m) = A |^ m;
theorem :: FLANG_2:23
m <= k & l <= n implies A |^ (k, l) c= A |^ (m, n);
theorem :: FLANG_2:24
m <= k & k <= n implies A |^ (m, n) = A |^ (m, k) \/ A |^ (k, n);
theorem :: FLANG_2:25
m <= k & k <= n implies A |^ (m, n) = A |^ (m, k) \/ A |^ (k + 1, n);
theorem :: FLANG_2:26
m <= n + 1 implies A |^ (m, n + 1) = A |^ (m, n) \/ (A |^ (n + 1));
theorem :: FLANG_2:27
m <= n implies A |^ (m, n) = A |^ m \/ A |^ (m + 1, n);
theorem :: FLANG_2:28
A |^ (n, n + 1) = A |^ n \/ A |^ (n + 1);
theorem :: FLANG_2:29
A c= B implies A |^ (m, n) c= B |^ (m, n);
theorem :: FLANG_2:30
x in A & x <> <%>E & (m > 0 or n > 0) implies A |^ (m, n) <> {<%>E};
theorem :: FLANG_2:31
A |^ (m, n) = {<%>E} iff
(m <= n & A = {<%>E}) or (m = 0 & n = 0) or (m = 0 & A = {});
theorem :: FLANG_2:32
A |^ (m, n) c= A*;
theorem :: FLANG_2:33
<%>E in A |^ (m, n) iff m = 0 or (m <= n & <%>E in A);
theorem :: FLANG_2:34
<%>E in A & m <= n implies A |^ (m, n) = A |^ n;
theorem :: FLANG_2:35
A |^ (m, n) ^^ (A |^ k) = (A |^ k) ^^ (A |^ (m, n));
theorem :: FLANG_2:36
(A |^ (m, n)) ^^ A = A ^^ (A |^ (m, n));
theorem :: FLANG_2:37
m <= n & k <= l implies (A |^ (m, n)) ^^ (A |^ (k, l)) = A |^ (m + k, n + l);
theorem :: FLANG_2:38
A |^ (m + 1, n + 1) = (A |^ (m, n)) ^^ A;
theorem :: FLANG_2:39
(A |^ (m, n)) ^^ (A |^ (k, l)) = (A |^ (k, l)) ^^ (A |^ (m, n));
theorem :: FLANG_2:40
(A |^ (m, n)) |^ k = A |^ (m * k, n * k);
theorem :: FLANG_2:41
(A |^ (k + 1)) |^ (m, n) c= ((A |^ k) |^ (m, n)) ^^ (A |^ (m, n));
theorem :: FLANG_2:42
(A |^ k) |^ (m, n) c= A |^ (k * m, k * n);
theorem :: FLANG_2:43
(A |^ k) |^ (m, n) c= (A |^ (m, n)) |^ k;
theorem :: FLANG_2:44
(A |^ (k + l)) |^ (m, n) c= ((A |^ k) |^ (m, n)) ^^ ((A |^ l) |^ (m, n));
theorem :: FLANG_2:45
A |^ (0, 0) = {<%>E};
theorem :: FLANG_2:46
A |^ (0, 1) = {<%>E} \/ A;
theorem :: FLANG_2:47
A |^ (1, 1) = A;
theorem :: FLANG_2:48
A |^ (0, 2) = {<%>E} \/ A \/ (A ^^ A);
theorem :: FLANG_2:49
A |^ (1, 2) = A \/ (A ^^ A);
theorem :: FLANG_2:50
A |^ (2, 2) = A ^^ A;
theorem :: FLANG_2:51
m > 0 & m <> n & A |^ (m, n) = {x} implies
for mn st m <= mn & mn <= n holds A |^ mn = {x};
theorem :: FLANG_2:52
m <> n & A |^ (m, n) = {x} implies x = <%>E;
theorem :: FLANG_2:53
<%x%> in A |^ (m, n) iff
<%x%> in A & m <= n & ((<%>E in A & (n > 0)) or (m <= 1 & 1 <= n));
theorem :: FLANG_2:54
(A /\ B) |^ (m, n) c= (A |^ (m, n)) /\ (B |^ (m, n));
theorem :: FLANG_2:55
(A |^ (m, n)) \/ (B |^ (m, n)) c= (A \/ B) |^ (m, n);
theorem :: FLANG_2:56
(A |^ (m, n)) |^ (k, l) c= A |^ (m * k, n * l);
theorem :: FLANG_2:57
m <= n & <%>E in B implies A c= A ^^ (B |^ (m, n)) & A c= (B |^ (m, n)) ^^ A;
theorem :: FLANG_2:58
m <= n & k <= l & A c= C |^ (m, n) & B c= C |^ (k, l) implies
A ^^ B c= C |^ (m + k, n + l);
theorem :: FLANG_2:59
(A |^ (m, n))* c= A*;
theorem :: FLANG_2:60
(A*) |^ (m, n) c= A*;
theorem :: FLANG_2:61
m <= n & n > 0 implies (A*) |^ (m, n) = A*;
theorem :: FLANG_2:62
m <= n & n > 0 & <%>E in A implies (A |^ (m, n))* = A*;
theorem :: FLANG_2:63
m <= n & <%>E in A implies (A |^ (m, n))* = (A*) |^ (m, n);
theorem :: FLANG_2:64
A c= B* implies A |^ (m, n) c= B*;
theorem :: FLANG_2:65
A c= B* implies B* = (B \/ (A |^ (m, n)))*;
theorem :: FLANG_2:66
A |^ (m, n) ^^ (A*) = A* ^^ (A |^ (m, n));
theorem :: FLANG_2:67
<%>E in A & m <= n implies A* = A* ^^ (A |^ (m, n));
theorem :: FLANG_2:68
A |^ (m, n) |^ k c= A*;
theorem :: FLANG_2:69
A |^ k |^ (m, n) c= A*;
theorem :: FLANG_2:70
m <= n implies (A |^ m)* c= (A |^ (m, n))*;
theorem :: FLANG_2:71
(A |^ (m, n)) |^ (k, l) c= A*;
theorem :: FLANG_2:72
<%>E in A & k <= n & l <= n implies A |^ (k, n) = A |^ (l, n);
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Optional Occurrence
:: Definition of ?
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, A;
func A? -> Subset of E^omega equals
:: FLANG_2:def 2
union { B: ex k st k <= 1 & B = A |^ k };
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Optional Occurrence
:: Properties of ?
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: FLANG_2:73
x in A? iff ex k st k <= 1 & x in A |^ k;
theorem :: FLANG_2:74
n <= 1 implies A |^ n c= A?;
theorem :: FLANG_2:75
A? = (A |^ 0) \/ (A |^ 1);
theorem :: FLANG_2:76
A? = {<%>E} \/ A;
theorem :: FLANG_2:77
A c= A?;
theorem :: FLANG_2:78
x in A? iff x = <%>E or x in A;
theorem :: FLANG_2:79
A? = A |^ (0, 1);
theorem :: FLANG_2:80
A? = A iff <%>E in A;
registration let E, A;
cluster A? -> non empty;
end;
theorem :: FLANG_2:81
A?? = A?;
theorem :: FLANG_2:82
A c= B implies A? c= B?;
theorem :: FLANG_2:83
x in A & x <> <%>E implies A? <> {<%>E};
theorem :: FLANG_2:84
A? = {<%>E} iff A = {} or A = {<%>E};
theorem :: FLANG_2:85
(A*)? = A* & (A?)* = A*;
theorem :: FLANG_2:86
A? c= A*;
theorem :: FLANG_2:87
(A /\ B)? = (A?) /\ (B?);
theorem :: FLANG_2:88
(A?) \/ (B?) = (A \/ B)?;
theorem :: FLANG_2:89
A? = {x} implies x = <%>E;
theorem :: FLANG_2:90
<%x%> in A? iff <%x%> in A;
theorem :: FLANG_2:91
(A?) ^^ A = A ^^ (A?);
theorem :: FLANG_2:92
(A?) ^^ A = A |^ (1, 2);
theorem :: FLANG_2:93
(A?) ^^ (A?) = A |^ (0, 2);
theorem :: FLANG_2:94
(A?) |^ k = (A?) |^ (0, k);
theorem :: FLANG_2:95
(A?) |^ k = A |^ (0, k);
theorem :: FLANG_2:96
m <= n implies A? |^ (m, n) = A? |^ (0, n);
theorem :: FLANG_2:97
A? |^ (0, n) = A |^ (0, n);
theorem :: FLANG_2:98
m <= n implies A? |^ (m, n) = A |^ (0, n);
theorem :: FLANG_2:99
(A |^ (1, n))? = A |^ (0, n);
theorem :: FLANG_2:100
<%>E in A & <%>E in B implies A? c= A ^^ B & A? c= B ^^ A;
theorem :: FLANG_2:101
A c= A ^^ (B?) & A c= (B?) ^^ A;
theorem :: FLANG_2:102
A c= C? & B c= C? implies A ^^ B c= C |^ (0, 2);
theorem :: FLANG_2:103
<%>E in A & n > 0 implies A? c= A |^ n;
theorem :: FLANG_2:104
(A?) ^^ (A |^ k) = (A |^ k) ^^ (A?);
theorem :: FLANG_2:105
A c= B* implies A? c= B*;
theorem :: FLANG_2:106
A c= B* implies B* = (B \/ (A?))*;
theorem :: FLANG_2:107
A? ^^ (A*) = A* ^^ (A?);
theorem :: FLANG_2:108
A? ^^ (A*) = A*;
theorem :: FLANG_2:109
A? |^ k c= A*;
theorem :: FLANG_2:110
(A |^ k)? c= A*;
theorem :: FLANG_2:111
(A?) ^^ (A |^ (m, n)) = (A |^ (m, n)) ^^ (A?);
theorem :: FLANG_2:112
(A?) ^^ (A |^ k) = A |^ (k, k + 1);
theorem :: FLANG_2:113
A? |^ (m, n) c= A*;
theorem :: FLANG_2:114
(A |^ (m, n))? c= A*;
theorem :: FLANG_2:115
A? = (A \ {<%>E})?;
theorem :: FLANG_2:116
A c= B? implies A? c= B?;
theorem :: FLANG_2:117
A c= B? implies B? = (B \/ A)?;
Top
:: Regular Expression Quantifiers -- $m$ to $n$ Occurrences
:: by Micha{\l} Trybulec
::
:: Received June 6, 2007
:: Copyright (c) 2007 Association of Mizar Users
environ
vocabularies BOOLE, FINSEQ_1, TARSKI, ALGSEQ_1, ARYTM_1, AFINSQ_1, MEASURE6,
GROUP_1, ARYTM, SETFAM_1, MODAL_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, XREAL_0,
XXREAL_0, AFINSQ_1, CATALAN2, FLANG_1;
constructors XXREAL_0, NAT_1, XREAL_0, CATALAN2, FLANG_1;
registrations SUBSET_1, RELSET_1, NAT_1, ORDINAL1, AFINSQ_1, XREAL_0,
XBOOLE_0, RELAT_1, FUNCT_1, ARYTM_3, XXREAL_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
theorems AFINSQ_1, NAT_1, REAL_1, SUBSET_1, TARSKI, XBOOLE_0, XBOOLE_1,
XREAL_1, ZFMISC_1, FLANG_1, XXREAL_0;
schemes CARD_FIL, DOMAIN_1, NAT_1;
begin
reserve E, x, y, X, Y, Z for set;
reserve A, B, C, D for Subset of E^omega;
reserve a, a1, a2, b, c, d for Element of E^omega;
reserve e for Element of E;
reserve i, j, k, l, kl, m, n, mn, n1, n2 for Nat;
reserve p, q, r, r1, r2 for real number;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries - Numbers:
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem LmNum19:
m + k <= i & i <= n + k implies
ex mn st mn + k = i & m <= mn & mn <= n
proof
assume
A: m + k <= i & i <= n + k;
then m + k <= m + i by XREAL_1:40;
then k <= i by XREAL_1:8;
then reconsider mn = i - k as Nat by NAT_1:21;
take mn;
thus mn + k = i;
m + k <= mn + k & mn + k <= n + k by A;
hence m <= mn & mn <= n by XREAL_1:8;
end;
theorem LmNum20:
m <= n & k <= l & m + k <= i & i <= n + l implies
ex mn, kl st mn + kl = i & m <= mn & mn <= n & k <= kl & kl <= l
proof
assume
A: m <= n & k <= l & m + k <= i & i <= n + l;
per cases;
suppose i <= n + k;
then consider mn such that
B2: mn + k = i & m <= mn & mn <= n by A, LmNum19;
take mn, k;
thus mn + k = i & m <= mn & mn <= n by B2;
thus k <= k & k <= l by A;
end;
suppose i > n + k;
then consider kl such that
B2: kl + n = i & k <= kl & kl <= l by A, LmNum19;
take n, kl;
thus n + kl = i & m <= n & n <= n by A, B2;
thus k <= kl & kl <= l by B2;
end;
end;
theorem LmNum30:
m < n implies ex k st m + k = n & k > 0
proof
assume
A: m < n;
then consider k such that
B: m + k = n by NAT_1:10;
m - m < n - m by A, XREAL_1:16;
hence thesis by B;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries - Sequences:
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem LmSeq20:
a ^ b = a or b ^ a = a implies b = {}
proof
assume
A: a ^ b = a or b ^ a = a;
per cases by A;
suppose a ^ b = a;
then len(a ^ b) = len(a) + len(b) & len(a ^ b) = len(a) by AFINSQ_1:20;
hence thesis by AFINSQ_1:18;
end;
suppose b ^ a = a;
then len(b ^ a) = len(b) + len(a) & len(b ^ a) = len(a) by AFINSQ_1:20;
hence thesis by AFINSQ_1:18;
end;
end;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Addenda - FLANG_1:
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem
(x in A or x in B) & x <> <%>E implies A ^^ B <> {<%>E}
proof
assume (x in A or x in B) & x <> <%>E;
then A <> {<%>E} or B <> {<%>E} by TARSKI:def 1;
hence thesis by FLANG_1:15;
end;
theorem
<%x%> in A ^^ B iff <%>E in A & <%x%> in B or <%x%> in A & <%>E in B
proof
thus <%x%> in A ^^ B implies <%>E in A & <%x%> in B or <%x%> in A & <%>E in B
proof
assume <%x%> in A ^^ B;
then consider a, b such that
A: a in A & b in B & <%x%> = a ^ b by FLANG_1:def 1;
thus thesis by A, FLANG_1:4;
end;
assume
B: <%>E in A & <%x%> in B or <%x%> in A & <%>E in B;
<%>E ^ <%x%> = <%x%> & <%x%> ^ <%>E = <%x%> by AFINSQ_1:32;
hence thesis by B, FLANG_1:def 1;
end;
theorem LmLang20:
x in A & x <> <%>E & n > 0 implies A |^ n <> {<%>E}
proof
assume that
A1: x in A & x <> <%>E and
A2: n > 0;
A <> {<%>E} by A1, TARSKI:def 1;
hence thesis by A2, FLANG_1:30;
end;
theorem
<%>E in A |^ n iff n = 0 or <%>E in A
proof
thus <%>E in A |^ n implies n = 0 or <%>E in A
proof
assume that
A1: <%>E in A |^ n and
A2: n <> 0 & not <%>E in A;
n > 0 by A2;
hence contradiction by A1, A2, FLANG_1:32;
end;
assume
B: n = 0 or <%>E in A;
per cases by B;
suppose n = 0;
then A |^ n = {<%>E} by FLANG_1:30;
hence thesis by ZFMISC_1:37;
end;
suppose <%>E in A;
hence thesis by FLANG_1:31;
end;
end;
theorem LmLang31:
<%x%> in A |^ n iff <%x%> in A & ((<%>E in A & n > 1) or n = 1)
proof
thus <%x%> in A |^ n implies <%x%> in A & ((<%>E in A & n > 1) or n = 1)
proof
assume
A1: <%x%> in A |^ n;
A |^ n c= A* by FLANG_1:43;
hence <%x%> in A by A1, FLANG_1:73;
assume
A2: (not <%>E in A or n <= 1) & n <> 1;
per cases by A2;
suppose
A3: not <%>E in A & n <> 1;
per cases by A3, NAT_1:26;
suppose n = 0;
then A |^ n = {<%>E} by FLANG_1:25;
hence contradiction by A1, TARSKI:def 1;
end;
suppose
A3a: n > 1;
then consider m such that
A3b: m + 1 = n by NAT_1:6;
<%x%> in (A |^ m) ^^ A by A1, A3b, FLANG_1:24;
then consider a, b such that
A3c: a in (A |^ m) & b in A & <%x%> = a ^ b by FLANG_1:def 1;
per cases by FLANG_1:4, A3c;
suppose
A3d: a = <%>E & b = <%x%>;
m + 1 > 0 + 1 by A3a, A3b;
then m > 0 by XREAL_1:8;
hence contradiction by A3, A3c, A3d, FLANG_1:32;
end;
suppose b = <%>E & a = <%x%>;
hence contradiction by A3c, A3;
end;
end;
end;
suppose n <= 1 & n <> 1;
then n = 0 by NAT_1:26;
then A |^ n = {<%>E} by FLANG_1:25;
hence contradiction by A1, TARSKI:def 1;
end;
end;
assume that
B1: <%x%> in A and
B2: (<%>E in A & n > 1) or n = 1;
per cases by B2;
suppose <%>E in A & n > 1;
then A c= A |^ n by FLANG_1:36;
hence thesis by B1;
end;
suppose n = 1;
hence thesis by B1, FLANG_1:26;
end;
end;
theorem LmLang32:
m <> n & A |^ m = {x} & A |^ n = {x} implies x = <%>E
proof
assume
A: m <> n & A |^ m = {x} & A |^ n = {x};
A1:
x in A |^ m & x in A |^ n by A, TARSKI:def 1;
per cases by A, REAL_1:def 5;
suppose m > n;
then consider k such that
B: n + k = m & k > 0 by LmNum30;
(A |^ n) ^^ (A |^ k) = A |^ m by B, FLANG_1:34;
then consider a, b such that
B1: a in A |^ n & b in A |^ k & x = a ^ b by A1, FLANG_1:def 1;
a = x by B1, A, TARSKI:def 1;
then b = <%>E by B1, LmSeq20;
then <%>E in A by B, B1, FLANG_1:32;
then <%>E in A |^ m & <%>E in A |^ n by FLANG_1:31;
hence thesis by A, TARSKI:def 1;
end;
suppose m < n;
then consider k such that
B: m + k = n & k > 0 by LmNum30;
(A |^ m) ^^ (A |^ k) = A |^ n by B, FLANG_1:34;
then consider a, b such that
B1: a in A |^ m & b in A |^ k & x = a ^ b by A1, FLANG_1:def 1;
a = x by B1, A, TARSKI:def 1;
then b = <%>E by B1, LmSeq20;
then <%>E in A by B, B1, FLANG_1:32;
then <%>E in A |^ m & <%>E in A |^ n by FLANG_1:31;
hence thesis by A, TARSKI:def 1;
end;
end;
theorem
(A |^ m) |^ n = (A |^ n) |^ m
proof
thus (A |^ m) |^ n = A |^ (m * n) by FLANG_1:35
.= (A |^ n) |^ m by FLANG_1:35;
end;
theorem LmLang50:
(A |^ m) ^^ (A |^ n) = (A |^ n) ^^ (A |^ m)
proof
thus (A |^ m) ^^ (A |^ n) = A |^ (m + n) by FLANG_1:34
.= (A |^ n) ^^ (A |^ m) by FLANG_1:34;
end;
theorem
<%>E in B implies A c= A ^^ (B |^ l) & A c= (B |^ l) ^^ A
proof
assume <%>E in B;
then <%>E in B |^ l by FLANG_1:31;
hence thesis by FLANG_1:17;
end;
theorem
A c= C |^ k & B c= C |^ l implies A ^^ B c= C |^ (k + l)
proof
assume A c= C |^ k & B c= C |^ l;
then A ^^ B c= (C |^ k) ^^ (C |^ l) by FLANG_1:18;
hence thesis by FLANG_1:34;
end;
theorem
x in A & x <> <%>E implies A* <> {<%>E}
proof
assume x in A & x <> <%>E;
then A <> {} & A <> {<%>E} by TARSKI:def 1;
hence thesis by FLANG_1:48;
end;
theorem LmLang70:
<%>E in A & n > 0 implies (A |^ n)* = A*
proof
assume
A: <%>E in A & n > 0;
B:
A* c= (A |^ n)*
proof
A c= A |^ n by A, FLANG_1:36;
hence thesis by FLANG_1:62;
end;
(A |^ n)* c= A* by FLANG_1:65;
hence thesis by B, XBOOLE_0:def 10;
end;
theorem LmLang80:
<%>E in A implies (A |^ n)* = (A*) |^ n
proof
assume
A: <%>E in A;
per cases;
suppose
B: n = 0;
thus (A |^ n)* = {<%>E}* by FLANG_1:25, B
.= {<%>E} by FLANG_1:48
.= (A*) |^ n by B, FLANG_1:25;
end;
suppose
C: n > 0;
then (A*) |^ n = A* by FLANG_1:67;
hence thesis by A, C, LmLang70;
end;
end;
theorem
A c= A ^^ (B*) & A c= (B*) ^^ A
proof
<%>E in B* by FLANG_1:49;
hence thesis by FLANG_1:17;
end;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Union of a Range of Powers
:: Definition of |^ (n, m)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, A;
let m, n;
func A |^ (m, n) -> Subset of E^omega equals
union { B: ex k st m <= k & k <= n & B = A |^ k };
coherence
proof
defpred P[set] means ex k st m <= k & k <= n & $1 = A |^ k;
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;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Union of a Range of Powers
:: Properties of |^ (n, m)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem ThRange10:
x in A |^ (m, n) iff ex k st m <= k & k <= n & x in A |^ k
proof
thus x in A |^ (m, n) implies ex k st m <= k & k <= n & x in A |^ k
proof
assume x in A |^ (m, n);
then consider X such that
A1: x in X and
A2: X in { B: ex k st m <= k & k <= n & B = A |^ k } by TARSKI:def 4;
defpred P[set] means ex k st m <= k & k <= n & $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 k such that
B: m <= k & k <= n & x in A |^ k;
defpred P[set] means ex k st m <= k & k <= n & $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 ThRange20:
m <= k & k <= n implies A |^ k c= A |^ (m, n)
proof
assume m <= k & k <= n;
then for x holds x in A |^ k implies x in A |^ (m, n) by ThRange10;
hence thesis by TARSKI:def 3;
end;
theorem ThRange30:
A |^ (m, n) = {} iff m > n or (m > 0 & A = {})
proof
thus A |^ (m, n) = {} implies m > n or (m > 0 & A = {})
proof
assume that
A1: A |^ (m, n) = {} and
A2: m <= n & (m <= 0 or A <> {});
B: now
assume
B1: m <= n & m = 0;
then {<%>E} = A |^ m by FLANG_1:30;
then <%>E in A |^ m by TARSKI:def 1;
hence contradiction by A1, B1, ThRange10;
end;
now
assume
C1: m <= n & A <> {};
then A |^ m <> {} by FLANG_1:28;
then ex a st a in A |^ m by SUBSET_1:10;
hence contradiction by A1, C1, ThRange10;
end;
hence thesis by A2, B;
end;
A:
now
assume
A1: m > n;
now
let x;
not (ex k st m <= k & k <= n & x in A |^ k) by A1, XXREAL_0:2;
hence not x in A |^ (m, n) by ThRange10;
end;
hence A |^ (m, n) = {} by XBOOLE_0:def 1;
end;
now
assume
B: m > 0 & A = {};
now
let x;
assume x in A |^ (m, n);
then consider k such that
B1: m <= k & k <= n & x in A |^ k by ThRange10;
thus contradiction by B, B1, FLANG_1:28;
end;
hence A |^ (m, n) = {} by XBOOLE_0:def 1;
end;
hence thesis by A;
end;
theorem ThRange40:
A |^ (m, m) = A |^ m
proof
A:
now
let x;
assume x in A |^ (m, m);
then consider k such that
A1: m <= k & k <= m & x in A |^ k by ThRange10;
thus x in A |^ m by A1, XXREAL_0:1;
end;
for x holds x in A |^ m implies x in A |^ (m, m) by ThRange10;
hence thesis by A, TARSKI:2;
end;
theorem ThRange50:
m <= k & l <= n implies A |^ (k, l) c= A |^ (m, n)
proof
assume
A: m <= k & l <= n;
thus thesis
proof
let x;
assume x in A |^ (k, l);
then consider kl such that
B: k <= kl & kl <= l & x in A |^ kl by ThRange10;
m <= kl & kl <= n by A, B, XXREAL_0:2;
hence x in A |^ (m, n) by B, ThRange10;
end;
end;
theorem
m <= k & k <= n implies A |^ (m, n) = A |^ (m, k) \/ A |^ (k, n)
proof
assume
A: m <= k & k <= n;
B:
A |^ (m, n) c= A |^ (m, k) \/ A |^ (k, n)
proof
let x;
assume x in A |^ (m, n);
then consider l such that
B1: m <= l & l <= n & x in A |^ l by ThRange10;
l <= k or l > k;
then x in A |^ (m, k) or x in A |^ (k, n) by B1, ThRange10;
hence x in A |^ (m, k) \/ A |^ (k, n) by XBOOLE_0:def 2;
end;
A |^ (m, k) \/ A |^ (k, n) c= A |^ (m, n)
proof
A |^ (m, k) c= A |^ (m, n) & A |^ (k, n) c= A |^ (m, n) by A, ThRange50;
hence thesis by XBOOLE_1:8;
end;
hence thesis by B, XBOOLE_0:def 10;
end;
theorem ThRange70:
m <= k & k <= n implies A |^ (m, n) = A |^ (m, k) \/ A |^ (k + 1, n)
proof
assume
A: m <= k & k <= n;
per cases;
suppose k < n;
then m <= k & m <= k + 1 & k <= n & k + 1 <= n by A, NAT_1:13;
then A |^ (m, k) c= A |^ (m, n) &
A |^ (k + 1, n) c= A |^ (m, n) by ThRange50;
then
B: A |^ (m, k) \/ A |^ (k + 1, n) c= A |^ (m, n) by XBOOLE_1:8;
A |^ (m, n) c= A |^ (m, k) \/ A |^ (k + 1, n)
proof
let x;
assume x in A |^ (m, n);
then consider mn such that
C: m <= mn & mn <= n & x in A |^ mn by ThRange10;
D: mn <= k implies x in A |^ (m, k) by C, ThRange10;
mn >= k + 1 implies x in A |^ (k + 1, n) by C, ThRange10;
hence x in A |^ (m, k) \/ A |^ (k + 1, n) by D, NAT_1:13, XBOOLE_0:def 2;
end;
hence thesis by B, XBOOLE_0:def 10;
end;
suppose
B: k >= n;
then k + 1 > n + 0 by XREAL_1:10;
then A |^ (k + 1, n) = {} by ThRange30;
hence thesis by B, A, XXREAL_0:1;
end;
end;
theorem ThRange80:
m <= n + 1 implies A |^ (m, n + 1) = A |^ (m, n) \/ (A |^ (n + 1))
proof
assume
A: m <= n + 1;
per cases by A, NAT_1:8;
suppose m <= n;
then m <= n & n < n + 1 by NAT_1:13;
then A |^ (m, n + 1) = A |^ (m, n) \/ A |^ (n + 1, n + 1) by ThRange70;
hence thesis by ThRange40;
end;
suppose
B: m = n + 1;
then
C: m > n by NAT_1:13;
thus A |^ (m, n + 1) = {} \/ A |^ (n + 1) by B, ThRange40
.= A |^ (m, n) \/ A |^ (n + 1) by C, ThRange30;
end;
end;
theorem
m <= n implies A |^ (m, n) = A |^ m \/ A |^ (m + 1, n)
proof
assume
A: m <= n;
per cases by A, REAL_1:def 5;
suppose m < n;
then A |^ (m, n) = A |^ (m, m) \/ A |^ (m + 1, n) by ThRange70;
hence thesis by ThRange40;
end;
suppose
B: m = n;
then
C: m + 1 > n by NAT_1:13;
thus A |^ (m, n) = A |^ m \/ {} by B, ThRange40
.= A |^ m \/ A |^ (m + 1, n) by C, ThRange30;
end;
end;
theorem ThRange100:
A |^ (n, n + 1) = A |^ n \/ A |^ (n + 1)
proof
n <= n + 1 by NAT_1:11;
hence A |^ (n, n + 1) = A |^ (n, n) \/ A |^ (n + 1) by ThRange80
.= A |^ n \/ A |^ (n + 1) by ThRange40;
end;
theorem ThRange110:
A c= B implies A |^ (m, n) c= B |^ (m, n)
proof
assume
A: A c= B;
thus thesis
proof
let x;
assume x in A |^ (m, n);
then consider k such that
B: m <= k & k <= n & x in A |^ k by ThRange10;
A |^ k c= B |^ k by A, FLANG_1:38;
hence x in B |^ (m, n) by B, ThRange10;
end;
end;
theorem ThRange120:
x in A & x <> <%>E & (m > 0 or n > 0) implies A |^ (m, n) <> {<%>E}
proof
assume that
A1: x in A & x <> <%>E and
A2: (m > 0 or n > 0);
per cases by A2;
suppose m > n;
hence thesis by ThRange30;
end;
suppose
B: m <= n & m > 0;
then
B1: A |^ m <> {<%>E} by A1, LmLang20;
A |^ m <> {} by A1, FLANG_1:28;
then consider x such that
B2: x in A |^ m & x <> <%>E by B1, ZFMISC_1:41;
A |^ m c= A |^ (m, n) by B, ThRange20;
hence thesis by B2, TARSKI:def 1;
end;
suppose
B: m <= n & n > 0;
then
B1: A |^ n <> {<%>E} by A1, LmLang20;
A |^ n <> {} by A1, FLANG_1:28;
then consider x such that
B2: x in A |^ n & x <> <%>E by B1, ZFMISC_1:41;
A |^ n c= A |^ (m, n) by B, ThRange20;
hence thesis by B2, TARSKI:def 1;
end;
end;
theorem ThRange130:
A |^ (m, n) = {<%>E} iff
(m <= n & A = {<%>E}) or (m = 0 & n = 0) or (m = 0 & A = {})
proof
thus A |^ (m, n) = {<%>E} implies
(m <= n & A = {<%>E}) or (m = 0 & n = 0) or (m = 0 & A = {})
proof
assume that
A: A |^ (m, n) = {<%>E} and
B: (m > n or A <> {<%>E}) & (m <> 0 or n <> 0) & (m <> 0 or A <> {});
per cases by B;
suppose m > n;
hence contradiction by A, ThRange30;
end;
suppose
B1: m <= n & A <> {<%>E} & (m <> 0 or (n <> 0 & A <> {}));
per cases by B1;
suppose
B1a: m <> 0;
per cases;
suppose
B1b: A = {};
m > 0 by B1a;
hence contradiction by A, B1b, ThRange30;
end;
suppose A <> {};
then consider x such that
B1c: x in A & x <> <%>E by B1, ZFMISC_1:41;
m > 0 by B1a;
hence contradiction by A, B1c, ThRange120;
end;
end;
suppose
B1a: n <> 0 & A <> {};
then consider x such that
B1b: x in A & x <> <%>E by B1, ZFMISC_1:41;
n > 0 by B1a;
hence contradiction by A, B1b, ThRange120;
end;
end;
end;
assume
C1: (m <= n & A = {<%>E}) or (m = 0 & n = 0) or (m = 0 & A = {});
per cases by C1;
suppose
C2: m <= n & A = {<%>E};
C3: now
let x;
assume x in A |^ (m, n);
then consider k such that
C3a: m <= k & k <= n & x in {<%>E} |^ k by C2, ThRange10;
thus x in {<%>E} by C3a, FLANG_1:30;
end;
now
let x;
assume x in {<%>E};
then
C4: x in {<%>E} |^ m by FLANG_1:30;
{<%>E} |^ m c= {<%>E} |^ (m, n) by C2, ThRange20;
hence x in A |^ (m, n) by C4, C2;
end;
hence thesis by C3, TARSKI:2;
end;
suppose
D: m = 0 & n = 0;
A |^ (0, 0) = A |^ 0 by ThRange40
.= {<%>E} by FLANG_1:30;
hence thesis by D;
end;
suppose
E: m = 0 & A = {};
E2: A |^ (1, n) = {}
proof
now
let x;
assume x in A |^ (1, n);
then consider k such that
E3: 1 <= k & k <= n & x in A |^ k by ThRange10;
thus contradiction by E, E3, FLANG_1:28;
end;
hence thesis by XBOOLE_0:def 1;
end;
A |^ (0, n) = A |^ (0, 0) \/ A |^ (0 + 1, n) by ThRange70
.= A |^ 0 \/ A |^ (0 + 1, n) by ThRange40
.= {<%>E} by E2, FLANG_1:30;
hence thesis by E;
end;
end;
theorem ThRange140:
A |^ (m, n) c= A*
proof
let x;
assume x in A |^ (m, n);
then consider k such that
A: m <= k & k <= n & x in A |^ k by ThRange10;
thus x in A* by A, FLANG_1:42;
end;
theorem ThRange150:
<%>E in A |^ (m, n) iff m = 0 or (m <= n & <%>E in A)
proof
thus <%>E in A |^ (m, n) implies m = 0 or (m <= n & <%>E in A)
proof
assume that
A: <%>E in A |^ (m, n) and
B: m <> 0 & (m > n or not <%>E in A);
per cases by B;
suppose m <> 0 & m > n;
hence contradiction by A, ThRange30;
end;
suppose
B1: m <> 0 & not <%>E in A;
consider k such that
B2: m <= k & k <= n & <%>E in A |^ k by A, ThRange10;
k > 0 by B1, B2;
hence contradiction by B1, B2, FLANG_1:32;
end;
end;
assume
C: m = 0 or (m <= n & <%>E in A);
per cases by C;
suppose
C1: m = 0;
{<%>E} = A |^ 0 by FLANG_1:30;
then {<%>E} c= A |^ (0, n) & <%>E in {<%>E} by ThRange20, TARSKI:def 1;
hence <%>E in A |^ (m, n) by C1;
end;
suppose
C2: m <= n & <%>E in A;
then
C3: <%>E in A |^ m by FLANG_1:31;
A |^ m c= A |^ (m, n) by C2, ThRange20;
hence <%>E in A |^ (m, n) by C3;
end;
end;
theorem ThRange160:
<%>E in A & m <= n implies A |^ (m, n) = A |^ n
proof
assume
A: <%>E in A & m <= n;
B:
A |^ (m, n) c= A |^ n
proof
C0:
now
let k such that
C: k <= n;
per cases by C, REAL_1:def 5;
suppose k < n;
hence A |^ k c= A |^ n by A, FLANG_1:37;
end;
suppose k = n;
hence A |^ k c= A |^ n;
end;
end;
let x such that
D: x in A |^ (m, n);
consider k such that
E: m <= k & k <= n & x in A |^ k by D, ThRange10;
A |^ k c= A |^ n by E, C0;
hence x in A |^ n by E;
end;
A |^ n c= A |^ (m, n) by A, ThRange20;
hence thesis by B, XBOOLE_0:def 10;
end;
theorem ThRange240:
A |^ (m, n) ^^ (A |^ k) = (A |^ k) ^^ (A |^ (m, n))
proof
A:
now
let x;
assume x in (A |^ (m, n)) ^^ (A |^ k);
then consider a, b such that
A1: a in A |^ (m, n) & b in (A |^ k) & x = a ^ b by FLANG_1:def 1;
consider mn such that
A2: m <= mn & mn <= n & a in A |^ mn by A1, ThRange10;
a ^ b in (A |^ mn) ^^ (A |^ k) by A1, A2, FLANG_1:def 1;
then
A3: a ^ b in (A |^ k) ^^ (A |^ mn) by LmLang50;
A |^ mn c= A |^ (m, n) by A2, ThRange20;
then (A |^ k) ^^ (A |^ mn) c= (A |^ k) ^^ (A |^ (m, n)) by FLANG_1:18;
hence x in (A |^ k) ^^ (A |^ (m, n)) by A3, A1;
end;
now
let x;
assume x in (A |^ k) ^^ (A |^ (m, n));
then consider a, b such that
A1: a in (A |^ k) & b in A |^ (m, n) & x = a ^ b by FLANG_1:def 1;
consider mn such that
A2: m <= mn & mn <= n & b in A |^ mn by A1, ThRange10;
a ^ b in (A |^ k) ^^ (A |^ mn) by A1, A2, FLANG_1:def 1;
then
A3: a ^ b in (A |^ mn) ^^ (A |^ k) by LmLang50;
A |^ mn c= A |^ (m, n) by A2, ThRange20;
then (A |^ mn) ^^ (A |^ k) c= (A |^ (m, n)) ^^ (A |^ k) by FLANG_1:18;
hence x in (A |^ (m, n)) ^^ (A |^ k) by A3, A1;
end;
hence thesis by A, TARSKI:2;
end;
theorem ThRange170:
(A |^ (m, n)) ^^ A = A ^^ (A |^ (m, n))
proof
thus (A |^ (m, n)) ^^ A = (A |^ (m, n)) ^^ (A |^ 1) by FLANG_1:26
.= (A |^ 1) ^^ (A |^ (m, n)) by ThRange240
.= A ^^ (A |^ (m, n)) by FLANG_1:26;
end;
theorem ThRange190:
m <= n & k <= l implies (A |^ (m, n)) ^^ (A |^ (k, l)) = A |^ (m + k, n + l)
proof
assume
A0: m <= n & k <= l;
A:
now
let x;
assume x in (A |^ (m, n)) ^^ (A |^ (k, l));
then consider a, b such that
A1: a in A |^ (m, n) & b in A |^ (k, l) & x = a ^ b by FLANG_1:def 1;
consider mn such that
A2: m <= mn & mn <= n & a in A |^ mn by A1, ThRange10;
consider kl such that
A3: k <= kl & kl <= l & b in A |^ kl by A1, ThRange10;
A4: a ^ b in A |^ (mn + kl) by A2, A3, FLANG_1:41;
A5: m + k <= mn + kl by A2, A3, XREAL_1:9;
mn + kl <= n + l by A2, A3, XREAL_1:9;
hence x in A |^ (m + k, n + l) by A1, A4, A5, ThRange10;
end;
now
let x;
assume x in A |^ (m + k, n + l);
then consider i such that
A1: m + k <= i & i <= n + l & x in A |^ i by ThRange10;
consider mn, kl such that
A2: mn + kl = i & m <= mn & mn <= n & k <= kl & kl <= l by A0, A1, LmNum20;
A3: A |^ mn c= A |^ (m, n) by A2, ThRange20;
A |^ kl c= A |^ (k, l) by A2, ThRange20;
then (A |^ mn) ^^ (A |^ kl) c=
(A |^ (m, n)) ^^ (A |^ (k, l)) by A3, FLANG_1:18;
then (A |^ (mn + kl)) c= (A |^ (m, n)) ^^ (A |^ (k, l)) by FLANG_1:34;
hence x in (A |^ (m, n)) ^^ (A |^ (k, l)) by A1, A2;
end;
hence thesis by A, TARSKI:2;
end;
theorem ThRange180:
A |^ (m + 1, n + 1) = (A |^ (m, n)) ^^ A
proof
per cases;
suppose m <= n;
hence A |^ (m + 1, n + 1) = (A |^ (m, n)) ^^ (A |^ (1, 1)) by ThRange190
.= (A |^ (m, n)) ^^ (A |^ 1) by ThRange40
.= (A |^ (m, n)) ^^ A by FLANG_1:26;
end;
suppose
A: m > n;
then A |^ (m, n) = {} by ThRange30;
then
A1: (A |^ (m, n)) ^^ A = {} by FLANG_1:13;
m + 1 > n + 1 by A, XREAL_1:10;
hence A |^ (m + 1, n + 1) = (A |^ (m, n)) ^^ A by A1, ThRange30;
end;
end;
theorem ThRange200:
(A |^ (m, n)) ^^ (A |^ (k, l)) = (A |^ (k, l)) ^^ (A |^ (m, n))
proof
per cases;
suppose
A: m <= n & k <= l;
thus (A |^ (m, n)) ^^ (A |^ (k, l))
= A |^ (m + k, n + l) by A, ThRange190
.= (A |^ (k, l)) ^^ (A |^ (m, n)) by A, ThRange190;
end;
suppose m > n;
then A |^ (m, n) = {} by ThRange30;
then (A |^ (m, n)) ^^ (A |^ (k, l)) = {} &
(A |^ (k, l)) ^^ (A |^ (m, n)) = {} by FLANG_1:13;
hence thesis;
end;
suppose k > l;
then A |^ (k, l) = {} by ThRange30;
then (A |^ (m, n)) ^^ (A |^ (k, l)) = {} &
(A |^ (k, l)) ^^ (A |^ (m, n)) = {} by FLANG_1:13;
hence thesis;
end;
end;
theorem ThRange210:
(A |^ (m, n)) |^ k = A |^ (m * k, n * k)
proof
per cases;
suppose
Aa: m <= n;
defpred P[Nat] means (A |^ (m, n)) |^ $1 = A |^ (m * $1, n * $1);
A: P[0]
proof
thus (A |^ (m, n)) |^ 0 = {<%>E} by FLANG_1:25
.= A |^ 0 by FLANG_1:25
.= A |^ (m * 0, n * 0) by ThRange40;
end;
B: now
let k;
Ab: m * k <= n * k by Aa, XREAL_1:66;
assume
B1: P[k];
(A |^ (m, n)) |^ (k + 1)
= (A |^ (m * k, n * k)) ^^ (A |^ (m, n)) by B1, FLANG_1:24
.= A |^ (m * k + m, n * k + n) by Aa, Ab, ThRange190
.= A |^ (m * (k + 1), n * (k + 1));
hence P[k + 1];
end;
for k holds P[k] from NAT_1:sch 2(A, B);
hence thesis;
end;
suppose
C: k = 0;
hence (A |^ (m, n)) |^ k = {<%>E} by FLANG_1:25
.= A |^ 0 by FLANG_1:25
.= A |^ (m * k, n * k) by C, ThRange40;
end;
suppose
D: m > n & k <> 0;
D1: k > 0 by D;
A |^ (m, n) = {} by D, ThRange30;
then
D2: (A |^ (m, n)) |^ k = {} by D1, FLANG_1:28;
m * k > n * k by D, D1, XREAL_1:70;
hence thesis by D2, ThRange30;
end;
end;
theorem ThRange211:
(A |^ (k + 1)) |^ (m, n) c= ((A |^ k) |^ (m, n)) ^^ (A |^ (m, n))
proof
let x;
assume x in (A |^ (k + 1)) |^ (m, n);
then consider mn such that
A2: m <= mn & mn <= n & x in (A |^ (k + 1)) |^ mn by ThRange10;
x in A |^ ((k + 1) * mn) by A2, FLANG_1:35;
then x in A |^ (k * mn + mn);
then x in (A |^ (k * mn)) ^^ (A |^ mn) by FLANG_1:34;
then
A4: x in ((A |^ k) |^ mn) ^^ (A |^ mn) by FLANG_1:35;
(A |^ k) |^ mn c= (A |^ k) |^ (m, n) by A2, ThRange20;
then ((A |^ k) |^ mn) ^^ (A |^ mn) c=
((A |^ k) |^ (m, n)) ^^ (A |^ mn) by FLANG_1:18;
then
A5: x in ((A |^ k) |^ (m, n)) ^^ (A |^ mn) by A4;
A |^ mn c= A |^ (m, n) by A2, ThRange20;
then ((A |^ k) |^ (m, n)) ^^ (A |^ mn) c=
((A |^ k) |^ (m, n)) ^^ (A |^ (m, n)) by FLANG_1:18;
hence x in ((A |^ k) |^ (m, n)) ^^ (A |^ (m, n)) by A5;
end;
theorem ThRange220:
(A |^ k) |^ (m, n) c= A |^ (k * m, k * n)
proof
per cases;
suppose
A: m <= n;
defpred P[Nat] means (A |^ $1) |^ (m, n) c= A |^ ($1 * m, $1 * n);
B: P[0]
proof
(A |^ 0) |^ (m, n) = {<%>E} |^ (m, n) by FLANG_1:25
.= {<%>E} by A, ThRange130
.= A |^ 0 by FLANG_1:25
.= A |^ (0 * m, 0 * n) by ThRange40;
hence thesis;
end;
C: now
let l;
C0: l * m <= l * n by A, XREAL_1:66;
assume
C1: P[l];
(A |^ (l + 1)) |^ (m, n)
c= ((A |^ l) |^ (m, n)) ^^ (A |^ (m, n)) by ThRange211;
then
C2: (A |^ (l + 1)) |^ (m, n)
c= ((A |^ l) |^ (m, n)) ^^ ((A |^ 1) |^ (m, n)) by FLANG_1:26;
C3: ((A |^ l) |^ (m, n)) ^^ ((A |^ 1) |^ (m, n))
c= (A |^ (l * m, l * n)) ^^ ((A |^ 1) |^ (m, n)) by C1, FLANG_1:18;
(A |^ (l * m, l * n)) ^^ ((A |^ 1) |^ (m, n))
= (A |^ (l * m, l * n)) ^^ (A |^ (m, n)) by FLANG_1:26
.= A |^ (l * m + m, l * n + n) by A, C0, ThRange190
.= A |^ ((l + 1) * m, (l + 1) * n);
hence P[l + 1] by C2, C3, XBOOLE_1:1;
end;
for l holds P[l] from NAT_1:sch 2(B, C);
hence thesis;
end;
suppose m > n;
then (A |^ k) |^ (m, n) = {} by ThRange30;
hence thesis by XBOOLE_1:2;
end;
end;
theorem
(A |^ k) |^ (m, n) c= (A |^ (m, n)) |^ k
proof
(A |^ (m, n)) |^ k = A |^ (m * k, n * k) by ThRange210;
hence thesis by ThRange220;
end;
theorem
(A |^ (k + l)) |^ (m, n) c= ((A |^ k) |^ (m, n)) ^^ ((A |^ l) |^ (m, n))
proof
let x;
assume x in (A |^ (k + l)) |^ (m, n);
then consider mn such that
A: m <= mn & mn <= n & x in (A |^ (k + l)) |^ mn by ThRange10;
x in A |^ ((k + l) * mn) by A, FLANG_1:35;
then x in A |^ (k * mn + l * mn);
then x in (A |^ (k * mn)) ^^ (A |^ (l * mn)) by FLANG_1:34;
then consider a, b such that
B: a in A |^ (k * mn) & b in A |^ (l * mn) & x = a ^ b by FLANG_1:def 1;
a in (A |^ k) |^ mn & b in (A |^ l) |^ mn by B, FLANG_1:35;
then a in (A |^ k) |^ (m, n) & b in (A |^ l) |^ (m, n) by A, ThRange10;
hence x in (A |^ k) |^ (m, n) ^^ (A |^ l) |^ (m, n) by B, FLANG_1:def 1;
end;
theorem ThRange250:
A |^ (0, 0) = {<%>E}
proof
thus A |^ (0, 0) = A |^ 0 by ThRange40
.= {<%>E} by FLANG_1:25;
end;
theorem ThRange260:
A |^ (0, 1) = {<%>E} \/ A
proof
thus A |^ (0, 1) = A |^ 0 \/ A |^ (0 + 1) by ThRange100
.= {<%>E} \/ A |^ 1 by FLANG_1:25
.= {<%>E} \/ A by FLANG_1:26;
end;
theorem
A |^ (1, 1) = A
proof
thus A |^ (1, 1) = A |^ 1 by ThRange40
.= A by FLANG_1:26;
end;
theorem
A |^ (0, 2) = {<%>E} \/ A \/ (A ^^ A)
proof
thus A |^ (0, 2) = A |^ (0, 1) \/ A |^ (1 + 1) by ThRange80
.= {<%>E} \/ A \/ A |^ (1 + 1) by ThRange260
.= {<%>E} \/ A \/ (A ^^ A) by FLANG_1:27;
end;
theorem
A |^ (1, 2) = A \/ (A ^^ A)
proof
thus A |^ (1, 2) = A |^ 1 \/ A |^ (1 + 1) by ThRange100
.= A \/ A |^ 2 by FLANG_1:26
.= A \/ (A ^^ A) by FLANG_1:27;
end;
theorem
A |^ (2, 2) = A ^^ A
proof
thus A |^ (2, 2) = A |^ 2 by ThRange40
.= A ^^ A by FLANG_1:27;
end;
theorem ThRange302:
m > 0 & m <> n & A |^ (m, n) = {x} implies
for mn st m <= mn & mn <= n holds A |^ mn = {x}
proof
assume
A1: m > 0 & m <> n & A |^ (m, n) = {x};
given mn such that
A2: m <= mn & mn <= n & A |^ mn <> {x};
per cases;
suppose A |^ mn = {};
then
B1: A = {} by FLANG_1:28;
x in A |^ (m, n) by A1, TARSKI:def 1;
then consider i such that
B2: m <= i & i <= n & x in A |^ i by ThRange10;
thus contradiction by A1, B1, B2, FLANG_1:28;
end;
suppose A |^ mn <> {};
then consider y such that
B1: y in A |^ mn & y <> x by A2, ZFMISC_1:41;
y in A |^ (m, n) by B1, A2, ThRange10;
hence contradiction by TARSKI:def 1, A1, B1;
end;
end;
theorem ThRange310:
m <> n & A |^ (m, n) = {x} implies x = <%>E
proof
assume
A: m <> n & A |^ (m, n) = {x};
per cases;
suppose m > n;
hence thesis by A, ThRange30;
end;
suppose
B: m = 0 & m <= n;
then {<%>E} = A |^ m by FLANG_1:25;
then <%>E in A |^ m by TARSKI:def 1;
then <%>E in A |^ (m, n) by B, ThRange10;
hence thesis by A, TARSKI:def 1;
end;
suppose m > 0 & m <= n;
then A |^ m = {x} & A |^ n = {x} by A, ThRange302;
hence thesis by A, LmLang32;
end;
end;
theorem ThRange320:
<%x%> in A |^ (m, n) iff
<%x%> in A & m <= n & ((<%>E in A & (n > 0)) or (m <= 1 & 1 <= n))
proof
thus <%x%> in A |^ (m, n) implies
<%x%> in A & m <= n & ((<%>E in A & (n > 0)) or (m <= 1 & 1 <= n))
proof
assume
A: <%x%> in A |^ (m, n);
then consider mn such that
B: m <= mn & mn <= n & <%x%> in A |^ mn by ThRange10;
thus thesis by A, B, LmLang31, ThRange30;
end;
assume
A: <%x%> in A & m <= n & ((<%>E in A & (n > 0)) or (m <= 1 & 1 <= n));
per cases by A;
suppose <%>E in A & (n > 0);
then A c= A |^ n by FLANG_1:36;
hence thesis by A, ThRange10;
end;
suppose
B: m <= 1 & 1 <= n;
<%x%> in A |^ 1 by A, FLANG_1:26;
hence thesis by B, ThRange10;
end;
end;
theorem
(A /\ B) |^ (m, n) c= (A |^ (m, n)) /\ (B |^ (m, n))
proof
let x;
assume x in (A /\ B) |^ (m, n);
then consider mn such that
A: m <= mn & mn <= n & x in (A /\ B) |^ mn by ThRange10;
(A /\ B) |^ mn c= (A |^ mn) /\ (B |^ mn) by FLANG_1:40;
then x in A |^ mn & x in B |^ mn by A, XBOOLE_0:def 3;
then x in A |^ (m, n) & x in B |^ (m, n) by A, ThRange10;
hence x in (A |^ (m, n)) /\ (B |^ (m, n)) by XBOOLE_0:def 3;
end;
theorem
(A |^ (m, n)) \/ (B |^ (m, n)) c= (A \/ B) |^ (m, n)
proof
let x;
assume
A: x in (A |^ (m, n)) \/ (B |^ (m, n));
per cases by A, XBOOLE_0:def 2;
suppose x in A |^ (m, n);
then consider mn such that
B: m <= mn & mn <= n & x in A |^ mn by ThRange10;
C: x in (A |^ mn) \/ (B |^ mn) by B, XBOOLE_0:def 2;
(A |^ mn) \/ (B |^ mn) c= (A \/ B) |^ mn by FLANG_1:39;
hence x in (A \/ B) |^ (m, n) by B, C, ThRange10;
end;
suppose x in B |^ (m, n);
then consider mn such that
B: m <= mn & mn <= n & x in B |^ mn by ThRange10;
C: x in (A |^ mn) \/ (B |^ mn) by B, XBOOLE_0:def 2;
(A |^ mn) \/ (B |^ mn) c= (A \/ B) |^ mn by FLANG_1:39;
hence x in (A \/ B) |^ (m, n) by B, C, ThRange10;
end;
end;
theorem
(A |^ (m, n)) |^ (k, l) c= A |^ (m * k, n * l)
proof
let x;
assume x in (A |^ (m, n)) |^ (k, l);
then consider kl such that
A1: k <= kl & kl <= l & x in (A |^ (m, n)) |^ kl by ThRange10;
A2:
x in A |^ (m * kl, n * kl) by A1, ThRange210;
m * k <= m * kl & n * kl <= n * l by A1, NAT_1:4;
then A |^ (m * kl, n * kl) c= A |^ (m * k, n * l) by ThRange50;
hence x in A |^ (m * k, n * l) by A2;
end;
theorem
m <= n & <%>E in B implies A c= A ^^ (B |^ (m, n)) & A c= (B |^ (m, n)) ^^ A
proof
assume m <= n & <%>E in B;
then <%>E in B |^ (m, n) by ThRange150;
hence thesis by FLANG_1:17;
end;
theorem
m <= n & k <= l & A c= C |^ (m, n) & B c= C |^ (k, l) implies
A ^^ B c= C |^ (m + k, n + l)
proof
assume
A: m <= n & k <= l & A c= C |^ (m, n) & B c= C |^ (k, l);
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 FLANG_1:def 1;
a ^ b in C |^ (m, n) ^^ C |^ (k, l) by FLANG_1:def 1, A, B;
hence x in C |^ (m + k, n + l) by A, B, ThRange190;
end;
end;
theorem
(A |^ (m, n))* c= A*
proof
let x;
assume x in (A |^ (m, n))*;
then consider k such that
B: x in A |^ (m, n) |^ k by FLANG_1:42;
C:
A |^ (m, n) |^ k = A |^ (m * k, n * k) by ThRange210;
A |^ (m * k, n * k) c= A* by ThRange140;
hence x in A* by B, C;
end;
theorem
(A*) |^ (m, n) c= A*
proof
let x;
assume x in (A*) |^ (m, n);
then consider mn such that
A: m <= mn & mn <= n & x in (A*) |^ mn by ThRange10;
(A*) |^ mn c= A* by FLANG_1:66;
hence x in A* by A;
end;
theorem
m <= n & n > 0 implies (A*) |^ (m, n) = A*
proof
assume
A: m <= n & n > 0;
<%>E in A* by FLANG_1:49;
hence (A*) |^ (m, n) = (A*) |^ n by A, ThRange160
.= A* by A, FLANG_1:67;
end;
theorem
m <= n & n > 0 & <%>E in A implies (A |^ (m, n))* = A*
proof
assume
A: m <= n & n > 0 & <%>E in A;
thus (A |^ (m, n))* = (A |^ n)* by A, ThRange160
.= A* by A, LmLang70;
end;
theorem
m <= n & <%>E in A implies (A |^ (m, n))* = (A*) |^ (m, n)
proof
assume
A: m <= n & <%>E in A;
then
B: (A |^ (m, n))* = (A |^ n)* by ThRange160;
<%>E in A* by FLANG_1:49;
then A* |^ (m, n) = A* |^ n by A, ThRange160;
hence thesis by A, B, LmLang80;
end;
theorem ThRange440:
A c= B* implies A |^ (m, n) c= B*
proof
assume
A: A c= B*;
thus thesis
proof
let x;
assume x in A |^ (m, n);
then consider mn such that
B: m <= mn & mn <= n & x in A |^ mn by ThRange10;
A |^ mn c= B* by A, FLANG_1:60;
hence x in B* by B;
end;
end;
theorem
A c= B* implies B* = (B \/ (A |^ (m, n)))*
proof
assume A c= B*;
then A |^ (m, n) c= B* by ThRange440;
hence thesis by FLANG_1:68;
end;
theorem ThRange450:
A |^ (m, n) ^^ (A*) = A* ^^ (A |^ (m, n))
proof
A0:
A |^ (m, n) ^^ (A*) c= A* ^^ (A |^ (m, n))
proof
let x;
assume x in A |^ (m, n) ^^ (A*);
then consider a, b such that
A1: a in A |^ (m, n) & b in A* & x = a ^ b by FLANG_1:def 1;
consider mn such that
A2: m <= mn & mn <= n & a in A |^ mn by A1, ThRange10;
consider k such that
A3: b in A |^ k by A1, FLANG_1:42;
a ^ b in A |^ (k + mn) by A2, A3, FLANG_1:41;
then
A4: a ^ b in A |^ k ^^ (A |^ mn) by FLANG_1:34;
A |^ k c= A* & A |^ mn c= A |^ (m, n) by FLANG_1:43, ThRange20, A2;
then A |^ k ^^ (A |^ mn) c= A* ^^ (A |^ (m, n)) by FLANG_1:18;
hence x in A* ^^ (A |^ (m, n)) by A1, A4;
end;
A* ^^ (A |^ (m, n)) c= A |^ (m, n) ^^ (A*)
proof
let x;
assume x in A* ^^ (A |^ (m, n));
then consider a, b such that
A1: a in A* & b in A |^ (m, n) & x = a ^ b by FLANG_1:def 1;
consider mn such that
A2: m <= mn & mn <= n & b in A |^ mn by A1, ThRange10;
consider k such that
A3: a in A |^ k by A1, FLANG_1:42;
a ^ b in A |^ (mn + k) by A2, A3, FLANG_1:41;
then
A4: a ^ b in A |^ mn ^^ (A |^ k) by FLANG_1:34;
A |^ k c= A* & A |^ mn c= A |^ (m, n) by FLANG_1:43, ThRange20, A2;
then A |^ mn ^^ (A |^ k) c= A |^ (m, n) ^^ (A*) by FLANG_1:18;
hence x in A |^ (m, n) ^^ (A*) by A1, A4;
end;
hence thesis by A0, XBOOLE_0:def 10;
end;
theorem
<%>E in A & m <= n implies A* = A* ^^ (A |^ (m, n))
proof
assume
A: <%>E in A & m <= n;
defpred P[Nat] means A* = A* ^^ (A |^ (m, m + $1));
B1:
P[0]
proof
thus A* = A* ^^ (A |^ m) by A, FLANG_1:56
.= A* ^^ (A |^ (m, m + 0)) by ThRange40;
end;
B2:
now
let i;
assume
B2a: P[i];
m <= m + (i + 1) by NAT_1:11;
then A |^ (m, m + (i + 1))
= A |^ (m, m + i) \/ (A |^ (m + i + 1)) by ThRange80;
then A* ^^ (A |^ (m, m + (i + 1)))
= A* \/ (A* ^^ (A |^ (m + i + 1))) by B2a, FLANG_1:21
.= A* \/ A* by A, FLANG_1:56;
hence P[i + 1];
end;
C:
for i holds P[i] from NAT_1:sch 2(B1, B2);
consider k such that
D: m + k = n by A, NAT_1:10;
thus thesis by C, D;
end;
theorem ThRange470:
A |^ (m, n) |^ k c= A*
proof
let x;
assume
A: x in A |^ (m, n) |^ k;
A |^ (m, n) c= A* by ThRange140;
then A |^ (m, n) |^ k c= A* by FLANG_1:60;
hence x in A* by A;
end;
theorem ThRange480:
A |^ k |^ (m, n) c= A*
proof
let x;
assume x in A |^ k |^ (m, n);
then consider mn such that
A: m <= mn & mn <= n & x in A |^ k |^ mn by ThRange10;
B:
x in A |^ (k * mn) by A, FLANG_1:35;
A |^ (k * mn) c= A* by FLANG_1:43;
hence x in A* by B;
end;
theorem
m <= n implies (A |^ m)* c= (A |^ (m, n))*
proof
assume m <= n;
then A |^ m c= A |^ (m, n) by ThRange20;
hence thesis by FLANG_1:62;
end;
theorem ThRange500:
(A |^ (m, n)) |^ (k, l) c= A*
proof
let x;
assume x in (A |^ (m, n)) |^ (k, l);
then consider kl such that
A: k <= kl & kl <= l & x in (A |^ (m, n)) |^ kl by ThRange10;
(A |^ (m, n)) |^ kl c= A* by ThRange470;
hence x in A* by A;
end;
theorem ThRange520:
<%>E in A & k <= n & l <= n implies A |^ (k, n) = A |^ (l, n)
proof
assume
A: <%>E in A & k <= n & l <= n;
hence A |^ (k, n) = A |^ n by ThRange160
.= A |^ (l, n) by A, ThRange160;
end;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Optional Occurrence
:: Definition of ?
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, A;
func A? -> Subset of E^omega equals
union { B: ex k st k <= 1 & B = A |^ k };
coherence
proof
defpred P[set] means ex k st k <= 1 & $1 = A |^ k;
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;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Optional Occurrence
:: Properties of ?
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem ThOpt10:
x in A? iff ex k st k <= 1 & x in A |^ k
proof
thus x in A? implies ex k st k <= 1 & x in A |^ k
proof
assume x in A?;
then consider X such that
A1: x in X and
A2: X in { B: ex k st k <= 1 & B = A |^ k } by TARSKI:def 4;
defpred P[set] means ex k st k <= 1 & $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 k such that
B: k <= 1 & x in A |^ k;
defpred P[set] means ex k st k <= 1 & $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
n <= 1 implies A |^ n c= A?
proof
assume n <= 1;
then for x holds x in A |^ n implies x in A? by ThOpt10;
hence thesis by TARSKI:def 3;
end;
theorem ThOpt40:
A? = (A |^ 0) \/ (A |^ 1)
proof
now
let x;
x in A? iff ex k st (k = 0 or k = 1) & x in A |^ k
proof
thus x in A? implies ex k st (k = 0 or k = 1) & x in A |^ k
proof
assume x in A?;
then consider k such that
A: k <= 1 & x in A |^ k by ThOpt10;
(k = 0 or k = 1) by A, NAT_1:26;
hence thesis by A;
end;
given k such that
B: (k = 0 or k = 1) & x in A |^ k;
thus thesis by B, ThOpt10;
end;
hence x in A? iff x in A |^ 0 or x in A |^ 1;
end;
hence thesis by XBOOLE_0:def 2;
end;
theorem ThOpt50:
A? = {<%>E} \/ A
proof
A |^ 0 = {<%>E} & A |^ 1 = A by FLANG_1:25, FLANG_1:26;
hence thesis by ThOpt40;
end;
theorem
A c= A?
proof
A? = {<%>E} \/ A by ThOpt50;
hence thesis by XBOOLE_1:7;
end;
theorem ThOpt60:
x in A? iff x = <%>E or x in A
proof
x in A? iff x in {<%>E} \/ A by ThOpt50;
then x in A? iff x in {<%>E} or x in A by XBOOLE_0:def 2;
hence thesis by TARSKI:def 1;
end;
theorem ThOpt70:
A? = A |^ (0, 1)
proof
thus A? = (A |^ 0) \/ (A |^ (0 + 1)) by ThOpt40
.= A |^ (0, 1) by ThRange100;
end;
theorem ThOpt80:
A? = A iff <%>E in A
proof
thus A? = A implies <%>E in A
proof
assume A? = A;
then A = {<%>E} \/ A by ThOpt50;
hence thesis by ZFMISC_1:45;
end;
assume <%>E in A;
then A = {<%>E} \/ A by ZFMISC_1:46;
hence thesis by ThOpt50;
end;
registration let E, A;
cluster A? -> non empty;
coherence
proof
<%>E in A? by ThOpt60;
hence thesis;
end;
end;
theorem
A?? = A?
proof
<%>E in A? by ThOpt60;
hence thesis by ThOpt80;
end;
theorem
A c= B implies A? c= B?
proof
assume A c= B;
then A |^ (0, 1) c= B |^ (0, 1) by ThRange110;
then A? c= B |^ (0, 1) by ThOpt70;
hence thesis by ThOpt70;
end;
theorem
x in A & x <> <%>E implies A? <> {<%>E}
proof
assume
A: x in A & x <> <%>E;
A? = A |^ (0, 1) by ThOpt70;
hence thesis by A, ThRange120;
end;
theorem
A? = {<%>E} iff A = {} or A = {<%>E}
proof
A? = A |^ (0, 1) by ThOpt70;
hence thesis by ThRange130;
end;
theorem
(A*)? = A* & (A?)* = A*
proof
A:
<%>E in A* by FLANG_1:49;
thus (A*)? = {<%>E} \/ (A*) by ThOpt50
.= A* by A, ZFMISC_1:46;
thus (A?)* = ({<%>E} \/ A)* by ThOpt50
.= A* by A, FLANG_1:69;
end;
theorem
A? c= A*
proof
A? = A |^ (0, 1) by ThOpt70;
hence thesis by ThRange140;
end;
theorem
(A /\ B)? = (A?) /\ (B?)
proof
thus (A /\ B)? = {<%>E} \/ (A /\ B) by ThOpt50
.= ({<%>E} \/ A) /\ ({<%>E} \/ B) by XBOOLE_1:24
.= (A?) /\ ({<%>E} \/ B) by ThOpt50
.= (A?) /\ (B?) by ThOpt50;
end;
theorem
(A?) \/ (B?) = (A \/ B)?
proof
thus (A \/ B)? = {<%>E} \/ (A \/ B) by ThOpt50
.= (A \/ {<%>E}) \/ (B \/ {<%>E}) by XBOOLE_1:5
.= (A?) \/ (B \/ {<%>E}) by ThOpt50
.= (A?) \/ (B?) by ThOpt50;
end;
theorem
A? = {x} implies x = <%>E
proof
A? = A |^ (0, 1) by ThOpt70;
hence thesis by ThRange310;
end;
theorem
<%x%> in A? iff <%x%> in A
proof
A? = A |^ (0, 1) by ThOpt70;
hence thesis by ThRange320;
end;
theorem
(A?) ^^ A = A ^^ (A?)
proof
A? = A |^ (0, 1) by ThOpt70;
hence thesis by ThRange170;
end;
theorem
(A?) ^^ A = A |^ (1, 2)
proof
A? = A |^ (0, 1) by ThOpt70;
then (A?) ^^ A = A |^ (0 + 1, 1 + 1) by ThRange180;
hence thesis;
end;
theorem ThOpt210:
(A?) ^^ (A?) = A |^ (0, 2)
proof
A? = A |^ (0, 1) by ThOpt70;
then (A?) ^^ (A?) = A |^ (0 + 0, 1 + 1) by ThRange190;
hence thesis;
end;
theorem ThOpt220:
(A?) |^ k = (A?) |^ (0, k)
proof
<%>E in A? by ThOpt60;
hence thesis by ThRange160;
end;
theorem ThOpt230:
(A?) |^ k = A |^ (0, k)
proof
defpred P[Nat] means (A?) |^ $1 = A |^ (0, $1);
A:
P[0]
proof
thus (A?) |^ 0 = {<%>E} by FLANG_1:25
.= A |^ (0, 0) by ThRange250;
end;
B:
now
let k;
assume
C: P[k];
(A?) |^ (k + 1) = ((A?) |^ k) ^^ ((A?) |^ 1) by FLANG_1:34
.= A |^ (0, k) ^^ (A?) by C, FLANG_1:26
.= A |^ (0, k) ^^ (A |^ (0, 1)) by ThOpt70
.= A |^ (0 + 0, k + 1) by ThRange190;
hence P[k + 1];
end;
for k holds P[k] from NAT_1:sch 2(A, B);
hence thesis;
end;
theorem ThOpt340:
m <= n implies A? |^ (m, n) = A? |^ (0, n)
proof
assume
A: m <= n;
<%>E in A? by ThOpt60;
hence thesis by A, ThRange520;
end;
theorem ThOpt350:
A? |^ (0, n) = A |^ (0, n)
proof
thus A? |^ (0, n) = A? |^ n by ThOpt220
.= A |^ (0, n) by ThOpt230;
end;
theorem ThOpt360:
m <= n implies A? |^ (m, n) = A |^ (0, n)
proof
assume m <= n;
hence A? |^ (m, n) = A? |^ (0, n) by ThOpt340
.= A |^ (0, n) by ThOpt350;
end;
theorem
(A |^ (1, n))? = A |^ (0, n)
proof
thus (A |^ (1, n))? = {<%>E} \/ (A |^ (1, n)) by ThOpt50
.= A |^ (0, 0) \/ (A |^ (0 + 1, n)) by ThRange250
.= A |^ (0, n) by ThRange70;
end;
theorem
<%>E in A & <%>E in B implies A? c= A ^^ B & A? c= B ^^ A
proof
assume
A: <%>E in A & <%>E in B;
then
B: A c= A ^^ B & A c= B ^^ A by FLANG_1:17;
<%>E in A ^^ B & <%>E in B ^^ A by A, FLANG_1:16;
then {<%>E} c= A ^^ B & {<%>E} c= B ^^ A by ZFMISC_1:37;
then {<%>E} \/ A c= A ^^ B & {<%>E} \/ A c= B ^^ A by B, XBOOLE_1:8;
hence thesis by ThOpt50;
end;
theorem
A c= A ^^ (B?) & A c= (B?) ^^ A
proof
<%>E in B? by ThOpt60;
hence thesis by FLANG_1:17;
end;
theorem
A c= C? & B c= C? implies A ^^ B c= C |^ (0, 2)
proof
assume A c= C? & B c= C?;
then A ^^ B c= (C?) ^^ (C?) by FLANG_1:18;
hence thesis by ThOpt210;
end;
theorem
<%>E in A & n > 0 implies A? c= A |^ n
proof
assume <%>E in A & n > 0;
then <%>E in A |^ n & A c= A |^ n by FLANG_1:31, FLANG_1:36;
then {<%>E} c= A |^ n & A c= A |^ n by ZFMISC_1:37;
then {<%>E} \/ A c= A |^ n by XBOOLE_1:8;
hence thesis by ThOpt50;
end;
theorem
(A?) ^^ (A |^ k) = (A |^ k) ^^ (A?)
proof
thus (A?) ^^ (A |^ k)
= ({<%>E} \/ A) ^^ (A |^ k) by ThOpt50
.= ({<%>E} ^^ (A |^ k)) \/ (A ^^ (A |^ k)) by FLANG_1:21
.= ({<%>E} ^^ (A |^ k)) \/ ((A |^ k) ^^ A) by FLANG_1:33
.= (A |^ k) \/ ((A |^ k) ^^ A) by FLANG_1:14
.= ((A |^ k) ^^ {<%>E}) \/ ((A |^ k) ^^ A) by FLANG_1:14
.= (A |^ k) ^^ (A \/ {<%>E}) by FLANG_1:21
.= (A |^ k) ^^ (A?) by ThOpt50;
end;
theorem ThOpt280:
A c= B* implies A? c= B*
proof
assume A c= B*;
then A |^ (0, 1) c= B* by ThRange440;
hence thesis by ThOpt70;
end;
theorem
A c= B* implies B* = (B \/ (A?))*
proof
assume A c= B*;
then A? c= B* by ThOpt280;
hence thesis by FLANG_1:68;
end;
theorem
A? ^^ (A*) = A* ^^ (A?)
proof
thus A? ^^ (A*) = A |^ (0, 1) ^^ (A*) by ThOpt70
.= A* ^^ (A |^ (0, 1)) by ThRange450
.= A* ^^ (A?) by ThOpt70;
end;
theorem
A? ^^ (A*) = A*
proof
A:
A ^^ (A*) c= A* by FLANG_1:54;
thus A? ^^ (A*) = ({<%>E} \/ A) ^^ (A*) by ThOpt50
.= {<%>E} ^^ (A*) \/ A ^^ (A*) by FLANG_1:21
.= A* \/ A ^^ (A*) by FLANG_1:14
.= A* by A, XBOOLE_1:12;
end;
theorem
A? |^ k c= A*
proof
A? |^ k = (A |^ (0, 1)) |^ k by ThOpt70;
hence thesis by ThRange470;
end;
theorem
(A |^ k)? c= A*
proof
(A |^ k)? = (A |^ k) |^ (0, 1) by ThOpt70;
hence thesis by ThRange480;
end;
theorem
(A?) ^^ (A |^ (m, n)) = (A |^ (m, n)) ^^ (A?)
proof
(A |^ (0, 1)) ^^ (A |^ (m, n))
= (A |^ (m, n)) ^^ (A |^ (0, 1)) by ThRange200;
then (A?) ^^ (A |^ (m, n)) = (A |^ (m, n)) ^^ (A |^ (0, 1)) by ThOpt70;
hence thesis by ThOpt70;
end;
theorem
(A?) ^^ (A |^ k) = A |^ (k, k + 1)
proof
(A |^ (0, 1)) ^^ (A |^ k) = (A |^ (0, 1)) ^^ (A |^ (k, k)) by ThRange40
.= A |^ (0 + k, 1 + k) by ThRange190;
hence thesis by ThOpt70;
end;
theorem
A? |^ (m, n) c= A*
proof
per cases;
suppose m <= n;
then A? |^ (m, n) = A |^ (0, n) by ThOpt360;
hence thesis by ThRange140;
end;
suppose m > n;
then A? |^ (m, n) = {} by ThRange30;
hence thesis by XBOOLE_1:2;
end;
end;
theorem
(A |^ (m, n))? c= A*
proof
(A |^ (m, n))? = (A |^ (m, n)) |^ (0, 1) by ThOpt70;
hence thesis by ThRange500;
end;
theorem
A? = (A \ {<%>E})?
proof
thus A? = {<%>E} \/ A by ThOpt50
.= {<%>E} \/ (A \ {<%>E}) by XBOOLE_1:39
.= (A \ {<%>E})? by ThOpt50;
end;
theorem
A c= B? implies A? c= B?
proof
assume
A: A c= B?;
<%>E in B? by ThOpt60;
then {<%>E} c= B? by ZFMISC_1:37;
then {<%>E} \/ A c= B? by A, XBOOLE_1:8;
hence thesis by ThOpt50;
end;
theorem
A c= B? implies B? = (B \/ A)?
proof
assume
A: A c= B?;
thus (B \/ A)? = {<%>E} \/ (B \/ A) by ThOpt50
.= ({<%>E} \/ B) \/ A by XBOOLE_1:4
.= B? \/ A by ThOpt50
.= B? by A, XBOOLE_1:12;
end;
Top
|