:: Full Trees
:: by Robert Milewski
::
:: Received February 25, 1998
:: Copyright (c) 1998-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, FINSEQ_1, ORDINAL4, XBOOLE_0, SUBSET_1, RELAT_1,
BINTREE1, TREES_1, MARGREL1, TARSKI, ORDINAL1, CARD_1, ARYTM_3, PARTFUN1,
FUNCT_1, XBOOLEAN, TREES_2, FINSEQ_2, TREES_4, ZFMISC_1, FUNCOP_1,
MCART_1, FINSEQ_5, NAT_1, BINARITH, CAT_1, XXREAL_0, EUCLID, FINSET_1,
POWER, ARYTM_1, BINARI_3, INT_1, ABIAN, BINTREE2, XCMPLX_0, FUNCT_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, XTUPLE_0, MCART_1, NAT_1, NAT_D, ABIAN, SERIES_1, RELAT_1,
MARGREL1, DOMAIN_1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, FINSET_1,
FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_5, BINARITH, BINARI_3, TREES_1,
TREES_2, TREES_4, BINTREE1, EUCLID, XXREAL_0;
constructors WELLORD2, DOMAIN_1, NAT_D, FINSEQOP, SERIES_1, BINARITH,
FINSEQ_5, TREES_9, ABIAN, EUCLID, BINTREE1, BINARI_3, RELSET_1, XTUPLE_0,
BINOP_1, PRE_POLY;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, XXREAL_0,
XREAL_0, NAT_1, FINSEQ_1, MARGREL1, TREES_2, TREES_9, BINTREE1, FINSEQ_2,
INT_1, XTUPLE_0, CARD_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities EUCLID, FINSEQ_2, MARGREL1, XBOOLEAN, BINOP_1;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, MCART_1, NAT_1, NAT_2, WELLORD2, ZFMISC_1, FUNCT_1, FUNCT_2,
CARD_1, CARD_2, POWER, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSEQ_5,
FINSEQ_6, BINARI_3, TREES_1, TREES_2, BINTREE1, XBOOLE_0, XBOOLE_1,
XREAL_1, NAT_D, PARTFUN1, XXREAL_0, XREAL_0, TREES_9, RELSET_1;
schemes FUNCT_2, NAT_1, FINSEQ_2, TREES_2, FUNCT_1;
begin :: Trees and Binary Trees
Lm1: for D being set, p, q being FinSequence of D holds p^q is FinSequence of
D;
Lm2: for D being non empty set, x being Element of D holds <*x*> is
FinSequence of D;
theorem Th1:
for D be set for p be FinSequence for n be Nat holds p
in D* implies p|Seg n in D*
proof
let D be set;
let p be FinSequence;
let n be Nat;
assume p in D*;
then p is FinSequence of D by FINSEQ_1:def 11;
then p|Seg n is FinSequence of D by FINSEQ_1:18;
hence thesis by FINSEQ_1:def 11;
end;
theorem Th2:
for T be binary Tree for t be Element of T holds t is FinSequence of BOOLEAN
proof
let T be binary Tree;
let t be Element of T;
defpred P[FinSequence] means $1 is Element of T implies rng $1 c= BOOLEAN;
A1: for p be FinSequence of NAT
for x be Element of NAT st P[p] holds P[p^<*x*>]
proof
let p be FinSequence of NAT;
let x be Element of NAT;
assume
A2: P[p];
assume
A3: p^<*x*> is Element of T;
then reconsider p1 = p as Element of T by TREES_1:21;
p^<*x*> in { p^<*n*> where n is Nat : p^<*n*> in T } by A3;
then
A4: p^<*x*> in succ p1 by TREES_2:def 5;
then not p in Leaves T by BINTREE1:3;
then succ p1 = { p^<* 0 *>, p^<*1*> } by BINTREE1:def 2;
then p^<*x*> = p^<* 0 *> or p^<*x*> = p^<*1*> by A4,TARSKI:def 2;
then x = 0 or x = 1 by FINSEQ_2:17;
then
A5: x in {0,1} by TARSKI:def 2;
A6: {x} c= BOOLEAN
by A5,TARSKI:def 1;
rng <*x*> = {x} by FINSEQ_1:38;
then (rng p) \/ (rng <*x*>) c= BOOLEAN by A2,A3,A6,TREES_1:21,XBOOLE_1:8;
hence thesis by FINSEQ_1:31;
end;
A7: P[<*>NAT] by XBOOLE_1:2;
for p be FinSequence of NAT holds P[p] from FINSEQ_2:sch 2(A7,A1);
then rng t c= BOOLEAN;
hence thesis by FINSEQ_1:def 4;
end;
definition
let T be binary Tree;
redefine mode Element of T -> FinSequence of BOOLEAN; :: redefines Element (SUBSET_1, definition)
coherence by Th2;
end;
theorem Th3:
for T be Tree st T = {0,1}* holds T is binary
proof
let T be Tree;
assume
A1: T = {0,1}*;
now
let t be Element of T;
assume not t in Leaves T;
{ t^<*n*> where n is Nat : t^<*n*> in T } = { t^<* 0 *>, t^
<* 1 *> }
proof
thus {t^<*n*> where n is Nat : t^<*n*> in T} c= { t^<* 0 *>,
t^<* 1 *> }
proof
let x be object;
assume x in { t^<*n*> where n is Nat : t^<*n*> in T };
then consider n be Nat such that
A2: x = t^<*n*> and
A3: t^<*n*> in T;
reconsider tn = t^<*n*> as FinSequence of ({0,1} qua set) by A1,A3,
FINSEQ_1:def 11;
len t + 1 in Seg (len t + 1) by FINSEQ_1:4;
then len t + 1 in Seg len tn by FINSEQ_2:16;
then len t + 1 in dom tn by FINSEQ_1:def 3;
then tn/.(len t + 1) = (t^<*n*>).(len t + 1) by PARTFUN1:def 6
.= n by FINSEQ_1:42;
then n = 0 or n = 1 by TARSKI:def 2;
hence thesis by A2,TARSKI:def 2;
end;
let x be object;
A4: t is FinSequence of {0,1} by A1,FINSEQ_1:def 11;
rng <* 1 *> c= {0,1}
proof
let z be object;
assume z in rng <* 1 *>;
then z in {1} by FINSEQ_1:38;
then z = 1 by TARSKI:def 1;
hence thesis by TARSKI:def 2;
end;
then <* 1 *> is FinSequence of {0,1} by FINSEQ_1:def 4;
then t^<* 1 *> is FinSequence of {0,1} by A4,Lm1;
then
A5: t^<* 1 *> in T by A1,FINSEQ_1:def 11;
assume x in { t^<* 0 *>, t^<* 1 *> };
then
A6: x = t^<* 0 *> or x = t^<* 1 *> by TARSKI:def 2;
rng <* 0 *> c= {0,1}
proof
let z be object;
assume z in rng <* 0 *>;
then z in {0} by FINSEQ_1:38;
then z = 0 by TARSKI:def 1;
hence thesis by TARSKI:def 2;
end;
then <* 0 *> is FinSequence of {0,1} by FINSEQ_1:def 4;
then t^<* 0 *> is FinSequence of {0,1} by A4,Lm1;
then t^<* 0 *> in T by A1,FINSEQ_1:def 11;
hence thesis by A5,A6;
end;
hence succ t = { t^<* 0 *>, t^<* 1 *> } by TREES_2:def 5;
end;
hence thesis by BINTREE1:def 2;
end;
theorem Th4:
for T be Tree st T = {0,1}* holds Leaves T = {}
proof
A1: {0} c= BOOLEAN
proof
let z be object;
assume z in {0};
then z = FALSE by TARSKI:def 1;
hence thesis;
end;
let T be Tree;
assume
A2: T = {0,1}*;
assume Leaves T <> {};
then consider x be object such that
A3: x in Leaves T by XBOOLE_0:def 1;
reconsider x1 = x as Element of T by A3;
T is binary by A2,Th3;
then
A4: x1 is FinSequence of BOOLEAN by Th2;
then reconsider x1 = x as FinSequence of NAT;
set y1 = x1 ^ <* 0 *>;
0 in {0} by TARSKI:def 1;
then <* 0 *> is FinSequence of BOOLEAN by A1,Lm2;
then y1 is FinSequence of BOOLEAN by A4,Lm1;
then
A5: y1 in T by A2,FINSEQ_1:def 11;
x1 is_a_proper_prefix_of y1 by TREES_1:8;
hence contradiction by A3,A5,TREES_1:def 5;
end;
theorem
for T be binary Tree for n be Nat for t be Element of T st
t in T-level n holds t is Element of n-tuples_on BOOLEAN
proof
let T be binary Tree;
let n be Nat;
let t be Element of T;
assume t in T-level n;
then t in { w where w is Element of T : len w = n } by TREES_2:def 6;
then ex t2 be Element of T st t2 = t & len t2 = n;
hence thesis by FINSEQ_2:92;
end;
theorem
for T be Tree st for t be Element of T holds succ t = { t^<* 0 *>, t^
<* 1 *> } holds Leaves T = {}
proof
let T be Tree;
assume
A1: for t be Element of T holds succ t = { t^<* 0 *>, t^<* 1 *> };
assume Leaves T <> {};
then consider x be object such that
A2: x in Leaves T by XBOOLE_0:def 1;
reconsider t = x as Element of T by A2;
succ t = { t^<* 0 *>, t^<* 1 *> } by A1;
hence contradiction by A2,BINTREE1:3;
end;
theorem Th7:
for T be Tree st for t be Element of T holds succ t = { t^<* 0 *>
, t^<* 1 *> } holds T is binary
proof
let T be Tree;
assume for t be Element of T holds succ t = { t^<* 0 *>, t^<* 1 *> };
then
for t be Element of T st not t in Leaves T holds succ t = { t^<* 0 *>, t
^<* 1 *> };
hence thesis by BINTREE1:def 2;
end;
theorem Th8:
for T be Tree holds T = {0,1}* iff for t be Element of T holds
succ t = { t^<* 0 *>, t^<* 1 *> }
proof
let T be Tree;
thus T = {0,1}* implies for t be Element of T holds succ t = { t^<* 0 *>, t^
<* 1 *> }
proof
assume
A1: T = {0,1}*;
let t be Element of T;
T is binary & not t in Leaves T by A1,Th3,Th4;
hence thesis by BINTREE1:def 2;
end;
assume
A2: for t be Element of T holds succ t = { t^<* 0 *>, t^<* 1 *> };
thus T = {0,1}*
proof
thus T c= {0,1}*
proof
let x be object;
assume
A3: x in T;
T is binary by A2,Th7;
then x is FinSequence of {0,1} by A3,Th2;
hence thesis by FINSEQ_1:def 11;
end;
defpred P[FinSequence] means $1 in T;
let x be object;
assume x in {0,1}*;
then
A4: x is FinSequence of {0,1} by FINSEQ_1:def 11;
A5: for p be FinSequence of {0,1} for n be Element of {0,1} st P[p] holds
P[p^<*n*>]
proof
let p be FinSequence of {0,1};
let n be Element of {0,1};
A6: n = 0 or n = 1 by TARSKI:def 2;
assume p in T;
then reconsider p1 = p as Element of T;
succ p1 = { p1^<* 0 *>, p1^<* 1 *> } by A2;
then p^<*n*> in succ p1 by A6,TARSKI:def 2;
hence thesis;
end;
A7: P[<*> {0,1}] by TREES_1:22;
for p be FinSequence of {0,1} holds P[p] from FINSEQ_2:sch 2(A7, A5);
hence thesis by A4;
end;
end;
scheme
DecoratedBinTreeEx {A() -> non empty set, a() -> Element of A(),
P[object,object,object]}:
ex D be binary DecoratedTree of A() st dom D = {0,1}* & D.{} = a() & for
x be Node of D holds P[D.x,D.(x ^ <* 0 *>),D.(x ^ <*1*>)]
provided
A1: for a be Element of A() ex b,c be Element of A() st P[a,b,c]
proof
defpred Q[object,object] means
ex b,c be Element of A() st P[$1,b,c] & $2 = [b,c];
A2: for e be object st e in A() ex u be object st u in [:A(),A():] & Q[e,u]
proof
let e be object;
assume e in A();
then consider b,c be Element of A() such that
A3: P[e,b,c] by A1;
take u = [b,c];
thus u in [:A(),A():];
thus thesis by A3;
end;
consider f be Function such that
A4: dom f = A() and
A5: rng f c= [:A(),A():] and
A6: for e be object st e in A() holds Q[e,f.e] from FUNCT_1:sch 6(A2);
deffunc F(object) = IFEQ($1`2,0,(f.($1`1))`1,(f.($1`1))`2);
A7: for x be object st x in [:A(),NAT:] holds F(x) in A()
proof
let x be object;
assume x in [:A(),NAT:];
then x`1 in A() by MCART_1:10;
then
A8: f.(x`1) in rng f by A4,FUNCT_1:def 3;
then
A9: (f.(x`1))`2 in A() by A5,MCART_1:10;
A10: (f.(x`1))`1 in A() by A5,A8,MCART_1:10;
now
per cases;
suppose
x`2 = 0;
hence thesis by A10,FUNCOP_1:def 8;
end;
suppose
x`2 <> 0;
hence thesis by A9,FUNCOP_1:def 8;
end;
end;
hence thesis;
end;
consider F be Function of [:A(),NAT:],A() such that
A11: for x be object st x in [:A(),NAT:] holds F.x = F(x) from FUNCT_2:sch
2 ( A7);
deffunc F(set) = 2;
consider D be DecoratedTree of A() such that
A12: D.{} = a() and
A13: for d be Element of dom D holds succ d = { d^<*k*> where k is
Nat : k < F(D.d) } & for n be Nat st n < F(D.d) holds D.(
d^<*n*>) = F.(D.d,n) from TREES_2:sch 9;
now
let t be Element of dom D;
assume not t in Leaves dom D;
{ t^<*k*> where k is Nat : k < 2 } = { t^<* 0 *>, t^<* 1 *> }
proof
thus { t^<*k*> where k is Nat : k < 2 } c= { t^<* 0 *>, t^<*
1 *> }
proof
let v be object;
assume v in { t^<*k*> where k is Nat : k < 2 };
then consider k be Nat such that
A14: v = t^<*k*> and
A15: k < 2;
k = 0 or k = 1 by A15,NAT_1:23;
hence thesis by A14,TARSKI:def 2;
end;
let v be object;
assume v in { t^<* 0 *>, t^<* 1 *> };
then v = t^<* 0 *> or v = t^<* 1 *> by TARSKI:def 2;
hence thesis;
end;
hence succ t = { t^<* 0 *>, t^<* 1 *> } by A13;
end;
then dom D is binary by BINTREE1:def 2;
then reconsider D as binary DecoratedTree of A() by BINTREE1:def 3;
take D;
now
let t be Element of dom D;
{ t^<*k*> where k is Nat : k < 2 } = { t^<* 0 *>, t^<* 1 *> }
proof
thus { t^<*k*> where k is Nat : k < 2 } c= { t^<* 0 *>, t^<*
1 *> }
proof
let v be object;
assume v in { t^<*k*> where k is Nat : k < 2 };
then consider k be Nat such that
A16: v = t^<*k*> and
A17: k < 2;
k = 0 or k = 1 by A17,NAT_1:23;
hence thesis by A16,TARSKI:def 2;
end;
let v be object;
assume v in { t^<* 0 *>, t^<* 1 *> };
then v = t^<* 0 *> or v = t^<* 1 *> by TARSKI:def 2;
hence thesis;
end;
hence succ t = { t^<* 0 *>, t^<* 1 *> } by A13;
end;
hence dom D = {0,1}* by Th8;
thus D.{} = a() by A12;
let x be Node of D;
for e be set st e in A() holds P[e,F.(e,0),F.(e,1)]
proof
let e be set;
assume
A18: e in A();
then consider b,c be Element of A() such that
A19: P[e,b,c] and
A20: f.e = [b,c] by A6;
[e,1] in [:A(),NAT:] by A18,ZFMISC_1:87;
then
A21: F.[e,1] = IFEQ([e,1]`2,0,(f.([e,1]`1))`1,(f.([e,1]`1))`2) by A11
.= (f.([e,1]`1))`2 by FUNCOP_1:def 8
.= (f.e)`2
.= c by A20;
[e,0] in [:A(),NAT:] by A18,ZFMISC_1:87;
then F.[e,0] = IFEQ([e,0]`2,0,(f.([e,0]`1))`1,(f.([e,0]`1))`2) by A11
.= (f.([e,0]`1))`1 by FUNCOP_1:def 8
.= (f.e)`1
.= b by A20;
hence thesis by A19,A21;
end;
then P[D.x,F.(D.x,0),F.(D.x,1)];
then P[D.x,D.(x ^ <* 0 *>),F.(D.x,1)] by A13;
hence thesis by A13;
end;
scheme
DecoratedBinTreeEx1 {A() -> non empty set, a() -> Element of A(),
P,Q[object,object]}:
ex D be binary DecoratedTree of A() st dom D = {0,1}* & D.{} = a
() & for x be Node of D holds P[D.x,D.(x ^ <* 0 *>)] & Q[D.x,D.(x ^ <*1*>)]
provided
A1: for a be Element of A() ex b be Element of A() st P[a,b] and
A2: for a be Element of A() ex b be Element of A() st Q[a,b]
proof
deffunc F(set) = 2;
defpred P1[object,object] means
( $1`2 = 0 implies P[$1`1,$2] ) & ( $1`2 = 1
implies Q[$1`1,$2] );
A3: for e be object st e in [:A(),NAT:] ex u be object st u in A() & P1[e,u]
proof
let e be object;
assume e in [:A(),NAT:];
then reconsider e1 = e`1 as Element of A() by MCART_1:10;
consider u1 be Element of A() such that
A4: P[e1,u1] by A1;
consider u2 be Element of A() such that
A5: Q[e1,u2] by A2;
take u = IFEQ(e`2,0,u1,u2);
thus u in A();
thus e`2 = 0 implies P[e`1,u] by A4,FUNCOP_1:def 8;
thus thesis by A5,FUNCOP_1:def 8;
end;
consider F be Function such that
A6: dom F = [:A(),NAT:] & rng F c= A() and
A7: for e be object st e in [:A(),NAT:] holds P1[e,F.e] from FUNCT_1:sch 6
(A3 );
reconsider F as Function of [:A(),NAT:],A() by A6,FUNCT_2:2;
consider D be DecoratedTree of A() such that
A8: D.{} = a() and
A9: for d be Element of dom D holds succ d = { d^<*k*> where k is
Nat : k < F(D.d) } & for n be Nat st n < F(D.d) holds D.(
d^<*n*>) = F.(D.d,n) from TREES_2:sch 9;
now
let t be Element of dom D;
assume not t in Leaves dom D;
{ t^<*k*> where k is Nat : k < 2 } = { t^<* 0 *>, t^<* 1 *> }
proof
thus { t^<*k*> where k is Nat : k < 2 } c= { t^<* 0 *>, t^<*
1 *> }
proof
let v be object;
assume v in { t^<*k*> where k is Nat : k < 2 };
then consider k be Nat such that
A10: v = t^<*k*> and
A11: k < 2;
k = 0 or k = 1 by A11,NAT_1:23;
hence thesis by A10,TARSKI:def 2;
end;
let v be object;
assume v in { t^<* 0 *>, t^<* 1 *> };
then v = t^<* 0 *> or v = t^<* 1 *> by TARSKI:def 2;
hence thesis;
end;
hence succ t = { t^<* 0 *>, t^<* 1 *> } by A9;
end;
then dom D is binary by BINTREE1:def 2;
then reconsider D as binary DecoratedTree of A() by BINTREE1:def 3;
take D;
now
let t be Element of dom D;
{ t^<*k*> where k is Nat : k < 2 } = { t^<* 0 *>, t^<* 1 *> }
proof
thus { t^<*k*> where k is Nat : k < 2 } c= { t^<* 0 *>, t^<*
1 *> }
proof
let v be object;
assume v in { t^<*k*> where k is Nat : k < 2 };
then consider k be Nat such that
A12: v = t^<*k*> and
A13: k < 2;
k = 0 or k = 1 by A13,NAT_1:23;
hence thesis by A12,TARSKI:def 2;
end;
let v be object;
assume v in { t^<* 0 *>, t^<* 1 *> };
then v = t^<* 0 *> or v = t^<* 1 *> by TARSKI:def 2;
hence thesis;
end;
hence succ t = { t^<* 0 *>, t^<* 1 *> } by A9;
end;
hence dom D = {0,1}* by Th8;
thus D.{} = a() by A8;
let x be Node of D;
[D.x,0]`2 = 0;
then P[[D.x,0]`1,F.[D.x,0]] by A7;
then P[D.x,F.(D.x,0)];
hence P[D.x,D.(x ^ <* 0 *>)] by A9;
[D.x,1]`2 = 1;
then Q[[D.x,1]`1,F.[D.x,1]] by A7;
then Q[D.x,F.(D.x,1)];
hence thesis by A9;
end;
Lm3: for D be non empty set for f be FinSequence of D holds Rev f is
FinSequence of D;
definition
let T be binary Tree;
let n be non zero Nat;
func NumberOnLevel(n,T) -> Function of T-level n,NAT means
:Def1:
for t be Element of T st t in T-level n
for F be Element of n-tuples_on BOOLEAN st F = Rev t holds
it.t = (Absval F) + 1;
existence
proof
defpred P[object,object] means
ex t be Element of T st t = $1 & for F be Tuple
of n,BOOLEAN st F = Rev t holds $2 = (Absval F) + 1;
A1: for e be object st e in T-level n ex u be object st u in NAT & P[e,u]
proof
let e be object;
assume e in T-level n;
then e in { w where w is Element of T : len w = n } by TREES_2:def 6;
then consider t be Element of T such that
A2: t = e and
A3: len t = n;
len Rev t = n by A3,FINSEQ_5:def 3;
then reconsider F1 = Rev t
as Element of n-tuples_on BOOLEAN by FINSEQ_2:92;
take u = (Absval F1) + 1;
thus u in NAT;
take t;
thus t = e by A2;
let F be Tuple of n, BOOLEAN;
assume F = Rev t;
hence thesis;
end;
consider f be Function such that
A4: dom f = T-level n & rng f c= NAT and
A5: for e be object st e in T-level n holds P[e,f.e] from FUNCT_1:sch 6(
A1);
reconsider f as Function of T-level n,NAT by A4,FUNCT_2:2;
take f;
let t be Element of T;
assume t in T-level n;
then
A6: ex t1 be Element of T st t1 = t & for F be Tuple of n, BOOLEAN st F =
Rev t1 holds f.t = (Absval F) + 1 by A5;
let F be Element of n-tuples_on BOOLEAN;
assume F = Rev t;
hence thesis by A6;
end;
uniqueness
proof
let f1,f2 be Function of T-level n,NAT such that
A7: for t be Element of T st t in T-level n
for F be Element of n-tuples_on BOOLEAN
st F = Rev t holds f1.t = (Absval F) + 1 and
A8: for t be Element of T st t in T-level n
for F be Element of n-tuples_on BOOLEAN
st F = Rev t holds f2.t = (Absval F) + 1;
now
let x be object;
assume
A9: x in T-level n;
then x in { w where w is Element of T : len w = n } by TREES_2:def 6;
then consider t be Element of T such that
A10: t = x and
A11: len t = n;
len Rev t = n by A11,FINSEQ_5:def 3;
then reconsider F = Rev t
as Element of n-tuples_on BOOLEAN by FINSEQ_2:92;
thus f1.x = (Absval F) + 1 by A7,A9,A10
.= f2.x by A8,A9,A10;
end;
hence f1 = f2 by FUNCT_2:12;
end;
end;
registration
let T be binary Tree;
let n be non zero Nat;
cluster NumberOnLevel(n,T) -> one-to-one;
coherence
proof
now
let x1,x2 be object;
assume that
A1: x1 in dom NumberOnLevel(n,T) and
A2: x2 in dom NumberOnLevel(n,T) and
A3: NumberOnLevel(n,T).x1 = NumberOnLevel(n,T).x2;
A4: x1 in T-level n by A1,FUNCT_2:def 1;
then x1 in { w where w is Element of T : len w = n } by TREES_2:def 6;
then consider t1 be Element of T such that
A5: t1 = x1 and
A6: len t1 = n;
A7: x2 in T-level n by A2,FUNCT_2:def 1;
then x2 in { w where w is Element of T : len w = n } by TREES_2:def 6;
then consider t2 be Element of T such that
A8: t2 = x2 and
A9: len t2 = n;
len Rev t2 = n by A9,FINSEQ_5:def 3;
then reconsider F2 = Rev t2
as Element of n-tuples_on BOOLEAN by FINSEQ_2:92;
len Rev t1 = n by A6,FINSEQ_5:def 3;
then reconsider F1 = Rev t1
as Element of n-tuples_on BOOLEAN by FINSEQ_2:92;
(Absval F1) + 1 = NumberOnLevel(n,T).x1 by A4,A5,Def1
.= (Absval F2) + 1 by A3,A7,A8,Def1;
hence x1 = x2 by A5,A8,BINARI_3:2,3;
end;
hence thesis by FUNCT_1:def 4;
end;
end;
begin :: Full Trees
definition
let T be Tree;
attr T is full means
:Def2:
T = {0,1}*;
end;
theorem Th9:
{0,1}* is Tree
proof
set X = {0,1}*;
A1: now
let p be FinSequence of NAT;
assume
A2: p in X;
thus ProperPrefixes p c= X
proof
let y be object;
assume y in ProperPrefixes p;
then consider q be FinSequence such that
A3: y = q and
A4: q is_a_proper_prefix_of p by TREES_1:def 2;
q is_a_prefix_of p by A4;
then ex n be Nat st q = p|Seg n by TREES_1:def 1;
hence thesis by A2,A3,Th1;
end;
end;
A5: now
let p be FinSequence of NAT, k,n be Nat;
assume that
A6: p^<*k*> in X and
A7: n <= k;
A8: p^<*k*> is FinSequence of {0,1} by A6,FINSEQ_1:def 11;
then reconsider kk = <*k*> as FinSequence of {0,1} by FINSEQ_1:36;
1 in Seg 1 by FINSEQ_1:3;
then 1 in dom <*k*> by FINSEQ_1:38;
then kk.1 in {0,1} by FINSEQ_2:11;
then
A9: k in {0,1};
now
per cases by A9,TARSKI:def 2;
suppose
k = 0;
hence n = 0 or n = 1 by A7;
end;
suppose
A10: k = 1;
n = 1 or n = 0
proof
assume n <> 1;
then n < 0 + 1 by A7,A10,XXREAL_0:1;
hence thesis by NAT_1:13;
end;
hence n = 0 or n = 1;
end;
end;
then n in {0,1} by TARSKI:def 2;
then
A11: <*n*> is FinSequence of {0,1} by Lm2;
p is FinSequence of {0,1} by A8,FINSEQ_1:36;
then p^<*n*> is FinSequence of {0,1} by A11,Lm1;
hence p^<*n*> in X by FINSEQ_1:def 11;
end;
X c= NAT* by FINSEQ_1:62;
hence thesis by A1,A5,TREES_1:def 3;
end;
theorem Th10:
for T be Tree st T = {0,1}* for n be Nat holds 0*n in T-level n
proof
let T be Tree;
assume
A1: T = {0,1}*;
let n be Nat;
len (0*n) = n & 0*n in T by A1,BINARI_3:4,CARD_1:def 7;
then 0*n in { w where w is Element of T : len w = n };
hence thesis by TREES_2:def 6;
end;
theorem Th11:
for T be Tree st T = {0,1}* for n be non zero Nat
for y be Element of n-tuples_on BOOLEAN holds y in T-level n
proof
let T be Tree;
assume
A1: T = {0,1}*;
let n be non zero Nat;
let y be Element of n-tuples_on BOOLEAN;
y in { w where w is Element of T : len w = n } by A1;
hence thesis by TREES_2:def 6;
end;
registration
let T be binary Tree;
let n be Nat;
cluster T-level n -> finite;
coherence by TREES_9:46;
end;
registration
cluster full -> binary for Tree;
coherence by Th3;
end;
registration
cluster full for Tree;
existence by Th9,Def2;
end;
theorem Th12:
for T be full Tree for n be non zero Nat holds Seg (2 to_power
n) c= rng NumberOnLevel(n,T)
proof
let T be full Tree;
let n be non zero Nat;
let y be object;
assume y in Seg (2 to_power n);
then y in { k where k is Nat : 1 <= k & k <= 2 to_power n } by FINSEQ_1:def 1
;
then consider k be Nat such that
A1: k = y and
A2: 1 <= k and
A3: k <= 2 to_power n;
A4: k - 1 >= 1 - 1 by A2,XREAL_1:9;
set t = Rev (n-BinarySequence (k-'1));
A5: len t = len (n-BinarySequence (k-'1)) by FINSEQ_5:def 3
.= n by CARD_1:def 7;
then len Rev t = n by FINSEQ_5:def 3;
then reconsider F = Rev t as Element of n-tuples_on BOOLEAN by FINSEQ_2:92;
T = {0,1}* by Def2;
then t in T by FINSEQ_1:def 11;
then t in { w where w is Element of T : len w = n } by A5;
then
A6: t in T-level n by TREES_2:def 6;
then
A7: t in dom NumberOnLevel(n,T) by FUNCT_2:def 1;
k < 2 to_power n + 1 by A3,NAT_1:13;
then k - 1 < 2 to_power n by XREAL_1:19;
then
A8: k-'1 < 2 to_power n by A4,XREAL_0:def 2;
NumberOnLevel(n,T).t = (Absval F) + 1 by A6,Def1
.= (Absval (n-BinarySequence (k-'1))) + 1
.= k -' 1 + 1 by A8,BINARI_3:35
.= k - 1 + 1 by A4,XREAL_0:def 2
.= y by A1;
hence thesis by A7,FUNCT_1:def 3;
end;
definition
let T be full Tree;
let n be non zero Nat;
func FinSeqLevel(n,T) -> FinSequence of T-level n equals
NumberOnLevel(n,T)";
coherence
proof
reconsider k=n as non zero Nat;
T = {0,1}* by Def2;
then
A1: T-level n is non empty by Th10;
for y be object holds y in Seg (2 to_power n) iff
ex x be object st x in dom
NumberOnLevel(k,T) & y = NumberOnLevel(k,T).x
proof
let y be object;
thus y in Seg (2 to_power n) implies ex x be object st x in dom
NumberOnLevel(k,T) & y = NumberOnLevel(k,T).x
proof
assume
A2: y in Seg (2 to_power n);
take (NumberOnLevel(n,T)").y;
Seg (2 to_power n) c= rng NumberOnLevel(n,T) by Th12;
hence thesis by A2,FUNCT_1:32;
end;
given x be object such that
A3: x in dom NumberOnLevel(k,T) and
A4: y = NumberOnLevel(k,T).x;
A5: x in T-level n by A3,FUNCT_2:def 1;
then x in { t where t is Element of T : len t = n } by TREES_2:def 6;
then consider t be Element of T such that
A6: t = x and
A7: len t = n;
len Rev t = n by A7,FINSEQ_5:def 3;
then reconsider F = Rev t
as Element of n-tuples_on BOOLEAN by FINSEQ_2:92;
Absval F < 2 to_power n by BINARI_3:1;
then
A8: 1 <= (Absval F) + 1 & (Absval F) + 1 <= 2 to_power n by NAT_1:11,13;
y = (Absval F) + 1 by A4,A5,A6,Def1;
hence thesis by A8,FINSEQ_1:1;
end;
then rng NumberOnLevel(n,T) = Seg (2 to_power n) by FUNCT_1:def 3;
then
A9: dom (NumberOnLevel(k,T)") = Seg (2 to_power n) by FUNCT_1:33;
rng (NumberOnLevel(k,T)") = dom NumberOnLevel(k,T) by FUNCT_1:33
.= T-level n by FUNCT_2:def 1;
then NumberOnLevel(n,T)" is Function of Seg (2 to_power n), T-level n by A9
,FUNCT_2:2;
hence thesis by A1,FINSEQ_2:25;
end;
end;
registration
let T be full Tree;
let n be non zero Nat;
cluster FinSeqLevel(n,T) -> one-to-one;
coherence by FUNCT_1:40;
end;
theorem Th13:
for T be full Tree for n be non zero Nat holds
NumberOnLevel(n,T).(0*n) = 1
proof
let T be full Tree;
let n be non zero Nat;
A1: len Rev (0*n) = len 0*n by FINSEQ_5:def 3
.= n by CARD_1:def 7;
A2: T = {0,1}* by Def2;
then 0*n is Element of T by BINARI_3:4;
then Rev (0*n) is FinSequence of BOOLEAN by Lm3;
then reconsider F = Rev (0*n) as
Element of n-tuples_on BOOLEAN by A1,FINSEQ_2:92;
0*n in T-level n by A2,Th10;
hence NumberOnLevel(n,T).(0*n) = (Absval F) + 1 by Def1
.= 0 + 1 by BINARI_3:6,8
.= 1;
end;
theorem Th14:
for T be full Tree for n be non zero Nat for y be
Element of n-tuples_on BOOLEAN st y = 0*n
holds NumberOnLevel(n,T).'not' y = 2 to_power n
proof
let T be full Tree;
let n be non zero Nat;
let y be Element of n-tuples_on BOOLEAN;
assume
A1: y = 0*n;
then
A2: Rev 'not' y = 'not' y by BINARI_3:9;
len Rev 'not' y = len 'not' y by FINSEQ_5:def 3
.= n by CARD_1:def 7;
then reconsider F = Rev 'not' y as
Element of n-tuples_on BOOLEAN by FINSEQ_2:92;
reconsider ny = 'not' y as
Element of n-tuples_on BOOLEAN by FINSEQ_2:131;
T = {0,1}* by Def2;
then ny in T-level n by Th11;
hence NumberOnLevel(n,T).'not' y = (Absval F) + 1 by Def1
.= 2 to_power n - 1 + 1 by A1,A2,BINARI_3:7
.= 2 to_power n;
end;
theorem Th15:
for T be full Tree for n be non zero Nat holds
FinSeqLevel(n,T).1 = 0*n
proof
let T be full Tree;
let n be non zero Nat;
T = {0,1}* by Def2;
then 0*n in T-level n by Th10;
then
A1: 0*n in dom NumberOnLevel(n,T) by FUNCT_2:def 1;
1 = NumberOnLevel(n,T).(0*n) by Th13;
hence thesis by A1,FUNCT_1:32;
end;
theorem Th16:
for T be full Tree for n be non zero Nat for y be
Element of n-tuples_on BOOLEAN
st y = 0*n holds FinSeqLevel(n,T).(2 to_power n) = 'not' y
proof
let T be full Tree;
let n be non zero Nat;
let y be Element of n-tuples_on BOOLEAN;
reconsider ny = 'not' y as
Element of n-tuples_on BOOLEAN by FINSEQ_2:131;
T = {0,1}* by Def2;
then ny in T-level n by Th11;
then
A1: 'not' y in dom NumberOnLevel(n,T) by FUNCT_2:def 1;
assume y = 0*n;
then 2 to_power n = NumberOnLevel(n,T).'not' y by Th14;
hence thesis by A1,FUNCT_1:32;
end;
theorem Th17:
for T be full Tree for n be non zero Nat for i be
Nat st i in Seg (2 to_power n) holds FinSeqLevel(n,T).i = Rev (n
-BinarySequence (i-'1))
proof
let T be full Tree;
let n be non zero Nat;
let i be Nat;
reconsider nB = n-BinarySequence (i-'1) as Element of n-tuples_on BOOLEAN
by FINSEQ_2:131;
assume
A1: i in Seg (2 to_power n);
then
A2: 1 <= i by FINSEQ_1:1;
i <= 2 to_power n by A1,FINSEQ_1:1;
then i < 2 to_power n + 1 by NAT_1:13;
then i - 1 < 2 to_power n by XREAL_1:19;
then i-'1 < 2 to_power n by A2,XREAL_1:233;
then
A3: (Absval nB) + 1 = i-'1 + 1 by BINARI_3:35
.= i - 1 + 1 by A2,XREAL_1:233
.= i;
A4: len Rev nB = len nB by FINSEQ_5:def 3
.= n by CARD_1:def 7;
then reconsider RnB = Rev nB as
Element of n-tuples_on BOOLEAN by FINSEQ_2:92;
RnB in {0,1}* by FINSEQ_1:def 11;
then RnB is Element of T by Def2;
then RnB in { t where t is Element of T : len t = n } by A4;
then
A5: RnB in T-level n by TREES_2:def 6;
nB = Rev RnB;
then
A6: NumberOnLevel(n,T).RnB = (Absval nB) + 1 by A5,Def1;
RnB in dom NumberOnLevel(n,T) by A5,FUNCT_2:def 1;
hence thesis by A6,A3,FUNCT_1:32;
end;
theorem Th18:
for T be full Tree for n be Nat holds card (T-level n
) = 2 to_power n
proof
let T be full Tree;
defpred R[Nat] means card (T-level $1) = 2 to_power $1;
A1: T = {0,1}* by Def2;
A2: for n be Nat st R[n] holds R[n+1]
proof
defpred P[set,set] means ex p be FinSequence st p = $1 & $2 = p^<* 0 *>;
let n be Nat;
set Tn10 = { p where p is Element of T : len p = n+1 & p.(n+1) = 0 };
set Tn11 = { p where p is Element of T : len p = n+1 & p.(n+1) = 1 };
A3: (0*(n+1)).(n+1) = 0 by FINSEQ_1:4,FUNCOP_1:7;
len 0*(n+1) = n+1 & 0*(n+1) in T by A1,BINARI_3:4,CARD_1:def 7;
then
A4: 0*(n+1) in Tn10 by A3;
A5: Tn11 c= T-level (n+1)
proof
let x be object;
assume x in Tn11;
then consider p be Element of T such that
A6: p = x and
A7: len p = n+1 and
p.(n+1) = 1;
p in { w where w is Element of T : len w = n+1 } by A7;
hence thesis by A6,TREES_2:def 6;
end;
rng <*1*> c= {0,1}
proof
let z be object;
assume z in rng <*1*>;
then z in {1} by FINSEQ_1:38;
then z = 1 by TARSKI:def 1;
hence thesis by TARSKI:def 2;
end;
then
A8: <*1*> is FinSequence of {0,1} by FINSEQ_1:def 4;
defpred P1[set,set] means ex p be FinSequence st p = $1 & $2 = p^<* 1 *>;
A9: Tn10 c= T-level (n+1)
proof
let x be object;
assume x in Tn10;
then consider p be Element of T such that
A10: p = x and
A11: len p = n+1 and
p.(n+1) = 0;
p in { w where w is Element of T : len w = n+1 } by A11;
hence thesis by A10,TREES_2:def 6;
end;
0*n in {0,1}* by BINARI_3:4;
then 0*n is FinSequence of {0,1} by FINSEQ_1:def 11;
then 0*n^<*1*> is FinSequence of {0,1} by A8,Lm1;
then
A12: 0*n^<*1*> in T by A1,FINSEQ_1:def 11;
reconsider Tn = T-level n as finite non empty set by A1,Th10;
assume
A13: card (T-level n) = 2 to_power n;
len 0*n = n by CARD_1:def 7;
then
A14: (0*n^<*1*>).(n+1) = 1 by FINSEQ_1:42;
len (0*n^<*1*>) = len 0*n + 1 by FINSEQ_2:16
.= n+1 by CARD_1:def 7;
then 0*n^<*1*> in Tn11 by A12,A14;
then reconsider Tn10,Tn11 as non empty finite set by A4,A9,A5;
A15: Tn10 \/ Tn11 c= T-level (n+1) by A9,A5,XBOOLE_1:8;
A16: for x be Element of Tn ex y be Element of Tn11 st P1[x,y]
proof
let x be Element of Tn;
x in T-level n;
then x in { w where w is Element of T : len w = n } by TREES_2:def 6;
then consider p be Element of T such that
A17: p = x and
A18: len p = n;
set y = p^<*1*>;
p^<*1*> is FinSequence of {0,1} by A8,Lm1;
then
A19: y in T by A1,FINSEQ_1:def 11;
len y = n+1 & y.(n+1) = 1 by A18,FINSEQ_1:42,FINSEQ_2:16;
then y in { t where t is Element of T : len t = n+1 & t.(n+1) = 1 } by
A19;
then reconsider y as Element of Tn11;
take y,p;
thus thesis by A17;
end;
consider f1 be Function of Tn,Tn11 such that
A20: for x be Element of Tn holds P1[x,f1.x] from FUNCT_2:sch 3(A16);
now
let y be object;
assume y in Tn11;
then consider t be Element of T such that
A21: t = y and
A22: len t = n+1 and
A23: t.(n+1) = 1;
consider p be FinSequence of BOOLEAN, d be Element of BOOLEAN such that
A24: t = p^<*d*> by A22,FINSEQ_2:19;
reconsider x = p as object;
take x;
A25: len p + 1 = n+1 by A22,A24,FINSEQ_2:16;
p in T by A1,FINSEQ_1:def 11;
then
A26: p in { w where w is Element of T : len w = n } by A25;
hence x in Tn by TREES_2:def 6;
reconsider x9 = x as Element of Tn by A26,TREES_2:def 6;
ex q be FinSequence st q = x9 & f1.x9 = q^<*1*> by A20;
hence y = f1.x by A21,A23,A24,A25,FINSEQ_1:42;
end;
then
A27: rng f1 = Tn11 by FUNCT_2:10;
A28: for x be Element of Tn ex y be Element of Tn10 st P[x,y]
proof
let x be Element of Tn;
x in T-level n;
then x in { w where w is Element of T : len w = n } by TREES_2:def 6;
then consider p be Element of T such that
A29: p = x and
A30: len p = n;
set y = p^<* 0 *>;
rng <* 0 *> c= {0,1}
proof
let z be object;
assume z in rng <* 0 *>;
then z in {0} by FINSEQ_1:38;
then z = 0 by TARSKI:def 1;
hence thesis by TARSKI:def 2;
end;
then <* 0 *> is FinSequence of {0,1} by FINSEQ_1:def 4;
then p^<* 0 *> is FinSequence of {0,1} by Lm1;
then
A31: y in T by A1,FINSEQ_1:def 11;
len y = n+1 & y.(n+1) = 0 by A30,FINSEQ_1:42,FINSEQ_2:16;
then y in { t where t is Element of T : len t = n+1 & t.(n+1) = 0 } by
A31;
then reconsider y as Element of Tn10;
take y,p;
thus thesis by A29;
end;
consider f0 be Function of Tn,Tn10 such that
A32: for x be Element of Tn holds P[x,f0.x] from FUNCT_2:sch 3(A28);
now
let x1,x2 be object;
assume that
A33: x1 in dom f1 & x2 in dom f1 and
A34: f1.x1 = f1.x2;
reconsider x19= x1, x29= x2 as Element of Tn by A33,FUNCT_2:def 1;
(ex p1 be FinSequence st p1 = x19 & f1.x19 = p1^<*1*> )& ex p2 be
FinSequence st p2 = x29 & f1.x29 = p2^<*1*> by A20;
hence x1 = x2 by A34,FINSEQ_2:17;
end;
then Tn c= dom f1 & f1 is one-to-one by FUNCT_1:def 4,FUNCT_2:def 1;
then Tn,f1.:Tn are_equipotent by CARD_1:33;
then
A35: Tn,rng f1 are_equipotent by RELSET_1:22;
A36: T-level (n+1) c= Tn10 \/ Tn11
proof
let x be object;
assume x in T-level (n+1);
then x in { w where w is Element of T : len w = n+1 } by TREES_2:def 6;
then consider p be Element of T such that
A37: p = x and
A38: len p = n+1;
x in Tn10 or x in Tn11
proof
n+1 in Seg (n+1) by FINSEQ_1:4;
then n+1 in dom p by A38,FINSEQ_1:def 3;
then p.(n+1) in BOOLEAN by FINSEQ_2:11;
then
A39: p.(n+1) = 0 or p.(n+1) = 1 by TARSKI:def 2;
assume not x in Tn10;
hence thesis by A37,A38,A39;
end;
hence thesis by XBOOLE_0:def 3;
end;
now
let y be object;
assume y in Tn10;
then consider t be Element of T such that
A40: t = y and
A41: len t = n+1 and
A42: t.(n+1) = 0;
consider p be FinSequence of BOOLEAN, d be Element of BOOLEAN such that
A43: t = p^<*d*> by A41,FINSEQ_2:19;
reconsider x = p as object;
take x;
A44: len p + 1 = n+1 by A41,A43,FINSEQ_2:16;
p in T by A1,FINSEQ_1:def 11;
then
A45: p in { w where w is Element of T : len w = n } by A44;
hence x in Tn by TREES_2:def 6;
reconsider x9 = x as Element of Tn by A45,TREES_2:def 6;
ex q be FinSequence st q = x9 & f0.x9 = q^<* 0 *> by A32;
hence y = f0.x by A40,A42,A43,A44,FINSEQ_1:42;
end;
then
A46: rng f0 = Tn10 by FUNCT_2:10;
now
let x1,x2 be object;
assume that
A47: x1 in dom f0 & x2 in dom f0 and
A48: f0.x1 = f0.x2;
reconsider x19= x1, x29= x2 as Element of Tn by A47,FUNCT_2:def 1;
(ex p1 be FinSequence st p1 = x19 & f0.x19 = p1^<* 0 *> )& ex p2 be
FinSequence st p2 = x29 & f0.x29 = p2^<* 0 *> by A32;
hence x1 = x2 by A48,FINSEQ_2:17;
end;
then Tn c= dom f0 & f0 is one-to-one by FUNCT_1:def 4,FUNCT_2:def 1;
then Tn,f0.:Tn are_equipotent by CARD_1:33;
then Tn,rng f0 are_equipotent by RELSET_1:22;
then
A49: card Tn = card Tn10 by A46,CARD_1:5;
A50: Tn10 misses Tn11
proof
assume Tn10 /\ Tn11 <> {};
then consider x be object such that
A51: x in Tn10 /\ Tn11 by XBOOLE_0:def 1;
x in Tn11 by A51,XBOOLE_0:def 4;
then
A52: ex p2 be Element of T st p2 = x & len p2 = n+1 & p2.(n+ 1) = 1;
x in Tn10 by A51,XBOOLE_0:def 4;
then ex p1 be Element of T st p1 = x & len p1 = n+1 & p1.(n+ 1) = 0;
hence contradiction by A52;
end;
thus 2 to_power (n+1) = 2 to_power n * 2 to_power 1 by POWER:27
.= 2 * 2 to_power n by POWER:25
.= card Tn + card Tn by A13
.= card Tn10 + card Tn11 by A49,A35,A27,CARD_1:5
.= card (Tn10 \/ Tn11) by A50,CARD_2:40
.= card (T-level (n+1)) by A15,A36,XBOOLE_0:def 10;
end;
card (T-level 0) = card {{}} by TREES_9:44
.= 1 by CARD_1:30
.= 2 to_power 0 by POWER:24;
then
A53: R[0];
thus for n be Nat holds R[n] from NAT_1:sch 2(A53,A2);
end;
theorem Th19:
for T be full Tree for n be non zero Nat holds
len FinSeqLevel(n,T) = 2 to_power n
proof
let T be full Tree;
let n be non zero Nat;
rng FinSeqLevel(n,T) = dom NumberOnLevel(n,T) by FUNCT_1:33
.= T-level n by FUNCT_2:def 1;
then
A1: dom FinSeqLevel(n,T),T-level n are_equipotent by WELLORD2:def 4;
card Seg len FinSeqLevel(n,T) = card dom FinSeqLevel(n,T) by FINSEQ_1:def 3
.= card (T-level n) by A1,CARD_1:5
.= 2 to_power n by Th18;
hence thesis by FINSEQ_1:57;
end;
theorem Th20:
for T be full Tree for n be non zero Nat holds dom
FinSeqLevel(n,T) = Seg (2 to_power n)
proof
let T be full Tree;
let n be non zero Nat;
thus dom FinSeqLevel(n,T) = Seg len FinSeqLevel(n,T) by FINSEQ_1:def 3
.= Seg (2 to_power n) by Th19;
end;
theorem
for T be full Tree for n be non zero Nat holds
rng FinSeqLevel(n,T) = T-level n
proof
let T be full Tree;
let n be non zero Nat;
reconsider Tln = T-level n as finite set;
T = {0,1}* by Def2;
then T-level n is non empty by Th10;
then reconsider
p = FinSeqLevel(n,T) as Function of dom FinSeqLevel(n,T), T-level
n by FINSEQ_2:26;
reconsider dp = dom p as finite set;
card dp = card Seg (2 to_power n) by Th20
.= 2 to_power n by FINSEQ_1:57
.= card Tln by Th18; then
p is onto by FINSEQ_4:63;
hence thesis by FUNCT_2:def 3;
end;
theorem
for T be full Tree holds FinSeqLevel(1,T).1 = <* 0 *>
proof
let T be full Tree;
thus FinSeqLevel(1,T).1 = 0*1 by Th15
.= <* 0 *> by FINSEQ_2:59;
end;
theorem
for T be full Tree holds FinSeqLevel(1,T).2 = <* 1 *>
proof
let T be full Tree;
A1: 0*1 = <* FALSE *> by FINSEQ_2:59;
reconsider t =<* FALSE *> as Element of 1-tuples_on BOOLEAN
by FINSEQ_2:131;
thus FinSeqLevel(1,T).2 = FinSeqLevel(1,T).(2 to_power 1) by POWER:25
.= 'not' t by A1,Th16
.= <* 1 *> by BINARI_3:14;
end;
theorem
for T be full Tree for n,i be non zero Nat st i <= 2
to_power (n+1) for F be Element of n-tuples_on BOOLEAN
st F = FinSeqLevel(n,T).((i+1) div 2
) holds FinSeqLevel(n+1,T).i = F^<*(i+1) mod 2*>
proof
let T be full Tree;
let n,i be non zero Nat;
assume
A1: i <= 2 to_power (n+1);
A2: now
per cases;
suppose
i-'1 is odd;
then
A3: i-'1 mod 2 = 1 by NAT_2:22;
then i-'1 + (1+1)*1 mod 2 = 1 by NAT_D:21;
then i-'1 + 1 + 1 mod 2 = 1;
hence (i+1) mod 2 = (i-'1) mod 2 by A3,NAT_1:14,XREAL_1:235;
end;
suppose
i-'1 is even;
then
A4: i-'1 mod 2 = 0 by NAT_2:21;
then i-'1 + (1 + 1)*1 mod 2 = 0 by NAT_D:21;
then i-'1 + 1 + 1 mod 2 = 0;
hence (i+1) mod 2 = (i-'1) mod 2 by A4,NAT_1:14,XREAL_1:235;
end;
end;
let F be Element of n-tuples_on BOOLEAN;
assume
A5: F = FinSeqLevel(n,T).((i+1) div 2);
A6: 1 <= i by NAT_1:14;
then 1 + 1 <= i + 1 by XREAL_1:6;
then
A7: 1 <= (i+1) div 2 by NAT_2:13;
2 to_power (n+1) = (2 to_power n) * (2 to_power 1) by POWER:27
.= 2 * (2 to_power n) by POWER:25;
then (i+1) div 2 <= 2 to_power n by A1,NAT_2:25;
then
A8: (i+1) div 2 in Seg (2 to_power n) by A7,FINSEQ_1:1;
i + 1 >= 1 + 1 by A6,XREAL_1:6;
then
A9: 1 <= (i + 1) div 2 by NAT_2:13;
A10: (i-'1) div 2 = (i-'1) div 2 + 1 - 1
.= (i-'1 + (1 + 1)) div 2 - 1 by NAT_2:14
.= ((i-'1 + 1 + 1) div 2) - 1
.= ((i + 1) div 2) - 1 by NAT_1:14,XREAL_1:235
.= ((i + 1) div 2) -' 1 by A9,XREAL_1:233;
i in Seg (2 to_power (n+1)) by A1,A6,FINSEQ_1:1;
hence FinSeqLevel(n+1,T).i = Rev ((n+1)-BinarySequence (i-'1)) by Th17
.= Rev (<*(i-'1) mod 2*> ^ (n-BinarySequence ((i-'1) div 2))) by
BINARI_3:34
.= (Rev (n-BinarySequence (((i+1) div 2)-'1)))^<*(i+1) mod 2*> by A2,A10,
FINSEQ_6:24
.= F^<*(i+1) mod 2*> by A5,A8,Th17;
end;