:: Definition of Flat Poset and Existence Theorems for Recursive Call
::  by Kazuhisa Ishida , Yasunari Shidama and Adam Grabowski
:: 
:: Received February 11, 2014
:: Copyright (c) 2014-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 POSET_2, ORDERS_1, RELAT_1, RELAT_2, XBOOLE_0, STRUCT_0, FUNCT_1,
      FUNCT_2, NAT_1, TREES_2, LATTICE3, TARSKI, ORDERS_2, ORDINAL2, ARYTM_3,
      SEQM_3, LATTICES, YELLOW_0, POSET_1, NATTRA_1, MSAFREE1, ZFMISC_1,
      SUBSET_1, NUMBERS, CARD_1, XXREAL_0, ABIAN, PARTFUN1, MCART_1, YELLOW_3,
      ORDINAL1, WAYBEL_0, FINSET_1, TREES_1, PREFER_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1,
      FINSET_1, CARD_1, ORDERS_1, RELSET_1, PARTFUN1, DOMAIN_1, FUNCT_2,
      BINOP_1, FUNCOP_1, ORDINAL1, STRUCT_0, ORDERS_2, ORDERS_3, NUMBERS,
      NAT_1, XTUPLE_0, XXREAL_0, ABIAN, XCMPLX_0, FUNCT_3, POSET_1, LATTICES,
      YELLOW_2, YELLOW_3, LATTICE3, YELLOW_0, WAYBEL_0, LATTICE7, MCART_1;
 constructors RELAT_2, PARTFUN1, ORDERS_2, ORDERS_3, FUNCOP_1, FUNCT_3,
      FINSET_1, LATTICE7, CARD_1, BINOP_1, FUNCT_4, NAT_1, REAL_1, DOMAIN_1,
      XXREAL_0, ARYTM_0, NUMBERS, XCMPLX_0, XREAL_0, ARYTM_1, ABIAN, XTUPLE_0,
      LATTICE3, YELLOW_0, YELLOW_2, YELLOW_3, POSET_1, RELSET_1, MCART_1;
 registrations XBOOLE_0, ORDINAL1, SUBSET_1, RELSET_1, PARTFUN1, FUNCT_2,
      STRUCT_0, ORDERS_2, ORDERS_3, XREAL_0, NAT_1, RELAT_1, YELLOW_0,
      YELLOW_3, WAYBEL10, POSET_1, YELLOW10, XTUPLE_0, FINSET_1;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin :: Preliminaries

 reserve a,Z1,Z2,Z3 for set,
         x,y,z for object,
         k for Nat;

theorem :: POSET_2:1
  for P being lower-bounded non empty Poset,
      p being Element of P
        st p is_<=_than the carrier of P
            holds p = Bottom P;

theorem :: POSET_2:2
  for P being chain-complete non empty Poset,
      L being non empty Chain of P
  for p being Element of P st p in L holds p <= sup L;

theorem :: POSET_2:3
  for P being chain-complete non empty Poset,
      L being non empty Chain of P
  for p1 being Element of P st
     (for p being Element of P st p in L holds p<=p1) holds sup L <= p1;

begin :: Product of Poset

theorem :: POSET_2:4
  for P,Q being non empty RelStr,
      x being object holds
    x is Element of [:P,Q:]
     iff ex p being Element of P,q being Element of Q st x = [p,q];

definition let P,Q be non empty Poset;
           let L be non empty Chain of [:P,Q:];
  redefine func proj1 L -> non empty Chain of P;
   redefine func proj2 L -> non empty Chain of Q;
end;

:: Product of Function

registration
  let P,Q1,Q2 be non empty Poset;
  let f1 be monotone Function of P,Q1;
  let f2 be monotone Function of P,Q2;
  cluster <:f1,f2:> -> monotone for Function of P, [:Q1,Q2:];
end;

registration
  let P,Q be chain-complete non empty Poset;
  cluster [:P,Q:] -> chain-complete;
end;

theorem :: POSET_2:5
  for P,Q being chain-complete non empty Poset,
      L being non empty Chain of [:P,Q:] holds
    sup L = [sup (proj1 L), sup (proj2 L)];

registration
  let P,Q1,Q2 be strict chain-complete non empty Poset;
  let f1 be continuous Function of P,Q1;
  let f2 be continuous Function of P,Q2;
  cluster <:f1,f2:> -> continuous for Function of P,[:Q1,Q2:];
end;

