Jaskinie Podróże Nurki Grafika Mizar Teksty Kulinaria Lemkov Namiary Mapa RSS English
Spelunka Trybików Mizar Artykuły Kwantyfikatory w wyrażeniach regularnych - co najmniej m wystąpień YAC Software
  Wróć

Mizar

Eddie

Artykuły

Równoważność automatów deter ministycznych i epsilon niedeter ministycznych

Etykietowane systemy tranzycji stanów

Kwantyfikatory w wyrażeniach regularnych - co najmniej m wystąpień

Systemy przepisywania słów

Kwantyfikatory w wyrażeniach regularnych - od m do n wystąpień

Języki formalne - konkatenacja i domknięcie

Boole'owskie właściwości zbiorów

Homomorfizmy i izomorfizmy grup; grupa ilorazowa

Liczby całkowite

Syntaktyka Mizara-MSE

Kwantyfikatory w wyrażeniach regularnych - co najmniej m wystąpień
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: Identyfikator Mizar Mathematical Library: FLANG_3.
Abstrakt w wersji PDF: tutaj.
Motorola Software Group, 2007.

Pliki: Abstrakt
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: 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

Pełny artykuł
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: 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 Subset-Family 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 Subset-Family 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 Subset-Family 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 Subset-Family 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