:: On semilattice structure of {M}izar types
:: by Grzegorz Bancerek
::
:: Received August 8, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


begin

registration
cluster1 -element reflexive  -> 1 -element complete for RelStr ;
coherence
 for b1 being 1 -element RelStr st b1 is reflexive holds
b1 is complete ;
end;

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

definition
let T be RelStr ;
attrT is Noetherian  means :Def1: :: ABCMIZ_0:def 1
 the InternalRel of T is co-well_founded ;
end;

:: deftheorem Def1 defines Noetherian ABCMIZ_0:def_1_:_
 for T being RelStr holds
( T is Noetherian iff the InternalRel of T is co-well_founded );

registration
cluster1 -element  -> 1 -element Noetherian for RelStr ;
coherence
 for b1 being 1 -element RelStr holds b1 is Noetherian
proofend;
end;

definition
let T be non empty RelStr ;
redefine attr T is Noetherian  means :Def2: :: 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 ) );
compatibility
 ( T is Noetherian iff for A being non empty Subset of T ex a being Element of T st
( a in A &amp; ( for b being Element of T st b in A holds
not a < b ) ) )
proofend;
end;

:: deftheorem Def2 defines Noetherian ABCMIZ_0:def_2_:_
 for T being non empty RelStr holds
( T is Noetherian iff for A being non empty Subset of T ex a being Element of T st
( a in A &amp; ( for b being Element of T st b in A holds
not a < b ) ) );

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

:: deftheorem  defines Mizar-widening-like ABCMIZ_0:def_3_:_
 for T being Poset holds
( T is Mizar-widening-like iff ( T is sup-Semilattice &amp; T is Noetherian ) );

registration
cluster reflexive transitive antisymmetric Mizar-widening-like  ->  with_suprema upper-bounded Noetherian for RelStr ;
coherence
 for b1 being Poset st b1 is Mizar-widening-like holds
( b1 is Noetherian &amp; b1 is with_suprema &amp; b1 is upper-bounded )
proofend;
end;

registration
cluster reflexive transitive antisymmetric with_suprema Noetherian  ->  Mizar-widening-like for RelStr ;
coherence
 for b1 being sup-Semilattice st b1 is Noetherian holds
b1 is Mizar-widening-like
proofend;
end;

registration
cluster non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() up-complete /\-complete Mizar-widening-like for RelStr ;
existence
 ex b1 being complete sup-Semilattice st b1 is Mizar-widening-like
proofend;
end;

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

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

begin

