The abstract of the Mizar article:

Sets and Functions of Trees and Joining Operations of Trees

by

Grzegorz Bancerek

Received November 27, 1992

MML identifier: TREES_3

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_1, FUNCT_1, RELAT_1, FINSET_1, MCART_1, TREES_1, TREES_2,
      BOOLE, FUNCT_2, TARSKI, FINSEQ_2, FUNCOP_1, FUNCT_6, PARTFUN1, FUNCT_3,
      ARYTM_1, SQUARE_1, TREES_3;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0,
      NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSET_1, DOMAIN_1, SQUARE_1,
      FUNCOP_1, RELSET_1, FUNCT_2, FUNCT_3, FINSEQ_2, TREES_1, TREES_2,
      FUNCT_6;
 constructors FUNCT_5, NAT_1, DOMAIN_1, SQUARE_1, FUNCT_3, FINSEQ_2, TREES_2,
      FUNCT_6, MEMBERED, XBOOLE_0;
 clusters SUBSET_1, FINSEQ_1, TREES_1, TREES_2, FINSET_1, RELSET_1, CARD_1,
      XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2, NUMBERS;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin :: Finite sets

 reserve x,y,z for set, i,k,n for Nat, p,q,r,s for FinSequence,
  w for FinSequence of NAT, X,Y for set, f for Function;

begin :: Sets of trees

definition
 func Trees -> set means
:: TREES_3:def 1
   x in it iff x is Tree;
end;

definition
 cluster Trees -> non empty;
end;

definition
 func FinTrees -> Subset of Trees means
:: TREES_3:def 2

  x in it iff x is finite Tree;
end;

definition
 cluster FinTrees -> non empty;
end;

definition let IT be set;
 attr IT is constituted-Trees means
:: TREES_3:def 3

  for x st x in IT holds x is Tree;
 attr IT is constituted-FinTrees means
:: TREES_3:def 4

  for x st x in IT holds x is finite Tree;
 attr IT is constituted-DTrees means
:: TREES_3:def 5

  for x st x in IT holds x is DecoratedTree;
end;

theorem :: TREES_3:1
   X is constituted-Trees iff X c= Trees;

theorem :: TREES_3:2
   X is constituted-FinTrees iff X c= FinTrees;

theorem :: TREES_3:3
 X is constituted-Trees & Y is constituted-Trees iff X \/
 Y is constituted-Trees;

theorem :: TREES_3:4
   X is constituted-Trees & Y is constituted-Trees implies
   X \+\ Y is constituted-Trees;

theorem :: TREES_3:5
   X is constituted-Trees implies X /\ Y is constituted-Trees &
   Y /\ X is constituted-Trees & X \ Y is constituted-Trees;

theorem :: TREES_3:6
 X is constituted-FinTrees & Y is constituted-FinTrees iff
   X \/ Y is constituted-FinTrees;

theorem :: TREES_3:7
   X is constituted-FinTrees & Y is constituted-FinTrees implies
   X \+\ Y is constituted-FinTrees;

theorem :: TREES_3:8
   X is constituted-FinTrees implies X /\ Y is constituted-FinTrees &
   Y /\ X is constituted-FinTrees & X \ Y is constituted-FinTrees;

theorem :: TREES_3:9
 X is constituted-DTrees & Y is constituted-DTrees iff
   X \/ Y is constituted-DTrees;

theorem :: TREES_3:10
   X is constituted-DTrees & Y is constituted-DTrees implies
   X \+\ Y is constituted-DTrees;

theorem :: TREES_3:11
   X is constituted-DTrees implies X /\ Y is constituted-DTrees &
   Y /\ X is constituted-DTrees & X \ Y is constituted-DTrees;

theorem :: TREES_3:12
 {} is constituted-Trees constituted-FinTrees constituted-DTrees;

theorem :: TREES_3:13
 {x} is constituted-Trees iff x is Tree;

theorem :: TREES_3:14
 {x} is constituted-FinTrees iff x is finite Tree;

theorem :: TREES_3:15
 {x} is constituted-DTrees iff x is DecoratedTree;

theorem :: TREES_3:16
 {x,y} is constituted-Trees iff x is Tree & y is Tree;

theorem :: TREES_3:17
 {x,y} is constituted-FinTrees iff x is finite Tree & y is finite Tree;

