:: by Grzegorz Bancerek

::

:: Received August 8, 2003

:: Copyright (c) 2003-2021 Association of Mizar Users

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

for T being RelStr holds

( T is Noetherian iff the InternalRel of T is co-well_founded );

definition

let T be non empty RelStr ;

( 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 ) ) )

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

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

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

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

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

for T being Poset holds

( T is Mizar-widening-like iff ( T is sup-Semilattice & T is Noetherian ) );

registration

for b_{1} being Poset st b_{1} is Mizar-widening-like holds

( b_{1} is Noetherian & b_{1} is with_suprema & b_{1} is upper-bounded )
end;

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

coherence for b

( b

proof end;

registration

for b_{1} being sup-Semilattice st b_{1} is Noetherian holds

b_{1} is Mizar-widening-like
;

end;

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

coherence for b

b

registration

ex b_{1} being complete sup-Semilattice st b_{1} is Mizar-widening-like
end;

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

proof end;

registration
end;

definition

attr c_{1} is strict ;

struct AdjectiveStr -> ;

aggr AdjectiveStr(# adjectives, non-op #) -> AdjectiveStr ;

sel adjectives c_{1} -> set ;

sel non-op c_{1} -> UnOp of the adjectives of c_{1};

end;
struct AdjectiveStr -> ;

aggr AdjectiveStr(# adjectives, non-op #) -> AdjectiveStr ;

sel adjectives c

sel non-op c

:: deftheorem Def4 defines void ABCMIZ_0:def 4 :

for A being AdjectiveStr holds

( A is void iff the adjectives of A is empty );

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 ;

A2 is void ;

definition

let A be AdjectiveStr ;

let a be Element of the adjectives of A;

coherence

the non-op of A . a is adjective of A

end;
let a be Element of the adjectives of A;

coherence

the non-op of A . a is adjective of A

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

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 ;

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 ;

end;
attr A is involutive means :Def6: :: ABCMIZ_0:def 6

for a being adjective of A holds non- (non- a) = a;

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;

for a being adjective of A holds not non- a = a;

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

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

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 )

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

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

A2 is without_fixpoints

proof end;

registration

existence

ex b_{1} being strict AdjectiveStr st

( not b_{1} is void & b_{1} is involutive & b_{1} is without_fixpoints )

end;
ex b

( not b

proof end;

registration
end;

definition

attr c_{1} is strict ;

struct TA-structure -> RelStr , AdjectiveStr ;

aggr TA-structure(# carrier, adjectives, InternalRel, non-op, adj-map #) -> TA-structure ;

sel adj-map c_{1} -> Function of the carrier of c_{1},(Fin the adjectives of c_{1});

end;
struct TA-structure -> RelStr , AdjectiveStr ;

aggr TA-structure(# carrier, adjectives, InternalRel, non-op, adj-map #) -> TA-structure ;

sel adj-map c

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

coherence

not TA-structure(# X,A,r,n,a #) is empty ;

end;
let A be set ;

let r be Relation of X;

let n be UnOp of A;

let a be Function of X,(Fin A);

coherence

not TA-structure(# X,A,r,n,a #) is empty ;

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

coherence

not TA-structure(# X,A,r,n,a #) is void ;

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

coherence

not TA-structure(# X,A,r,n,a #) is void ;

registration

existence

ex b_{1} being TA-structure st

( b_{1} is 1 -element & b_{1} is reflexive & not b_{1} is void & b_{1} is involutive & b_{1} is without_fixpoints & b_{1} is strict )

end;
ex b

( b

proof end;

definition

let T be TA-structure ;

let t be Element of T;

coherence

the adj-map of T . t is Subset of the adjectives of T

end;
let t be Element of T;

coherence

the adj-map of T . t is Subset of the adjectives of T

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

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 ;

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 ;

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

for t being type of T

for a being adjective of T st a in adjs t holds

not non- a in adjs t;

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

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

T2 is consistent

proof end;

definition

let T be non empty TA-structure ;

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

the adj-map of T is join-preserving Function of T,((BoolePoset the adjectives of T) opp);

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

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

T2 is adj-structured

proof end;

definition

let T be reflexive transitive antisymmetric with_suprema TA-structure ;

( T is adj-structured iff for t1, t2 being type of T holds adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2) )

end;
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 for t1, t2 being type of T holds adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2);

( T is adj-structured iff for t1, t2 being type of T holds adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2) )

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

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

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;

ex b_{1} being Subset of T st

for x being object holds

( x in b_{1} iff ex t being type of T st

( x = t & a in adjs t ) )

for b_{1}, b_{2} being Subset of T st ( for x being object holds

( x in b_{1} iff ex t being type of T st

( x = t & a in adjs t ) ) ) & ( for x being object holds

( x in b_{2} iff ex t being type of T st

( x = t & a in adjs t ) ) ) holds

b_{1} = b_{2}

end;
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 for x being object holds

( x in it iff ex t being type of T st

( x = t & a in adjs t ) );

ex b

for x being object holds

( x in b

( x = t & a in adjs t ) )

proof end;

uniqueness for b

( x in b

( x = t & a in adjs t ) ) ) & ( for x being object holds

( x in b

( x = t & a in adjs t ) ) ) holds

b

proof 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_{3} being Subset of T holds

( b_{3} = types a iff for x being object holds

( x in b_{3} iff ex t being type of T st

( x = t & a in adjs t ) ) );

for T being TA-structure

for a being Element of the adjectives of T

for b

( b

( x in b

( x = t & a in adjs t ) ) );

definition

let T be non empty TA-structure ;

let A be Subset of the adjectives of T;

ex b_{1} being Subset of T st

for t being type of T holds

( t in b_{1} iff for a being adjective of T st a in A holds

t in types a )

for b_{1}, b_{2} being Subset of T st ( for t being type of T holds

( t in b_{1} 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_{2} iff for a being adjective of T st a in A holds

t in types a ) ) holds

b_{1} = b_{2}

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

ex b

for t being type of T holds

( t in b

t in types a )

proof end;

uniqueness for b

( t in b

t in types a ) ) & ( for t being type of T holds

( t in b

t in types a ) ) holds

b

proof 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_{3} being Subset of T holds

( b_{3} = types A iff for t being type of T holds

( t in b_{3} iff for a being adjective of T st a in A holds

t in types a ) );

for T being non empty TA-structure

for A being Subset of the adjectives of T

for b

( b

( t in b

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

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 }

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 )

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 )

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 }

for t being type of T holds adjs t = { a where a is adjective of T : t in types a }

proof end;

definition

let T be TA-structure ;

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

for a being adjective of T holds not (types a) \/ (types (non- a)) is empty ;

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

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

T2 is adjs-typed

proof end;

registration

ex b_{1} being 1 -element reflexive transitive antisymmetric complete upper-bounded strict TA-structure st

( not b_{1} is void & b_{1} is Mizar-widening-like & b_{1} is involutive & b_{1} is without_fixpoints & b_{1} is consistent & b_{1} is adj-structured & b_{1} is adjs-typed )
end;

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

( not b

proof end;

registration

let T be reflexive transitive antisymmetric with_suprema adj-structured TA-structure ;

let a be adjective of T;

coherence

( types a is lower & types a is directed )

end;
let a be adjective of T;

coherence

( types a is lower & types a is directed )

proof end;

registration

let T be reflexive transitive antisymmetric with_suprema adj-structured TA-structure ;

let A be Subset of the adjectives of T;

coherence

( types A is lower & types A is directed )

end;
let A be Subset of the adjectives of T;

coherence

( types A is lower & types A is directed )

proof end;

definition

let T be TA-structure ;

let t be Element of T;

let a be adjective of T;

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

ex t9 being type of T st

( t9 in types a & t9 <= t );

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

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;

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

ex t9 being type of T st

( A c= adjs t9 & t9 <= t );

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

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

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;

coherence

sup ((types a) /\ (downarrow t)) is type of T ;

end;
let t be Element of T;

let a be adjective of T;

coherence

sup ((types a) /\ (downarrow t)) is type of T ;

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

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

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)

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

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 )

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 )

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

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

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;

coherence

sup ((types A) /\ (downarrow t)) is type of T ;

end;
let t be type of T;

let A be Subset of the adjectives of T;

coherence

sup ((types A) /\ (downarrow t)) is type of T ;

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

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

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;

ex b_{1} being FinSequence of the carrier of T st

( len b_{1} = (len p) + 1 & b_{1} . 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_{1} . i holds

b_{1} . (i + 1) = a ast t ) )

