:: K\"onig's Lemma
:: by Grzegorz Bancerek
::
:: Received January 10, 1991
:: Copyright (c) 1991 Association of Mizar Users
theorem Th1: :: TREES_2:1
theorem Th2: :: TREES_2:2
theorem :: TREES_2:3
canceled;
theorem Th4: :: TREES_2:4
theorem :: TREES_2:5
canceled;
theorem Th6: :: TREES_2:6
theorem Th7: :: TREES_2:7
:: deftheorem defines = TREES_2:def 1 :
theorem :: TREES_2:8
theorem Th9: :: TREES_2:9
theorem :: TREES_2:10
:: 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 :: TREES_2:11
theorem :: TREES_2:12
theorem :: TREES_2:13
:: deftheorem defines -level TREES_2:def 6 :
theorem :: TREES_2:14
theorem :: TREES_2:15
theorem :: TREES_2:16
theorem :: TREES_2:17
theorem :: TREES_2:18
theorem Th19: :: TREES_2:19
theorem Th20: :: TREES_2:20
theorem Th21: :: TREES_2:21
theorem Th22: :: TREES_2:22
:: deftheorem Def7 defines Branch-like TREES_2:def 7 :
theorem Th23: :: TREES_2:23
theorem Th24: :: TREES_2:24
theorem Th25: :: TREES_2:25
theorem Th26: :: TREES_2:26
theorem Th27: :: TREES_2:27
theorem Th28: :: TREES_2:28
theorem Th29: :: TREES_2:29
theorem Th30: :: TREES_2:30
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
theorem Th31: :: TREES_2:31
theorem :: TREES_2:32
:: deftheorem Def8 defines DecoratedTree-like TREES_2:def 8 :
:: deftheorem Def9 defines ParametrizedSubset TREES_2:def 9 :
theorem Th33: :: TREES_2:33
:: deftheorem defines Leaves TREES_2:def 10 :
:: deftheorem Def11 defines | TREES_2:def 11 :
theorem Th34: :: TREES_2:34
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 :: TREES_2:def 12
(
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: :: TREES_2:35
theorem Th36: :: TREES_2:36
theorem Th37: :: TREES_2:37
theorem Th38: :: TREES_2:38
:: deftheorem defines branchdeg TREES_2:def 13 :
Lm2:
for f being Function st dom f is finite holds
f is finite
theorem :: TREES_2:39