flang_2.miz
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;
theorem ::
FLANG_2:1
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 ::
FLANG_2:2
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 ::
FLANG_2:3
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;
theorem ::
FLANG_2:4
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
theorem ::
FLANG_2:5
(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 ::
FLANG_2:6
<%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 ::
FLANG_2:7
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 ::
FLANG_2:8
(
<%> 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 ::
FLANG_2:9
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 ::
FLANG_2:10
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 ::
FLANG_2:11
((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 ::
FLANG_2:12
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 ::
FLANG_2:13
(
<%> 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 ::
FLANG_2:14
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 ::
FLANG_2:15
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 ::
FLANG_2:16
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,
FLANG_1: 61;
((A
|^ n)
* )
c= (A
* ) by
FLANG_1: 64;
hence thesis by
A1,
XBOOLE_0:def 10;
end;
theorem ::
FLANG_2:17
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 ::
FLANG_2:18
A
c= (A
^^ (B
* )) & A
c= ((B
* )
^^ A)
proof
(
<%> E)
in (B
* ) by
FLANG_1: 48;
hence thesis by
FLANG_1: 16;
end;
begin
definition
let E, A;
let m, n;
::
FLANG_2:def1
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
theorem ::
FLANG_2:19
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 ::
FLANG_2:20
Th20: m
<= k & k
<= n implies (A
|^ k)
c= (A
|^ (m,n)) by
Th19;
theorem ::
FLANG_2:21
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 ::
FLANG_2:22
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 be
object holds x
in (A
|^ m) implies x
in (A
|^ (m,m)) by
Th19;
hence thesis by
A1,
TARSKI: 2;
end;
theorem ::
FLANG_2:23
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 ::
FLANG_2:24
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 ::
FLANG_2:25
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 ::
FLANG_2:26
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 ::
FLANG_2:27
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 ::
FLANG_2:28
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 ::
FLANG_2:29
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 ::
FLANG_2:30
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 be
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 be
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 ::
FLANG_2:31
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 be
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 be
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 ::
FLANG_2:32
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 ::
FLANG_2:33
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 ::
FLANG_2:34
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 ::
FLANG_2:35
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 ::
FLANG_2:36
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 ::
FLANG_2:37
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 ::
FLANG_2:38
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 ::
FLANG_2:39
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 ::
FLANG_2:40
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 ::
FLANG_2:41
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 ::
FLANG_2:42
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 ::
FLANG_2:43
((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 ::
FLANG_2:44
((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 ::
FLANG_2:45
Th45: (A
|^ (
0 ,
0 ))
=
{(
<%> E)}
proof
thus (A
|^ (
0 ,
0 ))
= (A
|^
0 ) by
Th22
.=
{(
<%> E)} by
FLANG_1: 24;
end;
theorem ::
FLANG_2:46
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 ::
FLANG_2:47
(A
|^ (1,1))
= A
proof
thus (A
|^ (1,1))
= (A
|^ 1) by
Th22
.= A by
FLANG_1: 25;
end;
theorem ::
FLANG_2:48
(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 ::
FLANG_2:49
(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 ::
FLANG_2:50
(A
|^ (2,2))
= (A
^^ A)
proof
thus (A
|^ (2,2))
= (A
|^ 2) by
Th22
.= (A
^^ A) by
FLANG_1: 26;
end;
theorem ::
FLANG_2:51
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 be
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 ::
FLANG_2:52
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 ::
FLANG_2:53
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 ::
FLANG_2:54
((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 ::
FLANG_2:55
((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 ::
FLANG_2:56
((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 ::
FLANG_2:57
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 ::
FLANG_2:58
m
<= n & k
<= l & A
c= (C
|^ (m,n)) & B
c= (C
|^ (k,l)) implies (A
^^ B)
c= (C
|^ ((m
+ k),(n
+ l)))
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 ::
FLANG_2:59
((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 ::
FLANG_2:60
((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 ::
FLANG_2:61
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 ::
FLANG_2:62
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 ::
FLANG_2:63
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 ::
FLANG_2:64
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 ::
FLANG_2:65
A
c= (B
* ) implies (B
* )
= ((B
\/ (A
|^ (m,n)))
* ) by
Th64,
FLANG_1: 67;
theorem ::
FLANG_2:66
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 ::
FLANG_2:67
(
<%> 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 ::
FLANG_2:68
((A
|^ (m,n))
|^ k)
c= (A
* ) by
Th32,
FLANG_1: 59;
theorem ::
FLANG_2:69
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 ::
FLANG_2:70
m
<= n implies ((A
|^ m)
* )
c= ((A
|^ (m,n))
* ) by
Th20,
FLANG_1: 61;
theorem ::
FLANG_2:71
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 ::
FLANG_2:72
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
definition
let E, A;
::
FLANG_2:def2
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
theorem ::
FLANG_2:73
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 ::
FLANG_2:74
n
<= 1 implies (A
|^ n)
c= (A
? ) by
Th73;
theorem ::
FLANG_2:75
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 ::
FLANG_2:76
Th76: (A
? )
= (
{(
<%> E)}
\/ A)
proof
(A
|^
0 )
=
{(
<%> E)} & (A
|^ 1)
= A by
FLANG_1: 24,
FLANG_1: 25;
hence thesis by
Th75;
end;
theorem ::
FLANG_2:77
A
c= (A
? )
proof
(A
? )
= (
{(
<%> E)}
\/ A) by
Th76;
hence thesis by
XBOOLE_1: 7;
end;
theorem ::
FLANG_2:78
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 ::
FLANG_2:79
Th79: (A
? )
= (A
|^ (
0 ,1))
proof
thus (A
? )
= ((A
|^
0 )
\/ (A
|^ (
0
+ 1))) by
Th75
.= (A
|^ (
0 ,1)) by
Th28;
end;
theorem ::
FLANG_2:80
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 ::
FLANG_2:81
((A
? )
? )
= (A
? )
proof
(
<%> E)
in (A
? ) by
Th78;
hence thesis by
Th80;
end;
theorem ::
FLANG_2:82
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 ::
FLANG_2:83
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 ::
FLANG_2:84
(A
? )
=
{(
<%> E)} iff A
=
{} or A
=
{(
<%> E)}
proof
(A
? )
= (A
|^ (
0 ,1)) by
Th79;
hence thesis by
Th31;
end;
theorem ::
FLANG_2:85
((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,
FLANG_1: 68;
end;
theorem ::
FLANG_2:86
(A
? )
c= (A
* )
proof
(A
? )
= (A
|^ (
0 ,1)) by
Th79;
hence thesis by
Th32;
end;
theorem ::
FLANG_2:87
((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 ::
FLANG_2:88
((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 ::
FLANG_2:89
(A
? )
=
{x} implies x
= (
<%> E)
proof
(A
? )
= (A
|^ (
0 ,1)) by
Th79;
hence thesis by
Th52;
end;
theorem ::
FLANG_2:90
<%x%>
in (A
? ) iff
<%x%>
in A
proof
(A
? )
= (A
|^ (
0 ,1)) by
Th79;
hence thesis by
Th53;
end;
theorem ::
FLANG_2:91
((A
? )
^^ A)
= (A
^^ (A
? ))
proof
(A
? )
= (A
|^ (
0 ,1)) by
Th79;
hence thesis by
Th36;
end;
theorem ::
FLANG_2:92
((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 ::
FLANG_2:93
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 ::
FLANG_2:94
Th94: ((A
? )
|^ k)
= ((A
? )
|^ (
0 ,k))
proof
(
<%> E)
in (A
? ) by
Th78;
hence thesis by
Th34;
end;
theorem ::
FLANG_2:95
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 ::
FLANG_2:96
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 ::
FLANG_2:97
Th97: ((A
? )
|^ (
0 ,n))
= (A
|^ (
0 ,n))
proof
thus ((A
? )
|^ (
0 ,n))
= ((A
? )
|^ n) by
Th94
.= (A
|^ (
0 ,n)) by
Th95;
end;
theorem ::
FLANG_2:98
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 ::
FLANG_2:99
((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 ::
FLANG_2:100
(
<%> 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 ::
FLANG_2:101
A
c= (A
^^ (B
? )) & A
c= ((B
? )
^^ A)
proof
(
<%> E)
in (B
? ) by
Th78;
hence thesis by
FLANG_1: 16;
end;
theorem ::
FLANG_2:102
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 ::
FLANG_2:103
(
<%> 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 ::
FLANG_2:104
((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 ::
FLANG_2:105
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 ::
FLANG_2:106
A
c= (B
* ) implies (B
* )
= ((B
\/ (A
? ))
* ) by
Th105,
FLANG_1: 67;
theorem ::
FLANG_2:107
((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 ::
FLANG_2:108
((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 ::
FLANG_2:109
((A
? )
|^ k)
c= (A
* )
proof
((A
? )
|^ k)
= ((A
|^ (
0 ,1))
|^ k) by
Th79;
hence thesis by
Th32,
FLANG_1: 59;
end;
theorem ::
FLANG_2:110
((A
|^ k)
? )
c= (A
* )
proof
((A
|^ k)
? )
= ((A
|^ k)
|^ (
0 ,1)) by
Th79;
hence thesis by
Th69;
end;
theorem ::
FLANG_2:111
((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 ::
FLANG_2:112
((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 ::
FLANG_2:113
((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 ::
FLANG_2:114
((A
|^ (m,n))
? )
c= (A
* )
proof
((A
|^ (m,n))
? )
= ((A
|^ (m,n))
|^ (
0 ,1)) by
Th79;
hence thesis by
Th71;
end;
theorem ::
FLANG_2:115
(A
? )
= ((A
\
{(
<%> E)})
? )
proof
thus (A
? )
= (
{(
<%> E)}
\/ A) by
Th76
.= (
{(
<%> E)}
\/ (A
\
{(
<%> E)})) by
XBOOLE_1: 39
.= ((A
\
{(
<%> E)})
? ) by
Th76;
end;
theorem ::
FLANG_2:116
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 ::
FLANG_2:117
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;