environ
vocabularies HIDDEN, 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 HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, TREES_1, TREES_2;
definitions TARSKI, XBOOLE_0, TREES_1, TREES_2, RELAT_1;
theorems TARSKI, FUNCT_1, FINSEQ_1, TREES_1, TREES_2, XBOOLE_0, XBOOLE_1, RELAT_1, CARD_2;
schemes TREES_2;
registrations XBOOLE_0, RELSET_1, MEMBERED, FINSEQ_1, TREES_2, XXREAL_0;
constructors HIDDEN, XXREAL_0, NAT_1, MEMBERED, TREES_2, RELSET_1, FINSEQ_2;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET;
equalities ;
expansions TARSKI, XBOOLE_0, TREES_1;
definition
let T be
DecoratedTree;
let P be
AntiChain_of_Prefixes of
dom T;
let T1 be
DecoratedTree;
assume A1:
P <> {}
;
existence
ex b1 being DecoratedTree st
( dom b1 = 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 & b1 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & b1 . q = T1 . r ) ) ) )
uniqueness
for b1, b2 being DecoratedTree st dom b1 = 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 & b1 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & b1 . q = T1 . r ) ) ) & dom b2 = 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 & b2 . q = T . q ) or ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & b2 . q = T1 . r ) ) ) holds
b1 = b2
end;