:: Introduction to Trees
:: by Grzegorz Bancerek
::
:: Received October 25, 1989
:: Copyright (c) 1990-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, XBOOLE_0, SUBSET_1, FUNCT_1, FINSEQ_1, TARSKI, RELAT_1,
NAT_1, ORDINAL4, ARYTM_3, FINSET_1, CARD_1, XXREAL_0, ORDINAL1, TREES_1,
AMISTD_3, FINSEQ_2;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, XCMPLX_0, ORDINAL1,
NAT_1, NUMBERS, RELAT_1, FUNCT_1, FINSEQ_1, FINSEQ_2, FUNCT_2, FINSET_1,
XXREAL_0;
constructors ENUMSET1, WELLORD2, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, FINSEQ_2,
FUNCOP_1, FUNCT_2, RELSET_1, NUMBERS;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XXREAL_0,
XREAL_0, NAT_1, FINSEQ_1, CARD_1, RELSET_1, FINSEQ_2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, FINSET_1, FUNCT_1, WELLORD2, XBOOLE_0;
equalities ORDINAL1;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, NAT_1, FINSEQ_1, FINSET_1, FUNCT_1, CARD_1, RELAT_1,
GRFUNC_1, CARD_2, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1,
ENUMSET1, FINSEQ_2, FINSEQ_3, FUNCT_2;
schemes NAT_1, CLASSES1, XBOOLE_0, FUNCT_2;
begin
reserve:: D for non empty set,
X,x,y,z for set,
k,n,m for Nat ,
f for Function,
p,q,r for FinSequence of NAT;
::
:: Relations "is a prefix of", "is a proper prefix of" and
:: "are comparable" of finite sequences
::
notation
let p,q be FinSequence;
synonym p is_a_prefix_of↑ q for p c= q;
end;
definition
let p,q be FinSequence;
redefine pred p is_a_prefix_of q means :: redefines is_a_prefix_of (TREES_1, synonym) → c= (RELAT_1, redefinition) → c= (TARSKI, definition)
ex n st p = q|Seg n;
compatibility
proof
thus p c= q implies ex n st p = q|Seg n
proof
assume
A1: p c= q;
consider n be Nat such that
A2: dom p = Seg n by FINSEQ_1:def 2;
reconsider n as Nat;
take n;
thus thesis by A1,A2,GRFUNC_1:23;
end;
thus thesis by RELAT_1:59;
end;
end;
theorem Th1:
for p,q being FinSequence holds p is_a_prefix_of q iff
ex r being FinSequence st q = p^r
proof
let p,q be FinSequence;
thus p is_a_prefix_of q implies ex r being FinSequence st q = p^r
by FINSEQ_1:80;
given r being FinSequence such that
A1: q = p^r;
dom p = Seg len p & p = q|dom p by A1,FINSEQ_1:21,def 3;
hence thesis;
end;
::$CT
theorem Th2:
<*x*> is_a_prefix_of <*y*> implies x = y
proof
assume
A1: <*x*> is_a_prefix_of <*y*>;
len <*x*> = 1 & len <*y*> = 1 by FINSEQ_1:40;
then A2: <*x*> = <*y*> by A1,CARD_2:102;
<*x*>.1 = x;
hence thesis by A2,FINSEQ_1:40;
end;
notation
let p,q be FinSequence;
synonym p is_a_proper_prefix_of q for p c< q;
end;
theorem Th3:
for p,q being finite set st p,q are_c=-comparable & card p = card q holds
p = q
by CARD_2:102;
reserve p1,p2,p3 for FinSequence;
theorem Th4:
<*x*>,<*y*> are_c=-comparable implies x = y
proof
assume
A1: <*x*>,<*y*> are_c=-comparable;
len <*x*> = 1 & len <*y*> = 1 by FINSEQ_1:40;
then A2: <*x*> = <*y*> by A1,Th3;
<*x*>.1 = x;
hence thesis by A2,FINSEQ_1:40;
end;
theorem Th5:
for p,q being finite set st p c< q holds card p < card q
proof
let p,q be finite set;
assume that
A1: p c= q and
A2: p <> q;
A3: card p <= card q by A1,NAT_1:43;
p,q are_c=-comparable by A1;
hence thesis by A3,A2,Th3,XXREAL_0:1;
end;
theorem Th6:
p1^<*x*> is_a_prefix_of p2 implies p1 is_a_proper_prefix_of p2
proof
assume p1^<*x*> is_a_prefix_of p2;
then consider p3 such that
A1: p2 = p1^<*x*>^p3 by Th1;
p2 = p1^(<*x*>^p3) by A1,FINSEQ_1:32;
hence p1 is_a_prefix_of p2 by Th1;
assume p1 = p2;
then len p1 = len(p1^<*x*>) + len p3 by A1,FINSEQ_1:22
.= len p1 + len <*x*> + len p3 by FINSEQ_1:22
.= len p1 + 1 + len p3 by FINSEQ_1:39;
then len p1 + 1 <= len p1 by NAT_1:11;
hence contradiction by NAT_1:13;
end;
theorem Th7:
p1 is_a_prefix_of p2 implies p1 is_a_proper_prefix_of p2^<*x*>
proof
assume p1 is_a_prefix_of p2;
then consider p3 such that
A1: p2 = p1^p3 by Th1;
p2^<*x*> = p1^(p3^<*x*>) by A1,FINSEQ_1:32;
hence p1 is_a_prefix_of p2^<*x*> by Th1;
assume p1 = p2^<*x*>;
then len p2 = len(p2^<*x*>) + len p3 by A1,FINSEQ_1:22
.= len p2 + len <*x*> + len p3 by FINSEQ_1:22
.= len p2 + 1 + len p3 by FINSEQ_1:39;
then len p2 + 1 <= len p2 by NAT_1:11;
hence contradiction by NAT_1:13;
end;
theorem Th8:
p1 is_a_proper_prefix_of p2^<*x*> implies p1 is_a_prefix_of p2
proof
assume that
A1: p1 is_a_prefix_of p2^<*x*> and
A2: p1 <> p2^<*x*>;
A3: ex p3 st p2^<*x*> = p1^p3 by A1,Th1;
A4: len p1 <= len(p2^<*x*>) by A1,NAT_1:43;
len(p2^<*x*>) = len p2 + len <*x*> & len <*x*> = 1 by FINSEQ_1:22,39;
then len p1 < len p2 + 1 by A1,A2,A4,CARD_2:102,XXREAL_0:1;
then len p1 <= len p2 by NAT_1:13;
then ex p3 st p1^p3 = p2 by A3,FINSEQ_1:47;
hence thesis by Th1;
end;
theorem
{} is_a_proper_prefix_of p2 or {} <> p2 implies
p1 is_a_proper_prefix_of p1^p2
proof
assume
A1: {} is_a_proper_prefix_of p2 or {} <> p2;
thus p1 is_a_prefix_of p1^p2 by Th1;
assume p1 = p1^p2;
then len p1 = len p1 + len p2 by FINSEQ_1:22;
then p2 = {};
hence contradiction by A1;
end;
::
:: The set of proper prefixes of a finite sequence
::
definition
let p be FinSequence;
func ProperPrefixes p -> set means
:Def2:
for x being object holds
x in it iff ex q being FinSequence st x = q & q is_a_proper_prefix_of p;
existence
proof
set E = rng p;
defpred X[object] means ex q being FinSequence st $1 = q &
q is_a_proper_prefix_of p;
consider X such that
A1: for x being object holds x in X iff x in E* & X[x] from XBOOLE_0:sch 1;
take X;
let x be object;
thus x in X implies ex q being FinSequence st x = q &
q is_a_proper_prefix_of p by A1;
given q be FinSequence such that
A2: x = q and
A3: q is_a_proper_prefix_of p;
q is_a_prefix_of p by A3;
then ex n st q = p|Seg n;
then rng q c= E by RELAT_1:70;
then reconsider q as FinSequence of E by FINSEQ_1:def 4;
q in E* by FINSEQ_1:def 11;
hence thesis by A1,A2,A3;
end;
uniqueness
proof
let S1,S2 be set such that
A4: for x being object holds
x in
S1 iff ex q being FinSequence st x = q & q is_a_proper_prefix_of p and
A5: for x being object holds
x in S2 iff ex q being FinSequence st x = q & q is_a_proper_prefix_of p;
defpred X[object] means
ex q being FinSequence st $1 = q & q is_a_proper_prefix_of p;
A6: for x being object holds x in S1 iff X[x] by A4;
A7: for x being object holds x in S2 iff X[x] by A5;
thus thesis from XBOOLE_0:sch 2(A6,A7);
end;
end;
theorem Th10:
for p being FinSequence st x in ProperPrefixes p holds x is FinSequence
proof
let p be FinSequence;
assume x in ProperPrefixes p;
then
ex q being FinSequence st x = q & q is_a_proper_prefix_of p by Def2;
hence thesis;
end;
theorem Th11:
for p,q being FinSequence holds
p in ProperPrefixes q iff p is_a_proper_prefix_of q
proof
let p,q be FinSequence;
thus p in ProperPrefixes q implies p is_a_proper_prefix_of q
proof
assume p in ProperPrefixes q;
then
ex r being FinSequence st p = r & r is_a_proper_prefix_of q by Def2;
hence thesis;
end;
thus thesis by Def2;
end;
theorem Th12:
for p,q being FinSequence st p in ProperPrefixes q holds len p < len q
by Th11,Th5;
theorem
for p,q,r being FinSequence st q^r in ProperPrefixes p holds
q in ProperPrefixes p
proof
let p,q,r be FinSequence;
assume
A1: q^r in ProperPrefixes p;
A2: q is_a_prefix_of q^r by Th1;
q^r is_a_proper_prefix_of p by A1,Th11;
then q is_a_proper_prefix_of p by A2,XBOOLE_1:59;
hence thesis by Th11;
end;
theorem Th14:
ProperPrefixes {} = {} proof set x = the Element of ProperPrefixes {};
assume
A1: not thesis;
then reconsider x as FinSequence by Th10;
x is_a_proper_prefix_of {} by A1,Th11;
hence contradiction by XBOOLE_1:62;
end;
set D = { {} };
theorem Th15:
ProperPrefixes <*x*> = { {} }
proof
thus ProperPrefixes <*x*> c= D
proof
let y be object;
assume y in ProperPrefixes <*x*>;
then consider p being FinSequence such that
A1: y = p and
A2: p is_a_proper_prefix_of <*x*> by Def2;
A3: len p < len <*x*> by A2,Th5;
len <*x*> = 1 & 1 = 0+1 by FINSEQ_1:39;
then p = {} by A3,NAT_1:13;
hence thesis by A1,TARSKI:def 1;
end;
let y be object;
assume y in D;
then A4: y = {} by TARSKI:def 1;
{} is_a_prefix_of <*x*>;
then {} is_a_proper_prefix_of <*x*>;
hence thesis by A4,Def2;
end;
theorem
for p,q being FinSequence st p is_a_prefix_of q holds
ProperPrefixes p c= ProperPrefixes q
proof
let p,q be FinSequence such that
A1: p is_a_prefix_of q;
let x be object;
assume
A2: x in ProperPrefixes p;
then reconsider r = x as FinSequence by Th10;
r is_a_proper_prefix_of p by A2,Th11;
then r is_a_proper_prefix_of q by A1,XBOOLE_1:58;
hence thesis by Th11;
end;
theorem Th17:
for p,q,r being FinSequence st
q in ProperPrefixes p & r in ProperPrefixes p holds q,r are_c=-comparable
proof
let p,q,r be FinSequence;
assume q in ProperPrefixes p;
then
A1: ex q1 being FinSequence st q = q1 & q1 is_a_proper_prefix_of p by Def2;
assume r in ProperPrefixes p;
then
A2: ex r1 being FinSequence st r = r1 & r1 is_a_proper_prefix_of p by Def2;
q is_a_prefix_of p by A1;
then consider n such that
A3: q = p|Seg n;
r is_a_prefix_of p by A2;
then consider k such that
A4: r = p|Seg k;
A5: n <= k implies thesis
proof
assume n <= k;
then Seg n c= Seg k by FINSEQ_1:5;
then q = r|Seg n by A3,A4,FUNCT_1:51;
then q is_a_prefix_of r;
hence thesis;
end;
k <= n implies thesis
proof
assume k <= n;
then Seg k c= Seg n by FINSEQ_1:5;
then r = q|Seg k by A3,A4,FUNCT_1:51;
then r is_a_prefix_of q;
hence thesis;
end;
hence thesis by A5;
end;
::
:: Trees and their properties
::
definition
let X;
attr X is Tree-like means
:Def3:
X c= NAT* & (for p st p in X holds ProperPrefixes p c= X) &
for p,k,n st p^<*k*> in X & n <= k holds p^<*n*> in X;
end;
registration
cluster { {} } -> Tree-like;
coherence
proof
thus D c= NAT*
proof
let x be object;
assume x in D;
then x = {} by TARSKI:def 1;
hence thesis by FINSEQ_1:49;
end;
thus for p st p in D holds ProperPrefixes p c= D
by TARSKI:def 1,Th14;
thus thesis by TARSKI:def 1;
end;
end;
registration
cluster non empty Tree-like for set;
existence
proof
take D = { <*>(NAT) };
thus thesis;
end;
end;
definition
mode Tree is Tree-like non empty set;
end;
reserve T,T1 for Tree;
theorem Th18:
x in T implies x is FinSequence of NAT
proof
T c= NAT* by Def3;
hence thesis by FINSEQ_1:def 11;
end;
definition
let T;
redefine mode Element of T -> FinSequence of NAT; :: redefines Element (SUBSET_1, definition)
coherence by Th18;
end;
theorem Th19:
for p,q being FinSequence st p in T & q is_a_prefix_of p holds q in T
proof
let p,q be FinSequence;
assume that
A1: p in T and
A2: q is_a_prefix_of p;
reconsider r = p as Element of T by A1;
A3: ProperPrefixes r c= T by Def3;
q is_a_proper_prefix_of p or q = p by A2;
then q in ProperPrefixes p or p = q by Th11;
hence thesis by A3;
end;
theorem Th20:
for r being FinSequence st q^r in T holds q in T
proof
let r be FinSequence;
assume
A1: q^r in T;
then reconsider p = q^r as FinSequence of NAT by Th18;
reconsider s = p|Seg len q as FinSequence of NAT by FINSEQ_1:18;
len p = len q + len r by FINSEQ_1:22;
then len q <= len p by NAT_1:11;
then A2: len s = len q by FINSEQ_1:17;
now
let n be Nat;
assume 1 <= n & n <= len q;
then A3: n in Seg len q by FINSEQ_1:1;
Seg len q = dom q by FINSEQ_1:def 3;
then p.n = q.n by A3,FINSEQ_1:def 7;
hence q.n = s.n by A3,FUNCT_1:49;
end;
then q = s by A2,FINSEQ_1:14;
then A4: q is_a_prefix_of p;
now
assume q <> p;
then q is_a_proper_prefix_of p by A4;
then A5: q in ProperPrefixes p by Def2;
ProperPrefixes p c= T by A1,Def3;
hence thesis by A5;
end;
hence thesis by A1;
end;
theorem Th21:
{} in T & <*> NAT in T
proof
reconsider x = the Element of T as FinSequence of NAT;
x in T;
then
A1: {}^x in T by FINSEQ_1:34;
{} = <*> NAT;
hence thesis by A1,Th20;
end;
theorem
{ {} } is Tree;
registration
let T,T1;
cluster T \/ T1 -> Tree-like;
coherence
proof
set D = T \/ T1;
T c= NAT* & T1 c= NAT* by Def3;
hence D c= NAT* by XBOOLE_1:8;
thus for p st p in D holds ProperPrefixes p c= D
proof
let p;
assume p in D;
then p in T or p in T1 by XBOOLE_0:def 3;
then
A1: ProperPrefixes p c= T or ProperPrefixes p c= T1 by Def3;
T c= D & T1 c= D by XBOOLE_1:7;
hence thesis by A1;
end;
let p,k,n;
assume that
A2: p^<*k*> in D and
A3: n <= k;
p^<*k*> in T or p^<*k*> in T1 by A2,XBOOLE_0:def 3;
then p^<*n*> in T or p^<*n*> in T1 by A3,Def3;
hence thesis by XBOOLE_0:def 3;
end;
cluster T /\ T1 -> Tree-like non empty;
coherence
proof
set D = T /\ T1;
thus D is Tree-like
proof
T c= NAT* & T /\ T1 c= T by Def3,XBOOLE_1:17;
hence D c= NAT*;
thus for p st p in D holds ProperPrefixes p c= D
proof
let p;
assume
A4: p in D;
then
A5: p in T by XBOOLE_0:def 4;
A6: p in T1 by A4,XBOOLE_0:def 4;
A7: ProperPrefixes p c= T by A5,Def3;
ProperPrefixes p c= T1 by A6,Def3;
hence thesis by A7,XBOOLE_1:19;
end;
let p,k,n;
assume that
A8: p^<*k*> in D and
A9: n <= k;
A10: p^<*k*> in T by A8,XBOOLE_0:def 4;
A11: p^<*k*> in T1 by A8,XBOOLE_0:def 4;
A12: p^<*n*> in T by A9,A10,Def3;
p^<*n*> in T1 by A9,A11,Def3;
hence thesis by A12,XBOOLE_0:def 4;
end;
{} in T & {} in T1 by Th21;
hence thesis by XBOOLE_0:def 4;
end;
end;
theorem
T \/ T1 is Tree;
theorem
T /\ T1 is Tree;
::
:: Finite trees and their properties
::
registration
cluster finite for Tree;
existence
proof
take D;
thus thesis;
end;
end;
reserve fT,fT1 for finite Tree;
theorem
fT \/ fT1 is finite Tree;
theorem
fT /\ T is finite Tree;
::
:: Elementary trees
::
definition
let n;
func elementary_tree n -> Tree equals
{ <*k*> : k < n } \/ { {} };
correctness
proof
set IT = { <*k*> : k < n } \/ D;
IT is Tree-like
proof
thus IT c= NAT*
proof
let x be object;
assume x in IT;
then
A1: x in { <*k*> : k < n } or x in D by XBOOLE_0:def 3;
A2: {} in NAT* by FINSEQ_1:49;
now
assume x in { <*k*> : k < n };
then consider k such that
A3: x = <*k*> & k < n;
reconsider k as Element of NAT by ORDINAL1:def 12;
x = <*k*> by A3;
hence thesis by FINSEQ_1:def 11;
end;
hence thesis by A1,A2,TARSKI:def 1;
end;
thus for p st p in IT holds ProperPrefixes p c= IT
proof
let p;
assume p in IT;
then
A4: p in { <*k*> : k < n } or p in D by XBOOLE_0:def 3;
now
assume p in { <*k*> : k < n };
then ex k st p = <*k*> & k < n;
then ProperPrefixes p = D by Th15;
hence thesis by XBOOLE_1:7;
end;
hence thesis by A4,Th14,TARSKI:def 1;
end;
let p,k,m;
assume p^<*k*> in IT;
then p^<*k*> in
{ <*j*> where j is Nat : j < n } or p^<*k*> in D
by XBOOLE_0:def 3;
then consider l being Nat such that
A5: p^<*k*> = <*l*> and
A6: l < n by TARSKI:def 1;
len p + len <*k*> = len <*l*> by A5,FINSEQ_1:22
.= 1 by FINSEQ_1:39;
then len p + 1 = 0 + 1 by FINSEQ_1:39;
then A7: p = {};
then A8: <*k*> = <*l*> by A5,FINSEQ_1:34;
<*k*>.1 = k;
then A9: k = l by A8,FINSEQ_1:def 8;
assume
A10: m <= k;
A11: p^<*m*> = <*m*> by A7,FINSEQ_1:34;
m < n by A6,A9,A10,XXREAL_0:2;
then p^<*m*> in { <*j*> where j is Nat : j < n } by A11;
hence thesis by XBOOLE_0:def 3;
end;
hence thesis;
end;
end;
registration
let n;
cluster elementary_tree n -> finite;
coherence
proof
set IT = elementary_tree n;
IT,Seg(n+1) are_equipotent
proof
defpred F[object,object] means
$1 = {} & $2 = 1 or ex n st $1 = <*n*> & $2 = n+2;
A1: x in IT & F[x,y] & F[x,z] implies y = z
proof
assume that x in IT and
A2: (x = {} & y = 1 or ex n st x = <*n*> & y = n+2)&( x = {} & z = 1 or
ex n st x = <*n*> & z = n+2);
now
given n1 being Nat such that
A3: x = <*n1*> & y = n1+2;
given n2 being Nat such that
A4: x = <*n2*> & z = n2+2;
<*n1*>.1 = n1;
hence thesis by A3,A4,FINSEQ_1:def 8;
end;
hence thesis by A2;
end;
A5: for x being object st x in IT ex y being object st F[x,y]
proof let x be object;
assume
A6: x in IT;
A7: now
assume x in { <*k*> : k < n };
then consider k such that
A8: x = <*k*> and k < n;
reconsider y = k+2 as set;
take y;
thus F[x,y] by A8;
end;
now
assume
A9: x in D;
reconsider y = 1 as set;
take y;
thus F[x,y] by A9,TARSKI:def 1;
end;
hence thesis by A6,A7,XBOOLE_0:def 3;
end;
consider f such that
A10: dom f = IT &
for x being object st x in IT holds F[x,f.x] from CLASSES1:sch 1(A5);
take f;
thus f is one-to-one
proof
let x,y be object;
assume that
A11: x in dom f and
A12: y in dom f and
A13: f.x = f.y;
A14: x = {} & f.x = 1 or ex n st x = <*n*> & f.x = n+2 by A10,A11;
A15: y = {} & f.y = 1 or ex n st y = <*n*> & f.y = n+2 by A10,A12;
A16: now
assume that
x = {} and
A17: f.x = 1;
given n such that
y = <*n*> and
A18: f.y = n+2;
0+1 = n+1+1 by A13,A17,A18;
hence contradiction;
end;
now
assume that
y = {} and
A19: f.y = 1;
given n such that
x = <*n*> and
A20: f.x = n+2;
0+1 = n+1+1 by A13,A19,A20;
hence contradiction;
end;
hence thesis by A13,A14,A15,A16;
end;
thus dom f = IT by A10;
thus rng f c= Seg(n+1)
proof
let x be object;
assume x in rng f;
then consider y being object such that
A21: y in dom f and
A22: x = f.y by FUNCT_1:def 3;
1 <= 1+n by NAT_1:11;
then A23: 1 in Seg(n+1) by FINSEQ_1:1;
now
given k such that
A24: y = <*k*> and
A25: x = k+2;
y in { <*j*> where j is Nat : j < n } or y in D
by A10,A21,XBOOLE_0:def 3;
then consider l being Nat such that
A26: y = <*l*> & l < n by A24,TARSKI:def 1;
<*k*>.1 = k & <*l*>.1 = l;
then k+1 <= n by A24,A26,NAT_1:13;
then 1+0 <= k+1+1 & k+1+1 <= n+1 by XREAL_1:7;
hence thesis by A25,FINSEQ_1:1;
end;
hence thesis by A10,A21,A22,A23;
end;
let x be object;
assume
A27: x in Seg(n+1);
then reconsider k = x as Nat;
A28: 1 <= k by A27,FINSEQ_1:1;
A29: k <= n+1 by A27,FINSEQ_1:1;
{} in D by TARSKI:def 1;
then A30: {} in IT by XBOOLE_0:def 3;
then F[{},f.{}] by A10;
then A31: 1 in rng f by A10,A30,FUNCT_1:def 3;
now
assume 1 < k;
then 1+1 <= k by NAT_1:13;
then consider m be Nat such that
A32: k = 2+m by NAT_1:10;
reconsider m as Nat;
1+1+m = 1+(1+m);
then 1+m <= n by A29,A32,XREAL_1:6;
then m < n by NAT_1:13;
then <*m*> in { <*j*> where j is Nat : j < n };
then A33: <*m*> in IT by XBOOLE_0:def 3;
then F[<*m*>,f.<*m*>] by A10;
then k = f.<*m*> by A1,A32,A33;
hence k in rng f by A10,A33,FUNCT_1:def 3;
end;
hence thesis by A28,A31,XXREAL_0:1;
end;
hence thesis by CARD_1:38;
end;
end;
theorem Th27:
k < n implies <*k*> in elementary_tree n
proof
assume k < n;
then <*k*> in { <*j*> where j is Nat : j < n };
hence thesis by XBOOLE_0:def 3;
end;
theorem Th28:
elementary_tree 0 = { {} }
proof
now
set x = the Element of { <*j*> where j is Nat : j < 0 };
assume { <*j*> where j is Nat : j < 0 } <> {};
then x in { <*j*> where j is Nat : j < 0 };
then ex k st x = <*k*> & k < 0;
hence contradiction;
end;
hence thesis;
end;
theorem
p in elementary_tree n implies p = {} or ex k st k < n & p = <*k*>
proof
assume p in elementary_tree n;
then A1: p in D or p in { <*k*> : k < n } by XBOOLE_0:def 3;
p in { <*k*> : k < n } implies ex k st p = <*k*> & k < n;
hence thesis by A1,TARSKI:def 1;
end;
::
:: Leaves and subtrees
::
definition
let T;
func Leaves T -> Subset of T means
:Def5:
p in it iff p in T & not ex q st q in T & p is_a_proper_prefix_of q;
existence
proof
defpred X[object] means
for p st $1 = p for q st q in T holds not p is_a_proper_prefix_of q;
consider X such that
A1: for x being object holds x in X iff x in T & X[x] from XBOOLE_0:sch 1;
X c= T
by A1;
then reconsider X as Subset of T;
take X;
let p;
thus
p in X implies p in T & not ex q st q in T & p is_a_proper_prefix_of
q by A1;
assume that
A2: p in T and
A3: not ex q st q in T & p is_a_proper_prefix_of q;
for r being FinSequence of NAT st p = r
for q st q in T holds not r is_a_proper_prefix_of q by A3;
hence p in X by A1,A2;
end;
uniqueness
proof
let L1,L2 be Subset of T such that
A4: p in L1 iff p in T & not ex q st q in T & p is_a_proper_prefix_of q and
A5: p in L2 iff p in T & not ex q st q in T & p is_a_proper_prefix_of q;
A6: T c= NAT* by Def3;
then A7: L1 c= NAT*;
A8: L2 c= NAT* by A6;
now
let x be object;
thus x in L1 implies x in L2
proof
assume
A9: x in L1;
then reconsider p = x as FinSequence of NAT by A7,FINSEQ_1:def 11;
not ex q st q in T & p is_a_proper_prefix_of q by A4,A9;
hence thesis by A5,A9;
end;
assume
A10: x in L2;
then reconsider p = x as FinSequence of NAT by A8,FINSEQ_1:def 11;
not ex q st q in T & p is_a_proper_prefix_of q by A5,A10;
hence x in L1 by A4,A10;
end;
hence thesis by TARSKI:2;
end;
let p such that
A11: p in T;
func T|p -> Tree means :: subtree of T, which root is in p
:Def6:
q in it iff p^q in T;
existence
proof
defpred X[object] means for q st $1 = q holds p^q in T;
consider X such that
A12: for x being object holds x in X iff x in NAT* & X[x] from XBOOLE_0:sch 1;
<*> NAT in NAT* &
for q st <*> NAT = q holds p^q in T by A11,FINSEQ_1:34,def 11;
then reconsider X as non empty set by A12;
A13: X c= NAT*
by A12;
A14: now
let q such that
A15: q in X;
thus ProperPrefixes q c= X
proof
let x be object;
assume x in ProperPrefixes q;
then consider r being FinSequence such that
A16: x = r and
A17: r is_a_proper_prefix_of q by Def2;
r is_a_prefix_of q by A17;
then A18: ex n st r = q|Seg n;
then reconsider r as FinSequence of NAT by FINSEQ_1:18;
consider s being FinSequence such that
A19: q = r^s by A18,FINSEQ_1:80;
A20: p^q in T by A12,A15;
p^q = p^r^s by A19,FINSEQ_1:32;
then r in NAT* &
for q st r = q holds p^q in T by A20,Th20,FINSEQ_1:def 11;
hence thesis by A12,A16;
end;
end;
now
let q,k,n;
assume that
A21: q^<*k*> in X and
A22: n <= k;
reconsider kk=k, nn=n as Element of NAT by ORDINAL1:def 12;
p^(q^<*kk*>) in T by A12,A21;
then p^q^<*k*> in T by FINSEQ_1:32;
then p^q^<*n*> in T by A22,Def3;
then q^<*nn*> in NAT* &
for r st r = q^<*nn*> holds p^r in T by FINSEQ_1:32,def 11;
hence q^<*n*> in X by A12;
end;
then reconsider X as Tree by A13,A14,Def3;
take X;
let q;
thus q in X implies p^q in T by A12;
assume p^q in T;
then q
in NAT* & for r be FinSequence of NAT st q = r holds p^r in T by
FINSEQ_1:def 11;
hence thesis by A12;
end;
uniqueness
proof
let T1,T2 be Tree such that
A23: q in T1 iff p^q in T and
A24: q in T2 iff p^q in T;
now
let x be object;
thus x in T1 implies x in T2
proof
assume
A25: x in T1;
then reconsider q = x as FinSequence of NAT by Th18;
p^q in T by A23,A25;
hence thesis by A24;
end;
assume
A26: x in T2;
then reconsider q = x as FinSequence of NAT by Th18;
p^q in T by A24,A26;
hence x in T1 by A23;
end;
hence thesis by TARSKI:2;
end;
end;
theorem
T|(<*> NAT) = T
proof
A1: <*> NAT in T by Th21;
thus T|(<*> NAT) c= T
proof
let x be object;
assume x in T|(<*> NAT);
then reconsider p = x as Element of T|(<*> NAT);
{}^p = p by FINSEQ_1:34;
hence thesis by A1,Def6;
end;
let x be object;
assume x in T;
then reconsider p = x as Element of T;
{}^p = p by FINSEQ_1:34;
hence thesis by A1,Def6;
end;
registration
let T be finite Tree;
let p be Element of T;
cluster T|p -> finite;
coherence
proof
consider t being Function such that
A1: rng t = T and
A2: dom t in omega by FINSET_1:def 1;
defpred P[object,object] means
ex q st t.$1 = q & ((ex r st $2 = r & q = p^r) or
(for r holds q <> p^r) & $2 = <*> NAT);
A3: for x being object st x in dom t ex y being object st P[x,y]
proof
let x be object;
assume x in dom t;
then t.x in T by A1,FUNCT_1:def 3;
then reconsider q = t.x as FinSequence of NAT by Th18;
(ex r st q = p^r) implies thesis;
hence thesis;
end;
consider f being Function such that
A4: dom f = dom t &
for x being object st x in dom t holds P[x,f.x] from CLASSES1:sch 1(
A3);
T|p is finite
proof
take f;
thus rng f c= T|p
proof
let x be object;
assume x in rng f;
then consider y being object such that
A5: y in dom f and
A6: x = f.y by FUNCT_1:def 3;
consider q such that
A7: t.y = q and
A8: (ex r st x = r & q = p^r) or (for r holds q <> p^r) & x = <*> NAT
by A4,A5,A6;
assume
A9: not x in T|p;
p
^(<*> NAT) = p & q in T by A1,A4,A5,A7,FINSEQ_1:34,FUNCT_1:def 3;
hence contradiction by A8,A9,Def6;
end;
thus T|p c= rng f
proof
let x be object;
assume
A10: x in T|p;
then reconsider q = x as FinSequence of NAT by Th18;
p^q in T by A10,Def6;
then consider y being object such that
A11: y in dom t and
A12: p^q = t.y by A1,FUNCT_1:def 3;
P[y,f.y] by A4,A11;
then x = f.y by A12,FINSEQ_1:33;
hence thesis by A4,A11,FUNCT_1:def 3;
end;
thus thesis by A2,A4;
end;
hence thesis;
end;
end;
definition
let T;
assume
A1: Leaves T <> {};
mode Leaf of T -> Element of T means
it in Leaves T;
existence
proof set x = the Element of Leaves T;
reconsider x as Element of T by A1,TARSKI:def 3;
take x;
thus thesis by A1;
end;
end;
definition
let T;
mode Subtree of T -> Tree means
ex p being Element of T st it = T|p;
existence
proof set p = the Element of T;
take T|p, p;
thus thesis;
end;
end;
reserve t for Element of T;
definition
let T,p,T1;
assume
A1: p in T;
func T with-replacement (p,T1) -> Tree means
:Def9:
q in it iff q in T & not p is_a_proper_prefix_of q or
ex r st r in T1 & q = p^r;
existence
proof
reconsider p9 = p as Element of T by A1;
not p is_a_proper_prefix_of p9;
then p in { t : not p is_a_proper_prefix_of t };
then reconsider X = { t : not p is_a_proper_prefix_of t } \/
the set of all p^s where s is Element of T1 as non empty set;
A2: x in { t : not p is_a_proper_prefix_of t } implies
x is FinSequence of NAT & x in NAT* & x in T
proof
assume x in { t : not p is_a_proper_prefix_of t };
then A3: ex t st x = t & not p is_a_proper_prefix_of t;
hence x is FinSequence of NAT;
thus thesis by A3,FINSEQ_1:def 11;
end;
X is Tree-like
proof
thus X c= NAT*
proof
let x be object;
assume x in X;
then A4: x in { t : not p is_a_proper_prefix_of t } or
x in the set of all p^s where s is Element of T1
by XBOOLE_0:def 3;
now
assume x in the set of all p^s where s is Element of T1;
then ex s being Element of T1 st x = p^s;
hence x is FinSequence of NAT;
end;
hence thesis by A2,A4,FINSEQ_1:def 11;
end;
thus for q st q in X holds ProperPrefixes q c= X
proof
let q such that
A5: q in X;
A6: now
assume q in { t : not p is_a_proper_prefix_of t };
then A7: ex t st q = t & not p is_a_proper_prefix_of t;
then A8: ProperPrefixes q c= T by Def3;
thus ProperPrefixes q c= X
proof
let x be object;
assume
A9: x in ProperPrefixes q;
then consider p1 such that
A10: x = p1 and
A11: p1 is_a_proper_prefix_of q by Def2;
reconsider p1 as Element of T by A8,A9,A10;
not p is_a_proper_prefix_of p1 by A7,A11,XBOOLE_1:56;
then x in { s1 where s1 is Element of T :
not p is_a_proper_prefix_of s1 } by A10;
hence thesis by XBOOLE_0:def 3;
end;
end;
now
assume q in the set of all p^s where s is Element of T1;
then consider s being Element of T1 such that
A12: q = p^s;
thus ProperPrefixes q c= X
proof
let x be object;
assume
A13: x in ProperPrefixes q;
then reconsider r = x as FinSequence by Th10;
r is_a_proper_prefix_of p^s by A12,A13,Th11;
then r is_a_prefix_of p^s;
then consider r1 being FinSequence such that
A14: p^s = r^r1 by Th1;
A15: now
assume len p <= len r;
then consider r2 being FinSequence such that
A16: p^r2 = r by A14,FINSEQ_1:47;
p^s = p^(r2^r1) by A14,A16,FINSEQ_1:32;
then s = r2^r1 by FINSEQ_1:33;
then A17: dom
r2 = Seg len r2 & s|dom r2 = r2 by FINSEQ_1:21,def 3;
then reconsider r2 as FinSequence of NAT by FINSEQ_1:18;
r2 is_a_prefix_of s by A17;
then reconsider r2 as Element of T1 by Th19;
r = p^r2 by A16;
then r in the set of all p^v where v is Element of T1;
hence r in X by XBOOLE_0:def 3;
end;
now
assume len r <= len p;
then ex r2 being FinSequence st r^r2 = p by A14,FINSEQ_1:47;
then A18: p|dom r = r by FINSEQ_1:21;
A19: dom r = Seg len r by FINSEQ_1:def 3;
then
reconsider r3 = r as FinSequence of NAT by A18,FINSEQ_1:18;
A20: r3 is_a_prefix_of p by A18,A19;
then A21: not p is_a_proper_prefix_of r3 by XBOOLE_0:def 8;
reconsider r3 as Element of T by A1,A20,Th19;
r3 in { t : not p is_a_proper_prefix_of t } by A21;
hence r in X by XBOOLE_0:def 3;
end;
hence thesis by A15;
end;
end;
hence thesis by A5,A6,XBOOLE_0:def 3;
end;
let q,k,n such that
A22: q^<*k*> in X and
A23: n <= k;
A24: now
assume q^<*k*> in { t : not p is_a_proper_prefix_of t };
then A25: ex s being Element of T st
q^<*k*> = s & not p is_a_proper_prefix_of s;
then reconsider u = q^<*n*> as Element of T by A23,Def3;
now
assume p is_a_proper_prefix_of u;
then p is_a_prefix_of q by Th8;
hence contradiction by A25,Th7;
end;
then q^<*n*> in { t : not p is_a_proper_prefix_of t };
hence thesis by XBOOLE_0:def 3;
end;
now
assume q^<*k*> in the set of all p^s where s is Element of T1;
then consider s being Element of T1 such that
A26: q^<*k*> = p^s;
A27: now
assume len q <= len p;
then consider r being FinSequence such that
A28: q^r = p by A26,FINSEQ_1:47;
q^<*k*> = q^(r^s) by A26,A28,FINSEQ_1:32;
then A29: <*k*> = r^s by FINSEQ_1:33;
A30: now
assume
A31: r = <*k*>;
then reconsider s = q^<*n*> as Element of T by A1,A23,A28,Def3;
now
assume
A32: p is_a_proper_prefix_of s;
len p = len q + len <*k*> by A28,A31,FINSEQ_1:22
.= len q + 1 by FINSEQ_1:40
.= len q + len <*n*> by FINSEQ_1:40
.= len s by FINSEQ_1:22;
hence contradiction by A32,CARD_2:102;
end;
hence q^<*n*> in { t : not p is_a_proper_prefix_of t };
end;
now
assume that
A33: s = <*k*> and
A34: r = {};
s = {}^s & {} = <*> NAT by FINSEQ_1:34;
then {}^<*n*> in T1 by A23,A33,Def3;
then reconsider t = <*n*> as Element of T1 by FINSEQ_1:34;
q^<*n*> = p^t by A28,A34,FINSEQ_1:34;
hence
q^<*n*> in the set of all p^v where v is Element of T1;
end;
hence thesis by A29,A30,FINSEQ_1:88,XBOOLE_0:def 3;
end;
now
assume len p <= len q;
then consider r being FinSequence such that
A35: p^r = q by A26,FINSEQ_1:47;
p^(r^<*k*>) = p^s by A26,A35,FINSEQ_1:32;
then A36: r^<*k*> = s by FINSEQ_1:33;
then
dom r = Seg len r & s|dom r = r by FINSEQ_1:21,def 3;
then reconsider r as FinSequence of NAT by FINSEQ_1:18;
reconsider t = r^<*n*> as Element of T1 by A23,A36,Def3;
q^<*n*> = p^t by A35,FINSEQ_1:32;
then q^<*n*> in the set of all p^v where v is Element of T1;
hence thesis by XBOOLE_0:def 3;
end;
hence thesis by A27;
end;
hence thesis by A22,A24,XBOOLE_0:def 3;
end;
then reconsider X as Tree;
take X;
let q;
thus q in X implies q in T & not p is_a_proper_prefix_of q or
ex r st r in T1 & q = p^r
proof
assume
A37: q in X;
A38: now
assume q in { t : not p is_a_proper_prefix_of t };
then ex s being Element of T st q = s & not p is_a_proper_prefix_of s;
hence thesis;
end;
now
assume q in the set of all p^s where s is Element of T1;
then ex s being Element of T1 st q = p^s;
hence ex r st r in T1 & q = p^r;
end;
hence thesis by A37,A38,XBOOLE_0:def 3;
end;
assume
A39: q in T & not p is_a_proper_prefix_of q or ex r st r in T1 & q = p^r;
A40: q in T & not p is_a_proper_prefix_of q implies
q in { t : not p is_a_proper_prefix_of t };
(ex r st r in T1 & q = p^r)
implies q in the set of all p^v where v is Element of T1;
hence thesis by A39,A40,XBOOLE_0:def 3;
end;
uniqueness
proof
let S1,S2 be Tree such that
A41: q in S1 iff q in T & not p is_a_proper_prefix_of q or
ex r st r in T1 & q = p^r and
A42: q in S2 iff q in T & not p is_a_proper_prefix_of q or
ex r st r in T1 & q = p^r;
thus S1 c= S2
proof
let x be object;
assume
A43: x in S1;
then reconsider q = x as FinSequence of NAT by Th18;
q
in T & not p is_a_proper_prefix_of q or ex r st r in T1 & q = p^ r
by A41,A43;
hence thesis by A42;
end;
let x be object;
assume
A44: x in S2;
then reconsider q = x as FinSequence of NAT by Th18;
q in T & not p is_a_proper_prefix_of q or ex r st r in T1 & q = p^r
by A42,A44;
hence thesis by A41;
end;
end;
theorem Th31:
p in T implies T with-replacement (p,T1) =
{ t1 where t1 is Element of T : not p is_a_proper_prefix_of t1 } \/
the set of all p^s where s is Element of T1
proof
assume
A1: p in T;
thus
T with-replacement (p,T1) c= { t : not p is_a_proper_prefix_of t } \/
the set of all p^s where s is Element of T1
proof
let x be object;
assume
A2: x in T with-replacement (p,T1);
then reconsider q = x as FinSequence of NAT by Th18;
A3: (ex r st r in T1 & q = p^r) implies
x in the set of all p^s where s is Element of T1;
q in T & not p is_a_proper_prefix_of q implies
x in { t : not p is_a_proper_prefix_of t };
hence thesis by A1,A2,A3,Def9,XBOOLE_0:def 3;
end;
let x be object such that
A4: x in { t : not p is_a_proper_prefix_of t } \/
the set of all p^s where s is Element of T1;
A5: now
assume x in the set of all p^s where s is Element of T1;
then ex s being Element of T1 st x = p^s;
hence thesis by A1,Def9;
end;
now
assume x in { t : not p is_a_proper_prefix_of t };
then ex t st x = t & not p is_a_proper_prefix_of t;
hence thesis by A1,Def9;
end;
hence thesis by A4,A5,XBOOLE_0:def 3;
end;
theorem
p in T implies T1 = T with-replacement (p,T1)|p
proof
assume
A1: p in T;
then A2: p in T with-replacement (p,T1) by Def9;
thus T1 c= T with-replacement (p,T1)|p
proof
let x be object;
assume
A3: x in T1;
then reconsider q = x as FinSequence of NAT by Th18;
p^q in T with-replacement (p,T1) by A1,A3,Def9;
hence thesis by A2,Def6;
end;
let x be object;
assume
A4: x in T with-replacement (p,T1)|p;
then reconsider q = x as FinSequence of NAT by Th18;
A5: p^q in T with-replacement (p,T1) by A2,A4,Def6;
A6: now
assume that
p^q in T and
A7: not p is_a_proper_prefix_of p^q;
p is_a_prefix_of p^q by Th1;
then p^q = p by A7
.= p^{} by FINSEQ_1:34;
then q = {} by FINSEQ_1:33;
hence q in T1 by Th21;
end;
(ex r st r in T1 & p^q = p^r) implies q in T1 by FINSEQ_1:33;
hence thesis by A1,A5,A6,Def9;
end;
registration
let T be finite Tree, t be Element of T;
let T1 be finite Tree;
cluster T with-replacement (t,T1) -> finite;
coherence
proof
A1: { s where s is Element of T : not t is_a_proper_prefix_of s } c= T
proof
let x be object;
assume
x in { s where s is Element of T : not t is_a_proper_prefix_of s };
then
ex s being Element of T st x = s & not t is_a_proper_prefix_of s;
hence thesis;
end;
T1,the set of all t^s where s is Element of T1 are_equipotent
proof
defpred P[object,object] means ex q st $1 = q & $2 = t^q;
A2: for x being object holds x in T1 implies ex y being object st P[x,y]
proof let x be object;
assume x in T1;
then reconsider q = x as FinSequence of NAT by Th18;
t^q = t^q;
hence thesis;
end;
consider f such that
A3: dom f = T1 &
for x being object st x in T1 holds P[x,f.x] from CLASSES1:sch 1(A2);
take f;
thus f is one-to-one
proof
let x,y be object;
assume that
A4: x in dom f & y in dom f and
A5: f.x = f.y;
(
ex q st x = q & f.x = t^q)& ex r st y = r & f.y = t^r by A3,A4;
hence thesis by A5,FINSEQ_1:33;
end;
thus dom f = T1 by A3;
thus rng f c= the set of all t^s where s is Element of T1
proof
let x be object;
assume x in rng f;
then consider y being object such that
A6: y in dom f and
A7: x = f.y by FUNCT_1:def 3;
consider q such that
A8: y = q and
A9: f.y = t^q by A3,A6;
reconsider q as Element of T1 by A3,A6,A8;
x = t^q by A7,A9;
hence thesis;
end;
let x be object;
assume x in the set of all t^s where s is Element of T1;
then consider s being Element of T1 such that
A10: x = t^s;
P[s,f.s] by A3;
hence thesis by A3,A10,FUNCT_1:def 3;
end;
then the set of all t^s where s is Element of T1 is finite
by CARD_1:38;
then
{ v where v is Element of T : not t is_a_proper_prefix_of v } \/ the set of
all t^s
where s is Element of T1 is finite by A1;
hence thesis by Th31;
end;
end;
reserve w for FinSequence;
theorem Th33:
for p being FinSequence holds ProperPrefixes p,dom p are_equipotent
proof
let p be FinSequence;
defpred P[object,object] means ex w st $1 = w & $2 = (len w)+1;
A1: for x being object st x in ProperPrefixes p ex y being object st P[x,y]
proof
let x be object;
assume x in ProperPrefixes p;
then consider q being FinSequence such that
A2: x = q and q is_a_proper_prefix_of p by Def2;
reconsider y = (len q)+1 as set;
take y,q;
thus thesis by A2;
end;
consider f such that
A3: dom f = ProperPrefixes p and
A4: for x being object st x in ProperPrefixes p holds P[x,f.x]
from CLASSES1:sch 1(A1);
take f;
thus f is one-to-one
proof
let x,y be object;
assume that
A5: x in dom f & y in dom f and
A6: f.x = f.y;
(
ex q being FinSequence st x = q & f.x = (len q)+1 )& ex r being FinSequence
st y = r & f.x = (len r)+1 by A3,A4,A5,A6;
hence thesis by A3,A5,Th3,Th17;
end;
thus dom f = ProperPrefixes p by A3;
thus rng f c= dom p
proof
let x be object;
assume x in rng f;
then consider y being object such that
A7: y in dom f and
A8: x = f.y by FUNCT_1:def 3;
consider q being FinSequence such that
A9: y = q and
A10: x = (len q)+1 by A3,A4,A7,A8;
len q < len p by A3,A7,A9,Th12;
then 0+1 <= (len q)+1 & (len q)+1 <= len p by NAT_1:13;
then x in Seg len p by A10,FINSEQ_1:1;
hence thesis by FINSEQ_1:def 3;
end;
let x be object;
assume
A11: x in dom p;
then A12: x in Seg len p by FINSEQ_1:def 3;
reconsider n = x as Nat by A11;
A13: 1 <= n by A12,FINSEQ_1:1;
A14: n <= len p by A12,FINSEQ_1:1;
consider m be Nat such that
A15: n = 1+m by A13,NAT_1:10;
reconsider m as Nat;
reconsider q = p|Seg m as FinSequence by FINSEQ_1:15;
A16: m <= len p by A14,A15,NAT_1:13;
A17: m <> len p by A14,A15,NAT_1:13;
A18: len q = m by A16,FINSEQ_1:17;
A19: q is_a_prefix_of p;
len q = m by A16,FINSEQ_1:17;
then q is_a_proper_prefix_of p by A17,A19;
then A20: q in ProperPrefixes p by Th11;
then ex r being FinSequence st q = r & f.q = (len r)+1 by A4;
hence thesis by A3,A15,A18,A20,FUNCT_1:def 3;
end;
registration
let p be FinSequence;
cluster ProperPrefixes p -> finite;
coherence
proof
ProperPrefixes p,dom p are_equipotent by Th33;
hence thesis by CARD_1:38;
end;
end;
theorem
for p being FinSequence holds card ProperPrefixes p = len p
proof
let p be FinSequence;
A1: dom p = Seg len p by FINSEQ_1:def 3;
A2: ProperPrefixes p,dom p are_equipotent by Th33;
card dom p = card len p by A1,FINSEQ_1:55;
hence thesis by A2,CARD_1:5;
end;
::
:: Height and width of finite trees
::
definition
let IT be set;
attr IT is AntiChain_of_Prefixes-like means
:Def10:
(for x st x in IT holds x is FinSequence) &
for p1,p2 st p1 in IT & p2 in IT & p1 <> p2 holds
not p1,p2 are_c=-comparable;
end;
registration
cluster AntiChain_of_Prefixes-like for set;
existence
proof
take {};
thus for x st x in {} holds x is FinSequence;
let p1,p2;
thus thesis;
end;
end;
definition
mode AntiChain_of_Prefixes is AntiChain_of_Prefixes-like set;
end;
theorem Th35:
{ w } is AntiChain_of_Prefixes-like
proof
thus for x st x in { w } holds x is FinSequence by TARSKI:def 1;
let p1,p2;
assume that
A1: p1 in { w } and
A2: p2 in { w };
p1 = w by A1,TARSKI:def 1;
hence thesis by A2,TARSKI:def 1;
end;
theorem Th36:
not p1,p2 are_c=-comparable implies { p1,p2 } is AntiChain_of_Prefixes-like
proof
assume
A1: not p1,p2 are_c=-comparable;
thus for x st x in { p1,p2 } holds x is FinSequence by TARSKI:def 2;
let q1,q2 be FinSequence;
assume that
A2: q1 in { p1,p2 } and
A3: q2 in { p1,p2 };
A4: q1 = p1 or q1 = p2 by A2,TARSKI:def 2;
q2 = p1 or q2 = p2 by A3,TARSKI:def 2;
hence thesis by A1,A4;
end;
definition
let T;
mode AntiChain_of_Prefixes of T -> AntiChain_of_Prefixes means
:Def11:
it c= T;
existence
proof set t = the Element of T;
reconsider S = { t } as AntiChain_of_Prefixes by Th35;
take S;
let x be object;
assume x in S;
then x = t by TARSKI:def 1;
hence thesis;
end;
end;
reserve t1,t2 for Element of T;
theorem Th37:
{} is AntiChain_of_Prefixes of T & { {} } is AntiChain_of_Prefixes of T
proof
{} is AntiChain_of_Prefixes-like;
then reconsider S = {} as AntiChain_of_Prefixes;
S c= T;
hence {} is AntiChain_of_Prefixes of T by Def11;
reconsider S = D as AntiChain_of_Prefixes by Th35;
S is AntiChain_of_Prefixes of T
proof
let x be object;
assume x in S;
then x = {} by TARSKI:def 1;
hence thesis by Th21;
end;
hence thesis;
end;
theorem
{ t } is AntiChain_of_Prefixes of T
proof reconsider S = { t } as AntiChain_of_Prefixes by Th35;
S is AntiChain_of_Prefixes of T
proof
let x be object;
assume x in S;
then x = t by TARSKI:def 1;
hence thesis;
end;
hence thesis;
end;
theorem
not t1,t2 are_c=-comparable implies { t1,t2 } is AntiChain_of_Prefixes of T
proof
assume not t1,t2 are_c=-comparable;
then reconsider A = { t1,t2 } as AntiChain_of_Prefixes by Th36;
A is AntiChain_of_Prefixes of T
proof
let x be object;
assume x in A;
then x = t1 or x = t2 by TARSKI:def 2;
hence thesis;
end;
hence thesis;
end;
registration
let T be finite Tree;
cluster -> finite for AntiChain_of_Prefixes of T;
coherence
proof
let X be AntiChain_of_Prefixes of T;
X c= T by Def11;
hence thesis;
end;
end;
definition
let T be finite Tree;
func height T -> Nat means
:Def12:
(ex p st p in T & len p = it) & for p st p in T holds len p <= it;
existence
proof
consider n be Nat such that
A1: T,Seg n are_equipotent by FINSEQ_1:56;
defpred X[Nat] means for p st p in T holds len p <= $1;
A2: ex n be Nat st X[n]
proof
now
given p such that
A3: p in T and
A4: not len p <= n;
A5: ProperPrefixes p c= T by A3,Def3;
A6: ProperPrefixes p,dom p are_equipotent by Th33;
A7: card ProperPrefixes p c= card T by A5,CARD_1:11;
A8: card ProperPrefixes p = card dom p by A6,CARD_1:5;
A9: card
T = card Seg n & dom p = Seg len p by A1,CARD_1:5,FINSEQ_1:def 3;
Seg n c= Seg len p by A4,FINSEQ_1:5;
then A10: card Seg n c= card Seg len p by CARD_1:11;
card
Seg n = card n & card Seg len p = card len p by FINSEQ_1:55;
then card n = card len p by A7,A8,A9,A10;
hence contradiction by A4;
end;
then consider n be Nat such that
A11: X[n];
reconsider n as Nat;
take n;
thus thesis by A11;
end;
consider n being Nat such that
A12: X[n] and
A13: for m be Nat st X[m] holds n <= m from NAT_1:sch 5(A2);
set x = the Element of T;
reconsider n as Nat;
take n;
thus ex p st p in T & len p = n
proof
assume
A14: for p st p in T holds len p <> n;
reconsider x as FinSequence of NAT;
len x <= n by A12;
then len x < n by A14,XXREAL_0:1;
then consider k be Nat such that
A15: n = k+1 by NAT_1:6;
reconsider k as Nat;
for p st p in T holds len p <= k
proof
let p;
assume
A16: p in T;
then len p <= n by A12;
then len p < k+1 by A14,A15,A16,XXREAL_0:1;
hence thesis by NAT_1:13;
end;
then n <= k by A13;
hence contradiction by A15,NAT_1:13;
end;
let p;
assume p in T;
hence thesis by A12;
end;
uniqueness
proof
let l1,l2 be Nat;
given p1 being FinSequence of NAT such that
A17: p1 in T & len p1 = l1;
assume
A18: for p st p in T holds len p <= l1;
given p2 being FinSequence of NAT such that
A19: p2 in T & len p2 = l2;
assume for p st p in T holds len p <= l2;
then A20: l1 <= l2 by A17;
l2 <= l1 by A18,A19;
hence thesis by A20,XXREAL_0:1;
end;
func width T -> Nat means
:Def13:
ex X being AntiChain_of_Prefixes of T st it = card X &
for Y being AntiChain_of_Prefixes of T holds card Y <= card X;
existence
proof
defpred X[Nat] means ex X being finite set st $1 = card X & X c= T &
(for p,q st p in X & q in X & p <> q holds not p,q are_c=-comparable);
0 = card {} & for p,q st p in {} & q in {} & p <> q holds not p,q
are_c=-comparable;
then A21: ex n be Nat st X[n] by XBOOLE_1:2;
A22: for n be Nat st X[n] holds n <= card T
proof
let n be Nat;
given X being finite set such that
A23: n = card X & X c= T and
for p,q st p in X & q in X & p <> q holds not p,q are_c=-comparable;
A24: Segm card X c= Segm card T & card X = card n by A23,CARD_1:11;
card T = card Segm card T;
hence thesis by A24,NAT_1:40;
end;
consider n being Nat such that
A25: X[n] and
A26: for m be Nat st X[m] holds m <= n from NAT_1:sch 6(A22,A21);
consider X being finite set such that
A27: n = card X and
A28: X c= T and
A29: for p,q st p in X & q in X & p <> q holds not p,q are_c=-comparable
by A25;
X is AntiChain_of_Prefixes-like
proof
thus for x st x in X holds x is FinSequence
proof
let x;
assume
A30: x in X;
T c= NAT* by Def3;
hence thesis by A30,A28;
end;
let p1,p2;
assume
A31: p1 in X & p2 in X;
then reconsider q1 = p1, q2 = p2 as Element of T by A28;
p1 = q1 & p2 = q2;
hence thesis by A29,A31;
end;
then reconsider X as AntiChain_of_Prefixes;
reconsider X as AntiChain_of_Prefixes of T by A28,Def11;
reconsider n as Nat;
take n,X;
thus n = card X by A27;
let Y be AntiChain_of_Prefixes of T;
Y
c= T & for p,q st p in Y & q in Y & p <> q holds not p,q are_c=-comparable
by Def10,Def11;
hence thesis by A26,A27;
end;
uniqueness
proof
let n1,n2 be Nat;
given X1 being AntiChain_of_Prefixes of T such that
A32: n1 = card X1 and
A33: for Y being AntiChain_of_Prefixes of T holds card Y <= card X1;
given X2 being AntiChain_of_Prefixes of T such that
A34: n2 = card X2 and
A35: for Y being AntiChain_of_Prefixes of T holds card Y <= card X2;
A36: card X1 <= card X2 by A35;
card X2 <= card X1 by A33;
hence thesis by A32,A34,A36,XXREAL_0:1;
end;
end;
theorem
1 <= width fT
proof
(
ex X being AntiChain_of_Prefixes of fT st width fT = card X & for Y being
AntiChain_of_Prefixes of fT holds card Y <= card X)&
D is AntiChain_of_Prefixes of fT by Def13,Th37;
then card D <= width fT;
hence thesis by CARD_1:30;
end;
theorem
height elementary_tree 0 = 0
proof
now
thus ex p st p in elementary_tree 0 & len p = 0
proof
take <*> NAT;
thus thesis by Th28,TARSKI:def 1;
end;
let p;
assume p in elementary_tree 0;
then p = {} by Th28,TARSKI:def 1;
hence len p <= 0;
end;
hence thesis by Def12;
end;
theorem
height fT = 0 implies fT = elementary_tree 0
proof
assume
A1: height fT = 0;
thus fT c= elementary_tree 0
proof
let x be object;
assume x in fT;
then reconsider t = x as Element of fT;
len t = 0 by A1,Def12;
then x = {};
hence thesis by Th21;
end;
let x be object;
assume x in elementary_tree 0;
then x = {} by Th28,TARSKI:def 1;
hence thesis by Th21;
end;
theorem
height elementary_tree(n+1) = 1
proof
set T = elementary_tree(n+1);
now
thus ex p st p in T & len p = 1
proof
take p = <*0*>;
thus p in T by Th27;
thus thesis by FINSEQ_1:40;
end;
let p such that
A1: p in T;
A2: p in D implies p = {} by TARSKI:def 1;
now
assume p in { <*k*> : k < n+1 };
then ex k st p = <*k*> & k < n+1;
hence len p = 1 by FINSEQ_1:40;
end;
hence len p <= 1 by A1,A2,XBOOLE_0:def 3;
end;
hence thesis by Def12;
end;
theorem
width elementary_tree 0 = 1
proof
set T = elementary_tree 0;
now reconsider X = D as AntiChain_of_Prefixes of T by Th37;
take X;
thus 1 = card X by CARD_1:30;
let Y be AntiChain_of_Prefixes of T;
Y c= X by Def11,Th28;
hence card Y <= card X by NAT_1:43;
end;
hence thesis by Def13;
end;
theorem
width elementary_tree(n+1) = n+1
proof
set T = elementary_tree(n+1);
now
{ <*k*> : k < n+1 } is AntiChain_of_Prefixes-like
proof
thus x in { <*k*> : k < n+1 } implies x is FinSequence
proof
assume x in { <*k*> : k < n+1 };
then ex k st x = <*k*> & k < n+1;
hence thesis;
end;
let p1,p2;
assume p1 in { <*k*> : k < n+1 } & p2 in { <*m*> : m < n+1 };
then (
ex k st p1 = <*k*> & k < n+1)& ex m st p2 = <*m*> & m < n+1;
hence thesis by Th4;
end;
then reconsider X = { <*k*> : k < n+1 } as AntiChain_of_Prefixes;
X c= T by XBOOLE_1:7;
then reconsider X as AntiChain_of_Prefixes of T by Def11;
take X;
X,Seg(n+1) are_equipotent
proof
defpred P[object,object] means ex n st $1 = <*n*> & $2 = n+1;
A1: x in X & P[x,y] & P[x,z] implies y = z
proof
assume x in X;
given n1 being Nat such that
A2: x = <*n1*> & y = n1+1;
given n2 being Nat such that
A3: x = <*n2*> & z = n2+1;
<*n1*>.1 = n1;
hence thesis by A2,A3,FINSEQ_1:def 8;
end;
A4: for x being object holds x in X implies ex y being object st P[x,y]
proof let x be object;
assume x in X;
then consider k such that
A5: x = <*k*> and k < n+1;
reconsider y = k+1 as set;
take y;
thus thesis by A5;
end;
consider f such that
A6: dom f = X &
for x being object st x in X holds P[x,f.x] from CLASSES1:sch 1(A4);
take f;
thus f is one-to-one
proof
let x,y be object;
assume that
A7: x in dom f & y in dom f and
A8: f.x = f.y;
(ex k1 being Nat st x = <*k1*> & f.x = k1+1)&
ex k2 being Nat st y = <*k2*> & f.y = k2+1 by A6,A7;
hence thesis by A8;
end;
thus dom f = X by A6;
thus rng f c= Seg(n+1)
proof
let x be object;
assume x in rng f;
then consider y being object such that
A9: y in dom f and
A10: x = f.y by FUNCT_1:def 3;
consider k such that
A11: y = <*k*> and
A12: x = k+1 by A6,A9,A10;
consider m such that
A13: y = <*m*> & m < n+1 by A6,A9;
<*k*>.1 = k & <*m*>.1 = m;
then 0+1 <= k+1 & k+1 <= n+1 by A11,A13,NAT_1:13;
hence thesis by A12,FINSEQ_1:1;
end;
let x be object;
assume
A14: x in Seg(n+1);
then reconsider k = x as Nat;
A15: 1 <= k by A14,FINSEQ_1:1;
A16: k <= n+1 by A14,FINSEQ_1:1;
consider m be Nat such that
A17: k = 1+m by A15,NAT_1:10;
reconsider m as Nat;
m < n+1 by A16,A17,NAT_1:13;
then A18: <*m*> in X;
then P[<*m*>,f.<*m*>] by A6;
then x = f.<*m*> by A1,A17,A18;
hence thesis by A6,A18,FUNCT_1:def 3;
end;
then A19: card Seg(n+1) = card X by CARD_1:5;
hence n+1 = card X by FINSEQ_1:57;
let Y be AntiChain_of_Prefixes of T;
A20: Y c= T by Def11;
A21: {} in Y implies Y = D
proof
assume that
A22: {} in Y and
A23: Y <> D;
consider x being object such that
A24: not (x in Y iff x in D) by A23,TARSKI:2;
A25: {} <> x by A22,A24,TARSKI:def 1;
reconsider x as FinSequence of NAT by A20,A24,Th18;
{} is_a_prefix_of x;
then {},x are_c=-comparable;
hence contradiction by A22,A24,A25,Def10,TARSKI:def 1;
end;
A26: card D = 1 & 1 <= 1+n by CARD_1:30,NAT_1:11;
now
assume
A27: not {} in Y;
Y c= X
proof
let x be object;
assume
A28: x in Y;
then x in { <*k*> : k < n+1 } or x in D by A20,XBOOLE_0:def 3;
hence thesis by A27,A28,TARSKI:def 1;
end;
hence card Y <= card X by NAT_1:43;
end;
hence card Y <= card X by A19,A21,A26,FINSEQ_1:57;
end;
hence thesis by Def13;
end;
theorem
for t being Element of fT holds height(fT|t) <= height fT
proof
let t be Element of fT;
consider p such that
A1: p in fT|t and
A2: len p = height(fT|t) by Def12;
t^p in fT by A1,Def6;
then A3: len(t^p) <= height fT by Def12;
len(t^p) = len t + len p & len p <= len p + len t by FINSEQ_1:22,NAT_1:11;
hence thesis by A2,A3,XXREAL_0:2;
end;
theorem Th47:
for t being Element of fT st t <> {} holds height(fT|t) < height fT
proof
let t be Element of fT;
assume t <> {};
then A1: 0+1 <= len t by NAT_1:13;
consider p such that
A2: p in fT|t and
A3: len p = height(fT|t) by Def12;
t^p in fT by A2,Def6;
then A4: len(t^p) <= height fT by Def12;
len(t^p) = len t + len p & len p + 1 <= len t + len p by A1,FINSEQ_1:22
,XREAL_1:7;
then height(fT|t)+1 <= height fT by A3,A4,XXREAL_0:2;
hence thesis by NAT_1:13;
end;
scheme TreeInd { P[Tree] }: for fT holds P[fT]
provided
A1: for fT st
for n being Element of NAT st <*n*> in fT holds P[fT|<*n*>]
holds P[fT]
proof
defpred X[set] means for fT holds height fT = $1 implies P[fT];
A2: for n being Nat st for k being Nat st k < n holds X[k] holds X[n]
proof
let n be Nat such that
A3: for k being Nat st k < n for fT st height fT = k holds P[fT];
let fT such that
A4: height fT = n;
now
let k be Element of NAT;
assume <*k*> in fT;
then reconsider k9 = <*k*> as Element of fT;
height(fT|k9) < height fT by Th47;
hence P[fT|<*k*>] by A3,A4;
end;
hence thesis by A1;
end;
A5: for n be Nat holds X[n] from NAT_1:sch 4(A2);
let fT;
height fT = height fT;
hence thesis by A5;
end;
begin :: Addenda
:: from MODAL_1, 2007.03.14, A.T.
reserve s,t for FinSequence;
theorem
w^t is_a_proper_prefix_of w^s implies t is_a_proper_prefix_of s
proof
assume
A1: w^t is_a_proper_prefix_of w^s;
then w^t is_a_prefix_of w^s;
then consider a be FinSequence such that
A2: w^s = w^t^a by Th1;
w^t^a = w^(t^a) by FINSEQ_1:32;
then s= t^a by A2,FINSEQ_1:33;
then t is_a_prefix_of s by Th1;
hence thesis by A1;
end;
theorem
n <> m implies not <*n*> is_a_prefix_of <*m*>^s
proof
assume
A1: n <> m;
assume <*n*> is_a_prefix_of <*m*>^s;
then A2: ex a be FinSequence st <*m*>^s = <*n*>^a by Th1;
m = (<*m*>^s).1 by FINSEQ_1:41
.= n by A2,FINSEQ_1:41;
hence contradiction by A1;
end;
theorem
elementary_tree 1 = {{},<*0*>}
proof
now
let x be object;
thus x in {{},<*0*>} implies x in { <*n*> : n < 1 } or x in D
proof
assume x in {{},<*0*>};
then x = {} or x = <*0*> by TARSKI:def 2;
hence thesis by TARSKI:def 1;
end;
assume
A1: x in { <*n*> : n < 1 } or x in D;
now per cases by A1;
suppose
x in { <*n*> : n < 1 };
then consider n such that
A2: x = <*n*> and
A3: n < 1;
n = 0 by A3,NAT_1:25;
hence x in {{},<*0*>} by A2,TARSKI:def 2;
end;
suppose x in D;
then x = {} by TARSKI:def 1;
hence x in {{},<*0*>} by TARSKI:def 2;
end;
end;
hence x in {{},<*0*>};
end;
hence thesis by XBOOLE_0:def 3;
end;
theorem
not <*n*> is_a_proper_prefix_of <*m*>
by Th2;
theorem
elementary_tree 2 = {{},<*0*>,<*1*>}
proof
now
let x be object;
thus
x in {{},<*0*>,<*1*>} implies x in { <*n*> : n < 2 } or x in D
proof
assume x in {{},<*0*>,<*1*>};
then x = {} or x = <*0*> or x = <*1*> by ENUMSET1:def 1;
hence thesis by TARSKI:def 1;
end;
assume
A1: x in { <*n*> : n < 2 } or x in D;
now per cases by A1;
suppose
x in { <*n*> : n < 2 };
then consider n such that
A2: x = <*n*> and
A3: n < 2;
n = 0 or ... or n = 2 by A3;
hence x in {{},<*0*>,<*1*>} by A2,A3,ENUMSET1:def 1;
end;
suppose x in D;
then x = {} by TARSKI:def 1;
hence x in {{},<*0*>,<*1*>} by ENUMSET1:def 1;
end;
end;
hence x in {{},<*0*>,<*1*>};
end;
hence thesis by XBOOLE_0:def 3;
end;
:: from BINTREE1
theorem
for T being Tree, t being Element of T holds
t in Leaves T iff not t^<*0*> in T
proof
let T be Tree, t be Element of T;
hereby
assume
A1: t in Leaves T;
t is_a_proper_prefix_of t^<*0*> by Th6;
hence not t^<*0*> in T by A1,Def5;
end;
assume that
A2: not t^<*0*> in T and
A3: not t in Leaves T;
consider q being FinSequence of NAT such that
A4: q in T and
A5: t is_a_proper_prefix_of q by A3,Def5;
t is_a_prefix_of q by A5;
then consider r being FinSequence such that
A6: q = t^r by Th1;
reconsider r as FinSequence of NAT by A6,FINSEQ_1:36;
len q = len t+len r by A6,FINSEQ_1:22;
then len r <> 0 by A5,Th5;
then r <> {};
then consider p being FinSequence of NAT,
x being Element of NAT such that
A7: r = <*x*>^p by FINSEQ_2:130;
q = t^<*x*>^p by A6,A7,FINSEQ_1:32;
then t^<*x*> in T by A4,Th20;
hence contradiction by A2,Def3;
end;
theorem
for T being Tree, t being Element of T holds
t in Leaves T iff not ex n being Nat st t^<*n*> in T
proof
let T be Tree, t be Element of T;
hereby
assume
A1: t in Leaves T;
given n being Nat such that
A2: t^<*n*> in T;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
A3: not t is_a_proper_prefix_of t^<*nn*> by A1,A2,Def5;
t is_a_prefix_of t^<*n*> by Th1;
then A4: t = t^<*n*> by A3;
t = t^{} by FINSEQ_1:34;
hence contradiction by A4,FINSEQ_1:33;
end;
assume that
A5: not(ex n being Nat st t^<*n*> in T) and
A6: not t in Leaves T;
consider q being FinSequence of NAT such that
A7: q in T and
A8: t is_a_proper_prefix_of q by A6,Def5;
t is_a_prefix_of q by A8;
then consider r being FinSequence such that
A9: q = t^r by Th1;
reconsider r as FinSequence of NAT by A9,FINSEQ_1:36;
len q = len t+len r by A9,FINSEQ_1:22;
then len r <> 0 by A8,Th5;
then r <> {};
then consider p being FinSequence of NAT,
x being Element of NAT such that
A10: r = <*x*>^p by FINSEQ_2:130;
q = t^<*x*>^p by A9,A10,FINSEQ_1:32;
hence contradiction by A5,A7,Th20;
end;
definition
func TrivialInfiniteTree -> set equals
the set of all k |-> 0 where k is Nat;
coherence;
end;
registration
cluster TrivialInfiniteTree -> non empty Tree-like;
coherence
proof
set X = TrivialInfiniteTree;
0 |-> 0 in X;
hence X is non empty;
thus X c= NAT*
proof
let x be object;
assume x in X;
then ex k being Nat st x = k |-> 0;
hence thesis by FINSEQ_1:def 11;
end;
thus for p being FinSequence of NAT st p in X holds ProperPrefixes p c= X
proof
let p be FinSequence of NAT;
assume p in X;
then consider m being Nat such that
A1: p = m |-> 0;
let x be object;
assume
A2: x in ProperPrefixes p;
then reconsider x as FinSequence by Th10;
A3: for k being Nat st 1 <= k & k <= len x holds x.k = (len x |-> 0).k
proof
x is_a_proper_prefix_of p by A2,Th11;
then
A4: x c= p;
let k be Nat;
assume 1 <= k & k <= len x;
then
A5: k in dom x by FINSEQ_3:25;
thus (len x |-> 0).k = 0
.= p.k by A1
.= x.k by A5,A4,GRFUNC_1:2;
end;
len x = len (len x |-> 0) by CARD_1:def 7;
then x = len x |-> 0 by A3,FINSEQ_1:14;
hence thesis;
end;
let p be FinSequence of NAT, m, n be Nat;
assume p^<*m*> in X;
then consider k being Nat such that
A6: p^<*m*> = k |-> 0;
assume
A7: n <= m;
len (p^<*m*>) = len p + 1 by FINSEQ_2:16;
then (p^<*m*>).len (p^<*m*>) = m by FINSEQ_1:42;
then
A8: m = 0 by A6;
A9: for z being Nat st 1 <= z & z <= len (p^<*n*>) holds (len (p^<*n*>)
|-> 0).z = (p^<*n*>).z
proof
let z be Nat;
assume 1 <= z & z <= len (p^<*n*>);
thus (len (p^<*n*>) |-> 0).z = 0
.= (p^<*m*>).z by A6
.= (p^<*n*>).z by A7,A8;
end;
len (p^<*n*>) = len (len (p^<*n*>) |-> 0) by CARD_1:def 7;
then len (p^<*n*>) |-> 0 = p^<*n*> by A9,FINSEQ_1:14;
hence thesis;
end;
end;
theorem Th55:
NAT,TrivialInfiniteTree are_equipotent
proof
defpred P[Nat,set] means $2 = $1 |-> 0;
A1: for x being Element of NAT ex y being Element of TrivialInfiniteTree st
P[x,y]
proof
let x be Element of NAT;
x |-> 0 in TrivialInfiniteTree;
then reconsider y = x |-> 0 as Element of TrivialInfiniteTree;
take y;
thus thesis;
end;
consider f being sequence of TrivialInfiniteTree such that
A2: for x being Element of NAT holds P[x,f.x] from FUNCT_2:sch 3(A1);
take f;
thus f is one-to-one
proof
let x,y be object;
assume
A3: x in dom f & y in dom f;
assume
A4: f.x = f.y;
reconsider x, y as Element of NAT by A3,FUNCT_2:def 1;
( P[x,f.x])& P[y,f.y] by A2;
hence thesis by A4,FINSEQ_2:143;
end;
thus
A5: dom f = NAT by FUNCT_2:def 1;
thus rng f c= TrivialInfiniteTree by RELAT_1:def 19;
let a be object;
assume a in TrivialInfiniteTree;
then consider k being Nat such that
A6: a = k |-> 0;
A7: k in NAT by ORDINAL1:def 12;
then f.k = a by A2,A6;
hence thesis by A5,FUNCT_1:def 3,A7;
end;
registration
cluster TrivialInfiniteTree -> infinite;
coherence by Th55,CARD_1:38;
end;