:: On semilattice structure of {M}izar types
::  by Grzegorz Bancerek
::
:: Received August 8, 2003
:: Copyright (c) 2003-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 NUMBERS, ZFMISC_1, RELAT_2, REWRITE1, XBOOLE_0, ORDERS_2,
      PRELAMB, SUBSET_1, IDEAL_1, TARSKI, RELAT_1, STRUCT_0, ARYTM_3, XXREAL_0,
      WAYBEL_0, LATTICE3, LATTICES, EQREL_1, CARD_FIL, YELLOW_0, ORDINAL2,
      BINOP_1, FUNCT_1, OPOSET_1, CARD_1, FUNCOP_1, FINSUB_1, YELLOW_1,
      ARYTM_0, WELLORD2, FINSEQ_1, FUNCT_7, NAT_1, ORDINAL4, FINSET_1,
      FINSEQ_5, ARYTM_1, ABCMIZ_0, ABIAN, XCMPLX_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, RELAT_2, SUBSET_1, ORDINAL1,
      FINSUB_1, CARD_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1,
      ORDERS_1, FUNCOP_1, FINSET_1, FINSEQ_1, FUNCT_4, ALG_1, FINSEQ_5,
      NUMBERS, XCMPLX_0, NAT_1, DOMAIN_1, STRUCT_0, ORDERS_2, LATTICE3,
      REWRITE1, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_7, XXREAL_0;
 constructors FINSUB_1, NAT_1, FINSEQ_5, REWRITE1, BORSUK_1, LATTICE3,
      WAYBEL_0, YELLOW_1, FUNCOP_1, XREAL_0, NUMBERS;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_2, FINSET_1, FINSUB_1,
      XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, REWRITE1, STRUCT_0, LATTICE3,
      YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_7, YELLOW_9, ORDINAL1, CARD_1,
      RELSET_1;
 requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;


begin :: Semilattice of type widening

registration
  cluster reflexive -> complete for 1-element RelStr;
end;

definition
  let T be RelStr;
  mode type of T is Element of T;
end;

definition
  let T be RelStr;
  attr T is Noetherian means
:: ABCMIZ_0:def 1

  the InternalRel of T is co-well_founded;
end;

registration
  cluster -> Noetherian for 1-element RelStr;
end;

definition
  let T be non empty RelStr;
  redefine attr T is Noetherian means
:: ABCMIZ_0:def 2

  for A being non empty Subset of T
  ex a being Element of T st a in A & for b being Element of T st b in A holds
  not a < b;
end;

definition
  let T be Poset;
  attr T is Mizar-widening-like means
:: ABCMIZ_0:def 3
  T is sup-Semilattice & T is Noetherian;
end;

registration
  cluster Mizar-widening-like -> Noetherian with_suprema upper-bounded for
Poset;
end;

registration
  cluster Noetherian -> Mizar-widening-like for sup-Semilattice;
end;

registration
  cluster Mizar-widening-like for complete sup-Semilattice;
end;

registration
  let T be Noetherian RelStr;
  cluster the InternalRel of T -> co-well_founded;
end;

theorem :: ABCMIZ_0:1
  for T being Noetherian sup-Semilattice for I being Ideal of T
  holds ex_sup_of I, T & sup I in I;

begin :: Adjectives

