:: On semilattice structure of {M}izar types
:: by Grzegorz Bancerek
::
:: Received August 8, 2003
:: Copyright (c) 2003-2016 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;
begin :: Semilattice of type widening
registration
cluster reflexive -> complete for 1-element 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;
registration
cluster -> Noetherian for 1-element 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;
registration
cluster Mizar-widening-like -> Noetherian with_suprema upper-bounded for
Poset;
end;
registration
cluster Noetherian -> Mizar-widening-like for sup-Semilattice;
end;
registration
cluster Mizar-widening-like for complete sup-Semilattice;
end;
registration
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;
registration
cluster non void involutive without_fixpoints for strict AdjectiveStr;
end;
registration
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;
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;
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;
end;
registration
cluster 1-element reflexive non void involutive without_fixpoints
strict for 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 Function
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 object 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 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;
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;
end;
theorem :: ABCMIZ_0:18
for T being consistent TA-structure for a being adjective of T holds
types a misses types non-a;
registration
let T be adj-structured reflexive transitive antisymmetric with_suprema
TA-structure;
let a be adjective of T;
cluster types a -> lower directed;
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;
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
:: ABCMIZ_0:def 15
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
:: ABCMIZ_0:def 16
ex t9 being type of T st A c= adjs t9 & t9 <= t;
end;
theorem :: ABCMIZ_0:19
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:20
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: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 in adjs(a ast 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 ast t in types a;
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 for t9 being type of T st t9 <= t & a in adjs t9 holds a
is_applicable_to t & t9 <= a ast t;
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 st a in adjs t holds a is_applicable_to t & a ast t = 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,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:26
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:27
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 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;
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;
end;
theorem :: ABCMIZ_0:28
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:29
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:30
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:31
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:32
for p,q being FinSequence for i being Nat st i >= 1 & i <
len p holds (p$^q).i = p.i;
theorem :: ABCMIZ_0:33
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);
theorem :: ABCMIZ_0:34
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: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 for i
being Nat st i in dom v1 holds apply(v1^v2, t).i = apply(v1, t).i;
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 holds
apply(v1^v2, t).(len v1+1) = v1 ast t;
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
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 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 :: ABCMIZ_0:38
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:39
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:40
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:41
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;
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 s being
type of T st s in rng apply(v, t) holds v ast t <= s & s <= t;
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 holds v ast t
<= 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 rng v c=
adjs (v ast 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 for A being
Subset of the adjectives of T st A = rng v holds A is_applicable_to 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 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: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^v2 is_applicable_to t holds
v2^v1 is_applicable_to t;
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
v1^v2 ast t = v2^v1 ast t;
theorem :: ABCMIZ_0:49
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: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 c= adjs(A ast 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 ast t in types A;
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 for t9 being type of T st t9 <= t & A c= adjs t9
holds A is_applicable_to t & t9 <= A ast t;
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 st A c= adjs t holds A is_applicable_to t & A ast
t = t;
theorem :: ABCMIZ_0:54
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:55
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:56
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;
registration
cluster non void reflexive 1-element strict for 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 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 :: ABCMIZ_0:57
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:58
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:59
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:60
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: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 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:62
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:63
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 :: ABCMIZ_0:sch 1
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:64
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;
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;
end;
theorem :: ABCMIZ_0:65
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:66
for T being adj-structured antisymmetric non void reflexive
transitive with_suprema Noetherian TAS-structure holds T@--> c= the
InternalRel of T;
scheme :: ABCMIZ_0:sch 2
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:67
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:68
for T being Noetherian adj-structured reflexive transitive
antisymmetric non void with_suprema TAS-structure holds T@--> is irreflexive;
theorem :: ABCMIZ_0:69
for T being adj-structured antisymmetric non void reflexive
transitive with_suprema Noetherian TAS-structure holds T@--> is
strongly-normalizing;
theorem :: ABCMIZ_0:70
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@-->;
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 holds Rev apply(s, t) is RedSequence of 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 A is_properly_applicable_to t
holds T@--> reduces A ast t, t;
theorem :: ABCMIZ_0:73
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:74
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:75
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:76
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:77
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:78
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: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 <= 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 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);
theorem :: ABCMIZ_0:81
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: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 st t1 <= t2 holds radix 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 t being type
of T, a being adjective of T st a is_properly_applicable_to t holds radix (a
ast t) = radix t;