:: by Oleg Okhotnikov

::

:: Received October 1, 1995

:: Copyright (c) 1995-2021 Association of Mizar Users

definition

let T, T1 be Tree;

let P be AntiChain_of_Prefixes of T;

assume A1: P <> {} ;

ex b_{1} being Tree st

for q being FinSequence of NAT holds

( q in b_{1} iff ( ( q in T & ( 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 & r in T1 & q = p ^ r ) ) )

for b_{1}, b_{2} being Tree st ( for q being FinSequence of NAT holds

( q in b_{1} iff ( ( q in T & ( 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 & r in T1 & q = p ^ r ) ) ) ) & ( for q being FinSequence of NAT holds

( q in b_{2} iff ( ( q in T & ( 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 & r in T1 & q = p ^ r ) ) ) ) holds

b_{1} = b_{2}

end;
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 & ( 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 & r in T1 & q = p ^ r ) ) );

existence for q being FinSequence of NAT holds

( q in it iff ( ( q in T & ( 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 & r in T1 & q = p ^ r ) ) );

ex b

for q being FinSequence of NAT holds

( q in b

not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st

( p in P & r in T1 & q = p ^ r ) ) )

proof end;

uniqueness for b

( q in b

not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st

( p in P & r in T1 & q = p ^ r ) ) ) ) & ( for q being FinSequence of NAT holds

( q in b

not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st

( p in P & r in T1 & q = p ^ r ) ) ) ) holds

b

proof 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 b_{4} being Tree holds

( b_{4} = tree (T,P,T1) iff for q being FinSequence of NAT holds

( q in b_{4} iff ( ( q in T & ( 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 & r in T1 & q = p ^ r ) ) ) );

for T, T1 being Tree

for P being AntiChain_of_Prefixes of T st P <> {} holds

for b

( b

( q in b

not p is_a_proper_prefix_of q ) ) or ex p, r being FinSequence of NAT st

( p in P & r in T1 & 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 }

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 }

proof end;

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 }

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 }

proof end;

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 }

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 }

proof end;

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

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

proof end;

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 }

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 }

proof end;

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 }

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 }

proof end;

theorem :: TREES_A:8

for T, T1 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

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

proof end;

registration

let T be Tree;

existence

not for b_{1} being AntiChain_of_Prefixes of T holds b_{1} is empty

end;
existence

not for b

proof 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;
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;

definition

let T be DecoratedTree;

let P be AntiChain_of_Prefixes of dom T;

let T1 be DecoratedTree;

assume A1: P <> {} ;

ex b_{1} being DecoratedTree st

( dom b_{1} = tree ((dom T),P,(dom T1)) & ( 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 & b_{1} . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & b_{1} . q = T1 . r ) ) ) )

for b_{1}, b_{2} being DecoratedTree st dom b_{1} = tree ((dom T),P,(dom T1)) & ( 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 & b_{1} . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & b_{1} . q = T1 . r ) ) ) & dom b_{2} = tree ((dom T),P,(dom T1)) & ( 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 & b_{2} . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & b_{2} . q = T1 . r ) ) ) holds

b_{1} = b_{2}

end;
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)) & ( 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 & it . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & it . q = T1 . r ) ) ) );

existence ( dom it = tree ((dom T),P,(dom T1)) & ( 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 & it . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & it . q = T1 . r ) ) ) );

ex b

( dom b

( 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 & b

( p in P & r in dom T1 & q = p ^ r & b

proof end;

uniqueness for b

( 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 & b

( p in P & r in dom T1 & q = p ^ r & b

( 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 & b

( p in P & r in dom T1 & q = p ^ r & b

b

proof 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 b_{4} being DecoratedTree holds

( b_{4} = tree (T,P,T1) iff ( dom b_{4} = tree ((dom T),P,(dom T1)) & ( 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 & b_{4} . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & b_{4} . q = T1 . r ) ) ) ) );

for T being DecoratedTree

for P being AntiChain_of_Prefixes of dom T

for T1 being DecoratedTree st P <> {} holds

for b

( b

( 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 & b

( p in P & r in dom T1 & q = p ^ r & b

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 & (tree (T,P,T1)) . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & (tree (T,P,T1)) . q = T1 . r ) )

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 & (tree (T,P,T1)) . q = T . q ) or ex p, r being FinSequence of NAT st

( p in P & r in dom T1 & q = p ^ r & (tree (T,P,T1)) . q = T1 . r ) )

proof end;

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 & (T with-replacement (p,T1)) . q = T . q ) or ex r being FinSequence of NAT st

( r in dom T1 & q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) )

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 & (T with-replacement (p,T1)) . q = T . q ) or ex r being FinSequence of NAT st

( r in dom T1 & q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r ) )

proof end;

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)) & 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

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)) & 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

proof end;

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)) & 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

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)) & 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

proof end;

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)) & 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 & p9 in P & (tree (T,P,T1)) . q = T1 . r )

for P being AntiChain_of_Prefixes of dom T

for q being FinSequence of NAT st q in dom (tree (T,P,T1)) & 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 & p9 in P & (tree (T,P,T1)) . q = T1 . r )

proof end;

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)) & q in { (p ^ s) where s is Element of dom T1 : verum } holds

ex r being Element of dom T1 st

( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r )

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)) & q in { (p ^ s) where s is Element of dom T1 : verum } holds

ex r being Element of dom T1 st

( q = p ^ r & (T with-replacement (p,T1)) . q = T1 . r )

proof end;

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)

for t being Element of dom T holds tree (T,{t},T1) = T with-replacement (t,T1)

proof end;

registration

let D be non empty set ;

let T be DecoratedTree of D;

let P be non empty AntiChain_of_Prefixes of dom T;

let T1 be DecoratedTree of D;

coherence

tree (T,P,T1) is D -valued

end;
let T be DecoratedTree of D;

let P be non empty AntiChain_of_Prefixes of dom T;

let T1 be DecoratedTree of D;

coherence

tree (T,P,T1) is D -valued

proof end;