:: ABCMIZ_0 semantic presentation

registration

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

proof end;

end;

definition

let c₁ be RelStr ;
mode type of a₁ is Element of a₁;

end;

definition

let c₁ be RelStr ;
attr a₁ is Noetherian means :Def1: :: ABCMIZ_0:def 1
the InternalRel of a₁ 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 c₁ be non empty RelStr ;
redefine attr a₁ is Noetherian means :Def2: :: ABCMIZ_0:def 2
for b₁ being non empty Subset of a₁ ex b₂ being Element of a₁ st
( b₂ in b₁ & ( for b₃ being Element of a₁ st b₃ in b₁ holds
not b₂ < b₃ ) );
compatibility

proof end;

end;

:: deftheorem Def2 defines Noetherian ABCMIZ_0:def 2 :

definition

let c₁ be Poset;
attr a₁ is Mizar-widening-like means :: ABCMIZ_0:def 3
( a₁ is sup-Semilattice & a₁ is Noetherian );

end;

:: deftheorem Def3 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 c₁ be Noetherian RelStr ;
cluster the InternalRel of a₁ -> co-well_founded ;
coherence by Def1;

end;

theorem Th1: :: ABCMIZ_0:1

for b₁ being Noetherian sup-Semilattice
for b₂ being Ideal of b₁ holds
( ex_sup_of b₂,b₁ & sup b₂ in b₂ )

proof end;

definition

