:: BINTREE2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: BINTREE2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being set
for p being FinSequence
for n being Nat st p in D * holds
p | (Seg n) in D *
proof end;

theorem Th2: :: BINTREE2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being binary Tree
for t being Element of T holds t is FinSequence of BOOLEAN
proof end;

definition
let T be binary Tree;
:: original: Element
redefine mode Element of T -> FinSequence of BOOLEAN ;
coherence
for b1 being Element of T holds b1 is FinSequence of BOOLEAN
by Th2;
end;

theorem Th3: :: BINTREE2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree st T = {0,1} * holds
T is binary
proof end;

theorem Th4: :: BINTREE2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree st T = {0,1} * holds
Leaves T = {}
proof end;

theorem :: BINTREE2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being binary Tree
for n being Nat
for t being Element of T st t in T -level n holds
t is Tuple of n,BOOLEAN
proof end;

theorem :: BINTREE2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree st ( for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) holds
Leaves T = {}
proof end;

theorem Th7: :: BINTREE2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree st ( for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) holds
T is binary
proof end;

theorem Th8: :: BINTREE2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree holds
( T = {0,1} * iff for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} )
proof end;

scheme :: BINTREE2:sch 1
DecoratedBinTreeEx{ F1() -> non empty set , F2() -> Element of F1(), P1[ set , set , set ] } :
ex D being binary DecoratedTree of F1() st
( dom D = {0,1} * & D . {} = F2() & ( for x being Node of D holds P1[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)] ) )
provided
A1: for a being Element of F1() ex b, c being Element of F1() st P1[a,b,c]
proof end;

scheme :: BINTREE2:sch 2
DecoratedBinTreeEx1{ F1() -> non empty set , F2() -> Element of F1(), P1[ set , set ], P2[ set , set ] } :
ex D being binary DecoratedTree of F1() st
( dom D = {0,1} * & D . {} = F2() & ( for x being Node of D holds
( P1[D . x,D . (x ^ <*0*>)] & P2[D . x,D . (x ^ <*1*>)] ) ) )
provided
A1: for a being Element of F1() ex b being Element of F1() st P1[a,b] and
A2: for a being Element of F1() ex b being Element of F1() st P2[a,b]
proof end;

Lm1: for D being non empty set
for f being FinSequence of D holds Rev f is FinSequence of D
;

