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


registration
cluster 1 -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 ;
attr T 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
cluster 1 -element -> 1 -element Noetherian for RelStr ;
coherence
for b1 being 1 -element RelStr holds b1 is Noetherian
proof end;
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 & ( for b being Element of T st b in A holds
not a < b ) ) )
proof end;
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 & ( for b being Element of T st b in A holds
not a < b ) ) );

definition
let T be Poset;
attr T is Mizar-widening-like means :: ABCMIZ_0:def 3
( T is sup-Semilattice & 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 & 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 & b1 is with_suprema & b1 is upper-bounded )
proof end;
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
;
end;

registration
cluster non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V145() up-complete /\-complete Mizar-widening-like for RelStr ;
existence
ex b1 being complete sup-Semilattice st b1 is Mizar-widening-like
proof end;
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 & sup I in I )
proof end;

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

definition
let A be AdjectiveStr ;
attr A 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 & A1 is void holds
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;
coherence
the non-op of A . a is adjective of A
proof end;
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 ;
attr A is involutive means :Def6: :: 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
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} & the non-op of A . a1 = a2 & the non-op of A . a2 = a1 holds
( not A is void & A is involutive & A is without_fixpoints )
proof end;

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 #) & A1 is involutive holds
A2 is involutive
proof end;

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 #) & A1 is without_fixpoints holds
A2 is without_fixpoints
proof end;

registration
cluster strict non void involutive without_fixpoints for AdjectiveStr ;
existence
ex b1 being strict AdjectiveStr st
( not b1 is void & b1 is involutive & b1 is without_fixpoints )
proof end;
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
attr c1 is strict ;
struct TA-structure -> RelStr , AdjectiveStr ;
aggr TA-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
;
end;

registration
cluster 1 -element reflexive non void involutive without_fixpoints strict for TA-structure ;
existence
ex b1 being TA-structure st
( b1 is 1 -element & b1 is reflexive & not b1 is void & b1 is involutive & b1 is without_fixpoints & b1 is strict )
proof end;
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
proof end;
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 ;
attr T 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 #) & T1 is consistent holds
T2 is consistent
proof end;

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;

:: 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 #) & T1 is adj-structured holds
T2 is adj-structured
proof end;

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) )
proof end;
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
proof end;

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 object holds
( x in it iff ex t being type of T st
( x = t & a in adjs t ) );
existence
ex b1 being Subset of T st
for x being object holds
( x in b1 iff ex t being type of T st
( x = t & a in adjs t ) )
proof end;
uniqueness
for b1, b2 being Subset of T st ( for x being object holds
( x in b1 iff ex t being type of T st
( x = t & a in adjs t ) ) ) & ( for x being object holds
( x in b2 iff ex t being type of T st
( x = t & a in adjs t ) ) ) holds
b1 = b2
proof end;
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 object holds
( x in b3 iff ex t being type of T st
( x = t & 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 )
proof end;
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 ) ) & ( 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
proof end;
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
proof end;

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 }
proof end;

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 )
proof end;

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 )
proof end;

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 }
proof end;

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

definition
let T be TA-structure ;
attr T 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 #) & T1 is adjs-typed holds
T2 is adjs-typed
proof end;

registration
cluster non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V145() 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 & b1 is Mizar-widening-like & b1 is involutive & b1 is without_fixpoints & b1 is consistent & b1 is adj-structured & b1 is adjs-typed )
proof end;
end;

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

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 & types a is directed )
proof end;
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 & types A is directed )
proof end;
end;

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;

:: deftheorem 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 & t9 <= t ) );

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;

:: deftheorem 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 & 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
proof end;

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));
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
proof end;

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)
proof end;

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
proof end;

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 & a in adjs t9 holds
( a is_applicable_to t & t9 <= a ast t )
proof end;

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 & a ast t = t )
proof end;

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 & 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) )
proof end;

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
proof end;

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));
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
proof end;

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 & it . 1 = t & ( for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p & a = p . i & 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 & b1 . 1 = t & ( for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p & a = p . i & t = b1 . i holds
b1 . (i + 1) = a ast t ) )
proof end;
correctness
uniqueness
for b1, b2 being FinSequence of the carrier of T st len b1 = (len p) + 1 & b1 . 1 = t & ( for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p & a = p . i & t = b1 . i holds
b1 . (i + 1) = a ast t ) & len b2 = (len p) + 1 & b2 . 1 = t & ( for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p & a = p . i & t = b2 . i holds
b2 . (i + 1) = a ast t ) holds
b1 = b2
;
proof end;
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 & b4 . 1 = t & ( for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p & a = p . i & 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
proof end;
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*>
proof end;

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)*>
proof end;

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;
func v 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
proof end;
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
proof end;

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
proof end;

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)
proof end;

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)))
proof end;

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
proof end;

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
proof end;

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
proof end;

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;
pred v is_applicable_to t means :: 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 & a = v . i & s = (apply (v,t)) . i holds
a is_applicable_to s;
end;

