:: Full Trees
:: by Robert Milewski
::
:: Received February 25, 1998
:: Copyright (c) 1998 Association of Mizar Users
Lm1:
for D being set
for p, q being FinSequence of D holds p ^ q is FinSequence of D
;
Lm2:
for D being non empty set
for x being Element of D holds <*x*> is FinSequence of D
;
theorem Th1: :: BINTREE2:1
theorem Th2: :: BINTREE2:2
theorem Th3: :: BINTREE2:3
theorem Th4: :: BINTREE2:4
theorem :: BINTREE2:5
theorem :: BINTREE2:6
theorem Th7: :: BINTREE2:7
theorem Th8: :: BINTREE2:8
Lm3:
for D being non empty set
for f being FinSequence of D holds Rev f is FinSequence of D
;
:: deftheorem Def1 defines NumberOnLevel BINTREE2:def 1 :
:: deftheorem Def2 defines full BINTREE2:def 2 :
theorem Th9: :: BINTREE2:9
theorem Th10: :: BINTREE2:10
theorem Th11: :: BINTREE2:11
theorem Th12: :: BINTREE2:12
:: deftheorem defines FinSeqLevel BINTREE2:def 3 :
theorem Th13: :: BINTREE2:13
theorem Th14: :: BINTREE2:14
theorem Th15: :: BINTREE2:15
theorem Th16: :: BINTREE2:16
theorem Th17: :: BINTREE2:17
theorem Th18: :: BINTREE2:18
theorem Th19: :: BINTREE2:19
theorem Th20: :: BINTREE2:20
theorem :: BINTREE2:21
theorem :: BINTREE2:22
theorem :: BINTREE2:23
theorem :: BINTREE2:24