Copyright (c) 1994 Association of Mizar Users
environ
vocabulary FINSET_1, FUNCT_1, RELAT_1, FUNCOP_1, FUNCT_4, BOOLE, SQUARE_1,
FINSUB_1, SETWISEO, PBOOLE, TDGROUP, FINSEQ_1, CARD_3, ZF_REFLE, TARSKI,
FUNCT_5, FUNCT_2, PRALG_1, PRALG_2, MCART_1, FINSEQ_2, TREES_1, TREES_3,
TREES_2, FUNCT_6, TREES_4, CQC_LANG, CARD_1, PRE_CIRC, ORDINAL2, ARYTM,
MEMBERED, SEQ_2, SEQ_4, ARYTM_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, REAL_1, NAT_1, MCART_1, CARD_1, ORDINAL2, MEMBERED, SEQ_4,
RELAT_1, FUNCT_1, FINSET_1, FINSUB_1, SETWISEO, FUNCT_2, FUNCOP_1,
FUNCT_4, CARD_3, TREES_1, TREES_2, TREES_3, TREES_4, FUNCT_5, FUNCT_6,
PBOOLE, PRALG_1, MSUALG_1, PRALG_2, CQC_LANG, FINSEQ_1, FINSEQ_2;
constructors WELLORD2, NAT_1, SETWISEO, PRALG_2, CQC_LANG, XCMPLX_0, XREAL_0,
MEMBERED, SEQ_4, PSCOMP_1, XBOOLE_0;
clusters NUMBERS, SUBSET_1, FINSET_1, AMI_1, TREES_1, TREES_2, TREES_3,
DTCONSTR, PRELAMB, PRALG_1, MSUALG_1, PRVECT_1, FUNCT_1, RELSET_1,
XREAL_0, ARYTM_3, FINSEQ_1, REAL_1, FRAENKEL, MEMBERED, XBOOLE_0,
ORDINAL2;
requirements NUMERALS, REAL, BOOLE, SUBSET;
definitions TARSKI, PRALG_1, RELAT_1, MSUALG_1, WELLORD2, FUNCT_1, PBOOLE,
XBOOLE_0, SEQ_4;
theorems AXIOMS, TARSKI, ZFMISC_1, FINSUB_1, FINSEQ_1, FINSEQ_2, FINSEQ_3,
GRFUNC_1, FUNCT_1, FUNCT_2, FUNCT_4, FUNCT_5, TREES_1, TREES_2, TREES_3,
TREES_4, NAT_1, RELAT_1, CARD_3, ORDERS_1, FUNCOP_1, MCART_1, PBOOLE,
PRALG_2, MSUALG_1, CQC_LANG, CARD_2, CARD_1, FUNCT_6, REAL_1, FINSET_1,
AMI_1, RELSET_1, XBOOLE_0, XBOOLE_1, PARTFUN1, XCMPLX_1, MEMBERED,
PSCOMP_1, SEQ_4;
schemes SETWISEO, DOMAIN_1, MSUALG_1, MSUALG_2, RECDEF_1, FUNCT_1, FRAENKEL,
FINSEQ_1;
begin
scheme FraenkelFinIm{ A() -> finite non empty set, F(set) -> set, P[set] }:
{ F(x) where x is Element of A() : P[x] } is finite
proof
A1: A() is finite;
deffunc G(Element of A()) = F($1);
set B = { G(x) where x is Element of A() : x in A() };
A2: B is finite from FraenkelFin(A1);
{ F(x) where x is Element of A() : P[x] } c= B
proof let a be set;
assume a in { F(x) where x is Element of A() : P[x] };
then consider b being Element of A() such that
A3: F(b) = a and P[b];
thus thesis by A3;
end;
hence thesis by A2,FINSET_1:13;
end;
canceled;
theorem
for f being Function, x, y being set st dom f = {x} & rng f = {y}
holds f = { [x,y] }
proof
let f be Function,
x, y be set;
assume dom f = {x} & rng f = {y};
then f = {x} --> y by FUNCOP_1:15;
then f = [: {x}, {y} :] by FUNCOP_1:def 2;
hence f = { [x,y] } by ZFMISC_1:35;
end;
theorem Th3:
for f, g, h being Function st f c= g holds f +* h c= g +* h
proof
let f, g, h be Function;
assume
A1: f c= g;
then A2: dom f c= dom g by RELAT_1:25;
now
dom (f +* h) = dom f \/ dom h & dom (g +* h) = dom g \/ dom h
by FUNCT_4:def 1;
hence
dom (f +* h) c= dom (g +* h) by A2,XBOOLE_1:9;
let x be set;
assume
x in dom (f +* h);
then A3: x in dom f or x in dom h by FUNCT_4:13;
per cases;
suppose
A4: x in dom h;
hence (f +* h).x = h.x by FUNCT_4:14 .= (g +* h).x
by A4,FUNCT_4:14;
suppose
A5: not x in dom h;
then A6: (f +* h).x = f.x by FUNCT_4:12;
(g +* h).x = g.x by A5,FUNCT_4:12;
hence (f +* h).x = (g +* h).x by A1,A3,A5,A6,GRFUNC_1:8;
end;
hence f +* h c= g +* h by GRFUNC_1:8;
end;
theorem
for f, g, h being Function st f c= g & dom f misses dom h
holds f c= g +* h
proof
let f, g, h be Function;
assume f c= g;
then A1: f +* h c= g +* h by Th3;
assume
dom f misses dom h;
then f c= f +* h by FUNCT_4:33;
hence f c= g +* h by A1,XBOOLE_1:1;
end;
definition
cluster finite non empty natural-membered set;
existence
proof
consider A being finite non empty Subset of NAT;
take A;
thus A is finite non empty natural-membered;
end;
end;
definition let A be finite non empty real-membered set;
reconsider X' = A as finite non empty Subset of REAL by MEMBERED:2;
reconsider X' as Finite_Subset of REAL by FINSUB_1:def 5;
defpred P[Finite_Subset of REAL] means
$1 <> {}.REAL implies
ex m being Real st m in $1 & for x being Real st x in $1 holds x<=m;
A1: P[{}.REAL];
A2: now
let B be (Element of Fin REAL), b be Real;
assume
A3: P[B];
thus P[B \/ {b}]
proof
per cases;
suppose A4: B = {}.REAL;
assume B \/ {b} <> {}.REAL;
take bb = b;
bb in {b} by TARSKI:def 1;
hence bb in B \/ {b} by XBOOLE_0:def 2;
let x be Real;
assume x in B \/ {b};
hence x <= bb by A4,TARSKI:def 1;
suppose B <> {}.REAL; then consider m being Real such that
A5: m in B and
A6: for x being Real st x in B holds x <= m by A3;
now
per cases;
suppose
A7: m <= b;
take bb = b;
bb in {b} by TARSKI:def 1;
hence bb in B \/ {b} by XBOOLE_0:def 2;
let x be Real;
assume x in B \/ {b};
then x in B or x in {b} by XBOOLE_0:def 2;
then x <= m or x = b by A6,TARSKI:def 1;
hence x <= bb by A7,AXIOMS:22;
suppose
A8: b <= m;
take m;
thus m in B \/ {b} by A5,XBOOLE_0:def 2;
let x be Real;
assume x in B \/ {b};
then x in B or x in {b} by XBOOLE_0:def 2;
hence x <= m by A6,A8,TARSKI:def 1;
end;
hence P[B \/ {b}];
end;
end;
for B being Element of Fin REAL holds P[B] from FinSubInd3 (A1, A2);
then consider m being Real such that
A9: m in X' and
A10: for x being Real st x in X' holds x<=m;
A11: A is bounded_above
proof take m;
thus for r being real number st r in A holds r<=m by A10;
end;
reconsider X' as finite Subset of REAL;
A12: upper_bound A in A
proof :: jakim cudem to akceptuje, musi pluskwa ?
A13: for p being real number st p in X' holds m >= p by A10;
for q being real number st
for p being real number st p in X' holds q >= p holds q >= m
by A9;
hence thesis by A9,A13,PSCOMP_1:11;
end;
redefine func upper_bound A -> real number means
:Def1: it in A & for k being real number st k in A holds k <= it;
compatibility
proof let n be real number;
thus n = upper_bound A implies n in A &
for k being real number st k in A holds k <= n
by A11,A12,SEQ_4:def 4;
assume that
A14: n in A and
A15: for k being real number st k in A holds k <= n;
A16: for s being real number st s in A holds s <= n by A15;
for s being real number st 0<s ex r being real number st r in A & n-s < r
proof let s be real number such that
A17: 0<s;
take n;
thus n in A by A14;
n < n+s by A17,REAL_1:69;
hence n-s < n by REAL_1:84;
end;
hence n = upper_bound A by A11,A16,SEQ_4:def 4;
end;
coherence;
synonym max A;
end;
definition
let X be finite non empty natural-membered set;
canceled;
cluster max X -> natural;
coherence
proof max X in X by Def1;
hence max X is natural by MEMBERED:def 5;
end;
end;
begin
::---------------------------------------------------------------------------
:: Many Sorted Sets and Functions
::---------------------------------------------------------------------------
theorem
for I being set, MSS being ManySortedSet of I
holds MSS#.<*>I = {{}}
proof
let I be set, MSS be ManySortedSet of I;
reconsider eI = <*>I as Element of I* by FINSEQ_1:66;
thus MSS#.<*>I = product (MSS*eI) by MSUALG_1:def 3
.= {{}} by CARD_3:19,RELAT_1:62;
end;
reserve i,j,x,y for set,
g for Function;
scheme
MSSLambda2Part { I() -> set, P [set], F, G (set) -> set }:
ex f being ManySortedSet of I() st
for i being Element of I() st i in I()
holds (P[i] implies f.i = F(i)) & (not P[i] implies f.i = G(i))
proof
defpred Q[set,set] means
(P[$1] implies $2 = F($1)) & (not P[$1] implies $2 = G($1));
A1: now let i such that i in I();
thus ex j st Q[i,j]
proof
per cases;
suppose A2: P[i]; take F(i); thus thesis by A2;
suppose A3: not P[i]; take G(i); thus thesis by A3;
end;
end;
consider f being ManySortedSet of I() such that
A4: for i st i in I() holds Q[i,f.i] from MSSEx(A1);
take f;
thus thesis by A4;
end;
definition
let I be set;
let IT be ManySortedSet of I;
attr IT is locally-finite means
for i being set st i in I holds IT.i is finite;
end;
definition
let I be set;
cluster non-empty locally-finite ManySortedSet of I;
existence
proof
reconsider f = I --> {{}} as Function;
dom f = I by FUNCOP_1:19;
then reconsider f as ManySortedSet of I by PBOOLE:def 3;
take f;
thus f is non-empty
proof
let i be set;
assume i in I;
hence f.i is non empty by FUNCOP_1:13;
end;
thus f is locally-finite
proof
let i be set;
assume i in I;
hence f.i is finite by FUNCOP_1:13;
end;
end;
end;
definition
let I, A be set;
redefine func I --> A -> ManySortedSet of I;
coherence
proof
set f = I --> A;
dom f = I by FUNCOP_1:19;
hence f is ManySortedSet of I by PBOOLE:def 3;
end;
end;
definition
let I be set, M be ManySortedSet of I, A be Subset of I;
redefine func M | A -> ManySortedSet of A;
coherence
proof
set B = M | A;
A1: dom B = dom M /\ A by RELAT_1:90;
dom M = I by PBOOLE:def 3;
then dom B = A by A1,XBOOLE_1:28;
hence thesis by PBOOLE:def 3;
end;
end;
definition
let M be non-empty Function, A be set;
cluster M | A -> non-empty;
coherence
proof
rng(M|A) c= rng M by FUNCT_1:76;
hence not {} in rng(M|A) by RELAT_1:def 9;
end;
end;
theorem Th6:
for I being non empty set, B being non-empty ManySortedSet of I
holds union rng B is non empty
proof
let I be non empty set, B be non-empty ManySortedSet of I;
consider i being Element of I;
i in I; then i in dom B by PBOOLE:def 3;
then B.i <> {} & B.i in rng B by FUNCT_1:def 5;
hence union rng B is non empty by ORDERS_1:91;
end;
theorem Th7:
for I being set holds uncurry (I --> {}) = {}
proof
let I be set;
per cases;
suppose I = {};
then dom (I-->{}) = {} by FUNCOP_1:16;
hence thesis by FUNCT_5:50,RELAT_1:64;
suppose I <> {};
then rng (I --> {}) = {{}} by FUNCOP_1:14
.= Funcs({} qua set, {} qua set) by FUNCT_5:64;
then dom uncurry (I --> {}) = [:dom (I --> {}), {}:] by FUNCT_5:33
.= {} by ZFMISC_1:113;
hence thesis by RELAT_1:64;
end;
theorem
for I being non empty set, A being set,
B being non-empty ManySortedSet of I,
F being ManySortedFunction of (I --> A), B
holds dom commute F = A
proof
let I be non empty set, A be set, B be non-empty ManySortedSet of I,
F be ManySortedFunction of (I --> A), B;
A1: dom B = I & dom F = I by PBOOLE:def 3;
per cases;
suppose
A2: A is empty;
A3: rng F <> {} by A1,RELAT_1:65;
rng F c= {{}}
proof
let x be set;
assume
x in rng F;
then consider i being set such that
A4: i in I & x = F.i by A1,FUNCT_1:def 5;
A5: (I -->A).i = A by A4,FUNCOP_1:13;
x is Function of (I -->A).i, B.i by A4,MSUALG_1:def 2;
then x = {} by A2,A5,PARTFUN1:57;
hence thesis by TARSKI:def 1;
end;
then rng F = {{}} by A3,ZFMISC_1:39;
then A6: F = I --> {} by A1,FUNCOP_1:15;
commute F = curry' uncurry F by PRALG_2:def 5
.= {} by A6,Th7,FUNCT_5:49;
hence thesis by A2,RELAT_1:60;
suppose
A7: A is non empty;
union rng B is non empty by Th6;
then A8: Funcs (I, union rng B) is non empty by FUNCT_2:11;
rng F c= Funcs(A, union rng B)
proof
let x be set;
assume
x in rng F;
then consider i being set such that
A9: i in dom F & x = F.i by FUNCT_1:def 5;
(I -->A).i = A by A1,A9,FUNCOP_1:13;
then reconsider x' = x as Function of A, B.i by A1,A9,MSUALG_1:def 2;
B.i <> {} by A1,A9,PBOOLE:def 16;
then A10: dom x' = A & rng x' c= B.i by FUNCT_2:def 1,
RELSET_1:12;
B.i in rng B by A1,A9,FUNCT_1:def 5;
then B.i c= union rng B by ZFMISC_1:92;
then rng x' c= union rng B by A10,XBOOLE_1:1;
hence x in Funcs(A, union rng B) by A10,FUNCT_2:def 2;
end;
then F in Funcs (I, Funcs(A, union rng B)) by A1,FUNCT_2:def 2;
then commute F in Funcs (A, Funcs(I, union rng B)) by A7,PRALG_2:4;
then commute F is Function of A, Funcs(I, union rng B) by FUNCT_2:121;
hence dom commute F = A by A8,FUNCT_2:def 1;
end;
scheme
LambdaRecCorrD {D() -> non empty set,
A() -> Element of D(),
F(Nat, Element of D()) -> Element of D() } :
(ex f being Function of NAT, D() st f.0 = A()
& for i being Nat holds f.(i+1) = F(i, f.i))
& for f1, f2 being Function of NAT, D() st (f1.0 = A()
& for i being Nat holds f1.(i+1) = F(i, f1.i))
& (f2.0 = A() & for i being Nat holds f2.(i+1) = F(i,f2.i))
holds f1 = f2
proof
deffunc G(Nat,Element of D()) = F($1,$2);
thus ex f being Function of NAT, D() st f.0 = A()
& for i being Nat holds f.(i+1) = G(i,f.i) from LambdaRecExD;
let f1, f2 be Function of NAT, D() such that
A1: f1.0 = A() & for i being Nat holds f1.(i+1) = G(i,f1.i) and
A2: f2.0 = A() & for i being Nat holds f2.(i+1) = G(i,f2.i);
thus f1 = f2 from LambdaRecUnD(A1,A2);
end;
scheme
LambdaMSFD{J() -> non empty set, I() -> Subset of J(),
A, B() -> ManySortedSet of I(), F(set) -> set } :
ex f being ManySortedFunction of A(), B() st
for i being Element of J() st i in I() holds f.i = F(i)
provided
A1: for i being Element of J() st i in I()
holds F(i) is Function of A().i, B().i
proof
deffunc G(set) = F($1);
consider f being ManySortedSet of I() such that
A2: for i st i in I() holds f.i = G(i) from MSSLambda;
f is Function-yielding
proof let i;
assume i in dom f;
then A3: i in I() by PBOOLE:def 3;
then F(i) is Function by A1;
hence thesis by A2,A3;
end;
then reconsider f as ManySortedFunction of I();
f is ManySortedFunction of A(), B()
proof let i;
assume
A4: i in I();
then F(i) is Function of A().i, B().i by A1;
hence thesis by A2,A4;
end;
then reconsider f as ManySortedFunction of A(), B();
take f;
thus thesis by A2;
end;
definition
let F be non-empty Function, f be Function;
cluster F * f -> non-empty;
coherence
proof
rng(F*f) c= rng F by RELAT_1:45;
hence not {} in rng(F*f) by RELAT_1:def 9;
end;
end;
definition
let I be set, MSS be non-empty ManySortedSet of I;
cluster -> Function-like Relation-like Element of (product MSS);
coherence;
end;
theorem
for I being set, f being non-empty ManySortedSet of I, g being Function,
s being Element of product f
st dom g c= dom f & for x being set st x in dom g holds g.x in f.x
holds s+*g is Element of product f
proof
let I be set, f be non-empty ManySortedSet of I, g be Function,
s be Element of product f;
assume
A1: dom g c= dom f & for x being set st x in dom g holds g.x in f.x;
A2: dom (s+*g) = dom s \/ dom g by FUNCT_4:def 1;
dom s = dom f by CARD_3:18;
then A3: dom (s+*g) = dom f by A1,A2,XBOOLE_1:12;
now
let x be set;
assume
A4: x in dom f;
per cases;
suppose
A5: x in dom g;
then (s+*g).x = g.x by FUNCT_4:14;
hence (s+*g).x in f.x by A1,A5;
suppose
not x in dom g;
then A6: (s+*g).x = s.x by FUNCT_4:12;
ex g' being Function st s = g' & dom g' = dom f
& for x being set st x in dom f holds g'.x in f.x by CARD_3:def 5;
hence (s+*g).x in f.x by A4,A6;
end;
hence s+*g is Element of product f by A3,CARD_3:18;
end;
theorem
for A, B being non empty set,
C being non-empty ManySortedSet of A,
InpFs being ManySortedFunction of A --> B, C,
b being Element of B
ex c being ManySortedSet of A st c = (commute InpFs).b & c in C
proof let A , B be non empty set,
C be non-empty ManySortedSet of A,
InpFs be ManySortedFunction of A --> B, C,
b be Element of B;
A1: commute InpFs = curry' uncurry InpFs by PRALG_2:def 5;
A2: dom InpFs = A by PBOOLE:def 3;
dom(uncurry InpFs) = [:A,B:]
proof
thus dom(uncurry InpFs) c= [:A,B:]
proof let i;
assume i in dom(uncurry InpFs);
then consider x,g,y such that
A3: i = [x,y] and
A4: x in dom InpFs and
A5: g = InpFs.x and
A6: y in dom g by FUNCT_5:def 4;
A7: C.x <> {} by A2,A4,PBOOLE:def 16;
g is Function of (A-->B).x, C.x by A2,A4,A5,MSUALG_1:def 2;
then dom g = (A-->B).x by A7,FUNCT_2:def 1;
then dom g = B by A2,A4,FUNCOP_1:13;
hence i in [:A,B:] by A2,A3,A4,A6,ZFMISC_1:106;
end;
let i;
assume
A8: i in [:A,B:];
then A9: i = [i`1,i`2] by MCART_1:23;
A10: i`1 in dom InpFs by A2,A8,MCART_1:10;
reconsider g = InpFs.i`1 as Function;
A11: C.i`1 <> {} by A2,A10,PBOOLE:def 16;
g is Function of (A-->B).i`1, C.i`1 by A2,A10,MSUALG_1:def 2;
then dom g = (A-->B).i`1 by A11,FUNCT_2:def 1;
then dom g = B by A2,A10,FUNCOP_1:13;
then i`2 in dom g by A8,MCART_1:10;
hence i in dom(uncurry InpFs) by A9,A10,FUNCT_5:45;
end;
then consider g being Function such that
A12: (curry' uncurry InpFs).b = g & dom g = A and
rng g c= rng uncurry InpFs and
A13: for i st i in A holds g.i = (uncurry InpFs).[i,b] by FUNCT_5:39;
reconsider c = (commute InpFs).b as ManySortedSet of A
by A1,A12,PBOOLE:def 3;
take c;
thus c = (commute InpFs).b;
let i;
assume
A14: i in A;
reconsider h = InpFs.i as Function;
A15: C.i <> {} by A14,PBOOLE:def 16;
(A-->B).i = B by A14,FUNCOP_1:13;
then A16: h is Function of B, C.i by A14,MSUALG_1:def 2;
then A17: dom h = B by A15,FUNCT_2:def 1;
c.i = (uncurry InpFs).[i,b] by A1,A12,A13,A14
.= h.b by A2,A14,A17,FUNCT_5:45;
hence c.i in C.i by A15,A16,FUNCT_2:7;
end;
theorem
for I being set, M be ManySortedSet of I,
x, g being Function st x in product M
holds x * g in product (M * g)
proof
let I be set, M be ManySortedSet of I, x, g be Function;
assume
A1: x in product M;
set xg = x * g;
set Mg = M * g;
consider gg being Function such that
A2: x = gg & dom gg = dom M and
A3: for x being set st x in dom M holds gg.x in M.x by A1,CARD_3:def 5;
A4: dom xg = dom Mg by A2,FUNCOP_1:3;
now
let y be set; assume
y in dom Mg;
then A5: y in dom g & g.y in dom M by FUNCT_1:21;
then xg.y = x.(g.y) & Mg.y = M.(g.y) by FUNCT_1:23;
hence xg.y in Mg.y by A2,A3,A5;
end;
hence x * g in product (M * g) by A4,CARD_3:def 5;
end;
theorem
for n being Nat, a being set
holds product ( n |-> {a} ) = { n |-> a }
proof let n be Nat, a be set;
now let i;
hereby assume i in product ( n |-> {a} );
then consider g being Function such that
A1: i = g and
A2: dom g = dom( n |-> {a} ) and
A3: for x st x in dom( n |-> {a} ) holds g.x in ( n |-> {a} ).x
by CARD_3:def 5;
A4: dom g = Seg n by A2,FINSEQ_2:68;
now let x;
assume
A5: x in dom g;
then g.x in ( n |-> {a} ).x & x is Nat by A2,A3;
then g.x in {a} by A4,A5,FINSEQ_2:70;
hence g.x = a by TARSKI:def 1;
end;
then g = dom g --> a by FUNCOP_1:17;
hence i = n |-> a by A1,A4,FINSEQ_2:def 2;
end;
assume
A6: i = n |-> a;
then reconsider g = i as Function;
A7: dom g = Seg n by A6,FINSEQ_2:68 .= dom( n |-> {a} ) by FINSEQ_2:68;
now let x;
assume x in dom( n |-> {a} );
then x in Seg n by FINSEQ_2:68;
then g.x = a & ( n |-> {a} ).x = {a} by A6,FINSEQ_2:70;
hence g.x in ( n |-> {a} ).x by TARSKI:def 1;
end;
hence i in product ( n |-> {a} ) by A7,CARD_3:18;
end;
hence product ( n |-> {a} ) = { n |-> a } by TARSKI:def 1;
end;
begin
::---------------------------------------------------------------------------
:: Trees
::---------------------------------------------------------------------------
reserve T,T1 for finite Tree,
t,p for Element of T,
t1 for Element of T1;
definition
let D be non empty set;
cluster -> finite Element of FinTrees D;
coherence
proof
let t be Element of FinTrees D;
dom t is finite;
hence t is finite by AMI_1:21;
end;
end;
definition
let T be finite DecoratedTree, t be Element of dom T;
cluster T|t -> finite;
coherence
proof
dom(T|t) = (dom T)|t by TREES_2:def 11;
hence thesis by AMI_1:21;
end;
end;
theorem Th13:
T|p,{ t : p is_a_prefix_of t } are_equipotent
proof set X = { t : p is_a_prefix_of t };
deffunc F(Element of T|p) = p^$1;
consider f being Function such that
A1: dom f = T|p and
A2: for n being Element of T|p holds f.n = F(n) from LambdaB;
take f;
thus f is one-to-one
proof let x,y such that
A3: x in dom f and
A4: y in dom f and
A5: f.x = f.y;
reconsider m = x, n = y as Element of T|p by A1,A3,A4;
p^m = f.n by A2,A5 .= p^n by A2;
hence x = y by FINSEQ_1:46;
end;
thus dom f = T|p by A1;
thus rng f c= X
proof let i;
assume i in rng f;
then consider n being set such that
A6: n in dom f and
A7: i = f.n by FUNCT_1:def 5;
reconsider n as Element of T|p by A1,A6;
reconsider t = p^n as Element of T by TREES_1:def 9;
A8: f.n = p^n by A2;
p is_a_prefix_of t by TREES_1:8;
hence i in X by A7,A8;
end;
let i;
assume i in X;
then consider t being Element of T such that
A9: i = t & p is_a_prefix_of t;
consider n being FinSequence such that
A10: i = p^n by A9,TREES_1:8;
n is FinSequence of NAT by A9,A10,FINSEQ_1:50;
then reconsider n as Element of T|p by A9,A10,TREES_1:def 9;
i = f.n by A2,A10;
hence i in rng f by A1,FUNCT_1:def 5;
end;
definition
let T be finite DecoratedTree, t be Element of dom T;
let T1 be finite DecoratedTree;
cluster T with-replacement (t,T1) -> finite;
coherence
proof
dom (T with-replacement (t,T1)) =
dom T with-replacement (t,dom T1) by TREES_2:def 12;
hence thesis by AMI_1:21;
end;
end;
theorem Th14:
T with-replacement (p,T1) =
{ t : not p is_a_prefix_of t } \/ { p^t1 : not contradiction }
proof
defpred P1[set] means $1=$1;
defpred P2[set] means not contradiction;
deffunc F(FinSequence) = p^$1;
set A = { t : not p is_a_proper_prefix_of t },
B = { F(t1) : P1[t1] },
C = { t : not p is_a_prefix_of t },
D = { F(t1) : P2[t1] };
A1: for t1 holds P1[t1] iff P2[t1];
A2: B = D from Fraenkel6'(A1);
now let x;
hereby assume x in A;
then consider t such that
A3: x = t & not p is_a_proper_prefix_of t;
not p is_a_prefix_of t or t = p by A3,XBOOLE_0:def 8;
hence x in C or x in {p} by A3,TARSKI:def 1;
end;
assume x in C or x in {p};
then x = p or ex t st t = x & not p is_a_prefix_of t by TARSKI:def 1;
then consider t such that
A4: t = x and
A5: t = p or not p is_a_prefix_of t;
not p is_a_proper_prefix_of t by A5,XBOOLE_0:def 8;
hence x in A by A4;
end;
then A6: A = C \/ {p} by XBOOLE_0:def 2;
{} is Element of T1 & p^{} = p by FINSEQ_1:47,TREES_1:47;
then A7: p in D;
thus T with-replacement (p,T1) = C \/ {p} \/ D by A2,A6,TREES_1:64
.= C \/ ({p} \/ D) by XBOOLE_1:4
.= C \/ D by A7,ZFMISC_1:46;
end;
theorem Th15:
for f being FinSequence of NAT st f in T with-replacement (p,T1) &
p is_a_prefix_of f ex t1 st f = p^t1
proof let f be FinSequence of NAT such that
A1: f in T with-replacement (p,T1) and
A2: p is_a_prefix_of f;
A3: T with-replacement (p,T1) =
{ t : not p is_a_prefix_of t } \/ { p^t1 : not contradiction } by Th14;
not f in { t : not p is_a_prefix_of t }
proof assume f in { t : not p is_a_prefix_of t };
then ex t st f = t & not p is_a_prefix_of t;
hence contradiction by A2;
end;
then f in { p^t1 : not contradiction } by A1,A3,XBOOLE_0:def 2;
hence thesis;
end;
theorem Th16:
for p being Tree-yielding FinSequence, k being Nat st k+1 in dom p
holds (tree p)|<*k*> = p.(k+1)
proof let p be Tree-yielding FinSequence, k be Nat; assume
k+1 in dom p;
then k+1 <= len p by FINSEQ_3:27;
then k < len p by NAT_1:38;
hence (tree p)|<*k*> = p.(k+1) by TREES_3:52;
end;
theorem
for q being DTree-yielding FinSequence, k being Nat st k+1 in dom q
holds <*k*> in tree doms q
proof
let q be DTree-yielding FinSequence, k be Nat;
assume
A1: k+1 in dom q;
then A2: k+1 <= len q by FINSEQ_3:27;
k < k+1 by REAL_1:69;
then A3: k < len q by A2,AXIOMS:22;
A4: dom doms q = dom q & doms q is Tree-yielding by TREES_3:39;
then (doms q).(k+1) is Tree by A1,TREES_3:24;
then A5: {} in (doms q).(k+1) by TREES_1:47;
dom q = Seg len q & Seg len doms q = dom doms q by FINSEQ_1:def 3;
then A6: k < len doms q by A3,A4,FINSEQ_1:8;
<*k*> = <*k*>^{} by FINSEQ_1:47;
hence <*k*> in tree doms q by A5,A6,TREES_3:def 15;
end;
theorem Th18:
for p,q being Tree-yielding FinSequence, k being Nat
st len p = len q & k+1 in dom p &
for i being Nat st i in dom p & i <> k+1 holds p.i = q.i
for t being Tree st q.(k+1) = t
holds tree(q) = tree(p) with-replacement (<*k*>, t)
proof let p,q be Tree-yielding FinSequence, k be Nat such that
A1: len p = len q and
A2: k+1 in dom p and
A3: for i being Nat st i in dom p & i <> k+1 holds p.i = q.i;
set o = <*k*>;
k+1 <= len p by A2,FINSEQ_3:27;
then A4: k < len p by NAT_1:38;
let t be Tree;
assume
A5: q.(k+1) = t;
p.(k+1) is Tree by A2,TREES_3:24;
then A6: {} in p.(k+1) by TREES_1:47;
o = o^{} by FINSEQ_1:47;
then A7: o in tree(p) by A4,A6,TREES_3:def 15;
now let s be FinSequence of NAT;
hereby assume
A8: s in tree(q);
per cases by A8,TREES_3:def 15;
suppose s = {};
hence s in tree(p) & not o is_a_proper_prefix_of s or
ex r being FinSequence of NAT st r in
t & s = o^r by TREES_1:25,47;
suppose ex n being Nat, r being FinSequence
st n < len q & r in q.(n+1) & s = <*n*>^r;
then consider n being Nat, r being FinSequence such that
A9: n < len q & r in q.(n+1) & s = <*n*>^r;
now per cases;
case
A10: n = k;
reconsider r as FinSequence of NAT by A9,FINSEQ_1:50;
take r;
thus r in t & s = o^r by A5,A9,A10;
case
A11: n <> k;
then A12: n+1 <> k+1 by XCMPLX_1:2;
1 <= n+1 & n+1 <= len p by A1,A9,NAT_1:29,38;
then n+1 in dom p by FINSEQ_3:27;
then q.(n+1) = p.(n+1) by A3,A12;
hence s in tree(p) by A1,A9,TREES_3:def 15;
assume o is_a_proper_prefix_of s;
then o is_a_prefix_of s by XBOOLE_0:def 8;
then consider s1 being FinSequence such that
A13: s = o^s1 by TREES_1:8;
k = s.1 by A13,FINSEQ_1:58 .= n by A9,FINSEQ_1:58;
hence contradiction by A11;
end;
hence s in tree(p) & not o is_a_proper_prefix_of s or
ex r being FinSequence of NAT st r in t & s = o^r;
end;
assume
A14: s in tree(p) & not o is_a_proper_prefix_of s or
ex r being FinSequence of NAT st r in t & s = o^r;
per cases by A14;
suppose that
A15: s in tree(p) and
A16: not o is_a_proper_prefix_of s;
now per cases by A15,TREES_3:def 15;
suppose s = {};
hence s in tree(q) by TREES_1:47;
suppose
ex n being Nat, r being FinSequence
st n < len p & r in p.(n+1) & s = <*n*>^r;
then consider n being Nat, r being FinSequence such that
A17: n < len p & r in p.(n+1) & s = <*n*>^r;
now per cases;
suppose
A18: r = {};
1 <= n+1 & n+1 <= len q by A1,A17,NAT_1:29,38;
then n+1 in dom q by FINSEQ_3:27;
then q.(n+1) is Tree by TREES_3:24;
then r in q.(n+1) by A18,TREES_1:47;
hence s in tree(q) by A1,A17,TREES_3:def 15;
suppose
A19: r <> {};
now assume A20: n = k;
then A21: o is_a_prefix_of s by A17,TREES_1:8;
not s = o by A17,A19,A20,TREES_1:5;
hence contradiction by A16,A21,XBOOLE_0:def 8;
end;
then A22: n+1 <> k+1 by XCMPLX_1:2;
1 <= n+1 & n+1 <= len p by A17,NAT_1:29,38;
then n+1 in dom p by FINSEQ_3:27;
then q.(n+1) = p.(n+1) by A3,A22;
hence s in tree(q) by A1,A17,TREES_3:def 15;
end;
hence s in tree(q);
end;
hence s in tree(q);
suppose ex r being FinSequence of NAT st r in t & s = o^r;
then consider r being FinSequence of NAT such that
A23: r in t & s = o^r;
thus s in tree(q) by A1,A4,A5,A23,TREES_3:def 15;
end;
hence tree(q) = tree(p) with-replacement (o, t) by A7,TREES_1:def 12;
end;
theorem
for e1,e2 being finite DecoratedTree, x being set, k being Nat,
p being DTree-yielding FinSequence st
<*k*> in dom e1 & e1 = x-tree p
ex q being DTree-yielding FinSequence st
e1 with-replacement (<*k*>,e2) = x-tree q &
len q = len p & q.(k+1) = e2 &
for i being Nat st i in dom p & i <> k+1 holds q.i = p.i
proof
let e1,e2 be finite DecoratedTree, x be set, k be Nat,
p be DTree-yielding FinSequence such that
A1: <*k*> in dom e1 and
A2: e1 = x-tree p;
set o = <*k*>;
deffunc F(Nat) = IFEQ($1,k+1,e2,p.$1);
consider q being FinSequence such that
A3: len q = len p and
A4: for i being Nat st i in Seg len p holds q.i = F(i) from SeqLambda;
A5: dom p = Seg len p by FINSEQ_1:def 3;
A6: dom q = dom p by A3,FINSEQ_3:31;
now let x;
assume
A7: x in dom q;
then reconsider i = x as Nat;
A8: q.i = IFEQ(i,k+1,e2,p.i) by A4,A5,A6,A7;
i = k+1 or i <> k+1;
then q.i = e2 or q.i = p.i by A8,CQC_LANG:def 1;
hence q.x is DecoratedTree by A6,A7,TREES_3:26;
end;
then reconsider q as DTree-yielding FinSequence by TREES_3:26;
take q;
<*k*> = {} or
ex i being Nat, T being DecoratedTree, q being Node of T st
i < len p & T = p.(i+1) & <*k*> = <*i*>^q by A1,A2,TREES_4:11;
then consider j being Nat, T being DecoratedTree, w being Node of T
such that
A9: j < len p and T = p.(j+1) and
A10: <*k*> = <*j*>^w by TREES_1:4;
<*j*> <> {} by TREES_1:4;
then <*j*> = <*k*> by A10,TREES_1:6;
then A11: j = <*k*>.1 by FINSEQ_1:def 8 .= k by FINSEQ_1:def 8;
then 1 <= k+1 & k+1 <= len p by A9,NAT_1:29,38;
then A12: k+1 in dom p by FINSEQ_3:27;
then k+1 in Seg len p by FINSEQ_1:def 3;
then A13: q.(k+1) = IFEQ(k+1,k+1,e2,p.(k+1)) by A4
.= e2 by CQC_LANG:def 1;
consider qq being DTree-yielding FinSequence such that
A14: q = qq & dom(x-tree q) = tree doms qq by TREES_4:def 4;
consider pp being DTree-yielding FinSequence such that
A15: p = pp & dom(x-tree p) = tree doms pp by TREES_4:def 4;
reconsider dqq = doms qq as Tree-yielding FinSequence;
A16: len doms pp = len p by A15,TREES_3:40 .= len doms qq
by A3,A14,TREES_3:40;
A17: dom doms pp = dom p by A15,TREES_3:39;
A18: now let i be Nat;
assume
A19: i in dom doms pp & i <> k+1;
then A20: q.i = IFEQ(i,k+1,e2,p.i) by A4,A5,A17
.= p.i by A19,CQC_LANG:def 1;
reconsider pii = p.i as DecoratedTree
by A17,A19,TREES_3:26;
thus (doms pp).i = dom pii by A15,A17,A19,FUNCT_6:31
.= (doms qq).i by A6,A14,A17,A19,A20,FUNCT_6:31;
end;
(doms qq).(k+1) = dom e2 by A6,A12,A13,A14,FUNCT_6:31;
then A21: dom(x-tree q) = dom e1 with-replacement (o, dom e2) by A2,A12,A14,
A15,A16,A17,A18,Th18;
for f being FinSequence of NAT st
f in dom e1 with-replacement (o, dom e2) holds
(not o is_a_prefix_of f & (x-tree q).f = e1.f) or
ex r being FinSequence of NAT st r in dom e2 & f = o^ r &
(x-tree q).f = e2.r
proof let f be FinSequence of NAT;
assume
A22: f in dom e1 with-replacement (o, dom e2);
reconsider o' = o as Element of dom e1 by A1;
per cases by A22,Th15;
suppose
A23: not o' is_a_prefix_of f;
A24: (x-tree q).f = e1.f
proof
per cases by A14,A21,A22,TREES_3:def 15;
suppose
A25: f = {};
hence (x-tree q).f = x by TREES_4:def 4
.= e1.f by A2,A25,TREES_4:def 4;
suppose
ex w being Nat, u being FinSequence
st w < len(dqq) & u in (dqq).(w+1) & f = <*w*>^u;
then consider w be Nat, u being FinSequence such that
A26: w < len(doms q) and
A27: u in (doms q).(w+1) and
A28: f = <*w*>^u by A14;
reconsider u as FinSequence of NAT by A28,FINSEQ_1:50;
reconsider ww = <*w*> as FinSequence of NAT;
w <> k by A23,A28,TREES_1:8;
then A29: w+1 <> k+1 by XCMPLX_1:2;
A30: w < len q by A26,TREES_3:40;
then 1 <= w+1 & w+1 <= len p by A3,NAT_1:29,38;
then A31: w+1 in dom p by FINSEQ_3:27;
A32: (x-tree q)|<*w*> = q.(w+1) by A30,TREES_4:def 4;
A33: w+1 in dom doms p by A31,TREES_3:39;
A34: w+1 in dom doms q by A6,A31,TREES_3:39;
A35: q.(w+1) = IFEQ(w+1,k+1,e2,p.(w+1)) by A4,A5,A31
.= p.(w+1) by A29,CQC_LANG:def 1;
reconsider pw1 = p.(w+1) as DecoratedTree
by A31,TREES_3:26;
A36: (dom(x-tree q))|<*w*> = (doms q).(w+1) by A14,A34,Th16;
consider pp being DTree-yielding FinSequence such that
A37: p = pp & dom(x-tree p) = tree doms pp by TREES_4:def 4;
A38: (dom(x-tree p))|<*w*> = (doms p).(w+1) by A33,A37,Th16
.= dom pw1 by A31,FUNCT_6:31
.= (doms q).(w+1) by A6,A31,A35,FUNCT_6:31;
thus (x-tree q).f = ((x-tree q)|ww).u by A27,A28,A36,TREES_2:def 11
.= ((x-tree p)|ww).u by A3,A30,A32,A35,TREES_4:def 4
.= e1.f by A2,A27,A28,A38,TREES_2:def 11;
end;
assume
o is_a_prefix_of f or (x-tree q).f <> e1.f;
hence thesis by A23,A24;
suppose ex t1 being Element of dom e2 st f=o'^t1;
then consider r being Element of dom e2 such that
A39: f = o^r;
reconsider r as FinSequence of NAT;
assume o is_a_prefix_of f or (x-tree q).f <> e1.f;
take r;
thus
A40: r in dom e2;
A41: (x-tree q)|o = q.(k+1) by A3,A9,A11,TREES_4:def 4;
A42: r in (dom(x-tree q))|o by A1,A21,A40,TREES_1:66;
thus f = o^r by A39;
thus (x-tree q).f = e2.r by A13,A39,A41,A42,TREES_2:def 11;
end;
hence e1 with-replacement (o,e2) = x-tree q by A1,A21,TREES_2:def 12;
thus len q = len p by A3;
thus q.(k+1) = e2 by A13;
let i be Nat;
assume i in dom p;
then q.i = IFEQ(i,k+1,e2,p.i) by A4,A5;
hence thesis by CQC_LANG:def 1;
end;
theorem
for T being finite Tree, p being Element of T st p <> {}
holds card (T|p) < card T
proof let T be finite Tree, p be Element of T;
assume
A1: p <> {};
reconsider p' = p as Element of NAT* by FINSEQ_1:def 11;
set X = { p'^n where n is Element of NAT*: n in T|p };
A2: T|p,X are_equipotent
proof
deffunc F(Element of T|p) = p'^$1;
consider f being Function such that
A3: dom f = T|p and
A4: for n being Element of T|p holds f.n = F(n) from LambdaB;
take f;
thus f is one-to-one
proof let x,y such that
A5: x in dom f and
A6: y in dom f and
A7: f.x = f.y;
reconsider m = x, n = y as Element of T|p by A3,A5,A6;
p'^m = f.n by A4,A7 .= p'^n by A4;
hence x = y by FINSEQ_1:46;
end;
thus dom f = T|p by A3;
thus rng f c= X
proof let i;
assume i in rng f;
then consider n being set such that
A8: n in dom f and
A9: i = f.n by FUNCT_1:def 5;
T|p c= NAT* by TREES_1:def 5;
then reconsider n as Element of NAT* by A3,A8;
f.n = p'^n by A3,A4,A8;
hence i in X by A3,A8,A9;
end;
let i;
assume i in X;
then consider n being Element of NAT* such that
A10: i = p'^n and
A11: n in T|p;
reconsider n as Element of T|p by A11;
i = f.n by A4,A10;
hence i in rng f by A3,FUNCT_1:def 5;
end;
then reconsider X as finite set by CARD_1:68;
A12: X c= T
proof let i;
assume i in X;
then consider n being Element of NAT* such that
A13: i = p'^n & n in T|p;
thus i in T by A13,TREES_1:def 9;
end;
X <> T
proof assume X = T;
then {} in X by TREES_1:47;
then ex n being Element of NAT* st {} = p'^n & n in T|p;
hence contradiction by A1,FINSEQ_1:48;
end;
then A14: X c< T by A12,XBOOLE_0:def 8;
card X = card(T|p) by A2,CARD_1:81;
hence card (T|p) < card T by A14,CARD_2:67;
end;
theorem Th21:
for f being Function holds Card (f qua set) = Card dom f
proof let f be Function;
dom f,f are_equipotent
proof
deffunc F(set) = [$1,f.$1];
consider g being Function such that
A1: dom g = dom f and
A2: for x st x in dom f holds g.x = F(x) from Lambda;
take g;
thus g is one-to-one
proof let x,y;
assume
A3: x in dom g & y in dom g;
assume g.x = g.y;
then [x,f.x] = g.y by A1,A2,A3 .= [y,f.y] by A1,A2,A3;
hence x = y by ZFMISC_1:33;
end;
thus dom g = dom f by A1;
thus rng g c= f
proof let i;
assume i in rng g;
then consider x such that
A4: x in dom g and
A5: g.x = i by FUNCT_1:def 5;
g.x = [x,f.x] by A1,A2,A4;
hence i in f by A1,A4,A5,FUNCT_1:8;
end;
let i;
assume
A6: i in f;
then consider x,y such that
A7: i = [x,y] by RELAT_1:def 1;
A8: x in dom f & y = f.x by A6,A7,FUNCT_1:8;
then g.x = i by A2,A7;
hence i in rng g by A1,A8,FUNCT_1:def 5;
end;
hence Card (f qua set) = Card dom f by CARD_1:21;
end;
theorem Th22:
for T, T1 being finite Tree, p being Element of T
holds card(T with-replacement (p,T1)) + card (T|p) = card T + card T1
proof
let T, T1, p;
defpred P1[Element of T] means not p is_a_prefix_of $1;
defpred P2[Element of T] means p is_a_prefix_of $1;
set A = { t : P1[t] };
set B = { t : P2[t] };
set C = { p^t1 : not contradiction };
A1: A is Subset of T from SubsetD;
A2: B is Subset of T from SubsetD;
then reconsider A,B as finite set by A1;
A3: T with-replacement (p,T1) = A \/ C by Th14;
A4: A misses C
proof assume not thesis;
then consider x such that
A5: x in A /\ C by XBOOLE_0:4;
x in A by A5,XBOOLE_0:def 3;
then consider t such that
A6: x = t & not p is_a_prefix_of t;
x in C by A5,XBOOLE_0:def 3;
then ex t1 st x = p^t1;
hence contradiction by A6,TREES_1:8;
end;
now let x;
hereby assume x in T;
then reconsider t = x as Element of T;
p is_a_prefix_of t or not p is_a_prefix_of t;
hence x in A or x in B;
end;
assume x in A or x in B;
hence x in T by A1,A2;
end;
then A7: T = A \/ B by XBOOLE_0:def 2;
A8: A misses B
proof assume not thesis;
then consider x such that
A9: x in A /\ B by XBOOLE_0:4;
x in A & x in B by A9,XBOOLE_0:def 3;
then (ex t st x = t & not p is_a_prefix_of t)
& (ex t st x = t & p is_a_prefix_of t);
hence contradiction;
end;
A10: T1,C are_equipotent
proof
deffunc F(Element of T1) = p^$1;
consider f being Function such that
A11: dom f = T1 and
A12: for n being Element of T1 holds f.n = F(n) from LambdaB;
take f;
thus f is one-to-one
proof let x,y such that
A13: x in dom f and
A14: y in dom f and
A15: f.x = f.y;
reconsider m = x, n = y as Element of T1 by A11,A13,A14;
p^m = f.n by A12,A15 .= p^n by A12;
hence x = y by FINSEQ_1:46;
end;
thus dom f = T1 by A11;
thus rng f c= C
proof let i;
assume i in rng f;
then consider n being set such that
A16: n in dom f and
A17: i = f.n by FUNCT_1:def 5;
T1 c= NAT* by TREES_1:def 5;
then reconsider n as Element of NAT* by A11,A16;
f.n = p^n by A11,A12,A16;
hence i in C by A11,A16,A17;
end;
let i;
assume i in C;
then consider n being Element of T1 such that
A18: i = p^n;
i = f.n by A12,A18;
hence i in rng f by A11,FUNCT_1:def 5;
end;
then reconsider C as finite set by CARD_1:68;
A19: card T1 = card C by A10,CARD_1:81;
T|p,B are_equipotent by Th13;
then card(T|p) = card B by CARD_1:81;
hence card(T with-replacement (p,T1)) + card (T|p) =
card A + card C + card B by A3,A4,CARD_2:53
.= card A + card B + card C by XCMPLX_1:1
.= card T + card T1 by A7,A8,A19,CARD_2:53;
end;
theorem
for T, T1 being finite DecoratedTree,
p being Element of dom T
holds card(T with-replacement (p,T1)) + card (T|p) = card T + card T1
proof
let T, T1 be finite DecoratedTree, p be Element of dom T;
A1: dom (T with-replacement(p, T1)) =
dom T with-replacement (p, dom T1) & dom (T|p) = (dom T)|p
by TREES_2:def 11,def 12;
A2: card dom T = card T & card dom T1 = card T1 by Th21;
card dom (T with-replacement(p,T1)) = card(T with-replacement (p,T1)) &
card dom (T|p) = card (T|p) by Th21;
hence card(T with-replacement (p,T1)) + card (T|p)
= card T + card T1 by A1,A2,Th22;
end;
definition let x be set;
cluster root-tree x -> finite;
coherence
proof
root-tree x = {[{},x]} by TREES_4:6;
hence thesis;
end;
end;
theorem
for x being set
holds card root-tree x = 1
proof
let x be set;
root-tree x = {[{},x]} by TREES_4:6;
hence card root-tree x = 1 by CARD_1:79;
end;