:: deftheorem 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 & a = v . i & 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 ;

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 )
proof end;

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 & v2 is_applicable_to v1 ast t )
proof end;

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 & i1 <= i2 & i2 <= (len v) + 1 holds
for t1, t2 being type of T st t1 = (apply (v,t)) . i1 & t2 = (apply (v,t)) . i2 holds
t2 <= t1
proof end;

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 & s <= t )
proof end;

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
proof end;

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)
proof end;

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
proof end;

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 & rng v2 c= rng v1 holds
for s being type of T st s in rng (apply (v2,t)) holds
v1 ast t <= s
proof end;

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
proof end;

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
proof end;

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
proof end;

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)
proof end;

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
proof end;

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 & A c= adjs t9 holds
( A is_applicable_to t & t9 <= A ast t )
proof end;

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 & A ast t = t )
proof end;

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 & B c= A holds
B is_applicable_to t
proof end;

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} & B is_applicable_to t holds
a ast (A ast t) = B ast t
proof end;

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
proof end;

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)))
proof end;
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))) ) & ( for a being adjective of T holds b2 . a = sup ((types a) \/ (types (non- a))) ) holds
b1 = b2
proof end;
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
attr c1 is strict ;
struct TAS-structure -> TA-structure ;
aggr TAS-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
cluster 1 -element reflexive non void strict for TAS-structure ;
existence
ex b1 being TAS-structure st
( not b1 is void & b1 is reflexive & b1 is 1 -element & b1 is strict )
proof end;
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 ;
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;

:: 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 & ( types a <> {} & 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 )
proof end;
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;
pred a is_properly_applicable_to t means :: ABCMIZ_0:def 27
( t <= sub a & a is_applicable_to t );
end;

:: deftheorem 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 & 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;
pred v is_properly_applicable_to t means :: 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 & a = v . i & s = (apply (v,t)) . i holds
a is_properly_applicable_to s;
end;

:: deftheorem 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 & a = v . i & 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
proof end;

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 ;

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 )
proof end;

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 & v2 is_properly_applicable_to v1 ast t )
proof end;

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 & v2 is_properly_applicable_to v1 ast t holds
v1 ^ v2 is_properly_applicable_to t
proof end;

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

:: deftheorem 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 & s is_properly_applicable_to t ) );

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

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
proof end;

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

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 & 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 ) )
proof end;

definition
let T be non empty reflexive transitive non void TAS-structure ;
attr T 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 & a ast t1 <= t2 holds
ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t1 "\/" t2 & 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 & a ast t1 <= t2 holds
ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t1 "\/" t2 & 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 V145() 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 & b1 is involutive & b1 is without_fixpoints & b1 is consistent & b1 is adj-structured & b1 is adjs-typed & b1 is non-absorbing & b1 is subjected & b1 is commutative )
proof end;
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 & s is_properly_applicable_to t )
proof end;

definition
let T be non empty reflexive transitive non void TAS-structure ;
func T @--> -> 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 & a is_properly_applicable_to t2 & 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 & a is_properly_applicable_to t2 & a ast t2 = t1 ) )
proof end;
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 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) ) & ( 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 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) ) holds
b1 = b2
proof end;
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 & a is_properly_applicable_to t2 & 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
proof end;

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] & P1[y,z] holds
P1[x,z]
proof end;

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
proof end;

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

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
proof end;

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 & C is_properly_applicable_to t & 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 & s is_properly_applicable_to t holds
for i being Nat st 1 <= i & i <= len s holds
[((apply (s,t)) . (i + 1)),((apply (s,t)) . i)] in T @-->
proof end;

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 & C is_properly_applicable_to t & 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 & s is_properly_applicable_to t holds
Rev (apply (s,t)) is RedSequence of T @-->
proof end;

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
proof end;

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
proof end;

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
proof end;

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

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 & t1 = A ast t2 )
proof end;

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 & T @--> is with_UN_property )
proof end;

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
proof end;
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
proof end;

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 & A ast t9 = t )
}
holds
( ex_sup_of X,T & radix t = "\/" (X,T) )
proof end;

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 & a ast t1 <= radix t2 holds
t1 <= radix t2
proof end;

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
proof end;

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
proof end;