:: Regular Expression Quantifiers -- $m$ to $n$ Occurrences
:: by Micha{\l} Trybulec
::
:: Received June 6, 2007
:: Copyright (c) 2007-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, AFINSQ_1, NAT_1, ARYTM_3, XXREAL_0, ARYTM_1,
CARD_1, ORDINAL4, XBOOLE_0, FINSEQ_1, PRE_POLY, NEWTON, TARSKI, RELAT_1,
SETFAM_1, MODAL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, SETFAM_1,
XXREAL_0, AFINSQ_1, FLANG_1;
constructors NAT_1, XREAL_0, FLANG_1;
registrations SUBSET_1, NAT_1, ORDINAL1, AFINSQ_1, XREAL_0, XBOOLE_0,
XXREAL_0, FUNCT_1, RELAT_1, FINSET_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
expansions TARSKI;
theorems AFINSQ_1, NAT_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 for set;
reserve A, B, C for Subset of E^omega;
reserve a, b for Element of E^omega;
reserve i, k, l, kl, m, n, mn for Nat;
:: Preliminaries - Numbers:
theorem Th1:
m + k <= i & i <= n + k implies ex mn st mn + k = i & m <= mn & mn <= n
proof
assume that
A1: m + k <= i and
A2: i <= n + k;
m + k <= m + i by A1,XREAL_1:38;
then k <= i by XREAL_1:6;
then reconsider mn = i - k as Nat by NAT_1:21;
take mn;
thus mn + k = i;
m + k <= mn + k by A1;
hence thesis by A2,XREAL_1:6;
end;
theorem Th2:
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 that
A1: m <= n and
A2: k <= l and
A3: m + k <= i and
A4: i <= n + l;
per cases;
suppose
i <= n + k;
then consider mn such that
A5: mn + k = i & m <= mn & mn <= n by A3,Th1;
take mn, k;
thus mn + k = i & m <= mn & mn <= n by A5;
thus thesis by A2;
end;
suppose
i > n + k;
then consider kl such that
A6: kl + n = i and
A7: k <= kl & kl <= l by A4,Th1;
take n, kl;
thus n + kl = i & m <= n & n <= n by A1,A6;
thus thesis by A7;
end;
end;
theorem Th3:
m < n implies ex k st m + k = n & k > 0
proof
assume m < n;
then (ex k st m + k = n )& m - m < n - m by NAT_1:10,XREAL_1:14;
hence thesis;
end;
:: Preliminaries - Sequences:
theorem Th4:
a ^ b = a or b ^ a = a implies b = {}
proof
assume
A1: a ^ b = a or b ^ a = a;
per cases by A1;
suppose
A2: a ^ b = a;
len(a ^ b) = len(a) + len(b) by AFINSQ_1:17;
hence thesis by A2;
end;
suppose
A3: b ^ a = a;
len(b ^ a) = len(b) + len(a) by AFINSQ_1:17;
hence thesis by A3;
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:14;
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 ex a, b st a in A & b in B & <%x%> = a ^ b by FLANG_1:def 1;
hence thesis by FLANG_1:4;
end;
A1: {} ^ <%x%> = <%x%> & <%x%> ^ {} = <%x%>;
assume <%>E in A & <%x%> in B or <%x%> in A & <%>E in B;
hence thesis by A1,FLANG_1:def 1;
end;
theorem Th7:
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:29;
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 by FLANG_1:31;
assume
A1: n = 0 or <%>E in A;
per cases by A1;
suppose
n = 0;
then A |^ n = {<%>E} by FLANG_1:29;
hence thesis by ZFMISC_1:31;
end;
suppose
<%>E in A;
hence thesis by FLANG_1:30;
end;
end;
theorem Th9:
<%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:42;
hence <%x%> in A by A1,FLANG_1:72;
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:25;
suppose
n = 0;
then A |^ n = {<%>E} by FLANG_1:24;
hence contradiction by A1,TARSKI:def 1;
end;
suppose
A4: n > 1;
then consider m such that
A5: m + 1 = n by NAT_1:6;
<%x%> in (A |^ m) ^^ A by A1,A5,FLANG_1:23;
then consider a, b such that
A6: a in (A |^ m) and
A7: b in A and
A8: <%x%> = a ^ b by FLANG_1:def 1;
per cases by A8,FLANG_1:4;
suppose
A9: a = <%>E & b = <%x%>;
m + 1 > 0 + 1 by A4,A5;
then m > 0;
hence contradiction by A3,A6,A9,FLANG_1:31;
end;
suppose
b = <%>E & a = <%x%>;
hence contradiction by A3,A7;
end;
end;
end;
suppose
n <= 1 & n <> 1;
then n = 0 by NAT_1:25;
then A |^ n = {<%>E} by FLANG_1:24;
hence contradiction by A1,TARSKI:def 1;
end;
end;
assume that
A10: <%x%> in A and
A11: <%>E in A & n > 1 or n = 1;
per cases by A11;
suppose
<%>E in A & n > 1;
then A c= A |^ n by FLANG_1:35;
hence thesis by A10;
end;
suppose
n = 1;
hence thesis by A10,FLANG_1:25;
end;
end;
theorem Th10:
m <> n & A |^ m = {x} & A |^ n = {x} implies x = <%>E
proof
assume that
A1: m <> n and
A2: A |^ m = {x} and
A3: A |^ n = {x};
A4: x in A |^ m by A2,TARSKI:def 1;
A5: x in A |^ n by A3,TARSKI:def 1;
per cases by A1,XXREAL_0:1;
suppose
m > n;
then consider k such that
A6: n + k = m and
A7: k > 0 by Th3;
(A |^ n) ^^ (A |^ k) = A |^ m by A6,FLANG_1:33;
then consider a, b such that
A8: a in A |^ n and
A9: b in A |^ k and
A10: x = a ^ b by A4,FLANG_1:def 1;
a = x by A3,A8,TARSKI:def 1;
then b = <%>E by A10,Th4;
then <%>E in A by A7,A9,FLANG_1:31;
then <%>E in A |^ m by FLANG_1:30;
hence thesis by A2;
end;
suppose
m < n;
then consider k such that
A11: m + k = n and
A12: k > 0 by Th3;
(A |^ m) ^^ (A |^ k) = A |^ n by A11,FLANG_1:33;
then consider a, b such that
A13: a in A |^ m and
A14: b in A |^ k and
A15: x = a ^ b by A5,FLANG_1:def 1;
a = x by A2,A13,TARSKI:def 1;
then b = <%>E by A15,Th4;
then <%>E in A by A12,A14,FLANG_1:31;
then <%>E in A |^ m by FLANG_1:30;
hence thesis by A2;
end;
end;
theorem
(A |^ m) |^ n = (A |^ n) |^ m
proof
thus (A |^ m) |^ n = A |^ (m * n) by FLANG_1:34
.= (A |^ n) |^ m by FLANG_1:34;
end;
theorem Th12:
(A |^ m) ^^ (A |^ n) = (A |^ n) ^^ (A |^ m)
proof
thus (A |^ m) ^^ (A |^ n) = A |^ (m + n) by FLANG_1:33
.= (A |^ n) ^^ (A |^ m) by FLANG_1:33;
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:30;
hence thesis by FLANG_1:16;
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:17;
hence thesis by FLANG_1:33;
end;
theorem
x in A & x <> <%>E implies A* <> {<%>E}
proof
assume that
A1: x in A and
A2: x <> <%>E;
A <> {<%>E} by A1,A2,TARSKI:def 1;
hence thesis by A1,FLANG_1:47;
end;
theorem Th16:
<%>E in A & n > 0 implies (A |^ n)* = A*
proof
assume <%>E in A & n > 0;
then
A1: A* c= (A |^ n)* by FLANG_1:35,61;
(A |^ n)* c= A* by FLANG_1:64;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem Th17:
<%>E in A implies (A |^ n)* = (A*) |^ n
proof
assume
A1: <%>E in A;
per cases;
suppose
A2: n = 0;
hence (A |^ n)* = {<%>E}* by FLANG_1:24
.= {<%>E} by FLANG_1:47
.= (A*) |^ n by A2,FLANG_1:24;
end;
suppose
A3: n > 0;
then (A*) |^ n = A* by FLANG_1:66;
hence thesis by A1,A3,Th16;
end;
end;
theorem
A c= A ^^ (B*) & A c= (B*) ^^ A
proof
<%>E in B* by FLANG_1:48;
hence thesis by FLANG_1:16;
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 Th19:
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
defpred P[set] means ex k st m <= k & k <= n & $1 = A |^ k;
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;
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
A4: 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
A5: x in B and
A6: P[B] by A4;
reconsider A = { C: P[C] } as Subset-Family of E^omega from DOMAIN_1:sch 7;
B in A by A6;
hence thesis by A5,TARSKI:def 4;
end;
theorem Th20:
m <= k & k <= n implies A |^ k c= A |^ (m, n)
by Th19;
theorem Th21:
A |^ (m, n) = {} iff m > n or m > 0 & A = {}
proof
A1: now
assume
A2: m > 0 & A = {};
now
let x be object;
assume x in A |^ (m, n);
then ex k st m <= k & k <= n & x in A |^ k by Th19;
hence contradiction by A2,FLANG_1:27;
end;
hence A |^ (m, n) = {} by XBOOLE_0:def 1;
end;
thus A |^ (m, n) = {} implies m > n or m > 0 & A = {}
proof
assume that
A3: A |^ (m, n) = {} and
A4: m <= n &( m <= 0 or A <> {});
A5: now
assume that
A6: m <= n and
A7: A <> {};
A |^ m <> {} by A7,FLANG_1:27;
then ex a st a in A |^ m by SUBSET_1:4;
hence contradiction by A3,A6,Th19;
end;
now
assume that
A8: m <= n and
A9: m = 0;
{<%>E} = A |^ m by A9,FLANG_1:29;
then <%>E in A |^ m by TARSKI:def 1;
hence contradiction by A3,A8,Th19;
end;
hence thesis by A4,A5;
end;
now
assume
A10: m > n;
now
let x be object;
not (ex k st m <= k & k <= n & x in A |^ k) by A10,XXREAL_0:2;
hence not x in A |^ (m, n) by Th19;
end;
hence A |^ (m, n) = {} by XBOOLE_0:def 1;
end;
hence thesis by A1;
end;
theorem Th22:
A |^ (m, m) = A |^ m
proof
A1: now
let x be object;
assume x in A |^ (m, m);
then ex k st m <= k & k <= m & x in A |^ k by Th19;
hence x in A |^ m by XXREAL_0:1;
end;
for x being object holds x in A |^ m implies x in A |^ (m, m) by Th19;
hence thesis by A1,TARSKI:2;
end;
theorem Th23:
m <= k & l <= n implies A |^ (k, l) c= A |^ (m, n)
proof
assume
A1: m <= k & l <= n;
thus thesis
proof
let x be object;
assume x in A |^ (k, l);
then consider kl such that
A2: k <= kl & kl <= l and
A3: x in A |^ kl by Th19;
m <= kl & kl <= n by A1,A2,XXREAL_0:2;
hence thesis by A3,Th19;
end;
end;
theorem
m <= k & k <= n implies A |^ (m, n) = A |^ (m, k) \/ A |^ (k, n)
proof
A1: A |^ (m, n) c= A |^ (m, k) \/ A |^ (k, n)
proof
let x be object;
assume x in A |^ (m, n);
then consider l such that
A2: m <= l & l <= n & x in A |^ l by Th19;
l <= k or l > k;
then x in A |^ (m, k) or x in A |^ (k, n) by A2,Th19;
hence thesis by XBOOLE_0:def 3;
end;
assume m <= k & k <= n;
then A |^ (m, k) c= A |^ (m, n) & A |^ (k, n) c= A |^ (m, n) by Th23;
then A |^ (m, k) \/ A |^ (k, n) c= A |^ (m, n) by XBOOLE_1:8;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem Th25:
m <= k & k <= n implies A |^ (m, n) = A |^ (m, k) \/ A |^ (k + 1 , n)
proof
assume that
A1: m <= k and
A2: k <= n;
per cases;
suppose
A3: k < n;
m <= k + 1 by A1,NAT_1:13;
then
A4: A |^ (k + 1, n) c= A |^ (m, n) by Th23;
A5: A |^ (m, n) c= A |^ (m, k) \/ A |^ (k + 1, n)
proof
let x be object;
assume x in A |^ (m, n);
then consider mn such that
A6: m <= mn and
A7: mn <= n and
A8: x in A |^ mn by Th19;
A9: mn >= k + 1 implies x in A |^ (k + 1, n) by A7,A8,Th19;
mn <= k implies x in A |^ (m, k) by A6,A8,Th19;
hence thesis by A9,NAT_1:13,XBOOLE_0:def 3;
end;
A |^ (m, k) c= A |^ (m, n) by A3,Th23;
then A |^ (m, k) \/ A |^ (k + 1, n) c= A |^ (m, n) by A4,XBOOLE_1:8;
hence thesis by A5,XBOOLE_0:def 10;
end;
suppose
A10: k >= n;
then k + 1 > n + 0 by XREAL_1:8;
then A |^ (k + 1, n) = {} by Th21;
hence thesis by A2,A10,XXREAL_0:1;
end;
end;
theorem Th26:
m <= n + 1 implies A |^ (m, n + 1) = A |^ (m, n) \/ (A |^ (n + 1 ))
proof
assume
A1: m <= n + 1;
per cases by A1,NAT_1:8;
suppose
A2: m <= n;
n < n + 1 by NAT_1:13;
then A |^ (m, n + 1) = A |^ (m, n) \/ A |^ (n + 1, n + 1) by A2,Th25;
hence thesis by Th22;
end;
suppose
A3: m = n + 1;
then
A4: m > n by NAT_1:13;
thus A |^ (m, n + 1) = {} \/ A |^ (n + 1) by A3,Th22
.= A |^ (m, n) \/ A |^ (n + 1) by A4,Th21;
end;
end;
theorem
m <= n implies A |^ (m, n) = A |^ m \/ A |^ (m + 1, n)
proof
assume
A1: m <= n;
per cases by A1,XXREAL_0:1;
suppose
m < n;
then A |^ (m, n) = A |^ (m, m) \/ A |^ (m + 1, n) by Th25;
hence thesis by Th22;
end;
suppose
A2: m = n;
then
A3: m + 1 > n by NAT_1:13;
thus A |^ (m, n) = A |^ m \/ {} by A2,Th22
.= A |^ m \/ A |^ (m + 1, n) by A3,Th21;
end;
end;
theorem Th28:
A |^ (n, n + 1) = A |^ n \/ A |^ (n + 1)
proof
thus A |^ (n, n + 1) = A |^ (n, n) \/ A |^ (n + 1) by Th26,NAT_1:11
.= A |^ n \/ A |^ (n + 1) by Th22;
end;
theorem Th29:
A c= B implies A |^ (m, n) c= B |^ (m, n)
proof
assume
A1: A c= B;
thus thesis
proof
let x be object;
assume x in A |^ (m, n);
then consider k such that
A2: m <= k & k <= n & x in A |^ k by Th19;
A |^ k c= B |^ k by A1,FLANG_1:37;
hence thesis by A2,Th19;
end;
end;
theorem Th30:
x in A & x <> <%>E & (m > 0 or n > 0) implies A |^ (m, n) <> { <%>E}
proof
assume that
A1: x in A and
A2: x <> <%>E and
A3: m > 0 or n > 0;
per cases by A3;
suppose
m > n;
hence thesis by Th21;
end;
suppose
A4: m <= n & m > 0;
A5: A |^ m <> {} by A1,FLANG_1:27;
A |^ m <> {<%>E} by A1,A2,A4,Th7;
then
A6: ex x being object st x in A |^ m & x <> <%>E by A5,ZFMISC_1:35;
A |^ m c= A |^ (m, n) by A4,Th20;
hence thesis by A6,TARSKI:def 1;
end;
suppose
A7: m <= n & n > 0;
A8: A |^ n <> {} by A1,FLANG_1:27;
A |^ n <> {<%>E} by A1,A2,A7,Th7;
then
A9: ex x being object st x in A |^ n & x <> <%>E by A8,ZFMISC_1:35;
A |^ n c= A |^ (m, n) by A7,Th20;
hence thesis by A9,TARSKI:def 1;
end;
end;
theorem Th31:
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
A1: A |^ (m, n) = {<%>E} and
A2: ( m > n or A <> {<%>E})&( m <> 0 or n <> 0) &( m <> 0 or A <> {});
per cases by A2;
suppose
m > n;
hence contradiction by A1,Th21;
end;
suppose
A3: m <= n & A <> {<%>E} & (m <> 0 or n <> 0 & A <> {} );
per cases by A3;
suppose
A4: m <> 0;
per cases;
suppose
A = {};
hence contradiction by A1,A4,Th21;
end;
suppose
A <> {};
then ex x being object st x in A & x <> <%>E by A3,ZFMISC_1:35;
hence contradiction by A1,A4,Th30;
end;
end;
suppose
A5: n <> 0 & A <> {};
then ex x being object st x in A & x <> <%>E by A3,ZFMISC_1:35;
hence contradiction by A1,A5,Th30;
end;
end;
end;
assume
A6: m <= n & A = {<%>E} or m = 0 & n = 0 or m = 0 & A = {};
per cases by A6;
suppose
A7: m <= n & A = {<%>E};
A8: now
let x be object;
assume x in {<%>E};
then
A9: x in {<%>E} |^ m by FLANG_1:29;
{<%>E} |^ m c= {<%>E} |^ (m, n) by A7,Th20;
hence x in A |^ (m, n) by A7,A9;
end;
now
let x be object;
assume x in A |^ (m, n);
then ex k st m <= k & k <= n & x in {<%>E} |^ k by A7,Th19;
hence x in {<%>E} by FLANG_1:29;
end;
hence thesis by A8,TARSKI:2;
end;
suppose
A10: m = 0 & n = 0;
A |^ (0, 0) = A |^ 0 by Th22
.= {<%>E} by FLANG_1:29;
hence thesis by A10;
end;
suppose
A11: m = 0 & A = {};
now
let x be object;
assume x in A |^ (1, n);
then ex k st 1 <= k & k <= n & x in A |^ k by Th19;
hence contradiction by A11,FLANG_1:27;
end;
then
A12: A |^ (1, n) = {} by XBOOLE_0:def 1;
A |^ (0, n) = A |^ (0, 0) \/ A |^ (0 + 1, n) by Th25
.= A |^ 0 \/ A |^ (0 + 1, n) by Th22
.= {<%>E} by A12,FLANG_1:29;
hence thesis by A11;
end;
end;
theorem Th32:
A |^ (m, n) c= A*
proof
let x be object;
assume x in A |^ (m, n);
then ex k st m <= k & k <= n & x in A |^ k by Th19;
hence thesis by FLANG_1:41;
end;
theorem Th33:
<%>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
A1: <%>E in A |^ (m, n) and
A2: m <> 0 &( m > n or not <%>E in A);
per cases by A2;
suppose
m <> 0 & m > n;
hence contradiction by A1,Th21;
end;
suppose
A3: m <> 0 & not <%>E in A;
consider k such that
A4: m <= k and
k <= n and
A5: <%>E in A |^ k by A1,Th19;
k > 0 by A3,A4;
hence contradiction by A3,A5,FLANG_1:31;
end;
end;
assume
A6: m = 0 or m <= n & <%>E in A;
per cases by A6;
suppose
A7: m = 0;
{<%>E} = A |^ 0 by FLANG_1:29;
then
A8: {<%>E} c= A |^ (0, n) by Th20;
<%>E in {<%>E} by TARSKI:def 1;
hence thesis by A7,A8;
end;
suppose
m <= n & <%>E in A;
then <%>E in A |^ m & A |^ m c= A |^ (m, n) by Th20,FLANG_1:30;
hence thesis;
end;
end;
theorem Th34:
<%>E in A & m <= n implies A |^ (m, n) = A |^ n
proof
assume that
A1: <%>E in A and
A2: m <= n;
A3: A |^ (m, n) c= A |^ n
proof
A4: now
let k such that
A5: k <= n;
per cases by A5,XXREAL_0:1;
suppose
k < n;
hence A |^ k c= A |^ n by A1,FLANG_1:36;
end;
suppose
k = n;
hence A |^ k c= A |^ n;
end;
end;
let x be object;
assume x in A |^ (m, n);
then consider k such that
m <= k and
A6: k <= n and
A7: x in A |^ k by Th19;
A |^ k c= A |^ n by A4,A6;
hence thesis by A7;
end;
A |^ n c= A |^ (m, n) by A2,Th20;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem Th35:
A |^ (m, n) ^^ (A |^ k) = (A |^ k) ^^ (A |^ (m, n))
proof
A1: now
let x be object;
assume x in (A |^ k) ^^ (A |^ (m, n));
then consider a, b such that
A2: a in (A |^ k) and
A3: b in A |^ (m, n) and
A4: x = a ^ b by FLANG_1:def 1;
consider mn such that
A5: m <= mn & mn <= n and
A6: b in A |^ mn by A3,Th19;
A |^ mn c= A |^ (m, n) by A5,Th20;
then
A7: (A |^ mn) ^^ (A |^ k) c= (A |^ (m, n)) ^^ (A |^ k) by FLANG_1:17;
a ^ b in (A |^ k) ^^ (A |^ mn) by A2,A6,FLANG_1:def 1;
then a ^ b in (A |^ mn) ^^ (A |^ k) by Th12;
hence x in (A |^ (m, n)) ^^ (A |^ k) by A4,A7;
end;
now
let x be object;
assume x in (A |^ (m, n)) ^^ (A |^ k);
then consider a, b such that
A8: a in A |^ (m, n) and
A9: b in (A |^ k) and
A10: x = a ^ b by FLANG_1:def 1;
consider mn such that
A11: m <= mn & mn <= n and
A12: a in A |^ mn by A8,Th19;
A |^ mn c= A |^ (m, n) by A11,Th20;
then
A13: (A |^ k) ^^ (A |^ mn) c= (A |^ k) ^^ (A |^ (m, n)) by FLANG_1:17;
a ^ b in (A |^ mn) ^^ (A |^ k) by A9,A12,FLANG_1:def 1;
then a ^ b in (A |^ k) ^^ (A |^ mn) by Th12;
hence x in (A |^ k) ^^ (A |^ (m, n)) by A10,A13;
end;
hence thesis by A1,TARSKI:2;
end;
theorem Th36:
(A |^ (m, n)) ^^ A = A ^^ (A |^ (m, n))
proof
thus (A |^ (m, n)) ^^ A = (A |^ (m, n)) ^^ (A |^ 1) by FLANG_1:25
.= (A |^ 1) ^^ (A |^ (m, n)) by Th35
.= A ^^ (A |^ (m, n)) by FLANG_1:25;
end;
theorem Th37:
m <= n & k <= l implies (A |^ (m, n)) ^^ (A |^ (k, l)) = A |^ (m + k, n + l)
proof
assume
A1: m <= n & k <= l;
A2: now
let x be object;
assume x in A |^ (m + k, n + l);
then consider i such that
A3: m + k <= i & i <= n + l and
A4: x in A |^ i by Th19;
consider mn, kl such that
A5: mn + kl = i and
A6: m <= mn & mn <= n & k <= kl & kl <= l by A1,A3,Th2;
A |^ mn c= A |^ (m, n) & A |^ kl c= A |^ (k, l) by A6,Th20;
then (A |^ mn) ^^ (A |^ kl) c= (A |^ (m, n)) ^^ (A |^ (k, l)) by FLANG_1:17
;
then (A |^ (mn + kl)) c= (A |^ (m, n)) ^^ (A |^ (k, l)) by FLANG_1:33;
hence x in (A |^ (m, n)) ^^ (A |^ (k, l)) by A4,A5;
end;
now
let x be object;
assume x in (A |^ (m, n)) ^^ (A |^ (k, l));
then consider a, b such that
A7: a in A |^ (m, n) and
A8: b in A |^ (k, l) and
A9: x = a ^ b by FLANG_1:def 1;
consider kl such that
A10: k <= kl and
A11: kl <= l and
A12: b in A |^ kl by A8,Th19;
consider mn such that
A13: m <= mn and
A14: mn <= n and
A15: a in A |^ mn by A7,Th19;
A16: mn + kl <= n + l by A14,A11,XREAL_1:7;
a ^ b in A |^ (mn + kl) & m + k <= mn + kl by A13,A15,A10,A12,FLANG_1:40
,XREAL_1:7;
hence x in A |^ (m + k, n + l) by A9,A16,Th19;
end;
hence thesis by A2,TARSKI:2;
end;
theorem Th38:
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 Th37
.= (A |^ (m, n)) ^^ (A |^ 1) by Th22
.= (A |^ (m, n)) ^^ A by FLANG_1:25;
end;
suppose
A1: m > n;
then A |^ (m, n) = {} by Th21;
then
A2: (A |^ (m, n)) ^^ A = {} by FLANG_1:12;
m + 1 > n + 1 by A1,XREAL_1:8;
hence thesis by A2,Th21;
end;
end;
theorem Th39:
(A |^ (m, n)) ^^ (A |^ (k, l)) = (A |^ (k, l)) ^^ (A |^ (m, n))
proof
per cases;
suppose
A1: m <= n & k <= l;
hence (A |^ (m, n)) ^^ (A |^ (k, l)) = A |^ (m + k, n + l) by Th37
.= (A |^ (k, l)) ^^ (A |^ (m, n)) by A1,Th37;
end;
suppose
m > n;
then
A2: A |^ (m, n) = {} by Th21;
then (A |^ (m, n)) ^^ (A |^ (k, l)) = {} by FLANG_1:12;
hence thesis by A2,FLANG_1:12;
end;
suppose
k > l;
then
A3: A |^ (k, l) = {} by Th21;
then (A |^ (m, n)) ^^ (A |^ (k, l)) = {} by FLANG_1:12;
hence thesis by A3,FLANG_1:12;
end;
end;
theorem Th40:
(A |^ (m, n)) |^ k = A |^ (m * k, n * k)
proof
per cases;
suppose
A1: m <= n;
defpred P[Nat] means (A |^ (m, n)) |^ $1 = A |^ (m * $1, n * $1);
A2: now
let k;
A3: m * k <= n * k by A1,XREAL_1:64;
assume P[k];
then
(A |^ (m, n)) |^ (k + 1) = (A |^ (m * k, n * k)) ^^ (A |^ (m, n)) by
FLANG_1:23
.= A |^ (m * k + m, n * k + n) by A1,A3,Th37
.= A |^ (m * (k + 1), n * (k + 1));
hence P[k + 1];
end;
(A |^ (m, n)) |^ 0 = {<%>E} by FLANG_1:24
.= A |^ 0 by FLANG_1:24
.= A |^ (m * 0, n * 0) by Th22;
then
A4: P[0];
for k holds P[k] from NAT_1:sch 2(A4, A2);
hence thesis;
end;
suppose
A5: k = 0;
hence (A |^ (m, n)) |^ k = {<%>E} by FLANG_1:24
.= A |^ 0 by FLANG_1:24
.= A |^ (m * k, n * k) by A5,Th22;
end;
suppose
A6: m > n & k <> 0;
then A |^ (m, n) = {} by Th21;
then
A7: (A |^ (m, n)) |^ k = {} by A6,FLANG_1:27;
m * k > n * k by A6,XREAL_1:68;
hence thesis by A7,Th21;
end;
end;
theorem Th41:
(A |^ (k + 1)) |^ (m, n) c= ((A |^ k) |^ (m, n)) ^^ (A |^ (m, n) )
proof
let x be object;
assume x in (A |^ (k + 1)) |^ (m, n);
then consider mn such that
A1: m <= mn & mn <= n and
A2: x in (A |^ (k + 1)) |^ mn by Th19;
A |^ mn c= A |^ (m, n) by A1,Th20;
then
A3: ((A |^ k) |^ (m, n)) ^^ (A |^ mn) c= ((A |^ k) |^ (m, n)) ^^ (A |^ (m,
n)) by FLANG_1:17;
x in A |^ ((k + 1) * mn) by A2,FLANG_1:34;
then x in A |^ (k * mn + mn);
then x in (A |^ (k * mn)) ^^ (A |^ mn) by FLANG_1:33;
then
A4: x in ((A |^ k) |^ mn) ^^ (A |^ mn) by FLANG_1:34;
(A |^ k) |^ mn c= (A |^ k) |^ (m, n) by A1,Th20;
then ((A |^ k) |^ mn) ^^ (A |^ mn) c= ((A |^ k) |^ (m, n)) ^^ (A |^ mn) by
FLANG_1:17;
then x in ((A |^ k) |^ (m, n)) ^^ (A |^ mn) by A4;
hence thesis by A3;
end;
theorem Th42:
(A |^ k) |^ (m, n) c= A |^ (k * m, k * n)
proof
per cases;
suppose
A1: m <= n;
defpred P[Nat] means (A |^ $1) |^ (m, n) c= A |^ ($1 * m, $1 * n);
A2: now
let l;
A3: l * m <= l * n by A1,XREAL_1:64;
assume P[l];
then
A4: ((A |^ l) |^ (m, n)) ^^ ((A |^ 1) |^ (m, n)) c= (A |^ (l * m, l * n)
) ^^ ((A |^ 1) |^ (m, n)) by FLANG_1:17;
(A |^ (l + 1)) |^ (m, n) c= ((A |^ l) |^ (m, n)) ^^ (A |^ (m, n)) by Th41
;
then
A5: (A |^ (l + 1)) |^ (m, n) c= ((A |^ l) |^ (m, n)) ^^ ((A |^ 1) |^ (m,
n)) by FLANG_1:25;
(A |^ (l * m, l * n)) ^^ ((A |^ 1) |^ (m, n)) = (A |^ (l * m, l * n
)) ^^ (A |^ (m, n)) by FLANG_1:25
.= A |^ (l * m + m, l * n + n) by A1,A3,Th37
.= A |^ ((l + 1) * m, (l + 1) * n);
hence P[l + 1] by A5,A4,XBOOLE_1:1;
end;
(A |^ 0) |^ (m, n) = {<%>E} |^ (m, n) by FLANG_1:24
.= {<%>E} by A1,Th31
.= A |^ 0 by FLANG_1:24
.= A |^ (0 * m, 0 * n) by Th22;
then
A6: P[0];
for l holds P[l] from NAT_1:sch 2(A6, A2);
hence thesis;
end;
suppose
m > n;
then (A |^ k) |^ (m, n) = {} by Th21;
hence thesis;
end;
end;
theorem
(A |^ k) |^ (m, n) c= (A |^ (m, n)) |^ k
proof
(A |^ (m, n)) |^ k = A |^ (m * k, n * k) by Th40;
hence thesis by Th42;
end;
theorem
(A |^ (k + l)) |^ (m, n) c= ((A |^ k) |^ (m, n)) ^^ ((A |^ l) |^ (m, n ))
proof
let x be object;
assume x in (A |^ (k + l)) |^ (m, n);
then consider mn such that
A1: m <= mn & mn <= n and
A2: x in (A |^ (k + l)) |^ mn by Th19;
x in A |^ ((k + l) * mn) by A2,FLANG_1:34;
then x in A |^ (k * mn + l * mn);
then x in (A |^ (k * mn)) ^^ (A |^ (l * mn)) by FLANG_1:33;
then consider a, b such that
A3: a in A |^ (k * mn) and
A4: b in A |^ (l * mn) and
A5: x = a ^ b by FLANG_1:def 1;
b in (A |^ l) |^ mn by A4,FLANG_1:34;
then
A6: b in (A |^ l) |^ (m, n) by A1,Th19;
a in (A |^ k) |^ mn by A3,FLANG_1:34;
then a in (A |^ k) |^ (m, n) by A1,Th19;
hence thesis by A5,A6,FLANG_1:def 1;
end;
theorem Th45:
A |^ (0, 0) = {<%>E}
proof
thus A |^ (0, 0) = A |^ 0 by Th22
.= {<%>E} by FLANG_1:24;
end;
theorem Th46:
A |^ (0, 1) = {<%>E} \/ A
proof
thus A |^ (0, 1) = A |^ 0 \/ A |^ (0 + 1) by Th28
.= {<%>E} \/ A |^ 1 by FLANG_1:24
.= {<%>E} \/ A by FLANG_1:25;
end;
theorem
A |^ (1, 1) = A
proof
thus A |^ (1, 1) = A |^ 1 by Th22
.= A by FLANG_1:25;
end;
theorem
A |^ (0, 2) = {<%>E} \/ A \/ (A ^^ A)
proof
thus A |^ (0, 2) = A |^ (0, 1) \/ A |^ (1 + 1) by Th26
.= {<%>E} \/ A \/ A |^ (1 + 1) by Th46
.= {<%>E} \/ A \/ (A ^^ A) by FLANG_1:26;
end;
theorem
A |^ (1, 2) = A \/ (A ^^ A)
proof
thus A |^ (1, 2) = A |^ 1 \/ A |^ (1 + 1) by Th28
.= A \/ A |^ 2 by FLANG_1:25
.= A \/ (A ^^ A) by FLANG_1:26;
end;
theorem
A |^ (2, 2) = A ^^ A
proof
thus A |^ (2, 2) = A |^ 2 by Th22
.= A ^^ A by FLANG_1:26;
end;
theorem Th51:
m > 0 & A |^ (m, n) = {x} implies for mn st m <= mn & mn <= n
holds A |^ mn = {x}
proof
assume that
A1: m > 0 and
A2: A |^ (m, n) = {x};
given mn such that
A3: m <= mn & mn <= n and
A4: A |^ mn <> {x};
per cases;
suppose
A5: A |^ mn = {};
x in A |^ (m, n) by A2,TARSKI:def 1;
then
A6: ex i st m <= i & i <= n & x in A |^ i by Th19;
A = {} by A5,FLANG_1:27;
hence contradiction by A1,A6,FLANG_1:27;
end;
suppose
A |^ mn <> {};
then consider y being object such that
A7: y in A |^ mn and
A8: y <> x by A4,ZFMISC_1:35;
y in A |^ (m, n) by A3,A7,Th19;
hence contradiction by A2,A8,TARSKI:def 1;
end;
end;
theorem Th52:
m <> n & A |^ (m, n) = {x} implies x = <%>E
proof
assume that
A1: m <> n and
A2: A |^ (m, n) = {x};
per cases;
suppose
m > n;
hence thesis by A2,Th21;
end;
suppose
A3: m = 0 & m <= n;
then {<%>E} = A |^ m by FLANG_1:24;
then <%>E in A |^ m by TARSKI:def 1;
then <%>E in A |^ (m, n) by A3,Th19;
hence thesis by A2;
end;
suppose
m > 0 & m <= n;
then A |^ m = {x} & A |^ n = {x} by A2,Th51;
hence thesis by A1,Th10;
end;
end;
theorem Th53:
<%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
A1: <%x%> in A |^ (m, n);
then ex mn st m <= mn & mn <= n & <%x%> in A |^ mn by Th19;
hence thesis by A1,Th9,Th21;
end;
assume that
A2: <%x%> in A and
A3: m <= n and
A4: <%>E in A & n > 0 or m <= 1 & 1 <= n;
per cases by A4;
suppose
<%>E in A & n > 0;
then A c= A |^ n by FLANG_1:35;
hence thesis by A2,A3,Th19;
end;
suppose
A5: m <= 1 & 1 <= n;
<%x%> in A |^ 1 by A2,FLANG_1:25;
hence thesis by A5,Th19;
end;
end;
theorem
(A /\ B) |^ (m, n) c= (A |^ (m, n)) /\ (B |^ (m, n))
proof
let x be object;
assume x in (A /\ B) |^ (m, n);
then consider mn such that
A1: m <= mn & mn <= n and
A2: x in (A /\ B) |^ mn by Th19;
A3: (A /\ B) |^ mn c= (A |^ mn) /\ (B |^ mn) by FLANG_1:39;
then x in B |^ mn by A2,XBOOLE_0:def 4;
then
A4: x in B |^ (m, n) by A1,Th19;
x in A |^ mn by A2,A3,XBOOLE_0:def 4;
then x in A |^ (m, n) by A1,Th19;
hence thesis by A4,XBOOLE_0:def 4;
end;
theorem
(A |^ (m, n)) \/ (B |^ (m, n)) c= (A \/ B) |^ (m, n)
proof
let x be object;
assume
A1: x in (A |^ (m, n)) \/ (B |^ (m, n));
per cases by A1,XBOOLE_0:def 3;
suppose
x in A |^ (m, n);
then consider mn such that
A2: m <= mn & mn <= n and
A3: x in A |^ mn by Th19;
A4: (A |^ mn) \/ (B |^ mn) c= (A \/ B) |^ mn by FLANG_1:38;
x in (A |^ mn) \/ (B |^ mn) by A3,XBOOLE_0:def 3;
hence thesis by A2,A4,Th19;
end;
suppose
x in B |^ (m, n);
then consider mn such that
A5: m <= mn & mn <= n and
A6: x in B |^ mn by Th19;
A7: (A |^ mn) \/ (B |^ mn) c= (A \/ B) |^ mn by FLANG_1:38;
x in (A |^ mn) \/ (B |^ mn) by A6,XBOOLE_0:def 3;
hence thesis by A5,A7,Th19;
end;
end;
theorem
(A |^ (m, n)) |^ (k, l) c= A |^ (m * k, n * l)
proof
let x be object;
assume x in (A |^ (m, n)) |^ (k, l);
then consider kl such that
A1: k <= kl & kl <= l and
A2: x in (A |^ (m, n)) |^ kl by Th19;
m * k <= m * kl & n * kl <= n * l by A1,NAT_1:4;
then
A3: A |^ (m * kl, n * kl) c= A |^ (m * k, n * l) by Th23;
x in A |^ (m * kl, n * kl) by A2,Th40;
hence thesis by A3;
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 Th33;
hence thesis by FLANG_1:16;
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 that
A1: m <= n & k <= l and
A2: A c= C |^ (m, n) & B c= C |^ (k, l);
thus thesis
proof
let x be object;
assume x in A ^^ B;
then consider a, b such that
A3: a in A & b in B and
A4: x = a ^ b by FLANG_1:def 1;
a ^ b in C |^ (m, n) ^^ C |^ (k, l) by A2,A3,FLANG_1:def 1;
hence thesis by A1,A4,Th37;
end;
end;
theorem
(A |^ (m, n))* c= A*
proof
let x be object;
assume x in (A |^ (m, n))*;
then consider k such that
A1: x in A |^ (m, n) |^ k by FLANG_1:41;
A |^ (m, n) |^ k = A |^ (m * k, n * k) & A |^ (m * k, n * k) c= A* by Th32
,Th40;
hence thesis by A1;
end;
theorem
(A*) |^ (m, n) c= A*
proof
let x be object;
assume x in (A*) |^ (m, n);
then consider mn such that
m <= mn and
mn <= n and
A1: x in (A*) |^ mn by Th19;
(A*) |^ mn c= A* by FLANG_1:65;
hence thesis by A1;
end;
theorem
m <= n & n > 0 implies (A*) |^ (m, n) = A*
proof
assume that
A1: m <= n and
A2: n > 0;
<%>E in A* by FLANG_1:48;
hence (A*) |^ (m, n) = (A*) |^ n by A1,Th34
.= A* by A2,FLANG_1:66;
end;
theorem
m <= n & n > 0 & <%>E in A implies (A |^ (m, n))* = A*
proof
assume that
A1: m <= n and
A2: n > 0 and
A3: <%>E in A;
thus (A |^ (m, n))* = (A |^ n)* by A1,A3,Th34
.= A* by A2,A3,Th16;
end;
theorem
m <= n & <%>E in A implies (A |^ (m, n))* = (A*) |^ (m, n)
proof
assume that
A1: m <= n and
A2: <%>E in A;
(A |^ (m, n))* = (A |^ n)* & A* |^ (m, n) = A* |^ n by A1,A2,Th34,FLANG_1:48;
hence thesis by A2,Th17;
end;
theorem Th64:
A c= B* implies A |^ (m, n) c= B*
proof
assume
A1: A c= B*;
thus thesis
proof
let x be object;
assume x in A |^ (m, n);
then consider mn such that
m <= mn and
mn <= n and
A2: x in A |^ mn by Th19;
A |^ mn c= B* by A1,FLANG_1:59;
hence thesis by A2;
end;
end;
theorem
A c= B* implies B* = (B \/ (A |^ (m, n)))* by Th64,FLANG_1:67;
theorem Th66:
A |^ (m, n) ^^ (A*) = A* ^^ (A |^ (m, n))
proof
A1: A* ^^ (A |^ (m, n)) c= A |^ (m, n) ^^ (A*)
proof
let x be object;
assume x in A* ^^ (A |^ (m, n));
then consider a, b such that
A2: a in A* and
A3: b in A |^ (m, n) and
A4: x = a ^ b by FLANG_1:def 1;
consider k such that
A5: a in A |^ k by A2,FLANG_1:41;
consider mn such that
A6: m <= mn & mn <= n and
A7: b in A |^ mn by A3,Th19;
A |^ k c= A* & A |^ mn c= A |^ (m, n) by A6,Th20,FLANG_1:42;
then
A8: A |^ mn ^^ (A |^ k) c= A |^ (m, n) ^^ (A*) by FLANG_1:17;
a ^ b in A |^ (mn + k) by A7,A5,FLANG_1:40;
then a ^ b in A |^ mn ^^ (A |^ k) by FLANG_1:33;
hence thesis by A4,A8;
end;
A |^ (m, n) ^^ (A*) c= A* ^^ (A |^ (m, n))
proof
let x be object;
assume x in A |^ (m, n) ^^ (A*);
then consider a, b such that
A9: a in A |^ (m, n) and
A10: b in A* and
A11: x = a ^ b by FLANG_1:def 1;
consider k such that
A12: b in A |^ k by A10,FLANG_1:41;
consider mn such that
A13: m <= mn & mn <= n and
A14: a in A |^ mn by A9,Th19;
A |^ k c= A* & A |^ mn c= A |^ (m, n) by A13,Th20,FLANG_1:42;
then
A15: A |^ k ^^ (A |^ mn) c= A* ^^ (A |^ (m, n)) by FLANG_1:17;
a ^ b in A |^ (k + mn) by A14,A12,FLANG_1:40;
then a ^ b in A |^ k ^^ (A |^ mn) by FLANG_1:33;
hence thesis by A11,A15;
end;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem
<%>E in A & m <= n implies A* = A* ^^ (A |^ (m, n))
proof
assume that
A1: <%>E in A and
A2: m <= n;
A3: ex k st m + k = n by A2,NAT_1:10;
defpred P[Nat] means A* = A* ^^ (A |^ (m, m + $1));
A4: now
let i;
assume
A5: P[i];
A |^ (m, m + (i + 1)) = A |^ (m, m + i) \/ (A |^ (m + i + 1)) by Th26,
NAT_1:11;
then
A* ^^ (A |^ (m, m + (i + 1))) = A* \/ (A* ^^ (A |^ (m + i + 1))) by A5,
FLANG_1:20
.= A* \/ A* by A1,FLANG_1:55;
hence P[i + 1];
end;
A* = A* ^^ (A |^ m) by A1,FLANG_1:55
.= A* ^^ (A |^ (m, m + 0)) by Th22;
then
A6: P[0];
for i holds P[i] from NAT_1:sch 2(A6, A4);
hence thesis by A3;
end;
theorem
A |^ (m, n) |^ k c= A* by Th32,FLANG_1:59;
theorem Th69:
A |^ k |^ (m, n) c= A*
proof
let x be object;
assume x in A |^ k |^ (m, n);
then consider mn such that
m <= mn and
mn <= n and
A1: x in A |^ k |^ mn by Th19;
A2: A |^ (k * mn) c= A* by FLANG_1:42;
x in A |^ (k * mn) by A1,FLANG_1:34;
hence thesis by A2;
end;
theorem
m <= n implies (A |^ m)* c= (A |^ (m, n))* by Th20,FLANG_1:61;
theorem Th71:
(A |^ (m, n)) |^ (k, l) c= A*
proof
let x be object;
assume x in (A |^ (m, n)) |^ (k, l);
then consider kl such that
k <= kl and
kl <= l and
A1: x in (A |^ (m, n)) |^ kl by Th19;
(A |^ (m, n)) |^ kl c= A* by Th32,FLANG_1:59;
hence thesis by A1;
end;
theorem Th72:
<%>E in A & k <= n & l <= n implies A |^ (k, n) = A |^ (l, n)
proof
assume that
A1: <%>E in A and
A2: k <= n and
A3: l <= n;
thus A |^ (k, n) = A |^ n by A1,A2,Th34
.= A |^ (l, n) by A1,A3,Th34;
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 Th73:
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
defpred P[set] means ex k st k <= 1 & $1 = A |^ k;
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;
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
A4: k <= 1 & x in A |^ k;
defpred P[set] means ex k st k <= 1 & $1 = A |^ k;
consider B such that
A5: x in B and
A6: P[B] by A4;
reconsider A = { C: P[C] } as Subset-Family of E^omega from DOMAIN_1:sch 7;
B in A by A6;
hence thesis by A5,TARSKI:def 4;
end;
theorem
n <= 1 implies A |^ n c= A?
by Th73;
theorem Th75:
A? = (A |^ 0) \/ (A |^ 1)
proof
now
let x be object;
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
A1: k <= 1 and
A2: x in A |^ k by Th73;
k = 0 or k = 1 by A1,NAT_1:25;
hence thesis by A2;
end;
given k such that
A3: ( k = 0 or k = 1)& x in A |^ k;
thus thesis by A3,Th73;
end;
hence x in A? iff x in A |^ 0 or x in A |^ 1;
end;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th76:
A? = {<%>E} \/ A
proof
A |^ 0 = {<%>E} & A |^ 1 = A by FLANG_1:24,25;
hence thesis by Th75;
end;
theorem
A c= A?
proof
A? = {<%>E} \/ A by Th76;
hence thesis by XBOOLE_1:7;
end;
theorem Th78:
x in A? iff x = <%>E or x in A
proof
x in A? iff x in {<%>E} \/ A by Th76;
then x in A? iff x in {<%>E} or x in A by XBOOLE_0:def 3;
hence thesis by TARSKI:def 1;
end;
theorem Th79:
A? = A |^ (0, 1)
proof
thus A? = (A |^ 0) \/ (A |^ (0 + 1)) by Th75
.= A |^ (0, 1) by Th28;
end;
theorem Th80:
A? = A iff <%>E in A
proof
thus A? = A implies <%>E in A
proof
assume A? = A;
then A = {<%>E} \/ A by Th76;
hence thesis by ZFMISC_1:39;
end;
assume <%>E in A;
then A = {<%>E} \/ A by ZFMISC_1:40;
hence thesis by Th76;
end;
registration
let E, A;
cluster A? -> non empty;
coherence
proof
<%>E in A? by Th78;
hence thesis;
end;
end;
theorem
A?? = A?
proof
<%>E in A? by Th78;
hence thesis by Th80;
end;
theorem
A c= B implies A? c= B?
proof
assume A c= B;
then A |^ (0, 1) c= B |^ (0, 1) by Th29;
then A? c= B |^ (0, 1) by Th79;
hence thesis by Th79;
end;
theorem
x in A & x <> <%>E implies A? <> {<%>E}
proof
assume
A1: x in A & x <> <%>E;
A? = A |^ (0, 1) by Th79;
hence thesis by A1,Th30;
end;
theorem
A? = {<%>E} iff A = {} or A = {<%>E}
proof
A? = A |^ (0, 1) by Th79;
hence thesis by Th31;
end;
theorem
(A*)? = A* & (A?)* = A*
proof
thus (A*)? = {<%>E} \/ (A*) by Th76
.= A* by FLANG_1:48,ZFMISC_1:40;
thus (A?)* = ({<%>E} \/ A)* by Th76
.= A* by FLANG_1:48,68;
end;
theorem
A? c= A*
proof
A? = A |^ (0, 1) by Th79;
hence thesis by Th32;
end;
theorem
(A /\ B)? = (A?) /\ (B?)
proof
thus (A /\ B)? = {<%>E} \/ (A /\ B) by Th76
.= ({<%>E} \/ A) /\ ({<%>E} \/ B) by XBOOLE_1:24
.= (A?) /\ ({<%>E} \/ B) by Th76
.= (A?) /\ (B?) by Th76;
end;
theorem
(A?) \/ (B?) = (A \/ B)?
proof
thus (A \/ B)? = {<%>E} \/ (A \/ B) by Th76
.= (A \/ {<%>E}) \/ (B \/ {<%>E}) by XBOOLE_1:5
.= (A?) \/ (B \/ {<%>E}) by Th76
.= (A?) \/ (B?) by Th76;
end;
theorem
A? = {x} implies x = <%>E
proof
A? = A |^ (0, 1) by Th79;
hence thesis by Th52;
end;
theorem
<%x%> in A? iff <%x%> in A
proof
A? = A |^ (0, 1) by Th79;
hence thesis by Th53;
end;
theorem
(A?) ^^ A = A ^^ (A?)
proof
A? = A |^ (0, 1) by Th79;
hence thesis by Th36;
end;
theorem
(A?) ^^ A = A |^ (1, 2)
proof
A? = A |^ (0, 1) by Th79;
then (A?) ^^ A = A |^ (0 + 1, 1 + 1) by Th38;
hence thesis;
end;
theorem Th93:
(A?) ^^ (A?) = A |^ (0, 2)
proof
A? = A |^ (0, 1) by Th79;
then (A?) ^^ (A?) = A |^ (0 + 0, 1 + 1) by Th37;
hence thesis;
end;
theorem Th94:
(A?) |^ k = (A?) |^ (0, k)
proof
<%>E in A? by Th78;
hence thesis by Th34;
end;
theorem Th95:
(A?) |^ k = A |^ (0, k)
proof
defpred P[Nat] means (A?) |^ $1 = A |^ (0, $1);
A1: now
let k;
assume
A2: P[k];
(A?) |^ (k + 1) = ((A?) |^ k) ^^ ((A?) |^ 1) by FLANG_1:33
.= A |^ (0, k) ^^ (A?) by A2,FLANG_1:25
.= A |^ (0, k) ^^ (A |^ (0, 1)) by Th79
.= A |^ (0 + 0, k + 1) by Th37;
hence P[k + 1];
end;
(A?) |^ 0 = {<%>E} by FLANG_1:24
.= A |^ (0, 0) by Th45;
then
A3: P[0];
for k holds P[k] from NAT_1:sch 2(A3, A1);
hence thesis;
end;
theorem Th96:
m <= n implies A? |^ (m, n) = A? |^ (0, n)
proof
assume
A1: m <= n;
<%>E in A? by Th78;
hence thesis by A1,Th72;
end;
theorem Th97:
A? |^ (0, n) = A |^ (0, n)
proof
thus A? |^ (0, n) = A? |^ n by Th94
.= A |^ (0, n) by Th95;
end;
theorem Th98:
m <= n implies A? |^ (m, n) = A |^ (0, n)
proof
assume m <= n;
hence A? |^ (m, n) = A? |^ (0, n) by Th96
.= A |^ (0, n) by Th97;
end;
theorem
(A |^ (1, n))? = A |^ (0, n)
proof
thus (A |^ (1, n))? = {<%>E} \/ (A |^ (1, n)) by Th76
.= A |^ (0, 0) \/ (A |^ (0 + 1, n)) by Th45
.= A |^ (0, n) by Th25;
end;
theorem
<%>E in A & <%>E in B implies A? c= A ^^ B & A? c= B ^^ A
proof
assume that
A1: <%>E in A and
A2: <%>E in B;
<%>E in B ^^ A by A1,A2,FLANG_1:15;
then
A3: {<%>E} c= B ^^ A by ZFMISC_1:31;
<%>E in A ^^ B by A1,A2,FLANG_1:15;
then
A4: {<%>E} c= A ^^ B by ZFMISC_1:31;
A c= B ^^ A by A2,FLANG_1:16;
then
A5: {<%>E} \/ A c= B ^^ A by A3,XBOOLE_1:8;
A c= A ^^ B by A2,FLANG_1:16;
then {<%>E} \/ A c= A ^^ B by A4,XBOOLE_1:8;
hence thesis by A5,Th76;
end;
theorem
A c= A ^^ (B?) & A c= (B?) ^^ A
proof
<%>E in B? by Th78;
hence thesis by FLANG_1:16;
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:17;
hence thesis by Th93;
end;
theorem
<%>E in A & n > 0 implies A? c= A |^ n
proof
assume that
A1: <%>E in A and
A2: n > 0;
<%>E in A |^ n by A1,FLANG_1:30;
then
A3: {<%>E} c= A |^ n by ZFMISC_1:31;
A c= A |^ n by A1,A2,FLANG_1:35;
then {<%>E} \/ A c= A |^ n by A3,XBOOLE_1:8;
hence thesis by Th76;
end;
theorem
(A?) ^^ (A |^ k) = (A |^ k) ^^ (A?)
proof
thus (A?) ^^ (A |^ k) = ({<%>E} \/ A) ^^ (A |^ k) by Th76
.= ({<%>E} ^^ (A |^ k)) \/ (A ^^ (A |^ k)) by FLANG_1:20
.= ({<%>E} ^^ (A |^ k)) \/ ((A |^ k) ^^ A) by FLANG_1:32
.= (A |^ k) \/ ((A |^ k) ^^ A) by FLANG_1:13
.= ((A |^ k) ^^ {<%>E}) \/ ((A |^ k) ^^ A) by FLANG_1:13
.= (A |^ k) ^^ (A \/ {<%>E}) by FLANG_1:20
.= (A |^ k) ^^ (A?) by Th76;
end;
theorem Th105:
A c= B* implies A? c= B*
proof
assume A c= B*;
then A |^ (0, 1) c= B* by Th64;
hence thesis by Th79;
end;
theorem
A c= B* implies B* = (B \/ (A?))* by Th105,FLANG_1:67;
theorem
A? ^^ (A*) = A* ^^ (A?)
proof
thus A? ^^ (A*) = A |^ (0, 1) ^^ (A*) by Th79
.= A* ^^ (A |^ (0, 1)) by Th66
.= A* ^^ (A?) by Th79;
end;
theorem
A? ^^ (A*) = A*
proof
thus A? ^^ (A*) = ({<%>E} \/ A) ^^ (A*) by Th76
.= {<%>E} ^^ (A*) \/ A ^^ (A*) by FLANG_1:20
.= A* \/ A ^^ (A*) by FLANG_1:13
.= A* by FLANG_1:53,XBOOLE_1:12;
end;
theorem
A? |^ k c= A*
proof
A? |^ k = (A |^ (0, 1)) |^ k by Th79;
hence thesis by Th32,FLANG_1:59;
end;
theorem
(A |^ k)? c= A*
proof
(A |^ k)? = (A |^ k) |^ (0, 1) by Th79;
hence thesis by Th69;
end;
theorem
(A?) ^^ (A |^ (m, n)) = (A |^ (m, n)) ^^ (A?)
proof
(A |^ (0, 1)) ^^ (A |^ (m, n)) = (A |^ (m, n)) ^^ (A |^ (0, 1)) by Th39;
then (A?) ^^ (A |^ (m, n)) = (A |^ (m, n)) ^^ (A |^ (0, 1)) by Th79;
hence thesis by Th79;
end;
theorem
(A?) ^^ (A |^ k) = A |^ (k, k + 1)
proof
(A |^ (0, 1)) ^^ (A |^ k) = (A |^ (0, 1)) ^^ (A |^ (k, k)) by Th22
.= A |^ (0 + k, 1 + k) by Th37;
hence thesis by Th79;
end;
theorem
A? |^ (m, n) c= A*
proof
per cases;
suppose
m <= n;
then A? |^ (m, n) = A |^ (0, n) by Th98;
hence thesis by Th32;
end;
suppose
m > n;
then A? |^ (m, n) = {} by Th21;
hence thesis;
end;
end;
theorem
(A |^ (m, n))? c= A*
proof
(A |^ (m, n))? = (A |^ (m, n)) |^ (0, 1) by Th79;
hence thesis by Th71;
end;
theorem
A? = (A \ {<%>E})?
proof
thus A? = {<%>E} \/ A by Th76
.= {<%>E} \/ (A \ {<%>E}) by XBOOLE_1:39
.= (A \ {<%>E})? by Th76;
end;
theorem
A c= B? implies A? c= B?
proof
<%>E in B? by Th78;
then
A1: {<%>E} c= B? by ZFMISC_1:31;
assume A c= B?;
then {<%>E} \/ A c= B? by A1,XBOOLE_1:8;
hence thesis by Th76;
end;
theorem
A c= B? implies B? = (B \/ A)?
proof
assume
A1: A c= B?;
thus (B \/ A)? = {<%>E} \/ (B \/ A) by Th76
.= ({<%>E} \/ B) \/ A by XBOOLE_1:4
.= B? \/ A by Th76
.= B? by A1,XBOOLE_1:12;
end;