begin
theorem Th1:
theorem Th2:
theorem
canceled;
theorem Th4:
theorem
canceled;
theorem Th6:
theorem Th7:
:: deftheorem defines = TREES_2:def 1 :
theorem
theorem Th9:
theorem
:: deftheorem defines finite-order TREES_2:def 2 :
:: deftheorem Def3 defines Chain TREES_2:def 3 :
:: deftheorem Def4 defines Level TREES_2:def 4 :
:: deftheorem defines succ TREES_2:def 5 :
theorem
theorem
theorem
:: deftheorem defines -level TREES_2:def 6 :
theorem
theorem
theorem Th16:
theorem
theorem
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
:: deftheorem Def7 defines Branch-like TREES_2:def 7 :
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
Lm1:
for X being set st X is finite holds
ex n being Element of NAT st
for k being Element of NAT st k in X holds
k <= n
scheme
InfiniteChain{
F1()
-> set ,
F2()
-> set ,
P1[
set ],
P2[
set ,
set ] } :
provided
A1:
(
F2()
in F1() &
P1[
F2()] )
and A2:
for
x being
set st
x in F1() &
P1[
x] holds
ex
y being
set st
(
y in F1() &
P2[
x,
y] &
P1[
y] )
theorem Th31:
theorem
:: deftheorem Def8 defines DecoratedTree-like TREES_2:def 8 :
theorem Th33:
:: deftheorem TREES_2:def 9 :
canceled;
:: deftheorem defines Leaves TREES_2:def 10 :
:: deftheorem Def11 defines | TREES_2:def 11 :
theorem Th34:
definition
let T be
DecoratedTree;
let p be
FinSequence of
NAT ;
let T1 be
DecoratedTree;
assume A1:
p in dom T
;
func T with-replacement p,
T1 -> DecoratedTree means
(
dom it = (dom T) with-replacement p,
(dom T1) & ( for
q being
FinSequence of
NAT holds
( not
q in (dom T) with-replacement p,
(dom T1) or ( not
p is_a_prefix_of q &
it . q = T . q ) or ex
r being
FinSequence of
NAT st
(
r in dom T1 &
q = p ^ r &
it . q = T1 . r ) ) ) );
existence
ex b1 being DecoratedTree st
( dom b1 = (dom T) with-replacement p,(dom T1) & ( for q being FinSequence of NAT holds
( not q in (dom T) with-replacement p,(dom T1) or ( not p is_a_prefix_of q & b1 . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & b1 . q = T1 . r ) ) ) )
uniqueness
for b1, b2 being DecoratedTree st dom b1 = (dom T) with-replacement p,(dom T1) & ( for q being FinSequence of NAT holds
( not q in (dom T) with-replacement p,(dom T1) or ( not p is_a_prefix_of q & b1 . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & b1 . q = T1 . r ) ) ) & dom b2 = (dom T) with-replacement p,(dom T1) & ( for q being FinSequence of NAT holds
( not q in (dom T) with-replacement p,(dom T1) or ( not p is_a_prefix_of q & b2 . q = T . q ) or ex r being FinSequence of NAT st
( r in dom T1 & q = p ^ r & b2 . q = T1 . r ) ) ) holds
b1 = b2
end;
:: deftheorem defines with-replacement TREES_2:def 12 :
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
begin
:: deftheorem defines branchdeg TREES_2:def 13 :
Lm2:
for f being Function st dom f is finite holds
f is finite
theorem
theorem
theorem