attr a₁ is strict;
struct AdjectiveStr -> ;
aggr AdjectiveStr(# adjectives, non-op #) -> AdjectiveStr ;
sel adjectives c₁ -> set ;
sel non-op c₁ -> UnOp of the adjectives of a₁;

end;

definition

let c₁ 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 Th2: :: ABCMIZ_0:2

for b₁, b₂ being AdjectiveStr st the adjectives of b₁ = the adjectives of b₂ & b₁ is void holds
b₂ is void

proof end;

definition

let c₁ be AdjectiveStr ;
let c₂ be Element of the adjectives of c₁;
func non- c₂ -> adjective of a₁ equals :: ABCMIZ_0:def 5
the non-op of a₁ . a₂;
coherence

proof end;

end;

:: deftheorem Def5 defines non- ABCMIZ_0:def 5 :

theorem Th3: :: ABCMIZ_0:3

for b₁, b₂ being AdjectiveStr st AdjectiveStr(# the adjectives of b₁,the non-op of b₁ #) = AdjectiveStr(# the adjectives of b₂,the non-op of b₂ #) holds
for b₃ being adjective of b₁
for b₄ being adjective of b₂ st b₃ = b₄ holds
non- b₃ = non- b₄ ;

definition

let c₁ be AdjectiveStr ;
attr a₁ is involutive means :Def6: :: ABCMIZ_0:def 6
for b₁ being adjective of a₁ holds non- (non- b₁) = b₁;
attr a₁ is without_fixpoints means :: ABCMIZ_0:def 7
for b₁ being adjective of a₁ holds not non- b₁ = b₁;

end;

:: deftheorem Def6 defines involutive ABCMIZ_0:def 6 :

:: deftheorem Def7 defines without_fixpoints ABCMIZ_0:def 7 :

theorem Th4: :: ABCMIZ_0:4

for b₁, b₂ being set st b₁ <> b₂ holds
for b₃ being AdjectiveStr st the adjectives of b₃ = {b₁,b₂} & the non-op of b₃ . b₁ = b₂ & the non-op of b₃ . b₂ = b₁ holds
( not b₃ is void & b₃ is involutive & b₃ is without_fixpoints )

proof end;

theorem Th5: :: ABCMIZ_0:5

for b₁, b₂ being AdjectiveStr st AdjectiveStr(# the adjectives of b₁,the non-op of b₁ #) = AdjectiveStr(# the adjectives of b₂,the non-op of b₂ #) & b₁ is involutive holds
b₂ is involutive

proof end;

theorem Th6: :: ABCMIZ_0:6

for b₁, b₂ being AdjectiveStr st AdjectiveStr(# the adjectives of b₁,the non-op of b₁ #) = AdjectiveStr(# the adjectives of b₂,the non-op of b₂ #) & b₁ is without_fixpoints holds
b₂ is without_fixpoints

proof end;

registration

cluster strict non void involutive without_fixpoints AdjectiveStr ;
existence

proof end;

end;

registration

let c₁ be non void AdjectiveStr ;
cluster the adjectives of a₁ -> non empty ;
coherence by Def4;

end;

definition

attr a₁ 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 a₁, Fin the adjectives of a₁;

end;

registration

let c₁ be non empty set ;
let c₂ be set ;
let c₃ be Relation of c₁;
let c₄ be UnOp of c₂;
let c₅ be Function of c₁, Fin c₂;
cluster TA-structure(# a₁,a₂,a₃,a₄,a₅ #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

registration

let c₁ be set ;
let c₂ be non empty set ;
let c₃ be Relation of c₁;
let c₄ be UnOp of c₂;
let c₅ be Function of c₁, Fin c₂;
cluster TA-structure(# a₁,a₂,a₃,a₄,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 c₁ be TA-structure ;
let c₂ be Element of c₁;
func adjs c₂ -> Subset of the adjectives of a₁ equals :: ABCMIZ_0:def 8
the adj-map of a₁ . a₂;
coherence

proof end;

end;

:: deftheorem Def8 defines adjs ABCMIZ_0:def 8 :

theorem Th7: :: ABCMIZ_0:7

for b₁, b₂ being TA-structure st TA-structure(# the carrier of b₁,the adjectives of b₁,the InternalRel of b₁,the non-op of b₁,the adj-map of b₁ #) = TA-structure(# the carrier of b₂,the adjectives of b₂,the InternalRel of b₂,the non-op of b₂,the adj-map of b₂ #) holds
for b₃ being type of b₁
for b₄ being type of b₂ st b₃ = b₄ holds
adjs b₃ = adjs b₄ ;

definition

let c₁ be TA-structure ;
attr a₁ is consistent means :Def9: :: ABCMIZ_0:def 9
for b₁ being type of a₁
for b₂ being adjective of a₁ st b₂ in adjs b₁ holds
not non- b₂ in adjs b₁;

end;

:: deftheorem Def9 defines consistent ABCMIZ_0:def 9 :

theorem Th8: :: ABCMIZ_0:8

proof end;

definition

let c₁ be non empty TA-structure ;
attr a₁ is adj-structured means :: ABCMIZ_0:def 10
the adj-map of a₁ is join-preserving Function of a₁,((BoolePoset the adjectives of a₁) opp );

end;

:: deftheorem Def10 defines adj-structured ABCMIZ_0:def 10 :

theorem Th9: :: ABCMIZ_0:9

for b₁, b₂ being non empty TA-structure st TA-structure(# the carrier of b₁,the adjectives of b₁,the InternalRel of b₁,the non-op of b₁,the adj-map of b₁ #) = TA-structure(# the carrier of b₂,the adjectives of b₂,the InternalRel of b₂,the non-op of b₂,the adj-map of b₂ #) & b₁ is adj-structured holds
b₂ is adj-structured

proof end;

definition

let c₁ be reflexive transitive antisymmetric with_suprema TA-structure ;
redefine attr a₁ is adj-structured means :Def11: :: ABCMIZ_0:def 11
for b₁, b₂ being type of a₁ holds adjs (b₁ "\/" b₂) = (adjs b₁) /\ (adjs b₂);
compatibility

proof end;

end;

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

theorem Th10: :: ABCMIZ_0:10

for b₁ being reflexive transitive antisymmetric with_suprema TA-structure st b₁ is adj-structured holds
for b₂, b₃ being type of b₁ st b₂ <= b₃ holds
adjs b₃ c= adjs b₂

proof end;

definition

let c₁ be TA-structure ;
let c₂ be Element of the adjectives of c₁;
func types c₂ -> Subset of a₁ means :Def12: :: ABCMIZ_0:def 12
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being type of a₁ st
( b₁ = b₂ & a₂ in adjs b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines types ABCMIZ_0:def 12 :

definition

let c₁ be non empty TA-structure ;
let c₂ be Subset of the adjectives of c₁;
func types c₂ -> Subset of a₁ means :Def13: :: ABCMIZ_0:def 13
for b₁ being type of a₁ holds
( b₁ in a₃ iff for b₂ being adjective of a₁ st b₂ in a₂ holds
b₁ in types b₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines types ABCMIZ_0:def 13 :

theorem Th11: :: ABCMIZ_0:11

for b₁, b₂ being TA-structure st TA-structure(# the carrier of b₁,the adjectives of b₁,the InternalRel of b₁,the non-op of b₁,the adj-map of b₁ #) = TA-structure(# the carrier of b₂,the adjectives of b₂,the InternalRel of b₂,the non-op of b₂,the adj-map of b₂ #) holds
for b₃ being adjective of b₁
for b₄ being adjective of b₂ st b₃ = b₄ holds
types b₃ = types b₄

proof end;

theorem Th12: :: ABCMIZ_0:12

for b₁ being non empty TA-structure
for b₂ being adjective of b₁ holds types b₂ = { b₃ where B is type of b₁ : b₂ in adjs b₃ }

proof end;

theorem Th13: :: ABCMIZ_0:13

for b₁ being TA-structure
for b₂ being type of b₁
for b₃ being adjective of b₁ holds
( b₃ in adjs b₂ iff b₂ in types b₃ )

proof end;

theorem Th14: :: ABCMIZ_0:14

for b₁ being non empty TA-structure
for b₂ being type of b₁
for b₃ being Subset of the adjectives of b₁ holds
( b₃ c= adjs b₂ iff b₂ in types b₃ )

proof end;

theorem Th15: :: ABCMIZ_0:15

for b₁ being non void TA-structure
for b₂ being type of b₁ holds adjs b₂ = { b₃ where B is adjective of b₁ : b₂ in types b₃ }

proof end;

theorem Th16: :: ABCMIZ_0:16

for b₁ being non empty TA-structure holds types ({} the adjectives of b₁) = the carrier of b₁

proof end;

definition

let c₁ be TA-structure ;
attr a₁ is adjs-typed means :: ABCMIZ_0:def 14
for b₁ being adjective of a₁ holds not (types b₁) \/ (types (non- b₁)) is empty;

end;

:: deftheorem Def14 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 Th18: :: ABCMIZ_0:18

for b₁ being consistent TA-structure
for b₂ being adjective of b₁ holds types b₂ misses types (non- b₂)

proof end;

registration

let c₁ be reflexive transitive antisymmetric with_suprema adj-structured TA-structure ;
let c₂ be adjective of c₁;
cluster types a₂ -> directed lower ;
coherence

proof end;

end;

registration

let c₁ be reflexive transitive antisymmetric with_suprema adj-structured TA-structure ;
let c₂ be Subset of the adjectives of c₁;
cluster types a₂ -> directed lower ;
coherence

proof end;

end;

definition

let c₁ be TA-structure ;
let c₂ be Element of c₁;
let c₃ be adjective of c₁;
pred c₃ is_applicable_to c₂ means :Def15: :: ABCMIZ_0:def 15
ex b₁ being type of a₁ st
( b₁ in types a₃ & b₁ <= a₂ );

end;

:: deftheorem Def15 defines is_applicable_to ABCMIZ_0:def 15 :

definition

let c₁ be TA-structure ;
let c₂ be type of c₁;
let c₃ be Subset of the adjectives of c₁;
pred c₃ is_applicable_to c₂ means :Def16: :: ABCMIZ_0:def 16
ex b₁ being type of a₁ st
( a₃ c= adjs b₁ & b₁ <= a₂ );

end;

:: deftheorem Def16 defines is_applicable_to ABCMIZ_0:def 16 :

theorem Th19: :: ABCMIZ_0:19

canceled;

theorem Th20: :: ABCMIZ_0:20

for b₁ being reflexive transitive antisymmetric with_suprema adj-structured TA-structure
for b₂ being adjective of b₁
for b₃ being type of b₁ st b₂ is_applicable_to b₃ holds
(types b₂) /\ (downarrow b₃) is Ideal of b₁

proof end;

definition

let c₁ be non empty reflexive transitive TA-structure ;
let c₂ be Element of c₁;
let c₃ be adjective of c₁;
func c₃ ast c₂ -> type of a₁ equals :: ABCMIZ_0:def 17
sup ((types a₃) /\ (downarrow a₂));
coherence ;

end;

:: deftheorem Def17 defines ast ABCMIZ_0:def 17 :

theorem Th21: :: ABCMIZ_0:21

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for b₂ being type of b₁
for b₃ being adjective of b₁ st b₃ is_applicable_to b₂ holds
b₃ ast b₂ <= b₂

proof end;

theorem Th22: :: ABCMIZ_0:22

proof end;

theorem Th23: :: ABCMIZ_0:23

proof end;

theorem Th24: :: ABCMIZ_0:24

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for b₂ being type of b₁
for b₃ being adjective of b₁
for b₄ being type of b₁ st b₄ <= b₂ & b₃ in adjs b₄ holds
( b₃ is_applicable_to b₂ & b₄ <= b₃ ast b₂ )

proof end;

theorem Th25: :: ABCMIZ_0:25

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for b₂ being type of b₁
for b₃ being adjective of b₁ st b₃ in adjs b₂ holds
( b₃ is_applicable_to b₂ & b₃ ast b₂ = b₂ )

proof end;

theorem Th26: :: ABCMIZ_0:26

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for b₂ being type of b₁
for b₃, b₄ being adjective of b₁ st b₃ is_applicable_to b₂ & b₄ is_applicable_to b₃ ast b₂ holds
( b₄ is_applicable_to b₂ & b₃ is_applicable_to b₄ ast b₂ & b₃ ast (b₄ ast b₂) = b₄ ast (b₃ ast b₂) )

proof end;

theorem Th27: :: ABCMIZ_0:27

for b₁ being reflexive transitive antisymmetric with_suprema adj-structured TA-structure
for b₂ being Subset of the adjectives of b₁
for b₃ being type of b₁ st b₂ is_applicable_to b₃ holds
(types b₂) /\ (downarrow b₃) is Ideal of b₁

proof end;

definition

let c₁ be non empty reflexive transitive TA-structure ;
let c₂ be type of c₁;
let c₃ be Subset of the adjectives of c₁;
func c₃ ast c₂ -> type of a₁ equals :: ABCMIZ_0:def 18
sup ((types a₃) /\ (downarrow a₂));
coherence ;

end;

:: deftheorem Def18 defines ast ABCMIZ_0:def 18 :

theorem Th28: :: ABCMIZ_0:28

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

proof end;

definition

let c₁ be non empty reflexive transitive non void TA-structure ;
let c₂ be type of c₁;
let c₃ be FinSequence of the adjectives of c₁;
func apply c₃,c₂ -> FinSequence of the carrier of a₁ means :Def19: :: ABCMIZ_0:def 19
( len a₄ = (len a₃) + 1 & a₄ . 1 = a₂ & ( for b₁ being Nat
for b₂ being adjective of a₁
for b₃ being type of a₁ st b₁ in dom a₃ & b₂ = a₃ . b₁ & b₃ = a₄ . b₁ holds
a₄ . (b₁ + 1) = b₂ ast b₃ ) );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def19 defines apply ABCMIZ_0:def 19 :

registration

let c₁ be non empty reflexive transitive non void TA-structure ;
let c₂ be type of c₁;
let c₃ be FinSequence of the adjectives of c₁;
cluster apply a₃,a₂ -> non empty ;
coherence

proof end;

end;

theorem Th29: :: ABCMIZ_0:29

for b₁ being non empty reflexive transitive non void TA-structure
for b₂ being type of b₁ holds apply (<*> the adjectives of b₁),b₂ = <*b₂*>

proof end;

theorem Th30: :: ABCMIZ_0:30

for b₁ being non empty reflexive transitive non void TA-structure
for b₂ being type of b₁
for b₃ being adjective of b₁ holds apply <*b₃*>,b₂ = <*b₂,(b₃ ast b₂)*>

proof end;

definition

let c₁ be non empty reflexive transitive non void TA-structure ;
let c₂ be type of c₁;
let c₃ be FinSequence of the adjectives of c₁;
func c₃ ast c₂ -> type of a₁ equals :: ABCMIZ_0:def 20
(apply a₃,a₂) . ((len a₃) + 1);
coherence

proof end;

end;

:: deftheorem Def20 defines ast ABCMIZ_0:def 20 :

theorem Th31: :: ABCMIZ_0:31

for b₁ being non empty reflexive transitive non void TA-structure
for b₂ being type of b₁ holds (<*> the adjectives of b₁) ast b₂ = b₂

proof end;

theorem Th32: :: ABCMIZ_0:32

for b₁ being non empty reflexive transitive non void TA-structure
for b₂ being type of b₁
for b₃ being adjective of b₁ holds <*b₃*> ast b₂ = b₃ ast b₂

proof end;

theorem Th33: :: ABCMIZ_0:33

for b₁, b₂ being FinSequence
for b₃ being natural number st b₃ >= 1 & b₃ < len b₁ holds
(b₁ $^ b₂) . b₃ = b₁ . b₃

proof end;

theorem Th34: :: ABCMIZ_0:34

for b₁ being non empty FinSequence
for b₂ being FinSequence
for b₃ being natural number st b₃ < len b₂ holds
(b₁ $^ b₂) . ((len b₁) + b₃) = b₂ . (b₃ + 1)

proof end;

theorem Th35: :: ABCMIZ_0:35

for b₁ being non empty reflexive transitive non void TA-structure
for b₂ being type of b₁
for b₃, b₄ being FinSequence of the adjectives of b₁ holds apply (b₃ ^ b₄),b₂ = (apply b₃,b₂) $^ (apply b₄,(b₃ ast b₂))

proof end;

theorem Th36: :: ABCMIZ_0:36

for b₁ being non empty reflexive transitive non void TA-structure
for b₂ being type of b₁
for b₃, b₄ being FinSequence of the adjectives of b₁
for b₅ being natural number st b₅ in dom b₃ holds
(apply (b₃ ^ b₄),b₂) . b₅ = (apply b₃,b₂) . b₅

proof end;

theorem Th37: :: ABCMIZ_0:37

for b₁ being non empty reflexive transitive non void TA-structure
for b₂ being type of b₁
for b₃, b₄ being FinSequence of the adjectives of b₁ holds (apply (b₃ ^ b₄),b₂) . ((len b₃) + 1) = b₃ ast b₂

proof end;

theorem Th38: :: ABCMIZ_0:38

for b₁ being non empty reflexive transitive non void TA-structure
for b₂ being type of b₁
for b₃, b₄ being FinSequence of the adjectives of b₁ holds b₄ ast (b₃ ast b₂) = (b₃ ^ b₄) ast b₂

proof end;

definition

let c₁ be non empty reflexive transitive non void TA-structure ;
let c₂ be type of c₁;
let c₃ be FinSequence of the adjectives of c₁;
pred c₃ is_applicable_to c₂ means :Def21: :: ABCMIZ_0:def 21
for b₁ being natural number
for b₂ being adjective of a₁
for b₃ being type of a₁ st b₁ in dom a₃ & b₂ = a₃ . b₁ & b₃ = (apply a₃,a₂) . b₁ holds
b₂ is_applicable_to b₃;

end;

:: deftheorem Def21 defines is_applicable_to ABCMIZ_0:def 21 :

theorem Th39: :: ABCMIZ_0:39

for b₁ being non empty reflexive transitive non void TA-structure
for b₂ being type of b₁ holds <*> the adjectives of b₁ is_applicable_to b₂

proof end;

theorem Th40: :: ABCMIZ_0:40

for b₁ being non empty reflexive transitive non void TA-structure
for b₂ being type of b₁
for b₃ being adjective of b₁ holds
( b₃ is_applicable_to b₂ iff <*b₃*> is_applicable_to b₂ )

proof end;

theorem Th41: :: ABCMIZ_0:41

for b₁ being non empty reflexive transitive non void TA-structure
for b₂ being type of b₁
for b₃, b₄ being FinSequence of the adjectives of b₁ st b₃ ^ b₄ is_applicable_to b₂ holds
( b₃ is_applicable_to b₂ & b₄ is_applicable_to b₃ ast b₂ )

proof end;

theorem Th42: :: ABCMIZ_0:42

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for b₂ being type of b₁
for b₃ being FinSequence of the adjectives of b₁ st b₃ is_applicable_to b₂ holds
for b₄, b₅ being natural number st 1 <= b₄ & b₄ <= b₅ & b₅ <= (len b₃) + 1 holds
for b₆, b₇ being type of b₁ st b₆ = (apply b₃,b₂) . b₄ & b₇ = (apply b₃,b₂) . b₅ holds
b₇ <= b₆

proof end;

theorem Th43: :: ABCMIZ_0:43

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for b₂ being type of b₁
for b₃ being FinSequence of the adjectives of b₁ st b₃ is_applicable_to b₂ holds
for b₄ being type of b₁ st b₄ in rng (apply b₃,b₂) holds
( b₃ ast b₂ <= b₄ & b₄ <= b₂ )

proof end;

theorem Th44: :: ABCMIZ_0:44

proof end;

theorem Th45: :: ABCMIZ_0:45

proof end;

theorem Th46: :: ABCMIZ_0:46

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for b₂ being type of b₁
for b₃ being FinSequence of the adjectives of b₁ st b₃ is_applicable_to b₂ holds
for b₄ being Subset of the adjectives of b₁ st b₄ = rng b₃ holds
b₄ is_applicable_to b₂

proof end;

theorem Th47: :: ABCMIZ_0:47

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for b₂ being type of b₁
for b₃, b₄ being FinSequence of the adjectives of b₁ st b₃ is_applicable_to b₂ & rng b₄ c= rng b₃ holds
for b₅ being type of b₁ st b₅ in rng (apply b₄,b₂) holds
b₃ ast b₂ <= b₅

proof end;

theorem Th48: :: ABCMIZ_0:48

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for b₂ being type of b₁
for b₃, b₄ being FinSequence of the adjectives of b₁ st b₃ ^ b₄ is_applicable_to b₂ holds
b₄ ^ b₃ is_applicable_to b₂

proof end;

theorem Th49: :: ABCMIZ_0:49

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for b₂ being type of b₁
for b₃, b₄ being FinSequence of the adjectives of b₁ st b₃ ^ b₄ is_applicable_to b₂ holds
(b₃ ^ b₄) ast b₂ = (b₄ ^ b₃) ast b₂

proof end;

theorem Th50: :: ABCMIZ_0:50

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for b₂ being type of b₁
for b₃ being Subset of the adjectives of b₁ st b₃ is_applicable_to b₂ holds
b₃ ast b₂ <= b₂

proof end;

theorem Th51: :: ABCMIZ_0:51

proof end;

theorem Th52: :: ABCMIZ_0:52

proof end;

theorem Th53: :: ABCMIZ_0:53

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for b₂ being type of b₁
for b₃ being Subset of the adjectives of b₁
for b₄ being type of b₁ st b₄ <= b₂ & b₃ c= adjs b₄ holds
( b₃ is_applicable_to b₂ & b₄ <= b₃ ast b₂ )

proof end;

theorem Th54: :: ABCMIZ_0:54

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for b₂ being type of b₁
for b₃ being Subset of the adjectives of b₁ st b₃ c= adjs b₂ holds
( b₃ is_applicable_to b₂ & b₃ ast b₂ = b₂ )

proof end;

theorem Th55: :: ABCMIZ_0:55

for b₁ being TA-structure
for b₂ being type of b₁
for b₃, b₄ being Subset of the adjectives of b₁ st b₃ is_applicable_to b₂ & b₄ c= b₃ holds
b₄ is_applicable_to b₂

proof end;

theorem Th56: :: ABCMIZ_0:56

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for b₂ being type of b₁
for b₃ being adjective of b₁
for b₄, b₅ being Subset of the adjectives of b₁ st b₅ = b₄ \/ {b₃} & b₅ is_applicable_to b₂ holds
b₃ ast (b₄ ast b₂) = b₅ ast b₂

proof end;

theorem Th57: :: ABCMIZ_0:57

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for b₂ being type of b₁
for b₃ being FinSequence of the adjectives of b₁ st b₃ is_applicable_to b₂ holds
for b₄ being Subset of the adjectives of b₁ st b₄ = rng b₃ holds
b₃ ast b₂ = b₄ ast b₂

proof end;

definition

let c₁ be non empty non void TA-structure ;
func sub c₁ -> Function of the adjectives of a₁,the carrier of a₁ means :Def22: :: ABCMIZ_0:def 22
for b₁ being adjective of a₁ holds a₂ . b₁ = sup ((types b₁) \/ (types (non- b₁)));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def22 defines sub ABCMIZ_0:def 22 :

definition

attr a₁ 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 a₁,the carrier of a₁;

end;

registration

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

proof end;

end;

definition

let c₁ be non empty non void TAS-structure ;
let c₂ be adjective of c₁;
func sub c₂ -> type of a₁ equals :: ABCMIZ_0:def 23
the sub-map of a₁ . a₂;
coherence ;

end;

:: deftheorem Def23 defines sub ABCMIZ_0:def 23 :

definition

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

end;

:: deftheorem Def24 defines non-absorbing ABCMIZ_0:def 24 :

:: deftheorem Def25 defines subjected ABCMIZ_0:def 25 :

definition

let c₁ be non empty non void TAS-structure ;
redefine attr a₁ is non-absorbing means :: ABCMIZ_0:def 26
for b₁ being adjective of a₁ holds sub (non- b₁) = sub b₁;
compatibility

proof end;

end;

:: deftheorem Def26 defines non-absorbing ABCMIZ_0:def 26 :

definition

let c₁ be non empty non void TAS-structure ;
let c₂ be Element of c₁;
let c₃ be adjective of c₁;
pred c₃ is_properly_applicable_to c₂ means :Def27: :: ABCMIZ_0:def 27
( a₂ <= sub a₃ & a₃ is_applicable_to a₂ );

end;

:: deftheorem Def27 defines is_properly_applicable_to ABCMIZ_0:def 27 :

definition

let c₁ be non empty reflexive transitive non void TAS-structure ;
let c₂ be type of c₁;
let c₃ be FinSequence of the adjectives of c₁;
pred c₃ is_properly_applicable_to c₂ means :Def28: :: ABCMIZ_0:def 28
for b₁ being natural number
for b₂ being adjective of a₁
for b₃ being type of a₁ st b₁ in dom a₃ & b₂ = a₃ . b₁ & b₃ = (apply a₃,a₂) . b₁ holds
b₂ is_properly_applicable_to b₃;

end;

:: deftheorem Def28 defines is_properly_applicable_to ABCMIZ_0:def 28 :

theorem Th58: :: ABCMIZ_0:58

for b₁ being non empty reflexive transitive non void TAS-structure
for b₂ being type of b₁
for b₃ being FinSequence of the adjectives of b₁ st b₃ is_properly_applicable_to b₂ holds
b₃ is_applicable_to b₂

proof end;

theorem Th59: :: ABCMIZ_0:59

for b₁ being non empty reflexive transitive non void TAS-structure
for b₂ being type of b₁ holds <*> the adjectives of b₁ is_properly_applicable_to b₂

proof end;

theorem Th60: :: ABCMIZ_0:60

for b₁ being non empty reflexive transitive non void TAS-structure
for b₂ being type of b₁
for b₃ being adjective of b₁ holds
( b₃ is_properly_applicable_to b₂ iff <*b₃*> is_properly_applicable_to b₂ )

proof end;

theorem Th61: :: ABCMIZ_0:61

for b₁ being non empty reflexive transitive non void TAS-structure
for b₂ being type of b₁
for b₃, b₄ being FinSequence of the adjectives of b₁ st b₃ ^ b₄ is_properly_applicable_to b₂ holds
( b₃ is_properly_applicable_to b₂ & b₄ is_properly_applicable_to b₃ ast b₂ )

proof end;

theorem Th62: :: ABCMIZ_0:62

for b₁ being non empty reflexive transitive non void TAS-structure
for b₂ being type of b₁
for b₃, b₄ being FinSequence of the adjectives of b₁ st b₃ is_properly_applicable_to b₂ & b₄ is_properly_applicable_to b₃ ast b₂ holds
b₃ ^ b₄ is_properly_applicable_to b₂

proof end;

definition

let c₁ be non empty reflexive transitive non void TAS-structure ;
let c₂ be type of c₁;
let c₃ be Subset of the adjectives of c₁;
pred c₃ is_properly_applicable_to c₂ means :Def29: :: ABCMIZ_0:def 29
ex b₁ being FinSequence of the adjectives of a₁ st
( rng b₁ = a₃ & b₁ is_properly_applicable_to a₂ );

end;

:: deftheorem Def29 defines is_properly_applicable_to ABCMIZ_0:def 29 :

theorem Th63: :: ABCMIZ_0:63

for b₁ being non empty reflexive transitive non void TAS-structure
for b₂ being type of b₁
for b₃ being Subset of the adjectives of b₁ st b₃ is_properly_applicable_to b₂ holds
b₃ is finite

proof end;

theorem Th64: :: ABCMIZ_0:64

for b₁ being non empty reflexive transitive non void TAS-structure
for b₂ being type of b₁ holds {} the adjectives of b₁ is_properly_applicable_to b₂

proof end;

scheme :: ABCMIZ_0:sch 1
s1{ P₁[ set ] } :

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

provided

E65: ex b₁ being finite set st P₁[b₁]

proof end;

theorem Th65: :: ABCMIZ_0:65

for b₁ being non empty reflexive transitive non void TAS-structure
for b₂ being type of b₁
for b₃ being Subset of the adjectives of b₁ st b₃ is_properly_applicable_to b₂ holds
ex b₄ being Subset of the adjectives of b₁ st
( b₄ c= b₃ & b₄ is_properly_applicable_to b₂ & b₃ ast b₂ = b₄ ast b₂ & ( for b₅ being Subset of the adjectives of b₁ st b₅ c= b₄ & b₅ is_properly_applicable_to b₂ & b₃ ast b₂ = b₅ ast b₂ holds
b₅ = b₄ ) )

proof end;

definition

let c₁ be non empty reflexive transitive non void TAS-structure ;
attr a₁ is commutative means :Def30: :: ABCMIZ_0:def 30
for b₁, b₂ being type of a₁
for b₃ being adjective of a₁ st b₃ is_properly_applicable_to b₁ & b₃ ast b₁ <= b₂ holds
ex b₄ being finite Subset of the adjectives of a₁ st
( b₄ is_properly_applicable_to b₁ "\/" b₂ & b₄ ast (b₁ "\/" b₂) = b₂ );

end;

:: deftheorem Def30 defines commutative ABCMIZ_0:def 30 :

registration

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

proof end;

end;

theorem Th66: :: ABCMIZ_0:66

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure
for b₂ being type of b₁
for b₃ being Subset of the adjectives of b₁ st b₃ is_properly_applicable_to b₂ holds
ex b₄ being one-to-one FinSequence of the adjectives of b₁ st
( rng b₄ = b₃ & b₄ is_properly_applicable_to b₂ )

proof end;

definition

let c₁ be non empty reflexive transitive non void TAS-structure ;
func c₁ @--> -> Relation of a₁ means :Def31: :: ABCMIZ_0:def 31
for b₁, b₂ being type of a₁ holds
( [b₁,b₂] in a₂ iff ex b₃ being adjective of a₁ st
( not b₃ in adjs b₂ & b₃ is_properly_applicable_to b₂ & b₃ ast b₂ = b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th67: :: ABCMIZ_0:67

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure holds b₁ @--> c= the InternalRel of b₁

proof end;

scheme :: ABCMIZ_0:sch 2
s2{ F₁() -> non empty set , P₁[ set , set ], F₂() -> Relation of F₁() } :

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

provided

E70: for b₁, b₂ being Element of F₁() st [b₁,b₂] in F₂() holds
P₁[b₁,b₂] and
E71: for b₁ being Element of F₁() holds P₁[b₁,b₁] and
E72: for b₁, b₂, b₃ being Element of F₁() st P₁[b₁,b₂] & P₁[b₂,b₃] holds
P₁[b₁,b₃]

proof end;

theorem Th68: :: ABCMIZ_0:68

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure
for b₂, b₃ being type of b₁ st b₁ @--> reduces b₂,b₃ holds
b₂ <= b₃

proof end;

theorem Th69: :: ABCMIZ_0:69

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure holds b₁ @--> is irreflexive

proof end;

theorem Th70: :: ABCMIZ_0:70

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure holds b₁ @--> is strongly-normalizing

proof end;

theorem Th71: :: ABCMIZ_0:71

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure
for b₂ being type of b₁
for b₃ being finite Subset of the adjectives of b₁ st ( for b₄ being Subset of the adjectives of b₁ st b₄ c= b₃ & b₄ is_properly_applicable_to b₂ & b₃ ast b₂ = b₄ ast b₂ holds
b₄ = b₃ ) holds
for b₄ being one-to-one FinSequence of the adjectives of b₁ st rng b₄ = b₃ & b₄ is_properly_applicable_to b₂ holds
for b₅ being natural number st 1 <= b₅ & b₅ <= len b₄ holds
[((apply b₄,b₂) . (b₅ + 1)),((apply b₄,b₂) . b₅)] in b₁ @-->

proof end;

theorem Th72: :: ABCMIZ_0:72

proof end;

theorem Th73: :: ABCMIZ_0:73

proof end;

theorem Th74: :: ABCMIZ_0:74

for b₁ being non empty set
for b₂ being Relation of b₁
for b₃ being RedSequence of b₂ st b₃ . 1 in b₁ holds
b₃ is FinSequence of b₁

proof end;

theorem Th75: :: ABCMIZ_0:75

for b₁ being non empty set
for b₂ being Relation of b₁
for b₃ being Element of b₁
for b₄ being set st b₂ reduces b₃,b₄ holds
b₄ in b₁

proof end;

theorem Th76: :: ABCMIZ_0:76

for b₁ being non empty set
for b₂ being Relation of b₁ st b₂ is with_UN_property & b₂ is weakly-normalizing holds
for b₃ being Element of b₁ holds nf b₃,b₂ in b₁

proof end;

theorem Th77: :: ABCMIZ_0:77

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure
for b₂, b₃ being type of b₁ st b₁ @--> reduces b₂,b₃ holds
ex b₄ being finite Subset of the adjectives of b₁ st
( b₄ is_properly_applicable_to b₃ & b₂ = b₄ ast b₃ )

proof end;

theorem Th78: :: ABCMIZ_0:78

for b₁ being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure holds
( b₁ @--> is with_Church-Rosser_property & b₁ @--> is with_UN_property )

proof end;

definition

let c₁ be non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure ;
let c₂ be type of c₁;
func radix c₂ -> type of a₁ equals :: ABCMIZ_0:def 32
nf a₂,(a₁ @--> );
coherence

proof end;

end;

:: deftheorem Def32 defines radix ABCMIZ_0:def 32 :

theorem Th79: :: ABCMIZ_0:79

for b₁ being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure
for b₂ being type of b₁ holds b₁ @--> reduces b₂, radix b₂

proof end;

theorem Th80: :: ABCMIZ_0:80

for b₁ being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure
for b₂ being type of b₁ holds b₂ <= radix b₂

proof end;

theorem Th81: :: ABCMIZ_0:81

for b₁ being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure
for b₂ being type of b₁
for b₃ being set st b₃ = { b₄ where B is type of b₁ : ex b₁ being finite Subset of the adjectives of b₁ st
( b₅ is_properly_applicable_to b₄ & b₅ ast b₄ = b₂ ) } holds
( ex_sup_of b₃,b₁ & radix b₂ = "\/" b₃,b₁ )

proof end;

theorem Th82: :: ABCMIZ_0:82

for b₁ being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure
for b₂, b₃ being type of b₁
for b₄ being adjective of b₁ st b₄ is_properly_applicable_to b₂ & b₄ ast b₂ <= radix b₃ holds
b₂ <= radix b₃

proof end;

theorem Th83: :: ABCMIZ_0:83

for b₁ being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure
for b₂, b₃ being type of b₁ st b₂ <= b₃ holds
radix b₂ <= radix b₃

proof end;

theorem Th84: :: ABCMIZ_0:84

for b₁ being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure
for b₂ being type of b₁
for b₃ being adjective of b₁ st b₃ is_properly_applicable_to b₂ holds
radix (b₃ ast b₂) = radix b₂

proof end;