definition
let T be binary Tree;
let n be non empty Nat;
func NumberOnLevel n,T -> Function of T -level n, NAT means :Def1: :: BINTREE2:def 1
for t being Element of T st t in T -level n holds
for F being Tuple of n,BOOLEAN st F = Rev t holds
it . t = (Absval F) + 1;
existence
ex b1 being Function of T -level n, NAT st
for t being Element of T st t in T -level n holds
for F being Tuple of n,BOOLEAN st F = Rev t holds
b1 . t = (Absval F) + 1
proof end;
uniqueness
for b1, b2 being Function of T -level n, NAT st ( for t being Element of T st t in T -level n holds
for F being Tuple of n,BOOLEAN st F = Rev t holds
b1 . t = (Absval F) + 1 ) & ( for t being Element of T st t in T -level n holds
for F being Tuple of n,BOOLEAN st F = Rev t holds
b2 . t = (Absval F) + 1 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines NumberOnLevel BINTREE2:def 1 :
for T being binary Tree
for n being non empty Nat
for b3 being Function of T -level n, NAT holds
( b3 = NumberOnLevel n,T iff for t being Element of T st t in T -level n holds
for F being Tuple of n,BOOLEAN st F = Rev t holds
b3 . t = (Absval F) + 1 );

registration
let T be binary Tree;
let n be non empty Nat;
cluster NumberOnLevel n,T -> one-to-one ;
coherence
NumberOnLevel n,T is one-to-one
proof end;
end;

definition
let T be Tree;
attr T is full means :Def2: :: BINTREE2:def 2
T = {0,1} * ;
end;

:: deftheorem Def2 defines full BINTREE2:def 2 :
for T being Tree holds
( T is full iff T = {0,1} * );

theorem Th9: :: BINTREE2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{0,1} * is Tree
proof end;

theorem Th10: :: BINTREE2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree st T = {0,1} * holds
for n being Nat holds 0* n in T -level n
proof end;

theorem Th11: :: BINTREE2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree st T = {0,1} * holds
for n being non empty Nat
for y being Tuple of n,BOOLEAN holds y in T -level n
proof end;

registration
let T be binary Tree;
let n be Nat;
cluster T -level n -> finite ;
coherence
T -level n is finite
by QC_LANG4:19;
end;

registration
cluster full -> binary set ;
coherence
for b1 being Tree st b1 is full holds
b1 is binary
proof end;
end;

registration
cluster binary full set ;
existence
ex b1 being Tree st b1 is full
proof end;
end;

theorem Th12: :: BINTREE2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being full Tree
for n being non empty Nat holds Seg (2 to_power n) c= rng (NumberOnLevel n,T)
proof end;

definition
let T be full Tree;
let n be non empty Nat;
func FinSeqLevel n,T -> FinSequence of T -level n equals :: BINTREE2:def 3
(NumberOnLevel n,T) " ;
coherence
(NumberOnLevel n,T) " is FinSequence of T -level n
proof end;
end;

:: deftheorem defines FinSeqLevel BINTREE2:def 3 :
for T being full Tree
for n being non empty Nat holds FinSeqLevel n,T = (NumberOnLevel n,T) " ;

registration
let T be full Tree;
let n be non empty Nat;
cluster FinSeqLevel n,T -> one-to-one ;
coherence
FinSeqLevel n,T is one-to-one
by FUNCT_1:62;
end;

theorem Th13: :: BINTREE2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being full Tree
for n being non empty Nat holds (NumberOnLevel n,T) . (0* n) = 1
proof end;

theorem Th14: :: BINTREE2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being full Tree
for n being non empty Nat
for y being Tuple of n,BOOLEAN st y = 0* n holds
(NumberOnLevel n,T) . ('not' y) = 2 to_power n
proof end;

theorem Th15: :: BINTREE2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being full Tree
for n being non empty Nat holds (FinSeqLevel n,T) . 1 = 0* n
proof end;

theorem Th16: :: BINTREE2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being full Tree
for n being non empty Nat
for y being Tuple of n,BOOLEAN st y = 0* n holds
(FinSeqLevel n,T) . (2 to_power n) = 'not' y
proof end;

theorem Th17: :: BINTREE2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being full Tree
for n being non empty Nat
for i being Nat st i in Seg (2 to_power n) holds
(FinSeqLevel n,T) . i = Rev (n -BinarySequence (i -' 1))
proof end;

theorem Th18: :: BINTREE2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being full Tree
for n being Nat holds Card (T -level n) = 2 to_power n
proof end;

theorem Th19: :: BINTREE2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being full Tree
for n being non empty Nat holds len (FinSeqLevel n,T) = 2 to_power n
proof end;

theorem Th20: :: BINTREE2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being full Tree
for n being non empty Nat holds dom (FinSeqLevel n,T) = Seg (2 to_power n)
proof end;

theorem :: BINTREE2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being full Tree
for n being non empty Nat holds rng (FinSeqLevel n,T) = T -level n
proof end;

theorem :: BINTREE2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being full Tree holds (FinSeqLevel 1,T) . 1 = <*0*>
proof end;

theorem :: BINTREE2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being full Tree holds (FinSeqLevel 1,T) . 2 = <*1*>
proof end;

theorem :: BINTREE2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being full Tree
for n, i being non empty Nat st i <= 2 to_power (n + 1) holds
for F being Tuple of n,BOOLEAN st F = (FinSeqLevel n,T) . ((i + 1) div 2) holds
(FinSeqLevel (n + 1),T) . i = F ^ <*((i + 1) mod 2)*>
proof end;