let T be binary Tree; :: thesis: for t being Element of T holds t is FinSequence of BOOLEAN

let t be Element of T; :: thesis: t is FinSequence of BOOLEAN

defpred S_{1}[ FinSequence] means ( $1 is Element of T implies rng $1 c= BOOLEAN );

A1: for p being FinSequence of NAT

for x being Element of NAT st S_{1}[p] holds

S_{1}[p ^ <*x*>]
_{1}[ <*> NAT]
by XBOOLE_1:2;

for p being FinSequence of NAT holds S_{1}[p]
from FINSEQ_2:sch 2(A7, A1);

then rng t c= BOOLEAN ;

hence t is FinSequence of BOOLEAN by FINSEQ_1:def 4; :: thesis: verum

let t be Element of T; :: thesis: t is FinSequence of BOOLEAN

defpred S

A1: for p being FinSequence of NAT

for x being Element of NAT st S

S

proof

A7:
S
let p be FinSequence of NAT ; :: thesis: for x being Element of NAT st S_{1}[p] holds

S_{1}[p ^ <*x*>]

let x be Element of NAT ; :: thesis: ( S_{1}[p] implies S_{1}[p ^ <*x*>] )

assume A2: S_{1}[p]
; :: thesis: S_{1}[p ^ <*x*>]

assume A3: p ^ <*x*> is Element of T ; :: thesis: rng (p ^ <*x*>) c= BOOLEAN

then reconsider p1 = p as Element of T by TREES_1:21;

p ^ <*x*> in { (p ^ <*n*>) where n is Nat : p ^ <*n*> in T } by A3;

then A4: p ^ <*x*> in succ p1 by TREES_2:def 5;

then not p in Leaves T by BINTREE1:3;

then succ p1 = {(p ^ <*0*>),(p ^ <*1*>)} by BINTREE1:def 2;

then ( p ^ <*x*> = p ^ <*0*> or p ^ <*x*> = p ^ <*1*> ) by A4, TARSKI:def 2;

then ( x = 0 or x = 1 ) by FINSEQ_2:17;

then A5: x in {0,1} by TARSKI:def 2;

A6: {x} c= BOOLEAN by A5, TARSKI:def 1;

rng <*x*> = {x} by FINSEQ_1:38;

then (rng p) \/ (rng <*x*>) c= BOOLEAN by A2, A3, A6, TREES_1:21, XBOOLE_1:8;

hence rng (p ^ <*x*>) c= BOOLEAN by FINSEQ_1:31; :: thesis: verum

end;S

let x be Element of NAT ; :: thesis: ( S

assume A2: S

assume A3: p ^ <*x*> is Element of T ; :: thesis: rng (p ^ <*x*>) c= BOOLEAN

then reconsider p1 = p as Element of T by TREES_1:21;

p ^ <*x*> in { (p ^ <*n*>) where n is Nat : p ^ <*n*> in T } by A3;

then A4: p ^ <*x*> in succ p1 by TREES_2:def 5;

then not p in Leaves T by BINTREE1:3;

then succ p1 = {(p ^ <*0*>),(p ^ <*1*>)} by BINTREE1:def 2;

then ( p ^ <*x*> = p ^ <*0*> or p ^ <*x*> = p ^ <*1*> ) by A4, TARSKI:def 2;

then ( x = 0 or x = 1 ) by FINSEQ_2:17;

then A5: x in {0,1} by TARSKI:def 2;

A6: {x} c= BOOLEAN by A5, TARSKI:def 1;

rng <*x*> = {x} by FINSEQ_1:38;

then (rng p) \/ (rng <*x*>) c= BOOLEAN by A2, A3, A6, TREES_1:21, XBOOLE_1:8;

hence rng (p ^ <*x*>) c= BOOLEAN by FINSEQ_1:31; :: thesis: verum

for p being FinSequence of NAT holds S

then rng t c= BOOLEAN ;

hence t is FinSequence of BOOLEAN by FINSEQ_1:def 4; :: thesis: verum