:: Replacement of Subtrees in a Tree
:: by Oleg Okhotnikov
::
:: Received October 1, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users


begin

theorem Th1: :: TREES_A:1
for p, q, r, s being FinSequence st p ^ q = s ^ r holds
p,s are_c=-comparable
proofend;

definition
let T, T1 be Tree;
let P be AntiChain_of_Prefixes of T;
assume A1: P <> {} ;
func tree (T,P,T1) ->  Tree means :Def1: :: TREES_A:def 1
 for q being FinSequence of NAT holds
( q in it iff ( ( q in T &amp; ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P &amp; r in T1 &amp; q = p ^ r ) ) );
existence
 ex b1 being Tree st
for q being FinSequence of NAT holds
( q in b1 iff ( ( q in T &amp; ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P &amp; r in T1 &amp; q = p ^ r ) ) )
proofend;
uniqueness
 for b1, b2 being Tree st ( for q being FinSequence of NAT holds
( q in b1 iff ( ( q in T &amp; ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P &amp; r in T1 &amp; q = p ^ r ) ) ) ) &amp; ( for q being FinSequence of NAT holds
( q in b2 iff ( ( q in T &amp; ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P &amp; r in T1 &amp; q = p ^ r ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines tree TREES_A:def_1_:_
 for T, T1 being Tree
for P being AntiChain_of_Prefixes of T st P <> {} holds
for b4 being Tree holds
( b4 = tree (T,P,T1) iff for q being FinSequence of NAT holds
( q in b4 iff ( ( q in T &amp; ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st
( p in P &amp; r in T1 &amp; q = p ^ r ) ) ) );

theorem Th2: :: TREES_A:2
for T, T1 being Tree
for P being AntiChain_of_Prefixes of T st P <> {} holds
tree (T,P,T1) =  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }  \/  {  (p ^ s) where p is Element of T, s is Element of T1 : p in P  }
proofend;

theorem Th3: :: TREES_A:3
for T being Tree
for P being AntiChain_of_Prefixes of T holds  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  c=  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }
proofend;

theorem Th4: :: TREES_A:4
for T being Tree
for P being AntiChain_of_Prefixes of T holds P c=  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }
proofend;

theorem Th5: :: TREES_A:5
for T being Tree
for P being AntiChain_of_Prefixes of T holds  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1  }  \  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  = P
proofend;

theorem Th6: :: TREES_A:6
for T, T1 being Tree
for P being AntiChain_of_Prefixes of T holds P c=  {  (p ^ s) where p is Element of T, s is Element of T1 : p in P  }
proofend;

theorem Th7: :: TREES_A:7
for T, T1 being Tree
for P being AntiChain_of_Prefixes of T st P <> {} holds
tree (T,P,T1) =  {  t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  \/  {  (p ^ s) where p is Element of T, s is Element of T1 : p in P  }
proofend;

theorem :: TREES_A:8
for T1, T being Tree
for P being AntiChain_of_Prefixes of T
for p being FinSequence of NAT st p in P holds
T1 = (tree (T,P,T1)) | p
proofend;

registration
let T be Tree;
cluster non empty AntiChain_of_Prefixes-like for AntiChain_of_Prefixes of T;
existence
 not for b1 being AntiChain_of_Prefixes of T holds b1 is empty
proofend;
end;

definition
let T be Tree;
let t be Element of T;
:: original:{
redefine func{t} ->  AntiChain_of_Prefixes of T;
correctness
coherence
{t} is AntiChain_of_Prefixes of T;
by TREES_1:39;
end;

theorem Th9: :: TREES_A:9
for T, T1 being Tree
for t being Element of T holds tree (T,{t},T1) = T with-replacement (t,T1)
proofend;

definition
let T be DecoratedTree;
let P be AntiChain_of_Prefixes of dom T;
let T1 be DecoratedTree;
assume A1: P <> {} ;
func tree (T,P,T1) ->  DecoratedTree means :Def2: :: TREES_A:def 2
( dom it = tree ((dom T),P,(dom T1)) &amp; ( for q being FinSequence of NAT holds
( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q &amp; it . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P &amp; r in dom T1 &amp; q = p ^ r &amp; it . q = T1 . r ) ) ) );
existence
 ex b1 being DecoratedTree st
( dom b1 = tree ((dom T),P,(dom T1)) &amp; ( for q being FinSequence of NAT holds
( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q &amp; b1 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P &amp; r in dom T1 &amp; q = p ^ r &amp; b1 . q = T1 . r ) ) ) )
proofend;
uniqueness
 for b1, b2 being DecoratedTree st dom b1 = tree ((dom T),P,(dom T1)) &amp; ( for q being FinSequence of NAT holds
( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q &amp; b1 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P &amp; r in dom T1 &amp; q = p ^ r &amp; b1 . q = T1 . r ) ) ) &amp; dom b2 = tree ((dom T),P,(dom T1)) &amp; ( for q being FinSequence of NAT holds
( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q &amp; b2 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P &amp; r in dom T1 &amp; q = p ^ r &amp; b2 . q = T1 . r ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines tree TREES_A:def_2_:_
 for T being DecoratedTree
for P being AntiChain_of_Prefixes of dom T
for T1 being DecoratedTree st P <> {} holds
for b4 being DecoratedTree holds
( b4 = tree (T,P,T1) iff ( dom b4 = tree ((dom T),P,(dom T1)) &amp; ( for q being FinSequence of NAT holds
( not q in tree ((dom T),P,(dom T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q &amp; b4 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P &amp; r in dom T1 &amp; q = p ^ r &amp; b4 . q = T1 . r ) ) ) ) );

theorem Th10: :: TREES_A:10
for T, T1 being DecoratedTree
for P being AntiChain_of_Prefixes of dom T st P <> {} holds
for q being FinSequence of NAT holds
( not q in dom (tree (T,P,T1)) or for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q &amp; (tree (T,P,T1)) . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P &amp; r in dom T1 &amp; q = p ^ r &amp; (tree (T,P,T1)) . q = T1 . r ) )
proofend;

theorem Th11: :: TREES_A:11
for p being FinSequence of NAT
for T, T1 being DecoratedTree st p in dom T holds
for q being FinSequence of NAT holds
( not q in dom (T with-replacement (p,T1)) or ( not p is_a_prefix_of q &amp; (T with-replacement (p,T1)) . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 &amp; q = p ^ r &amp; (T with-replacement (p,T1)) . q = T1 . r ) )
proofend;

theorem Th12: :: TREES_A:12
for T, T1 being DecoratedTree
for P being AntiChain_of_Prefixes of dom T st P <> {} holds
for q being FinSequence of NAT st q in dom (tree (T,P,T1)) &amp; q in  {  t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1  }  holds
(tree (T,P,T1)) . q = T . q
proofend;

theorem Th13: :: TREES_A:13
for p being FinSequence of NAT
for T, T1 being DecoratedTree st p in dom T holds
for q being FinSequence of NAT st q in dom (T with-replacement (p,T1)) &amp; q in  {  t1 where t1 is Element of dom T : not p is_a_prefix_of t1  }  holds
(T with-replacement (p,T1)) . q = T . q
proofend;

theorem Th14: :: TREES_A:14
for T, T1 being DecoratedTree
for P being AntiChain_of_Prefixes of dom T
for q being FinSequence of NAT st q in dom (tree (T,P,T1)) &amp; q in  {  (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P  }  holds
ex p9 being Element of dom T ex r being Element of dom T1 st
( q = p9 ^ r &amp; p9 in P &amp; (tree (T,P,T1)) . q = T1 . r )
proofend;

theorem Th15: :: TREES_A:15
for p being FinSequence of NAT
for T, T1 being DecoratedTree st p in dom T holds
for q being FinSequence of NAT st q in dom (T with-replacement (p,T1)) &amp; q in  {  (p ^ s) where s is Element of dom T1 : s = s  }  holds
ex r being Element of dom T1 st
( q = p ^ r &amp; (T with-replacement (p,T1)) . q = T1 . r )
proofend;

theorem :: TREES_A:16
for T, T1 being DecoratedTree
for t being Element of dom T holds tree (T,{t},T1) = T with-replacement (t,T1)
proofend;

definition
let D be non empty set ;
let T be DecoratedTree of D;
let P be AntiChain_of_Prefixes of dom T;
let T1 be DecoratedTree of D;
assume A1: P <> {} ;
func tree (T,P,T1) ->  DecoratedTree of D equals :: TREES_A:def 3
 tree (T,P,T1);
coherence
 tree (T,P,T1) is DecoratedTree of D
proofend;
end;

:: deftheorem  defines tree TREES_A:def_3_:_
 for D being non empty set
for T being DecoratedTree of D
for P being AntiChain_of_Prefixes of dom T
for T1 being DecoratedTree of D st P <> {} holds
tree (T,P,T1) = tree (T,P,T1);