The abstract of the Mizar article:

On Semilattice Structure of Mizar Types

by

Grzegorz Bancerek

Received August 8, 2003

MML identifier: ABCMIZ_0

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSET_1, RELAT_1, ORDERS_1, IDEAL_1, REWRITE1, LATTICES, WAYBEL_0,
      FILTER_2, BOOLE, QUANTAL1, ORDINAL2, REALSET1, FUNCT_1, LATTICE3,
      BINOP_1, OPOSET_1, AMI_1, FINSUB_1, PRELAMB, PRE_TOPC, YELLOW_1,
      OPPCAT_1, BHSP_3, RELAT_2, FUNCOP_1, WELLORD2, MIDSP_3, YELLOW_0,
      FINSEQ_1, FUNCT_7, ARYTM, CARD_1, FINSEQ_5, ABCMIZ_0, ARYTM_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, RELAT_2, SUBSET_1, RELSET_1,
      ORDINAL1, FINSUB_1, CARD_1, FUNCT_1, FUNCT_2, BINOP_1, FINSET_1,
      FINSEQ_1, FUNCT_4, ALG_1, BORSUK_1, FINSEQ_5, ORDINAL2, XCMPLX_0,
      XREAL_0, NAT_1, STRUCT_0, PRE_TOPC, REALSET1, ORDERS_1, LATTICE3,
      REWRITE1, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_7;
 constructors FINSUB_1, BORSUK_1, ALG_1, FINSEQ_5, REALSET1, LATTICE3,
      REWRITE1, YELLOW_2, INT_1, NAT_1, DOMAIN_1;
 clusters XREAL_0, REWRITE1, SUBSET_1, FINSUB_1, FINSET_1, NAT_1, BINARITH,
      RELAT_1, STRUCT_0, RELSET_1, FINSEQ_5, LATTICE3, YELLOW_0, WAYBEL_0,
      YELLOW_1, YELLOW_7, YELLOW_9, FINSEQ_1;
 requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;


begin :: Semilattice of type widening

definition
 cluster trivial reflexive -> complete (non empty 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;

definition
 cluster trivial -> Noetherian (non empty 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;

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

definition
 cluster Noetherian -> Mizar-widening-like sup-Semilattice;
end;

definition
 cluster Mizar-widening-like (complete sup-Semilattice);
end;

definition
  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;

definition
 cluster non void involutive without_fixpoints (strict AdjectiveStr);
end;

definition
 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;

definition
 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;

definition
 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;

definition
 cluster trivial reflexive non empty non void involutive without_fixpoints
         strict 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 map 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 set 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
 for t being type of T
  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;

definition
 cluster non void Mizar-widening-like involutive without_fixpoints
   consistent adj-structured adjs-typed
   (complete upper-bounded non empty trivial
    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;

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

definition
 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;

theorem :: ABCMIZ_0:19
 for T being adj-structured (with_suprema reflexive antisymmetric transitive
             TA-structure)
 for a being adjective of T holds
   types a is empty or types a is Ideal of T;


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 t' being type of T st t' in types a & t' <= 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 t' being type of T st A c= adjs t' & t' <= t;
end;

theorem :: ABCMIZ_0:20
 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: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 ast t <= 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 in adjs(a ast t);

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
  st a is_applicable_to t
  holds a ast t in types a;

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
 for t' being type of T st t' <= t & a in adjs t'
  holds a is_applicable_to t & t' <= a ast 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 being adjective of T
  st a in adjs t
  holds a is_applicable_to t & a ast t = t;

theorem :: ABCMIZ_0:26
 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:27
 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:28
  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 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;

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;
  cluster apply(p,t) -> non empty;
end;

theorem :: ABCMIZ_0:29
 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:30
 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:31
 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:32
  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:33
  for p,q being FinSequence
  for i being natural number st i >= 1 & i < len p holds (p$^q).i = p.i;

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

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
   holds apply(v1^v2, t) = apply(v1, t) $^ apply(v2, v1 ast t);

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
  for i being natural number st i in dom v1
   holds apply(v1^v2, t).i = apply(v1, t).i;

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 apply(v1^v2, t).(len v1+1) = v1 ast t;

theorem :: ABCMIZ_0:38
 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 natural number, 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:39
 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:40
 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:41
 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: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 i1,i2 being natural number 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: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
 for s being type of T st s in rng apply(v, t)
  holds v ast t <= s & s <= 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 v ast t <= 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
  holds rng v c= adjs (v ast 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 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: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 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: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 v2^v1 is_applicable_to t;

theorem :: ABCMIZ_0:49
 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: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 ast t <= 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 c= adjs(A ast t);

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
  st A is_applicable_to t
  holds A ast t in types A;

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
 for t' being type of T st t' <= t & A c= adjs t'
  holds A is_applicable_to t & t' <= A ast t;

theorem :: ABCMIZ_0:54
 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:55
  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:56
 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:57
 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;

definition
 cluster non void reflexive trivial non empty strict 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 natural number, 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:58
 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:59
 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:60
 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: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^v2 is_properly_applicable_to t
  holds v1 is_properly_applicable_to t & v2 is_properly_applicable_to v1 ast t;

theorem :: ABCMIZ_0:62
 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:63
 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:64
 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 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:65
 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;

definition
 cluster Mizar-widening-like involutive without_fixpoints
   consistent adj-structured adjs-typed non-absorbing subjected commutative
  (complete upper-bounded non empty non void trivial reflexive
  transitive antisymmetric strict TAS-structure);
end;

theorem :: ABCMIZ_0:66
 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:67
 for T being adj-structured antisymmetric
     (non void reflexive transitive with_suprema Noetherian TAS-structure)
  holds T@--> c= the InternalRel of T;

scheme 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:68
 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:69
 for T being Noetherian adj-structured (reflexive transitive antisymmetric
             non void with_suprema TAS-structure)
  holds T@--> is irreflexive;

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

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
 for i being natural number st 1 <= i & i <= len s
  holds [apply(s, t).(i+1), apply(s, t).i] in 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 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:73
 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:74
  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:75
  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:76
  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:77
 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:78
 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: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@--> reduces 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
  holds t <= radix t;

theorem :: ABCMIZ_0:81
 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 = {t' where t' is type of T:
             ex A being finite Subset of the adjectives of T st
               A is_properly_applicable_to t' & A ast t' = t}
  holds ex_sup_of X, T & radix t = "\/"(X, T);

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, a being adjective of T
  st a is_properly_applicable_to t1 & a ast t1 <= radix t2
  holds 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 t1,t2 being type of T
  st t1 <= t2
  holds radix t1 <= radix t2;

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