:: On same equivalents of well-foundedness
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received February 25, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users
begin
:: General preliminaries
theorem
Th1
:
:: WELLFND1:1
for
X
being
functional
set
st ( for
f
,
g
being
Function
st
f
in
X
&
g
in
X
holds
f
tolerates
g
) holds
union
X
is
Function
proof
end;
scheme
:: WELLFND1:sch 1
PFSeparation
{
F
1
()
->
set
,
F
2
()
->
set
,
P
1
[
set
] } :
ex
PFS
being
Subset
of
(
PFuncs
(
F
1
(),
F
2
())
)
st
for
pfs
being
PartFunc
of
F
1
(),
F
2
() holds
(
pfs
in
PFS
iff
P
1
[
pfs
] )
proof
end;
:: Cardinals
registration
let
X
be
set
;
cluster
nextcard
X
->
non
empty
;
coherence
not
nextcard
X
is
empty
by
CARD_1:def 3
;
end;
registration
cluster
non
empty
epsilon-transitive
epsilon-connected
ordinal
non
finite
cardinal
regular
for
set
;
existence
ex
b
1
being
Aleph
st
b
1
is
regular
by
CARD_5:30
;
end;
theorem
Th2
:
:: WELLFND1:2
for
M
being
regular
Aleph
for
X
being
set
st
X
c=
M
&
card
X
in
M
holds
sup
X
in
M
proof
end;
:: Relational structures
theorem
Th3
:
:: WELLFND1:3
for
R
being
RelStr
for
x
being
set
holds the
InternalRel
of
R
-Seg
x
c=
the
carrier
of
R
proof
end;
definition
let
R
be
RelStr
;
let
X
be
Subset
of
R
;
redefine
attr
X
is
lower
means
:
Def1
:
:: WELLFND1:def 1
for
x
,
y
being
set
st
x
in
X
&
[
y
,
x
]
in
the
InternalRel
of
R
holds
y
in
X
;
compatibility
(
X
is
lower
iff for
x
,
y
being
set
st
x
in
X
&
[
y
,
x
]
in
the
InternalRel
of
R
holds
y
in
X
)
proof
end;
end;
::
deftheorem
Def1
defines
lower
WELLFND1:def 1 :
for
R
being
RelStr
for
X
being
Subset
of
R
holds
(
X
is
lower
iff for
x
,
y
being
set
st
x
in
X
&
[
y
,
x
]
in
the
InternalRel
of
R
holds
y
in
X
);
theorem
Th4
:
:: WELLFND1:4
for
R
being
RelStr
for
X
being
Subset
of
R
for
x
being
set
st
X
is
lower
&
x
in
X
holds
the
InternalRel
of
R
-Seg
x
c=
X
proof
end;
theorem
Th5
:
:: WELLFND1:5
for
R
being
RelStr
for
X
being
lower
Subset
of
R
for
Y
being
Subset
of
R
for
x
being
set
st
Y
=
X
\/
{
x
}
& the
InternalRel
of
R
-Seg
x
c=
X
holds
Y
is
lower
proof
end;
begin
definition
let
R
be
RelStr
;
attr
R
is
well_founded
means
:
Def2
:
:: WELLFND1:def 2
the
InternalRel
of
R
is_well_founded_in
the
carrier
of
R
;
end;
::
deftheorem
Def2
defines
well_founded
WELLFND1:def 2 :
for
R
being
RelStr
holds
(
R
is
well_founded
iff the
InternalRel
of
R
is_well_founded_in
the
carrier
of
R
);
registration
cluster
non
empty
well_founded
for
RelStr
;
existence
ex
b
1
being
RelStr
st
( not
b
1
is
empty
&
b
1
is
well_founded
)
proof
end;
end;
definition
let
R
be
RelStr
;
let
X
be
Subset
of
R
;
attr
X
is
well_founded
means
:
Def3
:
:: WELLFND1:def 3
the
InternalRel
of
R
is_well_founded_in
X
;
end;
::
deftheorem
Def3
defines
well_founded
WELLFND1:def 3 :
for
R
being
RelStr
for
X
being
Subset
of
R
holds
(
X
is
well_founded
iff the
InternalRel
of
R
is_well_founded_in
X
);
registration
let
R
be
RelStr
;
cluster
well_founded
for
Element
of
bool
the
carrier
of
R
;
existence
ex
b
1
being
Subset
of
R
st
b
1
is
well_founded
proof
end;
end;
definition
let
R
be
RelStr
;
func
well_founded-Part
R
->
Subset
of
R
means
:
Def4
:
:: WELLFND1:def 4
it
=
union
{
S
where
S
is
Subset
of
R
: (
S
is
well_founded
&
S
is
lower
)
}
;
existence
ex
b
1
being
Subset
of
R
st
b
1
=
union
{
S
where
S
is
Subset
of
R
: (
S
is
well_founded
&
S
is
lower
)
}
proof
end;
uniqueness
for
b
1
,
b
2
being
Subset
of
R
st
b
1
=
union
{
S
where
S
is
Subset
of
R
: (
S
is
well_founded
&
S
is
lower
)
}
&
b
2
=
union
{
S
where
S
is
Subset
of
R
: (
S
is
well_founded
&
S
is
lower
)
}
holds
b
1
=
b
2
;
end;
::
deftheorem
Def4
defines
well_founded-Part
WELLFND1:def 4 :
for
R
being
RelStr
for
b
2
being
Subset
of
R
holds
(
b
2
=
well_founded-Part
R
iff
b
2
=
union
{
S
where
S
is
Subset
of
R
: (
S
is
well_founded
&
S
is
lower
)
}
);
registration
let
R
be
RelStr
;
cluster
well_founded-Part
R
->
lower
well_founded
;
coherence
(
well_founded-Part
R
is
lower
&
well_founded-Part
R
is
well_founded
)
proof
end;
end;
theorem
Th6
:
:: WELLFND1:6
for
R
being non
empty
RelStr
for
x
being
Element
of
R
holds
{
x
}
is
well_founded
Subset
of
R
proof
end;
theorem
Th7
:
:: WELLFND1:7
for
R
being
RelStr
for
X
,
Y
being
well_founded
Subset
of
R
st
X
is
lower
holds
X
\/
Y
is
well_founded
Subset
of
R
proof
end;
theorem
Th8
:
:: WELLFND1:8
for
R
being
RelStr
holds
(
R
is
well_founded
iff
well_founded-Part
R
=
the
carrier
of
R
)
proof
end;
theorem
Th9
:
:: WELLFND1:9
for
R
being non
empty
RelStr
for
x
being
Element
of
R
st the
InternalRel
of
R
-Seg
x
c=
well_founded-Part
R
holds
x
in
well_founded-Part
R
proof
end;
:: Well-founded induction
scheme
:: WELLFND1:sch 2
WFMin
{
F
1
()
->
non
empty
RelStr
,
F
2
()
->
Element
of
F
1
(),
P
1
[
set
] } :
ex
x
being
Element
of
F
1
() st
(
P
1
[
x
] & ( for
y
being
Element
of
F
1
() holds
( not
x
<>
y
or not
P
1
[
y
] or not
[
y
,
x
]
in
the
InternalRel
of
F
1
() ) ) )
provided
A1
:
P
1
[
F
2
()]
and
A2
:
F
1
() is
well_founded
proof
end;
:: WF iff WFInduction
theorem
Th10
:
:: WELLFND1:10
for
R
being non
empty
RelStr
holds
(
R
is
well_founded
iff for
S
being
set
st ( for
x
being
Element
of
R
st the
InternalRel
of
R
-Seg
x
c=
S
holds
x
in
S
) holds
the
carrier
of
R
c=
S
)
proof
end;
scheme
:: WELLFND1:sch 3
WFInduction
{
F
1
()
->
non
empty
RelStr
,
P
1
[
set
] } :
for
x
being
Element
of
F
1
() holds
P
1
[
x
]
provided
A1
: for
x
being
Element
of
F
1
() st ( for
y
being
Element
of
F
1
() st
y
<>
x
&
[
y
,
x
]
in
the
InternalRel
of
F
1
() holds
P
1
[
y
] ) holds
P
1
[
x
]
and
A2
:
F
1
() is
well_founded
proof
end;
:: Well-foundedness and recursive definitions
definition
let
R
be non
empty
RelStr
;
let
V
be non
empty
set
;
let
H
be
Function
of
[:
the
carrier
of
R
,
(
PFuncs
( the
carrier
of
R
,
V
)
)
:]
,
V
;
let
F
be
Function
;
pred
F
is_recursively_expressed_by
H
means
:
Def5
:
:: WELLFND1:def 5
for
x
being
Element
of
R
holds
F
.
x
=
H
.
(
x
,
(
F
|
(
the
InternalRel
of
R
-Seg
x
)
)
);
end;
::
deftheorem
Def5
defines
is_recursively_expressed_by
WELLFND1:def 5 :
for
R
being non
empty
RelStr
for
V
being non
empty
set
for
H
being
Function
of
[:
the
carrier
of
R
,
(
PFuncs
( the
carrier
of
R
,
V
)
)
:]
,
V
for
F
being
Function
holds
(
F
is_recursively_expressed_by
H
iff for
x
being
Element
of
R
holds
F
.
x
=
H
.
(
x
,
(
F
|
(
the
InternalRel
of
R
-Seg
x
)
)
) );
:: Well foundedness and existence
theorem
:: WELLFND1:11
for
R
being non
empty
RelStr
holds
(
R
is
well_founded
iff for
V
being non
empty
set
for
H
being
Function
of
[:
the
carrier
of
R
,
(
PFuncs
( the
carrier
of
R
,
V
)
)
:]
,
V
ex
F
being
Function
of the
carrier
of
R
,
V
st
F
is_recursively_expressed_by
H
)
proof
end;
:: Uniqueness implies well-foundedness
theorem
:: WELLFND1:12
for
R
being non
empty
RelStr
for
V
being non
trivial
set
st ( for
H
being
Function
of
[:
the
carrier
of
R
,
(
PFuncs
( the
carrier
of
R
,
V
)
)
:]
,
V
for
F1
,
F2
being
Function
of the
carrier
of
R
,
V
st
F1
is_recursively_expressed_by
H
&
F2
is_recursively_expressed_by
H
holds
F1
=
F2
) holds
R
is
well_founded
proof
end;
:: Well-foundedness implies uniqueness
theorem
:: WELLFND1:13
for
R
being non
empty
well_founded
RelStr
for
V
being non
empty
set
for
H
being
Function
of
[:
the
carrier
of
R
,
(
PFuncs
( the
carrier
of
R
,
V
)
)
:]
,
V
for
F1
,
F2
being
Function
of the
carrier
of
R
,
V
st
F1
is_recursively_expressed_by
H
&
F2
is_recursively_expressed_by
H
holds
F1
=
F2
proof
end;
:: Well-foundedness and omega chains
definition
let
R
be
RelStr
;
let
f
be
sequence
of
R
;
attr
f
is
descending
means
:
Def6
:
:: WELLFND1:def 6
for
n
being
Nat
holds
(
f
.
(
n
+
1
)
<>
f
.
n
&
[
(
f
.
(
n
+
1
)
)
,
(
f
.
n
)
]
in
the
InternalRel
of
R
);
end;
::
deftheorem
Def6
defines
descending
WELLFND1:def 6 :
for
R
being
RelStr
for
f
being
sequence
of
R
holds
(
f
is
descending
iff for
n
being
Nat
holds
(
f
.
(
n
+
1
)
<>
f
.
n
&
[
(
f
.
(
n
+
1
)
)
,
(
f
.
n
)
]
in
the
InternalRel
of
R
) );
:: omega chains
theorem
:: WELLFND1:14
for
R
being non
empty
RelStr
holds
(
R
is
well_founded
iff for
f
being
sequence
of
R
holds not
f
is
descending
)
proof
end;