definition
attrc1 is strict ;
struct AdjectiveStr  -> ;
aggrAdjectiveStr(# adjectives, non-op #) ->  AdjectiveStr ;
sel adjectives c1 ->  set ;
sel non-op c1 ->  UnOp of the adjectives of c1;
end;

definition
let A be AdjectiveStr ;
attrA is void  means :Def4: :: ABCMIZ_0:def 4
 the adjectives of A is empty ;
mode adjective of A is Element of the adjectives of A;
end;

:: deftheorem Def4 defines void ABCMIZ_0:def_4_:_
 for A being AdjectiveStr holds
( A is void iff the adjectives of A is empty );

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

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;
coherence
 the non-op of A . a is adjective of A
proofend;
end;

:: deftheorem  defines non- ABCMIZ_0:def_5_:_
 for A being AdjectiveStr
for a being Element of the adjectives of A holds non- a = the non-op of A . a;

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

definition
let A be AdjectiveStr ;
attrA is involutive  means :Def6: :: ABCMIZ_0:def 6
 for a being adjective of A holds non- (non- a) = a;
attrA is without_fixpoints  means :: ABCMIZ_0:def 7
 for a being adjective of A holds not non- a = a;
end;

:: deftheorem Def6 defines involutive ABCMIZ_0:def_6_:_
 for A being AdjectiveStr holds
( A is involutive iff for a being adjective of A holds non- (non- a) = a );

:: deftheorem  defines without_fixpoints ABCMIZ_0:def_7_:_
 for A being AdjectiveStr holds
( A is without_fixpoints iff for a being adjective of A holds not non- a = a );

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

theorem Th5: :: ABCMIZ_0:5
for A1, A2 being AdjectiveStr st AdjectiveStr(# the adjectives of A1, the non-op of A1 #) = AdjectiveStr(# the adjectives of A2, the non-op of A2 #) &amp; A1 is involutive holds
A2 is involutive
proofend;

theorem Th6: :: ABCMIZ_0:6
for A1, A2 being AdjectiveStr st AdjectiveStr(# the adjectives of A1, the non-op of A1 #) = AdjectiveStr(# the adjectives of A2, the non-op of A2 #) &amp; A1 is without_fixpoints holds
A2 is without_fixpoints
proofend;

registration
cluster strict non void involutive without_fixpoints for AdjectiveStr ;
existence
 ex b1 being strict AdjectiveStr st
( not b1 is void &amp; b1 is involutive &amp; b1 is without_fixpoints )
proofend;
end;

registration
let A be non void AdjectiveStr ;
cluster the adjectives of A ->  non empty ;
coherence
 not the adjectives of A is empty by Def4;
end;

definition
attrc1 is strict ;
struct TA-structure  ->  RelStr , AdjectiveStr ;
aggrTA-structure(# carrier, adjectives, InternalRel, non-op, adj-map #) ->  TA-structure ;
sel adj-map c1 ->  Function of the carrier of c1,(Fin the adjectives of c1);
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 ;
coherence
 not TA-structure(# X,A,r,n,a #) is 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 ;
coherence
 not TA-structure(# X,A,r,n,a #) is void by Def4;
end;

registration
cluster1 -element reflexive non void involutive without_fixpoints strict for TA-structure ;
existence
 ex b1 being TA-structure st
( b1 is 1 -element &amp; b1 is reflexive &amp; not b1 is void &amp; b1 is involutive &amp; b1 is without_fixpoints &amp; b1 is strict )
proofend;
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;
coherence
 the adj-map of T . t is Subset of the adjectives of T
proofend;
end;

:: deftheorem  defines adjs ABCMIZ_0:def_8_:_
 for T being TA-structure
for t being Element of T holds adjs t = the adj-map of T . t;

theorem :: ABCMIZ_0:7
for T1, T2 being TA-structure st TA-structure(# the carrier of T1, the adjectives of T1, the InternalRel of T1, the non-op of T1, the adj-map of T1 #) = TA-structure(# the carrier of T2, the adjectives of T2, the InternalRel of T2, the non-op of T2, the adj-map of T2 #) holds
for t1 being type of T1
for t2 being type of T2 st t1 = t2 holds
adjs t1 = adjs t2 ;

definition
let T be TA-structure ;
attrT is consistent  means :Def9: :: 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;

:: deftheorem Def9 defines consistent ABCMIZ_0:def_9_:_
 for T being TA-structure holds
( T is consistent iff for t being type of T
for a being adjective of T st a in adjs t holds
not non- a in adjs t );

theorem Th8: :: ABCMIZ_0:8
for T1, T2 being TA-structure st TA-structure(# the carrier of T1, the adjectives of T1, the InternalRel of T1, the non-op of T1, the adj-map of T1 #) = TA-structure(# the carrier of T2, the adjectives of T2, the InternalRel of T2, the non-op of T2, the adj-map of T2 #) &amp; T1 is consistent holds
T2 is consistent
proofend;

definition
let T be non empty TA-structure ;
attrT 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;

:: deftheorem  defines adj-structured ABCMIZ_0:def_10_:_
 for T being non empty TA-structure holds
( T is adj-structured iff the adj-map of T is join-preserving Function of T,((BoolePoset the adjectives of T) opp) );

theorem Th9: :: ABCMIZ_0:9
for T1, T2 being non empty TA-structure st TA-structure(# the carrier of T1, the adjectives of T1, the InternalRel of T1, the non-op of T1, the adj-map of T1 #) = TA-structure(# the carrier of T2, the adjectives of T2, the InternalRel of T2, the non-op of T2, the adj-map of T2 #) &amp; T1 is adj-structured holds
T2 is adj-structured
proofend;

definition
let T be reflexive transitive antisymmetric with_suprema TA-structure ;
redefine attr T is adj-structured  means :Def11: :: ABCMIZ_0:def 11
 for t1, t2 being type of T holds adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2);
compatibility
 ( T is adj-structured iff for t1, t2 being type of T holds adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2) )
proofend;
end;

:: deftheorem Def11 defines adj-structured ABCMIZ_0:def_11_:_
 for T being reflexive transitive antisymmetric with_suprema TA-structure holds
( T is adj-structured iff for t1, t2 being type of T holds adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2) );

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

definition
let T be TA-structure ;
let a be Element of the adjectives of T;
func types a ->  Subset of T means :Def12: :: ABCMIZ_0:def 12
 for x being set holds
( x in it iff ex t being type of T st
( x = t &amp; a in adjs t ) );
existence
 ex b1 being Subset of T st
for x being set holds
( x in b1 iff ex t being type of T st
( x = t &amp; a in adjs t ) )
proofend;
uniqueness
 for b1, b2 being Subset of T st ( for x being set holds
( x in b1 iff ex t being type of T st
( x = t &amp; a in adjs t ) ) ) &amp; ( for x being set holds
( x in b2 iff ex t being type of T st
( x = t &amp; a in adjs t ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines types ABCMIZ_0:def_12_:_
 for T being TA-structure
for a being Element of the adjectives of T
for b3 being Subset of T holds
( b3 = types a iff for x being set holds
( x in b3 iff ex t being type of T st
( x = t &amp; a in adjs t ) ) );

definition
let T be non empty TA-structure ;
let A be Subset of the adjectives of T;
func types A ->  Subset of T means :Def13: :: 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 );
existence
 ex b1 being Subset of T st
for t being type of T holds
( t in b1 iff for a being adjective of T st a in A holds
t in types a )
proofend;
uniqueness
 for b1, b2 being Subset of T st ( for t being type of T holds
( t in b1 iff for a being adjective of T st a in A holds
t in types a ) ) &amp; ( for t being type of T holds
( t in b2 iff for a being adjective of T st a in A holds
t in types a ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def13 defines types ABCMIZ_0:def_13_:_
 for T being non empty TA-structure
for A being Subset of the adjectives of T
for b3 being Subset of T holds
( b3 = types A iff for t being type of T holds
( t in b3 iff for a being adjective of T st a in A holds
t in types a ) );

theorem Th11: :: ABCMIZ_0:11
for T1, T2 being TA-structure st TA-structure(# the carrier of T1, the adjectives of T1, the InternalRel of T1, the non-op of T1, the adj-map of T1 #) = TA-structure(# the carrier of T2, the adjectives of T2, the InternalRel of T2, the non-op of T2, the adj-map of T2 #) holds
for a1 being adjective of T1
for a2 being adjective of T2 st a1 = a2 holds
types a1 = types a2
proofend;

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  }
proofend;

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

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

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  }
proofend;

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

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

:: deftheorem  defines adjs-typed ABCMIZ_0:def_14_:_
 for T being TA-structure holds
( T is adjs-typed iff for a being adjective of T holds not (types a) \/ (types (non- a)) is empty );

theorem Th17: :: ABCMIZ_0:17
for T1, T2 being TA-structure st TA-structure(# the carrier of T1, the adjectives of T1, the InternalRel of T1, the non-op of T1, the adj-map of T1 #) = TA-structure(# the carrier of T2, the adjectives of T2, the InternalRel of T2, the non-op of T2, the adj-map of T2 #) &amp; T1 is adjs-typed holds
T2 is adjs-typed
proofend;

registration
cluster non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete Noetherian Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed for TA-structure ;
existence
 ex b1 being 1 -element reflexive transitive antisymmetric complete upper-bounded strict TA-structure st
( not b1 is void &amp; b1 is Mizar-widening-like &amp; b1 is involutive &amp; b1 is without_fixpoints &amp; b1 is consistent &amp; b1 is adj-structured &amp; b1 is adjs-typed )
proofend;
end;

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

registration
let T be reflexive transitive antisymmetric with_suprema adj-structured TA-structure ;
let a be adjective of T;
cluster types a ->  directed lower ;
coherence
 ( types a is lower &amp; types a is directed )
proofend;
end;

registration
let T be reflexive transitive antisymmetric with_suprema adj-structured TA-structure ;
let A be Subset of the adjectives of T;
cluster types A ->  directed lower ;
coherence
 ( types A is lower &amp; types A is directed )
proofend;
end;

begin

definition
let T be TA-structure ;
let t be Element of T;
let a be adjective of T;
preda is_applicable_to t means :Def15: :: ABCMIZ_0:def 15
 ex t9 being type of T st
( t9 in types a &amp; t9 <= t );
end;

:: deftheorem Def15 defines is_applicable_to ABCMIZ_0:def_15_:_
 for T being TA-structure
for t being Element of T
for a being adjective of T holds
( a is_applicable_to t iff ex t9 being type of T st
( t9 in types a &amp; t9 <= t ) );

definition
let T be TA-structure ;
let t be type of T;
let A be Subset of the adjectives of T;
predA is_applicable_to t means :Def16: :: ABCMIZ_0:def 16
 ex t9 being type of T st
( A c= adjs t9 &amp; t9 <= t );
end;

:: deftheorem Def16 defines is_applicable_to ABCMIZ_0:def_16_:_
 for T being TA-structure
for t being type of T
for A being Subset of the adjectives of T holds
( A is_applicable_to t iff ex t9 being type of T st
( A c= adjs t9 &amp; t9 <= t ) );

theorem Th19: :: ABCMIZ_0:19
for T being reflexive transitive antisymmetric with_suprema adj-structured 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
proofend;

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

:: deftheorem  defines ast ABCMIZ_0:def_17_:_
 for T being non empty reflexive transitive TA-structure
for t being Element of T
for a being adjective of T holds a ast t = sup ((types a) /\ (downarrow t));

theorem Th20: :: ABCMIZ_0:20
for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured 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
proofend;

theorem Th21: :: ABCMIZ_0:21
for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured 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)
proofend;

theorem Th22: :: ABCMIZ_0:22
for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured 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
proofend;

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

theorem Th24: :: ABCMIZ_0:24
for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured 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 &amp; a ast t = t )
proofend;

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

theorem Th26: :: ABCMIZ_0:26
for T being reflexive transitive antisymmetric with_suprema adj-structured 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
proofend;

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;
funcA ast t ->  type of T equals :: ABCMIZ_0:def 18
 sup ((types A) /\ (downarrow t));
coherence
 sup ((types A) /\ (downarrow t)) is type of T ;
end;

:: deftheorem  defines ast ABCMIZ_0:def_18_:_
 for T being non empty reflexive transitive TA-structure
for t being type of T
for A being Subset of the adjectives of T holds A ast t = sup ((types A) /\ (downarrow t));

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

definition
let T be non empty reflexive transitive non void 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 :Def19: :: ABCMIZ_0:def 19
( len it = (len p) + 1 &amp; it . 1 = t &amp; ( for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p &amp; a = p . i &amp; t = it . i holds
it . (i + 1) = a ast t ) );
existence
 ex b1 being FinSequence of the carrier of T st
( len b1 = (len p) + 1 &amp; b1 . 1 = t &amp; ( for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p &amp; a = p . i &amp; t = b1 . i holds
b1 . (i + 1) = a ast t ) )
proofend;
correctness
uniqueness
for b1, b2 being FinSequence of the carrier of T st len b1 = (len p) + 1 &amp; b1 . 1 = t &amp; ( for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p &amp; a = p . i &amp; t = b1 . i holds
b1 . (i + 1) = a ast t ) &amp; len b2 = (len p) + 1 &amp; b2 . 1 = t &amp; ( for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p &amp; a = p . i &amp; t = b2 . i holds
b2 . (i + 1) = a ast t ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def19 defines apply ABCMIZ_0:def_19_:_
 for T being non empty reflexive transitive non void TA-structure
for t being type of T
for p being FinSequence of the adjectives of T
for b4 being FinSequence of the carrier of T holds
( b4 = apply (p,t) iff ( len b4 = (len p) + 1 &amp; b4 . 1 = t &amp; ( for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p &amp; a = p . i &amp; t = b4 . i holds
b4 . (i + 1) = a ast t ) ) );

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

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

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

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

:: deftheorem  defines ast ABCMIZ_0:def_20_:_
 for T being non empty reflexive transitive non void TA-structure
for t being type of T
for v being FinSequence of the adjectives of T holds v ast t = (apply (v,t)) . ((len v) + 1);

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

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

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

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

theorem Th34: :: ABCMIZ_0:34
for T being non empty reflexive transitive non void 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)))
proofend;

theorem Th35: :: ABCMIZ_0:35
for T being non empty reflexive transitive non void 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
proofend;

theorem Th36: :: ABCMIZ_0:36
for T being non empty reflexive transitive non void 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
proofend;

theorem Th37: :: ABCMIZ_0:37
for T being non empty reflexive transitive non void 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
proofend;

definition
let T be non empty reflexive transitive non void TA-structure ;
let t be type of T;
let v be FinSequence of the adjectives of T;
predv is_applicable_to t means :Def21: :: ABCMIZ_0:def 21
 for i being Nat
for a being adjective of T
for s being type of T st i in dom v &amp; a = v . i &amp; s = (apply (v,t)) . i holds
a is_applicable_to s;
end;

:: deftheorem Def21 defines is_applicable_to ABCMIZ_0:def_21_:_
 for T being non empty reflexive transitive non void TA-structure
for t being type of T
for v being FinSequence of the adjectives of T holds
( v is_applicable_to t iff for i being Nat
for a being adjective of T
for s being type of T st i in dom v &amp; a = v . i &amp; s = (apply (v,t)) . i holds
a is_applicable_to s );

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

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

theorem Th40: :: ABCMIZ_0:40
for T being non empty reflexive transitive 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 is_applicable_to t &amp; v2 is_applicable_to v1 ast t )
proofend;

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

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

theorem Th43: :: ABCMIZ_0:43
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured 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
proofend;

theorem Th44: :: ABCMIZ_0:44
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured 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)
proofend;

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

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

theorem Th47: :: ABCMIZ_0:47
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured 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
proofend;

theorem :: ABCMIZ_0:48
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured 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
proofend;

theorem Th49: :: ABCMIZ_0:49
for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured 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
proofend;

theorem Th50: :: ABCMIZ_0:50
for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured 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)
proofend;

theorem :: ABCMIZ_0:51
for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured 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
proofend;

theorem Th52: :: ABCMIZ_0:52
for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured 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 &amp; A c= adjs t9 holds
( A is_applicable_to t &amp; t9 <= A ast t )
proofend;

theorem :: ABCMIZ_0:53
for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured 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 &amp; A ast t = t )
proofend;

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

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

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

begin

definition
let T be non empty non void TA-structure ;
func sub T ->  Function of the adjectives of T, the carrier of T means :Def22: :: ABCMIZ_0:def 22
 for a being adjective of T holds it . a = sup ((types a) \/ (types (non- a)));
existence
 ex b1 being Function of the adjectives of T, the carrier of T st
for a being adjective of T holds b1 . a = sup ((types a) \/ (types (non- a)))
proofend;
uniqueness
 for b1, b2 being Function of the adjectives of T, the carrier of T st ( for a being adjective of T holds b1 . a = sup ((types a) \/ (types (non- a))) ) &amp; ( for a being adjective of T holds b2 . a = sup ((types a) \/ (types (non- a))) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def22 defines sub ABCMIZ_0:def_22_:_
 for T being non empty non void TA-structure
for b2 being Function of the adjectives of T, the carrier of T holds
( b2 = sub T iff for a being adjective of T holds b2 . a = sup ((types a) \/ (types (non- a))) );

definition
attrc1 is strict ;
struct TAS-structure  ->  TA-structure ;
aggrTAS-structure(# carrier, adjectives, InternalRel, non-op, adj-map, sub-map #) ->  TAS-structure ;
sel sub-map c1 ->  Function of the adjectives of c1, the carrier of c1;
end;

registration
cluster1 -element reflexive non void strict for TAS-structure ;
existence
 ex b1 being TAS-structure st
( not b1 is void &amp; b1 is reflexive &amp; b1 is 1 -element &amp; b1 is strict )
proofend;
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;
coherence
 the sub-map of T . a is type of T ;
end;

:: deftheorem  defines sub ABCMIZ_0:def_23_:_
 for T being non empty non void TAS-structure
for a being adjective of T holds sub a = the sub-map of T . a;

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

:: deftheorem  defines non-absorbing ABCMIZ_0:def_24_:_
 for T being non empty non void TAS-structure holds
( T is non-absorbing iff the sub-map of T * the non-op of T = the sub-map of T );

:: deftheorem  defines subjected ABCMIZ_0:def_25_:_
 for T being non empty non void TAS-structure holds
( T is subjected iff for a being adjective of T holds
( (types a) \/ (types (non- a)) is_<=_than sub a &amp; ( types a <> {} &amp; types (non- a) <> {} implies sub a = sup ((types a) \/ (types (non- a))) ) ) );

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;
compatibility
 ( T is non-absorbing iff for a being adjective of T holds sub (non- a) = sub a )
proofend;
end;

:: deftheorem  defines non-absorbing ABCMIZ_0:def_26_:_
 for T being non empty non void TAS-structure holds
( T is non-absorbing iff for a being adjective of T holds sub (non- a) = sub a );

definition
let T be non empty non void TAS-structure ;
let t be Element of T;
let a be adjective of T;
preda is_properly_applicable_to t means :Def27: :: ABCMIZ_0:def 27
( t <= sub a &amp; a is_applicable_to t );
end;

:: deftheorem Def27 defines is_properly_applicable_to ABCMIZ_0:def_27_:_
 for T being non empty non void TAS-structure
for t being Element of T
for a being adjective of T holds
( a is_properly_applicable_to t iff ( t <= sub a &amp; a is_applicable_to t ) );

definition
let T be non empty reflexive transitive non void TAS-structure ;
let t be type of T;
let v be FinSequence of the adjectives of T;
predv is_properly_applicable_to t means :Def28: :: ABCMIZ_0:def 28
 for i being Nat
for a being adjective of T
for s being type of T st i in dom v &amp; a = v . i &amp; s = (apply (v,t)) . i holds
a is_properly_applicable_to s;
end;

:: deftheorem Def28 defines is_properly_applicable_to ABCMIZ_0:def_28_:_
 for T being non empty reflexive transitive non void TAS-structure
for t being type of T
for v being FinSequence of the adjectives of T holds
( v is_properly_applicable_to t iff for i being Nat
for a being adjective of T
for s being type of T st i in dom v &amp; a = v . i &amp; s = (apply (v,t)) . i holds
a is_properly_applicable_to s );

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

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

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

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

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

definition
let T be non empty reflexive transitive non void TAS-structure ;
let t be type of T;
let A be Subset of the adjectives of T;
predA is_properly_applicable_to t means :Def29: :: ABCMIZ_0:def 29
 ex s being FinSequence of the adjectives of T st
( rng s = A &amp; s is_properly_applicable_to t );
end;

:: deftheorem Def29 defines is_properly_applicable_to ABCMIZ_0:def_29_:_
 for T being non empty reflexive transitive non void TAS-structure
for t being type of T
for A being Subset of the adjectives of T holds
( A is_properly_applicable_to t iff ex s being FinSequence of the adjectives of T st
( rng s = A &amp; s is_properly_applicable_to t ) );

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

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

scheme :: ABCMIZ_0:sch 1
MinimalFiniteSet{ P1[ set ] } :
 ex A being finite set st
( P1[A] &amp; ( for B being set st B c= A &amp; P1[B] holds
B = A ) )
provided
A1: ex A being finite set st P1[A]
proofend;

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

definition
let T be non empty reflexive transitive non void TAS-structure ;
attrT is commutative  means :Def30: :: ABCMIZ_0:def 30
 for t1, t2 being type of T
for a being adjective of T st a is_properly_applicable_to t1 &amp; a ast t1 <= t2 holds
ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t1 "\/" t2 &amp; A ast (t1 "\/" t2) = t2 );
end;

:: deftheorem Def30 defines commutative ABCMIZ_0:def_30_:_
 for T being non empty reflexive transitive non void TAS-structure holds
( T is commutative iff for t1, t2 being type of T
for a being adjective of T st a is_properly_applicable_to t1 &amp; a ast t1 <= t2 holds
ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t1 "\/" t2 &amp; A ast (t1 "\/" t2) = t2 ) );

registration
cluster non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete Noetherian Mizar-widening-like non void involutive without_fixpoints consistent adj-structured adjs-typed strict non-absorbing subjected commutative for TAS-structure ;
existence
 ex b1 being 1 -element reflexive transitive antisymmetric complete upper-bounded non void strict TAS-structure st
( b1 is Mizar-widening-like &amp; b1 is involutive &amp; b1 is without_fixpoints &amp; b1 is consistent &amp; b1 is adj-structured &amp; b1 is adjs-typed &amp; b1 is non-absorbing &amp; b1 is subjected &amp; b1 is commutative )
proofend;
end;

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

begin

definition
let T be non empty reflexive transitive non void TAS-structure ;
funcT @-->  ->  Relation of T means :Def31: :: 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 &amp; a is_properly_applicable_to t2 &amp; a ast t2 = t1 ) );
existence
 ex b1 being Relation of T st
