Artykuł ten zawiera dowody kilku faktów,
które uzupełniają materiał przedstawiony w [1].
Następnie, bazując na tej teorii, rozbudowuje narzędzia do
dowodzenia faktów na temat języków formalnych w ogólności,
a kwantyfikatorów wyrażeń regularnych w szczególności.
W tym artykule dwa kwantyfikatory są zdefiniowane a ich właściwości udowodnione:
od m do n wystąpień (lub suma przedziału potęg)
oraz wystąpienie opcjonalne. Mimo, że wystąpienie opcjonalne
jest przypadkiem szczególnym pierwszego operatora (od 0 do 1 wystąpień),
często definiowane jest w zastosowaniach wyrażeń regularnych jako oddzielny
operator - stąd jego definicja i dowody właściwości w artykule.
Notacja i terminologia zostały zaczerpnięte z [2].
Sekcje:
- Pojęcia wstępne
- Uzupełnienia do FLANG_1
- Suma przedziału potęg
- Wystąpienie opcjonalne
Bibliografia:
Identyfikator Mizar Mathematical Library: FLANG_2.
Abstrakt w wersji PDF: tutaj.
Motorola Software Group, 2007.
Pliki:
:: 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)?;
Góra
:: 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;
Góra
|
Mizar
