### The Mizar article:

### Full Trees

**by****Robert Milewski**

- Received February 25, 1998
Copyright (c) 1998 Association of Mizar Users

- MML identifier: BINTREE2
- [ MML identifier index ]

environ vocabulary FINSEQ_1, RELAT_1, BINTREE1, TREES_1, MARGREL1, BOOLE, ORDINAL1, FUNCT_1, TREES_2, MIDSP_3, TREES_4, CQC_LANG, MCART_1, FINSEQ_5, BINARITH, CAT_1, EUCLID, FINSET_1, POWER, BINARI_3, ARYTM_1, ZF_LANG, CARD_1, FINSEQ_2, TARSKI, NAT_1, MATRIX_2, BINTREE2, FINSEQ_4; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, MCART_1, REAL_1, NAT_1, ABIAN, SERIES_1, RELAT_1, CARD_1, MARGREL1, DOMAIN_1, FUNCT_1, FUNCT_2, FINSET_1, CQC_LANG, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSEQ_5, BINARITH, BINARI_3, TREES_1, TREES_2, TREES_4, BINTREE1, EUCLID, MIDSP_3; constructors REAL_1, ABIAN, SERIES_1, DOMAIN_1, WELLORD2, TREES_9, CQC_LANG, FINSEQ_5, FINSEQOP, BINARITH, BINARI_3, BINTREE1, EUCLID, FINSEQ_4, INT_1, MEMBERED; clusters SUBSET_1, XREAL_0, RELSET_1, FINSET_1, BINTREE1, TREES_2, TREES_9, BINARITH, MARGREL1, FINSEQ_1, NAT_1, MEMBERED, NUMBERS, ORDINAL2; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, XBOOLE_0; theorems AXIOMS, TARSKI, MCART_1, REAL_1, NAT_1, NAT_2, WELLORD2, MARGREL1, ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_7, CARD_1, ALGSEQ_1, CARD_2, FINSET_1, POWER, CQC_LANG, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSEQ_5, FINSEQ_6, BINARITH, AMI_5, BINARI_3, TREES_1, TREES_2, BINTREE1, QC_LANG4, EUCLID, SCMFSA_7, GR_CY_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, RLVECT_1; schemes FUNCT_2, NAT_1, FINSEQ_2, TREES_2, COMPTS_1; begin :: Trees and Binary Trees 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:23; hence p|Seg n in D* 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; rng <*>NAT = {} by FINSEQ_1:27; then A1: _P[<*>NAT] by XBOOLE_1:2 ; A2: 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 A3: _P[p]; assume A4: p^<*x*> is Element of T; then reconsider p1 = p as Element of T by TREES_1:46; p^<*x*> in { p^<*n*> where n is Nat : p^<*n*> in T } by A4; then A5: p^<*x*> in succ p1 by TREES_2:def 5; then not p in Leaves T by BINTREE1:5; then succ p1 = { p^<* 0 *>, p^<*1*> } by BINTREE1:def 2; then p^<*x*> = p^<* 0 *> or p^<*x*> = p^<*1*> by A5,TARSKI:def 2; then x = 0 or x = 1 by FINSEQ_2:20; then A6: x in {0,1} by TARSKI:def 2; A7: {x} c= BOOLEAN proof let z be set; assume z in {x}; hence z in BOOLEAN by A6,MARGREL1:def 12,TARSKI:def 1; end; rng <*x*> = {x} by FINSEQ_1:55; then (rng p) \/ (rng <*x*>) c= BOOLEAN by A3,A4,A7,TREES_1:46,XBOOLE_1:8; hence rng (p^<*x*>) c= BOOLEAN by FINSEQ_1:44; end; for p be FinSequence of NAT holds _P[p] from IndSeqD(A1,A2); then rng t c= BOOLEAN; hence t is FinSequence of BOOLEAN by FINSEQ_1:def 4; end; definition let T be binary Tree; redefine mode Element of T -> FinSequence of BOOLEAN; 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 set; 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:6; then len t + 1 in Seg len tn by FINSEQ_2:19; then len t + 1 in dom tn by FINSEQ_1:def 3; then tn/.(len t + 1) = (t^<*n*>).(len t + 1) by FINSEQ_4:def 4 .= n by FINSEQ_1:59; then n = 0 or n = 1 by TARSKI:def 2; hence x in { t^<* 0 *>, t^<* 1 *> } by A2,TARSKI:def 2; end; let x be set; A4: t is FinSequence of {0,1} by A1,FINSEQ_1:def 11; rng <* 0 *> c= {0,1} proof let z be set; assume z in rng <* 0 *>; then z in {0} by FINSEQ_1:55; then z = 0 by TARSKI:def 1; hence z in {0,1} by TARSKI:def 2; end; then A5: <* 0 *> is FinSequence of {0,1} by FINSEQ_1:def 4; rng <* 1 *> c= {0,1} proof let z be set; assume z in rng <* 1 *>; then z in {1} by FINSEQ_1:55; then z = 1 by TARSKI:def 1; hence z in {0,1} by TARSKI:def 2; end; then A6: <* 1 *> is FinSequence of {0,1} by FINSEQ_1:def 4; t^<* 0 *> is FinSequence of {0,1} by A4,A5,SCMFSA_7:23; then A7: t^<* 0 *> in T by A1,FINSEQ_1:def 11; t^<* 1 *> is FinSequence of {0,1} by A4,A6,SCMFSA_7:23; then A8: t^<* 1 *> in T by A1,FINSEQ_1:def 11; assume x in { t^<* 0 *>, t^<* 1 *> }; then x = t^<* 0 *> or x = t^<* 1 *> by TARSKI:def 2; hence x in { t^<*n*> where n is Nat : t^<*n*> in T } by A7,A8; end; hence succ t = { t^<* 0 *>, t^<* 1 *> } by TREES_2:def 5; end; hence T is binary by BINTREE1:def 2; end; theorem Th4: for T be Tree st T = {0,1}* holds Leaves T = {} proof let T be Tree; assume A1: T = {0,1}*; assume Leaves T <> {}; then consider x be set such that A2: x in Leaves T by XBOOLE_0:def 1; reconsider x1 = x as Element of T by A2; T is binary by A1,Th3; then A3: x1 is FinSequence of BOOLEAN by Th2; then reconsider x1 = x as FinSequence of NAT; set y1 = x1 ^ <* 0 *>; A4: 0 in {0} by TARSKI:def 1; {0} c= BOOLEAN proof let z be set; assume z in {0}; then z = 0 by TARSKI:def 1; hence z in BOOLEAN by MARGREL1:def 13; end; then <* 0 *> is FinSequence of BOOLEAN by A4,SCMFSA_7:22; then y1 is FinSequence of BOOLEAN by A3,SCMFSA_7:23; then A5: y1 in T by A1,FINSEQ_1:def 11,MARGREL1:def 12; x1 is_a_proper_prefix_of y1 by TREES_1:31; hence contradiction by A2,A5,TREES_1:def 8; 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 Tuple of n,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 t is Tuple of n,BOOLEAN by FINSEQ_2:110; 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 set 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:5; 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 T is binary 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}*; then A2: T is binary by Th3; let t be Element of T; not t in Leaves T by A1,Th4; hence succ t = { t^<* 0 *>, t^<* 1 *> } by A2,BINTREE1:def 2; end; assume A3: 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 set; A4: T is binary by A3,Th7; assume x in T; then x is FinSequence of {0,1} by A4,Th2,MARGREL1:def 12; hence x in {0,1}* by FINSEQ_1:def 11; end; let x be set; assume x in {0,1}*; then A5: x is FinSequence of {0,1} by FINSEQ_1:def 11; defpred _P[FinSequence] means $1 in T; A6: _P[<*> {0,1}] by TREES_1:47; A7: 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}; assume p in T; then reconsider p1 = p as Element of T; A8: succ p1 = { p1^<* 0 *>, p1^<* 1 *> } by A3; n = 0 or n = 1 by TARSKI:def 2; then p^<*n*> in succ p1 by A8,TARSKI:def 2; hence p^<*n*> in T; end; for p be FinSequence of {0,1} holds _P[p] from IndSeqD(A6,A7); hence x in T by A5; end; end; scheme DecoratedBinTreeEx {A() -> non empty set, a() -> Element of A(), P[set,set,set]}: 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[set,set] means ex b,c be Element of A() st P[$1,b,c] & $2 = [b,c]; A2: for e be set st e in A() ex u be set st u in [:A(),A():] & Q[e,u] proof let e be set; 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 Q[e,u] 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 set st e in A() holds Q[e,f.e] from NonUniqBoundFuncEx(A2); deffunc _F(set) = IFEQ($1`2,0,(f.($1`1))`1,(f.($1`1))`2); A7: for x be set st x in [:A(),NAT:] holds _F(x) in A() proof let x be set; assume x in [:A(),NAT:]; then x`1 in A() by MCART_1:10; then f.(x`1) in rng f by A4,FUNCT_1:def 5; then A8: (f.(x`1))`1 in A() & (f.(x`1))`2 in A() by A5,MCART_1:10; now per cases; suppose x`2 = 0; hence IFEQ(x`2,0,(f.(x`1))`1,(f.(x`1))`2) in A() by A8,CQC_LANG:def 1; suppose x`2 <> 0; hence IFEQ(x`2,0,(f.(x`1))`1,(f.(x`1))`2) in A() by A8,CQC_LANG:def 1; end; hence IFEQ(x`2,0,(f.(x`1))`1,(f.(x`1))`2) in A(); end; consider F be Function of [:A(),NAT:],A() such that A9: for x be set st x in [:A(),NAT:] holds F.x = _F(x) from Lambda1(A7); A10: for e be set st e in A() holds P[e,F.[e,0],F.[e,1]] proof let e be set; assume A11: e in A(); then consider b,c be Element of A() such that A12: P[e,b,c] and A13: f.e = [b,c] by A6; A14: [e,0]`2 = 0 by MCART_1:7; [e,0] in [:A(),NAT:] by A11,ZFMISC_1:106; then A15: F.[e,0] = IFEQ([e,0]`2,0,(f.([e,0]`1))`1,(f.([e,0]`1))`2) by A9 .= (f.([e,0]`1))`1 by A14,CQC_LANG:def 1 .= (f.e)`1 by MCART_1:7 .= b by A13,MCART_1:7; A16: [e,1]`2 = 1 & 1 <> 0 by MCART_1:7; [e,1] in [:A(),NAT:] by A11,ZFMISC_1:106; then F.[e,1] = IFEQ([e,1]`2,0,(f.([e,1]`1))`1,(f.([e,1]`1))`2) by A9 .= (f.([e,1]`1))`2 by A16,CQC_LANG:def 1 .= (f.e)`2 by MCART_1:7 .= c by A13,MCART_1:7; hence P[e,F.[e,0],F.[e,1]] by A12,A15; end; deffunc _F(set) = 2; consider D be DecoratedTree of A() such that A17: D.{} = a() and A18: for d be Element of dom D holds succ d = { d^<*k*> where k is Nat : k < _F(D.d) } & for n be Nat, x be set st x = D.d & n < _F(x) holds D.(d^<*n*>) = F.[x,n] from DTreeStructFinEx; 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 set; assume v in { t^<*k*> where k is Nat : k < 2 }; then consider k be Nat such that A19: v = t^<*k*> and A20: k < 2; k = 0 or k = 1 by A20,ALGSEQ_1:4; hence v in { t^<* 0 *>, t^<* 1 *> } by A19,TARSKI:def 2; end; let v be set; assume v in { t^<* 0 *>, t^<* 1 *> }; then v = t^<* 0 *> or v = t^<* 1 *> by TARSKI:def 2; hence v in { t^<*k*> where k is Nat : k < 2 }; end; hence succ t = { t^<* 0 *>, t^<* 1 *> } by A18; 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 set; assume v in { t^<*k*> where k is Nat : k < 2 }; then consider k be Nat such that A21: v = t^<*k*> and A22: k < 2; k = 0 or k = 1 by A22,ALGSEQ_1:4; hence v in { t^<* 0 *>, t^<* 1 *> } by A21,TARSKI:def 2; end; let v be set; assume v in { t^<* 0 *>, t^<* 1 *> }; then v = t^<* 0 *> or v = t^<* 1 *> by TARSKI:def 2; hence v in { t^<*k*> where k is Nat : k < 2 }; end; hence succ t = { t^<* 0 *>, t^<* 1 *> } by A18; end; hence dom D = {0,1}* by Th8; thus D.{} = a() by A17; let x be Node of D; P[D.x,F.[D.x,0],F.[D.x,1]] by A10; then P[D.x,D.(x ^ <* 0 *>),F.[D.x,1]] by A18; hence P[D.x,D.(x ^ <* 0 *>),D.(x ^ <* 1 *>)] by A18; end; scheme DecoratedBinTreeEx1 {A() -> non empty set, a() -> Element of A(), P[set,set], Q[set,set]}: 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 defpred _P[set,set] means ( $1`2 = 0 implies P[$1`1,$2] ) & ( $1`2 = 1 implies Q[$1`1,$2] ); A3: for e be set st e in [:A(),NAT:] ex u be set st u in A() & _P[e,u] proof let e be set; 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,CQC_LANG:def 1; thus e`2 = 1 implies Q[e`1,u] by A5,CQC_LANG:def 1; end; consider F be Function such that A6: dom F = [:A(),NAT:] and A7: rng F c= A() and A8: for e be set st e in [:A(),NAT:] holds _P[e,F.e] from NonUniqBoundFuncEx(A3); reconsider F as Function of [:A(),NAT:],A() by A6,A7,FUNCT_2:4; deffunc _F(set) = 2; consider D be DecoratedTree of A() such that A9: D.{} = a() and A10: for d be Element of dom D holds succ d = { d^<*k*> where k is Nat : k < _F(D.d) } & for n be Nat, x be set st x = D.d & n < _F(x) holds D.(d^<*n*>) = F.[x,n] from DTreeStructFinEx; 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 set; assume v in { t^<*k*> where k is Nat : k < 2 }; then consider k be Nat such that A11: v = t^<*k*> and A12: k < 2; k = 0 or k = 1 by A12,ALGSEQ_1:4; hence v in { t^<* 0 *>, t^<* 1 *> } by A11,TARSKI:def 2; end; let v be set; assume v in { t^<* 0 *>, t^<* 1 *> }; then v = t^<* 0 *> or v = t^<* 1 *> by TARSKI:def 2; hence v in { t^<*k*> where k is Nat : k < 2 }; end; hence succ t = { t^<* 0 *>, t^<* 1 *> } by A10; 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 set; assume v in { t^<*k*> where k is Nat : k < 2 }; then consider k be Nat such that A13: v = t^<*k*> and A14: k < 2; k = 0 or k = 1 by A14,ALGSEQ_1:4; hence v in { t^<* 0 *>, t^<* 1 *> } by A13,TARSKI:def 2; end; let v be set; assume v in { t^<* 0 *>, t^<* 1 *> }; then v = t^<* 0 *> or v = t^<* 1 *> by TARSKI:def 2; hence v in { t^<*k*> where k is Nat : k < 2 }; end; hence succ t = { t^<* 0 *>, t^<* 1 *> } by A10; end; hence dom D = {0,1}* by Th8; thus D.{} = a() by A9; let x be Node of D; [D.x,0]`2 = 0 by MCART_1:7; then P[[D.x,0]`1,F.[D.x,0]] by A8; then P[D.x,F.[D.x,0]] by MCART_1:7; hence P[D.x,D.(x ^ <* 0 *>)] by A10; [D.x,1]`2 = 1 by MCART_1:7; then Q[[D.x,1]`1,F.[D.x,1]] by A8; then Q[D.x,F.[D.x,1]] by MCART_1:7; hence Q[D.x,D.(x ^ <* 1 *>)] by A10; end; Lm1: 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 empty 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 Tuple of n,BOOLEAN st F = Rev t holds it.t = (Absval F) + 1; existence proof defpred _P[set,set] 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 set st e in T-level n ex u be set st u in NAT & _P[e,u] proof let e be set; 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 Tuple of n,BOOLEAN by FINSEQ_2:110; 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 u = (Absval F) + 1; end; consider f be Function such that A4: dom f = T-level n and A5: rng f c= NAT and A6: for e be set st e in T-level n holds _P[e,f.e] from NonUniqBoundFuncEx(A1); reconsider f as Function of T-level n,NAT by A4,A5,FUNCT_2:4; take f; let t be Element of T; assume t in T-level n; then consider t1 be Element of T such that A7: t1 = t and A8: for F be Tuple of n,BOOLEAN st F = Rev t1 holds f.t = (Absval F) + 1 by A6; let F be Tuple of n,BOOLEAN; assume F = Rev t; hence f.t = (Absval F) + 1 by A7,A8; end; uniqueness proof let f1,f2 be Function of T-level n,NAT such that A9: for t be Element of T st t in T-level n for F be Tuple of n,BOOLEAN st F = Rev t holds f1.t = (Absval F) + 1 and A10: for t be Element of T st t in T-level n for F be Tuple of n,BOOLEAN st F = Rev t holds f2.t = (Absval F) + 1; now let x be set; assume A11: 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 A12: t = x and A13: len t = n; len Rev t = n by A13,FINSEQ_5:def 3; then reconsider F = Rev t as Tuple of n,BOOLEAN by FINSEQ_2:110; thus f1.x = (Absval F) + 1 by A9,A11,A12 .= f2.x by A10,A11,A12; end; hence f1 = f2 by FUNCT_2:18; end; end; definition let T be binary Tree; let n be non empty Nat; cluster NumberOnLevel(n,T) -> one-to-one; coherence proof now let x1,x2 be set; 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; len Rev t1 = n by A6,FINSEQ_5:def 3; then reconsider F1 = Rev t1 as Tuple of n,BOOLEAN by FINSEQ_2:110; 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 Tuple of n,BOOLEAN by FINSEQ_2:110; (Absval F1) + 1 = NumberOnLevel(n,T).x1 by A4,A5,Def1 .= (Absval F2) + 1 by A3,A7,A8,Def1; then Absval F1 = Absval F2 by XCMPLX_1:2; then F1 = F2 by BINARI_3:2; hence x1 = x2 by A5,A8,BINARI_3:3; end; hence NumberOnLevel(n,T) is one-to-one by FUNCT_1:def 8; 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: X c= NAT* by FUNCT_7:21; A2: now let p be FinSequence of NAT; assume A3: p in X; thus ProperPrefixes p c= X proof let y be set; assume y in ProperPrefixes p; then consider q be FinSequence such that A4: y = q and A5: q is_a_proper_prefix_of p by TREES_1:def 4; q is_a_prefix_of p by A5,XBOOLE_0:def 8; then consider n be Nat such that A6: q = p|Seg n by TREES_1:def 1; thus y in X by A3,A4,A6,Th1; end; end; now let p be FinSequence of NAT, k,n be Nat; assume that A7: p^<*k*> in X and A8: n <= k; A9: p^<*k*> is FinSequence of {0,1} by A7,FINSEQ_1:def 11; then A10: p is FinSequence of {0,1} & <*k*> is FinSequence of {0,1} by FINSEQ_1:50; reconsider kk = <*k*> as FinSequence of {0,1} by A9,FINSEQ_1:50; 1 in Seg 1 by FINSEQ_1:5; then 1 in dom <*k*> by FINSEQ_1:55; then kk.1 in {0,1} by FINSEQ_2:13; then A11: k in {0,1} by FINSEQ_1:57; now per cases by A11,TARSKI:def 2; suppose k = 0; hence n = 0 or n = 1 by A8,NAT_1:18; suppose A12: k = 1; n = 1 or n = 0 proof assume n <> 1; then n < 0 + 1 by A8,A12,REAL_1:def 5; then n <= 0 by NAT_1:38; hence n = 0 by NAT_1:18; end; hence n = 0 or n = 1; end; then n in {0,1} by TARSKI:def 2; then <*n*> is FinSequence of {0,1} by SCMFSA_7:22; then p^<*n*> is FinSequence of {0,1} by A10,SCMFSA_7:23; hence p^<*n*> in X by FINSEQ_1:def 11; end; hence {0,1}* is Tree by A1,A2,TREES_1:def 5; 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; A2: len 0*n = n by EUCLID:2; 0*n in T by A1,BINARI_3:5,MARGREL1:def 12; then 0*n in { w where w is Element of T : len w = n } by A2; hence 0*n in T-level n by TREES_2:def 6; end; theorem Th11: for T be Tree st T = {0,1}* for n be non empty Nat for y be Tuple of n,BOOLEAN holds y in T-level n proof let T be Tree; assume A1: T = {0,1}*; let n be non empty Nat; let y be Tuple of n,BOOLEAN; A2: len y = n by FINSEQ_2:109; y in T by A1,FINSEQ_1:def 11,MARGREL1:def 12; then y in { w where w is Element of T : len w = n } by A2; hence y in T-level n by TREES_2:def 6; end; definition let T be binary Tree; let n be Nat; cluster T-level n -> finite; coherence by QC_LANG4:19; end; definition cluster full -> binary Tree; coherence proof let T be Tree; assume T is full; then T = {0,1}* by Def2; hence T is binary by Th3; end; end; definition cluster full Tree; existence proof reconsider T = {0,1}* as Tree by Th9; take T; thus T is full by Def2; end; end; theorem Th12: for T be full Tree for n be non empty Nat holds Seg (2 to_power n) c= rng NumberOnLevel(n,T) proof let T be full Tree; let n be non empty Nat; let y be set; 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; set t = Rev (n-BinarySequence (k-'1)); T = {0,1}* by Def2; then A4: t in T by FINSEQ_1:def 11,MARGREL1:def 12; A5: len t = len (n-BinarySequence (k-'1)) by FINSEQ_5:def 3 .= n by FINSEQ_2:109; then t in { w where w is Element of T : len w = n } by A4; 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; len Rev t = n by A5,FINSEQ_5:def 3; then reconsider F = Rev t as Tuple of n,BOOLEAN by FINSEQ_2:110; A8: k - 1 >= 1 - 1 by A2,REAL_1:49; k < 2 to_power n + 1 by A3,NAT_1:38; then k - 1 < 2 to_power n by REAL_1:84; then A9: k-'1 < 2 to_power n by A8,BINARITH:def 3; NumberOnLevel(n,T).t = (Absval F) + 1 by A6,Def1 .= (Absval (n-BinarySequence (k-'1))) + 1 by FINSEQ_6:29 .= k -' 1 + 1 by A9,BINARI_3:36 .= k - 1 + 1 by A8,BINARITH:def 3 .= y by A1,XCMPLX_1:27; hence y in rng NumberOnLevel(n,T) by A7,FUNCT_1:def 5; end; definition let T be full Tree; let n be non empty Nat; func FinSeqLevel(n,T) -> FinSequence of T-level n equals :Def3: NumberOnLevel(n,T)"; coherence proof T = {0,1}* by Def2; then A1: T-level n is non empty by Th10; A2: rng (NumberOnLevel(n,T)") = dom NumberOnLevel(n,T) by FUNCT_1:55 .= T-level n by FUNCT_2:def 1; for y be set holds y in Seg (2 to_power n) iff ex x be set st x in dom NumberOnLevel(n,T) & y = NumberOnLevel(n,T).x proof let y be set; thus y in Seg (2 to_power n) implies ex x be set st x in dom NumberOnLevel(n,T) & y = NumberOnLevel(n,T).x proof assume A3: y in Seg (2 to_power n); take x = (NumberOnLevel(n,T)").y; Seg (2 to_power n) c= rng NumberOnLevel(n,T) by Th12; hence x in dom NumberOnLevel(n,T) & y = NumberOnLevel(n,T).x by A3,FUNCT_1:54; end; given x be set such that A4: x in dom NumberOnLevel(n,T) and A5: y = NumberOnLevel(n,T).x; A6: x in T-level n by A4,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 A7: t = x and A8: len t = n; len Rev t = n by A8,FINSEQ_5:def 3; then reconsider F = Rev t as Tuple of n,BOOLEAN by FINSEQ_2:110; A9: y = (Absval F) + 1 by A5,A6,A7,Def1; A10: 1 <= (Absval F) + 1 by NAT_1:29; Absval F < 2 to_power n by BINARI_3:1; then (Absval F) + 1 <= 2 to_power n by NAT_1:38; hence y in Seg (2 to_power n) by A9,A10,FINSEQ_1:3; end; then rng NumberOnLevel(n,T) = Seg (2 to_power n) by FUNCT_1:def 5; then dom (NumberOnLevel(n,T)") = Seg (2 to_power n) by FUNCT_1:55; then NumberOnLevel(n,T)" is Function of Seg (2 to_power n), T-level n by A2,FUNCT_2:4; hence NumberOnLevel(n,T)" is FinSequence of T-level n by A1,FINSEQ_2:28; end; end; definition let T be full Tree; let n be non empty Nat; cluster FinSeqLevel(n,T) -> one-to-one; coherence proof NumberOnLevel(n,T)" is one-to-one by FUNCT_1:62; hence FinSeqLevel(n,T) is one-to-one by Def3; end; end; theorem Th13: for T be full Tree for n be non empty Nat holds NumberOnLevel(n,T).(0*n) = 1 proof let T be full Tree; A1: T = {0,1}* by Def2; let n be non empty Nat; A2: 0*n is Element of T by A1,BINARI_3:5,MARGREL1:def 12; A3: 0*n in T-level n by A1,Th10; A4: Rev (0*n) is FinSequence of BOOLEAN by A2,Lm1; len Rev (0*n) = len 0*n by FINSEQ_5:def 3 .= n by EUCLID:2; then reconsider F = Rev (0*n) as Tuple of n,BOOLEAN by A4,FINSEQ_2:110; A5: Rev (0*n) = 0*n by BINARI_3:9; thus NumberOnLevel(n,T).(0*n) = (Absval F) + 1 by A3,Def1 .= 0 + 1 by A5,BINARI_3:7 .= 1; end; theorem Th14: for T be full Tree for n be non empty Nat for y be Tuple of n,BOOLEAN st y = 0*n holds NumberOnLevel(n,T).'not' y = 2 to_power n proof let T be full Tree; A1: T = {0,1}* by Def2; let n be non empty Nat; let y be Tuple of n,BOOLEAN; assume A2: y = 0*n; A3: 'not' y in T-level n by A1,Th11; len Rev 'not' y = len 'not' y by FINSEQ_5:def 3 .= n by FINSEQ_2:109; then reconsider F = Rev 'not' y as Tuple of n,BOOLEAN by FINSEQ_2:110; A4: Rev 'not' y = 'not' y by A2,BINARI_3:10; thus NumberOnLevel(n,T).'not' y = (Absval F) + 1 by A3,Def1 .= 2 to_power n - 1 + 1 by A2,A4,BINARI_3:8 .= 2 to_power n by XCMPLX_1:27; end; theorem Th15: for T be full Tree for n be non empty Nat holds FinSeqLevel(n,T).1 = 0*n proof let T be full Tree; A1: T = {0,1}* by Def2; let n be non empty Nat; 0*n in T-level n by A1,Th10; then A2: 0*n in dom NumberOnLevel(n,T) by FUNCT_2:def 1; A3: 1 = NumberOnLevel(n,T).(0*n) by Th13; thus FinSeqLevel(n,T).1 = NumberOnLevel(n,T)".1 by Def3 .= 0*n by A2,A3,FUNCT_1:54; end; theorem Th16: for T be full Tree for n be non empty Nat for y be Tuple of n,BOOLEAN st y = 0*n holds FinSeqLevel(n,T).(2 to_power n) = 'not' y proof let T be full Tree; A1: T = {0,1}* by Def2; let n be non empty Nat; let y be Tuple of n,BOOLEAN; assume A2: y = 0*n; 'not' y in T-level n by A1,Th11; then A3: 'not' y in dom NumberOnLevel(n,T) by FUNCT_2:def 1; A4: 2 to_power n = NumberOnLevel(n,T).'not' y by A2,Th14; thus FinSeqLevel(n,T).(2 to_power n) = NumberOnLevel(n,T)".(2 to_power n) by Def3 .= 'not' y by A3,A4,FUNCT_1:54; end; theorem Th17: for T be full Tree for n be non empty 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 empty Nat; let i be Nat; assume i in Seg (2 to_power n); then A1: 1 <= i & i <= 2 to_power n by FINSEQ_1:3; set nB = n-BinarySequence (i-'1); A2: len Rev nB = len nB by FINSEQ_5:def 3 .= n by FINSEQ_2:109; then reconsider RnB = Rev nB as Tuple of n,BOOLEAN by FINSEQ_2:110; RnB in {0,1}* by FINSEQ_1:def 11,MARGREL1:def 12; then RnB is Element of T by Def2; then RnB in { t where t is Element of T : len t = n } by A2; then A3: RnB in T-level n by TREES_2:def 6; nB = Rev RnB by FINSEQ_6:29; then A4: NumberOnLevel(n,T).RnB = (Absval nB) + 1 by A3,Def1; A5: RnB in dom NumberOnLevel(n,T) by A3,FUNCT_2:def 1; i < 2 to_power n + 1 by A1,NAT_1:38; then i - 1 < 2 to_power n by REAL_1:84; then i-'1 < 2 to_power n by A1,SCMFSA_7:3; then A6: (Absval nB) + 1 = i-'1 + 1 by BINARI_3:36 .= i - 1 + 1 by A1,SCMFSA_7:3 .= i by XCMPLX_1:27; thus FinSeqLevel(n,T).i = NumberOnLevel(n,T)".i by Def3 .= Rev (n-BinarySequence (i-'1)) by A4,A5,A6,FUNCT_1:54; 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; A1: T = {0,1}* by Def2; defpred _R[Nat] means Card (T-level $1) = 2 to_power $1; Card (T-level 0) = card {{}} by QC_LANG4:17 .= 1 by CARD_1:79 .= 2 to_power 0 by POWER:29; then A2: _R[0]; A3: for n be Nat st _R[n] holds _R[n+1] proof let n be Nat; assume A4: Card (T-level n) = 2 to_power n; set Tn1_0 = { p where p is Element of T : len p = n+1 & p.(n+1) = 0 }; set Tn1_1 = { p where p is Element of T : len p = n+1 & p.(n+1) = 1 }; A5: len 0*(n+1) = n+1 by EUCLID:2; A6: 0*(n+1) in T by A1,BINARI_3:5,MARGREL1:def 12; A7: n+1 in Seg (n+1) by FINSEQ_1:6; (0*(n+1)).(n+1) = ((n+1) |-> (0 qua Real)).(n+1) by EUCLID:def 4 .= 0 by A7,FINSEQ_2:70; then A8: 0*(n+1) in Tn1_0 by A5,A6; A9: len (0*n^<*1*>) = len 0*n + 1 by FINSEQ_2:19 .= n+1 by EUCLID:2; 0*n in {0,1}* by BINARI_3:5,MARGREL1:def 12; then A10: 0*n is FinSequence of {0,1} by FINSEQ_1:def 11; rng <*1*> c= {0,1} proof let z be set; assume z in rng <*1*>; then z in {1} by FINSEQ_1:55; then z = 1 by TARSKI:def 1; hence z in {0,1} by TARSKI:def 2; end; then A11: <*1*> is FinSequence of {0,1} by FINSEQ_1:def 4; then 0*n^<*1*> is FinSequence of {0,1} by A10,SCMFSA_7:23; then A12: 0*n^<*1*> in T by A1,FINSEQ_1:def 11; len 0*n = n by EUCLID:2; then (0*n^<*1*>).(n+1) = 1 by FINSEQ_1:59; then A13: 0*n^<*1*> in Tn1_1 by A9,A12; A14: Tn1_0 c= T-level (n+1) proof let x be set; assume x in Tn1_0; then consider p be Element of T such that A15: p = x and A16: len p = n+1 and p.(n+1) = 0; p in { w where w is Element of T : len w = n+1 } by A16; hence x in T-level (n+1) by A15,TREES_2:def 6; end; A17: Tn1_1 c= T-level (n+1) proof let x be set; assume x in Tn1_1; then consider p be Element of T such that A18: p = x and A19: len p = n+1 and p.(n+1) = 1; p in { w where w is Element of T : len w = n+1 } by A19; hence x in T-level (n+1) by A18,TREES_2:def 6; end; then reconsider Tn1_0,Tn1_1 as non empty finite set by A8,A13,A14,FINSET_1:13; A20: Tn1_0 \/ Tn1_1 c= T-level (n+1) by A14,A17,XBOOLE_1:8; A21: T-level (n+1) c= Tn1_0 \/ Tn1_1 proof let x be set; 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 A22: p = x and A23: len p = n+1; x in Tn1_0 or x in Tn1_1 proof assume A24: not x in Tn1_0; n+1 in Seg (n+1) by FINSEQ_1:6; then n+1 in dom p by A23,FINSEQ_1:def 3; then p.(n+1) in BOOLEAN by FINSEQ_2:13; then p.(n+1) = 0 or p.(n+1) = 1 by MARGREL1:def 12,TARSKI:def 2; hence x in Tn1_1 by A22,A23,A24; end; hence x in Tn1_0 \/ Tn1_1 by XBOOLE_0:def 2; end; A25: Tn1_0 misses Tn1_1 proof assume Tn1_0 /\ Tn1_1 <> {}; then consider x be set such that A26: x in Tn1_0 /\ Tn1_1 by XBOOLE_0:def 1; A27: x in Tn1_0 & x in Tn1_1 by A26,XBOOLE_0:def 3; then consider p1 be Element of T such that A28: p1 = x and len p1 = n+1 and A29: p1.(n+1) = 0; consider p2 be Element of T such that A30: p2 = x and len p2 = n+1 and A31: p2.(n+1) = 1 by A27; thus contradiction by A28,A29,A30,A31; end; reconsider Tn = T-level n as finite non empty set by A1,Th10; defpred _P[set,set] means ex p be FinSequence st p = $1 & $2 = p^<* 0 *>; A32: for x be Element of Tn ex y be Element of Tn1_0 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 A33: p = x and A34: len p = n; set y = p^<* 0 *>; rng <* 0 *> c= {0,1} proof let z be set; assume z in rng <* 0 *>; then z in {0} by FINSEQ_1:55; then z = 0 by TARSKI:def 1; hence z in {0,1} 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 MARGREL1:def 12,SCMFSA_7:23; then A35: y in T by A1,FINSEQ_1:def 11; A36: len y = n+1 by A34,FINSEQ_2:19; y.(n+1) = 0 by A34,FINSEQ_1:59; then y in { t where t is Element of T : len t = n+1 & t.(n+1) = 0 } by A35,A36; then reconsider y as Element of Tn1_0; take y,p; thus thesis by A33; end; defpred _P1[set,set] means ex p be FinSequence st p = $1 & $2 = p^<* 1 *>; A37: for x be Element of Tn ex y be Element of Tn1_1 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 A38: p = x and A39: len p = n; set y = p^<*1*>; p^<*1*> is FinSequence of {0,1} by A11,MARGREL1:def 12,SCMFSA_7:23; then A40: y in T by A1,FINSEQ_1:def 11; A41: len y = n+1 by A39,FINSEQ_2:19; y.(n+1) = 1 by A39,FINSEQ_1:59; then y in { t where t is Element of T : len t = n+1 & t.(n+1) = 1 } by A40,A41; then reconsider y as Element of Tn1_1; take y,p; thus thesis by A38; end; consider f0 be Function of Tn,Tn1_0 such that A42: for x be Element of Tn holds _P[x,f0.x] from FuncExD(A32); consider f1 be Function of Tn,Tn1_1 such that A43: for x be Element of Tn holds _P1[x,f1.x] from FuncExD(A37); A44: Tn c= dom f0 by FUNCT_2:def 1; now let x1,x2 be set; assume that A45: x1 in dom f0 and A46: x2 in dom f0 and A47: f0.x1 = f0.x2; reconsider x1'= x1, x2'= x2 as Element of Tn by A45,A46,FUNCT_2:def 1; consider p1 be FinSequence such that A48: p1 = x1' and A49: f0.x1' = p1^<* 0 *> by A42; consider p2 be FinSequence such that A50: p2 = x2' and A51: f0.x2' = p2^<* 0 *> by A42; thus x1 = x2 by A47,A48,A49,A50,A51,FINSEQ_2:20; end; then f0 is one-to-one by FUNCT_1:def 8; then Tn,f0.:Tn are_equipotent by A44,CARD_1:60; then A52: Tn,rng f0 are_equipotent by FUNCT_2:45; now let y be set; assume y in Tn1_0; then consider t be Element of T such that A53: t = y and A54: len t = n+1 and A55: t.(n+1) = 0; consider p be FinSequence of BOOLEAN, d be Element of BOOLEAN such that A56: t = p^<*d*> by A54,FINSEQ_2:22; A57: len p + 1 = n+1 by A54,A56,FINSEQ_2:19; then A58: len p = n by XCMPLX_1:2; reconsider x = p as set; take x; p in T by A1,FINSEQ_1:def 11,MARGREL1:def 12; then A59: p in { w where w is Element of T : len w = n } by A58; hence x in Tn by TREES_2:def 6; reconsider x' = x as Element of Tn by A59,TREES_2:def 6; consider q be FinSequence such that A60: q = x' and A61: f0.x' = q^<* 0 *> by A42; thus y = f0.x by A53,A55,A56,A57,A60,A61,FINSEQ_1:59; end; then rng f0 = Tn1_0 by FUNCT_2:16; then A62: card Tn = card Tn1_0 by A52,CARD_1:81; A63: Tn c= dom f1 by FUNCT_2:def 1; now let x1,x2 be set; assume that A64: x1 in dom f1 and A65: x2 in dom f1 and A66: f1.x1 = f1.x2; reconsider x1'= x1, x2'= x2 as Element of Tn by A64,A65,FUNCT_2:def 1; consider p1 be FinSequence such that A67: p1 = x1' and A68: f1.x1' = p1^<*1*> by A43; consider p2 be FinSequence such that A69: p2 = x2' and A70: f1.x2' = p2^<*1*> by A43; thus x1 = x2 by A66,A67,A68,A69,A70,FINSEQ_2:20; end; then f1 is one-to-one by FUNCT_1:def 8; then Tn,f1.:Tn are_equipotent by A63,CARD_1:60; then A71: Tn,rng f1 are_equipotent by FUNCT_2:45; now let y be set; assume y in Tn1_1; then consider t be Element of T such that A72: t = y and A73: len t = n+1 and A74: t.(n+1) = 1; consider p be FinSequence of BOOLEAN, d be Element of BOOLEAN such that A75: t = p^<*d*> by A73,FINSEQ_2:22; A76: len p + 1 = n+1 by A73,A75,FINSEQ_2:19; then A77: len p = n by XCMPLX_1:2; reconsider x = p as set; take x; p in T by A1,FINSEQ_1:def 11,MARGREL1:def 12; then A78: p in { w where w is Element of T : len w = n } by A77; hence x in Tn by TREES_2:def 6; reconsider x' = x as Element of Tn by A78,TREES_2:def 6; consider q be FinSequence such that A79: q = x' and A80: f1.x' = q^<*1*> by A43; thus y = f1.x by A72,A74,A75,A76,A79,A80,FINSEQ_1:59; end; then A81: rng f1 = Tn1_1 by FUNCT_2:16; thus 2 to_power (n+1) = 2 to_power n * 2 to_power 1 by POWER:32 .= 2 * 2 to_power n by POWER:30 .= card Tn + card Tn by A4,XCMPLX_1:11 .= card Tn1_0 + card Tn1_1 by A62,A71,A81,CARD_1:81 .= card (Tn1_0 \/ Tn1_1) by A25,CARD_2:53 .= Card (T-level (n+1)) by A20,A21,XBOOLE_0:def 10; end; thus for n be Nat holds _R[n] from Ind(A2,A3); end; theorem Th19: for T be full Tree for n be non empty Nat holds len FinSeqLevel(n,T) = 2 to_power n proof let T be full Tree; let n be non empty Nat; rng FinSeqLevel(n,T) = rng (NumberOnLevel(n,T)") by Def3 .= dom NumberOnLevel(n,T) by FUNCT_1:55 .= 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:21 .= 2 to_power n by Th18; hence thesis by FINSEQ_1:78; end; theorem Th20: for T be full Tree for n be non empty Nat holds dom FinSeqLevel(n,T) = Seg (2 to_power n) proof let T be full Tree; let n be non empty 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 empty Nat holds rng FinSeqLevel(n,T) = T-level n proof let T be full Tree; A1: T = {0,1}* by Def2; let n be non empty Nat; T-level n is non empty by A1,Th10; then reconsider p = FinSeqLevel(n,T) as Function of dom FinSeqLevel(n,T), T-level n by FINSEQ_2:30; Seg len FinSeqLevel(n,T) is finite; then reconsider dp = dom p as finite set by FINSEQ_1:def 3; reconsider Tln = T-level n as finite set; card dp = Card Seg (2 to_power n) by Th20 .= 2 to_power n by FINSEQ_1:78 .= card Tln by Th18; hence rng FinSeqLevel(n,T) = T-level n by FINSEQ_4:78; 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 .= 1 |-> (0 qua Real) by EUCLID:def 4 .= <* 0 *> by FINSEQ_2:73; end; theorem for T be full Tree holds FinSeqLevel(1,T).2 = <* 1 *> proof let T be full Tree; A1: 0*1 = 1 |-> (0 qua Real) by EUCLID:def 4 .= <* FALSE *> by FINSEQ_2:73,MARGREL1:36; thus FinSeqLevel(1,T).2 = FinSeqLevel(1,T).(2 to_power 1) by POWER:30 .= <* 1 *> by A1,Th16,BINARI_3:15,MARGREL1:36; end; theorem for T be full Tree for n,i be non empty Nat st i <= 2 to_power (n+1) for F be Tuple of n,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 empty Nat; assume A1: i <= 2 to_power (n+1); let F be Tuple of n,BOOLEAN; assume A2: F = FinSeqLevel(n,T).((i+1) div 2); A3: 1 <= i by RLVECT_1:99; then 1 + 1 <= i + 1 by AXIOMS:24; then A4: 1 <= (i+1) div 2 by NAT_2:15; 2 to_power (n+1) = (2 to_power n) * (2 to_power 1) by POWER:32 .= 2 * (2 to_power n) by POWER:30; then (i+1) div 2 <= 2 to_power n by A1,NAT_2:27; then A5: (i+1) div 2 in Seg (2 to_power n) by A4,FINSEQ_1:3; A6: now per cases; suppose i-'1 is odd; then A7: i-'1 mod 2 = 1 by NAT_2:24; then i-'1 + (1+1)*1 mod 2 = 1 by GR_CY_1:1; then i-'1 + 1 + 1 mod 2 = 1 by XCMPLX_1:1; hence (i+1) mod 2 = (i-'1) mod 2 by A3,A7,AMI_5:4; suppose i-'1 is even; then A8: i-'1 mod 2 = 0 by NAT_2:23; then i-'1 + (1 + 1)*1 mod 2 = 0 by GR_CY_1:1; then i-'1 + 1 + 1 mod 2 = 0 by XCMPLX_1:1; hence (i+1) mod 2 = (i-'1) mod 2 by A3,A8,AMI_5:4; end; i + 1 >= 1 + 1 by A3,AXIOMS:24; then A9: 1 <= (i + 1) div 2 by NAT_2:15; A10: (i-'1) div 2 = (i-'1) div 2 + 1 - 1 by XCMPLX_1:26 .= (i-'1 + (1 + 1)) div 2 - 1 by NAT_2:16 .= ((i-'1 + 1 + 1) div 2) - 1 by XCMPLX_1:1 .= ((i + 1) div 2) - 1 by A3,AMI_5:4 .= ((i + 1) div 2) -' 1 by A9,SCMFSA_7:3; i in Seg (2 to_power (n+1)) by A1,A3,FINSEQ_1:3; 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:35 .= (Rev (n-BinarySequence (((i+1) div 2)-'1)))^<*(i+1) mod 2*> by A6,A10,FINSEQ_6:28 .= F^<*(i+1) mod 2*> by A2,A5,Th17; end;

Back to top