definition
  struct AdjectiveStr (# adjectives -> set, non-op -> UnOp of the adjectives
  #);
end;

definition
  let A be AdjectiveStr;
  attr A is void means
:: ABCMIZ_0:def 4

  the adjectives of A is empty;
  mode adjective of A is Element of the adjectives of A;
end;

theorem :: ABCMIZ_0:2
  for A1,A2 being AdjectiveStr st the adjectives of A1 = the adjectives
  of A2 holds A1 is void implies A2 is void;

definition
  let A be AdjectiveStr;
  let a be Element of the adjectives of A;
  func non-a -> adjective of A equals
:: ABCMIZ_0:def 5
  (the non-op of A).a;
end;

theorem :: ABCMIZ_0:3
  for A1,A2 being AdjectiveStr st the AdjectiveStr of A1 = the
AdjectiveStr of A2 for a1 being adjective of A1, a2 being adjective of A2 st a1
  = a2 holds non-a1 = non-a2;

definition
  let A be AdjectiveStr;
  attr A is involutive means
:: ABCMIZ_0:def 6

  for a being adjective of A holds non-non-a = a;
  attr A is without_fixpoints means
:: ABCMIZ_0:def 7
  not ex a being adjective of A st non-a = a;
end;

theorem :: ABCMIZ_0:4
  for a1,a2 being set st a1 <> a2 for A being AdjectiveStr st the
adjectives of A = {a1,a2} & (the non-op of A).a1 = a2 & (the non-op of A).a2 =
  a1 holds A is non void involutive without_fixpoints;

theorem :: ABCMIZ_0:5
  for A1,A2 being AdjectiveStr st the AdjectiveStr of A1 = the
  AdjectiveStr of A2 holds A1 is involutive implies A2 is involutive;

theorem :: ABCMIZ_0:6
  for A1,A2 being AdjectiveStr st the AdjectiveStr of A1 = the
  AdjectiveStr of A2 holds A1 is without_fixpoints implies A2 is
  without_fixpoints;

registration
  cluster non void involutive without_fixpoints for strict AdjectiveStr;
end;

registration
  let A be non void AdjectiveStr;
  cluster the adjectives of A -> non empty;
end;

definition
  struct(RelStr,AdjectiveStr) TA-structure(# carrier, adjectives -> set,
    InternalRel -> (Relation of the carrier), non-op -> UnOp of the adjectives,
    adj-map -> Function of the carrier, Fin the adjectives #);
end;

registration
  let X be non empty set;
  let A be set;
  let r be Relation of X;
  let n be UnOp of A;
  let a be Function of X, Fin A;
  cluster TA-structure(#X,A,r,n,a#) -> non empty;
end;

registration
  let X be set;
  let A be non empty set;
  let r be Relation of X;
  let n be UnOp of A;
  let a be Function of X, Fin A;
  cluster TA-structure(#X,A,r,n,a#) -> non void;
end;

registration
  cluster 1-element reflexive non void involutive without_fixpoints
    strict for TA-structure;
end;

definition
  let T be TA-structure;
  let t be Element of T;
  func adjs t -> Subset of the adjectives of T equals
:: ABCMIZ_0:def 8
  (the adj-map of T).t;
end;

theorem :: ABCMIZ_0:7
  for T1,T2 being TA-structure st the TA-structure of T1 = the
  TA-structure of T2 for t1 being type of T1, t2 being type of T2 st t1 = t2
  holds adjs t1 = adjs t2;

definition
  let T be TA-structure;
  attr T is consistent means
:: ABCMIZ_0:def 9

  for t being type of T for a being
  adjective of T st a in adjs t holds not non-a in adjs t;
end;

theorem :: ABCMIZ_0:8
  for T1,T2 being TA-structure st the TA-structure of T1 = the
  TA-structure of T2 holds T1 is consistent implies T2 is consistent;

definition
  let T be non empty TA-structure;
  attr T is adj-structured means
:: ABCMIZ_0:def 10
  the adj-map of T is join-preserving Function
  of T, (BoolePoset the adjectives of T) opp;
end;

theorem :: ABCMIZ_0:9
  for T1,T2 being non empty TA-structure st the TA-structure of T1
  = the TA-structure of T2 holds T1 is adj-structured implies T2 is
  adj-structured;

definition
  let T be reflexive transitive antisymmetric with_suprema TA-structure;
  redefine attr T is adj-structured means
:: ABCMIZ_0:def 11

  for t1,t2 being type of T holds adjs(t1"\/"t2) = (adjs t1) /\ (adjs t2);
end;

theorem :: ABCMIZ_0:10
  for T being reflexive transitive antisymmetric with_suprema
TA-structure st T is adj-structured for t1,t2 being type of T st t1 <= t2 holds
  adjs t2 c= adjs t1;

definition
  let T be TA-structure;
  let a be Element of the adjectives of T;
  func types a -> Subset of T means
:: ABCMIZ_0:def 12

  for x being object holds x in it iff
  ex t being type of T st x = t & a in adjs t;
end;

definition
  let T be non empty TA-structure;
  let A be Subset of the adjectives of T;
  func types A -> Subset of T means
:: ABCMIZ_0:def 13

  for t being type of T holds t in
  it iff for a being adjective of T st a in A holds t in types a;
end;

theorem :: ABCMIZ_0:11
  for T1,T2 being TA-structure st the TA-structure of T1 = the
TA-structure of T2 for a1 being adjective of T1, a2 being adjective of T2 st a1
  = a2 holds types a1 = types a2;

theorem :: ABCMIZ_0:12
  for T being non empty TA-structure for a being adjective of T holds
  types a = {t where t is type of T: a in adjs t};

theorem :: ABCMIZ_0:13
  for T being TA-structure for t being type of T, a being
  adjective of T holds a in adjs t iff t in types a;

theorem :: ABCMIZ_0:14
  for T being non empty TA-structure for t being type of T, A
  being Subset of the adjectives of T holds A c= adjs t iff t in types A;

theorem :: ABCMIZ_0:15
  for T being non void TA-structure for t being type of T holds adjs t =
  {a where a is adjective of T: t in types a};

theorem :: ABCMIZ_0:16
  for T being non empty TA-structure holds types ({} the
  adjectives of T) = the carrier of T;

definition
  let T be TA-structure;
  attr T is adjs-typed means
:: ABCMIZ_0:def 14
  for a being adjective of T holds types a \/ types non-a is non empty;
end;

theorem :: ABCMIZ_0:17
  for T1,T2 being TA-structure st the TA-structure of T1 = the
  TA-structure of T2 holds T1 is adjs-typed implies T2 is adjs-typed;

registration
  cluster non void Mizar-widening-like involutive without_fixpoints consistent
adj-structured adjs-typed for complete upper-bounded 1-element reflexive
    transitive antisymmetric strict TA-structure;
end;

theorem :: ABCMIZ_0:18
  for T being consistent TA-structure for a being adjective of T holds
  types a misses types non-a;

registration
  let T be adj-structured reflexive transitive antisymmetric with_suprema
  TA-structure;
  let a be adjective of T;
  cluster types a -> lower directed;
end;

registration
  let T be adj-structured reflexive transitive antisymmetric with_suprema
  TA-structure;
  let A be Subset of the adjectives of T;
  cluster types A -> lower directed;
end;

begin :: Applicability of adjectives

definition
  let T be TA-structure;
  let t be Element of T;
  let a be adjective of T;
  pred a is_applicable_to t means
:: ABCMIZ_0:def 15

  ex t9 being type of T st t9 in types a & t9 <= t;
end;

definition
  let T be TA-structure;
  let t be type of T;
  let A be Subset of the adjectives of T;
  pred A is_applicable_to t means
:: ABCMIZ_0:def 16

  ex t9 being type of T st A c= adjs t9 & t9 <= t;
end;

theorem :: ABCMIZ_0:19
  for T being adj-structured reflexive transitive antisymmetric
with_suprema TA-structure for a being adjective of T for t being type of T st
  a is_applicable_to t holds types a /\ downarrow t is Ideal of T;

definition
  let T be non empty reflexive transitive TA-structure;
  let t be Element of T;
  let a be adjective of T;
  func a ast t -> type of T equals
:: ABCMIZ_0:def 17
  sup(types a /\ downarrow t);
end;

theorem :: ABCMIZ_0:20
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema TA-structure for t being type of T for a being
  adjective of T st a is_applicable_to t holds a ast t <= t;

theorem :: ABCMIZ_0:21
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema TA-structure for t being type of T for a being
  adjective of T st a is_applicable_to t holds a in adjs(a ast t);

theorem :: ABCMIZ_0:22
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema TA-structure for t being type of T for a being
  adjective of T st a is_applicable_to t holds a ast t in types a;

theorem :: ABCMIZ_0:23
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema TA-structure for t being type of T for a being
  adjective of T for t9 being type of T st t9 <= t & a in adjs t9 holds a
  is_applicable_to t & t9 <= a ast t;

theorem :: ABCMIZ_0:24
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema TA-structure for t being type of T for a being
  adjective of T st a in adjs t holds a is_applicable_to t & a ast t = t;

theorem :: ABCMIZ_0:25
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema TA-structure for t being type of T for a,b being
  adjective of T st a is_applicable_to t & b is_applicable_to a ast t holds b
  is_applicable_to t & a is_applicable_to b ast t & a ast (b ast t) = b ast (a
  ast t);

theorem :: ABCMIZ_0:26
  for T being adj-structured reflexive transitive antisymmetric
  with_suprema TA-structure for A being Subset of the adjectives of T for t
  being type of T st A is_applicable_to t holds types A /\ downarrow t is Ideal
  of T;

definition
  let T be non empty reflexive transitive TA-structure;
  let t be type of T;
  let A be Subset of the adjectives of T;
  func A ast t -> type of T equals
:: ABCMIZ_0:def 18
  sup(types A /\ downarrow t);
end;

theorem :: ABCMIZ_0:27
  for T being non empty reflexive transitive antisymmetric
  TA-structure for t being type of T holds ({} the adjectives of T) ast t = t;

definition
  let T be non empty non void reflexive transitive TA-structure;
  let t be type of T;
  let p be FinSequence of the adjectives of T;
  func apply(p,t) -> FinSequence of the carrier of T means
:: ABCMIZ_0:def 19

  len it =
  len p+1 & it.1 = t & for i being Element of NAT, a being adjective of T, t
  being type of T st i in dom p & a = p.i & t = it.i holds it.(i+1) = a ast t;
end;

registration
  let T be non empty non void reflexive transitive TA-structure;
  let t be type of T;
  let p be FinSequence of the adjectives of T;
  cluster apply(p,t) -> non empty;
end;

theorem :: ABCMIZ_0:28
  for T being non empty non void reflexive transitive TA-structure for t
  being type of T holds apply(<*> the adjectives of T, t) = <*t*>;

theorem :: ABCMIZ_0:29
  for T being non empty non void reflexive transitive TA-structure
for t being type of T, a be adjective of T holds apply(<*a*>, t) = <*t, a ast t
  *>;

definition
  let T be non empty non void reflexive transitive TA-structure;
  let t be type of T;
  let v be FinSequence of the adjectives of T;
  func v ast t -> type of T equals
:: ABCMIZ_0:def 20
  apply(v,t).(len v+1);
end;

theorem :: ABCMIZ_0:30
  for T being non empty non void reflexive transitive TA-structure for t
  being type of T holds (<*> the adjectives of T) ast t = t;

theorem :: ABCMIZ_0:31
  for T being non empty non void reflexive transitive TA-structure
  for t being type of T for a being adjective of T holds <*a*> ast t = a ast t;

theorem :: ABCMIZ_0:32
  for p,q being FinSequence for i being Nat st i >= 1 & i <
  len p holds (p$^q).i = p.i;

theorem :: ABCMIZ_0:33
  for p being non empty FinSequence, q being FinSequence for i
  being Nat st i < len q holds (p$^q).(len p+i) = q.(i+1);

theorem :: ABCMIZ_0:34
  for T being non empty non void reflexive transitive TA-structure
for t being type of T for v1,v2 being FinSequence of the adjectives of T holds
  apply(v1^v2, t) = apply(v1, t) $^ apply(v2, v1 ast t);

theorem :: ABCMIZ_0:35
  for T being non empty non void reflexive transitive TA-structure
for t being type of T for v1,v2 being FinSequence of the adjectives of T for i
  being Nat st i in dom v1 holds apply(v1^v2, t).i = apply(v1, t).i;

theorem :: ABCMIZ_0:36
  for T being non empty non void reflexive transitive TA-structure
for t being type of T for v1,v2 being FinSequence of the adjectives of T holds
  apply(v1^v2, t).(len v1+1) = v1 ast t;

theorem :: ABCMIZ_0:37
  for T being non empty non void reflexive transitive TA-structure
for t being type of T for v1,v2 being FinSequence of the adjectives of T holds
  v2 ast (v1 ast t) = v1^v2 ast t;

definition
  let T be non empty non void reflexive transitive TA-structure;
  let t be type of T;
  let v be FinSequence of the adjectives of T;
  pred v is_applicable_to t means
:: ABCMIZ_0:def 21

  for i being Nat, a being
  adjective of T, s being type of T st i in dom v & a = v.i & s = apply(v,t).i
  holds a is_applicable_to s;
end;

theorem :: ABCMIZ_0:38
  for T being non empty non void reflexive transitive TA-structure for t
  being type of T holds <*> the adjectives of T is_applicable_to t;

theorem :: ABCMIZ_0:39
  for T being non empty non void reflexive transitive TA-structure for t
  being type of T, a being adjective of T holds a is_applicable_to t iff <*a*>
  is_applicable_to t;

theorem :: ABCMIZ_0:40
  for T being non empty non void reflexive transitive TA-structure
for t being type of T for v1,v2 being FinSequence of the adjectives of T st v1^
v2 is_applicable_to t holds v1 is_applicable_to t & v2 is_applicable_to v1 ast
  t;

theorem :: ABCMIZ_0:41
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema non void TA-structure for t being type of T for v
  being FinSequence of the adjectives of T st v is_applicable_to t for i1,i2
being Nat st 1 <= i1 & i1 <= i2 & i2 <= len v+1 for t1,t2 being type
  of T st t1 = apply(v,t).i1 & t2 = apply(v,t).i2 holds t2 <= t1;

theorem :: ABCMIZ_0:42
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema non void TA-structure for t being type of T for v
  being FinSequence of the adjectives of T st v is_applicable_to t for s being
  type of T st s in rng apply(v, t) holds v ast t <= s & s <= t;

theorem :: ABCMIZ_0:43
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema non void TA-structure for t being type of T for v
being FinSequence of the adjectives of T st v is_applicable_to t holds v ast t
  <= t;

theorem :: ABCMIZ_0:44
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema non void TA-structure for t being type of T for v
being FinSequence of the adjectives of T st v is_applicable_to t holds rng v c=
  adjs (v ast t);

theorem :: ABCMIZ_0:45
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema non void TA-structure for t being type of T for v
  being FinSequence of the adjectives of T st v is_applicable_to t for A being
  Subset of the adjectives of T st A = rng v holds A is_applicable_to t;

theorem :: ABCMIZ_0:46
  for T being Noetherian adj-structured reflexive transitive
antisymmetric with_suprema non void TA-structure for t being type of T for v1,
  v2 being FinSequence of the adjectives of T st v1 is_applicable_to t & rng v2
  c= rng v1 for s being type of T st s in rng apply(v2,t) holds v1 ast t <= s;

theorem :: ABCMIZ_0:47
  for T being Noetherian adj-structured reflexive transitive
antisymmetric with_suprema non void TA-structure for t being type of T for v1,
  v2 being FinSequence of the adjectives of T st v1^v2 is_applicable_to t holds
  v2^v1 is_applicable_to t;

theorem :: ABCMIZ_0:48
  for T being Noetherian adj-structured reflexive transitive
antisymmetric with_suprema non void TA-structure for t being type of T for v1,
  v2 being FinSequence of the adjectives of T st v1^v2 is_applicable_to t holds
  v1^v2 ast t = v2^v1 ast t;

theorem :: ABCMIZ_0:49
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema TA-structure for t being type of T for A being
  Subset of the adjectives of T st A is_applicable_to t holds A ast t <= t;

theorem :: ABCMIZ_0:50
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema TA-structure for t being type of T for A being
Subset of the adjectives of T st A is_applicable_to t holds A c= adjs(A ast t);

theorem :: ABCMIZ_0:51
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema TA-structure for t being type of T for A being
Subset of the adjectives of T st A is_applicable_to t holds A ast t in types A;

theorem :: ABCMIZ_0:52
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema TA-structure for t being type of T for A being
Subset of the adjectives of T for t9 being type of T st t9 <= t & A c= adjs t9
  holds A is_applicable_to t & t9 <= A ast t;

theorem :: ABCMIZ_0:53
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema TA-structure for t being type of T for A being
Subset of the adjectives of T st A c= adjs t holds A is_applicable_to t & A ast
  t = t;

theorem :: ABCMIZ_0:54
  for T being TA-structure, t being type of T for A,B being Subset
  of the adjectives of T st A is_applicable_to t & B c= A holds B
  is_applicable_to t;

theorem :: ABCMIZ_0:55
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema non void TA-structure for t being type of T, a
being adjective of T for A,B being Subset of the adjectives of T st B = A \/ {a
  } & B is_applicable_to t holds a ast (A ast t) = B ast t;

theorem :: ABCMIZ_0:56
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema non void TA-structure for t being type of T for v
  being FinSequence of the adjectives of T st v is_applicable_to t for A being
  Subset of the adjectives of T st A = rng v holds v ast t = A ast t;

begin :: Subject function

definition
  let T be non empty non void TA-structure;
  func sub T -> Function of the adjectives of T, the carrier of T means
:: ABCMIZ_0:def 22


  for a being adjective of T holds it.a = sup(types a \/ types non-a);
end;

definition
  struct(TA-structure) TAS-structure(# carrier, adjectives -> set, InternalRel
    -> (Relation of the carrier), non-op -> UnOp of the adjectives, adj-map ->
    Function of the carrier, Fin the adjectives, sub-map -> Function of the
    adjectives, the carrier #);
end;

registration
  cluster non void reflexive 1-element strict for TAS-structure;
end;

definition
  let T be non empty non void TAS-structure;
  let a be adjective of T;
  func sub a -> type of T equals
:: ABCMIZ_0:def 23
  (the sub-map of T).a;
end;

definition
  let T be non empty non void TAS-structure;
  attr T is non-absorbing means
:: ABCMIZ_0:def 24
  (the sub-map of T)*(the non-op of T) = the sub-map of T;
  attr T is subjected means
:: ABCMIZ_0:def 25
  for a being adjective of T holds types a \/ types
non-a is_<=_than sub a & (types a <> {} & types non-a <> {} implies sub a = sup
  (types a \/ types non-a));
end;

definition
  let T be non empty non void TAS-structure;
  redefine attr T is non-absorbing means
:: ABCMIZ_0:def 26
  for a being adjective of T holds sub non-a = sub a;
end;

definition
  let T be non empty non void TAS-structure;
  let t be Element of T;
  let a be adjective of T;
  pred a is_properly_applicable_to t means
:: ABCMIZ_0:def 27

  t <= sub a & a is_applicable_to t;
end;

definition
  let T be non empty non void reflexive transitive TAS-structure;
  let t be type of T;
  let v be FinSequence of the adjectives of T;
  pred v is_properly_applicable_to t means
:: ABCMIZ_0:def 28

  for i being Nat,
a being adjective of T, s being type of T st i in dom v & a = v.i & s = apply(v
  ,t).i holds a is_properly_applicable_to s;
end;

theorem :: ABCMIZ_0:57
  for T being non empty non void reflexive transitive
TAS-structure for t being type of T, v being FinSequence of the adjectives of T
  st v is_properly_applicable_to t holds v is_applicable_to t;

theorem :: ABCMIZ_0:58
  for T being non empty non void reflexive transitive TAS-structure for
  t being type of T holds <*> the adjectives of T is_properly_applicable_to t;

theorem :: ABCMIZ_0:59
  for T being non empty non void reflexive transitive TAS-structure for
  t being type of T, a being adjective of T holds a is_properly_applicable_to t
  iff <*a*> is_properly_applicable_to t;

theorem :: ABCMIZ_0:60
  for T being non empty non void reflexive transitive
TAS-structure for t being type of T, v1,v2 being FinSequence of the adjectives
of T st v1^v2 is_properly_applicable_to t holds v1 is_properly_applicable_to t
  & v2 is_properly_applicable_to v1 ast t;

theorem :: ABCMIZ_0:61
  for T being non empty non void reflexive transitive
TAS-structure for t being type of T, v1,v2 being FinSequence of the adjectives
of T st v1 is_properly_applicable_to t & v2 is_properly_applicable_to v1 ast t
  holds v1^v2 is_properly_applicable_to t;

definition
  let T be non empty non void reflexive transitive TAS-structure;
  let t be type of T;
  let A be Subset of the adjectives of T;
  pred A is_properly_applicable_to t means
:: ABCMIZ_0:def 29

  ex s being FinSequence of
  the adjectives of T st rng s = A & s is_properly_applicable_to t;
end;

theorem :: ABCMIZ_0:62
  for T being non empty non void reflexive transitive
TAS-structure for t being type of T, A being Subset of the adjectives of T st A
  is_properly_applicable_to t holds A is finite;

theorem :: ABCMIZ_0:63
  for T being non empty non void reflexive transitive
  TAS-structure for t being type of T holds {} the adjectives of T
  is_properly_applicable_to t;

scheme :: ABCMIZ_0:sch 1
  MinimalFiniteSet{P[set]}: ex A being finite set st P[A] & for B being set st
  B c= A & P[B] holds B = A
provided
 ex A being finite set st P[A];

theorem :: ABCMIZ_0:64
  for T being non empty non void reflexive transitive
TAS-structure for t being type of T, A being Subset of the adjectives of T st A
is_properly_applicable_to t ex B being Subset of the adjectives of T st B c= A
& B is_properly_applicable_to t & A ast t = B ast t & for C being Subset of the
  adjectives of T st C c= B & C is_properly_applicable_to t & A ast t = C ast t
  holds C = B;

definition
  let T be non empty non void reflexive transitive TAS-structure;
  attr T is commutative means
:: ABCMIZ_0:def 30

  for t1,t2 being type of T, a being
  adjective of T st a is_properly_applicable_to t1 & a ast t1 <= t2 ex A being
finite Subset of the adjectives of T st A is_properly_applicable_to t1 "\/" t2
  & A ast (t1 "\/" t2) = t2;
end;

registration
  cluster Mizar-widening-like involutive without_fixpoints consistent
    adj-structured adjs-typed non-absorbing subjected commutative for complete
    upper-bounded non void 1-element reflexive transitive antisymmetric
    strict TAS-structure;
end;

theorem :: ABCMIZ_0:65
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema non void TAS-structure for t being type of T, A
being Subset of the adjectives of T st A is_properly_applicable_to t ex s being
  one-to-one FinSequence of the adjectives of T st rng s = A & s
  is_properly_applicable_to t;

begin :: Reduction of adjectives

definition
  let T be non empty non void reflexive transitive TAS-structure;
  func T @--> -> Relation of T means
:: ABCMIZ_0:def 31

  for t1,t2 being type of T holds [
  t1,t2] in it iff ex a being adjective of T st not a in adjs t2 & a
  is_properly_applicable_to t2 & a ast t2 = t1;
end;

theorem :: ABCMIZ_0:66
  for T being adj-structured antisymmetric non void reflexive
  transitive with_suprema Noetherian TAS-structure holds T@--> c= the
  InternalRel of T;

scheme :: ABCMIZ_0:sch 2
  RedInd{X() -> non empty set, P[set,set], R() -> Relation of X()}: for x,y
  being Element of X() st R() reduces x,y holds P[x,y]
provided
 for x,y being Element of X() st [x,y] in R() holds P[x,y] and
 for x being Element of X() holds P[x,x] and
 for x,y,z being Element of X() st P[x,y] & P[y,z] holds P[x,z];

theorem :: ABCMIZ_0:67
  for T being adj-structured antisymmetric non void reflexive
transitive with_suprema Noetherian TAS-structure for t1,t2 being type of T st
  T@--> reduces t1,t2 holds t1 <= t2;

theorem :: ABCMIZ_0:68
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric non void with_suprema TAS-structure holds T@--> is irreflexive;

theorem :: ABCMIZ_0:69
  for T being adj-structured antisymmetric non void reflexive
  transitive with_suprema Noetherian TAS-structure holds T@--> is
  strongly-normalizing;

theorem :: ABCMIZ_0:70
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema non void TAS-structure for t being type of T, A
  being finite Subset of the adjectives of T st for C being Subset of the
  adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t
holds C = A for s being one-to-one FinSequence of the adjectives of T st rng s
= A & s is_properly_applicable_to t for i being Nat st 1 <= i & i <=
  len s holds [apply(s, t).(i+1), apply(s, t).i] in T@-->;

theorem :: ABCMIZ_0:71
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema non void TAS-structure for t being type of T, A
  being finite Subset of the adjectives of T st for C being Subset of the
  adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t
holds C = A for s being one-to-one FinSequence of the adjectives of T st rng s
  = A & s is_properly_applicable_to t holds Rev apply(s, t) is RedSequence of T
  @-->;

theorem :: ABCMIZ_0:72
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema non void TAS-structure for t being type of T, A
  being finite Subset of the adjectives of T st A is_properly_applicable_to t
  holds T@--> reduces A ast t, t;

theorem :: ABCMIZ_0:73
  for X being non empty set for R being Relation of X for r being
  RedSequence of R st r.1 in X holds r is FinSequence of X;

theorem :: ABCMIZ_0:74
  for X being non empty set for R being Relation of X for x be
  Element of X, y being set st R reduces x,y holds y in X;

theorem :: ABCMIZ_0:75
  for X being non empty set for R being Relation of X st R is
  with_UN_property weakly-normalizing for x be Element of X holds nf(x, R) in X
;

theorem :: ABCMIZ_0:76
  for T being Noetherian adj-structured reflexive transitive
  antisymmetric with_suprema non void TAS-structure for t1, t2 being type of T
  st T@--> reduces t1, t2 ex A being finite Subset of the adjectives of T st A
  is_properly_applicable_to t2 & t1 = A ast t2;

theorem :: ABCMIZ_0:77
  for T being adj-structured antisymmetric commutative non void
  reflexive transitive with_suprema Noetherian TAS-structure holds T@--> is
  with_Church-Rosser_property with_UN_property;

begin :: Radix types

definition
  let T be adj-structured with_suprema antisymmetric commutative non empty
  non void reflexive transitive Noetherian TAS-structure;
  let t be type of T;
  func radix t -> type of T equals
:: ABCMIZ_0:def 32
  nf(t, T@-->);
end;

theorem :: ABCMIZ_0:78
  for T being adj-structured with_suprema antisymmetric
commutative non empty non void reflexive transitive Noetherian TAS-structure
  for t being type of T holds T@--> reduces t, radix t;

theorem :: ABCMIZ_0:79
  for T being adj-structured with_suprema antisymmetric commutative non
empty non void reflexive transitive Noetherian TAS-structure for t being type
  of T holds t <= radix t;

theorem :: ABCMIZ_0:80
  for T being adj-structured with_suprema antisymmetric
commutative non empty non void reflexive transitive Noetherian TAS-structure
  for t being type of T for X being set st X = {t9 where t9 is type of T: ex A
being finite Subset of the adjectives of T st A is_properly_applicable_to t9 &
  A ast t9 = t} holds ex_sup_of X, T & radix t = "\/"(X, T);

theorem :: ABCMIZ_0:81
  for T being adj-structured with_suprema antisymmetric
commutative non empty non void reflexive transitive Noetherian TAS-structure
  for t1,t2 being type of T, a being adjective of T st a
  is_properly_applicable_to t1 & a ast t1 <= radix t2 holds t1 <= radix t2;

theorem :: ABCMIZ_0:82
  for T being adj-structured with_suprema antisymmetric commutative non
  empty non void reflexive transitive Noetherian TAS-structure for t1,t2 being
  type of T st t1 <= t2 holds radix t1 <= radix t2;

theorem :: ABCMIZ_0:83
  for T being adj-structured with_suprema antisymmetric commutative non
empty non void reflexive transitive Noetherian TAS-structure for t being type
  of T, a being adjective of T st a is_properly_applicable_to t holds radix (a
  ast t) = radix t;