let T be Tree; ( T = {0,1} * implies T is binary )
assume A1:
T = {0,1} *
; T is binary
now for t being Element of T st not t in Leaves T holds
succ t = {(t ^ <*0*>),(t ^ <*1*>)}let t be
Element of
T;
( not t in Leaves T implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} )assume
not
t in Leaves T
;
succ t = {(t ^ <*0*>),(t ^ <*1*>)}
{ (t ^ <*n*>) where n is Nat : t ^ <*n*> in T } = {(t ^ <*0*>),(t ^ <*1*>)}
proof
thus
{ (t ^ <*n*>) where n is Nat : t ^ <*n*> in T } c= {(t ^ <*0*>),(t ^ <*1*>)}
XBOOLE_0:def 10 {(t ^ <*0*>),(t ^ <*1*>)} c= { (t ^ <*n*>) where n is Nat : t ^ <*n*> in T }
let x be
object ;
TARSKI:def 3 ( not x in {(t ^ <*0*>),(t ^ <*1*>)} or x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in T } )
A4:
t is
FinSequence of
{0,1}
by A1, FINSEQ_1:def 11;
rng <*1*> c= {0,1}
then
<*1*> is
FinSequence of
{0,1}
by FINSEQ_1:def 4;
then
t ^ <*1*> is
FinSequence of
{0,1}
by A4, Lm1;
then A5:
t ^ <*1*> in T
by A1, FINSEQ_1:def 11;
assume
x in {(t ^ <*0*>),(t ^ <*1*>)}
;
x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in T }
then A6:
(
x = t ^ <*0*> or
x = t ^ <*1*> )
by TARSKI:def 2;
rng <*0*> c= {0,1}
then
<*0*> is
FinSequence of
{0,1}
by FINSEQ_1:def 4;
then
t ^ <*0*> is
FinSequence of
{0,1}
by A4, Lm1;
then
t ^ <*0*> in T
by A1, FINSEQ_1:def 11;
hence
x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in T }
by A5, A6;
verum
end; hence
succ t = {(t ^ <*0*>),(t ^ <*1*>)}
by TREES_2:def 5;
verum end;
hence
T is binary
by BINTREE1:def 2; verum