Volume 15, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

### The abstract of the Mizar article:

### On Semilattice Structure of Mizar Types

**by****Grzegorz Bancerek**- Received August 8, 2003
- MML identifier: ABCMIZ_0

- [ Mizar article, MML identifier index ]

environ vocabulary FINSET_1, RELAT_1, ORDERS_1, IDEAL_1, REWRITE1, LATTICES, WAYBEL_0, FILTER_2, BOOLE, QUANTAL1, ORDINAL2, REALSET1, FUNCT_1, LATTICE3, BINOP_1, OPOSET_1, AMI_1, FINSUB_1, PRELAMB, PRE_TOPC, YELLOW_1, OPPCAT_1, BHSP_3, RELAT_2, FUNCOP_1, WELLORD2, MIDSP_3, YELLOW_0, FINSEQ_1, FUNCT_7, ARYTM, CARD_1, FINSEQ_5, ABCMIZ_0, ARYTM_1; notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, RELAT_2, SUBSET_1, RELSET_1, ORDINAL1, FINSUB_1, CARD_1, FUNCT_1, FUNCT_2, BINOP_1, FINSET_1, FINSEQ_1, FUNCT_4, ALG_1, BORSUK_1, FINSEQ_5, ORDINAL2, XCMPLX_0, XREAL_0, NAT_1, STRUCT_0, PRE_TOPC, REALSET1, ORDERS_1, LATTICE3, REWRITE1, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_7; constructors FINSUB_1, BORSUK_1, ALG_1, FINSEQ_5, REALSET1, LATTICE3, REWRITE1, YELLOW_2, INT_1, NAT_1, DOMAIN_1; clusters XREAL_0, REWRITE1, SUBSET_1, FINSUB_1, FINSET_1, NAT_1, BINARITH, RELAT_1, STRUCT_0, RELSET_1, FINSEQ_5, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_7, YELLOW_9, FINSEQ_1; requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM; begin :: Semilattice of type widening definition cluster trivial reflexive -> complete (non empty RelStr); 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 :: ABCMIZ_0:def 1 the InternalRel of T is co-well_founded; end; definition cluster trivial -> Noetherian (non empty RelStr); end; definition let T be non empty RelStr; redefine attr T is Noetherian means :: ABCMIZ_0:def 2 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; end; definition let T be Poset; attr T is Mizar-widening-like means :: ABCMIZ_0:def 3 T is sup-Semilattice & T is Noetherian; end; definition cluster Mizar-widening-like -> Noetherian with_suprema upper-bounded Poset; end; definition cluster Noetherian -> Mizar-widening-like sup-Semilattice; end; definition cluster Mizar-widening-like (complete sup-Semilattice); end; definition let T be Noetherian RelStr; cluster the InternalRel of T -> co-well_founded; end; theorem :: ABCMIZ_0:1 for T being Noetherian sup-Semilattice for I being Ideal of T holds ex_sup_of I, T & sup I in I; begin :: Adjectives definition struct AdjectiveStr (# adjectives -> set, non-op -> UnOp of the adjectives #); end; definition let A be AdjectiveStr; attr A is void means :: ABCMIZ_0:def 4 the adjectives of A is empty; mode adjective of A is Element of the adjectives of A; end; theorem :: ABCMIZ_0:2 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 :: ABCMIZ_0:def 5 (the non-op of A).a; end; theorem :: ABCMIZ_0:3 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 :: ABCMIZ_0:def 6 for a being adjective of A holds non-non-a = a; attr A is without_fixpoints means :: ABCMIZ_0:def 7 not ex a being adjective of A st non-a = a; end; theorem :: ABCMIZ_0:4 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; theorem :: ABCMIZ_0:5 for A1,A2 being AdjectiveStr st the AdjectiveStr of A1 = the AdjectiveStr of A2 holds A1 is involutive implies A2 is involutive; theorem :: ABCMIZ_0:6 for A1,A2 being AdjectiveStr st the AdjectiveStr of A1 = the AdjectiveStr of A2 holds A1 is without_fixpoints implies A2 is without_fixpoints; definition cluster non void involutive without_fixpoints (strict AdjectiveStr); end; definition let A be non void AdjectiveStr; cluster the adjectives of A -> non empty; end; definition struct(RelStr,AdjectiveStr) TA-structure(# carrier, adjectives -> set, InternalRel -> (Relation of the carrier), non-op -> UnOp of the adjectives, adj-map -> Function of the carrier, Fin the adjectives #); end; definition let X be non empty set; let A be set; let r be Relation of X; let n be UnOp of A; let a be Function of X, Fin A; cluster TA-structure(#X,A,r,n,a#) -> non empty; end; definition let X be set; let A be non empty set; let r be Relation of X; let n be UnOp of A; let a be Function of X, Fin A; cluster TA-structure(#X,A,r,n,a#) -> non void; end; definition cluster trivial reflexive non empty non void involutive without_fixpoints strict TA-structure; end; definition let T be TA-structure; let t be Element of T; func adjs t -> Subset of the adjectives of T equals :: ABCMIZ_0:def 8 (the adj-map of T).t; end; theorem :: ABCMIZ_0:7 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 :: ABCMIZ_0:def 9 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 :: ABCMIZ_0:8 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; definition let T be non empty TA-structure; attr T is adj-structured means :: ABCMIZ_0:def 10 the adj-map of T is join-preserving map of T, (BoolePoset the adjectives of T) opp; end; theorem :: ABCMIZ_0:9 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; definition let T be reflexive transitive antisymmetric with_suprema TA-structure; redefine attr T is adj-structured means :: ABCMIZ_0:def 11 for t1,t2 being type of T holds adjs(t1"\/"t2) = (adjs t1) /\ (adjs t2); end; theorem :: ABCMIZ_0:10 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; definition let T be TA-structure; let a be Element of the adjectives of T; func types a -> Subset of T means :: ABCMIZ_0:def 12 for x being set holds x in it iff ex t being type of T st x = t & a in adjs t; 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 :: ABCMIZ_0:def 13 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; end; theorem :: ABCMIZ_0:11 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; theorem :: ABCMIZ_0:12 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}; theorem :: ABCMIZ_0:13 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; theorem :: ABCMIZ_0:14 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; theorem :: ABCMIZ_0:15 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}; theorem :: ABCMIZ_0:16 for T being non empty TA-structure for t being type of T holds types ({} the adjectives of T) = the carrier of T; definition let T be TA-structure; attr T is adjs-typed means :: ABCMIZ_0:def 14 for a being adjective of T holds types a \/ types non-a is non empty; end; theorem :: ABCMIZ_0:17 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; definition cluster non void Mizar-widening-like involutive without_fixpoints consistent adj-structured adjs-typed (complete upper-bounded non empty trivial reflexive transitive antisymmetric strict TA-structure); end; theorem :: ABCMIZ_0:18 for T being consistent TA-structure for a being adjective of T holds types a misses types non-a; definition let T be adj-structured (reflexive transitive antisymmetric with_suprema TA-structure); let a be adjective of T; cluster types a -> lower directed; end; definition let T be adj-structured (reflexive transitive antisymmetric with_suprema TA-structure); let A be Subset of the adjectives of T; cluster types A -> lower directed; end; theorem :: ABCMIZ_0:19 for T being adj-structured (with_suprema reflexive antisymmetric transitive TA-structure) for a being adjective of T holds types a is empty or types a is Ideal of T; begin :: Applicability of adjectives definition let T be TA-structure; let t be Element of T; let a be adjective of T; pred a is_applicable_to t means :: ABCMIZ_0:def 15 ex t' being type of T st t' in types a & t' <= t; end; definition let T be TA-structure; let t be type of T; let A be Subset of the adjectives of T; pred A is_applicable_to t means :: ABCMIZ_0:def 16 ex t' being type of T st A c= adjs t' & t' <= t; end; theorem :: ABCMIZ_0:20 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; 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 :: ABCMIZ_0:def 17 sup(types a /\ downarrow t); end; theorem :: ABCMIZ_0:21 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; theorem :: ABCMIZ_0:22 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); theorem :: ABCMIZ_0:23 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; theorem :: ABCMIZ_0:24 for T being Noetherian adj-structured (reflexive transitive antisymmetric with_suprema TA-structure) for t being type of T for a being adjective of T for t' being type of T st t' <= t & a in adjs t' holds a is_applicable_to t & t' <= a ast t; theorem :: ABCMIZ_0:25 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; theorem :: ABCMIZ_0:26 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); theorem :: ABCMIZ_0:27 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; 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 :: ABCMIZ_0:def 18 sup(types A /\ downarrow t); end; theorem :: ABCMIZ_0:28 for T being non empty reflexive transitive antisymmetric TA-structure for t being type of T holds ({} the adjectives of T) ast t = t; 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 :: ABCMIZ_0:def 19 len it = len p+1 & it.1 = t & for i being Nat, a being adjective of T, t being type of T st i in dom p & a = p.i & t = it.i holds it.(i+1) = a ast t; end; definition let T be non empty non void reflexive transitive TA-structure; let t be type of T; let p be FinSequence of the adjectives of T; cluster apply(p,t) -> non empty; end; theorem :: ABCMIZ_0:29 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*>; theorem :: ABCMIZ_0:30 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*>; 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 :: ABCMIZ_0:def 20 apply(v,t).(len v+1); end; theorem :: ABCMIZ_0:31 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; theorem :: ABCMIZ_0:32 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; theorem :: ABCMIZ_0:33 for p,q being FinSequence for i being natural number st i >= 1 & i < len p holds (p$^q).i = p.i; theorem :: ABCMIZ_0:34 for p being non empty FinSequence, q being FinSequence for i being natural number st i < len q holds (p$^q).(len p+i) = q.(i+1); theorem :: ABCMIZ_0:35 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); theorem :: ABCMIZ_0:36 for T being non empty non void reflexive transitive TA-structure for t being type of T for v1,v2 being FinSequence of the adjectives of T for i being natural number st i in dom v1 holds apply(v1^v2, t).i = apply(v1, t).i; theorem :: ABCMIZ_0:37 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; theorem :: ABCMIZ_0:38 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; 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 :: ABCMIZ_0:def 21 for i being natural number, a being adjective of T, s being type of T st i in dom v & a = v.i & s = apply(v,t).i holds a is_applicable_to s; end; theorem :: ABCMIZ_0:39 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 :: ABCMIZ_0:40 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; theorem :: ABCMIZ_0:41 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; theorem :: ABCMIZ_0:42 for T being Noetherian adj-structured (reflexive transitive antisymmetric with_suprema non void TA-structure) for t being type of T for v being FinSequence of the adjectives of T st v is_applicable_to t for i1,i2 being natural number st 1 <= i1 & i1 <= i2 & i2 <= len v+1 for t1,t2 being type of T st t1 = apply(v,t).i1 & t2 = apply(v,t).i2 holds t2 <= t1; theorem :: ABCMIZ_0:43 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; theorem :: ABCMIZ_0:44 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; theorem :: ABCMIZ_0:45 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); theorem :: ABCMIZ_0:46 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; theorem :: ABCMIZ_0:47 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; theorem :: ABCMIZ_0:48 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; theorem :: ABCMIZ_0:49 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; theorem :: ABCMIZ_0:50 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; theorem :: ABCMIZ_0:51 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); theorem :: ABCMIZ_0:52 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; theorem :: ABCMIZ_0:53 for T being Noetherian adj-structured (reflexive transitive antisymmetric with_suprema TA-structure) for t being type of T for A being Subset of the adjectives of T for t' being type of T st t' <= t & A c= adjs t' holds A is_applicable_to t & t' <= A ast t; theorem :: ABCMIZ_0:54 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; theorem :: ABCMIZ_0:55 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; theorem :: ABCMIZ_0:56 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; theorem :: ABCMIZ_0:57 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; 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 :: ABCMIZ_0:def 22 for a being adjective of T holds it.a = sup(types a \/ types non-a); end; definition struct(TA-structure) TAS-structure(# carrier, adjectives -> set, InternalRel -> (Relation of the carrier), non-op -> UnOp of the adjectives, adj-map -> Function of the carrier, Fin the adjectives, sub-map -> Function of the adjectives, the carrier #); end; definition cluster non void reflexive trivial non empty strict TAS-structure; end; definition let T be non empty non void TAS-structure; let a be adjective of T; func sub a -> type of T equals :: ABCMIZ_0:def 23 (the sub-map of T).a; end; definition let T be non empty non void TAS-structure; attr T is non-absorbing means :: ABCMIZ_0:def 24 (the sub-map of T)*(the non-op of T) = the sub-map of T; attr T is subjected means :: ABCMIZ_0:def 25 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 :: ABCMIZ_0:def 26 for a being adjective of T holds sub non-a = sub a; 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 :: ABCMIZ_0:def 27 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 :: ABCMIZ_0:def 28 for i being natural number, a being adjective of T, s being type of T st i in dom v & a = v.i & s = apply(v,t).i holds a is_properly_applicable_to s; end; theorem :: ABCMIZ_0:58 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; theorem :: ABCMIZ_0:59 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 :: ABCMIZ_0:60 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; theorem :: ABCMIZ_0:61 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; theorem :: ABCMIZ_0:62 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; 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 :: ABCMIZ_0:def 29 ex s being FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t; end; theorem :: ABCMIZ_0:63 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 :: ABCMIZ_0:64 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; 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 ex A being finite set st P[A]; theorem :: ABCMIZ_0:65 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; definition let T be non empty non void reflexive transitive TAS-structure; attr T is commutative means :: ABCMIZ_0:def 30 for t1,t2 being type of T, a being adjective of T st a is_properly_applicable_to t1 & a ast t1 <= t2 ex A being finite Subset of the adjectives of T st A is_properly_applicable_to t1 "\/" t2 & A ast (t1 "\/" t2) = t2; end; definition cluster Mizar-widening-like involutive without_fixpoints consistent adj-structured adjs-typed non-absorbing subjected commutative (complete upper-bounded non empty non void trivial reflexive transitive antisymmetric strict TAS-structure); end; theorem :: ABCMIZ_0:66 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; begin :: Reduction of adjectives definition let T be non empty non void reflexive transitive TAS-structure; func T @--> -> Relation of T means :: ABCMIZ_0:def 31 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; end; theorem :: ABCMIZ_0:67 for T being adj-structured antisymmetric (non void reflexive transitive with_suprema Noetherian TAS-structure) holds T@--> c= the InternalRel of T; 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 for x,y being Element of X() st [x,y] in R() holds P[x,y] and for x being Element of X() holds P[x,x] and for x,y,z being Element of X() st P[x,y] & P[y,z] holds P[x,z]; theorem :: ABCMIZ_0:68 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; theorem :: ABCMIZ_0:69 for T being Noetherian adj-structured (reflexive transitive antisymmetric non void with_suprema TAS-structure) holds T@--> is irreflexive; theorem :: ABCMIZ_0:70 for T being adj-structured antisymmetric (non void reflexive transitive with_suprema Noetherian TAS-structure) holds T@--> is strongly-normalizing; theorem :: ABCMIZ_0:71 for T being Noetherian adj-structured (reflexive transitive antisymmetric with_suprema non void TAS-structure) for t being type of T, A being finite Subset of the adjectives of T st for C being Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t holds C = A for s being one-to-one FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t for i being natural number st 1 <= i & i <= len s holds [apply(s, t).(i+1), apply(s, t).i] in T@-->; theorem :: ABCMIZ_0:72 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@-->; theorem :: ABCMIZ_0:73 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; theorem :: ABCMIZ_0:74 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; theorem :: ABCMIZ_0:75 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; theorem :: ABCMIZ_0:76 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; theorem :: ABCMIZ_0:77 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; theorem :: ABCMIZ_0:78 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; 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 :: ABCMIZ_0:def 32 nf(t, T@-->); end; theorem :: ABCMIZ_0:79 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; theorem :: ABCMIZ_0:80 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; theorem :: ABCMIZ_0:81 for T being adj-structured with_suprema antisymmetric commutative (non empty non void reflexive transitive Noetherian TAS-structure) for t being type of T for X being set st X = {t' where t' is type of T: ex A being finite Subset of the adjectives of T st A is_properly_applicable_to t' & A ast t' = t} holds ex_sup_of X, T & radix t = "\/"(X, T); theorem :: ABCMIZ_0:82 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; theorem :: ABCMIZ_0:83 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; theorem :: ABCMIZ_0:84 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;

Back to top