:: On same equivalents of well-foundedness
::  by Piotr Rudnicki and Andrzej Trybulec
::
:: Received February 25, 1997
:: Copyright (c) 1997-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies FUNCT_1, PARTFUN1, TARSKI, RELAT_1, SUBSET_1, CARD_1, XBOOLE_0,
      CARD_5, ORDINAL2, ORDERS_2, WELLORD1, STRUCT_0, WAYBEL_0, XXREAL_0,
      ZFMISC_1, SETFAM_1, ORDINAL1, CARD_2, FINSET_1, FUNCOP_1, FUNCT_4, NAT_1,
      ARYTM_3, NUMBERS, WELLFND1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
      RELAT_1, FUNCT_1, BINOP_1, SETFAM_1, DOMAIN_1, XCMPLX_0, NAT_1, STRUCT_0,
      RELSET_1, PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1, WELLORD1, ORDINAL2,
      FINSET_1, CARD_2, ORDERS_2, CARD_5, RFUNCT_3, WAYBEL_0;
 constructors SETFAM_1, WELLORD1, BINOP_1, FUNCT_4, ORDINAL2, CARD_2, REALSET1,
      CARD_5, RFUNCT_3, WAYBEL_0, RELSET_1;
 registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCOP_1,
      CARD_1, CARD_5, STRUCT_0, WAYBEL_0, FUNCT_1, ZFMISC_1;
 requirements NUMERALS, SUBSET, BOOLE;


begin :: Preliminaries
:: General preliminaries

theorem :: 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;

scheme :: WELLFND1:sch 1
  PFSeparation {X, Y() -> set, P[set]}: ex PFS being Subset of PFuncs(X(), Y()
  ) st for pfs being PartFunc of X(), Y() holds pfs in PFS iff P[pfs];

:: Cardinals

registration
  let X be set;
  cluster nextcard X -> non empty;
end;

registration
  cluster regular for Aleph;
end;

theorem :: WELLFND1:2
  for M being regular Aleph, X being set st X c= M & card X in M
  holds sup X in M;

:: Relational structures

theorem :: WELLFND1:3
  for R being RelStr, x being set holds (the InternalRel of R)-Seg
  x c= the carrier of R;

definition
  let R be RelStr, X be Subset of R;
  redefine attr X is lower means
:: WELLFND1:def 1

  for x, y being object st x in X & [y, x] in the InternalRel of R
   holds y in X;
end;

theorem :: WELLFND1:4
  for R being RelStr, X being Subset of R, x being set st X is
  lower & x in X holds (the InternalRel of R)-Seg x c= X;

theorem :: WELLFND1:5
  for R being RelStr, X being lower Subset of R, Y being Subset of
  R, x being set st Y = X \/ {x} & (the InternalRel of R)-Seg x c= X holds Y is
  lower;

begin :: Well-founded relational structures

definition
  let R be RelStr;
  attr R is well_founded means
:: WELLFND1:def 2

  the InternalRel of R is_well_founded_in the carrier of R;
end;

registration
  cluster non empty well_founded for RelStr;
end;

definition
  let R be RelStr, X be Subset of R;
  attr X is well_founded means
:: WELLFND1:def 3

  the InternalRel of R is_well_founded_in X;
end;

registration
  let R be RelStr;
  cluster well_founded for Subset of R;
end;

definition
  let R be RelStr;
  func well_founded-Part R -> Subset of R means
:: WELLFND1:def 4

  it = union {S where S is Subset of R : S is well_founded lower};
end;

registration
  let R be RelStr;
  cluster well_founded-Part R -> lower well_founded;
end;

theorem :: WELLFND1:6
  for R being non empty RelStr, x be Element of R holds {x} is
  well_founded Subset of R;

theorem :: WELLFND1:7
  for R being RelStr, X, Y being well_founded Subset of R st X is
  lower holds X \/ Y is well_founded Subset of R;

theorem :: WELLFND1:8
  for R being RelStr holds R is well_founded iff well_founded-Part
  R = the carrier of R;

theorem :: WELLFND1:9
  for R being non empty RelStr, x being Element of R st (the
  InternalRel of R)-Seg x c= well_founded-Part R holds x in well_founded-Part R
;

:: Well-founded induction

scheme :: WELLFND1:sch 2
  WFMin {R() -> non empty RelStr, x() -> Element of R(), P[set]}: ex x being
Element of R() st P[x] & not ex y being Element of R() st x <> y & P[y] & [y,x]
  in the InternalRel of R()
provided
 P[x()] and
 R() is well_founded;

:: WF iff WFInduction

theorem :: 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;

scheme :: WELLFND1:sch 3
  WFInduction {R() -> non empty RelStr, P[set]}: for x being Element of R()
  holds P[x]
provided
 for x being Element of R() st for y being Element of R() st y <> x &
[y,x] in the InternalRel of R() holds P[y] holds P[x] and
 R() is well_founded;

:: Well-foundedness and recursive definitions

definition
  let R be non empty RelStr, V be non empty set, H be Function of [:the
  carrier of R, PFuncs(the carrier of R, V):], V, F be Function;
  pred F is_recursively_expressed_by H means
:: WELLFND1:def 5

  for x being Element of R holds F.x = H.(x, F|(the InternalRel of R)-Seg x);
end;

:: 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, 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;

:: Uniqueness implies well-foundedness

theorem :: WELLFND1:12
  for R being non empty RelStr, V being non trivial set st for H being
Function of [:the carrier of R, PFuncs(the carrier of R, V):], V, 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;

:: Well-foundedness implies uniqueness

theorem :: WELLFND1:13
  for R being non empty well_founded RelStr, V being non empty set, H
being Function of [:the carrier of R, PFuncs(the carrier of R, V):], V, 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;

:: Well-foundedness and omega chains

definition
  let R be RelStr, f be sequence of R;

  attr f is descending means
:: WELLFND1:def 6

  for n being Nat holds f.(n+1)
  <> f.n & [f.(n+1), f.n] in the InternalRel of R;
end;

:: omega chains

theorem :: WELLFND1:14
  for R being non empty RelStr holds R is well_founded iff not ex f
  being sequence of R st f is descending;