theorem :: TREES_3:18
 {x,y} is constituted-DTrees iff x is DecoratedTree & y is DecoratedTree;

theorem :: TREES_3:19
   X is constituted-Trees & Y c= X implies Y is constituted-Trees;

theorem :: TREES_3:20
   X is constituted-FinTrees & Y c= X implies Y is constituted-FinTrees;

theorem :: TREES_3:21
   X is constituted-DTrees & Y c= X implies Y is constituted-DTrees;

definition
 cluster finite constituted-Trees constituted-FinTrees non empty set;
 cluster finite constituted-DTrees non empty set;
end;

definition
 cluster constituted-FinTrees -> constituted-Trees set;
end;

definition let X be constituted-Trees set;
 cluster -> constituted-Trees Subset of X;
end;

definition let X be constituted-FinTrees set;
 cluster -> constituted-FinTrees Subset of X;
end;

definition let X be constituted-DTrees set;
 cluster -> constituted-DTrees Subset of X;
end;

definition
 let D be constituted-Trees non empty set;
 redefine mode Element of D -> Tree;
end;

definition
 let D be constituted-FinTrees non empty set;
 redefine mode Element of D -> finite Tree;
end;

definition
 let D be constituted-DTrees non empty set;
 redefine mode Element of D -> DecoratedTree;
end;

definition
 cluster Trees -> constituted-Trees;
end;

definition
 cluster constituted-FinTrees non empty Subset of Trees;
end;

definition
 cluster FinTrees -> constituted-FinTrees;
end;

definition let D be non empty set;
 mode DTree-set of D -> set means
:: TREES_3:def 6

  for x st x in it holds x is DecoratedTree of D;
end;

definition let D be non empty set;
 cluster -> constituted-DTrees DTree-set of D;
end;

definition let D be non empty set;
 cluster finite non empty DTree-set of D;
end;

definition let D be non empty set, E be non empty DTree-set of D;
 redefine mode Element of E -> DecoratedTree of D;
end;

definition let T be Tree, D be non empty set;
 redefine func Funcs(T,D) -> non empty DTree-set of D;
 mode Relation of T,D -> ParametrizedSubset of D;
end;

definition let T be Tree, D be non empty set;
 cluster -> DecoratedTree-like Function of T,D;
end;

 definition
  let D be non empty set;
  func Trees(D) -> DTree-set of D means
:: TREES_3:def 7

   for T being DecoratedTree of D holds T in it;
 end;

 definition
  let D be non empty set;
  cluster Trees(D) -> non empty;
 end;

 definition let D be non empty set;
  func FinTrees(D) -> DTree-set of D means
:: TREES_3:def 8
   for T being DecoratedTree of D holds dom T is finite iff T in it;
 end;

 definition let D be non empty set;
  cluster FinTrees D -> non empty;
  end;

theorem :: TREES_3:22
   for D being non empty set holds FinTrees D c= Trees D;

begin :: Functions yielding trees

definition let IT be Function;
 attr IT is Tree-yielding means
:: TREES_3:def 9

  rng IT is constituted-Trees;
 attr IT is FinTree-yielding means
:: TREES_3:def 10

  rng IT is constituted-FinTrees;
 attr IT is DTree-yielding means
:: TREES_3:def 11

  rng IT is constituted-DTrees;
end;

theorem :: TREES_3:23
 {} is Tree-yielding FinTree-yielding DTree-yielding;

theorem :: TREES_3:24
 f is Tree-yielding iff for x st x in dom f holds f.x is Tree;

theorem :: TREES_3:25
   f is FinTree-yielding iff for x st x in dom f holds f.x is finite Tree;

theorem :: TREES_3:26
 f is DTree-yielding iff for x st x in dom f holds f.x is DecoratedTree;

theorem :: TREES_3:27
 p is Tree-yielding & q is Tree-yielding iff p^q is Tree-yielding;

theorem :: TREES_3:28
 p is FinTree-yielding & q is FinTree-yielding iff p^q is FinTree-yielding;

theorem :: TREES_3:29
 p is DTree-yielding & q is DTree-yielding iff p^q is DTree-yielding;

theorem :: TREES_3:30
 <*x*> is Tree-yielding iff x is Tree;

theorem :: TREES_3:31
 <*x*> is FinTree-yielding iff x is finite Tree;