for t1, t2 being type of T holds
( [t1,t2] in b1 iff ex a being adjective of T st
( not a in adjs t2 &amp; a is_properly_applicable_to t2 &amp; a ast t2 = t1 ) )
proofend;
uniqueness
 for b1, b2 being Relation of T st ( for t1, t2 being type of T holds
( [t1,t2] in b1 iff ex a being adjective of T st
( not a in adjs t2 &amp; a is_properly_applicable_to t2 &amp; a ast t2 = t1 ) ) ) &amp; ( for t1, t2 being type of T holds
( [t1,t2] in b2 iff ex a being adjective of T st
( not a in adjs t2 &amp; a is_properly_applicable_to t2 &amp; a ast t2 = t1 ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def31 defines @--> ABCMIZ_0:def_31_:_
 for T being non empty reflexive transitive non void TAS-structure
for b2 being Relation of T holds
( b2 = T @--> iff for t1, t2 being type of T holds
( [t1,t2] in b2 iff ex a being adjective of T st
( not a in adjs t2 &amp; a is_properly_applicable_to t2 &amp; a ast t2 = t1 ) ) );

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

scheme :: ABCMIZ_0:sch 2
RedInd{ F1() ->  non empty set , P1[ set , set ], F2() ->  Relation of F1() } :
 for x, y being Element of F1() st F2() reduces x,y holds
P1[x,y]
provided
A1: for x, y being Element of F1() st [x,y] in F2() holds
P1[x,y] and
A2: for x being Element of F1() holds P1[x,x] and
A3: for x, y, z being Element of F1() st P1[x,y] &amp; P1[y,z] holds
P1[x,z]
proofend;

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

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

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

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

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

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

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

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

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

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

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

begin

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

:: deftheorem  defines radix ABCMIZ_0:def_32_:_
 for T being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure
for t being type of T holds radix t = nf (t,(T @-->));

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

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

theorem Th80: :: ABCMIZ_0:80
for T being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative 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 &amp; A ast t9 = t )  }  holds
( ex_sup_of X,T &amp; radix t = "\/" (X,T) )
proofend;

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

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

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