The abstract of the Mizar article:

Full Trees

by

Robert Milewski

Received February 25, 1998

MML identifier: BINTREE2

[ Mizar article, 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;


begin :: Trees and Binary Trees

  theorem :: BINTREE2:1
   for D be set
   for p be FinSequence
   for n be Nat holds
    p in D* implies p|Seg n in D*;

  theorem :: BINTREE2:2
   for T be binary Tree
   for t be Element of T holds
    t is FinSequence of BOOLEAN;

  definition
   let T be binary Tree;
   redefine mode Element of T -> FinSequence of BOOLEAN;
  end;

  theorem :: BINTREE2:3
   for T be Tree st T = {0,1}* holds
    T is binary;

  theorem :: BINTREE2:4
   for T be Tree st T = {0,1}* holds
    Leaves T = {};

  theorem :: BINTREE2:5
     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;

  theorem :: BINTREE2:6
     for T be Tree st
    for t be Element of T holds succ t = { t^<* 0 *>, t^<* 1 *> } holds
     Leaves T = {};

  theorem :: BINTREE2:7
   for T be Tree st
    for t be Element of T holds succ t = { t^<* 0 *>, t^<* 1 *> } holds
     T is binary;

  theorem :: BINTREE2:8
   for T be Tree holds
    T = {0,1}* iff
    for t be Element of T holds succ t = { t^<* 0 *>, t^<* 1 *> };

  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
     for a be Element of A() ex b,c be Element of A() st P[a,b,c];

  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
     for a be Element of A() ex b be Element of A() st P[a,b] and
     for a be Element of A() ex b be Element of A() st Q[a,b];

  definition
   let T be binary Tree;
   let n be non empty Nat;
   func NumberOnLevel(n,T) -> Function of T-level n,NAT means
:: BINTREE2:def 1
    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;
  end;

  definition
   let T be binary Tree;
   let n be non empty Nat;
   cluster NumberOnLevel(n,T) -> one-to-one;
  end;

begin :: Full Trees

  definition
   let T be Tree;
   attr T is full means
:: BINTREE2:def 2
    T = {0,1}*;
  end;

  theorem :: BINTREE2:9
   {0,1}* is Tree;

  theorem :: BINTREE2:10
   for T be Tree st T = {0,1}*
   for n be Nat holds
    0*n in T-level n;

  theorem :: BINTREE2:11
   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;

  definition
   let T be binary Tree;
   let n be Nat;
   cluster T-level n -> finite;
  end;

  definition
   cluster full -> binary Tree;
  end;

  definition
   cluster full Tree;
  end;

  theorem :: BINTREE2:12
   for T be full Tree
   for n be non empty Nat holds
    Seg (2 to_power n) c= rng NumberOnLevel(n,T);

  definition
   let T be full Tree;
   let n be non empty Nat;
   func FinSeqLevel(n,T) -> FinSequence of T-level n equals
:: BINTREE2:def 3
    NumberOnLevel(n,T)";
  end;

  definition
   let T be full Tree;
   let n be non empty Nat;
   cluster FinSeqLevel(n,T) -> one-to-one;
  end;

  theorem :: BINTREE2:13
   for T be full Tree
   for n be non empty Nat holds
    NumberOnLevel(n,T).(0*n) = 1;

  theorem :: BINTREE2:14
   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;

  theorem :: BINTREE2:15
   for T be full Tree
   for n be non empty Nat holds
    FinSeqLevel(n,T).1 = 0*n;

  theorem :: BINTREE2:16
   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;

  theorem :: BINTREE2:17
   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));

  theorem :: BINTREE2:18
   for T be full Tree
   for n be Nat holds
    Card (T-level n) = 2 to_power n;

  theorem :: BINTREE2:19
   for T be full Tree
   for n be non empty Nat holds
    len FinSeqLevel(n,T) = 2 to_power n;

  theorem :: BINTREE2:20
   for T be full Tree
   for n be non empty Nat holds
    dom FinSeqLevel(n,T) = Seg (2 to_power n);

  theorem :: BINTREE2:21
     for T be full Tree
   for n be non empty Nat holds
    rng FinSeqLevel(n,T) = T-level n;

  theorem :: BINTREE2:22
     for T be full Tree holds
    FinSeqLevel(1,T).1 = <* 0 *>;

  theorem :: BINTREE2:23
     for T be full Tree holds
    FinSeqLevel(1,T).2 = <* 1 *>;

  theorem :: BINTREE2:24
     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*>;