theorem :: TREES_3:32
 <*x*> is DTree-yielding iff x is DecoratedTree;

theorem :: TREES_3:33
 <*x,y*> is Tree-yielding iff x is Tree & y is Tree;

theorem :: TREES_3:34
 <*x,y*> is FinTree-yielding iff x is finite Tree & y is finite Tree;

theorem :: TREES_3:35
 <*x,y*> is DTree-yielding iff x is DecoratedTree & y is DecoratedTree;

theorem :: TREES_3:36
 i <> 0 implies (i |-> x is Tree-yielding iff x is Tree);

theorem :: TREES_3:37
 i <> 0 implies (i |-> x is FinTree-yielding iff x is finite Tree);

theorem :: TREES_3:38
 i <> 0 implies (i |-> x is DTree-yielding iff x is DecoratedTree);

definition
 cluster Tree-yielding FinTree-yielding non empty FinSequence;
 cluster DTree-yielding non empty FinSequence;
end;

definition
 cluster Tree-yielding FinTree-yielding non empty Function;
 cluster DTree-yielding non empty Function;
end;

definition
 cluster FinTree-yielding -> Tree-yielding Function;
end;

definition
 let D be constituted-Trees non empty set;
 cluster -> Tree-yielding FinSequence of D;
end;

definition let p,q be Tree-yielding FinSequence;
 cluster p^q -> Tree-yielding;
end;

definition
 let D be constituted-FinTrees non empty set;
 cluster -> FinTree-yielding FinSequence of D;
end;

definition let p,q be FinTree-yielding FinSequence;
 cluster p^q -> FinTree-yielding;
end;

definition
 let D be constituted-DTrees non empty set;
 cluster -> DTree-yielding FinSequence of D;
end;

definition let p,q be DTree-yielding FinSequence;
 cluster p^q -> DTree-yielding;
end;

definition let T be Tree;
 cluster <*T*> -> Tree-yielding non empty;
 let S be Tree;
 cluster <*T,S*> -> Tree-yielding non empty;
end;

definition let n be Nat, T be Tree;
 cluster n |-> T -> Tree-yielding;
end;

definition let T be finite Tree;
 cluster <*T*> -> FinTree-yielding;
 let S be finite Tree;
 cluster <*T,S*> -> FinTree-yielding;
end;

definition let n be Nat, T be finite Tree;
 cluster n |-> T -> FinTree-yielding;
end;

definition let T be DecoratedTree;
 cluster <*T*> -> DTree-yielding non empty;
 let S be DecoratedTree;
 cluster <*T,S*> -> DTree-yielding non empty;
end;

definition let n be Nat, T be DecoratedTree;
 cluster n |-> T -> DTree-yielding;
end;

theorem :: TREES_3:39
 for f being DTree-yielding Function holds dom doms f = dom f &
   doms f is Tree-yielding;

definition let p be DTree-yielding FinSequence;
 cluster doms p -> Tree-yielding FinSequence-like;
end;

theorem :: TREES_3:40
   for p being DTree-yielding FinSequence holds len doms p = len p;

begin :: Trees decorated by Cartesian product and structure of substitution

definition let D,E be non empty set;
 mode DecoratedTree of D,E is DecoratedTree of [:D,E:];
 mode DTree-set of D,E is DTree-set of [:D,E:];
end;

definition let T1,T2 be DecoratedTree;
 cluster <:T1,T2:> -> DecoratedTree-like;
end;

definition let D1,D2 be non empty set;
 let T1 be DecoratedTree of D1;
 let T2 be DecoratedTree of D2;
 redefine func <:T1,T2:> -> DecoratedTree of D1,D2;
end;

definition let D,E be non empty set;
 let T be DecoratedTree of D;
 let f be Function of D,E;
 redefine func f*T -> DecoratedTree of E;
end;

definition let D1,D2 be non empty set; redefine
 func pr1(D1,D2) -> Function of [:D1,D2:], D1;
 func pr2(D1,D2) -> Function of [:D1,D2:], D2;
end;

definition let D1,D2 be non empty set, T be DecoratedTree of D1,D2;
 func T`1 -> DecoratedTree of D1 equals
:: TREES_3:def 12
   pr1(D1,D2)*T;
 func T`2 -> DecoratedTree of D2 equals
:: TREES_3:def 13
   pr2(D1,D2)*T;
end;

