:: Subtrees
:: by Grzegorz Bancerek
::
:: Received November 25, 1994
:: Copyright (c) 1994-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 XBOOLE_0, TREES_3, SUBSET_1, FINSET_1, TREES_2, TREES_1, CARD_1,
ARYTM_3, NAT_1, ORDINAL4, FINSEQ_1, ARYTM_1, RELAT_1, FUNCT_1, TARSKI,
ORDINAL1, NUMBERS, XXREAL_0, ZFMISC_1, TREES_4, FUNCT_6, TREES_A,
TREES_9, MCART_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, CARD_1, ORDINAL1,
NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, FUNCT_6, NAT_1,
BINOP_1, FINSET_1, FINSEQ_1, FINSEQ_2, TREES_1, TREES_2, TREES_3,
TREES_4, MCART_1, XXREAL_0;
constructors WELLORD2, XXREAL_0, XREAL_0, NAT_1, FINSEQ_2, TREES_4, RELSET_1,
BINOP_1, FINSEQ_4, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XREAL_0,
FINSEQ_1, TREES_1, TREES_2, TREES_3, PRE_CIRC, CARD_1, RELSET_1, NAT_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, FUNCT_1, TREES_2, TREES_3;
equalities TREES_2, TREES_4, BINOP_1, ORDINAL1;
expansions TARSKI, XBOOLE_0, FUNCT_1, TREES_4;
theorems TARSKI, AXIOMS, ZFMISC_1, NAT_1, WELLORD2, FUNCT_1, FUNCT_2,
FINSEQ_1, FINSEQ_3, CARD_1, CARD_2, FUNCT_6, TREES_1, TREES_2, TREES_3,
TREES_4, RELSET_1, RELAT_1, XBOOLE_0, FINSET_1, XREAL_1, XXREAL_0,
ORDINAL1, FINSEQ_2, TREES_A, MCART_1, FINSEQ_6, XTUPLE_0;
schemes NAT_1, FUNCT_1, FINSEQ_1, CLASSES1, FUNCT_2, TREES_2;
begin :: Root tree and successors of node in decorated tree
definition
let D be non empty set;
let F be non empty DTree-set of D;
let Tset be non empty Subset of F;
redefine mode Element of Tset -> Element of F; :: redefines Element (SUBSET_1, definition)
coherence
proof
let x be Element of Tset;
thus thesis;
end;
end;
registration
cluster finite -> finite-order for Tree;
coherence
proof
let t be Tree;
assume t is finite;
then reconsider s = t as finite Tree;
take n = card s+1;
let x be Element of t;
deffunc U(Nat) = x^<*$1-1*>;
consider f being FinSequence such that
A1: len f = n & for i being Nat st i in dom f holds f.i = U(i) from
FINSEQ_1:sch 2;
A2: dom f = Seg n by A1,FINSEQ_1:def 3;
assume
A3: x^<*n*> in t;
A4: rng f c= succ x
proof
let y be object;
assume y in rng f;
then consider i being object such that
A5: i in dom f and
A6: y = f.i by FUNCT_1:def 3;
reconsider i as Nat by A5;
i >= 1 by A2,A5,FINSEQ_1:1;
then consider j being Nat such that
A7: i = 1+j by NAT_1:10;
reconsider j as Nat;
A8: j <= i by A7,NAT_1:11;
i <= n by A2,A5,FINSEQ_1:1;
then j <= n by A8,XXREAL_0:2;
then
A9: x^<*j*> in t by A3,TREES_1:def 3;
i-1 = j by A7;
then y = x^<*j*> by A1,A5,A6;
hence thesis by A9;
end;
A10: card succ x c= card t by CARD_1:11;
f is one-to-one
proof
let z,y be object;
assume that
A11: z in dom f & y in dom f and
A12: f.z = f.y;
reconsider i1 = z, i2 = y as Nat by A11;
f.z = x^<*i1-1*> & f.y = x^<*i2-1*> by A1,A11;
then <*i1-1*> = <*i2-1*> by A12,FINSEQ_1:33;
then i1-1 = <*i2-1*>.1
.= i2-1;
hence thesis;
end;
then card dom f c= card succ x by A4,CARD_1:10;
then
A13: Segm card dom f c= Segm card s by A10;
A14: card s <= n by NAT_1:11;
card Seg n = n by FINSEQ_1:57;
then n <= card s by A2,A13,NAT_1:39;
then n = card s + 0 by A14,XXREAL_0:1;
hence contradiction;
end;
end;
Lm1: for n being set, p being FinSequence st n in dom p
ex k being Nat st n = k+1 & k < len p
proof
let n be set, p be FinSequence;
assume
A1: n in dom p;
then reconsider n as Nat;
n >= 1 by A1,FINSEQ_3:25;
then consider k being Nat such that
A2: n = 1+k by NAT_1:10;
reconsider k as Nat;
take k;
n <= len p by A1,FINSEQ_3:25;
hence thesis by A2,NAT_1:13;
end;
Lm2: now
let p,q be FinSequence such that
A1: len p = len q and
A2: for i being Nat st i < len p holds p.(i+1) = q.(i+1);
A3: now
let i be Nat;
assume i in dom p;
then ex k being Nat st i = k+1 & k < len p by Lm1;
hence p.i = q.i by A2;
end;
dom p = dom q by A1,FINSEQ_3:29;
hence p = q by A3;
end;
Lm3: for n being Nat, p being FinSequence holds n < len p implies n
+1 in dom p & p.(n+1) in rng p
proof
let n be Nat, p be FinSequence;
A1: n+1 >= 0+1 by XREAL_1:7;
assume n < len p;
then n+1 <= len p by NAT_1:13;
then n+1 in dom p by A1,FINSEQ_3:25;
hence thesis by FUNCT_1:def 3;
end;
Lm4: now
let p be FinSequence;
let x be set;
assume x in rng p;
then consider y being object such that
A1: y in dom p and
A2: x = p.y by FUNCT_1:def 3;
ex k being Nat st y = k+1 & k < len p by A1,Lm1;
hence ex k being Nat st k < len p & x = p.(k+1) by A2;
end;
theorem Th1:
for t being DecoratedTree holds t|<*>NAT = t
proof
let t be DecoratedTree;
A1: dom (t|<*>NAT) = (dom t)|<*>NAT by TREES_2:def 10;
now
let p be FinSequence of NAT;
assume p in dom (t|<*>NAT);
hence (t|<*>NAT).p = t.({}^p) by A1,TREES_2:def 10
.= t.p by FINSEQ_1:34;
end;
hence thesis by A1,TREES_1:31;
end;
theorem Th2:
for t being Tree, p,q being FinSequence of NAT st p^q in t holds
t|(p^q) = (t|p)|q
proof
let t be Tree, p,q be FinSequence of NAT;
assume
A1: p^q in t;
let r be FinSequence of NAT;
A2: p in t by A1,TREES_1:21;
then q in t|p by A1,TREES_1:def 6;
then
A3: r in (t|p)|q iff q^r in t|p by TREES_1:def 6;
A4: p^q^r = p^(q^r) by FINSEQ_1:32;
r in t|(p^q) iff p^q^r in t by A1,TREES_1:def 6;
hence thesis by A2,A4,A3,TREES_1:def 6;
end;
theorem Th3:
for t being DecoratedTree, p,q being FinSequence of NAT st p^q in
dom t holds t|(p^q) = (t|p)|q
proof
let t be DecoratedTree, p,q be FinSequence of NAT;
A1: dom (t|p) = (dom t)|p by TREES_2:def 10;
A2: dom (t|(p^q)) = (dom t)|(p^q) by TREES_2:def 10;
assume
A3: p^q in dom t;
then
A4: p in dom t by TREES_1:21;
then
A5: q in (dom t)|p by A3,TREES_1:def 6;
A6: now
let a be FinSequence of NAT;
A7: p^q^a = p^(q^a) by FINSEQ_1:32;
assume
A8: a in dom (t|(p^q));
then p^q^a in dom t by A3,A2,TREES_1:def 6;
then
A9: q^a in (dom t)|p by A4,A7,TREES_1:def 6;
then
A10: a in ((dom t)|p)|q by A5,TREES_1:def 6;
thus (t|(p^q)).a = t.(p^q^a) by A2,A8,TREES_2:def 10
.= (t|p).(q^a) by A7,A9,TREES_2:def 10
.= ((t|p)|q).a by A1,A10,TREES_2:def 10;
end;
dom ((t|p)|q) = (dom (t|p))|q by TREES_2:def 10;
hence thesis by A3,A1,A2,A6,Th2;
end;
notation
let IT be DecoratedTree;
synonym IT is root↑ for IT is trivial;
end;
definition
let IT be DecoratedTree;
redefine attr IT is root means :: redefines root (TREES_9, synonym) → trivial (SUBSET_1, redefinition) → trivial (ZFMISC_1, definition)
dom IT = elementary_tree 0;
compatibility
proof
thus IT is root implies dom IT = elementary_tree 0
proof
dom IT is not empty;
then
A1: IT is not empty;
assume IT is root;
then consider x being object such that
A2: IT = {x} by A1,ZFMISC_1:131;
x in IT by A2,TARSKI:def 1;
then consider x1,x2 being object such that
A3: x = [x1,x2] by RELAT_1:def 1;
{} in dom IT & dom IT = {x1} by A2,A3,RELAT_1:9,TREES_1:22;
hence dom IT = elementary_tree 0 by TARSKI:def 1,TREES_1:29;
end;
thus thesis by TREES_1:29;
end;
end;
theorem Th4:
for t being DecoratedTree holds t is root iff {} in Leaves dom t
proof
let t be DecoratedTree;
reconsider e = {} as Node of t by TREES_1:22;
hereby
assume t is root;
then dom t = elementary_tree 0;
then not e^<*0*> in dom t by TARSKI:def 1,TREES_1:29;
hence {} in Leaves dom t by TREES_1:54;
end;
assume
A1: {} in Leaves dom t;
let p be FinSequence of NAT;
hereby
assume that
A2: p in dom t and
A3: not p in elementary_tree 0;
p <> {} by A3,TARSKI:def 1,TREES_1:29;
then consider q being FinSequence of NAT,
n being Element of NAT such that
A4: p = <*n*>^q by FINSEQ_2:130;
A5: e^<*n*> = <*n*> by FINSEQ_1:34;
<*n*> in dom t by A2,A4,TREES_1:21;
hence contradiction by A1,A5,TREES_1:55;
end;
assume p in elementary_tree 0;
then p = {} by TARSKI:def 1,TREES_1:29;
hence thesis by TREES_1:22;
end;
theorem Th5:
for t being Tree, p being Element of t holds t|p =
elementary_tree 0 iff p in Leaves t
proof
let t be Tree, p be Element of t;
A1: not <*0*> in elementary_tree 0 by TARSKI:def 1,TREES_1:29;
hereby
assume t|p = elementary_tree 0;
then not p^<*0*> in t by A1,TREES_1:def 6;
hence p in Leaves t by TREES_1:54;
end;
assume
A2: p in Leaves t;
let q be FinSequence of NAT;
hereby
assume q in t|p;
then p^q in t by TREES_1:def 6;
then
A3: not p is_a_proper_prefix_of p^q by A2,TREES_1:def 5;
p is_a_prefix_of p^q by TREES_1:1;
then p^q = p by A3
.= p^{} by FINSEQ_1:34;
then q = {} by FINSEQ_1:33;
hence q in elementary_tree 0 by TREES_1:22;
end;
assume q in elementary_tree 0;
then q = {} by TARSKI:def 1,TREES_1:29;
hence thesis by TREES_1:22;
end;
theorem
for t being DecoratedTree, p being Node of t holds t|p is root iff p
in Leaves dom t
proof
let t be DecoratedTree, p be Node of t;
A1: dom (t|p) = (dom t)|p by TREES_2:def 10;
thus thesis by A1,Th5;
end;
registration
cluster root for DecoratedTree;
existence
proof
take t = root-tree 0;
thus dom t = elementary_tree 0 by TREES_4:3;
end;
cluster finite non root for DecoratedTree;
existence
proof
take t = 0-tree root-tree 0;
dom t = ^dom root-tree 0 by TREES_4:13
.= elementary_tree 1 by TREES_3:67,TREES_4:3;
hence t is finite by FINSET_1:10;
assume dom t = elementary_tree 0;
then root-tree (t.{}) = t by TREES_4:5
.= 0-tree <*root-tree 0*>;
hence contradiction by TREES_4:17;
end;
end;
registration
let x be object;
cluster root-tree x -> finite root;
coherence
by TREES_4:3;
end;
definition
let IT be Tree;
attr IT is finite-branching means
:Def2:
for x being Element of IT holds succ x is finite;
end;
registration
cluster finite-order -> finite-branching for Tree;
coherence;
end;
definition
let IT be DecoratedTree;
attr IT is finite-order means
:Def3:
dom IT is finite-order;
attr IT is finite-branching means
:Def4:
dom IT is finite-branching;
end;
registration
cluster finite -> finite-order for DecoratedTree;
coherence;
cluster finite-order -> finite-branching for DecoratedTree;
coherence;
end;
registration
let t be finite-order DecoratedTree;
cluster dom t -> finite-order;
coherence by Def3;
end;
registration
let t be finite-branching DecoratedTree;
cluster dom t -> finite-branching;
coherence by Def4;
end;
registration
let t be finite-branching Tree;
let p be Element of t;
cluster succ p -> finite;
coherence by Def2;
end;
scheme
FinOrdSet{f(object) -> set, X() -> finite set}:
for n being Nat holds f(n) in X() iff n < card X()
provided
A1: for x being set st x in X() ex n being Nat st x = f(n) and
A2: for i,j being Nat st i < j & f(j) in X() holds f(i) in X( ) and
A3: for i,j being Nat st f(i) = f(j) holds i = j
proof
consider f being Function such that
A4: dom f = card X() & for x being object st x in card X() holds f.x = f(x
) from FUNCT_1:sch 3;
defpred X[Nat] means $1 < card X() implies f($1) in X();
A5: for n being Nat st X[n] holds X[n+1]
proof
let n be Nat such that
A6: n < card X() implies f(n) in X() and
A7: n+1 < card X() and
A8: not f(n+1) in X();
consider f being Function such that
A9: dom f = n+1 & for x being object st x in n+1 holds f.x = f(x) from
FUNCT_1:sch 3;
A10: n+1 = {k where k is Nat: k < n+1} by AXIOMS:4;
A11: n <= n+1 by NAT_1:11;
A12: rng f = X()
proof
hereby
let x be object;
assume x in rng f;
then consider y being object such that
A13: y in n+1 and
A14: x = f.y by A9,FUNCT_1:def 3;
consider k being Nat such that
A15: y = k and
A16: k < n+1 by A10,A13;
reconsider k as Nat;
k <= n by A16,NAT_1:13;
then k = n or k < n by XXREAL_0:1;
then f(k) in X() by A2,A6,A7,A11,XXREAL_0:2;
hence x in X() by A9,A13,A14,A15;
end;
let x be object;
assume
A17: x in X();
then consider k being Nat such that
A18: x = f(k) by A1;
now
assume k >= n+1;
then k = n+1 or k > n+1 by XXREAL_0:1;
hence contradiction by A2,A8,A17,A18;
end;
then
A19: k in n+1 by A10;
then x = f.k by A9,A18;
hence thesis by A9,A19,FUNCT_1:def 3;
end;
f is one-to-one
proof
let x1,x2 be object;
assume that
A20: x1 in dom f and
A21: x2 in dom f and
A22: f.x1 = f.x2;
( ex k being Nat st x1 = k & k < n+1)&
ex k being Nat st x2 = k & k < n+1 by A9,A10,A20,A21;
then
A23: f(x1) = f(x2) implies x1 = x2 by A3;
f(x1) = f.x1 by A9,A20;
hence thesis by A9,A21,A22,A23;
end;
then n+1,X() are_equipotent by A9,A12,WELLORD2:def 4;
hence thesis by A7,CARD_1:def 2;
end;
A24: card X() = {n where n is Nat: n < card X()} by AXIOMS:4;
f is one-to-one
proof
let x1,x2 be object;
assume that
A25: x1 in dom f and
A26: x2 in dom f;
( ex k being Nat st x1 = k & k < card X())&
ex k being Nat st x2 = k & k < card X() by A4,A24,A25,A26;
then
A27: f(x1) = f(x2) implies x1 = x2 by A3;
f(x1) = f.x1 by A4,A25;
hence thesis by A4,A26,A27;
end;
then
A28: dom f,rng f are_equipotent by WELLORD2:def 4;
then reconsider Y = rng f as finite set by A4,CARD_1:38;
A29: card rng f = card card X() by A4,A28,CARD_1:5
.= card X();
A30: now
given i being Nat such that
A31: i >= card X() and
A32: f(i) in X();
card X() < i or card X() = i by A31,XXREAL_0:1;
then
A33: f(card X()) in X() by A2,A32;
rng f c= X() \ {f(card X())}
proof
let x be object;
assume x in rng f;
then consider y being object such that
A34: y in card X() and
A35: x = f.y by A4,FUNCT_1:def 3;
consider k being Nat such that
A36: y = k and
A37: k < card X() by A24,A34;
A38: f(k) = x by A4,A34,A35,A36;
A39: now
assume x in {f(card X())};
then f(k) = f(card X()) by A38,TARSKI:def 1;
hence contradiction by A3,A37;
end;
f(k) in X() by A2,A33,A37;
hence thesis by A38,A39,XBOOLE_0:def 5;
end;
then
A40: card Y <= card ((X()) \ {f(card X())}) by NAT_1:43;
{f(card X())} c= X() by A33,ZFMISC_1:31;
then card Y <= (card X()) - card {f(card X())} by A40,CARD_2:44;
then card Y <= (card Y) - 1 by A29,CARD_2:42;
then card Y + 1 <= (card Y) - 1 + 1 by XREAL_1:7;
hence contradiction by NAT_1:13;
end;
A41: X[0]
proof
assume 0 < card X();
then reconsider X = X() as non empty set;
set x = the Element of X;
consider n being Nat such that
A42: x = f(n) by A1;
n = 0 or n > 0;
hence thesis by A2,A42;
end;
for n being Nat holds X[n] from NAT_1:sch 2(A41,A5);
hence thesis by A30;
end;
theorem Th7:
for t being finite-branching Tree, p being Element of t for n
being Nat holds p^<*n*> in succ p iff n < card succ p
proof
let t be finite-branching Tree, p be Element of t;
deffunc U(Nat) = p^<*$1*>;
A1: for x being set st x in succ p ex n being Nat st x = U(n)
proof
let x be set;
assume x in succ p;
then ex n being Nat st x = U(n) & U(n) in t;
hence thesis;
end;
A2: for i,j being Nat st i < j & U(j) in succ p holds U(i) in succ p
proof
let i,j be Nat;
assume
A3: i < j & p^<*j*> in succ p;
reconsider i,j as Nat;
p^<*i*> in t by A3,TREES_1:def 3;
hence thesis;
end;
A4: for i,j being Nat st U(i) = U(j) holds i = j
proof
let i,j be Nat;
assume p^<*i*> = p^<*j*>;
hence i = (p^<*j*>).(len p+1) by FINSEQ_1:42
.= j by FINSEQ_1:42;
end;
thus for n being Nat holds U(n) in succ p iff n < card succ p
from FinOrdSet(A1,A2,A4);
end;
definition
let t be finite-branching Tree;
let p be Element of t;
func p succ -> one-to-one FinSequence of t means
: Def5:
len it = card succ
p & rng it = succ p & for i being Nat st i < len it holds it.(i+1) =
p^<*i*>;
existence
proof
deffunc U(Nat) = p^<*$1-1*>;
consider q being FinSequence such that
A1: len q = card succ p & for i being Nat st i in dom q holds q.i = U(
i) from FINSEQ_1:sch 2;
A2: q is one-to-one
proof
let x1,x2 be object;
assume
A3: x1 in dom q & x2 in dom q;
then reconsider i1 = x1, i2 = x2 as Nat;
A4: (p^<*i1-1*>).(len p+1) = i1-1 & (p^<*i2-1*>).(len p+1) = i2-1 by
FINSEQ_1:42;
q.x1 = p^<*i1-1*> & q.x2 = p^<*i2-1*> by A1,A3;
hence thesis by A4;
end;
A5: for i being Nat st i < len q holds q.(i+1) = p^<*i*>
proof
let i be Nat;
assume i < len q;
then q.(i+1) = p^<*i+1-1*> by A1,Lm3;
hence thesis;
end;
A6: rng q c= succ p
proof
let x be object;
assume x in rng q;
then consider k being Nat such that
A7: k < len q and
A8: x = q.(k+1) by Lm4;
x = p^<*k*> by A5,A7,A8;
hence thesis by A1,A7,Th7;
end;
then reconsider q as one-to-one FinSequence of succ p by A2,FINSEQ_1:def 4;
take q;
thus len q = card succ p & rng q c= succ p by A1,A6;
thus succ p c= rng q
proof
let x be object;
assume
A9: x in succ p;
then consider n being Nat such that
A10: x = p^<*n*> and
p^<*n*> in t;
A11: n < card succ p by A9,A10,Th7;
then q.(n+1) = x by A1,A5,A10;
hence thesis by A1,A11,Lm3;
end;
thus thesis by A5;
end;
uniqueness
proof
let q1, q2 be one-to-one FinSequence of t such that
A12: len q1 = card succ p and
rng q1 = succ p and
A13: for i being Nat st i < len q1 holds q1.(i+1) = p^<*i*> and
A14: len q2 = card succ p and
rng q2 = succ p and
A15: for i being Nat st i < len q2 holds q2.(i+1) = p^<*i*>;
A16: dom q1 = Seg card succ p by A12,FINSEQ_1:def 3;
A17: now
let k be Nat;
assume k in Seg card succ p;
then consider n being Nat such that
A18: k = n+1 & n < len q1 by A16,Lm1;
thus q1.k = p^<*n*> by A13,A18
.= q2.k by A12,A14,A15,A18;
end;
dom q2 = Seg card succ p by A14,FINSEQ_1:def 3;
hence thesis by A16,A17;
end;
end;
definition
let t be finite-branching DecoratedTree;
let p be FinSequence such that
A1: p in dom t;
func succ(t,p) -> FinSequence means
: Def6:
ex q being Element of dom t st q = p & it = t*(q succ);
existence
proof
reconsider q = p as Element of dom t by A1;
rng (q succ) c= dom t;
then dom (t*(q succ)) = dom (q succ) by RELAT_1:27
.= Seg len (q succ) by FINSEQ_1:def 3;
then t*(q succ) is FinSequence by FINSEQ_1:def 2;
hence thesis;
end;
uniqueness;
end;
theorem Th8:
for t being finite-branching DecoratedTree ex x being set, p
being DTree-yielding FinSequence st t = x-tree p
proof
let t be finite-branching DecoratedTree;
take t.{};
reconsider e = {} as Node of t by TREES_1:22;
defpred X[object,object] means
ex n being Element of NAT st n+1 = $1 & $2 = t|<*n*>;
(dom t)-level 1 = succ e by TREES_2:13;
then reconsider A = (dom t)-level 1 as finite set;
reconsider e = {} as Element of dom t by TREES_1:22;
A1: for z being object st z in Seg card A ex u being object st X[z,u]
proof
let z be object;
assume
A2: z in Seg card A;
then reconsider m = z as Nat;
m >= 1 by A2,FINSEQ_1:1;
then consider n being Nat such that
A3: m = 1+n by NAT_1:10;
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider y = t|<*n*> as set;
take y, n;
thus thesis by A3;
end;
consider p being Function such that
A4: dom p = Seg card A and
A5: for z being object st z in Seg card A holds X[z,p.z]
from CLASSES1:sch
1( A1);
reconsider p as FinSequence by A4,FINSEQ_1:def 2;
A6: len p = card A by A4,FINSEQ_1:def 3;
A7: now
let x be object;
assume x in dom p;
then ex n being Element of NAT st n+1 = x & p.x = t|<*n*> by A4,A5;
hence p.x is DecoratedTree;
end;
A8: now
let n be Nat;
thus e^<*n*> = <*n*> & succ e = A by FINSEQ_1:34,TREES_2:13;
hence <*n*> in A iff n < card A by Th7;
end;
reconsider p as DTree-yielding FinSequence by A7,TREES_3:24;
A9: len doms p = len p by TREES_3:38;
now
let x be object;
hereby
assume that
A10: x in dom t and
A11: x <> {};
reconsider r = x as Node of t by A10;
consider q being FinSequence of NAT,
n being Element of NAT such that
A12: r = <*n*>^q by A11,FINSEQ_2:130;
A13: <*n*> in dom t by A12,TREES_1:21;
reconsider q as FinSequence;
reconsider nn=n as Nat;
take nn, q;
e^<*n*> = <*n*> by A8;
then <*n*> in A by A8,A13;
hence nn < len doms p by A6,A8,A9;
then
n+1 in dom p & ex k being Element of NAT st k+1 = n+1 & p.(n+1) = t
|<*k *> by A4,A5,A9,Lm3;
then (doms p).(n+1) = dom (t|<*n*>) by FUNCT_6:22
.= (dom t)|<*n*> by TREES_2:def 10;
hence q in (doms p).(nn+1) & x = <*nn*>^q by A12,A13,TREES_1:def 6;
end;
assume
A14: x = {} or ex n being Nat, q being FinSequence st n <
len doms p & q in (doms p).(n+1) & x = <*n*>^q;
assume
A15: not x in dom t;
then consider n being Nat, q being FinSequence such that
A16: n < len doms p and
A17: q in (doms p).(n+1) and
A18: x = <*n*>^q by A14,TREES_1:22;
reconsider n as Element of NAT by ORDINAL1:def 12;
n+1 in dom p & ex k being Element of NAT st k+1 = n+1 & p.(n+1) = t|
<*k *> by A4,A5,A9,A16,Lm3;
then (doms p).(n+1) = dom (t|<*n*>) by FUNCT_6:22
.= (dom t)|<*n*> by TREES_2:def 10;
then reconsider q as Element of (dom t)|<*n*> by A17;
<*n*> in A by A6,A8,A9,A16;
then <*n*>^q in dom t by TREES_1:def 6;
hence contradiction by A15,A18;
end;
then
A19: dom t = tree doms p by TREES_3:def 15;
take p;
now
let n be Nat;
assume n < len p;
then ex m being Element of NAT st m+1 = n+1 & p.(n+1) = t|<*m *>
by A4,A5,Lm3;
hence t|<*n*> = p.(n+1);
end;
hence thesis by A19,TREES_4:def 4;
end;
registration
let t be finite DecoratedTree;
let p be Node of t;
cluster t|p -> finite;
coherence;
end;
theorem Th9:
for t being finite Tree, p being Element of t st t = t|p holds p = {}
proof
let t be finite Tree, p be Element of t;
p <> {} implies height t > height (t|p) by TREES_1:48;
hence thesis;
end;
registration
let D be non empty set;
let S be non empty Subset of FinTrees D;
cluster -> finite for Element of S;
coherence;
end;
begin :: Set of subtrees of decorated tree
definition
let t be DecoratedTree;
func Subtrees t -> set equals
the set of all t|p where p is Node of t;
coherence;
end;
registration
let t be DecoratedTree;
cluster Subtrees t -> constituted-DTrees non empty;
coherence
proof
set p0 = the Node of t;
set S = the set of all t|p where p is Node of t;
t|p0 in S;
then reconsider S as non empty set;
S is constituted-DTrees
proof
let x be object;
assume x in S;
then ex p being Node of t st x = t|p;
hence thesis;
end;
hence thesis;
end;
end;
definition
let D be non empty set;
let t be DecoratedTree of D;
redefine func Subtrees t -> non empty Subset of Trees D; :: redefines Subtrees (TREES_9, definition)
coherence
proof
Subtrees t c= Trees D
proof
let x be object;
assume x in Subtrees t;
then ex p being Node of t st x = t|p;
hence thesis by TREES_3:def 7;
end;
hence thesis;
end;
end;
definition
let D be non empty set;
let t be finite DecoratedTree of D;
redefine func Subtrees t -> non empty Subset of FinTrees D; :: redefines Subtrees (TREES_9, definition)
coherence
proof
Subtrees t c= FinTrees D
proof
let x be object;
assume x in Subtrees t;
then ex p being Node of t st x = (t qua DecoratedTree of D)|p;
then reconsider x as finite DecoratedTree of D;
dom x is finite;
hence thesis by TREES_3:def 8;
end;
hence thesis;
end;
end;
registration
let t be finite DecoratedTree;
cluster -> finite for Element of Subtrees t;
coherence
proof
let x be Element of Subtrees t;
x in the set of all t|p where p is Node of t;
then ex p being Node of t st x = t|p;
hence thesis;
end;
end;
reserve x for set,
t,t1,t2 for DecoratedTree;
theorem Th10:
x in Subtrees t iff ex n being Node of t st x = t|n;
theorem Th11:
t in Subtrees t
proof
reconsider e = {} as Node of t by TREES_1:22;
t|e = t by Th1;
hence thesis;
end;
theorem
t1 is finite & Subtrees t1 = Subtrees t2 implies t1 = t2
proof
assume that
A1: t1 is finite and
A2: Subtrees t1 = Subtrees t2;
reconsider t = t1 as finite DecoratedTree by A1;
t1 in Subtrees t2 by A2,Th11;
then consider n being Node of t2 such that
A3: t1 = t2|n;
t2 in Subtrees t1 by A2,Th11;
then consider m being Node of t1 such that
A4: t2 = t1|m;
dom (t1|m) = (dom t1)|m by TREES_2:def 10;
then reconsider p = m^n as Element of dom t by A4,TREES_1:def 6;
t = t|p by A3,A4,Th3;
then dom t = (dom t)|p by TREES_2:def 10;
then n = {} by Th9;
hence thesis by A3,Th1;
end;
theorem
for n being Node of t holds Subtrees (t|n) c= Subtrees t
proof
let n be Node of t;
let x be object;
assume x in Subtrees (t|n);
then consider p being Node of t|n such that
A1: x = (t|n)|p;
dom (t|n) = (dom t)|n by TREES_2:def 10;
then reconsider q = n^p as Node of t by TREES_1:def 6;
x = t|q by A1,Th3;
hence thesis;
end;
definition
let t be DecoratedTree;
func FixedSubtrees t -> Subset of [:dom t, Subtrees t:] equals
the set of all [p,t|p]
where p is Node of t;
coherence
proof
set S = the set of all [p,t|p] where p is Node of t;
S c= [:dom t, Subtrees t:]
proof
let x be object;
assume x in S;
then consider p being Node of t such that
A1: x = [p,t|p];
t|p in Subtrees t;
hence thesis by A1,ZFMISC_1:87;
end;
hence thesis;
end;
end;
registration
let t be DecoratedTree;
cluster FixedSubtrees t -> non empty;
coherence
proof
set p0 = the Node of t;
set S = the set of all [p,t|p] where p is Node of t;
[p0,t|p0] in S;
hence thesis;
end;
end;
theorem
x in FixedSubtrees t iff ex n being Node of t st x = [n,t|n];
theorem Th15:
[{},t] in FixedSubtrees t
proof
reconsider e = {} as Node of t by TREES_1:22;
t|e = t by Th1;
hence thesis;
end;
theorem
FixedSubtrees t1 = FixedSubtrees t2 implies t1 = t2
proof
assume FixedSubtrees t1 = FixedSubtrees t2;
then [{},t1] in FixedSubtrees t2 by Th15;
then consider n being Node of t2 such that
A1: [{},t1] = [n,t2|n];
{} = n & t1 = t2|n by A1,XTUPLE_0:1;
hence thesis by Th1;
end;
definition
let t be DecoratedTree;
let C be set;
func C-Subtrees t -> Subset of Subtrees t equals
{t|p where p is Node of t:
not p in Leaves dom t or t.p in C};
coherence
proof
set W = {t|p where p is Node of t: not p in Leaves dom t or t.p in C};
W c= Subtrees t
proof
let x be object;
assume x in W;
then
ex p being Node of t st x = t|p & (not p in Leaves dom t or t.p in C );
hence thesis;
end;
hence thesis;
end;
end;
reserve C for set;
theorem Th17:
x in C-Subtrees t iff ex n being Node of t st x = t|n & (not n
in Leaves dom t or t.n in C);
theorem
C-Subtrees t is empty iff t is root & not t.{} in C
proof
reconsider e = {} as Node of t by TREES_1:22;
hereby
assume C-Subtrees t is empty;
then
A1: not t|e in C-Subtrees t;
then e in Leaves dom t;
hence t is root & not t.{} in C by A1,Th4;
end;
assume that
A2: t is root and
A3: not t.{} in C;
assume C-Subtrees t is not empty;
then reconsider S = C-Subtrees t as non empty Subset of Subtrees t;
set s = the Element of S;
consider n being Node of t such that
s = t|n and
A4: not n in Leaves dom t or t.n in C by Th17;
A5: dom t = {{}} by A2,TREES_1:29;
then n = {} by TARSKI:def 1;
then e^<*0*> in dom t by A3,A4,TREES_1:54;
hence contradiction by A5,TARSKI:def 1;
end;
definition
let t be finite DecoratedTree;
let C be set;
func C-ImmediateSubtrees t -> Function of C-Subtrees t, (Subtrees t)* means
for d being DecoratedTree st d in C-Subtrees t for p being FinSequence of
Subtrees t st p = it.d holds d = (d.{})-tree p;
existence
proof
defpred X[object,object] means
ex d being DecoratedTree, p being FinSequence of
Subtrees t st p = $2 & d = $1 & d = (d.{})-tree p;
A1: for x being object st x in C-Subtrees t
ex y being object st y in (Subtrees t)* & X[x, y]
proof
let x be object;
assume x in C-Subtrees t;
then reconsider s = x as Element of Subtrees t;
reconsider d = s as DecoratedTree;
consider sp being Node of t such that
A2: s = t|sp by Th10;
consider z being set, p being DTree-yielding FinSequence such that
A3: s = z-tree p by Th8;
rng p c= Subtrees t
proof
let x be object;
A4: dom (t|sp) = (dom t)|sp by TREES_2:def 10;
assume x in rng p;
then consider k being Nat such that
A5: k < len p & x = p.(k+1) by Lm4;
reconsider k as Element of NAT by ORDINAL1:def 12;
reconsider e = {} as Node of s|<*k*> by TREES_1:22;
A6: x = s|<*k*> by A3,A5,TREES_4:def 4;
<*k*>^e = <*k*> by FINSEQ_1:34;
then <*k*> in dom s by A3,A5,A6,TREES_4:11;
then reconsider q = sp^<*k*> as Node of t by A2,A4,TREES_1:def 6;
x = t|q by A2,A6,Th3;
hence thesis;
end;
then reconsider p as FinSequence of Subtrees t by FINSEQ_1:def 4;
reconsider y = p as set;
take y;
thus y in (Subtrees t)* by FINSEQ_1:def 11;
take d, p;
thus thesis by A3,TREES_4:def 4;
end;
consider f being Function such that
A7: dom f = C-Subtrees t & rng f c= (Subtrees t)* & for x being object
st x in C-Subtrees t holds X[x,f.x] from FUNCT_1:sch 6(A1);
reconsider f as Function of C-Subtrees t, (Subtrees t)* by A7,FUNCT_2:def 1
,RELSET_1:4;
take f;
let d be DecoratedTree;
assume d in C-Subtrees t;
then
ex d9 being DecoratedTree, p being FinSequence of Subtrees t st p = f
.d & d9 = d & d9 = (d9.{})-tree p by A7;
hence thesis;
end;
uniqueness
proof
let f1, f2 be Function of C-Subtrees t, (Subtrees t)* such that
A8: ( for d being DecoratedTree st d in C-Subtrees t for p being
FinSequence of Subtrees t st p = f1.d holds d = (d.{})-tree p)& for d being
DecoratedTree st d in C-Subtrees t for p being FinSequence of Subtrees t st p =
f2.d holds d = ( d.{})-tree p;
now
let x be object;
assume
A9: x in C-Subtrees t;
then reconsider s = x as Element of Subtrees t;
reconsider p1 = f1.s, p2 = f2.s as Element of (Subtrees t)* by A9,
FUNCT_2:5;
s = (s.{})-tree p1 & s = (s.{})-tree p2 by A8,A9;
hence f1.x = f2.x by TREES_4:15;
end;
hence f1 = f2 by FUNCT_2:12;
end;
end;
begin :: Set of subtrees of set of decorated tree
definition
let X be constituted-DTrees non empty set;
func Subtrees X -> set equals
the set of all t|p where t is Element of X, p is Node of t;
coherence;
end;
registration
let X be constituted-DTrees non empty set;
cluster Subtrees X -> constituted-DTrees non empty;
coherence
proof
set S = the set of all t|p where t is Element of X, p is Node of t;
set t = the Element of X,p0 = the Node of t;
t|p0 in S;
then reconsider S as non empty set;
S is constituted-DTrees
proof
let x be object;
assume x in S;
then ex t being Element of X, p being Node of t st x = t|p;
hence thesis;
end;
hence thesis;
end;
end;
definition
let D be non empty set;
let X be non empty Subset of Trees D;
redefine func Subtrees X -> non empty Subset of Trees D; :: redefines Subtrees (TREES_9, definition)
coherence
proof
Subtrees X c= Trees D
proof
let x be object;
assume x in Subtrees X;
then
ex t being Element of X, p being Node of t st x = (t qua Element of
Trees D)|p;
hence thesis by TREES_3:def 7;
end;
hence thesis;
end;
end;
definition
let D be non empty set;
let X be non empty Subset of FinTrees D;
redefine func Subtrees X -> non empty Subset of FinTrees D; :: redefines Subtrees (TREES_9, definition)
coherence
proof
Subtrees X c= FinTrees D
proof
let x be object;
assume x in Subtrees X;
then
ex t being Element of X, p being Node of t st x = ((t qua Element of
FinTrees D) qua DecoratedTree of D)|p;
then reconsider x as finite DecoratedTree of D;
dom x is finite;
hence thesis by TREES_3:def 8;
end;
hence thesis;
end;
end;
reserve X,Y for non empty constituted-DTrees set;
theorem Th19:
x in Subtrees X iff ex t being Element of X, n being Node of t st x = t|n;
theorem
t in X implies t in Subtrees X
proof
assume t in X;
then reconsider t as Element of X;
reconsider e = {} as Node of t by TREES_1:22;
t|e = t by Th1;
hence thesis;
end;
theorem
X c= Y implies Subtrees X c= Subtrees Y
proof
assume
A1: for x being object holds x in X implies x in Y;
let x be object;
assume x in Subtrees X;
then consider t being Element of X, p being Node of t such that
A2: x = t|p;
reconsider t as Element of Y by A1;
reconsider p as Node of t;
x = t|p by A2;
hence thesis;
end;
registration
let t be DecoratedTree;
cluster {t} -> constituted-DTrees;
coherence by TREES_3:14;
end;
theorem
Subtrees {t} = Subtrees t
proof
hereby
let x be object;
assume x in Subtrees {t};
then consider u being Element of {t}, p being Node of u such that
A1: x = u|p;
u = t by TARSKI:def 1;
hence x in Subtrees t by A1;
end;
let x be object;
assume x in Subtrees t;
then t in {t} & ex p being Node of t st x = t|p by TARSKI:def 1;
hence thesis;
end;
theorem
Subtrees X = union the set of all Subtrees t where t is Element of X
proof
hereby
let x be object;
assume x in Subtrees X;
then consider t being Element of X such that
A1: ex p being Node of t st x = t|p;
Subtrees t in the set of all Subtrees s where s is Element of X
& x in Subtrees t by A1;
hence
x in union the set of all Subtrees s where s is Element of X by
TARSKI:def 4;
end;
let x be object;
assume x in union the set of all Subtrees s where s is Element of X;
then consider Y being set such that
A2: x in Y and
A3: Y in the set of all Subtrees s where s is Element of X by
TARSKI:def 4;
consider t being Element of X such that
A4: Y = Subtrees t by A3;
ex p being Node of t st x = t|p by A2,A4;
hence thesis;
end;
definition
let X be constituted-DTrees non empty set;
let C be set;
func C-Subtrees X -> Subset of Subtrees X equals
{t|p where t is Element of
X, p is Node of t: not p in Leaves dom t or t.p in C};
coherence
proof
set W = {t|p where t is Element of X, p is Node of t: not p in Leaves dom
t or t.p in C};
W c= Subtrees X
proof
let x be object;
assume x in W;
then ex t being Element of X, p being Node of t st x = t|p & (not p in
Leaves dom t or t.p in C);
hence thesis;
end;
hence thesis;
end;
end;
theorem Th24:
x in C-Subtrees X iff ex t being Element of X, n being Node of t
st x = t|n & (not n in Leaves dom t or t.n in C);
theorem
C-Subtrees X is empty iff for t being Element of X holds t is root &
not t.{} in C
proof
hereby
assume
A1: C-Subtrees X is empty;
let t be Element of X;
reconsider e = {} as Node of t by TREES_1:22;
A2: not t|e in C-Subtrees X by A1;
then e in Leaves dom t;
hence t is root & not t.{} in C by A2,Th4;
end;
assume
A3: for t being Element of X holds t is root & not t.{} in C;
assume C-Subtrees X is not empty;
then reconsider S = C-Subtrees X as non empty Subset of Subtrees X;
set s = the Element of S;
consider t being Element of X, n being Node of t such that
s = t|n and
A4: not n in Leaves dom t or t.n in C by Th24;
reconsider e = {} as Node of t by TREES_1:22;
t is root by A3;
then
A5: dom t = {{}} by TREES_1:29;
then n = {} by TARSKI:def 1;
then e^<*0*> in dom t by A3,A4,TREES_1:54;
hence contradiction by A5,TARSKI:def 1;
end;
theorem
C-Subtrees {t} = C-Subtrees t
proof
hereby
let x be object;
assume x in C-Subtrees {t};
then consider u being Element of {t}, p being Node of u such that
A1: x = u|p &( not p in Leaves dom u or u.p in C);
u = t by TARSKI:def 1;
hence x in C-Subtrees t by A1;
end;
let x be object;
assume x in C-Subtrees t;
then
t in {t} & ex p being Node of t st x = t|p & (not p in Leaves dom t or t
.p in C) by TARSKI:def 1;
hence thesis;
end;
theorem
C-Subtrees X = union the set of all C-Subtrees t where t is Element of X
proof
hereby
let x be object;
assume x in C-Subtrees X;
then consider t being Element of X such that
A1: ex n being Node of t st x = t|n & (not n in Leaves dom t or t.n in C);
C-Subtrees t in the set of all C-Subtrees s where s is Element of X
& x in C-Subtrees t by A1;
hence x in union the set of all C-Subtrees s where s is Element of X
by TARSKI:def 4;
end;
let x be object;
assume x in union the set of all C-Subtrees s where s is Element of X;
then consider Y being set such that
A2: x in Y and
A3: Y in the set of all C-Subtrees s where s is Element of X by
TARSKI:def 4;
consider t being Element of X such that
A4: Y = C-Subtrees t by A3;
ex p being Node of t st x = t|p & (not p in Leaves dom t or t.p in C) by A2
,A4;
hence thesis;
end;
definition
let X be non empty constituted-DTrees set such that
A1: for t being Element of X holds t is finite;
let C be set;
func C-ImmediateSubtrees X -> Function of C-Subtrees X, (Subtrees X)* means
for d being DecoratedTree st d in C-Subtrees X for p being FinSequence of
Subtrees X st p = it.d holds d = (d.{})-tree p;
existence
proof
defpred X[object,object] means
ex d being DecoratedTree, p being FinSequence of
Subtrees X st p = $2 & d = $1 & d = (d.{})-tree p;
A2: for x being object st x in C-Subtrees X
ex y being object st y in (Subtrees X)* & X[x, y]
proof
let x be object;
assume x in C-Subtrees X;
then reconsider s = x as Element of Subtrees X;
reconsider d = s as DecoratedTree;
consider t being Element of X, sp being Node of t such that
A3: s = t|sp by Th19;
t is finite by A1;
then consider z being set, p being DTree-yielding FinSequence such that
A4: s = z-tree p by A3,Th8;
rng p c= Subtrees X
proof
let x be object;
A5: dom (t|sp) = (dom t)|sp by TREES_2:def 10;
assume x in rng p;
then consider k being Nat such that
A6: k < len p & x = p.(k+1) by Lm4;
reconsider k as Element of NAT by ORDINAL1:def 12;
reconsider e = {} as Node of s|<*k*> by TREES_1:22;
A7: x = s|<*k*> by A4,A6,TREES_4:def 4;
<*k*>^e = <*k*> by FINSEQ_1:34;
then <*k*> in dom s by A4,A6,A7,TREES_4:11;
then reconsider q = sp^<*k*> as Node of t by A3,A5,TREES_1:def 6;
x = t|q by A3,A7,Th3;
hence thesis;
end;
then reconsider p as FinSequence of Subtrees X by FINSEQ_1:def 4;
reconsider y = p as set;
take y;
thus y in (Subtrees X)* by FINSEQ_1:def 11;
take d, p;
thus thesis by A4,TREES_4:def 4;
end;
consider f being Function such that
A8: dom f = C-Subtrees X & rng f c= (Subtrees X)* & for x being object
st x in C-Subtrees X holds X[x,f.x] from FUNCT_1:sch 6(A2);
reconsider f as Function of C-Subtrees X, (Subtrees X)* by A8,FUNCT_2:def 1
,RELSET_1:4;
take f;
let d be DecoratedTree;
assume d in C-Subtrees X;
then
ex d9 being DecoratedTree, p being FinSequence of Subtrees X st p = f
.d & d9 = d & d9 = (d9.{})-tree p by A8;
hence thesis;
end;
uniqueness
proof
let f1, f2 be Function of C-Subtrees X, (Subtrees X)* such that
A9: ( for d being DecoratedTree st d in C-Subtrees X for p being
FinSequence of Subtrees X st p = f1.d holds d = (d.{})-tree p)& for d being
DecoratedTree st d in C-Subtrees X for p being FinSequence of Subtrees X st p =
f2.d holds d = ( d.{})-tree p;
now
let x be object;
assume
A10: x in C-Subtrees X;
then reconsider s = x as Element of Subtrees X;
reconsider p1 = f1.s, p2 = f2.s as Element of (Subtrees X)* by A10,
FUNCT_2:5;
s = (s.{})-tree p1 & s = (s.{})-tree p2 by A9,A10;
hence f1.x = f2.x by TREES_4:15;
end;
hence f1 = f2 by FUNCT_2:12;
end;
end;
registration
let t be Tree;
cluster empty for Element of t;
existence
proof
{} in t by TREES_1:22;
hence thesis;
end;
end;
theorem
for t being finite DecoratedTree, p being Element of dom t holds len
succ(t,p) = len (p succ) & dom succ(t,p) = dom (p succ)
proof
let t be finite DecoratedTree, p be Element of dom t;
( ex q being Element of dom t st q = p & succ(t,p) = t*(q succ))& rng (p
succ) c= dom t by Def6;
then dom succ(t,p) = dom (p succ) by RELAT_1:27;
hence thesis by FINSEQ_3:29;
end;
theorem Th29:
for p being FinTree-yielding FinSequence, n being empty Element
of tree p holds card succ n = len p
proof
let p be FinTree-yielding FinSequence, n be empty Element of tree p;
assume
A1: not thesis;
per cases by A1,XXREAL_0:1;
suppose
A2: card succ n < len p;
then (card succ n)+1 in dom p by Lm3;
then reconsider t = p.((card succ n)+1) as finite Tree by TREES_3:23;
A3: n^<*card succ n*> = <*card succ n*> by FINSEQ_1:34;
n in t & <*card succ n*>^n = <*card succ n*> by FINSEQ_1:34,TREES_1:22;
then n^<*card succ n*> in tree(p) by A2,A3,TREES_3:def 15;
then n^<*card succ n*> in succ n;
hence contradiction by Th7;
end;
suppose
card succ n > len p;
then n^<*len p*> in succ n by Th7;
then n^<*len p*> in tree(p);
then <*len p*> in tree(p) by FINSEQ_1:34;
then consider i being Nat, q being FinSequence such that
A4: i < len p and
q in p.(i+1) and
A5: <*len p*> = <*i*>^q by TREES_3:def 15;
len p = <*len p*>.1
.= i by A5,FINSEQ_1:41;
hence contradiction by A4;
end;
end;
theorem
for t being finite DecoratedTree, x being set, p being DTree-yielding
FinSequence st t = x-tree p for n being empty Element of dom t holds succ(t,n)
= roots p
proof
let t be finite DecoratedTree, x be set;
let p be DTree-yielding FinSequence such that
A1: t = x-tree p;
let n be empty Element of dom t;
A2: len doms p = len p by TREES_3:38;
now
let x be object;
assume x in dom doms p;
then consider i being Nat such that
A3: x = i+1 & i < len p by A2,Lm1;
reconsider i as Element of NAT by ORDINAL1:def 12;
A4: p.x = t|<*i*> by A1,A3,TREES_4:def 4;
n in dom (t|<*i*>) & <*i*>^n = <*i*> by FINSEQ_1:34,TREES_1:22;
then reconsider ii = <*i*> as Node of t by A1,A3,A4,TREES_4:11;
x in dom p by A3,Lm3;
then (doms p).x = dom (t|ii) by A4,FUNCT_6:22;
hence (doms p).x is finite Tree;
end;
then reconsider dp = doms p as FinTree-yielding FinSequence by TREES_3:23;
A5: dom t = tree dp by A1,TREES_4:10;
A6: ex q being Element of dom t st q = n & succ(t,n) = t*(q succ) by Def6;
rng (n succ) c= dom t;
then dom succ(t,n) = dom (n succ) by A6,RELAT_1:27;
then
A7: len succ(t,n) = len (n succ) by FINSEQ_3:29;
then
A8: len succ(t,n) = card succ n by Def5
.= len p by A2,A5,Th29;
A9: now
let i be Nat;
assume
A10: i < len p;
reconsider ii=i as Element of NAT by ORDINAL1:def 12;
i+1 in dom p by Lm3,A10;
then
A11: {} in (dom t)|<*ii*> & ex T being DecoratedTree st T = p.(i+1) & (
roots p).(i +1) = T.{} by TREES_1:22,TREES_3:def 18;
p.(i+1) = t|<*ii*> by A1,A10,TREES_4:def 4;
then
A12: (roots p).(i+1) = t.(<*i*>^{}) by A11,TREES_1:22,TREES_2:def 10;
i+1 in dom succ(t,n) by A8,A10,Lm3;
then succ(t,n).(i+1) = t.((n succ).(i+1)) by A6,FUNCT_1:12
.= t.(n^<*i*>) by A7,A8,A10,Def5
.= t.<*i*> by FINSEQ_1:34;
hence succ(t,n).(i+1) = (roots p).(i+1) by A12,FINSEQ_1:34;
end;
dom roots p = dom p by TREES_3:def 18;
then len roots p = len p by FINSEQ_3:29;
hence thesis by A8,A9,Lm2;
end;
registration
let T be finite-branching DecoratedTree, t being Node of T;
cluster T|t -> finite-branching;
coherence
proof
let x be Element of dom (T|t);
A1: dom (T|t) = (dom T) | t by TREES_2:def 10; then
x in (dom T) | t;then
reconsider tx = t^x as Element of dom T by TREES_1:def 6;
dom T = dom T with-replacement (t,(dom T)|t) by TREES_2:6;
then succ tx,succ x are_equipotent by A1,TREES_2:37;then
card succ x = card succ tx by CARD_1:5;
hence thesis;
end;
end;
theorem
for t being finite-branching DecoratedTree, p being Node of t,
q being Node of t|p holds succ(t,p^q) = succ(t|p,q)
proof
let t be finite-branching DecoratedTree, p be Node of t, q be Node of t|p;
A1: dom (t|p) = (dom t)|p by TREES_2:def 10;
then reconsider pq = p^q as Element of dom t by TREES_1:def 6;
reconsider q as Element of dom (t|p);
dom t = dom t with-replacement (p,(dom t)|p) by TREES_2:6;
then succ pq,succ q are_equipotent by A1,TREES_2:37;
then
A2: card succ q = card succ pq by CARD_1:5;
A3: ex r being Element of dom (t|p) st r = q & succ(t|p,q) = (t|p)*(r succ)
by Def6;
rng (q succ) c= dom (t|p);
then
A4: dom succ(t|p,q) = dom (q succ) by A3,RELAT_1:27;
A5: ex q being Element of dom t st q = pq & succ(t,pq) = t*(q succ) by Def6;
rng (pq succ) c= dom t;
then
A6: dom succ(t,pq) = dom (pq succ) by A5,RELAT_1:27;
A7: len (q succ) = card succ q by Def5;
A8: len (pq succ) = card succ pq by Def5;
then
A9: dom (pq succ) = dom (q succ) by A7,A2,FINSEQ_3:29;
now
let i be Nat;
assume
A10: i in dom (q succ);
then consider k being Nat such that
A11: i = k+1 and
A12: k < len (q succ) by Lm1;
A13: q^<*k*> in succ q by A7,A12,Th7;
reconsider k as Element of NAT by ORDINAL1:def 12;
thus succ(t,pq).i = t.((pq succ).i) by A5,A9,A6,A10,FUNCT_1:12
.= t.(pq^<*k*>) by A8,A7,A2,A11,A12,Def5
.= t.(p^(q^<*k*>)) by FINSEQ_1:32
.= (t|p).(q^<*k*>) by A1,A13,TREES_2:def 10
.= (t|p).((q succ).i) by A11,A12,Def5
.= succ(t|p,q).i by A3,A4,A10,FUNCT_1:12;
end;
hence thesis by A9,A6,A4;
end;
begin :: Moved from QC_LANG4, 2010.03.17, A.T
theorem Th32:
for n being Nat, r being FinSequence ex q being
FinSequence st q = r|Seg n & q is_a_prefix_of r
proof
let n be Nat, r be FinSequence;
r|Seg n is FinSequence by FINSEQ_1:15;
then consider q being FinSequence such that
A1: q = r|Seg n;
q is_a_prefix_of r by A1,TREES_1:def 1;
hence thesis by A1;
end;
theorem Th33:
for D being non empty set, r being FinSequence of D, r1,r2 being
FinSequence, k being Nat st k+1 <= len r & r1 = r|Seg (k+1) & r2 = r
|Seg k holds ex x being Element of D st r1 = r2^<*x*>
proof
let D be non empty set, r be FinSequence of D, r1,r2 be FinSequence, k be
Nat;
assume that
A1: k+1 <= len r and
A2: r1 = r|Seg (k+1) and
A3: r2 = r|Seg k;
k < len r by A1,NAT_1:13;
then
A4: len r2 = k by A3,FINSEQ_1:17;
r2 is_a_prefix_of r by A3,TREES_1:def 1;
then
A5: ex q2 being FinSequence st r = r2^q2 by TREES_1:1;
then reconsider r99 = r2 as FinSequence of D by FINSEQ_1:36;
r1 is_a_prefix_of r by A2,TREES_1:def 1;
then
A6: ex q1 being FinSequence st r = r1^q1 by TREES_1:1;
then reconsider r9 = r1 as FinSequence of D by FINSEQ_1:36;
A7: len r1 = k+1 by A1,A2,FINSEQ_1:17;
A8: now
assume r9 is_a_prefix_of r99;
then k+1 <= k+0 by A7,A4,NAT_1:43;
hence contradiction by XREAL_1:6;
end;
r9,r99 are_c=-comparable by A6,A5,TREES_A:1;
then r99 is_a_prefix_of r9 by A8;
then consider s being FinSequence such that
A9: r9 = r99^s by TREES_1:1;
reconsider s as FinSequence of D by A9,FINSEQ_1:36;
A10: len s = 1
proof
consider m being Nat such that
A11: m = len s;
k + 1 = k + m by A7,A4,A9,A11,FINSEQ_1:22;
hence thesis by A11;
end;
consider x being set such that
A12: x = s.1;
1 in {1} by TARSKI:def 1;
then 1 in dom s by A10,FINSEQ_1:2,def 3;
then
A13: x in rng s by A12,FUNCT_1:def 3;
s = <*x*> by A10,A12,FINSEQ_1:40;
hence thesis by A9,A13;
end;
theorem Th34:
for D being non empty set, r being FinSequence of D, r1 being
FinSequence st 1 <= len r & r1 = r|Seg 1 holds ex x being Element of D st r1 =
<*x*>
proof
let D be non empty set, r be FinSequence of D, r1 be FinSequence;
assume that
A1: 1 <= len r and
A2: r1 = r|Seg 1;
consider x being set such that
A3: x = r1.1;
1 in {1} by TARSKI:def 1;
then 1 in dom r1 by A1,A2,FINSEQ_1:2,17;
then
A4: x in rng r1 by A3,FUNCT_1:def 3;
len r1 = 1 by A1,A2,FINSEQ_1:17;
then
A5: r1 = <*x*> by A3,FINSEQ_1:40;
r1 is_a_prefix_of r by A2,TREES_1:def 1;
then ex q1 being FinSequence st r = r1^q1 by TREES_1:1;
then reconsider r9 = r1 as FinSequence of D by FINSEQ_1:36;
rng r9 c= D;
hence thesis by A5,A4;
end;
reserve T for DecoratedTree,
p for FinSequence of NAT;
theorem
T.p = (T|p).{}
proof
<*>NAT in (dom T)|p by TREES_1:22;
then (T|p).<*>NAT = T.(p^<*>NAT) by TREES_2:def 10
.= T.p by FINSEQ_1:34;
hence thesis;
end;
reserve T for finite-branching DecoratedTree,
t for Element of dom T,
x for FinSequence,
n, m for Nat;
theorem Th36:
succ(T,t) = T*(t succ)
proof
ex q being Element of dom T st q = t & succ(T,t) = T*(q succ) by Def6;
hence thesis;
end;
theorem Th37:
dom (T*(t succ)) = dom (t succ)
proof
rng (t succ) c= dom T;
hence thesis by RELAT_1:27;
end;
theorem Th38:
dom succ(T,t) = dom (t succ)
proof
thus dom succ(T,t) = dom (T*(t succ)) by Th36
.= dom (t succ) by Th37;
end;
theorem Th39:
t^<*n*> in dom T iff n+1 in dom (t succ)
proof
now
assume t^<*n*> in dom T;
then t^<*n*> in succ t;
then n < card succ t by Th7;
then n < len (t succ) by Def5;
then
A1: n+1 <= len (t succ) by NAT_1:13;
0+1 <= n+1 by XREAL_1:6;
then n+1 in Seg len (t succ) by A1,FINSEQ_1:1;
hence n+1 in dom (t succ) by FINSEQ_1:def 3;
end;
hence t^<*n*> in dom T implies n+1 in dom (t succ);
assume n+1 in dom (t succ);
then n+1 in Seg len (t succ) by FINSEQ_1:def 3;
then n+1 <= len (t succ) by FINSEQ_1:1;
then n < len (t succ) by NAT_1:13;
then n < card succ t by Def5;
then t^<*n*> in succ t by Th7;
hence thesis;
end;
theorem Th40:
for T, x, n st x^<*n*> in dom T holds T.(x^<*n*>) = succ(T,x).(n +1)
proof
let T, x, n;
assume
A1: x^<*n*> in dom T;
x is_a_prefix_of x^<*n*> by TREES_1:1;
then x in dom T by A1,TREES_1:20;
then consider q being Element of dom T such that
A2: q = x and
A3: succ(T,x) = T*(q succ) by Def6;
A4: n+1 in dom (q succ) by A1,A2,Th39;
then n+1 in Seg len (q succ) by FINSEQ_1:def 3;
then n+1 <= len (q succ) by FINSEQ_1:1;
then
A5: n < len (q succ) by NAT_1:13;
n+1 in dom (T*(q succ)) by A4,Th37;
then succ(T,x).(n+1) = T.((q succ).(n+1)) by A3,FUNCT_1:12
.= T.(x^<*n*>) by A2,A5,Def5;
hence thesis;
end;
reserve x, x9 for Element of dom T,
y9 for set;
theorem
x9 in succ x implies T.x9 in rng succ(T,x)
proof
assume x9 in succ x;
then consider n such that
A1: x9 = x^<*n*> and
x^<*n*> in dom T;
A2: T.x9 = (succ(T,x)).(n+1) by A1,Th40;
dom (succ(T,x)) = dom (T*(x succ)) by Th36
.= dom (x succ) by Th37;
then n+1 in dom succ(T,x) by A1,Th39;
hence thesis by A2,FUNCT_1:def 3;
end;
theorem
y9 in rng succ(T,x) implies ex x9 st y9 = T.x9 & x9 in succ x
proof
consider k be Nat such that
A1: dom succ(T,x) = Seg k by FINSEQ_1:def 2;
assume y9 in rng succ(T,x);
then consider n9 being object such that
A2: n9 in dom succ(T,x) and
A3: y9 = (succ(T,x)).n9 by FUNCT_1:def 3;
Seg k = { m where m is Nat : 1 <= m & m <= k } by FINSEQ_1:def 1;
then consider m9 being Nat such that
A4: n9 = m9 and
A5: 1 <= m9 and
m9 <= k by A2,A1;
m9 <> 0 by A5;
then consider n being Nat such that
A6: n+1 = m9 by NAT_1:6;
reconsider n as Nat;
n+1 in dom (x succ) by A2,A4,A6,Th38;
then x^<*n*> in dom T by Th39;
then consider x9 such that
A7: x9 = x^<*n*>;
A8: x9 in succ x by A7;
y9 = T.x9 by A3,A4,A6,A7,Th40;
hence thesis by A8;
end;
reserve n,k1,k2,l,k,m for Nat,
x,y for set;
scheme
ExDecTrees { D() -> non empty set, d() -> Element of D(), G(object) ->
FinSequence of D() }:
ex T being finite-branching DecoratedTree of D() st T.{}
= d() & for t being Element of dom T, w being Element of D() st w = T.t holds
succ(T,t) = G(w) proof
defpred P[object,object] means
(len G($1) = 0 & $2 = {}) or len G($1) <> 0 & ex m
st m+1 = len G($1) & $2 = {0} \/ Seg m;
A1: for x being object st x in D() ex y being object st P[x,y]
proof
let x be object such that
x in D();
per cases;
suppose
len G(x) = 0;
hence thesis;
end;
suppose
len G(x) <> 0;
then consider m being Nat such that
A2: m+1 = len G(x) by NAT_1:6;
reconsider m as Nat;
ex y st y = {0} \/ Seg m;
hence thesis by A2;
end;
end;
ex F being Function st dom F = D() &
for x being object st x in D() holds P[x,F.x]
from CLASSES1:sch 1(A1);
then consider F being Function such that
A3: for x being object
st x in D() holds len G(x) = 0 & F.x = {} or len G(x) <> 0 &
ex m st m+1 = len G(x) & F.x = {0} \/ Seg m;
deffunc F(set) = F.$1;
A4: for k,x st x in D() holds k in F(x) iff k+1 in Seg len G(x)
proof
let k,x such that
A5: x in D();
now
assume
A6: k in F(x);
then consider m such that
A7: m+1 = len G(x) and
A8: F.x = {0} \/ Seg m by A3,A5;
0 <= k & k <= m
proof
per cases by A6,A8,XBOOLE_0:def 3;
suppose
k in {0};
then k = 0 by TARSKI:def 1;
hence thesis;
end;
suppose
A9: k in Seg m;
thus thesis by A9,FINSEQ_1:1;
end;
end;
then 0+1 <= k+1 & k+1 <= m+1 by XREAL_1:6;
hence k+1 in Seg len G(x) by A7,FINSEQ_1:1;
end;
hence k in F(x) implies k+1 in Seg len G(x);
assume
A10: k+1 in Seg len G(x);
then len G(x) <> 0;
then consider m such that
A11: m+1 = len G(x) and
A12: F.x = {0} \/ Seg m by A3,A5;
k in {0} \/ Seg m
proof
per cases;
suppose
k = 0;
then k in {0} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
k <> 0;
then 0 < k;
then
A13: 0+1 <= k by NAT_1:13;
k+1 <= len G(x) by A10,FINSEQ_1:1;
then k <= m by A11,XREAL_1:6;
then k in Seg m by A13,FINSEQ_1:1;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis by A12;
end;
A14: for x being set, t being Element of dom T st x in D() holds { t^<*k*>:
k in F(x)} = { t^<*m*>: m+1 in Seg len G(x)}
proof
let x be set, t be Element of dom T such that
A15: x in D();
thus { t^<*k*>: k in F(x)} c= { t^<*m*>: m+1 in Seg len G(x)}
proof
let y be object;
assume y in { t^<*k*>: k in F(x)};
then consider k such that
A16: y = t^<*k*> and
A17: k in F(x);
k+1 in Seg len G(x) by A4,A15,A17;
hence thesis by A16;
end;
thus { t^<*m*>: m+1 in Seg len G(x)} c= { t^<*k*>: k in F(x)}
proof
let y be object;
assume y in { t^<*m*>: m+1 in Seg len G(x)};
then consider m such that
A18: y = t^<*m*> and
A19: m+1 in Seg len G(x);
m in F(x) by A4,A15,A19;
hence thesis by A18;
end;
end;
defpred P[set,set] means ex x,n st x in D() & $1 = [x,n] & (n in F(x) & $2 =
G(x).(n+1) or not n in F(x) & $2 = d());
A20: for c being Element of [:D(),NAT:] ex y being Element of D() st P[c,y]
proof
let c be Element of [:D(),NAT:];
c`1 in D() & c`2 in NAT by MCART_1:10;
then consider x being Element of D(), n being Nat such that
A21: x = c`1 & n = c`2;
A22: c = [x,n] by A21,MCART_1:21;
per cases;
suppose
A23: n in F(x);
then n+1 in Seg len G(x) by A4;
then n+1 in dom G(x) by FINSEQ_1:def 3;
then
A24: G(x).(n+1) in rng G(x) by FUNCT_1:def 3;
thus thesis by A22,A23,A24;
end;
suppose
not n in F(x);
hence thesis by A22;
end;
end;
ex S being Function of [:D(),NAT:],D() st for c being Element of [:D(),
NAT:] holds P[c,S.c] from FUNCT_2:sch 3(A20);
then consider S being Function of [: D(), NAT :],D() such that
A25: for c being Element of [: D(), NAT :] holds P[c,S.c];
A26: for n,x,m st m+1 = len G(x) & x in D() holds n in F(x) iff 0 <= n & n <= m
proof
let n,x,m such that
A27: m+1 = len G(x) and
A28: x in D();
thus n in F(x) implies 0 <= n & n <= m
proof
A29: ex k st k+1 = len G(x) & F(x) = {0} \/ Seg k by A3,A27,A28;
assume
A30: n in F(x);
per cases by A27,A30,A29,XBOOLE_0:def 3;
suppose
n in {0};
then n = 0 by TARSKI:def 1;
hence thesis;
end;
suppose
A31: n in Seg m;
thus thesis by A31,FINSEQ_1:1;
end;
end;
thus 0 <= n & n <= m implies n in F(x)
proof
assume that
0 <= n and
A32: n <= m;
A33: ex k st k+1 = len G(x) & F(x) = {0} \/ Seg k by A3,A27,A28;
per cases;
suppose
n = 0;
then n in {0} by TARSKI:def 1;
hence thesis by A33,XBOOLE_0:def 3;
end;
suppose
n <> 0;
then 0 < n;
then 0+1 <= n by NAT_1:13;
then n in Seg m by A32,FINSEQ_1:1;
hence thesis by A27,A33,XBOOLE_0:def 3;
end;
end;
end;
A34: for d being Element of D(), k1,k2 st k1 <= k2 & k2 in F(d) holds k1 in
F(d)
proof
let d be Element of D(), k1,k2;
assume that
A35: k1 <= k2 and
A36: k2 in F(d);
ex m st m+1 = len G(d) & F.d = {0} \/ Seg m by A3,A36;
then consider m such that
A37: m+1 = len G(d);
k2 <= m by A26,A36,A37;
then 0 <= k1 & k1 <= m by A35,XXREAL_0:2;
hence thesis by A26,A37;
end;
consider T being DecoratedTree of D() such that
A38: T.{} = d() & for t being Element of dom T holds succ t = { t^<*k*>:
k in F(T.t)} & for n st n in F(T.t) holds T.(t^<*n*>) = S.(T.t,n) from TREES_2:
sch 8(A34);
for t being Element of dom T holds succ t is finite
proof
let t be Element of dom T;
defpred P[set,object] means ex m st m+1 = $1 & $2 = t^<*m*>;
A39: for k be Nat st k in Seg len G(T.t) ex x being object st P[k,x]
proof
let k be Nat;
assume k in Seg len G(T.t);
then k <> 0 by FINSEQ_1:1;
then consider m being Nat such that
A40: m+1 = k by NAT_1:6;
reconsider m as Nat;
ex x st x = t^<*m*>;
hence thesis by A40;
end;
ex L being FinSequence st dom L = Seg len G(T.t) & for k be Nat st k
in Seg len G(T.t) holds P[k,L.k] from FINSEQ_1:sch 1(A39);
then consider L being FinSequence such that
A41: dom L = Seg len G(T.t) and
A42: for k be Nat st k in Seg len G(T.t) holds P[k,L.k];
A43: for k st 1 <= k+1 & k+1 <= len G(T.t) holds L.(k+1) = t^<*k*>
proof
let k;
assume 1 <= k+1 & k+1 <= len G(T.t);
then k+1 in Seg len G(T.t) by FINSEQ_1:1;
then ex m st m+1 = k+1 & L.(k+1) = t^<*m*> by A42;
hence thesis;
end;
A44: succ t = { t^<*k*>: k in F(T.t)} by A38;
succ t c= rng L
proof
let x be object;
assume x in succ t;
then consider k such that
A45: x = t^<*k*> and
A46: k in F(T.t) by A44;
A47: k+1 in Seg len G(T.t) by A4,A46;
then 1 <= k+1 & k+1 <= len G(T.t) by FINSEQ_1:1;
then L.(k+1) = t^<*k*> by A43;
hence thesis by A41,A45,A47,FUNCT_1:def 3;
end;
hence thesis;
end;
then dom T is finite-branching;
then reconsider T as finite-branching DecoratedTree of D() by Def4;
A48: for n, x st x in D() & n in F(x) holds S.(x,n) = G(x).(n+1)
proof
let n, x such that
A49: x in D() and
A50: n in F(x);
A51: n in NAT by ORDINAL1:def 12;
[x,n] in [: D(), NAT :] by A49,ZFMISC_1:def 2,A51;
then consider c being Element of [:D(),NAT:] such that
A52: c = [x,n];
consider x9 being set, n9 being Nat such that
x9 in D() and
A53: c = [x9,n9] and
A54: n9 in F(x9) & S.c = G(x9).(n9+1) or not n9 in F(x9) & S.c = d() by A25;
x9 = x by A52,A53,XTUPLE_0:1;
hence thesis by A50,A52,A53,A54,XTUPLE_0:1;
end;
now
let t be Element of dom T, w be Element of D() such that
A55: w = T . t;
succ t = { t^<*k*>: k in F(w)} by A38,A55;
then
A56: succ t = { t^<*k*>: k+1 in Seg len G(w)} by A14;
A57: dom G(w) = Seg len G(w) by FINSEQ_1:def 3;
A58: dom (t succ) = Seg len (t succ) by FINSEQ_1:def 3;
A59: dom (t succ) c= dom G(w)
proof
let n9 be object;
A60: Seg len (t succ) = { k where k is Nat : 1 <= k & k <= len (t succ)}
by FINSEQ_1:def 1;
assume n9 in dom (t succ);
then consider m being Nat such that
A61: n9 = m and
A62: 1 <= m and
A63: m <= len (t succ) by A58,A60;
0 <> m by A62;
then consider n being Nat such that
A64: m = n+1 by NAT_1:6;
reconsider n as Nat;
n+1 in dom (t succ) by A58,A60,A62,A63,A64;
then t^<*n*> in dom T by Th39;
then t^<*n*> in succ t;
then consider k such that
A65: t^<*k*> = t^<*n*> and
A66: k+1 in Seg len G(w) by A56;
<*k*> = <*n*> by A65,FINSEQ_1:33;
hence thesis by A57,A61,A64,A66,TREES_1:5;
end;
dom G(w) c= dom (t succ)
proof
let n9 be object;
A67: Seg len G(w) = { k where k is Nat : 1 <= k & k <= len G(w)}
by FINSEQ_1:def 1;
assume n9 in dom G(w);
then consider m being Nat such that
A68: n9 = m and
A69: 1 <= m and
A70: m <= len G(w) by A57,A67;
0 <> m by A69;
then consider n being Nat such that
A71: m = n+1 by NAT_1:6;
reconsider n as Nat;
n+1 in Seg len G(w) by A67,A69,A70,A71;
then t^<*n*> in succ t by A56;
hence thesis by A68,A71,Th39;
end;
then
A72: dom G(w) = dom (t succ) by A59;
then
A73: dom succ(T,t) = dom G(w) by Th38;
for m be Nat st m in dom succ(T,t) holds (succ(T,t)).m = G(w).m
proof
let m be Nat;
A74: Seg len G(w) = { k where k is Nat : 1 <= k & k <= len G(w)}
by FINSEQ_1:def 1;
assume
A75: m in dom succ(T,t);
then
A76: m in Seg len G(w) by A73,FINSEQ_1:def 3;
then len G(w) <> 0;
then consider l such that
A77: l+1 = len G(T.t) and
A78: F.(T.t) = {0} \/ Seg l by A3,A55;
consider k being Nat such that
A79: m = k and
A80: 1 <= k and
A81: k <= len G(w) by A76,A74;
0 <> k by A80;
then consider n being Nat such that
A82: m = n+1 by A79,NAT_1:6;
reconsider n as Nat;
A83: n <= l by A55,A79,A81,A82,A77,XREAL_1:6;
A84: n in {0} \/ Seg l
proof
per cases;
suppose
n = 0;
then n in {0} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
n <> 0;
then 0 < n;
then 0+1 <= n by NAT_1:13;
then n in Seg l by A83,FINSEQ_1:1;
hence thesis by XBOOLE_0:def 3;
end;
end;
n+1 in dom (t succ) by A75,A82,Th38;
then t^<*n*> in dom T by Th39;
then succ(T,t).(n+1) = T.(t^<*n*>) by Th40
.= S.(T.t,n) by A38,A78,A84
.= G(w).(n+1) by A48,A55,A78,A84;
hence thesis by A82;
end;
hence succ(T,t) = G(w) by A72,Th38;
end;
hence thesis by A38;
end;
theorem Th43:
for T being Tree, t being Element of T holds ProperPrefixes t is
finite Chain of T
proof
let T be Tree, t be Element of T;
ProperPrefixes t c= T & for p,q being FinSequence of NAT st p in
ProperPrefixes t & q in ProperPrefixes t holds p,q are_c=-comparable by
TREES_1:18,def 3;
hence thesis by TREES_2:def 3;
end;
theorem Th44:
for T being Tree holds T-level 0 = {{}}
proof
let T be Tree;
A1: {{}} c= { w where w is Element of T : len w = 0 }
proof
let x be object;
assume x in {{}};
then
A2: x = {} by TARSKI:def 1;
{} in T by TREES_1:22;
then consider t being Element of T such that
A3: t = {};
len t = 0 by A3;
hence thesis by A2,A3;
end;
{ w where w is Element of T : len w = 0 } c= {{}}
proof
let x be object;
assume x in { w where w is Element of T : len w = 0 };
then consider w being Element of T such that
A4: w = x and
A5: len w = 0;
w = {} by A5;
hence thesis by A4,TARSKI:def 1;
end;
hence thesis by A1;
end;
theorem Th45:
for T being Tree holds T-level (n+1) = union { succ w where w is
Element of T : len w = n }
proof
let T be Tree;
thus T-level (n+1) c= union { succ w where w is Element of T : len w = n }
proof
let x be object;
assume
A1: x in T-level (n+1);
then reconsider t = x as Element of T;
t|Seg n is FinSequence of NAT by FINSEQ_1:18;
then consider s being FinSequence of NAT such that
A2: s = t|Seg n;
s is_a_prefix_of t by A2,TREES_1:def 1;
then reconsider s as Element of T by TREES_1:20;
A3: ex w9 being Element of T st t = w9 & len w9 = n+1 by A1;
n+0 <= n+1 by XREAL_1:6;
then len s = n by A3,A2,FINSEQ_1:17;
then
A4: succ s in { succ w where w is Element of T : len w = n };
Seg (n+1) = dom t by A3,FINSEQ_1:def 3;
then t = t|Seg (n+1);
then ex m being Element of NAT st t = s^<*m*> by A3,A2,Th33;
then t in succ s;
hence thesis by A4,TARSKI:def 4;
end;
thus union { succ w where w is Element of T : len w = n } c= T-level (n+1)
proof
set X = { succ w where w is Element of T : len w = n };
let x be object;
assume x in union X;
then consider Y being set such that
A5: x in Y and
A6: Y in X by TARSKI:def 4;
consider w being Element of T such that
A7: Y = succ w and
A8: len w = n by A6;
reconsider t = x as Element of T by A5,A7;
consider k such that
A9: t = w^<*k*> and
w^<*k*> in T by A5,A7;
len <*k*> = 1 by FINSEQ_1:40;
then len t = n+1 by A8,A9,FINSEQ_1:22;
hence thesis;
end;
end;
theorem Th46:
for T being finite-branching Tree, n being Nat holds
T-level n is finite
proof
let T be finite-branching Tree;
defpred Q[Nat] means T-level $1 is finite;
A1: for n st Q[n] holds Q[n+1]
proof
let n such that
A2: T-level n is finite;
set X = { succ w where w is Element of T : len w = n };
A3: X is finite
proof
defpred P[object,object] means
ex w be Element of T st $1=w & $2=succ w;
A4: for x being object st x in T-level n ex y being object st P[x,y]
proof
let x be object;
assume x in T-level n;
then consider w being Element of T such that
A5: w = x;
consider y such that
A6: y = succ w;
take y,w;
thus thesis by A5,A6;
end;
consider f being Function such that
A7: dom f = T-level n &
for x being object st x in T-level n holds P[x,f.x] from
CLASSES1:sch 1(A4);
A8: X c= rng f
proof
let x be object;
assume x in X;
then consider w being Element of T such that
A9: x = succ w and
A10: len w = n;
A11: w in T-level n by A10;
then ex w9 being Element of T st w = w9 & f.w = succ w9 by A7;
hence thesis by A7,A9,A11,FUNCT_1:def 3;
end;
card rng f c= card dom f by CARD_1:12;
then rng f is finite by A2,A7;
hence thesis by A8;
end;
A12: for Y being set st Y in X holds Y is finite
proof
let Y be set;
assume Y in X;
then ex w being Element of T st Y = succ w & len w = n;
hence thesis;
end;
T-level (n+1) = union { succ w where w is Element of T : len w = n }
by Th45;
hence thesis by A3,A12,FINSET_1:7;
end;
A13: Q[0] by Th44;
thus for n holds Q[n] from NAT_1:sch 2(A13,A1);
end;
theorem Th47:
for T being finite-branching Tree holds T is finite iff ex n
being Nat st T-level n = {}
proof
let T be finite-branching Tree;
deffunc F(Nat) = T-level $1;
now
assume
A1: T is finite;
now
assume
A2: not ex n being Nat st T-level n = {};
A3: for n ex C being finite Chain of T st card C = n
proof
let n;
T-level n <> {} by A2;
then consider t being object such that
A4: t in T-level n by XBOOLE_0:def 1;
consider w being Element of T such that
t = w and
A5: len w = n by A4;
ProperPrefixes w is finite Chain of T by Th43;
then consider C being finite Chain of T such that
A6: C = ProperPrefixes w;
card C = n by A5,A6,TREES_1:35;
hence thesis;
end;
for t being Element of T holds succ t is finite;
then ex C being Chain of T st not C is finite by A3,TREES_2:29;
hence contradiction by A1;
end;
hence ex n being Nat st T-level n = {};
end;
hence T is finite implies ex n being Nat st T-level n = {};
given n such that
A7: T-level n = {};
set X = { F(m) where m is Nat : m <= n };
A8: T c= union X
proof
let x be object;
assume x in T;
then reconsider t = x as Element of T;
consider m such that
A9: m = len t;
A10: t in F(m) by A9;
len t < n
proof
consider q being FinSequence such that
A11: q = t|Seg n and
A12: q is_a_prefix_of t by Th32;
assume n <= len t;
then
A13: len q = n by A11,FINSEQ_1:17;
reconsider q as Element of T by A12,TREES_1:20;
q in T-level n by A13;
hence contradiction by A7;
end;
then F(m) in X by A9;
hence thesis by A10,TARSKI:def 4;
end;
A14: X is finite
proof
defpred P[set,object] means ex l,m st m = l+1 & $1 = m & F(l) = $2;
A15: for k be Nat st k in Seg(n+1) ex x being object st P[k,x]
proof
let k be Nat;
assume k in Seg(n+1);
then 0 <> k by FINSEQ_1:1;
then consider l being Nat such that
A16: k = l+1 by NAT_1:6;
reconsider l as Nat;
consider x such that
A17: x = F(l);
take x,l,l+1;
thus thesis by A16,A17;
end;
consider p being FinSequence such that
A18: dom p = Seg(n+1) & for k be Nat st k in Seg(n+1) holds P[k,p.k]
from FINSEQ_1:sch 1(A15);
A19: for k st k+1 in Seg (n+1) holds p.(k+1) = F(k)
proof
let k;
assume k+1 in Seg (n+1);
then ex l,m st m = l+1 & k+1 = m & F(l) = p.(k+1) by A18;
hence thesis;
end;
X c= rng p
proof
let y be object;
assume y in X;
then consider m such that
A20: y = F(m) and
A21: m <= n;
A22: 0+1 <= m+1 by XREAL_1:6;
m+1 <= n+1 by A21,XREAL_1:6;
then
A23: m+1 in Seg (n+1) by A22,FINSEQ_1:1;
then p.(m+1) = F(m) by A19;
hence thesis by A18,A20,A23,FUNCT_1:def 3;
end;
hence thesis;
end;
for Y being set st Y in X holds Y is finite
proof
let Y be set;
assume Y in X;
then ex m st Y = F(m) & m <= n;
hence thesis by Th46;
end;
then union X is finite by A14,FINSET_1:7;
hence thesis by A8;
end;
theorem Th48:
for T being finite-branching Tree st not T is finite ex C being
Chain of T st not C is finite
proof
let T be finite-branching Tree such that
A1: not T is finite;
A2: for n ex C being finite Chain of T st card C = n
proof
let n;
T-level n <> {} by A1,Th47;
then consider t being object such that
A3: t in T-level n by XBOOLE_0:def 1;
A4: ex w being Element of T st t = w & len w = n by A3;
reconsider t as Element of T by A3;
ProperPrefixes t is finite Chain of T by Th43;
then consider C being finite Chain of T such that
A5: C = ProperPrefixes t;
card C = n by A4,A5,TREES_1:35;
hence thesis;
end;
for t being Element of T holds succ t is finite;
hence thesis by A2,TREES_2:29;
end;
theorem Th49:
for T being finite-branching Tree st not T is finite ex B being
Branch of T st not B is finite
proof
let T be finite-branching Tree;
assume not T is finite;
then consider C being Chain of T such that
A1: not C is finite by Th48;
consider B being Branch of T such that
A2: C c= B by TREES_2:28;
not B is finite by A1,A2;
hence thesis;
end;
theorem Th50:
for T being Tree, C being Chain of T, t being Element of T st t
in C & not C is finite ex t9 being Element of T st t9 in C & t
is_a_proper_prefix_of t9
proof
let T be Tree, C be Chain of T, t be Element of T such that
A1: t in C and
A2: not C is finite;
now
assume
A3: not ex t9 being Element of T st t9 in C & t is_a_proper_prefix_of t9;
A4: for t9 being Element of T st t9 in C holds t9 is_a_prefix_of t
proof
let t9 be Element of T such that
A5: t9 in C;
now
assume
A6: not t9 is_a_prefix_of t;
t,t9 are_c=-comparable by A1,A5,TREES_2:def 3;
then t is_a_prefix_of t9 by A6;
then t is_a_proper_prefix_of t9 by A6;
hence contradiction by A3,A5;
end;
hence thesis;
end;
C c= ProperPrefixes t \/ {t}
proof
let x be object;
assume
A7: x in C;
then reconsider t9 = x as Element of T;
A8: t9 is_a_prefix_of t by A4,A7;
t9 in ProperPrefixes t \/ {t}
proof
per cases by A8;
suppose
t9 is_a_proper_prefix_of t;
then t9 in ProperPrefixes t by TREES_1:12;
hence thesis by XBOOLE_0:def 3;
end;
suppose
t9 = t;
then t9 in {t} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
hence contradiction by A2;
end;
hence thesis;
end;
theorem Th51:
for T being Tree, B being Branch of T, t being Element of T st t
in B & not B is finite ex t9 being Element of T st t9 in B & t9 in succ t
proof
let T be Tree, B be Branch of T, t be Element of T;
assume t in B & not B is finite;
then consider t99 being Element of T such that
A1: t99 in B and
A2: t is_a_proper_prefix_of t99 by Th50;
t is_a_prefix_of t99 by A2;
then consider r being FinSequence such that
A3: t99 = t^r by TREES_1:1;
reconsider r as FinSequence of NAT by A3,FINSEQ_1:36;
r|Seg 1 is FinSequence of NAT by FINSEQ_1:18;
then consider r1 being FinSequence of NAT such that
A4: r1 = r|Seg 1;
1 <= len r
proof
len t < len t99 by A2,TREES_1:6;
then consider m being Nat such that
A5: (len t) + m = len t99 by NAT_1:10;
m <> 0 by A2,A5,TREES_1:6;
then 0 < m;
then
A6: 0+1 <= m by NAT_1:13;
len t99 = (len t) + len r by A3,FINSEQ_1:22;
hence thesis by A5,A6;
end;
then consider n being Element of NAT such that
A7: r1 = <*n*> by A4,Th34;
A8: r1 is_a_prefix_of r by A4,TREES_1:def 1;
then
A9: t^r1 is_a_prefix_of t99 by A3,FINSEQ_6:13;
t^<*n*> in T by A3,A7,A8,FINSEQ_6:13,TREES_1:20;
then consider t9 being Element of T such that
A10: t9 = t^<*n*>;
t9 in succ t by A10;
hence thesis by A1,A7,A9,A10,TREES_2:25;
end;
theorem Th52:
for f being sequence of NAT st (for n holds f.(n+1) qua
Nat <= f.n qua Nat) ex m st for n st m <= n holds f.n = f
.m
proof
let f be sequence of NAT such that
A1: for n holds f.(n+1) qua Nat <= f.n qua Nat;
A2: for m,k st m <= k holds f.k qua Nat <= f.m qua Nat
proof
defpred P[Nat] means for m st m <= $1 holds f.$1 qua Element of
NAT <= f.m qua Nat;
A3: for k st P[k] holds P[k + 1]
proof
let k such that
A4: P[k];
now
let m;
assume
A5: m <= k+1;
per cases by A5,NAT_1:8;
suppose
A6: m <= k;
reconsider fk = f.k, fm = f.m, fk1 = f.(k+1) as Nat;
A7: fk1 <= fk by A1;
fk <= fm by A4,A6;
hence f.(k+1) qua Nat <= f.m qua Nat by A7,
XXREAL_0:2;
end;
suppose
m = k+1;
hence f.(k+1) qua Nat <= f.m qua Nat;
end;
end;
hence thesis;
end;
A8: P[0]
by XXREAL_0:1;
A9: for k holds P[k] from NAT_1:sch 2(A8,A3);
let m,k;
assume m <= k;
hence thesis by A9;
end;
defpred P[set] means $1 in rng f;
A10: ex k be Nat st P[k]
proof
consider y such that
A11: y = f.0;
reconsider k = y as Nat by A11;
take k;
dom f = NAT by FUNCT_2:def 1;
hence thesis by A11,FUNCT_1:def 3;
end;
ex k be Nat st P[k] & for n be Nat st P[n] holds k <= n from NAT_1:sch
5(A10);
then consider l be Nat such that
A12: l in rng f and
A13: for n be Nat st n in rng f holds l <= n;
consider x being object such that
A14: x in dom f and
A15: l = f.x by A12,FUNCT_1:def 3;
reconsider m = x as Nat by A14;
A16: dom f = NAT by FUNCT_2:def 1;
for k st m <= k holds f.k = f.m
proof
let k such that
A17: m <= k;
now
reconsider fk = f.k, fm = f.m as Nat;
assume
A18: f.k <> f.m;
fk <= fm by A2,A17;
then
A19: fk < fm by A18,XXREAL_0:1;
k in NAT by ORDINAL1:def 12;
then f.k in rng f by A16,FUNCT_1:def 3;
hence contradiction by A13,A15,A19;
end;
hence thesis;
end;
hence thesis;
end;
scheme
FinDecTree { D() -> non empty set,
T() -> finite-branching (DecoratedTree of D()),
F(Element of D()) -> Nat }:
T() is finite
provided
A1: for t,t9 being Element of dom T(), d being Element of D() st t9 in
succ t & d = T().t9 holds F(d) < F(T().t)
proof
now
assume not T() is finite;
then not dom T() is finite by FINSET_1:10;
then consider B being Branch of dom T() such that
A2: not B is finite by Th49;
defpred P[object,object] means
ex t,t9 being Element of dom T() st t9 in succ t
& t in B & t9 in B & $1 = T().t & $2 = T().t9;
defpred Q[object] means
ex t being Element of dom T() st t in B & $1 = T().t;
A3: for x being object st x in D() & Q[x]
ex y being object st y in D() & P[x,y] & Q[y]
proof
let x be object;
assume that
x in D() and
A4: Q[x];
consider t being Element of dom T() such that
A5: t in B and
A6: x = T() .t by A4;
consider t9 being Element of dom T() such that
A7: t9 in B & t9 in succ t by A2,A5,Th51;
ex y st y = T().t9;
hence thesis by A5,A6,A7;
end;
{} in B by TREES_2:26;
then Q[T().{}];
then
A8: T().{} in D() & Q[T().{}];
ex g being Function st dom g = NAT & rng g c= D() & g.0 = T().{} &
for k holds P[g.k,g.(k+1)] & Q[g.k] from TREES_2:sch 5(A8,A3);
then consider g being Function such that
dom g = NAT and
rng g c= D() and
g.0 = T().{} and
A9: for k holds (ex t,t9 being Element of dom T() st t9 in succ t & t
in B & t9 in B & g.k = T().t & g.(k+1) = T().t9) & ex t being Element of dom T(
) st t in B & g.k = T().t;
defpred P[object,object] means
ex d being Element of D() st d = g.$1 & $2 = F(d);
A10: for x being object st x in NAT ex y being object st y in NAT & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider k = x as Element of NAT;
consider t being Element of dom T() such that
t in B and
A11: g.k = T().t by A9;
reconsider y = F(T().t) as set;
take y;
y in NAT by ORDINAL1:def 12;
hence thesis by A11;
end;
ex f being sequence of NAT st for x being object st x in NAT
holds P[x,f.x]
from FUNCT_2:sch 1(A10);
then consider f being sequence of NAT such that
A12: for x being object st x in NAT
ex d being Element of D() st d = g.x & f.x = F( d);
A13: for k ex t,t9 being Element of dom T() st t9 in succ t & t in B & t9
in B & f.k = F(T().t) & f.(k+1) = F(T().t9)
proof
let k;
A14: ex t,t9 being Element of dom T() st t9 in succ t & t in B & t9 in B
& g.k = T().t & g.(k+1) = T().t9 by A9;
k in NAT by ORDINAL1:def 12;
then
(ex d being Element of D() st d = g.k & f.k = F(d) )& ex d1 being
Element of D() st d1 = g.(k+1) & f.(k+1) = F (d1) by A12;
hence thesis by A14;
end;
A15: for n ex t,t9 being Element of dom T() st t9 in succ t & f.n = F(T().
t) & f.(n+1) = F(T().t9) & f.(n+1) qua Nat < f.n qua Nat
proof
let n;
ex t,t9 being Element of dom T() st t9 in succ t & t in B & t9 in B
& f.n = F(T().t) & f.(n+1) = F(T().t9) by A13;
hence thesis by A1;
end;
for n holds f.(n+1) qua Nat <= f.n qua Nat
proof
let n;
ex t,t9 being Element of dom T() st t9 in succ t & f.n = F(T().t) &
f.(n+1) = F(T().t9) & f.(n+1) qua Nat < f.n qua Nat by
A15;
hence thesis;
end;
then consider m such that
A16: for n st m <= n holds f.n = f.m by Th52;
A17: m+0 <= m+1 by XREAL_1:6;
ex t,t9 being Element of dom T() st t9 in succ t & f.m = F(T().t) & f.
(m+1) = F(T().t9) & f.(m+1) qua Nat < f.m qua Nat by A15;
hence contradiction by A16,A17;
end;
hence thesis;
end;