uniqueness

for b_{1}, b_{2} being FinSequence of the carrier of T st len b_{1} = (len p) + 1 & b_{1} . 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_{1} . i holds

b_{1} . (i + 1) = a ast t ) & len b_{2} = (len p) + 1 & b_{2} . 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_{2} . i holds

b_{2} . (i + 1) = a ast t ) holds

b_{1} = b_{2};

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

ex b

( len b

for a being adjective of T

for t being type of T st i in dom p & a = p . i & t = b

b

proof end;

correctness uniqueness

for b

for a being adjective of T

for t being type of T st i in dom p & a = p . i & t = b

b

for a being adjective of T

for t being type of T st i in dom p & a = p . i & t = b

b

b

proof 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_{4} being FinSequence of the carrier of T holds

( b_{4} = apply (p,t) iff ( len b_{4} = (len p) + 1 & b_{4} . 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_{4} . i holds

b_{4} . (i + 1) = a ast t ) ) );

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

( b

for a being adjective of T

for t being type of T st i in dom p & a = p . i & t = b

b

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;

coherence

not apply (p,t) is empty

end;
let t be type of T;

let p be FinSequence of the adjectives of T;

coherence

not apply (p,t) is empty

proof 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*>

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)*>

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;

coherence

(apply (v,t)) . ((len v) + 1) is type of T

end;
let t be type of T;

let v be FinSequence of the adjectives of T;

coherence