theorem :: TREES_3:41
 for D1,D2 being non empty set, T being DecoratedTree of D1,D2,
   t being Element of dom T holds (T.t)`1 = T`1.t & T`2.t = (T.t)`2;

theorem :: TREES_3:42
   for D1,D2 being non empty set, T being DecoratedTree of D1,D2 holds
   <:T`1,T`2:> = T;

 definition let T be finite Tree;
  cluster Leaves T -> finite non empty;
 end;

definition let T be Tree, S be non empty Subset of T;
 redefine mode Element of S -> Element of T;
end;

definition let T be finite Tree;
 redefine mode Leaf of T -> Element of Leaves T;
end;

 definition
  let T be finite Tree;
  mode T-Substitution of T -> Tree means
:: TREES_3:def 14

   for t being Element of it holds t in T or
    ex l being Leaf of T st l is_a_proper_prefix_of t;
 end;

definition let T be finite Tree, t be Leaf of T, S be Tree;
 redefine func T with-replacement (t,S) -> T-Substitution of T;
end;

 definition let T be finite Tree;
  cluster finite T-Substitution of T;
 end;

 definition let n;
  mode T-Substitution of n is T-Substitution of elementary_tree n;
 end;

theorem :: TREES_3:43
   for T being Tree holds T is T-Substitution of 0;

theorem :: TREES_3:44
   for T1, T2 being Tree st T1-level 1 c= T2-level 1 &
   for n st <*n*> in T1 holds T1|<*n*> = T2|<*n*> holds T1 c= T2;

begin :: Joining of trees

canceled;