begin :: Flat Posets

definition let IT be RelStr;
  attr IT is flat means
:: POSET_2:def 1
  ex a being Element of IT st
    for x,y being Element of IT holds (x <= y iff x = a or x = y);
end;

registration
  cluster discrete -> reflexive for non empty RelStr;
end;

registration
  cluster trivial -> flat for discrete non empty RelStr;
end;

registration
  cluster strict non empty flat for Poset;
end;

registration
  cluster flat -> reflexive transitive antisymmetric for RelStr;
end;

registration
  cluster flat -> lower-bounded for non empty Poset;
end;

 reserve S for RelStr;
 reserve P,Q for non empty flat Poset;
 reserve p,p1,p2 for Element of P;
 reserve K for non empty Chain of P;

theorem :: POSET_2:6
  for P being non empty flat Poset,
      K being non empty Chain of P holds
    ex a being Element of P st K = {a} or K = {Bottom P, a};

theorem :: POSET_2:7
  for f being Function of P,Q holds
    ex a being Element of P st
      (K = {a} & f.:K = {f.a}) or
      (K = {Bottom P, a} & f.:K = {f.(Bottom P), f.a});

theorem :: POSET_2:8
  for f being Function of P,Q holds
    f.(Bottom P) = Bottom Q implies f is monotone;

theorem :: POSET_2:9
  K = {Bottom P, p} implies sup K = p;

registration
  cluster strict non empty flat chain-complete for Poset;
end;

:: If P,Q is non empty flat RelStr, then P,Q is always chain-complete poset
:: and function f : P -> Q st f.(Bottom P) = Bottom Q is always continuous
:: (so, it is monotone too).
:: So, we can use every theorems for continuous function on the non empty
:: chain-complete poset such as fix point theorem (see POSET_1).

registration
  cluster non empty flat -> chain-complete for Poset;
end;

theorem :: POSET_2:10
  for P,Q being strict non empty chain-complete flat Poset,
      f being Function of P,Q
     st f.(Bottom P) = Bottom Q holds f is continuous;

begin :: Primaries for existence theorem of recursive call using Flatten

 reserve X,Y for non empty set;

definition
  let X be non empty set;
  func FlatRelat(X) -> Relation of succ(X),succ(X) equals
:: POSET_2:def 2
    ({[X,X]} \/ [:{X},X:]) \/ id X;
end;

theorem :: POSET_2:11
  for x, y being Element of succ(X) holds
    [x,y] in FlatRelat(X) iff x = X or x = y;

definition let X be non empty set;
  func FlatPoset(X) -> strict non empty chain-complete flat Poset equals
