let T be Tree; :: thesis: ( T = {0,1} * implies T is binary )

assume A1: T = {0,1} * ; :: thesis: T is binary

assume A1: T = {0,1} * ; :: thesis: T is binary

now :: thesis: for t being Element of T st not t in Leaves T holds

succ t = {(t ^ <*0*>),(t ^ <*1*>)}

hence
T is binary
by BINTREE1:def 2; :: thesis: verumsucc t = {(t ^ <*0*>),(t ^ <*1*>)}

let t be Element of T; :: thesis: ( not t in Leaves T implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} )

assume not t in Leaves T ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}

{ (t ^ <*n*>) where n is Nat : t ^ <*n*> in T } = {(t ^ <*0*>),(t ^ <*1*>)}

end;assume not t in Leaves T ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}

{ (t ^ <*n*>) where n is Nat : t ^ <*n*> in T } = {(t ^ <*0*>),(t ^ <*1*>)}

proof

hence
succ t = {(t ^ <*0*>),(t ^ <*1*>)}
by TREES_2:def 5; :: thesis: verum
thus
{ (t ^ <*n*>) where n is Nat : t ^ <*n*> in T } c= {(t ^ <*0*>),(t ^ <*1*>)}
:: according to XBOOLE_0:def 10 :: thesis: {(t ^ <*0*>),(t ^ <*1*>)} c= { (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 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*>)} ; :: thesis: 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 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; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(t ^ <*0*>),(t ^ <*1*>)} or x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in T } )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in T } or x in {(t ^ <*0*>),(t ^ <*1*>)} )

assume x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in T } ; :: thesis: x in {(t ^ <*0*>),(t ^ <*1*>)}

then consider n being Nat such that

A2: x = t ^ <*n*> and

A3: t ^ <*n*> in T ;

reconsider tn = t ^ <*n*> as FinSequence of {0,1} by A1, A3, FINSEQ_1:def 11;

(len t) + 1 in Seg ((len t) + 1) by FINSEQ_1:4;

then (len t) + 1 in Seg (len tn) by FINSEQ_2:16;

then (len t) + 1 in dom tn by FINSEQ_1:def 3;

then tn /. ((len t) + 1) = (t ^ <*n*>) . ((len t) + 1) by PARTFUN1:def 6

.= n by FINSEQ_1:42 ;

then ( n = 0 or n = 1 ) by TARSKI:def 2;

hence x in {(t ^ <*0*>),(t ^ <*1*>)} by A2, TARSKI:def 2; :: thesis: verum

end;assume x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in T } ; :: thesis: x in {(t ^ <*0*>),(t ^ <*1*>)}

then consider n being Nat such that

A2: x = t ^ <*n*> and

A3: t ^ <*n*> in T ;

reconsider tn = t ^ <*n*> as FinSequence of {0,1} by A1, A3, FINSEQ_1:def 11;

(len t) + 1 in Seg ((len t) + 1) by FINSEQ_1:4;

then (len t) + 1 in Seg (len tn) by FINSEQ_2:16;

then (len t) + 1 in dom tn by FINSEQ_1:def 3;

then tn /. ((len t) + 1) = (t ^ <*n*>) . ((len t) + 1) by PARTFUN1:def 6

.= n by FINSEQ_1:42 ;

then ( n = 0 or n = 1 ) by TARSKI:def 2;

hence x in {(t ^ <*0*>),(t ^ <*1*>)} by A2, TARSKI:def 2; :: thesis: verum

A4: t is FinSequence of {0,1} by A1, FINSEQ_1:def 11;

rng <*1*> c= {0,1}

proof

then
<*1*> is FinSequence of {0,1}
by FINSEQ_1:def 4;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng <*1*> or z in {0,1} )

assume z in rng <*1*> ; :: thesis: z in {0,1}

then z in {1} by FINSEQ_1:38;

then z = 1 by TARSKI:def 1;

hence z in {0,1} by TARSKI:def 2; :: thesis: verum

end;assume z in rng <*1*> ; :: thesis: z in {0,1}

then z in {1} by FINSEQ_1:38;

then z = 1 by TARSKI:def 1;

hence z in {0,1} by TARSKI:def 2; :: thesis: verum

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*>)} ; :: thesis: 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}

proof

then
<*0*> is FinSequence of {0,1}
by FINSEQ_1:def 4;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng <*0*> or z in {0,1} )

assume z in rng <*0*> ; :: thesis: z in {0,1}

then z in {0} by FINSEQ_1:38;

then z = 0 by TARSKI:def 1;

hence z in {0,1} by TARSKI:def 2; :: thesis: verum

end;assume z in rng <*0*> ; :: thesis: z in {0,1}

then z in {0} by FINSEQ_1:38;

then z = 0 by TARSKI:def 1;

hence z in {0,1} by TARSKI:def 2; :: thesis: verum

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; :: thesis: verum