theorem :: TREES_3:46
   for T,T' being Tree, p being FinSequence of NAT st
   p in Leaves T holds T c= T with-replacement (p,T');

theorem :: TREES_3:47
   for T,T' being DecoratedTree, p being Element of dom T holds
   (T with-replacement (p,T')).p = T'.{};

theorem :: TREES_3:48
   for T,T' being DecoratedTree, p,q being Element of dom T st
   not p is_a_prefix_of q holds (T with-replacement (p,T')).q = T.q;

theorem :: TREES_3:49
   for T,T' being DecoratedTree, p being Element of dom T,
  q being Element of dom T' holds (T with-replacement (p,T')).(p^q) = T'.q;

definition let T1,T2 be Tree;
 cluster T1 \/ T2 -> non empty Tree-like;
end;

theorem :: TREES_3:50
 for T1,T2 being Tree, p being Element of T1 \/ T2 holds
  (p in T1 & p in T2 implies (T1 \/ T2)|p = (T1|p) \/ (T2|p)) &
   (not p in T1 implies (T1 \/ T2)|p = T2|p) &
    (not p in T2 implies (T1 \/ T2)|p = T1|p);

definition let p such that
  p is Tree-yielding;
 func tree p -> Tree means
:: TREES_3:def 15

  x in it iff x = {} or ex n,q st n < len p & q in p.(n+1) & x = <*n*>^q;
end;

definition let T be Tree;
 func ^T -> Tree equals
:: TREES_3:def 16

   tree<*T*>;
end;

definition let T1,T2 be Tree;
 func tree(T1,T2) -> Tree equals
:: TREES_3:def 17

   tree(<*T1,T2*>);
end;

theorem :: TREES_3:51
   p is Tree-yielding implies (<*n*>^q in tree(p) iff n < len p & q in p.(n+1))
;

theorem :: TREES_3:52
 p is Tree-yielding implies
  tree(p)-level 1 = {<*n*>: n < len p} &
   for n st n < len p holds (tree(p))|<*n*> = p.(n+1);

theorem :: TREES_3:53
   for p,q being Tree-yielding FinSequence st tree(p) = tree(q) holds p = q;

theorem :: TREES_3:54
 for p1,p2 being Tree-yielding FinSequence, T being Tree holds
   p in T iff <*len p1*>^p in tree(p1^<*T*>^p2);

theorem :: TREES_3:55
 tree({}) = elementary_tree 0;

theorem :: TREES_3:56
 p is Tree-yielding implies elementary_tree len p c= tree(p);

theorem :: TREES_3:57
 elementary_tree i = tree(i|->elementary_tree 0);

theorem :: TREES_3:58
 for T being Tree, p being Tree-yielding FinSequence holds
 tree(p^<*T*>) = (tree(p) \/ elementary_tree (len p + 1))
   with-replacement (<*len p*>, T);

theorem :: TREES_3:59
   for p being Tree-yielding FinSequence holds
  tree(p^<*elementary_tree 0*>) = tree(p) \/ elementary_tree (len p + 1);

theorem :: TREES_3:60
 for p, q being Tree-yielding FinSequence for T1,T2 be Tree holds
  tree(p^<*T1*>^q) = tree(p^<*T2*>^q) with-replacement(<*len p*>,T1);

theorem :: TREES_3:61
   for T being Tree holds ^T = elementary_tree 1 with-replacement(<*0*>, T);

theorem :: TREES_3:62
   for T1,T2 being Tree holds
   tree(T1,T2) = (elementary_tree 2 with-replacement(<*0*>,T1))
    with-replacement (<*1*>, T2);

definition let p be FinTree-yielding FinSequence;
 cluster tree(p) -> finite;
end;

definition let T be finite Tree;
 cluster ^T -> finite;
end;

definition let T1,T2 be finite Tree;
 cluster tree(T1,T2) -> finite;
end;

theorem :: TREES_3:63
 for T being Tree, x being set holds x in ^T iff x = {} or
   ex p st p in T & x = <*0*>^p;

theorem :: TREES_3:64
 for T being Tree, p being FinSequence holds p in T iff <*0*>^p in ^T;

theorem :: TREES_3:65
   for T being Tree holds elementary_tree 1 c= ^T;

theorem :: TREES_3:66
   for T1,T2 being Tree st T1 c= T2 holds ^T1 c= ^T2;

theorem :: TREES_3:67
   for T1,T2 being Tree st ^T1 = ^T2 holds T1 = T2;

theorem :: TREES_3:68
   for T being Tree holds (^T)|<*0*> = T;

theorem :: TREES_3:69
   for T1,T2 being Tree holds ^T1 with-replacement (<*0*>,T2) = ^T2;

theorem :: TREES_3:70
   ^elementary_tree 0 = elementary_tree 1;

theorem :: TREES_3:71
 for T1,T2 being Tree, x being set holds x in tree(T1,T2) iff x = {} or
   ex p st p in T1 & x = <*0*>^p or p in T2 & x = <*1*>^p;

theorem :: TREES_3:72
 for T1,T2 being Tree, p being FinSequence holds
   p in T1 iff <*0*>^p in tree(T1,T2);

theorem :: TREES_3:73
 for T1,T2 being Tree, p being FinSequence holds
   p in T2 iff <*1*>^p in tree(T1,T2);

theorem :: TREES_3:74
   for T1,T2 being Tree holds elementary_tree 2 c= tree(T1,T2);

theorem :: TREES_3:75
   for T1,T2, W1,W2 being Tree st T1 c= W1 & T2 c= W2 holds
   tree(T1,T2) c= tree(W1,W2);

theorem :: TREES_3:76
   for T1,T2, W1,W2 being Tree st tree(T1,T2) = tree(W1,W2) holds
   T1 = W1 & T2 = W2;

theorem :: TREES_3:77
   for T1,T2 being Tree holds tree(T1,T2)|<*0*> = T1 & tree(T1,T2)|<*1*> = T2;

theorem :: TREES_3:78
   for T,T1,T2 being Tree holds
   tree(T1,T2) with-replacement (<*0*>, T) = tree(T,T2) &
    tree(T1,T2) with-replacement (<*1*>, T) = tree(T1,T);

theorem :: TREES_3:79
   tree(elementary_tree 0, elementary_tree 0) = elementary_tree 2;

reserve w for FinTree-yielding FinSequence;

theorem :: TREES_3:80
 for w st for t being finite Tree st t in rng w holds height t <= n holds
   height tree(w) <= n+1;

theorem :: TREES_3:81
 for t being finite Tree st t in rng w holds height tree(w) > height t;

theorem :: TREES_3:82
 for t being finite Tree st t in rng w &
  for t' being finite Tree st t' in rng w holds height t' <= height t holds
   height tree(w) = (height t) + 1;

theorem :: TREES_3:83
   for T being finite Tree holds height ^T = (height T) + 1;

theorem :: TREES_3:84
   for T1,T2 being finite Tree holds
   height tree(T1,T2) = max(height T1, height T2)+1;