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