begin
:: deftheorem Def1 defines Noetherian ABCMIZ_0:def 1 :
:: deftheorem Def2 defines Noetherian ABCMIZ_0:def 2 :
:: deftheorem defines Mizar-widening-like ABCMIZ_0:def 3 :
theorem Th1:
begin
:: deftheorem Def4 defines void ABCMIZ_0:def 4 :
theorem
:: deftheorem defines non- ABCMIZ_0:def 5 :
theorem
:: deftheorem Def6 defines involutive ABCMIZ_0:def 6 :
:: deftheorem defines without_fixpoints ABCMIZ_0:def 7 :
theorem Th4:
theorem Th5:
theorem Th6:
:: deftheorem defines adjs ABCMIZ_0:def 8 :
theorem
:: deftheorem Def9 defines consistent ABCMIZ_0:def 9 :
theorem Th8:
:: deftheorem defines adj-structured ABCMIZ_0:def 10 :
theorem Th9:
:: deftheorem Def11 defines adj-structured ABCMIZ_0:def 11 :
theorem Th10:
:: deftheorem Def12 defines types ABCMIZ_0:def 12 :
:: deftheorem Def13 defines types ABCMIZ_0:def 13 :
theorem Th11:
theorem
theorem Th13:
theorem Th14:
theorem
theorem Th16:
:: deftheorem defines adjs-typed ABCMIZ_0:def 14 :
theorem Th17:
theorem
begin
:: deftheorem Def15 defines is_applicable_to ABCMIZ_0:def 15 :
:: deftheorem Def16 defines is_applicable_to ABCMIZ_0:def 16 :
theorem
canceled;
theorem Th20:
:: deftheorem defines ast ABCMIZ_0:def 17 :
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem
theorem Th27:
:: deftheorem defines ast ABCMIZ_0:def 18 :
theorem Th28:
:: deftheorem Def19 defines apply ABCMIZ_0:def 19 :
theorem
theorem Th30:
:: deftheorem defines ast ABCMIZ_0:def 20 :
theorem
theorem Th32:
theorem
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
:: deftheorem Def21 defines is_applicable_to ABCMIZ_0:def 21 :
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 :
:: deftheorem defines sub ABCMIZ_0:def 23 :
:: deftheorem defines non-absorbing ABCMIZ_0:def 24 :
:: deftheorem defines subjected ABCMIZ_0:def 25 :
:: deftheorem defines non-absorbing ABCMIZ_0:def 26 :
:: deftheorem Def27 defines is_properly_applicable_to ABCMIZ_0:def 27 :
:: deftheorem Def28 defines is_properly_applicable_to ABCMIZ_0:def 28 :
theorem Th58:
theorem
theorem
theorem Th61:
theorem Th62:
:: deftheorem Def29 defines is_properly_applicable_to ABCMIZ_0:def 29 :
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 :
theorem Th66:
begin
:: deftheorem Def31 defines @--> ABCMIZ_0:def 31 :
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 :
theorem Th79:
theorem
theorem Th81:
theorem Th82:
theorem
theorem