(apply (v,t)) . ((len v) + 1) is type of T

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

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;

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

for t being type of T

for a being adjective of T holds <*a*> ast t = a ast t

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)

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

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

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

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

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;

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

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;

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

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 ;

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 )

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 )

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

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 )

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

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)

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

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

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

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

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

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)

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

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 )

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 )

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

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

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

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 ;

ex b_{1} being Function of the adjectives of T, the carrier of T st

for a being adjective of T holds b_{1} . a = sup ((types a) \/ (types (non- a)))

for b_{1}, b_{2} being Function of the adjectives of T, the carrier of T st ( for a being adjective of T holds b_{1} . a = sup ((types a) \/ (types (non- a))) ) & ( for a being adjective of T holds b_{2} . a = sup ((types a) \/ (types (non- a))) ) holds

b_{1} = b_{2}

end;
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 for a being adjective of T holds it . a = sup ((types a) \/ (types (non- a)));

ex b

for a being adjective of T holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def22 defines sub ABCMIZ_0:def 22 :

for T being non empty non void TA-structure

for b_{2} being Function of the adjectives of T, the carrier of T holds

( b_{2} = sub T iff for a being adjective of T holds b_{2} . a = sup ((types a) \/ (types (non- a))) );

for T being non empty non void TA-structure

for b

( b

definition

attr c_{1} 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_{1} -> Function of the adjectives of c_{1}, the carrier of c_{1};

end;
struct TAS-structure -> TA-structure ;

aggr TAS-structure(# carrier, adjectives, InternalRel, non-op, adj-map, sub-map #) -> TAS-structure ;

sel sub-map c

registration

existence

ex b_{1} being TAS-structure st

( not b_{1} is void & b_{1} is reflexive & b_{1} is 1 -element & b_{1} is strict )

end;
ex b

( not b

proof end;

definition

let T be non empty non void TAS-structure ;

let a be adjective of T;

coherence

the sub-map of T . a is type of T ;

end;
let a be adjective of T;

coherence

the sub-map of T . a is type of T ;

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

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 ;

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

the sub-map of T * the non-op of T = the sub-map of T;

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

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

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 ;

( T is non-absorbing iff for a being adjective of T holds sub (non- a) = sub a )

end;
redefine attr T is non-absorbing means :: ABCMIZ_0:def 26

for a being adjective of T holds sub (non- a) = sub a;

compatibility for a being adjective of T holds sub (non- a) = sub a;

( T is non-absorbing iff for a being adjective of T holds sub (non- a) = sub a )

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

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

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;

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

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;

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

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

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 ;

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 )

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 )

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

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;

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

ex s being FinSequence of the adjectives of T st

( rng s = A & s is_properly_applicable_to t );

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

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 ;

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

for t being type of T holds {} the adjectives of T is_properly_applicable_to t

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

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 ;

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

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

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

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

ex b_{1} being 1 -element reflexive transitive antisymmetric complete upper-bounded non void strict TAS-structure st

( b_{1} is Mizar-widening-like & b_{1} is involutive & b_{1} is without_fixpoints & b_{1} is consistent & b_{1} is adj-structured & b_{1} is adjs-typed & b_{1} is non-absorbing & b_{1} is subjected & b_{1} is commutative )
end;

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

( b

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

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 ;

ex b_{1} being Relation of T st

for t1, t2 being type of T holds

( [t1,t2] in b_{1} iff ex a being adjective of T st

( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) )

for b_{1}, b_{2} being Relation of T st ( for t1, t2 being type of T holds

( [t1,t2] in b_{1} 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_{2} 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_{1} = b_{2}

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

ex b

for t1, t2 being type of T holds

( [t1,t2] in b

( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) )

proof end;

uniqueness for b

( [t1,t2] in b

( 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

( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) ) holds

b

proof end;

:: deftheorem Def31 defines @--> ABCMIZ_0:def 31 :

for T being non empty reflexive transitive non void TAS-structure

for b_{2} being Relation of T holds

( b_{2} = T @--> iff for t1, t2 being type of T holds

( [t1,t2] in b_{2} iff ex a being adjective of T st

( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) );

for T being non empty reflexive transitive non void TAS-structure

for b

( b

( [t1,t2] in b

( 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_{1}() -> non empty set , P_{1}[ set , set ], F_{2}() -> Relation of F_{1}() } :

provided

RedInd{ F

provided

A1:
for x, y being Element of F_{1}() st [x,y] in F_{2}() holds

P_{1}[x,y]
and

A2: for x being Element of F_{1}() holds P_{1}[x,x]
and

A3: for x, y, z being Element of F_{1}() st P_{1}[x,y] & P_{1}[y,z] holds

P_{1}[x,z]

P

A2: for x being Element of F

A3: for x, y, z being Element of F

P

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

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

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

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

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

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

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

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 )

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 )

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

coherence

nf (t,(T @-->)) is type of T

end;
let t be type of T;

coherence

nf (t,(T @-->)) is type of T

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

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

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;

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

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

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

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

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;