let T be full Tree; for n being non zero Nat
for i being Nat st i in Seg (2 to_power n) holds
(FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1))
let n be non zero Nat; for i being Nat st i in Seg (2 to_power n) holds
(FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1))
let i be Nat; ( i in Seg (2 to_power n) implies (FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1)) )
reconsider nB = n -BinarySequence (i -' 1) as Element of n -tuples_on BOOLEAN by FINSEQ_2:131;
assume A1:
i in Seg (2 to_power n)
; (FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1))
then A2:
1 <= i
by FINSEQ_1:1;
i <= 2 to_power n
by A1, FINSEQ_1:1;
then
i < (2 to_power n) + 1
by NAT_1:13;
then
i - 1 < 2 to_power n
by XREAL_1:19;
then
i -' 1 < 2 to_power n
by A2, XREAL_1:233;
then A3: (Absval nB) + 1 =
(i -' 1) + 1
by BINARI_3:35
.=
(i - 1) + 1
by A2, XREAL_1:233
.=
i
;
A4: len (Rev nB) =
len nB
by FINSEQ_5:def 3
.=
n
by CARD_1:def 7
;
then reconsider RnB = Rev nB as Element of n -tuples_on BOOLEAN by FINSEQ_2:92;
RnB in {0,1} *
by FINSEQ_1:def 11;
then
RnB is Element of T
by Def2;
then
RnB in { t where t is Element of T : len t = n }
by A4;
then A5:
RnB in T -level n
by TREES_2:def 6;
nB = Rev RnB
;
then A6:
(NumberOnLevel (n,T)) . RnB = (Absval nB) + 1
by A5, Def1;
RnB in dom (NumberOnLevel (n,T))
by A5, FUNCT_2:def 1;
hence
(FinSeqLevel (n,T)) . i = Rev (n -BinarySequence (i -' 1))
by A6, A3, FUNCT_1:32; verum