Copyright (c) 2003 Association of Mizar Users
environ
vocabulary FINSET_1, RELAT_1, ORDERS_1, IDEAL_1, REWRITE1, LATTICES, WAYBEL_0,
FILTER_2, BOOLE, QUANTAL1, ORDINAL2, REALSET1, FUNCT_1, LATTICE3,
BINOP_1, OPOSET_1, AMI_1, FINSUB_1, PRELAMB, PRE_TOPC, YELLOW_1,
OPPCAT_1, BHSP_3, RELAT_2, FUNCOP_1, WELLORD2, MIDSP_3, YELLOW_0,
FINSEQ_1, FUNCT_7, ARYTM, CARD_1, FINSEQ_5, ABCMIZ_0, ARYTM_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, RELAT_2, SUBSET_1, RELSET_1,
ORDINAL1, FINSUB_1, CARD_1, FUNCT_1, FUNCT_2, BINOP_1, FINSET_1,
FINSEQ_1, FUNCT_4, ALG_1, BORSUK_1, FINSEQ_5, ORDINAL2, XCMPLX_0,
XREAL_0, NAT_1, STRUCT_0, PRE_TOPC, REALSET1, ORDERS_1, LATTICE3,
REWRITE1, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_7;
constructors FINSUB_1, BORSUK_1, ALG_1, FINSEQ_5, REALSET1, LATTICE3,
REWRITE1, YELLOW_2, INT_1, NAT_1, DOMAIN_1;
clusters XREAL_0, REWRITE1, SUBSET_1, FINSUB_1, FINSET_1, NAT_1, BINARITH,
RELAT_1, STRUCT_0, RELSET_1, FINSEQ_5, LATTICE3, YELLOW_0, WAYBEL_0,
YELLOW_1, YELLOW_7, YELLOW_9, FINSEQ_1;
requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
definitions TARSKI, XBOOLE_0, RELAT_2, REALSET1, FUNCT_1, FINSEQ_1, LATTICE3,
REWRITE1, YELLOW_0, WAYBEL_0, LATTICE8;
theorems TARSKI, XBOOLE_0, XBOOLE_1, SUBSET_1, FINSUB_1, TEX_2, NAT_1,
FINSEQ_1, FINSET_1, CARD_1, CARD_2, TRIANG_1, TREES_1, FINSEQ_5,
FINSEQ_6, RELAT_1, RELSET_1, FUNCT_1, FUNCT_2, FUNCT_4, REALSET1,
FUNCOP_1, REAL_1, STRUCT_0, ORDERS_1, LATTICE3, YELLOW_0, WAYBEL_0,
YELLOW_1, AXIOMS, YELLOW_4, YELLOW_7, WAYBEL_6, WAYBEL_8, ZFMISC_1,
FINSEQ_2, FINSEQ_3, HILBERT2, T_0TOPSP, REWRITE1, XCMPLX_1, BINARITH,
ORDINAL2;
schemes XBOOLE_0, NAT_1, FUNCT_1, FUNCT_2, RECDEF_1, RELSET_1, BINARITH,
ORDERS_2, COMPTS_1;
begin :: Semilattice of type widening
definition
cluster trivial reflexive -> complete (non empty RelStr);
coherence
proof
let R be non empty RelStr;
assume
A1: for x,y being Element of R holds x = y;
assume
A2: for x being Element of R holds x <= x;
let X be set; consider a being Element of R;
take a; thus X is_<=_than a
proof
let b be Element of R; a = b by A1;
hence thesis by A2;
end;
let b be Element of R; a = b by A1;
hence thesis by A2;
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:
the InternalRel of T is co-well_founded;
end;
definition
cluster trivial -> Noetherian (non empty RelStr);
coherence
proof
let S be non empty RelStr;
assume
A1: for x,y being Element of S holds x = y;
set R = the InternalRel of S;
let Y be set; assume
A2: Y c= field R;
assume Y <> {}; then
reconsider X = Y as non empty set;
consider a being Element of X;
take a;
thus
A3: a in Y;
let b be set; assume b in Y; then
a in field R & b in field R &
field R c= (the carrier of S) \/ the carrier of S
by A2,A3,RELSET_1:19;
hence thesis by A1;
end;
end;
definition
let T be non empty RelStr;
redefine attr T is Noetherian means:Def2:
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 set R = the InternalRel of T;
thus T is Noetherian implies
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 assume
A1: for Y being set st Y c= field R & Y <> {}
ex a being set st a in Y &
for b being set st b in Y & a <> b holds not [a,b] in R;
let A be non empty Subset of T;
consider a being Element of A;
reconsider a as Element of T;
set Y = A /\ field R;
per cases;
suppose
A2: A misses field R;
take a; thus a in A;
let b be Element of T; assume b in A & a < b; then
a <= b by ORDERS_1:def 10; then
[a,b] in R by ORDERS_1:def 9; then
a in field R by RELAT_1:30;
hence contradiction by A2,XBOOLE_0:3;
suppose A meets field R; then
Y c= field R & Y <> {} by XBOOLE_0:def 7,XBOOLE_1:17; then
consider x being set such that
A3: x in Y and
A4: for y being set st y in Y & x <> y holds not [x,y] in R by A1;
x in A by A3,XBOOLE_0:def 3; then
reconsider x as Element of T;
take x; thus x in A by A3,XBOOLE_0:def 3;
let b be Element of T; assume
A5: b in A & x < b; then
x <= b & x <> b by ORDERS_1:def 10; then
A6: [x,b] in R by ORDERS_1:def 9; then
b in field R by RELAT_1:30; then
b in Y by A5,XBOOLE_0:def 3;
hence contradiction by A4,A5,A6;
end;
assume
A7: 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;
let Y be set;
assume
A8:Y c= field R & Y <> {};
field R c= (the carrier of T) \/ the carrier of T by RELSET_1:19; then
Y c= the carrier of T by A8,XBOOLE_1:1; then
reconsider A = Y as non empty Subset of T by A8;
consider a being Element of T such that
A9:a in A and
A10:for b being Element of T st b in A holds not a < b by A7;
take a; thus a in Y by A9;
let b be set; assume
A11:b in Y & a <> b; then b in A; then
reconsider b as Element of T;
not a < b by A10,A11; then
not a <= b by A11,ORDERS_1:def 10;
hence thesis by ORDERS_1:def 9;
end;
end;
definition
let T be Poset;
attr T is Mizar-widening-like means
T is sup-Semilattice &
T is Noetherian;
end;
definition
cluster Mizar-widening-like -> Noetherian with_suprema upper-bounded Poset;
coherence
proof let T be Poset; assume
A1: T is sup-Semilattice & T is Noetherian;
hence T is Noetherian with_suprema;
reconsider S = T as sup-Semilattice by A1;
the carrier of S c= the carrier of S; then
the carrier of S is non empty Subset of S; then
consider a being Element of T such that a in the carrier of T and
A2: for b being Element of T st b in the carrier of T holds not a < b
by A1,Def2;
take a; let b be Element of T;
a"\/"b in the carrier of S; then
a"\/"b >= a & not a < a"\/"b by A2,YELLOW_0:22; then
a"\/"b = a by ORDERS_1:def 10;
hence thesis by A1,YELLOW_0:22;
end;
end;
definition
cluster Noetherian -> Mizar-widening-like sup-Semilattice;
coherence
proof let T be sup-Semilattice such that
A1: T is Noetherian;
thus T is sup-Semilattice;
thus thesis by A1;
end;
end;
definition
cluster Mizar-widening-like (complete sup-Semilattice);
existence
proof
consider T being trivial LATTICE;
take T; thus T is sup-Semilattice;
thus thesis;
end;
end;
definition
let T be Noetherian RelStr;
cluster the InternalRel of T -> co-well_founded;
coherence by Def1;
end;
theorem Th1:
for T being Noetherian sup-Semilattice
for I being Ideal of T holds ex_sup_of I, T & sup I in I
proof
let T be Noetherian sup-Semilattice;
let I be Ideal of T;
consider a being Element of T such that
A1: a in I and
A2: for b being Element of T st b in I holds not a < b by Def2;
A3: I is_<=_than a
proof
let d be Element of T; assume
A4: d in I;
a"\/"d in I by A1,A4,WAYBEL_0:40; then
a <= a"\/"d & not a < a"\/"d by A2,YELLOW_0:22; then
a = a"\/"d by ORDERS_1:def 10;
hence thesis by YELLOW_0:22;
end;
for c being Element of T st I is_<=_than c holds a <= c
by A1,LATTICE3:def 9;
hence thesis by A1,A3,YELLOW_0:30;
end;
begin :: Adjectives
definition
struct AdjectiveStr (#
adjectives -> set,
non-op -> UnOp of the adjectives
#);
end;
definition
let A be AdjectiveStr;
attr A is void means:Def4:
the adjectives of A is empty;
mode adjective of A is Element of the adjectives of A;
end;
theorem
for A1,A2 being AdjectiveStr
st the adjectives of A1 = the adjectives of A2
holds A1 is void implies A2 is void
proof let A1,A2 be AdjectiveStr such that
A1: the adjectives of A1 = the adjectives of A2;
assume the adjectives of A1 is empty;
hence the adjectives of A2 is empty by A1;
end;
definition
let A be AdjectiveStr;
let a be Element of the adjectives of A;
func non-a -> adjective of A equals:Def6:
(the non-op of A).a;
coherence
proof
per cases;
suppose the adjectives of A is empty; then
a = {} & not a in the adjectives of A &
dom the non-op of A = the adjectives of A
by FUNCT_2:67,SUBSET_1:def 2;
hence thesis by FUNCT_1:def 4;
suppose the adjectives of A is non empty; then
(the non-op of A).a in the adjectives of A by FUNCT_2:7;
hence thesis;
end;
end;
theorem Th3:
for A1,A2 being AdjectiveStr
st the AdjectiveStr of A1 = the AdjectiveStr of A2
for a1 being adjective of A1, a2 being adjective of A2
st a1 = a2
holds non-a1 = non-a2
proof let A1,A2 be AdjectiveStr such that
A1: the AdjectiveStr of A1 = the AdjectiveStr of A2;
let a1 be adjective of A1, a2 be adjective of A2;
assume a1 = a2;
hence non-a1 = (the non-op of A1).a2 by Def6 .= non-a2 by A1,Def6;
end;
definition
let A be AdjectiveStr;
attr A is involutive means:Def7:
for a being adjective of A holds non-non-a = a;
attr A is without_fixpoints means
not ex a being adjective of A st non-a = a;
end;
theorem Th4:
for a1,a2 being set st a1 <> a2
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 A is non void involutive without_fixpoints
proof
let a1,a2 be set such that
A1: a1 <> a2;
let A be AdjectiveStr such that
A2: the adjectives of A = {a1,a2} and
A3: (the non-op of A).a1 = a2 and
A4: (the non-op of A).a2 = a1;
thus the adjectives of A is non empty by A2;
hereby
let a be adjective of A;
A5: a = a1 or a = a2 by A2,TARSKI:def 2;
thus non-non-a = (the non-op of A).non-a by Def6
.= a by A3,A4,A5,Def6;
end;
let a be adjective of A;
A6: a = a1 or a = a2 by A2,TARSKI:def 2;
assume non-a = a;
hence thesis by A1,A3,A4,A6,Def6;
end;
theorem Th5:
for A1,A2 being AdjectiveStr
st the AdjectiveStr of A1 = the AdjectiveStr of A2
holds A1 is involutive implies A2 is involutive
proof let A1,A2 be AdjectiveStr such that
A1: the AdjectiveStr of A1 = the AdjectiveStr of A2;
assume
A2: for a being adjective of A1 holds non-non-a = a;
let a be adjective of A2;
reconsider b = a as adjective of A1 by A1;
non-a = non-b by A1,Th3;
hence non-non-a = non-non-b by A1,Th3 .= a by A2;
end;
theorem Th6:
for A1,A2 being AdjectiveStr
st the AdjectiveStr of A1 = the AdjectiveStr of A2
holds A1 is without_fixpoints implies A2 is without_fixpoints
proof let A1,A2 be AdjectiveStr such that
A1: the AdjectiveStr of A1 = the AdjectiveStr of A2;
assume
A2: not ex a being adjective of A1 st non-a = a;
given a being adjective of A2 such that
A3: non-a = a;
reconsider b = a as adjective of A1 by A1;
non-b = b by A1,A3,Th3;
hence contradiction by A2;
end;
definition
cluster non void involutive without_fixpoints (strict AdjectiveStr);
existence
proof
reconsider x = 0, y = 1 as Element of {0,1} by TARSKI:def 2;
reconsider n = (0,1)-->(y,x) as UnOp of {0,1};
take AdjectiveStr(#{0,1}, n#);
0 <> 1 & n.x = y & n.y = x by FUNCT_4:66;
hence thesis by Th4;
end;
end;
definition
let A be non void AdjectiveStr;
cluster the adjectives of A -> non empty;
coherence by Def4;
end;
definition
struct(RelStr,AdjectiveStr) TA-structure(#
carrier, adjectives -> set,
InternalRel -> (Relation of the carrier),
non-op -> UnOp of the adjectives,
adj-map -> Function of the carrier, Fin the adjectives
#);
end;
definition
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;
definition
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;
definition
cluster trivial reflexive non empty non void involutive without_fixpoints
strict TA-structure;
existence
proof
consider R being trivial reflexive non empty RelStr,
A being non void involutive without_fixpoints AdjectiveStr,
f being Function of the carrier of R, Fin the adjectives of A;
take T = TA-structure(#
the carrier of R, the adjectives of A,
the InternalRel of R, the non-op of A,
f
#);
thus T is trivial by TEX_2:4;
the RelStr of R = the RelStr of T;
hence T is reflexive by WAYBEL_8:12;
thus T is non empty non void;
the AdjectiveStr of A = the AdjectiveStr of T;
hence T is involutive without_fixpoints by Th5,Th6;
thus thesis;
end;
end;
definition
let T be TA-structure;
let t be Element of T;
func adjs t -> Subset of the adjectives of T equals:Def9:
(the adj-map of T).t;
coherence
proof
per cases;
suppose the carrier of T is empty; then
t = {} & not t in the carrier of T &
dom the adj-map of T = the carrier of T
by FUNCT_2:def 1,SUBSET_1:def 2; then
(the adj-map of T).t = {} the adjectives of T by FUNCT_1:def 4;
hence thesis;
suppose the carrier of T is non empty; then
(the adj-map of T).t in Fin the adjectives of T by FUNCT_2:7;
hence thesis by FINSUB_1:32;
end;
end;
theorem Th7:
for T1,T2 being TA-structure
st the TA-structure of T1 = the TA-structure of T2
for t1 being type of T1, t2 being type of T2
st t1 = t2
holds adjs t1 = adjs t2
proof
let T1,T2 be TA-structure such that
A1: the TA-structure of T1 = the TA-structure of T2;
let t1 be type of T1, t2 be type of T2;
adjs t1 = (the adj-map of T1).t1 & adjs t2 = (the adj-map of T2).t2
by Def9;
hence thesis by A1;
end;
definition
let T be TA-structure;
attr T is consistent means:Def10:
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;
theorem Th8:
for T1,T2 being TA-structure
st the TA-structure of T1 = the TA-structure of T2
holds T1 is consistent implies T2 is consistent
proof
let T1,T2 be TA-structure such that
A1: the TA-structure of T1 = the TA-structure of T2 and
A2: for t being type of T1
for a being adjective of T1 st a in adjs t
holds not non-a in adjs t;
let t2 be type of T2, a2 be adjective of T2;
reconsider t1 = t2 as type of T1 by A1;
reconsider a1 = a2 as adjective of T1 by A1;
assume a2 in adjs t2; then
a1 in adjs t1 by A1,Th7; then
not non-a1 in adjs t1 by A2; then
the AdjectiveStr of T1 = the AdjectiveStr of T2 & not non-a1 in adjs t2
by A1,Th7;
hence thesis by Th3;
end;
definition
let T be non empty TA-structure;
attr T is adj-structured means
the adj-map of T is
join-preserving map of T, (BoolePoset the adjectives of T) opp;
end;
theorem Th9:
for T1,T2 being non empty TA-structure
st the TA-structure of T1 = the TA-structure of T2
holds T1 is adj-structured implies T2 is adj-structured
proof
let T1,T2 be non empty TA-structure such that
A1: the TA-structure of T1 = the TA-structure of T2;
assume
the adj-map of T1 is
join-preserving map of T1, (BoolePoset the adjectives of T1) opp; then
reconsider f = the adj-map of T1 as
join-preserving map of T1, (BoolePoset the adjectives of T1) opp;
reconsider g = f as map of T2, (BoolePoset the adjectives of T2) opp by A1;
A2: the RelStr of T1 = the RelStr of T2 & the RelStr of (BoolePoset the
adjectives of T1) opp = the RelStr of (BoolePoset the adjectives of T2) opp
by A1;
g is join-preserving
proof let x,y be type of T2;
reconsider x' = x, y' = y as type of T1 by A1;
assume
A3: ex_sup_of {x,y}, T2; then
A4: ex_sup_of {x',y'}, T1 & f preserves_sup_of {x',y'}
by A2,WAYBEL_0:def 35,YELLOW_0:14; then
A5: ex_sup_of f.:{x',y'}, (BoolePoset the adjectives of T1) opp &
sup (f.:{x',y'}) = f.sup {x',y'} by WAYBEL_0:def 31;
thus ex_sup_of g.:{x,y}, (BoolePoset the adjectives of T2) opp
by A1,A4,WAYBEL_0:def 31;
thus sup (g.:{x,y}) = g.sup {x,y} by A2,A3,A5,YELLOW_0:26;
end;
hence the adj-map of T2 is
join-preserving map of T2, (BoolePoset the adjectives of T2) opp by A1;
end;
definition
let T be reflexive transitive antisymmetric with_suprema TA-structure;
redefine attr T is adj-structured means:Def12:
for t1,t2 being type of T holds adjs(t1"\/"t2) = (adjs t1) /\ (adjs t2);
compatibility
proof
thus T is adj-structured implies
for t1,t2 being type of T holds adjs(t1"\/"t2) = (adjs t1) /\ (adjs t2)
proof assume the adj-map of T is
join-preserving map of T, (BoolePoset the adjectives of T) opp; then
reconsider f = the adj-map of T as
join-preserving map of T, (BoolePoset the adjectives of T) opp;
let t1,t2 be type of T;
thus adjs(t1"\/"t2) = f.(t1"\/"t2) by Def9
.= (f.t1) "\/" (f.t2) by WAYBEL_6:2
.= (~(f.t1)) "/\" (~(f.t2)) by YELLOW_7:22
.= (~(f.t1)) /\ (~(f.t2)) by YELLOW_1:17
.= (f.t1) /\ (~(f.t2)) by LATTICE3:def 7
.= (f.t1) /\ (f.t2) by LATTICE3:def 7
.= (adjs t1) /\ (f.t2) by Def9
.= (adjs t1) /\ (adjs t2) by Def9;
end;
assume
A1: for t1,t2 being type of T holds adjs(t1"\/"t2) = (adjs t1) /\ (adjs t2);
BoolePoset the adjectives of T = InclPoset bool the adjectives of T
by YELLOW_1:4
.= RelStr(#bool the adjectives of T, RelIncl bool the adjectives of T#)
by YELLOW_1:def 1; then
A2: (BoolePoset the adjectives of T) opp = RelStr(#bool the adjectives of T,
(RelIncl bool the adjectives of T)~#) by LATTICE3:def 5;
rng the adj-map of T c= Fin the adjectives of T & Fin the adjectives of T
c= bool the adjectives of T by FINSUB_1:26,RELSET_1:12; then
rng the adj-map of T c= the carrier of (BoolePoset the adjectives of T) opp
& dom the adj-map of T = the carrier of T
by A2,FUNCT_2:def 1,XBOOLE_1:1; then
the adj-map of T is Function of the carrier of T, the carrier of
(BoolePoset the adjectives of T) opp by FUNCT_2:4; then
reconsider f = the adj-map of T as map of T,
(BoolePoset the adjectives of T) opp;
now let t1,t2 be type of T;
thus f.(t1"\/"t2)
= adjs(t1"\/"t2) by Def9
.= (adjs t1)/\(adjs t2) by A1
.= (f.t1)/\(adjs t2) by Def9
.= (f.t1)/\(f.t2) by Def9
.= (~(f.t1))/\(f.t2) by LATTICE3:def 7
.= (~(f.t1))/\(~(f.t2)) by LATTICE3:def 7
.= (~(f.t1))"/\"(~(f.t2)) by YELLOW_1:17
.= f.t1 "\/" f.t2 by YELLOW_7:22;
end;
hence the adj-map of T is join-preserving
map of T, (BoolePoset the adjectives of T) opp by WAYBEL_6:2;
end;
end;
theorem Th10:
for T being reflexive transitive antisymmetric with_suprema
TA-structure
st T is adj-structured
for t1,t2 being type of T st t1 <= t2 holds adjs t2 c= adjs t1
proof let T be reflexive transitive antisymmetric with_suprema
TA-structure such that
A1: for t1,t2 being type of T holds adjs(t1"\/"t2) = (adjs t1) /\ (adjs t2);
let t1,t2 be type of T; assume t1 <= t2; then
t1"\/"t2 = t2 by YELLOW_0:24; then
adjs t2 = (adjs t1)/\(adjs t2) by A1;
hence adjs t2 c= adjs t1 by XBOOLE_1:17;
end;
definition
let T be TA-structure;
let a be Element of the adjectives of T;
func types a -> Subset of T means:Def13:
for x being set holds
x in it iff ex t being type of T st x = t & a in adjs t;
existence
proof
defpred _P[set] means ex t being type of T st $1 = t & a in adjs t;
consider tt being set such that
A1: for x being set holds x in tt iff
x in the carrier of T & _P[x] from Separation;
tt c= the carrier of T proof let x be set; thus thesis by A1; end; then
reconsider tt as Subset of T;
take tt; let x be set;
thus x in tt implies ex t being type of T st x = t & a in adjs t by A1;
given t being type of T such that
A2: x = t & a in adjs t;
now
assume not x in the carrier of T; then
the carrier of T is empty & dom the adj-map of T = the carrier of T
by A2,FUNCT_2:def 1; then
(the adj-map of T).t = {} by FUNCT_1:def 4;
hence contradiction by A2,Def9;
end;
hence thesis by A1,A2;
end;
uniqueness
proof
defpred _P[set] means ex t being type of T st $1 = t & a in adjs t;
let X1,X2 be Subset of T such that
A3: for x being set holds x in X1 iff _P[x] and
A4: for x being set holds x in X2 iff _P[x];
thus thesis from Extensionality(A3,A4);
end;
end;
definition
let T be non empty TA-structure;
let A be Subset of the adjectives of T;
func types A -> Subset of T means:Def14:
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
defpred _P[set] means
for a being adjective of T st a in A holds $1 in types a;
consider tt being set such that
A1: for x being set holds x in tt iff x in the carrier of T & _P[x]
from Separation;
tt c= the carrier of T proof let x be set; thus thesis by A1; end; then
reconsider tt as Subset of T;
take tt;
thus thesis by A1;
end;
uniqueness
proof let X1,X2 be Subset of T such that
A2: for t being type of T holds
t in X1 iff for a being adjective of T st a in A holds t in types a and
A3: for t being type of T holds
t in X2 iff for a being adjective of T st a in A holds t in types a;
now
let x be set;
x in X1 iff x is type of T &
for a being adjective of T st a in A holds x in types a by A2;
hence x in X1 iff x in X2 by A3;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th11:
for T1,T2 being TA-structure
st the TA-structure of T1 = the TA-structure of T2
for a1 being adjective of T1, a2 being adjective of T2 st a1 = a2
holds types a1 = types a2
proof
let T1,T2 be TA-structure such that
A1: the TA-structure of T1 = the TA-structure of T2;
let a1 be adjective of T1, a2 be adjective of T2 such that
A2: a1 = a2;
now
thus types a1 is Subset of T2 by A1;
let x be set;
hereby assume x in types a1; then
consider t1 being type of T1 such that
A3: x = t1 & a1 in adjs t1 by Def13;
reconsider t2 = t1 as type of T2 by A1;
adjs t1 = adjs t2 by A1,Th7;
hence ex t2 being type of T2 st x = t2 & a2 in adjs t2 by A2,A3;
end;
given t2 being type of T2 such that
A4: x = t2 & a2 in adjs t2;
reconsider t1 = t2 as type of T1 by A1;
adjs t1 = adjs t2 by A1,Th7;
hence x in types a1 by A2,A4,Def13;
end;
hence thesis by Def13;
end;
theorem
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
let T be non empty TA-structure;
let a be adjective of T;
set X = {t where t is type of T: a in adjs t};
X c= the carrier of T
proof let x be set; assume x in X; then
ex t being type of T st x = t & a in adjs t;
hence thesis;
end; then
reconsider X as Subset of T;
for x being set holds
x in X iff ex t being type of T st x = t & a in adjs t;
hence thesis by Def13;
end;
theorem Th13:
for T being TA-structure
for t being type of T, a being adjective of T
holds a in adjs t iff t in types a
proof
let T be TA-structure;
let t be type of T, a be adjective of T;
thus a in adjs t implies t in types a by Def13;
assume t in types a; then
ex t' being type of T st t = t' & a in adjs t' by Def13;
hence thesis;
end;
theorem Th14:
for T being non empty TA-structure
for t being type of T, A being Subset of the adjectives of T
holds A c= adjs t iff t in types A
proof
let T be non empty TA-structure;
let t be type of T, a be Subset of the adjectives of T;
hereby assume
a c= adjs t; then
for b being adjective of T st b in a holds t in types b by Th13;
hence t in types a by Def14;
end;
assume
A1: t in types a;
let x be set; assume
A2: x in a; then reconsider x as adjective of T;
t in types x by A1,A2,Def14;
hence thesis by Th13;
end;
theorem
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 let T be non void TA-structure;
let t be type of T;
set X = {a where a is adjective of T: t in types a};
thus adjs t c= X
proof
let x be set; assume
A1: x in adjs t; then
reconsider a = x as adjective of T;
t in types a by A1,Th13;
hence thesis;
end;
let x be set; assume x in X; then
ex a being adjective of T st x = a & t in types a;
hence thesis by Th13;
end;
theorem Th16:
for T being non empty TA-structure
for t being type of T
holds types ({} the adjectives of T) = the carrier of T
proof
let T be non empty TA-structure;
let t be type of T;
thus types ({} the adjectives of T) c= the carrier of T;
let x be set; assume x in the carrier of T; then
reconsider t = x as type of T;
for a being adjective of T st a in {} the adjectives of T
holds t in types a;
hence thesis by Def14;
end;
definition
let T be TA-structure;
attr T is adjs-typed means
for a being adjective of T holds types a \/ types non-a is non empty;
end;
theorem Th17:
for T1,T2 being TA-structure
st the TA-structure of T1 = the TA-structure of T2
holds T1 is adjs-typed implies T2 is adjs-typed
proof
let T1,T2 be TA-structure such that
A1: the TA-structure of T1 = the TA-structure of T2 and
A2: for a being adjective of T1 holds types a \/ types non-a is non empty;
let b be adjective of T2;
reconsider a = b as adjective of T1 by A1;
the AdjectiveStr of T1 = the AdjectiveStr of T2 by A1; then
non-a = non-b by Th3; then
types a = types b & types non-a = types non-b &
types a \/ types non-a is non empty by A1,A2,Th11;
hence thesis;
end;
definition
cluster non void Mizar-widening-like involutive without_fixpoints
consistent adj-structured adjs-typed
(complete upper-bounded non empty trivial
reflexive transitive antisymmetric strict TA-structure);
existence
proof
consider R being trivial reflexive non empty RelStr;
reconsider x = 0, y = 1 as Element of {0,1} by TARSKI:def 2;
reconsider n = (0,1)-->(y,x) as UnOp of {0,1};
{0} c= {0,1} by ZFMISC_1:12; then
reconsider A = {0} as Element of Fin {0,1} by FINSUB_1:def 5;
set f = (the carrier of R) --> A;
set T = TA-structure(#the carrier of R, {0,1},
the InternalRel of R, n, f#);
the RelStr of T = the RelStr of R; then
reconsider T as strict trivial reflexive non empty TA-structure
by TEX_2:4,WAYBEL_8:12;
take T; thus T is non void;
thus T is Mizar-widening-like;
A1: 0 <> 1 & n.x = y & n.y = x by FUNCT_4:66;
hence T is involutive without_fixpoints by Th4;
hereby
let t be type of T;
let a be adjective of T;
A2: (a = 0 or a = 1) & non-a = n.a by Def6,TARSKI:def 2;
adjs t = f.t by Def9 .= A by FUNCOP_1:13;
hence a in adjs t implies not non-a in adjs t by A1,A2,TARSKI:def 1;
end;
hereby
let t1,t2 be type of T;
adjs(t1"\/"t2) = f.(t1"\/"t2) & adjs t1 = f.t1 & adjs t2 = f.t2
by Def9; then
adjs(t1"\/"t2) = A & adjs t1 = A & adjs t2 = A by FUNCOP_1:13;
hence adjs(t1"\/"t2) = adjs t1 /\ adjs t2;
end;
let a be adjective of T;
A3: (a = 0 or a = 1) & non-a = n.a by Def6,TARSKI:def 2;
consider t being type of T;
adjs t = f.t by Def9 .= A by FUNCOP_1:13; then
a in adjs t or non-a in adjs t by A1,A3,TARSKI:def 1; then
t in types a or t in types non-a by Th13;
hence thesis by XBOOLE_0:def 2;
end;
end;
theorem
for T being consistent TA-structure
for a being adjective of T
holds types a misses types non-a
proof
let T be consistent TA-structure;
let a be adjective of T;
assume types a meets types non-a; then
consider x being set such that
A1: x in types a and
A2: x in types non-a by XBOOLE_0:3;
consider t1 being type of T such that
A3: x = t1 & a in adjs t1 by A1,Def13;
ex t2 being type of T st x = t2 & non-a in adjs t2 by A2,Def13;
hence thesis by A3,Def10;
end;
definition
let T be adj-structured (reflexive transitive antisymmetric with_suprema
TA-structure);
let a be adjective of T;
cluster types a -> lower directed;
coherence
proof
thus types a is lower
proof let x,y be Element of T;
assume x in types a & y <= x; then
a in adjs x & adjs x c= adjs y by Th10,Th13;
hence y in types a by Th13;
end;
let x,y be Element of T;
assume x in types a & y in types a; then
a in adjs x & a in adjs y by Th13; then
a in (adjs x)/\adjs y by XBOOLE_0:def 3; then
A1: a in adjs(x"\/"y) by Def12;
take x"\/"y;
thus thesis by A1,Th13,YELLOW_0:22;
end;
end;
definition
let T be adj-structured (reflexive transitive antisymmetric with_suprema
TA-structure);
let A be Subset of the adjectives of T;
cluster types A -> lower directed;
coherence
proof
thus types A is lower
proof let x,y be Element of T;
assume
A1: x in types A & y <= x;
now
let a be adjective of T; assume a in A; then
x in types a by A1,Def14; then
a in adjs x & adjs x c= adjs y by A1,Th10,Th13;
hence y in types a by Th13;
end;
hence thesis by Def14;
end;
let x,y be Element of T; assume
A2: x in types A & y in types A;
A3: now let a be adjective of T;
assume a in A; then
x in types a & y in types a by A2,Def14; then
a in adjs x & a in adjs y by Th13; then
a in (adjs x)/\adjs y by XBOOLE_0:def 3; then
a in adjs(x"\/"y) by Def12;
hence x"\/"y in types a by Th13;
end;
take x"\/"y;
thus thesis by A3,Def14,YELLOW_0:22;
end;
end;
theorem
for T being adj-structured (with_suprema reflexive antisymmetric transitive
TA-structure)
for a being adjective of T holds
types a is empty or types a is Ideal of T;
begin :: Applicability of adjectives
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:Def16:
ex t' being type of T st t' in types a & t' <= t;
end;
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:Def17:
ex t' being type of T st A c= adjs t' & t' <= t;
end;
theorem Th20:
for T being adj-structured (reflexive transitive antisymmetric with_suprema
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
let T be adj-structured (reflexive transitive antisymmetric with_suprema
TA-structure);
let a be adjective of T;
let t be type of T;
given t' being type of T such that
A1: t' in types a & t' <= t;
t' in downarrow t by A1,WAYBEL_0:17;
hence thesis by A1,WAYBEL_0:27,44,XBOOLE_0:def 3;
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:Def18:
sup(types a /\ downarrow t);
coherence;
end;
theorem Th21:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema 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
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema TA-structure);
let t be type of T;
let a be adjective of T;
assume a is_applicable_to t; then
types a /\ downarrow t is Ideal of T by Th20; then
sup (types a /\ downarrow t) in types a /\ downarrow t by Th1; then
a ast t in types a /\ downarrow t by Def18; then
a ast t in downarrow t by XBOOLE_0:def 3;
hence thesis by WAYBEL_0:17;
end;
theorem Th22:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema 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
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema TA-structure);
let t be type of T;
let a be adjective of T;
assume a is_applicable_to t; then
types a /\ downarrow t is Ideal of T by Th20; then
sup (types a /\ downarrow t) in types a /\ downarrow t by Th1; then
a ast t in types a /\ downarrow t by Def18; then
a ast t in types a by XBOOLE_0:def 3;
hence thesis by Th13;
end;
theorem Th23:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema 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
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema TA-structure);
let t be type of T;
let a be adjective of T;
assume a is_applicable_to t; then
types a /\ downarrow t is Ideal of T by Th20; then
sup (types a /\ downarrow t) in types a /\ downarrow t by Th1; then
a ast t in types a /\ downarrow t by Def18;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th24:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema 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
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema TA-structure);
let t be type of T;
let a be adjective of T;
let t' be type of T; assume
A1: t' <= t & a in adjs t'; then
A2: t' in downarrow t & t' in types a by Th13,WAYBEL_0:17;
thus a is_applicable_to t
proof
take t'; thus thesis by A1,Th13;
end; then
types a /\ downarrow t is Ideal of T by Th20; then
ex_sup_of types a /\ downarrow t, T &
a ast t = sup (types a /\ downarrow t) by Def18,Th1; then
a ast t is_>=_than types a /\ downarrow t & t' in types a /\ downarrow t
by A2,XBOOLE_0:def 3,YELLOW_0:30;
hence t' <= a ast t by LATTICE3:def 9;
end;
theorem Th25:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema 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
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema TA-structure);
let t be type of T;
let a be adjective of T; assume
A1: a in adjs t;
thus a is_applicable_to t by A1,Th24; then
t <= a ast t & a ast t <= t by A1,Th21,Th24;
hence thesis by YELLOW_0:def 3;
end;
theorem
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema 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
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema TA-structure);
let t be type of T;
let a,b be adjective of T such that
A1: a is_applicable_to t and
A2: b is_applicable_to a ast t;
A3: a ast t = sup (types a /\ downarrow t) & a ast t <= t & a ast t in types a
by A1,Def18,Th21,Th23;
A4: b ast (a ast t) = sup (types b /\ downarrow (a ast t)) by Def18;
consider t' being type of T such that
A5: t' in types b & t' <= a ast t by A2,Def16;
A6: t' <= t & b in adjs t' by A3,A5,Th13,YELLOW_0:def 2;
thus b is_applicable_to t
proof
take t'; thus thesis by A3,A5,YELLOW_0:def 2;
end; then
A7: b ast t = sup (types b /\ downarrow t) & b ast t <= t & b ast t in types b
by Def18,Th21,Th23;
thus
A8: a is_applicable_to b ast t
proof
take t';
a ast t in types a by A1,Th23;
hence t' in types a by A5,WAYBEL_0:def 19;
thus t' <= b ast t by A6,Th24;
end;
A9: a ast (b ast t) is_>=_than types b /\ downarrow (a ast t)
proof
let t' be type of T; assume t' in types b /\ downarrow (a ast t); then
t' in types b & t' in downarrow (a ast t) by XBOOLE_0:def 3; then
A10: b in adjs t' & t' <= a ast t by Th13,WAYBEL_0:17; then
t' <= t & t' in types a by A3,WAYBEL_0:def 19,YELLOW_0:def 2; then
t' <= b ast t & a in adjs t' by A10,Th13,Th24;
hence thesis by Th24;
end;
a ast (b ast t) <= b ast t by A8,Th21; then
a ast (b ast t) <= t & a in adjs (a ast (b ast t))
by A7,A8,Th22,YELLOW_0:def 2; then
a ast (b ast t) <= b ast t & a ast (b ast t) <= a ast t
by A8,Th21,Th24; then
a ast (b ast t) in types b & a ast (b ast t) in downarrow (a ast t)
by A7,WAYBEL_0:17,def 19; then
a ast (b ast t) in types b /\ downarrow (a ast t) by XBOOLE_0:def 3; then
for t' being type of T
st t' is_>=_than types b /\ downarrow (a ast t)
holds a ast (b ast t) <= t' by LATTICE3:def 9;
hence a ast (b ast t) = b ast (a ast t) by A4,A9,YELLOW_0:30;
end;
theorem Th27:
for T being adj-structured (reflexive transitive antisymmetric with_suprema
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
let T be adj-structured (reflexive transitive antisymmetric with_suprema
TA-structure);
let A be Subset of the adjectives of T;
let t be type of T;
given t' being type of T such that
A1: A c= adjs t' & t' <= t;
t' in downarrow t & t' in types A by A1,Th14,WAYBEL_0:17;
hence thesis by WAYBEL_0:27,44,XBOOLE_0:def 3;
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:Def19:
sup(types A /\ downarrow t);
coherence;
end;
theorem Th28:
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
let T be non empty reflexive transitive antisymmetric TA-structure;
let t be type of T;
set A = {} the adjectives of T;
types A = the carrier of T by Th16; then
types A /\ downarrow t = downarrow t by XBOOLE_1:28;
hence A ast t = sup downarrow t by Def19
.= t by WAYBEL_0:34;
end;
definition
let T be non empty non void reflexive transitive 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:Def20:
len it = len p+1 & it.1 = t &
for i being Nat, a being adjective of T, t being type of T
st i in dom p & a = p.i & t = it.i
holds it.(i+1) = a ast t;
existence
proof
defpred _P[set,set,set] means
ex a being adjective of T st
a = p.$1 & ($2 is not type of T & $3 = 0 or
ex t being type of T st t = $2 & $3 = a ast t);
A1: for i being Nat st 1 <= i & i < len p+1
for x being set
ex y being set st _P[i,x,y]
proof let i be Nat; assume
A2: 1 <= i;
assume i < len p+1; then
i <= len p by NAT_1:38; then
i in dom p by A2,FINSEQ_3:27; then
p.i in rng p & rng p c= the adjectives of T
by FINSEQ_1:def 4,FUNCT_1:12; then
reconsider a = p.i as adjective of T;
let x be set;
per cases; suppose
A3: x is not type of T; take 0, a; thus thesis by A3;
suppose x is type of T; then
reconsider t = x as type of T;
take a ast t, a; thus a = p.i;
thus thesis;
end;
A4: for n being Nat st 1 <= n & n < len p+1
for x,y1,y2 being set st _P[n,x,y1] & _P[n,x,y2]
holds y1 = y2;
consider q being FinSequence such that
A5: len q = len p+1 and
A6: q.1 = t or len p+1 = 0 and
A7: for i being Nat st 1 <= i & i < len p+1 holds _P[i,q.i,q.(i+1)]
from FinRecEx(A1,A4);
defpred _P[Nat] means $1 in dom q implies q.$1 is type of T;
A8: _P[0] by FINSEQ_3:26;
A9: now let k be Nat such that
A10: _P[k];
now assume
A11: k+1 in dom q;
(k <> 0 implies k > 0) & k+1 <= len q by A11,FINSEQ_3:27,NAT_1:19; then
A12: (k <> 0 implies k >= 0+1) & k < len q by NAT_1:38;
k <> 0 implies ex a being adjective of T st a = p.k &
(q.k is not type of T & q.(k+1) = 0
or ex t being type of T st t = q.k & q.(k+1) = a ast t) by A5,A7,A12;
hence q.(k+1) is type of T by A6,A10,A12,FINSEQ_3:27;
end;
hence _P[k+1];
end;
A13: for k being Nat holds _P[k] from Ind(A8,A9);
rng q c= the carrier of T
proof
let a be set; assume a in rng q; then
consider x being set such that
A14: x in dom q & a = q.x by FUNCT_1:def 5;
a is type of T by A13,A14;
hence a in the carrier of T;
end; then
reconsider q as FinSequence of the carrier of T by FINSEQ_1:def 4;
take q; thus len q = len p+1 & q.1 = t by A5,A6;
let i be Nat, a be adjective of T, t being type of T; assume
A15: i in dom p & a = p.i & t = q.i; then
i >= 1 & i <= len p by FINSEQ_3:27; then
i >= 1 & i < len p+1 by NAT_1:38; then
ex a being adjective of T st a = p.i & (q.i is not type of T & q.(i+1)=0 or
ex t being type of T st t = q.i & q.(i+1) = a ast t) by A7;
hence q.(i+1) = a ast t by A15;
end;
correctness
proof let q1, q2 be FinSequence of the carrier of T such that
A16: len q1 = len p+1 & q1.1 = t and
A17: for i being Nat, a being adjective of T, t being type of T
st i in dom p & a = p.i & t = q1.i
holds q1.(i+1) = a ast t and
A18: len q2 = len p+1 & q2.1 = t and
A19: for i being Nat, a being adjective of T, t being type of T
st i in dom p & a = p.i & t = q2.i
holds q2.(i+1) = a ast t;
A20: dom q1 = dom q2 by A16,A18,FINSEQ_3:31;
defpred _P[Nat] means $1 in dom q1 implies q1.$1 = q2.$1;
A21: _P[0] by FINSEQ_3:27;
A22: now let i be Nat such that
A23: _P[i];
now assume
A24: i+1 in dom q1;
i+1 <= len q1 & i <= i+1 by A24,FINSEQ_3:27,NAT_1:38; then
A25: i <= len p & i <= len q1 by A16,AXIOMS:22,REAL_1:53;
per cases by NAT_1:19; suppose i = 0;
hence q1.(i+1) = q2.(i+1) by A16,A18;
suppose i > 0; then
i >= 0+1 by NAT_1:38; then
A26: i in dom p & i in dom q1 by A25,FINSEQ_3:27; then
p.i in the adjectives of T by FINSEQ_2:13; then
reconsider a = p.i as adjective of T;
q1.i in the carrier of T by A26,FINSEQ_2:13; then
reconsider t = q1.i as type of T;
thus q1.(i+1) = a ast t by A17,A26
.= q2.(i+1) by A19,A23,A26;
end; hence _P[i+1];
end;
for i being Nat holds _P[i] from Ind(A21,A22);
hence thesis by A20,FINSEQ_1:17;
end;
end;
definition
let T be non empty non void reflexive transitive TA-structure;
let t be type of T;
let p be FinSequence of the adjectives of T;
cluster apply(p,t) -> non empty;
coherence
proof
len apply(p,t) = len p+1 by Def20;
hence thesis by FINSEQ_1:25;
end;
end;
theorem
for T being non empty non void reflexive transitive TA-structure
for t being type of T
holds apply(<*> the adjectives of T, t) = <*t*>
proof
let T be non empty non void reflexive transitive TA-structure;
let t be type of T;
len <*> the adjectives of T = 0 by FINSEQ_1:25; then
len apply(<*> the adjectives of T, t) = 0+1 &
apply(<*> the adjectives of T, t).1 = t by Def20;
hence thesis by FINSEQ_1:57;
end;
theorem Th30:
for T being non empty non void reflexive transitive TA-structure
for t being type of T, a be adjective of T
holds apply(<*a*>, t) = <*t, a ast t*>
proof
let T be non empty non void reflexive transitive TA-structure;
let t be type of T, a be adjective of T;
A1: len <*a*> = 1 by FINSEQ_1:57; then
A2: len apply(<*a*>, t) = 1+1 & apply(<*a*>, t).1 = t & <*a*>.1 = a &
1 in dom <*a*> by Def20,FINSEQ_1:57,FINSEQ_3:27; then
apply(<*a*>, t).(len <*a*>+1) = a ast t by A1,Def20;
hence thesis by A1,A2,FINSEQ_1:61;
end;
definition
let T be non empty non void reflexive transitive TA-structure;
let t be type of T;
let v be FinSequence of the adjectives of T;
func v ast t -> type of T equals:Def21:
apply(v,t).(len v+1);
coherence
proof
len v+1 >= 1 & len apply(v,t) = len v+1 by Def20,NAT_1:29; then
len v+1 in dom apply(v,t) by FINSEQ_3:27; then
apply(v,t).(len v+1) in the carrier of T by FINSEQ_2:13;
hence thesis;
end;
end;
theorem Th31:
for T being non empty non void reflexive transitive TA-structure
for t being type of T
holds (<*> the adjectives of T) ast t = t
proof
let T be non empty non void reflexive transitive TA-structure;
let t be type of T;
len <*> the adjectives of T = 0 by FINSEQ_1:25;
hence (<*> the adjectives of T) ast t
= apply(<*> the adjectives of T, t).(0+1) by Def21
.= t by Def20;
end;
theorem Th32:
for T being non empty non void reflexive transitive TA-structure
for t being type of T
for a being adjective of T
holds <*a*> ast t = a ast t
proof
let T be non empty non void reflexive transitive TA-structure;
let t be type of T;
let a be adjective of T;
apply(<*a*>, t) = <*t, a ast t*> & len <*a*> = 1 by Th30,FINSEQ_1:57; then
<*a*> ast t = <*t, a ast t*>.(1+1) by Def21;
hence thesis by FINSEQ_1:61;
end;
theorem
for p,q being FinSequence
for i being natural number st i >= 1 & i < len p holds (p$^q).i = p.i
proof
let p,q be FinSequence;
let i be natural number; assume
A1: i >= 1 & i < len p; then
len p > 0 by AXIOMS:22; then
A2: p <> {} by FINSEQ_1:25;
per cases;
suppose q = {}; hence thesis by REWRITE1:1;
suppose q <> {}; then
consider j being Nat, r being FinSequence such that
A3: len p = j+1 & r = p|Seg j & p$^q = r^q by A2,REWRITE1:def 1;
j < len p by A3,NAT_1:38; then
len r = j & i <= j & i is Nat
by A1,A3,FINSEQ_1:21,NAT_1:38,ORDINAL2:def 21; then
A4: i in dom r by A1,FINSEQ_3:27; then
(p$^q).i = r.i & p = r^<*p.len p*> by A3,FINSEQ_1:def 7,FINSEQ_3:61;
hence (p$^q).i = p.i by A4,FINSEQ_1:def 7;
end;
theorem Th34:
for p being non empty FinSequence, q being FinSequence
for i being natural number st i < len q holds (p$^q).(len p+i) = q.(i+1)
proof
let p be non empty FinSequence, q be FinSequence;
let i be natural number; assume
A1: i < len q; i >= 0 by NAT_1:18; then
q <> {} by A1,FINSEQ_1:25; then
consider j being Nat, r being FinSequence such that
A2: len p = j+1 & r = p|Seg j & p$^q = r^q by REWRITE1:def 1;
j < len p by A2,NAT_1:38; then
len r = j & i+1 >= 1 & i+1 <= len q & i+1 is Nat
by A1,A2,FINSEQ_1:21,NAT_1:29,38,ORDINAL2:def 21; then
len p+i =len r+(i+1) & i+1 in dom q by A2,FINSEQ_3:27,XCMPLX_1:1;
hence thesis by A2,FINSEQ_1:def 7;
end;
theorem Th35:
for T being non empty non void reflexive transitive 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)
proof
let T be non empty non void reflexive transitive TA-structure;
let t be type of T;
let v1,v2 be FinSequence of the adjectives of T;
A1: len apply(v1,t) = len v1+1 & len apply(v2, v1 ast t) = len v2+1
by Def20;
consider tt being FinSequence of the carrier of T,
q being Element of T such that
A2: apply(v1,t) = tt^<*q*> by HILBERT2:4;
A3: apply(v1, t) $^ apply(v2, v1 ast t) = tt^apply(v2, v1 ast t)
by A2,REWRITE1:2;
len <*q*> = 1 by FINSEQ_1:56; then
A4: len v1+1 = len tt+1 by A1,A2,FINSEQ_1:35; then
A5: len tt = len v1 by XCMPLX_1:2;
set s = apply(v1, t) $^ apply(v2, v1 ast t), p = v1^v2;
A6: len s = len tt+(len v2+1) by A1,A3,FINSEQ_1:35
.= len v1+len v2+1 by A5,XCMPLX_1:1
.= len p+1 by FINSEQ_1:35;
A7: s.1 = t
proof per cases by NAT_1:19;
suppose len v1 = 0; then
v1 = <*>the adjectives of T & tt = {} by A5,FINSEQ_1:25; then
s = apply(v2, v1 ast t) & v1 ast t = t by A3,Th31,FINSEQ_1:47;
hence thesis by Def20;
suppose len v1 > 0; then
len tt >= 0+1 & 0+1 = 1 & 1 <= 1 by A5,NAT_1:38; then
1 in dom tt by FINSEQ_3:27; then
s.1 = tt.1 & tt.1 = apply(v1, t).1 by A2,A3,FINSEQ_1:def 7;
hence thesis by Def20;
end;
now let i be Nat, a be adjective of T, t' be type of T such that
A8: i in dom p and
A9: a = p.i & t' = s.i;
A10: 1 <= i & i <= len p & len p = len v1+len v2
by A8,FINSEQ_1:35,FINSEQ_3:27;
A11: len apply(v2, v1 ast t) = len v2+1 by Def20;
per cases by AXIOMS:21;
suppose i < len v1; then
i+1 <= len v1 & i <= len v1 & i+1 >= 1 by NAT_1:29,38; then
A12: i in dom tt & i+1 in dom tt & i in dom v1 by A5,A10,FINSEQ_3:27; then
s.i = tt.i & tt.i = apply(v1, t).i & s.(i+1) = tt.(i+1) & p.i = v1.i &
tt.(i+1) = apply(v1, t).(i+1) by A2,A3,FINSEQ_1:def 7;
hence s.(i+1) = a ast t' by A9,A12,Def20;
suppose
A13: i = len v1;
1 <= len apply(v2, v1 ast t) by A11,NAT_1:29; then
A14: i in dom tt & i in dom v1 & 1 in dom apply(v2, v1 ast t)
by A5,A10,A13,FINSEQ_3:27; then
A15: s.i = tt.i & tt.i = apply(v1, t).i & s.(i+1) = apply(v2, v1 ast t).1 &
p.i = v1.i by A2,A3,A4,A13,FINSEQ_1:def 7; then
a ast t' = apply(v1, t).(i+1) by A9,A14,Def20 .= v1 ast t by A13,Def21;
hence s.(i+1) = a ast t' by A15,Def20;
suppose i > len v1; then
i >= len v1+1 by NAT_1:38; then
consider j being Nat such that
A16: i = len v1+1+j by NAT_1:28;
A17: i = j+1+len v1 & j+1+len v1+1 = j+1+1+len v1 by A16,XCMPLX_1:1; then
A18: 1+j >= 1 & 1+j <= len v2 & 0 <= 1 by A10,NAT_1:29,REAL_1:53; then
1+j+1 <= len v2+1 & 1+j+1 >= 1 & 1+j+0 <= len v2+1
by NAT_1:29,REAL_1:55; then
A19: j+1 in dom v2 & j+1 in dom apply(v2, v1 ast t) &
j+1+1 in dom apply(v2, v1 ast t) by A11,A18,FINSEQ_3:27; then
s.i = apply(v2, v1 ast t).(j+1) & p.i = v2.(j+1) &
s.(i+1) = apply(v2, v1 ast t).(j+1+1) by A3,A5,A17,FINSEQ_1:def 7;
hence s.(i+1) = a ast t' by A9,A19,Def20;
end;
hence thesis by A3,A6,A7,Def20;
end;
theorem Th36:
for T being non empty non void reflexive transitive TA-structure
for t being type of T
for v1,v2 being FinSequence of the adjectives of T
for i being natural number st i in dom v1
holds apply(v1^v2, t).i = apply(v1, t).i
proof
let T be non empty non void reflexive transitive TA-structure;
let t be type of T;
let v1,v2 be FinSequence of the adjectives of T; set v = v1^v2;
A1: len apply(v1,t) = len v1+1 & len apply(v2, v1 ast t) = len v2+1
by Def20;
consider tt being FinSequence of the carrier of T,
q being Element of T such that
A2: apply(v1,t) = tt^<*q*> by HILBERT2:4;
A3: apply(v,t) = apply(v1,t) $^ apply(v2, v1 ast t) by Th35
.= tt^apply(v2, v1 ast t) by A2,REWRITE1:2;
len <*q*> = 1 by FINSEQ_1:56; then
len v1+1 = len tt+1 by A1,A2,FINSEQ_1:35; then
A4: len v1 = len tt by XCMPLX_1:2;
let i be natural number; assume i in dom v1; then
i >= 1 & i <= len tt & i is Nat by A4,FINSEQ_3:27; then
i in dom tt by FINSEQ_3:27; then
apply(v,t).i = tt.i & tt.i = apply(v1,t).i by A2,A3,FINSEQ_1:def 7;
hence thesis;
end;
theorem Th37:
for T being non empty non void reflexive transitive 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
proof
let T be non empty non void reflexive transitive TA-structure;
let t be type of T;
let v1,v2 be FinSequence of the adjectives of T; set v = v1^v2;
A1: len apply(v1,t) = len v1+1 & len apply(v2, v1 ast t) = len v2+1
by Def20;
A2: apply(v,t) = apply(v1,t) $^ apply(v2, v1 ast t) by Th35;
0 < len apply(v2, v1 ast t) by A1,NAT_1:19; then
apply(v,t).(len v1+1+0) = apply(v2, v1 ast t).(0+1) by A1,A2,Th34;
hence thesis by Def20;
end;
theorem Th38:
for T being non empty non void reflexive transitive 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
proof
let T be non empty non void reflexive transitive TA-structure;
let t be type of T;
let v1,v2 be FinSequence of the adjectives of T; set v = v1^v2;
A1: len apply(v1,t) = len v1+1 & len apply(v2, v1 ast t) = len v2+1
by Def20;
consider tt being FinSequence of the carrier of T,
q being Element of T such that
A2: apply(v1,t) = tt^<*q*> by HILBERT2:4;
A3: apply(v,t) = apply(v1,t) $^ apply(v2, v1 ast t) by Th35
.= tt^apply(v2, v1 ast t) by A2,REWRITE1:2;
len apply(v2, v1 ast t) = len v2+1 & len v2+1 >= 1 by Def20,NAT_1:29; then
A4: len v2+1 in dom apply(v2, v1 ast t) by FINSEQ_3:27;
len <*q*> = 1 by FINSEQ_1:56; then
len v1+1 = len tt+1 by A1,A2,FINSEQ_1:35; then
A5: len v1 = len tt by XCMPLX_1:2;
thus v2 ast (v1 ast t) = apply(v2, v1 ast t).(len v2+1) by Def21
.= apply(v,t).(len tt+(len v2+1)) by A3,A4,FINSEQ_1:def 7
.= apply(v,t).(len v1+len v2+1) by A5,XCMPLX_1:1
.= apply(v,t).(len v+1) by FINSEQ_1:35
.= v ast t by Def21;
end;
definition
let T be non empty non void reflexive transitive TA-structure;
let t be type of T;
let v be FinSequence of the adjectives of T;
pred v is_applicable_to t means:Def22:
for i being natural number, a being adjective of T, s being type of T
st i in dom v & a = v.i & s = apply(v,t).i
holds a is_applicable_to s;
end;
theorem
for T being non empty non void reflexive transitive TA-structure
for t being type of T
holds <*> the adjectives of T is_applicable_to t
proof
let T be non empty non void reflexive transitive TA-structure;
let t be type of T;
let i be natural number;
thus thesis;
end;
theorem Th40:
for T being non empty non void reflexive transitive TA-structure
for t being type of T, a being adjective of T
holds a is_applicable_to t iff <*a*> is_applicable_to t
proof
let T be non empty non void reflexive transitive TA-structure;
let t be type of T;
let a be adjective of T; set v = <*a*>;
hereby assume
A1: a is_applicable_to t;
thus <*a*> is_applicable_to t
proof
let i be natural number, b be adjective of T, s be type of T;
assume i in dom v; then
i in Seg 1 by FINSEQ_1:55; then
i = 1 by FINSEQ_1:4,TARSKI:def 1; then
v.i = a & apply(v,t).i = t by Def20,FINSEQ_1:57;
hence thesis by A1;
end;
end;
assume
A2: for i being natural number, a' being adjective of T, s being type of T
st i in dom v & a' = v.i & s = apply(v,t).i
holds a' is_applicable_to s;
len v = 1 by FINSEQ_1:57; then
1 in dom v & v.1 = a & apply(v,t).1 = t by Def20,FINSEQ_1:57,FINSEQ_3:27;
hence a is_applicable_to t by A2;
end;
theorem Th41:
for T being non empty non void reflexive transitive 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
proof
let T be non empty non void reflexive transitive TA-structure;
let t be type of T;
let v1,v2 be FinSequence of the adjectives of T; set v = v1^v2;
assume
A1: for i being natural number, a being adjective of T, s being type of T
st i in dom v & a = v.i & s = apply(v,t).i
holds a is_applicable_to s;
hereby
let i be natural number, a be adjective of T, s be type of T such that
A2: i in dom v1 & a = v1.i & s = apply(v1,t).i;
dom v1 c= dom v by FINSEQ_1:39; then
i in dom v & a = v.i & s = apply(v,t).i by A2,Th36,FINSEQ_1:def 7;
hence a is_applicable_to s by A1;
end;
let i be natural number, a be adjective of T, s be type of T such that
A3: i in dom v2 & a = v2.i & s = apply(v2, v1 ast t).i;
A4: apply(v,t) = apply(v1,t)$^apply(v2, v1 ast t) by Th35;
i >= 1 by A3,FINSEQ_3:27; then
consider j being Nat such that
A5: i = 1+j by NAT_1:28;
i <= len v2 by A3,FINSEQ_3:27; then
len apply(v1,t) = len v1+1 & len apply(v2, v1 ast t) = len v2+1 &
j < len v2 by A5,Def20,NAT_1:38; then
len v1+i = len apply(v1,t)+j & j < len apply(v2, v1 ast t)
by A5,NAT_1:38,XCMPLX_1:1; then
len v1+i in dom v & a = v.(len v1+i) & s = apply(v,t).(len v1+i)
by A3,A4,A5,Th34,FINSEQ_1:41,def 7;
hence a is_applicable_to s by A1;
end;
theorem Th42:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TA-structure)
for t being type of T
for v being FinSequence of the adjectives of T
st v is_applicable_to t
for i1,i2 being natural number st 1 <= i1 & i1 <= i2 & i2 <= len v+1
for t1,t2 being type of T st t1 = apply(v,t).i1 & t2 = apply(v,t).i2
holds t2 <= t1
proof
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TA-structure);
let t be type of T;
let v be FinSequence of the adjectives of T such that
A1: for i being natural number, a being adjective of T, s being type of T
st i in dom v & a = v.i & s = apply(v,t).i
holds a is_applicable_to s;
let i1,i2 be natural number such that
A2: 1 <= i1 & i1 <= i2 & i2 <= len v+1;
A3: ex j being Nat st i2 = i1+j by A2,NAT_1:28;
A4: len apply(v,t) = len v+1 by Def20;
let s1,s2 be type of T;
defpred _P[Nat] means i1+$1 <= len apply(v,t) implies
for s being type of T st s = apply(v,t).(i1+$1) holds s <= s1;
assume
A5: s1 = apply(v,t).i1 & s2 = apply(v,t).i2; then
A6: _P[0];
A7: for i being Nat
st _P[i] holds _P[i+1]
proof let i be Nat such that
A8: _P[i] and
A9: i1+(i+1) <= len apply(v,t);
A10: i1 <= i1+i & i1+(i+1) = i1+i+1 by NAT_1:29,XCMPLX_1:1; then
A11: 1 <= i1+i & i1+i <= len v & i1+i is Nat
by A2,A4,A9,AXIOMS:22,ORDINAL2:def 21,REAL_1:53; then
A12: i1+i in dom v by FINSEQ_3:27; then
v.(i1+i) in rng v & rng v c= the adjectives of T
by FINSEQ_1:def 4,FUNCT_1:12; then
reconsider a = v.(i1+i) as adjective of T;
i1+i < len v+1 by A4,A9,A10,NAT_1:38; then
i1+i in dom apply(v,t) by A4,A11,FINSEQ_3:27; then
apply(v,t).(i1+i) in rng apply(v,t) & rng apply(v,t) c= the carrier of T
by FINSEQ_1:def 4,FUNCT_1:12; then
reconsider s = apply(v,t).(i1+i) as type of T;
A13: a is_applicable_to s by A1,A12;
A14: apply(v,t).(i1+i+1) = a ast s by A12,Def20;
s <= s1 & a ast s <= s by A8,A9,A10,A13,Th21,NAT_1:38;
hence thesis by A10,A14,YELLOW_0:def 2;
end;
for i being Nat holds _P[i] from Ind(A6,A7);
hence thesis by A2,A3,A4,A5;
end;
theorem Th43:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TA-structure)
for t being type of T
for v being FinSequence of the adjectives of T
st v is_applicable_to t
for s being type of T st s in rng apply(v, t)
holds v ast t <= s & s <= t
proof
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TA-structure);
let t be type of T;
let v be FinSequence of the adjectives of T such that
A1: v is_applicable_to t;
let s be type of T; assume s in rng apply(v,t); then
consider x being set such that
A2: x in dom apply(v,t) & s = apply(v,t).x by FUNCT_1:def 5;
reconsider x as Nat by A2;
A3: 1 <= 1 & x >= 1 & x <= len apply(v,t) & len v+1 <= len v+1
by A2,FINSEQ_3:27;
len apply(v,t) = len v+1 & apply(v,t).1 = t &
v ast t = apply(v,t).(len v+1) by Def20,Def21;
hence thesis by A1,A2,A3,Th42;
end;
theorem Th44:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void 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
proof
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TA-structure);
let t be type of T;
let v be FinSequence of the adjectives of T such that
A1: v is_applicable_to t;
len apply(v,t) = len v+1 & len v+1 >= 1 by Def20,NAT_1:29; then
len v+1 in dom apply(v, t) by FINSEQ_3:27; then
apply(v,t).(len v+1) in rng apply(v,t) by FUNCT_1:12; then
v ast t in rng apply(v,t) by Def21;
hence thesis by A1,Th43;
end;
theorem Th45:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void 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)
proof
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TA-structure);
let t be type of T;
let v be FinSequence of the adjectives of T such that
A1: v is_applicable_to t;
let a be set; assume
A2: a in rng v; then
consider x being set such that
A3: x in dom v & a = v.x by FUNCT_1:def 5;
reconsider x as Nat by A3;
rng v c= the adjectives of T by FINSEQ_1:def 4; then
reconsider a as adjective of T by A2;
A4: x >= 1 & x <= len v by A3,FINSEQ_3:27;
len apply(v,t) = len v+1 by Def20; then
x < len apply(v,t) & x+1 <= len apply(v,t) & x+1 >= 1
by A4,AXIOMS:24,NAT_1:38; then
x in dom apply(v,t) & x+1 in dom apply(v,t) by A4,FINSEQ_3:27; then
A5: apply(v,t).x in rng apply(v,t) & apply(v,t).(x+1) in rng apply(v,t) &
rng apply(v,t) c= the carrier of T
by FINSEQ_1:def 4,FUNCT_1:12; then
reconsider s = apply(v,t).x as type of T;
a is_applicable_to s by A1,A3,Def22; then
A6: a in adjs (a ast s) by Th22;
a ast s = apply(v,t).(x+1) by A3,Def20; then
a ast s >= v ast t by A1,A5,Th43; then
adjs (a ast s) c= adjs(v ast t) by Th10;
hence thesis by A6;
end;
theorem Th46:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TA-structure)
for t being type of T
for v being FinSequence of the adjectives of T
st v is_applicable_to t
for A being Subset of the adjectives of T st A = rng v
holds A is_applicable_to t
proof
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TA-structure);
let t be type of T;
let v be FinSequence of the adjectives of T;
assume v is_applicable_to t; then
v ast t <= t & rng v c= adjs (v ast t) by Th44,Th45;
hence thesis by Def17;
end;
theorem Th47:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void 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
for s being type of T st s in rng apply(v2,t)
holds v1 ast t <= s
proof
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TA-structure);
let t be type of T;
let v,v' be FinSequence of the adjectives of T such that
A1: v is_applicable_to t & rng v' c= rng v;
let s be type of T; assume
s in rng apply(v',t); then
consider x being set such that
A2: x in dom apply(v',t) & s = apply(v',t).x by FUNCT_1:def 5;
x in Seg len apply(v',t) by A2,FINSEQ_1:def 3; then
reconsider x as non empty Nat by BINARITH:5;
A3: x <= len apply(v',t) by A2,FINSEQ_3:27;
defpred _P[Nat] means
$1 <= len apply(v',t) implies
for s being type of T st s = apply(v',t).$1 holds v ast t <= s;
apply(v',t).1 = t by Def20; then
A4: _P[1] by A1,Th44;
A5: for i being non empty Nat st _P[i] holds _P[i+1]
proof let i be non empty Nat such that
A6: _P[i] and
A7: i+1 <= len apply(v',t);
A8: i > 0 & len apply(v',t) = len v'+1 by Def20,NAT_1:19; then
A9: 0+1 <= i & i <= len v' by A7,NAT_1:38,REAL_1:53; then
A10: i in dom v' by FINSEQ_3:27; then
A11: v'.i in rng v' & rng v' c= the adjectives of T
by FINSEQ_1:def 4,FUNCT_1:12; then
reconsider a = v'.i as adjective of T;
i < len v'+1 by A7,A8,NAT_1:38; then
i in dom apply(v',t) by A8,A9,FINSEQ_3:27; then
apply(v',t).i in rng apply(v',t) & rng apply(v',t) c= the carrier of T
by FINSEQ_1:def 4,FUNCT_1:12; then
reconsider s = apply(v',t).i as type of T;
A12: apply(v',t).(i+1) = a ast s by A10,Def20;
a in rng v & rng v c= adjs (v ast t) by A1,A11,Th45; then
v ast t <= s & a in adjs (v ast t) by A6,A7,NAT_1:38;
hence thesis by A12,Th24;
end;
for i being non empty Nat holds _P[i] from Ind_from_1(A4,A5);
hence thesis by A2,A3;
end;
theorem Th48:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema 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 v2^v1 is_applicable_to t
proof
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TA-structure);
let t be type of T;
let v1,v2 be FinSequence of the adjectives of T;
assume
A1: v1^v2 is_applicable_to t;
let i be natural number, a be adjective of T, s be type of T such that
A2: i in dom (v2^v1) & a = (v2^v1).i & s = apply(v2^v1,t).i;
A3: i >= 1 & i <= len (v2^v1) & i is Nat by A2,FINSEQ_3:27;
A4: rng (v1^v2) = rng v1 \/ rng v2 & rng (v2^v1) = rng v1 \/ rng v2
by FINSEQ_1:44;
i < len (v2^v1)+1 & len apply(v2^v1,t) = len (v2^v1)+1
by A3,Def20,NAT_1:38; then
i in dom apply(v2^v1,t) by A3,FINSEQ_3:27; then
s in rng apply(v2^v1,t) by A2,FUNCT_1:12; then
A5: (v1^v2) ast t <= s by A1,A4,Th47;
a in rng (v2^v1) & rng (v1^v2) c= adjs ((v1^v2) ast t)
by A1,A2,Th45,FUNCT_1:12;
hence thesis by A4,A5,Th24;
end;
theorem
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema 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^v2 ast t = v2^v1 ast t
proof
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TA-structure);
let t be type of T;
let v1,v2 be FinSequence of the adjectives of T;
assume
A1: v1^v2 is_applicable_to t; then
A2: v2^v1 is_applicable_to t by Th48;
A3: v1^v2 ast t = apply(v1^v2, t).(len (v1^v2)+1) &
v2^v1 ast t = apply(v2^v1, t).(len (v2^v1)+1) by Def21;
A4: len apply(v1^v2, t) = len (v1^v2)+1 &
len apply(v2^v1, t) = len (v2^v1)+1 by Def20;
A5: len (v1^v2) = len v1+len v2 & len (v2^v1) = len v1+len v2 by FINSEQ_1:35;
A6: rng (v1^v2) = rng v1 \/ rng v2 & rng (v2^v1) = rng v1 \/ rng v2
by FINSEQ_1:44;
len (v1^v2)+1 >= 1 by NAT_1:29; then
len (v1^v2)+1 in dom apply(v1^v2, t) & len (v1^v2)+1 in dom apply(v2^v1, t)
by A4,A5,FINSEQ_3:27; then
v1^v2 ast t in rng apply(v1^v2, t) & v2^v1 ast t in rng apply(v2^v1, t)
by A3,A5,FUNCT_1:12; then
v1^v2 ast t <= v2^v1 ast t & v2^v1 ast t <= v1^v2 ast t by A1,A2,A6,Th47;
hence thesis by YELLOW_0:def 3;
end;
theorem Th50:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema 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
proof
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema TA-structure);
let t be type of T;
let a be Subset of the adjectives of T;
assume a is_applicable_to t; then
types a /\ downarrow t is Ideal of T by Th27; then
sup (types a /\ downarrow t) in types a /\ downarrow t by Th1; then
a ast t in types a /\ downarrow t by Def19; then
a ast t in downarrow t by XBOOLE_0:def 3;
hence thesis by WAYBEL_0:17;
end;
theorem Th51:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema 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)
proof
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema TA-structure);
let t be type of T;
let a be Subset of the adjectives of T;
assume a is_applicable_to t; then
types a /\ downarrow t is Ideal of T by Th27; then
sup (types a /\ downarrow t) in types a /\ downarrow t by Th1; then
a ast t in types a /\ downarrow t by Def19; then
a ast t in types a by XBOOLE_0:def 3;
hence thesis by Th14;
end;
theorem
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema 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
proof
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema TA-structure);
let t be type of T;
let a be Subset of the adjectives of T;
assume a is_applicable_to t; then
types a /\ downarrow t is Ideal of T by Th27; then
sup (types a /\ downarrow t) in types a /\ downarrow t by Th1; then
a ast t in types a /\ downarrow t by Def19;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th53:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema TA-structure)
for t being type of T
for A being Subset of the adjectives of T
for t' being type of T st t' <= t & A c= adjs t'
holds A is_applicable_to t & t' <= A ast t
proof
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema TA-structure);
let t be type of T;
let a be Subset of the adjectives of T;
let t' be type of T; assume
A1: t' <= t & a c= adjs t'; then
A2: t' in downarrow t & t' in types a by Th14,WAYBEL_0:17;
thus a is_applicable_to t
proof
take t'; thus thesis by A1;
end; then
types a /\ downarrow t is Ideal of T by Th27; then
ex_sup_of types a /\ downarrow t, T &
a ast t = sup (types a /\ downarrow t) by Def19,Th1; then
a ast t is_>=_than types a /\ downarrow t & t' in types a /\ downarrow t
by A2,XBOOLE_0:def 3,YELLOW_0:30;
hence t' <= a ast t by LATTICE3:def 9;
end;
theorem
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema 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
proof
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema TA-structure);
let t be type of T;
let a be Subset of the adjectives of T; assume
A1: a c= adjs t;
thus a is_applicable_to t by A1,Th53; then
t <= a ast t & a ast t <= t by A1,Th50,Th53;
hence thesis by YELLOW_0:def 3;
end;
theorem Th55:
for T being TA-structure, 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
let T be TA-structure;
let t be type of T;
let A,B be Subset of the adjectives of T;
given t' being type of T such that
A1: A c= adjs t' & t' <= t;
assume
A2: B c= A;
take t';
thus thesis by A1,A2,XBOOLE_1:1;
end;
theorem Th56:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TA-structure)
for t being type of T, 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
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TA-structure);
let t be type of T, a be adjective of T;
let A,B be Subset of the adjectives of T such that
A1: B = A \/ {a} & B is_applicable_to t;
A2: A c= B & {a} c= B by A1,XBOOLE_1:7;
A3:A is_applicable_to t by A1,A2,Th55;
A4: types a /\ downarrow (A ast t) = types B /\ downarrow t
proof
thus types a /\ downarrow (A ast t) c= types B /\ downarrow t
proof
let x be set; assume
A5: x in types a /\ downarrow (A ast t); then
A6: x in types a & x in downarrow (A ast t) by XBOOLE_0:def 3;
reconsider t' = x as type of T by A5;
A7: t' <= A ast t & A ast t <= t & A c= adjs (A ast t)
by A3,A6,Th50,Th51,WAYBEL_0:17; then
t' <= t by YELLOW_0:def 2; then
A8: t' in downarrow t by WAYBEL_0:17;
a in adjs t' & adjs (A ast t) c= adjs t' by A6,A7,Th10,Th13; then
A c= adjs t' & {a} c= adjs t' by A7,XBOOLE_1:1,ZFMISC_1:37; then
B c= adjs t' by A1,XBOOLE_1:8; then
t' in types B by Th14;
hence thesis by A8,XBOOLE_0:def 3;
end;
let x be set; assume A9: x in types B /\ downarrow t; then
A10: x in types B & x in downarrow t by XBOOLE_0:def 3;
reconsider t' = x as type of T by A9;
A11: t' <= t & B c= adjs t' & a in B
by A2,A10,Th14,WAYBEL_0:17,ZFMISC_1:37; then
A c= adjs t' by A2,XBOOLE_1:1; then
t' <= A ast t & a in adjs t' by A11,Th53; then
t' in downarrow (A ast t) & t' in types a by Th13,WAYBEL_0:17;
hence thesis by XBOOLE_0:def 3;
end;
thus a ast (A ast t)
= sup(types B /\ downarrow t) by A4,Def18
.= B ast t by Def19;
end;
theorem Th57:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TA-structure)
for t being type of T
for v being FinSequence of the adjectives of T
st v is_applicable_to t
for A being Subset of the adjectives of T st A = rng v
holds v ast t = A ast t
proof
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TA-structure);
defpred P[Nat] means
for t being type of T, v being FinSequence of the adjectives of T
st $1 = len v & v is_applicable_to t
for A being Subset of the adjectives of T st A = rng v
holds v ast t = A ast t;
A1: P[0]
proof
let t be type of T;
let v be FinSequence of the adjectives of T;
assume 0 = len v; then
v = <*> the adjectives of T & rng {} = {} by FINSEQ_1:25; then
v ast t = t & rng v = {} the adjectives of T by Th31;
hence thesis by Th28;
end;
A2: now let n be Nat such that
A3: P[n];
now
let t be type of T, v be FinSequence of the adjectives of T such that
A4: n+1 = len v & v is_applicable_to t;
consider v1 being FinSequence of the adjectives of T,
a being Element of the adjectives of T such that
A5: v = v1^<*a*> by A4,FINSEQ_2:22;
reconsider a as adjective of T;
reconsider B = rng v1 as Subset of the adjectives of T
by FINSEQ_1:def 4;
len <*a*> = 1 by FINSEQ_1:57; then
len v = len v1+1 by A5,FINSEQ_1:35; then
len v1 = n & v1 is_applicable_to t & <*a*> is_applicable_to v1 ast t
by A4,A5,Th41,XCMPLX_1:2; then
A6: v1 ast t = B ast t & a is_applicable_to v1 ast t by A3,Th40;
let A be Subset of the adjectives of T;
assume
A7: A = rng v; then
A8: A = B \/ rng <*a*> by A5,FINSEQ_1:44 .= B \/ {a} by FINSEQ_1:55;
A9: A is_applicable_to t by A4,A7,Th46;
thus v ast t = <*a*> ast (v1 ast t) by A5,Th38
.= a ast (B ast t) by A6,Th32
.= A ast t by A8,A9,Th56;
end; hence P[n+1];
end;
A10: for n being Nat holds P[n] from Ind(A1,A2);
let t be type of T;
let v be FinSequence of the adjectives of T;
P[len v] by A10;
hence thesis;
end;
begin :: Subject function
definition
let T be non empty non void TA-structure;
func sub T -> Function of the adjectives of T, the carrier of T means:Def23:
for a being adjective of T holds it.a = sup(types a \/ types non-a);
existence
proof
deffunc F(Element of the adjectives of T) = sup(types $1 \/ types non-$1);
consider f being Function of the adjectives of T, the carrier of T such
that
A1: for a being Element of the adjectives of T holds f.a = F(a) from LambdaD;
take f;
thus thesis by A1;
end;
uniqueness
proof
let f1,f2 be Function of the adjectives of T, the carrier of T such that
A2: for a being adjective of T holds f1.a = sup(types a \/ types non-a) and
A3: for a being adjective of T holds f2.a = sup(types a \/ types non-a);
now let a be Element of the adjectives of T;
reconsider b = a as adjective of T;
thus f1.a = sup(types b \/ types non-b) by A2 .= f2.a by A3;
end;
hence thesis by FUNCT_2:113;
end;
end;
definition
struct(TA-structure) TAS-structure(#
carrier, adjectives -> set,
InternalRel -> (Relation of the carrier),
non-op -> UnOp of the adjectives,
adj-map -> Function of the carrier, Fin the adjectives,
sub-map -> Function of the adjectives, the carrier
#);
end;
definition
cluster non void reflexive trivial non empty strict TAS-structure;
existence
proof
consider P being non void reflexive trivial non empty TA-structure;
consider s being Function of the adjectives of P, the carrier of P;
take T = TAS-structure(#the carrier of P, the adjectives of P,
the InternalRel of P, the non-op of P, the adj-map of P, s#);
T is non empty & the RelStr of P = the RelStr of T by STRUCT_0:def 1;
hence thesis by Def4,TEX_2:4,WAYBEL_8:12;
end;
end;
definition
let T be non empty non void TAS-structure;
let a be adjective of T;
func sub a -> type of T equals:Def24:
(the sub-map of T).a;
coherence;
end;
definition
let T be non empty non void TAS-structure;
attr T is non-absorbing means
(the sub-map of T)*(the non-op of T) = the sub-map of T;
attr T is subjected means
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));
end;
definition
let T be non empty non void TAS-structure;
redefine attr T is non-absorbing means
for a being adjective of T holds sub non-a = sub a;
compatibility
proof
thus T is non-absorbing implies
for a being adjective of T holds sub non-a = sub a
proof assume
A1: (the sub-map of T)*(the non-op of T) = the sub-map of T;
let a be adjective of T;
thus sub non-a = (the sub-map of T).non-a by Def24
.= (the sub-map of T).((the non-op of T).a) by Def6
.= (the sub-map of T).a by A1,FUNCT_2:21
.= sub a by Def24;
end;
assume
A2: for a being adjective of T holds sub non-a = sub a;
now
let x be Element of the adjectives of T;
reconsider a = x as adjective of T;
thus ((the sub-map of T)*(the non-op of T)).x
= (the sub-map of T).((the non-op of T).a) by FUNCT_2:21
.= (the sub-map of T).non-a by Def6
.= sub non-a by Def24
.= sub a by A2
.= (the sub-map of T).x by Def24;
end;
hence (the sub-map of T)*(the non-op of T) = the sub-map of T
by FUNCT_2:113;
end;
end;
definition
let T be non empty non void TAS-structure;
let t be Element of T;
let a be adjective of T;
pred a is_properly_applicable_to t means:Def28:
t <= sub a & a is_applicable_to t;
end;
definition
let T be non empty non void reflexive transitive TAS-structure;
let t be type of T;
let v be FinSequence of the adjectives of T;
pred v is_properly_applicable_to t means:Def29:
for i being natural number, a being adjective of T, 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;
end;
theorem Th58:
for T being non empty non void reflexive transitive TAS-structure
for t being type of T, v being FinSequence of the adjectives of T
st v is_properly_applicable_to t
holds v is_applicable_to t
proof
let T be non empty non void reflexive transitive TAS-structure;
let t be type of T;
let v be FinSequence of the adjectives of T;
assume
A1: for i being natural number, a being adjective of T, 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;
let i be natural number, a be adjective of T, s be type of T such that
A2: i in dom v & a = v.i & s = apply(v, t).i;
a is_properly_applicable_to s by A1,A2;
hence thesis by Def28;
end;
theorem
for T being non empty non void reflexive transitive TAS-structure
for t being type of T
holds <*> the adjectives of T is_properly_applicable_to t
proof
let T be non empty non void reflexive transitive TAS-structure;
let t be type of T;
let i be natural number;
thus thesis;
end;
theorem
for T being non empty non void reflexive transitive TAS-structure
for t being type of T, a being adjective of T
holds a is_properly_applicable_to t iff <*a*> is_properly_applicable_to t
proof
let T be non empty non void reflexive transitive TAS-structure;
let t be type of T;
let a be adjective of T; set v = <*a*>;
hereby assume
A1: a is_properly_applicable_to t;
thus <*a*> is_properly_applicable_to t
proof
let i be natural number, b be adjective of T, s be type of T;
assume i in dom v; then
i in Seg 1 by FINSEQ_1:55; then
i = 1 by FINSEQ_1:4,TARSKI:def 1; then
v.i = a & apply(v,t).i = t by Def20,FINSEQ_1:57;
hence thesis by A1;
end;
end;
assume
A2: for i being natural number, a' being adjective of T, 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;
len v = 1 by FINSEQ_1:57; then
1 in dom v & v.1 = a & apply(v,t).1 = t by Def20,FINSEQ_1:57,FINSEQ_3:27;
hence a is_properly_applicable_to t by A2;
end;
theorem Th61:
for T being non empty non void reflexive transitive TAS-structure
for t being type of T, 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
let T be non empty non void reflexive transitive TAS-structure;
let t be type of T;
let v1,v2 be FinSequence of the adjectives of T; set v = v1^v2;
assume
A1: for i being natural number, a being adjective of T, 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;
hereby
let i be natural number, a be adjective of T, s be type of T such that
A2: i in dom v1 & a = v1.i & s = apply(v1,t).i;
dom v1 c= dom v by FINSEQ_1:39; then
i in dom v & a = v.i & s = apply(v,t).i by A2,Th36,FINSEQ_1:def 7;
hence a is_properly_applicable_to s by A1;
end;
let i be natural number, a be adjective of T, s be type of T such that
A3: i in dom v2 & a = v2.i & s = apply(v2, v1 ast t).i;
A4: apply(v,t) = apply(v1,t)$^apply(v2, v1 ast t) by Th35;
i >= 1 by A3,FINSEQ_3:27; then
consider j being Nat such that
A5: i = 1+j by NAT_1:28;
i <= len v2 by A3,FINSEQ_3:27; then
len apply(v1,t) = len v1+1 & len apply(v2, v1 ast t) = len v2+1 &
j < len v2 by A5,Def20,NAT_1:38; then
len v1+i = len apply(v1,t)+j & j < len apply(v2, v1 ast t)
by A5,NAT_1:38,XCMPLX_1:1; then
len v1+i in dom v & a = v.(len v1+i) & s = apply(v,t).(len v1+i)
by A3,A4,A5,Th34,FINSEQ_1:41,def 7;
hence a is_properly_applicable_to s by A1;
end;
theorem Th62:
for T being non empty non void reflexive transitive TAS-structure
for t being type of T, 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
let T be non empty non void reflexive transitive TAS-structure;
let t be type of T;
let v1,v2 be FinSequence of the adjectives of T; set v = v1^v2;
assume
A1: for i being natural number, a being adjective of T, s being type of T
st i in dom v1 & a = v1.i & s = apply(v1,t).i
holds a is_properly_applicable_to s;
assume
A2: for i being natural number, a being adjective of T, s being type of T
st i in dom v2 & a = v2.i & s = apply(v2, v1 ast t).i
holds a is_properly_applicable_to s;
let i be natural number, a be adjective of T, s be type of T such that
A3: i in dom v & a = v.i & s = apply(v, t).i;
A4: apply(v,t) = apply(v1,t)$^apply(v2, v1 ast t) by Th35;
A5: i >= 1 & i <= len v & i is Nat by A3,FINSEQ_3:27;
per cases;
suppose i <= len v1; then
A6: i in dom v1 by A5,FINSEQ_3:27; then
a = v1.i & s = apply(v1,t).i by A3,Th36,FINSEQ_1:def 7;
hence a is_properly_applicable_to s by A1,A6;
suppose i > len v1; then
i >= 1+len v1 by NAT_1:38; then
consider j being Nat such that
A7: i = len v1+1+j by NAT_1:28;
len v = len v1+len v2 & i = len v1+(j+1)
by A7,FINSEQ_1:35,XCMPLX_1:1; then
j+1 >= 1 & j+1 <= len v2 by A5,NAT_1:29,REAL_1:53; then
A8: len apply(v1,t) = len v1+1 & len apply(v2, v1 ast t) = len v2+1 &
j < len v2 & j+1 in dom v2 by Def20,FINSEQ_3:27,NAT_1:38; then
len v1+(j+1) = len apply(v1,t)+j & j < len apply(v2, v1 ast t)
by NAT_1:38,XCMPLX_1:1; then
a = v2.(1+j) & s = apply(v2,v1 ast t).(1+j)
by A3,A4,A7,A8,Th34,FINSEQ_1:def 7;
hence a is_properly_applicable_to s by A2,A8;
end;
definition
let T be non empty non void reflexive transitive TAS-structure;
let t be type of T;
let A be Subset of the adjectives of T;
pred A is_properly_applicable_to t means:Def30:
ex s being FinSequence of the adjectives of T st
rng s = A & s is_properly_applicable_to t;
end;
theorem Th63:
for T being non empty non void reflexive transitive TAS-structure
for t being type of T, A being Subset of the adjectives of T
st A is_properly_applicable_to t
holds A is finite
proof
let T be non empty non void reflexive transitive TAS-structure;
let t be type of T, A be Subset of the adjectives of T;
assume ex s being FinSequence of the adjectives of T st
rng s = A & s is_properly_applicable_to t;
hence thesis;
end;
theorem Th64:
for T being non empty non void reflexive transitive TAS-structure
for t being type of T
holds {} the adjectives of T is_properly_applicable_to t
proof
let T be non empty non void reflexive transitive TAS-structure;
let t be type of T;
take s = <*> the adjectives of T;
thus rng s = {} the adjectives of T;
let i be natural number;
thus thesis;
end;
scheme MinimalFiniteSet{P[set]}:
ex A being finite set st P[A] & for B being set st B c= A & P[B] holds B = A
provided
A1: ex A being finite set st P[A]
proof
consider A being finite set such that
A2: P[A] by A1;
defpred _P[set] means P[$1];
consider Y being set such that
A3: for x being set holds x in Y iff x in bool A & _P[x] from Separation;
A c= A; then
reconsider Y as non empty set by A2,A3;
A4: bool A is finite by FINSET_1:24;
Y c= bool A proof let x be set; thus thesis by A3; end; then
reconsider Y as finite non empty set by A4,FINSET_1:13;
defpred _R[set,set] means $1 c= $2;
A5: for x being Element of Y holds _R[x,x];
A6: for x,y being Element of Y st _R[x,y] & _R[y,x] holds x = y
by XBOOLE_0:def 10;
A7: for x,y,z being Element of Y st _R[x,y] & _R[y,z] holds _R[x,z]
by XBOOLE_1:1;
A8: for X being set st X c= Y &
(for x,y being Element of Y st x in X & y in X
holds _R[x,y] or _R[y,x]) holds
ex y being Element of Y st
for x being Element of Y st x in X holds _R[y,x]
proof let X be set such that
A9: X c= Y and
A10: for x,y being Element of Y st x in X & y in X holds _R[x,y] or _R[y,x];
per cases;
suppose
A11: X = {}; consider y being Element of Y;
take y;
thus for x being Element of Y st x in X holds y c= x by A11;
suppose
A12: X <> {}; consider x0 being Element of X; x0 in X by A12; then
reconsider x0 as Element of Y by A9;
deffunc F(set) = Card {y where y is Element of Y: y in X & y c< $1};
consider f being Function such that
A13: dom f = X & for x being set st x in X holds f.x = F(x) from Lambda;
set fx0 = {y where y is Element of Y: y in X & y c< x0};
fx0 c= Y
proof let a be set; assume a in fx0; then
ex y being Element of Y st a = y & y in X & y c< x0;
hence thesis;
end; then
reconsider fx0 as finite set by FINSET_1:13;
defpred _P[Nat] means
ex x being Element of Y st x in X & $1 = f.x;
f.x0 = card fx0 by A12,A13; then
A14: ex n being Nat st _P[n] by A12;
A15: for k being Nat st k<>0 & _P[k] ex n being Nat st n<k & _P[n]
proof let k being Nat such that
A16: k <> 0;
given x being Element of Y such that
A17: x in X & k = f.x;
set A = {z where z is Element of Y: z in X & z c< x};
reconsider A as non empty set by A13,A16,A17,CARD_1:78;
consider z being Element of A; z in A; then
consider y being Element of Y such that
A18: z = y & y in X & y c< x;
set fx0 = {a where a is Element of Y: a in X & a c< y};
fx0 c= Y
proof let a be set; assume a in fx0; then
ex z being Element of Y st a = z & z in X & z c< y;
hence thesis;
end; then
reconsider fx0 as finite set by FINSET_1:13;
reconsider n = card fx0 as Nat;
set fx = {a where a is Element of Y: a in X & a c< x};
fx c= Y
proof let a be set; assume a in fx; then
ex z being Element of Y st a = z & z in X & z c< x;
hence thesis;
end; then
reconsider fx as finite set by FINSET_1:13;
A19: k = card fx by A13,A17;
take n;
A20: fx0 c= fx
proof
let a be set; assume a in fx0; then
consider b being Element of Y such that
A21: a = b & b in X & b c< y;
b c< x by A18,A21,XBOOLE_1:56;
hence thesis by A21;
end; then
card fx0 c= card fx by CARD_1:27; then
A22: n <= k by A19,CARD_1:56;
not ex a being Element of Y st y = a & a in X & a c< y; then
y in fx & not y in fx0 by A18; then
card fx <> card fx0 by A20,TRIANG_1:3;
hence n < k by A19,A22,REAL_1:def 5;
take y; thus y in X & n = f.y by A13,A18;
end;
_P[0] from Regr(A14,A15); then
consider y being Element of Y such that
A23: y in X & 0 = f.y;
A24: f.y = Card {z where z is Element of Y: z in X & z c< y} by A13,A23;
take y;
let x be Element of Y; assume
A25: x in X; then
x c= y or y c= x by A10,A23; then
x c< y or y c= x by XBOOLE_0:def 8; then
x in {z where z is Element of Y: z in X & z c< y} or y c= x by A25;
hence _R[y,x] by A23,A24,CARD_2:59;
end;
consider x being Element of Y such that
A26: for y being Element of Y st x <> y holds not _R[y,x]
from Zorn_Min(A5,A6,A7,A8);
x in bool A by A3; then
reconsider x as finite set by FINSET_1:13;
take x; thus P[x] by A3;
let B be set; assume
A27: B c= x & P[B];
x in bool A by A3; then
B c= A by A27,XBOOLE_1:1; then
B in Y by A3,A27;
hence thesis by A26,A27;
end;
theorem Th65:
for T being non empty non void reflexive transitive TAS-structure
for t being type of T, A being Subset of the adjectives of T
st A is_properly_applicable_to t
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
let T be non empty non void reflexive transitive TAS-structure;
let t be type of T, A be Subset of the adjectives of T;
defpred _P[set] means
ex B being Subset of the adjectives of T st
$1 = B & $1 c= A & B is_properly_applicable_to t & A ast t = B ast t;
assume A is_properly_applicable_to t; then
A is finite & A c= A & A is_properly_applicable_to t & A ast t = A ast t
by Th63; then
A1: ex a being finite set st _P[a];
consider B being finite set such that
A2: _P[B] and
A3: for C being set st C c= B & _P[C] holds C = B from MinimalFiniteSet(A1);
reconsider B as Subset of the adjectives of T by A2;
take B;
thus B c= A & B is_properly_applicable_to t & A ast t = B ast t by A2;
let C be Subset of the adjectives of T; assume
A4: C c= B; then
C c= A by A2,XBOOLE_1:1;
hence thesis by A3,A4;
end;
definition
let T be non empty non void reflexive transitive TAS-structure;
attr T is commutative means :Def31:
for t1,t2 being type of T, a being adjective of T
st a is_properly_applicable_to t1 & a ast t1 <= t2
ex A being finite Subset of the adjectives of T
st A is_properly_applicable_to t1 "\/" t2 &
A ast (t1 "\/" t2) = t2;
end;
definition
cluster Mizar-widening-like involutive without_fixpoints
consistent adj-structured adjs-typed non-absorbing subjected commutative
(complete upper-bounded non empty non void trivial reflexive
transitive antisymmetric strict TAS-structure);
existence
proof consider P being non void Mizar-widening-like involutive
without_fixpoints consistent adj-structured adjs-typed
(trivial non empty reflexive complete strict TA-structure);
set T = TAS-structure(#the carrier of P, the adjectives of P,
the InternalRel of P, the non-op of P, the adj-map of P, sub P#);
T is non empty & the RelStr of P = the RelStr of T by STRUCT_0:def 1; then
reconsider T as non void trivial non empty reflexive strict TAS-structure
by Def4,TEX_2:4,WAYBEL_8:12;
take T; thus T is Mizar-widening-like;
the AdjectiveStr of P = the AdjectiveStr of T;
hence T is involutive without_fixpoints by Th5,Th6;
thus T is consistent adj-structured adjs-typed by Th8,Th9,Th17;
A1:the AdjectiveStr of P = the AdjectiveStr of T;
A2:the RelStr of P = the RelStr of T;
hereby
let a be adjective of T;
reconsider b = a as adjective of P;
thus sub non-a = (sub P).non-a by Def24
.= (sub P).non-b by A1,Th3
.= sup (types non-b \/ types non-non-b) by Def23
.= sup (types non-b \/ types b) by Def7
.= (sub P).a by Def23
.= sub a by Def24;
end;
thus T is subjected
proof
let a be adjective of T;
reconsider b = a as adjective of P;
non-a = non-b by A1,Th3; then
types a = types b & types non-a = types non-b by Th11; then
types a \/ types non-a = types b \/ types non-b &
ex_sup_of types a \/ types non-a, T by YELLOW_0:17; then
sup (types a \/ types non-a) = sup (types b \/ types non-b)
by A2,YELLOW_0:26; then
sup (types a \/ types non-a) = (sub P).b by Def23 .= sub a by Def24;
hence thesis by YELLOW_0:32;
end;
let t1,t2 be type of T, a be adjective of T such that
a is_properly_applicable_to t1 & a ast t1 <= t2;
take A = {} the adjectives of T;
thus A is_properly_applicable_to t1 "\/" t2 by Th64;
thus A ast (t1 "\/" t2) = t2 by REALSET1:def 20;
end;
end;
theorem Th66:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TAS-structure)
for t being type of T, A being Subset of the adjectives of T
st A is_properly_applicable_to t
ex s being one-to-one FinSequence of the adjectives of T st
rng s = A & s is_properly_applicable_to t
proof
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TAS-structure);
let t be type of T, A be Subset of the adjectives of T;
given s' being FinSequence of the adjectives of T such that
A1: rng s' = A & s' is_properly_applicable_to t;
defpred _P[Nat] means
ex s being FinSequence of the adjectives of T st
$1 = len s & rng s = A & s is_properly_applicable_to t;
len s' = len s'; then
A2: ex k being Nat st _P[k] by A1;
consider k being Nat such that
A3: _P[k] and
A4: for n being Nat st _P[n] holds k <= n from Min(A2);
consider s being FinSequence of the adjectives of T such that
A5: k = len s & rng s = A & s is_properly_applicable_to t by A3;
s is one-to-one
proof
let x,y be set; assume
A6: x in dom s & y in dom s & s.x = s.y & x <> y; then
reconsider x,y as Nat;
x < y or x > y by A6,REAL_1:def 5; then
consider x,y being Nat such that
A7: x in dom s & y in dom s & x < y & s.x = s.y by A6;
y >= 1 by A7,FINSEQ_3:27; then
consider i being Nat such that
A8: y = 1+i by NAT_1:28;
reconsider s1 = s|Seg i as FinSequence of the adjectives of T
by FINSEQ_1:23;
s1 c= s by TREES_1:def 1; then
consider s2 being FinSequence such that
A9: s = s1^s2 by TREES_1:8;
reconsider s2 as FinSequence of the adjectives of T by A9,FINSEQ_1:50;
reconsider s21 = s2|Seg 1 as FinSequence of the adjectives of T
by FINSEQ_1:23;
A10: y <= len s & i < y by A7,A8,FINSEQ_3:27,NAT_1:38; then
i <= len s by AXIOMS:22; then
A11: len s = len s1+len s2 & len s1 = i by A9,FINSEQ_1:21,35; then
A12: len s2 >= 1 by A8,A10,REAL_1:53; then
A13: len s21 = 1 by FINSEQ_1:21; then
A14: s21 = <*s21.1*> by FINSEQ_1:57; then
A15: rng s21 = {s21.1} by FINSEQ_1:56; then
{s21.1} c= the adjectives of T by FINSEQ_1:def 4; then
s21.1 in the adjectives of T by ZFMISC_1:37; then
reconsider a = s21.1 as adjective of T;
s21 c= s2 by TREES_1:def 1; then
consider s22 being FinSequence such that
A16: s2 = s21^s22 by TREES_1:8;
reconsider s22 as FinSequence of the adjectives of T by A16,FINSEQ_1:50;
A17: 1 in dom s2 by A12,FINSEQ_3:27;
A18: a = s2.1 by A14,A16,FINSEQ_1:58 .= s.y by A8,A9,A11,A17,FINSEQ_1:def 7;
x <= i & x >= 1 by A7,A8,FINSEQ_3:27,NAT_1:38; then
A19: x in dom s1 & s1 is_properly_applicable_to t
by A5,A9,A11,Th61,FINSEQ_3:27; then
a = s1.x & s1 is_applicable_to t by A7,A9,A18,Th58,FINSEQ_1:def 7; then
A20: a in rng s1 & rng s1 c= adjs (s1 ast t) by A19,Th45,FUNCT_1:12; then
A21: s1 ast t = a ast (s1 ast t) by Th25 .= s21 ast (s1 ast t) by A14,Th32;
s2 is_properly_applicable_to s1 ast t by A5,A9,Th61; then
s22 is_properly_applicable_to s1 ast t by A16,A21,Th61; then
A22: s1^s22 is_properly_applicable_to t by A19,Th62;
rng s21 c= rng s1 by A15,A20,ZFMISC_1:37; then
rng s1 \/ rng s21 = rng s1 by XBOOLE_1:12; then
rng (s1^s22) = rng s1 \/ rng s21 \/ rng s22 & rng s = rng s1 \/ rng s2 &
rng s2 = rng s21 \/ rng s22 by A9,A16,FINSEQ_1:44; then
rng (s1^s22) = A by A5,XBOOLE_1:4; then
k <= len (s1^s22) by A4,A22; then
k <= len s1+len s22 & len s2 = len s21+len s22 by A16,FINSEQ_1:35; then
len s21+len s22 <= 0+len s22 by A5,A11,REAL_1:53;
hence thesis by A13,REAL_1:53;
end;
hence thesis by A5;
end;
begin :: Reduction of adjectives
definition
let T be non empty non void reflexive transitive TAS-structure;
func T @--> -> Relation of T means:Def32:
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
proof
defpred _P[Element of T, Element of T] means
ex a being adjective of T st not a in adjs $2 &
a is_properly_applicable_to $2 & a ast $2 = $1;
consider R being Relation of the carrier of T such that
A1: for t1,t2 being Element of T
holds [t1,t2] in R iff _P[t1,t2] from Rel_On_Dom_Ex;
reconsider R as Relation of T;
take R; thus thesis by A1;
end;
uniqueness
proof let R1,R2 be Relation of T such that
A2: for t1,t2 being type of T holds [t1,t2] in R1 iff
ex a being adjective of T st not a in adjs t2 &
a is_properly_applicable_to t2 & a ast t2 = t1 and
A3: for t1,t2 being type of T holds [t1,t2] in R2 iff
ex a being adjective of T st not a in adjs t2 &
a is_properly_applicable_to t2 & a ast t2 = t1;
now let t1,t2 be Element of T;
[t1,t2] in R1 iff
ex a being adjective of T st not a in adjs t2 &
a is_properly_applicable_to t2 & a ast t2 = t1 by A2;
hence [t1,t2] in R1 iff [t1,t2] in R2 by A3;
end;
hence thesis by T_0TOPSP:1;
end;
end;
theorem Th67:
for T being adj-structured antisymmetric
(non void reflexive transitive with_suprema Noetherian TAS-structure)
holds T@--> c= the InternalRel of T
proof
let T be adj-structured with_suprema antisymmetric
(non empty non void reflexive transitive Noetherian TAS-structure);
let t1,t2 be Element of T;
reconsider q1 = t1, q2 = t2 as type of T;
assume [t1,t2] in T@-->; then
consider a being adjective of T such that
not a in adjs q2 and
A1: a is_properly_applicable_to q2 and
A2: a ast q2 = q1 by Def32;
a is_applicable_to q2 by A1,Def28; then
q1 <= q2 by A2,Th21;
hence thesis by ORDERS_1:def 9;
end;
scheme RedInd{X() -> non empty set, P[set,set], R() -> Relation of X()}:
for x,y being Element of X() st R() reduces x,y holds P[x,y]
provided
A1: for x,y being Element of X() st [x,y] in R() holds P[x,y]
and
A2: for x being Element of X() holds P[x,x]
and
A3: for x,y,z being Element of X() st P[x,y] & P[y,z] holds P[x,z]
proof
let x,y be Element of X();
given p being RedSequence of R() such that
A4: p.1 = x & p.len p = y;
defpred _P[Nat] means 1+$1 <= len p implies P[x, p.(1+$1)];
A5: _P[0] by A2,A4;
A6: now let i be Nat such that
A7: _P[i];
now assume
A8: 1+(i+1) <= len p;
i+1 < len p & i+1 >= 1 & 1+(i+1) >= 1 by A8,NAT_1:29,38; then
P[x, p.(1+i)] & i+1 in dom p & 1+(i+1) in dom p
by A7,A8,FINSEQ_3:27; then
A9: [p.(i+1), p.(1+(i+1))] in R() by REWRITE1:def 2; then
A10: p.(i+1) in X() & p.(1+(i+1)) in X() by ZFMISC_1:106; then
P[p.(i+1), p.(1+(i+1))] by A1,A9;
hence P[x, p.(1+(i+1))] by A3,A7,A8,A10,NAT_1:38;
end; hence _P[i+1];
end;
len p > 0 by REWRITE1:def 2; then
len p >= 0+1 by NAT_1:38; then
A11: ex n being Nat st len p = 1+n by NAT_1:28;
for n being Nat holds _P[n] from Ind(A5,A6);
hence thesis by A4,A11;
end;
theorem Th68:
for T being adj-structured antisymmetric
(non void reflexive transitive with_suprema Noetherian TAS-structure)
for t1,t2 being type of T st T@--> reduces t1,t2
holds t1 <= t2
proof
let T be adj-structured with_suprema antisymmetric
(non empty non void reflexive transitive Noetherian TAS-structure);
let t1,t2 be type of T;
set R = T@-->;
defpred _P[Element of T, Element of T] means
$1 <= $2;
A1: now let x,y be Element of T;
R c= the InternalRel of T by Th67;
hence [x,y] in R implies _P[x, y] by ORDERS_1:def 9;
end;
A2: for x being Element of T holds _P[x, x];
A3: for x,y,z be Element of T
holds _P[x, y] & _P[y, z] implies _P[x, z] by YELLOW_0:def 2;
for x,y being Element of T st R reduces x,y holds _P[x,y]
from RedInd(A1,A2,A3);
hence thesis;
end;
theorem Th69:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
non void with_suprema TAS-structure)
holds T@--> is irreflexive
proof
let T be Noetherian adj-structured (reflexive transitive antisymmetric
non void with_suprema TAS-structure);
set R = T@-->;
let x be set; assume x in field R; assume
A1: [x,x] in R; then
x in the carrier of T by ZFMISC_1:106; then
reconsider x as type of T;
consider a being adjective of T such that
A2: not a in adjs x and
A3: a is_properly_applicable_to x & a ast x = x by A1,Def32;
a is_applicable_to x by A3,Def28;
hence thesis by A2,A3,Th22;
end;
theorem Th70:
for T being adj-structured antisymmetric
(non void reflexive transitive with_suprema Noetherian TAS-structure)
holds T@--> is strongly-normalizing
proof
let T be adj-structured with_suprema antisymmetric
(non empty non void reflexive transitive Noetherian TAS-structure);
set R = T@-->, Q = the InternalRel of T;
A1: R c= Q by Th67; then
A2: field R c= field Q by RELAT_1:31;
R is co-well_founded
proof
let Y be set; assume
A3: Y c= field R & Y <> {}; then
Y c= field Q by A2,XBOOLE_1:1; then
consider a being set such that
A4: a in Y & for b being set st b in Y & a <> b holds not [a,b] in Q
by A3,REWRITE1:def 16;
take a;
thus thesis by A1,A4;
end; then
R is irreflexive co-well_founded Relation by Th69;
hence thesis;
end;
theorem Th71:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TAS-structure)
for t being type of T, 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
for s being one-to-one FinSequence of the adjectives of T
st rng s = A & s is_properly_applicable_to t
for i being natural number st 1 <= i & i <= len s
holds [apply(s, t).(i+1), apply(s, t).i] in T@-->
proof
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TAS-structure);
let t be type of T, A be finite Subset of the adjectives of T such that
A1: 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;
let s be one-to-one FinSequence of the adjectives of T such that
A2: rng s = A & s is_properly_applicable_to t;
A3: len apply(s, t) = len s+1 by Def20;
let j be natural number; assume
A4: 1 <= j & j <= len s; then
j < len s+1 & j is Nat by NAT_1:38,ORDINAL2:def 21; then
A5: j in dom s & j in dom apply(s, t) by A3,A4,FINSEQ_3:27; then
s.j in rng s & rng s c= the adjectives of T
by FINSEQ_1:def 4,FUNCT_1:12; then
reconsider a = s.j as adjective of T;
apply(s, t).j in rng apply(s, t) & rng apply(s, t) c= the carrier of T
by A5,FINSEQ_1:def 4,FUNCT_1:12; then
reconsider tt = apply(s, t).j as type of T;
A6: apply(s, t).(j+1) = a ast tt & a is_properly_applicable_to tt
by A2,A5,Def20,Def29;
not a in adjs tt
proof assume
A7: a in adjs tt;
consider i being Nat such that
A8: j = 1+i by A4,NAT_1:28;
reconsider s1 = s|Seg i as FinSequence of the adjectives of T
by FINSEQ_1:23;
s1 c= s by TREES_1:def 1; then
consider s2 being FinSequence such that
A9: s = s1^s2 by TREES_1:8;
reconsider s2 as FinSequence of the adjectives of T by A9,FINSEQ_1:50;
reconsider s21 = s2|Seg 1 as FinSequence of the adjectives of T
by FINSEQ_1:23;
i <= len s by A4,A8,NAT_1:38; then
A10: len s = len s1+len s2 & len s1 = i by A9,FINSEQ_1:21,35; then
A11: len s2 >= 1 by A4,A8,REAL_1:53; then
A12: len s21 = 1 by FINSEQ_1:21; then
A13: s21 = <*s21.1*> by FINSEQ_1:57; then
A14: rng s21 = {s21.1} by FINSEQ_1:56; then
{s21.1} c= the adjectives of T by FINSEQ_1:def 4; then
s21.1 in the adjectives of T by ZFMISC_1:37; then
reconsider b = s21.1 as adjective of T;
s21 c= s2 by TREES_1:def 1; then
consider s22 being FinSequence such that
A15: s2 = s21^s22 by TREES_1:8;
reconsider s22 as FinSequence of the adjectives of T by A15,FINSEQ_1:50;
A16: 1 in dom s2 by A11,FINSEQ_3:27;
A17: b = s2.1 by A13,A15,FINSEQ_1:58 .= a by A8,A9,A10,A16,FINSEQ_1:def 7;
A18: s1 is_properly_applicable_to t by A2,A9,A10,Th61;
s1 ast t = tt by A8,A9,A10,Th37; then
A19: s1 ast t = a ast (s1 ast t) by A7,Th25
.= s21 ast (s1 ast t) by A13,A17,Th32;
s2 is_properly_applicable_to s1 ast t by A2,A9,Th61; then
s22 is_properly_applicable_to s1 ast t by A15,A19,Th61; then
A20: s1^s22 is_properly_applicable_to t by A18,Th62; then
A21: s1^s22 is_applicable_to t & s is_applicable_to t by A2,Th58;
reconsider B = rng (s1^s22) as Subset of the adjectives of T
by FINSEQ_1:def 4;
s ast t = s2 ast (s1 ast t) by A9,Th38
.= s22 ast (s1 ast t) by A15,A19,Th38
.= s1^s22 ast t by Th38; then
A22: A ast t = s1^s22 ast t by A2,A21,Th57 .= B ast t by A21,Th57;
A23: B is_properly_applicable_to t by A20,Def30;
A24: B = rng s1 \/ rng s22 & A = rng s1 \/ rng s2 &
rng s2 = rng s21 \/ rng s22 by A2,A9,A15,FINSEQ_1:44; then
rng s22 c= rng s2 by XBOOLE_1:7; then
B c= A by A24,XBOOLE_1:9; then
A25: B = A by A1,A22,A23;
a in rng s21 by A14,A17,TARSKI:def 1; then
a in rng s2 by A24,XBOOLE_0:def 2; then
A26: a in B by A24,A25,XBOOLE_0:def 2;
per cases by A24,A26,XBOOLE_0:def 2;
suppose a in rng s1; then
consider x being set such that
A27: x in dom s1 & a = s1.x by FUNCT_1:def 5;
reconsider x as Nat by A27;
dom s1 c= dom s & x <= len s1 by A9,A27,FINSEQ_1:39,FINSEQ_3:27; then
x < j & x in dom s & s.x = a by A8,A9,A10,A27,FINSEQ_1:def 7,NAT_1:38;
hence contradiction by A5,FUNCT_1:def 8;
suppose a in rng s22; then
consider x being set such that
A28: x in dom s22 & a = s22.x by FUNCT_1:def 5;
reconsider x as Nat by A28;
x >= 0+1 by A28,FINSEQ_3:27; then
x > 0 by NAT_1:38; then
A29: x+1+i = j+x & j+x > j+0 by A8,REAL_1:53,XCMPLX_1:1;
1+x in dom s2 & s2.(1+x) = a by A12,A15,A28,FINSEQ_1:41,def 7; then
i+(1+x) in dom s & s.(i+(1+x)) = a by A9,A10,FINSEQ_1:41,def 7;
hence contradiction by A5,A29,FUNCT_1:def 8;
end;
hence [apply(s, t).(j+1), apply(s, t).j] in T@--> by A6,Def32;
end;
theorem Th72:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TAS-structure)
for t being type of T, 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
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
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TAS-structure);
let t be type of T, A be finite Subset of the adjectives of T such that
A1: 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;
let s be one-to-one FinSequence of the adjectives of T such that
A2: rng s = A & s is_properly_applicable_to t;
A3: len Rev apply(s, t) = len apply(s, t) & len apply(s, t) = len s+1 &
dom Rev apply(s, t) = dom apply(s, t) by Def20,FINSEQ_5:60,def 3;
hence len Rev apply(s, t) > 0 by NAT_1:19;
let i be Nat; assume
i in dom Rev apply(s, t) & i+1 in dom Rev apply(s, t); then
A4: i >= 1 & i+1 <= len s+1 & (Rev apply(s, t)).i = apply(s, t).(len s+1-i+1) &
(Rev apply(s, t)).(i+1) = apply(s, t).(len s+1-(i+1)+1)
by A3,FINSEQ_3:27,FINSEQ_5:def 3; then
consider j being Nat such that
A5: len s+1 = i+1+j by NAT_1:28;
i+1+j = j+1+i & i+1+j = j+i+1 by XCMPLX_1:1; then
A6: len s+1-(i+1) = j & len s+1-i = j+1 & len s = i+j by A5,XCMPLX_1:2,26;
then j+1 >= 1 & j+1 <= len s by A4,AXIOMS:24,NAT_1:29;
hence thesis by A1,A2,A4,A6,Th71;
end;
theorem Th73:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TAS-structure)
for t being type of T, A being finite Subset of the adjectives of T
st A is_properly_applicable_to t
holds T@--> reduces A ast t, t
proof
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TAS-structure);
let t be type of T, A be finite Subset of the adjectives of T such that
A1: A is_properly_applicable_to t;
set R = T@-->;
consider A' being Subset of the adjectives of T such that
A2: A' c= A & A' is_properly_applicable_to t & A ast t = A' ast t and
A3: 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' by A1,Th65;
consider s being one-to-one FinSequence of the adjectives of T such that
A4: rng s = A' & s is_properly_applicable_to t by A2,Th66;
A5: s is_applicable_to t by A4,Th58;
reconsider p = Rev apply(s, t) as RedSequence of R by A2,A3,A4,Th72;
take p;
thus p.1 = apply(s, t).len apply(s, t) by FINSEQ_5:65
.= apply(s, t).(len s+1) by Def20
.= s ast t by Def21
.= A ast t by A2,A4,A5,Th57;
thus p.len p = p.len apply(s, t) by FINSEQ_5:def 3
.= apply(s, t).1 by FINSEQ_5:65
.= t by Def20;
end;
theorem Th74:
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
proof
let X be non empty set;
let R be Relation of X;
let p be RedSequence of R such that
A1: p.1 in X;
let x be set; assume x in rng p; then
consider i being set such that
A2: i in dom p & x = p.i by FUNCT_1:def 5;
reconsider i as Nat by A2;
A3: i >= 1 by A2,FINSEQ_3:27;
per cases by A3,AXIOMS:21;
suppose i = 1; hence x in X by A1,A2;
suppose i > 1; then
i >= 1+1 by NAT_1:38; then
consider j being Nat such that
A4: i = 1+1+j by NAT_1:28;
A5: i = j+1+1 & i <= len p by A2,A4,FINSEQ_3:27,XCMPLX_1:1; then
A6: j+1 >= 1 & j+1+1 >= 1 & j+1 < len p by NAT_1:29,38;
j+1 in dom p by A6,FINSEQ_3:27; then
[p.(j+1), x] in R by A2,A5,REWRITE1:def 2;
hence x in X by ZFMISC_1:106;
end;
theorem Th75:
for X being non empty set
for R being Relation of X
for x be Element of X, y being set st R reduces x,y
holds y in X
proof
let X be non empty set;
let R be Relation of X;
let x be Element of X, y be set;
given p being RedSequence of R such that
A1: p.1 = x & p.len p = y;
len p > 0 by REWRITE1:def 2; then
len p >= 0+1 by NAT_1:38; then
len p in dom p & p is FinSequence of X by A1,Th74,FINSEQ_3:27; then
y in rng p & rng p c= X by A1,FINSEQ_1:def 4,FUNCT_1:12;
hence thesis;
end;
theorem Th76:
for X being non empty set
for R being Relation of X
st R is with_UN_property weakly-normalizing
for x be Element of X
holds nf(x, R) in X
proof
let X be non empty set;
let R be Relation of X such that
A1: R is with_UN_property weakly-normalizing;
let x be Element of X;
nf(x,R) is_a_normal_form_of x, R by A1,REWRITE1:55; then
R reduces x, nf(x,R) by REWRITE1:def 6;
hence thesis by Th75;
end;
theorem Th77:
for T being Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TAS-structure)
for t1, t2 being type of T st T@--> reduces t1, t2
ex A being finite Subset of the adjectives of T
st A is_properly_applicable_to t2 & t1 = A ast t2
proof
let T be Noetherian adj-structured (reflexive transitive antisymmetric
with_suprema non void TAS-structure);
let t1,t2 be type of T;
set R = T@-->;
given p being RedSequence of R such that
A1: p.1 = t1 & t2 = p.len p;
len p > 0 by REWRITE1:def 2; then
A2: len p >= 0+1 by NAT_1:38; then
consider i being Nat such that
A3: len p = 1+i by NAT_1:28;
defpred _P[set,set] means
ex j being Nat,
a being adjective of T, t being type of T st
$2 = a & $1 = j & a ast t = p.j & t = p.(j+1) &
a is_properly_applicable_to t;
A4: now let x be set; assume
A5: x in Seg i; then reconsider j = x as Nat;
A6: j >= 1 & j <= i by A5,FINSEQ_1:3; then
1 <= j+1 & j+1 <= len p & j < len p by A3,AXIOMS:24,NAT_1:38; then
j in dom p & j+1 in dom p by A6,FINSEQ_3:27; then
A7: [p.j, p.(j+1)] in R by REWRITE1:def 2; then
p.j in the carrier of T & p.(j+1) in the carrier of T
by ZFMISC_1:106; then
reconsider q1 = p.j, q2 = p.(j+1) as type of T;
ex a being adjective of T st not a in adjs q2 &
a is_properly_applicable_to q2 & a ast q2 = q1 by A7,Def32;
hence ex y being set st y in the adjectives of T & _P[x,y];
end;
consider f being Function such that
A8: dom f = Seg i & rng f c= the adjectives of T and
A9: for x being set st x in Seg i holds _P[x,f.x] from NonUniqBoundFuncEx(A4);
f is FinSequence by A8,FINSEQ_1:def 2; then
reconsider f as FinSequence of the adjectives of T by A8,FINSEQ_1:def 4;
set r = Rev f;
defpred _P[Nat] means
1+$1 <= len p implies (Rev p).(1+$1) = apply(r, t2).(1+$1);
A10: len r = len f & len apply(r, t2) = len r+1 & len f = i & len Rev p = len p
by A8,Def20,FINSEQ_1:def 3,FINSEQ_5:def 3; then
1 in dom Rev p & len p-1+1 = len p by A2,FINSEQ_3:27,XCMPLX_1:27; then
(Rev p).1 = t2 by A1,FINSEQ_5:def 3; then
A11: _P[0] by Def20;
A12: now let j be Nat such that
A13: _P[j];
now assume
A14: 1+(j+1) <= len p;
j+1 <= i by A3,A14,REAL_1:53; then
consider x being Nat such that
A15: i = j+1+x by NAT_1:28;
A16: i = x+1+j by A15,XCMPLX_1:1; then
x+1 >= 1 & i >= x+1 by NAT_1:29; then
x+1 in Seg i by FINSEQ_1:3; then
consider k being Nat, a being adjective of T, t being type of T such that
A17: f.(x+1) = a & x+1 = k & a ast t = p.k & t = p.(k+1) &
a is_properly_applicable_to t by A9;
i+1 = j+1+(x+1) by A15,XCMPLX_1:1; then
A18: i+1-(j+1) = x+1 by XCMPLX_1:26;
A19: i+1-(1+(j+1)) = x+((j+1)+1)-(1+(j+1)) by A15,XCMPLX_1:1
.= x by XCMPLX_1:26;
j <= i by A16,NAT_1:29; then
j+1 >= 1 & j+1 <= i & j+1 <= i+1 by A15,AXIOMS:24,NAT_1:29; then
A20: j+1 in dom r & j+1 in dom apply(r, t2) by A10,FINSEQ_3:27; then
1+(j+1) >= 1 & j+1 >= 1 & j+1 < len p by A14,NAT_1:29,38; then
j+1 in dom Rev p & 1+(j+1) in dom Rev p &
(Rev p).(1+j) = apply(r, t2).(1+j) by A10,A13,A14,FINSEQ_3:27; then
A21: (Rev p).(j+1) = p.(x+1+1) & (Rev p).(1+(j+1)) = p.(x+1)
by A3,A18,A19,FINSEQ_5:def 3;
r.(j+1) = f.(len f-(j+1)+1) by A20,FINSEQ_5:def 3
.= a by A10,A15,A17,XCMPLX_1:26;
hence (Rev p).(1+(j+1)) = apply(r, t2).(1+(j+1))
by A13,A14,A17,A20,A21,Def20,NAT_1:38;
end; hence _P[j+1];
end;
A22: for j being Nat holds _P[j] from Ind(A11,A12);
now
let j be Nat; assume 1 <= j; then
ex k being Nat st j = 1+k by NAT_1:28;
hence j <= len p implies (Rev p).j = apply(r, t2).j by A22;
end; then
A23: Rev p = apply(r, t2) by A3,A10,FINSEQ_1:18; then
A24: p = Rev apply(r, t2) by FINSEQ_6:29;
reconsider A = rng f as finite Subset of the adjectives of T by A8;
take A;
A25: r is_properly_applicable_to t2
proof
let j be natural number, a be adjective of T, s be type of T;
assume
A26: j in dom r & a = r.j & s = apply(r,t2).j; then
j in dom f & j >= 1 & j <= len r by FINSEQ_3:27,FINSEQ_5:60; then
consider k being Nat such that
A27: len r = j+k by NAT_1:28;
len r = len f by FINSEQ_5:def 3; then
A28: len f-j = k & k-1+1 = k & j >= 1
by A26,A27,FINSEQ_3:27,XCMPLX_1:26,27; then
k+1 >= 1 & k+1 <= i by A10,A27,AXIOMS:24,NAT_1:29; then
len f-j+1 in Seg i by A28,FINSEQ_1:3; then
consider o being Nat, b being adjective of T, u being type of T such that
A29: f.(len f-j+1) = b & len f-j+1 = o & b ast u = p.o & u = p.(o+1) &
b is_properly_applicable_to u by A9;
i+1 = k+1+j & (i+1)-(o+1) = (i+1)-o-1 by A10,A27,XCMPLX_1:1,36; then
(i+1)-(o+1) = j-1 & o+1 >= 1 & o+1 <= len p
by A3,A28,A29,AXIOMS:24,NAT_1:29,XCMPLX_1:26; then
A30: len (apply(r, t2))-(o+1)+1 = j & o+1 in dom p
by A10,FINSEQ_3:27,XCMPLX_1:27;
a = b by A26,A29,FINSEQ_5:def 3;
hence a is_properly_applicable_to s by A24,A26,A29,A30,FINSEQ_5:def 3;
end;
A31: rng r = A by FINSEQ_5:60;
thus A is_properly_applicable_to t2
proof
take r; thus thesis by A25,FINSEQ_5:60;
end;
r is_applicable_to t2 by A25,Th58; then
A ast t2 = r ast t2 by A31,Th57 .= apply(r, t2).(len r+1) by Def21;
hence t1 = A ast t2 by A1,A10,A23,FINSEQ_5:65;
end;
theorem Th78:
for T being adj-structured antisymmetric commutative
(non void reflexive transitive with_suprema Noetherian TAS-structure)
holds T@--> is with_Church-Rosser_property with_UN_property
proof
let T be adj-structured with_suprema antisymmetric commutative
(non empty non void reflexive transitive Noetherian TAS-structure);
set R = T@-->;
R is locally-confluent
proof
let a,b,c be set;
assume
A1: [a,b] in R & [a,c] in R; then
a in the carrier of T & b in the carrier of T & c in the carrier of T
by ZFMISC_1:106; then
reconsider t = a, t1 = b, t2 = c as type of T;
consider a2 being adjective of T such that
A2: not a2 in adjs t1 &
a2 is_properly_applicable_to t1 & a2 ast t1 = t by A1,Def32;
consider a3 being adjective of T such that
A3: not a3 in adjs t2 &
a3 is_properly_applicable_to t2 & a3 ast t2 = t by A1,Def32;
a2 is_applicable_to t1 & a3 is_applicable_to t2 by A2,A3,Def28; then
A4: t <= t1 & t <= t2 by A2,A3,Th21; then
consider A being finite Subset of the adjectives of T such that
A5: A is_properly_applicable_to t1 "\/" t2 &
A ast (t1 "\/" t2) = t1 by A3,Def31;
consider B being finite Subset of the adjectives of T such that
A6: B is_properly_applicable_to t1 "\/" t2 &
B ast (t1 "\/" t2) = t2 by A2,A4,Def31;
set tt = t1 "\/" t2;
take tt;
thus thesis by A5,A6,Th73;
end; then
R is strongly-normalizing locally-confluent Relation by Th70;
hence thesis;
end;
begin :: Radix types
definition
let T be adj-structured with_suprema antisymmetric commutative
(non empty non void reflexive transitive Noetherian TAS-structure);
let t be type of T;
func radix t -> type of T equals :Def33:
nf(t, T@-->);
coherence
proof
T@--> is with_Church-Rosser_property with_UN_property strongly-normalizing
Relation by Th70,Th78; then
nf(t, T@-->) in the carrier of T by Th76;
hence thesis;
end;
end;
theorem Th79:
for T being adj-structured with_suprema antisymmetric commutative
(non empty non void reflexive transitive Noetherian TAS-structure)
for t being type of T
holds T@--> reduces t, radix t
proof
let T be adj-structured with_suprema antisymmetric commutative
(non empty non void reflexive transitive Noetherian TAS-structure);
let t be type of T;
set R = T@-->;
R is with_Church-Rosser_property with_UN_property strongly-normalizing
Relation by Th70,Th78; then
nf(t, R) is_a_normal_form_of t, R by REWRITE1:55; then
R reduces t, nf(t,R) by REWRITE1:def 6;
hence R reduces t, radix t by Def33;
end;
theorem Th80:
for T being adj-structured with_suprema antisymmetric commutative
(non empty non void reflexive transitive Noetherian TAS-structure)
for t being type of T
holds t <= radix t
proof
let T be adj-structured with_suprema antisymmetric commutative
(non empty non void reflexive transitive Noetherian TAS-structure);
let t be type of T;
set R = T@-->;
R reduces t, radix t by Th79;
hence thesis by Th68;
end;
theorem Th81:
for T being adj-structured with_suprema antisymmetric commutative
(non empty non void reflexive transitive Noetherian TAS-structure)
for t being type of T
for X being set st X = {t' where t' is type of T:
ex A being finite Subset of the adjectives of T st
A is_properly_applicable_to t' & A ast t' = t}
holds ex_sup_of X, T & radix t = "\/"(X, T)
proof
let T be adj-structured with_suprema antisymmetric commutative
(non empty non void reflexive transitive Noetherian TAS-structure);
let t be type of T;
set R = T@-->;
set AA = {t' where t' is type of T:
ex A being finite Subset of the adjectives of T st
A is_properly_applicable_to t' & A ast t' = t};
A1: R is with_Church-Rosser_property with_UN_property strongly-normalizing
Relation by Th70,Th78;
A2: radix t is_>=_than AA
proof
let tt be type of T; assume tt in AA; then
ex t' being type of T st tt = t' &
ex A being finite Subset of the adjectives of T st
A is_properly_applicable_to t' & A ast t' = t; then
R reduces t, tt by Th73; then
t, tt are_convertible_wrt R by REWRITE1:26; then
nf(t, R) = nf(tt, R) by A1,REWRITE1:56; then
nf(t, R) is_a_normal_form_of tt, R by A1,REWRITE1:55; then
R reduces tt, nf(t,R) by REWRITE1:def 6; then
R reduces tt, radix t by Def33;
hence thesis by Th68;
end;
R reduces t, radix t by Th79; then
ex A being finite Subset of the adjectives of T
st A is_properly_applicable_to radix t & A ast radix t = t by Th77; then
radix t in AA; then
for t' being type of T st t' is_>=_than AA holds radix t <= t'
by LATTICE3:def 9;
hence thesis by A2,YELLOW_0:30;
end;
theorem Th82:
for T being adj-structured with_suprema antisymmetric commutative
(non empty non void reflexive transitive Noetherian TAS-structure)
for t1,t2 being type of T, a being adjective of T
st a is_properly_applicable_to t1 & a ast t1 <= radix t2
holds t1 <= radix t2
proof
let T be adj-structured with_suprema antisymmetric commutative
(non empty non void reflexive transitive Noetherian TAS-structure);
let t1,t2 be type of T, a be adjective of T;
set R = T@-->;
A1: R is with_Church-Rosser_property with_UN_property strongly-normalizing
Relation by Th70,Th78;
set AA = {t' where t' is type of T:
ex A being finite Subset of the adjectives of T st
A is_properly_applicable_to t' & A ast t' = t2};
assume
A2: a is_properly_applicable_to t1 & a ast t1 <= radix t2;
consider A being finite Subset of the adjectives of T such that
A3: A is_properly_applicable_to t1 "\/" radix t2 &
A ast (t1 "\/" radix t2) = radix t2 by A2,Def31;
nf(t2, R) is_a_normal_form_of t2, R by A1,REWRITE1:55; then
R reduces t2, nf(t2,R) by REWRITE1:def 6; then
R reduces t2, radix t2 by Def33; then
consider B being finite Subset of the adjectives of T such that
A4: B is_properly_applicable_to radix t2 & t2 = B ast radix t2 by Th77;
consider v1 being FinSequence of the adjectives of T such that
A5: rng v1 = A & v1 is_properly_applicable_to t1 "\/" radix t2 by A3,Def30;
consider v2 being FinSequence of the adjectives of T such that
A6: rng v2 = B & v2 is_properly_applicable_to radix t2 by A4,Def30;
A7: rng (v1^v2) = A \/ B by A5,A6,FINSEQ_1:44;
A8: v1 is_applicable_to t1 "\/" radix t2 & v2 is_applicable_to radix t2
by A5,A6,Th58; then
A9: radix t2 = v1 ast (t1 "\/" radix t2) by A3,A5,Th57; then
v1^v2 is_properly_applicable_to t1 "\/" radix t2 by A5,A6,Th62; then
A10: A \/ B is_properly_applicable_to t1 "\/" radix t2 &
v1^v2 is_applicable_to t1 "\/" radix t2 by A7,Def30,Th58; then
(A \/ B) ast (t1 "\/" radix t2) = v1^v2 ast (t1 "\/" radix t2) by A7,Th57
.= v2 ast radix t2 by A9,Th38
.= t2 by A4,A6,A8,Th57; then
t1 "\/" radix t2 in AA & ex_sup_of AA, T by A10,Th81; then
t1 "\/" radix t2 <= "\/"(AA, T) by YELLOW_4:1; then
t1 "\/" radix t2 <= radix t2 & t1 "\/" radix t2 >= t1
by Th81,YELLOW_0:22;
hence thesis by YELLOW_0:def 2;
end;
theorem
for T being adj-structured with_suprema antisymmetric commutative
(non empty non void reflexive transitive Noetherian TAS-structure)
for t1,t2 being type of T
st t1 <= t2
holds radix t1 <= radix t2
proof
let T be adj-structured with_suprema antisymmetric commutative
(non empty non void reflexive transitive Noetherian TAS-structure);
set R = T@-->;
let t1, t2 be type of T such that
A1: t1 <= t2;
t2 <= radix t2 by Th80; then
A2: t1 <= radix t2 & R reduces t1, radix t1 by A1,Th79,YELLOW_0:def 2;
set X = the carrier of T;
defpred P[Element of X, Element of X] means
$1 <= radix t2 implies $2 <= radix t2;
A3: now let x,y be Element of X;
reconsider t1 = x, t2 = y as type of T;
assume [x,y] in R; then
ex a being adjective of T st
not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 by
Def32;
hence P[x,y] by Th82;
end;
A4: for x being Element of X holds P[x,x];
A5: for x,y,z being Element of X st P[x,y] & P[y,z] holds P[x,z];
for x,y being Element of T st R reduces x,y holds P[x,y]
from RedInd(A3,A4,A5);
hence thesis by A2;
end;
theorem
for T being adj-structured with_suprema antisymmetric commutative
(non empty non void reflexive transitive Noetherian TAS-structure)
for t being type of T, a being adjective of T
st a is_properly_applicable_to t
holds radix (a ast t) = radix t
proof
let T be adj-structured with_suprema antisymmetric commutative
(non empty non void reflexive transitive Noetherian TAS-structure);
A1: T@--> is with_Church-Rosser_property with_UN_property strongly-normalizing
Relation by Th70,Th78;
let t be type of T, a be adjective of T; assume
A2: a is_properly_applicable_to t;
a in adjs t or not a in adjs t; then
a ast t = t or [a ast t, t] in T@--> by A2,Def32,Th25; then
T@--> reduces a ast t,t by REWRITE1:13,16; then
a ast t, t are_convertible_wrt T@--> by REWRITE1:26; then
nf(a ast t, T@-->) = nf(t, T@-->) by A1,REWRITE1:56;
hence radix (a ast t) = nf(t, T@-->) by Def33 .= radix t by Def33;
end;