:: The Incompleteness of the Lattice of Substitutions
:: by Adam Grabowski
::
:: Received July 17, 2000
:: Copyright (c) 2000-2026 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, ABIAN, RELAT_1, CARD_1, ARYTM_3, ORDERS_2, SUBSET_1,
TARSKI, ZFMISC_1, FUNCT_1, XXREAL_0, FINSET_1, XBOOLE_0, FINSEQ_1,
MCART_1, LATTICES, LATTICE3, PBOOLE, EQREL_1, FINSUB_1, PARTFUN1,
HEYTING1, SUBSTLAT, NORMFORM, REALSET1, STRUCT_0, BINOP_1, RELAT_2,
ORDINAL4, CAT_1, YELLOW_0, WELLORD1, HEYTING2, REWRITE1, HEYTING3,
XCMPLX_0, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1,
FUNCT_1, ORDERS_2, MEMBERED, XCMPLX_0, NAT_1, FINSEQ_1, BINOP_1,
FINSET_1, FINSUB_1, PARTFUN1, LATTICES, DOMAIN_1, REALSET1, STRUCT_0,
SUBSTLAT, XTUPLE_0, MCART_1, WELLORD1, YELLOW_0, ABIAN, XXREAL_2,
LATTICE3, HEYTING2, XXREAL_0;
constructors BINOP_1, TOLER_1, REALSET1, ABIAN, LATTICE3, YELLOW_0, HEYTING2,
VALUED_1, XXREAL_2, RELSET_1, XTUPLE_0, XXREAL_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, PARTFUN1, FINSET_1,
FINSUB_1, XXREAL_0, NAT_1, MEMBERED, FINSEQ_1, REALSET1, ABIAN, STRUCT_0,
LATTICES, LATTICE3, YELLOW_0, YELLOW_1, SUBSTLAT, XXREAL_2, RELAT_1,
HEYTING2, XTUPLE_0, XCMPLX_0;
requirements SUBSET, BOOLE, NUMERALS, REAL, ARITHM;
definitions TARSKI, LATTICE3, FUNCT_1, XBOOLE_0;
equalities LATTICE3, BINOP_1, REALSET1, WELLORD1;
expansions TARSKI, LATTICE3, XBOOLE_0;
theorems HEYTING2, ZFMISC_1, PARTFUN1, YELLOW_0, LATTICE3, TARSKI, NAT_1,
LATTICE5, FINSEQ_1, FUNCT_5, ORDERS_2, YELLOW_5, SUBSTLAT, FINSUB_1,
WAYBEL15, LATTICES, GRFUNC_1, RELAT_1, SYSREL, BINOP_1, FUNCT_1, FUNCT_2,
XBOOLE_0, XBOOLE_1, ORDINAL1, XREAL_1, XXREAL_0, XXREAL_2, PRE_POLY,
ABIAN, XTUPLE_0;
schemes LMOD_7, XBOOLE_0;
begin :: Preliminaries
scheme
SSubsetUniq { R() -> 1-sorted, P[object] } :
for A1, A2 being Subset of R() st (
for x being object holds x in A1 iff P[x]) &
(for x being object holds x in A2 iff P[
x]) holds A1 = A2 proof
let A1, A2 be Subset of R();
assume that
A1: for x being object holds x in A1 iff P[x] and
A2: for x being object holds x in A2 iff P[x];
thus A1 c= A2
by A1,A2;
let x be object;
assume x in A2;
then P[x] by A2;
hence thesis by A1;
end;
Lm1: for A, x being set holds [:A, {x}:] is Function
proof
let A, x be set;
set X = [:A, {x}:];
X is Function-like
proof
let y,y1,y2 be object;
assume that
A1: [y,y1] in X and
A2: [y,y2] in X;
y1 = x by A1,ZFMISC_1:106;
hence thesis by A2,ZFMISC_1:106;
end;
hence thesis;
end;
registration
let A, x be set;
cluster [:A, {x}:] -> Function-like;
coherence by Lm1;
end;
Lm2: 0 = 2 * 0;
Lm3: 1 = 0 + 1;
theorem Th1:
for X being finite non empty Subset of NAT holds ex n being
Element of NAT st X c= Seg n \/ {0}
proof
let X be finite non empty Subset of NAT;
reconsider m = max X as Element of NAT by ORDINAL1:def 12;
take m;
let x be object;
A1: Seg m c= Seg m \/ {0} by XBOOLE_1:7;
A2: {0} c= Seg m \/ {0} by XBOOLE_1:7;
assume
A3: x in X;
then reconsider n = x as Element of NAT;
A4: n <= m by A3,XXREAL_2:def 8;
per cases by NAT_1:25;
suppose
1 <= n;
then n in Seg m by A4,FINSEQ_1:1;
hence thesis by A1;
end;
suppose
0 = n;
then n in {0} by TARSKI:def 1;
hence thesis by A2;
end;
end;
theorem
for X being finite Subset of NAT holds ex k being odd Element of NAT
st not k in X
proof
let X be finite Subset of NAT;
per cases;
suppose
X is non empty;
then consider n being Element of NAT such that
A1: X c= Seg n \/ {0} by Th1;
A2: not 2*n+1 in X
proof
A3: not 2*n+1 in {0} by TARSKI:def 1;
assume 2*n+1 in X;
then 2*n+1 in Seg n by A1,A3,XBOOLE_0:def 3;
then
A4: 2*n+1 <= n by FINSEQ_1:1;
1*n <= 2*n by NAT_1:4;
hence thesis by A4,NAT_1:13;
end;
assume for k being odd Element of NAT holds k in X;
hence contradiction by A2;
end;
suppose
X is empty;
hence thesis;
end;
end;
theorem Th3:
for k being Element of NAT, X being finite non empty Subset of [:
NAT,{k}:] holds ex n being non zero Element of NAT st X c= [:Seg n \/ {0},{k}
:]
proof
let k be Element of NAT;
let X be finite non empty Subset of [:NAT,{k}:];
reconsider pX = proj1 X as finite non empty Subset of NAT by FUNCT_5:11;
reconsider mpX = max pX as Element of NAT by ORDINAL1:def 12;
reconsider m = mpX + 1 as non zero Element of NAT;
take m;
let x be object;
A1: Seg m c= Seg m \/ {0} by XBOOLE_1:7;
A2: {0} c= Seg m \/ {0} by XBOOLE_1:7;
assume
A3: x in X;
then consider x1,x2 being object such that
A4: x1 in NAT and
A5: x2 in {k} and
A6: x = [x1,x2] by ZFMISC_1:def 2;
reconsider n = x`1 as Element of NAT by A4,A6;
n in pX by A3,A6,XTUPLE_0:def 12;
then max pX <= m & n <= max pX by NAT_1:11,XXREAL_2:def 8;
then
A7: n <= m by XXREAL_0:2;
per cases by NAT_1:25;
suppose
1 <= n;
then n in Seg m by A7,FINSEQ_1:1;
hence thesis by A5,A6,A1,ZFMISC_1:87;
end;
suppose
0 = n;
then n in {0} by TARSKI:def 1;
hence thesis by A5,A6,A2,ZFMISC_1:87;
end;
end;
theorem Th4:
for m being Element of NAT, X being finite non empty Subset of [:
NAT,{m}:] holds ex k being non zero Element of NAT st not [2*k+1,m] in X
proof
let m be Element of NAT;
let X be finite non empty Subset of [:NAT,{m}:];
consider n being non zero Element of NAT such that
A1: X c= [:Seg n \/ {0},{m}:] by Th3;
A2: not [2*n+1,m] in X
proof
assume [2*n+1,m] in X;
then
A3: 2*n+1 in Seg n \/ {0} by A1,ZFMISC_1:87;
not 2*n+1 in {0} by TARSKI:def 1;
then 2*n+1 in Seg n by A3,XBOOLE_0:def 3;
then
A4: 2*n+1 <= n by FINSEQ_1:1;
1*n <= 2*n by NAT_1:4;
hence thesis by A4,NAT_1:13;
end;
assume for k being non zero Element of NAT holds [2*k+1,m] in X;
hence contradiction by A2;
end;
theorem
for m being Element of NAT, X being finite Subset of [:NAT,{m}:] ex k
being Element of NAT st for l being Element of NAT st l >= k holds not [l,m] in
X
proof
let m be Element of NAT;
let X be finite Subset of [:NAT,{m}:];
per cases;
suppose
X is non empty;
then reconsider X9 = X as finite non empty Subset of [:NAT,{m}:];
consider n being non zero Element of NAT such that
A1: X9 c= [:Seg n \/ {0},{m}:] by Th3;
take k = n+1;
let l be Element of NAT;
assume
A2: l >= k;
assume [l,m] in X;
then
A3: l in Seg n \/ {0} by A1,ZFMISC_1:87;
now
per cases by A3,XBOOLE_0:def 3;
suppose
l in Seg n;
then l <= n by FINSEQ_1:1;
hence contradiction by A2,NAT_1:13;
end;
suppose
l in {0};
hence contradiction by A2,TARSKI:def 1;
end;
end;
hence thesis;
end;
suppose
X is empty;
then for l being Element of NAT st l >= 0 holds not [l,m] in X;
hence thesis;
end;
end;
theorem
for L being upper-bounded Lattice holds Top L = Top LattPOSet L
proof
let L be upper-bounded Lattice;
set x = %Top LattPOSet L;
now
let a be Element of L;
a% <= x% by YELLOW_0:45;
then a [= x by LATTICE3:7;
hence x"\/"a = x & a"\/"x = x by LATTICES:def 3;
end;
hence thesis by LATTICES:def 17;
end;
theorem
for L being lower-bounded Lattice holds Bottom L = Bottom LattPOSet L
proof
let L be lower-bounded Lattice;
set x = %Bottom LattPOSet L;
now
let a be Element of L;
a% >= x% by YELLOW_0:44;
then x [= a by LATTICE3:7;
hence x"/\"a = x & a"/\"x = x by LATTICES:4;
end;
hence thesis by LATTICES:def 16;
end;
begin :: Poset of Substitutions
theorem
for V being set, C being finite set, A, B being Element of Fin PFuncs
(V, C) st A = {} & B <> {} holds B =>> A = {}
proof
let V be set, C be finite set, A, B be Element of Fin PFuncs (V, C);
assume
A1: A = {} & B <> {};
assume B =>> A <> {};
then consider k being object such that
A2: k in B =>> A by XBOOLE_0:def 1;
ex f being PartFunc of B, A st k = union {f.i \ i where i is Element of
PFuncs (V, C) : i in B} & dom f = B by A2,HEYTING2:15;
hence thesis by A1;
end;
theorem Th9:
for V, V9, C, C9 being set st V c= V9 & C c= C9 holds
SubstitutionSet (V, C) c= SubstitutionSet (V9, C9)
proof
let V, V9, C, C9 be set;
assume V c= V9 & C c= C9;
then
A1: PFuncs (V,C) c= PFuncs (V9,C9) by PARTFUN1:50;
let x be object;
assume x in SubstitutionSet (V, C);
then
x in { A where A is Element of Fin PFuncs (V,C) : ( for u being set st u
in A holds u is finite ) & for s, t being Element of PFuncs (V, C) holds ( s in
A & t in A & s c= t implies s = t ) } by SUBSTLAT:def 1;
then consider B being Element of Fin PFuncs (V,C) such that
A2: B = x & for u being set st u in B holds u is finite and
A3: for s, t being Element of PFuncs (V, C) holds ( s in B & t in B & s
c= t implies s = t );
A4: B in Fin PFuncs (V,C) & Fin PFuncs (V,C) c= Fin PFuncs (V9,C9) by A1,
FINSUB_1:10;
A5: B c= PFuncs (V,C) by FINSUB_1:def 5;
reconsider B as Element of Fin PFuncs (V9, C9) by A4;
for s, t being Element of PFuncs (V9, C9) st s in B & t in B & s c= t
holds s = t by A3,A5;
then x in { D where D is Element of Fin PFuncs (V9, C9) : ( for u being set
st u in D holds u is finite ) & for s, t being Element of PFuncs (V9, C9) holds
( s in D & t in D & s c= t implies s = t ) } by A2;
hence thesis by SUBSTLAT:def 1;
end;
theorem Th10:
for V, V9, C, C9 being set, A being Element of Fin PFuncs (V, C)
, B being Element of Fin PFuncs (V9, C9) st V c= V9 & C c= C9 & A = B holds mi
A = mi B
proof
let V, V9, C, C9 be set, A be Element of Fin PFuncs (V, C), B be Element of
Fin PFuncs (V9, C9);
assume that
A1: V c= V9 & C c= C9 and
A2: A = B;
hereby
let x be object;
A3: PFuncs (V,C) c= PFuncs (V9,C9) by A1,PARTFUN1:50;
assume
A4: x in mi A;
then x in { t where t is Element of PFuncs (V, C) : t is finite & for s
being Element of PFuncs (V, C) holds ( s in A & s c= t iff s = t ) } by
SUBSTLAT:def 2;
then consider f being Element of PFuncs (V, C) such that
A5: f = x and
A6: f is finite and
for s being Element of PFuncs (V, C) holds ( s in A & s c= f iff s = f );
reconsider f as Element of PFuncs (V9, C9) by A3;
for s being Element of PFuncs (V9, C9) holds s in B & s c= f iff s = f
by A2,A4,A5,SUBSTLAT:6;
then x in { t where t is Element of PFuncs (V9, C9) : t is finite & for s
being Element of PFuncs (V9, C9) holds ( s in B & s c= t iff s = t ) } by A5,A6
;
hence x in mi B by SUBSTLAT:def 2;
end;
let x be object;
assume
A7: x in mi B;
then x in { t where t is Element of PFuncs (V9, C9) : t is finite & for s
being Element of PFuncs (V9, C9) holds ( s in B & s c= t iff s = t ) } by
SUBSTLAT:def 2;
then ex f being Element of PFuncs (V9, C9) st f = x & f is finite & for s
being Element of PFuncs (V9, C9) holds ( s in B & s c= f iff s = f );
then reconsider x9 = x as finite set;
mi B c= B & for b being finite set st b in A & b c= x9 holds b = x9 by A2,A7,
SUBSTLAT:6;
hence thesis by A2,A7,SUBSTLAT:7;
end;
theorem
for V, V9, C, C9 being set st V c= V9 & C c= C9 holds the L_join of
SubstLatt (V, C) = (the L_join of SubstLatt (V9, C9))||the carrier of SubstLatt
(V, C)
proof
let V, V9, C, C9 be set;
set K = SubstLatt (V, C), L = SubstLatt (V9, C9);
A1: SubstitutionSet (V, C) = the carrier of K by SUBSTLAT:def 4;
A2: dom (the L_join of L) = [:the carrier of L, the carrier of L:] by
FUNCT_2:def 1;
reconsider B1 = the L_join of K as BinOp of the carrier of K;
set B2 = (the L_join of L)||the carrier of K;
assume
A3: V c= V9 & C c= C9;
SubstitutionSet (V9, C9) = the carrier of L by SUBSTLAT:def 4;
then the carrier of K c= the carrier of L by A1,A3,Th9;
then
A4: dom B2 = [:the carrier of K, the carrier of K:] by A2,RELAT_1:62
,ZFMISC_1:96;
A5: SubstitutionSet (V, C) c= SubstitutionSet (V9, C9) by A3,Th9;
rng B2 c= the carrier of K
proof
let x be object;
assume x in rng B2;
then consider y being object such that
A6: y in dom B2 and
A7: x = B2.y by FUNCT_1:def 3;
consider y1, y2 being object such that
A8: y1 in the carrier of K & y2 in the carrier of K and
A9: y = [y1, y2] by A4,A6,ZFMISC_1:def 2;
y1 in SubstitutionSet (V, C) & y2 in SubstitutionSet (V, C) by A8,
SUBSTLAT:def 4;
then reconsider
y19 = y1, y29 = y2 as Element of SubstitutionSet (V9, C9) by A5;
reconsider y11 = y1, y22 = y2 as Element of SubstitutionSet (V, C) by A8,
SUBSTLAT:def 4;
B2.y = (the L_join of L). (y1, y2) by A4,A6,A9,FUNCT_1:49
.= mi (y19 \/ y29) by SUBSTLAT:def 4
.= mi (y11 \/ y22) by A3,Th10;
hence thesis by A1,A7;
end;
then reconsider B2 as BinOp of the carrier of K by A4,FUNCT_2:2;
now
let a, b be Element of K;
reconsider a9 = a, b9 = b as Element of SubstitutionSet (V, C) by
SUBSTLAT:def 4;
a9 in SubstitutionSet (V, C) & b9 in SubstitutionSet (V, C);
then reconsider
a1 = a, b1 = b as Element of SubstitutionSet (V9, C9) by A5;
thus B1.(a, b) = mi (a9 \/ b9) by SUBSTLAT:def 4
.= mi (a1 \/ b1) by A3,Th10
.= (the L_join of L).(a, b) by SUBSTLAT:def 4
.= B2.[a, b] by FUNCT_1:49
.= B2.(a, b);
end;
hence thesis by BINOP_1:2;
end;
definition
let V, C be set;
func SubstPoset (V, C) -> RelStr equals
LattPOSet SubstLatt (V, C);
coherence;
end;
registration
let V, C be set;
cluster SubstPoset (V, C) -> with_suprema with_infima;
coherence;
end;
registration
let V, C be set;
cluster SubstPoset (V, C) -> reflexive antisymmetric transitive;
coherence;
end;
theorem Th12:
for V, C being set, a, b being Element of SubstPoset (V, C)
holds a <= b iff for x being set st x in a ex y being set st y in b & y c= x
proof
let V, C be set;
let a, b be Element of SubstPoset (V, C);
reconsider a9 = a, b9 = b as Element of SubstLatt (V, C);
reconsider a1 = a, b1 = b as Element of SubstitutionSet (V, C) by
SUBSTLAT:def 4;
A1: a9% = a & b9% = b;
hereby
assume a <= b;
then a9 [= b9 by A1,LATTICE3:7;
then a9 = a9 "/\" b9 by LATTICES:4
.= (the L_meet of SubstLatt (V, C)).(a9,b9) by LATTICES:def 2
.= mi (a1 ^ b1) by SUBSTLAT:def 4;
hence for x being set st x in a ex y being set st y in b & y c= x by
HEYTING2:4;
end;
assume for x being set st x in a ex y being set st y in b & y c= x;
then mi (a1 ^ b1) = a1 by HEYTING2:5;
then a9 = (the L_meet of SubstLatt (V, C)).(a9,b9) by SUBSTLAT:def 4
.= a9 "/\" b9 by LATTICES:def 2;
then a9 [= b9 by LATTICES:4;
hence thesis by A1,LATTICE3:7;
end;
theorem
for V, V9, C, C9 being set st V c= V9 & C c= C9 holds SubstPoset (V, C
) is full SubRelStr of SubstPoset (V9, C9)
proof
let V, V9, C, C9 be set;
set K = SubstPoset (V, C), L = SubstPoset (V9, C9);
A1: the carrier of K = SubstitutionSet (V, C) & the carrier of L =
SubstitutionSet (V9, C9) by SUBSTLAT:def 4;
assume V c= V9 & C c= C9;
then
A2: the carrier of K c= the carrier of L by A1,Th9;
now
let a, b be object;
assume
A3: [a,b] in the InternalRel of K;
then reconsider a9 = a, b9 = b as Element of K by ZFMISC_1:87;
a in the carrier of K & b in the carrier of K by A3,ZFMISC_1:87;
then reconsider a1 = a, b1 = b as Element of L by A2;
a9 <= b9 by A3,ORDERS_2:def 5;
then for x being set st x in a9 ex y being set st y in b9 & y c= x by Th12;
then a1 <= b1 by Th12;
hence [a,b] in the InternalRel of L by ORDERS_2:def 5;
end;
then the InternalRel of K c= the InternalRel of L by RELAT_1:def 3;
then reconsider K as SubRelStr of L by A2,YELLOW_0:def 13;
now
let x, y be object;
assume
A4: [x,y] in (the InternalRel of L) |_2 the carrier of K;
then
A5: [x,y] in (the InternalRel of L) by XBOOLE_0:def 4;
then reconsider p = x, q = y as Element of L by ZFMISC_1:87;
[x,y] in [:the carrier of K, the carrier of K:] by A4,XBOOLE_0:def 4;
then reconsider p9 = x, q9 = y as Element of K by ZFMISC_1:87;
p <= q by A5,ORDERS_2:def 5;
then for a being set st a in p ex b being set st b in q & b c= a by Th12;
then p9 <= q9 by Th12;
hence [x,y] in the InternalRel of K by ORDERS_2:def 5;
end;
then
A6: (the InternalRel of L) |_2 the carrier of K c= the InternalRel of K by
RELAT_1:def 3;
now
let x, y be object;
assume
A7: [x,y] in the InternalRel of K;
then reconsider p = x, q = y as Element of K by ZFMISC_1:87;
reconsider p9 = p, q9 = q as Element of L by A2;
p <= q by A7,ORDERS_2:def 5;
then for a being set st a in p ex b being set st b in q & b c= a by Th12;
then p9 <= q9 by Th12;
then [p9,q9] in the InternalRel of L by ORDERS_2:def 5;
hence [x,y] in (the InternalRel of L) |_2 the carrier of K by A7,
XBOOLE_0:def 4;
end;
then the InternalRel of K c= (the InternalRel of L) |_2 the carrier of K by
RELAT_1:def 3;
then the InternalRel of K = (the InternalRel of L) |_2 the carrier of K by A6
;
hence thesis by YELLOW_0:def 14;
end;
definition
let n, k be Nat;
func PFArt (n, k) -> Element of PFuncs (NAT, {k}) means
:Def2:
for x being object
holds x in it iff ( ex m being odd Element of NAT st m <= 2*n & [m,k] = x )
or [2*n,k] = x;
existence
proof
defpred P[object] means
( ex m being odd Element of NAT st m <= 2*n & [m,k]
= $1 ) or [2*n,k] = $1;
consider X being set such that
A1: for x being object holds x in X iff x in [:NAT,{k}:] & P[x] from
XBOOLE_0:sch 1;
A2: X c= [:NAT,{k}:]
by A1;
then reconsider X9 = X as Function by GRFUNC_1:1;
dom X9 c= NAT & rng X9 c= {k} by A2,SYSREL:3;
then reconsider X as Element of PFuncs (NAT, {k}) by PARTFUN1:def 3;
take X;
let x be object;
thus x in X implies ( ex m being odd Element of NAT st m <= 2*n & [m,k] =
x ) or [2*n,k] = x by A1;
assume
A3: ( ex m being odd Element of NAT st m <= 2*n & [m,k] = x ) or [2*n, k] = x;
A4: 2*n in NAT by ORDINAL1:def 12;
per cases by A3;
suppose
ex m being odd Element of NAT st m <= 2*n & [m,k] = x;
then x in [:NAT,{k}:] by ZFMISC_1:106;
hence thesis by A1,A3;
end;
suppose
A5: [2*n,k] = x;
then x in [:NAT,{k}:] by ZFMISC_1:106,A4;
hence thesis by A1,A5;
end;
end;
uniqueness
proof
defpred P[object] means
( ex m being odd Element of NAT st m <= 2*n & [m,k] =
$1 ) or [2*n,k] = $1;
A6: for X1,X2 being Element of PFuncs (NAT, {k}) st (for x being object
holds x in X1 iff P[x]) &
(for x being object holds x in X2 iff P[x]) holds X1 =
X2 from LMOD_7:sch 1;
let X1,X2 be Element of PFuncs (NAT, {k});
assume ( for x being object holds x in X1 iff P[x])&
for x being object holds
x in X2 iff P [x];
hence thesis by A6;
end;
end;
registration
let n, k be Element of NAT;
cluster PFArt (n, k) -> finite;
coherence
proof
PFArt (n, k) c= [:Seg (2*n) \/ {0}, {k}:]
proof
let t be object;
assume
A1: t in PFArt (n, k);
per cases by A1,Def2;
suppose
ex m1 being odd Element of NAT st m1 <= 2*n & [m1,k] = t;
then consider m1 being odd Element of NAT such that
A2: m1 <= 2*n and
A3: [m1,k] = t;
1 <= m1 by ABIAN:12;
then m1 in Seg (2*n) by A2,FINSEQ_1:1;
then m1 in Seg (2*n) \/ {0} by XBOOLE_0:def 3;
hence thesis by A3,ZFMISC_1:106;
end;
suppose
A4: [2*n,k] = t;
now
per cases;
suppose
A5: n is non zero;
A6: n <= 2*n by XREAL_1:151;
1 <= n by A5,NAT_1:14;
then 1 <= 2*n by A6,XXREAL_0:2;
then 2*n in Seg (2*n) by FINSEQ_1:1;
then 2*n in Seg (2*n) \/ {0} by XBOOLE_0:def 3;
hence thesis by A4,ZFMISC_1:106;
end;
suppose
n is zero;
then 2*n in {0} by TARSKI:def 1;
then 2*n in Seg (2*n) \/ {0} by XBOOLE_0:def 3;
hence thesis by A4,ZFMISC_1:106;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
definition
let n, k be Nat;
func PFCrt (n, k) -> Element of PFuncs (NAT, {k}) means
:Def3:
for x being object
holds x in it iff ex m being odd Element of NAT st m <= 2*n + 1 & [m,k] = x;
existence
proof
defpred P[object] means
ex m being odd Element of NAT st m <= 2*n + 1 & [m,k]
= $1;
consider X being set such that
A1: for x being object holds x in X iff x in [:NAT,{k}:] & P[x] from
XBOOLE_0:sch 1;
A2: X c= [:NAT,{k}:]
by A1;
then reconsider X9 = X as Function by GRFUNC_1:1;
dom X9 c= NAT & rng X9 c= {k} by A2,SYSREL:3;
then reconsider X as Element of PFuncs (NAT, {k}) by PARTFUN1:def 3;
take X;
let x be object;
thus x in X implies ex m being odd Element of NAT st m <= 2*n + 1 & [m,k]
= x by A1;
given m being odd Element of NAT such that
A3: m <= 2*n + 1 and
A4: [m,k] = x;
x in [:NAT,{k}:] by A4,ZFMISC_1:106;
hence thesis by A1,A3,A4;
end;
uniqueness
proof
defpred P[object] means
ex m being odd Element of NAT st m <= 2*n + 1 & [m,k] = $1;
A5: for X1,X2 being Element of PFuncs (NAT, {k}) st
(for x being object holds
x in X1 iff P[x]) &
(for x being object holds x in X2 iff P[x]) holds X1 = X2
from
LMOD_7:sch 1;
let X1,X2 being Element of PFuncs (NAT, {k});
assume ( for x being object holds x in X1 iff P[x])&
for x being object holds x
in X2 iff P [x];
hence thesis by A5;
end;
end;
registration
let n,k be Element of NAT;
cluster PFCrt (n,k) -> finite;
coherence
proof
set x = PFCrt (n,k);
x c= [:Seg (2*n+1), {k}:]
proof
let t be object;
assume t in x;
then consider m being odd Element of NAT such that
A1: m <= 2*n + 1 and
A2: [m,k] = t by Def3;
1 <= m by ABIAN:12;
then m in Seg (2*n+1) by A1,FINSEQ_1:1;
hence thesis by A2,ZFMISC_1:106;
end;
hence thesis;
end;
end;
theorem
for n, k being Element of NAT holds [2*n+1,k] in PFCrt (n,k) by Def3;
theorem Th15:
for n, k being Element of NAT holds PFCrt (n,k) misses {[2*n+3,k ]}
proof
let n, k be Element of NAT;
assume PFCrt (n,k) /\ {[2*n+3,k]} <> {};
then consider x being object such that
A1: x in PFCrt (n,k) /\ {[2*n+3,k]} by XBOOLE_0:def 1;
x in PFCrt (n,k) by A1,XBOOLE_0:def 4;
then consider m being odd Element of NAT such that
A2: m <= 2*n + 1 and
A3: [m,k] = x by Def3;
x in {[2*n+3,k]} by A1,XBOOLE_0:def 4;
then x = [2*n+3,k] by TARSKI:def 1;
then m = 2*n+3 by A3,XTUPLE_0:1;
hence thesis by A2,XREAL_1:6;
end;
Lm4: for n being Element of NAT holds 2*n + 1 <= 2*(n+1) + 1
proof
let n be Element of NAT;
2*(n+1) + 1 = 2*n + 1 + 2;
hence thesis by NAT_1:11;
end;
theorem Th16:
for n, k being Element of NAT holds PFCrt (n+1,k) = PFCrt (n,k)
\/ {[2*n+3,k]}
proof
let n,k be Element of NAT;
A1: 2*(n+1)+1 = 2*n+3;
thus PFCrt (n+1,k) c= PFCrt (n,k) \/ {[2*n+3,k]}
proof
let x be object;
assume x in PFCrt (n+1,k);
then consider m being odd Element of NAT such that
A2: m <= 2*(n+1) + 1 and
A3: [m,k] = x by Def3;
per cases by A2,NAT_1:9;
suppose
m <= 2*(n+1);
then m <= 2*n + 1 or m = 2*n + 1 + 1 by NAT_1:8;
then x in PFCrt (n,k) by A3,Def3;
hence thesis by XBOOLE_0:def 3;
end;
suppose
m = 2*(n+1) + 1;
then x in {[2*n+3,k]} by A3,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
end;
let x be object;
assume
A4: x in PFCrt (n,k) \/ {[2*n+3,k]};
per cases by A4,XBOOLE_0:def 3;
suppose
x in PFCrt (n,k);
then consider m being odd Element of NAT such that
A5: m <= 2*n + 1 and
A6: [m,k] = x by Def3;
2*n+1 <= 2*(n+1)+1 by Lm4;
then m <= 2*(n+1) + 1 by A5,XXREAL_0:2;
hence thesis by A6,Def3;
end;
suppose
x in {[2*n+3,k]};
then x = [2*n+3,k] by TARSKI:def 1;
hence thesis by A1,Def3;
end;
end;
Lm5: for n, n9 being Element of NAT holds not PFCrt (n+1,n9) c= PFCrt (n,n9)
proof
let n, n9 be Element of NAT;
set k = [2*n+3,n9];
PFCrt (n+1,n9) = PFCrt (n,n9) \/ {[2*n+3,n9]} by Th16;
then {k} c= PFCrt (n+1,n9) by XBOOLE_1:7;
then
A1: k in PFCrt (n+1,n9) by ZFMISC_1:31;
PFCrt (n,n9) misses {[2*n+3,n9]} by Th15;
then PFCrt (n,n9) /\ {[2*n+3,n9]} = {};
hence thesis by A1,ZFMISC_1:46;
end;
theorem Th17:
for n, k being Element of NAT holds PFCrt (n,k) c< PFCrt (n+1,k)
proof
let n,k be Element of NAT;
thus PFCrt (n,k) c= PFCrt (n+1,k)
proof
let x be object;
assume x in PFCrt (n,k);
then consider m being odd Element of NAT such that
A1: m <= 2*n + 1 and
A2: [m,k] = x by Def3;
2*n + 1 <= 2*(n+1) + 1 by Lm4;
then m <= 2*(n+1) + 1 by A1,XXREAL_0:2;
hence thesis by A2,Def3;
end;
thus thesis by Lm5;
end;
registration
let n, k be Element of NAT;
cluster PFArt (n, k) -> non empty;
coherence
proof
[2*n, k] in PFArt (n, k) by Def2;
hence thesis;
end;
end;
theorem Th18:
for n, m, k being Element of NAT holds not PFArt (n, m) c= PFCrt (k, m)
proof
let n, m, k be Element of NAT;
set x = [2*n,m];
A1: not x in PFCrt (k,m)
proof
assume x in PFCrt (k,m);
then ex m9 being odd Element of NAT st m9 <= 2*k + 1 & [m9,m] = x by Def3;
hence thesis by XTUPLE_0:1;
end;
x in PFArt (n, m) by Def2;
hence thesis by A1;
end;
Lm6: for n, k being Element of NAT holds PFCrt (n,k) c= PFCrt (n+1,k)
proof
let n, k be Element of NAT;
PFCrt (n,k) c< PFCrt (n+1,k) by Th17;
hence thesis;
end;
theorem
for n, m, k being Element of NAT st n <= k holds PFCrt (n,m) c= PFCrt (k,m)
proof
let n, m, k be Element of NAT;
assume n <= k;
then 2*n <= 2*k by NAT_1:4;
then
A1: 2*n + 1 <= 2*k + 1 by XREAL_1:6;
let x be object;
assume x in PFCrt (n, m);
then consider m9 being odd Element of NAT such that
A2: m9 <= 2*n + 1 and
A3: [m9,m] = x by Def3;
m9 <= 2*k + 1 by A1,A2,XXREAL_0:2;
hence thesis by A3,Def3;
end;
Lm7: for n, m, k being Element of NAT st n < k holds PFCrt (n,m) c= PFArt (k,m
)
proof
let n, m, k be Element of NAT;
assume n < k;
then 2*n < 2*k by XREAL_1:68;
then
A1: 2*n + 1 <= 2*k by NAT_1:13;
let x be object;
assume x in PFCrt (n,m);
then consider p being odd Element of NAT such that
A2: p <= 2*n + 1 and
A3: [p,m] = x by Def3;
p <= 2*k by A1,A2,XXREAL_0:2;
hence thesis by A3,Def2;
end;
theorem
for n being Element of NAT holds PFArt (1,n) = { [1,n], [2,n] }
proof
let n be Element of NAT;
thus PFArt (1, n) c= { [1,n], [2,n] }
proof
let x be object;
assume
A1: x in PFArt (1, n);
per cases by A1,Def2;
suppose ex m being odd Element of NAT st m <= 2*1 & [m,n] = x;
then consider m being odd Element of NAT such that
A2: m <= 2*1 & [m,n] = x;
m = 0 or ... or m = 2 by A2;
then x = [1,n] by A2;
hence thesis by TARSKI:def 2;
end;
suppose
[2*1,n] = x;
hence thesis by TARSKI:def 2;
end;
end;
let x be object;
assume
A3: x in { [1,n], [2,n] };
per cases by A3,TARSKI:def 2;
suppose
A4: x = [1,n];
1 <= 2 * 1;
hence thesis by A4,Def2,Lm2,Lm3;
end;
suppose
x = [2,n];
then x = [2*1,n];
hence thesis by Def2;
end;
end;
definition
let n, k be Nat;
func PFBrt (n,k) -> Element of Fin PFuncs (NAT, {k}) means
:Def4:
for x being object
holds x in it iff ( ex m being non zero Element of NAT st m <= n & x
= PFArt (m,k) ) or x = PFCrt (n,k);
existence
proof
defpred P[object] means
( ex m being non zero Element of NAT st m <= n & $1
= PFArt (m,k) ) or $1 = PFCrt (n,k);
consider X being set such that
A1: for x being object holds x in X iff x in PFuncs (NAT, {k}) & P[x]
from XBOOLE_0:sch 1;
A2: X c= bool [:Seg (2*n+1), {k}:]
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume
A3: x in X;
per cases by A1,A3;
suppose
A4: ex m being non zero Element of NAT st m <= n & x = PFArt (m,k );
A5: 2*n <= 2*n+1 by NAT_1:11;
consider m being non zero Element of NAT such that
A6: m <= n and
A7: x = PFArt (m,k) by A4;
2*m <= 2*n by A6,NAT_1:4;
then
A8: 2*m <= 2*n+1 by A5,XXREAL_0:2;
xx c= [:Seg (2*n+1), {k}:]
proof
let t be object;
assume
A9: t in xx;
per cases by A7,A9,Def2;
suppose
ex m1 being odd Element of NAT st m1 <= 2*m & [m1,k] = t;
then consider m1 being odd Element of NAT such that
A10: m1 <= 2*m and
A11: [m1,k] = t;
A12: 1 <= m1 by ABIAN:12;
m1 <= 2*n+1 by A8,A10,XXREAL_0:2;
then m1 in Seg (2*n+1) by A12,FINSEQ_1:1;
hence thesis by A11,ZFMISC_1:106;
end;
suppose
A13: [2*m,k] = t;
1 <= 2*m by NAT_1:14;
then 2*m in Seg (2*n+1) by A8,FINSEQ_1:1;
hence thesis by A13,ZFMISC_1:106;
end;
end;
hence thesis;
end;
suppose
A14: x = PFCrt (n,k);
xx c= [:Seg (2*n+1), {k}:]
proof
let t be object;
assume t in xx;
then consider m being odd Element of NAT such that
A15: m <= 2*n + 1 and
A16: [m,k] = t by A14,Def3;
1 <= m by ABIAN:12;
then m in Seg (2*n+1) by A15,FINSEQ_1:1;
hence thesis by A16,ZFMISC_1:106;
end;
hence thesis;
end;
end;
X c= PFuncs (NAT, {k})
by A1;
then reconsider X as Element of Fin PFuncs (NAT, {k}) by A2,FINSUB_1:def 5;
take X;
let x be object;
thus x in X implies ( ex m being non zero Element of NAT st m <= n & x =
PFArt (m,k) ) or x = PFCrt (n,k) by A1;
assume ( ex m being non zero Element of NAT st m <= n & x = PFArt (m,k)
) or x = PFCrt (n,k);
hence thesis by A1;
end;
uniqueness
proof
defpred P[object] means
( ex m being non zero Element of NAT st m <= n & $1
= PFArt (m,k) ) or $1 = PFCrt (n,k);
A17: for X1,X2 being Element of Fin PFuncs (NAT, {k}) st
(for x being object
holds x in X1 iff P[x]) &
(for x being object holds x in X2 iff P[x]) holds X1 =
X2 from LMOD_7:sch 1;
let X1,X2 being Element of Fin PFuncs (NAT, {k});
assume ( for x being object holds x in X1 iff P[x])&
for x being object holds
x in X2 iff P [x];
hence thesis by A17;
end;
end;
theorem
for n, k being Element of NAT, x being set st x in PFBrt (n+1,k) holds
ex y being set st y in PFBrt (n,k) & y c= x
proof
let n, k be Element of NAT, x be set;
assume
A1: x in PFBrt (n+1,k);
per cases by A1,Def4;
suppose
ex m being non zero Element of NAT st m <= n+1 & x = PFArt (m,k);
then consider m being non zero Element of NAT such that
A2: m <= n+1 and
A3: x = PFArt (m,k);
thus ex y being set st y in PFBrt (n,k) & y c= x
proof
per cases by A2,NAT_1:8;
suppose
A4: m <= n;
take y = x;
thus y in PFBrt (n,k) by A3,A4,Def4;
thus thesis;
end;
suppose
A5: m = n+1;
take PFCrt (n,k);
n < n+1 by NAT_1:13;
hence thesis by A3,A5,Def4,Lm7;
end;
end;
end;
suppose
A6: x = PFCrt (n+1,k);
take y = PFCrt (n,k);
thus y in PFBrt (n,k) by Def4;
thus thesis by A6,Lm6;
end;
end;
theorem
for n, k being Element of NAT holds not PFCrt (n,k) in PFBrt (n+1,k)
proof
let n, k be Element of NAT;
assume PFCrt (n,k) in PFBrt (n+1,k);
then
( ex m being non zero Element of NAT st m <= n+1 & PFCrt (n,k) = PFArt
(m,k) ) or PFCrt (n,k) = PFCrt (n+1,k) by Def4;
hence thesis by Th17,Th18;
end;
Lm8: for n, k being Element of NAT, x being set st x in PFBrt (n,k) holds x is
finite
proof
let n,k be Element of NAT, x be set;
assume x in PFBrt (n,k);
then
A1: ( ex m being non zero Element of NAT st m <= n & x = PFArt (m,k) ) or x
= PFCrt (n,k) by Def4;
per cases by A1;
suppose
ex m being Element of NAT st m <= n & x = PFArt (m,k);
hence thesis;
end;
suppose
x = PFCrt (n,k);
hence thesis;
end;
end;
theorem Th23:
for n, m, k being Element of NAT st PFArt (n,m) c= PFArt (k,m) holds n = k
proof
let n, m, k be Element of NAT;
assume
A1: PFArt (n,m) c= PFArt (k,m);
assume n <> k;
then 2*n <> 2*k;
then
A2: [2*n,m] <> [2*k,m] by XTUPLE_0:1;
[2*n,m] in PFArt (n,m) by Def2;
then ex m9 being odd Element of NAT st m9 <= 2*k & [m9,m] = [ 2*n,m] by A1,A2
,Def2;
hence thesis by XTUPLE_0:1;
end;
theorem Th24:
for n, m, k being Element of NAT holds PFCrt (n,m) c= PFArt (k,m ) iff n < k
proof
let n, m, k be Element of NAT;
thus PFCrt (n,m) c= PFArt (k,m) implies n < k
proof
assume
A1: PFCrt (n,m) c= PFArt (k,m);
assume
A2: k <= n;
A3: not [2*n+1,m] in PFArt (k,m)
proof
assume
A4: [2*n+1,m] in PFArt (k,m);
per cases by A4,Def2;
suppose
A5: ex m9 being odd Element of NAT st m9 <= 2*k & [m9,m] = [2*n+1, m];
A6: 2*k <= 2*n by A2,NAT_1:4;
2*n+1 <= 2*k by A5,XTUPLE_0:1;
hence thesis by A6,NAT_1:13;
end;
suppose
[2*k,m] = [2*n+1,m];
hence thesis by XTUPLE_0:1;
end;
end;
[2*n+1,m] in PFCrt (n,m) by Def3;
hence thesis by A1,A3;
end;
thus thesis by Lm7;
end;
begin :: Incompleteness
theorem Th25:
for n, k being Element of NAT holds PFBrt (n,k) is Element of
SubstPoset (NAT, {k})
proof
let n, k be Element of NAT;
A1: for s, t being Element of PFuncs (NAT,{k}) holds ( s in PFBrt (n,k) & t
in PFBrt (n,k) & s c= t implies s = t )
proof
let s, t be Element of PFuncs (NAT,{k});
assume that
A2: s in PFBrt (n,k) and
A3: t in PFBrt (n,k) and
A4: s c= t;
A5: ( ex m being non zero Element of NAT st m <= n & s = PFArt (m,k) ) or
s = PFCrt (n,k) by A2,Def4;
A6: ( ex m being non zero Element of NAT st m <= n & t = PFArt (m,k) ) or
t = PFCrt (n,k) by A3,Def4;
per cases by A5,A6;
suppose
( ex m being Element of NAT st m <= n & s = PFArt (m,k) ) & ex m
being Element of NAT st m <= n & t = PFArt (m,k);
hence thesis by A4,Th23;
end;
suppose
( ex m being Element of NAT st m <= n & s = PFArt (m,k) ) & t =
PFCrt (n,k);
hence thesis by A4,Th18;
end;
suppose
s = PFCrt (n,k) & ex m being Element of NAT st m <= n & t = PFArt (m,k);
hence thesis by A4,Th24;
end;
suppose
s = PFCrt (n,k) & t = PFCrt (n,k);
hence thesis;
end;
end;
for u being set st u in PFBrt (n,k) holds u is finite by Lm8;
then SubstitutionSet (NAT, {k}) = the carrier of SubstPoset (NAT, {k}) &
PFBrt (n,k) in { A where A is Element of Fin PFuncs (NAT,{k}) : ( for u being
set st u in A holds u is finite ) & for s, t being Element of PFuncs (NAT,{k})
holds ( s in A & t in A & s c= t implies s = t ) } by A1,SUBSTLAT:def 4;
hence thesis by SUBSTLAT:def 1;
end;
definition
let k be Element of NAT;
func PFDrt k -> Subset of SubstPoset (NAT, {k}) means
:Def5:
for x being object
holds x in it iff ex n being non zero Element of NAT st x = PFBrt (n,k);
existence
proof
defpred P[object] means
ex n being non zero Element of NAT st $1 = PFBrt (n,k);
consider X being set such that
A1: for x being object holds x in X iff x in the carrier of SubstPoset (
NAT, {k}) & P[x] from XBOOLE_0:sch 1;
X c= the carrier of SubstPoset (NAT, {k})
by A1;
then reconsider X9 = X as Subset of SubstPoset (NAT, {k});
take X9;
let x be object;
thus x in X9 implies ex n being non zero Element of NAT st x = PFBrt (n,k
) by A1;
given n being non zero Element of NAT such that
A2: x = PFBrt (n, k);
x is Element of SubstPoset (NAT, {k}) by A2,Th25;
hence thesis by A1,A2;
end;
uniqueness
proof
defpred P[object] means
ex n being non zero Element of NAT st $1 = PFBrt (n,k);
A3: for A1, A2 being Subset of SubstPoset (NAT, {k}) st
(for x being object
holds x in A1 iff P[x]) &
(for x being object holds x in A2 iff P[x]) holds A1 =
A2 from SSubsetUniq;
let A1, A2 being Subset of SubstPoset (NAT, {k});
assume ( for x being object holds x in A1 iff P[x])&
for x being object holds x
in A2 iff P [x];
hence thesis by A3;
end;
end;
theorem
for k being Element of NAT holds PFBrt (1,k) = { PFArt (1,k), PFCrt (1 ,k) }
proof
let k be Element of NAT;
thus PFBrt (1,k) c= { PFArt (1,k), PFCrt (1,k) }
proof
let x be object;
assume
A1: x in PFBrt (1,k);
per cases by A1,Def4;
suppose
ex m being non zero Element of NAT st m <= 1 & x = PFArt (m,k);
then consider m being non zero Element of NAT such that
A2: m <= 1 and
A3: x = PFArt (m,k);
m >= 1 by NAT_1:14;
then m = 1 by A2,XXREAL_0:1;
hence thesis by A3,TARSKI:def 2;
end;
suppose
x = PFCrt (1,k);
hence thesis by TARSKI:def 2;
end;
end;
let x be object;
assume
A4: x in { PFArt (1,k), PFCrt (1,k) };
per cases by A4,TARSKI:def 2;
suppose
x = PFArt (1,k);
hence thesis by Def4;
end;
suppose
x = PFCrt (1,k);
hence thesis by Def4;
end;
end;
theorem Th27:
for k being Element of NAT holds PFBrt (1,k) <> {{}}
proof
let k be Element of NAT;
PFArt (1,k) in PFBrt (1,k) by Def4;
hence thesis by TARSKI:def 1;
end;
registration
let k be Element of NAT;
cluster PFBrt (1,k) -> non empty;
coherence
proof
PFArt (1,k) in PFBrt (1,k) by Def4;
hence thesis;
end;
end;
theorem Th28:
for n, k being Element of NAT holds { PFArt (n,k) } is Element
of SubstPoset (NAT, {k})
proof
let n, k be Element of NAT;
SubstitutionSet (NAT, {k}) = the carrier of SubstPoset (NAT, {k}) by
SUBSTLAT:def 4;
hence thesis by HEYTING2:2;
end;
theorem Th29:
for k being Element of NAT, V, X being set, a being Element of
SubstPoset (V, {k}) st X in a holds X is finite Subset of [:V, {k}:]
proof
let k be Element of NAT;
let V, X be set;
let a be Element of SubstPoset (V, {k});
assume
A1: X in a;
A2: PFuncs (V, {k}) c= bool [:V, {k}:] by PRE_POLY:16;
A3: SubstitutionSet (V, {k}) = the carrier of SubstPoset (V, {k}) by
SUBSTLAT:def 4;
then a in SubstitutionSet (V, {k});
then a c= PFuncs (V, {k}) by FINSUB_1:def 5;
then X in PFuncs (V, {k}) by A1;
hence thesis by A3,A1,A2,HEYTING2:1;
end;
theorem Th30:
for m being Element of NAT, a being Element of SubstPoset (NAT,
{m}) st PFDrt m is_>=_than a holds for X being non empty set st X in a holds
not ( for n being Element of NAT st [n,m] in X holds n is odd )
proof
let m be Element of NAT;
let a be Element of SubstPoset (NAT, {m});
assume
A1: PFDrt m is_>=_than a;
let X be non empty set;
assume
A2: X in a;
then reconsider X9= X as finite non empty Subset of [:NAT,{m}:] by Th29;
assume
A3: for n being Element of NAT st [n,m] in X holds n is odd;
A4: now
let k be non zero Element of NAT;
reconsider Pk = PFBrt (k,m) as Element of SubstPoset (NAT, {m}) by Th25;
A5: [2*k+1,m] in PFCrt (k,m) by Def3;
Pk in PFDrt m by Def5;
then a <= Pk by A1;
then consider y being set such that
A6: y in Pk and
A7: y c= X by A2,Th12;
A8: not ex m9 being Element of NAT st m9 <= k & y = PFArt (m9,m)
proof
given m9 being Element of NAT such that
m9 <= k and
A9: y = PFArt (m9,m);
[2*m9,m] in PFArt (m9,m) by Def2;
hence thesis by A3,A7,A9;
end;
( ex m9 being non zero Element of NAT st m9 <= k & y = PFArt (m9,m) )
or y = PFCrt (k,m) by A6,Def4;
hence [2*k+1,m] in X by A7,A8,A5;
end;
ex l being non zero Element of NAT st not [2*l+1,m] in X9 by Th4;
hence thesis by A4;
end;
theorem Th31:
for k being Element of NAT, a, b being Element of SubstPoset (
NAT, {k}), X being Subset of SubstPoset (NAT, {k}) st a is_<=_than X & b
is_<=_than X holds a "\/" b is_<=_than X
proof
let k be Element of NAT;
let a, b be Element of SubstPoset (NAT, {k}), X be Subset of SubstPoset (NAT
, {k});
assume
A1: a is_<=_than X & b is_<=_than X;
let c be Element of SubstPoset (NAT, {k});
assume c in X;
then a <= c & b <= c by A1;
hence thesis by YELLOW_5:9;
end;
registration
let k be Element of NAT;
cluster non empty for Element of SubstPoset (NAT, {k});
existence
proof
SubstitutionSet (NAT, {k}) = the carrier of SubstPoset (NAT, {k}) by
SUBSTLAT:def 4;
then reconsider E = {{}} as Element of SubstPoset (NAT, {k}) by SUBSTLAT:2;
take E;
thus thesis;
end;
end;
Lm9: for a being non empty set st a <> {{}} & {} in a ex b being set st b in a
& b <> {}
proof
let a be non empty set;
assume that
A1: a <> {{}} and
A2: {} in a;
assume
A3: for b being set st b in a holds b = {};
a = {{}}
proof
thus a c= {{}}
proof
let x be object;
assume x in a;
then x = {} by A3;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {{}};
hence thesis by A2,TARSKI:def 1;
end;
hence thesis by A1;
end;
theorem Th32:
for n being Element of NAT, a being Element of SubstPoset (NAT,
{n}) st {} in a holds a = {{}}
proof
let n be Element of NAT;
let a be Element of SubstPoset (NAT, {n});
assume
A1: {} in a;
SubstitutionSet (NAT, {n}) = the carrier of SubstPoset (NAT, {n}) by
SUBSTLAT:def 4;
then
A2: a in SubstitutionSet (NAT, {n});
assume a <> {{}};
then ex k being set st k in a & k <> {} by A1,Lm9;
hence thesis by A2,A1,SUBSTLAT:5,XBOOLE_1:2;
end;
theorem Th33:
for k being Element of NAT, a being non empty Element of
SubstPoset (NAT, {k}) st a <> {{}} ex f being finite Function st f in a & f <>
{}
proof
let k be Element of NAT;
let a be non empty Element of SubstPoset (NAT, {k});
assume
A1: a <> {{}};
consider f being object such that
A2: f in a by XBOOLE_0:def 1;
SubstitutionSet (NAT, {k}) = the carrier of SubstPoset (NAT, {k}) by
SUBSTLAT:def 4;
then reconsider f as finite Function by A2,HEYTING2:1;
take f;
thus f in a by A2;
assume f = {};
hence thesis by A1,A2,Th32;
end;
theorem Th34:
for k being Element of NAT, a being non empty Element of
SubstPoset (NAT, {k}), a9 being Element of Fin PFuncs (NAT, {k}) st a <> {{}} &
a = a9 holds Involved a9 is finite non empty Subset of NAT
proof
let k be Element of NAT;
let a be non empty Element of SubstPoset (NAT, {k});
let a9 be Element of Fin PFuncs (NAT, {k});
assume that
A1: a <> {{}} and
A2: a = a9;
consider f being finite Function such that
A3: f in a and
A4: f <> {} by A1,Th33;
ex k1 being object st k1 in dom f by A4,XBOOLE_0:def 1;
hence thesis by A2,A3,HEYTING2:6,def 1;
end;
theorem Th35:
for k being Element of NAT, a being Element of SubstPoset (NAT,
{k}), a9 being Element of Fin PFuncs (NAT, {k}), B being finite non empty
Subset of NAT st B = Involved a9 & a9 = a holds for X being set st X in a for l
being Element of NAT st l > (max B) + 1 holds not [l,k] in X
proof
let k be Element of NAT, a be Element of SubstPoset (NAT, {k}), a9 be
Element of Fin PFuncs (NAT, {k}), B be finite non empty Subset of NAT;
assume that
A1: B = Involved a9 and
A2: a9 = a;
let X be set;
assume
A3: X in a;
SubstitutionSet (NAT, {k}) = the carrier of SubstPoset (NAT, {k}) by
SUBSTLAT:def 4;
then reconsider X9 = X as finite Function by A3,HEYTING2:1;
let l be Element of NAT;
assume
A4: l > max B + 1;
assume [l,k] in X;
then l in dom X9 by XTUPLE_0:def 12;
then l in Involved a9 by A2,A3,HEYTING2:def 1;
then max B + 1 >= max B & max B >= l by A1,NAT_1:11,XXREAL_2:def 8;
hence thesis by A4,XXREAL_0:2;
end;
theorem Th36:
for k being Element of NAT holds Top SubstPoset (NAT, {k}) = {{} }
proof
let k be Element of NAT;
SubstitutionSet (NAT, {k}) = the carrier of SubstPoset (NAT, {k}) by
SUBSTLAT:def 4;
then reconsider a = {{}} as Element of SubstPoset (NAT, {k}) by SUBSTLAT:2;
A1: for b being Element of SubstPoset (NAT, {k}) st b is_<=_than {} holds a
>= b
proof
let b be Element of SubstPoset (NAT, {k});
assume b is_<=_than {};
now
let x be set;
assume x in b;
take y = {};
thus y in a & y c= x by TARSKI:def 1;
end;
hence thesis by Th12;
end;
a is_<=_than {};
then a = "/\"({},SubstPoset (NAT, {k})) by A1,YELLOW_0:31;
hence thesis by YELLOW_0:def 12;
end;
theorem Th37:
for k being Element of NAT holds Bottom SubstPoset (NAT, {k}) = {}
proof
let k be Element of NAT;
SubstitutionSet (NAT, {k}) = the carrier of SubstPoset (NAT, {k}) by
SUBSTLAT:def 4;
then reconsider a = {} as Element of SubstPoset (NAT, {k}) by SUBSTLAT:1;
A1: for b being Element of SubstPoset (NAT, {k}) st b is_>=_than {} holds a
<= b
proof
let b be Element of SubstPoset (NAT, {k});
assume b is_>=_than {};
for x be set st x in a ex y being set st y in b & y c= x;
hence thesis by Th12;
end;
a is_>=_than {};
then a = "\/"({},SubstPoset (NAT, {k})) by A1,YELLOW_0:30;
hence thesis by YELLOW_0:def 11;
end;
theorem Th38:
for k being Element of NAT, a, b being Element of SubstPoset (
NAT, {k}) st a <= b & a = {{}} holds b = {{}}
proof
let k be Element of NAT, a, b be Element of SubstPoset (NAT, {k});
assume
A1: a <= b & a = {{}};
Top SubstPoset (NAT, {k}) = {{}} by Th36;
hence thesis by A1,WAYBEL15:3;
end;
theorem Th39:
for k being Element of NAT, a, b being Element of SubstPoset (
NAT, {k}) st a <= b & b = {} holds a = {}
proof
let k be Element of NAT, a, b be Element of SubstPoset (NAT, {k});
assume
A1: a <= b & b = {};
Bottom SubstPoset (NAT, {k}) = {} by Th37;
hence thesis by A1,YELLOW_5:19;
end;
theorem Th40:
for m being Element of NAT, a being Element of SubstPoset (NAT,
{m}) st PFDrt m is_>=_than a holds a <> {{}}
proof
let m be Element of NAT;
reconsider P1 = PFBrt (1,m) as Element of SubstPoset (NAT, {m}) by Th25;
let a be Element of SubstPoset (NAT, {m});
assume
A1: PFDrt m is_>=_than a;
PFBrt (1,m) in PFDrt m by Def5;
then
A2: P1 >= a by A1;
assume
A3: a = {{}};
Top SubstPoset (NAT, {m}) = {{}} by Th36;
hence thesis by A3,A2,Th27,WAYBEL15:3;
end;
Lm10: for m being Element of NAT holds SubstPoset (NAT, {m}) is not complete
proof
let m be Element of NAT;
reconsider Cos = { PFArt (1,m) } as Element of SubstPoset (NAT, {m}) by Th28;
assume SubstPoset (NAT, {m}) is complete;
then consider a being Element of SubstPoset (NAT, {m}) such that
A1: PFDrt m is_>=_than a and
A2: for b being Element of SubstPoset (NAT, {m}) st PFDrt m is_>=_than b
holds a >= b by LATTICE5:def 2;
SubstitutionSet (NAT, {m}) = the carrier of SubstPoset (NAT, {m}) by
SUBSTLAT:def 4;
then a in SubstitutionSet (NAT, {m});
then reconsider a9 = a as Element of Fin PFuncs (NAT, {m});
set Mi = Involved a9;
PFDrt m is_>=_than Cos
proof
let u be Element of SubstPoset (NAT, {m});
assume u in PFDrt m;
then consider n1 being non zero Element of NAT such that
A3: u = PFBrt (n1,m) by Def5;
now
let d be set;
assume d in Cos;
then
A4: d = PFArt (1,m) by TARSKI:def 1;
1 <= n1 by NAT_1:14;
then d in PFBrt (n1,m) by A4,Def4;
hence ex e be set st e in u & e c= d by A3;
end;
hence thesis by Th12;
end;
then a <> {} by A2,Th39;
then reconsider Mi as finite non empty Subset of NAT by A1,Th34,Th40;
reconsider mX = max Mi + 1 as non zero Element of NAT;
reconsider Sum = { PFArt (mX,m) } as Element of SubstPoset (NAT, {m}) by Th28
;
set b = a "\/" Sum;
Sum is_<=_than PFDrt m
proof
let t be Element of SubstPoset (NAT, {m});
assume t in PFDrt m;
then consider n being non zero Element of NAT such that
A5: t = PFBrt (n,m) by Def5;
for x being set st x in Sum ex y being set st y in t & y c= x
proof
let x be set;
assume
A6: x in Sum;
then
A7: x = PFArt (mX,m) by TARSKI:def 1;
per cases;
suppose
A8: n < mX;
take y = PFCrt (n,m);
thus y in t by A5,Def4;
thus thesis by A7,A8,Lm7;
end;
suppose
A9: n >= mX;
take y = PFArt (mX,m);
thus y in t by A5,A9,Def4;
thus thesis by A6,TARSKI:def 1;
end;
end;
hence Sum <= t by Th12;
end;
then
A10: PFDrt m is_>=_than b by A1,Th31;
A11: a <> b
proof
A12: PFArt (mX,m) in Sum by TARSKI:def 1;
assume
A13: a = b;
then Sum <= a by YELLOW_0:24;
then consider g being set such that
A14: g in a and
A15: g c= PFArt (mX,m) by A12,Th12;
per cases;
suppose
g is non empty;
then consider n being Element of NAT such that
A16: [n,m] in g and
A17: n is even by A1,A14,Th30;
now
per cases by A15,A16,Def2;
suppose
ex m9 being odd Element of NAT st m9 <= 2*mX & [m9,m] = [n, m];
hence thesis by A17,XTUPLE_0:1;
end;
suppose
[2*mX,m] = [n,m];
hence thesis by A14,A16,Th35,XREAL_1:155;
end;
end;
hence thesis;
end;
suppose
A18: g is empty;
reconsider P1 = PFBrt (1,m) as Element of SubstPoset (NAT, {m}) by Th25;
PFBrt (1,m) in PFDrt m by Def5;
then
A19: P1 >= b by A10;
PFBrt (1,m) <> {{}} by Th27;
hence thesis by A13,A14,A18,A19,Th32,Th38;
end;
end;
a <= b by YELLOW_0:22;
then a < b by A11,ORDERS_2:def 6;
hence contradiction by A2,A10,ORDERS_2:6;
end;
registration
let m be Element of NAT;
cluster SubstPoset (NAT, {m}) -> non complete;
coherence by Lm10;
end;
registration
let m be Element of NAT;
cluster SubstLatt (NAT, {m}) -> non complete;
coherence
proof
assume SubstLatt (NAT, {m}) is complete;
then reconsider K = SubstLatt (NAT, {m}) as complete Lattice;
LattPOSet K is complete & SubstPoset (NAT, {m}) is non complete;
hence thesis;
end;
end;