:: 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 b₁ being 1 -element RelStr st b₁ is reflexive holds
b₁ 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 b₁ being 1 -element RelStr holds b₁ 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 b₁ being Poset st b₁ is Mizar-widening-like holds
( b₁ is Noetherian & b₁ is with_suprema & b₁ is upper-bounded )

proof end;

end;

registration

cluster reflexive transitive antisymmetric with_suprema Noetherian -> Mizar-widening-like for RelStr ;

coherence
for b₁ being sup-Semilattice st b₁ is Noetherian holds
b₁ 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 b₁ being complete sup-Semilattice st b₁ 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 c₁ is strict ;
struct AdjectiveStr -> ;
aggr AdjectiveStr(# adjectives, non-op #) -> AdjectiveStr ;
sel adjectives c₁ -> set ;
sel non-op c₁ -> UnOp of the adjectives of c₁;

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 b₁ being strict AdjectiveStr st
( not b₁ is void & b₁ is involutive & b₁ 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 c₁ is strict ;
struct TA-structure -> RelStr , AdjectiveStr ;
aggr TA-structure(# carrier, adjectives, InternalRel, non-op, adj-map #) -> TA-structure ;
sel adj-map c₁ -> Function of the carrier of c₁,(Fin the adjectives of c₁);

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 b₁ being TA-structure st
( b₁ is 1 -element & b₁ is reflexive & not b₁ is void & b₁ is involutive & b₁ is without_fixpoints & b₁ 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 b₁ being Subset of T st
for x being object holds
( x in b₁ iff ex t being type of T st
( x = t & a in adjs t ) )

proof end;

uniqueness
for b₁, b₂ being Subset of T st ( for x being object holds
( x in b₁ iff ex t being type of T st
( x = t & a in adjs t ) ) ) & ( for x being object holds
( x in b₂ iff ex t being type of T st
( x = t & a in adjs t ) ) ) holds
b₁ = b₂

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 b₃ being Subset of T holds
( b₃ = types a iff for x being object holds
( x in b₃ 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 b₁ being Subset of T st
for t being type of T holds
( t in b₁ iff for a being adjective of T st a in A holds
t in types a )

proof end;

uniqueness
for b₁, b₂ being Subset of T st ( for t being type of T holds
( t in b₁ 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 b₂ iff for a being adjective of T st a in A holds
t in types a ) ) holds
b₁ = b₂

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 b₃ being Subset of T holds
( b₃ = types A iff for t being type of T holds
( t in b₃ 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 b₁ being 1 -element reflexive transitive antisymmetric complete upper-bounded strict TA-structure st
( not b₁ is void & b₁ is Mizar-widening-like & b₁ is involutive & b₁ is without_fixpoints & b₁ is consistent & b₁ is adj-structured & b₁ 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 b₁ being FinSequence of the carrier of T st
( len b₁ = (len p) + 1 & b₁ . 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 = b₁ . i holds
b₁ . (i + 1) = a ast t ) )

proof end;

correctness
uniqueness
for b₁, b₂ being FinSequence of the carrier of T st len b₁ = (len p) + 1 & b₁ . 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 = b₁ . i holds
b₁ . (i + 1) = a ast t ) & len b₂ = (len p) + 1 & b₂ . 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 = b₂ . i holds
b₂ . (i + 1) = a ast t ) holds
b₁ = b₂;

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 b₄ being FinSequence of the carrier of T holds
( b₄ = apply (p,t) iff ( len b₄ = (len p) + 1 & b₄ . 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 = b₄ . i holds
b₄ . (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 b₁ being Function of the adjectives of T, the carrier of T st
for a being adjective of T holds b₁ . a = sup ((types a) \/ (types (non- a)))

proof end;

uniqueness
for b₁, b₂ being Function of the adjectives of T, the carrier of T st ( for a being adjective of T holds b₁ . a = sup ((types a) \/ (types (non- a))) ) & ( for a being adjective of T holds b₂ . a = sup ((types a) \/ (types (non- a))) ) holds
b₁ = b₂

proof end;

end;

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

definition

attr c₁ is strict ;
struct TAS-structure -> TA-structure ;
aggr TAS-structure(# carrier, adjectives, InternalRel, non-op, adj-map, sub-map #) -> TAS-structure ;
sel sub-map c₁ -> Function of the adjectives of c₁, the carrier of c₁;

end;

registration

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

existence
ex b₁ being TAS-structure st
( not b₁ is void & b₁ is reflexive & b₁ is 1 -element & b₁ 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{ P₁[ set ] } :

ex A being finite set st
( P₁[A] & ( for B being set st B c= A & P₁[B] holds
B = A ) )

provided

A1: ex A being finite set st P₁[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 b₁ being 1 -element reflexive transitive antisymmetric complete upper-bounded non void strict TAS-structure st
( b₁ is Mizar-widening-like & b₁ is involutive & b₁ is without_fixpoints & b₁ is consistent & b₁ is adj-structured & b₁ is adjs-typed & b₁ is non-absorbing & b₁ is subjected & b₁ 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 b₁ being Relation of T st
for t1, t2 being type of T holds
( [t1,t2] in b₁ 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 b₁, b₂ being Relation of T st ( for t1, t2 being type of T holds
( [t1,t2] in b₁ 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 b₂ iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def31 defines @--> ABCMIZ_0:def 31 :
for T being non empty reflexive transitive non void TAS-structure
for b₂ being Relation of T holds
( b₂ = T @--> iff for t1, t2 being type of T holds
( [t1,t2] in b₂ 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{ F₁() -> non empty set , P₁[ set , set ], F₂() -> Relation of F₁() } :

for x, y being Element of F₁() st F₂() reduces x,y holds
P₁[x,y]

provided

A1: for x, y being Element of F₁() st [x,y] in F₂() holds
P₁[x,y] and
A2: for x being Element of F₁() holds P₁[x,x] and
A3: for x, y, z being Element of F₁() st P₁[x,y] & P₁[y,z] holds
P₁[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;