let T be Tree; :: thesis: ( T = {0,1} * implies 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*>)}
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*>)}
proof
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 }
proof
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;
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 } )
A4: t is FinSequence of {0,1} by A1, FINSEQ_1:def 11;
rng <*1*> c= {0,1}
proof
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;
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*>)} ; :: 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
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;
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; :: thesis: verum
end;
hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by TREES_2:def 5; :: thesis: verum
end;
hence T is binary by BINTREE1:def 2; :: thesis: verum