begin
:: 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 );
:: 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 ) ) );
:: 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 ) );
theorem Th1:
begin
:: deftheorem Def4 defines void ABCMIZ_0:def 4 :
for A being AdjectiveStr holds
( A is void iff the adjectives of A is empty );
theorem
:: deftheorem defines non- ABCMIZ_0:def 5 :
for A being AdjectiveStr
for a being Element of the adjectives of A holds non- a = the non-op of A . a;
theorem
:: deftheorem Def6 defines involutive ABCMIZ_0:def 6 :
for A being AdjectiveStr holds
( A is involutive iff for a being adjective of A holds non- (non- a) = a );
:: deftheorem defines without_fixpoints ABCMIZ_0:def 7 :
for A being AdjectiveStr holds
( A is without_fixpoints iff for a being adjective of A holds not non- a = a );
theorem Th4:
theorem Th5:
theorem Th6:
:: deftheorem defines adjs ABCMIZ_0:def 8 :
for T being TA-structure
for t being Element of T holds adjs t = the adj-map of T . t;
theorem
:: deftheorem Def9 defines consistent ABCMIZ_0:def 9 :
for T being TA-structure holds
( T is consistent iff for t being type of T
for a being adjective of T st a in adjs t holds
not non- a in adjs t );
theorem Th8:
:: deftheorem defines adj-structured ABCMIZ_0:def 10 :
for T being non empty TA-structure holds
( T is adj-structured iff the adj-map of T is join-preserving Function of T,((BoolePoset the adjectives of T) opp) );
theorem Th9:
:: deftheorem Def11 defines adj-structured ABCMIZ_0:def 11 :
for T being reflexive transitive antisymmetric with_suprema TA-structure holds
( T is adj-structured iff for t1, t2 being type of T holds adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2) );
theorem Th10:
:: deftheorem Def12 defines types ABCMIZ_0:def 12 :
for T being TA-structure
for a being Element of the adjectives of T
for b3 being Subset of T holds
( b3 = types a iff for x being set holds
( x in b3 iff ex t being type of T st
( x = t & a in adjs t ) ) );
:: deftheorem Def13 defines types ABCMIZ_0:def 13 :
for T being non empty TA-structure
for A being Subset of the adjectives of T
for b3 being Subset of T holds
( b3 = types A iff for t being type of T holds
( t in b3 iff for a being adjective of T st a in A holds
t in types a ) );
theorem Th11:
theorem
theorem Th13:
theorem Th14:
theorem
theorem Th16:
:: deftheorem defines adjs-typed ABCMIZ_0:def 14 :
for T being TA-structure holds
( T is adjs-typed iff for a being adjective of T holds not (types a) \/ (types (non- a)) is empty );
theorem Th17:
theorem
begin
:: deftheorem Def15 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 ) );
:: deftheorem Def16 defines is_applicable_to ABCMIZ_0:def 16 :
for T being TA-structure
for t being type of T
for A being Subset of the adjectives of T holds
( A is_applicable_to t iff ex t9 being type of T st
( A c= adjs t9 & t9 <= t ) );
theorem
canceled;
theorem Th20:
:: deftheorem defines ast ABCMIZ_0:def 17 :
for T being non empty reflexive transitive TA-structure
for t being Element of T
for a being adjective of T holds a ast t = sup ((types a) /\ (downarrow t));
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem
theorem Th27:
:: deftheorem defines ast ABCMIZ_0:def 18 :
for T being non empty reflexive transitive TA-structure
for t being type of T
for A being Subset of the adjectives of T holds A ast t = sup ((types A) /\ (downarrow t));
theorem Th28:
:: deftheorem Def19 defines apply ABCMIZ_0:def 19 :
for T being non empty reflexive transitive non void TA-structure
for t being type of T
for p being FinSequence of the adjectives of T
for b4 being FinSequence of the carrier of T holds
( b4 = apply (p,t) iff ( len b4 = (len p) + 1 & b4 . 1 = t & ( for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p & a = p . i & t = b4 . i holds
b4 . (i + 1) = a ast t ) ) );
theorem
theorem Th30:
:: deftheorem defines ast ABCMIZ_0:def 20 :
for T being non empty reflexive transitive non void TA-structure
for t being type of T
for v being FinSequence of the adjectives of T holds v ast t = (apply (v,t)) . ((len v) + 1);
theorem
theorem Th32:
theorem
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
:: deftheorem Def21 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 natural number
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
theorem
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem
theorem Th50:
theorem Th51:
theorem
theorem Th53:
theorem
theorem Th55:
theorem Th56:
theorem Th57:
begin
:: deftheorem Def22 defines sub ABCMIZ_0:def 22 :
for T being non empty non void TA-structure
for b2 being Function of the adjectives of T, the carrier of T holds
( b2 = sub T iff for a being adjective of T holds b2 . a = sup ((types a) \/ (types (non- a))) );
:: 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;
:: deftheorem defines non-absorbing ABCMIZ_0:def 24 :
for T being non empty non void TAS-structure holds
( T is non-absorbing iff the sub-map of T * the non-op of T = the sub-map of T );
:: deftheorem defines subjected ABCMIZ_0:def 25 :
for T being non empty non void TAS-structure holds
( T is subjected iff for a being adjective of T holds
( (types a) \/ (types (non- a)) is_<=_than sub a & ( types a <> {} & types (non- a) <> {} implies sub a = sup ((types a) \/ (types (non- a))) ) ) );
:: 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 );
:: deftheorem Def27 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 ) );
:: deftheorem Def28 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 natural number
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 Th58:
theorem
theorem
theorem Th61:
theorem Th62:
:: deftheorem Def29 defines is_properly_applicable_to ABCMIZ_0:def 29 :
for T being non empty reflexive transitive non void TAS-structure
for t being type of T
for A being Subset of the adjectives of T holds
( A is_properly_applicable_to t iff ex s being FinSequence of the adjectives of T st
( rng s = A & s is_properly_applicable_to t ) );
theorem Th63:
theorem Th64:
scheme
MinimalFiniteSet{
P1[
set ] } :
ex
A being
finite set st
(
P1[
A] & ( for
B being
set st
B c= A &
P1[
B] holds
B = A ) )
provided
theorem Th65:
:: 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 ) );
theorem Th66:
begin
:: deftheorem Def31 defines @--> ABCMIZ_0:def 31 :
for T being non empty reflexive transitive non void TAS-structure
for b2 being Relation of T holds
( b2 = T @--> iff for t1, t2 being type of T holds
( [t1,t2] in b2 iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) );
theorem Th67:
scheme
RedInd{
F1()
-> non
empty set ,
P1[
set ,
set ],
F2()
-> Relation of
F1() } :
provided
A1:
for
x,
y being
Element of
F1() st
[x,y] in F2() holds
P1[
x,
y]
and A2:
for
x being
Element of
F1() holds
P1[
x,
x]
and A3:
for
x,
y,
z being
Element of
F1() st
P1[
x,
y] &
P1[
y,
z] holds
P1[
x,
z]
theorem Th68:
theorem Th69:
theorem Th70:
theorem Th71:
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
theorem Th76:
theorem Th77:
theorem Th78:
begin
:: deftheorem defines radix ABCMIZ_0:def 32 :
for T being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure
for t being type of T holds radix t = nf (t,(T @-->));
theorem Th79:
theorem
theorem Th81:
theorem Th82:
theorem
theorem