:: ABCMIZ_0 semantic presentation

registration

cluster non empty trivial reflexive -> non empty complete RelStr ;
coherence

proof end;

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 :

registration

cluster non empty trivial -> non empty Noetherian RelStr ;
coherence

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

proof end;

end;

:: deftheorem Def2 defines Noetherian ABCMIZ_0:def 2 :

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 :

registration

cluster Mizar-widening-like -> with_suprema upper-bounded Noetherian RelStr ;
coherence

proof end;

end;

registration

cluster Noetherian -> upper-bounded Noetherian Mizar-widening-like RelStr ;
coherence

proof end;

end;

registration

cluster complete Noetherian Mizar-widening-like RelStr ;
existence

proof end;

end;

registration

let T be Noetherian RelStr ;
cluster the InternalRel of T -> co-well_founded ;
coherence 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 :

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

proof end;

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

proof end;

end;

:: deftheorem defines non- ABCMIZ_0:def 5 :

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 :

:: deftheorem defines without_fixpoints ABCMIZ_0:def 7 :

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

proof end;

end;

registration

let A be non void AdjectiveStr ;
cluster the adjectives of A -> non empty ;
coherence 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 by STRUCT_0:def 1;

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

end;

registration

cluster non empty trivial reflexive complete Noetherian Mizar-widening-like non void involutive without_fixpoints strict TA-structure ;
existence

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

proof end;

end;

:: deftheorem defines adjs ABCMIZ_0:def 8 :

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 :

theorem Th8: :: ABCMIZ_0:8

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 :

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

proof end;

end;

:: deftheorem Def11 defines adj-structured ABCMIZ_0:def 11 :

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 set holds
( x in it iff ex t being type of T st
( x = t & a in adjs t ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines types ABCMIZ_0:def 12 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines types ABCMIZ_0:def 13 :

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 :

theorem Th17: :: ABCMIZ_0:17

proof end;

registration

cluster non empty trivial reflexive transitive antisymmetric complete upper-bounded Noetherian Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure ;
existence

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

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

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 :Def15: :: ABCMIZ_0:def 15
ex t' being type of T st
( t' in types a & t' <= t );

end;

:: deftheorem Def15 defines is_applicable_to ABCMIZ_0:def 15 :

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 :Def16: :: ABCMIZ_0:def 16
ex t' being type of T st
( A c= adjs t' & t' <= t );

end;

:: deftheorem Def16 defines is_applicable_to ABCMIZ_0:def 16 :

theorem :: ABCMIZ_0:19

canceled;

theorem Th20: :: ABCMIZ_0:20

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 ;

end;

:: deftheorem defines ast ABCMIZ_0:def 17 :

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 ast t <= 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 in adjs (a ast t)

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

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

proof end;

theorem Th25: :: ABCMIZ_0:25

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

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 Th27: :: ABCMIZ_0:27

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 ;

end;

:: deftheorem defines ast ABCMIZ_0:def 18 :

theorem Th28: :: ABCMIZ_0:28

for T being non empty reflexive transitive antisymmetric TA-structure
for t being type of T holds ({} the adjectives of T) ast t = t

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