:: POSET_2:def 3
    RelStr(#succ(X), FlatRelat(X)#);
end;

theorem :: POSET_2:12
  for x, y being Element of FlatPoset(X) holds
    x <= y iff x = X or x = y;

theorem :: POSET_2:13
  X is Element of FlatPoset(X);

registration
  let X;
  reduce Bottom FlatPoset(X) to X;
end;

definition
  let x be object;
  let X,Y be non empty set;
  let f be Function of X,Y;
  func Flatten(f,x) -> set equals
:: POSET_2:def 4
  f.x if x in X otherwise Y;
end;

definition
  let X,Y be non empty set;
  let f be Function of X,Y;
  func Flatten f -> Function of FlatPoset(X),FlatPoset(Y) means
:: POSET_2:def 5

    it.X = Y &
    for x being Element of FlatPoset(X) st x <> X holds it.x = f.x;
end;

registration
  let X,Y be non empty set;
  let f be Function of X,Y;
  cluster Flatten f -> continuous;
end;

theorem :: POSET_2:14
  for f being Function of X,Y st
    x in X holds (Flatten f).x in Y;

definition let X,Y;
  func FlatConF(X,Y) -> strict chain-complete non empty Poset equals
:: POSET_2:def 6
    ConPoset(FlatPoset(X),FlatPoset(Y));
end;

registration let L be flat Poset;
  cluster -> finite for Chain of L;
end;

registration
  cluster non empty flat lower-bounded for LATTICE;
end;

theorem :: POSET_2:15
  for L being non empty LATTICE,
      x being Element of L,
      A being Chain of x,x holds
    card A = 1;

theorem :: POSET_2:16
  for L being non empty flat lower-bounded LATTICE,
      x being Element of L,
      A being Chain of Bottom L, x holds
    card A <= 2;

theorem :: POSET_2:17
  for L being finite lower-bounded antisymmetric non empty LATTICE holds
    L is flat iff for x being Element of L holds height x <= 2;

begin :: Existence theorem of recursive call for sigle-equation

 reserve D for Subset of X;
 reserve I for Function of X,Y;
 reserve J for Function of [:X,Y:], Y;
 reserve E for Function of X,X;

definition
  let X be non empty set;
  let D be Subset of X;
  let E be Function of X,X;
  pred E is_well_founded_with_minimal_set D means
:: POSET_2:def 7
  ex l being Function of X,NAT st for x being Element of X holds
     (l.x <= 0 implies x in D) &
     (not x in D implies l.(E.x) < l.x);
end;

definition
  let X,Y be non empty set;
  let D be Subset of X;
  let I be Function of X,Y;
  let J be Function of [:X,Y:], Y;
  let x, y be object;
  func BaseFunc01(x,y,I,J,D) -> set equals
:: POSET_2:def 8
    I.x if x in D,
    J.[x,y] if (not x in D) & x in X & y in Y
    otherwise Y;
end;

definition
  let X,Y be non empty set;
  let D be Subset of X;
  let I be Function of X,Y;
  let J be Function of [:X,Y:], Y;
  let E be Function of X,X;
  let h be object;
  assume
  h is continuous Function of FlatPoset(X),FlatPoset(Y);
  func RecFunc01(h,E,I,J,D)
        -> continuous Function of FlatPoset(X),FlatPoset(Y) means
:: POSET_2:def 9

   for x being Element of FlatPoset(X),
       f being continuous Function of FlatPoset(X),FlatPoset(Y)
        st h = f holds
     it.x = BaseFunc01(x,f.((Flatten E).x),I,J,D);
end;

theorem :: POSET_2:18
  ex W being continuous Function of FlatConF(X,Y),FlatConF(X,Y)
    st for f being Element of ConFuncs(FlatPoset(X),FlatPoset(Y))
      holds W.f = RecFunc01(f,E,I,J,D);

theorem :: POSET_2:19
  ex f being set st f in ConFuncs(FlatPoset(X),FlatPoset(Y)) &
     f = RecFunc01(f,E,I,J,D);

theorem :: POSET_2:20
  E is_well_founded_with_minimal_set D implies
    ex f being continuous Function of FlatPoset(X),FlatPoset(Y) st
       for x being Element of X holds
           f.x in Y & f.x = BaseFunc01(x,f.(E.x),I,J,D);

:: Existence

theorem :: POSET_2:21
  E is_well_founded_with_minimal_set D implies
    ex f being Function of X,Y st
       for x being Element of X holds
         (x in D implies f.x = I.x) &
         (not x in D implies f.x = J.[x,f.(E.x)]);

:: Uniqueness

theorem :: POSET_2:22
  for f1,f2 being Function of X,Y holds
    E is_well_founded_with_minimal_set D &
    (for x being Element of X holds
       (x in D implies f1.x = I.x) &
       (not x in D implies f1.x = J.[x,f1.(E.x)])) &
    (for x being Element of X holds
       (x in D implies f2.x = I.x) &
       (not x in D implies f2.x = J.[x,f2.(E.x)]))
      implies f1 = f2;

begin :: Existence theorem of recursive calls for 2-equations

 reserve D for Subset of X;
 reserve I,I1,I2 for Function of X,Y;
 reserve J,J1,J2 for Function of [:X,Y,Y:], Y;
 reserve E1,E2 for Function of X,X;

definition
  let X be non empty set;
  let D be Subset of X;
  let E1,E2 be Function of X,X;
  pred E1,E2 is_well_founded_with_minimal_set D means
:: POSET_2:def 10
  ex l being Function of X,NAT st for x being Element of X holds
     (l.x <= 0 implies x in D) &
     (not x in D implies l.(E1.x) < l.x & l.(E2.x) < l.x);
end;

definition
  let X,Y be non empty set;
  let D be Subset of X;
  let I be Function of X,Y;
  let J be Function of [:X,Y,Y:], Y;
  let x, y1, y2 be object;
  func BaseFunc02(x,y1,y2,I,J,D) -> set equals
:: POSET_2:def 11
     I.x if x in D,
     J.[x,y1,y2] if (not x in D) & (x in X & y1 in Y & y2 in Y)
     otherwise Y;
end;

definition
  let X,Y be non empty set;
  let D be Subset of X;
  let I be Function of X,Y;
  let J be Function of [:X,Y,Y:], Y;
  let E1,E2 be Function of X,X;
  let h1,h2 be object;
  assume
h1 is continuous Function of FlatPoset(X),FlatPoset(Y) &
    h2 is continuous Function of FlatPoset(X),FlatPoset(Y);
  func RecFunc02(h1,h2,E1,E2,I,J,D)
        -> continuous Function of FlatPoset(X),FlatPoset(Y) means
:: POSET_2:def 12

   for x being Element of FlatPoset X,
       f1,f2 being continuous Function of FlatPoset(X),FlatPoset(Y)
       st h1 = f1 & h2 = f2 holds
     it.x = BaseFunc02(x,f1.((Flatten E1).x),f2.((Flatten E2).x),I,J,D);
end;

theorem :: POSET_2:23
  ex W being continuous Function of
            [:FlatConF(X,Y),FlatConF(X,Y):],FlatConF(X,Y)
     st for f being set
             st f in [:ConFuncs(FlatPoset(X),FlatPoset(Y)),
                       ConFuncs(FlatPoset(X),FlatPoset(Y)):]
            holds W.f = RecFunc02(f`1,f`2,E1,E2,I,J,D);

theorem :: POSET_2:24
  ex f,g being set st
     f in ConFuncs(FlatPoset(X),FlatPoset(Y)) &
     g in ConFuncs(FlatPoset(X),FlatPoset(Y)) &
     f = RecFunc02(f,g,E1,E2,I1,J1,D) &
     g = RecFunc02(f,g,E1,E2,I2,J2,D);

theorem :: POSET_2:25
  E1,E2 is_well_founded_with_minimal_set D implies
    ex f,g being continuous Function of FlatPoset(X),FlatPoset(Y) st
       for x being Element of X holds
           (f.x in Y & f.x = BaseFunc02(x,f.(E1.x),g.(E2.x),I1,J1,D) &
            g.x in Y & g.x = BaseFunc02(x,f.(E1.x),g.(E2.x),I2,J2,D));

:: Existence

theorem :: POSET_2:26
  E1,E2 is_well_founded_with_minimal_set D implies
    ex f,g being Function of X,Y st
       for x being Element of X holds
         (x in D implies f.x = I1.x & g.x = I2.x) &
         (not x in D implies f.x = J1.[x,f.(E1.x),g.(E2.x)] &
                             g.x = J2.[x,f.(E1.x),g.(E2.x)]);

:: Uniqueness

theorem :: POSET_2:27
  for f1,g1,f2,g2 being Function of X,Y holds
    E1,E2 is_well_founded_with_minimal_set D &
    (for x being Element of X holds
         (x in D implies f1.x = I1.x & g1.x = I2.x) &
         (not x in D implies f1.x = J1.[x,f1.(E1.x),g1.(E2.x)] &
                             g1.x = J2.[x,f1.(E1.x),g1.(E2.x)]) ) &
    (for x being Element of X holds
         (x in D implies f2.x = I1.x & g2.x = I2.x) &
         (not x in D implies f2.x = J1.[x,f2.(E1.x),g2.(E2.x)] &
                             g2.x = J2.[x,f2.(E1.x),g2.(E2.x)]) )
         implies f1 = f2 & g1 = g2;

:: In the case of I1 = I2 (=I) and J1 = J2 (=J), we get the following theorems.
:: For example, they are used to define the evaluate function for the binary tree(x) ,
:: when the treatments of the left side sub tree(E1.x) and the right side sub tree(E2.x) are same.

:: Existence
theorem :: POSET_2:28
  E1,E2 is_well_founded_with_minimal_set D implies
    ex f being Function of X,Y st
       for x being Element of X holds
         (x in D implies f.x = I.x) &
         (not x in D implies f.x = J.[x,f.(E1.x),f.(E2.x)]);

:: Uniqueness

theorem :: POSET_2:29
  for f1,f2 being Function of X,Y holds
    E1,E2 is_well_founded_with_minimal_set D &
    (for x being Element of X holds
       (x in D implies f1.x = I.x) &
       (not x in D implies f1.x = J.[x,f1.(E1.x),f1.(E2.x)])) &
    (for x being Element of X holds
       (x in D implies f2.x = I.x) &
       (not x in D implies f2.x = J.[x,f2.(E1.x),f2.(E2.x)]))
      implies f1 = f2;