:: Replacement of Subtrees in a Tree :: by Oleg Okhotnikov :: :: Received October 1, 1995 :: Copyright (c) 1995-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies TREES_1, FINSEQ_1, NUMBERS, SUBSET_1, ORDINAL4, XBOOLE_0, TARSKI, RELAT_1, XXREAL_0, ARYTM_3, TREES_2, FUNCT_1, TREES_A, NAT_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, TREES_1, TREES_2; constructors XXREAL_0, NAT_1, MEMBERED, TREES_2, RELSET_1, FINSEQ_2; registrations XBOOLE_0, RELSET_1, MEMBERED, FINSEQ_1, TREES_2, XXREAL_0; requirements NUMERALS, BOOLE, SUBSET; begin reserve T, T1 for Tree, P for AntiChain_of_Prefixes of T, p1 for FinSequence, p, q, r, s, p9 for FinSequence of NAT, x, Z for set, t for Element of T, k, n for Nat; theorem :: TREES_A:1 for p,q,r,s being FinSequence st p^q = s^r holds p,s are_c=-comparable; definition let T,T1; let P such that P<>{}; func tree(T,P,T1) -> Tree means :: TREES_A:def 1 q in it iff (q in T & for p st p in P holds not p is_a_proper_prefix_of q) or ex p,r st p in P & r in T1 & q = p^r; end; theorem :: TREES_A:2 P <> {} implies tree(T,P,T1) = {t1 where t1 is Element of T : for p 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 }; theorem :: TREES_A:3 {t1 where t1 is Element of T : for p st p in P holds not p is_a_prefix_of t1} c= {t1 where t1 is Element of T : for p st p in P holds not p is_a_proper_prefix_of t1}; theorem :: TREES_A:4 P c= {t1 where t1 is Element of T : for p st p in P holds not p is_a_proper_prefix_of t1}; theorem :: TREES_A:5 {t1 where t1 is Element of T : for p st p in P holds not p is_a_proper_prefix_of t1} \ {t1 where t1 is Element of T : for p st p in P holds not p is_a_prefix_of t1} = P; theorem :: TREES_A:6 for T, T1, P holds P c= { p^s where p is Element of T, s is Element of T1 : p in P }; theorem :: TREES_A:7 P <> {} implies tree(T,P,T1) = {t1 where t1 is Element of T : for p 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 }; theorem :: TREES_A:8 p in P implies T1 = tree(T,P,T1)|p; registration let T; cluster non empty for AntiChain_of_Prefixes of T; end; definition let T; let t be Element of T; redefine func {t} -> AntiChain_of_Prefixes of T; end; theorem :: TREES_A:9 tree(T,{t},T1) = T with-replacement (t,T1); reserve T,T1 for DecoratedTree, P for AntiChain_of_Prefixes of dom T, t for Element of dom T, p1, p2, r1, r2 for FinSequence of NAT; definition let T,P,T1; assume P<>{}; func tree(T,P,T1) -> DecoratedTree means :: TREES_A:def 2 dom it = tree(dom T, P, dom T1) & for q st q in tree(dom T, P, dom T1) holds (for p st p in P holds not p is_a_prefix_of q & it.q = T.q) or ex p,r st p in P & r in dom T1 & q = p^r & it.q = T1.r; end; theorem :: TREES_A:10 P<>{} implies for q st q in dom tree(T,P,T1) holds (for p st p in P holds not p is_a_prefix_of q & tree(T,P,T1).q = T.q) or ex p,r st p in P & r in dom T1 & q = p^r & tree(T,P,T1).q = T1.r; theorem :: TREES_A:11 p in dom T implies for q st q in dom (T with-replacement (p,T1)) holds not p is_a_prefix_of q & T with-replacement (p,T1).q = T.q or ex r st r in dom T1 & q = p^r & T with-replacement (p,T1).q = T1.r; theorem :: TREES_A:12 P<>{} implies for q st q in dom tree(T,P,T1) & q in {t1 where t1 is Element of dom T : for p st p in P holds not p is_a_prefix_of t1} holds tree(T,P,T1).q = T.q; theorem :: TREES_A:13 p in dom T implies for q 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; theorem :: TREES_A:14 for q 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, r being Element of dom T1 st q = p9^r & p9 in P & tree(T,P,T1).q = T1.r; theorem :: TREES_A:15 p in dom T implies for q st q in dom (T with-replacement (p,T1)) & q in the set of all p^s where s is Element of dom T1 ex r being Element of dom T1 st q = p^r & T with-replacement (p,T1).q = T1.r; theorem :: TREES_A:16 tree(T,{t},T1) = T with-replacement (t,T1); reserve D for non empty set, T,T1 for DecoratedTree of D, P for non empty AntiChain_of_Prefixes of dom T; registration let D,T,P,T1; cluster tree(T,P,T1) -> D-valued; end;