Jest to drugi artykuł na temat kwantyfikatorów w wyrażeniach regularnych.
[1] wprowadzał kwantyfikatory: od m do n wystąpień oraz wystąpienie opcjonalne.
W FLANG_3 zostały wprowadzone następujące kwantyfikatory:
co najmniej m wystąpień, domknięcie dodatnie (co najmniej jedno wystąpienie).
Notacja i terminologia zostały zaczerpnięte z [2],
natomiast niektóre właściwości wyrażeń regularnych z [3].
Sekcje:
 Pojęcia wstępne
 Co najmniej m wystąpień
 Domknięcie dodatnie
Bibliografia:
 [1] Michał Trybulec: "Kwantyfikatory w wyrażeniach regularnych  od m do n wystąpień", Formalized Mathematics, 2007
 [2] Larry Wall, Tom Christiansen, Jon Orwant: "Programming Perl, Third Edition", O'Reilly Media, 2000
 [3] William M. Waite, Gerhard Goos: "Konstrukcja kompilatorów", SpringerVerlag New York Inc., 1984
Identyfikator Mizar Mathematical Library: FLANG_3.
Abstrakt w wersji PDF: tutaj.
Motorola Software Group, 2007.
Pliki:
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Regular Expression Quantifiers  at least m Occurrences
:: Micha{\l} Trybulec
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
environ
vocabularies
BOOLE, FINSEQ_1, TARSKI, AFINSQ_1, MEASURE6, GROUP_1, ARYTM, SETFAM_1,
MODAL_1, FLANG_3, ALGSEQ_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, FLANG_2;
constructors
XXREAL_0, NAT_1, XREAL_0, CATALAN2, FLANG_1, FLANG_2;
registrations
SUBSET_1, RELSET_1, NAT_1, ORDINAL1, AFINSQ_1, XREAL_0, XBOOLE_0, ARYTM_3,
XXREAL_0;
requirements
NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions
TARSKI;
theorems
NAT_1, TARSKI, REAL_2, XBOOLE_0, XBOOLE_1, XREAL_1, ZFMISC_1, FLANG_1,
XXREAL_0, FLANG_2;
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, ab, bc 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;
theorem :: FLANG_3:1
B c= A* implies A* ^^ B c= A* & B ^^ (A*) c= A*;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: At least n Occurences
:: Definition of ^.. n
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, A, n;
func A ^.. n > Subset of E^omega equals
:: FLANG_3:def 1
union { B: ex m st n <= m & B = A ^ m };
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: At least n Occurences
:: Properties of ^.. n
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: FLANG_3:2
x in A ^.. n iff ex m st n <= m & x in A ^ m;
theorem :: FLANG_3:3
n <= m implies A ^ m c= A ^.. n;
theorem :: FLANG_3:4
A ^.. n = {} iff n > 0 & A = {};
theorem :: FLANG_3:5
m <= n implies A ^.. n c= A ^.. m;
theorem :: FLANG_3:6
k <= m implies A ^ (m, n) c= A ^.. k;
theorem :: FLANG_3:7
m <= n + 1 implies A ^ (m, n) \/ A ^.. (n + 1) = A ^.. m;
theorem :: FLANG_3:8
A ^ n \/ A ^.. (n + 1) = A ^.. n;
theorem :: FLANG_3:9
A ^.. n c= A*;
theorem :: FLANG_3:10
<%>E in A ^.. n iff n = 0 or <%>E in A;
theorem :: FLANG_3:11
A ^.. n = A* iff <%>E in A or n = 0;
theorem :: FLANG_3:12
A* = A ^ (0, n) \/ A ^.. (n + 1);
theorem :: FLANG_3:13
A c= B implies A ^.. n c= B ^.. n;
theorem :: FLANG_3:14
x in A & x <> <%>E implies A ^.. n <> {<%>E};
theorem :: FLANG_3:15
A ^.. n = {<%>E} iff A = {<%>E} or (n = 0 & A = {});
theorem :: FLANG_3:16
A ^.. (n + 1) = (A ^.. n) ^^ A;
theorem :: FLANG_3:17
(A ^.. m) ^^ (A*) = A ^.. m;
theorem :: FLANG_3:18
(A ^.. m) ^^ (A ^.. n) = A ^.. (m + n);
theorem :: FLANG_3:19
n > 0 implies (A ^.. m) ^ n = A ^.. (m * n);
theorem :: FLANG_3:20
(A ^.. n)* = (A ^.. n)?;
theorem :: FLANG_3:21
A c= C ^.. m & B c= C ^.. n implies A ^^ B c= C ^.. (m + n);
theorem :: FLANG_3:22
A ^.. (n + k) = (A ^.. n) ^^ (A ^ k);
theorem :: FLANG_3:23
A ^^ (A ^.. n) = (A ^.. n) ^^ A;
theorem :: FLANG_3:24
(A ^ k) ^^ (A ^.. n) = (A ^.. n) ^^ (A ^ k);
theorem :: FLANG_3:25
(A ^ (k, l)) ^^ (A ^.. n) = (A ^.. n) ^^ (A ^ (k, l));
theorem :: FLANG_3:26
<%>E in B implies A c= A ^^ (B ^.. n) & A c= (B ^.. n) ^^ A;
theorem :: FLANG_3:27
(A ^.. m) ^^ (A ^.. n) = (A ^.. n) ^^ (A ^.. m);
theorem :: FLANG_3:28
A c= B ^.. k & n > 0 implies A ^ n c= B ^.. k;
theorem :: FLANG_3:29
A c= B ^.. k & n > 0 implies A ^.. n c= B ^.. k;
theorem :: FLANG_3:30
A* ^^ A = A ^.. 1;
theorem :: FLANG_3:31
A* ^^ (A ^ k) = A ^.. k;
theorem :: FLANG_3:32
(A ^.. m) ^^ (A*) = A* ^^ (A ^.. m);
theorem :: FLANG_3:33
k <= l implies (A ^.. n) ^^ (A ^ (k, l)) = A ^.. (n + k);
theorem :: FLANG_3:34
k <= l implies A* ^^ (A ^ (k, l)) = A ^.. k;
theorem :: FLANG_3:35
(A ^ m) ^.. n c= A ^.. (m * n);
theorem :: FLANG_3:36
(A ^ m) ^.. n c= (A ^.. n) ^ m;
theorem :: FLANG_3:37
a in C ^.. m & b in C ^.. n implies a ^ b in C ^.. (m + n);
theorem :: FLANG_3:38
A ^.. k = {x} implies x = <%>E;
theorem :: FLANG_3:39
A c= B* implies A ^.. n c= B*;
theorem :: FLANG_3:40
A? c= A ^.. k iff k = 0 or <%>E in A;
theorem :: FLANG_3:41
A ^.. k ^^ (A?) = A ^.. k;
theorem :: FLANG_3:42
A ^.. k ^^ (A?) = A? ^^ (A ^.. k);
theorem :: FLANG_3:43
B c= A* implies A ^.. k ^^ B c= A ^.. k & B ^^ (A ^.. k) c= A ^.. k;
theorem :: FLANG_3:44
(A /\ B) ^.. k c= (A ^.. k) /\ (B ^.. k);
theorem :: FLANG_3:45
(A ^.. k) \/ (B ^.. k) c= (A \/ B) ^.. k;
theorem :: FLANG_3:46
<%x%> in A ^.. k iff <%x%> in A & (<%>E in A or k <= 1);
theorem :: FLANG_3:47
A c= B ^.. k implies B ^.. k = (B \/ A) ^.. k;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Positive Closure
:: Definition of +
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, A;
func A+ > Subset of E^omega equals
:: FLANG_3:def 2
union { B: ex n st n > 0 & B = A ^ n };
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Positive Closure
:: Properties of +
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem :: FLANG_3:48
x in A+ iff ex n st n > 0 & x in A ^ n;
theorem :: FLANG_3:49
n > 0 implies A ^ n c= A+;
theorem :: FLANG_3:50
A+ = A ^.. 1;
theorem :: FLANG_3:51
A+ = {} iff A = {};
theorem :: FLANG_3:52
A+ = (A*) ^^ A;
theorem :: FLANG_3:53
A* = {<%>E} \/ (A+);
theorem :: FLANG_3:54
A+ = A ^ (1, n) \/ A ^.. (n + 1);
theorem :: FLANG_3:55
A+ c= A*;
theorem :: FLANG_3:56
<%>E in A+ iff <%>E in A;
theorem :: FLANG_3:57
A+ = A* iff <%>E in A;
theorem :: FLANG_3:58
A c= B implies A+ c= B+;
theorem :: FLANG_3:59
A c= A+;
theorem :: FLANG_3:60
(A*)+ = A* & (A+)* = A*;
theorem :: FLANG_3:61
A c= B* implies A+ c= B*;
theorem :: FLANG_3:62
(A+)+ = A+;
theorem :: FLANG_3:63
x in A & x <> <%>E implies A+ <> {<%>E};
theorem :: FLANG_3:64
A+ = {<%>E} iff A = {<%>E};
theorem :: FLANG_3:65
(A+)? = A* & (A?)+ = A*;
theorem :: FLANG_3:66
a in C+ & b in C+ implies a ^ b in C+;
theorem :: FLANG_3:67
A c= C+ & B c= C+ implies A ^^ B c= C+;
theorem :: FLANG_3:68
A ^^ A c= A+;
theorem :: FLANG_3:69
A+ = {x} implies x = <%>E;
theorem :: FLANG_3:70
A ^^ (A+) = (A+) ^^ A;
theorem :: FLANG_3:71
(A ^ k) ^^ (A+) = (A+) ^^ (A ^ k);
theorem :: FLANG_3:72
(A ^ (m, n)) ^^ (A+) = A+ ^^ (A ^ (m, n));
theorem :: FLANG_3:73
<%>E in B implies A c= A ^^ (B+) & A c= (B+) ^^ A;
theorem :: FLANG_3:74
A+ ^^ (A+) = A ^.. 2;
theorem :: FLANG_3:75
A+ ^^ (A ^ k) = A ^.. (k + 1);
theorem :: FLANG_3:76
A+ ^^ A = A ^.. 2;
theorem :: FLANG_3:77
k <= l implies A+ ^^ (A ^ (k, l)) = A ^.. (k + 1);
theorem :: FLANG_3:78
A c= B+ & n > 0 implies A ^ n c= B+;
theorem :: FLANG_3:79
A+ ^^ (A?) = A? ^^ (A+);
theorem :: FLANG_3:80
A+ ^^ (A?) = A+;
theorem :: FLANG_3:81
A? c= A+ iff <%>E in A;
theorem :: FLANG_3:82
A c= B+ implies A+ c= B+;
theorem :: FLANG_3:83
A c= B+ implies B+ = (B \/ A)+;
theorem :: FLANG_3:84
n > 0 implies A ^.. n c= A+;
theorem :: FLANG_3:85
m > 0 implies A ^ (m, n) c= A+;
theorem :: FLANG_3:86
A* ^^ (A+) = A+ ^^ (A*);
theorem :: FLANG_3:87
A+ ^ k c= A ^.. k;
theorem :: FLANG_3:88
A+ ^ (m, n) c= A ^.. m;
theorem :: FLANG_3:89
A c= B+ & n > 0 implies A ^.. n c= B+;
theorem :: FLANG_3:90
A+ ^^ (A ^.. k) = A ^.. (k + 1);
theorem :: FLANG_3:91
A+ ^^ (A ^.. k) = A ^.. k ^^ (A+);
theorem :: FLANG_3:92
A+ ^^ (A*) = A+;
theorem :: FLANG_3:93
B c= A* implies A+ ^^ B c= A+ & B ^^ (A+) c= A+;
theorem :: FLANG_3:94
(A /\ B)+ c= (A+) /\ (B+);
theorem :: FLANG_3:95
(A+) \/ (B+) c= (A \/ B)+;
theorem :: FLANG_3:96
<%x%> in A+ iff <%x%> in A;
Góra
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Regular Expression Quantifiers  at least m Occurrences
:: Micha{\l} Trybulec
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
environ
vocabularies
BOOLE, FINSEQ_1, TARSKI, AFINSQ_1, MEASURE6, GROUP_1, ARYTM, SETFAM_1,
MODAL_1, FLANG_3, ALGSEQ_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, FLANG_2;
constructors
XXREAL_0, NAT_1, XREAL_0, CATALAN2, FLANG_1, FLANG_2;
registrations
SUBSET_1, RELSET_1, NAT_1, ORDINAL1, AFINSQ_1, XREAL_0, XBOOLE_0, ARYTM_3,
XXREAL_0;
requirements
NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions
TARSKI;
theorems
NAT_1, TARSKI, REAL_2, XBOOLE_0, XBOOLE_1, XREAL_1, ZFMISC_1, FLANG_1,
XXREAL_0, FLANG_2;
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, ab, bc 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;
theorem
B c= A* implies A* ^^ B c= A* & B ^^ (A*) c= A*
proof
assume B c= A*;
then A* ^^ B c= A* ^^ (A*) & B ^^ (A*) c= A* ^^ (A*) by FLANG_1:18;
hence thesis by FLANG_1:64;
end;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: At least n Occurences
:: Definition of ^.. n
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, A, n;
func A ^.. n > Subset of E^omega equals
union { B: ex m st n <= m & B = A ^ m };
coherence
proof
defpred P[set] means ex m st n <= m & $1 = A ^ m;
reconsider M = { B: P[B] } as SubsetFamily of E^omega from DOMAIN_1:sch 7;
union M is Subset of E^omega;
hence thesis;
end;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: At least n Occurences
:: Properties of ^.. n
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem ThPlus10:
x in A ^.. n iff ex m st n <= m & x in A ^ m
proof
thus x in A ^.. n implies ex m st n <= m & x in A ^ m
proof
assume x in A ^.. n;
then consider X such that
A1: x in X and
A2: X in { B: ex m st n <= m & B = A ^ m } by TARSKI:def 4;
defpred P[set] means ex m st n <= m & $1 = A ^ m;
A3: X in { B: P[B] } by A2;
P[X] from CARD_FIL:sch 1(A3);
hence thesis by A1;
end;
given m such that
B: n <= m & x in A ^ m;
defpred P[set] means ex m st n <= m & $1 = A ^ m;
consider B such that
D: x in B & P[B] by B;
reconsider A = { C : P[C] } as SubsetFamily of E^omega from DOMAIN_1:sch 7;
B in A by D;
hence thesis by D, TARSKI:def 4;
end;
theorem ThPlus20:
n <= m implies A ^ m c= A ^.. n
proof
assume n <= m;
then for x holds x in A ^ m implies x in A ^.. n by ThPlus10;
hence thesis by TARSKI:def 3;
end;
theorem ThPlus30:
A ^.. n = {} iff n > 0 & A = {}
proof
thus A ^.. n = {} implies n > 0 & A = {}
proof
assume that
A1: A ^.. n = {} and
A2: n <= 0 or A <> {};
A3: n <= 0 implies <%>E in A ^.. n
proof
assume n <= 0;
then
A3a: n = 0;
A ^ 0 c= A ^.. 0 by ThPlus20;
then {<%>E} c= A ^.. 0 by FLANG_1:25;
hence thesis by A3a, ZFMISC_1:37;
end;
A4: A <> {} implies A ^.. n <> {}
proof
assume
A4a: A <> {};
now
let m;
consider m such that
A4b: n <= m;
A ^ m <> {} by A4a, FLANG_1:28;
then consider x such that
A4c: x in A ^ m by XBOOLE_0:def 1;
thus A ^.. n <> {} by A4b, A4c, ThPlus10;
end;
hence thesis;
end;
thus contradiction by A1, A2, A3, A4;
end;
assume
B1: n > 0 & A = {};
now
let x;
assume x in A ^.. n;
then consider m such that
B2: n <= m & x in A ^ m by ThPlus10;
thus contradiction by B1, B2, FLANG_1:28;
end;
hence thesis by XBOOLE_0:def 1;
end;
theorem ThPlus40:
m <= n implies A ^.. n c= A ^.. m
proof
assume
A: m <= n;
now
let x;
assume x in A ^.. n;
then consider k such that
B: n <= k & x in A ^ k by ThPlus10;
m <= k by A, B,XXREAL_0:2;
hence x in A ^.. m by B, ThPlus10;
end;
hence thesis by TARSKI:def 3;
end;
theorem ThPlus50:
k <= m implies A ^ (m, n) c= A ^.. k
proof
assume
A: k <= m;
now
let x;
assume x in A ^ (m, n);
then consider l such that
B: m <= l & l <= n & x in A ^ l by FLANG_2:19;
k <= l by A, B, XXREAL_0:2;
hence x in A ^.. k by B, ThPlus10;
end;
hence thesis by TARSKI:def 3;
end;
theorem ThPlus60:
m <= n + 1 implies A ^ (m, n) \/ A ^.. (n + 1) = A ^.. m
proof
assume m <= n + 1;
then
B1: A ^.. (n + 1) c= A ^.. m by ThPlus40;
A ^ (m, n) c= A ^.. m by ThPlus50;
then
B3: A ^ (m, n) \/ A ^.. (n + 1) c= A ^.. m by B1, XBOOLE_1:8;
A ^.. m c= A ^ (m, n) \/ A ^.. (n + 1)
proof
now
let x;
assume x in A ^.. m;
then consider k such that
B4a: m <= k & x in A ^ k by ThPlus10;
B4b: k <= n implies x in A ^ (m, n) by B4a, FLANG_2:19;
now
assume k > n;
then k >= n + 1 by NAT_1:13;
hence x in A ^.. (n + 1) by B4a, ThPlus10;
end;
hence x in A ^ (m, n) \/ A ^.. (n + 1) by B4b, XBOOLE_0:def 2;
end;
hence thesis by TARSKI:def 3;
end;
hence thesis by B3, XBOOLE_0:def 10;
end;
theorem
A ^ n \/ A ^.. (n + 1) = A ^.. n
proof
A:
n <= n + 1 by NAT_1:13;
thus A ^ n \/ A ^.. (n + 1) = A ^ (n, n) \/ A ^.. (n + 1) by FLANG_2:22
.= A ^.. n by A, ThPlus60;
end;
theorem ThPlus71:
A ^.. n c= A*
proof
now
let x;
assume x in A ^.. n;
then consider k such that
A: n <= k & x in A ^ k by ThPlus10;
thus x in A* by A, FLANG_1:42;
end;
hence thesis by TARSKI:def 3;
end;
theorem ThPlus72:
<%>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 <%>E in A ^.. n;
then consider k such that
A: n <= k & <%>E in A ^ k by ThPlus10;
n = 0 or n > 0;
hence thesis by A, FLANG_1:32;
end;
assume
B: n = 0 or <%>E in A;
per cases by B;
suppose
C: n = 0;
{<%>E} = A ^ 0 by FLANG_1:25;
then <%>E in A ^ n by C, TARSKI:def 1;
hence thesis by ThPlus10;
end;
suppose <%>E in A;
then <%>E in A ^ n by FLANG_1:31;
hence thesis by ThPlus10;
end;
end;
theorem ThPlus80:
A ^.. n = A* iff <%>E in A or n = 0
proof
thus A ^.. n = A* implies <%>E in A or n = 0
proof
assume that
A1: A ^.. n = A* and
A2: not <%>E in A & n <> 0;
<%>E in A* & not <%>E in A ^.. n by A2, ThPlus72, FLANG_1:49;
hence contradiction by A1;
end;
assume
B: <%>E in A or n = 0;
per cases by B;
suppose <%>E in A;
B1: A ^.. n c= A* by ThPlus71;
B2: A* c= A ^.. n
proof
now
let x;
assume x in A*;
then consider k such that
B2a: x in A ^ k by FLANG_1:42;
per cases;
suppose n <= k;
hence x in A ^.. n by B2a, ThPlus10;
end;
suppose k < n;
then A ^ k c= A ^ n by B, FLANG_1:37;
hence x in A ^.. n by B2a, ThPlus10;
end;
end;
hence thesis by TARSKI:def 3;
end;
thus thesis by B1, B2, XBOOLE_0:def 10;
end;
suppose
D: n = 0;
D1: now
let x;
assume x in A ^.. n;
then consider k such that
D2: 0 <= k & x in A ^ k by D, ThPlus10;
thus x in A* by D2, FLANG_1:42;
end;
now
let x;
assume x in A*;
then consider k such that
D2: x in A ^ k by FLANG_1:42;
thus x in A ^.. n by D, D2, ThPlus10;
end;
hence thesis by D1, TARSKI:2;
end;
end;
theorem
A* = A ^ (0, n) \/ A ^.. (n + 1)
proof
thus A* = A ^.. 0 by ThPlus80
.= A ^ (0, n) \/ A ^.. (n + 1) by ThPlus60;
end;
theorem ThPlus100:
A c= B implies A ^.. n c= B ^.. n
proof
assume
A: A c= B;
now
let x;
assume x in A ^.. n;
then consider k such that
B: n <= k & x in A ^ k by ThPlus10;
A ^ k c= B ^ k by A, FLANG_1:38;
hence x in B ^.. n by B, ThPlus10;
end;
hence thesis by TARSKI:def 3;
end;
theorem ThPlus110:
x in A & x <> <%>E implies A ^.. n <> {<%>E}
proof
assume
A: x in A & x <> <%>E;
per cases;
suppose
B: n = 0;
x in A ^ 1 by A, FLANG_1:26;
then x in A ^.. n by B, ThPlus10;
hence thesis by A, TARSKI:def 1;
end;
suppose n > 0;
then
C1: A ^ n <> {<%>E} by A, FLANG_2:7;
A ^ n <> {} by A, FLANG_1:28;
then consider y such that
C2: y in A ^ n & y <> <%>E by C1, ZFMISC_1:41;
y in A ^.. n by C2, ThPlus10;
hence thesis by C2, TARSKI:def 1;
end;
end;
theorem ThPlus120:
A ^.. n = {<%>E} iff A = {<%>E} or (n = 0 & A = {})
proof
thus A ^.. n = {<%>E} implies A = {<%>E} or (n = 0 & A = {})
proof
assume that
A1: A ^.. n = {<%>E} and
A2: A <> {<%>E} and
A3: n <> 0 or A <> {};
per cases by A3;
suppose
A4a: n <> 0;
<%>E in A ^.. n by A1, ZFMISC_1:37;
then consider k such that
A4b: n <= k & <%>E in A ^ k by ThPlus10;
k > 0 by A4a, A4b;
then
A4c: <%>E in A by A4b, FLANG_1:32;
not ex x st x in A & x <> <%>E by A1, ThPlus110;
hence contradiction by A2, A4c, ZFMISC_1:41;
end;
suppose A <> {};
then consider x such that
A5: x in A & x <> <%>E by A2, ZFMISC_1:41;
thus contradiction by A1, A5, ThPlus110;
end;
end;
assume
B: A = {<%>E} or (n = 0 & A = {});
per cases by B;
suppose
B1: A = {<%>E};
C: now
let x;
assume x in A ^.. n;
then consider k such that
B1a: n <= k & x in A ^ k by ThPlus10;
thus x in {<%>E} by B1a, B1, FLANG_1:29;
end;
now
let x;
assume x in {<%>E};
then x in A ^ n by B1, FLANG_1:29;
hence x in A ^.. n by ThPlus10;
end;
hence thesis by C, TARSKI:2;
end;
suppose
B2: n = 0 & A = {};
thus A ^.. n = A* by B2, ThPlus80
.= {<%>E} by B2, FLANG_1:48;
end;
end;
theorem ThPlus124:
A ^.. (n + 1) = (A ^.. n) ^^ A
proof
A:
(A ^.. n) ^^ A c= A ^.. (n + 1)
proof
now
let x;
assume x in (A ^.. n) ^^ A;
then consider a, b such that
A1: a in (A ^.. n) & b in A & x = a ^ b by FLANG_1:def 1;
A2: b in A ^ 1 by A1, FLANG_1:26;
consider k such that
A3: n <= k & a in A ^ k by A1, ThPlus10;
A4: x in A ^ (k + 1) by A1, A2, A3, FLANG_1:41;
n + 1 <= k + 1 by A3, XREAL_1:8;
hence x in A ^.. (n + 1) by A4, ThPlus10;
end;
hence thesis by TARSKI:def 3;
end;
A ^.. (n + 1) c= (A ^.. n) ^^ A
proof
now
let x;
assume x in A ^.. (n + 1);
then consider k such that
B1: n + 1 <= k & x in A ^ k by ThPlus10;
consider l such that
B2: l + 1 = k by B1, NAT_1:6;
B3: n <= l by B1, B2, XREAL_1:8;
x in (A ^ l) ^^ (A ^ 1) by B1, B2, FLANG_1:34;
then consider a, b such that
B4: a in A ^ l & b in A ^ 1 & x = a ^ b by FLANG_1:def 1;
a in A ^.. n by B3, B4, ThPlus10;
then x in (A ^.. n) ^^ (A ^ 1) by B4, FLANG_1:def 1;
hence x in (A ^.. n) ^^ A by FLANG_1:26;
end;
hence thesis by TARSKI:def 3;
end;
hence thesis by A, XBOOLE_0:def 10;
end;
theorem ThPlus123:
(A ^.. m) ^^ (A*) = A ^.. m
proof
A:
(A ^.. m) ^^ (A*) c= A ^.. m
proof
now
let x;
assume x in (A ^.. m) ^^ (A*);
then consider a, b such that
A1: a in A ^.. m & b in A* & x = a ^ b by FLANG_1:def 1;
consider k such that
A2: b in A ^ k by A1, FLANG_1:42;
consider l such that
A3: m <= l & a in A ^ l by A1, ThPlus10;
A4: a ^ b in A ^ (l + k) by A2, A3, FLANG_1:41;
l + k >= m by A3, NAT_1:12;
hence x in A ^.. m by A1, A4, ThPlus10;
end;
hence thesis by TARSKI:def 3;
end;
A ^.. m c= (A ^.. m) ^^ (A*)
proof
<%>E in A* by FLANG_1:49;
hence thesis by FLANG_1:17;
end;
hence thesis by A, XBOOLE_0:def 10;
end;
theorem ThPlus122:
(A ^.. m) ^^ (A ^.. n) = A ^.. (m + n)
proof
defpred P[Nat] means (A ^.. m) ^^ (A ^.. $1) = A ^.. (m + $1);
B1:
P[0]
proof
thus (A ^.. m) ^^ (A ^.. 0) = (A ^.. m) ^^ (A*) by ThPlus80
.= (A ^.. (m + 0)) by ThPlus123;
end;
B2:
now
let n;
assume
B2a: P[n];
(A ^.. m) ^^ (A ^.. (n + 1))
= (A ^.. m) ^^ ((A ^.. n) ^^ A) by ThPlus124
.= A ^.. (m + n) ^^ A by B2a, FLANG_1:19
.= A ^.. (m + n + 1) by ThPlus124;
hence P[n + 1];
end;
for n holds P[n] from NAT_1:sch 2(B1, B2);
hence thesis;
end;
theorem ThPlus121:
n > 0 implies (A ^.. m) ^ n = A ^.. (m * n)
proof
defpred P[Nat] means $1 > 0 implies (A ^.. m) ^ $1 = A ^.. (m * $1);
B1:
P[0];
B2:
now
let n;
assume
B2a: P[n];
now
assume n + 1 > 0;
per cases;
suppose
B2b: n = 0;
thus (A ^.. m) ^ (n + 1) = A ^.. (m * (n + 1)) by B2b, FLANG_1:26;
end;
suppose
B2c: n > 0;
thus (A ^.. m) ^ (n + 1)
= (A ^.. (m * n)) ^^ (A ^.. m) by B2a, B2c, FLANG_1:24
.= A ^.. (m * n + m) by ThPlus122
.= A ^.. (m * (n + 1));
end;
end;
hence P[n + 1];
end;
for n holds P[n] from NAT_1:sch 2(B1, B2);
hence thesis;
end;
theorem
(A ^.. n)* = (A ^.. n)?
proof
A:
(A ^.. n)? c= (A ^.. n)* by FLANG_2:86;
(A ^.. n)* c= (A ^.. n)?
proof
now
let x;
assume x in (A ^.. n)*;
then consider k such that
A: x in (A ^.. n) ^ k by FLANG_1:42;
per cases;
suppose k = 0;
then x in (A ^.. n) ^ 0 \/ (A ^.. n) ^ 1 by A, XBOOLE_0:def 2;
hence x in (A ^.. n)? by FLANG_2:75;
end;
suppose
B: k > 0;
then
B1: k >= 0 + 1 by NAT_1:13;
(A ^.. n) ^ k c= A ^.. (n * k) by B, ThPlus121;
then consider l such that
B2: n * k <= l & x in A ^ l by A, ThPlus10;
n * k >= n by B1, REAL_2:146;
then l >= n by B2, XXREAL_0:2;
then x in A ^.. n by B2, ThPlus10;
then x in (A ^.. n) ^ 1 by FLANG_1:26;
then x in (A ^.. n) ^ 0 \/ (A ^.. n) ^ 1 by XBOOLE_0:def 2;
hence x in (A ^.. n)? by FLANG_2:75;
end;
end;
hence thesis by TARSKI:def 3;
end;
hence thesis by A, XBOOLE_0:def 10;
end;
theorem ThPlus130:
A c= C ^.. m & B c= C ^.. n implies A ^^ B c= C ^.. (m + n)
proof
assume
A: A c= C ^.. m & B c= C ^.. n;
thus x in A ^^ B implies x in C ^.. (m + n)
proof
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) ^^ (C ^.. n) by A, B, FLANG_1:def 1;
hence thesis by B, ThPlus122;
end;
end;
theorem ThPlus140:
A ^.. (n + k) = (A ^.. n) ^^ (A ^ k)
proof
defpred P[Nat] means A ^.. (n + $1) = (A ^.. n) ^^ (A ^ $1);
A:
P[0]
proof
thus A ^.. (n + 0) = (A ^.. n) ^^ {<%>E} by FLANG_1:14
.= (A ^.. n) ^^ (A ^ 0) by FLANG_1:25;
end;
B:
now
let k be Nat;
assume
C: P[k];
A ^.. (n + (k + 1)) = (A ^.. (n + k + 1))
.= (A ^.. n) ^^ (A ^ k) ^^ A by C, ThPlus124
.= (A ^.. n) ^^ ((A ^ k) ^^ A) by FLANG_1:19
.= (A ^.. n) ^^ (A ^ (k + 1)) by FLANG_1:24;
hence P[k + 1];
end;
for k being Nat holds P[k] from NAT_1:sch 2(A, B);
hence thesis;
end;
theorem ThPlus150:
A ^^ (A ^.. n) = (A ^.. n) ^^ A
proof
defpred P[Nat] means A ^^ (A ^.. $1) = (A ^.. $1) ^^ A;
A:
P[0]
proof
thus A ^^ (A ^.. 0) = A ^^ (A*) by ThPlus80
.= (A*) ^^ A by FLANG_1:58
.= (A ^.. 0) ^^ A by ThPlus80;
end;
B:
now
let k be Nat;
assume
C: P[k];
A ^^ (A ^.. (k + 1)) = A ^^ ((A ^.. k) ^^ A) by ThPlus124
.= (A ^.. k) ^^ A ^^ A by C, FLANG_1:19
.= (A ^.. (k + 1)) ^^ A by ThPlus124;
hence P[k + 1];
end;
for k being Nat holds P[k] from NAT_1:sch 2(A, B);
hence thesis;
end;
theorem ThPlus160:
(A ^ k) ^^ (A ^.. n) = (A ^.. n) ^^ (A ^ k)
proof
defpred P[Nat] means (A ^ $1) ^^ (A ^.. n) = (A ^.. n) ^^ (A ^ $1);
A:
P[0]
proof
thus (A ^ 0) ^^ (A ^.. n) = {<%>E} ^^ (A ^.. n) by FLANG_1:25
.= (A ^.. n) by FLANG_1:14
.= (A ^.. n) ^^ {<%>E} by FLANG_1:14
.= (A ^.. n) ^^ (A ^ 0) by FLANG_1:25;
end;
B:
now
let k;
assume
C: P[k];
(A ^ (k + 1)) ^^ (A ^.. n)
= ((A ^ k) ^^ A) ^^ (A ^.. n) by FLANG_1:24
.= (A ^^ (A ^ k)) ^^ (A ^.. n) by FLANG_1:33
.= A ^^ ((A ^.. n) ^^ (A ^ k)) by C, FLANG_1:19
.= (A ^^ (A ^.. n)) ^^ (A ^ k) by FLANG_1:19
.= (A ^.. n) ^^ A ^^ (A ^ k) by ThPlus150
.= (A ^.. n) ^^ (A ^^ (A ^ k)) by FLANG_1:19
.= (A ^.. n) ^^ ((A ^ k) ^^ A) by FLANG_1:33
.= (A ^.. n) ^^ (A ^ (k + 1)) by FLANG_1:24;
hence P[k + 1];
end;
for k holds P[k] from NAT_1:sch 2(A, B);
hence thesis;
end;
theorem ThPlus170:
(A ^ (k, l)) ^^ (A ^.. n) = (A ^.. n) ^^ (A ^ (k, l))
proof
defpred P[Nat] means
(A ^ (k, l)) ^^ (A ^.. $1) = (A ^.. $1) ^^ (A ^ (k, l));
A:
P[0]
proof
thus (A ^ (k, l)) ^^ (A ^.. 0) = (A ^ (k, l)) ^^ (A*) by ThPlus80
.= A* ^^ (A ^ (k, l)) by FLANG_2:66
.= (A ^.. 0) ^^ (A ^ (k, l)) by ThPlus80;
end;
B:
now
let n;
assume
C: P[n];
(A ^ (k, l)) ^^ (A ^.. (n + 1))
= (A ^ (k, l)) ^^ ((A ^.. n) ^^ A) by ThPlus124
.= (A ^.. n) ^^ (A ^ (k, l)) ^^ A by C, FLANG_1:19
.= (A ^.. n) ^^ ((A ^ (k, l)) ^^ A) by FLANG_1:19
.= (A ^.. n) ^^ (A ^^ (A ^ (k, l))) by FLANG_2:36
.= (A ^.. n) ^^ A ^^ (A ^ (k, l)) by FLANG_1:19
.= (A ^.. (n + 1)) ^^ (A ^ (k, l)) by ThPlus124;
hence P[n + 1];
end;
for n holds P[n] from NAT_1:sch 2(A, B);
hence thesis;
end;
theorem
<%>E in B implies A c= A ^^ (B ^.. n) & A c= (B ^.. n) ^^ A
proof
assume <%>E in B;
then <%>E in B ^.. n by ThPlus72;
hence thesis by FLANG_1:17;
end;
theorem ThPlus190:
(A ^.. m) ^^ (A ^.. n) = (A ^.. n) ^^ (A ^.. m)
proof
thus (A ^.. m) ^^ (A ^.. n) = A ^.. (m + n) by ThPlus122
.= (A ^.. n) ^^ (A ^.. m) by ThPlus122;
end;
theorem ThPlus200:
A c= B ^.. k & n > 0 implies A ^ n c= B ^.. k
proof
assume
A: A c= B ^.. k & n > 0;
defpred P[Nat] means $1 > 0 implies A ^ $1 c= B ^.. k;
B:
P[0];
C:
now
let m;
assume
D: P[m];
per cases;
suppose m <= 0;
then m = 0;
hence P[m + 1] by A, FLANG_1:26;
end;
suppose m > 0;
then (A ^ m) ^^ A c= (B ^.. k) ^^ (B ^.. k) by A, D, FLANG_1:18;
then A ^ (m + 1) c= (B ^.. k) ^^ (B ^.. k) by FLANG_1:24;
then
E: A ^ (m + 1) c= (B ^.. (k + k)) by ThPlus122;
k + k >= k by NAT_1:11;
then B ^.. (k + k) c= B ^.. k by ThPlus40;
hence P[m + 1] by E, XBOOLE_1:1;
end;
end;
for m holds P[m] from NAT_1:sch 2(B, C);
hence thesis by A;
end;
theorem ThPlus201:
A c= B ^.. k & n > 0 implies A ^.. n c= B ^.. k
proof
assume
A: A c= B ^.. k & n > 0;
let x;
assume x in A ^.. n;
then consider m such that
B: m >= n & x in A ^ m by ThPlus10;
A ^ m c= B ^.. k by A, B, ThPlus200;
hence x in B ^.. k by B;
end;
theorem ThPlus210:
A* ^^ A = A ^.. 1
proof
A:
now
let x;
assume x in A ^.. 1;
then consider n such that
A1: n >= 1 & x in A ^ n by ThPlus10;
consider m such that
A2: m + 1 = n by A1, NAT_1:6;
A ^ (m + 1) c= (A*) ^^ A by FLANG_1:52;
hence x in (A*) ^^ A by A1, A2;
end;
B:
now
let x;
assume x in (A*) ^^ A;
then consider a1, a2 such that
B1: a1 in A* & a2 in A & x = a1 ^ a2 by FLANG_1:def 1;
B2: a2 in A ^ 1 by B1, FLANG_1:26;
consider n such that
B3: a1 in A ^ n by B1, FLANG_1:42;
a1 ^ a2 in A ^ (n + 1) & n + 1 >= 1 by B2, B3, FLANG_1:41, NAT_1:11;
hence x in A ^.. 1 by B1, ThPlus10;
end;
thus thesis by A, B, TARSKI:2;
end;
theorem
A* ^^ (A ^ k) = A ^.. k
proof
defpred P[Nat] means A* ^^ (A ^ $1) = A ^.. $1;
A:
P[0]
proof
thus A* ^^ (A ^ 0) = A* ^^ {<%>E} by FLANG_1:25
.= A* by FLANG_1:14
.= A ^.. 0 by ThPlus80;
end;
B:
now
let k;
assume
C: P[k];
A* ^^ (A ^ (k + 1)) = A* ^^ ((A ^ k) ^^ A) by FLANG_1:24
.= A ^.. k ^^ A by C, FLANG_1:19
.= A ^.. (k + 1) by ThPlus124;
hence P[k + 1];
end;
for k holds P[k] from NAT_1:sch 2(A, B);
hence thesis;
end;
theorem ThPlus230:
(A ^.. m) ^^ (A*) = A* ^^ (A ^.. m)
proof
thus (A ^.. m) ^^ (A*) = (A ^.. m) ^^ (A ^.. 0) by ThPlus80
.= (A ^.. 0) ^^ (A ^.. m) by ThPlus190
.= A* ^^ (A ^.. m) by ThPlus80;
end;
theorem ThPlus235:
k <= l implies (A ^.. n) ^^ (A ^ (k, l)) = A ^.. (n + k)
proof
assume
A: k <= l;
B:
(A ^.. n) ^^ (A ^ (k, l)) c= A ^.. (n + k)
proof
let x;
assume x in (A ^.. n) ^^ (A ^ (k, l));
then consider a, b such that
C: a in A ^.. n & b in A ^ (k, l) & x = a ^ b by FLANG_1:def 1;
A ^ (k, l) c= A ^.. k by ThPlus50;
then a ^ b in (A ^.. n) ^^ (A ^.. k) by C, FLANG_1:def 1;
hence x in A ^.. (n + k) by C, ThPlus122;
end;
A ^.. (n + k) c= (A ^.. n) ^^ (A ^ (k, l))
proof
let x;
assume x in A ^.. (n + k);
then consider i such that
D: i >= n + k & x in A ^ i by ThPlus10;
consider m such that
E: n + k + m = i by D, NAT_1:10;
i = n + m + k by E;
then x in (A ^ (n + m)) ^^ (A ^ k) by D, FLANG_1:34;
then consider a, b such that
F: a in A ^ (n + m) & b in A ^ k & x = a ^ b by FLANG_1:def 1;
G: A ^ k c= A ^ (k, l) by A, FLANG_2:20;
n + m >= n by NAT_1:11;
then A ^ (n + m) c= A ^.. n by ThPlus20;
hence x in (A ^.. n) ^^ (A ^ (k, l)) by F, G, FLANG_1:def 1;
end;
hence thesis by B, XBOOLE_0:def 10;
end;
theorem
k <= l implies A* ^^ (A ^ (k, l)) = A ^.. k
proof
assume k <= l;
then (A ^.. 0) ^^ (A ^ (k, l)) = A ^.. (0 + k) by ThPlus235;
hence thesis by ThPlus80;
end;
theorem ThPlus250:
(A ^ m) ^.. n c= A ^.. (m * n)
proof
let x;
assume x in (A ^ m) ^.. n;
then consider k such that
A: k >= n & x in (A ^ m) ^ k by ThPlus10;
B:
x in A ^ (m * k) by A, FLANG_1:35;
m * k >= m * n by A, XREAL_1:66;
hence x in A ^.. (m * n) by B, ThPlus10;
end;
theorem
(A ^ m) ^.. n c= (A ^.. n) ^ m
proof
per cases;
suppose
A: m > 0;
(A ^ m) ^.. n c= A ^.. (m * n) by ThPlus250;
hence thesis by A, ThPlus121;
end;
suppose m <= 0;
then
A: m = 0;
(A ^ m) ^.. n = {<%>E} ^.. n by A, FLANG_1:25
.= {<%>E} by ThPlus120
.= (A ^.. n) ^ m by A, FLANG_1:25;
hence thesis;
end;
end;
theorem ThPlus270:
a in C ^.. m & b in C ^.. n implies a ^ b in C ^.. (m + n)
proof
assume a in C ^.. m & b in C ^.. n;
then
A: a ^ b in (C ^.. m) ^^ (C ^.. n) by FLANG_1:def 1;
(C ^.. m) ^^ (C ^.. n) c= C ^.. (m + n) by ThPlus130;
hence thesis by A;
end;
theorem ThPlus280:
A ^.. k = {x} implies x = <%>E
proof
assume
A: A ^.. k = {x} & x <> <%>E;
then
B: x in A ^.. k by ZFMISC_1:37;
k + k >= k by NAT_1:11;
then
C: A ^.. (k + k) c= A ^.. k by ThPlus40;
reconsider a = x as Element of E^omega by A, ZFMISC_1:37;
D:
a ^ a in A ^.. (k + k) by B, ThPlus270;
a ^ a <> x by A, FLANG_1:12;
hence thesis by A, C, D, TARSKI:def 1;
end;
theorem
A c= B* implies A ^.. n c= B*
proof
assume
A: A c= B*;
let x;
assume x in A ^.. n;
then consider k such that
B: k >= n & x in A ^ k by ThPlus10;
A ^ k c= B* by A, FLANG_1:60;
hence x in B* by B;
end;
theorem ThPlus300:
A? c= A ^.. k iff k = 0 or <%>E in A
proof
thus A? c= A ^.. k implies k = 0 or <%>E in A
proof
assume
A: A? c= A ^.. k;
<%>E in A? by FLANG_2:78;
hence thesis by A, ThPlus72;
end;
assume k = 0 or <%>E in A;
then A ^.. k = A* by ThPlus80;
hence thesis by FLANG_2:86;
end;
theorem ThPlus305:
A ^.. k ^^ (A?) = A ^.. k
proof
thus A ^.. k ^^ (A?) = A ^.. k ^^ (A ^ (0, 1)) by FLANG_2:79
.= A ^.. (k + 0) by ThPlus235
.= A ^.. k;
end;
theorem
A ^.. k ^^ (A?) = A? ^^ (A ^.. k)
proof
thus A ^.. k ^^ (A?) = A ^.. k ^^ (A ^ (0, 1)) by FLANG_2:79
.= A ^ (0, 1) ^^ (A ^.. k) by ThPlus170
.= A? ^^ (A ^.. k) by FLANG_2:79;
end;
theorem
B c= A* implies A ^.. k ^^ B c= A ^.. k & B ^^ (A ^.. k) c= A ^.. k
proof
assume B c= A*;
then A ^.. k ^^ B c= A ^.. k ^^ (A*) &
B ^^ (A ^.. k) c= A* ^^ (A ^.. k) by FLANG_1:18;
then A ^.. k ^^ B c= A ^.. k ^^ (A*) &
B ^^ (A ^.. k) c= A ^.. k ^^ (A*) by ThPlus230;
hence thesis by ThPlus123;
end;
theorem ThPlus330:
(A /\ B) ^.. k c= (A ^.. k) /\ (B ^.. k)
proof
thus x in (A /\ B) ^.. k implies x in (A ^.. k) /\ (B ^.. k)
proof
assume x in (A /\ B) ^.. k;
then consider m such that
A: k <= m & x in (A /\ B) ^ m by ThPlus10;
(A /\ B) ^ m c= (A ^ m) /\ (B ^ m) by FLANG_1:40;
then
B: x in (A ^ m) /\ (B ^ m) by A;
A ^ m c= A ^.. k & B ^ m c= B ^.. k by A, ThPlus20;
then (A ^ m) /\ (B ^ m) c= (A ^.. k) /\ (B ^.. k) by XBOOLE_1:27;
hence thesis by B;
end;
end;
theorem ThPlus340:
(A ^.. k) \/ (B ^.. k) c= (A \/ B) ^.. k
proof
thus x in (A ^.. k) \/ (B ^.. k) implies x in (A \/ B) ^.. k
proof
assume
A: x in (A ^.. k) \/ (B ^.. k);
per cases by A, XBOOLE_0:def 2;
suppose x in (A ^.. k);
then consider m such that
B: k <= m & x in A ^ m by ThPlus10;
C: A ^ m c= (A ^ m) \/ (B ^ m) by XBOOLE_1:7;
(A ^ m) \/ (B ^ m) c= (A \/ B) ^ m by FLANG_1:39;
then A ^ m c= (A \/ B) ^ m by C, XBOOLE_1:1;
then
D: x in (A \/ B) ^ m by B;
(A \/ B) ^ m c= (A \/ B) ^.. k by B, ThPlus20;
hence thesis by D;
end;
suppose x in (B ^.. k);
then consider m such that
B: k <= m & x in B ^ m by ThPlus10;
C: B ^ m c= (A ^ m) \/ (B ^ m) by XBOOLE_1:7;
(A ^ m) \/ (B ^ m) c= (A \/ B) ^ m by FLANG_1:39;
then B ^ m c= (A \/ B) ^ m by C, XBOOLE_1:1;
then
D: x in (A \/ B) ^ m by B;
(A \/ B) ^ m c= (A \/ B) ^.. k by B, ThPlus20;
hence thesis by D;
end;
end;
end;
theorem ThPlus350:
<%x%> in A ^.. k iff <%x%> in A & (<%>E in A or k <= 1)
proof
thus <%x%> in A ^.. k implies <%x%> in A & (<%>E in A or k <= 1)
proof
assume <%x%> in A ^.. k;
then consider m such that
A: k <= m & <%x%> in A ^ m by ThPlus10;
thus thesis by A, FLANG_2:9;
end;
assume
A: <%x%> in A & (<%>E in A or k <= 1);
per cases by A, NAT_1:26;
suppose <%>E in A & k > 1;
then <%x%> in A ^ k by A, FLANG_2:9;
hence thesis by ThPlus10;
end;
suppose k = 0;
then A ^.. k = A* by ThPlus80;
hence thesis by A, FLANG_1:73;
end;
suppose k = 1;
then <%x%> in A ^ k by A, FLANG_1:26;
hence thesis by ThPlus10;
end;
end;
theorem ThPlus360:
A c= B ^.. k implies B ^.. k = (B \/ A) ^.. k
proof
assume
A: A c= B ^.. k;
B ^ 1 c= B ^.. 1 by ThPlus20;
then
A1: B c= B ^.. 1 by FLANG_1:26;
defpred P[Nat] means $1 >= k implies (B \/ A) ^ $1 c= B ^.. k;
B:
P[0]
proof
assume 0 >= k;
then k = 0;
then
B1: B ^.. k = B* by ThPlus80;
B2: (B \/ A) ^ 0 = {<%>E} by FLANG_1:25;
<%>E in B* by FLANG_1:49;
hence thesis by B1, B2, ZFMISC_1:37;
end;
C:
now
let n;
assume
C0: P[n];
now
assume
CY: n + 1 >= k;
per cases by CY, NAT_1:8;
suppose
CX: n + 1 = k;
per cases;
suppose k = 0;
hence (B \/ A) ^ (n + 1) c= B ^.. k by CX;
end;
suppose
D1: k > 0;
then k >= 0 + 1 by NAT_1:13;
then B ^.. k c= B ^.. 1 by ThPlus40;
then A c= B ^.. 1 by A, XBOOLE_1:1;
then B \/ A c= B ^.. 1 by A1, XBOOLE_1:8;
then
D: (B \/ A) ^ k c= (B ^.. 1) ^ k by FLANG_1:38;
(B ^.. 1) ^ k c= B ^.. (1 * k) by D1, ThPlus121;
hence (B \/ A) ^ (n + 1) c= B ^.. k by CX, D, XBOOLE_1:1;
end;
end;
suppose
CX: n >= k;
C1: (B \/ A) ^ (n + 1)
= (B \/ A) ^ n ^^ (B \/ A) by FLANG_1:24
.= (B \/ A) ^ n ^^ B \/ (B \/ A) ^ n ^^ A by FLANG_1:21;
C3': (B \/ A) ^ n ^^ B c= B ^.. (k + 1) by C0, CX, A1, ThPlus130;
k + 1 >= k by NAT_1:11;
then B ^.. (k + 1) c= B ^.. k by ThPlus40;
then
C3: (B \/ A) ^ n ^^ B c= B ^.. k by C3', XBOOLE_1:1;
C4: (B \/ A) ^ n ^^ A c= B ^.. (k + k) by A, C0, CX, ThPlus130;
k + k >= k by NAT_1:11;
then B ^.. (k + k) c= B ^.. k by ThPlus40;
then (B \/ A) ^ n ^^ A c= B ^.. k by C4, XBOOLE_1:1;
hence (B \/ A) ^ (n + 1) c= B ^.. k by C1, C3, XBOOLE_1:8;
end;
end;
hence P[n + 1];
end;
D:
for n holds P[n] from NAT_1:sch 2(B, C);
E:
(B \/ A) ^.. k c= B ^.. k
proof
let x;
assume x in (B \/ A) ^.. k;
then consider n such that
E1: n >= k & x in (B \/ A) ^ n by ThPlus10;
(B \/ A) ^ n c= B ^.. k by D, E1;
hence x in B ^.. k by E1;
end;
B c= B \/ A by XBOOLE_1:7;
then B ^.. k c= (B \/ A) ^.. k by ThPlus100;
hence thesis by E, XBOOLE_0:def 10;
end;
begin
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Positive Closure
:: Definition of +
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let E, A;
func A+ > Subset of E^omega equals
union { B: ex n st n > 0 & B = A ^ n };
coherence
proof
defpred P[set] means ex n st n > 0 & $1 = A ^ n;
reconsider M = { B: P[B] } as SubsetFamily of E^omega from DOMAIN_1:sch 7;
union M is Subset of E^omega;
hence thesis;
end;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Positive Closure
:: Properties of +
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem ThPos10:
x in A+ iff ex n st n > 0 & x in A ^ n
proof
thus x in A+ implies ex n st n > 0 & x in A ^ n
proof
assume x in A+;
then consider X such that
A1: x in X and
A2: X in { B: ex n st n > 0 & B = A ^ n } by TARSKI:def 4;
defpred P[set] means ex n st n > 0 & $1 = A ^ n;
A3: X in { B: P[B] } by A2;
P[X] from CARD_FIL:sch 1(A3);
hence thesis by A1;
end;
given n such that
B: n > 0 & x in A ^ n;
defpred P[set] means ex n st n > 0 & $1 = A ^ n;
consider B such that
D: x in B & P[B] by B;
reconsider A = { C : P[C] } as SubsetFamily of E^omega from DOMAIN_1:sch 7;
B in A by D;
hence thesis by D, TARSKI:def 4;
end;
theorem ThPos20:
n > 0 implies A ^ n c= A+
proof
assume n > 0;
then for x holds x in A ^ n implies x in A+ by ThPos10;
hence thesis by TARSKI:def 3;
end;
theorem ThPos40:
A+ = A ^.. 1
proof
A:
now
let x;
assume x in A ^.. 1;
then consider k such that
B: 1 <= k & x in A ^ k by ThPlus10;
thus x in A+ by B, ThPos10;
end;
now
let x;
assume x in A+;
then consider k such that
C: 0 < k & x in A ^ k by ThPos10;
0 + 1 <= k by C, NAT_1:13;
hence x in A ^.. 1 by C, ThPlus10;
end;
hence thesis by A, TARSKI:2;
end;
theorem
A+ = {} iff A = {}
proof
A+ = A ^.. 1 by ThPos40;
hence thesis by ThPlus30;
end;
theorem ThPos50:
A+ = (A*) ^^ A
proof
A* ^^ A = A ^.. 1 by ThPlus210;
hence thesis by ThPos40;
end;
theorem ThPos60:
A* = {<%>E} \/ (A+)
proof
thus A* = {<%>E} \/ ((A*) ^^ A) by FLANG_1:57
.= {<%>E} \/ (A+) by ThPos50;
end;
theorem
A+ = A ^ (1, n) \/ A ^.. (n + 1)
proof
A:
0 + 1 <= n + 1 by XREAL_1:9;
thus A+ = A ^.. 1 by ThPos40
.= A ^ (1, n) \/ A ^.. (n + 1) by A, ThPlus60;
end;
theorem ThPos80:
A+ c= A*
proof
A ^.. 1 c= A* by ThPlus71;
hence thesis by ThPos40;
end;
theorem ThPos90:
<%>E in A+ iff <%>E in A
proof
A+ = A ^.. 1 by ThPos40;
hence thesis by ThPlus72;
end;
theorem ThPos100:
A+ = A* iff <%>E in A
proof
thus A+ = A* implies <%>E in A
proof
assume A+ = A*;
then <%>E in A+ by FLANG_1:49;
hence thesis by ThPos90;
end;
assume <%>E in A;
then A* = (A*) ^^ A by FLANG_1:55;
hence thesis by ThPos50;
end;
theorem ThPos110:
A c= B implies A+ c= B+
proof
assume A c= B;
then A ^.. 1 c= B ^.. 1 by ThPlus100;
then A+ c= B ^.. 1 by ThPos40;
hence thesis by ThPos40;
end;
theorem ThPos120:
A c= A+
proof
A ^ 1 c= A+ by ThPos20;
hence thesis by FLANG_1:26;
end;
theorem ThPos130:
(A*)+ = A* & (A+)* = A*
proof
A:
A* c= (A*)+ by ThPos120;
A c= A+ by ThPos120;
then
B: A* c= (A+)* by FLANG_1:62;
C:
(A*)+ c= A*
proof
now
let x;
assume x in (A*)+;
then consider k such that
C1: 0 < k & x in (A*) ^ k by ThPos10;
(A*) ^ k c= A* by FLANG_1:66;
hence x in A* by C1;
end;
hence thesis by TARSKI:def 3;
end;
D:
(A+)* c= A*
proof
now
let x;
assume x in (A+)*;
then consider k such that
D1: x in (A+) ^ k by FLANG_1:42;
A+ c= A* by ThPos80;
then (A+) ^ k c= A* by FLANG_1:60;
hence x in A* by D1;
end;
hence thesis by TARSKI:def 3;
end;
thus thesis by A, B, C, D, XBOOLE_0:def 10;
end;
theorem ThPos140:
A c= B* implies A+ c= B*
proof
assume A c= B*;
then A+ c= (B*)+ by ThPos110;
hence thesis by ThPos130;
end;
theorem
(A+)+ = A+
proof
A:
A+ c= (A+)+ by ThPos120;
(A+)+ c= A+
proof
now
let x;
assume that
B: x in (A+)+;
per cases;
suppose x = <%>E;
hence x in A+ by B, ThPos90;
end;
suppose x <> <%>E;
then
C1: not x in {<%>E} by TARSKI:def 1;
A+ c= A* by ThPos80;
then (A+)+ c= A* by ThPos140;
then x in A* by B;
then x in (A+) \/ {<%>E} by ThPos60;
hence x in A+ by C1, XBOOLE_0:def 2;
end;
end;
hence thesis by TARSKI:def 3;
end;
hence thesis by A, XBOOLE_0:def 10;
end;
theorem
x in A & x <> <%>E implies A+ <> {<%>E}
proof
assume
A: x in A & x <> <%>E;
A+ = A ^.. 1 by ThPos40;
hence thesis by A, ThPlus110;
end;
theorem
A+ = {<%>E} iff A = {<%>E}
proof
A+ = A ^.. 1 by ThPos40;
hence thesis by ThPlus120;
end;
theorem
(A+)? = A* & (A?)+ = A*
proof
thus (A+)? = {<%>E} \/ (A+) by FLANG_2:76
.= A* by ThPos60;
thus (A?)+ = A*
proof
<%>E in A? by FLANG_2:78;
then (A?)+ = (A?)* by ThPos100;
hence thesis by FLANG_2:85;
end;
end;
theorem ThPos190:
a in C+ & b in C+ implies a ^ b in C+
proof
assume
A: a in C+ & b in C+;
consider k such that
Ak: k > 0 & a in C ^ k by A, ThPos10;
consider l such that
Al: l > 0 & b in C ^ l by A, ThPos10;
A2:
k + l > 0 by Ak, XREAL_1:36;
a ^ b in C ^ (k + l) by Ak, Al, FLANG_1:41;
hence thesis by A2, ThPos10;
end;
theorem
A c= C+ & B c= C+ implies A ^^ B c= C+
proof
assume
A: A c= C+ & B c= C+;
now
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;
thus x in C+ by A, B, ThPos190;
end;
hence thesis by TARSKI:def 3;
end;
theorem
A ^^ A c= A+
proof
A ^^ A = A ^ 2 by FLANG_1:27;
hence thesis by ThPos20;
end;
theorem
A+ = {x} implies x = <%>E
proof
assume A+ = {x} & x <> <%>E;
then A ^.. 1 = {x} & x <> <%>E by ThPos40;
hence thesis by ThPlus280;
end;
theorem
A ^^ (A+) = (A+) ^^ A
proof
thus A ^^ (A+) = A ^^ (A ^.. 1) by ThPos40
.= (A ^.. 1) ^^ A by ThPlus150
.= A+ ^^ A by ThPos40;
end;
theorem
(A ^ k) ^^ (A+) = (A+) ^^ (A ^ k)
proof
thus (A ^ k) ^^ (A+) = (A ^ k) ^^ (A ^.. 1) by ThPos40
.= (A ^.. 1) ^^ (A ^ k) by ThPlus160
.= A+ ^^ (A ^ k) by ThPos40;
end;
theorem ThPos250:
(A ^ (m, n)) ^^ (A+) = A+ ^^ (A ^ (m, n))
proof
thus (A ^ (m, n)) ^^ (A+) = (A ^ (m, n)) ^^ (A ^.. 1) by ThPos40
.= (A ^.. 1) ^^ (A ^ (m, n)) by ThPlus170
.= A+ ^^ (A ^ (m, n)) by ThPos40;
end;
theorem
<%>E in B implies A c= A ^^ (B+) & A c= (B+) ^^ A
proof
assume <%>E in B;
then B+ = B* by ThPos100;
hence thesis by FLANG_2:18;
end;
theorem
A+ ^^ (A+) = A ^.. 2
proof
thus A+ ^^ (A+) = A ^.. 1 ^^ (A+) by ThPos40
.= A ^.. 1 ^^ (A ^.. 1) by ThPos40
.= A ^.. (1 + 1) by ThPlus122
.= A ^.. 2;
end;
theorem ThPos280:
A+ ^^ (A ^ k) = A ^.. (k + 1)
proof
thus A+ ^^ (A ^ k) = (A ^.. 1) ^^ (A ^ k) by ThPos40
.= A ^.. (k + 1) by ThPlus140;
end;
theorem
A+ ^^ A = A ^.. 2
proof
A+ ^^ A = A+ ^^ (A ^ 1) by FLANG_1:26
.= A ^.. (1 + 1) by ThPos280;
hence thesis;
end;
theorem
k <= l implies A+ ^^ (A ^ (k, l)) = A ^.. (k + 1)
proof
assume k <= l;
then (A ^.. 1) ^^ (A ^ (k, l)) = A ^.. (1 + k) by ThPlus235;
hence thesis by ThPos40;
end;
theorem
A c= B+ & n > 0 implies A ^ n c= B+
proof
assume
A: A c= B+ & n > 0;
then A c= B ^.. 1 by ThPos40;
then A ^ n c= B ^.. 1 by A, ThPlus200;
hence thesis by ThPos40;
end;
theorem
A+ ^^ (A?) = A? ^^ (A+)
proof
thus A+ ^^ (A?) = A+ ^^ (A ^ (0, 1)) by FLANG_2:79
.= A ^ (0, 1) ^^ (A+) by ThPos250
.= A? ^^ (A+) by FLANG_2:79;
end;
theorem
A+ ^^ (A?) = A+
proof
thus A+ ^^ (A?) = A ^.. 1 ^^ (A?) by ThPos40
.= A ^.. 1 by ThPlus305
.= A+ by ThPos40;
end;
theorem
A? c= A+ iff <%>E in A
proof
A+ = A ^.. 1 by ThPos40;
hence thesis by ThPlus300;
end;
theorem
A c= B+ implies A+ c= B+
proof
assume A c= B+;
then A c= B ^.. 1 by ThPos40;
then A ^.. 1 c= B ^.. 1 by ThPlus201;
then A+ c= B ^.. 1 by ThPos40;
hence A+ c= B+ by ThPos40;
end;
theorem
A c= B+ implies B+ = (B \/ A)+
proof
assume A c= B+;
then A c= B ^.. 1 by ThPos40;
then B ^.. 1 = (B \/ A) ^.. 1 by ThPlus360;
then B ^.. 1 = (B \/ A)+ by ThPos40;
hence thesis by ThPos40;
end;
theorem
n > 0 implies A ^.. n c= A+
proof
assume
A: n > 0;
let x;
assume x in A ^.. n;
then consider k such that
B: k >= n & x in A ^ k by ThPlus10;
thus x in A+ by A, B, ThPos10;
end;
theorem
m > 0 implies A ^ (m, n) c= A+
proof
assume
A: m > 0;
let x;
assume x in A ^ (m, n);
then consider k such that
B: m <= k & k <= n & x in A ^ k by FLANG_2:19;
thus x in A+ by A, B, ThPos10;
end;
theorem ThPos380:
A* ^^ (A+) = A+ ^^ (A*)
proof
thus A* ^^ (A+) = A* ^^ (A ^.. 1) by ThPos40
.= (A ^.. 1) ^^ (A*) by ThPlus230
.= A+ ^^ (A*) by ThPos40;
end;
theorem ThPos390:
A+ ^ k c= A ^.. k
proof
per cases;
suppose k > 0;
then (A ^.. 1) ^ k c= A ^.. (1 * k) by ThPlus121;
hence thesis by ThPos40;
end;
suppose
A: k = 0;
then
B: A+ ^ k = {<%>E} by FLANG_1:25;
A ^.. 0 = A* by ThPlus80;
then <%>E in A ^.. 0 by FLANG_1:49;
hence thesis by A, B, ZFMISC_1:37;
end;
end;
theorem
A+ ^ (m, n) c= A ^.. m
proof
let x;
assume x in A+ ^ (m, n);
then consider k such that
B: m <= k & k <= n & x in A+ ^ k by FLANG_2:19;
A+ ^ k c= A ^.. k by ThPos390;
then
1C: x in A ^.. k by B;
A ^.. k c= A ^.. m by B, ThPlus40;
hence thesis by 1C;
end;
theorem
A c= B+ & n > 0 implies A ^.. n c= B+
proof
assume
A: A c= B+ & n > 0;
A c= B ^.. 1 by A, ThPos40;
then A ^.. n c= B ^.. 1 by A, ThPlus201;
hence thesis by ThPos40;
end;
theorem ThPos420:
A+ ^^ (A ^.. k) = A ^.. (k + 1)
proof
thus A+ ^^ (A ^.. k) = (A ^.. 1) ^^ (A ^.. k) by ThPos40
.= A ^.. (k + 1) by ThPlus122;
end;
theorem
A+ ^^ (A ^.. k) = A ^.. k ^^ (A+)
proof
thus A+ ^^ (A ^.. k) = A ^.. (k + 1) by ThPos420
.= (A ^.. k) ^^ (A ^.. 1) by ThPlus122
.= A ^.. k ^^ (A+) by ThPos40;
end;
theorem ThPos429:
A+ ^^ (A*) = A+
proof
thus A+ ^^ (A*) = (A ^.. 1) ^^ (A*) by ThPos40
.= A ^.. 1 by ThPlus123
.= A+ by ThPos40;
end;
theorem
B c= A* implies A+ ^^ B c= A+ & B ^^ (A+) c= A+
proof
assume B c= A*;
then A+ ^^ B c= A+ ^^ (A*) & B ^^ (A+) c= A* ^^ (A+) by FLANG_1:18;
then A+ ^^ B c= A+ ^^ (A*) & B ^^ (A+) c= A+ ^^ (A*) by ThPos380;
hence thesis by ThPos429;
end;
theorem
(A /\ B)+ c= (A+) /\ (B+)
proof
(A /\ B)+ = (A /\ B) ^.. 1 & A+ = A ^.. 1 & B+ = B ^.. 1 by ThPos40;
hence thesis by ThPlus330;
end;
theorem
(A+) \/ (B+) c= (A \/ B)+
proof
(A \/ B)+ = (A \/ B) ^.. 1 & A+ = A ^.. 1 & B+ = B ^.. 1 by ThPos40;
hence thesis by ThPlus340;
end;
theorem
<%x%> in A+ iff <%x%> in A
proof
A+ = A ^.. 1 by ThPos40;
hence thesis by ThPlus350;
end;
Góra
