:: On semilattice structure of {M}izar types
:: by Grzegorz Bancerek
::
:: Received August 8, 2003
:: Copyright (c) 2003-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ZFMISC_1, RELAT_2, REWRITE1, XBOOLE_0, ORDERS_2,
PRELAMB, SUBSET_1, IDEAL_1, TARSKI, RELAT_1, STRUCT_0, ARYTM_3, XXREAL_0,
WAYBEL_0, LATTICE3, LATTICES, EQREL_1, CARD_FIL, YELLOW_0, ORDINAL2,
BINOP_1, FUNCT_1, OPOSET_1, CARD_1, FUNCOP_1, FINSUB_1, YELLOW_1,
ARYTM_0, WELLORD2, FINSEQ_1, FUNCT_7, NAT_1, ORDINAL4, FINSET_1,
FINSEQ_5, ARYTM_1, ABCMIZ_0, ABIAN, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, RELAT_2, SUBSET_1, ORDINAL1,
FINSUB_1, CARD_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1,
ORDERS_1, FUNCOP_1, FINSET_1, FINSEQ_1, FUNCT_4, ALG_1, FINSEQ_5,
NUMBERS, XCMPLX_0, NAT_1, DOMAIN_1, STRUCT_0, ORDERS_2, LATTICE3,
REWRITE1, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_7, XXREAL_0;
constructors FINSUB_1, NAT_1, FINSEQ_5, REWRITE1, BORSUK_1, LATTICE3,
WAYBEL_0, YELLOW_1, FUNCOP_1, XREAL_0, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_2, FINSET_1, FINSUB_1,
XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, FINSEQ_5, REWRITE1, STRUCT_0,
LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_7, YELLOW_9, ORDINAL1,
CARD_1, RELSET_1;
requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
definitions TARSKI, XBOOLE_0, RELAT_2, FUNCT_1, FINSEQ_1, LATTICE3, REWRITE1,
YELLOW_0, WAYBEL_0, RELSET_1;
equalities FINSEQ_1, LATTICE3, CARD_1, ORDINAL1;
expansions TARSKI, XBOOLE_0, FUNCT_1, FINSEQ_1, LATTICE3, REWRITE1, WAYBEL_0;
theorems TARSKI, XBOOLE_0, XBOOLE_1, SUBSET_1, FINSUB_1, NAT_1, FINSEQ_1,
CARD_1, TREES_1, FINSEQ_5, RELAT_1, RELSET_1, FUNCT_1, FUNCT_2, FUNCT_4,
FUNCOP_1, STRUCT_0, ORDERS_2, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_4,
YELLOW_7, WAYBEL_6, WAYBEL_8, ZFMISC_1, FINSEQ_2, FINSEQ_3, HILBERT2,
REWRITE1, ORDINAL1, XREAL_1, XXREAL_0, CARD_2;
schemes XBOOLE_0, NAT_1, FUNCT_1, FUNCT_2, RECDEF_1, RELSET_1, ORDERS_1,
XFAMILY;
begin :: Semilattice of type widening
registration
cluster reflexive -> complete for 1-element RelStr;
coherence;
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;
registration
cluster -> Noetherian for 1-element RelStr;
coherence
proof
let S be 1-element RelStr;
let Y be set;
set R = the InternalRel of S;
assume
A1: Y c= field R;
assume Y <> {};
then reconsider X = Y as non empty set;
set a = the Element of X;
take a;
thus a in Y;
A2: a in field R by A1;
let b be object;
A3: field R c= (the carrier of S) \/ the carrier of S by RELSET_1:8;
assume b in Y;
then b in field R by A1;
hence thesis by A2,A3,ZFMISC_1:def 10;
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 object st a in
Y & for b being object st b in Y & a <> b holds not [a,b] in R;
let A be non empty Subset of T;
set a = the 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 that
b in A and
A3: a < b;
a <= b by A3,ORDERS_2:def 6;
then [a,b] in R by ORDERS_2:def 5;
then a in field R by RELAT_1:15;
hence contradiction by A2,XBOOLE_0:3;
end;
suppose
A meets field R;
then Y <> {};
then consider x being object such that
A4: x in Y and
A5: for y being object st y in Y & x <> y holds not [x,y] in R by A1,
XBOOLE_1:17;
reconsider x as Element of T by A4;
take x;
thus x in A by A4,XBOOLE_0:def 4;
let b be Element of T;
assume that
A6: b in A and
A7: x < b;
x <= b by A7,ORDERS_2:def 6;
then
A8: [x,b] in R by ORDERS_2:def 5;
then b in field R by RELAT_1:15;
then b in Y by A6,XBOOLE_0:def 4;
hence contradiction by A5,A7,A8;
end;
end;
assume
A9: 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 that
A10: Y c= field R and
A11: Y <> {};
field R c= (the carrier of T) \/ the carrier of T by RELSET_1:8;
then reconsider A = Y as non empty Subset of T by A10,A11,XBOOLE_1:1;
consider a being Element of T such that
A12: a in A and
A13: for b being Element of T st b in A holds not a < b by A9;
take a;
thus a in Y by A12;
let b be object;
assume that
A14: b in Y and
A15: a <> b;
b in A by A14;
then reconsider b as Element of T;
not a < b by A13,A14;
then not a <= b by A15,ORDERS_2:def 6;
hence thesis by ORDERS_2:def 5;
end;
end;
definition
let T be Poset;
attr T is Mizar-widening-like means
T is sup-Semilattice & T is Noetherian;
end;
registration
cluster Mizar-widening-like -> Noetherian with_suprema upper-bounded for
Poset;
coherence
proof
let T be Poset;
assume that
A1: T is sup-Semilattice and
A2: T is Noetherian;
reconsider S = T as sup-Semilattice by A1;
the carrier of S c= the carrier of S;
then consider a being Element of T such that
a in the carrier of T and
A3: for b being Element of T st b in the carrier of T holds not a < b
by A2,Def2;
thus T is Noetherian with_suprema by A1,A2;
take a;
let b be Element of T;
A4: a"\/"b in the carrier of S;
then
A5: a"\/"b >= a by YELLOW_0:22;
not a < a"\/"b by A3,A4;
then a"\/"b = a by A5,ORDERS_2:def 6;
hence thesis by A1,YELLOW_0:22;
end;
end;
registration
cluster Noetherian -> Mizar-widening-like for sup-Semilattice;
coherence;
end;
registration
cluster Mizar-widening-like for complete sup-Semilattice;
existence
proof
set T =the 1-element LATTICE;
take T;
thus T is sup-Semilattice;
thus thesis;
end;
end;
registration
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 d in I;
then a"\/"d in I by A1,WAYBEL_0:40;
then
A4: not a < a"\/"d by A2;
a <= a"\/"d by YELLOW_0:22;
then a = a"\/"d by A4,ORDERS_2:def 6;
hence thesis by YELLOW_0:22;
end;
for c being Element of T st I is_<=_than c holds a <= c by A1;
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;
definition
let A be AdjectiveStr;
let a be Element of the adjectives of A;
func non-a -> adjective of A equals
(the non-op of A).a;
coherence
proof
per cases;
suppose
A1: the adjectives of A is empty;
then
A2: dom the non-op of A = the adjectives of A;
a = {} by A1,SUBSET_1:def 1;
hence thesis by A1,A2,FUNCT_1:def 2;
end;
suppose
the adjectives of A is non empty;
hence thesis by FUNCT_2:5;
end;
end;
end;
theorem
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;
definition
let A be AdjectiveStr;
attr A is involutive means
:Def6:
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;
a = a1 or a = a2 by A2,TARSKI:def 2;
hence non-non-a = a by A3,A4;
end;
let a be adjective of A;
assume
A5: non-a = a;
a = a1 or a = a2 by A2,TARSKI:def 2;
hence thesis by A1,A3,A4,A5;
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;
thus non-non-a = non-non-b by A1
.= 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;
hence contradiction by A2;
end;
registration
cluster non void involutive without_fixpoints for 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#);
A1: n.y = x by FUNCT_4:63;
n.x = y by FUNCT_4:63;
hence thesis by A1,Th4;
end;
end;
registration
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;
registration
let X be non empty set;
let A be set;
let r be Relation of X;
let n be UnOp of A;
let a be Function of X, Fin A;
cluster TA-structure(#X,A,r,n,a#) -> non empty;
coherence;
end;
registration
let X be set;
let A be non empty set;
let r be Relation of X;
let n be UnOp of A;
let a be Function of X, Fin A;
cluster TA-structure(#X,A,r,n,a#) -> non void;
coherence;
end;
registration
cluster 1-element reflexive non void involutive without_fixpoints
strict for TA-structure;
existence
proof
set R = the reflexive 1-element RelStr,A = the non void involutive
without_fixpoints AdjectiveStr,f = the 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 1-element by STRUCT_0:def 19;
the RelStr of R = the RelStr of T;
hence T is reflexive by WAYBEL_8:12;
thus T is 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
(the adj-map of T).t;
coherence
proof
per cases;
suppose
A1: the carrier of T is empty;
then dom the adj-map of T = the carrier of T;
then (the adj-map of T).t = {} the adjectives of T by A1,FUNCT_1:def 2;
hence thesis;
end;
suppose
the carrier of T is non empty;
then (the adj-map of T).t in Fin the adjectives of T by FUNCT_2:5;
hence thesis by FINSUB_1:16;
end;
end;
end;
theorem
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;
definition
let T be TA-structure;
attr T is consistent means
:Def9:
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 a1 = a2 as adjective of T1 by A1;
reconsider t1 = t2 as type of T1 by A1;
assume a2 in adjs t2;
then not non-a1 in adjs t1 by A1,A2;
hence thesis by A1;
end;
definition
let T be non empty TA-structure;
attr T is adj-structured means
the adj-map of T is join-preserving Function
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 Function of T1, (BoolePoset the
adjectives of T1) opp;
then reconsider f = the adj-map of T1 as join-preserving Function of T1, (
BoolePoset the adjectives of T1) opp;
reconsider g = f as Function of T2, (BoolePoset the adjectives of T2) opp by
A1;
A2: the RelStr of T1 = the RelStr of T2 by A1;
g is join-preserving
proof
let x,y be type of T2;
reconsider x9 = x, y9 = y as type of T1 by A1;
assume
A3: ex_sup_of {x,y}, T2;
then
A4: ex_sup_of {x9,y9}, T1 by A2,YELLOW_0:14;
A5: f preserves_sup_of {x9,y9} by WAYBEL_0:def 35;
hence ex_sup_of g.:{x,y}, (BoolePoset the adjectives of T2) opp by A1,A4;
sup (f.:{x9,y9}) = f.sup {x9,y9} by A4,A5;
hence thesis by A1,A2,A3,YELLOW_0:26;
end;
hence the adj-map of T2 is join-preserving Function 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
:Def11:
for t1,t2 being type of T holds adjs(t1"\/"t2) = (adjs t1) /\ (adjs t2);
compatibility
proof
A1: dom the adj-map of T = the carrier of T by FUNCT_2:def 1;
A2: Fin the adjectives of T c= bool the adjectives of T by FINSUB_1:13;
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
rng the adj-map of T c= the carrier of (BoolePoset the adjectives of T
) opp by A2;
then reconsider f = the adj-map of T as Function of T, (BoolePoset the
adjectives of T) opp by A1,FUNCT_2:2;
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 Function of T, (BoolePoset
the adjectives of T) opp;
then reconsider f = the adj-map of T as join-preserving Function of T, (
BoolePoset the adjectives of T) opp;
let t1,t2 be type of T;
thus adjs(t1"\/"t2) = (f.t1) "\/" (f.t2) by WAYBEL_6:2
.= (~(f.t1)) "/\" (~(f.t2)) by YELLOW_7:22
.= (adjs t1) /\ (adjs t2) by YELLOW_1:17;
end;
assume
A3: for t1,t2 being type of T holds adjs(t1"\/"t2) = (adjs t1) /\ ( adjs t2);
now
let t1,t2 be type of T;
thus f.(t1"\/"t2) = adjs(t1"\/"t2) .= (adjs t1)/\(adjs t2) by A3
.= (~(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 Function 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 thesis 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
:Def12:
for x being object holds x in it iff
ex t being type of T st x = t & a in adjs t;
existence
proof
defpred P[object] means ex t being type of T st $1 = t & a in adjs t;
consider tt being set such that
A1: for x being object holds x in tt iff x in the carrier of T & P[x]
from XBOOLE_0:sch 1;
tt c= the carrier of T
by A1;
then reconsider tt as Subset of T;
take tt;
let x be object;
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 and
A3: a in adjs t;
now
A4: dom the adj-map of T = the carrier of T by FUNCT_2:def 1;
assume not x in the carrier of T;
hence contradiction by A2,A3,A4,FUNCT_1:def 2;
end;
hence thesis by A1,A2,A3;
end;
uniqueness
proof
defpred P[object] means ex t being type of T st $1 = t & a in adjs t;
let X1,X2 be Subset of T such that
A5: for x being object holds x in X1 iff P[x] and
A6: for x being object holds x in X2 iff P[x];
thus thesis from XBOOLE_0:sch 2(A5,A6);
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
:Def13:
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[object] 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 object holds x in tt iff x in the carrier of T & P[x]
from XBOOLE_0:sch 1;
tt c= the carrier of T
by A1;
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 object;
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 object;
hereby
assume x in types a1;
then consider t1 being type of T1 such that
A3: x = t1 and
A4: a1 in adjs t1 by Def12;
reconsider t2 = t1 as type of T2 by A1;
adjs t1 = adjs t2 by A1;
hence ex t2 being type of T2 st x = t2 & a2 in adjs t2 by A2,A3,A4;
end;
given t2 being type of T2 such that
A5: x = t2 and
A6: a2 in adjs t2;
reconsider t1 = t2 as type of T1 by A1;
adjs t1 = adjs t2 by A1;
hence x in types a1 by A2,A5,A6,Def12;
end;
hence thesis by Def12;
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 object;
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 object
holds x in X iff ex t being type of T st x = t & a in adjs t;
hence thesis by Def12;
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 Def12;
assume t in types a;
then ex t9 being type of T st t = t9 & a in adjs t9 by Def12;
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 Def13;
end;
assume
A1: t in types a;
let x be object;
assume
A2: x in a;
then reconsider x as adjective of T;
t in types x by A1,A2,Def13;
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 object;
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 object;
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 holds types ({} the
adjectives of T) = the carrier of T
proof
let T be non empty TA-structure;
thus types ({} the adjectives of T) c= the carrier of T;
let x be object;
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 Def13;
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;
A3: types a \/ types non-a is non empty by A2;
types a = types b by A1,Th11;
hence thesis by A1,A3,Th11;
end;
registration
cluster non void Mizar-widening-like involutive without_fixpoints consistent
adj-structured adjs-typed for complete upper-bounded 1-element reflexive
transitive antisymmetric strict TA-structure;
existence
proof
{0} c= {0,1} by ZFMISC_1:7;
then reconsider A = {0} as Element of Fin {0,1} by FINSUB_1:def 5;
reconsider x = 0, y = 1 as Element of {0,1} by TARSKI:def 2;
set R =the reflexive 1-element RelStr;
reconsider n = (0,1)-->(y,x) as UnOp of {0,1};
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 1-element reflexive TA-structure by
STRUCT_0:def 19,WAYBEL_8:12;
take T;
thus T is non void;
thus T is Mizar-widening-like;
A1: n.y = x by FUNCT_4:63;
A2: n.x = y by FUNCT_4:63;
hence T is involutive without_fixpoints by A1,Th4;
hereby
let t be type of T;
let a be adjective of T;
A3: adjs t = A by FUNCOP_1:7;
a = 0 or a = 1 by TARSKI:def 2;
hence a in adjs t implies not non-a in adjs t by A2,A3,TARSKI:def 1;
end;
set t = the type of T;
hereby
let t1,t2 be type of T;
A4: adjs t2 = A by FUNCOP_1:7;
adjs t1 = A by FUNCOP_1:7;
hence adjs(t1"\/"t2) = adjs t1 /\ adjs t2 by A4,FUNCOP_1:7;
end;
let a be adjective of T;
A5: adjs t = A by FUNCOP_1:7;
a = 0 or a = 1 by TARSKI:def 2;
then a in adjs t or non-a in adjs t by A1,A5,TARSKI:def 1;
then t in types a or t in types non-a by Th13;
hence thesis;
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 object such that
A1: x in types a and
A2: x in types non-a by XBOOLE_0:3;
A3: ex t2 being type of T st x = t2 & non-a in adjs t2 by A2,Def12;
ex t1 being type of T st x = t1 & a in adjs t1 by A1,Def12;
hence thesis by A3,Def9;
end;
registration
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 that
A1: x in types a and
A2: y <= x;
A3: adjs x c= adjs y by A2,Th10;
a in adjs x by A1,Th13;
hence thesis by A3,Th13;
end;
let x,y be Element of T;
assume that
A4: x in types a and
A5: y in types a;
take x"\/"y;
A6: a in adjs y by A5,Th13;
a in adjs x by A4,Th13;
then a in (adjs x)/\adjs y by A6,XBOOLE_0:def 4;
then a in adjs(x"\/"y) by Def11;
hence thesis by Th13,YELLOW_0:22;
end;
end;
registration
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 that
A1: x in types A and
A2: y <= x;
now
let a be adjective of T;
assume a in A;
then x in types a by A1,Def13;
then
A3: a in adjs x by Th13;
adjs x c= adjs y by A2,Th10;
hence y in types a by A3,Th13;
end;
hence thesis by Def13;
end;
let x,y be Element of T;
assume that
A4: x in types A and
A5: y in types A;
take x"\/"y;
now
let a be adjective of T;
assume
A6: a in A;
then y in types a by A5,Def13;
then
A7: a in adjs y by Th13;
x in types a by A4,A6,Def13;
then a in adjs x by Th13;
then a in (adjs x)/\adjs y by A7,XBOOLE_0:def 4;
then a in adjs(x"\/"y) by Def11;
hence x"\/"y in types a by Th13;
end;
hence thesis by Def13,YELLOW_0:22;
end;
end;
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
ex t9 being type of T st t9 in types a & t9 <= 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
ex t9 being type of T st A c= adjs t9 & t9 <= t;
end;
theorem Th19:
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 t9 being type of T such that
A1: t9 in types a and
A2: t9 <= t;
t9 in downarrow t by A2,WAYBEL_0:17;
hence thesis by A1,WAYBEL_0:27,44,XBOOLE_0:def 4;
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
sup(types a /\ downarrow t);
coherence;
end;
theorem Th20:
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 Th19;
then sup (types a /\ downarrow t) in types a /\ downarrow t by Th1;
then a ast t in downarrow t by XBOOLE_0:def 4;
hence thesis by WAYBEL_0:17;
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 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 Th19;
then sup (types a /\ downarrow t) in types a /\ downarrow t by Th1;
then a ast t in types a by XBOOLE_0:def 4;
hence thesis by Th13;
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 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 Th19;
then sup (types a /\ downarrow t) in types a /\ downarrow t by Th1;
hence thesis by XBOOLE_0:def 4;
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 for t9 being type of T st t9 <= t & a in adjs t9 holds a
is_applicable_to t & t9 <= 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 t9 be type of T;
assume that
A1: t9 <= t and
A2: a in adjs t9;
A3: t9 in downarrow t by A1,WAYBEL_0:17;
thus a is_applicable_to t
by A1,A2,Th13;
then types a /\ downarrow t is Ideal of T by Th19;
then ex_sup_of types a /\ downarrow t, T by Th1;
then
A4: a ast t is_>=_than types a /\ downarrow t by YELLOW_0:30;
t9 in types a by A2,Th13;
then t9 in types a /\ downarrow t by A3,XBOOLE_0:def 4;
hence thesis by A4;
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 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;
hence a is_applicable_to t by Th23;
then
A2: a ast t <= t by Th20;
t <= a ast t by A1,Th23;
hence thesis by A2,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;
consider t9 being type of T such that
A3: t9 in types b and
A4: t9 <= a ast t by A2;
A5: b in adjs t9 by A3,Th13;
A6: a ast t <= t by A1,Th20;
thus
A7: b is_applicable_to t
by A6,A3,A4,YELLOW_0:def 2;
A8: t9 <= t by A6,A4,YELLOW_0:def 2;
thus
A9: a is_applicable_to b ast t
proof
take t9;
a ast t in types a by A1,Th22;
hence t9 in types a by A4,WAYBEL_0:def 19;
thus t9 <= b ast t by A8,A5,Th23;
end;
then
A10: a ast (b ast t) <= b ast t by Th20;
A11: a ast t in types a by A1,Th22;
A12: a ast (b ast t) is_>=_than types b /\ downarrow (a ast t)
proof
let t9 be type of T;
assume
A13: t9 in types b /\ downarrow (a ast t);
then t9 in types b by XBOOLE_0:def 4;
then
A14: b in adjs t9 by Th13;
t9 in downarrow (a ast t) by A13,XBOOLE_0:def 4;
then
A15: t9 <= a ast t by WAYBEL_0:17;
then t9 in types a by A11,WAYBEL_0:def 19;
then
A16: a in adjs t9 by Th13;
t9 <= t by A6,A15,YELLOW_0:def 2;
then t9 <= b ast t by A14,Th23;
hence thesis by A16,Th23;
end;
b ast t <= t by A7,Th20;
then
A17: a ast (b ast t) <= t by A10,YELLOW_0:def 2;
a in adjs (a ast (b ast t)) by A9,Th21;
then a ast (b ast t) <= a ast t by A17,Th23;
then
A18: a ast (b ast t) in downarrow (a ast t) by WAYBEL_0:17;
A19: a ast (b ast t) <= b ast t by A9,Th20;
b ast t in types b by A7,Th22;
then a ast (b ast t) in types b by A19,WAYBEL_0:def 19;
then a ast (b ast t) in types b /\ downarrow (a ast t) by A18,XBOOLE_0:def 4;
then for t9 being type of T st t9 is_>=_than types b /\ downarrow (a ast t)
holds a ast (b ast t) <= t9;
hence thesis by A12,YELLOW_0:30;
end;
theorem Th26:
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 t9 being type of T such that
A1: A c= adjs t9 and
A2: t9 <= t;
A3: t9 in downarrow t by A2,WAYBEL_0:17;
t9 in types A by A1,Th14;
hence thesis by A3,WAYBEL_0:27,44,XBOOLE_0:def 4;
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
sup(types A /\ downarrow t);
coherence;
end;
theorem Th27:
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 thesis 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
:Def19:
len it =
len p+1 & it.1 = t & for i being Element of 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:13;
then i in dom p by A2,FINSEQ_3:25;
then p.i in rng p by FUNCT_1:3;
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;
end;
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;
end;
consider q being FinSequence such that
A4: len q = len p+1 and
A5: q.1 = t or len p+1 = 0 and
A6: for i being Nat st 1 <= i & i < len p+1 holds P[i,q.i,
q.(i+1)] from RECDEF_1:sch 3(A1);
defpred P[Nat] means $1 in dom q implies q.$1 is type of T;
A7: now
let k be Nat such that
A8: P[k];
now
assume k+1 in dom q;
then k+1 <= len q by FINSEQ_3:25;
then
A9: k < len q by NAT_1:13;
A10: k <> 0 implies k >= 0+1 by NAT_1:13;
then
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 A4,A6,A9;
hence q.(k+1) is type of T by A5,A8,A10,A9,FINSEQ_3:25;
end;
hence P[k+1];
end;
A11: P[0] by FINSEQ_3:24;
A12: for k being Nat holds P[k] from NAT_1:sch 2(A11,A7);
rng q c= the carrier of T
proof
let a be object;
assume a in rng q;
then ex x being object st x in dom q & a = q.x by FUNCT_1:def 3;
then a is type of T by A12;
hence thesis;
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 A4,A5;
let i be Element of NAT, a be adjective of T, t being type of T;
assume that
A13: i in dom p and
A14: a = p.i and
A15: t = q.i;
i <= len p by A13,FINSEQ_3:25;
then
A16: i < len p+1 by NAT_1:13;
i >= 1 by A13,FINSEQ_3:25;
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 A6,A16;
hence thesis by A14,A15;
end;
correctness
proof
let q1, q2 be FinSequence of the carrier of T such that
A17: len q1 = len p+1 and
A18: q1.1 = t and
A19: for i being Element of 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
A20: len q2 = len p+1 and
A21: q2.1 = t and
A22: for i being Element of 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;
defpred P[Nat] means $1 in dom q1 implies q1.$1 = q2.$1;
A23: now
let i be Nat such that
A24: P[i];
now
assume i+1 in dom q1;
then
A25: i+1 <= len q1 by FINSEQ_3:25;
then
A26: i <= len q1 by NAT_1:13;
A27: i <= len p by A17,A25,XREAL_1:6;
per cases;
suppose
i = 0;
hence q1.(i+1) = q2.(i+1) by A18,A21;
end;
suppose
i > 0;
then
A28: i >= 0+1 by NAT_1:13;
then
A29: i in dom p by A27,FINSEQ_3:25;
then reconsider a = p.i as adjective of T by FINSEQ_2:11;
i in dom q1 by A26,A28,FINSEQ_3:25;
then reconsider t = q1.i as type of T by FINSEQ_2:11;
thus q1.(i+1) = a ast t by A19,A29
.= q2.(i+1) by A22,A24,A26,A28,A29,FINSEQ_3:25;
end;
end;
hence P[i+1];
end;
A30: P[0] by FINSEQ_3:25;
A31: for i being Nat holds P[i] from NAT_1:sch 2(A30,A23);
dom q1 = dom q2 by A17,A20,FINSEQ_3:29;
hence thesis by A31;
end;
end;
registration
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 Def19;
hence thesis;
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;
A1: apply(<*> the adjectives of T, t).1 = t by Def19;
len apply(<*> the adjectives of T, t) = 0+1 by Def19,CARD_1:27;
hence thesis by A1,FINSEQ_1:40;
end;
theorem Th29:
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: <*a*>.1 = a by FINSEQ_1:40;
A2: apply(<*a*>, t).1 = t by Def19;
A3: len <*a*> = 1 by FINSEQ_1:40;
then
A4: len apply(<*a*>, t) = 1+1 by Def19;
1 in dom <*a*> by A3,FINSEQ_3:25;
then apply(<*a*>, t).(len <*a*>+1) = a ast t by A3,A2,A1,Def19;
hence thesis by A3,A4,A2,FINSEQ_1:44;
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
apply(v,t).(len v+1);
coherence
proof
A1: len v+1 >= 1 by NAT_1:11;
len apply(v,t) = len v+1 by Def19;
then len v+1 in dom apply(v,t) by A1,FINSEQ_3:25;
hence thesis by FINSEQ_2:11;
end;
end;
theorem
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 by Def19;
theorem Th31:
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;
A1: len <*a*> = 1 by FINSEQ_1:40;
apply(<*a*>, t) = <*t, a ast t*> by Th29;
hence thesis by A1,FINSEQ_1:44;
end;
theorem
for p,q being FinSequence for i being Nat st i >= 1 & i <
len p holds (p$^q).i = p.i
proof
let p,q be FinSequence;
let i be Nat;
assume that
A1: i >= 1 and
A2: i < len p;
per cases;
suppose
q = {};
hence thesis by REWRITE1:1;
end;
suppose
q <> {};
then consider j being Nat, r being FinSequence such that
A3: len p = j+1 and
A4: r = p|Seg j and
A5: p$^q = r^q by A2,CARD_1:27,REWRITE1:def 1;
A6: p = r^<*p.len p*> by A3,A4,FINSEQ_3:55;
j < len p by A3,NAT_1:13;
then
A7: len r = j by A4,FINSEQ_1:17;
i <= j by A2,A3,NAT_1:13;
then
A8: i in dom r by A1,A7,FINSEQ_3:25;
then (p$^q).i = r.i by A5,FINSEQ_1:def 7;
hence thesis by A8,A6,FINSEQ_1:def 7;
end;
end;
theorem Th33:
for p being non empty FinSequence, q being FinSequence for i
being Nat 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 Nat;
A1: i+1 >= 1 by NAT_1:11;
assume
A2: i < len q;
then consider j being Nat, r being FinSequence such that
A3: len p = j+1 and
A4: r = p|Seg j and
A5: p$^q = r^q by CARD_1:27,REWRITE1:def 1;
i+1 <= len q by A2,NAT_1:13;
then
A6: i+1 in dom q by A1,FINSEQ_3:25;
j < len p by A3,NAT_1:13;
then len r = j by A4,FINSEQ_1:17;
then len p+i =len r+(i+1) by A3;
hence thesis by A5,A6,FINSEQ_1:def 7;
end;
theorem Th34:
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;
consider tt being FinSequence of the carrier of T, q being Element of T such
that
A1: apply(v1,t) = tt^<*q*> by HILBERT2:4;
set s = apply(v1, t) $^ apply(v2, v1 ast t), p = v1^v2;
A2: len apply(v1,t) = len v1+1 by Def19;
A3: apply(v1, t) $^ apply(v2, v1 ast t) = tt^apply(v2, v1 ast t) by A1,
REWRITE1:2;
len <*q*> = 1 by FINSEQ_1:39;
then
A4: len v1+1 = len tt+1 by A2,A1,FINSEQ_1:22;
A5: s.1 = t
proof
per cases;
suppose
A6: len v1 = 0;
then tt = {} by A4;
then
A7: s = apply(v2, v1 ast t) by A3,FINSEQ_1:34;
v1 ast t = t by A6,Def19;
hence thesis by A7,Def19;
end;
suppose
len v1 > 0;
then len tt >= 0+1 by A4,NAT_1:13;
then
A8: 1 in dom tt by FINSEQ_3:25;
then
A9: tt.1 = apply(v1, t).1 by A1,FINSEQ_1:def 7;
s.1 = tt.1 by A3,A8,FINSEQ_1:def 7;
hence thesis by A9,Def19;
end;
end;
A10: now
A11: len p = len v1+len v2 by FINSEQ_1:22;
A12: len apply(v2, v1 ast t) = len v2+1 by Def19;
let i be Element of NAT, a be adjective of T, t9 be type of T such that
A13: i in dom p and
A14: a = p.i and
A15: t9 = s.i;
A16: 1 <= i by A13,FINSEQ_3:25;
A17: i <= len p by A13,FINSEQ_3:25;
per cases by XXREAL_0:1;
suppose
A18: i < len v1;
A19: i+1 >= 1 by NAT_1:11;
i+1 <= len v1 by A18,NAT_1:13;
then
A20: i+1 in dom tt by A4,A19,FINSEQ_3:25;
then
A21: s.(i+1) = tt.(i+1) by A3,FINSEQ_1:def 7;
A22: i in dom tt by A4,A16,A18,FINSEQ_3:25;
then
A23: s.i = tt.i by A3,FINSEQ_1:def 7;
A24: tt.(i+1) = apply(v1, t).(i+1) by A1,A20,FINSEQ_1:def 7;
A25: tt.i = apply(v1, t).i by A1,A22,FINSEQ_1:def 7;
A26: i in dom v1 by A16,A18,FINSEQ_3:25;
then p.i = v1 .i by FINSEQ_1:def 7;
hence s.(i+1) = a ast t9 by A14,A15,A26,A23,A25,A21,A24,Def19;
end;
suppose
A27: i = len v1;
1 <= len apply(v2, v1 ast t) by A12,NAT_1:11;
then 1 in dom apply(v2, v1 ast t) by FINSEQ_3:25;
then
A28: s.(i+1) = apply(v2, v1 ast t) .1 by A3,A4,A27,FINSEQ_1:def 7;
A29: i in dom tt by A4,A16,A27,FINSEQ_3:25;
then
A30: s.i = tt.i by A3,FINSEQ_1:def 7;
A31: tt.i = apply(v1, t).i by A1,A29,FINSEQ_1:def 7;
A32: i in dom v1 by A16,A27,FINSEQ_3:25;
then p.i = v1.i by FINSEQ_1:def 7;
then a ast t9 = v1 ast t by A14,A15,A27,A32,A30,A31,Def19;
hence s.(i+1) = a ast t9 by A28,Def19;
end;
suppose
i > len v1;
then i >= len v1+1 by NAT_1:13;
then consider j being Nat such that
A33: i = len v1+1+j by NAT_1:10;
A34: 1+j+1 >= 1 by NAT_1:11;
A35: j+1+len v1+1 = j+1+1+len v1;
A36: 1+j >= 1 by NAT_1:11;
A37: i = j+1+len v1 by A33;
then
A38: 1+j <= len v2 by A17,A11,XREAL_1:6;
then 1+j+0 <= len v2+1 by XREAL_1:7;
then j+1 in dom apply(v2, v1 ast t) by A12,A36,FINSEQ_3:25;
then
A39: s.i = apply(v2, v1 ast t).(j+1) by A3,A4,A37,FINSEQ_1:def 7;
1+j+1 <= len v2+1 by A38,XREAL_1:7;
then j+1+1 in dom apply(v2, v1 ast t) by A12,A34,FINSEQ_3:25;
then
A40: s.(i+1) = apply(v2, v1 ast t).(j+1+1) by A3,A4,A33,A35,FINSEQ_1:def 7;
A41: j+1 in dom v2 by A36,A38,FINSEQ_3:25;
then p.i = v2.(j+1) by A37,FINSEQ_1:def 7;
hence s.(i+1) = a ast t9 by A14,A15,A41,A39,A40,Def19;
end;
end;
len apply(v2, v1 ast t) = len v2+1 by Def19;
then len s = len tt+(len v2+1) by A3,FINSEQ_1:22
.= len v1+len v2+1 by A4
.= len p+1 by FINSEQ_1:22;
hence thesis by A3,A5,A10,Def19;
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 for i
being Nat 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;
consider tt being FinSequence of the carrier of T, q being Element of T such
that
A1: apply(v1,t) = tt^<*q*> by HILBERT2:4;
let i be Nat;
A2: len apply(v1,t) = len v1+1 by Def19;
assume
A3: i in dom v1;
then
A4: i >= 1 by FINSEQ_3:25;
len <*q*> = 1 by FINSEQ_1:39;
then len v1+1 = len tt+1 by A2,A1,FINSEQ_1:22;
then i <= len tt by A3,FINSEQ_3:25;
then
A5: i in dom tt by A4,FINSEQ_3:25;
apply(v,t) = apply(v1,t) $^ apply(v2, v1 ast t) by Th34
.= tt^apply(v2, v1 ast t) by A1,REWRITE1:2;
then apply(v,t).i = tt.i by A5,FINSEQ_1:def 7;
hence thesis by A1,A5,FINSEQ_1:def 7;
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 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(v2, v1 ast t) = len v2+1 by Def19;
A2: apply(v,t) = apply(v1,t) $^ apply(v2, v1 ast t) by Th34;
len apply(v1,t) = len v1+1 by Def19;
then apply(v,t).(len v1+1+0) = apply(v2, v1 ast t).(0+1) by A1,A2,Th33;
hence thesis by Def19;
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
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;
consider tt being FinSequence of the carrier of T, q being Element of T such
that
A1: apply(v1,t) = tt^<*q*> by HILBERT2:4;
A2: len apply(v1,t) = len v1+1 by Def19;
len <*q*> = 1 by FINSEQ_1:39;
then
A3: len v1+1 = len tt+1 by A2,A1,FINSEQ_1:22;
A4: len v2+1 >= 1 by NAT_1:11;
len apply(v2, v1 ast t) = len v2+1 by Def19;
then
A5: len v2+1 in dom apply(v2, v1 ast t) by A4,FINSEQ_3:25;
apply(v,t) = apply(v1,t) $^ apply(v2, v1 ast t) by Th34
.= tt^apply(v2, v1 ast t) by A1,REWRITE1:2;
hence v2 ast (v1 ast t) = apply(v,t).(len tt+(len v2+1)) by A5,FINSEQ_1:def 7
.= apply(v,t).(len v1+len v2+1) by A3
.= v ast t by FINSEQ_1:22;
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
for i being Nat, 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;
theorem
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*>;
A1: v.1 = a by FINSEQ_1:40;
hereby
assume
A2: a is_applicable_to t;
thus <*a*> is_applicable_to t
proof
let i be Nat, b be adjective of T, s be type of T;
assume i in dom v;
then i in Seg 1 by FINSEQ_1:38;
then
A3: i = 1 by FINSEQ_1:2,TARSKI:def 1;
then v.i = a by FINSEQ_1:40;
hence thesis by A2,A3,Def19;
end;
end;
assume
A4: for i being Nat, a9 being adjective of T, s being type of
T st i in dom v & a9 = v.i & s = apply(v,t).i holds a9 is_applicable_to s;
len v = 1 by FINSEQ_1:40;
then
A5: 1 in dom v by FINSEQ_3:25;
apply(v,t).1 = t by Def19;
hence thesis by A4,A5,A1;
end;
theorem Th40:
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;
A1: apply(v,t) = apply(v1,t)$^apply(v2, v1 ast t) by Th34;
A2: len apply(v2, v1 ast t) = len v2+1 by Def19;
assume
A3: for i being Nat, 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
A4: dom v1 c= dom v by FINSEQ_1:26;
let i be Nat, a be adjective of T, s be type of T such that
A5: i in dom v1 and
A6: a = v1.i and
A7: s = apply(v1,t).i;
A8: a = v.i by A5,A6,FINSEQ_1:def 7;
s = apply(v,t).i by A5,A7,Th35;
hence a is_applicable_to s by A3,A5,A4,A8;
end;
let i be Nat, a be adjective of T, s be type of T such that
A9: i in dom v2 and
A10: a = v2.i and
A11: s = apply(v2, v1 ast t).i;
A12: a = v.(len v1+i) by A9,A10,FINSEQ_1:def 7;
i >= 1 by A9,FINSEQ_3:25;
then consider j being Nat such that
A13: i = 1+j by NAT_1:10;
i <= len v2 by A9,FINSEQ_3:25;
then j < len v2 by A13,NAT_1:13;
then
A14: j < len apply(v2, v1 ast t) by A2,NAT_1:13;
len apply(v1,t) = len v1+1 by Def19;
then len v1+i = len apply(v1,t)+j by A13;
then s = apply(v,t).(len v1+i) by A11,A1,A13,A14,Th33;
hence thesis by A3,A9,A12,FINSEQ_1:28;
end;
theorem Th41:
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 Nat 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 Nat, 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 Nat such that
A2: 1 <= i1 and
A3: i1 <= i2 and
A4: i2 <= len v+1;
consider j being Nat such that
A5: i2 = i1+j by A3,NAT_1:10;
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;
A6: len apply(v,t) = len v+1 by Def19;
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);
i1 <= i1+i by NAT_1:11;
then
A10: 1 <= i1+i by A2,XXREAL_0:2;
A11: i1+(i+1) = i1+i+1;
then i1+i <= len v by A6,A9,XREAL_1:6;
then
A12: i1+i in dom v by A10,FINSEQ_3:25;
then v.(i1+i) in rng v by FUNCT_1:3;
then reconsider a = v.(i1+i) as adjective of T;
i1+i < len v+1 by A6,A9,A11,NAT_1:13;
then i1+i in dom apply(v,t) by A6,A10,FINSEQ_3:25;
then apply(v,t).(i1+i) in rng apply(v,t) by FUNCT_1:3;
then reconsider s = apply(v,t).(i1+i) as type of T;
A13: apply(v,t).(i1+i+1) = a ast s by A12,Def19;
A14: a ast s <= s by A1,A12,Th20;
s <= s1 by A8,A9,A11,NAT_1:13;
hence thesis by A13,A14,YELLOW_0:def 2;
end;
assume that
A15: s1 = apply(v,t).i1 and
A16: s2 = apply(v,t).i2;
A17: P[0] by A15;
for i being Nat holds P[i] from NAT_1:sch 2(A17,A7);
hence thesis by A4,A5,A6,A16;
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 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;
A2: len apply(v,t) = len v+1 by Def19;
let s be type of T;
assume s in rng apply(v,t);
then consider x being object such that
A3: x in dom apply(v,t) and
A4: s = apply(v,t).x by FUNCT_1:def 3;
reconsider x as Element of NAT by A3;
A5: x <= len apply(v,t) by A3,FINSEQ_3:25;
A6: apply(v,t).1 = t by Def19;
x >= 1 by A3,FINSEQ_3:25;
hence thesis by A1,A4,A5,A2,A6,Th41;
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 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;
A2: len v+1 >= 1 by NAT_1:11;
len apply(v,t) = len v+1 by Def19;
then len v+1 in dom apply(v, t) by A2,FINSEQ_3:25;
then apply(v,t).(len v+1) in rng apply(v,t) by FUNCT_1:3;
hence thesis by A1,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 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 object;
assume
A2: a in rng v;
then consider x being object such that
A3: x in dom v and
A4: a = v.x by FUNCT_1:def 3;
reconsider a as adjective of T by A2;
reconsider x as Element of NAT by A3;
A5: x >= 1 by A3,FINSEQ_3:25;
then
A6: x+1 >= 1 by NAT_1:13;
A7: len apply(v,t) = len v+1 by Def19;
A8: x <= len v by A3,FINSEQ_3:25;
then x+1 <= len apply(v,t) by A7,XREAL_1:6;
then x+1 in dom apply(v,t) by A6,FINSEQ_3:25;
then
A9: apply(v,t).(x+1) in rng apply(v,t) by FUNCT_1:3;
x < len apply(v,t) by A8,A7,NAT_1:13;
then x in dom apply(v,t) by A5,FINSEQ_3:25;
then apply(v,t).x in rng apply(v,t) by FUNCT_1:3;
then reconsider s = apply(v,t).x as type of T;
a ast s = apply(v,t).(x+1) by A3,A4,Def19;
then a ast s >= v ast t by A1,A9,Th42;
then
A10: adjs (a ast s) c= adjs(v ast t) by Th10;
a is_applicable_to s by A1,A3,A4;
then a in adjs (a ast s) by Th21;
hence thesis by A10;
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 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
A1: v is_applicable_to t;
then
A2: rng v c= adjs (v ast t) by Th44;
v ast t <= t by A1,Th43;
hence thesis by A2;
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 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,v9 be FinSequence of the adjectives of T such that
A1: v is_applicable_to t and
A2: rng v9 c= rng v;
defpred P[Nat] means $1 <= len apply(v9,t) implies for s being type of T st
s = apply(v9,t).$1 holds v ast t <= s;
A3: for i being non zero Nat st P[i] holds P[i+1]
proof
A4: rng v c= adjs (v ast t) by A1,Th44;
let i be non zero Nat such that
A5: P[i] and
A6: i+1 <= len apply(v9,t);
A7: 0+1 <= i by NAT_1:13;
A8: len apply(v9,t) = len v9+1 by Def19;
then i < len v9+1 by A6,NAT_1:13;
then i in dom apply(v9,t) by A8,A7,FINSEQ_3:25;
then apply(v9,t).i in rng apply(v9,t) by FUNCT_1:3;
then reconsider s = apply(v9,t).i as type of T;
A9: v ast t <= s by A5,A6,NAT_1:13;
i <= len v9 by A6,A8,XREAL_1:6;
then
A10: i in dom v9 by A7,FINSEQ_3:25;
then
A11: v9.i in rng v9 by FUNCT_1:3;
then reconsider a = v9.i as adjective of T;
A12: a in rng v by A2,A11;
apply(v9,t).(i+1) = a ast s by A10,Def19;
hence thesis by A12,A4,A9,Th23;
end;
apply(v9,t).1 = t by Def19;
then
A13: P[1] by A1,Th43;
A14: for i being non zero Nat holds P[i] from NAT_1:sch 10(A13,A3);
let s be type of T;
assume s in rng apply(v9,t);
then consider x being object such that
A15: x in dom apply(v9,t) and
A16: s = apply(v9,t).x by FUNCT_1:def 3;
A17: x in Seg len apply(v9,t) by A15,FINSEQ_1:def 3;
reconsider x as Element of NAT by A15;
reconsider x as non zero Element of NAT by A17,FINSEQ_1:1;
x <= len apply(v9,t) by A15,FINSEQ_3:25;
hence thesis by A16,A14;
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^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;
A1: rng (v1^v2) = rng v1 \/ rng v2 by FINSEQ_1:31;
assume
A2: v1^v2 is_applicable_to t;
then
A3: rng (v1^v2) c= adjs ((v1^v2) ast t) by Th44;
let i be Nat, a be adjective of T, s be type of T such that
A4: i in dom (v2^v1) and
A5: a = (v2^v1).i and
A6: s = apply(v2^v1,t).i;
A7: a in rng (v2^v1) by A4,A5,FUNCT_1:3;
A8: len apply(v2^v1,t) = len (v2^v1)+1 by Def19;
A9: rng (v2^v1) = rng v1 \/ rng v2 by FINSEQ_1:31;
i <= len (v2^v1) by A4,FINSEQ_3:25;
then
A10: i < len (v2^v1)+1 by NAT_1:13;
i >= 1 by A4,FINSEQ_3:25;
then i in dom apply(v2^v1,t) by A10,A8,FINSEQ_3:25;
then s in rng apply(v2^v1,t) by A6,FUNCT_1:3;
then (v1^v2) ast t <= s by A2,A1,A9,Th46;
hence thesis by A1,A9,A7,A3,Th23;
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;
A2: len (v1^v2) = len v1+len v2 by FINSEQ_1:22;
A3: rng (v1^v2) = rng v1 \/ rng v2 by FINSEQ_1:31;
A4: len (v2^v1) = len v1+len v2 by FINSEQ_1:22;
A5: len (v1^v2)+1 >= 1 by NAT_1:11;
A6: rng (v2^v1) = rng v1 \/ rng v2 by FINSEQ_1:31;
len apply(v2^v1, t) = len (v2^v1)+1 by Def19;
then len (v1^v2)+1 in dom apply(v2^ v1, t) by A2,A4,A5,FINSEQ_3:25;
then v2^v1 ast t in rng apply(v2^v1, t) by A2,A4,FUNCT_1:3;
then
A7: v1^v2 ast t <= v2^v1 ast t by A1,A3,A6,Th46;
len apply(v1^v2, t) = len (v1^v2)+1 by Def19;
then len (v1^v2)+1 in dom apply(v1^v2, t) by A5,FINSEQ_3:25;
then v1^v2 ast t in rng apply(v1^v2, t) by FUNCT_1:3;
then v2^v1 ast t <= v1^v2 ast t by A1,A3,A6,Th46,Th47;
hence thesis by A7,YELLOW_0:def 3;
end;
theorem Th49:
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 Th26;
then sup (types a /\ downarrow t) in types a /\ downarrow t by Th1;
then a ast t in downarrow t by XBOOLE_0:def 4;
hence thesis by WAYBEL_0:17;
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 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 Th26;
then sup (types a /\ downarrow t) in types a /\ downarrow t by Th1;
then a ast t in types a by XBOOLE_0:def 4;
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 Th26;
then sup (types a /\ downarrow t) in types a /\ downarrow t by Th1;
hence thesis by XBOOLE_0:def 4;
end;
theorem Th52:
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 t9 being type of T st t9 <= t & A c= adjs t9
holds A is_applicable_to t & t9 <= 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 t9 be type of T;
assume that
A1: t9 <= t and
A2: a c= adjs t9;
A3: t9 in downarrow t by A1,WAYBEL_0:17;
thus a is_applicable_to t
by A1,A2;
then types a /\ downarrow t is Ideal of T by Th26;
then ex_sup_of types a /\ downarrow t, T by Th1;
then
A4: a ast t is_>=_than types a /\ downarrow t by YELLOW_0:30;
t9 in types a by A2,Th14;
then t9 in types a /\ downarrow t by A3,XBOOLE_0:def 4;
hence thesis by A4;
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;
hence a is_applicable_to t by Th52;
then
A2: a ast t <= t by Th49;
t <= a ast t by A1,Th52;
hence thesis by A2,YELLOW_0:def 3;
end;
theorem Th54:
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 t9 being type of T such that
A1: A c= adjs t9 and
A2: t9 <= t;
assume
A3: B c= A;
take t9;
thus thesis by A1,A2,A3;
end;
theorem Th55:
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} and
A2: B is_applicable_to t;
A3: A is_applicable_to t by A1,A2,Th54,XBOOLE_1:7;
A4: {a} c= B by A1,XBOOLE_1:7;
A5: A c= B by A1,XBOOLE_1:7;
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 object;
assume
A6: x in types a /\ downarrow (A ast t);
then reconsider t9 = x as type of T;
x in types a by A6,XBOOLE_0:def 4;
then a in adjs t9 by Th13;
then
A7: {a} c= adjs t9 by ZFMISC_1:31;
x in downarrow (A ast t) by A6,XBOOLE_0:def 4;
then
A8: t9 <= A ast t by WAYBEL_0:17;
then
A9: adjs (A ast t) c= adjs t9 by Th10;
A ast t <= t by A3,Th49;
then t9 <= t by A8,YELLOW_0:def 2;
then
A10: t9 in downarrow t by WAYBEL_0:17;
A c= adjs (A ast t) by A3,Th50;
then A c= adjs t9 by A9;
then B c= adjs t9 by A1,A7,XBOOLE_1:8;
then t9 in types B by Th14;
hence thesis by A10,XBOOLE_0:def 4;
end;
let x be object;
assume
A11: x in types B /\ downarrow t;
then reconsider t9 = x as type of T;
x in downarrow t by A11,XBOOLE_0:def 4;
then
A12: t9 <= t by WAYBEL_0:17;
x in types B by A11,XBOOLE_0:def 4;
then
A13: B c= adjs t9 by Th14;
then A c= adjs t9 by A5;
then t9 <= A ast t by A12,Th52;
then
A14: t9 in downarrow (A ast t) by WAYBEL_0:17;
a in B by A4,ZFMISC_1:31;
then t9 in types a by A13,Th13;
hence thesis by A14,XBOOLE_0:def 4;
end;
hence thesis;
end;
theorem Th56:
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;
let t be type of T;
let v be FinSequence of the adjectives of T;
A1: now
let n be Nat such that
A2: P[n];
now
let t be type of T, v be FinSequence of the adjectives of T such that
A3: n+1 = len v and
A4: 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 A3,FINSEQ_2:19;
reconsider B = rng v1 as Subset of the adjectives of T;
reconsider a as adjective of T;
len <*a*> = 1 by FINSEQ_1:40;
then
A6: len v = len v1+1 by A5,FINSEQ_1:22;
v1 is_applicable_to t by A4,A5,Th40;
then
A7: v1 ast t = B ast t by A2,A3,A6;
let A be Subset of the adjectives of T;
assume
A8: A = rng v;
then
A9: A = B \/ rng <*a*> by A5,FINSEQ_1:31
.= B \/ {a} by FINSEQ_1:38;
thus v ast t = <*a*> ast (v1 ast t) by A5,Th37
.= a ast (B ast t) by A7,Th31
.= A ast t by A4,A8,A9,Th45,Th55;
end;
hence P[n+1];
end;
A10: P[0]
proof
let t be type of T;
let v be FinSequence of the adjectives of T;
assume
A11: 0 = len v;
then v = <*> the adjectives of T;
then
A12: rng v = {} the adjectives of T;
v ast t = t by A11,Def19;
hence thesis by A12,Th27;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A10,A1);
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
:Def22
:
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
FUNCT_2:sch 4;
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:63;
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;
registration
cluster non void reflexive 1-element strict for TAS-structure;
existence
proof
set P = the non void reflexive 1-element TA-structure;
set s = the 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#);
the RelStr of P = the RelStr of T;
hence thesis by STRUCT_0:def 19,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
(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
by FUNCT_2:15;
assume
A1: 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 = sub non-a by FUNCT_2:15
.= sub a by A1
.= (the sub-map of T).x;
end;
hence (the sub-map of T)*(the non-op of T) = the sub-map of T by FUNCT_2:63
;
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
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
for i being Nat,
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 Th57:
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 Nat, 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 Nat, a be adjective of T, s be type of T such that
A2: i in dom v and
A3: a = v.i and
A4: s = apply(v, t).i;
a is_properly_applicable_to s by A1,A2,A3,A4;
hence thesis;
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;
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*>;
A1: v.1 = a by FINSEQ_1:40;
hereby
assume
A2: a is_properly_applicable_to t;
thus <*a*> is_properly_applicable_to t
proof
let i be Nat, b be adjective of T, s be type of T;
assume i in dom v;
then i in Seg 1 by FINSEQ_1:38;
then
A3: i = 1 by FINSEQ_1:2,TARSKI:def 1;
then v.i = a by FINSEQ_1:40;
hence thesis by A2,A3,Def19;
end;
end;
assume
A4: for i being Nat, a9 being adjective of T, s being type of
T st i in dom v & a9 = v.i & s = apply(v,t).i holds a9
is_properly_applicable_to s;
len v = 1 by FINSEQ_1:40;
then
A5: 1 in dom v by FINSEQ_3:25;
apply(v,t).1 = t by Def19;
hence thesis by A4,A5,A1;
end;
theorem Th60:
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;
A1: apply(v,t) = apply(v1,t)$^apply(v2, v1 ast t) by Th34;
A2: len apply(v2, v1 ast t) = len v2+1 by Def19;
assume
A3: for i being Nat, 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
A4: dom v1 c= dom v by FINSEQ_1:26;
let i be Nat, a be adjective of T, s be type of T such that
A5: i in dom v1 and
A6: a = v1.i and
A7: s = apply(v1,t).i;
A8: a = v.i by A5,A6,FINSEQ_1:def 7;
s = apply(v,t).i by A5,A7,Th35;
hence a is_properly_applicable_to s by A3,A5,A4,A8;
end;
let i be Nat, a be adjective of T, s be type of T such that
A9: i in dom v2 and
A10: a = v2.i and
A11: s = apply(v2, v1 ast t).i;
A12: a = v.(len v1+i) by A9,A10,FINSEQ_1:def 7;
i >= 1 by A9,FINSEQ_3:25;
then consider j being Nat such that
A13: i = 1+j by NAT_1:10;
i <= len v2 by A9,FINSEQ_3:25;
then j < len v2 by A13,NAT_1:13;
then
A14: j < len apply(v2, v1 ast t) by A2,NAT_1:13;
len apply(v1,t) = len v1+1 by Def19;
then len v1+i = len apply(v1,t)+j by A13;
then s = apply(v,t).(len v1+i) by A11,A1,A13,A14,Th33;
hence thesis by A3,A9,A12,FINSEQ_1:28;
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 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 Nat, 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 Nat, 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;
A3: apply(v,t) = apply(v1,t)$^apply(v2, v1 ast t) by Th34;
let i be Nat, a be adjective of T, s be type of T such that
A4: i in dom v and
A5: a = v.i and
A6: s = apply(v, t).i;
A7: i >= 1 by A4,FINSEQ_3:25;
A8: i <= len v by A4,FINSEQ_3:25;
per cases;
suppose
i <= len v1;
then
A9: i in dom v1 by A7,FINSEQ_3:25;
then
A10: a = v1.i by A5,FINSEQ_1:def 7;
s = apply(v1,t).i by A6,A9,Th35;
hence thesis by A1,A9,A10;
end;
suppose
i > len v1;
then i >= 1+len v1 by NAT_1:13;
then consider j being Nat such that
A11: i = len v1+1+j by NAT_1:10;
A12: len apply(v2, v1 ast t) = len v2+1 by Def19;
A13: len v = len v1+len v2 by FINSEQ_1:22;
A14: len apply(v1,t) = len v1+1 by Def19;
i = len v1+(j+1) by A11;
then
A15: j+1 <= len v2 by A8,A13,XREAL_1:6;
then j < len v2 by NAT_1:13;
then j < len apply(v2, v1 ast t) by A12,NAT_1:13;
then
A16: s = apply(v2,v1 ast t).(1+j) by A6,A3,A11,A14,Th33;
j+1 >= 1 by NAT_1:11;
then
A17: j+1 in dom v2 by A15,FINSEQ_3:25;
len v1+(j+1) = len apply(v1,t)+j by A14;
then a = v2.(1+j) by A5,A11,A17,FINSEQ_1:def 7;
hence thesis by A2,A17,A16;
end;
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
ex s being FinSequence of
the adjectives of T st rng s = A & s is_properly_applicable_to t;
end;
theorem
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;
theorem Th63:
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 Nat;
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 R[set,set] means $1 c= $2;
consider Y being set such that
A3: for x being set holds x in Y iff x in bool A & P[x] from XFAMILY:
sch 1;
A c= A;
then reconsider Y as non empty set by A2,A3;
Y c= bool A
by A3;
then reconsider Y as finite non empty set;
A4: for x,y being Element of Y st R[x,y] & R[y,x] holds x = y;
A5: for x,y,z being Element of Y st R[x,y] & R[y,z] holds R[x,z] by XBOOLE_1:1;
A6: 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
A7: X c= Y and
A8: 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
A9: X = {};
set y = the Element of Y;
take y;
thus thesis by A9;
end;
suppose
A10: X <> {};
set x0 = the Element of X;
x0 in X by A10;
then reconsider x0 as Element of Y by A7;
deffunc F(set) = card {y where y is Element of Y: y in X & y c< $1};
consider f being Function such that
A11: dom f = X & for x being set st x in X holds f.x = F(x) from
FUNCT_1:sch 5;
defpred P[Nat] means ex x being Element of Y st x in X & $1 = f.x;
A12: for k being Nat st k<>0 & P[k] ex n being Nat st n 0;
given x being Element of Y such that
A14: x in X and
A15: k = f.x;
set fx = {a where a is Element of Y: a in X & a c< x};
fx c= Y
proof
let a be object;
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;
A16: k = card fx by A11,A14,A15;
set A = {z where z is Element of Y: z in X & z c< x};
reconsider A as non empty set by A11,A13,A14,A15,CARD_1:27;
set z = the Element of A;
z in A;
then consider y being Element of Y such that
A17: z = y and
A18: y in X and
A19: 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 object;
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;
reconsider n = card fx0 as Element of NAT;
take n;
not ex a being Element of Y st y = a & a in X & a c< y;
then
A20: not y in fx0;
A21: y in fx by A17;
A22: fx0 c= fx
proof
let a be object;
assume a in fx0;
then consider b being Element of Y such that
A23: a = b and
A24: b in X and
A25: b c< y;
b c< x by A19,A25,XBOOLE_1:56;
hence thesis by A23,A24;
end;
then Segm card fx0 c= Segm card fx by CARD_1:11;
then n <= k by A16,NAT_1:39;
hence n < k by A16,A22,A21,A20,CARD_2:102,XXREAL_0:1;
take y;
thus thesis by A11,A18;
end;
set fx0 = {y where y is Element of Y: y in X & y c< x0};
fx0 c= Y
proof
let a be object;
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;
f.x0 = card fx0 by A10,A11;
then
A26: ex n being Nat st P[n] by A10;
P[0] from NAT_1:sch 7(A26,A12);
then consider y being Element of Y such that
A27: y in X and
A28: 0 = f.y;
take y;
let x be Element of Y;
assume
A29: x in X;
then x c= y or y c= x by A8,A27;
then x c< y or y c= x;
then
A30: x in {z where z is Element of Y: z in X & z c< y} or y c= x by A29;
f.y = card {z where z is Element of Y: z in X & z c< y} by A11,A27;
hence thesis by A28,A30;
end;
end;
A31: for x being Element of Y holds R[x,x];
consider x being Element of Y such that
A32: for y being Element of Y st x <> y holds not R[y,x] from ORDERS_1:
sch 2(A31,A4,A5,A6);
x in bool A by A3;
then reconsider x as finite set;
take x;
thus P[x] by A3;
let B be set;
assume that
A33: B c= x and
A34: P[B];
x in bool A by A3;
then B c= A by A33,XBOOLE_1:1;
then B in Y by A3,A34;
hence thesis by A32,A33;
end;
theorem Th64:
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
A1: A is_properly_applicable_to t;
A2: ex a being finite set st P[a] by A1;
consider B being finite set such that
A3: P[B] and
A4: for C being set st C c= B & P[C] holds C = B from MinimalFiniteSet(
A2);
reconsider B as Subset of the adjectives of T by A3;
take B;
thus B c= A & B is_properly_applicable_to t & A ast t = B ast t by A3;
let C be Subset of the adjectives of T;
assume
A5: C c= B;
then C c= A by A3,XBOOLE_1:1;
hence thesis by A4,A5;
end;
definition
let T be non empty non void reflexive transitive TAS-structure;
attr T is commutative means
:Def30:
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;
registration
cluster Mizar-widening-like involutive without_fixpoints consistent
adj-structured adjs-typed non-absorbing subjected commutative for complete
upper-bounded non void 1-element reflexive transitive antisymmetric
strict TAS-structure;
existence
proof
set P = the non void Mizar-widening-like involutive without_fixpoints
consistent adj-structured adjs-typed 1-element 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#);
the RelStr of P = the RelStr of T;
then reconsider
T as non void 1-element reflexive strict TAS-structure
by Def4,STRUCT_0:def 19,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;
hereby
let a be adjective of T;
reconsider b = a as adjective of P;
thus sub non-a = sup (types non-b \/ types non-non-b) by Def22
.= sup (types non-b \/ types b) by Def6
.= sub a by Def22;
end;
A1: the RelStr of P = the RelStr of T;
thus T is subjected
proof
let a be adjective of T;
reconsider b = a as adjective of P;
A2: types non-a = types non-b by Th11;
types a = types b by Th11;
then sup (types a \/ types non-a) = sup (types b \/ types non-b) by A1,A2
,YELLOW_0:17,26;
then sup (types a \/ types non-a) = sub a by Def22;
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 and
a ast t1 <= t2;
take A = {} the adjectives of T;
thus A is_properly_applicable_to t1 "\/" t2 by Th63;
thus A ast (t1 "\/" t2) = t2 by STRUCT_0:def 10;
end;
end;
theorem Th65:
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 s9 being FinSequence of the adjectives of T such that
A1: rng s9 = A and
A2: s9 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 s9 = len s9;
then
A3: ex k being Nat st P[k] by A1,A2;
consider k being Nat such that
A4: P[k] and
A5: for n being Nat st P[n] holds k <= n from NAT_1:sch 5(A3);
consider s being FinSequence of the adjectives of T such that
A6: k = len s and
A7: rng s = A and
A8: s is_properly_applicable_to t by A4;
s is one-to-one
proof
let x,y be object;
assume that
A9: x in dom s and
A10: y in dom s and
A11: s.x = s.y and
A12: x <> y;
reconsider x,y as Element of NAT by A9,A10;
x < y or x > y by A12,XXREAL_0:1;
then consider x,y being Element of NAT such that
A13: x in dom s and
A14: y in dom s and
A15: x < y and
A16: s.x = s.y by A9,A10,A11;
A17: x >= 1 by A13,FINSEQ_3:25;
y >= 1 by A14,FINSEQ_3:25;
then consider i being Nat such that
A18: y = 1+i by NAT_1:10;
reconsider i as Element of NAT by ORDINAL1:def 12;
reconsider s1 = s|Seg i as FinSequence of the adjectives of T by
FINSEQ_1:18;
A19: y <= len s by A14,FINSEQ_3:25;
then i <= len s by A18,NAT_1:13;
then
A20: len s1 = i by FINSEQ_1:17;
x <= i by A15,A18,NAT_1:13;
then
A21: x in dom s1 by A20,A17,FINSEQ_3:25;
s1 c= s by TREES_1:def 1;
then consider s2 being FinSequence such that
A22: s = s1^s2 by TREES_1:1;
reconsider s2 as FinSequence of the adjectives of T by A22,FINSEQ_1:36;
A23: len s = len s1+len s2 by A22,FINSEQ_1:22;
then
A24: len s2 >= 1 by A18,A19,A20,XREAL_1:6;
then
A25: 1 in dom s2 by FINSEQ_3:25;
reconsider s21 = s2|Seg 1 as FinSequence of the adjectives of T by
FINSEQ_1:18;
s21 c= s2 by TREES_1:def 1;
then consider s22 being FinSequence such that
A26: s2 = s21^s22 by TREES_1:1;
reconsider s22 as FinSequence of the adjectives of T by A26,FINSEQ_1:36;
A27: len s21 = 1 by A24,FINSEQ_1:17;
then
A28: s21 = <*s21.1*> by FINSEQ_1:40;
then
A29: rng s21 = {s21.1} by FINSEQ_1:39;
then reconsider a = s21.1 as adjective of T by ZFMISC_1:31;
A30: rng s2 = rng s21 \/ rng s22 by A26,FINSEQ_1:31;
a = s2.1 by A28,A26,FINSEQ_1:41
.= s.y by A18,A22,A20,A25,FINSEQ_1:def 7;
then a = s1.x by A16,A22,A21,FINSEQ_1:def 7;
then
A31: a in rng s1 by A21,FUNCT_1:3;
then rng s21 c= rng s1 by A29,ZFMISC_1:31;
then rng s1 \/ rng s21 = rng s1 by XBOOLE_1:12;
then
A32: rng (s1^s22) = rng s1 \/ rng s21 \/ rng s22 by FINSEQ_1:31;
A33: s2 is_properly_applicable_to s1 ast t by A8,A22,Th60;
A34: s1 is_properly_applicable_to t by A8,A22,A23,Th60;
then rng s1 c= adjs (s1 ast t) by Th44,Th57;
then s1 ast t = a ast (s1 ast t) by A31,Th24
.= s21 ast (s1 ast t) by A28,Th31;
then s22 is_properly_applicable_to s1 ast t by A26,A33,Th60;
then
A35: s1^s22 is_properly_applicable_to t by A34,Th61;
A36: len s2 = len s21+len s22 by A26,FINSEQ_1:22;
rng s = rng s1 \/ rng s2 by A22,FINSEQ_1:31;
then k <= len (s1^s22) by A5,A7,A35,A32,A30,XBOOLE_1:4;
then k <= len s1+len s22 by FINSEQ_1:22;
then len s21+len s22 <= 0+len s22 by A6,A23,A36,XREAL_1:6;
hence thesis by A27,XREAL_1:6;
end;
hence thesis by A7,A8;
end;
begin :: Reduction of adjectives
definition
let T be non empty non void reflexive transitive TAS-structure;
func T @--> -> Relation of T means
:Def31:
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
RELSET_1:sch 2;
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;
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;
end;
theorem Th66:
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 Def31;
a is_applicable_to q2 by A1;
then q1 <= q2 by A2,Th20;
hence thesis by ORDERS_2:def 5;
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 and
A5: p.len p = y;
defpred P[Nat] means 1+$1 <= len p implies P[x, p.(1+$1)];
A6: now
let i be Nat such that
A7: P[i];
now
A8: i+1 >= 1 by NAT_1:11;
assume
A9: 1+(i+1) <= len p;
1+(i+1) >= 1 by NAT_1:11;
then
A10: 1+(i+1) in dom p by A9,FINSEQ_3:25;
i+1 < len p by A9,NAT_1:13;
then i+1 in dom p by A8,FINSEQ_3:25;
then
A11: [p.(i+1), p.(1+(i+1))] in R() by A10,REWRITE1:def 2;
then
A12: p.(1+(i+1)) in X() by ZFMISC_1:87;
A13: p.(i+1) in X() by A11,ZFMISC_1:87;
then P[p.(i+1), p.(1+(i+1))] by A1,A11,A12;
hence P[x, p.(1+(i+1))] by A3,A7,A9,A13,A12,NAT_1:13;
end;
hence P[i+1];
end;
A14: P[0] by A2,A4;
A15: for n being Nat holds P[n] from NAT_1:sch 2(A14,A6);
len p >= 0+1 by NAT_1:13;
then consider n being Nat such that
A16: len p = 1+n by NAT_1:10;
thus thesis by A5,A16,A15;
end;
theorem Th67:
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: for x,y,z be Element of T holds P[x, y] & P[y, z] implies P[x, z] by
YELLOW_0:def 2;
A2: now
let x,y be Element of T;
R c= the InternalRel of T by Th66;
hence [x,y] in R implies P[x, y] by ORDERS_2:def 5;
end;
A3: for x being Element of T holds P[x, x];
for x,y being Element of T st R reduces x,y holds P[x,y] from RedInd(A2,
A3,A1);
hence thesis;
end;
theorem Th68:
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 object;
assume x in field R;
assume
A1: [x,x] in R;
then reconsider x as type of T by ZFMISC_1:87;
consider a being adjective of T such that
A2: not a in adjs x and
A3: a is_properly_applicable_to x and
A4: a ast x = x by A1,Def31;
a is_applicable_to x by A3;
hence thesis by A2,A4,Th21;
end;
theorem Th69:
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: field R c= field Q by Th66,RELAT_1:16;
A2: R c= Q by Th66;
R is co-well_founded
proof
let Y be set;
assume that
A3: Y c= field R and
A4: Y <> {};
Y c= field Q by A1,A3;
then consider a being object such that
A5: a in Y and
A6: for b being object st b in Y & a <> b holds not [a,b] in Q by A4,
REWRITE1:def 16;
take a;
thus thesis by A2,A5,A6;
end;
then R is irreflexive co-well_founded Relation by Th68;
hence thesis;
end;
theorem Th70:
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 Nat 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 and
A3: s is_properly_applicable_to t;
let j be Nat;
assume that
A4: 1 <= j and
A5: j <= len s;
A6: len apply(s, t) = len s+1 by Def19;
j < len s+1 by A5,NAT_1:13;
then j in dom apply(s, t) by A6,A4,FINSEQ_3:25;
then apply(s, t).j in rng apply(s, t) by FUNCT_1:3;
then reconsider tt = apply(s, t).j as type of T;
A7: j in dom s by A4,A5,FINSEQ_3:25;
then s.j in rng s by FUNCT_1:3;
then reconsider a = s.j as adjective of T;
A8: apply(s, t).(j+1) = a ast tt by A7,Def19;
A9: not a in adjs tt
proof
assume
A10: a in adjs tt;
consider i being Nat such that
A11: j = 1+i by A4,NAT_1:10;
reconsider i as Element of NAT by ORDINAL1:def 12;
reconsider s1 = s|Seg i as FinSequence of the adjectives of T by
FINSEQ_1:18;
s1 c= s by TREES_1:def 1;
then consider s2 being FinSequence such that
A12: s = s1^s2 by TREES_1:1;
reconsider s2 as FinSequence of the adjectives of T by A12,FINSEQ_1:36;
A13: len s = len s1+len s2 by A12,FINSEQ_1:22;
then
A14: s1 is_properly_applicable_to t by A3,A12,Th60;
reconsider s21 = s2|Seg 1 as FinSequence of the adjectives of T by
FINSEQ_1:18;
i <= len s by A5,A11,NAT_1:13;
then
A15: len s1 = i by FINSEQ_1:17;
then
A16: len s2 >= 1 by A5,A11,A13,XREAL_1:6;
then
A17: len s21 = 1 by FINSEQ_1:17;
then
A18: s21 = <*s21.1*> by FINSEQ_1:40;
then
A19: rng s21 = {s21.1} by FINSEQ_1:39;
then reconsider b = s21.1 as adjective of T by ZFMISC_1:31;
A20: 1 in dom s2 by A16,FINSEQ_3:25;
s21 c= s2 by TREES_1:def 1;
then consider s22 being FinSequence such that
A21: s2 = s21^s22 by TREES_1:1;
reconsider s22 as FinSequence of the adjectives of T by A21,FINSEQ_1:36;
A22: rng s2 = rng s21 \/ rng s22 by A21,FINSEQ_1:31;
then
A23: rng s22 c= rng s2 by XBOOLE_1:7;
A24: b = s2.1 by A18,A21,FINSEQ_1:41
.= a by A11,A12,A15,A20,FINSEQ_1:def 7;
then a in rng s21 by A19,TARSKI:def 1;
then
A25: a in rng s2 by A22,XBOOLE_0:def 3;
s1 ast t = tt by A11,A12,A13,A15,Th36;
then
A26: s1 ast t = a ast (s1 ast t) by A10,Th24
.= s21 ast (s1 ast t) by A18,A24,Th31;
s2 is_properly_applicable_to s1 ast t by A3,A12,Th60;
then s22 is_properly_applicable_to s1 ast t by A21,A26,Th60;
then
A27: s1^s22 is_properly_applicable_to t by A14,Th61;
reconsider B = rng (s1^s22) as Subset of the adjectives of T;
A28: B = rng s1 \/ rng s22 by FINSEQ_1:31;
A29: A = rng s1 \/ rng s2 by A2,A12,FINSEQ_1:31;
s ast t = s2 ast (s1 ast t) by A12,Th37
.= s22 ast (s1 ast t) by A21,A26,Th37
.= s1^s22 ast t by Th37;
then
A30: A ast t = s1^s22 ast t by A2,A3,Th56,Th57
.= B ast t by A27,Th56,Th57;
B is_properly_applicable_to t by A27;
then B = A by A1,A30,A28,A29,A23,XBOOLE_1:9;
then
A31: a in B by A29,A25,XBOOLE_0:def 3;
per cases by A28,A31,XBOOLE_0:def 3;
suppose
a in rng s1;
then consider x being object such that
A32: x in dom s1 and
A33: a = s1.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A32;
x <= len s1 by A32,FINSEQ_3:25;
then
A34: x < j by A11,A15,NAT_1:13;
A35: dom s1 c= dom s by A12,FINSEQ_1:26;
s.x = a by A12,A32,A33,FINSEQ_1:def 7;
hence contradiction by A7,A32,A35,A34,FUNCT_1:def 4;
end;
suppose
a in rng s22;
then consider x being object such that
A36: x in dom s22 and
A37: a = s22.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A36;
A38: 1+x in dom s2 by A17,A21,A36,FINSEQ_1:28;
x >= 0+1 by A36,FINSEQ_3:25;
then
A39: j+x > j+0 by XREAL_1:6;
s2.(1+x) = a by A17,A21,A36,A37,FINSEQ_1:def 7;
then
A40: s.(i+(1+x)) = a by A12,A15,A38,FINSEQ_1:def 7;
i+(1+x) in dom s by A12,A15,A38,FINSEQ_1:28;
hence contradiction by A7,A11,A39,A40,FUNCT_1:def 4;
end;
end;
a is_properly_applicable_to tt by A3,A7;
hence thesis by A8,A9,Def31;
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 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 and
A3: s is_properly_applicable_to t;
A4: len Rev apply(s, t) = len apply(s, t) by FINSEQ_5:def 3;
hence len Rev apply(s, t) > 0;
let i be Nat;
assume that
A5: i in dom Rev apply(s, t) and
A6: i+1 in dom Rev apply(s, t);
A7: len apply(s, t) = len s+1 by Def19;
then
A8: (Rev apply(s, t)).i = apply(s, t).(len s+1 -i +1) by A5,FINSEQ_5:def 3;
i+1 <= len s+1 by A4,A7,A6,FINSEQ_3:25;
then consider j being Nat such that
A9: len s+1 = i+1+j by NAT_1:10;
A10: (Rev apply(s, t)).(i+1) = apply(s, t).(len s+1-(i+1)+1) by A7,A6,
FINSEQ_5:def 3;
A11: i >= 1 by A5,FINSEQ_3:25;
len s = i+j by A9;
then
A12: j+1 <= len s by A11,XREAL_1:6;
j+1 >= 1 by NAT_1:11;
hence thesis by A1,A2,A3,A8,A10,A9,A12,Th70;
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 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;
set R = T@-->;
let t be type of T, A be finite Subset of the adjectives of T;
assume A is_properly_applicable_to t;
then consider A9 being Subset of the adjectives of T such that
A9 c= A and
A1: A9 is_properly_applicable_to t and
A2: A ast t = A9 ast t and
A3: for C being Subset of the adjectives of T st C c= A9 & C
is_properly_applicable_to t & A ast t = C ast t holds C = A9 by Th64;
consider s being one-to-one FinSequence of the adjectives of T such that
A4: rng s = A9 and
A5: s is_properly_applicable_to t by A1,Th65;
reconsider p = Rev apply(s, t) as RedSequence of R by A2,A3,A4,A5,Th71;
take p;
thus p.1 = apply(s, t).len apply(s, t) by FINSEQ_5:62
.= s ast t by Def19
.= A ast t by A2,A4,A5,Th56,Th57;
thus p.len p = p.len apply(s, t) by FINSEQ_5:def 3
.= apply(s, t).1 by FINSEQ_5:62
.= t by Def19;
end;
theorem Th73:
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 object;
assume x in rng p;
then consider i being object such that
A2: i in dom p and
A3: x = p.i by FUNCT_1:def 3;
reconsider i as Element of NAT by A2;
A4: i >= 1 by A2,FINSEQ_3:25;
per cases by A4,XXREAL_0:1;
suppose
i = 1;
hence thesis by A1,A3;
end;
suppose
i > 1;
then i >= 1+1 by NAT_1:13;
then consider j being Nat such that
A5: i = 1+1+j by NAT_1:10;
A6: i = j+1+1 by A5;
A7: j+1 >= 1 by NAT_1:11;
i <= len p by A2,FINSEQ_3:25;
then j+1 < len p by A6,NAT_1:13;
then j+1 in dom p by A7,FINSEQ_3:25;
then [p.(j+1), x] in R by A2,A3,A6,REWRITE1:def 2;
hence thesis by ZFMISC_1:87;
end;
end;
theorem Th74:
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 and
A2: p.len p = y;
len p >= 0+1 by NAT_1:13;
then len p in dom p by FINSEQ_3:25;
then
A3: y in rng p by A2,FUNCT_1:3;
p is FinSequence of X by A1,Th73;
then rng p c= X by FINSEQ_1:def 4;
hence thesis by A3;
end;
theorem Th75:
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:54;
then R reduces x, nf(x,R);
hence thesis by Th74;
end;
theorem Th76:
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 and
A2: t2 = p.len p;
defpred P[object,object] means
ex j being Element of 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;
A3: len Rev p = len p by FINSEQ_5:def 3;
A4: len p-1+1 = len p;
A5: len p >= 0+1 by NAT_1:13;
then consider i being Nat such that
A6: len p = 1+i by NAT_1:10;
reconsider i as Element of NAT by ORDINAL1:def 12;
A7: now
let x be object;
assume
A8: x in Seg i;
then reconsider j = x as Element of NAT;
A9: j >= 1 by A8,FINSEQ_1:1;
then
A10: 1 <= j+1 by NAT_1:13;
A11: j <= i by A8,FINSEQ_1:1;
then j < len p by A6,NAT_1:13;
then
A12: j in dom p by A9,FINSEQ_3:25;
j+1 <= len p by A6,A11,XREAL_1:6;
then j+1 in dom p by A10,FINSEQ_3:25;
then
A13: [p.j, p.(j+1)] in R by A12,REWRITE1:def 2;
then reconsider q1 = p.j, q2 = p.(j+1) as type of T by ZFMISC_1:87;
ex a being adjective of T st not a in adjs q2 & a
is_properly_applicable_to q2 & a ast q2 = q1 by A13,Def31;
hence ex y being object st y in the adjectives of T & P[x,y];
end;
consider f being Function such that
A14: dom f = Seg i & rng f c= the adjectives of T and
A15: for x being object st x in Seg i holds P[x,f.x] from FUNCT_1:sch 6(A7);
f is FinSequence by A14,FINSEQ_1:def 2;
then reconsider f as FinSequence of the adjectives of T by A14,FINSEQ_1:def 4
;
A16: len f = i by A14,FINSEQ_1:def 3;
set r = Rev f;
defpred P[Nat] means 1+$1 <= len p implies (Rev p).(1+$1) = apply
(r, t2).(1+$1);
A17: len r = len f by FINSEQ_5:def 3;
A18: now
let j be Nat such that
A19: P[j];
now
A20: j+1 >= 1 by NAT_1:11;
assume
A21: 1+(j+1) <= len p;
then j+1 <= i by A6,XREAL_1:6;
then consider x being Nat such that
A22: i = j+1+x by NAT_1:10;
reconsider x as Element of NAT by ORDINAL1:def 12;
A23: i+1-(j+1) = x+1 by A22;
j+1 < len p by A21,NAT_1:13;
then j+1 in dom Rev p by A3,A20,FINSEQ_3:25;
then
A24: (Rev p).(j+1) = p.(x+1+1) by A6,A23,FINSEQ_5:def 3;
A25: i+1-(1+(j+1)) = x by A22;
1+(j+1) >= 1 by NAT_1:11;
then 1+(j+1) in dom Rev p by A3,A21,FINSEQ_3:25;
then
A26: (Rev p).(1+(j+1)) = p.(x+1) by A6,A25,FINSEQ_5:def 3;
i = x+1+j by A22;
then
A27: i >= x+1 by NAT_1:11;
x+1 >= 1 by NAT_1:11;
then x+1 in Seg i by A27;
then consider
k being Element of NAT, a being adjective of T, t being type of
T such that
A28: f.(x+1) = a and
A29: x+1 = k and
A30: a ast t = p.k and
A31: t = p.(k+1) and
a is_properly_applicable_to t by A15;
A32: j+1 >= 1 by NAT_1:11;
j+1 <= i by A22,NAT_1:11;
then
A33: j+1 in dom r by A17,A16,A32,FINSEQ_3:25;
then r.(j+1) = f.(len f-(j+1)+1) by FINSEQ_5:def 3
.= a by A16,A22,A28;
hence (Rev p).(1+(j+1)) = apply(r, t2).(1+(j+1)) by A19,A21,A29,A30,A31
,A33,A24,A26,Def19,NAT_1:13;
end;
hence P[j+1];
end;
reconsider A = rng f as finite Subset of the adjectives of T;
take A;
A34: len apply(r, t2) = len r+1 by Def19;
1 in dom Rev p by A5,A3,FINSEQ_3:25;
then (Rev p).1 = t2 by A2,A4,FINSEQ_5:def 3;
then
A35: P[0] by Def19;
A36: for j being Nat holds P[j] from NAT_1:sch 2(A35,A18);
now
let j be Nat;
assume 1 <= j;
then consider k being Nat such that
A37: j = 1+k by NAT_1:10;
thus j <= len p implies (Rev p).j = apply(r, t2).j by A36,A37;
end;
then
A38: Rev p = apply(r, t2) by A6,A17,A34,A16,A3;
then
A39: p = Rev apply(r, t2);
A40: r is_properly_applicable_to t2
proof
let j be Nat, a be adjective of T, s be type of T;
assume that
A41: j in dom r and
A42: a = r.j and
A43: s = apply(r,t2).j;
j <= len r by A41,FINSEQ_3:25;
then consider k being Nat such that
A44: len r = j+k by NAT_1:10;
A45: len r = len f by FINSEQ_5:def 3;
reconsider k as Element of NAT by ORDINAL1:def 12;
A46: k+1 >= 1 by NAT_1:11;
A47: j >= 1 by A41,FINSEQ_3:25;
then k+1 <= i by A16,A44,A45,XREAL_1:6;
then len f-j+1 in Seg i by A44,A45,A46;
then consider
o being Element of NAT, b being adjective of T, u being type of T
such that
A48: f.(len f-j+1) = b and
A49: len f-j+1 = o and
b ast u = p.o and
A50: u = p.(o+1) and
A51: b is_properly_applicable_to u by A15;
A52: o+1 >= 1 by NAT_1:11;
i+1 = k+1+j by A17,A16,A44;
then o+1 <= len p by A6,A44,A45,A47,A49,XREAL_1:6;
then
A53: o+1 in dom p by A52,FINSEQ_3:25;
A54: a = b by A41,A42,A48,FINSEQ_5:def 3;
len (apply(r, t2))-(o+1)+1 = j by A17,A34,A49;
hence thesis by A39,A43,A50,A51,A53,A54,FINSEQ_5:def 3;
end;
thus A is_properly_applicable_to t2
proof
take r;
thus thesis by A40,FINSEQ_5:57;
end;
rng r = A by FINSEQ_5:57;
then A ast t2 = r ast t2 by A40,Th56,Th57
.= apply(r, t2).(len r+1);
hence thesis by A1,A34,A3,A38,FINSEQ_5:62;
end;
theorem Th77:
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 object;
assume that
A1: [a,b] in R and
A2: [a,c] in R;
reconsider t = a, t1 = b, t2 = c as type of T by A1,A2,ZFMISC_1:87;
consider a2 being adjective of T such that
not a2 in adjs t1 and
A3: a2 is_properly_applicable_to t1 and
A4: a2 ast t1 = t by A1,Def31;
set tt = t1 "\/" t2;
take tt;
consider a3 being adjective of T such that
not a3 in adjs t2 and
A5: a3 is_properly_applicable_to t2 and
A6: a3 ast t2 = t by A2,Def31;
a3 is_applicable_to t2 by A5;
then t <= t2 by A6,Th20;
then
A7: ex B being finite Subset of the adjectives of T st B
is_properly_applicable_to t1 "\/" t2 & B ast (t1 "\/" t2) = t2 by A3,A4
,Def30;
a2 is_applicable_to t1 by A3;
then t <= t1 by A4,Th20;
then ex A being finite Subset of the adjectives of T st A
is_properly_applicable_to t1 "\/" t2 & A ast (t1 "\/" t2) = t1 by A5,A6
,Def30;
hence thesis by A7,Th72;
end;
then R is strongly-normalizing locally-confluent Relation by Th69;
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
nf(t, T@-->);
coherence
proof
T@--> is with_Church-Rosser_property with_UN_property
strongly-normalizing Relation by Th69,Th77;
hence thesis by Th75;
end;
end;
theorem Th78:
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 Th69,Th77;
then nf(t, R) is_a_normal_form_of t, R by REWRITE1:54;
hence thesis;
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 holds t <= radix t by Th67,Th78;
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 for X being set st X = {t9 where t9 is type of T: ex A
being finite Subset of the adjectives of T st A is_properly_applicable_to t9 &
A ast t9 = 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 = {t9 where t9 is type of T: ex A being finite Subset of the
adjectives of T st A is_properly_applicable_to t9 & A ast t9 = t};
A1: R is with_Church-Rosser_property with_UN_property strongly-normalizing
Relation by Th69,Th77;
A2: radix t is_>=_than AA
proof
let tt be type of T;
assume tt in AA;
then ex t9 being type of T st tt = t9 & ex A being finite Subset of the
adjectives of T st A is_properly_applicable_to t9 & A ast t9 = t;
then R reduces t, tt by Th72;
then t, tt are_convertible_wrt R by REWRITE1:25;
then nf(t, R) = nf(tt, R) by A1,REWRITE1:55;
then nf(t, R) is_a_normal_form_of tt, R by A1,REWRITE1:54;
then R reduces tt, nf(t,R);
hence thesis by Th67;
end;
ex A being finite Subset of the adjectives of T st A
is_properly_applicable_to radix t & A ast radix t = t by Th76,Th78;
then radix t in AA;
then for t9 being type of T st t9 is_>=_than AA holds radix t <= t9;
hence thesis by A2,YELLOW_0:30;
end;
theorem Th81:
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@-->;
set AA = {t9 where t9 is type of T: ex A being finite Subset of the
adjectives of T st A is_properly_applicable_to t9 & A ast t9 = t2};
assume that
A1: a is_properly_applicable_to t1 and
A2: 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 and
A4: A ast (t1 "\/" radix t2) = radix t2 by A1,A2,Def30;
consider v1 being FinSequence of the adjectives of T such that
A5: rng v1 = A and
A6: v1 is_properly_applicable_to t1 "\/" radix t2 by A3;
R is with_Church-Rosser_property with_UN_property strongly-normalizing
Relation by Th69,Th77;
then nf(t2, R) is_a_normal_form_of t2, R by REWRITE1:54;
then R reduces t2, nf(t2,R);
then consider B being finite Subset of the adjectives of T such that
A7: B is_properly_applicable_to radix t2 and
A8: t2 = B ast radix t2 by Th76;
consider v2 being FinSequence of the adjectives of T such that
A9: rng v2 = B and
A10: v2 is_properly_applicable_to radix t2 by A7;
A11: rng (v1^v2) = A \/ B by A5,A9,FINSEQ_1:31;
A12: radix t2 = v1 ast (t1 "\/" radix t2) by A4,A5,A6,Th56,Th57;
then
A13: v1^v2 is_properly_applicable_to t1 "\/" radix t2 by A6,A10,Th61;
then
A14: A \/ B is_properly_applicable_to t1 "\/" radix t2 by A11;
(A \/ B) ast (t1 "\/" radix t2) = v1^v2 ast (t1 "\/" radix t2) by A11,A13
,Th56,Th57
.= v2 ast radix t2 by A12,Th37
.= t2 by A8,A9,A10,Th56,Th57;
then t1 "\/" radix t2 in AA by A14;
then t1 "\/" radix t2 <= "\/"(AA, T) by Th80,YELLOW_4:1;
then
A15: t1 "\/" radix t2 <= radix t2 by Th80;
t1 "\/" radix t2 >= t1 by YELLOW_0:22;
hence thesis by A15,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 Th67,Th78;
then
A2: t1 <= radix t2 by A1,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: for x,y,z being Element of X st P[x,y] & P[y,z] holds P[x,z];
A4: 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 Def31;
hence P[x,y] by Th81;
end;
A5: for x being Element of X holds P[x,x];
for x,y being Element of T st R reduces x,y holds P[x,y] from RedInd(A4,
A5,A3);
hence thesis by A2,Th78;
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;
let t be type of T, a be adjective of T;
A1: a in adjs t or not a in adjs t;
assume a is_properly_applicable_to t;
then a ast t = t or [a ast t, t] in T@--> by A1,Def31,Th24;
then T@--> reduces a ast t,t by REWRITE1:12,15;
then
A2: a ast t, t are_convertible_wrt T@--> by REWRITE1:25;
T@--> is with_Church-Rosser_property with_UN_property
strongly-normalizing Relation by Th69,Th77;
hence thesis by A2,REWRITE1:55;
end;